fixed loop stuff

src/main/scala/biabduction/Abduction.scala

@@ -215,6 +215,7 @@ object AbductionFold extends AbductionRule {
           // TODO nklose if the predicate is conditional in a weird way, then this might be wrong?
           case Some((field, chunk)) =>
             val wildcards = q.s.constrainableARPs -- q.s.constrainableARPs
+
             val fargs = pred.formalArgs.map(_.localVar)
             val eArgs = a.loc.args
             val formalsToActuals: Map[ast.LocalVar, ast.Exp] = fargs.zip(eArgs).to(Map)
@@ -371,6 +372,7 @@ object AbductionApply extends AbductionRule {
   }
 }
 
+// TODO nklose this should actually do a package after simulating it. Then we do not have issues with the correct state at the end
 object AbductionPackage extends AbductionRule {
 
   override def apply(q: AbductionQuestion)(Q: Option[AbductionQuestion] => VerificationResult): VerificationResult = {

src/main/scala/biabduction/Abstraction.scala

@@ -1,6 +1,6 @@
 package viper.silicon.biabduction
 
-import viper.silicon.interfaces.VerificationResult
+import viper.silicon.interfaces.{Success, VerificationResult}
 import viper.silicon.interfaces.state.Chunk
 import viper.silicon.resources._
 import viper.silicon.rules._
@@ -41,12 +41,34 @@ object AbstractionFold extends AbstractionRule {
         val wildcards = q.s.constrainableARPs -- q.s.constrainableARPs
         executionFlowController.tryOrElse0(q.s, q.v) {
           (s1, v1, T) =>
+
+            val fargs = pred.formalArgs.map(_.localVar)
+            val eArgs = q.varTran.transformTerm(chunk.args.head)
+            val formalsToActuals: Map[LocalVar, Exp] = fargs.zip(eArgs).to(Map)
+            val reasonTransformer = (n: viper.silver.verifier.errors.ErrorNode) => n.replace(formalsToActuals)
+            val pveTransformed = pve.withReasonNodeTransformed(reasonTransformer)
+
             // TODO nklose this can branch
-            predicateSupporter.fold(s1, pred, List(chunk.args.head), None, terms.FullPerm, Some(FullPerm()()), wildcards, pve, v1)(T)
-        } { 
-          (s2, v2) => Q(Some(q.copy(s = s2, v = v2))) 
+            predicateSupporter.fold(s1, pred, List(chunk.args.head), None, terms.FullPerm, Some(FullPerm()()), wildcards, pveTransformed, v1)(T)
+        } {
+          (s2, v2) => Q(Some(q.copy(s = s2, v = v2)))
         } {
-          _ => checkChunks(rest, q)(Q)
+          f =>
+            executionFlowController.tryOrElse0(q.s, q.v) {
+              (s3, v3, T) =>
+                BiAbductionSolver.solveAbduction(s3, v3, f, None) { (s4, res, v4) =>
+                  res.state match {
+                    case Seq() => T(s4, v4)
+                    case _ => f
+                  }
+                }
+            } {
+              (s5, v5) =>
+                Q(Some(q.copy(s = s5, v = v5)))
+            } {
+              f =>
+                checkChunks(rest, q)(Q)
+            }
         }
     }
   }
@@ -60,6 +82,7 @@ object AbstractionFold extends AbstractionRule {
 
 object AbstractionPackage extends AbstractionRule {
 
+  // TODO nklose we should only trigger on fields for which there is a recursive predicate call
   @tailrec
   private def findWandFieldChunk(chunks: Seq[Chunk], q: AbstractionQuestion): Option[(Exp, BasicChunk)] = {
     chunks match {
@@ -76,24 +99,25 @@ object AbstractionPackage extends AbstractionRule {
   override def apply(q: AbstractionQuestion)(Q: Option[AbstractionQuestion] => VerificationResult): VerificationResult = {
 
     findWandFieldChunk(q.s.h.values.toSeq, q) match {
-    case None => Q(None)
-    case Some((lhsArg, chunk)) =>
-      val pred = q.fields(abductionUtils.getField(chunk.id, q.s.program))
-      val lhs = PredicateAccessPredicate(PredicateAccess(Seq(lhsArg), pred)(NoPosition, NoInfo, NoTrafos), FullPerm()())()
-      val rhsArg = q.varTran.transformTerm(chunk.args.head).get
-      val rhs = PredicateAccessPredicate(PredicateAccess(Seq(rhsArg), pred)(NoPosition, NoInfo, NoTrafos), FullPerm()())()
-      val wand = MagicWand(lhs, rhs)()
-      executor.exec(q.s, Assert(wand)(), q.v) {
-        (s1, sv) =>
-          Q(Some(q.copy(s = s1, v = sv)))}
+      case None => Q(None)
+      case Some((lhsArg, chunk)) =>
+        val pred = q.fields(abductionUtils.getField(chunk.id, q.s.program))
+        val lhs = PredicateAccessPredicate(PredicateAccess(Seq(lhsArg), pred)(NoPosition, NoInfo, NoTrafos), FullPerm()())()
+        val rhsArg = q.varTran.transformTerm(chunk.args.head).get
+        val rhs = PredicateAccessPredicate(PredicateAccess(Seq(rhsArg), pred)(NoPosition, NoInfo, NoTrafos), FullPerm()())()
+        val wand = MagicWand(lhs, rhs)()
+        executor.exec(q.s, Assert(wand)(), q.v) {
+          (s1, v1) =>
+            Q(Some(q.copy(s = s1, v = v1)))
+        }
     }
   }
 }
 
 object AbstractionJoin extends AbstractionRule {
 
   override def apply(q: AbstractionQuestion)(Q: Option[AbstractionQuestion] => VerificationResult): VerificationResult = {
-    val wands = q.s.h.values.collect { case wand: MagicWandChunk => q.varTran.transformChunk(wand) }.collect{case Some(wand: MagicWand) => wand}.toSeq
+    val wands = q.s.h.values.collect { case wand: MagicWandChunk => q.varTran.transformChunk(wand) }.collect { case Some(wand: MagicWand) => wand }.toSeq
     val pairs = wands.combinations(2).toSeq
     pairs.collectFirst {
       case wands if wands(0).right == wands(1).left => (wands(0), wands(1))
@@ -102,7 +126,8 @@ object AbstractionJoin extends AbstractionRule {
       case None => Q(None)
       case (Some((w1, w2))) =>
         magicWandSupporter.packageWand(q.s, MagicWand(w1.left, w2.right)(), Seqn(Seq(Apply(w1)(), Apply(w2)()), Seq())(), pve, q.v) {
-          (s1, wandChunk, v1) => Q(Some(q.copy(s = s1.copy(h = s1.h.+(wandChunk)), v = v1)))
+          (s1, wandChunk, v1) =>
+            Q(Some(q.copy(s = s1.copy(h = s1.reserveHeaps.head.+(wandChunk)), v = v1)))
         }
     }
   }
@@ -111,14 +136,15 @@ object AbstractionJoin extends AbstractionRule {
 object AbstractionApply extends AbstractionRule {
 
   override def apply(q: AbstractionQuestion)(Q: Option[AbstractionQuestion] => VerificationResult): VerificationResult = {
-    val wands = q.s.h.values.collect { case wand: MagicWandChunk => q.varTran.transformChunk(wand) }.collect {case Some(wand: MagicWand) => wand}
-    val targets = q.s.h.values.collect { case c: BasicChunk if !q.fixedChunks.contains(c) => q.varTran.transformChunk(c) }.collect {case Some(exp) => exp}.toSeq
+    val wands = q.s.h.values.collect { case wand: MagicWandChunk => q.varTran.transformChunk(wand) }.collect { case Some(wand: MagicWand) => wand }
+    val targets = q.s.h.values.collect { case c: BasicChunk if !q.fixedChunks.contains(c) => q.varTran.transformChunk(c) }.collect { case Some(exp) => exp }.toSeq
 
-    wands.collectFirst{case wand if targets.contains(wand.left) => wand } match {
+    wands.collectFirst { case wand if targets.contains(wand.left) => wand } match {
       case None => Q(None)
       case Some(wand) =>
         magicWandSupporter.applyWand(q.s, wand, pve, q.v) {
-          (s1, v1) => Q(Some(q.copy(s = s1, v = v1)))
+          (s1, v1) =>
+            Q(Some(q.copy(s = s1, v = v1)))
         }
     }
   }

src/main/scala/biabduction/BiAbduction.scala

@@ -6,7 +6,7 @@ import viper.silicon.interfaces.state.{Chunk, NonQuantifiedChunk}
 import viper.silicon.rules.consumer.consumes
 import viper.silicon.rules.{executionFlowController, executor, producer}
 import viper.silicon.state._
-import viper.silicon.state.terms.Term
+import viper.silicon.state.terms.{Term, True}
 import viper.silicon.utils.ast.BigAnd
 import viper.silicon.utils.freshSnap
 import viper.silicon.verifier.Verifier
@@ -79,10 +79,11 @@ case class AbductionSuccess(s: State, v: Verifier, pcs: PathConditionStack, stat
   def getStatements(bcExps: Seq[Option[Exp]]): Option[Seq[Stmt]] = {
     if (stmts.isEmpty) {
       Some(Seq())
-    } else if (bcExps.contains(None)) {
-      None
+      // TODO nklose we are over approximating here, this is probably wrong in general but good in practise
+    //} else if (bcExps.contains(None)) {
+    //  None
     } else {
-      val con = BigAnd(bcExps.map { case Some(e) => e })
+      val con = BigAnd(bcExps.collect { case Some(e) => e })
       con match {
         case _: TrueLit => Some(stmts)
         case _ => Some(Seq(If(con, Seqn(stmts, Seq())(), Seqn(Seq(), Seq())())()))
@@ -153,21 +154,27 @@ case class LoopInvariantSuccess(s: State, v: Verifier, invs: Seq[Exp] = Seq(), l
 case class FramingSuccess(s: State, v: Verifier, posts: Seq[Exp], stmts: Seq[Stmt], loc: Positioned, pcs: PathConditionStack, varTran: VarTransformer) extends BiAbductionSuccess {
   override def toString: String = "Successful framing"
 
-  def getBcExps(bcsTerms: Seq[Term]): Option[Exp] = {
-    val varTrans = VarTransformer(s, v, s.g.values, s.h)
+  def getBcExps(bcsTerms: Seq[Term], targetVars: Map[AbstractLocalVar, (Term, Option[Exp])]): Option[Exp] = {
+    val varTrans = VarTransformer(s, v, targetVars, s.h)
     val bcExps = bcsTerms.map { t => varTrans.transformTerm(t) }
+
+    // TODO this is possibly unsound but better in practise
+    Some(BigAnd(bcExps.collect { case Some(e) => e }))
+    /*
     if (bcExps.contains(None)) {
       None
     } else {
       Some(BigAnd(bcExps.map { case Some(e) => e }))
-    }
+    }*/
   }
 
 
   def addToMethod(m: Method, bcs: Seq[Term]): Option[Method] = {
     val prevPcs = v.decider.pcs
     v.decider.setPcs(pcs)
-    val bcExpsOpt = getBcExps(bcs)
+    val formals = m.formalArgs.map(_.localVar) ++ m.formalReturns.map(_.localVar)
+    val vars = s.g.values.collect { case (var2, t) if formals.contains(var2) => (var2, t) }
+    val bcExpsOpt = getBcExps(bcs, vars)
     v.decider.setPcs(prevPcs)
 
     bcExpsOpt.flatMap { bcExps =>
@@ -307,8 +314,7 @@ object BiAbductionSolver {
   def solveAbstraction(s: State, v: Verifier, fixedChunks: Seq[Chunk] = Seq())(Q: (State, Seq[Exp], Verifier) => VerificationResult): VerificationResult = {
     val q = AbstractionQuestion(s, v, fixedChunks)
     AbstractionApplier.applyRules(q) { q1 =>
-      val tra = VarTransformer(q1.s, q1.v, q1.s.g.values, q1.s.h)
-      val res = q1.s.h.values.collect { case c: NonQuantifiedChunk => tra.transformChunk(c) }.collect { case Some(e) => e }.toSeq
+      val res = VarTransformer(q1.s, q1.v, q1.s.g.values, q1.s.h).transformState(q1.s)
       Q(q1.s, res, q1.v)
     }
   }
@@ -358,7 +364,7 @@ object BiAbductionSolver {
     val abdReses = abductionUtils.getAbductionSuccesses(nf)
     val abdCases = abdReses.groupBy(res => (res.trigger, res.stmts, res.state)).flatMap {
       case (_, reses) =>
-        val unjoined = reses.map(res => (Seq(res), res.pcs.branchConditions))
+        val unjoined = reses.map(res => (Seq(res), res.pcs.branchConditions.distinct.filter(_ != True)))
         val joined = abductionUtils.joinBcs(unjoined)
         joined.map {
           case (reses, pcs) =>
@@ -373,21 +379,27 @@ object BiAbductionSolver {
     val frames = abductionUtils.getFramingSuccesses(nf)
     val frameCases = frames.groupBy(f => (f.posts, f.stmts)).flatMap {
       case (_, frs) =>
-        val unjoined = frs.map(fr => (Seq(fr), fr.pcs.branchConditions))
+        val unjoined = frs.map(fr => (Seq(fr), fr.pcs.branchConditions.distinct.filter(_ != True)))
         val joined = abductionUtils.joinBcs(unjoined)
         joined.map {
           case (frs, pcs) =>
             frs.head -> pcs
         }
     }
-    frameCases.foldLeft[Option[Method]](Some(m))((m1, res) => m1.flatMap { mm => res._1.addToMethod(mm, res._2) })
+
+    // We get a framing result for every branch that reaches the end. So we can remove bcs that hold in every case, as they
+    // are guaranteed to hold.
+    val allTerms = frameCases.values
+    val alwaysTerms = allTerms.head.filter {t => allTerms.forall(_.contains(t))}
+
+    frameCases.foldLeft[Option[Method]](Some(m))((m1, res) => m1.flatMap { mm => res._1.addToMethod(mm, res._2.diff(alwaysTerms)) })
   }
 
   def resolveLoopInvResults(m: Method, nf: NonFatalResult): Option[Method] = {
     val invs = abductionUtils.getInvariantSuccesses(nf)
     val invCases = invs.groupBy(inv => (inv.loop, inv.invs)).flatMap {
       case (_, invs) =>
-        val unjoined = invs.map(inv => (Seq(inv), inv.pcs.branchConditions))
+        val unjoined = invs.map(inv => (Seq(inv), inv.pcs.branchConditions.distinct.filter(_ != True)))
         val joined = abductionUtils.joinBcs(unjoined)
         joined.map {
           case (invs, pcs) =>
@@ -508,4 +520,5 @@ object abductionUtils {
       case _ => None
     }
   }
+
 }

src/main/scala/biabduction/Invariant.scala

@@ -50,13 +50,19 @@ object LoopInvariantSolver {
               case f: Failure => f
               case abdRes: NonFatalResult =>
                 // TODO nklose we do not guarantee length 1 here anymore
-                val abd = abductionUtils.getAbductionSuccesses(abdRes).head
+                abductionUtils.getAbductionSuccesses(abdRes) match {
+                  case Seq(AbductionSuccess(s5, v5, _, Seq(), _, _)) =>
+                    val unfolded = VarTransformer(s5, v5, s5.g.values, s5.h).transformState(s5)
+                    Q(unfolded)
+                }
+                /*
                 val unfolds = abd.stmts.collect { case Unfold(pa) => (pa.toString -> pa.loc.predicateBody(s.program, Set()).get) }.toMap
                 val unfolded = inverted.map {
                   case inv: PredicateAccessPredicate => unfolds.getOrElse(inv.toString, inv)
                   case inv => inv
                 }
                 Q1(unfolded)
+                */
             }
         }
       }
@@ -100,13 +106,9 @@ object LoopInvariantSolver {
                           loopConBcs: Seq[Term] = Seq(),
                           iteration: Int = 1): VerificationResult = {
 
-
     // Produce the already known invariants. They are consumed at the end of the loop body, so we need to do this every iteration
     produces(s, freshSnap, loopHead.invs, ContractNotWellformed, v) { (sPreInv, vPreInv) =>
 
-      //var loopCondTerm: Option[Term] = None
-      //val oldPcs = vPreInv.decider.pcs.branchConditions
-
       // Run the loop the first time to check whether we abduce any new state
       executionFlowController.locally(sPreInv, vPreInv) { (sFP, vFP) =>
 
@@ -125,27 +127,15 @@ object LoopInvariantSolver {
           // We assume there is only one loop internal edge
           val loopConExp = loopEdges.head.asInstanceOf[ConditionalEdge[Stmt, Exp]].condition
 
-          //evaluator.eval(sPreInv0, loopConExp, pve, vPreInv0) { (sPreInv, loopConTerm, _, vPreInv) =>
-
-          //val newLoopCons = loopConBcs :+ loopCondTerm.get
-
           val abdReses = abductionUtils.getAbductionSuccesses(nonf)
           val preStateVars = sPreInv.g.values.filter { case (v, _) => origVars.contains(v) }
           val newStateOpt = abdReses.flatMap { case abd => abd.getPreconditions(preStateVars, sPreInv.h, Seq()).get }
 
-          //val newStateHeadOpt = abdReses.collect { case abd if abd.trigger.contains(loopConExp) => abd.toPrecondition(preStateVars, sPreInv.h) }
-          //if (newStateOpt.contains(None)) {
-          //  return Failure(pve dueTo DummyReason)
-          //}
-
           // We still need to remove the current loop condition
           val newState = newStateOpt.map(_.transform {
             case im: Implies if im.left == loopConExp => im.right
           })
 
-          //val newStateHead = newStateHeadOpt.flatMap(_.get)
-          //val abductionResults = newStateHead ++ newStateBody
-
           // Do the second pass so that we can compare the state at the end of the loop with the state at the beginning
           // Get the state at the beginning of the loop with the abduced things added
           producer.produces(sPreInv, freshSnap, newState, pveLam, vPreInv) { (sPreAbd0, vPreAbd0) =>
@@ -158,14 +148,15 @@ object LoopInvariantSolver {
               }, sPreAbd, vPreAbd) { chunks =>
 
                 val allChunks = chunks.keys
-                //val fixedChunks = chunks.collect({ case (c, loc) if newStateHead.contains(loc) => c }).toSeq
 
                 val newPreState0 = sPreAbd.copy(h = q.preHeap.+(Heap(allChunks)))
                 BiAbductionSolver.solveAbstraction(newPreState0, vPreAbd) {
                   (newPreState, newPreAbstraction0, newPreV) =>
 
                     val preTran = VarTransformer(newPreState, newPreV, preStateVars, newPreState.h)
                     val newPreAbstraction = newPreAbstraction0.map(e => preTran.transformExp(e, strict = false).get)
+
+
 
                     executor.follows(sPreAbd, loopEdges, pveLam, vPreAbd, joinPoint)((sPost, vPost) => {
 
@@ -174,6 +165,11 @@ object LoopInvariantSolver {
                         val postStateVars = sPostAbs.g.values.filter { case (v, _) => origVars.contains(v) }
                         val postTran = VarTransformer(sPostAbs, vPostAbs, postStateVars, sPostAbs.h)
                         val postAbstraction = postAbstraction0.map(e => postTran.transformExp(e, strict = false).get)
+
+                        println("\nIteration: " + iteration)
+                        println("New state:\n    " + newState.mkString("\n    "))
+                        println("New pre abstraction:\n    " + newPreAbstraction.mkString("\n    "))
+                        println("New post abstraction:\n    " + postAbstraction.mkString("\n    "))
 
                         // If the pushed forward abstraction is the same as the previous one, we are done
                         if (newPreAbstraction == q.preAbstraction && postAbstraction == q.postAbstraction) {
@@ -198,7 +194,6 @@ object LoopInvariantSolver {
               }
             }
           }
-        //}
       }
     }
   }