Merge pull request #852 from viperproject/meilers_record_merge_var_constraints

Recording constraints for newly-introduced variables during state consolidation

Author: marcoeilers

src/main/scala/rules/Evaluator.scala

@@ -185,7 +185,7 @@ object evaluator extends EvaluationRules {
          *       term returned by eval, mark as constrainable on client-side (e.g. in consumer).
          */
         val s1 =
-          s.copy(functionRecorder = s.functionRecorder.recordArp(tVar, tConstraints))
+          s.copy(functionRecorder = s.functionRecorder.recordConstrainedVar(tVar, tConstraints))
            .setConstrainable(Seq(tVar), true)
         Q(s1, tVar, v)
 

src/main/scala/rules/MoreCompleteExhaleSupporter.scala

@@ -365,7 +365,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
         )
 
         v.decider.assume(constraint)
-        newFr = newFr.recordArp(permTaken, constraint)
+        newFr = newFr.recordConstrainedVar(permTaken, constraint)
 
         ch.withPerm(PermMinus(ch.perm, permTaken))
       })

src/main/scala/rules/StateConsolidator.scala

@@ -216,7 +216,7 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol
          * to use t1 or t2 and constrain it.
          */
         val t3 = v.decider.fresh(t1.sort)
-        (fr.recordFreshSnapshot(t3), t3, And(Implies(b1, t3 === t1), Implies(b2, t3 === t2)))
+        (fr.recordConstrainedVar(t3, And(Implies(b1, t3 === t1), Implies(b2, t3 === t2))), t3, And(Implies(b1, t3 === t1), Implies(b2, t3 === t2)))
     }
   }
 

src/main/scala/supporters/functions/FunctionData.scala

