Solver-checking for definite aliases (if we haven't already) to get k…

…nown symbol for MCE snapshot
viperproject · Jan 20, 2024 · 71a75af · 71a75af
1 parent 9d7abee
commit 71a75af
Show file tree

Hide file tree

Showing 2 changed files with 32 additions and 10 deletions.
diff --git a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala
@@ -32,6 +32,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
                             relevantChunks: Seq[NonQuantifiedChunk],
                             resource: ast.Resource,
                             args: Seq[Term],
+                            knownValue: Option[Option[Term]],
                             v: Verifier)
                            : (State, TaggedSummarisingSnapshot, Seq[Term], Term) = {
 
@@ -75,11 +76,30 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
     val taggedSummarisingSnapshot =
       summarisingSnapshotDefinitions
         .collectFirst {
-          case Equals(`?s`, snap) => ReusedSummarisingSnapshot(snap)
+          case Equals(`?s`, snap) =>
+            ReusedSummarisingSnapshot(snap)
         }.getOrElse({
-          // val ss = v.decider.appliedFresh("ss", sort, s.relevantQuantifiedVariables)
-          val ss = v.decider.appliedFresh("ss", sort, s.functionRecorderQuantifiedVariables())
-          FreshSummarisingSnapshot(ss)
+          knownValue match {
+            case Some(Some(v)) =>
+              ReusedSummarisingSnapshot(v)
+            case _ =>
+              val definiteAliasValue = knownValue match {
+                case None =>
+                  // We have not yet checked for a definite alias
+                  val id = ChunkIdentifier(resource, s.program)
+                  chunkSupporter.findChunk[NonQuantifiedChunk](relevantChunks, id, args, v).map(_.snap)
+                case Some(v) =>
+                  // We have checked for a definite alias and may or may not have found one.
+                  v
+              }
+              definiteAliasValue match {
+                case Some(v) =>
+                  ReusedSummarisingSnapshot(v)
+                case None =>
+                  val ss = v.decider.appliedFresh("ss", sort, s.functionRecorderQuantifiedVariables())
+                  FreshSummarisingSnapshot(ss)
+              }
+          }
         })
 
     val summarisingSnapshot = taggedSummarisingSnapshot.snapshot
@@ -97,6 +117,8 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
                         relevantChunks: Seq[NonQuantifiedChunk],
                         resource: ast.Resource,
                         args: Seq[Term],
+                        knownValue: Option[Option[Term]], // None if we have not yet checked for a definite alias,
+                                                          // Some(v) if we have checked and the result was v
                         v: Verifier)
                        (Q: (State, Term, Seq[Term], Term, Verifier) => VerificationResult)
                        : VerificationResult = {
@@ -112,7 +134,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
         return Q(s, chunk.snap, Seq(), NoPerm, v)
       }
     }
-    val (s1, taggedSnap, snapDefs, permSum) = summariseOnly(s, relevantChunks, resource, args, v)
+    val (s1, taggedSnap, snapDefs, permSum) = summariseOnly(s, relevantChunks, resource, args, knownValue, v)
 
     v.decider.assumeDefinition(And(snapDefs))
 //    v.decider.assume(PermAtMost(permSum, FullPerm())) /* Done in StateConsolidator instead */
@@ -150,7 +172,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
         createFailure(ve, v, s)
       }
     } else {
-      summarise(s, relevantChunks, resource, args, v)((s1, snap, _, permSum, v1) =>
+      summarise(s, relevantChunks, resource, args, None, v)((s1, snap, _, permSum, v1) =>
         v.decider.assert(IsPositive(permSum)) {
           case true =>
             Q(s1, snap, v1)
@@ -188,7 +210,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
     val id = ChunkIdentifier(resource, s.program)
     val relevantChunks = findChunksWithID[NonQuantifiedChunk](h.values, id).toSeq
 
-    summarise(s, relevantChunks, resource, args, v)((s1, snap, _, permSum, v1) =>
+    summarise(s, relevantChunks, resource, args, None, v)((s1, snap, _, permSum, v1) =>
       v.decider.assert(IsPositive(permSum)) {
         case true =>
           Q(s1, h, Some(snap), v1)
@@ -291,7 +313,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
 
         val s0 = s.copy(functionRecorder = currentFunctionRecorder)
 
-        summarise(s0, relevantChunks.toSeq, resource, args, v)((s1, snap, _, _, v1) => {
+        summarise(s0, relevantChunks.toSeq, resource, args, Some(definiteAlias.map(_.snap)), v)((s1, snap, _, _, v1) => {
           val condSnap = if (v1.decider.check(IsPositive(perms), Verifier.config.checkTimeout())) {
             snap
           } else {
@@ -356,7 +378,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
     v.decider.assert(totalPermTaken !== NoPerm) {
       case true =>
         v.decider.assume(perms === totalPermTaken)
-        summarise(s1, relevantChunks.toSeq, resource, args, v)((s2, snap, _, _, v1) =>
+        summarise(s1, relevantChunks.toSeq, resource, args, None, v)((s2, snap, _, _, v1) =>
           Q(s2, updatedChunks, Some(snap), v1))
       case false =>
         createFailure(ve, v, s)

diff --git a/src/test/resources/issue387/jonas_viktor.vpr b/src/test/resources/issue387/jonas_viktor.vpr
@@ -42,7 +42,7 @@ method foo() {
         !(q < i.val_int) ||
         idx_into(to_domain(a.val_ref), q) <=
         idx_into(to_domain(a.val_ref), i.val_int)))
-  //:: UnexpectedOutput(assert.failed:assertion.false, /silicon/issue/387/)
+
   assert (unfolding acc(usize(i), write) in
       (forall q: Int :: { idx_into(to_domain(a.val_ref), q) }
         !(q < i.val_int) ||