Skip to content

Commit 4c8edc0

Browse files
Ang9876Ang9876
authored
set sanity check (#852)
1 parent 9fd3265 commit 4c8edc0

File tree

2 files changed

+105
-82
lines changed

2 files changed

+105
-82
lines changed

‎Src/PCompiler/CompilerCore/Backend/PVerifier/Uclid5CodeGenerator.cs

Lines changed: 104 additions & 81 deletions
Original file line numberDiff line numberDiff line change
@@ -38,6 +38,7 @@ public class PVerifierCodeGenerator : ICodeGenerator
3838
private Dictionary<Invariant, HashSet<Invariant>> _invariantDependencies;
3939
private HashSet<Invariant> _provenInvariants;
4040
private Scope _globalScope;
41+
private Invariant _defaultInv;
4142

4243
public bool HasCompilationStage => true;
4344

@@ -161,17 +162,18 @@ public void Compile(ICompilerConfiguration job)
161162

162163
Console.WriteLine();
163164
}
164-
165+
165166
succeededInv.ExceptWith(failedInv);
166167
job.Output.WriteInfo($"\n🎉 Verified {succeededInv.Count} invariants!");
167168
foreach (var inv in succeededInv)
168169
{
169-
job.Output.WriteInfo($"✅ {inv.Name.Replace("_PGROUP_", ": ")}");
170-
}
171-
172-
if (!missingDefault && failMessages.Count == 0)
173-
{
174-
job.Output.WriteInfo($"✅ default P proof obligations");
170+
if (!inv.IsDefault) {
171+
job.Output.WriteInfo($"✅ {inv.Name.Replace("_PGROUP_", ": ")}");
172+
}
173+
else {
174+
job.Output.WriteInfo($"✅ default P proof obligations");
175+
}
176+
175177
}
176178

