diff --git a/Source/Directory.Build.props b/Source/Directory.Build.props index 42658918d..ec349a347 100644 --- a/Source/Directory.Build.props +++ b/Source/Directory.Build.props @@ -2,7 +2,7 @@ - 3.3.1 + 3.3.2 net6.0 false Boogie diff --git a/Source/ExecutionEngine/Caching/CachedVerificationResultInjector.cs b/Source/ExecutionEngine/Caching/CachedVerificationResultInjector.cs new file mode 100644 index 000000000..15d903ca8 --- /dev/null +++ b/Source/ExecutionEngine/Caching/CachedVerificationResultInjector.cs @@ -0,0 +1,313 @@ +using System; +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using System.Linq; +using VC; + +namespace Microsoft.Boogie; + +sealed class CachedVerificationResultInjector : StandardVisitor +{ + private ExecutionEngineOptions options; + readonly Program Program; + + // TODO(wuestholz): We should probably increase the threshold to something like 2 seconds. + static readonly double TimeThreshold = -1.0d; + Program programInCachedSnapshot; + Implementation currentImplementation; + int assumptionVariableCount; + int temporaryVariableCount; + + public static readonly CachedVerificationResultInjectorStatistics Statistics = + new CachedVerificationResultInjectorStatistics(); + + int FreshAssumptionVariableName + { + get { return assumptionVariableCount++; } + } + + int FreshTemporaryVariableName + { + get { return temporaryVariableCount++; } + } + + CachedVerificationResultInjector(ExecutionEngineOptions options, Program program) + { + Program = program; + this.options = options; + } + + public Implementation Inject(Implementation implementation, Program programInCachedSnapshot) + { + Contract.Requires(implementation != null && programInCachedSnapshot != null); + + this.programInCachedSnapshot = programInCachedSnapshot; + assumptionVariableCount = 0; + temporaryVariableCount = 0; + currentImplementation = implementation; + + #region Introduce explict assumption about the precondition. + + var oldProc = programInCachedSnapshot.FindProcedure(currentImplementation.Proc.Name); + if (oldProc != null + && oldProc.DependencyChecksum != currentImplementation.Proc.DependencyChecksum + && currentImplementation.ExplicitAssumptionAboutCachedPrecondition == null) + { + var axioms = new List(); + var after = new List(); + Expr assumedExpr = new LiteralExpr(Token.NoToken, false); + var canUseSpecs = DependencyCollector.CanExpressOldSpecs(oldProc, Program, true); + if (canUseSpecs && oldProc.SignatureEquals(options, currentImplementation.Proc)) + { + var always = Substituter.SubstitutionFromDictionary(currentImplementation.GetImplFormalMap(options), true, + currentImplementation.Proc); + var forOld = Substituter.SubstitutionFromDictionary(new Dictionary()); + var clauses = oldProc.Requires.Select(r => + Substituter.FunctionCallReresolvingApply(always, forOld, r.Condition, Program)); + var conj = Expr.And(clauses, true); + assumedExpr = conj != null + ? FunctionExtractor.Extract(conj, Program, axioms) + : new LiteralExpr(Token.NoToken, true); + } + + if (assumedExpr != null) + { + var lv = new LocalVariable(Token.NoToken, + new TypedIdent(Token.NoToken, string.Format("a##cached##{0}", FreshAssumptionVariableName), Type.Bool), + new QKeyValue(Token.NoToken, "assumption", new List(), null)); + currentImplementation.InjectAssumptionVariable(lv, !canUseSpecs); + var lhs = new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, lv)); + var rhs = LiteralExpr.And(new IdentifierExpr(Token.NoToken, lv), assumedExpr); + var assumed = new AssignCmd(currentImplementation.tok, new List {lhs}, new List {rhs}); + assumed.IrrelevantForChecksumComputation = true; + currentImplementation.ExplicitAssumptionAboutCachedPrecondition = assumed; + after.Add(assumed); + } + + if (options.TraceCachingForTesting || options.TraceCachingForBenchmarking) { + using var tokTxtWr = new TokenTextWriter("", options.OutputWriter, false, false, options); + var loc = currentImplementation.tok != null && currentImplementation.tok != Token.NoToken + ? string.Format("{0}({1},{2})", currentImplementation.tok.filename, currentImplementation.tok.line, + currentImplementation.tok.col) + : ""; + options.OutputWriter.WriteLine("Processing implementation {0} (at {1}):", currentImplementation.VerboseName, loc); + foreach (var a in axioms) + { + options.OutputWriter.Write(" >>> added axiom: "); + a.Expr.Emit(tokTxtWr); + options.OutputWriter.WriteLine(); + } + + foreach (var b in after) + { + options.OutputWriter.Write(" >>> added after assuming the current precondition: "); + b.Emit(tokTxtWr, 0); + } + } + } + + #endregion + + var result = VisitImplementation(currentImplementation); + currentImplementation = null; + this.programInCachedSnapshot = null; + return result; + } + + public static void Inject(ExecutionEngine engine, Program program, + IReadOnlyList implementations, string requestId, + string programId, out long[] cachingActionCounts) + { + var eai = new CachedVerificationResultInjector(engine.Options, program); + + cachingActionCounts = new long[Enum.GetNames(typeof(VC.ConditionGeneration.CachingAction)).Length]; + var run = new CachedVerificationResultInjectorRun + { + Start = DateTime.UtcNow, ImplementationCount = implementations.Count(), + CachingActionCounts = cachingActionCounts + }; + foreach (var impl in implementations) + { + var vr = engine.Cache.Lookup(impl, engine.Options.RunDiagnosticsOnTimeout, out var priority); + if (vr != null && vr.ProgramId == programId) + { + if (priority == Priority.LOW) + { + run.LowPriorityImplementationCount++; + } + else if (priority == Priority.MEDIUM) + { + run.MediumPriorityImplementationCount++; + } + else if (priority == Priority.HIGH) + { + run.HighPriorityImplementationCount++; + } + else if (priority == Priority.SKIP) + { + run.SkippedImplementationCount++; + } + + if (priority == Priority.LOW || priority == Priority.MEDIUM || engine.Options.VerifySnapshots >= 3) + { + if (TimeThreshold < vr.End.Subtract(vr.Start).TotalMilliseconds) + { + eai.SetErrorAndAssertionChecksumsInCachedSnapshot(impl, vr); + if (vr.ProgramId != null) + { + var p = engine.Cache.CachedProgram(vr.ProgramId); + if (p != null) + { + eai.Inject(impl, p); + run.TransformedImplementationCount++; + } + } + } + } + } + } + + run.End = DateTime.UtcNow; + Statistics.AddRun(requestId, run); + } + + private void SetErrorAndAssertionChecksumsInCachedSnapshot(Implementation implementation, + ImplementationRunResult result) + { + if (result.VcOutcome == VcOutcome.Errors && result.Errors != null && + result.Errors.Count < options.ErrorLimit) + { + implementation.SetErrorChecksumToCachedError(result.Errors.Select(cex => + new Tuple(cex.Checksum, cex.SugaredCmdChecksum, cex))); + implementation.AssertionChecksumsInCachedSnapshot = result.AssertionChecksums; + } + else if (result.VcOutcome == VcOutcome.Correct) + { + implementation.SetErrorChecksumToCachedError(new List>()); + implementation.AssertionChecksumsInCachedSnapshot = result.AssertionChecksums; + } + } + + public override Cmd VisitCallCmd(CallCmd node) + { + var result = base.VisitCallCmd(node); + + var oldProc = programInCachedSnapshot.FindProcedure(node.Proc.Name); + if (oldProc != null + && oldProc.DependencyChecksum != node.Proc.DependencyChecksum + && node.AssignedAssumptionVariable == null) + { + var before = new List(); + var beforePreconditionCheck = new List(); + var after = new List(); + var axioms = new List(); + Expr assumedExpr = new LiteralExpr(Token.NoToken, false); + // TODO(wuestholz): Try out two alternatives: only do this for low priority implementations or not at all. + var canUseSpecs = DependencyCollector.CanExpressOldSpecs(oldProc, Program); + if (canUseSpecs && oldProc.SignatureEquals(options, node.Proc)) + { + var desugaring = node.GetDesugaring(options); + Contract.Assert(desugaring != null); + var precond = node.CheckedPrecondition(oldProc, Program, e => FunctionExtractor.Extract(e, Program, axioms)); + if (precond != null) + { + var assume = new AssumeCmd(node.tok, precond, + new QKeyValue(Token.NoToken, "precondition_previous_snapshot", new List(), null)); + assume.IrrelevantForChecksumComputation = true; + beforePreconditionCheck.Add(assume); + } + + var unmods = node.UnmodifiedBefore(oldProc); + var eqs = new List(); + foreach (var unmod in unmods) + { + var oldUnmod = new LocalVariable(Token.NoToken, + new TypedIdent(Token.NoToken, string.Format("{0}##old##{1}", unmod.Name, FreshTemporaryVariableName), + unmod.Type)); + var lhs = new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, oldUnmod)); + var rhs = new IdentifierExpr(Token.NoToken, unmod.Decl); + var cmd = new AssignCmd(Token.NoToken, new List {lhs}, new List {rhs}); + cmd.IrrelevantForChecksumComputation = true; + before.Add(cmd); + var eq = LiteralExpr.Eq(new IdentifierExpr(Token.NoToken, oldUnmod), + new IdentifierExpr(Token.NoToken, unmod.Decl)); + eq.Type = Type.Bool; + eq.TypeParameters = SimpleTypeParamInstantiation.EMPTY; + eqs.Add(eq); + } + + var mods = node.ModifiedBefore(oldProc); + var oldSubst = new Dictionary(); + foreach (var mod in mods) + { + var oldMod = new LocalVariable(Token.NoToken, + new TypedIdent(Token.NoToken, string.Format("{0}##old##{1}", mod.Name, FreshTemporaryVariableName), + mod.Type)); + oldSubst[mod.Decl] = new IdentifierExpr(Token.NoToken, oldMod); + var lhs = new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, oldMod)); + var rhs = new IdentifierExpr(Token.NoToken, mod.Decl); + var cmd = new AssignCmd(Token.NoToken, new List {lhs}, new List {rhs}); + cmd.IrrelevantForChecksumComputation = true; + before.Add(cmd); + } + + assumedExpr = node.Postcondition(oldProc, eqs, oldSubst, Program, + e => FunctionExtractor.Extract(e, Program, axioms)); + if (assumedExpr == null) + { + assumedExpr = new LiteralExpr(Token.NoToken, true); + } + } + + if (assumedExpr != null) + { + var lv = new LocalVariable(Token.NoToken, + new TypedIdent(Token.NoToken, string.Format("a##cached##{0}", FreshAssumptionVariableName), Type.Bool), + new QKeyValue(Token.NoToken, "assumption", new List(), null)); + node.AssignedAssumptionVariable = lv; + currentImplementation.InjectAssumptionVariable(lv, !canUseSpecs); + var lhs = new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, lv)); + var rhs = LiteralExpr.And(new IdentifierExpr(Token.NoToken, lv), assumedExpr); + var assumed = new AssignCmd(node.tok, new List {lhs}, new List {rhs}); + assumed.IrrelevantForChecksumComputation = true; + after.Add(assumed); + } + + node.ExtendDesugaring(options, before, beforePreconditionCheck, after); + if (options.TraceCachingForTesting || options.TraceCachingForBenchmarking) { + using var tokTxtWr = new TokenTextWriter("", options.OutputWriter, false, false, options); + var loc = node.tok != null && node.tok != Token.NoToken + ? $"{node.tok.filename}({node.tok.line},{node.tok.col})" + : ""; + options.OutputWriter.WriteLine("Processing call to procedure {0} in implementation {1} (at {2}):", node.Proc.VerboseName, + currentImplementation.VerboseName, loc); + foreach (var a in axioms) + { + options.OutputWriter.Write(" >>> added axiom: "); + a.Expr.Emit(tokTxtWr); + options.OutputWriter.WriteLine(); + } + + foreach (var b in before) + { + options.OutputWriter.Write(" >>> added before: "); + b.Emit(tokTxtWr, 0); + } + + foreach (var b in beforePreconditionCheck) + { + options.OutputWriter.Write(" >>> added before precondition check: "); + b.Emit(tokTxtWr, 0); + } + + foreach (var a in after) + { + options.OutputWriter.Write(" >>> added after: "); + a.Emit(tokTxtWr, 0); + } + } + } + + return result; + } +} \ No newline at end of file diff --git a/Source/ExecutionEngine/Caching/CachedVerificationResultInjectorRun.cs b/Source/ExecutionEngine/Caching/CachedVerificationResultInjectorRun.cs new file mode 100644 index 000000000..c7d1e1b7a --- /dev/null +++ b/Source/ExecutionEngine/Caching/CachedVerificationResultInjectorRun.cs @@ -0,0 +1,24 @@ +using System; + +namespace Microsoft.Boogie; + +struct CachedVerificationResultInjectorRun +{ + public DateTime Start { get; internal set; } + + public DateTime End { get; internal set; } + + public int TransformedImplementationCount { get; internal set; } + + public int ImplementationCount { get; internal set; } + + public int SkippedImplementationCount { get; set; } + + public int LowPriorityImplementationCount { get; set; } + + public int MediumPriorityImplementationCount { get; set; } + + public int HighPriorityImplementationCount { get; set; } + + public long[] CachingActionCounts { get; set; } +} \ No newline at end of file diff --git a/Source/ExecutionEngine/Caching/CachedVerificationResultInjectorStatistics.cs b/Source/ExecutionEngine/Caching/CachedVerificationResultInjectorStatistics.cs new file mode 100644 index 000000000..a410b3763 --- /dev/null +++ b/Source/ExecutionEngine/Caching/CachedVerificationResultInjectorStatistics.cs @@ -0,0 +1,35 @@ +using System.Collections.Concurrent; +using System.IO; +using System.Linq; + +namespace Microsoft.Boogie; + +sealed class CachedVerificationResultInjectorStatistics +{ + ConcurrentDictionary runs = + new ConcurrentDictionary(); + + public bool AddRun(string requestId, CachedVerificationResultInjectorRun run) + { + return runs.TryAdd(requestId, run); + } + + public string Output(bool printTime = false) + { + var wr = new StringWriter(); + if (runs.Any()) + { + wr.WriteLine("Cached verification result injector statistics as CSV:"); + wr.WriteLine("Request ID, Transformed, Low, Medium, High, Skipped{0}", printTime ? ", Time (ms)" : ""); + foreach (var kv in runs.OrderBy(kv => ExecutionEngine.AutoRequestId(kv.Key))) + { + var t = printTime ? string.Format(", {0,8:F0}", kv.Value.End.Subtract(kv.Value.Start).TotalMilliseconds) : ""; + wr.WriteLine("{0,-19}, {1,3}, {2,3}, {3,3}, {4,3}, {5,3}{6}", kv.Key, kv.Value.TransformedImplementationCount, + kv.Value.LowPriorityImplementationCount, kv.Value.MediumPriorityImplementationCount, + kv.Value.HighPriorityImplementationCount, kv.Value.SkippedImplementationCount, t); + } + } + + return wr.ToString(); + } +} \ No newline at end of file diff --git a/Source/ExecutionEngine/Caching/DependencyCollector.cs b/Source/ExecutionEngine/Caching/DependencyCollector.cs new file mode 100644 index 000000000..650b7669a --- /dev/null +++ b/Source/ExecutionEngine/Caching/DependencyCollector.cs @@ -0,0 +1,155 @@ +using System; +using System.Diagnostics.Contracts; +using System.Linq; + +namespace Microsoft.Boogie; + +sealed class DependencyCollector : ReadOnlyVisitor +{ + private DeclWithFormals currentDeclaration; + private Axiom currentAxiom; + + public static void Collect(ExecutionEngineOptions options, Program program) + { + var start = DateTime.UtcNow; + + var dc = new DependencyCollector(); + dc.VisitProgram(program); + + var end = DateTime.UtcNow; + if (options.TraceCachingForDebugging) + { + options.OutputWriter.WriteLine("Collected dependencies within {0:F0} ms.", end.Subtract(start).TotalMilliseconds); + } + } + + public static bool CanExpressOldSpecs(Procedure oldProc, Program newProg, bool ignoreModifiesClauses = false) + { + Contract.Requires(oldProc != null && newProg != null); + + var funcs = newProg.Functions; + var globals = newProg.GlobalVariables; + return oldProc.DependenciesCollected + && (oldProc.FunctionDependencies == null || oldProc.FunctionDependencies.All(dep => + funcs.Any(f => f.Name == dep.Name && f.DependencyChecksum == dep.DependencyChecksum))) + && (ignoreModifiesClauses || oldProc.Modifies.All(m => globals.Any(g => g.Name == m.Name))); + } + + public override Procedure VisitProcedure(Procedure node) + { + currentDeclaration = node; + + foreach (var param in node.InParams) + { + if (param.TypedIdent != null && param.TypedIdent.WhereExpr != null) + { + VisitExpr(param.TypedIdent.WhereExpr); + } + } + + var result = base.VisitProcedure(node); + node.DependenciesCollected = true; + currentDeclaration = null; + return result; + } + + public override Implementation VisitImplementation(Implementation node) + { + currentDeclaration = node; + + foreach (var param in node.InParams) + { + if (param.TypedIdent != null && param.TypedIdent.WhereExpr != null) + { + VisitExpr(param.TypedIdent.WhereExpr); + } + } + + if (node.Proc != null) + { + node.AddProcedureDependency(node.Proc); + } + + var result = base.VisitImplementation(node); + node.DependenciesCollected = true; + currentDeclaration = null; + return result; + } + + public override Axiom VisitAxiom(Axiom node) + { + if (node.DependenciesCollected) + { + if (currentDeclaration != null && node.FunctionDependencies != null) + { + foreach (var f in node.FunctionDependencies) + { + currentDeclaration.AddFunctionDependency(f); + } + } + + return node; + } + + currentAxiom = node; + var result = base.VisitAxiom(node); + node.DependenciesCollected = true; + currentAxiom = null; + return result; + } + + public override Function VisitFunction(Function node) + { + currentDeclaration = node; + + if (node.DefinitionAxiom != null) + { + VisitAxiom(node.DefinitionAxiom); + } + + if (node.OtherDefinitionAxioms != null) + { + foreach (var a in node.OtherDefinitionAxioms) + { + if (a != node.DefinitionAxiom) + { + VisitAxiom(a); + } + } + } + + var result = base.VisitFunction(node); + node.DependenciesCollected = true; + currentDeclaration = null; + return result; + } + + public override Cmd VisitCallCmd(CallCmd node) + { + if (currentDeclaration != null) + { + currentDeclaration.AddProcedureDependency(node.Proc); + } + + return base.VisitCallCmd(node); + } + + public override Expr VisitNAryExpr(NAryExpr node) + { + var funCall = node.Fun as FunctionCall; + if (funCall != null) + { + if (currentDeclaration != null) + { + currentDeclaration.AddFunctionDependency(funCall.Func); + } + + if (currentAxiom != null) + { + currentAxiom.AddFunctionDependency(funCall.Func); + } + } + + return base.VisitNAryExpr(node); + } +} \ No newline at end of file diff --git a/Source/ExecutionEngine/Caching/EmptyVerificationResultCache.cs b/Source/ExecutionEngine/Caching/EmptyVerificationResultCache.cs new file mode 100644 index 000000000..84e393b0c --- /dev/null +++ b/Source/ExecutionEngine/Caching/EmptyVerificationResultCache.cs @@ -0,0 +1,26 @@ +#nullable enable +using System.Runtime.Caching; + +namespace Microsoft.Boogie; + +public class EmptyVerificationResultCache : IVerificationResultCache { + public Program? CachedProgram(string programId) { + return null; + } + + public void SetProgram(string programId, Program program, CacheItemPolicy policy) { + } + + public int VerificationPriority(Implementation implementation, bool runDiagnosticsOnTimeout) { + Lookup(implementation, runDiagnosticsOnTimeout, out var priority); + return priority; + } + + public ImplementationRunResult? Lookup(Implementation impl, bool runDiagnosticsOnTimeout, out int priority) { + priority = Priority.HIGH; + return null; + } + + public void Insert(Implementation implementation, ImplementationRunResult result) { + } +} \ No newline at end of file diff --git a/Source/ExecutionEngine/Caching/FunctionExtractor.cs b/Source/ExecutionEngine/Caching/FunctionExtractor.cs new file mode 100644 index 000000000..a2c7b634b --- /dev/null +++ b/Source/ExecutionEngine/Caching/FunctionExtractor.cs @@ -0,0 +1,85 @@ +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using System.Linq; + +namespace Microsoft.Boogie; + +sealed class FunctionExtractor : StandardVisitor +{ + readonly Dictionary Substitutions = new Dictionary(); + + public override Expr VisitIdentifierExpr(IdentifierExpr node) + { + if (node.Decl == null || !(node.Decl is LocalVariable || node.Decl is Formal || node.Decl is GlobalVariable)) + { + return node; + } + else + { + if (!Substitutions.TryGetValue(node.Decl, out var boundVar)) + { + boundVar = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, node.Name, node.Type)); + Substitutions[node.Decl] = boundVar; + } + + return new IdentifierExpr(node.tok, boundVar); + } + } + + public static Expr Extract(Expr expr, Program program, List axioms) + { + Contract.Requires(expr != null && program != null && !program.TopLevelDeclarationsAreFrozen && axioms != null); + + if (expr is LiteralExpr) + { + return expr; + } + + var extractor = new FunctionExtractor(); + + var body = extractor.VisitExpr(expr); + + var name = program.FreshExtractedFunctionName(); + var originalVars = extractor.Substitutions.Keys.ToList(); + var formalInArgs = originalVars.Select(v => new Formal(Token.NoToken, + new TypedIdent(Token.NoToken, extractor.Substitutions[v].Name, extractor.Substitutions[v].TypedIdent.Type), + true)).ToList(); + var formalOutArg = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, name + "$result$", expr.Type), false); + var func = new Function(Token.NoToken, name, formalInArgs, formalOutArg); + func.AddAttribute("never_pattern"); + + var boundVars = originalVars.Select(k => extractor.Substitutions[k]); + var axiomCall = new NAryExpr(Token.NoToken, new FunctionCall(func), + boundVars.Select(b => new IdentifierExpr(Token.NoToken, b)).ToList()); + axiomCall.Type = expr.Type; + axiomCall.TypeParameters = SimpleTypeParamInstantiation.EMPTY; + var eq = LiteralExpr.Eq(axiomCall, body); + eq.Type = body.Type; + eq.TypeParameters = SimpleTypeParamInstantiation.EMPTY; + if (0 < formalInArgs.Count) + { + var forallExpr = new ForallExpr(Token.NoToken, boundVars.ToList(), + new Trigger(Token.NoToken, true, new List {axiomCall}), eq); + body = forallExpr; + forallExpr.Attributes = new QKeyValue(Token.NoToken, "weight", + new List {new LiteralExpr(Token.NoToken, BaseTypes.BigNum.FromInt(30))}, null); + body.Type = Type.Bool; + } + else + { + body = eq; + } + + var axiom = new Axiom(Token.NoToken, body); + func.DefinitionAxiom = axiom; + program.AddTopLevelDeclaration(func); + program.AddTopLevelDeclaration(axiom); + axioms.Add(axiom); + + var call = new NAryExpr(Token.NoToken, new FunctionCall(func), + originalVars.Select(v => new IdentifierExpr(Token.NoToken, v)).ToList()); + call.Type = expr.Type; + call.TypeParameters = SimpleTypeParamInstantiation.EMPTY; + return call; + } +} \ No newline at end of file diff --git a/Source/ExecutionEngine/Caching/IVerificationResultCache.cs b/Source/ExecutionEngine/Caching/IVerificationResultCache.cs new file mode 100644 index 000000000..6858f34d0 --- /dev/null +++ b/Source/ExecutionEngine/Caching/IVerificationResultCache.cs @@ -0,0 +1,12 @@ +#nullable enable +using System.Runtime.Caching; + +namespace Microsoft.Boogie; + +public interface IVerificationResultCache { + Program? CachedProgram(string programId); + void SetProgram(string programId, Program program, CacheItemPolicy policy); + int VerificationPriority(Implementation implementation, bool runDiagnosticsOnTimeout); + ImplementationRunResult? Lookup(Implementation impl, bool runDiagnosticsOnTimeout, out int priority); + void Insert(Implementation implementation, ImplementationRunResult result); +} \ No newline at end of file diff --git a/Source/ExecutionEngine/Caching/OtherDefinitionAxiomsCollector.cs b/Source/ExecutionEngine/Caching/OtherDefinitionAxiomsCollector.cs new file mode 100644 index 000000000..a7a31e240 --- /dev/null +++ b/Source/ExecutionEngine/Caching/OtherDefinitionAxiomsCollector.cs @@ -0,0 +1,68 @@ +using System; +using System.Collections.Generic; + +namespace Microsoft.Boogie; + +sealed class OtherDefinitionAxiomsCollector : ReadOnlyVisitor +{ + private ExecutionEngineOptions options; + Axiom currentAxiom; + Trigger currentTrigger; + + public OtherDefinitionAxiomsCollector(ExecutionEngineOptions options) + { + this.options = options; + } + + public static void Collect(ExecutionEngineOptions options, IEnumerable axioms) + { + var start = DateTime.UtcNow; + + var v = new OtherDefinitionAxiomsCollector(options); + foreach (var a in axioms) + { + v.currentAxiom = a; + v.VisitExpr(a.Expr); + v.currentAxiom = null; + } + + var end = DateTime.UtcNow; + if (options.TraceCachingForDebugging) + { + options.OutputWriter.WriteLine("Collected other definition axioms within {0:F0} ms.", + end.Subtract(start).TotalMilliseconds); + } + } + + public override QuantifierExpr VisitQuantifierExpr(QuantifierExpr node) + { + currentTrigger = node.Triggers; + while (currentTrigger != null) + { + foreach (var e in currentTrigger.Tr) + { + VisitExpr(e); + } + + currentTrigger = currentTrigger.Next; + } + + return base.VisitQuantifierExpr(node); + } + + public override Expr VisitNAryExpr(NAryExpr node) + { + var funCall = node.Fun as FunctionCall; + if (funCall != null && funCall.Func != null && funCall.Func.Checksum != null && funCall.Func.Checksum != "stable") + { + if (funCall.ArgumentCount == 0 || currentTrigger != null) + { + // We found a function call within a trigger of a quantifier expression, or the function does not take any + // arguments so we don't expect it ever to sit inside a quantifier. + funCall.Func.OtherDefinitionAxioms.Add(currentAxiom); + } + } + + return base.VisitNAryExpr(node); + } +} \ No newline at end of file diff --git a/Source/ExecutionEngine/Caching/Priority.cs b/Source/ExecutionEngine/Caching/Priority.cs new file mode 100644 index 000000000..e6611e964 --- /dev/null +++ b/Source/ExecutionEngine/Caching/Priority.cs @@ -0,0 +1,9 @@ +namespace Microsoft.Boogie; + +internal static class Priority +{ + public static readonly int LOW = 1; // the same snapshot has been verified before, but a callee has changed + public static readonly int MEDIUM = 2; // old snapshot has been verified before + public static readonly int HIGH = 3; // has been never verified before + public static readonly int SKIP = int.MaxValue; // highest priority to get them done as soon as possible +} \ No newline at end of file diff --git a/Source/ExecutionEngine/Caching/VerificationResultCache.cs b/Source/ExecutionEngine/Caching/VerificationResultCache.cs new file mode 100644 index 000000000..91aaca841 --- /dev/null +++ b/Source/ExecutionEngine/Caching/VerificationResultCache.cs @@ -0,0 +1,86 @@ +#nullable enable +using System; +using System.Diagnostics.Contracts; +using System.Runtime.Caching; +using System.Text.RegularExpressions; +using VC; + +namespace Microsoft.Boogie +{ + public sealed class VerificationResultCache : IVerificationResultCache + { + private readonly MemoryCache programCache = new("ProgramCache"); + private readonly MemoryCache Cache = new("VerificationResultCache"); + + public Program? CachedProgram(string programId) { + return programCache.Get(programId) as Program; + } + + private readonly CacheItemPolicy Policy = new CacheItemPolicy + {SlidingExpiration = new TimeSpan(0, 10, 0), Priority = CacheItemPriority.Default}; + + public void Insert(Implementation impl, ImplementationRunResult result) + { + Contract.Requires(result != null); + Cache.Set(impl.Id, result, Policy); + } + + + public ImplementationRunResult? Lookup(Implementation impl, bool runDiagnosticsOnTimeout, out int priority) + { + var result = Cache.Get(impl.Id) as ImplementationRunResult; + if (result == null) + { + priority = Priority.HIGH; + } + else if (result.Checksum != impl.Checksum) + { + priority = Priority.MEDIUM; + } + else if (impl.DependencyChecksum == null || result.DependenciesChecksum != impl.DependencyChecksum) + { + priority = Priority.LOW; + } + else if (result.VcOutcome == VcOutcome.TimedOut && runDiagnosticsOnTimeout) + { + priority = Priority.MEDIUM; + } + else + { + priority = Priority.SKIP; + } + + return result; + } + + + public void Clear() + { + Cache.Trim(100); + } + + + public void RemoveMatchingKeys(Regex keyRegexp) + { + foreach (var kv in Cache) + { + if (keyRegexp.IsMatch(kv.Key)) + { + Cache.Remove(kv.Key); + } + } + } + + + public int VerificationPriority(Implementation impl, bool runDiagnosticsOnTimeout) + { + Lookup(impl, runDiagnosticsOnTimeout, out var priority); + return priority; + } + + public void SetProgram(string programId, Program program, CacheItemPolicy policy) + { + programCache.Set(programId, program, policy); + } + } +} \ No newline at end of file diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index f206c6612..72002036b 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -45,14 +45,14 @@ public static int AutoRequestId(string id) { return -1; } - public readonly VerificationResultCache Cache; + public readonly IVerificationResultCache Cache; static readonly CacheItemPolicy policy = new CacheItemPolicy { SlidingExpiration = new TimeSpan(0, 10, 0), Priority = CacheItemPriority.Default }; public const int StackSize = 16 * 1024 * 1024; - public ExecutionEngine(ExecutionEngineOptions options, VerificationResultCache cache, TaskScheduler scheduler, bool disposeScheduler = false) { + public ExecutionEngine(ExecutionEngineOptions options, IVerificationResultCache cache, TaskScheduler scheduler, bool disposeScheduler = false) { Options = options; Cache = cache; CheckerPool = new CheckerPool(options); diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs deleted file mode 100644 index 1385c03d6..000000000 --- a/Source/ExecutionEngine/VerificationResultCache.cs +++ /dev/null @@ -1,765 +0,0 @@ -using System; -using System.Collections.Concurrent; -using System.Collections.Generic; -using System.Diagnostics.Contracts; -using System.IO; -using System.Linq; -using System.Runtime.Caching; -using System.Text.RegularExpressions; -using VC; - -namespace Microsoft.Boogie -{ - struct CachedVerificationResultInjectorRun - { - public DateTime Start { get; internal set; } - - public DateTime End { get; internal set; } - - public int TransformedImplementationCount { get; internal set; } - - public int ImplementationCount { get; internal set; } - - public int SkippedImplementationCount { get; set; } - - public int LowPriorityImplementationCount { get; set; } - - public int MediumPriorityImplementationCount { get; set; } - - public int HighPriorityImplementationCount { get; set; } - - public long[] CachingActionCounts { get; set; } - } - - - sealed class CachedVerificationResultInjectorStatistics - { - ConcurrentDictionary runs = - new ConcurrentDictionary(); - - public bool AddRun(string requestId, CachedVerificationResultInjectorRun run) - { - return runs.TryAdd(requestId, run); - } - - public string Output(bool printTime = false) - { - var wr = new StringWriter(); - if (runs.Any()) - { - wr.WriteLine("Cached verification result injector statistics as CSV:"); - wr.WriteLine("Request ID, Transformed, Low, Medium, High, Skipped{0}", printTime ? ", Time (ms)" : ""); - foreach (var kv in runs.OrderBy(kv => ExecutionEngine.AutoRequestId(kv.Key))) - { - var t = printTime ? string.Format(", {0,8:F0}", kv.Value.End.Subtract(kv.Value.Start).TotalMilliseconds) : ""; - wr.WriteLine("{0,-19}, {1,3}, {2,3}, {3,3}, {4,3}, {5,3}{6}", kv.Key, kv.Value.TransformedImplementationCount, - kv.Value.LowPriorityImplementationCount, kv.Value.MediumPriorityImplementationCount, - kv.Value.HighPriorityImplementationCount, kv.Value.SkippedImplementationCount, t); - } - } - - return wr.ToString(); - } - } - - - sealed class CachedVerificationResultInjector : StandardVisitor - { - private ExecutionEngineOptions options; - readonly Program Program; - - // TODO(wuestholz): We should probably increase the threshold to something like 2 seconds. - static readonly double TimeThreshold = -1.0d; - Program programInCachedSnapshot; - Implementation currentImplementation; - int assumptionVariableCount; - int temporaryVariableCount; - - public static readonly CachedVerificationResultInjectorStatistics Statistics = - new CachedVerificationResultInjectorStatistics(); - - int FreshAssumptionVariableName - { - get { return assumptionVariableCount++; } - } - - int FreshTemporaryVariableName - { - get { return temporaryVariableCount++; } - } - - CachedVerificationResultInjector(ExecutionEngineOptions options, Program program) - { - Program = program; - this.options = options; - } - - public Implementation Inject(Implementation implementation, Program programInCachedSnapshot) - { - Contract.Requires(implementation != null && programInCachedSnapshot != null); - - this.programInCachedSnapshot = programInCachedSnapshot; - assumptionVariableCount = 0; - temporaryVariableCount = 0; - currentImplementation = implementation; - - #region Introduce explict assumption about the precondition. - - var oldProc = programInCachedSnapshot.FindProcedure(currentImplementation.Proc.Name); - if (oldProc != null - && oldProc.DependencyChecksum != currentImplementation.Proc.DependencyChecksum - && currentImplementation.ExplicitAssumptionAboutCachedPrecondition == null) - { - var axioms = new List(); - var after = new List(); - Expr assumedExpr = new LiteralExpr(Token.NoToken, false); - var canUseSpecs = DependencyCollector.CanExpressOldSpecs(oldProc, Program, true); - if (canUseSpecs && oldProc.SignatureEquals(options, currentImplementation.Proc)) - { - var always = Substituter.SubstitutionFromDictionary(currentImplementation.GetImplFormalMap(options), true, - currentImplementation.Proc); - var forOld = Substituter.SubstitutionFromDictionary(new Dictionary()); - var clauses = oldProc.Requires.Select(r => - Substituter.FunctionCallReresolvingApply(always, forOld, r.Condition, Program)); - var conj = Expr.And(clauses, true); - assumedExpr = conj != null - ? FunctionExtractor.Extract(conj, Program, axioms) - : new LiteralExpr(Token.NoToken, true); - } - - if (assumedExpr != null) - { - var lv = new LocalVariable(Token.NoToken, - new TypedIdent(Token.NoToken, string.Format("a##cached##{0}", FreshAssumptionVariableName), Type.Bool), - new QKeyValue(Token.NoToken, "assumption", new List(), null)); - currentImplementation.InjectAssumptionVariable(lv, !canUseSpecs); - var lhs = new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, lv)); - var rhs = LiteralExpr.And(new IdentifierExpr(Token.NoToken, lv), assumedExpr); - var assumed = new AssignCmd(currentImplementation.tok, new List {lhs}, new List {rhs}); - assumed.IrrelevantForChecksumComputation = true; - currentImplementation.ExplicitAssumptionAboutCachedPrecondition = assumed; - after.Add(assumed); - } - - if (options.TraceCachingForTesting || options.TraceCachingForBenchmarking) { - using var tokTxtWr = new TokenTextWriter("", options.OutputWriter, false, false, options); - var loc = currentImplementation.tok != null && currentImplementation.tok != Token.NoToken - ? string.Format("{0}({1},{2})", currentImplementation.tok.filename, currentImplementation.tok.line, - currentImplementation.tok.col) - : ""; - options.OutputWriter.WriteLine("Processing implementation {0} (at {1}):", currentImplementation.VerboseName, loc); - foreach (var a in axioms) - { - options.OutputWriter.Write(" >>> added axiom: "); - a.Expr.Emit(tokTxtWr); - options.OutputWriter.WriteLine(); - } - - foreach (var b in after) - { - options.OutputWriter.Write(" >>> added after assuming the current precondition: "); - b.Emit(tokTxtWr, 0); - } - } - } - - #endregion - - var result = VisitImplementation(currentImplementation); - currentImplementation = null; - this.programInCachedSnapshot = null; - return result; - } - - public static void Inject(ExecutionEngine engine, Program program, - IReadOnlyList implementations, string requestId, - string programId, out long[] cachingActionCounts) - { - var eai = new CachedVerificationResultInjector(engine.Options, program); - - cachingActionCounts = new long[Enum.GetNames(typeof(VC.ConditionGeneration.CachingAction)).Length]; - var run = new CachedVerificationResultInjectorRun - { - Start = DateTime.UtcNow, ImplementationCount = implementations.Count(), - CachingActionCounts = cachingActionCounts - }; - foreach (var impl in implementations) - { - var vr = engine.Cache.Lookup(impl, engine.Options.RunDiagnosticsOnTimeout, out var priority); - if (vr != null && vr.ProgramId == programId) - { - if (priority == Priority.LOW) - { - run.LowPriorityImplementationCount++; - } - else if (priority == Priority.MEDIUM) - { - run.MediumPriorityImplementationCount++; - } - else if (priority == Priority.HIGH) - { - run.HighPriorityImplementationCount++; - } - else if (priority == Priority.SKIP) - { - run.SkippedImplementationCount++; - } - - if (priority == Priority.LOW || priority == Priority.MEDIUM || engine.Options.VerifySnapshots >= 3) - { - if (TimeThreshold < vr.End.Subtract(vr.Start).TotalMilliseconds) - { - eai.SetErrorAndAssertionChecksumsInCachedSnapshot(impl, vr); - if (vr.ProgramId != null) - { - var p = engine.Cache.CachedProgram(vr.ProgramId); - if (p != null) - { - eai.Inject(impl, p); - run.TransformedImplementationCount++; - } - } - } - } - } - } - - run.End = DateTime.UtcNow; - Statistics.AddRun(requestId, run); - } - - private void SetErrorAndAssertionChecksumsInCachedSnapshot(Implementation implementation, - ImplementationRunResult result) - { - if (result.VcOutcome == VcOutcome.Errors && result.Errors != null && - result.Errors.Count < options.ErrorLimit) - { - implementation.SetErrorChecksumToCachedError(result.Errors.Select(cex => - new Tuple(cex.Checksum, cex.SugaredCmdChecksum, cex))); - implementation.AssertionChecksumsInCachedSnapshot = result.AssertionChecksums; - } - else if (result.VcOutcome == VcOutcome.Correct) - { - implementation.SetErrorChecksumToCachedError(new List>()); - implementation.AssertionChecksumsInCachedSnapshot = result.AssertionChecksums; - } - } - - public override Cmd VisitCallCmd(CallCmd node) - { - var result = base.VisitCallCmd(node); - - var oldProc = programInCachedSnapshot.FindProcedure(node.Proc.Name); - if (oldProc != null - && oldProc.DependencyChecksum != node.Proc.DependencyChecksum - && node.AssignedAssumptionVariable == null) - { - var before = new List(); - var beforePreconditionCheck = new List(); - var after = new List(); - var axioms = new List(); - Expr assumedExpr = new LiteralExpr(Token.NoToken, false); - // TODO(wuestholz): Try out two alternatives: only do this for low priority implementations or not at all. - var canUseSpecs = DependencyCollector.CanExpressOldSpecs(oldProc, Program); - if (canUseSpecs && oldProc.SignatureEquals(options, node.Proc)) - { - var desugaring = node.GetDesugaring(options); - Contract.Assert(desugaring != null); - var precond = node.CheckedPrecondition(oldProc, Program, e => FunctionExtractor.Extract(e, Program, axioms)); - if (precond != null) - { - var assume = new AssumeCmd(node.tok, precond, - new QKeyValue(Token.NoToken, "precondition_previous_snapshot", new List(), null)); - assume.IrrelevantForChecksumComputation = true; - beforePreconditionCheck.Add(assume); - } - - var unmods = node.UnmodifiedBefore(oldProc); - var eqs = new List(); - foreach (var unmod in unmods) - { - var oldUnmod = new LocalVariable(Token.NoToken, - new TypedIdent(Token.NoToken, string.Format("{0}##old##{1}", unmod.Name, FreshTemporaryVariableName), - unmod.Type)); - var lhs = new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, oldUnmod)); - var rhs = new IdentifierExpr(Token.NoToken, unmod.Decl); - var cmd = new AssignCmd(Token.NoToken, new List {lhs}, new List {rhs}); - cmd.IrrelevantForChecksumComputation = true; - before.Add(cmd); - var eq = LiteralExpr.Eq(new IdentifierExpr(Token.NoToken, oldUnmod), - new IdentifierExpr(Token.NoToken, unmod.Decl)); - eq.Type = Type.Bool; - eq.TypeParameters = SimpleTypeParamInstantiation.EMPTY; - eqs.Add(eq); - } - - var mods = node.ModifiedBefore(oldProc); - var oldSubst = new Dictionary(); - foreach (var mod in mods) - { - var oldMod = new LocalVariable(Token.NoToken, - new TypedIdent(Token.NoToken, string.Format("{0}##old##{1}", mod.Name, FreshTemporaryVariableName), - mod.Type)); - oldSubst[mod.Decl] = new IdentifierExpr(Token.NoToken, oldMod); - var lhs = new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, oldMod)); - var rhs = new IdentifierExpr(Token.NoToken, mod.Decl); - var cmd = new AssignCmd(Token.NoToken, new List {lhs}, new List {rhs}); - cmd.IrrelevantForChecksumComputation = true; - before.Add(cmd); - } - - assumedExpr = node.Postcondition(oldProc, eqs, oldSubst, Program, - e => FunctionExtractor.Extract(e, Program, axioms)); - if (assumedExpr == null) - { - assumedExpr = new LiteralExpr(Token.NoToken, true); - } - } - - if (assumedExpr != null) - { - var lv = new LocalVariable(Token.NoToken, - new TypedIdent(Token.NoToken, string.Format("a##cached##{0}", FreshAssumptionVariableName), Type.Bool), - new QKeyValue(Token.NoToken, "assumption", new List(), null)); - node.AssignedAssumptionVariable = lv; - currentImplementation.InjectAssumptionVariable(lv, !canUseSpecs); - var lhs = new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, lv)); - var rhs = LiteralExpr.And(new IdentifierExpr(Token.NoToken, lv), assumedExpr); - var assumed = new AssignCmd(node.tok, new List {lhs}, new List {rhs}); - assumed.IrrelevantForChecksumComputation = true; - after.Add(assumed); - } - - node.ExtendDesugaring(options, before, beforePreconditionCheck, after); - if (options.TraceCachingForTesting || options.TraceCachingForBenchmarking) { - using var tokTxtWr = new TokenTextWriter("", options.OutputWriter, false, false, options); - var loc = node.tok != null && node.tok != Token.NoToken - ? $"{node.tok.filename}({node.tok.line},{node.tok.col})" - : ""; - options.OutputWriter.WriteLine("Processing call to procedure {0} in implementation {1} (at {2}):", node.Proc.VerboseName, - currentImplementation.VerboseName, loc); - foreach (var a in axioms) - { - options.OutputWriter.Write(" >>> added axiom: "); - a.Expr.Emit(tokTxtWr); - options.OutputWriter.WriteLine(); - } - - foreach (var b in before) - { - options.OutputWriter.Write(" >>> added before: "); - b.Emit(tokTxtWr, 0); - } - - foreach (var b in beforePreconditionCheck) - { - options.OutputWriter.Write(" >>> added before precondition check: "); - b.Emit(tokTxtWr, 0); - } - - foreach (var a in after) - { - options.OutputWriter.Write(" >>> added after: "); - a.Emit(tokTxtWr, 0); - } - } - } - - return result; - } - } - - - sealed class FunctionExtractor : StandardVisitor - { - readonly Dictionary Substitutions = new Dictionary(); - - public override Expr VisitIdentifierExpr(IdentifierExpr node) - { - if (node.Decl == null || !(node.Decl is LocalVariable || node.Decl is Formal || node.Decl is GlobalVariable)) - { - return node; - } - else - { - if (!Substitutions.TryGetValue(node.Decl, out var boundVar)) - { - boundVar = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, node.Name, node.Type)); - Substitutions[node.Decl] = boundVar; - } - - return new IdentifierExpr(node.tok, boundVar); - } - } - - public static Expr Extract(Expr expr, Program program, List axioms) - { - Contract.Requires(expr != null && program != null && !program.TopLevelDeclarationsAreFrozen && axioms != null); - - if (expr is LiteralExpr) - { - return expr; - } - - var extractor = new FunctionExtractor(); - - var body = extractor.VisitExpr(expr); - - var name = program.FreshExtractedFunctionName(); - var originalVars = extractor.Substitutions.Keys.ToList(); - var formalInArgs = originalVars.Select(v => new Formal(Token.NoToken, - new TypedIdent(Token.NoToken, extractor.Substitutions[v].Name, extractor.Substitutions[v].TypedIdent.Type), - true)).ToList(); - var formalOutArg = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, name + "$result$", expr.Type), false); - var func = new Function(Token.NoToken, name, formalInArgs, formalOutArg); - func.AddAttribute("never_pattern"); - - var boundVars = originalVars.Select(k => extractor.Substitutions[k]); - var axiomCall = new NAryExpr(Token.NoToken, new FunctionCall(func), - boundVars.Select(b => new IdentifierExpr(Token.NoToken, b)).ToList()); - axiomCall.Type = expr.Type; - axiomCall.TypeParameters = SimpleTypeParamInstantiation.EMPTY; - var eq = LiteralExpr.Eq(axiomCall, body); - eq.Type = body.Type; - eq.TypeParameters = SimpleTypeParamInstantiation.EMPTY; - if (0 < formalInArgs.Count) - { - var forallExpr = new ForallExpr(Token.NoToken, boundVars.ToList(), - new Trigger(Token.NoToken, true, new List {axiomCall}), eq); - body = forallExpr; - forallExpr.Attributes = new QKeyValue(Token.NoToken, "weight", - new List {new LiteralExpr(Token.NoToken, BaseTypes.BigNum.FromInt(30))}, null); - body.Type = Type.Bool; - } - else - { - body = eq; - } - - var axiom = new Axiom(Token.NoToken, body); - func.DefinitionAxiom = axiom; - program.AddTopLevelDeclaration(func); - program.AddTopLevelDeclaration(axiom); - axioms.Add(axiom); - - var call = new NAryExpr(Token.NoToken, new FunctionCall(func), - originalVars.Select(v => new IdentifierExpr(Token.NoToken, v)).ToList()); - call.Type = expr.Type; - call.TypeParameters = SimpleTypeParamInstantiation.EMPTY; - return call; - } - } - - - sealed class OtherDefinitionAxiomsCollector : ReadOnlyVisitor - { - private ExecutionEngineOptions options; - Axiom currentAxiom; - Trigger currentTrigger; - - public OtherDefinitionAxiomsCollector(ExecutionEngineOptions options) - { - this.options = options; - } - - public static void Collect(ExecutionEngineOptions options, IEnumerable axioms) - { - var start = DateTime.UtcNow; - - var v = new OtherDefinitionAxiomsCollector(options); - foreach (var a in axioms) - { - v.currentAxiom = a; - v.VisitExpr(a.Expr); - v.currentAxiom = null; - } - - var end = DateTime.UtcNow; - if (options.TraceCachingForDebugging) - { - options.OutputWriter.WriteLine("Collected other definition axioms within {0:F0} ms.", - end.Subtract(start).TotalMilliseconds); - } - } - - public override QuantifierExpr VisitQuantifierExpr(QuantifierExpr node) - { - currentTrigger = node.Triggers; - while (currentTrigger != null) - { - foreach (var e in currentTrigger.Tr) - { - VisitExpr(e); - } - - currentTrigger = currentTrigger.Next; - } - - return base.VisitQuantifierExpr(node); - } - - public override Expr VisitNAryExpr(NAryExpr node) - { - var funCall = node.Fun as FunctionCall; - if (funCall != null && funCall.Func != null && funCall.Func.Checksum != null && funCall.Func.Checksum != "stable") - { - if (funCall.ArgumentCount == 0 || currentTrigger != null) - { - // We found a function call within a trigger of a quantifier expression, or the function does not take any - // arguments so we don't expect it ever to sit inside a quantifier. - funCall.Func.OtherDefinitionAxioms.Add(currentAxiom); - } - } - - return base.VisitNAryExpr(node); - } - } - - - sealed class DependencyCollector : ReadOnlyVisitor - { - private DeclWithFormals currentDeclaration; - private Axiom currentAxiom; - - public static void Collect(ExecutionEngineOptions options, Program program) - { - var start = DateTime.UtcNow; - - var dc = new DependencyCollector(); - dc.VisitProgram(program); - - var end = DateTime.UtcNow; - if (options.TraceCachingForDebugging) - { - options.OutputWriter.WriteLine("Collected dependencies within {0:F0} ms.", end.Subtract(start).TotalMilliseconds); - } - } - - public static bool CanExpressOldSpecs(Procedure oldProc, Program newProg, bool ignoreModifiesClauses = false) - { - Contract.Requires(oldProc != null && newProg != null); - - var funcs = newProg.Functions; - var globals = newProg.GlobalVariables; - return oldProc.DependenciesCollected - && (oldProc.FunctionDependencies == null || oldProc.FunctionDependencies.All(dep => - funcs.Any(f => f.Name == dep.Name && f.DependencyChecksum == dep.DependencyChecksum))) - && (ignoreModifiesClauses || oldProc.Modifies.All(m => globals.Any(g => g.Name == m.Name))); - } - - public override Procedure VisitProcedure(Procedure node) - { - currentDeclaration = node; - - foreach (var param in node.InParams) - { - if (param.TypedIdent != null && param.TypedIdent.WhereExpr != null) - { - VisitExpr(param.TypedIdent.WhereExpr); - } - } - - var result = base.VisitProcedure(node); - node.DependenciesCollected = true; - currentDeclaration = null; - return result; - } - - public override Implementation VisitImplementation(Implementation node) - { - currentDeclaration = node; - - foreach (var param in node.InParams) - { - if (param.TypedIdent != null && param.TypedIdent.WhereExpr != null) - { - VisitExpr(param.TypedIdent.WhereExpr); - } - } - - if (node.Proc != null) - { - node.AddProcedureDependency(node.Proc); - } - - var result = base.VisitImplementation(node); - node.DependenciesCollected = true; - currentDeclaration = null; - return result; - } - - public override Axiom VisitAxiom(Axiom node) - { - if (node.DependenciesCollected) - { - if (currentDeclaration != null && node.FunctionDependencies != null) - { - foreach (var f in node.FunctionDependencies) - { - currentDeclaration.AddFunctionDependency(f); - } - } - - return node; - } - - currentAxiom = node; - var result = base.VisitAxiom(node); - node.DependenciesCollected = true; - currentAxiom = null; - return result; - } - - public override Function VisitFunction(Function node) - { - currentDeclaration = node; - - if (node.DefinitionAxiom != null) - { - VisitAxiom(node.DefinitionAxiom); - } - - if (node.OtherDefinitionAxioms != null) - { - foreach (var a in node.OtherDefinitionAxioms) - { - if (a != node.DefinitionAxiom) - { - VisitAxiom(a); - } - } - } - - var result = base.VisitFunction(node); - node.DependenciesCollected = true; - currentDeclaration = null; - return result; - } - - public override Cmd VisitCallCmd(CallCmd node) - { - if (currentDeclaration != null) - { - currentDeclaration.AddProcedureDependency(node.Proc); - } - - return base.VisitCallCmd(node); - } - - public override Expr VisitNAryExpr(NAryExpr node) - { - var funCall = node.Fun as FunctionCall; - if (funCall != null) - { - if (currentDeclaration != null) - { - currentDeclaration.AddFunctionDependency(funCall.Func); - } - - if (currentAxiom != null) - { - currentAxiom.AddFunctionDependency(funCall.Func); - } - } - - return base.VisitNAryExpr(node); - } - } - - - static internal class Priority - { - public static readonly int LOW = 1; // the same snapshot has been verified before, but a callee has changed - public static readonly int MEDIUM = 2; // old snapshot has been verified before - public static readonly int HIGH = 3; // has been never verified before - public static readonly int SKIP = int.MaxValue; // highest priority to get them done as soon as possible - } - - - public sealed class VerificationResultCache - { - - private readonly MemoryCache programCache = new("ProgramCache"); - private readonly MemoryCache Cache = new("VerificationResultCache"); - - public Program CachedProgram(string programId) { - var result = programCache.Get(programId) as Program; - return result; - } - - private readonly CacheItemPolicy Policy = new CacheItemPolicy - {SlidingExpiration = new TimeSpan(0, 10, 0), Priority = CacheItemPriority.Default}; - - public void Insert(Implementation impl, ImplementationRunResult result) - { - Contract.Requires(impl != null); - Contract.Requires(result != null); - - Cache.Set(impl.Id, result, Policy); - } - - - public ImplementationRunResult Lookup(Implementation impl, bool runDiagnosticsOnTimeout, out int priority) - { - Contract.Requires(impl != null); - - var result = Cache.Get(impl.Id) as ImplementationRunResult; - if (result == null) - { - priority = Priority.HIGH; - } - else if (result.Checksum != impl.Checksum) - { - priority = Priority.MEDIUM; - } - else if (impl.DependencyChecksum == null || result.DependenciesChecksum != impl.DependencyChecksum) - { - priority = Priority.LOW; - } - else if (result.VcOutcome == VcOutcome.TimedOut && runDiagnosticsOnTimeout) - { - priority = Priority.MEDIUM; - } - else - { - priority = Priority.SKIP; - } - - return result; - } - - - public void Clear() - { - Cache.Trim(100); - } - - - public void RemoveMatchingKeys(Regex keyRegexp) - { - Contract.Requires(keyRegexp != null); - - foreach (var kv in Cache) - { - if (keyRegexp.IsMatch(kv.Key)) - { - Cache.Remove(kv.Key); - } - } - } - - - public int VerificationPriority(Implementation impl, bool runDiagnosticsOnTimeout) - { - Contract.Requires(impl != null); - - Lookup(impl, runDiagnosticsOnTimeout, out var priority); - return priority; - } - - public void SetProgram(string programId, Program program, CacheItemPolicy policy) - { - programCache.Set(programId, program, policy); - } - } -} \ No newline at end of file