Skip to content

Commit 9fd3265

Browse files
authored
[fix] duplicated call stmts of spec procedures (#851)
1 parent 323da0d commit 9fd3265

File tree

1 file changed

+23
-8
lines changed

1 file changed

+23
-8
lines changed

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

Lines changed: 23 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -296,6 +296,7 @@ public IEnumerable<CompiledFile> GenerateCode(ICompilerConfiguration job, Scope
296296
_commands = [];
297297
_globalScope = globalScope;
298298
BuildDependencies(globalScope);
299+
PopulateSpecHandlers((from m in _globalScope.AllDecls.OfType<Machine>() where m.IsSpec select m).ToList());
299300
var filenamePrefix = $"{job.ProjectName}_";
300301
List<CompiledFile> files = [];
301302
// if there are no proof commands, then create two:
@@ -358,6 +359,26 @@ bool emitCode (ProofCommand cmd) => job.TargetProofBlocks.Count == 0 ||
358359
return files;
359360
}
360361

362+
private void PopulateSpecHandlers(IEnumerable<Machine> specs)
363+
{
364+
foreach (var spec in specs)
365+
{
366+
var events = spec.Observes.Events;
367+
foreach (var e in events)
368+
{
369+
var procedureName = $"{SpecPrefix}{spec.Name}_{e.Name}";
370+
if (_specListenMap.ContainsKey(e))
371+
{
372+
_specListenMap[e].Add(procedureName);
373+
}
374+
else
375+
{
376+
_specListenMap.Add(e, [procedureName]);
377+
}
378+
}
379+
}
380+
}
381+
361382
private CompiledFile GenerateCompiledFile(ProofCommand cmd, string name, Machine m, State s, Event e)
362383
{
363384
var filename = name;
@@ -979,14 +1000,8 @@ private void GenerateSpecHandlers(List<Machine> specs)
9791000
foreach (var e in events)
9801001
{
9811002
var procedureName = $"{SpecPrefix}{spec.Name}_{e.Name}";
982-
if (_specListenMap.ContainsKey(e))
983-
{
984-
_specListenMap[e].Add(procedureName);
985-
}
986-
else
987-
{
988-
_specListenMap.Add(e, [procedureName]);
989-
}
1003+
Trace.Assert(_specListenMap.ContainsKey(e) && _specListenMap[e].Contains(procedureName),
1004+
$"Procedure {procedureName} is not generated for Spec {spec.Name} that listens to {e.Name}");
9901005

9911006
EmitLine($"procedure [inline] {procedureName}({SpecPrefix}Payload: {TypeToString(e.PayloadType)})");
9921007
EmitLine("{");

0 commit comments

Comments
 (0)