No commit message

No commit message

WISHLIST

@@ -6,6 +6,8 @@ PS: generate VCs for pattern-matching
 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)
+PS: implement @induct tactic
+PS: use a theory plugin to instantiate/unroll function bodies
 
 Wishes granted so far
 ---------------------

src/funcheck/FunCheckPlugin.scala

@@ -28,7 +28,8 @@ class FunCheckPlugin(val global: Global) extends Plugin {
     "  -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"
+    "  -P:funcheck:XP                 Enable weird transformations and other bug-producing features" + "\n" +
+    "  -P:funcheck:PLDI               PLDI 2011 settings. Subject to change. Same warning as for XP."
   )
 
   /** Processes the command-line options. */
@@ -46,6 +47,7 @@ class FunCheckPlugin(val global: Global) extends Plugin {
         case "nobapa"     =>                     purescala.Settings.useBAPA = false
         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 "PLDI"       =>                     { purescala.Settings.experimental = true; purescala.Settings.useInstantiator = true; purescala.Settings.useBAPA = false; purescala.Settings.zeroInlining = 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)): _*)
         case s if s.startsWith("extensions=") => purescala.Settings.extensionNames = splitList(s.substring("extensions=".length, s.length))

src/purescala/DefaultTactic.scala

@@ -38,38 +38,42 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
           }
 
           import Analysis._
-        
-          if(Settings.experimental) {
-            reporter.info("Raw:")
-            reporter.info(withPrec)
-            reporter.info("Raw, expanded:")
-            reporter.info(expandLets(withPrec))
-          }
-          reporter.info(" - inlining...")
-          val expr0 = inlineNonRecursiveFunctions(program, withPrec)
-          if(Settings.experimental) {
-            reporter.info("Inlined:")
-            reporter.info(expr0)
-            reporter.info("Inlined, expanded:")
-            reporter.info(expandLets(expr0))
-          }
-          reporter.info(" - unrolling...")
-          val expr1 = unrollRecursiveFunctions(program, expr0, Settings.unrollingLevel)
-          if(Settings.experimental) {
-            reporter.info("Unrolled:")
-            reporter.info(expr1)
-            reporter.info("Unrolled, expanded:")
-            reporter.info(expandLets(expr1))
-          }
-          reporter.info(" - inlining contracts...")
-          val expr2 = inlineContracts(expr1)
-          if(Settings.experimental) {
-            reporter.info("Contract'ed:")
-            reporter.info(expr2)
-            reporter.info("Contract'ed, expanded:")
-            reporter.info(expandLets(expr2))
+
+          if(Settings.zeroInlining) {
+            withPrec
+          } else {
+            if(Settings.experimental) {
+              reporter.info("Raw:")
+              reporter.info(withPrec)
+              reporter.info("Raw, expanded:")
+              reporter.info(expandLets(withPrec))
+            }
+            reporter.info(" - inlining...")
+            val expr0 = inlineNonRecursiveFunctions(program, withPrec)
+            if(Settings.experimental) {
+              reporter.info("Inlined:")
+              reporter.info(expr0)
+              reporter.info("Inlined, expanded:")
+              reporter.info(expandLets(expr0))
+            }
+            reporter.info(" - unrolling...")
+            val expr1 = unrollRecursiveFunctions(program, expr0, Settings.unrollingLevel)
+            if(Settings.experimental) {
+              reporter.info("Unrolled:")
+              reporter.info(expr1)
+              reporter.info("Unrolled, expanded:")
+              reporter.info(expandLets(expr1))
+            }
+            reporter.info(" - inlining contracts...")
+            val expr2 = inlineContracts(expr1)
+            if(Settings.experimental) {
+              reporter.info("Contract'ed:")
+              reporter.info(expr2)
+              reporter.info("Contract'ed, expanded:")
+              reporter.info(expandLets(expr2))
+            }
+            expr2
           }
-          expr2
         }
         Seq(new VerificationCondition(theExpr, functionDefinition, VCKind.Postcondition, this))
       }

src/purescala/Settings.scala

@@ -12,5 +12,7 @@ object Settings {
   var runDefaultExtensions: Boolean = true
   var noForallAxioms: Boolean = true
   var unrollingLevel: Int = 0
+  var zeroInlining : Boolean = false
   var useBAPA: Boolean = true
+  var useInstantiator: Boolean = false
 }

src/purescala/Z3Solver.scala

@@ -8,11 +8,14 @@ import Trees._
 import TypeTrees._
 
 import z3plugins.bapa.{BAPATheory, BAPATheoryEqc, BAPATheoryBubbles}
+import z3plugins.instantiator.Instantiator
 
 import scala.collection.mutable.{HashMap => MutableHashMap}
 
 class Z3Solver(val reporter: Reporter) extends Solver(reporter) with Z3ModelReconstruction {
   import Settings.useBAPA
+  import Settings.useInstantiator
+
   val description = "Z3 Solver"
   override val shortDescription = "Z3"
 
@@ -31,20 +34,16 @@ class Z3Solver(val reporter: Reporter) extends Solver(reporter) with Z3ModelReco
     )
   toggleWarningMessages(true)
 
-  private var z3: Z3Context = null
+  protected[purescala] var z3: Z3Context = null
+  protected[purescala] var program: Program = null
   private var bapa: BAPATheoryType = null
