Skip to content

Commit 398413d

Browse files
keyboardDrummerkeyboardDrummer
authored
No cache (#964)
### Changes - Enable not using a verification result cache, using the new class `EmptyVerificationResultCache` ### Testing - Manually tried out using EmptyVerificationResultCache in Dafny, which reduces memory pressure
1 parent 5f94789 commit 398413d

13 files changed

+816
-768
lines changed

‎Source/Directory.Build.props

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22

33
<!-- Target framework and package configuration -->
44
<PropertyGroup>
5-
<Version>3.3.1</Version>
5+
<Version>3.3.2</Version>
66
<TargetFramework>net6.0</TargetFramework>
77
<GeneratePackageOnBuild>false</GeneratePackageOnBuild>
88
<Authors>Boogie</Authors>

‎Source/ExecutionEngine/Caching/CachedVerificationResultInjector.cs

Lines changed: 313 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,313 @@
1+
using System;
2+
using System.Collections.Generic;
3+
using System.Diagnostics.Contracts;
4+
using System.Linq;
5+
using VC;
6+
7+
namespace Microsoft.Boogie;
8+
9+
sealed class CachedVerificationResultInjector : StandardVisitor
10+
{
11+
private ExecutionEngineOptions options;
12+
readonly Program Program;
13+
14+
// TODO(wuestholz): We should probably increase the threshold to something like 2 seconds.
15+
static readonly double TimeThreshold = -1.0d;
16+
Program programInCachedSnapshot;
17+
Implementation currentImplementation;
18+
int assumptionVariableCount;
19+
int temporaryVariableCount;
20+
21+
public static readonly CachedVerificationResultInjectorStatistics Statistics =
22+
new CachedVerificationResultInjectorStatistics();
23+
24+
int FreshAssumptionVariableName
25+
{
26+
get { return assumptionVariableCount++; }
27+
}
28+
29+
int FreshTemporaryVariableName
30+
{
31+
get { return temporaryVariableCount++; }
32+
}
33+
34+
CachedVerificationResultInjector(ExecutionEngineOptions options, Program program)
35+
{
36+
Program = program;
37+
this.options = options;
38+
}
39+
40+
public Implementation Inject(Implementation implementation, Program programInCachedSnapshot)
41+
{
42+
Contract.Requires(implementation != null && programInCachedSnapshot != null);
43+
44+
this.programInCachedSnapshot = programInCachedSnapshot;
45+
assumptionVariableCount = 0;
46+
temporaryVariableCount = 0;
47+
currentImplementation = implementation;
48+
49+
#region Introduce explict assumption about the precondition.
50+
51+
var oldProc = programInCachedSnapshot.FindProcedure(currentImplementation.Proc.Name);
52+
if (oldProc != null
53+
&& oldProc.DependencyChecksum != currentImplementation.Proc.DependencyChecksum
54+
&& currentImplementation.ExplicitAssumptionAboutCachedPrecondition == null)
55+
{
56+
var axioms = new List<Axiom>();
57+
var after = new List<Cmd>();
58+
Expr assumedExpr = new LiteralExpr(Token.NoToken, false);
59+
var canUseSpecs = DependencyCollector.CanExpressOldSpecs(oldProc, Program, true);
60+
if (canUseSpecs && oldProc.SignatureEquals(options, currentImplementation.Proc))
61+
{
62+
var always = Substituter.SubstitutionFromDictionary(currentImplementation.GetImplFormalMap(options), true,
63+
currentImplementation.Proc);
64+
var forOld = Substituter.SubstitutionFromDictionary(new Dictionary<Variable, Expr>());
65+
var clauses = oldProc.Requires.Select(r =>
66+
Substituter.FunctionCallReresolvingApply(always, forOld, r.Condition, Program));
67+
var conj = Expr.And(clauses, true);
68+
assumedExpr = conj != null
69+
? FunctionExtractor.Extract(conj, Program, axioms)
70+
: new LiteralExpr(Token.NoToken, true);
71+
}
72+
73+
if (assumedExpr != null)
74+
{
75+
var lv = new LocalVariable(Token.NoToken,
76+
new TypedIdent(Token.NoToken, string.Format("a##cached##{0}", FreshAssumptionVariableName), Type.Bool),
77+
new QKeyValue(Token.NoToken, "assumption", new List<object>(), null));
78+
currentImplementation.InjectAssumptionVariable(lv, !canUseSpecs);
79+
var lhs = new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, lv));
80+
var rhs = LiteralExpr.And(new IdentifierExpr(Token.NoToken, lv), assumedExpr);
81+
var assumed = new AssignCmd(currentImplementation.tok, new List<AssignLhs> {lhs}, new List<Expr> {rhs});
82+
assumed.IrrelevantForChecksumComputation = true;
83+
currentImplementation.ExplicitAssumptionAboutCachedPrecondition = assumed;
84+
after.Add(assumed);
85+
}
86+
87+
if (options.TraceCachingForTesting || options.TraceCachingForBenchmarking) {
88+
using var tokTxtWr = new TokenTextWriter("<console>", options.OutputWriter, false, false, options);
89+
var loc = currentImplementation.tok != null && currentImplementation.tok != Token.NoToken
90+
? string.Format("{0}({1},{2})", currentImplementation.tok.filename, currentImplementation.tok.line,
91+
currentImplementation.tok.col)
92+
: "<unknown location>";
93+
options.OutputWriter.WriteLine("Processing implementation {0} (at {1}):", currentImplementation.VerboseName, loc);
94+
foreach (var a in axioms)
95+
{
96+
options.OutputWriter.Write(" >>> added axiom: ");
97+
a.Expr.Emit(tokTxtWr);
98+
options.OutputWriter.WriteLine();
99+
}
100+
101+
foreach (var b in after)
102+
{
103+
options.OutputWriter.Write(" >>> added after assuming the current precondition: ");
104+
b.Emit(tokTxtWr, 0);
105+
}
106+
}
107+
}
108+
109+
#endregion
110+
111+
var result = VisitImplementation(currentImplementation);
112+
currentImplementation = null;
113+
this.programInCachedSnapshot = null;
114+
return result;
115+
}
116+
117+
public static void Inject(ExecutionEngine engine, Program program,
118+
IReadOnlyList<Implementation> implementations, string requestId,
119+
string programId, out long[] cachingActionCounts)
120+
{
121+
var eai = new CachedVerificationResultInjector(engine.Options, program);
122+
123+
cachingActionCounts = new long[Enum.GetNames(typeof(VC.ConditionGeneration.CachingAction)).Length];
124+
var run = new CachedVerificationResultInjectorRun
125+
{
126+
Start = DateTime.UtcNow, ImplementationCount = implementations.Count(),
127+
CachingActionCounts = cachingActionCounts
128+
};
129+
foreach (var impl in implementations)
130+
{
131+
var vr = engine.Cache.Lookup(impl, engine.Options.RunDiagnosticsOnTimeout, out var priority);
132+
if (vr != null && vr.ProgramId == programId)
133+
{
134+
if (priority == Priority.LOW)
135+
{
136+
run.LowPriorityImplementationCount++;
137+
}
138+
else if (priority == Priority.MEDIUM)
139+
{
140+
run.MediumPriorityImplementationCount++;
141+
}
142+
else if (priority == Priority.HIGH)
143+
{
144+
run.HighPriorityImplementationCount++;
145+
}
146+
else if (priority == Priority.SKIP)
147+
{
148+
run.SkippedImplementationCount++;
149+
}
150+
151+
if (priority == Priority.LOW || priority == Priority.MEDIUM || engine.Options.VerifySnapshots >= 3)
152+
{
153+
if (TimeThreshold < vr.End.Subtract(vr.Start).TotalMilliseconds)
154+
{
155+
eai.SetErrorAndAssertionChecksumsInCachedSnapshot(impl, vr);
156+
if (vr.ProgramId != null)
157+
{
158+
var p = engine.Cache.CachedProgram(vr.ProgramId);
159+
if (p != null)
160+
{
161+
eai.Inject(impl, p);
162+
run.TransformedImplementationCount++;
163+
}
164+
}
165+
}
166+
}
167+
}
168+
}
169+
170+
run.End = DateTime.UtcNow;
171+
Statistics.AddRun(requestId, run);
172+
}
173+
174+
private void SetErrorAndAssertionChecksumsInCachedSnapshot(Implementation implementation,
175+
ImplementationRunResult result)
176+
{
177+
if (result.VcOutcome == VcOutcome.Errors && result.Errors != null &&
178+
result.Errors.Count < options.ErrorLimit)
179+
{
180+
implementation.SetErrorChecksumToCachedError(result.Errors.Select(cex =>
181+
new Tuple<byte[], byte[], object>(cex.Checksum, cex.SugaredCmdChecksum, cex)));
182+
implementation.AssertionChecksumsInCachedSnapshot = result.AssertionChecksums;
183+
}
184+
else if (result.VcOutcome == VcOutcome.Correct)
185+
{
186+
implementation.SetErrorChecksumToCachedError(new List<Tuple<byte[], byte[], object>>());
187+
implementation.AssertionChecksumsInCachedSnapshot = result.AssertionChecksums;
188+
}
189+
}
190+
191+
public override Cmd VisitCallCmd(CallCmd node)
192+
{
193+
var result = base.VisitCallCmd(node);
194+
195+
var oldProc = programInCachedSnapshot.FindProcedure(node.Proc.Name);
196+
if (oldProc != null
197+
&& oldProc.DependencyChecksum != node.Proc.DependencyChecksum
198+
&& node.AssignedAssumptionVariable == null)
199+
{
200+
var before = new List<Cmd>();
201+
var beforePreconditionCheck = new List<Cmd>();
202+
var after = new List<Cmd>();
203+
var axioms = new List<Axiom>();
204+
Expr assumedExpr = new LiteralExpr(Token.NoToken, false);
205+
// TODO(wuestholz): Try out two alternatives: only do this for low priority implementations or not at all.
206+
var canUseSpecs = DependencyCollector.CanExpressOldSpecs(oldProc, Program);
207+
if (canUseSpecs && oldProc.SignatureEquals(options, node.Proc))
208+
{
209+
var desugaring = node.GetDesugaring(options);
210+
Contract.Assert(desugaring != null);
211+
var precond = node.CheckedPrecondition(oldProc, Program, e => FunctionExtractor.Extract(e, Program, axioms));
212+
if (precond != null)
213+
{
214+
var assume = new AssumeCmd(node.tok, precond,
215+
new QKeyValue(Token.NoToken, "precondition_previous_snapshot", new List<object>(), null));
216+
assume.IrrelevantForChecksumComputation = true;
217+
beforePreconditionCheck.Add(assume);
218+
}
219+
220+
var unmods = node.UnmodifiedBefore(oldProc);
221+
var eqs = new List<Expr>();
222+
foreach (var unmod in unmods)
223+
{
224+
var oldUnmod = new LocalVariable(Token.NoToken,
225+
new TypedIdent(Token.NoToken, string.Format("{0}##old##{1}", unmod.Name, FreshTemporaryVariableName),
226+
unmod.Type));
227+
var lhs = new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, oldUnmod));
228+
var rhs = new IdentifierExpr(Token.NoToken, unmod.Decl);
229+
var cmd = new AssignCmd(Token.NoToken, new List<AssignLhs> {lhs}, new List<Expr> {rhs});
230+
cmd.IrrelevantForChecksumComputation = true;
231+
before.Add(cmd);
232+
var eq = LiteralExpr.Eq(new IdentifierExpr(Token.NoToken, oldUnmod),
233+
new IdentifierExpr(Token.NoToken, unmod.Decl));
234+
eq.Type = Type.Bool;
235+
eq.TypeParameters = SimpleTypeParamInstantiation.EMPTY;
236+
eqs.Add(eq);
237+
}
238+
239+
var mods = node.ModifiedBefore(oldProc);
240+
var oldSubst = new Dictionary<Variable, Expr>();
241+
foreach (var mod in mods)
242+
{
243+
var oldMod = new LocalVariable(Token.NoToken,
244+
new TypedIdent(Token.NoToken, string.Format("{0}##old##{1}", mod.Name, FreshTemporaryVariableName),
245+
mod.Type));
246+
oldSubst[mod.Decl] = new IdentifierExpr(Token.NoToken, oldMod);
247+
var lhs = new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, oldMod));
248+
var rhs = new IdentifierExpr(Token.NoToken, mod.Decl);
249+
var cmd = new AssignCmd(Token.NoToken, new List<AssignLhs> {lhs}, new List<Expr> {rhs});
250+
cmd.IrrelevantForChecksumComputation = true;
251+
before.Add(cmd);
252+
}
253+
254+
assumedExpr = node.Postcondition(oldProc, eqs, oldSubst, Program,
255+
e => FunctionExtractor.Extract(e, Program, axioms));
256+
if (assumedExpr == null)
257+
{
258+
assumedExpr = new LiteralExpr(Token.NoToken, true);
259+
}
260+
}
261+
262+
if (assumedExpr != null)
263+
{
264+
var lv = new LocalVariable(Token.NoToken,
265+
new TypedIdent(Token.NoToken, string.Format("a##cached##{0}", FreshAssumptionVariableName), Type.Bool),
266+
new QKeyValue(Token.NoToken, "assumption", new List<object>(), null));
267+
node.AssignedAssumptionVariable = lv;
268+
currentImplementation.InjectAssumptionVariable(lv, !canUseSpecs);
269+
var lhs = new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, lv));
270+
var rhs = LiteralExpr.And(new IdentifierExpr(Token.NoToken, lv), assumedExpr);
271+
var assumed = new AssignCmd(node.tok, new List<AssignLhs> {lhs}, new List<Expr> {rhs});
272+
assumed.IrrelevantForChecksumComputation = true;
273+
after.Add(assumed);
274+
}
275+
276+
node.ExtendDesugaring(options, before, beforePreconditionCheck, after);
277+
if (options.TraceCachingForTesting || options.TraceCachingForBenchmarking) {
278+
using var tokTxtWr = new TokenTextWriter("<console>", options.OutputWriter, false, false, options);
279+
var loc = node.tok != null && node.tok != Token.NoToken
280+
? $"{node.tok.filename}({node.tok.line},{node.tok.col})"
281+
: "<unknown location>";
282+
options.OutputWriter.WriteLine("Processing call to procedure {0} in implementation {1} (at {2}):", node.Proc.VerboseName,
283+
currentImplementation.VerboseName, loc);
284+
foreach (var a in axioms)
285+
{
286+
options.OutputWriter.Write(" >>> added axiom: ");
287+
a.Expr.Emit(tokTxtWr);
288+
options.OutputWriter.WriteLine();
289+
}
290+
291+
foreach (var b in before)
292+
{
293+
options.OutputWriter.Write(" >>> added before: ");
294+
b.Emit(tokTxtWr, 0);
295+
}
296+
297+
foreach (var b in beforePreconditionCheck)
298+
{
299+
options.OutputWriter.Write(" >>> added before precondition check: ");
300+
b.Emit(tokTxtWr, 0);
301+
}
302+
303+
foreach (var a in after)
304+
{
305+
options.OutputWriter.Write(" >>> added after: ");
306+
a.Emit(tokTxtWr, 0);
307+
}
308+
}
309+
}
310+
311+
return result;
312+
}
313+
}

