Field and predicate specific FVFs

src/main/resources/field_value_functions_axioms.smt2

@@ -11,24 +11,22 @@
 ; The axiom therefore needs to be emitted after the sort wrappers have
 ; been emitted.
 
-(assert (forall ((vs $FVF<$T$>) (ws $FVF<$T$>)) (!
+(assert (forall ((vs $FVF<$FLD$>) (ws $FVF<$FLD$>)) (!
     (=>
       (and
         (Set_equal ($FVF.domain_$FLD$ vs) ($FVF.domain_$FLD$ ws))
         (forall ((x $Ref)) (!
           (=>
             (Set_in x ($FVF.domain_$FLD$ vs))
             (= ($FVF.lookup_$FLD$ vs x) ($FVF.lookup_$FLD$ ws x)))
-          ; :pattern ((Set_in x ($FVF.domain_$FLD$ vs)))
           :pattern (($FVF.lookup_$FLD$ vs x) ($FVF.lookup_$FLD$ ws x))
-          :qid |qp.$FVF<$T$>-eq-inner|
+          :qid |qp.$FVF<$FLD$>-eq-inner|
           )))
       (= vs ws))
-    :pattern (($SortWrappers.$FVF<$T$>To$Snap vs)
-              ($SortWrappers.$FVF<$T$>To$Snap ws)
-;              ($FVF.after_$FLD$ vs ws)
+    :pattern (($SortWrappers.$FVF<$FLD$>To$Snap vs)
+              ($SortWrappers.$FVF<$FLD$>To$Snap ws)
               )
-    :qid |qp.$FVF<$T$>-eq-outer|
+    :qid |qp.$FVF<$FLD$>-eq-outer|
     )))
 
 (assert (forall ((r $Ref) (pm $FPM)) (!

src/main/resources/field_value_functions_declarations.smt2

@@ -7,9 +7,9 @@
 ;   - $S$ is the sort corresponding to the type of the field
 ;   - $T$ is the sanitized name of the sort corresponding to the type of the field
 
-(declare-fun $FVF.domain_$FLD$ ($FVF<$T$>) Set<$Ref>)
-(declare-fun $FVF.lookup_$FLD$ ($FVF<$T$> $Ref) $S$)
-(declare-fun $FVF.after_$FLD$ ($FVF<$T$> $FVF<$T$>) Bool)
+(declare-fun $FVF.domain_$FLD$ ($FVF<$FLD$>) Set<$Ref>)
+(declare-fun $FVF.lookup_$FLD$ ($FVF<$FLD$> $Ref) $S$)
+(declare-fun $FVF.after_$FLD$ ($FVF<$FLD$> $FVF<$FLD$>) Bool)
 (declare-fun $FVF.loc_$FLD$ ($S$ $Ref) Bool)
 (declare-fun $FVF.perm_$FLD$ ($FPM $Ref) $Perm)
-(declare-const $fvfTOP_$FLD$ $FVF<$T$>)
+(declare-const $fvfTOP_$FLD$ $FVF<$FLD$>)

src/main/resources/predicate_snap_functions_axioms.smt2

@@ -10,7 +10,7 @@
 ; The axiom therefore needs to be emitted after the sort wrappers have
 ; been emitted.
 
-(assert (forall ((vs $PSF<$S$>) (ws $PSF<$S$>)) (!
+(assert (forall ((vs $PSF<$PRD$>) (ws $PSF<$PRD$>)) (!
     (=>
       (and
         (Set_equal ($PSF.domain_$PRD$ vs) ($PSF.domain_$PRD$ ws))
@@ -20,14 +20,14 @@
             (= ($PSF.lookup_$PRD$ vs x) ($PSF.lookup_$PRD$ ws x)))
           ; :pattern ((Set_in x ($PSF.domain_$PRD$ vs)))
           :pattern (($PSF.lookup_$PRD$ vs x) ($PSF.lookup_$PRD$ ws x))
-          :qid |qp.$PSF<$S$>-eq-inner|
+          :qid |qp.$PSF<$PRD$>-eq-inner|
           )))
       (= vs ws))
-    :pattern (($SortWrappers.$PSF<$S$>To$Snap vs)
-              ($SortWrappers.$PSF<$S$>To$Snap ws)
+    :pattern (($SortWrappers.$PSF<$PRD$>To$Snap vs)
+              ($SortWrappers.$PSF<$PRD$>To$Snap ws)
 ;              ($PSF.after_$PRD$ vs ws)
               )
-    :qid |qp.$PSF<$S$>-eq-outer|
+    :qid |qp.$PSF<$PRD$>-eq-outer|
     )))
 
 (assert (forall ((s $Snap) (pm $PPM)) (!

src/main/resources/predicate_snap_functions_declarations.smt2

@@ -6,9 +6,9 @@
 ;   - $PRD$ is a Silver predicate name
 ;   - $S$ is the sort corresponding to the type of the predicate arguments
 
-(declare-fun $PSF.domain_$PRD$ ($PSF<$S$>) Set<$Snap>)
-(declare-fun $PSF.lookup_$PRD$ ($PSF<$S$> $Snap) $S$)
-(declare-fun $PSF.after_$PRD$ ($PSF<$S$> $PSF<$S$>) Bool)
+(declare-fun $PSF.domain_$PRD$ ($PSF<$PRD$>) Set<$Snap>)
+(declare-fun $PSF.lookup_$PRD$ ($PSF<$PRD$> $Snap) $S$)
+(declare-fun $PSF.after_$PRD$ ($PSF<$PRD$> $PSF<$PRD$>) Bool)
 (declare-fun $PSF.loc_$PRD$ ($S$ $Snap) Bool)
 (declare-fun $PSF.perm_$PRD$ ($PPM $Snap) $Perm)
-(declare-const $psfTOP_$PRD$ $PSF<$S$>)
+(declare-const $psfTOP_$PRD$ $PSF<$PRD$>)

src/main/scala/decider/TermToSMTLib2Converter.scala

@@ -56,8 +56,8 @@ class TermToSMTLib2Converter
        */
       ""
 
-    case sorts.FieldValueFunction(codomainSort) => text("$FVF<") <> doRender(codomainSort, true) <> ">"
-    case sorts.PredicateSnapFunction(codomainSort) => text("$PSF<") <> doRender(codomainSort, true) <> ">"
+    case sorts.FieldValueFunction(_, fieldName) => text("$FVF<") <> text(fieldName) <> ">"
+    case sorts.PredicateSnapFunction(_, predName) => text("$PSF<") <> text(predName) <> ">"
 
     case sorts.FieldPermFunction() => text("$FPM")
     case sorts.PredicatePermFunction() => text("$PPM")
@@ -271,7 +271,7 @@ class TermToSMTLib2Converter
 //    }
 
     case FieldTrigger(field, fvf, at) => parens(text("$FVF.loc_") <> field <+> (fvf.sort match {
-      case sorts.FieldValueFunction(_) => render(Lookup(field, fvf, at)) <+> render(at)
+      case sorts.FieldValueFunction(_, _) => render(Lookup(field, fvf, at)) <+> render(at)
       case _ => render(fvf) <+> render(at)
     }))
 

src/main/scala/decider/TermToZ3APIConverter.scala

@@ -119,11 +119,10 @@ class TermToZ3APIConverter
          */
         ???
 
-      case sorts.FieldValueFunction(codomainSort) => {
-        val name = convertSortName(codomainSort)
-        ctx.mkUninterpretedSort("$FVF<" + name + ">")
+      case sorts.FieldValueFunction(_, fieldName) => {
+        ctx.mkUninterpretedSort("$FVF<" + fieldName + ">")
       }
-      case sorts.PredicateSnapFunction(codomainSort) => ctx.mkUninterpretedSort("$PSF<" + convertSortName(codomainSort) + ">")
+      case sorts.PredicateSnapFunction(_, predName) => ctx.mkUninterpretedSort("$PSF<" + predName + ">")
 
       case sorts.FieldPermFunction() => ctx.mkUninterpretedSort("$FPM") // text("$FPM")
       case sorts.PredicatePermFunction() => ctx.mkUninterpretedSort("$PPM") // text("$PPM")
@@ -153,8 +152,8 @@ class TermToZ3APIConverter
          */
         ???
 
-      case sorts.FieldValueFunction(codomainSort) => Some(ctx.mkSymbol("$FVF<" + convertSortName(codomainSort) + ">")) //
-      case sorts.PredicateSnapFunction(codomainSort) => Some(ctx.mkSymbol("$PSF<" + convertSortName(codomainSort) + ">"))
+      case sorts.FieldValueFunction(_, fieldName) => Some(ctx.mkSymbol("$FVF<" + fieldName + ">")) //
+      case sorts.PredicateSnapFunction(_, predName) => Some(ctx.mkSymbol("$PSF<" + predName + ">"))
 
       case sorts.FieldPermFunction() => Some(ctx.mkSymbol("$FPM")) // text("$FPM")
       case sorts.PredicatePermFunction() => Some(ctx.mkSymbol("$PPM")) // text("$PPM")
@@ -401,7 +400,7 @@ class TermToZ3APIConverter
         createApp("$FVF.lookup_" + field, Seq(fvf, at), term.sort)
 
       case FieldTrigger(field, fvf, at) => createApp("$FVF.loc_" + field, (fvf.sort match {
-        case sorts.FieldValueFunction(_) => Seq(Lookup(field, fvf, at), at)
+        case sorts.FieldValueFunction(_, _) => Seq(Lookup(field, fvf, at), at)
         case _ => Seq(fvf, at)
       }), term.sort)
 

src/main/scala/logger/writer/TermWriter.scala

@@ -49,8 +49,10 @@ object TermWriter {
       case sorts.Set(elementsSort) => s("Set", elementsSort)
       case sorts.Multiset(elementsSort) => s("Multiset", elementsSort)
       case sorts.UserSort(id) => JsObject("id" -> JsString("UserSort"), "name" -> JsString(id.name))
-      case sorts.FieldValueFunction(codomainSort) => s("FVF", codomainSort)
-      case sorts.PredicateSnapFunction(codomainSort) => s("PSF", codomainSort)
+      case sorts.FieldValueFunction(codomainSort, fieldName) => JsObject("id" -> JsString("FVF"),
+        "fieldName" -> JsString(fieldName), "elementSort" -> toJSON(codomainSort))
+      case sorts.PredicateSnapFunction(codomainSort, predName) => JsObject("id" -> JsString("PSF"),
+        "predName" -> JsString(predName), "elementSort" -> toJSON(codomainSort))
       case simple => JsObject("id" -> JsString(simple.id.name))
     }
   }

src/main/scala/rules/Producer.scala

@@ -334,7 +334,7 @@ object producer extends ProductionRules {
           else Some(forall.triggers)
         evalQuantified(s, Forall, forall.variables, Seq(cond), Seq(acc.loc.rcv, acc.perm), optTrigger, qid, pve, v) {
           case (s1, qvars, Seq(tCond), Seq(tRcvr, tPerm), tTriggers, (auxGlobals, auxNonGlobals), v1) =>
-            val tSnap = sf(sorts.FieldValueFunction(v1.symbolConverter.toSort(acc.loc.field.typ)), v1)
+            val tSnap = sf(sorts.FieldValueFunction(v1.symbolConverter.toSort(acc.loc.field.typ), acc.loc.field.name), v1)
 //            v.decider.assume(PermAtMost(tPerm, FullPerm()))
             quantifiedChunkSupporter.produce(
               s1,
@@ -365,7 +365,7 @@ object producer extends ProductionRules {
           else Some(forall.triggers)
         evalQuantified(s, Forall, forall.variables, Seq(cond), acc.perm +: acc.loc.args, optTrigger, qid, pve, v) {
           case (s1, qvars, Seq(tCond), Seq(tPerm, tArgs @ _*), tTriggers, (auxGlobals, auxNonGlobals), v1) =>
-            val tSnap = sf(sorts.PredicateSnapFunction(s1.predicateSnapMap(predicate)), v1)
+            val tSnap = sf(sorts.PredicateSnapFunction(s1.predicateSnapMap(predicate), predicate.name), v1)
             quantifiedChunkSupporter.produce(
               s1,
               forall,
@@ -397,7 +397,7 @@ object producer extends ProductionRules {
         val qid = MagicWandIdentifier(wand, s.program).toString
         evalQuantified(s, Forall, forall.variables, Seq(cond), bodyVars, optTrigger, qid, pve, v) {
           case (s1, qvars, Seq(tCond), tArgs, tTriggers, (auxGlobals, auxNonGlobals), v1) =>
-            val tSnap = sf(sorts.PredicateSnapFunction(sorts.Snap), v1)
+            val tSnap = sf(sorts.PredicateSnapFunction(sorts.Snap, qid), v1)
             quantifiedChunkSupporter.produce(
               s1,
               forall,

src/main/scala/rules/QuantifiedChunkSupport.scala

@@ -1495,12 +1495,12 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
     val snapshotMapSort =
       resource match {
         case field: ast.Field =>
-          sorts.FieldValueFunction(v.symbolConverter.toSort(field.typ))
+          sorts.FieldValueFunction(v.symbolConverter.toSort(field.typ), field.name)
         case predicate: ast.Predicate =>
           // TODO: Reconsider use of and general design behind s.predicateSnapMap
-          sorts.PredicateSnapFunction(s.predicateSnapMap(predicate))
-        case _: ast.MagicWand =>
-          sorts.PredicateSnapFunction(sorts.Snap)
+          sorts.PredicateSnapFunction(s.predicateSnapMap(predicate), predicate.name)
+        case w: ast.MagicWand =>
+          sorts.PredicateSnapFunction(sorts.Snap, MagicWandIdentifier(w, s.program).toString)
         case _ =>
           sys.error(s"Found yet unsupported resource $resource (${resource.getClass.getSimpleName})")
       }

src/main/scala/state/Chunks.scala

@@ -131,7 +131,7 @@ case class QuantifiedMagicWandChunk(id: MagicWandIdentifier,
                                     hints: Seq[Term] = Nil)
     extends QuantifiedBasicChunk {
 
-  require(wsf.sort == terms.sorts.PredicateSnapFunction(sorts.Snap), s"Quantified magic wand chunk values must be of sort MagicWandSnapFunction ($wsf), but found ${wsf.sort}")
+  require(wsf.sort.isInstanceOf[terms.sorts.PredicateSnapFunction] && wsf.sort.asInstanceOf[terms.sorts.PredicateSnapFunction].codomainSort == sorts.Snap, s"Quantified magic wand chunk values must be of sort MagicWandSnapFunction ($wsf), but found ${wsf.sort}")
   require(perm.sort == sorts.Perm, s"Permissions $perm must be of sort Perm, but found ${perm.sort}")
 
   override val resourceID = MagicWandID

src/main/scala/state/Terms.scala

@@ -65,13 +65,13 @@ object sorts {
     override lazy val toString = id.toString
   }
 
-  case class FieldValueFunction(codomainSort: Sort) extends Sort {
-    val id = Identifier(s"FVF[$codomainSort]")
+  case class FieldValueFunction(codomainSort: Sort, fieldName: String) extends Sort {
+    val id = Identifier(s"FVF[$fieldName]")
     override lazy val toString = id.toString
   }
 
-  case class PredicateSnapFunction(codomainSort: Sort) extends Sort {
-    val id = Identifier(s"PSF[$codomainSort]")
+  case class PredicateSnapFunction(codomainSort: Sort, predName: String) extends Sort {
+    val id = Identifier(s"PSF[$predName]")
     override lazy val toString = id.toString
   }
 

src/main/scala/supporters/SnapshotSupporter.scala

@@ -82,7 +82,7 @@ class DefaultSnapshotSupporter(symbolConverter: SymbolConverter) extends Snapsho
         getOptimalSnapshotSortFromPair(a1, a2, () => findCommonSort())
 
       case QuantifiedPermissionAssertion(_, _, acc: ast.FieldAccessPredicate) =>
-        (sorts.FieldValueFunction(symbolConverter.toSort(acc.loc.field.typ)), false)
+        (sorts.FieldValueFunction(symbolConverter.toSort(acc.loc.field.typ), acc.loc.field.name), false)
 
       case _ =>
         (sorts.Snap, false)

src/main/scala/supporters/qps/FieldValueFunctionsContributor.scala

@@ -60,8 +60,7 @@ class DefaultFieldValueFunctionsContributor(preambleReader: PreambleReader[Strin
     // WARNING: DefaultSetsContributor contributes a sort that is due to QPs over fields
 
     collectedSorts = (
-        collectedFields.map(f => sorts.FieldValueFunction(symbolConverter.toSort(f.typ)))
-      + sorts.FieldValueFunction(sorts.Ref))
+        collectedFields.map(f => sorts.FieldValueFunction(symbolConverter.toSort(f.typ), f.name)))
 
     collectedFunctionDecls = generateFunctionDecls
     collectedAxioms = generateAxioms

src/main/scala/supporters/qps/PredicateAndWandSnapFunctionsContributor.scala

@@ -94,13 +94,12 @@ class DefaultPredicateAndWandSnapFunctionsContributor(preambleReader: PreambleRe
 
     // WARNING: DefaultSetsContributor contributes a sort that is due to QPs over predicates and wands
 
-    collectedSorts =
-      collectedPredicates.map(predicate =>
-        sorts.PredicateSnapFunction(predicateSnapGenerator.getSnap(predicate)._1))
+    collectedSorts = collectedPredicates.map(predicate =>
+        sorts.PredicateSnapFunction(predicateSnapGenerator.getSnap(predicate)._1, predicate.name)) ++ collectedWandIdentifiers.map(identifier => sorts.PredicateSnapFunction(sorts.Snap, identifier.toString))
 
-    if (collectedPredicates.nonEmpty || collectedWandIdentifiers.nonEmpty) {
-      collectedSorts += sorts.PredicateSnapFunction(sorts.Snap)
-    }
+    //if (collectedPredicates.nonEmpty || collectedWandIdentifiers.nonEmpty) {
+    //  collectedSorts += sorts.PredicateSnapFunction(sorts.Snap, "Wand")
+    //}
 
     collectedFunctionDecls = generateFunctionDecls
     collectedAxioms = generateAxioms