From 9d196e432c2cb49179428490bd20b1d186dd0efe Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ali=20Sinan=20K=C3=B6ksal?= <alisinan@gmail.com>
Date: Mon, 23 May 2011 20:43:26 +0000
Subject: [PATCH] we now generate VCs for map accesses
---
src/funcheck/CodeExtraction.scala | 7 +++--
src/purescala/DefaultTactic.scala | 31 ++++++++++++++++++++++-
src/purescala/FairZ3Solver.scala | 5 +---
src/purescala/VerificationCondition.scala | 1 +
4 files changed, 37 insertions(+), 7 deletions(-)
diff --git a/src/funcheck/CodeExtraction.scala b/src/funcheck/CodeExtraction.scala
index 2b89efb9a..49174d469 100644
--- a/src/funcheck/CodeExtraction.scala
+++ b/src/funcheck/CodeExtraction.scala
@@ -543,13 +543,16 @@ trait CodeExtraction extends Extractors {
case ExMapApply(m,f) => {
val rm = rec(m)
val rf = rec(f)
- MapGet(rm, rf).setType(rm.getType match {
+ val tpe = rm.getType match {
case MapType(_,toType) => toType
case _ => {
if (!silent) unit.error(tree.pos, "apply on non-map expression")
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)
}
case ExMapIsDefinedAt(m,k) => {
val rm = rec(m)
diff --git a/src/purescala/DefaultTactic.scala b/src/purescala/DefaultTactic.scala
index 0b4cb1924..e4797d1be 100644
--- a/src/purescala/DefaultTactic.scala
+++ b/src/purescala/DefaultTactic.scala
@@ -155,8 +155,37 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
toRet
}
+ def generateMapAccessChecks(function: FunDef) : Seq[VerificationCondition] = {
+ val toRet = if (function.hasBody) {
+ val cleanBody = matchToIfThenElse(function.body.get)
+
+ val allPathConds = collectWithPathCondition((t => t match {
+ case Error("key not found for map access") => 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.MapAccess,
+ this.asInstanceOf[DefaultTactic]).setPosInfo(pc._2.asInstanceOf[Error])
+ ).toSeq
+ } else {
+ Seq.empty
+ }
+
+ toRet
+ }
+
def generateMiscCorrectnessConditions(function: FunDef) : Seq[VerificationCondition] = {
- Seq.empty
+ generateMapAccessChecks(function)
}
// prec: there should be no lets and no pattern-matching in this expression
diff --git a/src/purescala/FairZ3Solver.scala b/src/purescala/FairZ3Solver.scala
index d40e54ed8..c1a61b698 100644
--- a/src/purescala/FairZ3Solver.scala
+++ b/src/purescala/FairZ3Solver.scala
@@ -886,11 +886,8 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
}
case mg @ MapGet(m,k) => m.getType match {
case MapType(fromType, toType) =>
- val errorAST = z3.mkFreshConst("errorValue", typeToSort(toType))
- // exprToZ3Id += (e -> errorAST)
- // z3IdToExpr += (errorAST -> e)
val selected = z3.mkSelect(rec(m), rec(k))
- z3.mkITE(z3.mkDistinct(selected, mapRangeNoneConstructors(toType)()), mapRangeValueSelectors(toType)(selected), errorAST)
+ mapRangeValueSelectors(toType)(selected)
case errorType => scala.Predef.error("Unexpected type for map: " + (ex, errorType))
}
case MapUnion(m1,m2) => m1.getType match {
diff --git a/src/purescala/VerificationCondition.scala b/src/purescala/VerificationCondition.scala
index b62c5f176..7c6710fa2 100644
--- a/src/purescala/VerificationCondition.scala
+++ b/src/purescala/VerificationCondition.scala
@@ -48,4 +48,5 @@ object VCKind extends Enumeration {
val Precondition = Value("precond.")
val Postcondition = Value("postcond.")
val ExhaustiveMatch = Value("match.")
+ val MapAccess = Value("map acc.")
}
--
GitLab