Skip to content

Record snapshots in FunctionRecorder with context information #928

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
marcoeilers merged 3 commits into from
Jun 13, 2025
Merged

Record snapshots in FunctionRecorder with context information #928

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
5098428
WIP
marcoeilers May 30, 2025
9ba09e6
Fixing issues #715 and #926
marcoeilers Jun 3, 2025
a28fe96
Merge branch 'master' into meilers_funcrec_fix
marcoeilers Jun 3, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion silver
Open in desktop
Submodule silver updated 3 files
+27 −0 src/test/resources/all/issues/silicon/0715.vpr
+183 −0 src/test/resources/all/issues/silicon/0715_2.vpr
+28 −0 src/test/resources/all/issues/silicon/0926.vpr
13 changes: 8 additions & 5 deletions src/main/scala/rules/Evaluator.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -373,12 +373,12 @@ object evaluator extends EvaluationRules {
evalInOldState(s, lbl, e0, pve, v)((s1, t0, e0New, v1) =>
Q(s1, t0, e0New.map(ast.LabelledOld(_, lbl)(old.pos, old.info, old.errT)), v1))}

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

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

val tQuant = Quantification(qantOp, tVars, tBody, tTriggers, name, quantWeight)
val eQuantNew = Option.when(withExp)(buildQuantExp(qantOp, eVars.get, bodyNew.get.head, Seq.empty))
Q(s1, tQuant, eQuantNew, v1)
val s2 = s1.copy(functionRecorder = s1.functionRecorder.leaveQuantifiedExp(sourceQuant))
Q(s2, tQuant, eQuantNew, v1)
case (s1, _, _, _, _, None, v1) =>
// This should not happen unless the current path is dead.
if (v1.decider.checkSmoke(true)) {
Expand Down
6 changes: 3 additions & 3 deletions src/main/scala/supporters/functions/FunctionData.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -100,8 +100,8 @@ class FunctionData(val programFunction: ast.Function,
*/

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

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

val fapp = App(triggerFunction, args)
Expand Down
75 changes: 56 additions & 19 deletions src/main/scala/supporters/functions/FunctionRecorder.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,10 +19,10 @@ import viper.silicon.state.terms._
// etc. as well.
trait FunctionRecorder extends Mergeable[FunctionRecorder] {
def data: Option[FunctionData]
private[functions] def locToSnaps: Map[ast.LocationAccess, InsertionOrderedSet[(Stack[Term], Term)]]
def locToSnap: Map[ast.LocationAccess, Term]
private[functions] def fappToSnaps: Map[ast.FuncApp, InsertionOrderedSet[(Stack[Term], Term)]]
def fappToSnap: Map[ast.FuncApp, Term]
private[functions] def locToSnaps: Map[(ast.LocationAccess, Seq[ExpContext]), InsertionOrderedSet[(Stack[Term], Term)]]
def locToSnap: Map[(ast.LocationAccess, Seq[ExpContext]), Term]
private[functions] def fappToSnaps: Map[(ast.FuncApp, Seq[ExpContext]), InsertionOrderedSet[(Stack[Term], Term)]]
def fappToSnap: Map[(ast.FuncApp, Seq[ExpContext]), Term]
def freshFvfsAndDomains: InsertionOrderedSet[SnapshotMapDefinition]
def freshFieldInvs: InsertionOrderedSet[InverseFunctions]
def freshConstrainedVars: InsertionOrderedSet[(Var, Term)]
Expand All @@ -41,19 +41,28 @@ trait FunctionRecorder extends Mergeable[FunctionRecorder] {
def recordFreshMacro(decl: MacroDecl): FunctionRecorder
def depth: Int
def changeDepthBy(delta: Int): FunctionRecorder
def enterLet(l: ast.Let): FunctionRecorder
def leaveLet(l: ast.Let): FunctionRecorder
def enterQuantifiedExp(q: ast.QuantifiedExp): FunctionRecorder
def leaveQuantifiedExp(q: ast.QuantifiedExp): FunctionRecorder
}

trait ExpContext
case class LetContext(l: ast.Let) extends ExpContext
case class QuantifierContext(q: ast.QuantifiedExp) extends ExpContext

case class ActualFunctionRecorder(private val _data: FunctionData,
private[functions] val locToSnaps: Map[ast.LocationAccess, InsertionOrderedSet[(Stack[Term], Term)]] = Map(),
private[functions] val fappToSnaps: Map[ast.FuncApp, InsertionOrderedSet[(Stack[Term], Term)]] = Map(),
private[functions] val locToSnaps: Map[(ast.LocationAccess, Seq[ExpContext]), InsertionOrderedSet[(Stack[Term], Term)]] = Map(),
private[functions] val fappToSnaps: Map[(ast.FuncApp, Seq[ExpContext]), InsertionOrderedSet[(Stack[Term], Term)]] = Map(),
freshFvfsAndDomains: InsertionOrderedSet[SnapshotMapDefinition] = InsertionOrderedSet(),
freshFieldInvs: InsertionOrderedSet[InverseFunctions] = InsertionOrderedSet(),
freshConstrainedVars: InsertionOrderedSet[(Var, Term)] = InsertionOrderedSet(),
freshConstraints: InsertionOrderedSet[Term] = InsertionOrderedSet(),
freshSnapshots: InsertionOrderedSet[Function] = InsertionOrderedSet(),
freshPathSymbols: InsertionOrderedSet[Function] = InsertionOrderedSet(),
freshMacros: InsertionOrderedSet[MacroDecl] = InsertionOrderedSet(),
depth: Int = 0)
depth: Int = 0,
private val _context: Seq[ExpContext] = Seq())
extends FunctionRecorder {

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

private def exprToSnap[E <: ast.Exp]
(recordings: Map[E, InsertionOrderedSet[(Stack[Term], Term)]])
: Map[E, Term] = {
(recordings: Map[(E, Seq[ExpContext]), InsertionOrderedSet[(Stack[Term], Term)]])
: Map[(E, Seq[ExpContext]), Term] = {

recordings.map { case (expr, guardsToSnap) =>
expr -> toTerm(guardsToSnap, None)
Expand Down Expand Up @@ -148,20 +157,20 @@ case class ActualFunctionRecorder(private val _data: FunctionData,
}
}

def locToSnap: Map[ast.LocationAccess, Term] = exprToSnap(locToSnaps)
def fappToSnap: Map[ast.FuncApp, Term] = exprToSnap(fappToSnaps)
def locToSnap: Map[(ast.LocationAccess, Seq[ExpContext]), Term] = exprToSnap(locToSnaps)
def fappToSnap: Map[(ast.FuncApp, Seq[ExpContext]), Term] = exprToSnap(fappToSnaps)

private def recordExpressionSnapshot[E <: ast.Exp]
(loc: E,
guards: Stack[Term],
snap: Term,
recordings: Map[E, InsertionOrderedSet[(Stack[Term], Term)]])
: Option[Map[E, InsertionOrderedSet[(Stack[Term], Term)]]] = {
recordings: Map[(E, Seq[ExpContext]), InsertionOrderedSet[(Stack[Term], Term)]])
: Option[Map[(E, Seq[ExpContext]), InsertionOrderedSet[(Stack[Term], Term)]]] = {

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

Some(recordings + (loc -> guardsToSnaps))
Some(recordings + ((loc, _context) -> guardsToSnaps))
} else {
None
}
Expand Down Expand Up @@ -212,6 +221,30 @@ case class ActualFunctionRecorder(private val _data: FunctionData,
def changeDepthBy(delta: Int): ActualFunctionRecorder =
copy(depth = depth + delta)

def enterLet(l: ast.Let): FunctionRecorder = {
copy(_context = _context :+ LetContext(l))
}

def leaveLet(l: ast.Let): FunctionRecorder = {
assert(_context.nonEmpty && (_context.last match {
case LetContext(`l`) => true
case _ => false
}))
copy(_context = _context.init)
}

def enterQuantifiedExp(q: ast.QuantifiedExp): FunctionRecorder = {
copy(_context = _context :+ QuantifierContext(q))
}

def leaveQuantifiedExp(q: ast.QuantifiedExp): FunctionRecorder = {
assert(_context.nonEmpty && (_context.last match {
case QuantifierContext(`q`) => true
case _ => false
}))
copy(_context = _context.init)
}

def merge(other: FunctionRecorder): ActualFunctionRecorder = {
if (depth > 1) return this

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

case object NoopFunctionRecorder extends FunctionRecorder {
val data: Option[FunctionData] = None
private[functions] val fappToSnaps: Map[ast.FuncApp, InsertionOrderedSet[(Stack[Term], Term)]] = Map.empty
val fappToSnap: Map[ast.FuncApp, Term] = Map.empty
private[functions] val locToSnaps: Map[ast.LocationAccess, InsertionOrderedSet[(Stack[Term], Term)]] = Map.empty
val locToSnap: Map[ast.LocationAccess, Term] = Map.empty
private[functions] val fappToSnaps: Map[(ast.FuncApp, Seq[ExpContext]), InsertionOrderedSet[(Stack[Term], Term)]] = Map.empty
val fappToSnap: Map[(ast.FuncApp, Seq[ExpContext]), Term] = Map.empty
private[functions] val locToSnaps: Map[(ast.LocationAccess, Seq[ExpContext]), InsertionOrderedSet[(Stack[Term], Term)]] = Map.empty
val locToSnap: Map[(ast.LocationAccess, Seq[ExpContext]), Term] = Map.empty
val freshFvfsAndDomains: InsertionOrderedSet[SnapshotMapDefinition] = InsertionOrderedSet.empty
val freshFieldInvs: InsertionOrderedSet[InverseFunctions] = InsertionOrderedSet.empty
val freshConstrainedVars: InsertionOrderedSet[(Var, Term)] = InsertionOrderedSet.empty
Expand All @@ -300,4 +333,8 @@ case object NoopFunctionRecorder extends FunctionRecorder {
def recordPathSymbol(symbol: Function): NoopFunctionRecorder.type = this
def recordFreshMacro(decl: MacroDecl): NoopFunctionRecorder.type = this
def changeDepthBy(delta: Int): NoopFunctionRecorder.type = this
def enterLet(l: ast.Let): FunctionRecorder = this
def leaveLet(l: ast.Let): FunctionRecorder = this
def enterQuantifiedExp(q: ast.QuantifiedExp): FunctionRecorder = this
def leaveQuantifiedExp(q: ast.QuantifiedExp): FunctionRecorder = this
}
21 changes: 16 additions & 5 deletions src/main/scala/supporters/functions/HeapAccessReplacingExpressionTranslator.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,6 +34,7 @@ class HeapAccessReplacingExpressionTranslator(symbolConverter: SymbolConverter,
private var data: FunctionData = _
private var ignoreAccessPredicates = false
private var failed = false
private var context: Seq[ExpContext] = Seq.empty

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

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

case _: ast.Result => data.formalResult
case l@ast.Let(lvd, e, body) =>
val bvar = translate(toSort)(lvd.localVar)
val tE = translate(toSort)(e)
context = context :+ LetContext(l)
val tBody = translate(toSort)(body)
context = context.init
Comment thread
marcoeilers marked this conversation as resolved.
Let(bvar.asInstanceOf[Var], tE, tBody)

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

tQuant.transform({ case v: Var =>
val res = tQuant.transform({ case v: Var =>
v.id match {
case sid: SuffixedIdentifier if names.contains(sid.prefix.name) =>
Var(SimpleIdentifier(sid.prefix.name), v.sort, false)
case _ => v
}
})()
context = context.init
res

case loc: ast.LocationAccess => getOrFail(data.locToSnap, loc, toSort(loc.typ), Option.when(Verifier.config.enableDebugging())(extractPTypeFromExp(loc)))
case loc: ast.LocationAccess => getOrFail(data.locToSnap, loc, context, toSort(loc.typ), Option.when(Verifier.config.enableDebugging())(extractPTypeFromExp(loc)))
case ast.Unfolding(_, eIn) => translate(toSort)(eIn)
case ast.Applying(_, eIn) => translate(toSort)(eIn)
case ast.Asserting(_, eIn) => translate(toSort)(eIn)
Expand All @@ -143,7 +154,7 @@ class HeapAccessReplacingExpressionTranslator(symbolConverter: SymbolConverter,
case _ => symbolConverter.toFunction(silverFunc)
}
val args = eFApp.args map (arg => translate(arg))
val snap = getOrFail(data.fappToSnap, eFApp, sorts.Snap, Option.when(Verifier.config.enableDebugging())(PUnknown()))
val snap = getOrFail(data.fappToSnap, eFApp, context, sorts.Snap, Option.when(Verifier.config.enableDebugging())(PUnknown()))
val fapp = App(fun, snap +: args)

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

def getOrFail[K <: ast.Positioned](map: Map[K, Term], key: K, sort: Sort, pType: Option[PType]): Term =
map.get(key) match {
def getOrFail[K <: ast.Positioned](map: Map[(K, Seq[ExpContext]), Term], key: K, ctx: Seq[ExpContext], sort: Sort, pType: Option[PType]): Term =
map.get((key, ctx)) match {
case Some(s) =>
s.convert(sort)
case None =>
Expand Down
⚡