Got reassignement thing working

src/main/scala/biabduction/Abduction.scala

@@ -266,7 +266,7 @@ object AbductionApply extends AbductionRule[MagicWand] {
             case m: MagicWandChunk if m.id.ghostFreeWand.structure(q.s.program).right == 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(q.s, q.v, q.s.g.values.keys.toSeq, strict = false)
+              val varTransformer = VarTransformer(q.s, q.v, q.s.g.values, q.s.h, strict = false)
               val lhsArgs = lhsTerms.map(t => varTransformer.transformTerm(t))
               if (lhsArgs.contains(None)) {
                 None

src/main/scala/biabduction/BiAbduction.scala

@@ -58,11 +58,12 @@ object BiAbductionSolver {
       case _ => qPre
     }
 
-    val ins = s.currentMember match {
+    val ins = q.s.currentMember match {
       case Some(m: Method) => m.formalArgs.map(_.localVar)
       case _ => Seq()
     }
-    val varTrans = VarTransformer(q.s, q.v, ins)
+
+    val varTrans = VarTransformer(q.s, q.v, q.s.g.values.collect { case (v: AbstractLocalVar, t: Term) if ins.contains(v) => (v, t)}, q.s.oldHeaps.head._2)
 
     val q1 = AbductionApplier.apply(q)
 
@@ -71,24 +72,24 @@ object BiAbductionSolver {
       // TODO it is possible that we want to transform variable in a non-strict way before abstraction
       val pres = AbstractionApplier.apply(AbstractionQuestion(q1.foundPrecons, q1.s.program)).exps
 
-      // TODO if some path conditions already contain Ands, then we might reject clauses that we could actually handle
-      val bcs = q1.v.decider.pcs.branchConditionExps.collect { case Some(e) if varTrans.transformExp(e).isDefined && e != TrueLit()() => varTrans.transformExp(e).get }
+      // TODO There is a common case where we add x != null because we know acc(x.next). We want to remove this bc
+      val bcs = q1.v.decider.pcs.branchConditionExps.collect { case Some(e) if varTrans.transformExp(e).isDefined && e != TrueLit()() => varTrans.transformExp(e).get }.toSet
 
       // TODO Weak transformation of statements to original variables (Viper encoding can introduce new variables)
+      val presTransformed = pres.map { varTrans.transformExp }
 
-      val presTransformed = pres.map { (e: Exp) =>
-        varTrans.transformExp(e) match {
-          case Some(e1) => e1
-          case _ => e
-        }
-      }.map { e =>
-        bcs match {
-          case Seq() => e
-          case _ => Implies(BigAnd(bcs), e)()
+      if (presTransformed.contains(None)) {
+        BiAbductionFailure(q1.s, q1.v)
+      } else {
+        val presFinal = presTransformed.map { e =>
+          if(bcs.isEmpty){
+            e.get
+          } else {
+            Implies(BigAnd(bcs), e.get)()
+          }
         }
+        AbductionSuccess(q1.s, q1.v, presFinal, q1.foundStmts, loc = loc)
       }
-      AbductionSuccess(q1.s, q1.v, presTransformed, q1.foundStmts, loc = loc)
-
     } else {
       BiAbductionFailure(q1.s, q1.v)
     }
@@ -100,7 +101,7 @@ object BiAbductionSolver {
       case Some(m: Method) => m.formalArgs.map(_.localVar) ++ m.formalReturns.map(_.localVar)
       case _ => Seq()
     }
-    val tra = VarTransformer(s, v, formals)
+    val tra = VarTransformer(s, v, s.g.values.filter(formals.contains), s.h)
     val res = s.h.values.collect { case c: BasicChunk => tra.transformChunk(c) }.collect { case Some(e) => e }.toSeq
 
     val absRes = AbstractionApplier.apply(AbstractionQuestion(res, s.program)).exps

src/main/scala/biabduction/Invariant.scala

@@ -18,7 +18,7 @@ import viper.silver.verifier.errors.Internal
 // abstractions contains the abstractions after each loop iteration
 // assignments contains the value (as an expression at the beginning of the loop!) of the iterated variables after each loop iteration
 // newRelState contains the things we abduce during the current iteration
-case class InvariantAbductionQuestion(abstraction: Seq[Exp], absValues: Map[AbstractLocalVar, Exp], newRelState: Seq[Exp])
+case class InvariantAbductionQuestion(abstraction: Seq[Exp], absValues: Map[AbstractLocalVar, Exp])
 
 object LoopInvariantSolver {
 
@@ -33,43 +33,48 @@ object LoopInvariantSolver {
     }
   }
 
-  def solveLoopInvariants(s: State,
-                          v: Verifier,
+  def solveLoopInvariants(sPre: State,
+                          vPre: Verifier,
                           loopEdges: Seq[Edge[Stmt, Exp]],
                           joinPoint: Option[SilverBlock],
-                          absVarTran: VarTransformer,
-                          q: InvariantAbductionQuestion = InvariantAbductionQuestion(Seq(), Map(), Seq()))
+                          origState: State,
+                          origVer: Verifier,
+                          q: InvariantAbductionQuestion = InvariantAbductionQuestion(Seq(), Map()))
                          (Q: BiAbductionResult => VerificationResult): VerificationResult = {
 
-    // Assumme that we have the things in nextState
-    producer.produces(s, freshSnap, q.newRelState, pveLam, v) { (s2, v2) =>
+    // Assumme that we have the previous abstraction
+    //producer.produces(s, freshSnap, q.abstraction, pveLam, v) { (s2, v2) =>
 
-      // TODO this is not the way to find the vars, it should be the vars not assigned to in the loop
-      val relVarTrans = VarTransformer(s2, v2, s2.g.values.keys.toSeq, strict = false)
 
-      // Run the loop
-      // This continuation should never be called, we are only following the inner loop edges, which either
-      // fails, or returns a Success with the found postconditions. So the match (and the collectFirst) below should always succeed.
-      val res = executor.follows(s2, loopEdges, pveLam, v2, joinPoint)((_, _) => Success())
+    // Run the loop
+    // This continuation should never be called, we are only following the inner loop edges, which either
+    // fails, or returns a Success with the found postconditions. So the match (and the collectFirst) below should always succeed.
+    executor.follows(sPre, loopEdges, pveLam, vPre, joinPoint)((_, _) => Success()) match {
 
-      res match {
-        // If we find a new precondition, add it to next state and restart
-        case Failure(res, _) =>
-          res.failureContexts.head.asInstanceOf[SiliconFailureContext].abductionResult match {
-            // Success should never occur here, they should be wrapped into a Success in the Executor
-            case None | Some(_: BiAbductionFailure) => Q(BiAbductionFailure(s2, v2))
+      // Abduction has Failed
+      case Failure(res, _) =>
+        res.failureContexts.head.asInstanceOf[SiliconFailureContext].abductionResult match {
+          // Success should never occur here, they should be wrapped into a Success in the Executor
+          case None | Some(_: BiAbductionFailure) => Q(BiAbductionFailure(sPre, vPre))
 
-            //case Some(a: AbductionSuccess) =>
-            //  val newState = q.newRelState ++ a.pre
-            //  solve(s, v, loopEdges, joinPoint, absVarTran, q.copy(newRelState = newState))(Q)
-          }
+          //case Some(a: AbductionSuccess) =>
+          //  val newState = q.newRelState ++ a.pre
+          //  solve(s, v, loopEdges, joinPoint, absVarTran, q.copy(newRelState = newState))(Q)
+        }
+
+      // A NonFatalResult will be a chain of Successes and Unreachables. Each Success can contain an AbductionSucess
+      // There should exactly one FramingSuccess in the chain
+      case nonf: NonFatalResult =>
 
-        // A NonFatalResult will be a chain of Successes and Unreachables. Each Success can contain an AbductionSucess
-        // There should exactly one FramingSuccess in the chain
-        case nonf: NonFatalResult =>
+        val abdReses = (nonf +: nonf.previous).collect { case Success(Some(abd: AbductionSuccess)) => abd }
+        val newState = abdReses.flatMap(_.pre)
 
-          val abdReses = (nonf +: nonf.previous).collect { case Success(Some(abd: AbductionSuccess)) => abd }
-          val newState = q.newRelState ++ abdReses.flatMap(_.pre)
+        // Get the state at the beginning of the loop with with the abduced things added
+        producer.produces(sPre, freshSnap, abdReses.flatMap(_.pre), pveLam, vPre) { (sPreAbd, vPreAbd) =>
+
+          // TODO this is not the way to find the vars, it should be the vars not assigned to in the loop
+          // TODO nklose this is nonsense now. Think about what should really happen here!
+          val relVarTrans = VarTransformer(sPreAbd, vPreAbd, sPre.g.values, sPre.h, strict = false)
 
           // The framing result contains the state at the end of the loop
           // TODO we should also track the framed stuff to generate invariants for loops with changing heaps
@@ -81,6 +86,8 @@ object LoopInvariantSolver {
           val relValues = framingRes.s.g.values.collect { case (v, t) => (v, relVarTrans.transformTerm(t)) }
             .collect { case (v, e) if e.isDefined && e.get != v => (v, e.get) }
 
+          val absVarTran = VarTransformer(framingRes.s, framingRes.v, origState.g.values, origState.h)
+
           // The absolute values at the end of the loop, by combining the values before the iteration with the absolute
           // values from the last iteration
           val newAbsValues: Map[AbstractLocalVar, Exp] = relValues.collect { case (v: AbstractLocalVar, e: Exp) => (v, e.transform {
@@ -94,7 +101,7 @@ object LoopInvariantSolver {
             case lv: LocalVar if q.absValues.contains(lv) => q.absValues(lv)
           }).map(absVarTran.transformExp(_).get)
 
-          val newAbstraction = AbstractionApplier.apply(AbstractionQuestion(q.abstraction ++ newAbsState, s.program)).exps
+          val newAbstraction = AbstractionApplier.apply(AbstractionQuestion(q.abstraction ++ newAbsState, sPre.program)).exps
 
           // The re-assignments of this iteration in terms of the absolute values
           // This is a meaningful sentence that makes perfect sense.
@@ -115,11 +122,10 @@ object LoopInvariantSolver {
             Q(LoopInvariantSuccess(framingRes.s, framingRes.v, invs = relAbstraction.flatMap(getInvariant)))
           } else {
             // Else continue with next iteration, using the state from the end of the loop
-            solveLoopInvariants(framingRes.s, framingRes.v, loopEdges, joinPoint, absVarTran, q.copy(abstraction = newAbstraction,
-              absValues = newAbsValues,
-              newRelState = Seq()))(Q)
+            solveLoopInvariants(framingRes.s, framingRes.v, loopEdges, joinPoint, origState, origVer, q.copy(abstraction = newAbstraction,
+              absValues = newAbsValues))(Q)
           }
-      }
+        }
     }
   }
 }

src/main/scala/biabduction/VarTransformer.scala

@@ -1,49 +1,62 @@
 package viper.silicon.biabduction
 
+import viper.silicon.interfaces.{Failure, Success}
 import viper.silicon.resources.{FieldID, PredicateID}
-import viper.silicon.state.terms.{BuiltinEquals, Term, Var}
-import viper.silicon.state.{BasicChunk, State, terms}
+import viper.silicon.rules.{chunkSupporter, evaluator}
+import viper.silicon.rules.chunkSupporter.findChunk
+import viper.silicon.state.terms.{BuiltinEquals, Term, Var, sorts}
+import viper.silicon.state.{BasicChunk, ChunkIdentifier, Heap, State, terms}
 import viper.silicon.verifier.Verifier
 import viper.silver.ast._
+import viper.silver.verifier.PartialVerificationError
+import viper.silver.verifier.errors.Internal
 
-case class VarTransformer(s: State, v: Verifier, targets: Seq[AbstractLocalVar], strict: Boolean = true) {
+case class VarTransformer(s: State, v: Verifier, targetVars: Map[AbstractLocalVar, Term], targetHeap: Heap, strict: Boolean = true) {
+
+  val pve: PartialVerificationError = Internal()
 
   // The symbolic values of the target vars in the store. Everything else is an attempt to match things to these terms
-  val targetMap: Map[Term, AbstractLocalVar] = targets.view.map(localVar => s.g.get(localVar).get -> localVar).toMap
+  //val targetMap: Map[Term, AbstractLocalVar] = targets.view.map(localVar => s.g.get(localVar).get -> localVar).toMap
+  val directTargets = targetVars.map(_.swap)
+  val pointsTargets = targetHeap.values.collect {
+    case c: BasicChunk if c.resourceID == FieldID && directTargets.contains(c.args.head) =>
+      c.snap -> FieldAccess(directTargets(c.args.head), abductionUtils.getField(c.id, s.program))()
+  }.toMap
+  val targets: Map[Term, Exp] = directTargets ++ pointsTargets
 
-  // Fields chunks as a map
-  val points: Map[Term, Term] = s.h.values.collect { case c: BasicChunk if c.resourceID == FieldID => c.args.head -> c.snap }.toMap
+  // Current chunks as a map
+  //val points: Map[Term, Term] = s.h.values.collect { case c: BasicChunk if c.resourceID == FieldID => c.args.head -> c.snap }.toMap
 
   // All other terms that might be interesting. Currently everything in the store and everything in field chunks
-  val allTerms: Seq[Term] = (s.g.values.values ++ s.h.values.collect { case c: BasicChunk if c.resourceID == FieldID => Seq(c.args.head, c.snap) }.flatten).collect {case t: Var => t}.toSeq
+  val currentTerms: Seq[Term] = (s.g.values.values ++ s.h.values.collect { case c: BasicChunk if c.resourceID == FieldID => Seq(c.args.head, c.snap) }.flatten).toSeq //.collect { case t: Var => t }
 
   // Ask the decider whether any of the terms are equal to a target.
-  val aliases: Map[Term, AbstractLocalVar] = allTerms.map { t =>
-    t -> targetMap.collectFirst { case (t1, e) if t.sort == t1.sort && v.decider.check(BuiltinEquals(t, t1), Verifier.config.checkTimeout()) => e }
+  val matches: Map[Term, Exp] = currentTerms.map { t =>
+    t -> targets.collectFirst { case (t1, e) if t.sort == t1.sort && v.decider.check(BuiltinEquals(t, t1), Verifier.config.checkTimeout()) => e }
   }.collect { case (t2, Some(e)) => t2 -> e }.toMap
 
   // Field Chunks where the snap is equal to a known alias. This is only relevant for expression, not for chunks I think.
-  val snaps: Seq[BasicChunk] = s.h.values.collect { case c: BasicChunk if c.resourceID == FieldID && aliases.contains(c.snap) => c }.toSeq
+  //val snaps: Seq[BasicChunk] = s.h.values.collect { case c: BasicChunk if c.resourceID == FieldID && aliases.contains(c.snap) => c }.toSeq
 
   def transformTerm(t: Term): Option[Exp] = {
 
     t match {
       case terms.FullPerm => Some(FullPerm()())
-      case _ =>
-        // Check for direct aliases
-        val direct = aliases.get(t)
-        if (direct.isDefined) {
-          direct
-        } else {
-          // Check for field accesses pointing to the term
-          points.collectFirst { case (f, v) if v == t && aliases.contains(f) => FieldAccess(aliases(f), s.program.fields.head)() }
-        }
+      case _ => matches.get(t)
+      /*/ Check for direct aliases
+      val direct = matches.get(t)
+      if (direct.isDefined) {
+        direct
+      } else {
+        // Check for field accesses pointing to the term
+        points.collectFirst { case (f, v) if v == t && matches.contains(f) => FieldAccess(matches(f), s.program.fields.head)() }
+      }*/
     }
   }
 
   def onlyTargets(e: Exp): Boolean = {
     val vars = e.collect { case lv: LocalVar => lv }.toSeq
-    vars.forall(targets.contains(_))
+    vars.forall(targetVars.contains(_))
   }
 
   def transformChunk(b: BasicChunk): Option[Exp] = {
@@ -56,27 +69,39 @@ case class VarTransformer(s: State, v: Verifier, targets: Seq[AbstractLocalVar],
     }
   }
 
-  // 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 transformExp(e: Exp): Option[Exp] = {
 
-    val varMap = e.collect { case lc: LocalVar => lc -> transformTerm(s.g(lc)) }.collect { case (k, Some(v)) => k -> v }.toMap
-
-    val onlyVars = e.transform {
-      case lc: LocalVar if !targets.contains(lc) => varMap.getOrElse(lc, lc)
+    val transformed = e.transform {
+      case fa: FieldAccess =>
+        var t: Term = terms.Unit
+        // TODO if we ever call this on state that has been abduced, we might need to access the "lost chunks" here
+        val res = evaluator.eval(s, fa, pve, v)((_, t2, _) => {
+          t = t2
+          Success()
+        })
+        res match {
+          case _: Success => transformTerm(t).getOrElse(fa)
+          case _ => fa
+        }
+      case lv: LocalVar => transformTerm(s.g(lv)).getOrElse(lv)
     }
 
-    val accesses = onlyVars.transform {
-      // TODO this will not catch z.next.next -> x
-      case fa@FieldAccess(rcv: LocalVar, _) if !onlyTargets(fa) =>
-        snaps.collectFirst { case c: BasicChunk if c.args.head == s.g(rcv) => aliases(c.snap) }.getOrElse(fa)
-    }
+    //val varMap = e.collect { case lc: LocalVar => lc -> transformTerm(s.g(lc)) }.collect { case (k, Some(v)) => k -> v }.toMap
+
+    //val onlyVars = e.transform {
+    //  case lc: LocalVar if !targets.contains(lc) => varMap.getOrElse(lc, lc)
+    //}
+
+    //val accesses = onlyVars.transform {
+    //  // TODO this will not catch z.next.next -> x
+    //  case fa@FieldAccess(rcv: LocalVar, _) if !onlyTargets(fa) =>
+    //    snaps.collectFirst { case c: BasicChunk if c.args.head == s.g(rcv) => matches(c.snap) }.getOrElse(fa)
+    //}
 
-    if (strict && !onlyTargets(accesses)) {
+    if (strict && !onlyTargets(transformed)) {
       None
     } else {
-      Some(accesses)
+      Some(transformed)
     }
   }
 }

src/main/scala/rules/Executor.scala

@@ -294,8 +294,10 @@ object executor extends ExecutionRules {
                             case Failure(_, _) => edgeCondWelldefinedness
                             case Success(_) =>
 
+                              val varTra = VarTransformer(s, v, s.g.values, s.h)
+
                               // Try to find invariants
-                              LoopInvariantSolver.solveLoopInvariants(s4, v3, otherEdges, joinPoint, VarTransformer(s, v, nwvs, strict = false)) {
+                              LoopInvariantSolver.solveLoopInvariants(s4, v3, otherEdges, joinPoint, s, v) {
                                 case BiAbductionFailure(_, _) =>
                                   println("Failed to find loop invariants")
                                   follows(s4, sortedEdges, WhileFailed, v3, joinPoint)(Q)
@@ -738,7 +740,9 @@ object executor extends ExecutionRules {
                 })
               }
             }
-          case _ => executed
+          case Some(_: BiAbductionFailure) =>
+            println("Abduction failed")
+            executed
         }
       case _ => executed
     }

src/main/scala/rules/SymbolicExecutionRules.scala

@@ -84,7 +84,7 @@ trait SymbolicExecutionRules {
       case reason: MagicWandChunkNotFound => Some(reason.offendingNode)
       case _ => None
     }
-    val abductionResult = abdGoal.map{acc => BiAbductionSolver.solve(s, v, Seq(acc), aqTrafo, ve.pos)}
+    val abductionResult = abdGoal.map{acc => BiAbductionSolver.solveAbduction(s, v, Seq(acc), aqTrafo, ve.pos)}
 
     res.failureContexts = Seq(SiliconFailureContext(branchconditions, counterexample, reasonUnknown, abductionResult))
     Failure(res, v.reportFurtherErrors())