Moved everything into consume

src/main/scala/biabduction/BiAbduction.scala

@@ -2,14 +2,16 @@ package viper.silicon.biabduction
 
 import viper.silicon.decider.PathConditionStack
 import viper.silicon.interfaces.{Failure, NonFatalResult, Success, VerificationResult}
-import viper.silicon.rules.executionFlowController
+import viper.silicon.rules.{executionFlowController, executor, producer}
 import viper.silicon.state._
 import viper.silicon.state.terms.Term
 import viper.silicon.utils.ast.BigAnd
+import viper.silicon.utils.freshSnap
 import viper.silicon.verifier.Verifier
 import viper.silver.ast._
-import viper.silver.verifier.errors.Internal
-import viper.silver.verifier.{AbductionQuestionTransformer, DummyReason, PartialVerificationError, VerificationError}
+import viper.silver.verifier.errors.{ErrorWrapperWithTransformers, Internal}
+import viper.silver.verifier.reasons.{InsufficientPermission, MagicWandChunkNotFound}
+import viper.silver.verifier.{DummyReason, PartialVerificationError, VerificationError}
 
 trait BiAbductionResult {
   def s: State
@@ -111,14 +113,29 @@ trait BiAbductionRule[S] {
 
 }
 
-// TODO nklose can we move this all into happening for consumes only?
 object BiAbductionSolver {
 
-  def solveAbduction(s: State, v: Verifier, goal: Seq[Exp], tra: Option[AbductionQuestionTransformer], loc: Position): Seq[BiAbductionResult] = {
+  def solveAbduction(s: State, v: Verifier, ve: VerificationError, f: Failure)(Q: (State, Verifier) => VerificationResult): VerificationResult = {
 
-    val res = executionFlowController.locally(s, v)((s1, v1) => {
+    val abdGoal: Option[AccessPredicate] = ve.reason match {
+      case reason: InsufficientPermission =>
+        val acc = reason.offendingNode match {
+          case n: FieldAccess => FieldAccessPredicate(n, FullPerm()())()
+          case n: PredicateAccess => PredicateAccessPredicate(n, FullPerm()())()
+        }
+        Some(acc)
+      case reason: MagicWandChunkNotFound => Some(reason.offendingNode)
+      case _ => None
+    }
+    val tra = ve match {
+      case ErrorWrapperWithTransformers(_, _, aqTra) => Some(aqTra)
+      case _ => None
+    }
+
+    // TODO nklose I want to do the abduction locally and then continue with the result
+    executionFlowController.locally(s, v)((s1, v1) => {
 
-      val qPre = AbductionQuestion(s1, v1, goal)
+      val qPre = AbductionQuestion(s1, v1, Seq(abdGoal.get))
 
       val q = tra match {
         case Some(trafo) => trafo.f(qPre).asInstanceOf[AbductionQuestion]
@@ -127,19 +144,16 @@ object BiAbductionSolver {
 
       AbductionApplier.applyRules(q){ q1 =>
         if (q1.goal.isEmpty) {
-          Success(Some(AbductionSuccess(q.s, q.v, q.v.decider.pcs.duplicate(), q1.foundState, q1.foundStmts, loc = loc)))
+          producer.produces(s, freshSnap, q1.foundState, _ => Internal(), v) {(s1, v1) =>
+            executor.execs (s1, q1.foundStmts.reverse, v1) {(s2, v2) =>
+              Q(s2, v2) && Success(Some(AbductionSuccess(q.s, q.v, q.v.decider.pcs.duplicate(), q1.foundState, q1.foundStmts, loc = ve.pos)))
+            }
+          }
         } else {
-          Failure(Internal() dueTo DummyReason)
+          f
         }
       }
     })
-
-    res match {
-      case nf: NonFatalResult =>
-        abductionUtils.getAbductionResults(nf)
-      case _ =>
-        Seq(BiAbductionFailure(s, v))
-    }
   }
 
   def solveAbstraction(s: State, v: Verifier, exps: Seq[Exp])(Q: Seq[Exp] => VerificationResult): VerificationResult = {
@@ -182,18 +196,18 @@ object abductionUtils {
   }
 
   def getVars(t: Term, g: Store): Seq[AbstractLocalVar] = {
-    g.values.collect({ case (v, t1) if t1 == t => v }).toSeq
+    g.values.collect({ case (v, (t1, _)) if t1 == t => v }).toSeq
   }
 
   def getField(name: BasicChunkIdentifier, p: Program): Field = {
     p.fields.find(_.name == name.name).get
   }
-  
+
   def getPredicate(name: BasicChunkIdentifier, p: Program): Predicate ={
     p.predicates.find(_.name == name.name).get
   }
 
-  def getAbductionResults(vr: NonFatalResult): Seq[AbductionSuccess] = {
+  def getAbductionSuccesses(vr: NonFatalResult): Seq[AbductionSuccess] = {
     (vr +: vr.previous).collect { case Success(Some(abd: AbductionSuccess)) => abd }
   }
 

src/main/scala/biabduction/Invariant.scala

@@ -65,7 +65,7 @@ object LoopInvariantSolver {
 
         case nonf: NonFatalResult =>
 
-          val abdReses = abductionUtils.getAbductionResults(nonf)
+          val abdReses = abductionUtils.getAbductionSuccesses(nonf)
           val preStateVars = sPreInv.g.values.filter { case (v, _) => absVars.contains(v) }
           val newStateOpt = abdReses.map { abd => abd.toPrecondition(preStateVars, sPreInv.h, Seq(loopCondition)) }
           if (newStateOpt.contains(None)) {

src/main/scala/interfaces/Verification.scala

@@ -107,8 +107,7 @@ case class Failure/*[ST <: Store[ST],
 
 case class SiliconFailureContext(branchConditions: Seq[ast.Exp],
                                  counterExample: Option[Counterexample],
-                                 reasonUnknown: Option[String],
-                                 abductionResult: Option[Seq[BiAbductionResult]]) extends FailureContext {
+                                 reasonUnknown: Option[String]) extends FailureContext {
 
   lazy val branchConditionString: String = {
     if (branchConditions.nonEmpty) {

src/main/scala/rules/ChunkSupporter.scala

@@ -6,6 +6,7 @@
 
 package viper.silicon.rules
 
+import viper.silicon.biabduction.{AbductionSuccess, BiAbductionSolver}
 import viper.silicon.debugger.DebugExp
 import viper.silicon.interfaces.state._
 import viper.silicon.interfaces.{Success, VerificationResult}
@@ -14,10 +15,14 @@ import viper.silicon.state._
 import viper.silicon.state.terms._
 import viper.silicon.state.terms.perms.IsPositive
 import viper.silicon.utils.ast.buildMinExp
+import viper.silicon.utils.freshSnap
 import viper.silicon.verifier.Verifier
 import viper.silver.ast
+import viper.silver.ast.{AccessPredicate, FieldAccess, FieldAccessPredicate, FullPerm, PredicateAccess, PredicateAccessPredicate}
 import viper.silver.parser.PUnknown
-import viper.silver.verifier.VerificationError
+import viper.silver.verifier.{AbductionQuestionTransformer, VerificationError}
+import viper.silver.verifier.errors.ErrorWrapperWithTransformers
+import viper.silver.verifier.reasons.{InsufficientPermission, MagicWandChunkNotFound}
 
 import scala.reflect.ClassTag
 
@@ -140,11 +145,10 @@ object chunkSupporter extends ChunkSupportRules {
             case _ if v1.decider.checkSmoke(true) =>
               Success() // TODO: Mark branch as dead?
             case _ =>
-
-              // TODO nklose: we should move abduction out of createFailure to here and then just recurse with the results
-              // This should also replace the result handling in executor and consumer
-              // We can then do the abduction on the "original" state s, not the partial heap h
-              createFailure(ve, v1, s1, "consuming chunk", true)
+              val f = createFailure(ve, v1, s1, "consuming chunk", true)
+              BiAbductionSolver.solveAbduction(s, v, ve, f)((s2, v2) =>
+                consume2(s2, h, resource, args, argsExp, perms, permsExp, ve, v2)(Q)
+              )
           }
         }
       )(Q)

src/main/scala/rules/Consumer.scala

@@ -165,7 +165,7 @@ object consumer extends ConsumptionRules {
      * consume.
      */
     val sInit = s.copy(h = h)
-    val res = executionFlowController.tryOrFail2[Heap, Term](sInit, v) ((s0, v1, QS) => {
+    executionFlowController.tryOrFail2[Heap, Term](sInit, v) ((s0, v1, QS) => {
       val h0 = s0.h /* h0 is h, but potentially consolidated */
       val s1 = s0.copy(h = s.h) /* s1 is s, but the retrying flag might be set */
 
@@ -175,26 +175,6 @@ object consumer extends ConsumptionRules {
         v2.symbExLog.closeScope(sepIdentifier)
         QS(s2, h2, snap2, v2)})
     })(Q)
-
-    res match {
-      case f@Failure(ve, _) if abductionLocation.isDefined =>
-        ve.failureContexts.head.asInstanceOf[SiliconFailureContext].abductionResult match {
-          case Some((as: AbductionSuccess) :: rest ) => {
-            // Current assumption: we always do this recursively up the stack, so we only have to do the head
-            producer.produces(s, freshSnap, as.state, ContractNotWellformed, v) { (s1, v1) =>
-              executor.execs(s1, as.stmts.reverse, v1) { (s2, v2) =>
-                // TODO nklose this is not working. The abduced heap chunk is not being consumed
-                val restSuc = rest.foldLeft[VerificationResult](Success()){ case (suc, abs: AbductionSuccess) => suc && Success(Some(abs.copy(loc = abductionLocation.get))) }
-                restSuc && Success(Some(as.copy(loc = abductionLocation.get))) && wrappedConsumeTlc(s2, s2.h, a, pve, v2, abductionLocation)(Q)
-              }
-            }
-          }
-          case Some(Seq(_: BiAbductionFailure)) =>
-            //println("Abduction failed")
-            f
-        }
-      case res => res
-    }
   }
 
   private def consumeTlc(s: State, h: Heap, a: ast.Exp, pve: PartialVerificationError, v: Verifier, abductionLocation: Option[Position])

src/main/scala/rules/ExecutionFlowController.scala

@@ -180,7 +180,7 @@ object executionFlowController extends ExecutionFlowRules {
                 (F: FatalResult => VerificationResult): VerificationResult ={
     tryOrElseWithResult[scala.Null](s, v)(((s1, v1, QS) => action(s1, v1, (s2, v2) => QS(s2, null, v2))))((s2, _, v2) => Q(s2, v2))(F)
   }
-
+  
   private def tryOrElseWithResult[R](s: State, v: Verifier)
                   (action: (State, Verifier, (State, R, Verifier) => VerificationResult) => VerificationResult)
                   (Q: (State, R, Verifier) => VerificationResult)

src/main/scala/rules/Executor.scala

@@ -399,7 +399,7 @@ object executor extends ExecutionRules {
         v.decider.prover.comment(stmt.toString())
     }
 
-    val executed = stmt match {
+    stmt match {
       case ast.Seqn(stmts, _) =>
         execs(s, stmts, v)(Q)
 
@@ -766,28 +766,6 @@ object executor extends ExecutionRules {
            | _: ast.ExtensionStmt
            | _: ast.While => sys.error(s"Unexpected statement (${stmt.getClass.getName}): $stmt")
     }
-
-    // TODO nklose: make everything happen in consume, nothing here.
-    executed match {
-
-      case Failure(_: PostconditionViolated, _) => executed // Postconditions are handled elsewhere, we do not want to restart for them
-      case Failure(ve, _) if ve.failureContexts.nonEmpty =>
-        val abReses = ve.failureContexts.head.asInstanceOf[SiliconFailureContext].abductionResult.get
-        abReses.head match {
-          case as: AbductionSuccess =>
-            producer.produces(s, freshSnap, as.state, ContractNotWellformed, v) { (s1, v1) =>
-              executor.execs(s1, as.stmts.reverse, v1) { (s2, v2) =>
-                val restSuc = abReses.tail.foldLeft[VerificationResult](Success()){ case (suc, abs: AbductionSuccess) => suc && Success(Some(abs.copy(loc = stmt.pos))) }
-                restSuc && Success(Some(as)) && exec(s2, stmt, v2)((s3, v3) => Q(s3, v3))
-              }
-            }
-
-          case _: BiAbductionFailure =>
-            //println("Abduction failed")
-            executed
-        }
-      case _ => executed
-    }
   }
 
    private def ssaifyRhs(rhs: Term, rhsExp: ast.Exp, rhsExpNew: Option[ast.Exp], name: String, typ: ast.Type, v: Verifier, s : State): (Term, Option[ast.Exp]) = {

src/main/scala/rules/SymbolicExecutionRules.scala

@@ -7,18 +7,14 @@
 package viper.silicon.rules
 
 import viper.silicon.debugger.DebugExp
-import viper.silicon.interfaces.{Failure, SiliconDebuggingFailureContext, SiliconFailureContext, SiliconMappedCounterexample, SiliconNativeCounterexample, SiliconVariableCounterexample}
-import viper.silicon.biabduction.{BiAbductionResult, BiAbductionSolver, AbductionQuestion}
-import viper.silicon.interfaces.{Failure, SiliconFailureContext, SiliconMappedCounterexample, SiliconNativeCounterexample, SiliconVariableCounterexample}
+import viper.silicon.interfaces._
 import viper.silicon.state.State
 import viper.silicon.state.terms.{False, Term}
 import viper.silicon.verifier.Verifier
 import viper.silver.ast
-import viper.silver.ast.{AccessPredicate, FieldAccess, FieldAccessPredicate, FullPerm, PredicateAccess, PredicateAccessPredicate}
 import viper.silver.frontend.{MappedModel, NativeModel, VariablesModel}
 import viper.silver.verifier.errors.ErrorWrapperWithTransformers
-import viper.silver.verifier.reasons.{InsufficientPermission, MagicWandChunkNotFound}
-import viper.silver.verifier.{AbductionQuestionTransformer, Counterexample, CounterexampleTransformer, VerificationError}
+import viper.silver.verifier.{Counterexample, CounterexampleTransformer, VerificationError}
 
 trait SymbolicExecutionRules {
   lazy val withExp = Verifier.config.enableDebugging()
@@ -50,11 +46,9 @@ trait SymbolicExecutionRules {
   protected def createFailure(ve: VerificationError, v: Verifier, s: State, failedAssert: Term, failedAssertExp: Option[DebugExp], generateNewModel: Boolean): Failure = {
     if (s.retryLevel == 0 && !ve.isExpected) v.errorsReportedSoFar.incrementAndGet()
     var ceTrafo: Option[CounterexampleTransformer] = None
-    var aqTrafo: Option[AbductionQuestionTransformer] = None
     val res = ve match {
-      case ErrorWrapperWithTransformers(wrapped, ceTra, aqTra) =>
+      case ErrorWrapperWithTransformers(wrapped, ceTra, _) =>
         ceTrafo = Some(ceTra)
-        aqTrafo = Some(aqTra)
         wrapped
       case _ => ve
     }
@@ -100,25 +94,15 @@ trait SymbolicExecutionRules {
         })
     } else Seq()
 
-    val abdGoal: Option[AccessPredicate] = ve.reason match {
-      case reason: InsufficientPermission =>
-        val acc = reason.offendingNode match {
-          case n: FieldAccess => FieldAccessPredicate(n, FullPerm()())()
-          case n: PredicateAccess => PredicateAccessPredicate(n, FullPerm()())()
-        }
-        Some(acc)
-      case reason: MagicWandChunkNotFound => Some(reason.offendingNode)
-      case _ => None
-    }
-    val abductionResult = abdGoal.map{acc => BiAbductionSolver.solveAbduction(s, v, Seq(acc), aqTrafo, ve.pos)}
+
 
     if (Verifier.config.enableDebugging()){
       val assumptions = v.decider.pcs.assumptionExps
       res.failureContexts = Seq(SiliconDebuggingFailureContext(v.decider.pcs.branchConditionExps.map(bce => bce._1 -> bce._2.get),
         counterexample, reasonUnknown, Some(s), Some(v), v.decider.prover.getAllEmits(), v.decider.prover.preambleAssumptions,
         v.decider.macroDecls, v.decider.functionDecls, assumptions, failedAssert, failedAssertExp.get))
     } else {
-      res.failureContexts = Seq(SiliconFailureContext(branchconditions, counterexample, reasonUnknown, abductionResult))
+      res.failureContexts = Seq(SiliconFailureContext(branchconditions, counterexample, reasonUnknown))
     }
 
     Failure(res, v.reportFurtherErrors())

src/main/scala/supporters/MethodSupporter.scala

@@ -138,7 +138,7 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent {
           // Collect all the abductions and try to generate preconditions
           val ins = method.formalArgs.map(_.localVar)
           val inVars = s.g.values.collect { case (v, t) if ins.contains(v) => (v, t) }
-          val abds = abductionUtils.getAbductionResults(suc)
+          val abds = abductionUtils.getAbductionSuccesses(suc)
           val pres = abds.map {abd => abd.toPrecondition(inVars, abd.s.oldHeaps.head._2)}
           // If we fail to generate preconditions somewhere, then we actually fail
           if(pres.contains(None)){