diff --git a/lib-bin/libz3.so b/lib-bin/libz3.so
index a6ea716dd3c70164f2308536703537ae61663166..694ad9d01ee9b32055f9d5384b6c7ff9594eb030 100755
Binary files a/lib-bin/libz3.so and b/lib-bin/libz3.so differ
diff --git a/lib/z3.jar b/lib/z3.jar
index e40a8c348760944735605957c8a5d45f5dada7db..de54f24a71c5bab3e7fb506c76eecf4e5a9ae642 100644
Binary files a/lib/z3.jar and b/lib/z3.jar differ
diff --git a/src/funcheck/FunCheckPlugin.scala b/src/funcheck/FunCheckPlugin.scala
index 2ec1ba007071e67b47509f7a19eb787757de9495..826e99d2d18678fb61728961e69813b7024b206c 100644
--- a/src/funcheck/FunCheckPlugin.scala
+++ b/src/funcheck/FunCheckPlugin.scala
@@ -26,6 +26,7 @@ class FunCheckPlugin(val global: Global) extends Plugin {
" -P:funcheck:unrolling=[0,1,2] Unrolling depth for recursive functions" + "\n" +
" -P:funcheck:axioms Generate simple forall axioms for recursive functions when possible" + "\n" +
" -P:funcheck:tolerant Silently extracts non-pure function bodies as ''unknown''" + "\n" +
+ " -P:funcheck:nobapa Disable BAPA Z3 extension" + "\n" +
" -P:funcheck:quiet No info and warning messages from the extensions" + "\n" +
" -P:funcheck:XP Enable weird transformations and other bug-producing features"
)
@@ -42,6 +43,7 @@ class FunCheckPlugin(val global: Global) extends Plugin {
case "quiet" => purescala.Settings.quietExtensions = true
case "nodefaults" => purescala.Settings.runDefaultExtensions = false
case "axioms" => purescala.Settings.noForallAxioms = false
+ case "nobapa" => purescala.Settings.useBAPA = false
case "XP" => purescala.Settings.experimental = true
case s if s.startsWith("unrolling=") => purescala.Settings.unrollingLevel = try { s.substring("unrolling=".length, s.length).toInt } catch { case _ => 0 }
case s if s.startsWith("functions=") => purescala.Settings.functionsToAnalyse = Set(splitList(s.substring("functions=".length, s.length)): _*)
diff --git a/src/purescala/Analysis.scala b/src/purescala/Analysis.scala
index 6a88eb3b64837cc9e62e1d1b12c3bf26fce959f2..4f2f8778fe8aa7bcdbd02fc6cb08b88dbee0f8e6 100644
--- a/src/purescala/Analysis.scala
+++ b/src/purescala/Analysis.scala
@@ -35,7 +35,7 @@ class Analysis(val program: Program) {
def checkVerificationConditions : Unit = {
// just for the summary:
- var verifiedVCs: List[(String,String,String,String)] = Nil
+ var verifiedVCs: List[(String,String,String,String,String)] = Nil
var analysedFunctions: MutableSet[String] = MutableSet.empty
solverExtensions.foreach(_.setProgram(program))
@@ -45,14 +45,14 @@ class Analysis(val program: Program) {
if(funDef.body.isDefined) {
val vc = postconditionVC(funDef)
if(vc == BooleanLiteral(false)) {
- verifiedVCs = (funDef.id.toString, "postcondition", "invalid", "trivial") :: verifiedVCs
+ verifiedVCs = (funDef.id.toString, "postcondition", "invalid", "trivial", "--") :: verifiedVCs
} else if(vc == BooleanLiteral(true)) {
if(funDef.hasPostcondition) {
- verifiedVCs = (funDef.id.toString, "postcondition", "valid", "tautology") :: verifiedVCs
+ verifiedVCs = (funDef.id.toString, "postcondition", "valid", "tautology", "--") :: verifiedVCs
}
} else {
reporter.info("Verification condition (post) for ==== " + funDef.id + " ====")
- if(Settings.unrollingLevel == 0) {
+ if(true || Settings.unrollingLevel == 0) {
reporter.info(simplifyLets(vc))
} else {
reporter.info("(not showing unrolled VCs)")
@@ -72,16 +72,22 @@ class Analysis(val program: Program) {
false
} else {
superseeded = superseeded ++ Set(se.superseeds: _*)
- se.solve(vc) match {
+
+ val t1 = System.nanoTime
+ val solverResult = se.solve(vc)
+ val t2 = System.nanoTime
+ val dt = ((t2 - t1) / 1000000) / 1000.0
+
+ solverResult match {
case None => false
case Some(true) => {
reporter.info("==== VALID ====")
- verifiedVCs = (funDef.id.toString, "postcondition", "valid", se.shortDescription) :: verifiedVCs
+ verifiedVCs = (funDef.id.toString, "postcondition", "valid", se.shortDescription, dt + "s.") :: verifiedVCs
true
}
case Some(false) => {
reporter.error("==== INVALID ====")
- verifiedVCs = (funDef.id.toString, "postcondition", "invalid", se.shortDescription) :: verifiedVCs
+ verifiedVCs = (funDef.id.toString, "postcondition", "invalid", se.shortDescription, dt + "s.") :: verifiedVCs
true
}
}
@@ -89,7 +95,7 @@ class Analysis(val program: Program) {
}) match {
case None => {
reporter.warning("No solver could prove or disprove the verification condition.")
- verifiedVCs = (funDef.id.toString, "postcondition", "unknown", "---") :: verifiedVCs
+ verifiedVCs = (funDef.id.toString, "postcondition", "unknown", "--", "--") :: verifiedVCs
}
case _ =>
}
@@ -97,7 +103,7 @@ class Analysis(val program: Program) {
} else {
if(funDef.postcondition.isDefined) {
reporter.warning(funDef, "Could not verify postcondition: function implementation is unknown.")
- verifiedVCs = (funDef.id.toString, "postcondition", "unknown", "no body") :: verifiedVCs
+ verifiedVCs = (funDef.id.toString, "postcondition", "unknown", "no body", "--") :: verifiedVCs
}
}
}
@@ -107,14 +113,16 @@ class Analysis(val program: Program) {
val col1wdth = verifiedVCs.map(_._1).map(_.length).max + 2
val col2wdth = verifiedVCs.map(_._2).map(_.length).max + 2
val col3wdth = verifiedVCs.map(_._3).map(_.length).max + 2
- val col4wdth = verifiedVCs.map(_._4).map(_.length).max
- def mk1line(line: (String,String,String,String)) : String = {
+ val col4wdth = verifiedVCs.map(_._4).map(_.length).max + 2
+ val col5wdth = verifiedVCs.map(_._5).map(_.length).max
+ def mk1line(line: (String,String,String,String,String)) : String = {
line._1 + (" " * (col1wdth - line._1.length)) +
line._2 + (" " * (col2wdth - line._2.length)) +
line._3 + (" " * (col3wdth - line._3.length)) +
- line._4
+ line._4 + (" " * (col4wdth - line._4.length)) +
+ line._5
}
- val dashes : String = "=" * (col1wdth + col2wdth + col3wdth + col4wdth)
+ val dashes : String = "=" * (col1wdth + col2wdth + col3wdth + col4wdth + col5wdth)
reporter.info("Summary:\n" + dashes + "\n" + verifiedVCs.sortWith(_._1 < _._1).map(mk1line(_)).mkString("\n") + "\n" + dashes)
} else {
reporter.info("No verification conditions were generated.")
@@ -187,11 +195,25 @@ class Analysis(val program: Program) {
}
object Analysis {
+ private val keepCallWhenInlined: Boolean = true
+
+ private def defineOneInlining(f : FunctionInvocation) : (Expr, Expr) = {
+ val FunctionInvocation(fd, args) = f
+ val newLetIDs = fd.args.map(a => FreshIdentifier("arg_" + a.id.name, true).setType(a.tpe)).toList
+ val substMap = Map[Expr,Expr]((fd.args.map(_.toVariable) zip newLetIDs.map(Variable(_))) : _*)
+ val newBody = replace(substMap, freshenLocals(fd.body.get))
+ val newFunctionCall = FunctionInvocation(fd, newLetIDs.map(Variable(_))).setType(f.getType)
+ val callID = FreshIdentifier("call_" + fd.id.name, true).setType(newBody.getType)
+ val callTree = Let(callID, (newLetIDs zip args).foldRight(newBody)((iap, e) => Let(iap._1, iap._2, e)), Variable(callID))
+
+ (Equals(newFunctionCall, Variable(callID)), callTree)
+ }
+
private def inlineFunctionCall(f : FunctionInvocation) : Expr = {
val FunctionInvocation(fd, args) = f
val newLetIDs = fd.args.map(a => FreshIdentifier("arg_" + a.id.name, true).setType(a.tpe)).toList
val substMap = Map[Expr,Expr]((fd.args.map(_.toVariable) zip newLetIDs.map(Variable(_))) : _*)
- val newBody = replace(substMap, fd.body.get)
+ val newBody = replace(substMap, freshenLocals(fd.body.get))
simplifyLets((newLetIDs zip args).foldRight(newBody)((iap, e) => Let(iap._1, iap._2, e)))
}
@@ -200,7 +222,7 @@ object Analysis {
case f @ FunctionInvocation(fd, args) if fd.hasImplementation && !program.isRecursive(fd) => Some(inlineFunctionCall(f))
case _ => None
}
-
+
var change: Boolean = true
var toReturn: Expr = expression
while(change) {
@@ -212,21 +234,52 @@ object Analysis {
}
def unrollRecursiveFunctions(program: Program, expression: Expr, times: Int) : Expr = {
- def applyToCall(e: Expr) : Option[Expr] = e match {
- case f @ FunctionInvocation(fd, args) if fd.hasImplementation && program.isRecursive(fd) => Some(inlineFunctionCall(f))
- case _ => None
+ def urf1(expression: Expr, times: Int) : Expr = {
+ var newEqs: List[Expr] = Nil
+
+ def applyToCall(e: Expr) : Option[Expr] = e match {
+ case f @ FunctionInvocation(fd, args) if fd.hasImplementation && program.isRecursive(fd) => {
+ val (newEq, bdy) = defineOneInlining(f)
+ newEqs = newEq :: newEqs
+ Some(bdy)
+ }
+ case _ => None
+ }
+
+ var remaining = if(times < 0) 0 else times
+ var change: Boolean = true
+ var toReturn: Expr = expression
+ while(remaining > 0 && change) {
+ val (t,c) = searchAndReplaceDFSandTrackChanges(applyToCall)(toReturn)
+ change = c
+ toReturn = inlineNonRecursiveFunctions(program, t)
+ remaining = remaining - 1
+ }
+ liftLets(Implies(And(newEqs.reverse), toReturn))
}
- var remaining = if(times < 0) 0 else times
- var change: Boolean = true
- var toReturn: Expr = expression
- while(remaining > 0 && change) {
- val (t,c) = searchAndReplaceDFSandTrackChanges(applyToCall)(toReturn)
- change = c
- toReturn = inlineNonRecursiveFunctions(program, t)
- remaining = remaining - 1
+ def urf2(expression: Expr, times: Int) : Expr = {
+ def applyToCall(e: Expr) : Option[Expr] = e match {
+ case f @ FunctionInvocation(fd, args) if fd.hasImplementation && program.isRecursive(fd) => Some(inlineFunctionCall(f))
+ case _ => None
+ }
+
+ var remaining = if(times < 0) 0 else times
+ var change: Boolean = true
+ var toReturn: Expr = expression
+ while(remaining > 0 && change) {
+ val (t,c) = searchAndReplaceDFSandTrackChanges(applyToCall)(toReturn)
+ change = c
+ toReturn = inlineNonRecursiveFunctions(program, t)
+ remaining = remaining - 1
+ }
+ toReturn
}
- toReturn
+
+ if(keepCallWhenInlined)
+ urf1(expression, times)
+ else
+ urf2(expression, times)
}
def inlineContracts(expression: Expr) : Expr = {
@@ -241,7 +294,7 @@ object Analysis {
val substMap = Map[Expr,Expr]((fd.args.map(_.toVariable) zip argsAsLetVars) : _*) + (ResultVariable() -> Variable(resultAsLet))
// this thing is full of let variables! We will need to lift the let
// defs. later to make sure they capture this
- val trueFact = replace(substMap, fd.postcondition.get)
+ val trueFact = replace(substMap, freshenLocals(fd.postcondition.get))
val defList: Seq[(Identifier,Expr)] = ((argsAsLet :+ resultAsLet) zip (args :+ newFunCall))
trueThings = trueFact :: trueThings
// again: these let defs. need eventually to capture the "true thing"
diff --git a/src/purescala/Settings.scala b/src/purescala/Settings.scala
index 9dda6e21ae36f680344d23266b002a3b9f837015..8be325547994522268aee17396920a8cb74963cb 100644
--- a/src/purescala/Settings.scala
+++ b/src/purescala/Settings.scala
@@ -12,4 +12,5 @@ object Settings {
var runDefaultExtensions: Boolean = true
var noForallAxioms: Boolean = true
var unrollingLevel: Int = 0
+ var useBAPA: Boolean = true
}
diff --git a/src/purescala/Trees.scala b/src/purescala/Trees.scala
index cafc43db50c49ca75a8e517c37f49bd819778376..f15671b320786af27fb173d7c32d036b56762011 100644
--- a/src/purescala/Trees.scala
+++ b/src/purescala/Trees.scala
@@ -64,9 +64,19 @@ object Trees {
def expressions = List(guard, rhs)
}
- sealed abstract class Pattern
- case class InstanceOfPattern(binder: Option[Identifier], classTypeDef: ClassTypeDef) extends Pattern // c: Class
- case class WildcardPattern(binder: Option[Identifier]) extends Pattern // c @ _
+ sealed abstract class Pattern {
+ val subPatterns: Seq[Pattern]
+ val binder: Option[Identifier]
+
+ private def subBinders = subPatterns.map(_.binders).foldLeft[Set[Identifier]](Set.empty)(_ ++ _)
+ def binders: Set[Identifier] = subBinders ++ (if(binder.isDefined) Set(binder.get) else Set.empty)
+ }
+ case class InstanceOfPattern(binder: Option[Identifier], classTypeDef: ClassTypeDef) extends Pattern { // c: Class
+ val subPatterns = Seq.empty
+ }
+ case class WildcardPattern(binder: Option[Identifier]) extends Pattern { // c @ _
+ val subPatterns = Seq.empty
+ }
case class CaseClassPattern(binder: Option[Identifier], caseClassDef: CaseClassDef, subPatterns: Seq[Pattern]) extends Pattern
// case class ExtractorPattern(binder: Option[Identifier],
// extractor : ExtractorTypeDef,
@@ -561,6 +571,38 @@ object Trees {
(res, somethingChanged)
}
+ // rewrites pattern-matching expressions to use fresh variables for the binders
+ def freshenLocals(expr: Expr) : Expr = {
+ def rewritePattern(p: Pattern, sm: Map[Identifier,Identifier]) : Pattern = p match {
+ case InstanceOfPattern(Some(b), ctd) => InstanceOfPattern(Some(sm(b)), ctd)
+ case WildcardPattern(Some(b)) => WildcardPattern(Some(sm(b)))
+ case CaseClassPattern(ob, ccd, sps) => CaseClassPattern(ob.map(sm(_)), ccd, sps.map(rewritePattern(_, sm)))
+ case other => other
+ }
+
+ def freshenCase(cse: MatchCase) : MatchCase = {
+ val allBinders: Set[Identifier] = cse.pattern.binders
+ val subMap: Map[Identifier,Identifier] = Map(allBinders.map(i => (i, FreshIdentifier(i.name, true).setType(i.getType))).toSeq : _*)
+ val subVarMap: Map[Expr,Expr] = subMap.map(kv => (Variable(kv._1) -> Variable(kv._2)))
+
+ cse match {
+ case SimpleCase(pattern, rhs) => SimpleCase(rewritePattern(pattern, subMap), replace(subVarMap, rhs))
+ case GuardedCase(pattern, guard, rhs) => GuardedCase(rewritePattern(pattern, subMap), replace(subVarMap, guard), replace(subVarMap, rhs))
+ }
+ }
+
+ def applyToTree(e : Expr) : Option[Expr] = e match {
+ case m @ MatchExpr(s, cses) => Some(MatchExpr(s, cses.map(freshenCase(_))).setType(m.getType))
+ case l @ Let(i,e,b) => {
+ val newID = FreshIdentifier(i.name, true).setType(i.getType)
+ Some(Let(newID, e, replace(Map(Variable(i) -> Variable(newID)), b)))
+ }
+ case _ => None
+ }
+
+ searchAndReplaceDFS(applyToTree)(expr)
+ }
+
// convert describes how to compute a value for the leaves (that includes
// functions with no args.)
// combine descriess how to combine two values
diff --git a/src/purescala/Z3Solver.scala b/src/purescala/Z3Solver.scala
index cb16c5cfcbea22eb1cea679004e5a432d142306a..418bb1f20f6eb04a7d53683dcb94b8d82ce7a664 100644
--- a/src/purescala/Z3Solver.scala
+++ b/src/purescala/Z3Solver.scala
@@ -10,6 +10,7 @@ import TypeTrees._
import z3plugins.bapa.BAPATheory
class Z3Solver(reporter: Reporter) extends Solver(reporter) {
+ import Settings.useBAPA
val description = "Z3 Solver"
override val shortDescription = "Z3"
@@ -45,7 +46,8 @@ class Z3Solver(reporter: Reporter) extends Solver(reporter) {
z3.delete
}
z3 = new Z3Context(z3cfg)
- bapa = new BAPATheory(z3)
+ // z3.traceToStdout
+ if(useBAPA) bapa = new BAPATheory(z3)
counter = 0
prepareSorts
prepareFunctions
@@ -244,7 +246,7 @@ class Z3Solver(reporter: Reporter) extends Solver(reporter) {
adtSorts(cd)
}
}
- case IntSetType => bapa.mkSetSort
+ case IntSetType if(useBAPA) => bapa.mkSetSort
case SetType(base) => setSorts.get(base) match {
case Some(s) => s
case None => {
@@ -372,41 +374,41 @@ class Z3Solver(reporter: Reporter) extends Solver(reporter) {
abstractedFormula = true
z3.mkApp(functionDefToDef(fd), args.map(rec(_)): _*)
}
- case e @ EmptySet(_) => if(e.getType == IntSetType) {
+ case e @ EmptySet(_) => if(useBAPA && e.getType == IntSetType) {
bapa.mkEmptySet
} else {
z3.mkEmptySet(typeToSort(e.getType.asInstanceOf[SetType].base))
}
case SetEquals(s1,s2) => z3.mkEq(rec(s1), rec(s2))
- case ElementOfSet(e, s) if s.getType == IntSetType => {
+ case ElementOfSet(e, s) if(useBAPA && s.getType == IntSetType) => {
bapa.mkElementOf(rec(e), rec(s))
}
- case SubsetOf(s1,s2) => if(s1.getType == IntSetType) {
+ case SubsetOf(s1,s2) => if(useBAPA && s1.getType == IntSetType) {
bapa.mkSubsetEq(rec(s1), rec(s2))
} else {
z3.mkSetSubset(rec(s1), rec(s2))
}
- case SetIntersection(s1,s2) => if(s1.getType == IntSetType) {
+ case SetIntersection(s1,s2) => if(useBAPA && s1.getType == IntSetType) {
bapa.mkIntersect(rec(s1), rec(s2))
} else {
z3.mkSetIntersect(rec(s1), rec(s2))
}
- case SetUnion(s1,s2) => if(s1.getType == IntSetType) {
+ case SetUnion(s1,s2) => if(useBAPA && s1.getType == IntSetType) {
bapa.mkUnion(rec(s1), rec(s2))
} else {
z3.mkSetUnion(rec(s1), rec(s2))
}
- case SetDifference(s1,s2) => if(s1.getType == IntSetType) {
+ case SetDifference(s1,s2) => if(useBAPA && s1.getType == IntSetType) {
bapa.mkIntersect(rec(s1), bapa.mkComplement(rec(s2)))
} else {
z3.mkSetDifference(rec(s1), rec(s2))
}
- case f @ FiniteSet(elems) => if(f.getType == IntSetType) {
+ case f @ FiniteSet(elems) => if(useBAPA && f.getType == IntSetType) {
elems.map(e => bapa.mkSingleton(rec(e))).reduceLeft(bapa.mkUnion(_,_))
} else {
elems.foldLeft(z3.mkEmptySet(typeToSort(f.getType.asInstanceOf[SetType].base)))((ast,el) => z3.mkSetAdd(ast,rec(el)))
}
- case SetCardinality(s) if s.getType == IntSetType => {
+ case SetCardinality(s) if (useBAPA && s.getType == IntSetType) => {
bapa.mkCard(rec(s))
}
case _ => {
diff --git a/vmcai2011-testcases/ListProperties.scala b/vmcai2011-testcases/ListProperties.scala
new file mode 100644
index 0000000000000000000000000000000000000000..c884ed883e1d6c3f5f63cc729ca5e2c1915d3f19
--- /dev/null
+++ b/vmcai2011-testcases/ListProperties.scala
@@ -0,0 +1,44 @@
+import scala.collection.immutable.Set
+
+object IntListProperties {
+ sealed abstract class IntList
+ case class Cons(head: Int, tail: IntList) extends IntList
+ case class Nil() extends IntList
+
+ def size(list: IntList) : Int = (list match {
+ case Nil() => 0
+ case Cons(_, xs) => 1 + size(xs)
+ }) ensuring(_ >= 0)
+
+ def content(list: IntList) : Set[Int] = (list match {
+ case Nil() => Set.empty[Int]
+ case Cons(x, xs) => Set(x) ++ content(xs)
+ }) //ensuring(_.size <= size(list))
+
+ def removeDuplicates(list: IntList) : IntList = (list match {
+ case Nil() => Nil()
+ case Cons(x, xs) => Cons(x, removeDuplicates(removeFrom(x, xs)))
+ }) ensuring(newList => content(newList) == content(list))
+ def removeFrom(v: Int, list: IntList) : IntList = (list match {
+ case Nil() => Nil()
+ case Cons(x, xs) => {
+ val rest = removeFrom(v, xs)
+ if(v == x) rest else Cons(x, rest)
+ }
+ }) ensuring(newList => content(newList) == content(list) -- Set(v))
+
+// def reverse(list: IntList) : IntList = reverse0(list, Nil())
+// def reverse0(list1: IntList, list2: IntList) : IntList = list1 match {
+// case Nil() => list2
+// case Cons(x, xs) => reverse0(xs, Cons(x, list2))
+// }
+//
+// def concat(list1: IntList, list2: IntList) : IntList = concat0(list1, list2, Nil())
+// def concat0(list1: IntList, list2: IntList, list3: IntList) : IntList = list1 match {
+// case Nil() => list2 match {
+// case Nil() => reverse(list3)
+// case Cons(y, ys) => concat0(Nil(), ys, Cons(y, list3))
+// }
+// case Cons(x, xs) => concat0(xs, list2, Cons(x, list3))
+// }
+}