Skip to content

Commit d27a6c9

Browse files
marcoeilersmarcoeilers
authored
Record snapshots in FunctionRecorder with context information (#928)
1 parent 9b05c87 commit d27a6c9

5 files changed

Lines changed: 84 additions & 33 deletions

File tree

‎silver‎

‎src/main/scala/rules/Evaluator.scala‎

Lines changed: 8 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -373,12 +373,12 @@ object evaluator extends EvaluationRules {
373373
evalInOldState(s, lbl, e0, pve, v)((s1, t0, e0New, v1) =>
374374
Q(s1, t0, e0New.map(ast.LabelledOld(_, lbl)(old.pos, old.info, old.errT)), v1))}
375375

376-
case ast.Let(x, e0, e1) =>
376+
case l@ast.Let(x, e0, e1) =>
377377
eval(s, e0, pve, v)((s1, t0, e0New, v1) => {
378378
val t = v1.decider.appliedFresh("letvar", v1.symbolConverter.toSort(x.typ), s1.relevantQuantifiedVariables.map(_._1))
379379
val debugExp = Option.when(withExp)(DebugExp.createInstance("letvar assignment", InsertionOrderedSet(DebugExp.createInstance(ast.EqCmp(x.localVar, e0)(), ast.EqCmp(x.localVar, e0New.get)()))))
380380
v1.decider.assumeDefinition(BuiltinEquals(t, t0), debugExp)
381-
val newFuncRec = s1.functionRecorder.recordFreshSnapshot(t.applicable.asInstanceOf[Function])
381+
val newFuncRec = s1.functionRecorder.recordFreshSnapshot(t.applicable.asInstanceOf[Function]).enterLet(l)
382382
val possibleTriggersBefore = if (s1.recordPossibleTriggers) s1.possibleTriggers else Map.empty
383383
eval(s1.copy(g = s1.g + (x.localVar, (t0, e0New)), functionRecorder = newFuncRec), e1, pve, v1)((s2, t2, e1New, v2) => {
384384
val newPossibleTriggers = if (s2.recordPossibleTriggers) {
@@ -388,7 +388,8 @@ object evaluator extends EvaluationRules {
388388
} else {
389389
s2.possibleTriggers
390390
}
391-
Q(s2.copy(possibleTriggers = newPossibleTriggers), t2, e0New.map(ast.Let(x, _, e1New.get)(e.pos, e.info, e.errT)), v2)
391+
val s3 = s2.copy(possibleTriggers = newPossibleTriggers, functionRecorder = s2.functionRecorder.leaveLet(l))
392+
Q(s3, t2, e0New.map(ast.Let(x, _, e1New.get)(e.pos, e.info, e.errT)), v2)
392393
})
393394
})
394395

@@ -828,7 +829,8 @@ object evaluator extends EvaluationRules {
828829
}
829830
}
830831
val name = s"prog.$posString"
831-
evalQuantified(s, qantOp, eQuant.variables, Nil, Seq(body), Some(eTriggers), name, pve, v){
832+
val s0 = s.copy(functionRecorder = s.functionRecorder.enterQuantifiedExp(sourceQuant))
833+
evalQuantified(s0, qantOp, eQuant.variables, Nil, Seq(body), Some(eTriggers), name, pve, v){
832834
case (s1, tVars, eVars, _, _, Some((Seq(tBody), bodyNew, tTriggers, (tAuxGlobal, tAux), auxExps)), v1) =>
833835
val tAuxHeapIndep = tAux.flatMap(v.quantifierSupporter.makeTriggersHeapIndependent(_, v1.decider.fresh))
834836
val auxGlobalsExp = auxExps.map(_._1)
@@ -857,7 +859,8 @@ object evaluator extends EvaluationRules {
857859

858860
val tQuant = Quantification(qantOp, tVars, tBody, tTriggers, name, quantWeight)
859861
val eQuantNew = Option.when(withExp)(buildQuantExp(qantOp, eVars.get, bodyNew.get.head, Seq.empty))
860-
Q(s1, tQuant, eQuantNew, v1)
862+
val s2 = s1.copy(functionRecorder = s1.functionRecorder.leaveQuantifiedExp(sourceQuant))
863+
Q(s2, tQuant, eQuantNew, v1)
861864
case (s1, _, _, _, _, None, v1) =>
862865
// This should not happen unless the current path is dead.
863866
if (v1.decider.checkSmoke(true)) {

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -100,8 +100,8 @@ class FunctionData(val programFunction: ast.Function,
100100
*/
101101

102102
private[functions] var verificationFailures: Seq[FatalResult] = Vector.empty
103-
private[functions] var locToSnap: Map[ast.LocationAccess, Term] = Map.empty
104-
private[functions] var fappToSnap: Map[ast.FuncApp, Term] = Map.empty
103+
private[functions] var locToSnap: Map[(ast.LocationAccess, Seq[ExpContext]), Term] = Map.empty
104+
private[functions] var fappToSnap: Map[(ast.FuncApp, Seq[ExpContext]), Term] = Map.empty
105105
private[this] var freshFvfsAndDomains: InsertionOrderedSet[SnapshotMapDefinition] = InsertionOrderedSet.empty
106106
private[this] var freshFieldInvs: InsertionOrderedSet[InverseFunctions] = InsertionOrderedSet.empty
107107
private[this] var freshConstrainedVars: InsertionOrderedSet[(Var, Term)] = InsertionOrderedSet.empty
@@ -251,7 +251,7 @@ class FunctionData(val programFunction: ast.Function,
251251

252252
/* TODO: Don't use translatePrecondition - refactor expressionTranslator */
253253
val args = (
254-
expressionTranslator.getOrFail(locToSnap, predAcc, sorts.Snap, Option.when(Verifier.config.enableDebugging())(PUnknown()))
254+
expressionTranslator.getOrFail(locToSnap, predAcc, Seq(), sorts.Snap, Option.when(Verifier.config.enableDebugging())(PUnknown()))
255255
+: expressionTranslator.translatePrecondition(program, predAcc.args, this))
256256

257257
val fapp = App(triggerFunction, args)

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

Lines changed: 56 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -19,10 +19,10 @@ import viper.silicon.state.terms._
1919
// etc. as well.
2020
trait FunctionRecorder extends Mergeable[FunctionRecorder] {
2121
def data: Option[FunctionData]
22-
private[functions] def locToSnaps: Map[ast.LocationAccess, InsertionOrderedSet[(Stack[Term], Term)]]
23-
def locToSnap: Map[ast.LocationAccess, Term]
24-
private[functions] def fappToSnaps: Map[ast.FuncApp, InsertionOrderedSet[(Stack[Term], Term)]]
25-
def fappToSnap: Map[ast.FuncApp, Term]
22+
private[functions] def locToSnaps: Map[(ast.LocationAccess, Seq[ExpContext]), InsertionOrderedSet[(Stack[Term], Term)]]
23+
def locToSnap: Map[(ast.LocationAccess, Seq[ExpContext]), Term]
24+
private[functions] def fappToSnaps: Map[(ast.FuncApp, Seq[ExpContext]), InsertionOrderedSet[(Stack[Term], Term)]]
25+
def fappToSnap: Map[(ast.FuncApp, Seq[ExpContext]), Term]
2626
def freshFvfsAndDomains: InsertionOrderedSet[SnapshotMapDefinition]
2727
def freshFieldInvs: InsertionOrderedSet[InverseFunctions]
2828
def freshConstrainedVars: InsertionOrderedSet[(Var, Term)]
@@ -41,19 +41,28 @@ trait FunctionRecorder extends Mergeable[FunctionRecorder] {
4141
def recordFreshMacro(decl: MacroDecl): FunctionRecorder
4242
def depth: Int
4343
def changeDepthBy(delta: Int): FunctionRecorder
44+
def enterLet(l: ast.Let): FunctionRecorder
45+
def leaveLet(l: ast.Let): FunctionRecorder
46+
def enterQuantifiedExp(q: ast.QuantifiedExp): FunctionRecorder
47+
def leaveQuantifiedExp(q: ast.QuantifiedExp): FunctionRecorder
4448
}
4549

50+
trait ExpContext
51+
case class LetContext(l: ast.Let) extends ExpContext
52+
case class QuantifierContext(q: ast.QuantifiedExp) extends ExpContext
53+
4654
case class ActualFunctionRecorder(private val _data: FunctionData,
47-
private[functions] val locToSnaps: Map[ast.LocationAccess, InsertionOrderedSet[(Stack[Term], Term)]] = Map(),
48-
private[functions] val fappToSnaps: Map[ast.FuncApp, InsertionOrderedSet[(Stack[Term], Term)]] = Map(),
55+
private[functions] val locToSnaps: Map[(ast.LocationAccess, Seq[ExpContext]), InsertionOrderedSet[(Stack[Term], Term)]] = Map(),
56+
private[functions] val fappToSnaps: Map[(ast.FuncApp, Seq[ExpContext]), InsertionOrderedSet[(Stack[Term], Term)]] = Map(),
4957
freshFvfsAndDomains: InsertionOrderedSet[SnapshotMapDefinition] = InsertionOrderedSet(),
5058
freshFieldInvs: InsertionOrderedSet[InverseFunctions] = InsertionOrderedSet(),
5159
freshConstrainedVars: InsertionOrderedSet[(Var, Term)] = InsertionOrderedSet(),
5260
freshConstraints: InsertionOrderedSet[Term] = InsertionOrderedSet(),
5361
freshSnapshots: InsertionOrderedSet[Function] = InsertionOrderedSet(),
5462
freshPathSymbols: InsertionOrderedSet[Function] = InsertionOrderedSet(),
5563
freshMacros: InsertionOrderedSet[MacroDecl] = InsertionOrderedSet(),
56-
depth: Int = 0)
64+
depth: Int = 0,
65+
private val _context: Seq[ExpContext] = Seq())
5766
extends FunctionRecorder {
5867

5968
/* Depth is intended to reflect how often a nested function application or unfolding expression
@@ -93,8 +102,8 @@ case class ActualFunctionRecorder(private val _data: FunctionData,
93102
val data = Some(_data)
94103

95104
private def exprToSnap[E <: ast.Exp]
96-
(recordings: Map[E, InsertionOrderedSet[(Stack[Term], Term)]])
97-
: Map[E, Term] = {
105+
(recordings: Map[(E, Seq[ExpContext]), InsertionOrderedSet[(Stack[Term], Term)]])
106+
: Map[(E, Seq[ExpContext]), Term] = {
98107

99108
recordings.map { case (expr, guardsToSnap) =>
100109
expr -> toTerm(guardsToSnap, None)
@@ -148,20 +157,20 @@ case class ActualFunctionRecorder(private val _data: FunctionData,
148157
}
149158
}
150159

151-
def locToSnap: Map[ast.LocationAccess, Term] = exprToSnap(locToSnaps)
152-
def fappToSnap: Map[ast.FuncApp, Term] = exprToSnap(fappToSnaps)
160+
def locToSnap: Map[(ast.LocationAccess, Seq[ExpContext]), Term] = exprToSnap(locToSnaps)
161+
def fappToSnap: Map[(ast.FuncApp, Seq[ExpContext]), Term] = exprToSnap(fappToSnaps)
153162

154163
private def recordExpressionSnapshot[E <: ast.Exp]
155164
(loc: E,
156165
guards: Stack[Term],
157166
snap: Term,
158-
recordings: Map[E, InsertionOrderedSet[(Stack[Term], Term)]])
159-
: Option[Map[E, InsertionOrderedSet[(Stack[Term], Term)]]] = {
167+
recordings: Map[(E, Seq[ExpContext]), InsertionOrderedSet[(Stack[Term], Term)]])
168+
: Option[Map[(E, Seq[ExpContext]), InsertionOrderedSet[(Stack[Term], Term)]]] = {
160169

161170
if (depth == 0) {
162-
val guardsToSnaps = recordings.getOrElse(loc, InsertionOrderedSet()) + (guards -> snap)
171+
val guardsToSnaps = recordings.getOrElse((loc, _context), InsertionOrderedSet()) + (guards -> snap)
163172

164-
Some(recordings + (loc -> guardsToSnaps))
173+
Some(recordings + ((loc, _context) -> guardsToSnaps))
165174
} else {
166175
None
167176
}
@@ -212,6 +221,30 @@ case class ActualFunctionRecorder(private val _data: FunctionData,
212221
def changeDepthBy(delta: Int): ActualFunctionRecorder =
213222
copy(depth = depth + delta)
214223

224+
def enterLet(l: ast.Let): FunctionRecorder = {
225+
copy(_context = _context :+ LetContext(l))
226+
}
227+
228+
def leaveLet(l: ast.Let): FunctionRecorder = {
229+
assert(_context.nonEmpty && (_context.last match {
230+
case LetContext(`l`) => true
231+
case _ => false
232+
}))
233+
copy(_context = _context.init)
234+
}
235+
236+
def enterQuantifiedExp(q: ast.QuantifiedExp): FunctionRecorder = {
237+
copy(_context = _context :+ QuantifierContext(q))
238+
}
239+
240+
def leaveQuantifiedExp(q: ast.QuantifiedExp): FunctionRecorder = {
241+
assert(_context.nonEmpty && (_context.last match {
242+
case QuantifierContext(`q`) => true
243+
case _ => false
244+
}))
245+
copy(_context = _context.init)
246+
}
247+
215248
def merge(other: FunctionRecorder): ActualFunctionRecorder = {
216249
if (depth > 1) return this
217250

@@ -271,10 +304,10 @@ case class ActualFunctionRecorder(private val _data: FunctionData,
271304

272305
case object NoopFunctionRecorder extends FunctionRecorder {
273306
val data: Option[FunctionData] = None
274-
private[functions] val fappToSnaps: Map[ast.FuncApp, InsertionOrderedSet[(Stack[Term], Term)]] = Map.empty
275-
val fappToSnap: Map[ast.FuncApp, Term] = Map.empty
276-
private[functions] val locToSnaps: Map[ast.LocationAccess, InsertionOrderedSet[(Stack[Term], Term)]] = Map.empty
277-
val locToSnap: Map[ast.LocationAccess, Term] = Map.empty
307+
private[functions] val fappToSnaps: Map[(ast.FuncApp, Seq[ExpContext]), InsertionOrderedSet[(Stack[Term], Term)]] = Map.empty
308+
val fappToSnap: Map[(ast.FuncApp, Seq[ExpContext]), Term] = Map.empty
309+
private[functions] val locToSnaps: Map[(ast.LocationAccess, Seq[ExpContext]), InsertionOrderedSet[(Stack[Term], Term)]] = Map.empty
310+
val locToSnap: Map[(ast.LocationAccess, Seq[ExpContext]), Term] = Map.empty
278311
val freshFvfsAndDomains: InsertionOrderedSet[SnapshotMapDefinition] = InsertionOrderedSet.empty
279312
val freshFieldInvs: InsertionOrderedSet[InverseFunctions] = InsertionOrderedSet.empty
280313
val freshConstrainedVars: InsertionOrderedSet[(Var, Term)] = InsertionOrderedSet.empty
@@ -300,4 +333,8 @@ case object NoopFunctionRecorder extends FunctionRecorder {
300333
def recordPathSymbol(symbol: Function): NoopFunctionRecorder.type = this
301334
def recordFreshMacro(decl: MacroDecl): NoopFunctionRecorder.type = this
302335
def changeDepthBy(delta: Int): NoopFunctionRecorder.type = this
336+
def enterLet(l: ast.Let): FunctionRecorder = this
337+
def leaveLet(l: ast.Let): FunctionRecorder = this
338+
def enterQuantifiedExp(q: ast.QuantifiedExp): FunctionRecorder = this
339+
def leaveQuantifiedExp(q: ast.QuantifiedExp): FunctionRecorder = this
303340
}

‎src/main/scala/supporters/functions/HeapAccessReplacingExpressionTranslator.scala‎

Lines changed: 16 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -34,6 +34,7 @@ class HeapAccessReplacingExpressionTranslator(symbolConverter: SymbolConverter,
3434
private var data: FunctionData = _
3535
private var ignoreAccessPredicates = false
3636
private var failed = false
37+
private var context: Seq[ExpContext] = Seq.empty
3738

3839
var functionData: Map[ast.Function, FunctionData] = _
3940

@@ -95,6 +96,13 @@ class HeapAccessReplacingExpressionTranslator(symbolConverter: SymbolConverter,
9596
case q: ast.Forall if !q.isPure && ignoreAccessPredicates => True
9697

9798
case _: ast.Result => data.formalResult
99+
case l@ast.Let(lvd, e, body) =>
100+
val bvar = translate(toSort)(lvd.localVar)
101+
val tE = translate(toSort)(e)
102+
context = context :+ LetContext(l)
103+
val tBody = translate(toSort)(body)
104+
context = context.init
105+
Let(bvar.asInstanceOf[Var], tE, tBody)
98106

99107
case v: ast.AbstractLocalVar =>
100108
data.formalArgs.get(v) match {
@@ -114,18 +122,21 @@ class HeapAccessReplacingExpressionTranslator(symbolConverter: SymbolConverter,
114122
* occurrence of 'x@i' is replaced by 'x', for all variables 'x@i' where the prefix
115123
* 'x' is bound by the surrounding quantifier.
116124
*/
125+
context = context :+ QuantifierContext(eQuant)
117126
val tQuant = super.translate(symbolConverter.toSort)(eQuant).asInstanceOf[Quantification]
118127
val names = tQuant.vars.map(_.id.name)
119128

120-
tQuant.transform({ case v: Var =>
129+
val res = tQuant.transform({ case v: Var =>
121130
v.id match {
122131
case sid: SuffixedIdentifier if names.contains(sid.prefix.name) =>
123132
Var(SimpleIdentifier(sid.prefix.name), v.sort, false)
124133
case _ => v
125134
}
126135
})()
136+
context = context.init
137+
res
127138

128-
case loc: ast.LocationAccess => getOrFail(data.locToSnap, loc, toSort(loc.typ), Option.when(Verifier.config.enableDebugging())(extractPTypeFromExp(loc)))
139+
case loc: ast.LocationAccess => getOrFail(data.locToSnap, loc, context, toSort(loc.typ), Option.when(Verifier.config.enableDebugging())(extractPTypeFromExp(loc)))
129140
case ast.Unfolding(_, eIn) => translate(toSort)(eIn)
130141
case ast.Applying(_, eIn) => translate(toSort)(eIn)
131142
case ast.Asserting(_, eIn) => translate(toSort)(eIn)
@@ -143,7 +154,7 @@ class HeapAccessReplacingExpressionTranslator(symbolConverter: SymbolConverter,
143154
case _ => symbolConverter.toFunction(silverFunc)
144155
}
145156
val args = eFApp.args map (arg => translate(arg))
146-
val snap = getOrFail(data.fappToSnap, eFApp, sorts.Snap, Option.when(Verifier.config.enableDebugging())(PUnknown()))
157+
val snap = getOrFail(data.fappToSnap, eFApp, context, sorts.Snap, Option.when(Verifier.config.enableDebugging())(PUnknown()))
147158
val fapp = App(fun, snap +: args)
148159

149160
val callerHeight = data.height
@@ -157,8 +168,8 @@ class HeapAccessReplacingExpressionTranslator(symbolConverter: SymbolConverter,
157168
case _ => super.translate(symbolConverter.toSort)(e)
158169
}
159170

160-
def getOrFail[K <: ast.Positioned](map: Map[K, Term], key: K, sort: Sort, pType: Option[PType]): Term =
161-
map.get(key) match {
171+
def getOrFail[K <: ast.Positioned](map: Map[(K, Seq[ExpContext]), Term], key: K, ctx: Seq[ExpContext], sort: Sort, pType: Option[PType]): Term =
172+
map.get((key, ctx)) match {
162173
case Some(s) =>
163174
s.convert(sort)
164175
case None =>

0 commit comments

Comments
 (0)
⚡