some unrolling, more options

src/funcheck/FunCheckPlugin.scala

@@ -24,6 +24,7 @@ class FunCheckPlugin(val global: Global) extends Plugin {
     "  -P:funcheck:nodefaults         Runs only the analyses provided by the extensions" + "\n" +
     "  -P:funcheck:functions=fun1:... Only generates verification conditions for the specified functions" + "\n" +
     "  -P:funcheck:unrolling=[0,1,2]  Unrolling depth for recursive functions" + "\n" + 
+    "  -P:funcheck:noaxioms           Don't generate forall axioms for recursive functions" + "\n" + 
     "  -P:funcheck:tolerant           Silently extracts non-pure function bodies as ''unknown''" + "\n" +
     "  -P:funcheck:quiet              No info and warning messages from the extensions"
   )
@@ -39,6 +40,7 @@ class FunCheckPlugin(val global: Global) extends Plugin {
         case "tolerant"   =>                     silentlyTolerateNonPureBodies = true
         case "quiet"      =>                     purescala.Settings.quietExtensions = true
         case "nodefaults" =>                     purescala.Settings.runDefaultExtensions = false
+        case "noaxioms"   =>                     purescala.Settings.noForallAxioms = 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/Analysis.scala

@@ -115,15 +115,12 @@ class Analysis(val program: Program) {
       }
 
       import Analysis._
-      val newExpr0 = unrollRecursiveFunctions(program, withPrec, Settings.unrollingLevel)
-      val (newExpr1, sideExprs1) = rewriteSimplePatternMatching(newExpr0)
-      val (newExpr2, sideExprs2) = inlineFunctionsAndContracts(program, newExpr1)
-
-      if(sideExprs1.isEmpty && sideExprs2.isEmpty) {
-        newExpr2
-      } else {
-        Implies(And(sideExprs1 ++ sideExprs2), newExpr2)
-      }
+      val (newExpr0, sideExprs0) = unrollRecursiveFunctions(program, withPrec, Settings.unrollingLevel)
+      val expr0 = Implies(And(sideExprs0), newExpr0)
+      val (newExpr1, sideExprs1) = rewriteSimplePatternMatching(expr0)
+      val expr1 = Implies(And(sideExprs1), newExpr1)
+      val (newExpr2, sideExprs2) = inlineFunctionsAndContracts(program, expr1)
+      Implies(And(sideExprs2), newExpr2)
     }
   }
 
@@ -164,27 +161,44 @@ object Analysis {
     (searchAndApply(isFunCall, applyToCall, expr), extras.reverse)
   }
 