-  private var program: Program = null
+  private var instantiator: Instantiator = null
   private var neverInitialized = true
 
   private val IntSetType = SetType(Int32Type)
 
   override def setProgram(prog: Program): Unit = {
     program = prog
-    // commented out: Z3 is now restarted for each VC... Could be slow if we
-    // have axioms, but we'll make sure we don't count that in the timing..
-    // The main advantage is that Z3 is not overwhelmed with old axioms (in
-    // BAPA theory)
-    // restartZ3
   }
 
   private def restartZ3: Unit = {
@@ -56,6 +55,8 @@ class Z3Solver(val reporter: Reporter) extends Solver(reporter) with Z3ModelReco
     z3 = new Z3Context(z3cfg)
     // z3.traceToStdout
     if (useBAPA) bapa = new BAPATheoryType(z3)
+    if (useInstantiator) instantiator = new Instantiator(this)
+
     counter = 0
     prepareSorts
     prepareFunctions
@@ -159,16 +160,29 @@ class Z3Solver(val reporter: Reporter) extends Solver(reporter) with Z3ModelReco
     // ...and now everything should be in there...
   }
 
-  private var functionDefToDef: Map[FunDef, Z3FuncDecl] = Map.empty
+  def functionDefToDef(funDef: FunDef) : Z3FuncDecl = {
+    if(useInstantiator) {
+      instantiator.functionDefToDef(funDef)
+    } else {
+      functionMap.getOrElse(funDef, scala.Predef.error("No Z3 definition found for function symbol " + funDef.id.name + ". This is clearly an error (Instantiator is off)."))
+    }
+  }
+  private var functionMap: Map[FunDef, Z3FuncDecl] = Map.empty
 
   def prepareFunctions: Unit = {
     for (funDef <- program.definedFunctions) {
       val sortSeq = funDef.args.map(vd => typeToSort(vd.tpe))
-      functionDefToDef = functionDefToDef + (funDef -> z3.mkFreshFuncDecl(funDef.id.name, sortSeq, typeToSort(funDef.returnType)))
+      val returnSort = typeToSort(funDef.returnType)
+
+      if(useInstantiator) {
+        instantiator.registerFunction(funDef, sortSeq, returnSort)
+      } else {
+        functionMap = functionMap + (funDef -> z3.mkFreshFuncDecl(funDef.id.name, sortSeq, returnSort))
+      }
     }
 
     // Attempts to universally quantify all functions !
-    if (!Settings.noForallAxioms) {
+    if (!Settings.noForallAxioms && !Settings.useInstantiator) {
       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 {
@@ -436,8 +450,7 @@ class Z3Solver(val reporter: Reporter) extends Solver(reporter) with Z3ModelReco
         val tester = adtTesters(ccd)
         tester(rec(e))
       }
-      case f@FunctionInvocation(fd, args) if functionDefToDef.isDefinedAt(fd) => {
-        abstractedFormula = true
+      case f@FunctionInvocation(fd, args) => {
         z3.mkApp(functionDefToDef(fd), args.map(rec(_)): _*)
       }
       case e@EmptySet(_) => if (useBAPA && e.getType == IntSetType) {

src/purescala/z3plugins/instantiator/Instantiator.scala

+package purescala.z3plugins.instantiator
+
+import z3.scala._
+
+import purescala.Common._
+import purescala.Trees._
+import purescala.TypeTrees._
+import purescala.Definitions._
+
+import purescala.Z3Solver
+
+class Instantiator(val z3Solver: Z3Solver) extends Z3Theory(z3Solver.z3, "Instantiator") {
+  import z3Solver.{z3,program,typeToSort}
+
+  setCallbacks(
+    reduceApp = true,
+//    finalCheck = true,
+//    push = true,
+//    pop = true,
+    newApp = true,
+    newAssignment = true,
+    newRelevant = true,
+//    newEq = true,
+//    newDiseq = true,
+//    reset = true,
+    restart = true
+  )
+
+  showCallbacks(true)
+
+  private var functionMap : Map[FunDef,Z3FuncDecl] = Map.empty
+
+  protected[purescala] def registerFunction(funDef: FunDef, sorts: Seq[Z3Sort], returnSort: Z3Sort) : Unit = {
+    functionMap = functionMap + (funDef -> mkTheoryFuncDecl(z3.mkStringSymbol(funDef.id.uniqueName), sorts, returnSort)) 
+  }
+
+  def functionDefToDef(funDef: FunDef) : Z3FuncDecl = {
+    functionMap.getOrElse(funDef, scala.Predef.error("No Z3 definition found for function symbol "+ funDef.id.name + " in Instantiator."))
+  }
+
+  override def newAssignment(ast: Z3AST, polarity: Boolean) : Unit = {
+
+  }
+
+  override def newApp(ast: Z3AST) : Unit = {
+
+  }
+
+  override def newRelevant(ast: Z3AST) : Unit = {
+
+  }
+
+  override def restart : Unit = { }
+}

testcases/Test.scala

+import funcheck.Utils._
 
 object Test {
   sealed abstract class List
@@ -22,5 +23,5 @@ object Test {
 
   def sameSorted(list: List) : Boolean = {
     isSorted(list) == isSorted2(list)
-  } ensuring(r=>r)
+  } holds
 }