Reworked result juggling and var trans

src/main/scala/biabduction/Abduction.scala

@@ -22,7 +22,7 @@ object AbductionApplier extends RuleApplier[SiliconAbductionQuestion] {
 // TODO nklose: cant we just join the check and apply and return either None or Some(AbductionQuestion)?
 
 case class SiliconAbductionQuestion(s: State, v: Verifier, goal: Seq[Exp],
-                                    lostAccesses: Map[Exp, Term] = Map(), foundPrecons: Seq[Exp] = Seq(),
+                                    lostAccesses: Map[Exp, Term] = Map(), foundState: Seq[Exp] = Seq(),
                                     foundStmts: Seq[Stmt] = Seq()) extends BiAbductionQuestion
 
 /**
@@ -226,7 +226,7 @@ object AbductionListUnfold extends AbductionRule[FieldAccessPredicate] {
     eval(q.s, nNl, pve, q.v) { case (s1, arg, v1) => {
       val isNl = q.v.decider.check(arg, Verifier.config.checkTimeout())
       // Add x != null to result if it does not hold
-      val r1 = if (isNl) q.foundPrecons else q.foundPrecons :+ nNl
+      val r1 = if (isNl) q.foundState else q.foundState :+ nNl
 
       // Exchange list(x) with list(x.next) in the state
       // Unfold
@@ -239,7 +239,7 @@ object AbductionListUnfold extends AbductionRule[FieldAccessPredicate] {
           // Remove the access chunk
           consumer.consume(s2, inst, pve, v2)((s3, snap, v3) => {
             val lost = q.lostAccesses + (inst.loc -> SortWrapper(snap, sorts.Ref))
-            Q(q.copy(s = s3, v = v3, goal = g1, foundPrecons = r1, foundStmts = q.foundStmts :+ unfold, lostAccesses = lost))
+            Q(q.copy(s = s3, v = v3, goal = g1, foundState = r1, foundStmts = q.foundStmts :+ unfold, lostAccesses = lost))
           })
         })
       }
@@ -323,7 +323,7 @@ object AbductionPackage extends AbductionRule[MagicWand] {
 
       val g1 = q.goal.filterNot(_ == inst)
       val stmts = q.foundStmts :+ Package(inst, Seqn(packRes.foundStmts.reverse, Seq())())()
-      val pres = q.foundPrecons ++ packRes.foundPrecons
+      val pres = q.foundState ++ packRes.foundState
       Q(q.copy(s = packRes.s, v = packRes.v, goal = g1, foundStmts = stmts))
     })
   }
@@ -348,6 +348,8 @@ object AbductionMissing extends AbductionRule[Seq[AccessPredicate]] {
 
   override protected def apply(q: SiliconAbductionQuestion, inst: Seq[AccessPredicate])(Q: SiliconAbductionQuestion => VerificationResult): VerificationResult = {
     val g1 = q.goal.filterNot(inst.contains)
-    Q(q.copy(goal = g1, foundPrecons = q.foundPrecons ++ inst))
+    Q(q.copy(goal = g1, foundState = q.foundState ++ inst))
   }
+
+  override protected def instanceString(inst: Seq[AccessPredicate]): String = inst.mkString(" && ")
 }

src/main/scala/biabduction/BiAbduction.scala

@@ -1,22 +1,15 @@
 package viper.silicon.biabduction
 
+import viper.silicon.decider.PathConditionStack
 import viper.silicon.interfaces.{Failure, VerificationResult}
 import viper.silicon.state._
 import viper.silicon.state.terms.Term
 import viper.silicon.utils.ast.BigAnd
 import viper.silicon.verifier.Verifier
-import viper.silver.ast
 import viper.silver.ast._
 import viper.silver.verifier.errors.Internal
 import viper.silver.verifier.{AbductionQuestionTransformer, DummyReason, PartialVerificationError, VerificationError}
 
-// TODO we want to continue execution if we abduce successfully. Idea:
-// - Hook into the "Try or Fail" methods
-// - Instead of actually failing, do bi-abduction
-// - track the results somewhere
-// - produce the precondition, execute the statements, and continue execution
-// - At the end, do abstraction on all the found preconditions. Find the necessary statements for the abstractions
-
 trait BiAbductionResult {
   def s: State
 
@@ -25,28 +18,56 @@ trait BiAbductionResult {
 
 trait BiAbductionSuccess extends BiAbductionResult
 
-case class AbductionSuccess(s: State, v: Verifier, pre: Seq[Exp] = Seq(), stmts: Seq[Stmt] = Seq(), loc: Position) extends BiAbductionSuccess {
+case class AbductionSuccess(s: State, v: Verifier, pcs: PathConditionStack, state: Seq[Exp] = Seq(), stmts: Seq[Stmt] = Seq(), loc: Position) extends BiAbductionSuccess {
+
+  val line = loc match {
+    case sp: SourcePosition => sp.start.line.toString
+    case lc: HasLineColumn => lc.line.toString
+    case _ => "No Position"
+  }
+
   override def toString: String = {
+    "Successful abduction at line " + line + ":\n" + "Abduced state\n" + state.map(_.toString()).mkString("\n") + "\nAbduced statements\n" + stmts.reverse.map(_.toString()).mkString("\n")
+  }
+
+  def toPrecondition(preVars: Map[AbstractLocalVar, Term], preHeap: Heap): Option[Seq[Exp]] = {
+
+    // We have to use the pcs from the abduction point
+    val prevPcs = v.decider.pcs
+    v.decider.setPcs(pcs)
+    val varTrans = VarTransformer(s, v, preVars, preHeap)
+    val presTransformed = state.map { varTrans.transformExp }
 
-    val line = loc match {
-      case sp: ast.SourcePosition => sp.start.line
-      case lc: ast.HasLineColumn => lc.line
+    if (presTransformed.contains(None)) { // We could not express the state as a precondition
+      None
+    } else {
+      // TODO There is a common case where we add x != null because we know acc(x.next). We want to remove this bc
+      // If performing the abduction somehow introduces branches, then this could cause problems here.
+      // TODO for loops, we would like to remove the loop condition from conditions we find. How do we do that?
+      val bcs = v.decider.pcs.branchConditionExps.collect { case Some(e) if varTrans.transformExp(e).isDefined && e != TrueLit()() => varTrans.transformExp(e).get }.toSet
+      val presFinal = presTransformed.map { e =>
+        if(bcs.isEmpty){
+          e.get
+        } else {
+          Implies(BigAnd(bcs), e.get)()
+        }
+      }
+      v.decider.setPcs(prevPcs)
+      Some(presFinal)
     }
-    "Successful abduction at line " + line.toString + ":\n" + "Abduced preconditions\n" + pre.map(_.toString()).mkString("\n") + "\nAbduced statements\n" + stmts.reverse.map(_.toString()).mkString("\n")
   }
 }
 
 case class LoopInvariantSuccess(s: State, v: Verifier, invs: Seq[Exp] = Seq(), stmts: Seq[Stmt] = Seq()) extends BiAbductionSuccess {
   override def toString: String = "Successful loop invariant abduction"
 }
 
-case class FramingSuccess(s: State, v: Verifier, posts: Seq[Exp]) extends BiAbductionSuccess
+case class FramingSuccess(s: State, v: Verifier, pcs: PathConditionStack, posts: Seq[Exp]) extends BiAbductionSuccess
 
 case class BiAbductionFailure(s: State, v: Verifier) extends BiAbductionResult {
   override def toString: String = "Abduction failed"
 }
 
-
 object BiAbductionSolver {
 
   def solveAbduction(s: State, v: Verifier, goal: Seq[Exp], tra: Option[AbductionQuestionTransformer], loc: Position): BiAbductionResult = {
@@ -58,55 +79,24 @@ object BiAbductionSolver {
       case _ => qPre
     }
 
-    val ins = q.s.currentMember match {
-      case Some(m: Method) => m.formalArgs.map(_.localVar)
-      case _ => Seq()
-    }
-
-    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)
 
     if (q1.goal.isEmpty) {
-
-      // 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 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 }
-
-      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)
-      }
+      // TODO if we abstract then the statements may become incorrect
+      //val state = AbstractionApplier.apply(AbstractionQuestion(q1.foundState, q1.s.program)).exps
+      AbductionSuccess(q.s, q.v, q.v.decider.pcs.duplicate(), q1.foundState, q1.foundStmts, loc = loc)
     } else {
       BiAbductionFailure(q1.s, q1.v)
     }
   }
 
-  def solveFraming(s: State, v: Verifier): FramingSuccess = {
+  def solveFraming(s: State, v: Verifier, postVars: Map[AbstractLocalVar, Term]): FramingSuccess = {
 
-    val formals = s.currentMember match {
-      case Some(m: Method) => m.formalArgs.map(_.localVar) ++ m.formalReturns.map(_.localVar)
-      case _ => Seq()
-    }
-    val tra = VarTransformer(s, v, s.g.values.filter(formals.contains), s.h)
+    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 absRes = AbstractionApplier.apply(AbstractionQuestion(res, s.program)).exps
-    FramingSuccess(s, v, posts = absRes)
-    //"Abduced postconditions\n" + absRes.map(_.toString()).mkString("\n")
+    FramingSuccess(s, v, v.decider.pcs.duplicate(), posts = absRes)
   }
 }
 
@@ -141,12 +131,14 @@ trait BiAbductionRule[S, T] {
   def checkAndApply(q: S, rule: Int)(Q: (S, Int) => VerificationResult): VerificationResult = {
     check(q) {
       case Some(e) =>
-        println("Applied rule " + this.getClass.getSimpleName)
+        println("Applied rule " + this.getClass.getSimpleName + " on " + this.instanceString(e))
         apply(q, e)(Q(_, 0))
       case None => Q(q, rule + 1)
     }
   }
 
+  protected def instanceString(inst: T): String = inst.toString
+
   protected def check(q: S)(Q: Option[T] => VerificationResult): VerificationResult
 
   protected def apply(q: S, inst: T)(Q: S => VerificationResult): VerificationResult

src/main/scala/biabduction/Invariant.scala

@@ -42,7 +42,7 @@ object LoopInvariantSolver {
                           q: InvariantAbductionQuestion = InvariantAbductionQuestion(Seq(), Map()))
                          (Q: BiAbductionResult => VerificationResult): VerificationResult = {
 
-    // Assumme that we have the previous abstraction
+    // Assume that we have the previous abstraction
     //producer.produces(s, freshSnap, q.abstraction, pveLam, v) { (s2, v2) =>
 
 
@@ -67,40 +67,42 @@ object LoopInvariantSolver {
       case nonf: NonFatalResult =>
 
         val abdReses = (nonf +: nonf.previous).collect { case Success(Some(abd: AbductionSuccess)) => abd }
-        val newState = abdReses.flatMap(_.pre)
+        val newStateOpt = abdReses.map { abd => abd.toPrecondition(sPre.g.values, sPre.h)}
+        if(newStateOpt.contains(None)){
+          return Q(BiAbductionFailure(sPre, vPre))
+        }
+        val newState = newStateOpt.flatMap(_.get)
 
         // 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)
+        producer.produces(sPre, freshSnap, abdReses.flatMap(_.state), pveLam, vPre) { (sPreAbd, vPreAbd) =>
 
           // 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
+          // TODO branching will lead to multiple of these occuring
           val framingRes = (nonf +: nonf.previous).collect { case Success(Some(framing: FramingSuccess)) => framing } match {
             case Seq(res) => res
           }
 
-          // Values of the variables in terms of the beginning of the loop
+          // Values of the variables at the end of loop in terms of the beginning of the loop
+          val relVarTrans = VarTransformer(sPre, vPre, sPre.g.values, sPre.h, strict = false)
           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 {
+          val newAbsValues: Map[AbstractLocalVar, Exp] = relValues.collect { case (v, e) => (v, e.transform {
             case lv: LocalVar if q.absValues.contains(lv) => q.absValues(lv)
           })
           }.collect { case (v, e) => (v, absVarTran.transformExp(e).get) }
 
           // Perform abstraction on the found state for that loop iteration
+          // TODO nklose this is not working?
           // TODO there is an assumption here that the re-assignment happens at the end of the loop
           val newAbsState = newState.map(e => e.transform {
             case lv: LocalVar if q.absValues.contains(lv) => q.absValues(lv)
           }).map(absVarTran.transformExp(_).get)
-
           val newAbstraction = AbstractionApplier.apply(AbstractionQuestion(q.abstraction ++ newAbsState, sPre.program)).exps
 
           // The re-assignments of this iteration in terms of the absolute values

src/main/scala/biabduction/VarTransformer.scala

@@ -1,11 +1,10 @@
 package viper.silicon.biabduction
 
-import viper.silicon.interfaces.{Failure, Success}
+import viper.silicon.interfaces.state.NonQuantifiedChunk
 import viper.silicon.resources.{FieldID, PredicateID}
-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.state.terms.{BuiltinEquals, Term}
+import viper.silicon.state._
 import viper.silicon.verifier.Verifier
 import viper.silver.ast._
 import viper.silver.verifier.PartialVerificationError
@@ -17,44 +16,31 @@ case class VarTransformer(s: State, v: Verifier, targetVars: Map[AbstractLocalVa
 
   // 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 directTargets = targetVars.map(_.swap)
-  val pointsTargets = targetHeap.values.collect {
+  private val directTargets = targetVars.map(_.swap)
+  private 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
 
-  // 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 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 }
+  private 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.distinct //.collect { case t: Var => t }
 
   // Ask the decider whether any of the terms are equal to a target.
+  // TODO the decider is an object which changes. So the path conditions go away. We need to do this earlier
   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
-
   def transformTerm(t: Term): Option[Exp] = {
 
     t match {
       case terms.FullPerm => Some(FullPerm()())
       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 = {
+  private def onlyTargets(e: Exp): Boolean = {
     val vars = e.collect { case lv: LocalVar => lv }.toSeq
     vars.forall(targetVars.contains(_))
   }
@@ -71,33 +57,23 @@ case class VarTransformer(s: State, v: Verifier, targetVars: Map[AbstractLocalVa
 
   def transformExp(e: Exp): Option[Exp] = {
 
+    // TODO we need to be stricter here. If we can't find a match for a exp which uses
+    // input vars, then we need to fail (see hidden.vpr)
     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 fa@FieldAccess(lv: LocalVar, _) =>
+        val args = List(s.g.get(lv).get)
+        val resource = fa.res(s.program)
+        val id = ChunkIdentifier(resource, s.program)
+        findChunk[NonQuantifiedChunk](s.h.values, id, args, v) match {
+          case Some(c) =>
+            transformTerm(c.snap).getOrElse(fa)
+          case None => fa
         }
+      case fa@FieldAccess(rec, _) =>
+        val rcv = transformExp(rec).getOrElse(rec)
+        FieldAccess(rcv, fa.field)()
       case lv: LocalVar => transformTerm(s.g(lv)).getOrElse(lv)
     }
-
-    //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(transformed)) {
       None
     } else {