did some stuff I guess

src/main/scala/biabduction/Abduction.scala

@@ -309,6 +309,7 @@ object AbductionUnfold extends AbductionRule {
       case Some(a: FieldAccessPredicate) =>
         val g1 = q.goal.filterNot(a == _)
 
+
         // If we fail for a, then we recurse and try for other fields
         val R = () => apply(q.copy(goal = g1)) {
           case Some(q2) => Q(Some(q2.copy(goal = a +: q2.goal)))
@@ -345,7 +346,8 @@ object AbductionApply extends AbductionRule {
         // chunk is our goal, so the rule can be applied
         evals(q.s, subexps, _ => pve, q.v)((s1, args, _, v1) => {
           val matchingWand = s1.h.values.collect {
-            case m: MagicWandChunk if m.id.ghostFreeWand.structure(s1.program).right == goalStructure.right && m.args.takeRight(args.length) == args =>
+            // If the wand in the state contains our goal in the right-hand-side, then we would like to apply the wand
+            case m: MagicWandChunk if m.id.ghostFreeWand.structure(s1.program).right.contains(goalStructure.right) && m.args.takeRight(args.length) == args =>
               // If we find a matching wand, we have to find an expression representing the left hand side of the wand
               val lhsTerms = m.args.dropRight(args.length)
               val varTransformer = VarTransformer(s1, v1, s1.g.values, s1.h)
@@ -354,10 +356,10 @@ object AbductionApply extends AbductionRule {
                 None
               } else {
                 val formalLhsArgs = m.id.ghostFreeWand.subexpressionsToEvaluate(s1.program).dropRight(args.length)
-                val lhs = m.id.ghostFreeWand.left.transform {
+                val wand = m.id.ghostFreeWand.transform {
                   case n if formalLhsArgs.contains(n) => lhsArgs(formalLhsArgs.indexOf(n)).get // I am assuming that the subexpressions are unique, which should hold
                 }
-                Some(MagicWand(lhs, g)())
+                Some(wand)
               }
           }.collectFirst { case c if c.isDefined => c.get }
           matchingWand match {
@@ -370,7 +372,7 @@ object AbductionApply extends AbductionRule {
                 } else {
                   magicWandSupporter.applyWand(lhsRes.s, wand, pve, lhsRes.v) { (s2, v2) =>
                     val g1 = q.goal.filterNot(_ == wand.right)
-                    val stmts = q.foundStmts ++ lhsRes.foundStmts :+ Apply(wand)()
+                    val stmts = (q.foundStmts ++ lhsRes.foundStmts :+ Apply(wand)()).distinct // TODO there is a weird duplication here sometimes
                     val state = q.foundState ++ lhsRes.foundState
                     val lost = q.lostAccesses ++ lhsRes.lostAccesses
                     Q(Some(AbductionQuestion(s2, v2, g1, lost, state, stmts, q.trigger, q.stateAllowed)))
@@ -405,7 +407,7 @@ object AbductionPackage extends AbductionRule {
 
           // TODO This may produce things that are already in the state
           producer.produce(s0, freshSnap, wand.left, pve, v0) { (s1, v1) =>
-            val packQ = q.copy(s = s1, v = v1, goal = Seq(wand.right))
+            val packQ = q.copy(s = s1, v = v1, goal = wand.right.topLevelConjuncts)
             AbductionApplier.applyRules(packQ) { packRes =>
               if (packRes.goal.nonEmpty) {
                 Failure(pve dueTo(DummyReason))

src/main/scala/biabduction/Abstraction.scala

@@ -31,47 +31,33 @@ object AbstractionFold extends AbstractionRule {
     if (bc.resourceID != FieldID) None else {
       val field = abductionUtils.getField(bc.id, q.s.program)
 
-      q.s.program.predicates.collectFirst { case pred if pred.collect{case fa: FieldAccess => fa.field}.toSeq.contains(field) => pred }
+      q.s.program.predicates.collectFirst { case pred if pred.collect { case fa: FieldAccess => fa.field }.toSeq.contains(field) => pred }
     }
   }
 
   private def checkChunks(chunks: Seq[(BasicChunk, Predicate)], q: AbstractionQuestion)(Q: Option[AbstractionQuestion] => VerificationResult): VerificationResult = {
     chunks match {
       case _ if chunks.isEmpty => Q(None)
       case (chunk, pred) +: 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) {
-          (s1, v1, T) =>
+        q.varTran.transformTerm(chunk.args.head) match {
+          case None => checkChunks(rest, q)(Q)
+          case Some(eArgs) =>
 
-            //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)
 
-            val fold = Fold(PredicateAccessPredicate(PredicateAccess(Seq(eArgs.get), pred.name)(), FullPerm()())())()
-            executor.exec(s1, fold, v1, None, abdStateAllowed = false)(T)
-
-            // TODO nklose this can branch
-            //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)))
-        } {
+            executionFlowController.tryOrElse0(q.s, q.v) {
+              (s1, v1, T) =>
 
-          f => checkChunks(rest, q)(Q)
+                val fold = Fold(PredicateAccessPredicate(PredicateAccess(Seq(eArgs), pred.name)(), FullPerm()())())()
+                executor.exec(s1, fold, v1, None, abdStateAllowed = false)(T)
 
-            /*
-            executionFlowController.tryOrElse0(q.s, q.v) {
-              (s3, v3, T) =>
-                BiAbductionSolver.solveAbductionForError(s3, v3, f, stateAllowed = false, None) { T }
+              // TODO nklose this can branch
+              //predicateSupporter.fold(s1, pred, List(chunk.args.head), None, terms.FullPerm, Some(FullPerm()()), wildcards, pveTransformed, v1)(T)
             } {
-              (s5, v5) =>
-                Q(Some(q.copy(s = s5, v = v5)))
+              (s2, v2) => Q(Some(q.copy(s = s2, v = v2)))
             } {
               f =>
                 checkChunks(rest, q)(Q)
-            }*/
+            }
         }
     }
   }
@@ -91,12 +77,12 @@ object AbstractionPackage extends AbstractionRule {
     if (bc.resourceID != FieldID) None else {
 
       // TODO this fails if the sorts don't line up
-      q.s.g.termValues.collectFirst{ case (lv, term) if term.sort == bc.snap.sort && q.v.decider.check(terms.Equals(term, bc.snap), Verifier.config.checkTimeout())   => lv} match {
+      q.s.g.termValues.collectFirst { case (lv, term) if term.sort == bc.snap.sort && q.v.decider.check(terms.Equals(term, bc.snap), Verifier.config.checkTimeout()) => lv } match {
         case None => None
         case Some(lhsArgExp) =>
           val field = abductionUtils.getField(bc.id, q.s.program)
           // TODO we assume each field only appears in at most one predicate
-          val predOpt = q.s.program.predicates.collectFirst { case pred if pred.collect{case fa: FieldAccess => fa.field}.toSeq.contains(field) => pred }
+          val predOpt = q.s.program.predicates.collectFirst { case pred if pred.collect { case fa: FieldAccess => fa.field }.toSeq.contains(field) => pred }
           predOpt.flatMap { pred =>
             val recPredOpt = pred.collectFirst {
               case recPred@PredicateAccess(Seq(FieldAccess(_, field2)), _) if field == field2 => recPred

src/main/scala/biabduction/BiAbduction.scala

@@ -51,7 +51,7 @@ case class AbductionSuccess(s: State, v: Verifier, pcs: PathConditionStack, stat
         case None => body
         case Some(t: Stmt) if t == abductionUtils.dummyEndStmt =>
           addToInnerBody(body, finalStmt)
-          //Seqn(, body.scopedSeqnDeclarations)(body.pos, body.info, body.errT)
+        //Seqn(, body.scopedSeqnDeclarations)(body.pos, body.info, body.errT)
 
         case Some(t: Stmt) if abductionUtils.isEndOfLoopStmt(t) =>
           val loop = abductionUtils.getWhile(t.asInstanceOf[Label].invs.head, m)
@@ -60,16 +60,16 @@ case class AbductionSuccess(s: State, v: Verifier, pcs: PathConditionStack, stat
           body.transform { case stmt if stmt == loop => newLoop }
         case Some(t: Stmt) =>
           body.transform {
-            case stmt if stmt == t =>
+            case stmt: Stmt if stmt == t && stmt.pos == t.pos =>
               Seqn(finalStmt :+ t, Seq())(t.pos, t.info, t.errT)
           }
         case Some(e: Exp) => body.transform {
-          case ifStmt: If if ifStmt.cond == e => Seqn(stmts :+ ifStmt, Seq())(ifStmt.pos, ifStmt.info, ifStmt.errT)
-          case whileStmt: While if whileStmt.cond == e => Seqn(stmts :+ whileStmt, Seq())(whileStmt.pos, whileStmt.info, whileStmt.errT)
+          case ifStmt: If if ifStmt.cond == e && ifStmt.cond.pos == e.pos => Seqn(stmts :+ ifStmt, Seq())(ifStmt.pos, ifStmt.info, ifStmt.errT)
+          case whileStmt: While if whileStmt.cond == e && whileStmt.cond.pos == e.pos => Seqn(stmts :+ whileStmt, Seq())(whileStmt.pos, whileStmt.info, whileStmt.errT)
         }
       }
-
-      Some(m.copy(pres = (m.pres ++ pres.get).distinct, body = Some(newBody))(pos = m.pos, info = m.info, errT = m.errT))
+      
+      Some(m.copy(pres = abductionUtils.sortExps(pres.get ++ m.pres).distinct, body = Some(newBody))(pos = m.pos, info = m.info, errT = m.errT))
     }
   }
 
@@ -328,20 +328,16 @@ object BiAbductionSolver {
                 val newState = q1.foundState.reverse
                 val newStmts = q1.foundStmts
 
-                // TODO nklose created chunks can go away again before we finish abduction, due to a package or a fold
-                // We have to do this in place when the chunks are created and not here
-                //abductionUtils.findChunks(newLocs, q1.s, q1.v, Internal()) { newChunks =>
                 if (q1.v.decider.checkSmoke()) {
                   Success(Some(BiAbductionFailure(s, v, initPcs)))
                 } else {
-                  val newChunks = newState.collect { case (e, c: Some[BasicChunk]) => c.get }
+                  val newChunks = newState.collect { case (_, c: Some[BasicChunk]) => c.get }
                   val newOldHeaps = q1.s.oldHeaps.map { case (label, heap) => (label, heap + Heap(newChunks)) }
                   val s1 = q1.s.copy(oldHeaps = newOldHeaps)
                   val fieldChunks = newState.collect { case (fa: FieldAccessPredicate, c) => (c.get, fa.loc) }.toMap
                   val abd = AbductionSuccess(s1, q1.v, q1.v.decider.pcs.duplicate(), newState, newStmts, fieldChunks, trigger)
                   Success(Some(abd)) && Q(s1, q1.v)
                 }
-                //}
               } else {
                 f
               }
@@ -404,7 +400,7 @@ object BiAbductionSolver {
   def resolveAbductionResults(m: Method, nf: NonFatalResult): Option[Method] = {
     val abdReses = abductionUtils.getAbductionSuccesses(nf)
     val newMatches = abdReses.flatMap(_.newFieldChunks).toMap
-    val abdCases = abdReses.groupBy(res => (res.trigger, res.stmts, res.state))
+    val abdCases = abdReses.groupBy(res => (res.trigger.get, res.trigger.get.pos, res.stmts, res.state))
 
     // Try to join by bc terms
     val joinedCases = abdCases.flatMap {
@@ -444,7 +440,6 @@ object BiAbductionSolver {
     val formals = m.formalArgs.map(_.localVar) ++ m.formalReturns.map(_.localVar)
     val vars = frames.head.s.g.values.collect { case (var2, t) if formals.contains(var2) => (var2, t) }
 
-
     val cases = frames.map(f => (f.posts.diff(everyPosts), f.getBcExps(f.pcs.branchConditions.distinct.filter(_ != True), vars))).distinct
 
     // We can remove bcs that hold in every branch
@@ -477,6 +472,7 @@ object BiAbductionSolver {
 
     val invsSuccs = abductionUtils.getInvariantSuccesses(nf)
 
+    // there is an issue here if the same loop is repeated twice in the same method
     val reses = invsSuccs.groupBy(inv => inv.loop).map {
       case (loop, cases) =>
 
@@ -501,8 +497,8 @@ object BiAbductionSolver {
     Some(reses.foldLeft(m) { case (m1, (loop, inv)) =>
       val body = m1.body.get
       val newBody = body.transform {
-        case l: While if l.cond == loop.cond =>
-          l.copy(invs = l.invs ++ inv)(pos = l.pos, info = l.info, errT = l.errT)
+        case l: While if l.cond == loop.cond && l.cond.pos == loop.cond.pos =>
+          l.copy(invs = inv ++ l.invs)(pos = l.pos, info = l.info, errT = l.errT)
         case other => other
       }
       m1.copy(body = Some(newBody))(pos = m.pos, info = m.info, errT = m.errT)
@@ -601,18 +597,18 @@ object abductionUtils {
 
   def getWhile(condition: Exp, method: Method): While = {
     method.body.get.toSeq.collectFirst {
-      case w: While if w.cond == condition => w
+      case w: While if w.cond.pos == condition.pos => w
     }.get
   }
 
   def joinBcs[T](bcs: Seq[(Seq[T], Seq[Term])]): Seq[(Seq[T], Seq[Term])] = {
     bcs.combinations(2).collectFirst {
-      case Seq((a_res, a_pcs), (b_res, b_pcs)) if canJoin(a_pcs, b_pcs).isDefined =>
+      case Seq((a_res, a_pcs), (b_res, b_pcs)) if canJoin(a_pcs, b_pcs).isDefined => Seq((a_res, a_pcs), (b_res, b_pcs))
+    } match {
+      case Some(Seq((a_res, a_pcs), (b_res, b_pcs))) =>
         val rest = bcs.filter { case (c_res, _) => c_res != a_res && c_res != b_res }
         val joined = canJoin(a_pcs, b_pcs).get
         joinBcs(rest :+ (a_res ++ b_res, joined))
-    } match {
-      case Some(joined) => joined
       case None => bcs
     }
   }