Separating definitions and other assumptions to fix a wand-related unsoundness

src/main/scala/decider/Decider.scala

@@ -40,7 +40,8 @@ trait Decider {
   def setPathConditionMark(): Mark
 
   def assume(t: Term): Unit
-  def assume(ts: InsertionOrderedSet[Term], enforceAssumption: Boolean = false): Unit
+  def assumeDefinition(t: Term): Unit
+  def assume(ts: InsertionOrderedSet[Term], enforceAssumption: Boolean = false, isDefinition: Boolean = false): Unit
   def assume(ts: Iterable[Term]): Unit
 
   def check(t: Term, timeout: Int): Boolean
@@ -209,23 +210,30 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
       assume(InsertionOrderedSet(Seq(t)), false)
     }
 
+    override def assumeDefinition(t: Term): Unit =
+      assume(InsertionOrderedSet(Seq(t)), false, true)
+
     def assume(terms: Iterable[Term]): Unit =
       assume(InsertionOrderedSet(terms), false)
 
-    def assume(terms: InsertionOrderedSet[Term], enforceAssumption: Boolean = false): Unit = {
+    def assume(terms: InsertionOrderedSet[Term], enforceAssumption: Boolean = false, isDefinition: Boolean = false): Unit = {
       val filteredTerms =
         if (enforceAssumption) terms
         else terms filterNot isKnownToBeTrue
 
-      if (filteredTerms.nonEmpty) assumeWithoutSmokeChecks(filteredTerms)
+      if (filteredTerms.nonEmpty) assumeWithoutSmokeChecks(filteredTerms, isDefinition)
     }
 
-    private def assumeWithoutSmokeChecks(terms: InsertionOrderedSet[Term]) = {
+    private def assumeWithoutSmokeChecks(terms: InsertionOrderedSet[Term], isDefinition: Boolean = false) = {
       val assumeRecord = new DeciderAssumeRecord(terms)
       val sepIdentifier = symbExLog.openScope(assumeRecord)
 
       /* Add terms to Silicon-managed path conditions */
-      terms foreach pathConditions.add
+      if (isDefinition) {
+        terms foreach pathConditions.addDefinition
+      } else {
+        terms foreach pathConditions.add
+      }
 
       /* Add terms to the prover's assumptions */
       terms foreach prover.assume

src/main/scala/decider/PathConditions.scala

@@ -24,8 +24,11 @@ trait RecordedPathConditions {
   def branchConditions: Stack[Term]
   def branchConditionExps: Stack[Option[ast.Exp]]
   def assumptions: InsertionOrderedSet[Term]
+  def definingAssumptions: InsertionOrderedSet[Term]
   def declarations: InsertionOrderedSet[Decl]
 
+  def definitionsOnly: RecordedPathConditions
+
   def contains(assumption: Term): Boolean
 
   def conditionalized: Seq[Term]
@@ -42,6 +45,7 @@ trait RecordedPathConditions {
 trait PathConditionStack extends RecordedPathConditions {
   def setCurrentBranchCondition(condition: Term, conditionExp: Option[ast.Exp]): Unit
   def add(assumption: Term): Unit
+  def addDefinition(assumption: Term): Unit
   def add(declaration: Decl): Unit
   def pushScope(): Unit
   def popScope(): Unit
@@ -64,17 +68,31 @@ private class PathConditionStackLayer
   private var _branchConditionExp: Option[Option[ast.Exp]] = None
   private var _globalAssumptions: InsertionOrderedSet[Term] = InsertionOrderedSet.empty
   private var _nonGlobalAssumptions: InsertionOrderedSet[Term] = InsertionOrderedSet.empty
+  private var _globalDefiningAssumptions: InsertionOrderedSet[Term] = InsertionOrderedSet.empty
+  private var _nonGlobalDefiningAssumptions: InsertionOrderedSet[Term] = InsertionOrderedSet.empty
   private var _declarations: InsertionOrderedSet[Decl] = InsertionOrderedSet.empty
 
   def branchCondition: Option[Term] = _branchCondition
   def branchConditionExp: Option[Option[ast.Exp]] = _branchConditionExp
   def globalAssumptions: InsertionOrderedSet[Term] = _globalAssumptions
+  def globalDefiningAssumptions: InsertionOrderedSet[Term] = _globalDefiningAssumptions
+  def nonGlobalDefiningAssumptions: InsertionOrderedSet[Term] = _nonGlobalDefiningAssumptions
   def nonGlobalAssumptions: InsertionOrderedSet[Term] = _nonGlobalAssumptions
   def declarations: InsertionOrderedSet[Decl] = _declarations
 
   def assumptions: InsertionOrderedSet[Term] = globalAssumptions ++ nonGlobalAssumptions
   def pathConditions: InsertionOrderedSet[Term] = assumptions ++ branchCondition
 
+  def definitionsOnly(): PathConditionStackLayer = {
+    val result = new PathConditionStackLayer
+    result._globalAssumptions = _globalDefiningAssumptions
+    result._globalDefiningAssumptions = _globalDefiningAssumptions
+    result._nonGlobalAssumptions = _nonGlobalDefiningAssumptions
+    result._nonGlobalDefiningAssumptions = _nonGlobalDefiningAssumptions
+    result._declarations = _declarations
+    result
+  }
+
   def branchCondition_=(condition: Term): Unit = {
     assert(_branchCondition.isEmpty,
              s"Branch condition is already set (to ${_branchCondition.get}), "
@@ -104,6 +122,20 @@ private class PathConditionStackLayer
       _nonGlobalAssumptions += assumption
   }
 
+  def addDefinition(assumption: Term): Unit = {
+    assert(
+      !assumption.isInstanceOf[And],
+      s"Unexpectedly found a conjunction (should have been split): $assumption")
+
+    if (PathConditions.isGlobal(assumption)) {
+      _globalAssumptions += assumption
+      _globalDefiningAssumptions += assumption
+    } else {
+      _nonGlobalAssumptions += assumption
+      _nonGlobalDefiningAssumptions += assumption
+    }
+  }
+
   def add(declaration: Decl): Unit = _declarations += declaration
 
   def contains(pathCondition: Term): Boolean = {
@@ -134,6 +166,9 @@ private trait LayeredPathConditionStackLike {
   protected def assumptions(layers: Stack[PathConditionStackLayer]): InsertionOrderedSet[Term] =
     InsertionOrderedSet(layers.flatMap(_.assumptions)) // Note: Performance?
 
+  protected def definingAssumptions(layers: Stack[PathConditionStackLayer]): InsertionOrderedSet[Term] =
+    InsertionOrderedSet(layers.flatMap(_.globalDefiningAssumptions) ++ layers.flatMap(_.nonGlobalDefiningAssumptions)) // Note: Performance?
+
   protected def declarations(layers: Stack[PathConditionStackLayer]): InsertionOrderedSet[Decl] =
     InsertionOrderedSet(layers.flatMap(_.declarations)) // Note: Performance?
 
@@ -199,12 +234,17 @@ private class DefaultRecordedPathConditions(from: Stack[PathConditionStackLayer]
   val branchConditions: Stack[Term] = branchConditions(from)
   val branchConditionExps: Stack[Option[ast.Exp]] = branchConditionExps(from)
   val assumptions: InsertionOrderedSet[Term] = assumptions(from)
+  val definingAssumptions: InsertionOrderedSet[Term] = definingAssumptions(from)
   val declarations: InsertionOrderedSet[Decl] = declarations(from)
 
   def contains(assumption: Term): Boolean = contains(from, assumption)
 
   val conditionalized: Seq[Term] = conditionalized(from)
 
+  def definitionsOnly(): RecordedPathConditions = {
+    new DefaultRecordedPathConditions(from.map(_.definitionsOnly))
+  }
+
   def quantified(quantifier: Quantifier,
                  qvars: Seq[Var],
                  triggers: Seq[Trigger],
@@ -248,6 +288,15 @@ private[decider] class LayeredPathConditionStack
     allAssumptions ++= tlcs
   }
 
+  def addDefinition(assumption: Term): Unit = {
+    /* TODO: Would be cleaner to not add assumptions that are already set as branch conditions */
+
+    val tlcs = assumption.topLevelConjuncts
+
+    tlcs foreach layers.head.addDefinition
+    allAssumptions ++= tlcs
+  }
+
   def add(declaration: Decl): Unit = {
     layers.head.add(declaration)
   }
@@ -311,6 +360,9 @@ private[decider] class LayeredPathConditionStack
   def declarations: InsertionOrderedSet[Decl] =
     InsertionOrderedSet(layers.flatMap(_.declarations)) // Note: Performance?
 
+  def definingAssumptions: InsertionOrderedSet[Term] =
+    InsertionOrderedSet(layers.flatMap(_.globalDefiningAssumptions) ++ layers.flatMap(_.nonGlobalDefiningAssumptions)) // Note: Performance?
+
   def contains(assumption: Term): Boolean = allAssumptions.contains(assumption)
 
   def conditionalized: Seq[Term] = conditionalized(layers)
@@ -357,6 +409,14 @@ private[decider] class LayeredPathConditionStack
     clonedStack
   }
 
+  override def definitionsOnly: RecordedPathConditions = {
+    val result = duplicate()
+    result.layers = layers map (_.definitionsOnly())
+    result.allAssumptions = InsertionOrderedSet(layers.flatMap(_.globalDefiningAssumptions) ++
+      layers.flatMap(_.nonGlobalDefiningAssumptions))
+    result
+  }
+
   override def toString: String =  {
     val sb = new StringBuilder(s"${this.getClass.getSimpleName}:\n")
     val sep = s" ${"-" * 10}\n"

src/main/scala/rules/Evaluator.scala

@@ -171,7 +171,7 @@ object evaluator extends EvaluationRules {
 
       case _: ast.WildcardPerm =>
         val (tVar, tConstraints) = v.decider.freshARP()
-        v.decider.assume(tConstraints)
+        v.decider.assumeDefinition(tConstraints)
         /* TODO: Only record wildcards in State.constrainableARPs that are used in exhale
          *       position. Currently, wildcards used in inhale position (only) may not be removed
          *       from State.constrainableARPs (potentially inefficient, but should be sound).
@@ -292,7 +292,7 @@ object evaluator extends EvaluationRules {
       case ast.Let(x, e0, e1) =>
         eval(s, e0, pve, v)((s1, t0, v1) => {
           val t = v1.decider.appliedFresh("letvar", v1.symbolConverter.toSort(x.typ), s1.relevantQuantifiedVariables)
-          v1.decider.assume(t === t0)
+          v1.decider.assumeDefinition(t === t0)
           val newFuncRec = s1.functionRecorder.recordFreshSnapshot(t.applicable.asInstanceOf[Function])
           eval(s1.copy(g = s1.g + (x.localVar, t0), functionRecorder = newFuncRec), e1, pve, v1)(Q)
         })

src/main/scala/rules/Executor.scala

@@ -339,7 +339,7 @@ object executor extends ExecutionRules {
                 val h3 = Heap(remainingChunks ++ otherChunks)
                 val (sm, smValueDef) = quantifiedChunkSupporter.singletonSnapshotMap(s3, field, Seq(tRcvr), tRhs, v2)
                 v1.decider.prover.comment("Definitional axioms for singleton-FVF's value")
-                v1.decider.assume(smValueDef)
+                v1.decider.assumeDefinition(smValueDef)
                 val ch = quantifiedChunkSupporter.createSingletonQuantifiedChunk(Seq(`?r`), field, Seq(tRcvr), FullPerm, sm, s.program)
                 if (s3.heapDependentTriggers.contains(field))
                   v1.decider.assume(FieldTrigger(field.name, sm, tRcvr))
@@ -374,7 +374,7 @@ object executor extends ExecutionRules {
           if (s.qpFields.contains(field)) {
             val (sm, smValueDef) = quantifiedChunkSupporter.singletonSnapshotMap(s, field, Seq(tRcvr), snap, v)
             v.decider.prover.comment("Definitional axioms for singleton-FVF's value")
-            v.decider.assume(smValueDef)
+            v.decider.assumeDefinition(smValueDef)
             quantifiedChunkSupporter.createSingletonQuantifiedChunk(Seq(`?r`), field, Seq(tRcvr), p, sm, s.program)
           } else {
             BasicChunk(FieldID, BasicChunkIdentifier(field.name), Seq(tRcvr), snap, p)
@@ -627,7 +627,7 @@ object executor extends ExecutionRules {
           *   reported by Silicon issue #328.
           */
          val t = v.decider.fresh(name, v.symbolConverter.toSort(typ))
-         v.decider.assume(t === rhs)
+         v.decider.assumeDefinition(t === rhs)
 
          t
      }

src/main/scala/rules/MagicWandSupporter.scala

@@ -261,27 +261,18 @@ object magicWandSupporter extends SymbolicExecutionRules {
         var conservedPcs: Vector[RecordedPathConditions] = Vector.empty
         var conservedPcsStack: Stack[Vector[RecordedPathConditions]] = s5.conservedPcs
 
-        // Do not record further path conditions if the current state is inconsistent.
-        // This is an ad-hoc workaround to mitigate the following problem: producing a wand's LHS
-        // and executing the packaging proof code can introduce definitional path conditions, e.g.
+        // Producing a wand's LHS and executing the packaging proof code can introduce definitional path conditions, e.g.
         // new permission and snapshot maps, which are in general necessary to proceed after the
         // package statement, e.g. to know which permissions have been consumed.
-        // Since the current implementation doesn't properly differentiate between definitional
-        // and arbitrary path conditions, all path conditions are recorded — which is unsound.
-        // To somewhat improve the situation, such that "non-malevolent" usage of wands works
-        // as expected, we simply check if the current state is known to be inconsistent, and if
-        // it is, we don't record (any further) path conditions.
-        // TODO: Fix this. Might require a substantial redesign of Silicon's path conditions, though.
-
-        if (!v4.decider.checkSmoke()) {
-          conservedPcs = s5.conservedPcs.head :+ pcs
-
-          conservedPcsStack =
-            s5.conservedPcs.tail match {
-              case empty @ Seq() => empty
-              case head +: tail => (head ++ conservedPcs) +: tail
-            }
-        }
+        // Here, we want to keep *only* the definitions, but no other path conditions.
+
+        conservedPcs = s5.conservedPcs.head :+ pcs.definitionsOnly
+
+        conservedPcsStack =
+          s5.conservedPcs.tail match {
+            case empty @ Seq() => empty
+            case head +: tail => (head ++ conservedPcs) +: tail
+          }
 
         val s6 = s5.copy(conservedPcs = conservedPcsStack, recordPcs = s.recordPcs)
 
@@ -296,7 +287,7 @@ object magicWandSupporter extends SymbolicExecutionRules {
           val (sm, smValueDef) =
             quantifiedChunkSupporter.singletonSnapshotMap(s5, wand, args, MagicWandSnapshot(freshSnapRoot, snap), v4)
           v4.decider.prover.comment("Definitional axioms for singleton-SM's value")
-          v4.decider.assume(smValueDef)
+          v4.decider.assumeDefinition(smValueDef)
           val ch = quantifiedChunkSupporter.createSingletonQuantifiedChunk(formalVars, wand, args, FullPerm, sm, s.program)
           appendToResults(s5, ch, v4.decider.pcs.after(preMark), v4)
           Success()

src/main/scala/rules/MoreCompleteExhaleSupporter.scala

@@ -114,7 +114,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
     }
     val (s1, taggedSnap, snapDefs, permSum) = summariseOnly(s, relevantChunks, resource, args, v)
 
-    v.decider.assume(And(snapDefs))
+    v.decider.assumeDefinition(And(snapDefs))
 //    v.decider.assume(PermAtMost(permSum, FullPerm())) /* Done in StateConsolidator instead */
 
     val s2 =

src/main/scala/rules/PredicateSupporter.scala

@@ -72,7 +72,7 @@ object predicateSupporter extends PredicateSupportRules {
         val (sm, smValueDef) =
           quantifiedChunkSupporter.singletonSnapshotMap(s2, predicate, tArgs, predSnap, v1)
         v1.decider.prover.comment("Definitional axioms for singleton-SM's value")
-        v1.decider.assume(smValueDef)
+        v1.decider.assumeDefinition(smValueDef)
         val ch =
           quantifiedChunkSupporter.createSingletonQuantifiedChunk(
             formalArgs, predicate, tArgs, tPerm, sm, s.program)

src/main/scala/rules/Producer.scala

@@ -301,7 +301,7 @@ object producer extends ProductionRules {
             quantifiedChunkSupporter.singletonSnapshotMap(s1, wand, args, sf(sorts.Snap, v1), v1)
           v1.decider.prover.comment("Definitional axioms for singleton-SM's value")
           val definitionalAxiomMark = v1.decider.setPathConditionMark()
-          v1.decider.assume(smValueDef)
+          v1.decider.assumeDefinition(smValueDef)
           val conservedPcs =
             if (s1.recordPcs) (s1.conservedPcs.head :+ v1.decider.pcs.after(definitionalAxiomMark)) +: s1.conservedPcs.tail
             else s1.conservedPcs

src/main/scala/rules/QuantifiedChunkSupport.scala

@@ -967,7 +967,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
     val (sm, smValueDef) = quantifiedChunkSupporter.singletonSnapshotMap(s, resource, tArgs, tSnap, v)
     v.decider.prover.comment("Definitional axioms for singleton-SM's value")
     val definitionalAxiomMark = v.decider.setPathConditionMark()
-    v.decider.assume(smValueDef)
+    v.decider.assumeDefinition(smValueDef)
     val conservedPcs =
       if (s.recordPcs) (s.conservedPcs.head :+ v.decider.pcs.after(definitionalAxiomMark)) +: s.conservedPcs.tail
       else s.conservedPcs