Started reworking 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(false),
+    default = Some(true), // Set to true for biabduction testing
     noshort = true
   )
 

src/main/scala/biabduction/Abstraction.scala

@@ -1,64 +1,118 @@
 package viper.silicon.biabduction
 
 import viper.silicon.interfaces.VerificationResult
-import viper.silicon.rules.evaluator
-import viper.silicon.state.State
-import viper.silicon.state.terms.True
+import viper.silicon.resources._
+import viper.silicon.rules._
+import viper.silicon.state._
 import viper.silicon.verifier.Verifier
 import viper.silver.ast._
 
 object AbstractionApplier extends RuleApplier[AbstractionQuestion] {
   override val rules: Seq[AbstractionRule] = Seq(AbstractionFold, AbstractionPackage, AbstractionJoin, AbstractionApply)
 }
 
-case class AbstractionQuestion(exps: Seq[Exp], s: State, v: Verifier)
+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 isTriggerField(bc: BasicChunk): Boolean = {
+    bc.resourceID match {
+      case FieldID => fields.contains(abductionUtils.getField(bc.id, s.program))
+      case _ => false
+    }
+  }
+}
 
 trait AbstractionRule extends BiAbductionRule[AbstractionQuestion]
 
 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 =>
+        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) =>
+            predicateSupporter.fold(s1, pred, List(chunk.args.head), None, terms.FullPerm, Some(FullPerm()()), wildcards, pve, v1)(T)
+        } { (s2, v2) => Q(Some(q.copy(s = s2, v = v2))) } {
+          _ => checkChunks(rest, q)(Q)
+        }
+    }
+  }
+
   override def apply(q: AbstractionQuestion)(Q: Option[AbstractionQuestion] => VerificationResult): VerificationResult = {
-    Q(None)
+    val candChunks = q.s.h.values.collect { case bc: BasicChunk if q.isTriggerField(bc) => bc }.toSeq
+    checkChunks(candChunks, q)(Q)
   }
 }
 
+
+// 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 {
 
+  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 None => findWandFieldChunk(rest, q)
+          case Some(lhs) => Some((lhs, chunk))
+        }
+    }
+  }
+
   override def apply(q: AbstractionQuestion)(Q: Option[AbstractionQuestion] => VerificationResult): VerificationResult = {
-    Q(None)
+
+    val candChunks = q.s.h.values.collect { case bc: BasicChunk if q.isTriggerField(bc) => bc }.toSeq
+
+    findWandFieldChunk(candChunks, q) match {
+    case None => Q(None)
+    case Some((lhsArg, chunk)) =>
+      val pred = q.fields(abductionUtils.getField(chunk.id, q.s.program))
+      val lhs = PredicateAccessPredicate(PredicateAccess(Seq(lhsArg), pred)(NoPosition, NoInfo, NoTrafos), FullPerm()())()
+      val rhsArg = q.varTran.transformTerm(chunk.args.head).get
+      val rhs = PredicateAccessPredicate(PredicateAccess(Seq(rhsArg), pred)(NoPosition, NoInfo, NoTrafos), FullPerm()())()
+      val wand = MagicWand(lhs, rhs)()
+      executor.exec(q.s, Assert(wand)(), q.v) { (s1, sv) => Q(Some(q.copy(s = s1, v = sv)))}
+    }
   }
 }
 
 object AbstractionJoin extends AbstractionRule {
 
   override def apply(q: AbstractionQuestion)(Q: Option[AbstractionQuestion] => VerificationResult): VerificationResult = {
-    val wands = q.exps.collect { case wand: MagicWand => wand }
+    val wands = q.s.h.values.collect { case wand: MagicWandChunk => q.varTran.transformChunk(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(inst)) =>
-        val exps1 = q.exps.filterNot(exp => inst._1 == exp || inst._2 == exp) :+ MagicWand(inst._1.left, inst._2.right)()
-        Q(Some(q.copy(exps = exps1)))
+      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)))
+        }
     }
   }
 }
 
 object AbstractionApply extends AbstractionRule {
 
   override def apply(q: AbstractionQuestion)(Q: Option[AbstractionQuestion] => VerificationResult): VerificationResult = {
-    val wands = q.exps.collect { case wand: MagicWand => wand }
-    val matches = wands.filter(wand => q.exps.contains(wand.left))
-    if (matches.isEmpty) {
-      Q(None)
-    } else {
-      val lefts = matches.map(_.left)
-      val rights = matches.map(_.right)
-
-      val exps1 = q.exps.filterNot(matches.contains).filter(lefts.contains(_)) ++ rights
-      Q(Some(q.copy(exps = exps1)))
+    val wands = q.s.h.values.collect { case wand: MagicWandChunk => q.varTran.transformChunk(wand) }.collect {case Some(wand: MagicWand) => wand}
+    val targets = q.s.h.values.collect { case c: BasicChunk => q.varTran.transformChunk(c) }.collect {case Some(exp) => exp}.toSeq
+
+    wands.collectFirst{case wand if targets.contains(wand.left) => wand } match {
+      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))
+        }
     }
   }
 }