‎Source/ExecutionEngine/Caching/CachedVerificationResultInjectorRun.cs

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
using System;
2+
3+
namespace Microsoft.Boogie;
4+
5+
struct CachedVerificationResultInjectorRun
6+
{
7+
public DateTime Start { get; internal set; }
8+
9+
public DateTime End { get; internal set; }
10+
11+
public int TransformedImplementationCount { get; internal set; }
12+
13+
public int ImplementationCount { get; internal set; }
14+
15+
public int SkippedImplementationCount { get; set; }
16+
17+
public int LowPriorityImplementationCount { get; set; }
18+
19+
public int MediumPriorityImplementationCount { get; set; }
20+
21+
public int HighPriorityImplementationCount { get; set; }
22+
23+
public long[] CachingActionCounts { get; set; }
24+
}

‎Source/ExecutionEngine/Caching/CachedVerificationResultInjectorStatistics.cs

Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
using System.Collections.Concurrent;
2+
using System.IO;
3+
using System.Linq;
4+
5+
namespace Microsoft.Boogie;
6+
7+
sealed class CachedVerificationResultInjectorStatistics
8+
{
9+
ConcurrentDictionary<string, CachedVerificationResultInjectorRun> runs =
10+
new ConcurrentDictionary<string, CachedVerificationResultInjectorRun>();
11+
12+
public bool AddRun(string requestId, CachedVerificationResultInjectorRun run)
13+
{
14+
return runs.TryAdd(requestId, run);
15+
}
16+
17+
public string Output(bool printTime = false)
18+
{
19+
var wr = new StringWriter();
20+
if (runs.Any())
21+
{
22+
wr.WriteLine("Cached verification result injector statistics as CSV:");
23+
wr.WriteLine("Request ID, Transformed, Low, Medium, High, Skipped{0}", printTime ? ", Time (ms)" : "");
24+
foreach (var kv in runs.OrderBy(kv => ExecutionEngine.AutoRequestId(kv.Key)))
25+
{
26+
var t = printTime ? string.Format(", {0,8:F0}", kv.Value.End.Subtract(kv.Value.Start).TotalMilliseconds) : "";
27+
wr.WriteLine("{0,-19}, {1,3}, {2,3}, {3,3}, {4,3}, {5,3}{6}", kv.Key, kv.Value.TransformedImplementationCount,
28+
kv.Value.LowPriorityImplementationCount, kv.Value.MediumPriorityImplementationCount,
29+
kv.Value.HighPriorityImplementationCount, kv.Value.SkippedImplementationCount, t);
30+
}
31+
}
32+
33+
return wr.ToString();
34+
}
35+
}

0 commit comments

Comments
 (0)