@@ -93,15 +93,15 @@ class FunctionData(val programFunction: ast.Function,
   private[functions] var fappToSnap: Map[ast.FuncApp, Term] = Map.empty
   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 freshConstrainedVars: 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
   private[this] var freshSymbolsAcrossAllPhases: InsertionOrderedSet[Decl] = InsertionOrderedSet.empty
 
   private[functions] def getFreshFieldInvs: InsertionOrderedSet[InverseFunctions] = freshFieldInvs
-  private[functions] def getFreshArps: InsertionOrderedSet[Var] = freshArps.map(_._1)
+  private[functions] def getFreshConstrainedVars: InsertionOrderedSet[Var] = freshConstrainedVars.map(_._1)
   private[functions] def getFreshSymbolsAcrossAllPhases: InsertionOrderedSet[Decl] = freshSymbolsAcrossAllPhases
 
   private[functions] def advancePhase(recorders: Seq[FunctionRecorder]): Unit = {
@@ -117,14 +117,14 @@ class FunctionData(val programFunction: ast.Function,
     fappToSnap = mergedFunctionRecorder.fappToSnap
     freshFvfsAndDomains = mergedFunctionRecorder.freshFvfsAndDomains
     freshFieldInvs = mergedFunctionRecorder.freshFieldInvs
-    freshArps = mergedFunctionRecorder.freshArps
+    freshConstrainedVars = mergedFunctionRecorder.freshConstrainedVars
     freshConstraints = mergedFunctionRecorder.freshConstraints
     freshSnapshots = mergedFunctionRecorder.freshSnapshots
     freshPathSymbols = mergedFunctionRecorder.freshPathSymbols
     freshMacros = mergedFunctionRecorder.freshMacros
 
     freshSymbolsAcrossAllPhases ++= freshPathSymbols map FunctionDecl
-    freshSymbolsAcrossAllPhases ++= freshArps.map(pair => FunctionDecl(pair._1))
+    freshSymbolsAcrossAllPhases ++= freshConstrainedVars.map(pair => FunctionDecl(pair._1))
     freshSymbolsAcrossAllPhases ++= freshSnapshots map FunctionDecl
     freshSymbolsAcrossAllPhases ++= freshFieldInvs.flatMap(i => (i.inverses ++ i.images) map FunctionDecl)
     freshSymbolsAcrossAllPhases ++= freshMacros
@@ -145,7 +145,7 @@ class FunctionData(val programFunction: ast.Function,
     val nested = (
          freshFieldInvs.flatMap(_.definitionalAxioms)
       ++ freshFvfsAndDomains.flatMap (fvfDef => fvfDef.domainDefinitions ++ fvfDef.valueDefinitions)
-      ++ freshArps.map(_._2)
+      ++ freshConstrainedVars.map(_._2)
       ++ freshConstraints)
 
     // Filter out nested definitions that contain free variables.

src/main/scala/supporters/functions/FunctionRecorder.scala

@@ -25,7 +25,7 @@ trait FunctionRecorder extends Mergeable[FunctionRecorder] {
   def fappToSnap: Map[ast.FuncApp, Term]
   def freshFvfsAndDomains: InsertionOrderedSet[SnapshotMapDefinition]
   def freshFieldInvs: InsertionOrderedSet[InverseFunctions]
-  def freshArps: InsertionOrderedSet[(Var, Term)]
+  def freshConstrainedVars: InsertionOrderedSet[(Var, Term)]
   def freshConstraints: InsertionOrderedSet[Term]
   def freshSnapshots: InsertionOrderedSet[Function]
   def freshPathSymbols: InsertionOrderedSet[Function]
@@ -34,7 +34,7 @@ trait FunctionRecorder extends Mergeable[FunctionRecorder] {
   def recordSnapshot(fapp: ast.FuncApp, guards: Stack[Term], snap: Term): FunctionRecorder
   def recordFvfAndDomain(fvfDef: SnapshotMapDefinition): FunctionRecorder
   def recordFieldInv(inv: InverseFunctions): FunctionRecorder
-  def recordArp(arp: Var, constraint: Term): FunctionRecorder
+  def recordConstrainedVar(v: Var, constraint: Term): FunctionRecorder
   def recordConstraint(constraint: Term): FunctionRecorder
   def recordFreshSnapshot(snap: Function): FunctionRecorder
   def recordPathSymbol(symbol: Function): FunctionRecorder
@@ -48,7 +48,7 @@ case class ActualFunctionRecorder(private val _data: FunctionData,
                                   private[functions] val fappToSnaps: Map[ast.FuncApp, InsertionOrderedSet[(Stack[Term], Term)]] = Map(),
                                   freshFvfsAndDomains: InsertionOrderedSet[SnapshotMapDefinition] = InsertionOrderedSet(),
                                   freshFieldInvs: InsertionOrderedSet[InverseFunctions] = InsertionOrderedSet(),
-                                  freshArps: InsertionOrderedSet[(Var, Term)] = InsertionOrderedSet(),
+                                  freshConstrainedVars: InsertionOrderedSet[(Var, Term)] = InsertionOrderedSet(),
                                   freshConstraints: InsertionOrderedSet[Term] = InsertionOrderedSet(),
                                   freshSnapshots: InsertionOrderedSet[Function] = InsertionOrderedSet(),
                                   freshPathSymbols: InsertionOrderedSet[Function] = InsertionOrderedSet(),
@@ -189,8 +189,8 @@ case class ActualFunctionRecorder(private val _data: FunctionData,
     if (depth <= 2) copy(freshFieldInvs = freshFieldInvs + inv)
     else this
 
-  def recordArp(arp: Var, constraint: Term): ActualFunctionRecorder =
-    if (depth <= 2) copy(freshArps = freshArps + ((arp, constraint)))
+  def recordConstrainedVar(arp: Var, constraint: Term): ActualFunctionRecorder =
+    if (depth <= 2) copy(freshConstrainedVars = freshConstrainedVars + ((arp, constraint)))
     else this
 
   def recordConstraint(constraint: Term): ActualFunctionRecorder =
@@ -237,7 +237,7 @@ case class ActualFunctionRecorder(private val _data: FunctionData,
 
     val fvfs = freshFvfsAndDomains ++ other.freshFvfsAndDomains
     val fieldInvs = freshFieldInvs ++ other.freshFieldInvs
-    val arps = freshArps ++ other.freshArps
+    val arps = freshConstrainedVars ++ other.freshConstrainedVars
     val constraints = freshConstraints ++ other.freshConstraints
     val snaps = freshSnapshots ++ other.freshSnapshots
     val symbols = freshPathSymbols ++ other.freshPathSymbols
@@ -247,7 +247,7 @@ case class ActualFunctionRecorder(private val _data: FunctionData,
          fappToSnaps = fts,
          freshFvfsAndDomains = fvfs,
          freshFieldInvs = fieldInvs,
-         freshArps = arps,
+         freshConstrainedVars = arps,
          freshConstraints = constraints,
          freshSnapshots = snaps,
          freshPathSymbols = symbols,
@@ -277,7 +277,7 @@ case object NoopFunctionRecorder extends FunctionRecorder {
   val locToSnap: Map[ast.LocationAccess, Term] = Map.empty
   val freshFvfsAndDomains: InsertionOrderedSet[SnapshotMapDefinition] = InsertionOrderedSet.empty
   val freshFieldInvs: InsertionOrderedSet[InverseFunctions] = InsertionOrderedSet.empty
-  val freshArps: InsertionOrderedSet[(Var, Term)] = InsertionOrderedSet.empty
+  val freshConstrainedVars: InsertionOrderedSet[(Var, Term)] = InsertionOrderedSet.empty
   val freshConstraints: InsertionOrderedSet[Term] = InsertionOrderedSet.empty
   val freshSnapshots: InsertionOrderedSet[Function] = InsertionOrderedSet.empty
   val freshPathSymbols: InsertionOrderedSet[Function] = InsertionOrderedSet.empty
@@ -294,7 +294,7 @@ case object NoopFunctionRecorder extends FunctionRecorder {
   def recordFvfAndDomain(fvfDef: SnapshotMapDefinition): NoopFunctionRecorder.type = this
   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 recordConstrainedVar(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