Postsubmission started working on stuff

viperproject · Feb 20, 2025 · 3ae6bee · 3ae6bee
1 parent e2eb54d
commit 3ae6bee
Show file tree

Hide file tree

Showing 198 changed files with 1,368 additions and 2,110 deletions.
diff --git a/src/main/scala/biabduction/Abduction.scala b/src/main/scala/biabduction/Abduction.scala
@@ -372,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)()).distinct // TODO there is a weird duplication here sometimes
+                    val stmts: Seq[Stmt] = ((q.foundStmts :+ Apply(wand)()) ++ lhsRes.foundStmts ).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)))
@@ -410,12 +410,12 @@ object AbductionPackage extends AbductionRule {
             val packQ = q.copy(s = s1, v = v1, goal = wand.right.topLevelConjuncts)
             AbductionApplier.applyRules(packQ) { packRes =>
               if (packRes.goal.nonEmpty) {
-                Failure(pve dueTo(DummyReason))
+                Failure(pve dueTo (DummyReason))
                 //T(BiAbductionFailure(packRes.s, packRes.v, packRes.v.decider.pcs.duplicate()))
               } else {
                 val newState = packRes.foundState
                 val newStmts = packRes.foundStmts
-                Success(Some(AbductionSuccess(packRes.s, packRes.v, packRes.v.decider.pcs.duplicate(), newState, newStmts, Map(), None)))
+                Success(Some(AbductionSuccess(packRes.s, packRes.v, packRes.v.decider.pcs.duplicate(), newState, newStmts, Map(), Seq(), None)))
               }
             }
           }
@@ -424,18 +424,38 @@ object AbductionPackage extends AbductionRule {
           case suc: NonFatalResult =>
 
             val abdRes = abductionUtils.getAbductionSuccesses(suc)
-            val stmts = abdRes.flatMap(_.stmts)//.reverse
+            val stmts = abdRes.flatMap(_.stmts).reverse
             val state = abdRes.flatMap(_.state).reverse
+
+
 
-            produces(q.s, freshSnap, state.map(_._1), _ => pve, q.v){ (s1, v1) =>
-              val script = Seqn(stmts, Seq())()
-              magicWandSupporter.packageWand(s1, wand, script, pve, v1) {
-                (s2, wandChunk, v2) =>
-                  val g1 = q.goal.filterNot(_ == wand)
-                  val finalStmts = q.foundStmts :+ Package(wand, script)()
-                  val finalState = q.foundState ++ state
-                  //val lost = q.lostAccesses ++ packRes.lostAccesses
-                  Q(Some(q.copy(s = s2.copy(h = s2.reserveHeaps.head.+(wandChunk)), v = v2, goal = g1, foundStmts = finalStmts, foundState = finalState)))
+            produces(q.s, freshSnap, state.map(_._1), _ => pve, q.v) { (s1, v1) =>
+              val locs: Seq[LocationAccess] = state.map {
+                case (p: FieldAccessPredicate, _) => p.loc
+                case (p: PredicateAccessPredicate, _) => p.loc
+              }
+              abductionUtils.findChunks(locs, s1, v1, Internal()) { newChunks =>
+
+                val newOldHeaps = s1.oldHeaps.map{ case (s, h) => (s, h + Heap(newChunks.keys))}
+                val sPack = s1.copy(oldHeaps = newOldHeaps)
+
+                // TODO the script needs to be self-framing (so field accesses need to be resolved to vars)
+                val script = Seqn(stmts, Seq())()
+                val tran = VarTransformer(sPack, v1, sPack.g.values, sPack.h)
+                script.transform{
+                  case e: FieldAccess => 
+                    val lv = tran.transformExp(e, strict = false)
+                    lv.get
+                }
+
+                magicWandSupporter.packageWand(sPack, wand, script, pve, v1) {
+                  (s2, wandChunk, v2) =>
+                    val g1 = q.goal.filterNot(_ == wand)
+                    val finalStmts = q.foundStmts :+ Package(wand, script)()
+                    val finalState = q.foundState ++ state
+                    //val lost = q.lostAccesses ++ packRes.lostAccesses
+                    Q(Some(q.copy(s = s2.copy(h = s2.reserveHeaps.head.+(wandChunk)), v = v2, goal = g1, foundStmts = finalStmts, foundState = finalState)))
+                }
               }
             }
         }
@@ -459,11 +479,15 @@ object AbductionMissing extends AbductionRule {
     } else {
       val g1 = q.goal.filterNot(accs.contains)
       producer.produces(q.s, freshSnap, accs, _ => pve, q.v) { (s1, v1) =>
-        val locs: Map[LocationAccess, Exp] = accs.map {p => p.loc -> p}.toMap
+        val locs: Map[LocationAccess, Exp] = accs.map { p => p.loc -> p }.toMap
         abductionUtils.findChunks(locs.keys.toSeq, s1, v1, Internal()) { newChunks =>
-          val newState = newChunks.map {case (c, loc) => (locs(loc), Some(c))}
-          Q(Some(q.copy(s = s1, v = v1, goal = g1, foundState = q.foundState ++ newState)))
-      }
+
+          val newOldHeaps = s1.oldHeaps.map { case (label, heap) => (label, heap + Heap(newChunks.keys)) }
+          val s2 = s1.copy(oldHeaps = newOldHeaps)
+
+          val newState = newChunks.map { case (c, loc) => (locs(loc), Some(c)) }
+          Q(Some(q.copy(s = s2, v = v1, goal = g1, foundState = q.foundState ++ newState)))
+        }
       }
     }
   }

