From 50a8dda1be76422e2ed43156bd48df3c9f527b4f Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Tue, 26 Oct 2010 15:58:11 +0000
Subject: [PATCH]
---
WISHLIST | 7 +++--
src/funcheck/CodeExtraction.scala | 4 +++
src/funcheck/Extractors.scala | 10 +++++++
src/funcheck/FunCheckPlugin.scala | 3 +-
src/purescala/Analysis.scala | 50 +++++++++++++++----------------
src/purescala/Settings.scala | 1 -
src/purescala/Z3Solver.scala | 11 ++++---
testcases/ExprComp.scala | 1 +
8 files changed, 50 insertions(+), 37 deletions(-)
diff --git a/WISHLIST b/WISHLIST
index f3f3f786d..fa1ab68c2 100644
--- a/WISHLIST
+++ b/WISHLIST
@@ -1,14 +1,15 @@
Add here what you would love FunCheck to be able to do
------------------------------------------------------
-PS: rewrite pattern-matching translator to use if-then-else
PS: generate VCs for preconditions
PS: generate VCs for pattern-matching
-PS: support multiple top-level objects, and use 'private' accessor to indicate what's part of the interface
+PS: support multiple top-level objects
+PS: use 'private' accessor to indicate what's part of the interface
PS: support tuples (including natively in Z3)
-
Wishes granted so far
---------------------
PS: create a wishlist
+PS: rewrite pattern-matching translator to use if-then-else
+VK: add IsValid class to allow for writing just "holds" in place of ensuring(_ == true)
diff --git a/src/funcheck/CodeExtraction.scala b/src/funcheck/CodeExtraction.scala
index 5817434ed..c76e1ca7f 100644
--- a/src/funcheck/CodeExtraction.scala
+++ b/src/funcheck/CodeExtraction.scala
@@ -227,6 +227,10 @@ trait CodeExtraction extends Extractors {
realBody = body2
ensCont = Some(c1)
}
+ case ExHoldsExpression(body2) => {
+ realBody = body2
+ ensCont = Some(ResultVariable().setType(BooleanType))
+ }
case _ => ;
}
diff --git a/src/funcheck/Extractors.scala b/src/funcheck/Extractors.scala
index 110efa675..3b540a735 100644
--- a/src/funcheck/Extractors.scala
+++ b/src/funcheck/Extractors.scala
@@ -41,6 +41,16 @@ trait Extractors {
}
}
+ object ExHoldsExpression {
+ def unapply(tree: Select) : Option[Tree] = tree match {
+ case Select(Apply(Select(Select(funcheckIdent, utilsName), any2IsValidName), realExpr :: Nil), holdsName) if (
+ utilsName.toString == "Utils" &&
+ any2IsValidName.toString == "any2IsValid" &&
+ holdsName.toString == "holds") => Some(realExpr)
+ case _ => None
+ }
+ }
+
object ExRequiredExpression {
/** Extracts the 'require' contract from an expression (only if it's the
* first call in the block). */
diff --git a/src/funcheck/FunCheckPlugin.scala b/src/funcheck/FunCheckPlugin.scala
index 4a580fa23..6bed3131a 100644
--- a/src/funcheck/FunCheckPlugin.scala
+++ b/src/funcheck/FunCheckPlugin.scala
@@ -27,7 +27,6 @@ class FunCheckPlugin(val global: Global) extends Plugin {
" -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:newPM Use the new pattern-matching translator" + "\n" +
" -P:funcheck:quiet No info and warning messages from the extensions" + "\n" +
" -P:funcheck:XP Enable weird transformations and other bug-producing features"
)
@@ -45,7 +44,7 @@ class FunCheckPlugin(val global: Global) extends Plugin {
case "nodefaults" => purescala.Settings.runDefaultExtensions = false
case "axioms" => purescala.Settings.noForallAxioms = false
case "nobapa" => purescala.Settings.useBAPA = false
- case "newPM" => purescala.Settings.useNewPatternMatchingTranslator = true
+ case "newPM" => { println("''newPM'' is no longer a command-line option, because the new translation is now on by default."); System.exit(0) }
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 daff57637..4ffa87ea5 100644
--- a/src/purescala/Analysis.scala
+++ b/src/purescala/Analysis.scala
@@ -259,29 +259,29 @@ object Analysis {
// Rewrites pattern matching expressions where the cases simply correspond to
// the list of constructors
- def rewriteSimplePatternMatching(expression: Expr) : Expr = {
- var extras : List[Expr] = Nil
-
- def rewritePM(e: Expr) : Option[Expr] = e match {
- // case NotSoSimplePatternMatching(_) => None
- case SimplePatternMatching(scrutinee, classType, casesInfo) => {
- val newVar = Variable(FreshIdentifier("pm", true)).setType(e.getType)
- val scrutAsLetID = FreshIdentifier("scrut", true).setType(scrutinee.getType)
- val lle : List[(Variable,List[Expr])] = casesInfo.map(cseInfo => {
- val (ccd, newPID, argIDs, rhs) = cseInfo
- val newPVar = Variable(newPID)
- val argVars = argIDs.map(Variable(_))
- (newPVar, List(Equals(newPVar, CaseClass(ccd, argVars)), Implies(Equals(Variable(scrutAsLetID), newPVar), Equals(newVar, rhs))))
- }).toList
- val (newPVars, newExtras) = lle.unzip
- extras = Let(scrutAsLetID, scrutinee, And(Or(newPVars.map(Equals(Variable(scrutAsLetID), _))), And(newExtras.flatten))) :: extras
- Some(newVar)
- }
- case m @ MatchExpr(s,_) => Settings.reporter.error("Untranslatable PM expression on type " + s.getType + " : " + m); None
- case _ => None
- }
-
- val newExpr = searchAndReplaceDFS(rewritePM)(expression)
- liftLets(Implies(And(extras), newExpr))
- }
+ // def rewriteSimplePatternMatching(expression: Expr) : Expr = {
+ // var extras : List[Expr] = Nil
+
+ // def rewritePM(e: Expr) : Option[Expr] = e match {
+ // // case NotSoSimplePatternMatching(_) => None
+ // case SimplePatternMatching(scrutinee, classType, casesInfo) => {
+ // val newVar = Variable(FreshIdentifier("pm", true)).setType(e.getType)
+ // val scrutAsLetID = FreshIdentifier("scrut", true).setType(scrutinee.getType)
+ // val lle : List[(Variable,List[Expr])] = casesInfo.map(cseInfo => {
+ // val (ccd, newPID, argIDs, rhs) = cseInfo
+ // val newPVar = Variable(newPID)
+ // val argVars = argIDs.map(Variable(_))
+ // (newPVar, List(Equals(newPVar, CaseClass(ccd, argVars)), Implies(Equals(Variable(scrutAsLetID), newPVar), Equals(newVar, rhs))))
+ // }).toList
+ // val (newPVars, newExtras) = lle.unzip
+ // extras = Let(scrutAsLetID, scrutinee, And(Or(newPVars.map(Equals(Variable(scrutAsLetID), _))), And(newExtras.flatten))) :: extras
+ // Some(newVar)
+ // }
+ // case m @ MatchExpr(s,_) => Settings.reporter.error("Untranslatable PM expression on type " + s.getType + " : " + m); None
+ // case _ => None
+ // }
+
+ // val newExpr = searchAndReplaceDFS(rewritePM)(expression)
+ // liftLets(Implies(And(extras), newExpr))
+ // }
}
diff --git a/src/purescala/Settings.scala b/src/purescala/Settings.scala
index 51225d73f..8be325547 100644
--- a/src/purescala/Settings.scala
+++ b/src/purescala/Settings.scala
@@ -13,5 +13,4 @@ object Settings {
var noForallAxioms: Boolean = true
var unrollingLevel: Int = 0
var useBAPA: Boolean = true
- var useNewPatternMatchingTranslator: Boolean = false
}
diff --git a/src/purescala/Z3Solver.scala b/src/purescala/Z3Solver.scala
index eca0b4ccd..666b1a3f9 100644
--- a/src/purescala/Z3Solver.scala
+++ b/src/purescala/Z3Solver.scala
@@ -165,16 +165,14 @@ class Z3Solver(reporter: Reporter) extends Solver(reporter) with Z3ModelReconstr
functionDefToDef = functionDefToDef + (funDef -> z3.mkFreshFuncDecl(funDef.id.name, sortSeq, typeToSort(funDef.returnType)))
}
- // universally quantifies all functions !
+ // Attempts to universally quantify all functions !
if (!Settings.noForallAxioms) {
- for (funDef <- program.definedFunctions) if (funDef.hasImplementation && program.isRecursive(funDef) && funDef.args.size > 0) {
+ for (funDef <- program.definedFunctions) if (funDef.hasImplementation /* && program.isRecursive(funDef) */ && funDef.args.size > 0) {
// println("Generating forall axioms for " + funDef.id.name)
funDef.body.get match {
case SimplePatternMatching(scrutinee, _, infos) if (
- // funDef.args.size == 1 && funDef.args(0).toVariable == scrutinee
funDef.args.size >= 1 && funDef.args.map(_.toVariable).contains(scrutinee)
) => {
- // println("...has simple PM structure.")
infos.foreach(i => if (!contains(i._4, _.isInstanceOf[MatchExpr])) {
val argsAsVars: Seq[Option[Variable]] = funDef.args.map(a => {
val v = a.toVariable
@@ -195,7 +193,8 @@ class Z3Solver(reporter: Reporter) extends Solver(reporter) with Z3ModelReconstr
}
}
}
- val (ccd, pid, subids, rhs) = i
+ val (ccd, pid, subids, dirtyRHS) = i
+ val cleanRHS = matchToIfThenElse(dirtyRHS)
val argSorts: Seq[Z3Sort] = subids.map(id => typeToSort(id.getType))
val boundVars = argSorts.zip((c + 1) until (c + 1 + argSorts.size)).map(p => z3.mkBound(p._2, p._1))
val matcher: Z3AST = adtConstructors(ccd)(boundVars: _*)
@@ -211,7 +210,7 @@ class Z3Solver(reporter: Reporter) extends Solver(reporter) with Z3ModelReconstr
case Some(v) => v
}))
- val toConvert = Equals(fOfT, rhs)
+ val toConvert = Equals(fOfT, cleanRHS)
//println(toConvert)
val initialMap: Map[String, Z3AST] =
Map((funDef.args.map(_.id) zip otherFunBounds).map(_ match {
diff --git a/testcases/ExprComp.scala b/testcases/ExprComp.scala
index 34c343c8a..df71a041d 100644
--- a/testcases/ExprComp.scala
+++ b/testcases/ExprComp.scala
@@ -60,6 +60,7 @@ object ExprComp {
case NStack(v1,vs1) => vs1 match {
case EStack() => Fail()
case NStack(v2,vs2) => Fail() // should be: run(rest, NStack(evalOp(v1,op,v2),vs2))
+ //case NStack(v2,vs2) => run(rest, NStack(evalOp(v1,op,v2),vs2))
}
}
}
--
GitLab