diff --git a/src/funcheck/AnalysisComponent.scala b/src/funcheck/AnalysisComponent.scala
index 1b0c267047989130dd1c53ddb983eb87908f471f..30d73b01546d1344b0b0a16c909f751bcd2287df 100644
--- a/src/funcheck/AnalysisComponent.scala
+++ b/src/funcheck/AnalysisComponent.scala
@@ -39,8 +39,8 @@ class AnalysisComponent(val global: Global, val pluginInstance: FunCheckPlugin)
println("Extraction complete. Now terminating the compiler process.")
exit(0)
} else {
- println("Extracted program for " + unit + ": ")
- println(prog)
+ println("Extracted program for " + unit + ". Re-run with -P:funcheck:parse to see the output.")
+ //println(prog)
}
println("Starting analysis.")
diff --git a/src/funcheck/CodeExtraction.scala b/src/funcheck/CodeExtraction.scala
index c76e1ca7fac947785e0b2fd076a088b918190e2a..23562e7740363a7c79d76e7ee0ccb575332d3d73 100644
--- a/src/funcheck/CodeExtraction.scala
+++ b/src/funcheck/CodeExtraction.scala
@@ -156,7 +156,7 @@ trait CodeExtraction extends Extractors {
case ExMainFunctionDef() => ;
case dd @ ExFunctionDef(n,p,t,b) => {
val mods = dd.mods
- val funDef = extractFunSig(n, p, t)
+ val funDef = extractFunSig(n, p, t).setPosInfo(dd.pos.line, dd.pos.column)
if(mods.isPrivate) funDef.addAnnotation("private")
for(a <- dd.symbol.annotations) {
a.atp.safeToString match {
@@ -503,20 +503,20 @@ trait CodeExtraction extends Extractors {
val r3 = rec(t3)
IfExpr(r1, r2, r3).setType(leastUpperBound(r2.getType, r3.getType))
}
- case ExLocalCall(sy,nm,ar) => {
+ case lc @ ExLocalCall(sy,nm,ar) => {
if(defsToDefs.keysIterator.find(_ == sy).isEmpty) {
if(!silent)
unit.error(tr.pos, "Invoking an invalid function.")
throw ImpureCodeEncounteredException(tr)
}
val fd = defsToDefs(sy)
- FunctionInvocation(fd, ar.map(rec(_))).setType(fd.returnType)
+ FunctionInvocation(fd, ar.map(rec(_))).setType(fd.returnType).setPosInfo(lc.pos.line,lc.pos.column)
}
- case ExPatternMatching(sel, cses) => {
+ case pm @ ExPatternMatching(sel, cses) => {
val rs = rec(sel)
val rc = cses.map(rewriteCaseDef(_))
val rt: purescala.TypeTrees.TypeTree = rc.map(_.rhs.getType).reduceLeft(leastUpperBound(_,_))
- MatchExpr(rs, rc).setType(rt)
+ MatchExpr(rs, rc).setType(rt).setPosInfo(pm.pos.line,pm.pos.column)
}
// this one should stay after all others, cause it also catches UMinus
@@ -582,4 +582,8 @@ trait CodeExtraction extends Extractors {
rec(tree)
}
+
+ def mkPosString(pos: scala.tools.nsc.util.Position) : String = {
+ pos.line + "," + pos.column
+ }
}
diff --git a/src/purescala/Analysis.scala b/src/purescala/Analysis.scala
index 4ffa87ea535e4a2c90393b025c8675c96243838e..c29a2b19ee8475f9a2c03850022e5dcd02a5d06d 100644
--- a/src/purescala/Analysis.scala
+++ b/src/purescala/Analysis.scala
@@ -49,7 +49,7 @@ class Analysis(val program: Program) {
var allVCs: Seq[VerificationCondition] = Seq.empty
val analysedFunctions: MutableSet[String] = MutableSet.empty
- for(funDef <- program.definedFunctions.toList.sortWith((fd1, fd2) => fd1.id.name < fd2.id.name) if (Settings.functionsToAnalyse.isEmpty || Settings.functionsToAnalyse.contains(funDef.id.name))) {
+ for(funDef <- program.definedFunctions.toList.sortWith((fd1, fd2) => fd1 < fd2) if (Settings.functionsToAnalyse.isEmpty || Settings.functionsToAnalyse.contains(funDef.id.name))) {
analysedFunctions += funDef.id.name
val tactic: Tactic =
@@ -59,11 +59,13 @@ class Analysis(val program: Program) {
defaultTactic
}
+ def vcSort(vc1: VerificationCondition, vc2: VerificationCondition) : Boolean = (vc1 < vc2)
+
if(funDef.body.isDefined) {
- allVCs ++= tactic.generatePreconditions(funDef)
- allVCs ++= tactic.generatePostconditions(funDef)
- allVCs ++= tactic.generatePatternMatchingExhaustivenessChecks(funDef)
- allVCs ++= tactic.generateMiscCorrectnessConditions(funDef)
+ allVCs ++= tactic.generatePreconditions(funDef).sortWith(vcSort)
+ allVCs ++= tactic.generatePatternMatchingExhaustivenessChecks(funDef).sortWith(vcSort)
+ allVCs ++= tactic.generatePostconditions(funDef).sortWith(vcSort)
+ allVCs ++= tactic.generateMiscCorrectnessConditions(funDef).sortWith(vcSort)
}
}
@@ -79,12 +81,13 @@ class Analysis(val program: Program) {
val funDef = vcInfo.funDef
val vc = vcInfo.condition
- reporter.info("Verification condition (post) for ==== " + funDef.id + " ====")
- if(true || Settings.unrollingLevel == 0) {
- reporter.info(simplifyLets(vc))
- } else {
- reporter.info("(not showing unrolled VCs)")
- }
+ reporter.info("Now considering '" + vcInfo.kind + "' VC for " + funDef.id + "...")
+ // reporter.info("Verification condition (post) for ==== " + funDef.id + " ====")
+ // if(Settings.unrollingLevel == 0) {
+ // reporter.info(simplifyLets(vc))
+ // } else {
+ // reporter.info("(not showing unrolled VCs)")
+ // }
// try all solvers until one returns a meaningful answer
var superseeded : Set[String] = Set.empty[String]
diff --git a/src/purescala/Common.scala b/src/purescala/Common.scala
index 141cb71cca3cf5a8523ad8cb2dea9274b8b9d35c..3c1abef7d9fa2b9173133b32e5283b8c1039ecff 100644
--- a/src/purescala/Common.scala
+++ b/src/purescala/Common.scala
@@ -47,4 +47,33 @@ object Common {
object FreshIdentifier {
def apply(name: String, alwaysShowUniqueID: Boolean = false) : Identifier = new Identifier(name, UniqueCounter.next, alwaysShowUniqueID)
}
+
+ trait ScalacPositional {
+ self =>
+
+ private var prow: Int = -1078
+ private var pcol: Int = -1078
+
+ def setPosInfo(row: Int, col: Int) : self.type = {
+ prow = row
+ pcol = col
+ this
+ }
+
+ def setPosInfo(from: ScalacPositional) : self.type = {
+ val (or,oc) = from.posIntInfo
+ prow = or
+ pcol = oc
+ this
+ }
+
+ def posIntInfo : (Int,Int) = (prow,pcol)
+
+ def posInfo : String = if(prow != -1078) "(" + prow + "," + pcol + ")" else ""
+
+ def <(other: ScalacPositional) : Boolean = {
+ val (orow,ocol) = other.posIntInfo
+ prow < orow || (prow == orow && pcol < ocol)
+ }
+ }
}
diff --git a/src/purescala/DefaultTactic.scala b/src/purescala/DefaultTactic.scala
index cecf3427837916ed70cc8ef675f599d9ebc312b6..b7e586a396495c10d7558fe872f1b7bd7ecbb1fe 100644
--- a/src/purescala/DefaultTactic.scala
+++ b/src/purescala/DefaultTactic.scala
@@ -81,44 +81,77 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
}
}
- private val errConds : MutableMap[FunDef,Seq[VerificationCondition]] = MutableMap.empty
- private def errorConditions(function: FunDef) : Seq[VerificationCondition] = {
- if(errConds.isDefinedAt(function)) {
- errConds(function)
- } else {
- val conds = if(function.hasBody) {
- val bodyToUse = if(function.hasPrecondition) {
- IfExpr(function.precondition.get, function.body.get, Error("XXX").setType(function.returnType)).setType(function.returnType)
- } else {
- function.body.get
- }
- val withExplicit = expandLets(explicitPreconditions(matchToIfThenElse(bodyToUse)))
-
- val allPathConds = collectWithPathCondition((_ match { case Error(_) => true ; case _ => false }), withExplicit)
-
- allPathConds.filter(_._2 != Error("XXX")).map(pc => pc._2 match {
- case Error("precondition violated") => new VerificationCondition(Not(And(pc._1)), function, VCKind.Precondition, this)
- case Error("non-exhaustive match") => new VerificationCondition(Not(And(pc._1)), function, VCKind.ExhaustiveMatch, this)
- case _ => scala.Predef.error("Don't know what to do with this path condition target: " + pc._2)
- }).toSeq
+ def generatePreconditions(function: FunDef) : Seq[VerificationCondition] = {
+ val toRet = if(function.hasBody) {
+ val cleanBody = matchToIfThenElse(function.body.get)
+
+ val allPathConds = collectWithPathCondition((t => t match {
+ case FunctionInvocation(fd, _) if(fd.hasPrecondition) => true
+ case _ => false
+ }), cleanBody)
+
+ def withPrecIfDefined(path: Seq[Expr], shouldHold: Expr) : Expr = if(function.hasPrecondition) {
+ Not(And(And(matchToIfThenElse(function.precondition.get) +: path), Not(shouldHold)))
} else {
- Seq.empty
+ Not(And(And(path), Not(shouldHold)))
}
- errConds(function) = conds
- conds
+
+ allPathConds.map(pc => {
+ val path : Seq[Expr] = pc._1
+ val fi = pc._2.asInstanceOf[FunctionInvocation]
+ val FunctionInvocation(fd, args) = fi
+ val prec : Expr = freshenLocals(matchToIfThenElse(fd.precondition.get))
+ val newLetIDs = fd.args.map(a => FreshIdentifier("arg_" + a.id.name, true).setType(a.tpe))
+ val substMap = Map[Expr,Expr]((fd.args.map(_.toVariable) zip newLetIDs.map(Variable(_))) : _*)
+ val newBody : Expr = replace(substMap, prec)
+ val newCall : Expr = (newLetIDs zip args).foldRight(newBody)((iap, e) => Let(iap._1, iap._2, e))
+
+ new VerificationCondition(
+ withPrecIfDefined(path, newCall),
+ function,
+ VCKind.Precondition,
+ this).setPosInfo(fi)
+ }).toSeq
+ } else {
+ Seq.empty
}
- }
- def generatePreconditions(function: FunDef) : Seq[VerificationCondition] = {
- val toRet = errorConditions(function).filter(_.kind == VCKind.Precondition)
+ // println("PRECS VCs FOR " + function.id.name)
+ // println(toRet.toList.map(vc => vc.posInfo + " -- " + vc.condition).mkString("\n\n"))
- println("PRECONDITIONS FOR " + function.id.name)
- println(toRet.map(_.condition).toList.mkString("\n"))
toRet
}
def generatePatternMatchingExhaustivenessChecks(function: FunDef) : Seq[VerificationCondition] = {
- errorConditions(function).filter(_.kind == VCKind.ExhaustiveMatch)
+ val toRet = if(function.hasBody) {
+ val cleanBody = matchToIfThenElse(function.body.get)
+
+ val allPathConds = collectWithPathCondition((t => t match {
+ case Error("non-exhaustive match") => true
+ case _ => false
+ }), cleanBody)
+
+ def withPrecIfDefined(conds: Seq[Expr]) : Expr = if(function.hasPrecondition) {
+ Not(And(matchToIfThenElse(function.precondition.get), And(conds)))
+ } else {
+ Not(And(conds))
+ }
+
+ allPathConds.map(pc =>
+ new VerificationCondition(
+ withPrecIfDefined(pc._1),
+ function,
+ VCKind.ExhaustiveMatch,
+ this).setPosInfo(pc._2.asInstanceOf[Error])
+ ).toSeq
+ } else {
+ Seq.empty
+ }
+
+ // println("MATCHING VCs FOR " + function.id.name)
+ // println(toRet.toList.map(vc => vc.posInfo + " -- " + vc.condition).mkString("\n\n"))
+
+ toRet
}
def generateMiscCorrectnessConditions(function: FunDef) : Seq[VerificationCondition] = {
@@ -135,6 +168,10 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
}
expr match {
+ case Let(i,e,b) => {
+ rec(e, path)
+ rec(b, Equals(Variable(i), e) :: path)
+ }
case IfExpr(cond, then, elze) => {
rec(cond, path)
rec(then, cond :: path)
diff --git a/src/purescala/Definitions.scala b/src/purescala/Definitions.scala
index 6f1dcfef95ba104b06fda0ea04fc2822e2576340..297d8d0257ac75d6026b76c3e48daea0f8e5fbb6 100644
--- a/src/purescala/Definitions.scala
+++ b/src/purescala/Definitions.scala
@@ -224,7 +224,7 @@ object Definitions {
}
}
}
- class FunDef(val id: Identifier, val returnType: TypeTree, val args: VarDecls) extends Definition {
+ class FunDef(val id: Identifier, val returnType: TypeTree, val args: VarDecls) extends Definition with ScalacPositional {
var body: Option[Expr] = None
var precondition: Option[Expr] = None
var postcondition: Option[Expr] = None
diff --git a/src/purescala/Extensions.scala b/src/purescala/Extensions.scala
index f97c25d00dd7edb71540e60e12eb0d3eb0875bfa..7b1331748b369fea23bc605b559ed97733aba2a3 100644
--- a/src/purescala/Extensions.scala
+++ b/src/purescala/Extensions.scala
@@ -85,7 +85,11 @@ object Extensions {
}
// these extensions are always loaded, unless specified otherwise
val defaultExtensions: Seq[Extension] = if(Settings.runDefaultExtensions) {
- (new Z3Solver(extensionsReporter)) :: Nil
+ if(false && Settings.useInstantiator) {
+ (new IterativeZ3Solver(extensionsReporter)) :: Nil
+ } else {
+ (new Z3Solver(extensionsReporter)) :: Nil
+ }
} else {
Nil
}
diff --git a/src/purescala/IterativeZ3Solver.scala b/src/purescala/IterativeZ3Solver.scala
new file mode 100644
index 0000000000000000000000000000000000000000..479ee402e7f2062a8c99623f797ebb87d3e96bc0
--- /dev/null
+++ b/src/purescala/IterativeZ3Solver.scala
@@ -0,0 +1,17 @@
+package purescala
+
+import z3.scala._
+import Common._
+import Definitions._
+import Extensions._
+import Trees._
+import TypeTrees._
+
+class IterativeZ3Solver(reporter: Reporter) extends Z3Solver(reporter) {
+ override val description = "Z3 Solver (w/ feedback loop)"
+ override val shortDescription = "Z3/loop"
+
+ override def solve(expression: Expr) : Option[Boolean] = {
+ Some(false)
+ }
+}
diff --git a/src/purescala/PrettyPrinter.scala b/src/purescala/PrettyPrinter.scala
index 8c81b5e8f16d090ea6d3c219d73fa2ac49dfa56d..f8edbd8daef7b1d34673ef1538f4d701c24b3b67 100644
--- a/src/purescala/PrettyPrinter.scala
+++ b/src/purescala/PrettyPrinter.scala
@@ -146,7 +146,7 @@ object PrettyPrinter {
nsb
}
- case MatchExpr(s, csc) => {
+ case mex @ MatchExpr(s, csc) => {
def ppc(sb: StringBuffer, p: Pattern): StringBuffer = p match {
//case InstanceOfPattern(None, ctd) =>
//case InstanceOfPattern(Some(id), ctd) =>
@@ -171,7 +171,11 @@ object PrettyPrinter {
var nsb = sb
nsb == pp(s, nsb, lvl)
- nsb.append(" match {\n")
+ // if(mex.posInfo != "") {
+ // nsb.append(" match@(" + mex.posInfo + ") {\n")
+ // } else {
+ nsb.append(" match {\n")
+ // }
csc.foreach(cs => {
ind(nsb, lvl+1)
diff --git a/src/purescala/Trees.scala b/src/purescala/Trees.scala
index de585fcb3a5203766a447991c28af46ec20b8183..4945b0fdabf587ab14322cef6d50a754ea3badd0 100644
--- a/src/purescala/Trees.scala
+++ b/src/purescala/Trees.scala
@@ -19,7 +19,7 @@ object Trees {
/* This describes computational errors (unmatched case, taking min of an
* empty set, division by zero, etc.). It should always be typed according to
* the expected type. */
- case class Error(description: String) extends Expr with Terminal
+ case class Error(description: String) extends Expr with Terminal with ScalacPositional
/* Like vals */
case class Let(binder: Identifier, value: Expr, body: Expr) extends Expr {
@@ -30,7 +30,7 @@ object Trees {
}
/* Control flow */
- case class FunctionInvocation(funDef: FunDef, args: Seq[Expr]) extends Expr with FixedType {
+ case class FunctionInvocation(funDef: FunDef, args: Seq[Expr]) extends Expr with FixedType with ScalacPositional {
val fixedType = funDef.returnType
}
case class IfExpr(cond: Expr, then: Expr, elze: Expr) extends Expr
@@ -50,7 +50,7 @@ object Trees {
def unapply(me: MatchExpr) : Option[(Expr,Seq[MatchCase])] = if (me == null) None else Some((me.scrutinee, me.cases))
}
- class MatchExpr(val scrutinee: Expr, val cases: Seq[MatchCase]) extends Expr {
+ class MatchExpr(val scrutinee: Expr, val cases: Seq[MatchCase]) extends Expr with ScalacPositional {
def scrutineeClassType: ClassType = scrutinee.getType.asInstanceOf[ClassType]
}
@@ -377,7 +377,7 @@ object Trees {
object NAryOperator {
def unapply(expr: Expr) : Option[(Seq[Expr],(Seq[Expr])=>Expr)] = expr match {
- case FunctionInvocation(fd, args) => Some((args, FunctionInvocation(fd, _)))
+ case fi @ FunctionInvocation(fd, args) => Some((args, (as => FunctionInvocation(fd, as).setPosInfo(fi))))
case CaseClass(cd, args) => Some((args, CaseClass(cd, _)))
case And(args) => Some((args, And.apply))
case Or(args) => Some((args, Or.apply))
@@ -474,7 +474,7 @@ object Trees {
else
i
}
- case m @ MatchExpr(scrut,cses) => MatchExpr(rec(scrut), cses.map(inCase(_))).setType(m.getType)
+ case m @ MatchExpr(scrut,cses) => MatchExpr(rec(scrut), cses.map(inCase(_))).setType(m.getType).setPosInfo(m)
case t if t.isInstanceOf[Terminal] => t
case unhandled => scala.Predef.error("Non-terminal case should be handled in searchAndReplace: " + unhandled)
}
@@ -565,7 +565,7 @@ object Trees {
val rscrut = rec(scrut)
val (newCses,changes) = cses.map(inCase(_)).unzip
applySubst(if(rscrut != scrut || changes.exists(res=>res)) {
- MatchExpr(rscrut, newCses).setType(m.getType)
+ MatchExpr(rscrut, newCses).setType(m.getType).setPosInfo(m)
} else {
m
})
@@ -619,7 +619,7 @@ object Trees {
}
def applyToTree(e : Expr) : Option[Expr] = e match {
- case m @ MatchExpr(s, cses) => Some(MatchExpr(s, cses.map(freshenCase(_))).setType(m.getType))
+ case m @ MatchExpr(s, cses) => Some(MatchExpr(s, cses.map(freshenCase(_))).setType(m.getType).setPosInfo(m))
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)))
@@ -792,7 +792,7 @@ object Trees {
case v @ Variable(id) if s.isDefinedAt(id) => rec(s(id), s)
case l @ Let(i,e,b) => rec(b, s + (i -> rec(e, s)))
case i @ IfExpr(t1,t2,t3) => IfExpr(rec(t1, s),rec(t2, s),rec(t3, s)).setType(i.getType)
- case m @ MatchExpr(scrut,cses) => MatchExpr(rec(scrut, s), cses.map(inCase(_, s))).setType(m.getType)
+ case m @ MatchExpr(scrut,cses) => MatchExpr(rec(scrut, s), cses.map(inCase(_, s))).setType(m.getType).setPosInfo(m)
case n @ NAryOperator(args, recons) => {
var change = false
val rargs = args.map(a => {
@@ -956,23 +956,23 @@ object Trees {
})
}
- def explicitPreconditions(expr: Expr) : Expr = {
- def rewriteFunctionCall(e: Expr) : Option[Expr] = e match {
- case fi @ FunctionInvocation(fd, args) if(fd.hasPrecondition && fd.precondition.get != BooleanLiteral(true)) => {
- val fTpe = fi.getType
- val prec = matchToIfThenElse(fd.precondition.get)
- val newLetIDs = fd.args.map(a => FreshIdentifier("precarg_" + a.id.name, true).setType(a.tpe))
- val substMap = Map[Expr,Expr]((fd.args.map(_.toVariable) zip newLetIDs.map(Variable(_))) : _*)
- val newPrec = replace(substMap, prec)
- val newThen = FunctionInvocation(fd, newLetIDs.map(_.toVariable)).setType(fTpe)
- val ifExpr: Expr = IfExpr(newPrec, newThen, Error("precondition violated").setType(fTpe)).setType(fTpe)
- Some((newLetIDs zip args).foldRight(ifExpr)((iap,e) => Let(iap._1, iap._2, e)))
- }
- case _ => None
- }
-
- searchAndReplaceDFS(rewriteFunctionCall)(expr)
- }
+// def explicitPreconditions(expr: Expr) : Expr = {
+// def rewriteFunctionCall(e: Expr) : Option[Expr] = e match {
+// case fi @ FunctionInvocation(fd, args) if(fd.hasPrecondition && fd.precondition.get != BooleanLiteral(true)) => {
+// val fTpe = fi.getType
+// val prec = matchToIfThenElse(fd.precondition.get)
+// val newLetIDs = fd.args.map(a => FreshIdentifier("precarg_" + a.id.name, true).setType(a.tpe))
+// val substMap = Map[Expr,Expr]((fd.args.map(_.toVariable) zip newLetIDs.map(Variable(_))) : _*)
+// val newPrec = replace(substMap, prec)
+// val newThen = FunctionInvocation(fd, newLetIDs.map(_.toVariable)).setType(fTpe).setPosInfo(fi)
+// val ifExpr: Expr = IfExpr(newPrec, newThen, Error("precondition violated").setType(fTpe).setPosInfo(fi)).setType(fTpe)
+// Some((newLetIDs zip args).foldRight(ifExpr)((iap,e) => Let(iap._1, iap._2, e)))
+// }
+// case _ => None
+// }
+//
+// searchAndReplaceDFS(rewriteFunctionCall)(expr)
+// }
private var matchConverterCache = new scala.collection.mutable.HashMap[Expr,Expr]()
/** Rewrites all pattern-matching expressions into if-then-else expressions,
@@ -1020,7 +1020,7 @@ object Trees {
def rewritePM(e: Expr) : Option[Expr] = e match {
case m @ MatchExpr(scrut, cases) => {
- println("Rewriting the following PM: " + e)
+ // println("Rewriting the following PM: " + e)
val condsAndRhs = for(cse <- cases) yield {
val map = mapForPattern(scrut, cse.pattern)
@@ -1033,8 +1033,12 @@ object Trees {
(realCond, newRhs)
}
- val bigIte = condsAndRhs.foldRight[Expr](Error("non-exhaustive match").setType(bestRealType(m.getType)))((p1, ex) => {
- IfExpr(p1._1, p1._2, ex).setType(m.getType)
+ val bigIte = condsAndRhs.foldRight[Expr](Error("non-exhaustive match").setType(bestRealType(m.getType)).setPosInfo(m))((p1, ex) => {
+ if(p1._1 == BooleanLiteral(true)) {
+ p1._2
+ } else {
+ IfExpr(p1._1, p1._2, ex).setType(m.getType)
+ }
})
//println(condsAndRhs)
Some(bigIte)
diff --git a/src/purescala/VerificationCondition.scala b/src/purescala/VerificationCondition.scala
index d43458ba4fec20e83e2f48c67c74a8af2e5f6d46..b62c5f176f1bf3cfd534a1599c8c4f6d92be7a7a 100644
--- a/src/purescala/VerificationCondition.scala
+++ b/src/purescala/VerificationCondition.scala
@@ -1,11 +1,12 @@
package purescala
-import purescala.Extensions._
-import purescala.Trees._
-import purescala.Definitions._
+import Extensions._
+import Trees._
+import Definitions._
+import Common._
/** This is just to hold some history information. */
-class VerificationCondition(val condition: Expr, val funDef: FunDef, val kind: VCKind.Value, val tactic: Tactic, val info: String = "") {
+class VerificationCondition(val condition: Expr, val funDef: FunDef, val kind: VCKind.Value, val tactic: Tactic, val info: String = "") extends ScalacPositional {
// None = still unknown
// Some(true) = valid
// Some(false) = valid
@@ -32,15 +33,15 @@ class VerificationCondition(val condition: Expr, val funDef: FunDef, val kind: V
private def timeStr = time.map(t => "%-3.3f".format(t)).getOrElse("")
def infoLine : String = {
- "║ %-20s %-10s %-8s %-10s %-7s %7s ║" format (funDef.id.toString, kind, status, tacticStr, solverStr, timeStr)
+ "║ %-25s %-9s %9s %-8s %-10s %-7s %7s ║" format (funDef.id.toString, kind, posInfo, status, tacticStr, solverStr, timeStr)
}
}
object VerificationCondition {
- val infoFooter : String = "╚" + ("═" * 69) + "╝"
+ val infoFooter : String = "╚" + ("═" * 83) + "╝"
val infoHeader : String = ". ┌─────────┐\n" +
- "╔═╡ Summary ╞" + ("═" * 57) + "╗\n" +
- "║ └─────────┘" + (" " * 57) + "║"
+ "╔═╡ Summary ╞" + ("═" * 71) + "╗\n" +
+ "║ └─────────┘" + (" " * 71) + "║"
}
object VCKind extends Enumeration {
diff --git a/src/purescala/Z3Solver.scala b/src/purescala/Z3Solver.scala
index e837ba80b5fae1d57d5207cc6d6f21a8d824da9c..24af2daf339239e70f8c57cc0c0591504d159433 100644
--- a/src/purescala/Z3Solver.scala
+++ b/src/purescala/Z3Solver.scala
@@ -448,7 +448,7 @@ class Z3Solver(val reporter: Reporter) extends Solver(reporter) with Z3ModelReco
case Some(ast) => ast
case None => {
if (id.isLetBinder) {
- scala.Predef.error("Error in formula being translated to Z3: identifier " + id + " seems to have escaped its let-definition")
+ //scala.Predef.error("Error in formula being translated to Z3: identifier " + id + " seems to have escaped its let-definition")
}
val newAST = z3.mkFreshConst(id.name, typeToSort(v.getType))
z3Vars = z3Vars + (id -> newAST)
diff --git a/src/purescala/z3plugins/instantiator/Instantiator.scala b/src/purescala/z3plugins/instantiator/Instantiator.scala
index 0b861a084ac8feb71788f0385181dd5fefc0771a..b5834f139c9f6e7a15eafeafc6e6c3874992d4ae 100644
--- a/src/purescala/z3plugins/instantiator/Instantiator.scala
+++ b/src/purescala/z3plugins/instantiator/Instantiator.scala
@@ -262,7 +262,7 @@ class Instantiator(val z3Solver: Z3Solver) extends Z3Theory(z3Solver.z3, "Instan
canAssertAxiom = true
if (toAssertASAP.nonEmpty) {
- println("In a safe block. " + toAssertASAP.size + " axioms to add.")
+ // println("In a safe block. " + toAssertASAP.size + " axioms to add.")
for ((lvl, ax) <- toAssertASAP) {
if(lvl <= pushLevel) {
assertAxiomNow(ax)
diff --git a/testcases/RedBlack.scala b/testcases/RedBlack.scala
deleted file mode 100644
index b3368ad0031259523903de41a3789c6d182daae9..0000000000000000000000000000000000000000
--- a/testcases/RedBlack.scala
+++ /dev/null
@@ -1,288 +0,0 @@
-//SJ: I tried to modify this so that funcheck doesn't give Z3 translation
-// warnings, but didn't manage quite yet
-
-import scala.collection.immutable.Set
-
-object RedBlack {
-
- abstract sealed class Color;
- case class Red() extends Color;
- case class Black() extends Color;
-
- abstract sealed class Tree;
- case class Leaf() extends Tree;
- case class Node(color : Color, left: Tree, elem: Int, right: Tree) extends Tree;
-
- // Invariant 1. No red node has a red parent
- def invariant1(t: Tree): Boolean = t match {
- case Leaf() => true
- case Node(color, left, _, right) => color match {
- case Black() => invariant1(left) && invariant1(right)
- case Red() => left match {
- case Node(col2, _, _, _) => col2 match {
- case Red() => false
- case _ => right match {
- case Node(col3, _, _, _) => col3 match {
- case Red() => false
- case _ => invariant1(left) && invariant1(right)
- }
- }
- }
- case Leaf() => right match {
- case Node(col3, _, _, _) => col3 match {
- case Red() => false
- case _ => invariant1(left) && invariant1(right)
- }
- }
- }
- }
- }
- /// Invariant 1 END
-
- // Invariant 2. Each path from the root to an
- // empty node contains the same number of black
- // nodes
-
- def countBlackNodes(t: Tree): Int = t match {
- case Leaf() => 1
- case Node(color, left, _, _) => color match {
- case Red() => countBlackNodes(left)
- case Black() => countBlackNodes(left) + 1
- }
- }
-
- def invariant2(t: Tree, n: Int): Boolean = t match {
- case Leaf() => if (n == 1) true else false
- case Node(color, left, _, right) => color match {
- case Red() => invariant2(left, n) && invariant2(right, n)
- case Black() => invariant2(left, n-1) && invariant2(right, n-1)
- }
- }
-
- /// Invariant 2 END
-
- def member(t: Tree, e: Int): Boolean = t match {
- case Leaf() => false
- case Node(_, left, x, right) => if (x == e) true
- else if (e < x) member( left, e)
- else member(right, e)
- }
-
- def contents(t: Tree): Set[Int] = t match {
- case Leaf() => Set.empty
- case Node(_, left, x, right) => contents(left) ++ contents(right) ++ Set(x)
- }
-
- def makeBlack(t: Node) = {
- //require(t != Leaf())
- //val Node(_, left, x, right) = t
- //Node(Black(), left, x, right)
- Node(Black(), t.left, t.elem, t.right)
- } ensuring ((x:Tree) => x match {case Node(col, _, _, _) => (col==Black()); case _ => false})
-
- def ins_(t: Tree, e: Int): Node = t match {
- case Leaf() => Node(Red(), Leaf(), e, Leaf())
- case n@Node(color, left, x, right) => if (x<e) balance(Node(color, ins_(left, e), x, right))
- else if (x > e) balance(Node(color, left, x, ins_(right, e)))
- else n //Element already exists
- }
-
-// def balance(t: Node) : Node = {
- //require(t != Leaf())
-// t match {
-// case Node(Black(), Node(Red(), Node(Red(), a, x, b), y, c), z, d) => Node(Red(), Node(Black(), a, x, b), y, Node(Black(), c, z, d))
-// case Node(Black(), Node(Red(), a, x, Node(Red(), b, y, c)), z, d) => Node(Red(), Node(Black(), a, x, b), y, Node(Black(), c, z, d))
-// case Node(Black(), a, x, Node(Red(), Node(Red(), b, y, c), z, d)) => Node(Red(), Node(Black(), a, x, b), y, Node(Black(), c, z, d))
-// case Node(Black(), a, x, Node(Red(), b, y, Node(Red(), c, z, d))) => Node(Red(), Node(Black(), a, x, b), y, Node(Black(), c, z, d))
-// case n@Node(_,_,_,_) => n
-// }
-// } //ensuring (_ => true)
-
- def balance(t: Node) : Node = {
- //require(t != Leaf())
- t.color match {
- case Black() => t.left match {
- case Node(cl,ll,el,rl) => cl match {
- case Red() => ll match {
- case Node(cll,lll,ell,rll) => cll match {
- case Red() => Node(Red(), Node(Black(), lll, ell, rll), el, Node(Black(), rl, t.elem, t.right))
- case Black() => rl match {
- case Node(crl,lrl,erl,rrl) => crl match {
- case Red() => Node(Red(), Node(Black(), ll, el, lrl), erl, Node(Black(), rrl, t.elem, t.right))
- case Black() => t.right match {
- case Node(cr,lr,er,rr) => cr match {
- case Red() => lr match {
- case Node(clr,llr,elr,rlr) => clr match {
- case Red() => Node(Red(), Node(Black(), t.left, t.elem, llr), elr, Node(Black(), rlr, er, rr))
- case Black() => rr match {
- case Node(crr,lrr,err,rrr) => crr match {
- case Red() => Node(Red(), Node(Black(), t.left, t.elem, lr), er, Node(Black(), lrr, err, rrr))
- case Black() => t
- }
- case Leaf() => t
- }
- }
- case Leaf() => rr match {
- case Node(crr,lrr,err,rrr) => crr match {
- case Red() => Node(Red(), Node(Black(), t.left, t.elem, lr), er, Node(Black(), lrr, err, rrr))
- case Black() => t
- }
- case Leaf() => t
- }
- }
- case Black() => t
- }
- case Leaf() => t
- }
- }
- case Leaf() => t.right match {
- case Node(cr,lr,er,rr) => cr match {
- case Red() => lr match {
- case Node(clr,llr,elr,rlr) => clr match {
- case Red() => Node(Red(), Node(Black(), t.left, t.elem, llr), elr, Node(Black(), rlr, er, rr))
- case Black() => rr match {
- case Node(crr,lrr,err,rrr) => crr match {
- case Red() => Node(Red(), Node(Black(), t.left, t.elem, lr), er, Node(Black(), lrr, err, rrr))
- case Black() => t
- }
- case Leaf() => t
- }
- }
- case Leaf() => rr match {
- case Node(crr,lrr,err,rrr) => crr match {
- case Red() => Node(Red(), Node(Black(), t.left, t.elem, lr), er, Node(Black(), lrr, err, rrr))
- case Black() => t
- }
- case Leaf() => t
- }
- }
- case Black() => t
- }
- case Leaf() => t
- }
- }
- }
- case Leaf() => rl match {
- case Node(crl,lrl,erl,rrl) => crl match {
- case Red() => Node(Red(), Node(Black(), ll, el, lrl), erl, Node(Black(), rrl, t.elem, t.right))
- case Black() => t.right match {
- case Node(cr,lr,er,rr) => cr match {
- case Red() => lr match {
- case Node(clr,llr,elr,rlr) => clr match {
- case Red() => Node(Red(), Node(Black(), t.left, t.elem, llr), elr, Node(Black(), rlr, er, rr))
- case Black() => rr match {
- case Node(crr,lrr,err,rrr) => crr match {
- case Red() => Node(Red(), Node(Black(), t.left, t.elem, lr), er, Node(Black(), lrr, err, rrr))
- case Black() => t
- }
- case Leaf() => t
- }
- }
- case Leaf() => rr match {
- case Node(crr,lrr,err,rrr) => crr match {
- case Red() => Node(Red(), Node(Black(), t.left, t.elem, lr), er, Node(Black(), lrr, err, rrr))
- case Black() => t
- }
- case Leaf() => t
- }
- }
- case Black() => t
- }
- case Leaf() => t
- }
- }
- case Leaf() => t.right match {
- case Node(cr,lr,er,rr) => cr match {
- case Red() => lr match {
- case Node(clr,llr,elr,rlr) => clr match {
- case Red() => Node(Red(), Node(Black(), t.left, t.elem, llr), elr, Node(Black(), rlr, er, rr))
- case Black() => rr match {
- case Node(crr,lrr,err,rrr) => crr match {
- case Red() => Node(Red(), Node(Black(), t.left, t.elem, lr), er, Node(Black(), lrr, err, rrr))
- case Black() => t
- }
- case Leaf() => t
- }
- }
- case Leaf() => rr match {
- case Node(crr,lrr,err,rrr) => crr match {
- case Red() => Node(Red(), Node(Black(), t.left, t.elem, lr), er, Node(Black(), lrr, err, rrr))
- case Black() => t
- }
- case Leaf() => t
- }
- }
- case Black() => t
- }
- case Leaf() => t
- }
- }
- }
- case Black() => t.right match {
- case Node(cr,lr,er,rr) => cr match {
- case Red() => lr match {
- case Node(clr,llr,elr,rlr) => clr match {
- case Red() => Node(Red(), Node(Black(), t.left, t.elem, llr), elr, Node(Black(), rlr, er, rr))
- case Black() => rr match {
- case Node(crr,lrr,err,rrr) => crr match {
- case Red() => Node(Red(), Node(Black(), t.left, t.elem, lr), er, Node(Black(), lrr, err, rrr))
- case Black() => t
- }
- case Leaf() => t
- }
- }
- case Leaf() => rr match {
- case Node(crr,lrr,err,rrr) => crr match {
- case Red() => Node(Red(), Node(Black(), t.left, t.elem, lr), er, Node(Black(), lrr, err, rrr))
- case Black() => t
- }
- case Leaf() => t
- }
- }
- case Black() => t
- }
- case Leaf() => t
- }
- }
- case Leaf() => t.right match {
- case Node(cr,lr,er,rr) => cr match {
- case Red() => lr match {
- case Node(clr,llr,elr,rlr) => clr match {
- case Red() => Node(Red(), Node(Black(), t.left, t.elem, llr), elr, Node(Black(), rlr, er, rr))
- case Black() => rr match {
- case Node(crr,lrr,err,rrr) => crr match {
- case Red() => Node(Red(), Node(Black(), t.left, t.elem, lr), er, Node(Black(), lrr, err, rrr))
- case Black() => t
- }
- case Leaf() => t
- }
- }
- case Leaf() => rr match {
- case Node(crr,lrr,err,rrr) => crr match {
- case Red() => Node(Red(), Node(Black(), t.left, t.elem, lr), er, Node(Black(), lrr, err, rrr))
- case Black() => t
- }
- case Leaf() => t
- }
- }
- case Black() => t
- }
- case Leaf() => t
- }
- }
- case Red() => t
- }
- }
-
- def insert(t: Tree, e: Int): Tree = makeBlack( ins_(t, e) ) ensuring {res => invariant1(res) && invariant2(res, countBlackNodes(res))}
-
- def main(args : Array[String]) = {
- var rb : Tree = Leaf()
- for(ii <- 1 to 10) {
- rb = insert( rb, ii )
- println(rb)
- }
- }
-}
-
-