diff --git a/demo/AssociativeListReloaded.scala b/demo/AssociativeListReloaded.scala index 927de56369816e058be6a90edfea82522eb79b8a..a8ea94c725fc41f0e5ca375970b56b38b9cede2b 100644 --- a/demo/AssociativeListReloaded.scala +++ b/demo/AssociativeListReloaded.scala @@ -59,8 +59,9 @@ object AssociativeList { } holds def weird(m : Map[Int,Int], k : Int, v : Int) : Boolean = { - !(m(k) == v) || m.isDefinedAt(k) - } holds + m(k) == v && !m.isDefinedAt(k) + // m.isDefinedAt(k) || !(m(k) == v) + } ensuring(res => !res) // def prop0(l : List, m : Map[Int,Int]) : Boolean = { // size(l) > 4 && asMap(l) == m diff --git a/src/funcheck/CodeExtraction.scala b/src/funcheck/CodeExtraction.scala index 49174d46989189cc12e45bfea7f0658a4fcc63ef..a7c24795a67dda3384ab3ee3114f7dfd8b9b5131 100644 --- a/src/funcheck/CodeExtraction.scala +++ b/src/funcheck/CodeExtraction.scala @@ -550,9 +550,7 @@ trait CodeExtraction extends Extractors { throw ImpureCodeEncounteredException(tree) } } - val mg = MapGet(rm, rf).setType(tpe) - val ida = MapIsDefinedAt(rm, rf) - IfExpr(ida, mg, Error("key not found for map access").setType(tpe)).setType(tpe) + MapGet(rm, rf).setType(tpe) } case ExMapIsDefinedAt(m,k) => { val rm = rec(m) diff --git a/src/purescala/DefaultTactic.scala b/src/purescala/DefaultTactic.scala index e4797d1beb5dc57e7244208058cb55b9c717e570..ee452eb352af5d86d85b99862256085e148f8c3f 100644 --- a/src/purescala/DefaultTactic.scala +++ b/src/purescala/DefaultTactic.scala @@ -157,7 +157,7 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) { def generateMapAccessChecks(function: FunDef) : Seq[VerificationCondition] = { val toRet = if (function.hasBody) { - val cleanBody = matchToIfThenElse(function.body.get) + val cleanBody = mapGetWithChecks(matchToIfThenElse(function.body.get)) val allPathConds = collectWithPathCondition((t => t match { case Error("key not found for map access") => true @@ -165,7 +165,7 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) { }), cleanBody) def withPrecIfDefined(conds: Seq[Expr]) : Expr = if (function.hasPrecondition) { - Not(And(matchToIfThenElse(function.precondition.get), And(conds))) + Not(And(mapGetWithChecks(matchToIfThenElse(function.precondition.get)), And(conds))) } else { Not(And(conds)) } diff --git a/src/purescala/FairZ3Solver.scala b/src/purescala/FairZ3Solver.scala index c1a61b6981a8c016b9a4a20c1908e653e8738c95..a47375f2d701389af60ea7c99f95023204e87753 100644 --- a/src/purescala/FairZ3Solver.scala +++ b/src/purescala/FairZ3Solver.scala @@ -504,7 +504,7 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac } } case (Some(true), m) => { // SAT - // println("the model is") + // println("Model returned by Z3:") // println(m) validatingStopwatch.start val (trueModel, model) = validateAndDeleteModel(m, toCheckAgainstModels, varsInVC, evaluator) @@ -786,9 +786,9 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac case v@Variable(id) => z3Vars.get(id) match { 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") - } + // if (id.isLetBinder) { + // scala.Predef.error("Error in formula being translated to Z3: identifier " + id + " seems to have escaped its let-definition") + // } val newAST = z3.mkFreshConst(id.uniqueName/*name*/, typeToSort(v.getType)) z3Vars = z3Vars + (id -> newAST) exprToZ3Id += (v -> newAST) diff --git a/src/purescala/Trees.scala b/src/purescala/Trees.scala index a24b4c5c7ca79e934f7c3ef238d1956b3e2462ff..d66a25d1125feb11f79d90c60a3340ba1d68ffc1 100644 --- a/src/purescala/Trees.scala +++ b/src/purescala/Trees.scala @@ -1110,6 +1110,31 @@ object Trees { searchAndReplaceDFS(rewritePM)(expr) } + private var mapGetConverterCache = new scala.collection.mutable.HashMap[Expr,Expr]() + /** Rewrites all map accesses with additional error conditions. */ + def mapGetWithChecks(expr: Expr) : Expr = { + val toRet = if (mapGetConverterCache.isDefinedAt(expr)) { + matchConverterCache(expr) + } else { + val converted = convertMapGet(expr) + mapGetConverterCache(expr) = converted + converted + } + + toRet + } + + private def convertMapGet(expr: Expr) : Expr = { + def rewriteMapGet(e: Expr) : Option[Expr] = e match { + case mg @ MapGet(m,k) => + val ida = MapIsDefinedAt(m, k) + Some(IfExpr(ida, mg, Error("key not found for map access").setType(mg.getType)).setType(mg.getType)) + case _ => None + } + + searchAndReplaceDFS(rewriteMapGet)(expr) + } + // prec: expression does not contain match expressions def measureADTChildrenDepth(expression: Expr) : Int = { import scala.math.max