diff --git a/src/main/scala/biabduction/Abstraction.scala b/src/main/scala/biabduction/Abstraction.scala
@@ -1,14 +1,12 @@
 package viper.silicon.biabduction
 
-import viper.silicon.interfaces.{Failure, Success, VerificationResult}
+import viper.silicon.interfaces.{NonFatalResult, VerificationResult}
 import viper.silicon.interfaces.state.Chunk
 import viper.silicon.resources._
 import viper.silicon.rules._
 import viper.silicon.state._
 import viper.silicon.verifier.Verifier
 import viper.silver.ast._
-import viper.silver.verifier.DummyReason
-import viper.silver.verifier.errors.FoldFailed
 
 import scala.annotation.tailrec
 
@@ -73,52 +71,95 @@ object AbstractionFold extends AbstractionRule {
   }
 }
 
+/*
+object AbstractionPackage extends AbstractionRule {
+  private def getFieldPredicate(bc: BasicChunk, q: AbstractionQuestion): Option[(Predicate, Exp)] = {
+    if (bc.resourceID != FieldID) None else {
+      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)
+          val pred = q.s.program.predicates.collectFirst { case pred if pred.collect { case fa: FieldAccess => fa.field }.toSeq.contains(field) => pred }
+          (pred, lhsArgExp)
+      }    }}
+  private def checkChunks(chunks: Seq[(BasicChunk, Predicate, Exp)], q: AbstractionQuestion)(Q: Option[AbstractionQuestion] => VerificationResult): VerificationResult = {
+    chunks match {
+      case _ if chunks.isEmpty => Q(None)
+      case (chunk, pred, lhsArg) +: rest =>
+        q.varTran.transformTerm(chunk.args.head) match {
+          case None => checkChunks(rest, q)(Q)
+          case Some(eArgs) =>
+            val rhs = PredicateAccessPredicate(PredicateAccess(Seq(eArgs), pred.name)(), FullPerm()())()
+            val foldRes = executionFlowController.locally(q.s, q.v) { (s1, v1) =>
+              executor.exec(s1, Fold(rhs)(), v1, None) { (_, _) =>
+                Success()
+              }           }
+            foldRes match {
+              case f: FatalResult => checkChunks(rest, q)(Q)
+              case nf: NonFatalResult =>
+                val missingState = abductionUtils.getAbductionSuccesses(nf).flatMap(_.state.flatMap(_._1.topLevelConjuncts))
+                val fieldAccess = FieldAccess(eArgs, field)()
+                val lhs = missingState.collectFirst {
+                  case pred: PredicateAccessPredicate if pred.map{case FieldAccess(_, field) => field}.contains(field) => pred
+                }}
+*/
 
 object AbstractionPackage extends AbstractionRule {
 
   // TODO if the fold fails for a different reason than the recursive predicate missing, then this will do nonsense
-  // We should actually check what is missing and be smarter about what we package.
-  private def checkField(bc: BasicChunk, q: AbstractionQuestion): Option[MagicWand] = {
-    if (bc.resourceID != FieldID) None else {
+  // TODO TODO TODO We should actually check what is missing and be smarter about what we package.
+  // Do a fold with abduction, see what the result is and go from there
+  private def checkField(bc: BasicChunk, q: AbstractionQuestion)(Q: Option[MagicWand] => VerificationResult): VerificationResult = {
 
-      // 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 {
-        case None => None
+    // We can only create a magic wand if we have a local variable that is equal to the field
+    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 => Q(None)
         case Some(lhsArgExp) =>
+
+          // Now we check whether the predicate contains a predicate call on the field
           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 }
-          predOpt.flatMap { pred =>
-            val recPredOpt = pred.collectFirst {
-              case recPred@PredicateAccess(Seq(FieldAccess(_, field2)), _) if field == field2 => recPred
-            }
-            recPredOpt.flatMap { recPred =>
-              val lhs = PredicateAccessPredicate(PredicateAccess(Seq(lhsArgExp), recPred.predicateName)(NoPosition, NoInfo, NoTrafos), FullPerm()())()
-              val rhsArg = q.varTran.transformTerm(bc.args.head).get
-              val rhs = PredicateAccessPredicate(PredicateAccess(Seq(rhsArg), pred)(NoPosition, NoInfo, NoTrafos), FullPerm()())()
-              Some(MagicWand(lhs, rhs)())
-            }
+          q.s.program.predicates.collectFirst { case pred if pred.collect { case fa: FieldAccess => fa.field }.toSeq.contains(field) => pred } match {
+            case None => Q(None)
+            case Some(pred) =>
+                pred.collectFirst {
+                  case recPred@PredicateAccess(Seq(FieldAccess(_, field2)), _) if field == field2 => recPred
+                } match {
+                  case None => Q(None)
+                  case Some(recPred) =>
+                    val lhs = PredicateAccessPredicate(PredicateAccess(Seq(lhsArgExp), recPred.predicateName)(NoPosition, NoInfo, NoTrafos), FullPerm()())()
+
+                    // We only want to create the wand if the inner predicate is not present in the current state.
+                    abductionUtils.findChunkFromExp(lhs.loc, q.s, q.v, pve){
+                      case Some(_) => Q(None)
+                      case None =>
+                        q.varTran.transformTerm(bc.args.head) match {
+                          case None => Q(None)
+                          case Some(rhsArg) =>
+                            val rhs = PredicateAccessPredicate(PredicateAccess(Seq(rhsArg), pred)(NoPosition, NoInfo, NoTrafos), FullPerm()())()
+                            Q(Some(MagicWand(lhs, rhs)()))
+                        }
+                    }
+                }
           }
       }
-    }
   }
 
-  @tailrec
-  private def findWand(chunks: Seq[Chunk], q: AbstractionQuestion): Option[MagicWand] = {
+  private def findWand(chunks: Seq[Chunk], q: AbstractionQuestion)(Q: Option[MagicWand] => VerificationResult): VerificationResult = {
     chunks match {
-      case Seq() => None
-      case (chunk: BasicChunk) +: rest =>
-        checkField(chunk, q) match {
-          case None => findWand(rest, q)
-          case wand => wand
+      case Seq() => Q(None)
+      case (chunk: BasicChunk) +: rest if chunk.resourceID == FieldID =>
+        checkField(chunk, q){
+          case None => findWand(rest, q)(Q)
+          case wand => Q(wand)
         }
-      case (_: Chunk) +: rest => findWand(rest, q)
+      case (_: Chunk) +: rest => findWand(rest, q)(Q)
     }
   }
 
   override def apply(q: AbstractionQuestion)(Q: Option[AbstractionQuestion] => VerificationResult): VerificationResult = {
 
-    findWand(q.s.h.values.toSeq, q) match {
+    findWand(q.s.h.values.toSeq, q) {
       case None => Q(None)
       case Some(wand) =>
         executor.exec(q.s, Assert(wand)(), q.v) {