src/main/scala/biabduction/BiAbduction.scala

@@ -152,15 +152,19 @@ object BiAbductionSolver {
 
 
 
-  def solveAbstraction(s: State, v: Verifier, exps: Seq[Exp])(Q: Seq[Exp] => VerificationResult): VerificationResult = {
-    executionFlowController.locallyWithResult[Seq[Exp]](s, v)((s1, v1, QS) => {
-      val q = AbstractionQuestion(exps, s1, v1)
-      AbstractionApplier.applyRules(q){ q1 =>
-        QS(q1.exps)
-      }
-    })(Q)
+  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))
+    } match {
+      case NonFatalResult =>
+        val exps = abductionUtils.getFramingSuccesses(res).head
+        Q(exps.s, exps.v, exps.posts)
+    }
   }
 
+  // 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. 
   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)

src/main/scala/biabduction/VarTransformer.scala

@@ -8,8 +8,6 @@ import viper.silicon.state._
 import viper.silicon.verifier.Verifier
 import viper.silver.ast
 import viper.silver.ast._
-//import viper.silver.verifier.PartialVerificationError
-//import viper.silver.verifier.errors.Internal
 
 case class VarTransformer(s: State, v: Verifier, targetVars: Map[AbstractLocalVar, (Term, Option[ast.Exp])], targetHeap: Heap) {
 
@@ -20,10 +18,10 @@ case class VarTransformer(s: State, v: Verifier, targetVars: Map[AbstractLocalVa
 
   private def resolveMatches(): Map[Term, Exp] = {
 
-    val allTerms: Seq[Term] = (s.g.values.values.map{case (t1, _) => t1}
+    val allTerms: Seq[Term] = (s.g.values.values.map { case (t1, _) => t1 }
       ++ s.h.values.collect { case c: BasicChunk if c.resourceID == FieldID => Seq(c.args.head, c.snap) }.flatten
       ++ targetVars.values.map(_._1)
-      ++ v.decider.pcs.branchConditions.collect{ case t => t.subterms.collect{case tVar: Var => tVar}}.flatten).toSeq.distinct
+      ++ v.decider.pcs.branchConditions.collect { case t => t.subterms.collect { case tVar: Var => tVar } }.flatten).toSeq.distinct
 
     // 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
@@ -34,15 +32,16 @@ case class VarTransformer(s: State, v: Verifier, targetVars: Map[AbstractLocalVa
     }.collect { case (t2, Some(e)) => t2 -> e }.toMap
 
     resolveChunks(directAliases, targetHeap.values.collect { case c: BasicChunk
-      if c.resourceID == FieldID && !(directAliases.contains(c.args.head) && directAliases.contains(c.snap)) => c }.toSeq, allTerms.filter(!directAliases.contains(_)))
+      if c.resourceID == FieldID && !(directAliases.contains(c.args.head) && directAliases.contains(c.snap)) => c
+    }.toSeq, allTerms.filter(!directAliases.contains(_)))
   }
 
   private def resolveChunks(currentMatches: Map[Term, Exp], remainingChunks: Seq[BasicChunk], remainingTerms: Seq[Term]): Map[Term, Exp] = {
-    remainingChunks.collectFirst { case c if currentMatches.contains(c.args.head) => c} match {
+    remainingChunks.collectFirst { case c if currentMatches.contains(c.args.head) => c } match {
       case None => currentMatches
       case Some(c) =>
         val newExp = FieldAccess(currentMatches(c.args.head), abductionUtils.getField(c.id, s.program))()
-        val newMatches = currentMatches ++ remainingTerms.collect{ case t if t.sort == c.snap.sort && v.decider.check(BuiltinEquals(t, c.snap), Verifier.config.checkTimeout()) => t -> newExp }
+        val newMatches = currentMatches ++ remainingTerms.collect { case t if t.sort == c.snap.sort && v.decider.check(BuiltinEquals(t, c.snap), Verifier.config.checkTimeout()) => t -> newExp }
         resolveChunks(newMatches, remainingChunks.filter(_ != c), remainingTerms.filter(!newMatches.contains(_)))
     }
   }
@@ -62,14 +61,26 @@ case class VarTransformer(s: State, v: Verifier, targetVars: Map[AbstractLocalVa
     }
   }
 
-  def transformChunk(b: BasicChunk): Option[Exp] = {
+  def transformChunk(b: NonQuantifiedChunk): Option[Exp] = {
 
-    val rcv = transformTerm(b.args.head)
-    (b, rcv) match {
-      case (_, None) => None
-      case (BasicChunk(FieldID, _, _, _, _, _, _), rcv) => Some(FieldAccessPredicate(FieldAccess(rcv.get, abductionUtils.getField(b.id, s.program))(), transformTerm(b.perm).get)())
-      case (BasicChunk(PredicateID, id, _, _, _, _, _), rcv) => Some(PredicateAccessPredicate(PredicateAccess(Seq(rcv.get), id.name)(), transformTerm(b.perm).get)())
-        //Some(abductionUtils.getPredicate(s.program, rcv.get, transformTerm(b.perm).get))
+    b match {
+      case bc: BasicChunk =>
+        val rcv = transformTerm(bc.args.head)
+        (bc, rcv) match {
+          case (_, None) => None
+          case (BasicChunk(FieldID, _, _, _, _, _, _), rcv) => Some(FieldAccessPredicate(FieldAccess(rcv.get, abductionUtils.getField(bc.id, s.program))(), transformTerm(b.perm).get)())
+          case (BasicChunk(PredicateID, id, _, _, _, _, _), rcv) => Some(PredicateAccessPredicate(PredicateAccess(Seq(rcv.get), id.name)(), transformTerm(b.perm).get)())
+
+        }
+      case mwc: MagicWandChunk =>
+        val rcvs = mwc.args.map(a => a -> transformTerm(a)).toMap
+        if (rcvs.values.toSeq.contains(None)) None else {
+          val shape = mwc.id.ghostFreeWand
+          val expBindings = mwc.bindings.map(b => b._1 -> rcvs(b._2._1).get)
+          val instantiated = shape.replace(expBindings)
+          Some(instantiated)
+          //Some(abductionUtils.getPredicate(s.program, rcv.get, transformTerm(b.perm).get))
+        }
     }
   }
 
@@ -122,12 +133,12 @@ case class VarTransformer(s: State, v: Verifier, targetVars: Map[AbstractLocalVa
           }
         case lv: LocalVar => {
           val term: Term = s.g.values.getOrElse(lv, targetVars(lv))._1
-          transformTerm(term).get 
+          transformTerm(term).get
         }
       }
       Some(res)
     } catch {
-      case _: NoSuchElementException => if(strict) None else Some(e)
+      case _: NoSuchElementException => if (strict) None else Some(e)
     }
   }
 }

src/main/scala/supporters/MethodSupporter.scala

@@ -178,7 +178,7 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent {
         consumes(s, posts, postViolated, v)(QS)
       } {
         (s1: State, _: Term, v1: Verifier) => {
-          // TODO nklose This fails to generate statements if we do abstraction
+          // TODO nklose We want to do abstraction, but that might require adding folds and such...
           val formals = method.formalArgs.map(_.localVar) ++ method.formalReturns.map(_.localVar)
           val vars = s1.g.values.collect { case (v2, t) if formals.contains(v2) => (v2, t) }
           val newPosts = BiAbductionSolver.solveFraming(s1, v1, vars, method.pos)