Revamped loops for new abstraction

src/main/scala/Config.scala

@@ -820,7 +820,7 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
 
   val enableDebugging: ScallopOption[Boolean] = opt[Boolean]("enableDebugging",
     descr = "Enable debugging mode",
-    default = Some(true), // Set to true for biabduction testing
+    default = Some(false),
     noshort = true
   )
 

src/main/scala/biabduction/Abduction.scala

@@ -116,7 +116,7 @@ object AbductionRemove extends AbductionRule {
   private def consumeChunks(chunks: Seq[BasicChunk], q: AbductionQuestion)(Q: AbductionQuestion => VerificationResult): VerificationResult = {
     chunks match {
       case Seq() => Q(q)
-      case c :: cs =>
+      case c +: cs =>
         val c1 = findChunk[BasicChunk](q.s.h.values, c.id, c.args, q.v).get
         val resource: Resource = c.resourceID match {
           case PredicateID => q.s.program.predicates.head
@@ -191,7 +191,7 @@ object AbductionFold extends AbductionRule {
   protected def findFirstFieldChunk(locs: Seq[FieldAccess], q: AbductionQuestion)(Q: Option[(FieldAccess, BasicChunk)] => VerificationResult): VerificationResult = {
     locs match {
       case Seq() => Q(None)
-      case loc :: rest =>
+      case loc +: rest =>
         checkChunk(loc, q.s, q.v, q.lostAccesses) {
           case Some(chunk) => Q(Some(loc, chunk))
           case None => findFirstFieldChunk(rest, q)(Q)

src/main/scala/biabduction/Abstraction.scala

@@ -7,6 +7,8 @@ import viper.silicon.state._
 import viper.silicon.verifier.Verifier
 import viper.silver.ast._
 
+import scala.annotation.tailrec
+
 object AbstractionApplier extends RuleApplier[AbstractionQuestion] {
   override val rules: Seq[AbstractionRule] = Seq(AbstractionFold, AbstractionPackage, AbstractionJoin, AbstractionApply)
 }
@@ -16,7 +18,7 @@ case class AbstractionQuestion(s: State, v: Verifier) {
   // TODO we assume each field only appears in at most one predicate
   def fields: Map[Field, Predicate] = s.program.predicates.flatMap { pred => pred.body.get.collect { case fa: FieldAccessPredicate => (fa.loc.field, pred) } }.toMap
 
-  def varTran = VarTransformer(s, v, s.g.values, Heap())
+  def varTran: VarTransformer = VarTransformer(s, v, s.g.values, Heap())
 
   def isTriggerField(bc: BasicChunk): Boolean = {
     bc.resourceID match {
@@ -33,7 +35,7 @@ object AbstractionFold extends AbstractionRule {
   private def checkChunks(chunks: Seq[BasicChunk], q: AbstractionQuestion)(Q: Option[AbstractionQuestion] => VerificationResult): VerificationResult = {
     chunks match {
       case Seq() => Q(None)
-      case chunk :: rest =>
+      case chunk +: rest =>
         val pred = q.fields(abductionUtils.getField(chunk.id, q.s.program))
         val wildcards = q.s.constrainableARPs -- q.s.constrainableARPs
         executionFlowController.tryOrElse0(q.s, q.v) {
@@ -52,16 +54,16 @@ object AbstractionFold extends AbstractionRule {
 }
 
 
-// TODO nklose Never fold. Instead, check if there exists a var in the state so that the field access is equal to it. If so, then we can package where the var gives us the lhs.
 object AbstractionPackage extends AbstractionRule {
 
+  @tailrec
   private def findWandFieldChunk(chunks: Seq[BasicChunk], q: AbstractionQuestion): Option[(Exp, BasicChunk)] = {
     chunks match {
       case Seq() => None
-      case chunk :: rest =>
-        q.varTran.transformChunk(chunk) match {
+      case chunk +: rest =>
+        q.varTran.transformTerm(chunk.snap) match {
           case None => findWandFieldChunk(rest, q)
-          case Some(lhs) => Some((lhs, chunk))
+          case Some(snap) => Some((snap, chunk))
         }
     }
   }
@@ -86,16 +88,16 @@ object AbstractionPackage extends AbstractionRule {
 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) }.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))
       case wands if wands(1).right == wands(0).left => (wands(1), wands(0))
     } match {
       case None => Q(None)
       case (Some((w1, w2))) =>
-        magicWandSupporter.packageWand(q.s, MagicWand(w1.left, w2.right)(), Seq(Apply(w1), Apply(w2)), pve, q.v) {
-          (s1, v1) => Q(Some(q.copy(s = s1, v = v1)))
+        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)))
         }
     }
   }
@@ -111,7 +113,7 @@ object AbstractionApply extends AbstractionRule {
       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

@@ -2,6 +2,7 @@ package viper.silicon.biabduction
 
 import viper.silicon.decider.PathConditionStack
 import viper.silicon.interfaces._
+import viper.silicon.interfaces.state.NonQuantifiedChunk
 import viper.silicon.rules.{executionFlowController, executor, producer}
 import viper.silicon.state._
 import viper.silicon.state.terms.Term
@@ -152,23 +153,22 @@ object BiAbductionSolver {
 
 
 
-  def solveAbstraction(s: State, v: Verifier)(Q: (State, Verifier, Seq[Exp]) => VerificationResult): VerificationResult = {
-    val q = AbstractionQuestion(s1, v1)
-    val res = AbstractionApplier.applyRules(q) { q1 =>
-      Success(solveFraming(q1.s, q1.v, q1.s.g.values))
+  def solveAbstraction(s: State, v: Verifier)(Q: (State, Seq[Exp], Verifier) => VerificationResult): VerificationResult = {
+    val q = AbstractionQuestion(s, v)
+    AbstractionApplier.applyRules(q) { q1 =>
+      Success(Some(solveFraming(q1.s, q1.v, q1.s.g.values)))
     } match {
-      case NonFatalResult =>
+      case res: NonFatalResult =>
         val exps = abductionUtils.getFramingSuccesses(res).head
-        Q(exps.s, exps.v, exps.posts)
+        Q(exps.s, exps.posts, exps.v)
     }
   }
 
-  // TODO nklose we would like to abstract postconditions, but we cannot do it here anymore! We call this from an abstraction rule
-  // So we have to do this only where we generate the postconditions. 
+  // This does not do abstraction, but just transforms state back into expressions.
   def solveFraming(s: State, v: Verifier, postVars: Map[AbstractLocalVar, (Term, Option[Exp])], loc: Position = NoPosition, ignoredBcs: Seq[Exp] = Seq()): FramingSuccess = {
 
     val tra = VarTransformer(s, v, postVars, s.h)
-    val res = s.h.values.collect { case c: BasicChunk => tra.transformChunk(c) }.collect { case Some(e) => e }.toSeq
+    val res = s.h.values.collect { case c: NonQuantifiedChunk => tra.transformChunk(c) }.collect { case Some(e) => e }.toSeq
     val bcs = v.decider.pcs.branchConditions.map { term => tra.transformTerm(term) }.collect { case Some(e) if e != TrueLit()() && !ignoredBcs.contains(e) => e }.toSet
     val posts = res.map { e =>
       if (bcs.isEmpty) {