Recording missing constraint about MCE wildcards in FunctionRecorder

viper-admin · Mar 26, 2024 · c475ee5 · c475ee5
1 parent 50f8adf
commit c475ee5
Show file tree

Hide file tree

Showing 3 changed files with 20 additions and 3 deletions.
diff --git a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala
@@ -369,12 +369,15 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
         ch.withPerm(PermMinus(ch.perm, permTaken))
       })
 
-    v.decider.assume(
+    val totalTakenBounds =
       Implies(
         totalPermSum !== NoPerm,
         And(
           PermLess(NoPerm, totalPermTaken),
-          PermLess(totalPermTaken, totalPermSum))))
+          PermLess(totalPermTaken, totalPermSum)))
+    v.decider.assume(totalTakenBounds)
+
+    newFr = newFr.recordConstraint(totalTakenBounds)
 
     val s1 = s.copy(functionRecorder = newFr)
 

diff --git a/src/main/scala/supporters/functions/FunctionData.scala b/src/main/scala/supporters/functions/FunctionData.scala
@@ -94,6 +94,7 @@ class FunctionData(val programFunction: ast.Function,
   private[this] var freshFvfsAndDomains: InsertionOrderedSet[SnapshotMapDefinition] = InsertionOrderedSet.empty
   private[this] var freshFieldInvs: InsertionOrderedSet[InverseFunctions] = InsertionOrderedSet.empty
   private[this] var freshArps: InsertionOrderedSet[(Var, Term)] = InsertionOrderedSet.empty
+  private[this] var freshConstraints: InsertionOrderedSet[Term] = InsertionOrderedSet.empty
   private[this] var freshSnapshots: InsertionOrderedSet[Function] = InsertionOrderedSet.empty
   private[this] var freshPathSymbols: InsertionOrderedSet[Function] = InsertionOrderedSet.empty
   private[this] var freshMacros: InsertionOrderedSet[MacroDecl] = InsertionOrderedSet.empty
@@ -117,6 +118,7 @@ class FunctionData(val programFunction: ast.Function,
     freshFvfsAndDomains = mergedFunctionRecorder.freshFvfsAndDomains
     freshFieldInvs = mergedFunctionRecorder.freshFieldInvs
     freshArps = mergedFunctionRecorder.freshArps
+    freshConstraints = mergedFunctionRecorder.freshConstraints
     freshSnapshots = mergedFunctionRecorder.freshSnapshots
     freshPathSymbols = mergedFunctionRecorder.freshPathSymbols
     freshMacros = mergedFunctionRecorder.freshMacros
@@ -143,7 +145,8 @@ class FunctionData(val programFunction: ast.Function,
     val nested = (
          freshFieldInvs.flatMap(_.definitionalAxioms)
       ++ freshFvfsAndDomains.flatMap (fvfDef => fvfDef.domainDefinitions ++ fvfDef.valueDefinitions)
-      ++ freshArps.map(_._2))
+      ++ freshArps.map(_._2)
+      ++ freshConstraints)
 
     // Filter out nested definitions that contain free variables.
     // This should not happen, but currently can, due to bugs in the function axiomatisation code.

diff --git a/src/main/scala/supporters/functions/FunctionRecorder.scala b/src/main/scala/supporters/functions/FunctionRecorder.scala
@@ -26,6 +26,7 @@ trait FunctionRecorder extends Mergeable[FunctionRecorder] {
   def freshFvfsAndDomains: InsertionOrderedSet[SnapshotMapDefinition]
   def freshFieldInvs: InsertionOrderedSet[InverseFunctions]
   def freshArps: InsertionOrderedSet[(Var, Term)]
+  def freshConstraints: InsertionOrderedSet[Term]
   def freshSnapshots: InsertionOrderedSet[Function]
   def freshPathSymbols: InsertionOrderedSet[Function]
   def freshMacros: InsertionOrderedSet[MacroDecl]
@@ -34,6 +35,7 @@ trait FunctionRecorder extends Mergeable[FunctionRecorder] {
   def recordFvfAndDomain(fvfDef: SnapshotMapDefinition): FunctionRecorder
   def recordFieldInv(inv: InverseFunctions): FunctionRecorder
   def recordArp(arp: Var, constraint: Term): FunctionRecorder
+  def recordConstraint(constraint: Term): FunctionRecorder
   def recordFreshSnapshot(snap: Function): FunctionRecorder
   def recordPathSymbol(symbol: Function): FunctionRecorder
   def recordFreshMacro(decl: MacroDecl): FunctionRecorder
@@ -47,6 +49,7 @@ case class ActualFunctionRecorder(private val _data: FunctionData,
                                   freshFvfsAndDomains: InsertionOrderedSet[SnapshotMapDefinition] = InsertionOrderedSet(),
                                   freshFieldInvs: InsertionOrderedSet[InverseFunctions] = InsertionOrderedSet(),
                                   freshArps: InsertionOrderedSet[(Var, Term)] = InsertionOrderedSet(),
+                                  freshConstraints: InsertionOrderedSet[Term] = InsertionOrderedSet(),
                                   freshSnapshots: InsertionOrderedSet[Function] = InsertionOrderedSet(),
                                   freshPathSymbols: InsertionOrderedSet[Function] = InsertionOrderedSet(),
                                   freshMacros: InsertionOrderedSet[MacroDecl] = InsertionOrderedSet(),
@@ -190,6 +193,10 @@ case class ActualFunctionRecorder(private val _data: FunctionData,
     if (depth <= 2) copy(freshArps = freshArps + ((arp, constraint)))
     else this
 
+  def recordConstraint(constraint: Term): ActualFunctionRecorder =
+    if (depth <= 2) copy(freshConstraints = freshConstraints + constraint)
+    else this
+
   def recordFreshSnapshot(snap: Function): ActualFunctionRecorder =
     if (depth <= 1) copy(freshSnapshots = freshSnapshots + snap)
     else this
@@ -231,6 +238,7 @@ case class ActualFunctionRecorder(private val _data: FunctionData,
     val fvfs = freshFvfsAndDomains ++ other.freshFvfsAndDomains
     val fieldInvs = freshFieldInvs ++ other.freshFieldInvs
     val arps = freshArps ++ other.freshArps
+    val constraints = freshConstraints ++ other.freshConstraints
     val snaps = freshSnapshots ++ other.freshSnapshots
     val symbols = freshPathSymbols ++ other.freshPathSymbols
     val macros = freshMacros ++ other.freshMacros
@@ -240,6 +248,7 @@ case class ActualFunctionRecorder(private val _data: FunctionData,
          freshFvfsAndDomains = fvfs,
          freshFieldInvs = fieldInvs,
          freshArps = arps,
+         freshConstraints = constraints,
          freshSnapshots = snaps,
          freshPathSymbols = symbols,
          freshMacros = macros)
@@ -269,6 +278,7 @@ case object NoopFunctionRecorder extends FunctionRecorder {
   val freshFvfsAndDomains: InsertionOrderedSet[SnapshotMapDefinition] = InsertionOrderedSet.empty
   val freshFieldInvs: InsertionOrderedSet[InverseFunctions] = InsertionOrderedSet.empty
   val freshArps: InsertionOrderedSet[(Var, Term)] = InsertionOrderedSet.empty
+  val freshConstraints: InsertionOrderedSet[Term] = InsertionOrderedSet.empty
   val freshSnapshots: InsertionOrderedSet[Function] = InsertionOrderedSet.empty
   val freshPathSymbols: InsertionOrderedSet[Function] = InsertionOrderedSet.empty
   val freshMacros: InsertionOrderedSet[MacroDecl] = InsertionOrderedSet.empty
@@ -285,6 +295,7 @@ case object NoopFunctionRecorder extends FunctionRecorder {
   def recordFieldInv(inv: InverseFunctions): NoopFunctionRecorder.type = this
   def recordSnapshot(fapp: ast.FuncApp, guards: Stack[Term], snap: Term): NoopFunctionRecorder.type = this
   def recordArp(arp: Var, constraint: Term): NoopFunctionRecorder.type = this
+  def recordConstraint(constraint: Term): NoopFunctionRecorder.type = this
   def recordFreshSnapshot(snap: Function): NoopFunctionRecorder.type = this
   def recordPathSymbol(symbol: Function): NoopFunctionRecorder.type = this
   def recordFreshMacro(decl: MacroDecl): NoopFunctionRecorder.type = this