induction tactic for generating precondition VCs; prove that map and

append commute

demo/ListOperations.scala

@@ -75,6 +75,25 @@ object ListOperations {
       case Cons(x,xs) => Cons(x, append(xs, l2))
     }) ensuring(content(_) == content(l1) ++ content(l2))
 
+    def map(f : Map[Int,Int], l : List) : List = {
+      require(definedForAll(f, l))
+      l match {
+        case Nil() => Nil()
+        case Cons(x, xs) => Cons(f(x), map(f, xs))
+      }
+    }
+
+    @induct
+    def appendMapCommute(l1 : List, l2 : List, f : Map[Int, Int]) : Boolean = {
+      require(definedForAll(f, l1) && definedForAll(f, l2))
+      map(f, append(l1, l2)) == append(map(f, l1), map(f, l2))
+    } holds
+
+    def definedForAll(f : Map[Int, Int], l : List) : Boolean = l match {
+      case Nil() => true
+      case Cons(x, xs) => f.isDefinedAt(x) && definedForAll(f, xs)
+    }
+
     @induct
     def nilAppend(l : List) : Boolean = (append(l, Nil()) == l) holds
 

src/purescala/DefaultTactic.scala

@@ -189,7 +189,7 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
     }
 
     // prec: there should be no lets and no pattern-matching in this expression
-    private def collectWithPathCondition(matcher: Expr=>Boolean, expression: Expr) : Set[(Seq[Expr],Expr)] = {
+    def collectWithPathCondition(matcher: Expr=>Boolean, expression: Expr) : Set[(Seq[Expr],Expr)] = {
       var collected : Set[(Seq[Expr],Expr)] = Set.empty
 
       def rec(expr: Expr, path: List[Expr]) : Unit = {

src/purescala/FairZ3Solver.scala

@@ -666,6 +666,7 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
               //z3.assertCnstr(toZ3Formula(z3, And(newClauses)).get)
               blockingSet = blockingSet ++ Set(newBlockers.map(p => if(p._2) Not(Variable(p._1)) else Variable(p._1)) : _*)
             }
+            reporter.info(" - finished unrolling")
             unrollingStopwatch.stop
           }
         }

src/purescala/InductionTactic.scala

@@ -9,18 +9,6 @@ class InductionTactic(reporter: Reporter) extends DefaultTactic(reporter) {
   override val description = "Induction tactic for suitable functions"
   override val shortDescription = "induction"
 
-  private def singleAbsClassDef(args: VarDecls) : Option[AbstractClassDef] = {
-    val filtered = args.filter(arg =>
-      arg.getType match {
-        case AbstractClassType(_) => true
-        case _ => false
-      })
-    if (filtered.size != 1) None else (filtered.head.getType match {
-      case AbstractClassType(classDef) => Some(classDef)
-      case _ => scala.sys.error("This should not happen.")
-    })
-  } 
-
   private def firstAbsClassDef(args: VarDecls) : Option[(AbstractClassDef, VarDecl)] = {
     val filtered = args.filter(arg =>
       arg.getType match {
@@ -86,4 +74,82 @@ class InductionTactic(reporter: Reporter) extends DefaultTactic(reporter) {
         defaultPost
     }
   }
+
+  override def generatePreconditions(function: FunDef) : Seq[VerificationCondition] = {
+    val defaultPrec = super.generatePreconditions(function)
+    firstAbsClassDef(function.args) match {
+      case Some((classDef, arg)) => {
+        val toRet = if(function.hasBody) {
+          val cleanBody = expandLets(matchToIfThenElse(function.body.get))
+
+          val allPathConds = collectWithPathCondition((t => t match {
+            case FunctionInvocation(fd, _) if(fd.hasPrecondition) => true
+            case _ => false
+          }), cleanBody)
+
+          def withPrec(path: Seq[Expr], shouldHold: Expr) : Expr = if(function.hasPrecondition) {
+            Not(And(And(matchToIfThenElse(function.precondition.get) +: path), Not(shouldHold)))
+          } else {
+            Not(And(And(path), Not(shouldHold)))
+          }
+
+          val conditionsForAllPaths : Seq[Seq[VerificationCondition]] = allPathConds.map(pc => {
+            val path : Seq[Expr] = pc._1
+            val fi = pc._2.asInstanceOf[FunctionInvocation]
+            val FunctionInvocation(fd, args) = fi
+
+            val conditionsForEachChild = (for (child <- classDef.knownChildren) yield (child match {
+              case ccd @ CaseClassDef(id, prnt, vds) => {
+                val argAsVar = arg.toVariable
+                val selectors = selectorsOfParentType(classDefToClassType(classDef), ccd, argAsVar)
+                
+                val prec : Expr = freshenLocals(matchToIfThenElse(fd.precondition.get))
+                val newLetIDs = fd.args.map(a => FreshIdentifier("arg_" + a.id.name, true).setType(a.tpe))
+                val substMap = Map[Expr,Expr]((fd.args.map(_.toVariable) zip newLetIDs.map(Variable(_))) : _*)
+                val newBody : Expr = replace(substMap, prec)
+                val newCall : Expr = (newLetIDs zip args).foldRight(newBody)((iap, e) => Let(iap._1, iap._2, e))
+
+                val toProve = withPrec(path, newCall)
+
+                val conditionForChild =
+                  if (selectors.isEmpty)
+                    toProve
+                  else {
+                    val inductiveHypothesis = (for (sel <- selectors) yield {
+                      val prec : Expr = freshenLocals(matchToIfThenElse(fd.precondition.get))
+                      val newLetIDs = fd.args.map(a => FreshIdentifier("arg_" + a.id.name, true).setType(a.tpe))
+                      val substMap = Map[Expr,Expr]((fd.args.map(_.toVariable) zip newLetIDs.map(Variable(_))) : _*)
+                      val newBody : Expr = replace(substMap, prec)
+                      val newCall : Expr = (newLetIDs zip args).foldRight(newBody)((iap, e) => Let(iap._1, iap._2, e))
+
+                      val toReplace = withPrec(path, newCall)
+                      replace(Map(argAsVar -> sel), toReplace)
+                    })
+                    Implies(And(inductiveHypothesis), toProve)
+                  }
+                new VerificationCondition(Implies(CaseClassInstanceOf(ccd, argAsVar), conditionForChild), function, VCKind.Precondition, this).setPosInfo(fi)
+              }
+              case _ => scala.sys.error("Abstract class has non-case class subtype")
+            }))
+            println("Induction tactic yields the following VCs:")
+            println(conditionsForEachChild.map(vc => vc.condition).mkString("\n"))
+            conditionsForEachChild
+          }).toSeq
+
+          conditionsForAllPaths.flatten
+        } else {
+          Seq.empty
+        }
+
+        // println("PRECS VCs FOR " + function.id.name)
+        // println(toRet.toList.map(vc => vc.posInfo + " -- " + vc.condition).mkString("\n\n"))
+
+        toRet
+      }
+      case None => {
+        reporter.warning("Induction tactic currently supports exactly one argument of abstract class type")
+        defaultPrec
+      }
+    }
+  }
 }