Skip to content

Commit 815835e

Browse files
marcoeilersmarcoeilers
authored
Merge pull request #649 from viperproject/meilers_field_specific_fvfs
Field and predicate specific FVFs
2 parents 2c417ef + 05ebd21 commit 815835e

14 files changed

Lines changed: 48 additions & 54 deletions

‎src/main/resources/field_value_functions_axioms.smt2‎

Lines changed: 5 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -11,24 +11,22 @@
1111
; The axiom therefore needs to be emitted after the sort wrappers have
1212
; been emitted.
1313

14-
(assert (forall ((vs $FVF<$T$>) (ws $FVF<$T$>)) (!
14+
(assert (forall ((vs $FVF<$FLD$>) (ws $FVF<$FLD$>)) (!
1515
(=>
1616
(and
1717
(Set_equal ($FVF.domain_$FLD$ vs) ($FVF.domain_$FLD$ ws))
1818
(forall ((x $Ref)) (!
1919
(=>
2020
(Set_in x ($FVF.domain_$FLD$ vs))
2121
(= ($FVF.lookup_$FLD$ vs x) ($FVF.lookup_$FLD$ ws x)))
22-
; :pattern ((Set_in x ($FVF.domain_$FLD$ vs)))
2322
:pattern (($FVF.lookup_$FLD$ vs x) ($FVF.lookup_$FLD$ ws x))
24-
:qid |qp.$FVF<$T$>-eq-inner|
23+
:qid |qp.$FVF<$FLD$>-eq-inner|
2524
)))
2625
(= vs ws))
27-
:pattern (($SortWrappers.$FVF<$T$>To$Snap vs)
28-
($SortWrappers.$FVF<$T$>To$Snap ws)
29-
; ($FVF.after_$FLD$ vs ws)
26+
:pattern (($SortWrappers.$FVF<$FLD$>To$Snap vs)
27+
($SortWrappers.$FVF<$FLD$>To$Snap ws)
3028
)
31-
:qid |qp.$FVF<$T$>-eq-outer|
29+
:qid |qp.$FVF<$FLD$>-eq-outer|
3230
)))
3331

3432
(assert (forall ((r $Ref) (pm $FPM)) (!

‎src/main/resources/field_value_functions_declarations.smt2‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -7,9 +7,9 @@
77
; - $S$ is the sort corresponding to the type of the field
88
; - $T$ is the sanitized name of the sort corresponding to the type of the field
99

10-
(declare-fun $FVF.domain_$FLD$ ($FVF<$T$>) Set<$Ref>)
11-
(declare-fun $FVF.lookup_$FLD$ ($FVF<$T$> $Ref) $S$)
12-
(declare-fun $FVF.after_$FLD$ ($FVF<$T$> $FVF<$T$>) Bool)
10+
(declare-fun $FVF.domain_$FLD$ ($FVF<$FLD$>) Set<$Ref>)
11+
(declare-fun $FVF.lookup_$FLD$ ($FVF<$FLD$> $Ref) $S$)
12+
(declare-fun $FVF.after_$FLD$ ($FVF<$FLD$> $FVF<$FLD$>) Bool)
1313
(declare-fun $FVF.loc_$FLD$ ($S$ $Ref) Bool)
1414
(declare-fun $FVF.perm_$FLD$ ($FPM $Ref) $Perm)
15-
(declare-const $fvfTOP_$FLD$ $FVF<$T$>)
15+
(declare-const $fvfTOP_$FLD$ $FVF<$FLD$>)

‎src/main/resources/predicate_snap_functions_axioms.smt2‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@
1010
; The axiom therefore needs to be emitted after the sort wrappers have
1111
; been emitted.
1212

13-
(assert (forall ((vs $PSF<$S$>) (ws $PSF<$S$>)) (!
13+
(assert (forall ((vs $PSF<$PRD$>) (ws $PSF<$PRD$>)) (!
1414
(=>
1515
(and
1616
(Set_equal ($PSF.domain_$PRD$ vs) ($PSF.domain_$PRD$ ws))
@@ -20,14 +20,14 @@
2020
(= ($PSF.lookup_$PRD$ vs x) ($PSF.lookup_$PRD$ ws x)))
2121
; :pattern ((Set_in x ($PSF.domain_$PRD$ vs)))
2222
:pattern (($PSF.lookup_$PRD$ vs x) ($PSF.lookup_$PRD$ ws x))
23-
:qid |qp.$PSF<$S$>-eq-inner|
23+
:qid |qp.$PSF<$PRD$>-eq-inner|
2424
)))
2525
(= vs ws))
26-
:pattern (($SortWrappers.$PSF<$S$>To$Snap vs)
27-
($SortWrappers.$PSF<$S$>To$Snap ws)
26+
:pattern (($SortWrappers.$PSF<$PRD$>To$Snap vs)
27+
($SortWrappers.$PSF<$PRD$>To$Snap ws)
2828
; ($PSF.after_$PRD$ vs ws)
2929
)
30-
:qid |qp.$PSF<$S$>-eq-outer|
30+
:qid |qp.$PSF<$PRD$>-eq-outer|
3131
)))
3232

3333
(assert (forall ((s $Snap) (pm $PPM)) (!

‎src/main/resources/predicate_snap_functions_declarations.smt2‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -6,9 +6,9 @@
66
; - $PRD$ is a Silver predicate name
77
; - $S$ is the sort corresponding to the type of the predicate arguments
88

9-
(declare-fun $PSF.domain_$PRD$ ($PSF<$S$>) Set<$Snap>)
10-
(declare-fun $PSF.lookup_$PRD$ ($PSF<$S$> $Snap) $S$)
11-
(declare-fun $PSF.after_$PRD$ ($PSF<$S$> $PSF<$S$>) Bool)
9+
(declare-fun $PSF.domain_$PRD$ ($PSF<$PRD$>) Set<$Snap>)
10+
(declare-fun $PSF.lookup_$PRD$ ($PSF<$PRD$> $Snap) $S$)
11+
(declare-fun $PSF.after_$PRD$ ($PSF<$PRD$> $PSF<$PRD$>) Bool)
1212
(declare-fun $PSF.loc_$PRD$ ($S$ $Snap) Bool)
1313
(declare-fun $PSF.perm_$PRD$ ($PPM $Snap) $Perm)
14-
(declare-const $psfTOP_$PRD$ $PSF<$S$>)
14+
(declare-const $psfTOP_$PRD$ $PSF<$PRD$>)

‎src/main/scala/decider/TermToSMTLib2Converter.scala‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -56,8 +56,8 @@ class TermToSMTLib2Converter
5656
*/
5757
""
5858

59-
case sorts.FieldValueFunction(codomainSort) => text("$FVF<") <> doRender(codomainSort, true) <> ">"
60-
case sorts.PredicateSnapFunction(codomainSort) => text("$PSF<") <> doRender(codomainSort, true) <> ">"
59+
case sorts.FieldValueFunction(_, fieldName) => text("$FVF<") <> text(fieldName) <> ">"
60+
case sorts.PredicateSnapFunction(_, predName) => text("$PSF<") <> text(predName) <> ">"
6161

6262
case sorts.FieldPermFunction() => text("$FPM")
6363
case sorts.PredicatePermFunction() => text("$PPM")
@@ -271,7 +271,7 @@ class TermToSMTLib2Converter
271271
// }
272272

273273
case FieldTrigger(field, fvf, at) => parens(text("$FVF.loc_") <> field <+> (fvf.sort match {
274-
case sorts.FieldValueFunction(_) => render(Lookup(field, fvf, at)) <+> render(at)
274+
case sorts.FieldValueFunction(_, _) => render(Lookup(field, fvf, at)) <+> render(at)
275275
case _ => render(fvf) <+> render(at)
276276
}))
277277

‎src/main/scala/decider/TermToZ3APIConverter.scala‎

Lines changed: 6 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -119,11 +119,10 @@ class TermToZ3APIConverter
119119
*/
120120
???
121121

122-
case sorts.FieldValueFunction(codomainSort) => {
123-
val name = convertSortName(codomainSort)
124-
ctx.mkUninterpretedSort("$FVF<" + name + ">")
122+
case sorts.FieldValueFunction(_, fieldName) => {
123+
ctx.mkUninterpretedSort("$FVF<" + fieldName + ">")
125124
}
126-
case sorts.PredicateSnapFunction(codomainSort) => ctx.mkUninterpretedSort("$PSF<" + convertSortName(codomainSort) + ">")
125+
case sorts.PredicateSnapFunction(_, predName) => ctx.mkUninterpretedSort("$PSF<" + predName + ">")
127126

128127
case sorts.FieldPermFunction() => ctx.mkUninterpretedSort("$FPM") // text("$FPM")
129128
case sorts.PredicatePermFunction() => ctx.mkUninterpretedSort("$PPM") // text("$PPM")
@@ -153,8 +152,8 @@ class TermToZ3APIConverter
153152
*/
154153
???
155154

156-
case sorts.FieldValueFunction(codomainSort) => Some(ctx.mkSymbol("$FVF<" + convertSortName(codomainSort) + ">")) //
157-
case sorts.PredicateSnapFunction(codomainSort) => Some(ctx.mkSymbol("$PSF<" + convertSortName(codomainSort) + ">"))
155+
case sorts.FieldValueFunction(_, fieldName) => Some(ctx.mkSymbol("$FVF<" + fieldName + ">")) //
156+
case sorts.PredicateSnapFunction(_, predName) => Some(ctx.mkSymbol("$PSF<" + predName + ">"))
158157

159158
case sorts.FieldPermFunction() => Some(ctx.mkSymbol("$FPM")) // text("$FPM")
160159
case sorts.PredicatePermFunction() => Some(ctx.mkSymbol("$PPM")) // text("$PPM")
@@ -401,7 +400,7 @@ class TermToZ3APIConverter
401400
createApp("$FVF.lookup_" + field, Seq(fvf, at), term.sort)
402401

403402
case FieldTrigger(field, fvf, at) => createApp("$FVF.loc_" + field, (fvf.sort match {
404-
case sorts.FieldValueFunction(_) => Seq(Lookup(field, fvf, at), at)
403+
case sorts.FieldValueFunction(_, _) => Seq(Lookup(field, fvf, at), at)
405404
case _ => Seq(fvf, at)
406405
}), term.sort)
407406

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

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -49,8 +49,10 @@ object TermWriter {
4949
case sorts.Set(elementsSort) => s("Set", elementsSort)
5050
case sorts.Multiset(elementsSort) => s("Multiset", elementsSort)
5151
case sorts.UserSort(id) => JsObject("id" -> JsString("UserSort"), "name" -> JsString(id.name))
52-
case sorts.FieldValueFunction(codomainSort) => s("FVF", codomainSort)
53-
case sorts.PredicateSnapFunction(codomainSort) => s("PSF", codomainSort)
52+
case sorts.FieldValueFunction(codomainSort, fieldName) => JsObject("id" -> JsString("FVF"),
53+
"fieldName" -> JsString(fieldName), "elementSort" -> toJSON(codomainSort))
54+
case sorts.PredicateSnapFunction(codomainSort, predName) => JsObject("id" -> JsString("PSF"),
55+
"predName" -> JsString(predName), "elementSort" -> toJSON(codomainSort))
5456
case simple => JsObject("id" -> JsString(simple.id.name))
5557
}
5658
}

‎src/main/scala/rules/Producer.scala‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -334,7 +334,7 @@ object producer extends ProductionRules {
334334
else Some(forall.triggers)
335335
evalQuantified(s, Forall, forall.variables, Seq(cond), Seq(acc.loc.rcv, acc.perm), optTrigger, qid, pve, v) {
336336
case (s1, qvars, Seq(tCond), Seq(tRcvr, tPerm), tTriggers, (auxGlobals, auxNonGlobals), v1) =>
337-
val tSnap = sf(sorts.FieldValueFunction(v1.symbolConverter.toSort(acc.loc.field.typ)), v1)
337+
val tSnap = sf(sorts.FieldValueFunction(v1.symbolConverter.toSort(acc.loc.field.typ), acc.loc.field.name), v1)
338338
// v.decider.assume(PermAtMost(tPerm, FullPerm()))
339339
quantifiedChunkSupporter.produce(
340340
s1,
@@ -365,7 +365,7 @@ object producer extends ProductionRules {
365365
else Some(forall.triggers)
366366
evalQuantified(s, Forall, forall.variables, Seq(cond), acc.perm +: acc.loc.args, optTrigger, qid, pve, v) {
367367
case (s1, qvars, Seq(tCond), Seq(tPerm, tArgs @ _*), tTriggers, (auxGlobals, auxNonGlobals), v1) =>
368-
val tSnap = sf(sorts.PredicateSnapFunction(s1.predicateSnapMap(predicate)), v1)
368+
val tSnap = sf(sorts.PredicateSnapFunction(s1.predicateSnapMap(predicate), predicate.name), v1)
369369
quantifiedChunkSupporter.produce(
370370
s1,
371371
forall,
@@ -397,7 +397,7 @@ object producer extends ProductionRules {
397397
val qid = MagicWandIdentifier(wand, s.program).toString
398398
evalQuantified(s, Forall, forall.variables, Seq(cond), bodyVars, optTrigger, qid, pve, v) {
399399
case (s1, qvars, Seq(tCond), tArgs, tTriggers, (auxGlobals, auxNonGlobals), v1) =>
400-
val tSnap = sf(sorts.PredicateSnapFunction(sorts.Snap), v1)
400+
val tSnap = sf(sorts.PredicateSnapFunction(sorts.Snap, qid), v1)
401401
quantifiedChunkSupporter.produce(
402402
s1,
403403
forall,

‎src/main/scala/rules/QuantifiedChunkSupport.scala‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1495,12 +1495,12 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
14951495
val snapshotMapSort =
14961496
resource match {
14971497
case field: ast.Field =>
1498-
sorts.FieldValueFunction(v.symbolConverter.toSort(field.typ))
1498+
sorts.FieldValueFunction(v.symbolConverter.toSort(field.typ), field.name)
14991499
case predicate: ast.Predicate =>
15001500
// TODO: Reconsider use of and general design behind s.predicateSnapMap
1501-
sorts.PredicateSnapFunction(s.predicateSnapMap(predicate))
1502-
case _: ast.MagicWand =>
1503-
sorts.PredicateSnapFunction(sorts.Snap)
1501+
sorts.PredicateSnapFunction(s.predicateSnapMap(predicate), predicate.name)
1502+
case w: ast.MagicWand =>
1503+
sorts.PredicateSnapFunction(sorts.Snap, MagicWandIdentifier(w, s.program).toString)
15041504
case _ =>
15051505
sys.error(s"Found yet unsupported resource $resource (${resource.getClass.getSimpleName})")
15061506
}

‎src/main/scala/state/Chunks.scala‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -131,7 +131,7 @@ case class QuantifiedMagicWandChunk(id: MagicWandIdentifier,
131131
hints: Seq[Term] = Nil)
132132
extends QuantifiedBasicChunk {
133133

134-
require(wsf.sort == terms.sorts.PredicateSnapFunction(sorts.Snap), s"Quantified magic wand chunk values must be of sort MagicWandSnapFunction ($wsf), but found ${wsf.sort}")
134+
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}")
135135
require(perm.sort == sorts.Perm, s"Permissions $perm must be of sort Perm, but found ${perm.sort}")
136136

137137
override val resourceID = MagicWandID

0 commit comments

Comments
 (0)
⚡