diff --git a/silver b/silver index 63c30b18f..505e28157 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 63c30b18fdafd81d90eabbc8bccfd13a31becd61 +Subproject commit 505e2815754275c9755af46d25601777e5bff9db diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala index 102273136..be3f27ab4 100644 --- a/src/main/scala/rules/Evaluator.scala +++ b/src/main/scala/rules/Evaluator.scala @@ -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) { @@ -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) }) }) @@ -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) @@ -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)) { diff --git a/src/main/scala/supporters/functions/FunctionData.scala b/src/main/scala/supporters/functions/FunctionData.scala index 2d7b68138..786156fcf 100644 --- a/src/main/scala/supporters/functions/FunctionData.scala +++ b/src/main/scala/supporters/functions/FunctionData.scala @@ -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 @@ -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) diff --git a/src/main/scala/supporters/functions/FunctionRecorder.scala b/src/main/scala/supporters/functions/FunctionRecorder.scala index 7bf06dd7c..0991dbc4b 100644 --- a/src/main/scala/supporters/functions/FunctionRecorder.scala +++ b/src/main/scala/supporters/functions/FunctionRecorder.scala @@ -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)] @@ -41,11 +41,19 @@ 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(), @@ -53,7 +61,8 @@ case class ActualFunctionRecorder(private val _data: FunctionData, 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 @@ -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) @@ -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 } @@ -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 @@ -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 @@ -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 } diff --git a/src/main/scala/supporters/functions/HeapAccessReplacingExpressionTranslator.scala b/src/main/scala/supporters/functions/HeapAccessReplacingExpressionTranslator.scala index 4b70d2140..bc215fad3 100644 --- a/src/main/scala/supporters/functions/HeapAccessReplacingExpressionTranslator.scala +++ b/src/main/scala/supporters/functions/HeapAccessReplacingExpressionTranslator.scala @@ -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] = _ @@ -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 + Let(bvar.asInstanceOf[Var], tE, tBody) case v: ast.AbstractLocalVar => data.formalArgs.get(v) match { @@ -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) @@ -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 @@ -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 =>