-  def unrollRecursiveFunctions(program: Program, expr: Expr, times: Int) : Expr = {
-    def isRecursiveCall(e: Expr) = e match {
-      case f @ FunctionInvocation(fd, _) if fd.hasImplementation && program.isRecursive(fd) => true
-      case _ => false
-    }
-    def unrollCall(t: Int)(e: Expr) = e match {
-      case f @ FunctionInvocation(fd, args) if fd.hasImplementation && program.isRecursive(fd) => {
-        val newLetIDs = fd.args.map(a => FreshIdentifier(a.id.name, true).setType(a.tpe))
-        val newLetVars = newLetIDs.map(Variable(_))
-        val substs: Map[Expr,Expr] = Map((fd.args.map(_.toVariable) zip newLetVars) :_*)
-        val bodyWithLetVars: Expr = replace(substs, fd.body.get)
-        val bigLet = (newLetIDs zip args).foldLeft(bodyWithLetVars)((e,p) => Let(p._1, p._2, e))
-        unrollRecursiveFunctions(program, bigLet, t - 1)
+  def unrollRecursiveFunctions(program: Program, expression: Expr, times: Int) : (Expr,Seq[Expr]) = {
+    var extras : List[Expr] = Nil
+
+    def urf(expr: Expr, left: Int) : Expr = {
+      def isRecursiveCall(e: Expr) = e match {
+        case f @ FunctionInvocation(fd, _) if fd.hasImplementation && program.isRecursive(fd) => true
+        case _ => false
       }
-      case o => o
+      def unrollCall(t: Int)(e: Expr) = e match {
+        case f @ FunctionInvocation(fd, args) if fd.hasImplementation && program.isRecursive(fd) => {
+          val newLetIDs = fd.args.map(a => FreshIdentifier(a.id.name, true).setType(a.tpe))
+          val newLetVars = newLetIDs.map(Variable(_))
+          val substs: Map[Expr,Expr] = Map((fd.args.map(_.toVariable) zip newLetVars) :_*)
+          val bodyWithLetVars: Expr = replace(substs, fd.body.get)
+          if(fd.hasPostcondition) {
+            val post = fd.postcondition.get
+            val newVar = Variable(FreshIdentifier("call", true)).setType(fd.returnType)
+            val newExtra1 = Equals(newVar, bodyWithLetVars)
+            val newExtra2 = replace(substs + (ResultVariable() -> newVar), post)
+            val bigLet = (newLetIDs zip args).foldLeft(And(newExtra1, newExtra2))((e,p) => Let(p._1, p._2, e))
+            extras = bigLet :: extras
+            newVar
+          } else {
+            val bigLet = (newLetIDs zip args).foldLeft(bodyWithLetVars)((e,p) => Let(p._1, p._2, e))
+            urf(bigLet, t-1)
+          }
+        }
+        case o => o
+      }
+
+      if(left > 0)
+        searchAndApply(isRecursiveCall, unrollCall(left), expr, false)
+      else
+        expr
     }
 
-    if(times > 0)
-      searchAndApply(isRecursiveCall, unrollCall(times), expr, false)
-    else
-      expr
+    val finalE = urf(expression, times)
+    (finalE, extras.reverse)
   }
 
   // Rewrites pattern matching expressions where the cases simply correspond to

src/purescala/Settings.scala

@@ -9,5 +9,6 @@ object Settings {
   var reporter: Reporter = new DefaultReporter
   var quietReporter: Reporter = new QuietReporter
   var runDefaultExtensions: Boolean = true
+  var noForallAxioms: Boolean = false
   var unrollingLevel: Int = 0
 }

src/purescala/Trees.scala

@@ -51,7 +51,11 @@ object Trees {
 
   /* Propositional logic */
   object And {
-    def apply(exprs: Seq[Expr]) : And = new And(exprs)
+    def apply(exprs: Seq[Expr]) : Expr = exprs.size match {
+      case 0 => BooleanLiteral(true)
+      case 1 => exprs.head
+      case _ => new And(exprs)
+    }
 
     def apply(l: Expr, r: Expr): Expr = (l,r) match {
       case (And(exs1), And(exs2)) => And(exs1 ++ exs2)
@@ -61,7 +65,7 @@ object Trees {
     }
 
     def unapply(and: And) : Option[Seq[Expr]] = 
-        if(and == null) None else Some(and.exprs)
+      if(and == null) None else Some(and.exprs)
   }
 
   class And(val exprs: Seq[Expr]) extends Expr with FixedType {
@@ -69,7 +73,11 @@ object Trees {
   }
 
   object Or {
-    def apply(exprs: Seq[Expr]) : Or = new Or(exprs)
+    def apply(exprs: Seq[Expr]) : Expr = exprs.size match {
+      case 0 => BooleanLiteral(false)
+      case 1 => exprs.head
+      case _ => new Or(exprs)
+    }
 
     def apply(l: Expr, r: Expr): Expr = (l,r) match {
       case (Or(exs1), Or(exs2)) => Or(exs1 ++ exs2)
@@ -79,7 +87,7 @@ object Trees {
     }
 
     def unapply(or: Or) : Option[Seq[Expr]] = 
-        if(or == null) None else Some(or.exprs)
+      if(or == null) None else Some(or.exprs)
   }
 
   class Or(val exprs: Seq[Expr]) extends Expr with FixedType {
@@ -90,7 +98,20 @@ object Trees {
     val fixedType = BooleanType
   }
 
-  case class Implies(left: Expr, right: Expr) extends Expr with FixedType {
+  object Implies {
+    def apply(left: Expr, right: Expr) : Expr = (left,right) match {
+      case (BooleanLiteral(false), _) => BooleanLiteral(true)
+      case (_, BooleanLiteral(true)) => BooleanLiteral(true)
+      case (BooleanLiteral(true), r) => r
+      case (l, BooleanLiteral(false)) => Not(l)
+      case (l1, Implies(l2, r2)) => Implies(And(l1, l2), r2)
+      case _ => new Implies(left, right)
+    }
+    def unapply(imp: Implies) : Option[(Expr,Expr)] =
+      if(imp == null) None else Some(imp.left, imp.right)
+  }
+
+  class Implies(val left: Expr, val right: Expr) extends Expr with FixedType {
     val fixedType = BooleanType
   }
 
@@ -227,7 +248,7 @@ object Trees {
     def unapply(expr: Expr) : Option[(Expr,Expr,(Expr,Expr)=>Expr)] = expr match {
       case Equals(t1,t2) => Some((t1,t2,Equals))
       case Iff(t1,t2) => Some((t1,t2,Iff))
-      case Implies(t1,t2) => Some((t1,t2,Implies))
+      case Implies(t1,t2) => Some((t1,t2, ((e1,e2) => Implies(e1,e2))))
       case Plus(t1,t2) => Some((t1,t2,Plus))
       case Minus(t1,t2) => Some((t1,t2,Minus))
       case Times(t1,t2) => Some((t1,t2,Times))

src/purescala/Z3Solver.scala

@@ -138,37 +138,45 @@ class Z3Solver(reporter: Reporter) extends Solver(reporter) {
     }
 
     // universally quantifies all functions !
-    for(funDef <- program.definedFunctions) if(funDef.hasImplementation && funDef.args.size > 0) {
-      val argSorts: Seq[Z3Sort] = funDef.args.map(vd => typeToSort(vd.getType).get)
-      val boundVars = argSorts.zipWithIndex.map(p => z3.mkBound(p._2, p._1))
-      val pattern: Z3Pattern = z3.mkPattern(functionDefToDef(funDef)(boundVars: _*))
-      val nameTypePairs = argSorts.map(s => (z3.mkIntSymbol(nextIntForSymbol()), s))
-      val fOfX: Expr = FunctionInvocation(funDef, funDef.args.map(_.toVariable))
-      val toConvert: Expr = if(funDef.hasPrecondition) {
-        Implies(funDef.precondition.get, Equals(fOfX, funDef.body.get))
-      } else {
-        Equals(fOfX, funDef.body.get)
-      }
-      val (newExpr1, sideExprs1) = Analysis.rewriteSimplePatternMatching(toConvert)
-      val (newExpr2, sideExprs2) = (newExpr1, Nil) // Analysis.inlineFunctionsAndContracts(program, newExpr1)
-      val finalToConvert = if(sideExprs1.isEmpty && sideExprs2.isEmpty) {
-        newExpr2
-      } else {
-        Implies(And(sideExprs1 ++ sideExprs2), newExpr2)
-      }
-      val initialMap: Map[Identifier,Z3AST] = Map((funDef.args.map(_.id) zip boundVars):_*)
-      toZ3Formula(z3, finalToConvert, initialMap) match {
-        case Some(axiomTree) => {
-          val quantifiedAxiom = z3.mkForAll(0, List(pattern), nameTypePairs, axiomTree)
-          //z3.printAST(quantifiedAxiom)
-          z3.assertCnstr(quantifiedAxiom)
+    if(!Settings.noForallAxioms) {
+      import Analysis.SimplePatternMatching
+      for(funDef <- program.definedFunctions) if(funDef.hasImplementation && program.isRecursive(funDef) && funDef.args.size > 0) {
+        funDef.body.get match {
+          case SimplePatternMatching(_,_,_) => reporter.info("There's a good opportunity for a good axiomatization of " + funDef.id.name)
+          case _ => ;
         }
-        case None => {
-          reporter.warning("Could not generate forall axiom for " + funDef.id.name)
-          reporter.warning(toConvert)
-          reporter.warning(newExpr1)
-          reporter.warning(newExpr2)
-          reporter.warning(finalToConvert)
+
+        val argSorts: Seq[Z3Sort] = funDef.args.map(vd => typeToSort(vd.getType).get)
+        val boundVars = argSorts.zipWithIndex.map(p => z3.mkBound(p._2, p._1))
+        val pattern: Z3Pattern = z3.mkPattern(functionDefToDef(funDef)(boundVars: _*))
+        val nameTypePairs = argSorts.map(s => (z3.mkIntSymbol(nextIntForSymbol()), s))
+        val fOfX: Expr = FunctionInvocation(funDef, funDef.args.map(_.toVariable))
+        val toConvert: Expr = if(funDef.hasPrecondition) {
+          Implies(funDef.precondition.get, Equals(fOfX, funDef.body.get))
+        } else {
+          Equals(fOfX, funDef.body.get)
+        }
+        val (newExpr1, sideExprs1) = Analysis.rewriteSimplePatternMatching(toConvert)
+        val (newExpr2, sideExprs2) = (newExpr1, Nil) // Analysis.inlineFunctionsAndContracts(program, newExpr1)
+        val finalToConvert = if(sideExprs1.isEmpty && sideExprs2.isEmpty) {
+          newExpr2
+        } else {
+          Implies(And(sideExprs1 ++ sideExprs2), newExpr2)
+        }
+        val initialMap: Map[Identifier,Z3AST] = Map((funDef.args.map(_.id) zip boundVars):_*)
+        toZ3Formula(z3, finalToConvert, initialMap) match {
+          case Some(axiomTree) => {
+            val quantifiedAxiom = z3.mkForAll(0, List(pattern), nameTypePairs, axiomTree)
+            //z3.printAST(quantifiedAxiom)
+            z3.assertCnstr(quantifiedAxiom)
+          }
+          case None => {
+            reporter.warning("Could not generate forall axiom for " + funDef.id.name)
+            reporter.warning(toConvert)
+            reporter.warning(newExpr1)
+            reporter.warning(newExpr2)
+            reporter.warning(finalToConvert)
+          }
         }
       }
     }