177179
MarkProvenInvariants(succeededInv);
@@ -244,9 +246,18 @@ private void ProcessFailureMessages(List<Match> collection, string[] query, stri
244246
var line = query[int.Parse(feedback.Second.ToString()) - 1];
245247
var step = feedback.First.ToString().Contains("[Step #0]") ? "(base case)" : "";
246248
var matchName = Regex.Match(line, @"// Failed to verify invariant (.*) at (.*)");
247-
var invName = matchName.Groups[1].Value.Replace("_PGROUP_", ": ");
248-
failedInv.Add(invName);
249-
failMessages.Add($"{reason} {line.Split("//").Last()} {step}");
249+
if (matchName.Success) {
250+
var invName = matchName.Groups[1].Value.Replace("_PGROUP_", ": ");
251+
failedInv.Add(invName);
252+
failMessages.Add($"{reason} {line.Split("// ").Last()} {step}");
253+
}
254+
255+
var matchDefault = Regex.Match(line,
256+
@"(// Failed to verify that (.*) never receives (.*) in (.*)|// Failed to ensure unique action IDs at (.*)|// Failed to ensure increasing action IDs at (.*)|// Failed to ensure that received is a subset of sent at (.*))");
257+
if (matchDefault.Success) {
258+
failedInv.Add("default");
259+
failMessages.Add($"{reason} {line.Split("// ").Last()}");
260+
}
250261
}
251262
}
252263
}
@@ -277,6 +288,9 @@ private void ProcessFailureMessages(List<Match> collection, string[] query, stri
277288

278289
return (succeededInv, failedInv.Select(x =>
279290
{
291+
if (x == "default") {
292+
return _defaultInv;
293+
}
280294
_globalScope.Get(x, out Invariant i);
281295
return i;
282296
}).ToHashSet(), failMessages);
@@ -300,7 +314,7 @@ public IEnumerable<CompiledFile> GenerateCode(ICompilerConfiguration job, Scope
300314
var filenamePrefix = $"{job.ProjectName}_";
301315
List<CompiledFile> files = [];
302316
// if there are no proof commands, then create two:
303-
// - one called default for checking that everything is handled
317+
// - one called default for checking that everything is handled and sanity checkings
304318
// - one with all the invariants as goals
305319
if (!globalScope.ProofCommands.Any())
306320
{
@@ -341,7 +355,7 @@ bool emitCode (ProofCommand cmd) => job.TargetProofBlocks.Count == 0 ||
341355
if (proofCmd.Goals.Count == 1 && proofCmd.Goals[0].IsDefault)
342356
{
343357
proofCmd.Name = "default";
344-
proofCmd.Goals = [];
358+
_defaultInv = proofCmd.Goals[0];
345359
_commands.Add(proofCmd);
346360
_proofCommandToFiles.Add(proofCmd, []);
347361
files.AddRange(CompileToFile($"{filenamePrefix}default", proofCmd));
@@ -424,29 +438,26 @@ private List<CompiledFile> CompileToFile(string name, ProofCommand cmd)
424438
files.Add(_src);
425439
GenerateMain(null, null, null, cmd);
426440
}
427-
else
441+
foreach (var m in machines)
428442
{
429-
foreach (var m in machines)
443+
if (_ctx.Job.CheckOnly == null || _ctx.Job.CheckOnly.Contains(m.Name))
430444
{
431-
if (_ctx.Job.CheckOnly == null || _ctx.Job.CheckOnly.Contains(m.Name))
445+
foreach (var s in m.States)
432446
{
433-
foreach (var s in m.States)
447+
if (_ctx.Job.CheckOnly == null || _ctx.Job.CheckOnly.Contains(s.Name))
434448
{
435-
if (_ctx.Job.CheckOnly == null || _ctx.Job.CheckOnly.Contains(s.Name))
436-
{
437-
_src = GenerateCompiledFile(cmd, name, m, s, null);
438-
files.Add(_src);
439-
GenerateMain(m, s, null, cmd);
440-
}
449+
_src = GenerateCompiledFile(cmd, name, m, s, null);
450+
files.Add(_src);
451+
GenerateMain(m, s, null, cmd, cmd.Name == "default");
452+
}
441453

442-
foreach (var e in events.Where(e => !e.IsNullEvent && !e.IsHaltEvent && s.HasHandler(e)))
454+
foreach (var e in events.Where(e => !e.IsNullEvent && !e.IsHaltEvent && s.HasHandler(e)))
455+
{
456+
if (_ctx.Job.CheckOnly == null || _ctx.Job.CheckOnly.Contains(e.Name))
443457
{
444-
if (_ctx.Job.CheckOnly == null || _ctx.Job.CheckOnly.Contains(e.Name))
445-
{
446-
_src = GenerateCompiledFile(cmd, name, m, s, e);
447-
files.Add(_src);
448-
GenerateMain(m, s, e, cmd);
449-
}
458+
_src = GenerateCompiledFile(cmd, name, m, s, e);
459+
files.Add(_src);
460+
GenerateMain(m, s, e, cmd, cmd.Name == "default");
450461
}
451462
}
452463
}
@@ -458,7 +469,7 @@ private List<CompiledFile> CompileToFile(string name, ProofCommand cmd)
458469
}
459470

460471
private void BuildDependencies(Scope globalScope)
461-
{
472+
{
462473
foreach (var cmd in globalScope.ProofCommands)
463474
{
464475
foreach (var goal in cmd.Goals)
@@ -1041,11 +1052,8 @@ private void GenerateSpecHandlers(List<Machine> specs)
10411052
/********************************
10421053
* Traverse the P AST and generate the UCLID5 code using the types and helpers defined above
10431054
*******************************/
1044-
private void GenerateMain(Machine machine, State state, Event @event, ProofCommand cmd)
1055+
private void GenerateMain(Machine machine, State state, Event @event, ProofCommand cmd, bool generateSanityChecks = false)
10451056
{
1046-
// cmd.Proof is default iff all the others are null
1047-
Trace.Assert((cmd.Name == "default") == (machine is null && state is null && @event is null));
1048-
10491057
EmitLine("module main {");
10501058

10511059
var machines = (from m in _globalScope.AllDecls.OfType<Machine>() where !m.IsSpec select m).ToList();
@@ -1095,10 +1103,10 @@ private void GenerateMain(Machine machine, State state, Event @event, ProofComma
10951103
EmitLine("");
10961104

10971105
// global functions
1098-
GenerateGlobalProcedures(_globalScope.AllDecls.OfType<Function>(), cmd.Goals);
1106+
GenerateGlobalProcedures(_globalScope.AllDecls.OfType<Function>(), cmd.Goals, generateSanityChecks);
10991107

11001108
// Spec support
1101-
GenerateSpecProcedures(specs, cmd.Goals); // generate spec methods, called by spec handlers
1109+
GenerateSpecProcedures(specs, cmd.Goals, generateSanityChecks); // generate spec methods, called by spec handlers
11021110
GenerateSpecHandlers(specs); // will populate _specListenMap, which is used when ever there is a send statement
11031111
EmitLine("");
11041112

@@ -1126,7 +1134,9 @@ private void GenerateMain(Machine machine, State state, Event @event, ProofComma
11261134

11271135
foreach (var inv in cmd.Goals)
11281136
{
1129-
EmitLine($"define {InvariantPrefix}{inv.Name}(): boolean = {ExprToString(inv.Body)};");
1137+
if (!inv.IsDefault) {
1138+
EmitLine($"define {InvariantPrefix}{inv.Name}(): boolean = {ExprToString(inv.Body)};");
1139+
}
11301140
}
11311141

11321142
EmitLine("");
@@ -1154,7 +1164,7 @@ private void GenerateMain(Machine machine, State state, Event @event, ProofComma
11541164
GenerateOptionTypes();
11551165
EmitLine("");
11561166

1157-
if (cmd.Name == "default")
1167+
if (cmd.Name == "default" && machine == null && state == null && @event == null)
11581168
{
11591169
GenerateInitBlock(machines, specs, _globalScope.AllDecls.OfType<AssumeOnStart>());
11601170
EmitLine("");
@@ -1172,17 +1182,17 @@ private void GenerateMain(Machine machine, State state, Event @event, ProofComma
11721182
else
11731183
{
11741184
// non-handler functions for handlers
1175-
GenerateMachineProcedures(machine, cmd.Goals); // generate machine methods, called by handlers below
1185+
GenerateMachineProcedures(machine, cmd.Goals, generateSanityChecks); // generate machine methods, called by handlers below
11761186
EmitLine("");
11771187

11781188
// generate the handlers
11791189
if (@event != null)
11801190
{
1181-
GenerateEventHandler(state, @event, cmd.Goals, cmd.Premises);
1191+
GenerateEventHandler(state, @event, cmd.Goals, cmd.Premises, generateSanityChecks);
11821192
}
11831193
else
11841194
{
1185-
GenerateEntryHandler(state, cmd.Goals, cmd.Premises);
1195+
GenerateEntryHandler(state, cmd.Goals, cmd.Premises, generateSanityChecks);
11861196
}
11871197

11881198
EmitLine("");
@@ -1394,14 +1404,16 @@ private void GenerateEntryHandler(State s, List<Invariant> goals, List<Invariant
13941404
EmitLine($"\trequires {EventOrGotoAdtIsGoto(action)};");
13951405
EmitLine($"\trequires {GotoAdtIsS(g, s)};");
13961406
EmitLine($"\trequires {MachineStateAdtInS(targetMachineState, s.OwningMachine, s)};");
1407+
1408+
EmitLine($"\trequires {InvariantPrefix}Unique_Actions();");
1409+
EmitLine($"\trequires {InvariantPrefix}Increasing_Action_Count();");
1410+
EmitLine($"\trequires {InvariantPrefix}Received_Subset_Sent();");
1411+
13971412
if (generateSanityChecks)
13981413
{
1399-
EmitLine($"\trequires {InvariantPrefix}Unique_Actions();");
1400-
EmitLine($"\tensures {InvariantPrefix}Unique_Actions();");
1401-
EmitLine($"\trequires {InvariantPrefix}Increasing_Action_Count();");
1402-
EmitLine($"\tensures {InvariantPrefix}Increasing_Action_Count();");
1403-
EmitLine($"\trequires {InvariantPrefix}Received_Subset_Sent();");
1404-
EmitLine($"\tensures {InvariantPrefix}Received_Subset_Sent();");
1414+
EmitLine($"\tensures {InvariantPrefix}Unique_Actions(); // Failed to ensure unique action IDs at {GetLocation(s)}");
1415+
EmitLine($"\tensures {InvariantPrefix}Increasing_Action_Count(); // Failed to ensure increasing action IDs at {GetLocation(s)}");
1416+
EmitLine($"\tensures {InvariantPrefix}Received_Subset_Sent(); // Failed to ensure that received is a subset of sent at {GetLocation(s)}");
14051417
}
14061418

14071419
foreach (var reqs in requires)
@@ -1411,9 +1423,11 @@ private void GenerateEntryHandler(State s, List<Invariant> goals, List<Invariant
14111423

14121424
foreach (var inv in goals)
14131425
{
1414-
EmitLine($"\trequires {InvariantPrefix}{inv.Name}();");
1415-
EmitLine(
1426+
if (!inv.IsDefault) {
1427+
EmitLine($"\trequires {InvariantPrefix}{inv.Name}();");
1428+
EmitLine(
14161429
$"\tensures {InvariantPrefix}{inv.Name}(); // Failed to verify invariant {inv.Name.Replace("_PGROUP_", ": ")} at {GetLocation(s)}");
1430+
}
14171431
}
14181432

14191433
EmitLine("{");
@@ -1479,28 +1493,32 @@ private void GenerateEventHandler(State s, Event ev, List<Invariant> goals, List
14791493
EmitLine($"\trequires {MachineStateAdtInS(targetMachineState, s.OwningMachine, s)};");
14801494
EmitLine($"\trequires {EventOrGotoAdtIsEvent(action)};");
14811495
EmitLine($"\trequires {EventAdtIsE(e, ev)};");
1482-
if (generateSanityChecks)
1483-
{
1484-
EmitLine($"\trequires {InvariantPrefix}Unique_Actions();");
1485-
EmitLine($"\tensures {InvariantPrefix}Unique_Actions();");
1486-
EmitLine($"\trequires {InvariantPrefix}Increasing_Action_Count();");
1487-
EmitLine($"\tensures {InvariantPrefix}Increasing_Action_Count();");
1488-
EmitLine($"\trequires {InvariantPrefix}Received_Subset_Sent();");
1489-
EmitLine($"\tensures {InvariantPrefix}Received_Subset_Sent();");
1490-
}
1496+
1497+
EmitLine($"\trequires {InvariantPrefix}Unique_Actions();");
1498+
EmitLine($"\trequires {InvariantPrefix}Increasing_Action_Count();");
1499+
EmitLine($"\trequires {InvariantPrefix}Received_Subset_Sent();");
14911500

14921501
var handler = s.AllEventHandlers.ToDictionary()[ev];
14931502

1503+
if (generateSanityChecks)
1504+
{
1505+
EmitLine($"\tensures {InvariantPrefix}Unique_Actions(); // Failed to ensure unique action IDs at {GetLocation(handler)}");
1506+
EmitLine($"\tensures {InvariantPrefix}Increasing_Action_Count(); // Failed to ensure increasing action IDs at {GetLocation(handler)}");
1507+
EmitLine($"\tensures {InvariantPrefix}Received_Subset_Sent(); // Failed to ensure that received is a subset of sent at {GetLocation(handler)}");
1508+
}
1509+
14941510
foreach (var reqs in requires)
14951511
{
14961512
EmitLine($"\trequires {InvariantPrefix}{reqs.Name}();");
14971513
}
14981514

14991515
foreach (var inv in goals)
15001516
{
1501-
EmitLine($"\trequires {InvariantPrefix}{inv.Name}();");
1502-
EmitLine(
1503-
$"\tensures {InvariantPrefix}{inv.Name}(); // Failed to verify invariant {inv.Name.Replace("_PGROUP_", ": ")} at {GetLocation(handler)}");
1517+
if (!inv.IsDefault) {
1518+
EmitLine($"\trequires {InvariantPrefix}{inv.Name}();");
1519+
EmitLine(
1520+
$"\tensures {InvariantPrefix}{inv.Name}(); // Failed to verify invariant {inv.Name.Replace("_PGROUP_", ": ")} at {GetLocation(handler)}");
1521+
}
15041522
}
15051523

15061524
switch (handler)
@@ -1515,8 +1533,8 @@ private void GenerateEventHandler(State s, Event ev, List<Invariant> goals, List
15151533
var name = f.Name == "" ? $"{BuiltinPrefix}{f.Owner.Name}_f{line}" : f.Name;
15161534
var payload = f.Signature.Parameters.Count > 0 ? $", {EventAdtSelectPayload(e, ev)}" : "";
15171535
EmitLine("{");
1518-
EmitLine($"{received} = {received}[{label} -> true];");
15191536
EmitLine($"call {name}({target}{payload});");
1537+
EmitLine($"{received} = {received}[{label} -> true];");
15201538
foreach (var reqs in requires)
15211539
{
15221540
EmitLine($"assume {InvariantPrefix}{reqs.Name}();");
@@ -1811,25 +1829,27 @@ private void GenerateStmt(IPStmt stmt, Machine specMachine, List<Invariant> goal
18111829
EmitLine($"while ({checker} != {collection})");
18121830
foreach (var inv in goals)
18131831
{
1814-
EmitLine(
1815-
$"\tinvariant {InvariantPrefix}{inv.Name}(); // Failed to verify invariant {inv.Name.Replace("_PGROUP_", ": ")} at {GetLocation(fstmt)}");
1832+
if (!inv.IsDefault) {
1833+
EmitLine($"\tinvariant {InvariantPrefix}{inv.Name}(); // Failed to verify invariant {inv.Name.Replace("_PGROUP_", ": ")} at {GetLocation(fstmt)}");
1834+
}
1835+
18161836
}
18171837

18181838
if (generateSanityChecks)
18191839
{
1820-
EmitLine($"\tinvariant {InvariantPrefix}Unique_Actions();");
1821-
EmitLine($"\tinvariant {InvariantPrefix}Increasing_Action_Count();");
1822-
EmitLine($"\tinvariant {InvariantPrefix}Received_Subset_Sent();");
1823-
// ensure uniqueness for the new ones too
1824-
EmitLine(
1825-
$"\tinvariant forall (a1: {LabelAdt}, a2: {LabelAdt}) :: (a1 != a2 && {LocalPrefix}sent[a1] && {LocalPrefix}sent[a2]) ==> {LabelAdtSelectActionCount("a1")} != {LabelAdtSelectActionCount("a2")};");
1826-
EmitLine(
1827-
$"\tinvariant forall (a: {LabelAdt}) :: {LocalPrefix}sent[a] ==> {LabelAdtSelectActionCount("a")} < {BuiltinPrefix}ActionCount;");
1828-
1829-
// ensure we only ever add sends
1830-
EmitLine(
1831-
$"\tinvariant forall (e: {LabelAdt}) :: {StateAdtSelectSent(StateVar)}[e] ==> {LocalPrefix}sent[e];");
1840+
EmitLine($"\tinvariant {InvariantPrefix}Unique_Actions(); // Failed to ensure unique action IDs at {GetLocation(fstmt)}");
1841+
EmitLine($"\tinvariant {InvariantPrefix}Increasing_Action_Count(); // Failed to ensure increasing action IDs at {GetLocation(fstmt)}");
1842+
EmitLine($"\tinvariant {InvariantPrefix}Received_Subset_Sent(); // Failed to ensure that received is a subset of sent at {GetLocation(fstmt)}");
18321843
}
1844+
1845+
// ensure uniqueness for the new ones too
1846+
EmitLine(
1847+
$"\tinvariant forall (a1: {LabelAdt}, a2: {LabelAdt}) :: (a1 != a2 && {LocalPrefix}sent[a1] && {LocalPrefix}sent[a2]) ==> {LabelAdtSelectActionCount("a1")} != {LabelAdtSelectActionCount("a2")};");
1848+
EmitLine(
1849+
$"\tinvariant forall (a: {LabelAdt}) :: {LocalPrefix}sent[a] ==> {LabelAdtSelectActionCount("a")} < {BuiltinPrefix}ActionCount;");
1850+
// ensure we only ever add sends
1851+
EmitLine(
1852+
$"\tinvariant forall (e: {LabelAdt}) :: {StateAdtSelectSent(StateVar)}[e] ==> {LocalPrefix}sent[e];");
18331853

18341854
// user given invariants
18351855
foreach (var inv in fstmt.Invariants)
@@ -1860,13 +1880,16 @@ private void GenerateStmt(IPStmt stmt, Machine specMachine, List<Invariant> goal
18601880
EmitLine($"while ({checker} != {collection})");
18611881
foreach (var inv in goals)
18621882
{
1863-
EmitLine(
1864-
$"\tinvariant {InvariantPrefix}{inv.Name}(); // Failed to verify invariant {inv.Name.Replace("_PGROUP_", ": ")} at {GetLocation(fstmt)}");
1883+
if (!inv.IsDefault) {
1884+
EmitLine($"\tinvariant {InvariantPrefix}{inv.Name}(); // Failed to verify invariant {inv.Name.Replace("_PGROUP_", ": ")} at {GetLocation(fstmt)}");
1885+
}
18651886
}
18661887

1867-
EmitLine($"\tinvariant {InvariantPrefix}Unique_Actions();");
1868-
EmitLine($"\tinvariant {InvariantPrefix}Increasing_Action_Count();");
1869-
EmitLine($"\tinvariant {InvariantPrefix}Received_Subset_Sent();");
1888+
if (generateSanityChecks) {
1889+
EmitLine($"\tinvariant {InvariantPrefix}Unique_Actions(); // Failed to ensure unique action IDs at {GetLocation(fstmt)}");
1890+
EmitLine($"\tinvariant{InvariantPrefix}Increasing_Action_Count(); // Failed to ensure increasing action IDs at {GetLocation(fstmt)}");
1891+
EmitLine($"\tinvariant {InvariantPrefix}Received_Subset_Sent(); // Failed to ensure that received is a subset of sent at {GetLocation(fstmt)}");
1892+
}
18701893
// ensure uniqueness for the new ones too
18711894
EmitLine(
18721895
$"\tinvariant forall (a1: {LabelAdt}, a2: {LabelAdt}) :: (a1 != a2 && {LocalPrefix}sent[a1] && {LocalPrefix}sent[a2]) ==> {LabelAdtSelectActionCount("a1")} != {LabelAdtSelectActionCount("a2")};");

0 commit comments

Comments
 (0)