From 1eaf909d3ed3ef47f0304ee6c1be2b221e4c4b1c Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Thu, 2 Jun 2011 16:46:49 +0200
Subject: [PATCH] Support for --BV flag to use bit-vectors instead of
mathematical ints.
---
src/funcheck/FunCheckPlugin.scala | 6 ++++--
src/purescala/FairZ3Solver.scala | 34 ++++++++++++++++++++-----------
src/purescala/Settings.scala | 2 ++
3 files changed, 28 insertions(+), 14 deletions(-)
diff --git a/src/funcheck/FunCheckPlugin.scala b/src/funcheck/FunCheckPlugin.scala
index c11533467..c5bcb8d9c 100644
--- a/src/funcheck/FunCheckPlugin.scala
+++ b/src/funcheck/FunCheckPlugin.scala
@@ -33,6 +33,7 @@ class FunCheckPlugin(val global: Global, val actionAfterExtraction : Option[Prog
" -P:funcheck:testbounds=l:u Lower and upper bounds for integers in recursive datatypes" + "\n" +
" -P:funcheck:timeout=N Sets a timeout of N seconds" + "\n" +
" -P:funcheck:XP Enable weird transformations and other bug-producing features" + "\n" +
+ " -P:funcheck:BV Use bit-vectors for integers" + "\n" +
" -P:funcheck:prune Use additional SMT queries to rule out some unrollings" + "\n" +
" -P:funcheck:cores Use UNSAT cores in the unrolling/refinement step" + "\n" +
" -P:funcheck:quickcheck Use QuickCheck-like random search in parrallel with Z3" + "\n" +
@@ -53,8 +54,9 @@ class FunCheckPlugin(val global: Global, val actionAfterExtraction : Option[Prog
case "bapa" => purescala.Settings.useBAPA = true
case "impure" => purescala.Settings.impureTestcases = true
case "XP" => purescala.Settings.experimental = true
- case "prune" => purescala.Settings.pruneBranches = true
- case "cores" => purescala.Settings.useCores = true
+ case "BV" => purescala.Settings.bitvectorBitwidth = Some(32)
+ case "prune" => purescala.Settings.pruneBranches = true
+ case "cores" => purescala.Settings.useCores = true
case "quickcheck" => purescala.Settings.useQuickCheck = true
case "noLuckyTests" => purescala.Settings.luckyTest = false
case s if s.startsWith("unrolling=") => purescala.Settings.unrollingLevel = try { s.substring("unrolling=".length, s.length).toInt } catch { case _ => 0 }
diff --git a/src/purescala/FairZ3Solver.scala b/src/purescala/FairZ3Solver.scala
index 28e78b837..e3a4002ae 100644
--- a/src/purescala/FairZ3Solver.scala
+++ b/src/purescala/FairZ3Solver.scala
@@ -15,6 +15,8 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
// assert(Settings.useFairInstantiator)
private final val UNKNOWNASSAT : Boolean = !Settings.noForallAxioms
+ private final val USEBV : Boolean = Settings.bitvectorBitwidth.isDefined
+ private final val BVWIDTH : Int = Settings.bitvectorBitwidth.getOrElse(-1)
val description = "Fair Z3 Solver"
override val shortDescription = "Z3-f"
@@ -121,7 +123,11 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
case Some(z3sort) => z3sort
case None => {
import Z3Context.{ADTSortReference, RecursiveType, RegularSort}
- intSort = z3.mkIntSort
+ intSort = if(USEBV) {
+ z3.mkBVSort(BVWIDTH)
+ } else {
+ z3.mkIntSort
+ }
boolSort = z3.mkBoolSort
def typeToSortRef(tt: TypeTree): ADTSortReference = tt match {
@@ -163,7 +169,11 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
import Z3Context.{ADTSortReference, RecursiveType, RegularSort}
// NOTE THAT abstract classes that extend abstract classes are not
// currently supported in the translation
- intSort = z3.mkIntSort
+ intSort = if(USEBV) {
+ z3.mkBVSort(BVWIDTH)
+ } else {
+ z3.mkIntSort
+ }
boolSort = z3.mkBoolSort
setSorts = Map.empty
setCardFuns = Map.empty
@@ -349,7 +359,7 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
case None => {
val newSetSort = z3.mkSetSort(typeToSort(base))
setSorts = setSorts + (base -> newSetSort)
- val newCardFun = z3.mkFreshFuncDecl("card", Seq(newSetSort), z3.mkIntSort)
+ val newCardFun = z3.mkFreshFuncDecl("card", Seq(newSetSort), intSort)
setCardFuns = setCardFuns + (base -> newCardFun)
newSetSort
}
@@ -859,15 +869,15 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
case IntLiteral(v) => z3.mkInt(v, intSort)
case BooleanLiteral(v) => if (v) z3.mkTrue() else z3.mkFalse()
case Equals(l, r) => z3.mkEq(rec(l), rec(r))
- case Plus(l, r) => z3.mkAdd(rec(l), rec(r))
- case Minus(l, r) => z3.mkSub(rec(l), rec(r))
- case Times(l, r) => z3.mkMul(rec(l), rec(r))
- case Division(l, r) => z3.mkDiv(rec(l), rec(r))
- case UMinus(e) => z3.mkUnaryMinus(rec(e))
- case LessThan(l, r) => z3.mkLT(rec(l), rec(r))
- case LessEquals(l, r) => z3.mkLE(rec(l), rec(r))
- case GreaterThan(l, r) => z3.mkGT(rec(l), rec(r))
- case GreaterEquals(l, r) => z3.mkGE(rec(l), rec(r))
+ case Plus(l, r) => if(USEBV) z3.mkBVAdd(rec(l), rec(r)) else z3.mkAdd(rec(l), rec(r))
+ case Minus(l, r) => if(USEBV) z3.mkBVSub(rec(l), rec(r)) else z3.mkSub(rec(l), rec(r))
+ case Times(l, r) => if(USEBV) z3.mkBVMul(rec(l), rec(r)) else z3.mkMul(rec(l), rec(r))
+ case Division(l, r) => if(USEBV) z3.mkBVSdiv(rec(l), rec(r)) else z3.mkDiv(rec(l), rec(r))
+ case UMinus(e) => if(USEBV) z3.mkBVNeg(rec(e)) else z3.mkUnaryMinus(rec(e))
+ case LessThan(l, r) => if(USEBV) z3.mkBVSlt(rec(l), rec(r)) else z3.mkLT(rec(l), rec(r))
+ case LessEquals(l, r) => if(USEBV) z3.mkBVSle(rec(l), rec(r)) else z3.mkLE(rec(l), rec(r))
+ case GreaterThan(l, r) => if(USEBV) z3.mkBVSgt(rec(l), rec(r)) else z3.mkGT(rec(l), rec(r))
+ case GreaterEquals(l, r) => if(USEBV) z3.mkBVSge(rec(l), rec(r)) else z3.mkGE(rec(l), rec(r))
case c@CaseClass(cd, args) => {
val constructor = adtConstructors(cd)
constructor(args.map(rec(_)): _*)
diff --git a/src/purescala/Settings.scala b/src/purescala/Settings.scala
index b369a6387..651a13c26 100644
--- a/src/purescala/Settings.scala
+++ b/src/purescala/Settings.scala
@@ -23,4 +23,6 @@ object Settings {
var solverTimeout : Option[Int] = None
var luckyTest : Boolean = true
var useQuickCheck : Boolean = false
+ // When this is None, use real integers
+ var bitvectorBitwidth : Option[Int] = None
}
--
GitLab