From 84dc2e6d04429b2339ffec2a76b89e2900fdd309 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Thu, 18 Aug 2022 13:57:15 +0200 Subject: [PATCH 1/7] WIP --- src/main/scala/Silicon.scala | 12 +++-- .../extensions/TryBlockParserPlugin.scala | 8 +-- src/main/scala/interfaces/Preamble.scala | 4 -- src/main/scala/interfaces/Verification.scala | 13 ++--- src/main/scala/reporting/Converter.scala | 8 +-- .../scala/reporting/MultiRunRecorder.scala | 2 +- src/main/scala/rules/ChunkSupporter.scala | 4 +- src/main/scala/rules/Consumer.scala | 20 ++++---- src/main/scala/rules/Evaluator.scala | 34 ++++++------- src/main/scala/rules/Executor.scala | 16 +++--- src/main/scala/rules/MagicWandSupporter.scala | 10 ++-- .../rules/MoreCompleteExhaleSupporter.scala | 6 +-- src/main/scala/rules/PredicateSupporter.scala | 8 +-- src/main/scala/rules/Producer.scala | 18 +++---- .../scala/rules/QuantifiedChunkSupport.scala | 49 +++++++++++-------- src/main/scala/rules/StateConsolidator.scala | 2 +- .../scala/rules/SymbolicExecutionRules.scala | 2 +- src/main/scala/state/State.scala | 16 ++++-- src/main/scala/state/SymbolConverter.scala | 12 ++--- src/main/scala/state/Terms.scala | 12 ++--- .../BuiltinDomainsContributor.scala | 14 ++++-- src/main/scala/supporters/Domains.scala | 8 +-- .../supporters/ExpressionTranslator.scala | 3 +- .../PredicateVerificationUnit.scala | 10 +--- .../functions/FunctionVerificationUnit.scala | 15 ++---- ...pAccessReplacingExpressionTranslator.scala | 2 +- .../verifier/DefaultMasterVerifier.scala | 38 ++++++++------ src/main/scala/verifier/Verifier.scala | 7 ++- src/test/scala/CounterexampleTests.scala | 36 +++++++------- 29 files changed, 208 insertions(+), 181 deletions(-) diff --git a/src/main/scala/Silicon.scala b/src/main/scala/Silicon.scala index cb655972b..bbf4785f7 100644 --- a/src/main/scala/Silicon.scala +++ b/src/main/scala/Silicon.scala @@ -178,7 +178,7 @@ class Silicon(val reporter: Reporter, private var debugInfo: Seq[(String, Any)] * TODO: Figure out what happens when ViperServer is used. */ config.file.foreach(filename => { if (filename != Silicon.dummyInputFilename && !config.ignoreFile.getOrElse(false)) { - viper.silicon.verifier.Verifier.inputFile = Some(Paths.get(filename)) + //viper.silicon.verifier.Verifier.inputFile = Some(Paths.get(filename)) } }) @@ -373,8 +373,14 @@ class SiliconFrontend(override val reporter: Reporter, } } -object SiliconRunner extends SiliconFrontend(StdIOReporter()) { +object SiliconRunner extends SiliconRunnerInstance { def main(args: Array[String]): Unit = { + runMain(args) + } +} + +class SiliconRunnerInstance extends SiliconFrontend(StdIOReporter()) { + def runMain(args: Array[String]): Unit = { var exitCode = 1 /* Only 0 indicates no error - we're pessimistic here */ try { @@ -427,6 +433,6 @@ object SiliconRunner extends SiliconFrontend(StdIOReporter()) { */ } - sys.exit(exitCode) + //sys.exit(exitCode) } } diff --git a/src/main/scala/extensions/TryBlockParserPlugin.scala b/src/main/scala/extensions/TryBlockParserPlugin.scala index bb4eac4a3..4bf37db8c 100644 --- a/src/main/scala/extensions/TryBlockParserPlugin.scala +++ b/src/main/scala/extensions/TryBlockParserPlugin.scala @@ -6,13 +6,13 @@ package viper.silicon.extensions -import viper.silver.parser.FastParser._ -import viper.silver.parser.ParserExtension +import viper.silver.parser.{FastParser, ParserExtension} import viper.silver.plugin.{ParserPluginTemplate, SilverPlugin} -class TryBlockParserPlugin extends SilverPlugin with ParserPluginTemplate { +class TryBlockParserPlugin(fp: FastParser) extends SilverPlugin with ParserPluginTemplate { import fastparse._ - import viper.silver.parser.FastParser.whitespace + import viper.silver.parser.FastParserCompanion.whitespace + import fp.{FP, block} private val tryKeyword = "try" diff --git a/src/main/scala/interfaces/Preamble.scala b/src/main/scala/interfaces/Preamble.scala index e32603bc0..6f9b895bb 100644 --- a/src/main/scala/interfaces/Preamble.scala +++ b/src/main/scala/interfaces/Preamble.scala @@ -34,8 +34,6 @@ trait PreambleContributor[+SO, +SY, +AX] extends StatefulComponent { def axiomsAfterAnalysis: Iterable[AX] def emitAxiomsAfterAnalysis(sink: ProverLike): Unit - - def updateGlobalStateAfterAnalysis(): Unit } trait VerifyingPreambleContributor[+SO, +SY, +AX, U <: ast.Node] @@ -50,6 +48,4 @@ trait VerifyingPreambleContributor[+SO, +SY, +AX, U <: ast.Node] def axiomsAfterVerification: Iterable[AX] def emitAxiomsAfterVerification(sink: ProverLike): Unit - - def contributeToGlobalStateAfterVerification(): Unit } diff --git a/src/main/scala/interfaces/Verification.scala b/src/main/scala/interfaces/Verification.scala index ac85e3f62..d06afa388 100644 --- a/src/main/scala/interfaces/Verification.scala +++ b/src/main/scala/interfaces/Verification.scala @@ -7,13 +7,13 @@ package viper.silicon.interfaces import viper.silicon.interfaces.state.Chunk -import viper.silicon.reporting.{Converter, ExtractedModel, ExtractedModelEntry, GenericDomainInterpreter, - ModelInterpreter, ExtractedFunction, DomainEntry, VarEntry, RefEntry, NullRefEntry, UnprocessedModelEntry} +import viper.silicon.reporting.{Converter, DomainEntry, ExtractedFunction, ExtractedModel, ExtractedModelEntry, GenericDomainInterpreter, ModelInterpreter, NullRefEntry, RefEntry, UnprocessedModelEntry, VarEntry} import viper.silicon.state.{State, Store} -import viper.silver.verifier.{Counterexample, FailureContext, Model, VerificationError, ValueEntry, ApplicationEntry, ConstantEntry} +import viper.silver.verifier.{ApplicationEntry, ConstantEntry, Counterexample, FailureContext, Model, ValueEntry, VerificationError} import viper.silicon.state.terms.Term import viper.silicon.verifier.Verifier import viper.silver.ast +import viper.silver.ast.Program /* * Results @@ -144,11 +144,12 @@ case class SiliconVariableCounterexample(internalStore: Store, nativeModel: Mode case class SiliconMappedCounterexample(internalStore: Store, heap: Iterable[Chunk], oldHeaps: State.OldHeaps, - nativeModel: Model) + nativeModel: Model, + program: Program) extends SiliconCounterexample { val converter: Converter = - Converter(nativeModel, internalStore, heap, oldHeaps, Verifier.program) + Converter(nativeModel, internalStore, heap, oldHeaps, program) val model: Model = nativeModel val interpreter: ModelInterpreter[ExtractedModelEntry, Seq[ExtractedModelEntry]] = GenericDomainInterpreter(converter) @@ -226,6 +227,6 @@ case class SiliconMappedCounterexample(internalStore: Store, } override def withStore(s: Store): SiliconCounterexample = { - SiliconMappedCounterexample(s, heap, oldHeaps, nativeModel) + SiliconMappedCounterexample(s, heap, oldHeaps, nativeModel, program) } } \ No newline at end of file diff --git a/src/main/scala/reporting/Converter.scala b/src/main/scala/reporting/Converter.scala index 286271e74..f1eda91e9 100644 --- a/src/main/scala/reporting/Converter.scala +++ b/src/main/scala/reporting/Converter.scala @@ -622,7 +622,7 @@ object Converter { } catch { case _: Throwable => Seq() } - val translatedFunctions = x._1.functions.map(y => translateFunction(model, heap, y, x._2)) + val translatedFunctions = x._1.functions.map(y => translateFunction(model, heap, y, x._2, program)) DomainEntry(x._1.name, types, translatedFunctions) }).toSeq } @@ -634,7 +634,7 @@ object Converter { val funcs = program.collect { case f: ast.Function => f } - funcs.map(x => translateFunction(model, heap, x, silicon.toMap(Nil))).toSeq + funcs.map(x => translateFunction(model, heap, x, silicon.toMap(Nil), program)).toSeq } def errorfunc(problem: String): ExtractedFunction = @@ -648,7 +648,7 @@ object Converter { * @param genmap map of generic types to concrete types * @return */ - def translateFunction(model: Model, heap: ExtractedHeap, func: ast.FuncLike, genmap: Map[ast.TypeVar, ast.Type]): ExtractedFunction = { + def translateFunction(model: Model, heap: ExtractedHeap, func: ast.FuncLike, genmap: Map[ast.TypeVar, ast.Type], program: ast.Program): ExtractedFunction = { def toSort(typ: ast.Type): Either[Throwable, Sort] = Try(symbolConverter.toSort(typ)).toEither def toSortWithSubstitutions(typ: ast.Type, typeErrorMsg: String): Either[String, Sort] = { toSort(typ) @@ -675,7 +675,7 @@ object Converter { val smtfunc = func match { case t: ast.Function => symbolConverter.toFunction(t).id - case t: ast.DomainFunc => symbolConverter.toFunction(t, argSort :+ resSort).id + case t: ast.DomainFunc => symbolConverter.toFunction(t, argSort :+ resSort, program).id case t: ast.BackendFunc => symbolConverter.toFunction(t).id } val kek = smtfunc.toString diff --git a/src/main/scala/reporting/MultiRunRecorder.scala b/src/main/scala/reporting/MultiRunRecorder.scala index dd3916de0..229db0eef 100644 --- a/src/main/scala/reporting/MultiRunRecorder.scala +++ b/src/main/scala/reporting/MultiRunRecorder.scala @@ -96,7 +96,7 @@ object MultiRunRecorders extends StatefulComponent { private val sinks = mutable.ArrayBuffer.empty[PrintWriter] protected def config: Config = Verifier.config - protected def source: Option[String] = Verifier.inputFile.map(_.toString) + protected def source: Option[String] = ??? // Verifier.inputFile.map(_.toString) protected def sink(name: String): PrintWriter = { val writer = diff --git a/src/main/scala/rules/ChunkSupporter.scala b/src/main/scala/rules/ChunkSupporter.scala index 68d17bd01..55d45649c 100644 --- a/src/main/scala/rules/ChunkSupporter.scala +++ b/src/main/scala/rules/ChunkSupporter.scala @@ -101,7 +101,7 @@ object chunkSupporter extends ChunkSupportRules { (Q: (State, Heap, Option[Term], Verifier) => VerificationResult) : VerificationResult = { - val id = ChunkIdentifier(resource, Verifier.program) + val id = ChunkIdentifier(resource, s.program) if (s.exhaleExt) { val failure = createFailure(ve, v, s) magicWandSupporter.transfer(s, perms, failure, v)(consumeGreedy(_, _, id, args, _, _))((s1, optCh, v1) => @@ -213,7 +213,7 @@ object chunkSupporter extends ChunkSupportRules { (Q: (State, Term, Verifier) => VerificationResult) : VerificationResult = { - val id = ChunkIdentifier(resource, Verifier.program) + val id = ChunkIdentifier(resource, s.program) findChunk[NonQuantifiedChunk](h.values, id, args, v) match { case Some(ch) if v.decider.check(IsPositive(ch.perm), Verifier.config.checkTimeout()) => diff --git a/src/main/scala/rules/Consumer.scala b/src/main/scala/rules/Consumer.scala index 15c9b9242..f95607fc6 100644 --- a/src/main/scala/rules/Consumer.scala +++ b/src/main/scala/rules/Consumer.scala @@ -247,7 +247,7 @@ object consumer extends ConsumptionRules { } case QuantifiedPermissionAssertion(forall, cond, acc: ast.PredicateAccessPredicate) => - val predicate = Verifier.program.findPredicate(acc.loc.predicateName) + val predicate = s.program.findPredicate(acc.loc.predicateName) /* TODO: Quantified codomain variables are used in axioms and chunks (analogous to `?r`) * and need to be instantiated in several places. Hence, they need to be known, * which is more complicated if fresh identifiers are used. @@ -284,9 +284,9 @@ object consumer extends ConsumptionRules { } case QuantifiedPermissionAssertion(forall, cond, wand: ast.MagicWand) => - val bodyVars = wand.subexpressionsToEvaluate(Verifier.program) + val bodyVars = wand.subexpressionsToEvaluate(s.program) val formalVars = bodyVars.indices.toList.map(i => Var(Identifier(s"x$i"), v.symbolConverter.toSort(bodyVars(i).typ))) - val qid = MagicWandIdentifier(wand, Verifier.program).toString + val qid = MagicWandIdentifier(wand, s.program).toString val optTrigger = if (forall.triggers.isEmpty) None else Some(forall.triggers) @@ -344,9 +344,9 @@ object consumer extends ConsumptionRules { Q(s4, h3, snap, v3)})})) case ast.AccessPredicate(loc @ ast.PredicateAccess(eArgs, predname), ePerm) - if s.qpPredicates.contains(Verifier.program.findPredicate(predname)) => + if s.qpPredicates.contains(s.program.findPredicate(predname)) => - val predicate = Verifier.program.findPredicate(predname) + val predicate = s.program.findPredicate(predname) val formalVars = s.predicateFormalVarMap(predicate) evals(s, eArgs, _ => pve, v)((s1, tArgs, v1) => @@ -383,7 +383,7 @@ object consumer extends ConsumptionRules { eval(s, perm, pve, v)((s1, tPerm, v1) => evalLocationAccess(s1, locacc, pve, v1)((s2, _, tArgs, v2) => permissionSupporter.assertNotNegative(s2, tPerm, perm, pve, v2)((s3, v3) => { - val resource = locacc.res(Verifier.program) + val resource = locacc.res(s.program) val loss = PermTimes(tPerm, s3.permissionScalingFactor) val ve = pve dueTo InsufficientPermission(locacc) val description = s"consume ${a.pos}: $a" @@ -396,17 +396,17 @@ object consumer extends ConsumptionRules { createFailure(viper.silicon.utils.consistency.createUnexpectedInhaleExhaleExpressionError(a), v, s) /* Handle wands */ - case wand: ast.MagicWand if s.qpMagicWands.contains(MagicWandIdentifier(wand, Verifier.program)) => - val bodyVars = wand.subexpressionsToEvaluate(Verifier.program) + case wand: ast.MagicWand if s.qpMagicWands.contains(MagicWandIdentifier(wand, s.program)) => + val bodyVars = wand.subexpressionsToEvaluate(s.program) val formalVars = bodyVars.indices.toList.map(i => Var(Identifier(s"x$i"), v.symbolConverter.toSort(bodyVars(i).typ))) evals(s, bodyVars, _ => pve, v)((s1, tArgs, v1) => { val (relevantChunks, _) = - quantifiedChunkSupporter.splitHeap[QuantifiedMagicWandChunk](s1.h, MagicWandIdentifier(wand, Verifier.program)) + quantifiedChunkSupporter.splitHeap[QuantifiedMagicWandChunk](s1.h, MagicWandIdentifier(wand, s.program)) val (smDef1, smCache1) = quantifiedChunkSupporter.summarisingSnapshotMap( s1, wand, formalVars, relevantChunks, v1) - v1.decider.assume(PredicateTrigger(MagicWandIdentifier(wand, Verifier.program).toString, smDef1.sm, tArgs)) + v1.decider.assume(PredicateTrigger(MagicWandIdentifier(wand, s.program).toString, smDef1.sm, tArgs)) val loss = PermTimes(FullPerm(), s1.permissionScalingFactor) quantifiedChunkSupporter.consumeSingleLocation( diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala index 6ea9fd16f..8692b0f1e 100644 --- a/src/main/scala/rules/Evaluator.scala +++ b/src/main/scala/rules/Evaluator.scala @@ -254,7 +254,7 @@ object evaluator extends EvaluationRules { case fa: ast.FieldAccess => evalLocationAccess(s, fa, pve, v)((s1, _, tArgs, v1) => { val ve = pve dueTo InsufficientPermission(fa) - val resource = fa.res(Verifier.program) + val resource = fa.res(s.program) chunkSupporter.lookup(s1, s1.h, resource, tArgs, ve, v1)((s2, h2, tSnap, v2) => { val fr = s2.functionRecorder.recordSnapshot(fa, v2.decider.pcs.branchConditions, tSnap) val s3 = s2.copy(h = h2, functionRecorder = fr) @@ -416,7 +416,7 @@ object evaluator extends EvaluationRules { evals(s, eArgs, _ => pve, v)((s1, tArgs, v1) => { val inSorts = tArgs map (_.sort) val outSort = v1.symbolConverter.toSort(dfa.typ) - val fi = v1.symbolConverter.toFunction(Verifier.program.findDomainFunction(funcName), inSorts :+ outSort) + val fi = v1.symbolConverter.toFunction(s.program.findDomainFunction(funcName), inSorts :+ outSort, s.program) Q(s1, App(fi, tArgs), v1)}) case ast.BackendFuncApp(func, eArgs) => @@ -427,7 +427,7 @@ object evaluator extends EvaluationRules { case ast.CurrentPerm(resacc) => val h = s.partiallyConsumedHeap.getOrElse(s.h) evalResourceAccess(s, resacc, pve, v)((s1, identifier, args, v1) => { - val res = resacc.res(Verifier.program) + val res = resacc.res(s.program) /* It is assumed that, for a given field/predicate/wand identifier (res) * either only quantified or only non-quantified chunks are used. */ @@ -441,7 +441,7 @@ object evaluator extends EvaluationRules { case wand: ast.MagicWand => val (relevantChunks, _) = quantifiedChunkSupporter.splitHeap[QuantifiedMagicWandChunk](h, identifier) - val bodyVars = wand.subexpressionsToEvaluate(Verifier.program) + val bodyVars = wand.subexpressionsToEvaluate(s.program) val formalVars = bodyVars.indices.toList.map(i => Var(Identifier(s"x$i"), v1.symbolConverter.toSort(bodyVars(i).typ))) val (s2, smDef, pmDef) = quantifiedChunkSupporter.heapSummarisingMaps(s1, wand, formalVars, relevantChunks, v1) @@ -577,13 +577,13 @@ object evaluator extends EvaluationRules { val s1 = s.copy(h = s.partiallyConsumedHeap.getOrElse(s.h)) - val resIdent = ChunkIdentifier(resourceAccess.res(Verifier.program), Verifier.program) + val resIdent = ChunkIdentifier(resourceAccess.res(s.program), s.program) val args = resourceAccess match { case fa: ast.FieldAccess => Seq(fa.rcv) case pa: ast.PredicateAccess => pa.args - case w: ast.MagicWand => w.subexpressionsToEvaluate(Verifier.program) + case w: ast.MagicWand => w.subexpressionsToEvaluate(s.program) } - val usesQPChunks = resourceAccess.res(Verifier.program) match { + val usesQPChunks = resourceAccess.res(s.program) match { case _: ast.MagicWand => s1.qpMagicWands.contains(resIdent.asInstanceOf[MagicWandIdentifier]) case field: ast.Field => s1.qpFields.contains(field) case pred: ast.Predicate => s1.qpPredicates.contains(pred) @@ -647,7 +647,7 @@ object evaluator extends EvaluationRules { } case fapp @ ast.FuncApp(funcName, eArgs) => - val func = Verifier.program.findFunction(funcName) + val func = s.program.findFunction(funcName) val s0 = s.copy(hackIssue387DisablePermissionConsumption = Verifier.config.enableMoreCompleteExhale()) evals2(s0, eArgs, Nil, _ => pve, v)((s1, tArgs, v1) => { // bookkeeper.functionApplications += 1 @@ -738,7 +738,7 @@ object evaluator extends EvaluationRules { acc @ ast.PredicateAccessPredicate(pa @ ast.PredicateAccess(eArgs, predicateName), ePerm), eIn) => - val predicate = Verifier.program.findPredicate(predicateName) + val predicate = s.program.findPredicate(predicateName) if (s.cycles(predicate) < Verifier.config.recursivePredicateUnfoldings()) { evals(s, eArgs, _ => pve, v)((s1, tArgs, v1) => eval(s1, ePerm, pve, v1)((s2, tPerm, v2) => @@ -767,7 +767,7 @@ object evaluator extends EvaluationRules { * to the function arguments and the predicate snapshot * (see 'predicateTriggers' in FunctionData.scala). */ - v4.decider.assume(App(Verifier.predicateData(predicate).triggerFunction, snap.convert(terms.sorts.Snap) +: tArgs)) + v4.decider.assume(App(s.predicateData(predicate).triggerFunction, snap.convert(terms.sorts.Snap) +: tArgs)) val body = predicate.body.get /* Only non-abstract predicates can be unfolded */ val s7 = s6.scalePermissionFactor(tPerm) val insg = s7.g + Store(predicate.formalArgs map (_.localVar) zip tArgs) @@ -1094,7 +1094,7 @@ object evaluator extends EvaluationRules { resacc match { case wand : ast.MagicWand => magicWandSupporter.evaluateWandArguments(s, wand, pve, v)((s1, tArgs, v1) => - Q(s1, MagicWandIdentifier(wand, Verifier.program), tArgs, v1)) + Q(s1, MagicWandIdentifier(wand, s.program), tArgs, v1)) case ast.FieldAccess(eRcvr, field) => eval(s, eRcvr, pve, v)((s1, tRcvr, v1) => Q(s1, BasicChunkIdentifier(field.name), tRcvr :: Nil, v1)) @@ -1414,7 +1414,7 @@ object evaluator extends EvaluationRules { var axioms = Seq.empty[Term] var triggers = Seq.empty[Term] var mostRecentTrig: PredicateTrigger = null - val codomainQVars = s.predicateFormalVarMap(pa.loc(Verifier.program)) + val codomainQVars = s.predicateFormalVarMap(pa.loc(s.program)) val (relevantChunks, _) = quantifiedChunkSupporter.splitHeap[QuantifiedPredicateChunk](s.h, BasicChunkIdentifier(pa.predicateName)) val optSmDomainDefinitionCondition = @@ -1422,7 +1422,7 @@ object evaluator extends EvaluationRules { else None val (smDef1, smCache1) = quantifiedChunkSupporter.summarisingSnapshotMap( - s, pa.loc(Verifier.program), codomainQVars, relevantChunks, v, optSmDomainDefinitionCondition) + s, pa.loc(s.program), codomainQVars, relevantChunks, v, optSmDomainDefinitionCondition) val s1 = s.copy(smCache = smCache1) evals(s1, pa.args, _ => pve, v)((_, tArgs, _) => { @@ -1440,11 +1440,11 @@ object evaluator extends EvaluationRules { var axioms = Seq.empty[Term] var triggers = Seq.empty[Term] var mostRecentTrig: PredicateTrigger = null - val wandHoles = wand.subexpressionsToEvaluate(Verifier.program) + val wandHoles = wand.subexpressionsToEvaluate(s.program) val codomainQVars = wandHoles.indices.toList.map(i => Var(Identifier(s"x$i"), v.symbolConverter.toSort(wandHoles(i).typ))) val (relevantChunks, _) = - quantifiedChunkSupporter.splitHeap[QuantifiedMagicWandChunk](s.h, MagicWandIdentifier(wand, Verifier.program)) + quantifiedChunkSupporter.splitHeap[QuantifiedMagicWandChunk](s.h, MagicWandIdentifier(wand, s.program)) val optSmDomainDefinitionCondition = if (s.smDomainNeeded) { v.logger.debug("Axiomatisation of an SM domain missing!"); None } else None @@ -1453,9 +1453,9 @@ object evaluator extends EvaluationRules { s, wand, codomainQVars, relevantChunks, v, optSmDomainDefinitionCondition) val s1 = s.copy(smCache = smCache1) - evals(s1, wand.subexpressionsToEvaluate(Verifier.program), _ => pve, v)((_, tArgs, _) => { + evals(s1, wand.subexpressionsToEvaluate(s.program), _ => pve, v)((_, tArgs, _) => { axioms = axioms ++ smDef1.valueDefinitions - mostRecentTrig = PredicateTrigger(MagicWandIdentifier(wand, Verifier.program).toString, smDef1.sm, tArgs) + mostRecentTrig = PredicateTrigger(MagicWandIdentifier(wand, s.program).toString, smDef1.sm, tArgs) triggers = triggers :+ mostRecentTrig Success() }) diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala index 7c4da2e65..08e30aa66 100644 --- a/src/main/scala/rules/Executor.scala +++ b/src/main/scala/rules/Executor.scala @@ -311,7 +311,7 @@ object executor extends ExecutionRules { val (sm, smValueDef) = quantifiedChunkSupporter.singletonSnapshotMap(s3, field, Seq(tRcvr), tRhs, v2) v1.decider.prover.comment("Definitional axioms for singleton-FVF's value") v1.decider.assume(smValueDef) - val ch = quantifiedChunkSupporter.createSingletonQuantifiedChunk(Seq(`?r`), field, Seq(tRcvr), FullPerm(), sm) + val ch = quantifiedChunkSupporter.createSingletonQuantifiedChunk(Seq(`?r`), field, Seq(tRcvr), FullPerm(), sm, s.program) v1.decider.assume(FieldTrigger(field.name, sm, tRcvr)) Q(s3.copy(h = h3 + ch), v2) case (Incomplete(_), s3, _) => @@ -322,7 +322,7 @@ object executor extends ExecutionRules { val pve = AssignmentFailed(ass) eval(s, eRcvr, pve, v)((s1, tRcvr, v1) => eval(s1, rhs, pve, v1)((s2, tRhs, v2) => { - val resource = fa.res(Verifier.program) + val resource = fa.res(s.program) val ve = pve dueTo InsufficientPermission(fa) val description = s"consume ${ass.pos}: $ass" chunkSupporter.consume(s2, s2.h, resource, Seq(tRcvr), FullPerm(), ve, v2, description)((s3, h3, _, v3) => { @@ -345,7 +345,7 @@ object executor extends ExecutionRules { val (sm, smValueDef) = quantifiedChunkSupporter.singletonSnapshotMap(s, field, Seq(tRcvr), snap, v) v.decider.prover.comment("Definitional axioms for singleton-FVF's value") v.decider.assume(smValueDef) - quantifiedChunkSupporter.createSingletonQuantifiedChunk(Seq(`?r`), field, Seq(tRcvr), p, sm) + quantifiedChunkSupporter.createSingletonQuantifiedChunk(Seq(`?r`), field, Seq(tRcvr), p, sm, s.program) } else { BasicChunk(FieldID, BasicChunkIdentifier(field.name), Seq(tRcvr), snap, p) } @@ -411,7 +411,7 @@ object executor extends ExecutionRules { if !Verifier.config.disableHavocHack407() && methodName.startsWith(hack407_method_name_prefix) => val resourceName = methodName.stripPrefix(hack407_method_name_prefix) - val member = Verifier.program.collectFirst { + val member = s.program.collectFirst { case m: ast.Field if m.name == resourceName => m case m: ast.Predicate if m.name == resourceName => m }.getOrElse(sys.error(s"Found $methodName, but no matching field or predicate $resourceName")) @@ -433,7 +433,7 @@ object executor extends ExecutionRules { Q(s1, v) case call @ ast.MethodCall(methodName, eArgs, lhs) => - val meth = Verifier.program.findMethod(methodName) + val meth = s.program.findMethod(methodName) val fargs = meth.formalArgs.map(_.localVar) val formalsToActuals: Map[ast.LocalVar, ast.Exp] = fargs.zip(eArgs).to(Map) val reasonTransformer = (n: viper.silver.verifier.errors.ErrorNode) => n.replace(formalsToActuals) @@ -474,7 +474,7 @@ object executor extends ExecutionRules { Q(s6, v3)})})}) case fold @ ast.Fold(ast.PredicateAccessPredicate(ast.PredicateAccess(eArgs, predicateName), ePerm)) => - val predicate = Verifier.program.findPredicate(predicateName) + val predicate = s.program.findPredicate(predicateName) val pve = FoldFailed(fold) evals(s, eArgs, _ => pve, v)((s1, tArgs, v1) => eval(s1, ePerm, pve, v1)((s2, tPerm, v2) => @@ -483,7 +483,7 @@ object executor extends ExecutionRules { predicateSupporter.fold(s3, predicate, tArgs, tPerm, wildcards, pve, v3)(Q)}))) case unfold @ ast.Unfold(ast.PredicateAccessPredicate(pa @ ast.PredicateAccess(eArgs, predicateName), ePerm)) => - val predicate = Verifier.program.findPredicate(predicateName) + val predicate = s.program.findPredicate(predicateName) val pve = UnfoldFailed(unfold) evals(s, eArgs, _ => pve, v)((s1, tArgs, v1) => eval(s1, ePerm, pve, v1)((s2, tPerm, v2) => { @@ -536,7 +536,7 @@ object executor extends ExecutionRules { case ch: QuantifiedMagicWandChunk => val (relevantChunks, _) = quantifiedChunkSupporter.splitHeap[QuantifiedMagicWandChunk](s2.h, ch.id) - val bodyVars = wand.subexpressionsToEvaluate(Verifier.program) + val bodyVars = wand.subexpressionsToEvaluate(s.program) val formalVars = bodyVars.indices.toList.map(i => Var(Identifier(s"x$i"), v1.symbolConverter.toSort(bodyVars(i).typ))) val (smDef, smCache) = quantifiedChunkSupporter.summarisingSnapshotMap( diff --git a/src/main/scala/rules/MagicWandSupporter.scala b/src/main/scala/rules/MagicWandSupporter.scala index 7fe65c517..5e0bbf3d3 100644 --- a/src/main/scala/rules/MagicWandSupporter.scala +++ b/src/main/scala/rules/MagicWandSupporter.scala @@ -106,7 +106,7 @@ object magicWandSupporter extends SymbolicExecutionRules { (Q: (State, MagicWandChunk, Verifier) => VerificationResult) : VerificationResult = { evaluateWandArguments(s, wand, pve, v)((s1, ts, v1) => - Q(s1, MagicWandChunk(MagicWandIdentifier(wand, Verifier.program), s1.g.values, ts, snap, FullPerm()), v1) + Q(s1, MagicWandChunk(MagicWandIdentifier(wand, s.program), s1.g.values, ts, snap, FullPerm()), v1) ) } @@ -117,7 +117,7 @@ object magicWandSupporter extends SymbolicExecutionRules { (Q: (State, Seq[Term], Verifier) => VerificationResult) : VerificationResult = { val s1 = s.copy(exhaleExt = false) - val es = wand.subexpressionsToEvaluate(Verifier.program) + val es = wand.subexpressionsToEvaluate(s.program) evals(s1, es, _ => pve, v)((s2, ts, v1) => { Q(s2.copy(exhaleExt = s.exhaleExt), ts, v1) @@ -289,15 +289,15 @@ object magicWandSupporter extends SymbolicExecutionRules { } val preMark = v3.decider.setPathConditionMark() - if (s4.qpMagicWands.contains(MagicWandIdentifier(wand, Verifier.program))) { - val bodyVars = wand.subexpressionsToEvaluate(Verifier.program) + if (s4.qpMagicWands.contains(MagicWandIdentifier(wand, s.program))) { + val bodyVars = wand.subexpressionsToEvaluate(s.program) val formalVars = bodyVars.indices.toList.map(i => Var(Identifier(s"x$i"), v.symbolConverter.toSort(bodyVars(i).typ))) evals(s4, bodyVars, _ => pve, v3)((s5, args, v4) => { val (sm, smValueDef) = quantifiedChunkSupporter.singletonSnapshotMap(s5, wand, args, MagicWandSnapshot(freshSnapRoot, snap), v4) v4.decider.prover.comment("Definitional axioms for singleton-SM's value") v4.decider.assume(smValueDef) - val ch = quantifiedChunkSupporter.createSingletonQuantifiedChunk(formalVars, wand, args, FullPerm(), sm) + val ch = quantifiedChunkSupporter.createSingletonQuantifiedChunk(formalVars, wand, args, FullPerm(), sm, s.program) appendToResults(s5, ch, v4.decider.pcs.after(preMark), v4) Success() }) diff --git a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala index 7ff88e5f2..50a1c3f25 100644 --- a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala +++ b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala @@ -141,7 +141,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { (Q: (State, Term, Verifier) => VerificationResult) : VerificationResult = { - val id = ChunkIdentifier(resource, Verifier.program) + val id = ChunkIdentifier(resource, s.program) val relevantChunks = findChunksWithID[NonQuantifiedChunk](h.values, id).toSeq if (relevantChunks.isEmpty) { @@ -186,7 +186,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { (Q: (State, Heap, Option[Term], Verifier) => VerificationResult) : VerificationResult = { - val id = ChunkIdentifier(resource, Verifier.program) + val id = ChunkIdentifier(resource, s.program) val relevantChunks = findChunksWithID[NonQuantifiedChunk](h.values, id).toSeq summarise(s, relevantChunks, resource, args, v)((s1, snap, _, permSum, v1) => @@ -208,7 +208,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { (Q: (State, Heap, Option[Term], Verifier) => VerificationResult) : VerificationResult = { - val id = ChunkIdentifier(resource, Verifier.program) + val id = ChunkIdentifier(resource, s.program) val relevantChunks = ListBuffer[NonQuantifiedChunk]() val otherChunks = ListBuffer[Chunk]() h.values foreach { diff --git a/src/main/scala/rules/PredicateSupporter.scala b/src/main/scala/rules/PredicateSupporter.scala index 8a8f1579e..668503ebd 100644 --- a/src/main/scala/rules/PredicateSupporter.scala +++ b/src/main/scala/rules/PredicateSupporter.scala @@ -60,7 +60,7 @@ object predicateSupporter extends PredicateSupportRules { smDomainNeeded = true) .scalePermissionFactor(tPerm) consume(s1, body, pve, v)((s1a, snap, v1) => { - val predTrigger = App(Verifier.predicateData(predicate).triggerFunction, + val predTrigger = App(s1a.predicateData(predicate).triggerFunction, snap.convert(terms.sorts.Snap) +: tArgs) v1.decider.assume(predTrigger) val s2 = s1a.setConstrainable(constrainableWildcards, false) @@ -73,7 +73,7 @@ object predicateSupporter extends PredicateSupportRules { v1.decider.assume(smValueDef) val ch = quantifiedChunkSupporter.createSingletonQuantifiedChunk( - formalArgs, predicate, tArgs, tPerm, sm) + formalArgs, predicate, tArgs, tPerm, sm, s.program) val h3 = s2.h + ch val smDef = SnapshotMapDefinition(predicate, sm, Seq(smValueDef), Seq()) val smCache = { @@ -135,7 +135,7 @@ object predicateSupporter extends PredicateSupportRules { produce(s3, toSf(snap), body, pve, v1)((s4, v2) => { v2.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.afterUnfold) val predicateTrigger = - App(Verifier.predicateData(predicate).triggerFunction, + App(s4.predicateData(predicate).triggerFunction, snap.convert(terms.sorts.Snap) +: tArgs) v2.decider.assume(predicateTrigger) Q(s4.copy(g = s.g, @@ -151,7 +151,7 @@ object predicateSupporter extends PredicateSupportRules { produce(s3, toSf(snap), body, pve, v1)((s4, v2) => { v2.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.afterUnfold) val predicateTrigger = - App(Verifier.predicateData(predicate).triggerFunction, snap +: tArgs) + App(s4.predicateData(predicate).triggerFunction, snap +: tArgs) v2.decider.assume(predicateTrigger) val s5 = s4.copy(g = s.g, permissionScalingFactor = s.permissionScalingFactor) diff --git a/src/main/scala/rules/Producer.scala b/src/main/scala/rules/Producer.scala index b295abbf9..e320de0b4 100644 --- a/src/main/scala/rules/Producer.scala +++ b/src/main/scala/rules/Producer.scala @@ -261,12 +261,12 @@ object producer extends ProductionRules { }}))) case ast.PredicateAccessPredicate(ast.PredicateAccess(eArgs, predicateName), perm) => - val predicate = Verifier.program.findPredicate(predicateName) + val predicate = s.program.findPredicate(predicateName) evals(s, eArgs, _ => pve, v)((s1, tArgs, v1) => eval(s1, perm, pve, v1)((s1a, tPerm, v1a) => permissionSupporter.assertNotNegative(s1a, tPerm, perm, pve, v1a)((s2, v2) => { val snap = sf( - predicate.body.map(v2.snapshotSupporter.optimalSnapshotSort(_, Verifier.program)._1) + predicate.body.map(v2.snapshotSupporter.optimalSnapshotSort(_, s.program)._1) .getOrElse(sorts.Snap), v2) val gain = PermTimes(tPerm, s2.permissionScalingFactor) if (s2.qpPredicates.contains(predicate)) { @@ -279,13 +279,13 @@ object producer extends ProductionRules { val ch = BasicChunk(PredicateID, BasicChunkIdentifier(predicate.name), tArgs, snap1, gain) chunkSupporter.produce(s2, s2.h, ch, v2)((s3, h3, v3) => { if (Verifier.config.enablePredicateTriggersOnInhale() && s3.functionRecorder == NoopFunctionRecorder) { - v3.decider.assume(App(Verifier.predicateData(predicate).triggerFunction, snap1 +: tArgs)) + v3.decider.assume(App(s3.predicateData(predicate).triggerFunction, snap1 +: tArgs)) } Q(s3.copy(h = h3), v3)}) }}))) - case wand: ast.MagicWand if s.qpMagicWands.contains(MagicWandIdentifier(wand, Verifier.program)) => - val bodyVars = wand.subexpressionsToEvaluate(Verifier.program) + case wand: ast.MagicWand if s.qpMagicWands.contains(MagicWandIdentifier(wand, s.program)) => + val bodyVars = wand.subexpressionsToEvaluate(s.program) val formalVars = bodyVars.indices.toList.map(i => Var(Identifier(s"x$i"), v.symbolConverter.toSort(bodyVars(i).typ))) evals(s, bodyVars, _ => pve, v)((s1, args, v1) => { val (sm, smValueDef) = @@ -297,7 +297,7 @@ object producer extends ProductionRules { if (s1.recordPcs) (s1.conservedPcs.head :+ v1.decider.pcs.after(definitionalAxiomMark)) +: s1.conservedPcs.tail else s1.conservedPcs val ch = - quantifiedChunkSupporter.createSingletonQuantifiedChunk(formalVars, wand, args, FullPerm(), sm) + quantifiedChunkSupporter.createSingletonQuantifiedChunk(formalVars, wand, args, FullPerm(), sm, s.program) val h2 = s1.h + ch val (relevantChunks, _) = quantifiedChunkSupporter.splitHeap[QuantifiedMagicWandChunk](h2, ch.id) @@ -352,7 +352,7 @@ object producer extends ProductionRules { } case QuantifiedPermissionAssertion(forall, cond, acc: ast.PredicateAccessPredicate) => - val predicate = Verifier.program.findPredicate(acc.loc.predicateName) + val predicate = s.program.findPredicate(acc.loc.predicateName) val formalVars = s.predicateFormalVarMap(predicate) val qid = acc.loc.predicateName val optTrigger = @@ -384,12 +384,12 @@ object producer extends ProductionRules { } case QuantifiedPermissionAssertion(forall, cond, wand: ast.MagicWand) => - val bodyVars = wand.subexpressionsToEvaluate(Verifier.program) + val bodyVars = wand.subexpressionsToEvaluate(s.program) val formalVars = bodyVars.indices.toList.map(i => Var(Identifier(s"x$i"), v.symbolConverter.toSort(bodyVars(i).typ))) val optTrigger = if (forall.triggers.isEmpty) None else Some(forall.triggers) - val qid = MagicWandIdentifier(wand, Verifier.program).toString + 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) diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala index 0886cc286..d43466226 100644 --- a/src/main/scala/rules/QuantifiedChunkSupport.scala +++ b/src/main/scala/rules/QuantifiedChunkSupport.scala @@ -150,7 +150,8 @@ trait QuantifiedChunkSupport extends SymbolicExecutionRules { resource: ast.Resource, arguments: Seq[Term], permissions: Term, - sm: Term) + sm: Term, + program: ast.Program) : QuantifiedBasicChunk /** Creates a quantified chunk corresponding to the assertion @@ -181,7 +182,8 @@ trait QuantifiedChunkSupport extends SymbolicExecutionRules { additionalInvArgs: Seq[Var], userProvidedTriggers: Option[Seq[Trigger]], qidPrefix: String, - v: Verifier) + v: Verifier, + program: ast.Program) : (QuantifiedBasicChunk, InverseFunctions) def splitHeap[CH <: QuantifiedBasicChunk : NotNothing : ClassTag] @@ -202,7 +204,8 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { resource: ast.Resource, arguments: Seq[Term], permissions: Term, - sm: Term) + sm: Term, + program: ast.Program) : QuantifiedBasicChunk = { val condition = @@ -225,7 +228,8 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { None, Some(conditionalizedPermissions), Some(arguments), - hints) + hints, + program) } /** @inheritdoc [[QuantifiedChunkSupport.createQuantifiedChunk]] */ @@ -239,7 +243,8 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { additionalInvArgs: Seq[Var], userProvidedTriggers: Option[Seq[Trigger]], qidPrefix: String, - v: Verifier) + v: Verifier, + program: ast.Program) : (QuantifiedBasicChunk, InverseFunctions) = { val inverseFunctions = @@ -273,7 +278,8 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { Some(inverseFunctions), Some(conditionalizedPermissions), None, - hints) + hints, + program) (ch, inverseFunctions) } @@ -310,7 +316,8 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { optInverseFunctions: Option[InverseFunctions], optInitialCond: Option[Term], optSingletonArguments: Option[Seq[Term]], - hints: Seq[Term]) + hints: Seq[Term], + program: ast.Program) : QuantifiedBasicChunk = { resource match { @@ -340,7 +347,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { case wand: ast.MagicWand => QuantifiedMagicWandChunk( - MagicWandIdentifier(wand, Verifier.program), + MagicWandIdentifier(wand, program), codomainQVars, sm, permissions, @@ -481,7 +488,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { case predicate: ast.Predicate => SetIn(qvar, PredicateDomain(predicate.name, sm)) case wand: ast.MagicWand => - SetIn(qvar, PredicateDomain(MagicWandIdentifier(wand, Verifier.program).toString, sm)) + SetIn(qvar, PredicateDomain(MagicWandIdentifier(wand, s.program).toString, sm)) } val valueDefinitions = @@ -742,7 +749,8 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { additionalInvArgs = s.relevantQuantifiedVariables(tArgs), userProvidedTriggers = optTrigger.map(_ => tTriggers), qidPrefix = qid, - v = v) + v = v, + program = s.program) val (effectiveTriggers, effectiveTriggersQVars) = optTrigger match { case Some(_) => @@ -761,7 +769,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { resource match { case p: ast.Predicate if pt.predname == p.name => PredicateTrigger(pt.predname, tSnap, pt.args) - case wand: ast.MagicWand if pt.predname == MagicWandIdentifier(wand, Verifier.program).toString => + case wand: ast.MagicWand if pt.predname == MagicWandIdentifier(wand, s.program).toString => PredicateTrigger(pt.predname, tSnap, pt.args) case _ => pt } @@ -846,7 +854,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { case _: ast.Field => Seq(`?r`) case p: ast.Predicate => s.predicateFormalVarMap(p) case w: ast.MagicWand => - val bodyVars = w.subexpressionsToEvaluate(Verifier.program) + val bodyVars = w.subexpressionsToEvaluate(s.program) bodyVars.indices.toList.map(i => Var(Identifier(s"x$i"), v.symbolConverter.toSort(bodyVars(i).typ))) } val h1 = s.h + ch @@ -889,7 +897,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { val conservedPcs = if (s.recordPcs) (s.conservedPcs.head :+ v.decider.pcs.after(definitionalAxiomMark)) +: s.conservedPcs.tail else s.conservedPcs - val ch = quantifiedChunkSupporter.createSingletonQuantifiedChunk(formalQVars, resource, tArgs, tPerm, sm) + val ch = quantifiedChunkSupporter.createSingletonQuantifiedChunk(formalQVars, resource, tArgs, tPerm, sm, s.program) val h1 = s.h + ch val interpreter = new NonQuantifiedPropertyInterpreter(h1.values, v) @@ -980,7 +988,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { val loss = PermTimes(tPerm, s.permissionScalingFactor) val (relevantChunks, otherChunks) = quantifiedChunkSupporter.splitHeap[QuantifiedBasicChunk]( - h, ChunkIdentifier(resource, Verifier.program)) + h, ChunkIdentifier(resource, s.program)) val (smDef1, smCache1) = quantifiedChunkSupporter.summarisingSnapshotMap( s, resource, formalQVars, relevantChunks, v) @@ -1019,7 +1027,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { v)((s2, heap, rPerm, v2) => { val (relevantChunks, otherChunks) = quantifiedChunkSupporter.splitHeap[QuantifiedBasicChunk]( - heap, ChunkIdentifier(resource, Verifier.program)) + heap, ChunkIdentifier(resource, s.program)) val (result, s3, remainingChunks) = quantifiedChunkSupporter.removePermissions( s2, @@ -1051,7 +1059,8 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { s3.relevantQuantifiedVariables(tArgs), optTrigger.map(_ => tTriggers), qid, - v2 + v2, + s.program ) val h2 = Heap(remainingChunks ++ otherChunks) val s4 = s3.copy(smCache = smCache2, @@ -1113,13 +1122,13 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { (Q: (State, Heap, Term, Verifier) => VerificationResult) : VerificationResult = { - val resource = resourceAccess.res(Verifier.program) + val resource = resourceAccess.res(s.program) val failure = resourceAccess match { case locAcc: ast.LocationAccess => createFailure(pve dueTo InsufficientPermission(locAcc), v, s) case wand: ast.MagicWand => createFailure(pve dueTo MagicWandChunkNotFound(wand), v, s) case _ => sys.error(s"Found resource $resourceAccess, which is not yet supported as a quantified resource.") } - val chunkIdentifier = ChunkIdentifier(resource, Verifier.program) + val chunkIdentifier = ChunkIdentifier(resource, s.program) val chunkOrderHeuristics = optChunkOrderHeuristic match { case Some(heuristics) => @@ -1159,7 +1168,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { } val consumedChunk = quantifiedChunkSupporter.createSingletonQuantifiedChunk( - codomainQVars, resource, arguments, permsTaken, smDef1.sm) + codomainQVars, resource, arguments, permsTaken, smDef1.sm, s.program) val s3 = s2.copy(functionRecorder = s2.functionRecorder.recordFvfAndDomain(smDef1), smCache = smCache1) (result, s3, h2, Some(consumedChunk)) @@ -1223,7 +1232,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { val rmPermRecord = new CommentRecord("removePermissions", s, v.decider.pcs) val sepIdentifier = SymbExLogger.currentLog().openScope(rmPermRecord) - val requiredId = ChunkIdentifier(resource, Verifier.program) + val requiredId = ChunkIdentifier(resource, s.program) assert( relevantChunks forall (_.id == requiredId), s"Expected only chunks for resource $resource, but got: $relevantChunks") diff --git a/src/main/scala/rules/StateConsolidator.scala b/src/main/scala/rules/StateConsolidator.scala index 6c155e5a3..0dce34aed 100644 --- a/src/main/scala/rules/StateConsolidator.scala +++ b/src/main/scala/rules/StateConsolidator.scala @@ -236,7 +236,7 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol for each field. Nearly identical to what the evaluator does for perm(x.f) if f is a QP field */ chunksPerField.foldLeft(si) { case (si, (fieldName, fieldChunks)) => - val field = Verifier.program.findField(fieldName) + val field = s.program.findField(fieldName) val (sn, smDef, pmDef) = quantifiedChunkSupporter.heapSummarisingMaps(si, field, args, fieldChunks, v) val trigger = FieldTrigger(field.name, smDef.sm, receiver) diff --git a/src/main/scala/rules/SymbolicExecutionRules.scala b/src/main/scala/rules/SymbolicExecutionRules.scala index f7ebd1545..0fdbe20ca 100644 --- a/src/main/scala/rules/SymbolicExecutionRules.scala +++ b/src/main/scala/rules/SymbolicExecutionRules.scala @@ -38,7 +38,7 @@ trait SymbolicExecutionRules { case VariablesModel => SiliconVariableCounterexample(s.g, nativeModel) case MappedModel => - SiliconMappedCounterexample(s.g, s.h.values, s.oldHeaps, nativeModel) + SiliconMappedCounterexample(s.g, s.h.values, s.oldHeaps, nativeModel, s.program) } val finalCE = ceTrafo match { case Some(trafo) => trafo.f(ce) diff --git a/src/main/scala/state/State.scala b/src/main/scala/state/State.scala index fa0895ff0..46cf8f7a9 100644 --- a/src/main/scala/state/State.scala +++ b/src/main/scala/state/State.scala @@ -13,11 +13,15 @@ import viper.silicon.common.collections.immutable.InsertionOrderedSet import viper.silicon.decider.RecordedPathConditions import viper.silicon.state.State.OldHeaps import viper.silicon.state.terms.{Term, Var} -import viper.silicon.supporters.functions.{FunctionRecorder, NoopFunctionRecorder} +import viper.silicon.supporters.PredicateData +import viper.silicon.supporters.functions.{FunctionData, FunctionRecorder, NoopFunctionRecorder} import viper.silicon.{Map, Stack} final case class State(g: Store = Store(), h: Heap = Heap(), + program: ast.Program, + predicateData: Map[ast.Predicate, PredicateData], + functionData: Map[ast.Function, FunctionData], oldHeaps: OldHeaps = Map.empty, parallelizeBranches: Boolean = false, @@ -121,7 +125,10 @@ object State { def merge(s1: State, s2: State): State = { s1 match { /* Decompose state s1 */ - case State(g1, h1, oldHeaps1, + case State(g1, h1, program, + predicateData, + functionData, + oldHeaps1, parallelizeBranches1, recordVisited1, visited1, methodCfg1, invariantContexts1, @@ -142,7 +149,10 @@ object State { /* Decompose state s2: most values must match those of s1 */ s2 match { - case State(`g1`, `h1`, `oldHeaps1`, + case State(`g1`, `h1`, + `program`, + `predicateData`, `functionData`, + `oldHeaps1`, `parallelizeBranches1`, `recordVisited1`, `visited1`, `methodCfg1`, `invariantContexts1`, diff --git a/src/main/scala/state/SymbolConverter.scala b/src/main/scala/state/SymbolConverter.scala index 282fff624..d956309c9 100644 --- a/src/main/scala/state/SymbolConverter.scala +++ b/src/main/scala/state/SymbolConverter.scala @@ -15,8 +15,8 @@ trait SymbolConverter { def toSortSpecificId(name: String, sorts: Seq[Sort]): Identifier - def toFunction(function: ast.DomainFunc): terms.DomainFun - def toFunction(function: ast.DomainFunc, sorts: Seq[Sort]): terms.DomainFun + def toFunction(function: ast.DomainFunc, prog: ast.Program): terms.DomainFun + def toFunction(function: ast.DomainFunc, sorts: Seq[Sort], prog: ast.Program): terms.DomainFun def toFunction(function: ast.BackendFunc): terms.SMTFun @@ -53,11 +53,11 @@ class DefaultSymbolConverter extends SymbolConverter { def toSortSpecificId(name: String, sorts: Seq[Sort]): Identifier = Identifier(name + sorts.mkString("[",",","]")) - def toFunction(function: ast.DomainFunc): terms.DomainFun = { + def toFunction(function: ast.DomainFunc, program: ast.Program): terms.DomainFun = { val inSorts = function.formalArgs map (_.typ) map toSort val outSort = toSort(function.typ) - toFunction(function, inSorts :+ outSort) + toFunction(function, inSorts :+ outSort, program) } def toFunction(function: ast.BackendFunc): terms.SMTFun = { @@ -69,12 +69,12 @@ class DefaultSymbolConverter extends SymbolConverter { terms.SMTFun(id, inSorts, outSort) } - def toFunction(function: ast.DomainFunc, sorts: Seq[Sort]): terms.DomainFun = { + def toFunction(function: ast.DomainFunc, sorts: Seq[Sort], program: ast.Program): terms.DomainFun = { assert(sorts.nonEmpty, "Expected at least one sort, but found none") val inSorts = sorts.init val outSort = sorts.last - val domainFunc = Verifier.program.findDomainFunctionOptionally(function.name) + val domainFunc = program.findDomainFunctionOptionally(function.name) val id = if (domainFunc.isEmpty) Identifier(function.name) else toSortSpecificId(function.name, Seq(outSort)) terms.DomainFun(id, inSorts, outSort) diff --git a/src/main/scala/state/Terms.scala b/src/main/scala/state/Terms.scala index 9ef303fdc..dfa1adbc5 100644 --- a/src/main/scala/state/Terms.scala +++ b/src/main/scala/state/Terms.scala @@ -1987,8 +1987,8 @@ object ResourceTriggerFunction { def apply(predicate: ast.Predicate, sm: Term, args: Seq[Term]): PredicateTrigger = PredicateTrigger(predicate.name, sm, args) - def apply(wand: ast.MagicWand, sm: Term, args: Seq[Term]): PredicateTrigger = { - val wandId = MagicWandIdentifier(wand, Verifier.program).toString + def apply(wand: ast.MagicWand, sm: Term, args: Seq[Term], program: ast.Program): PredicateTrigger = { + val wandId = MagicWandIdentifier(wand, program).toString PredicateTrigger(wandId, sm, args) } @@ -2011,8 +2011,8 @@ object ResourceLookup { def apply(predicate: ast.Predicate, sm: Term, args: Seq[Term]): PredicateLookup = PredicateLookup(predicate.name, sm, args) - def apply(wand: ast.MagicWand, sm: Term, args: Seq[Term]): PredicateLookup = { - val wandId = MagicWandIdentifier(wand, Verifier.program).toString + def apply(wand: ast.MagicWand, sm: Term, args: Seq[Term], program: ast.Program): PredicateLookup = { + val wandId = MagicWandIdentifier(wand, program).toString PredicateLookup(wandId, sm, args) } @@ -2035,8 +2035,8 @@ object ResourcePermissionLookup { def apply(predicate: ast.Predicate, sm: Term, args: Seq[Term]): PredicatePermLookup = PredicatePermLookup(predicate.name, sm, args) - def apply(wand: ast.MagicWand, sm: Term, args: Seq[Term]): PredicatePermLookup = { - val wandId = MagicWandIdentifier(wand, Verifier.program).toString + def apply(wand: ast.MagicWand, sm: Term, args: Seq[Term], program: ast.Program): PredicatePermLookup = { + val wandId = MagicWandIdentifier(wand, program).toString PredicatePermLookup(wandId, sm, args) } diff --git a/src/main/scala/supporters/BuiltinDomainsContributor.scala b/src/main/scala/supporters/BuiltinDomainsContributor.scala index a27ef44e6..28708d6f4 100644 --- a/src/main/scala/supporters/BuiltinDomainsContributor.scala +++ b/src/main/scala/supporters/BuiltinDomainsContributor.scala @@ -8,6 +8,7 @@ package viper.silicon.supporters import java.io.File import java.net.URL + import scala.annotation.unused import scala.reflect.ClassTag import viper.silver.ast @@ -16,6 +17,7 @@ import viper.silicon.interfaces.PreambleContributor import viper.silicon.interfaces.decider.ProverLike import viper.silicon.state.DefaultSymbolConverter import viper.silicon.state.terms._ +import viper.silver.ast.LineCol abstract class BuiltinDomainsContributor extends PreambleContributor[Sort, DomainFun, Term] { type BuiltinDomainType <: ast.GenericType @@ -87,7 +89,7 @@ abstract class BuiltinDomainsContributor extends PreambleContributor[Sort, Domai val sourceDomainInstantiations = sourceDomainInstantiationsWithType.map(x => x._2) collectSorts(sourceDomainTypeInstances) - collectFunctions(sourceDomainInstantiations) + collectFunctions(sourceDomainInstantiations, program) collectAxioms(sourceDomainInstantiationsWithType) } @@ -109,10 +111,10 @@ abstract class BuiltinDomainsContributor extends PreambleContributor[Sort, Domai }) } - protected def collectFunctions(domains: Set[ast.Domain]): Unit = { + protected def collectFunctions(domains: Set[ast.Domain], program: ast.Program): Unit = { domains foreach ( _.functions foreach (df => - collectedFunctions += symbolConverter.toFunction(df))) + collectedFunctions += symbolConverter.toFunction(df, program))) } protected def collectAxioms(domains: Set[(ast.DomainType, ast.Domain)]): Unit = { @@ -190,7 +192,9 @@ private object utils { source.close() } - viper.silver.parser.FastParser.parse(content, fromPath) match { + val fp = new viper.silver.parser.FastParser() + val lc = new LineCol(fp) + fp.parse(content, fromPath) match { case fastparse.Parsed.Success(parsedProgram: viper.silver.parser.PProgram, _) => assert(parsedProgram.errors.isEmpty, s"Unexpected parsing errors: ${parsedProgram.errors}") @@ -202,7 +206,7 @@ private object utils { program case fastparse.Parsed.Failure(msg, index, _) => - val (line, col) = ast.LineCol(index) + val (line, col) = lc.apply(index) sys.error(s"Failure: $msg, at ${viper.silver.ast.FilePosition(fromPath, line, col)}") //? val pos = extra.input.prettyIndex(index).split(":").map(_.toInt) //? sys.error(s"Failure: $msg, at ${viper.silver.ast.FilePosition(fromPath, pos(0), pos(1))}") diff --git a/src/main/scala/supporters/Domains.scala b/src/main/scala/supporters/Domains.scala index 3d10fdaf0..8cfb6e46f 100644 --- a/src/main/scala/supporters/Domains.scala +++ b/src/main/scala/supporters/Domains.scala @@ -14,7 +14,7 @@ import viper.silicon.interfaces.PreambleContributor import viper.silicon.interfaces.decider.ProverLike import viper.silicon.state.{SymbolConverter, terms} import viper.silicon.state.terms.{Distinct, DomainFun, Sort, Symbol, Term} -import viper.silver.ast.NamedDomainAxiom +import viper.silver.ast.{NamedDomainAxiom, Program} trait DomainsContributor[SO, SY, AX, UA] extends PreambleContributor[SO, SY, AX] { def uniquenessAssumptionsAfterAnalysis: Iterable[UA] @@ -56,7 +56,7 @@ class DefaultDomainsContributor(symbolConverter: SymbolConverter, necessaryDomainTypes map (cdt => domainNameMap(cdt.domainName).instantiate(cdt, program)) collectDomainSorts(necessaryDomainTypes) - collectDomainMembers(instantiatedDomains) + collectDomainMembers(instantiatedDomains, program) } private def collectDomainSorts(domainTypes: Iterable[ast.DomainType]): Unit = { @@ -68,7 +68,7 @@ class DefaultDomainsContributor(symbolConverter: SymbolConverter, }) } - private def collectDomainMembers(instantiatedDomains: Set[ast.Domain]): Unit = { + private def collectDomainMembers(instantiatedDomains: Set[ast.Domain], program: ast.Program): Unit = { /* Since domain member instances come with Silver types, but the corresponding prover * declarations work with Silicon sorts, it can happen that two instances with different types * result in the same function declaration because the types are mapped to the same sort(s). @@ -84,7 +84,7 @@ class DefaultDomainsContributor(symbolConverter: SymbolConverter, instantiatedDomains foreach (domain => { domain.functions foreach (function => { - val fct = symbolConverter.toFunction(function) + val fct = symbolConverter.toFunction(function, program) collectedFunctions += fct diff --git a/src/main/scala/supporters/ExpressionTranslator.scala b/src/main/scala/supporters/ExpressionTranslator.scala index 174bb9eb1..ec559e225 100644 --- a/src/main/scala/supporters/ExpressionTranslator.scala +++ b/src/main/scala/supporters/ExpressionTranslator.scala @@ -19,6 +19,7 @@ trait ExpressionTranslator { * was done before - but that is less efficient and creates lots of additional noise output * in the prover log. */ + protected def program: ast.Program protected def translate(toSort: ast.Type => Sort) (exp: ast.Exp) @@ -125,7 +126,7 @@ trait ExpressionTranslator { val tArgs = args map f val inSorts = tArgs map (_.sort) val outSort = toSort(exp.typ) - val domainFunc = Verifier.program.findDomainFunctionOptionally(funcName) + val domainFunc = program.findDomainFunctionOptionally(funcName) val id = if (domainFunc.isEmpty) Identifier(funcName) else Identifier(funcName + Seq(outSort).mkString("[",",","]")) val df = Fun(id, inSorts, outSort) App(df, tArgs) diff --git a/src/main/scala/supporters/PredicateVerificationUnit.scala b/src/main/scala/supporters/PredicateVerificationUnit.scala index efa9f04a7..7db3a727f 100644 --- a/src/main/scala/supporters/PredicateVerificationUnit.scala +++ b/src/main/scala/supporters/PredicateVerificationUnit.scala @@ -50,7 +50,7 @@ trait DefaultPredicateVerificationUnitProvider extends VerifierComponent { v: Ve object predicateSupporter extends PredicateVerificationUnit with StatefulComponent { import viper.silicon.rules.producer._ - private var predicateData: Map[ast.Predicate, PredicateData] = Map.empty + /*private*/ var predicateData: Map[ast.Predicate, PredicateData] = Map.empty def data = predicateData def units = predicateData.keys.toSeq @@ -79,10 +79,6 @@ trait DefaultPredicateVerificationUnitProvider extends VerifierComponent { v: Ve val axiomsAfterAnalysis: Iterable[Term] = Seq.empty def emitAxiomsAfterAnalysis(sink: ProverLike): Unit = () - def updateGlobalStateAfterAnalysis(): Unit = { - Verifier.predicateData = predicateData - } - /* Verification and subsequent preamble contribution */ def verify(sInit: State, predicate: ast.Predicate): Seq[VerificationResult] = { @@ -124,10 +120,6 @@ trait DefaultPredicateVerificationUnitProvider extends VerifierComponent { v: Ve val axiomsAfterVerification: Iterable[Term] = Seq.empty def emitAxiomsAfterVerification(sink: ProverLike): Unit = () - def contributeToGlobalStateAfterVerification(): Unit = { - Verifier.predicateData = predicateData - } - /* Lifetime */ def start(): Unit = {} diff --git a/src/main/scala/supporters/functions/FunctionVerificationUnit.scala b/src/main/scala/supporters/functions/FunctionVerificationUnit.scala index 8c1c40b04..bc49b1c70 100644 --- a/src/main/scala/supporters/functions/FunctionVerificationUnit.scala +++ b/src/main/scala/supporters/functions/FunctionVerificationUnit.scala @@ -22,6 +22,7 @@ import viper.silicon.common.collections.immutable.InsertionOrderedSet import viper.silicon.decider.Decider import viper.silicon.logger.SymbExLogger import viper.silicon.rules.{consumer, evaluator, executionFlowController, producer} +import viper.silicon.supporters.PredicateData import viper.silicon.verifier.{Verifier, VerifierComponent} import viper.silicon.utils.{freshSnap, toSf} @@ -46,7 +47,7 @@ trait DefaultFunctionVerificationUnitProvider extends VerifierComponent { v: Ver import evaluator._ @unused private var program: ast.Program = _ - private var functionData: Map[ast.Function, FunctionData] = Map.empty + /*private*/ var functionData: Map[ast.Function, FunctionData] = Map.empty private var emittedFunctionAxioms: Vector[Term] = Vector.empty private var freshVars: Vector[Var] = Vector.empty private var postConditionAxioms: Vector[Term] = Vector.empty @@ -62,6 +63,8 @@ trait DefaultFunctionVerificationUnitProvider extends VerifierComponent { v: Ver symbolConverter, fresh, resolutionFailureMessage, (_, _) => false, reporter) } + var predicateData: Map[ast.Predicate, PredicateData] = _ + def units = functionData.keys.toSeq /* Preamble contribution */ @@ -86,7 +89,7 @@ trait DefaultFunctionVerificationUnitProvider extends VerifierComponent { v: Ver heights.map { case (func, height) => val quantifiedFields = InsertionOrderedSet(ast.utility.QuantifiedPermissions.quantifiedFields(func, program)) val data = new FunctionData(func, height, quantifiedFields, program)(symbolConverter, expressionTranslator, - identifierFactory, pred => Verifier.predicateData(pred), Verifier.config, + identifierFactory, pred => predicateData(pred), Verifier.config, reporter) func -> data}) @@ -135,10 +138,6 @@ trait DefaultFunctionVerificationUnitProvider extends VerifierComponent { v: Ver val axiomsAfterAnalysis: Iterable[Term] = Seq.empty def emitAxiomsAfterAnalysis(sink: ProverLike): Unit = () - def updateGlobalStateAfterAnalysis(): Unit = { - Verifier.functionData = functionData - } - def getPostConditionAxioms() = this.postConditionAxioms /* Verification and subsequent preamble contribution */ @@ -299,10 +298,6 @@ trait DefaultFunctionVerificationUnitProvider extends VerifierComponent { v: Ver emittedFunctionAxioms foreach sink.assume } - def contributeToGlobalStateAfterVerification(): Unit = { - Verifier.functionData = functionData - } - /* Lifetime */ def start(): Unit = {} diff --git a/src/main/scala/supporters/functions/HeapAccessReplacingExpressionTranslator.scala b/src/main/scala/supporters/functions/HeapAccessReplacingExpressionTranslator.scala index 708fabb49..c1cdbce9d 100644 --- a/src/main/scala/supporters/functions/HeapAccessReplacingExpressionTranslator.scala +++ b/src/main/scala/supporters/functions/HeapAccessReplacingExpressionTranslator.scala @@ -25,7 +25,7 @@ class HeapAccessReplacingExpressionTranslator(symbolConverter: SymbolConverter, extends ExpressionTranslator with LazyLogging { - private var program: ast.Program = _ + protected var program: ast.Program = _ @unused private var func: ast.Function = _ private var data: FunctionData = _ private var ignoreAccessPredicates = false diff --git a/src/main/scala/verifier/DefaultMasterVerifier.scala b/src/main/scala/verifier/DefaultMasterVerifier.scala index b0c97f19d..e0bd3bf64 100644 --- a/src/main/scala/verifier/DefaultMasterVerifier.scala +++ b/src/main/scala/verifier/DefaultMasterVerifier.scala @@ -8,6 +8,7 @@ package viper.silicon.verifier import java.text.SimpleDateFormat import java.util.concurrent._ + import scala.annotation.unused import scala.collection.mutable import scala.util.Random @@ -24,7 +25,7 @@ import viper.silicon.reporting.{MultiRunRecorders, condenseToViperResult} import viper.silicon.state._ import viper.silicon.state.terms.{Decl, Sort, Term, sorts} import viper.silicon.supporters._ -import viper.silicon.supporters.functions.DefaultFunctionVerificationUnitProvider +import viper.silicon.supporters.functions.{DefaultFunctionVerificationUnitProvider, FunctionData} import viper.silicon.supporters.qps._ import viper.silicon.utils.Counter import viper.silver.ast.{BackendType, Member} @@ -159,14 +160,12 @@ class DefaultMasterVerifier(config: Config, override val reporter: Reporter) println(program) } - Verifier.program = program - predSnapGenerator.setup(program) // TODO: Why did Nadja put this here? allProvers.comment("Started: " + new SimpleDateFormat("yyyy-MM-dd HH:mm:ss").format(System.currentTimeMillis()) /*bookkeeper.formattedStartTime*/) allProvers.comment("Silicon.version: " + Silicon.version) - allProvers.comment(s"Input file: ${Verifier.inputFile.getOrElse("")}") + //allProvers.comment(s"Input file: ${Verifier.inputFile.getOrElse("")}") allProvers.comment(s"Verifier id: $uniqueId") allProvers.comment("-" * 60) allProvers.comment("Begin preamble") @@ -174,7 +173,7 @@ class DefaultMasterVerifier(config: Config, override val reporter: Reporter) allProvers.comment("/" * 10 + " Static preamble") emitStaticPreamble(allProvers) - analyzeProgramAndEmitPreambleContributions(program, allProvers) // TODO: Add support for cfgs. + val (functionData, predicateData) = analyzeProgramAndEmitPreambleContributions(program, allProvers) // TODO: Add support for cfgs. allProvers.comment("End preamble") allProvers.comment("-" * 60) @@ -190,7 +189,7 @@ class DefaultMasterVerifier(config: Config, override val reporter: Reporter) */ val functionVerificationResults = functionsSupporter.units.toList flatMap (function => { val startTime = System.currentTimeMillis() - val results = functionsSupporter.verify(createInitialState(function, program), function) + val results = functionsSupporter.verify(createInitialState(function, program, functionData, predicateData), function) val elapsed = System.currentTimeMillis() - startTime reporter report VerificationResultMessage(s"silicon", function, elapsed, condenseToViperResult(results)) logger debug s"Silicon finished verification of function `${function.name}` in ${viper.silver.reporter.format.formatMillisReadably(elapsed)} seconds with the following result: ${condenseToViperResult(results).toString}" @@ -199,7 +198,7 @@ class DefaultMasterVerifier(config: Config, override val reporter: Reporter) val predicateVerificationResults = predicateSupporter.units.toList flatMap (predicate => { val startTime = System.currentTimeMillis() - val results = predicateSupporter.verify(createInitialState(predicate, program), predicate) + val results = predicateSupporter.verify(createInitialState(predicate, program, functionData, predicateData), predicate) val elapsed = System.currentTimeMillis() - startTime reporter report VerificationResultMessage(s"silicon", predicate, elapsed, condenseToViperResult(results)) logger debug s"Silicon finished verification of predicate `${predicate.name}` in ${viper.silver.reporter.format.formatMillisReadably(elapsed)} seconds with the following result: ${condenseToViperResult(results).toString}" @@ -221,7 +220,7 @@ class DefaultMasterVerifier(config: Config, override val reporter: Reporter) val verificationTaskFutures: Seq[Future[Seq[VerificationResult]]] = program.methods.filterNot(excludeMethod).map(method => { - val s = createInitialState(method, program)/*.copy(parallelizeBranches = true)*/ /* [BRANCH-PARALLELISATION] */ + val s = createInitialState(method, program, functionData, predicateData)/*.copy(parallelizeBranches = true)*/ /* [BRANCH-PARALLELISATION] */ _verificationPoolManager.queueVerificationTask(v => { val startTime = System.currentTimeMillis() @@ -234,7 +233,7 @@ class DefaultMasterVerifier(config: Config, override val reporter: Reporter) setErrorScope(results, method) }) }) ++ cfgs.map(cfg => { - val s = createInitialState(cfg, program)/*.copy(parallelizeBranches = true)*/ /* [BRANCH-PARALLELISATION] */ + val s = createInitialState(cfg, program, functionData, predicateData)/*.copy(parallelizeBranches = true)*/ /* [BRANCH-PARALLELISATION] */ _verificationPoolManager.queueVerificationTask(v => { val startTime = System.currentTimeMillis() @@ -262,12 +261,15 @@ class DefaultMasterVerifier(config: Config, override val reporter: Reporter) ++ methodVerificationResults) } - private def createInitialState(member: ast.Member, program: ast.Program): State = { + private def createInitialState(member: ast.Member, program: ast.Program, + functionData: Map[ast.Function, FunctionData], predicateData: Map[ast.Predicate, PredicateData]): State = { val quantifiedFields = InsertionOrderedSet(ast.utility.QuantifiedPermissions.quantifiedFields(member, program)) val quantifiedPredicates = InsertionOrderedSet(ast.utility.QuantifiedPermissions.quantifiedPredicates(member, program)) val quantifiedMagicWands = InsertionOrderedSet(ast.utility.QuantifiedPermissions.quantifiedMagicWands(member, program)).map(MagicWandIdentifier(_, program)) - State(qpFields = quantifiedFields, + State(program=program, functionData = functionData, + predicateData = predicateData, + qpFields = quantifiedFields, qpPredicates = quantifiedPredicates, qpMagicWands = quantifiedMagicWands, predicateSnapMap = predSnapGenerator.snapMap, @@ -275,12 +277,14 @@ class DefaultMasterVerifier(config: Config, override val reporter: Reporter) isMethodVerification = member.isInstanceOf[ast.Member]) } - private def createInitialState(@unused cfg: SilverCfg, program: ast.Program): State = { + private def createInitialState(@unused cfg: SilverCfg, program: ast.Program, + functionData: Map[ast.Function, FunctionData], predicateData: Map[ast.Predicate, PredicateData]): State = { val quantifiedFields = InsertionOrderedSet(program.fields) val quantifiedPredicates = InsertionOrderedSet(program.predicates) val quantifiedMagicWands = InsertionOrderedSet[MagicWandIdentifier]() // TODO: Implement support for quantified magic wands. - State(qpFields = quantifiedFields, + State(program=program, functionData = functionData, + predicateData = predicateData, qpFields = quantifiedFields, qpPredicates = quantifiedPredicates, qpMagicWands = quantifiedMagicWands, predicateSnapMap = predSnapGenerator.snapMap, @@ -387,11 +391,13 @@ class DefaultMasterVerifier(config: Config, override val reporter: Reporter) predicateSupporter ) - private def analyzeProgramAndEmitPreambleContributions(program: ast.Program, sink: ProverLike): Unit = { + private def analyzeProgramAndEmitPreambleContributions(program: ast.Program, sink: ProverLike) = { analysisOrder foreach (component => { component.analyze(program) - component.updateGlobalStateAfterAnalysis() }) + val predicateData = predicateSupporter.predicateData + val functionData = functionsSupporter.functionData + functionsSupporter.predicateData = predicateData sink.comment("/" * 10 + " Sorts") sortDeclarationOrder foreach (component => @@ -424,6 +430,8 @@ class DefaultMasterVerifier(config: Config, override val reporter: Reporter) sink.comment("/" * 10 + " Axioms") axiomDeclarationOrder foreach (component => component.emitAxiomsAfterAnalysis(sink)) + + (functionData, predicateData) } private def emitSortWrappers(ss: Iterable[Sort], sink: ProverLike): Unit = { diff --git a/src/main/scala/verifier/Verifier.scala b/src/main/scala/verifier/Verifier.scala index 9029ea9a4..c0ef4e64f 100644 --- a/src/main/scala/verifier/Verifier.scala +++ b/src/main/scala/verifier/Verifier.scala @@ -46,8 +46,6 @@ trait Verifier { || Verifier.config.numberOfErrorsToReport() == 0); } -/* TODO: Replace getters and setters by public vars - TODO: Add a description to each var that explain when it is expected to be set */ object Verifier { val PRE_STATE_LABEL = "old" val MAGIC_WAND_LHS_STATE_LABEL = ast.LabelledOld.LhsOldLabel @@ -55,6 +53,11 @@ object Verifier { private var _config: Config = _ def config: Config = _config /*private*/ def config_=(config: Config): Unit = { _config = config } +} + +/* TODO: Replace getters and setters by public vars + TODO: Add a description to each var that explain when it is expected to be set */ +class VerifierState { private var _program: ast.Program = _ def program: ast.Program = _program diff --git a/src/test/scala/CounterexampleTests.scala b/src/test/scala/CounterexampleTests.scala index 22978c818..8dae07ff1 100644 --- a/src/test/scala/CounterexampleTests.scala +++ b/src/test/scala/CounterexampleTests.scala @@ -12,8 +12,7 @@ import fastparse._ import viper.silicon.interfaces.SiliconMappedCounterexample import viper.silicon.reporting.{ExtractedModel, ExtractedModelEntry, LitIntEntry, LitPermEntry, NullRefEntry, RecursiveRefEntry, RefEntry, SeqEntry} import viper.silicon.state.terms.Rational -import viper.silicon.tests.CounterexampleParser.ExpectedCounterexample -import viper.silver.parser.FastParser.{_line_offset, whitespace} +import viper.silver.parser.FastParserCompanion.whitespace import viper.silver.parser.{FastParser, PAccPred, PBinExp, PExp, PFieldAccess, PIdnUse, PIntLit, PLookup, PUnExp} import viper.silver.verifier.{FailureContext, VerificationError} @@ -57,17 +56,19 @@ class CounterexampleTests extends SiliconTests { private def isExpectedCounterexample(annotation: String, file: Path, lineNr: Int): Option[TestAnnotation] = { def parseExpectedCounterexample(id: OutputAnnotationId, expectedCounterexampleString: String): Option[ExpectedCounterexampleAnnotation] = { // in order to reuse as much of the existing Viper parser as possible, we have to initialize the `_file` and `_line_offset` fields: - FastParser._file = file.toAbsolutePath + val fp = new FastParser() + fp._file = file.toAbsolutePath val lines = expectedCounterexampleString.linesWithSeparators - _line_offset = (lines.map(_.length) ++ Seq(0)).toArray + fp._line_offset = (lines.map(_.length) ++ Seq(0)).toArray var offset = 0 - for (i <- _line_offset.indices) { - val line_length = _line_offset(i) - _line_offset(i) = offset + for (i <- fp._line_offset.indices) { + val line_length = fp._line_offset(i) + fp._line_offset(i) = offset offset += line_length } + val cParser = new CounterexampleParser(fp) // now parsing is actually possible: - fastparse.parse(expectedCounterexampleString, CounterexampleParser.expectedCounterexample(_)) match { + fastparse.parse(expectedCounterexampleString, cParser.expectedCounterexample(_)) match { case Parsed.Success(expectedCounterexample, _) => Some(ExpectedCounterexampleAnnotation(id, file, lineNr, expectedCounterexample)) case Parsed.Failure(_, _, extra) => println(s"Parsing expected counterexample failed in file $file: ${extra.trace().longAggregateMsg}") @@ -172,16 +173,17 @@ case class ExpectedCounterexampleAnnotation(id: OutputAnnotationId, file: Path, * Currently, a counterexample is expressed by a comma separated list of access predicates and equalities (using the * same syntax as in Viper) */ -object CounterexampleParser { +class CounterexampleParser(fp: FastParser) { + def expectedCounterexample[_: P]: P[ExpectedCounterexample] = - (Start ~ "(" ~ (FastParser.accessPred | FastParser.eqExp).rep(0, ",") ~ ")" ~ End) + (Start ~ "(" ~ (fp.accessPred | fp.eqExp).rep(0, ",") ~ ")" ~ End) .map(ExpectedCounterexample) +} - case class ExpectedCounterexample(exprs: Seq[PExp]) { - assert(exprs.forall { - case _: PAccPred => true - case PBinExp(_, "==", _) => true - case _ => false - }) - } +case class ExpectedCounterexample(exprs: Seq[PExp]) { + assert(exprs.forall { + case _: PAccPred => true + case PBinExp(_, "==", _) => true + case _ => false + }) } From 97d67b9d08c8badfd09a1a08f2635464b69f5481 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Thu, 18 Aug 2022 15:00:34 +0200 Subject: [PATCH 2/7] WIP --- src/main/scala/extensions/TryBlockParserPlugin.scala | 4 ++-- .../scala/supporters/BuiltinDomainsContributor.scala | 2 +- src/main/scala/supporters/Domains.scala | 9 ++++++--- src/main/scala/supporters/ExpressionTranslator.scala | 5 ++--- src/test/scala/PortableSiliconTests.scala | 2 +- src/test/scala/SiliconTests.scala | 2 +- src/test/scala/SymbExLoggerTests.scala | 2 +- 7 files changed, 14 insertions(+), 12 deletions(-) diff --git a/src/main/scala/extensions/TryBlockParserPlugin.scala b/src/main/scala/extensions/TryBlockParserPlugin.scala index 4bf37db8c..fd19cafcc 100644 --- a/src/main/scala/extensions/TryBlockParserPlugin.scala +++ b/src/main/scala/extensions/TryBlockParserPlugin.scala @@ -6,13 +6,13 @@ package viper.silicon.extensions -import viper.silver.parser.{FastParser, ParserExtension} +import viper.silver.parser.FastParser import viper.silver.plugin.{ParserPluginTemplate, SilverPlugin} class TryBlockParserPlugin(fp: FastParser) extends SilverPlugin with ParserPluginTemplate { import fastparse._ import viper.silver.parser.FastParserCompanion.whitespace - import fp.{FP, block} + import fp.{FP, block, ParserExtension} private val tryKeyword = "try" diff --git a/src/main/scala/supporters/BuiltinDomainsContributor.scala b/src/main/scala/supporters/BuiltinDomainsContributor.scala index 28708d6f4..892756d2a 100644 --- a/src/main/scala/supporters/BuiltinDomainsContributor.scala +++ b/src/main/scala/supporters/BuiltinDomainsContributor.scala @@ -129,7 +129,7 @@ abstract class BuiltinDomainsContributor extends PreambleContributor[Sort, Domai * are preserved. */ val domainName = f"${d.domainName}[${d.typVarsMap.values.map(t => symbolConverter.toSort(t)).mkString(",")}]" - domainTranslator.translateAxiom(ax, symbolConverter.toSort).transform { + domainTranslator.translateAxiom(ax, symbolConverter.toSort, true).transform { case q@Quantification(_,_,_,_,name,_) if name != "" => q.copy(name = f"${domainName}_${name}") case Equals(t1, t2) => BuiltinEquals(t1, t2) diff --git a/src/main/scala/supporters/Domains.scala b/src/main/scala/supporters/Domains.scala index 8cfb6e46f..7a253b96a 100644 --- a/src/main/scala/supporters/Domains.scala +++ b/src/main/scala/supporters/Domains.scala @@ -132,15 +132,16 @@ class DefaultDomainsContributor(symbolConverter: SymbolConverter, } trait DomainsTranslator[R] { - def translateAxiom(ax: ast.DomainAxiom, toSort: ast.Type => Sort): R + def translateAxiom(ax: ast.DomainAxiom, toSort: ast.Type => Sort, builtin: Boolean = false): R } class DefaultDomainsTranslator() extends DomainsTranslator[Term] with ExpressionTranslator { - def translateAxiom(ax: ast.DomainAxiom, toSort: ast.Type => Sort): Term = { - translate(toSort)(ax.exp) match { + def translateAxiom(ax: ast.DomainAxiom, toSort: ast.Type => Sort, builtin: Boolean = false): Term = { + isBuiltin = builtin + val res = translate(toSort)(ax.exp) match { case terms.Quantification(q, vars, body, triggers, "", _) => val qid = ax match { case axiom: NamedDomainAxiom => s"prog.${axiom.name}" @@ -151,5 +152,7 @@ class DefaultDomainsTranslator() case other => other } + isBuiltin = false + res } } diff --git a/src/main/scala/supporters/ExpressionTranslator.scala b/src/main/scala/supporters/ExpressionTranslator.scala index ec559e225..07997090c 100644 --- a/src/main/scala/supporters/ExpressionTranslator.scala +++ b/src/main/scala/supporters/ExpressionTranslator.scala @@ -19,7 +19,7 @@ trait ExpressionTranslator { * was done before - but that is less efficient and creates lots of additional noise output * in the prover log. */ - protected def program: ast.Program + protected var isBuiltin: Boolean = false protected def translate(toSort: ast.Type => Sort) (exp: ast.Exp) @@ -126,8 +126,7 @@ trait ExpressionTranslator { val tArgs = args map f val inSorts = tArgs map (_.sort) val outSort = toSort(exp.typ) - val domainFunc = program.findDomainFunctionOptionally(funcName) - val id = if (domainFunc.isEmpty) Identifier(funcName) else Identifier(funcName + Seq(outSort).mkString("[",",","]")) + val id = if (isBuiltin) Identifier(funcName) else Identifier(funcName + Seq(outSort).mkString("[",",","]")) val df = Fun(id, inSorts, outSort) App(df, tArgs) diff --git a/src/test/scala/PortableSiliconTests.scala b/src/test/scala/PortableSiliconTests.scala index 4fc17a98e..16813a870 100644 --- a/src/test/scala/PortableSiliconTests.scala +++ b/src/test/scala/PortableSiliconTests.scala @@ -100,7 +100,7 @@ class PortableSiliconTests extends SilSuite with StatisticalTestSuite { /* If needed, Silicon reads the filename of the program under verification from Verifier.inputFile. When the test suite is executed (sbt test/testOnly), Verifier.inputFile is set here. When Silicon is run from the command line, Verifier.inputFile is set in src/main/scala/Silicon.scala. */ - viper.silicon.verifier.Verifier.inputFile = Some(files.head) + //viper.silicon.verifier.Verifier.inputFile = Some(files.head) val fe = new SiliconFrontend(NoopReporter)//SiliconFrontendWithUnitTesting() fe.init(verifier) diff --git a/src/test/scala/SiliconTests.scala b/src/test/scala/SiliconTests.scala index 5c19f50e9..260745565 100644 --- a/src/test/scala/SiliconTests.scala +++ b/src/test/scala/SiliconTests.scala @@ -31,7 +31,7 @@ class SiliconTests extends SilSuite { /* If needed, Silicon reads the filename of the program under verification from Verifier.inputFile. When the test suite is executed (sbt test/testOnly), Verifier.inputFile is set here. When Silicon is run from the command line, Verifier.inputFile is set in src/main/scala/Silicon.scala. */ - viper.silicon.verifier.Verifier.inputFile = Some(files.head) + //viper.silicon.verifier.Verifier.inputFile = Some(files.head) val fe = new SiliconFrontend(NoopReporter) fe.init(verifier) diff --git a/src/test/scala/SymbExLoggerTests.scala b/src/test/scala/SymbExLoggerTests.scala index af904cc20..863dc52df 100644 --- a/src/test/scala/SymbExLoggerTests.scala +++ b/src/test/scala/SymbExLoggerTests.scala @@ -27,7 +27,7 @@ class SymbExLoggerTests extends SilSuite { /* If needed, Silicon reads the filename of the program under verification from Verifier.inputFile. When the test suite is executed (sbt test/testOnly), Verifier.inputFile is set here. When Silicon is run from the command line, Verifier.inputFile is set in src/main/scala/Silicon.scala. */ - viper.silicon.verifier.Verifier.inputFile = Some(files.head) + //viper.silicon.verifier.Verifier.inputFile = Some(files.head) // For Unit-Testing of the Symbolic Execution Logging, the name of the file // to be tested must be known, which is why it's passed here to the SymbExLogger-Object. From 438397b1d9a662e19007e84eff17b26f639c8b48 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Thu, 18 Aug 2022 16:43:04 +0200 Subject: [PATCH 3/7] Setting multi run recorder state --- src/main/scala/Silicon.scala | 8 +++++--- src/main/scala/reporting/MultiRunRecorder.scala | 2 +- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/src/main/scala/Silicon.scala b/src/main/scala/Silicon.scala index bbf4785f7..dc07227fd 100644 --- a/src/main/scala/Silicon.scala +++ b/src/main/scala/Silicon.scala @@ -9,6 +9,7 @@ package viper.silicon import java.nio.file.Paths import java.text.SimpleDateFormat import java.util.concurrent.{Callable, Executors, TimeUnit, TimeoutException} + import scala.collection.immutable.ArraySeq import scala.util.{Left, Right} import ch.qos.logback.classic.{Level, Logger} @@ -20,11 +21,12 @@ import viper.silver.reporter._ import viper.silver.verifier.{AbstractVerificationError => SilAbstractVerificationError, Failure => SilFailure, Success => SilSuccess, TimeoutOccurred => SilTimeoutOccurred, VerificationResult => SilVerificationResult, Verifier => SilVerifier} import viper.silicon.interfaces.Failure import viper.silicon.logger.SymbExLogger -import viper.silicon.reporting.condenseToViperResult +import viper.silicon.reporting.{MultiRunRecorders, condenseToViperResult} import viper.silicon.verifier.DefaultMasterVerifier -import viper.silicon.decider.{Z3ProverStdIO, Cvc5ProverStdIO} +import viper.silicon.decider.{Cvc5ProverStdIO, Z3ProverStdIO} import viper.silver.cfg.silver.SilverCfg import viper.silver.logger.ViperStdOutLogger + import scala.util.chaining._ object Silicon { @@ -178,7 +180,7 @@ class Silicon(val reporter: Reporter, private var debugInfo: Seq[(String, Any)] * TODO: Figure out what happens when ViperServer is used. */ config.file.foreach(filename => { if (filename != Silicon.dummyInputFilename && !config.ignoreFile.getOrElse(false)) { - //viper.silicon.verifier.Verifier.inputFile = Some(Paths.get(filename)) + MultiRunRecorders.source = Some(filename) } }) diff --git a/src/main/scala/reporting/MultiRunRecorder.scala b/src/main/scala/reporting/MultiRunRecorder.scala index 229db0eef..ac51df9d2 100644 --- a/src/main/scala/reporting/MultiRunRecorder.scala +++ b/src/main/scala/reporting/MultiRunRecorder.scala @@ -96,7 +96,7 @@ object MultiRunRecorders extends StatefulComponent { private val sinks = mutable.ArrayBuffer.empty[PrintWriter] protected def config: Config = Verifier.config - protected def source: Option[String] = ??? // Verifier.inputFile.map(_.toString) + var source: Option[String] = None protected def sink(name: String): PrintWriter = { val writer = From 4fe8ba3cc86db8be7511fa20f19ba9170c737516 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Mon, 22 Aug 2022 14:43:32 +0200 Subject: [PATCH 4/7] Cleanup --- silver | 2 +- src/main/scala/Silicon.scala | 22 ++++++++---------- .../BuiltinDomainsContributor.scala | 2 +- .../verifier/DefaultMasterVerifier.scala | 4 ++-- src/main/scala/verifier/Verifier.scala | 23 ------------------- src/test/scala/CounterexampleTests.scala | 3 ++- src/test/scala/PortableSiliconTests.scala | 5 ---- src/test/scala/SiliconTests.scala | 5 ---- src/test/scala/SymbExLoggerTests.scala | 5 ---- 9 files changed, 15 insertions(+), 56 deletions(-) diff --git a/silver b/silver index 918bafa77..ff430f7e6 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 918bafa770a88e1b488d9a93ad5eb250be41e983 +Subproject commit ff430f7e63b4a102369d9c89e594332df9248201 diff --git a/src/main/scala/Silicon.scala b/src/main/scala/Silicon.scala index dc07227fd..60fc38447 100644 --- a/src/main/scala/Silicon.scala +++ b/src/main/scala/Silicon.scala @@ -169,20 +169,16 @@ class Silicon(val reporter: Reporter, private var debugInfo: Seq[(String, Any)] logger.debug(s"$name started ${new SimpleDateFormat("yyyy-MM-dd HH:mm:ss z").format(System.currentTimeMillis())}") - /* If available, save the filename corresponding to the program under verification in Verifier.inputFile. - * See also src/test/scala/SiliconTests.scala, where the analogous happens if Silicon is executed while - * running the test suite. - * Do not save the filename if the filename corresponds to the dummy one or `--ignoreFile` has been specified. + /* Do not save the filename if the filename corresponds to the dummy one or `--ignoreFile` has been specified. * Clients assume that the filename is ignored if `--ignoreFile` is used but calling `Paths.get` on it effectively * tries to parse the given string as path. For example, the following string causes an exception on Windows (and * only on Windows): `_programID_d:\a\test` * * TODO: Figure out what happens when ViperServer is used. */ - config.file.foreach(filename => { - if (filename != Silicon.dummyInputFilename && !config.ignoreFile.getOrElse(false)) { - MultiRunRecorders.source = Some(filename) - } - }) + val inputFile: Option[String] = + if (config.file() != Silicon.dummyInputFilename && !config.ignoreFile.getOrElse(false)) Some(config.file()) + else None + MultiRunRecorders.source = inputFile // TODO: Check consistency of cfgs. val consistencyErrors = utils.consistency.check(program) @@ -194,7 +190,7 @@ class Silicon(val reporter: Reporter, private var debugInfo: Seq[(String, Any)] val executor = Executors.newSingleThreadExecutor() val future = executor.submit(new Callable[List[Failure]] { - def call(): List[Failure] = runVerifier(program, cfgs) + def call(): List[Failure] = runVerifier(program, cfgs, inputFile) }) try { @@ -237,11 +233,11 @@ class Silicon(val reporter: Reporter, private var debugInfo: Seq[(String, Any)] } } - private def runVerifier(program: ast.Program, cfgs: Seq[SilverCfg]): List[Failure] = { + private def runVerifier(program: ast.Program, cfgs: Seq[SilverCfg], inputFile: Option[String]): List[Failure] = { // verifier.bookkeeper.branches = 1 /*verifier.bookkeeper.*/startTime = System.currentTimeMillis() - val results = verifier.verify(program, cfgs) + val results = verifier.verify(program, cfgs, inputFile) /*verifier.bookkeeper.*/elapsedMillis = System.currentTimeMillis() - /*verifier.bookkeeper.*/startTime @@ -435,6 +431,6 @@ class SiliconRunnerInstance extends SiliconFrontend(StdIOReporter()) { */ } - //sys.exit(exitCode) + sys.exit(exitCode) } } diff --git a/src/main/scala/supporters/BuiltinDomainsContributor.scala b/src/main/scala/supporters/BuiltinDomainsContributor.scala index 892756d2a..cbf44c19a 100644 --- a/src/main/scala/supporters/BuiltinDomainsContributor.scala +++ b/src/main/scala/supporters/BuiltinDomainsContributor.scala @@ -206,7 +206,7 @@ private object utils { program case fastparse.Parsed.Failure(msg, index, _) => - val (line, col) = lc.apply(index) + val (line, col) = lc.getPos(index) sys.error(s"Failure: $msg, at ${viper.silver.ast.FilePosition(fromPath, line, col)}") //? val pos = extra.input.prettyIndex(index).split(":").map(_.toInt) //? sys.error(s"Failure: $msg, at ${viper.silver.ast.FilePosition(fromPath, pos(0), pos(1))}") diff --git a/src/main/scala/verifier/DefaultMasterVerifier.scala b/src/main/scala/verifier/DefaultMasterVerifier.scala index e0bd3bf64..d5c006366 100644 --- a/src/main/scala/verifier/DefaultMasterVerifier.scala +++ b/src/main/scala/verifier/DefaultMasterVerifier.scala @@ -135,7 +135,7 @@ class DefaultMasterVerifier(config: Config, override val reporter: Reporter) /* Program verification */ - def verify(originalProgram: ast.Program, cfgs: Seq[SilverCfg]): List[VerificationResult] = { + def verify(originalProgram: ast.Program, cfgs: Seq[SilverCfg], inputFile: Option[String]): List[VerificationResult] = { /** Trigger computation is currently not thread-safe; hence, all triggers are computed * up-front, before the program is verified in parallel. * This is done bottom-up to ensure that nested quantifiers are transformed as well @@ -165,7 +165,7 @@ class DefaultMasterVerifier(config: Config, override val reporter: Reporter) allProvers.comment("Started: " + new SimpleDateFormat("yyyy-MM-dd HH:mm:ss").format(System.currentTimeMillis()) /*bookkeeper.formattedStartTime*/) allProvers.comment("Silicon.version: " + Silicon.version) - //allProvers.comment(s"Input file: ${Verifier.inputFile.getOrElse("")}") + allProvers.comment(s"Input file: ${inputFile.getOrElse("")}") allProvers.comment(s"Verifier id: $uniqueId") allProvers.comment("-" * 60) allProvers.comment("Begin preamble") diff --git a/src/main/scala/verifier/Verifier.scala b/src/main/scala/verifier/Verifier.scala index c0ef4e64f..c3c2430e7 100644 --- a/src/main/scala/verifier/Verifier.scala +++ b/src/main/scala/verifier/Verifier.scala @@ -55,27 +55,4 @@ object Verifier { /*private*/ def config_=(config: Config): Unit = { _config = config } } -/* TODO: Replace getters and setters by public vars - TODO: Add a description to each var that explain when it is expected to be set */ -class VerifierState { - - private var _program: ast.Program = _ - def program: ast.Program = _program - /*private*/ def program_=(program: ast.Program): Unit = { _program = program } - - private var _inputFile: Option[Path] = None - def inputFile: Option[Path] = _inputFile - /*private*/ def inputFile_=(file: Option[Path]): Unit = { _inputFile = file } - - private var _predicateData: Map[ast.Predicate, PredicateData] = _ - def predicateData: Map[ast.Predicate, PredicateData] = _predicateData - /*private*/ def predicateData_=(predicateData: Map[ast.Predicate, PredicateData]): Unit = - { _predicateData = predicateData } - - private var _functionData: Map[ast.Function, FunctionData] = _ - def functionData: Map[ast.Function, FunctionData] = _functionData - /*private*/ def functionData_=(functionData: Map[ast.Function, FunctionData]): Unit = - { _functionData = functionData } -} - trait VerifierComponent { this: Verifier => } diff --git a/src/test/scala/CounterexampleTests.scala b/src/test/scala/CounterexampleTests.scala index 8dae07ff1..4fee83ac9 100644 --- a/src/test/scala/CounterexampleTests.scala +++ b/src/test/scala/CounterexampleTests.scala @@ -174,9 +174,10 @@ case class ExpectedCounterexampleAnnotation(id: OutputAnnotationId, file: Path, * same syntax as in Viper) */ class CounterexampleParser(fp: FastParser) { + import fp.{accessPred, eqExp} def expectedCounterexample[_: P]: P[ExpectedCounterexample] = - (Start ~ "(" ~ (fp.accessPred | fp.eqExp).rep(0, ",") ~ ")" ~ End) + (Start ~ "(" ~ (accessPred | eqExp).rep(0, ",") ~ ")" ~ End) .map(ExpectedCounterexample) } diff --git a/src/test/scala/PortableSiliconTests.scala b/src/test/scala/PortableSiliconTests.scala index 16813a870..235202a4e 100644 --- a/src/test/scala/PortableSiliconTests.scala +++ b/src/test/scala/PortableSiliconTests.scala @@ -97,11 +97,6 @@ class PortableSiliconTests extends SilSuite with StatisticalTestSuite { override def frontend(verifier: Verifier, files: Seq[Path]): SiliconFrontend = { require(files.length == 1, "tests should consist of exactly one file") - /* If needed, Silicon reads the filename of the program under verification from Verifier.inputFile. - When the test suite is executed (sbt test/testOnly), Verifier.inputFile is set here. When Silicon is - run from the command line, Verifier.inputFile is set in src/main/scala/Silicon.scala. */ - //viper.silicon.verifier.Verifier.inputFile = Some(files.head) - val fe = new SiliconFrontend(NoopReporter)//SiliconFrontendWithUnitTesting() fe.init(verifier) fe.reset(files.head) diff --git a/src/test/scala/SiliconTests.scala b/src/test/scala/SiliconTests.scala index 260745565..027bd3da2 100644 --- a/src/test/scala/SiliconTests.scala +++ b/src/test/scala/SiliconTests.scala @@ -28,11 +28,6 @@ class SiliconTests extends SilSuite { override def frontend(verifier: Verifier, files: Seq[Path]): SiliconFrontend = { require(files.length == 1, "tests should consist of exactly one file") - /* If needed, Silicon reads the filename of the program under verification from Verifier.inputFile. - When the test suite is executed (sbt test/testOnly), Verifier.inputFile is set here. When Silicon is - run from the command line, Verifier.inputFile is set in src/main/scala/Silicon.scala. */ - //viper.silicon.verifier.Verifier.inputFile = Some(files.head) - val fe = new SiliconFrontend(NoopReporter) fe.init(verifier) fe.reset(files.head) diff --git a/src/test/scala/SymbExLoggerTests.scala b/src/test/scala/SymbExLoggerTests.scala index 863dc52df..6601faf21 100644 --- a/src/test/scala/SymbExLoggerTests.scala +++ b/src/test/scala/SymbExLoggerTests.scala @@ -24,11 +24,6 @@ class SymbExLoggerTests extends SilSuite { override def frontend(verifier: Verifier, files: Seq[Path]): Frontend = { require(files.length == 1, "tests should consist of exactly one file") - /* If needed, Silicon reads the filename of the program under verification from Verifier.inputFile. - When the test suite is executed (sbt test/testOnly), Verifier.inputFile is set here. When Silicon is - run from the command line, Verifier.inputFile is set in src/main/scala/Silicon.scala. */ - //viper.silicon.verifier.Verifier.inputFile = Some(files.head) - // For Unit-Testing of the Symbolic Execution Logging, the name of the file // to be tested must be known, which is why it's passed here to the SymbExLogger-Object. // SymbExLogger.reset() cleans the logging object (only relevant for verifying multiple From 93c83e06705a4bd3132966f6e16e833092f69e17 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Mon, 22 Aug 2022 18:51:52 +0200 Subject: [PATCH 5/7] Fixed accidential infinite recursion --- .../scala/rules/QuantifiedChunkSupport.scala | 30 +++++++++---------- src/main/scala/state/Terms.scala | 12 ++++---- 2 files changed, 21 insertions(+), 21 deletions(-) diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala index d43466226..5455b41d0 100644 --- a/src/main/scala/rules/QuantifiedChunkSupport.scala +++ b/src/main/scala/rules/QuantifiedChunkSupport.scala @@ -493,8 +493,8 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { val valueDefinitions = relevantChunks map (chunk => { - val lookupSummary = ResourceLookup(resource, sm, Seq(qvar)) - val lookupChunk = ResourceLookup(resource, chunk.snapshotMap, Seq(qvar)) + val lookupSummary = ResourceLookup(resource, sm, Seq(qvar), s.program) + val lookupChunk = ResourceLookup(resource, chunk.snapshotMap, Seq(qvar), s.program) // This is justified even for vacuous predicates (e.g. with body "true") and wands because // qvar is the tuple of predicate arguments, and thus unrelated to the actual body @@ -518,8 +518,8 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { val resourceTriggerDefinition = Forall( qvar, - And(relevantChunks map (chunk => ResourceTriggerFunction(resource, chunk.snapshotMap, Seq(qvar)))), - Trigger(ResourceLookup(resource, sm, Seq(qvar))), + And(relevantChunks map (chunk => ResourceTriggerFunction(resource, chunk.snapshotMap, Seq(qvar), s.program))), + Trigger(ResourceLookup(resource, sm, Seq(qvar), s.program)), s"qp.psmResTrgDef${v.counter(this).next()}", isGlobal = true) @@ -538,7 +538,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { (sm, valueDefinitions :+ resourceTriggerDefinition, optDomainDefinition) } - private def summarisePerm(@unused s: State, + private def summarisePerm(s: State, relevantChunks: Seq[QuantifiedBasicChunk], codomainQVars: Seq[Var], resource: ast.Resource, @@ -548,7 +548,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { val pm = freshPermMap(resource, Seq(), v) - val permSummary = ResourcePermissionLookup(resource, pm, codomainQVars) + val permSummary = ResourcePermissionLookup(resource, pm, codomainQVars, s.program) val valueDefinitions = Forall( @@ -558,7 +558,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { s"qp.resPrmSumDef${v.counter(this).next()}", isGlobal = true) - val resourceTriggerFunction = ResourceTriggerFunction(resource, smDef.sm, codomainQVars) + val resourceTriggerFunction = ResourceTriggerFunction(resource, smDef.sm, codomainQVars, s.program) // TODO: Quantify over snapshot if resource is predicate. // Also check other places where a similar quantifier is constructed. @@ -567,8 +567,8 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { codomainQVars, And(resourceTriggerFunction +: relevantChunks.map(chunk => - ResourceTriggerFunction(resource, chunk.snapshotMap, codomainQVars))), - Trigger(ResourcePermissionLookup(resource, pm, codomainQVars)), + ResourceTriggerFunction(resource, chunk.snapshotMap, codomainQVars, s.program))), + Trigger(ResourcePermissionLookup(resource, pm, codomainQVars, s.program)), s"qp.resTrgDef${v.counter(this).next()}", isGlobal = true) @@ -608,7 +608,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { val additionalSmArgs = s.relevantQuantifiedVariables(arguments) val sm = freshSnapshotMap(s, resource, additionalSmArgs, v) - val smValueDef = ResourceLookup(resource, sm, arguments) === value + val smValueDef = ResourceLookup(resource, sm, arguments, s.program) === value (sm, smValueDef) } @@ -863,7 +863,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { val (smDef1, smCache1) = quantifiedChunkSupporter.summarisingSnapshotMap( s, resource, codomainVars, relevantChunks, v) - val trigger = ResourceTriggerFunction(resource, smDef1.sm, codomainVars) + val trigger = ResourceTriggerFunction(resource, smDef1.sm, codomainVars, s.program) val qvarsToInv = inv.qvarsToInversesOf(codomainVars) val condOfInv = tCond.replace(qvarsToInv) v.decider.assume(Forall(codomainVars, Implies(condOfInv, trigger), Trigger(inv.inversesOf(codomainVars)))) //effectiveTriggers map (t => Trigger(t.p map (_.replace(qvarsToInv)))))) @@ -997,7 +997,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { val receiverInjectivityCheck = quantifiedChunkSupporter.injectivityAxiom( qvars = qvars, - condition = And(tCond, ResourceTriggerFunction(resource, smDef1.sm, tArgs)), + condition = And(tCond, ResourceTriggerFunction(resource, smDef1.sm, tArgs, s.program)), perms = tPerm, arguments = tArgs, triggers = Nil, @@ -1015,7 +1015,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { v.decider.assume( Forall( formalQVars, - Implies(condOfInvOfLoc, ResourceTriggerFunction(resource, smDef1.sm, formalQVars)), + Implies(condOfInvOfLoc, ResourceTriggerFunction(resource, smDef1.sm, formalQVars, s.program)), Trigger(inverseFunctions.inversesOf(formalQVars)))) /* TODO: Try to unify the upcoming if/else-block, their code is rather similar */ @@ -1175,7 +1175,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { })((s4, optCh, v2) => optCh match { case Some(ch) => - val snap = ResourceLookup(resource, ch.snapshotMap, arguments).convert(sorts.Snap) + val snap = ResourceLookup(resource, ch.snapshotMap, arguments, s4.program).convert(sorts.Snap) Q(s4, s4.h, snap, v2) case _ => Q(s4, s4.h, v2.decider.fresh(sorts.Snap), v2) @@ -1209,7 +1209,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { v = v) val s2 = s1.copy(functionRecorder = s1.functionRecorder.recordFvfAndDomain(smDef1), smCache = smCache1) - val snap = ResourceLookup(resource, smDef1.sm, arguments).convert(sorts.Snap) + val snap = ResourceLookup(resource, smDef1.sm, arguments, s2.program).convert(sorts.Snap) Q(s2, h1, snap, v) case (Incomplete(_), _, _) => failure diff --git a/src/main/scala/state/Terms.scala b/src/main/scala/state/Terms.scala index dfa1adbc5..421d05e5a 100644 --- a/src/main/scala/state/Terms.scala +++ b/src/main/scala/state/Terms.scala @@ -1971,13 +1971,13 @@ object fromSnapTree extends ((Term, Int) => Seq[Term]) { } object ResourceTriggerFunction { - def apply(resource: ast.Resource, sm: Term, args: Seq[Term]): Term = { + def apply(resource: ast.Resource, sm: Term, args: Seq[Term], program: ast.Program): Term = { resource match { case f: ast.Field => assert(args.size == 1) apply(f, sm, args.head) case p: ast.Predicate => apply(p, sm, args) - case w: ast.MagicWand => apply(w, sm, args) + case w: ast.MagicWand => apply(w, sm, args, program) } } @@ -1995,13 +1995,13 @@ object ResourceTriggerFunction { } object ResourceLookup { - def apply(resource: ast.Resource, sm: Term, args: Seq[Term]): Term = { + def apply(resource: ast.Resource, sm: Term, args: Seq[Term], program: ast.Program): Term = { resource match { case f: ast.Field => assert(args.size == 1) apply(f, sm, args.head) case p: ast.Predicate => apply(p, sm, args) - case w: ast.MagicWand => apply(w, sm, args) + case w: ast.MagicWand => apply(w, sm, args, program) } } @@ -2019,13 +2019,13 @@ object ResourceLookup { } object ResourcePermissionLookup { - def apply(resource: ast.Resource, sm: Term, args: Seq[Term]): Term = { + def apply(resource: ast.Resource, sm: Term, args: Seq[Term], program: ast.Program): Term = { resource match { case f: ast.Field => assert(args.size == 1) apply(f, sm, args.head) case p: ast.Predicate => apply(p, sm, args) - case w: ast.MagicWand => apply(w, sm, args) + case w: ast.MagicWand => apply(w, sm, args, program) } } From d890110e4402f059e36a31960118602e78345b3a Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Thu, 1 Sep 2022 14:40:51 +0200 Subject: [PATCH 6/7] Changes after review --- .../scala/reporting/MultiRunRecorder.scala | 5 +++++ .../verifier/DefaultMasterVerifier.scala | 22 +++++++++++++------ 2 files changed, 20 insertions(+), 7 deletions(-) diff --git a/src/main/scala/reporting/MultiRunRecorder.scala b/src/main/scala/reporting/MultiRunRecorder.scala index ac51df9d2..f72f90207 100644 --- a/src/main/scala/reporting/MultiRunRecorder.scala +++ b/src/main/scala/reporting/MultiRunRecorder.scala @@ -96,6 +96,11 @@ object MultiRunRecorders extends StatefulComponent { private val sinks = mutable.ArrayBuffer.empty[PrintWriter] protected def config: Config = Verifier.config + + /** + The source is set by the Silicon verifier (in method [[viper.silicon.Silicon.verify]]) after parsing and type + checking but before consistency checks and verification. + */ var source: Option[String] = None protected def sink(name: String): PrintWriter = { diff --git a/src/main/scala/verifier/DefaultMasterVerifier.scala b/src/main/scala/verifier/DefaultMasterVerifier.scala index 4b07379f5..1120183af 100644 --- a/src/main/scala/verifier/DefaultMasterVerifier.scala +++ b/src/main/scala/verifier/DefaultMasterVerifier.scala @@ -271,13 +271,16 @@ class DefaultMasterVerifier(config: Config, override val reporter: Reporter) ++ methodVerificationResults) } - private def createInitialState(member: ast.Member, program: ast.Program, - functionData: Map[ast.Function, FunctionData], predicateData: Map[ast.Predicate, PredicateData]): State = { + private def createInitialState(member: ast.Member, + program: ast.Program, + functionData: Map[ast.Function, FunctionData], + predicateData: Map[ast.Predicate, PredicateData]): State = { val quantifiedFields = InsertionOrderedSet(ast.utility.QuantifiedPermissions.quantifiedFields(member, program)) val quantifiedPredicates = InsertionOrderedSet(ast.utility.QuantifiedPermissions.quantifiedPredicates(member, program)) val quantifiedMagicWands = InsertionOrderedSet(ast.utility.QuantifiedPermissions.quantifiedMagicWands(member, program)).map(MagicWandIdentifier(_, program)) - State(program=program, functionData = functionData, + State(program = program, + functionData = functionData, predicateData = predicateData, qpFields = quantifiedFields, qpPredicates = quantifiedPredicates, @@ -287,14 +290,19 @@ class DefaultMasterVerifier(config: Config, override val reporter: Reporter) isMethodVerification = member.isInstanceOf[ast.Member]) } - private def createInitialState(@unused cfg: SilverCfg, program: ast.Program, - functionData: Map[ast.Function, FunctionData], predicateData: Map[ast.Predicate, PredicateData]): State = { + private def createInitialState(@unused cfg: SilverCfg, + program: ast.Program, + functionData: Map[ast.Function, FunctionData], + predicateData: Map[ast.Predicate, PredicateData]): State = { val quantifiedFields = InsertionOrderedSet(program.fields) val quantifiedPredicates = InsertionOrderedSet(program.predicates) val quantifiedMagicWands = InsertionOrderedSet[MagicWandIdentifier]() // TODO: Implement support for quantified magic wands. - State(program=program, functionData = functionData, - predicateData = predicateData, qpFields = quantifiedFields, + State( + program = program, + functionData = functionData, + predicateData = predicateData, + qpFields = quantifiedFields, qpPredicates = quantifiedPredicates, qpMagicWands = quantifiedMagicWands, predicateSnapMap = predSnapGenerator.snapMap, From 6f278a47388dcb64fba90ab8d9df7f15a920c6ba Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Thu, 1 Sep 2022 14:58:39 +0200 Subject: [PATCH 7/7] Updated submodule --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index 186c3250f..fdcaed397 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 186c3250f2ae79e184db02db548e95a43c0fadb6 +Subproject commit fdcaed397a1deedf64d3e371b863fcb134818a66