Fixing potential unsoundness in QP state consolidation (#910)

Author: marcoeilers

silver

@@ -232,28 +232,31 @@ trait QuantifiedChunkSupport extends SymbolicExecutionRules {
    *
    * @param fr The functionRecorder to use when new snapshot maps are generated.
    * @param field The name of the field.
+   * @param fqvars Arguments of the current function if we are currently verifying one, i.e., functionRecorderQVars.
    * @param t1 The first chunk's snapshot map.
    * @param t2 The second chunk's snapshot map.
    * @param p1 The first chunk's permission amount, should be constrained by the domain.
    * @param p2 The second chunk's permission amount, should be constrained by the domain.
    * @param v The verifier to use.
    * @return A tuple (fr, sm, def) of functionRecorder, a snapshot map sm and a term def constraining sm.
    */
-  def combineFieldSnapshotMaps(fr: FunctionRecorder, field: String, t1: Term, t2: Term, p1: Term, p2: Term, v: Verifier): (FunctionRecorder, Term, Term)
+  def combineFieldSnapshotMaps(fr: FunctionRecorder, field: String, fqvars: Seq[Var],t1: Term, t2: Term, p1: Term, p2: Term, v: Verifier): (FunctionRecorder, Term, Term)
 
   /** Merge the snapshots of two quantified heap chunks that denote the same predicate
    *
    * @param fr The functionRecorder to use when new snapshot maps are generated.
    * @param predicate The name of the predicate.
    * @param qVars The variables over which p1 and p2 are defined
+   * @param fqvars Arguments of the current function if we are currently verifying one, i.e., functionRecorderQVars.
    * @param t1 The first chunk's snapshot map.
    * @param t2 The second chunk's snapshot map.
    * @param p1 The first chunk's permission amount, should be constrained by the domain.
    * @param p2 The second chunk's permission amount, should be constrained by the domain.
    * @param v The verifier to use.
    * @return A tuple (fr, sm, def) of functionRecorder, a snapshot map sm and a term def constraining sm.
    */
-  def combinePredicateSnapshotMaps(fr: FunctionRecorder, predicate: String, qVars: Seq[Var], t1: Term, t2: Term, p1: Term, p2: Term, v: Verifier): (FunctionRecorder, Term, Term)
+  def combinePredicateSnapshotMaps(fr: FunctionRecorder, predicate: String, qVars: Seq[Var], fqvars: Seq[Var],
+                                   t1: Term, t2: Term, p1: Term, p2: Term, v: Verifier): (FunctionRecorder, Term, Term)
 }
 
 object quantifiedChunkSupporter extends QuantifiedChunkSupport {
@@ -2094,7 +2097,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
   }
 
   // Based on StateConsolidator#combineSnapshots
-  override def combineFieldSnapshotMaps(fr: FunctionRecorder, field: String, t1: Term, t2: Term, p1: Term, p2: Term, v: Verifier): (FunctionRecorder, Term, Term) = {
+  override def combineFieldSnapshotMaps(fr: FunctionRecorder, field: String, fqvars: Seq[Var], t1: Term, t2: Term, p1: Term, p2: Term, v: Verifier): (FunctionRecorder, Term, Term) = {
     val lookupT1 = Lookup(field, t1, `?r`)
     val lookupT2 = Lookup(field, t2, `?r`)
     val (fr2, sm, smDef, triggers) = (IsPositive(p1), IsPositive(p2)) match {
@@ -2108,18 +2111,18 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
          * we have to introduce a fresh snapshot. Note that it is not sound
          * to use t1 or t2 and constrain it.
          */
-        val t3 = v.decider.fresh(t1.sort, Option.when(withExp)(PUnknown()))
+        val t3 = v.decider.appliedFresh("ms", t1.sort, fqvars)
         val lookupT3 = Lookup(field, t3, `?r`)
         val constraint = And(Implies(b1, lookupT3 === lookupT1), Implies(b2, lookupT3 === lookupT2))
         val triggers = Seq(Trigger(lookupT1), Trigger(lookupT2), Trigger(lookupT3))
-        (fr.recordConstrainedVar(t3, Forall(`?r`, constraint, triggers)), t3, constraint, triggers)
+        (fr.recordPathSymbol(t3.applicable.asInstanceOf[Function]).recordConstraint(Forall(`?r`, constraint, triggers)), t3, constraint, triggers)
     }
 
     (fr2, sm, Forall(`?r`, smDef, triggers))
   }
 
   // Based on StateConsolidator#combineSnapshots
-  override def combinePredicateSnapshotMaps(fr: FunctionRecorder, predicate: String, qVars: Seq[Var], t1: Term, t2: Term, p1: Term, p2: Term, v: Verifier): (FunctionRecorder, Term, Term) = {
+  override def combinePredicateSnapshotMaps(fr: FunctionRecorder, predicate: String, qVars: Seq[Var], fqvars: Seq[Var], t1: Term, t2: Term, p1: Term, p2: Term, v: Verifier): (FunctionRecorder, Term, Term) = {
     val lookupT1 = PredicateLookup(predicate, t1, qVars)
     val lookupT2 = PredicateLookup(predicate, t2, qVars)
     val (fr2, sm, smDef, triggers) = (IsPositive(p1), IsPositive(p2)) match {
@@ -2133,10 +2136,11 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
          * we have to introduce a fresh snapshot. Note that it is not sound
          * to use t1 or t2 and constrain it.
          */
-        val t3 = v.decider.fresh(t1.sort, Option.when(withExp)(PUnknown()))
+        val t3 = v.decider.appliedFresh("ms", t1.sort, fqvars)
         val lookupT3 = PredicateLookup(predicate, t3, qVars)
-        (fr.recordConstrainedVar(t3, And(Implies(b1, lookupT3 === lookupT1), Implies(b2, lookupT3 === lookupT2))), t3,
-          And(Implies(b1, lookupT3 === lookupT1), Implies(b2, lookupT3 === lookupT2)), Seq(Trigger(lookupT1), Trigger(lookupT2), Trigger(lookupT3)))
+        val constraint = And(Implies(b1, lookupT3 === lookupT1), Implies(b2, lookupT3 === lookupT2))
+        val triggers = Seq(Trigger(lookupT1), Trigger(lookupT2), Trigger(lookupT3))
+        (fr.recordPathSymbol(t3.applicable.asInstanceOf[Function]).recordConstraint(Forall(qVars, constraint, triggers)), t3, constraint, triggers)
     }
 
     (fr2, sm, Forall(qVars, smDef, triggers))

src/main/scala/rules/QuantifiedChunkSupport.scala

@@ -207,14 +207,14 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol
       assert(l.quantifiedVars == Seq(`?r`))
       assert(r.quantifiedVars == Seq(`?r`))
       // We need to use l.perm/r.perm here instead of perm1 and perm2 since the permission amount might be dependent on the condition/domain
-      val (fr2, combinedSnap, snapEq) = quantifiedChunkSupporter.combineFieldSnapshotMaps(fr1, id1.name, fvf1, fvf2, l.perm, r.perm, v)
+      val (fr2, combinedSnap, snapEq) = quantifiedChunkSupporter.combineFieldSnapshotMaps(fr1, id1.name, qvars, fvf1, fvf2, l.perm, r.perm, v)
       val permSum = PermPlus(perm1, perm2)
       val permSumExp = perm1Exp.map(p1 => ast.PermAdd(p1, perm2Exp.get)())
       val bestHints = if (hints1.nonEmpty) hints1 else hints2
       Some(fr2, QuantifiedFieldChunk(id1, combinedSnap, condition1, condition1Exp, permSum, permSumExp, invs1, singletonRcvr1, singletonRcvr1Exp, bestHints), snapEq)
     case (l@QuantifiedPredicateChunk(id1, qVars1, qVars1Exp, psf1, _, _, perm1, perm1Exp, _, _, _, _),
           r@QuantifiedPredicateChunk(_, qVars2, qVars2Exp, psf2, condition2, condition2Exp, perm2, perm2Exp, invs2, singletonArgs2, singletonArgs2Exp, hints2)) =>
-      val (fr2, combinedSnap, snapEq) = quantifiedChunkSupporter.combinePredicateSnapshotMaps(fr1, id1.name, qVars2, psf1, psf2, l.perm.replace(qVars1, qVars2), r.perm, v)
+      val (fr2, combinedSnap, snapEq) = quantifiedChunkSupporter.combinePredicateSnapshotMaps(fr1, id1.name, qVars2, qvars, psf1, psf2, l.perm.replace(qVars1, qVars2), r.perm, v)
 
       val permSum = PermPlus(perm1.replace(qVars1, qVars2), perm2)
       val permSumExp = perm1Exp.map(p1 => ast.PermAdd(p1.replace(qVars1Exp.get.zip(qVars2Exp.get).toMap), perm2Exp.get)())