Started working on framing

src/main/scala/biabduction/Abduction.scala

@@ -74,7 +74,7 @@ trait AbductionRule[T] extends BiAbductionRule[SiliconAbductionQuestion, T] {
 
   protected def unfoldPredicate(q: SiliconAbductionQuestion, rec: Exp, p: Exp)(Q: (State, Verifier) => VerificationResult): VerificationResult = {
     val predicate = q.s.program.predicates.head
-    val pa = getPredicate(q.s.program, rec, p)
+    val pa = utils.getPredicate(q.s.program, rec, p)
     evals(q.s, Seq(rec), _ => pve, q.v)((s1, tArgs, v1) =>
       eval(s1, p, pve, v1)((s2, tPerm, v2) => {
         permissionSupporter.assertPositive(s2, tPerm, p, pve, v2)((s3, v3) => {
@@ -192,7 +192,7 @@ object AbductionListFold extends AbductionRule[PredicateAccessPredicate] {
     q.goal match {
       case Seq() => Q(None)
       case (a: PredicateAccessPredicate) :: as =>
-        val next = getNextAccess(q.s.program, a.loc.args.head, a.perm)
+        val next = utils.getNextAccess(q.s.program, a.loc.args.head, a.perm)
         checkChunk(next.loc, next.perm, q.s, q.v) {
           case true => Q(Some(a))
           case false => check(q.copy(goal = as))(Q)
@@ -202,8 +202,8 @@ object AbductionListFold extends AbductionRule[PredicateAccessPredicate] {
   }
 
   override protected def apply(q: SiliconAbductionQuestion, inst: PredicateAccessPredicate)(Q: SiliconAbductionQuestion => VerificationResult): VerificationResult = {
-    val headNext = getNextAccess(q.s.program, inst.loc.args.head, inst.perm)
-    val nextList = getPredicate(q.s.program, headNext.loc, inst.perm)
+    val headNext = utils.getNextAccess(q.s.program, inst.loc.args.head, inst.perm)
+    val nextList = utils.getPredicate(q.s.program, headNext.loc, inst.perm)
     val g1: Seq[Exp] = q.goal.filterNot(_ == inst) :+ nextList
     val fold = Fold(inst)()
     consumer.consume(q.s, headNext, pve, q.v)((s1, _, v1) => Q(q.copy(s = s1, v = v1, goal = g1, foundStmts = q.foundStmts :+ fold)))
@@ -219,7 +219,7 @@ object AbductionListUnfold extends AbductionRule[FieldAccessPredicate] {
     q.goal match {
       case Seq() => Q(None)
       case (a: FieldAccessPredicate) :: as =>
-        val pred = getPredicate(q.s.program, a.loc.rcv, a.perm)
+        val pred = utils.getPredicate(q.s.program, a.loc.rcv, a.perm)
         checkChunk(pred.loc, pred.perm, q.s, q.v) {
           case true => Q(Some(a))
           case false => check(q.copy(goal = as))(Q)
@@ -238,7 +238,7 @@ object AbductionListUnfold extends AbductionRule[FieldAccessPredicate] {
     val nNl = NeCmp(inst.loc.rcv, NullLit()())()
     val r1 = q.foundPrecons :+ nNl
 
-    val unfold = Unfold(getPredicate(q.s.program, inst.loc.rcv, inst.perm))()
+    val unfold = Unfold(utils.getPredicate(q.s.program, inst.loc.rcv, inst.perm))()
 
 
     // Exchange list(x) with list(x.next) in the state
@@ -277,7 +277,7 @@ object PackageRule extends AbductionRule[MagicWand] {
     val g1 = q.goal.filterNot(_ == inst) :+ inst.right
 
     // We find the proof script later on, so we leave it empty here
-    // TODO we have to seperate proof script statements from normal statements
+    // TODO we have to separate proof script statements from normal statements
     val stmts = q.foundStmts :+ Package(inst, Seqn(Seq(), Seq())())()
 
     producer.produce(q.s, freshSnap, inst.left, pve, q.v)((s1, v1) => {

src/main/scala/biabduction/Abstraction.scala

@@ -30,7 +30,7 @@ object AbstractionListFold extends AbstractionRule[Map[Exp, Seq[Exp]]] {
 
   override protected def apply(q: AbstractionQuestion, inst: Map[Exp, Seq[Exp]])(Q: AbstractionQuestion => VerificationResult): VerificationResult = {
     val all = inst.values.flatten.toSeq
-    val exps1 = q.exps.filterNot(all.contains) ++ inst.keys.map { head => getPredicate(q.s.program, head, FullPerm()()) }
+    val exps1 = q.exps.filterNot(all.contains) ++ inst.keys.map { head => utils.getPredicate(q.s.program, head, FullPerm()()) }
     Q(q.copy(exps = exps1))
   }
 }
@@ -72,7 +72,6 @@ object AbstractionJoin extends AbstractionRule[Seq[(MagicWand, MagicWand)]] {
     } else {
       Q(Some(pairs))
     }
-
   }
 
   override protected def apply(q: AbstractionQuestion, inst: Seq[(MagicWand, MagicWand)])(Q: AbstractionQuestion => VerificationResult): VerificationResult = {

src/main/scala/biabduction/BiAbduction.scala

@@ -9,6 +9,13 @@ import viper.silver.ast._
 import viper.silver.verifier.errors.Internal
 import viper.silver.verifier.{DummyReason, PartialVerificationError}
 
+// TODO we want to continue execution if we abduce successfully. Idea:
+// - Hook into the "Try or Fail" methods
+// - Instead of actually failing, do bi-abduction
+// - track the results somewhere
+// - produce the precondition, execute the statements, and continue execution
+// - At the end, do abstraction on all the found preconditions. Find the necessary statements for the abstractions
+
 object BiAbductionSolver {
 
   def solve(q: SiliconAbductionQuestion): String = {
@@ -27,12 +34,12 @@ object BiAbductionSolver {
       val pres = AbstractionApplier.apply(AbstractionQuestion(q1.foundPrecons, q1.s)).exps
 
       // TODO if some path conditions already contain Ands, then we might reject clauses that we could actually handle
-      val bcs = BigAnd(q1.v.decider.pcs.branchConditionExps.collect { case Some(e) if varTrans.transformToInputs(e).isDefined => varTrans.transformToInputs(e).get })
+      val bcs = BigAnd(q1.v.decider.pcs.branchConditionExps.collect { case Some(e) if varTrans.transformVars(e).isDefined => varTrans.transformVars(e).get })
 
       // TODO Weak transformation of statements to original variables
 
       val rt = pres.map { (e: Exp) =>
-        (varTrans.transformToInputs(e), bcs) match {
+        (varTrans.transformVars(e), bcs) match {
           case (Some(e1), TrueLit()) => e1.toString()
           case (Some(e1), bcs) => Implies(bcs, e1)().toString()
           case _ => "Could not be transformed to inputs: " + e.toString()
@@ -68,6 +75,24 @@ trait RuleApplier[S] {
   }
 }
 
+object utils {
+  // TODO We currently assume that there is only one predicate and one field
+  def getPredicate(p: Program, rec: Exp, e: Exp): PredicateAccessPredicate = {
+    PredicateAccessPredicate(PredicateAccess(Seq(rec), p.predicates.head.name)(), e)()
+  }
+
+  def getNextAccess(p: Program, rec: Exp, perm: Exp): FieldAccessPredicate = {
+    FieldAccessPredicate(FieldAccess(rec, p.fields.head)(), perm)()
+  }
+
+  def getVars(t: Term, g: Store): Seq[AbstractLocalVar] = {
+    g.values.collect({ case (v, t1) if t1 == t => v }).toSeq
+  }
+
+  def getField(name: BasicChunkIdentifier, p: Program) = {
+    p.fields.find(_.name == name.name).get
+  }
+}
 
 
 trait BiAbductionRule[S, T] {
@@ -85,85 +110,68 @@ trait BiAbductionRule[S, T] {
 
   protected def apply(q: S, inst: T)(Q: S => VerificationResult): VerificationResult
 
-  // TODO We currently assume that there is only one predicate and one field
-  protected def getPredicate(p: Program, rec: Exp, e: Exp): PredicateAccessPredicate = {
-    PredicateAccessPredicate(PredicateAccess(Seq(rec), p.predicates.head.name)(), e)()
-  }
-
-  protected def getNextAccess(p: Program, rec: Exp, e: Exp): FieldAccessPredicate = {
-    FieldAccessPredicate(FieldAccess(rec, p.fields.head)(), e)()
-  }
 }
 
 case class varTransformer(s: State, targets: Seq[LocalVar], strict: Boolean = true) {
 
-  private def getVars(t: Term, g: Store): Seq[AbstractLocalVar] = {
-    g.values.collect({ case (v, t1) if t1 == t => v }).toSeq
-  }
-
-  private def getField(name: BasicChunkIdentifier) = {
-    s.program.fields.find(_.name == name.name).get
-  }
-
-
   // TODO the original work introduces logical vars representing the original input values. They attempt (I think) to transform
   // to these vars. See the "Rename" algorithm in the original paper.
   // At the end, they can be re-replaced by the input parameters. Do we have to do this?
-  def transformToInputs(e: Exp): Option[Exp] = {
+  def transformVars(e: Exp): Option[Exp] = {
 
     val targetMap: Map[Term, LocalVar] = targets.view.map(localVar => s.g.get(localVar).get -> localVar).toMap
 
     // Find the Vars in the Store which point to the same symbolic value as each input
-    val aliases = targetMap.keys.flatMap { t: Term => getVars(t, s.g).map(_ -> targetMap(t)) }.toMap
+    val aliases = targetMap.keys.flatMap { t: Term => utils.getVars(t, s.g).map(_ -> targetMap(t)) }.toMap
     //s.g.values.collect({ case (v: LocalVar, t: Term) if inputs.contains(t) && !inputs.values.toSeq.contains(v) => v -> inputs(t) })
 
     // Find field chunks where the something points to an input var
     val pointers = s.h.values.collect { case c: BasicChunk if c.resourceID == FieldID && targetMap.contains(c.snap) =>
-      getVars(c.args.head, s.g).map(FieldAccess(_, getField(c.id))() -> targetMap(c.snap))
+      utils.getVars(c.args.head, s.g).map(FieldAccess(_, utils.getField(c.id, s.program))() -> targetMap(c.snap))
     }.flatten.toMap
 
     e match {
       case lc: LocalVar =>
         val lcTra = aliases.get(lc)
-        if(lcTra.isEmpty && !strict) Some(lc) else lcTra
+        if (lcTra.isEmpty && !strict) Some(lc) else lcTra
 
-      case Not(e1) => transformToInputs(e1).map(Not(_)())
+      case Not(e1) => transformVars(e1).map(Not(_)())
 
       case And(e1, e2) =>
-        val tra1 = transformToInputs(e1)
-        val tra2 = transformToInputs(e2)
+        val tra1 = transformVars(e1)
+        val tra2 = transformVars(e2)
         if (tra1.isEmpty || tra2.isEmpty) None else Some(And(tra1.get, tra2.get)())
 
       case NeCmp(e1, e2) =>
-        val tra1 = transformToInputs(e1)
-        val tra2 = transformToInputs(e2)
+        val tra1 = transformVars(e1)
+        val tra2 = transformVars(e2)
         if (tra1.isEmpty || tra2.isEmpty) None else Some(NeCmp(tra1.get, tra2.get)())
 
 
       case EqCmp(e1, e2) =>
-        val tra1 = transformToInputs(e1)
-        val tra2 = transformToInputs(e2)
+        val tra1 = transformVars(e1)
+        val tra2 = transformVars(e2)
         if (tra1.isEmpty || tra2.isEmpty) None else Some(EqCmp(tra1.get, tra2.get)())
 
 
       case nl: NullLit => Some(nl)
 
       case fa: FieldAccess =>
-        if(pointers.contains(fa)){
+        if (pointers.contains(fa)) {
           Some(pointers(fa))
         } else {
-          transformToInputs(fa.rcv).map{rcv1: Exp => fa.copy(rcv = rcv1)(fa.pos, fa.info, fa.errT)}
+          transformVars(fa.rcv).map { rcv1: Exp => fa.copy(rcv = rcv1)(fa.pos, fa.info, fa.errT) }
         }
 
-      case fap: FieldAccessPredicate => transformToInputs(fap.loc).collect{case e1: FieldAccess => fap.copy(loc = e1)(fap.pos, fap.info, fap.errT)}
+      case fap: FieldAccessPredicate => transformVars(fap.loc).collect { case e1: FieldAccess => fap.copy(loc = e1)(fap.pos, fap.info, fap.errT) }
 
-      case pa: PredicateAccess => val traArgs = pa.args.map(transformToInputs)
-        if(traArgs.contains(None)) None else Some(pa.copy(args = traArgs.map(_.get))(pa.pos, pa.info, pa.errT))
+      case pa: PredicateAccess => val traArgs = pa.args.map(transformVars)
+        if (traArgs.contains(None)) None else Some(pa.copy(args = traArgs.map(_.get))(pa.pos, pa.info, pa.errT))
 
-      case pap: PredicateAccessPredicate => transformToInputs(pap.loc).collect{case e1: PredicateAccess => pap.copy(loc = e1)(pap.pos, pap.info, pap.errT) }
+      case pap: PredicateAccessPredicate => transformVars(pap.loc).collect { case e1: PredicateAccess => pap.copy(loc = e1)(pap.pos, pap.info, pap.errT) }
 
-      case MagicWand(e1, e2) => val tra1 = transformToInputs(e1)
-        val tra2 = transformToInputs(e2)
+      case MagicWand(e1, e2) => val tra1 = transformVars(e1)
+        val tra2 = transformVars(e2)
         if (tra1.isEmpty || tra2.isEmpty) None else Some(MagicWand(tra1.get, tra2.get)())
     }
   }

src/main/scala/biabduction/Framing.scala

@@ -0,0 +1,37 @@
+package biabduction
+
+import viper.silicon.biabduction.{utils, varTransformer}
+import viper.silicon.resources.FieldID
+import viper.silicon.state.{BasicChunk, State}
+import viper.silicon.verifier.Verifier
+import viper.silver.ast.{Exp, FieldAccessPredicate, Method, PredicateAccessPredicate}
+
+// TODO This is a bad name for what is actually happening
+
+object Framing {
+
+  def generatePostconditions(s: State, v: Verifier): Seq[Exp] = {
+
+    val formals = s.currentMember match {
+      case Some(m: Method) => m.formalArgs.map(_.localVar) ++ m.formalReturns.map(_.localVar)
+      case _ => Seq()
+    }
+
+    val posts: Seq[Exp] = s.h.values.collect { case c: BasicChunk =>
+      if (c.resourceID == FieldID) {
+        utils.getNextAccess(s.program, c.args.head, c.perm)
+      } else {
+        utils.getPredicate(s.program, c.args.head, c.perm)
+      }
+    }
+
+    val tra = varTransformer(s, formals)
+    posts.map(_.map(tra.transformVars(_))
+
+  }
+
+
+}
+
+
+}

src/main/scala/supporters/MethodSupporter.scala

@@ -112,6 +112,7 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent { v: Verif
                executionFlowController.locally(s2a, v2)((s3, v3) =>  {
                   exec(s3, body, v3)((s4, v4) =>
                     consumes(s4, posts, postViolated, v4)((_, _, _) =>
+                      // TODO nklose This is where we should hook in to infer postconditions
                       Success()))}) }  )})})
 
       v.decider.resetProverOptions()