From 7ded32158cd0fb63aa3c1bea349c21a0f35e9aee Mon Sep 17 00:00:00 2001 From: Ankush Desai Date: Tue, 9 Apr 2024 14:07:53 -0700 Subject: [PATCH 1/5] Added support for generating a warning when spec handles an event but does not add it in its observes list (#716) --- .../DefaultTranslationErrorHandler.cs | 5 ++++ .../CompilerCore/ITranslationErrorHandler.cs | 2 ++ .../CompilerCore/TypeChecker/Analyzer.cs | 2 +- .../TypeChecker/MachineChecker.cs | 23 ++++++++++++++++++- .../Correct/monitorobserves/observes.p | 14 +++++++++++ 5 files changed, 44 insertions(+), 2 deletions(-) create mode 100644 Tst/RegressionTests/Feature1SMLevelDecls/Correct/monitorobserves/observes.p diff --git a/Src/PCompiler/CompilerCore/DefaultTranslationErrorHandler.cs b/Src/PCompiler/CompilerCore/DefaultTranslationErrorHandler.cs index ccacf6fcf..4aef965ae 100644 --- a/Src/PCompiler/CompilerCore/DefaultTranslationErrorHandler.cs +++ b/Src/PCompiler/CompilerCore/DefaultTranslationErrorHandler.cs @@ -334,5 +334,10 @@ private string DeclarationName(IPDecl method) { return method.Name.Length > 0 ? method.Name : $"at {locationResolver.GetLocation(method.SourceLocation)}"; } + + public string SpecObservesSetIncompleteWarning(ParserRuleContext ctx, PEvent ev, Machine machine) + { + return $"[!Warning!]\n[{locationResolver.GetLocation(ctx, ctx.start)}] Event {ev.Name} is not in the observes list of the spec machine {machine.Name}. The event-handler is never triggered as the event is not observed by the spec.\n[!Warning!]"; + } } } \ No newline at end of file diff --git a/Src/PCompiler/CompilerCore/ITranslationErrorHandler.cs b/Src/PCompiler/CompilerCore/ITranslationErrorHandler.cs index 00e12c244..402a5fc5d 100644 --- a/Src/PCompiler/CompilerCore/ITranslationErrorHandler.cs +++ b/Src/PCompiler/CompilerCore/ITranslationErrorHandler.cs @@ -117,5 +117,7 @@ Exception DuplicateStartState( Exception IllegalChooseSubExprType(PParser.ChooseExprContext context, PLanguageType subExprType); Exception IllegalFunctionUsedInSpecMachine(Function function, Machine callerOwner); + + String SpecObservesSetIncompleteWarning(ParserRuleContext loc, PEvent ev, Machine machine); } } \ No newline at end of file diff --git a/Src/PCompiler/CompilerCore/TypeChecker/Analyzer.cs b/Src/PCompiler/CompilerCore/TypeChecker/Analyzer.cs index 050be18cc..97ee4dabd 100644 --- a/Src/PCompiler/CompilerCore/TypeChecker/Analyzer.cs +++ b/Src/PCompiler/CompilerCore/TypeChecker/Analyzer.cs @@ -20,7 +20,7 @@ public static Scope AnalyzeCompilationUnit(ICompilerConfiguration config, // Step 2: Validate machine specifications foreach (var machine in globalScope.Machines) { - MachineChecker.Validate(handler, machine); + MachineChecker.Validate(handler, machine, config); } // Step 3: Fill function bodies diff --git a/Src/PCompiler/CompilerCore/TypeChecker/MachineChecker.cs b/Src/PCompiler/CompilerCore/TypeChecker/MachineChecker.cs index 628d9cac5..b8f0a5cdd 100644 --- a/Src/PCompiler/CompilerCore/TypeChecker/MachineChecker.cs +++ b/Src/PCompiler/CompilerCore/TypeChecker/MachineChecker.cs @@ -11,13 +11,34 @@ namespace Plang.Compiler.TypeChecker { public static class MachineChecker { - public static void Validate(ITranslationErrorHandler handler, Machine machine) + public static void Validate(ITranslationErrorHandler handler, Machine machine, ICompilerConfiguration job) { var startState = FindStartState(machine, handler); var startStatePayloadType = GetStatePayload(startState); Debug.Assert(startStatePayloadType.IsSameTypeAs(machine.PayloadType)); ValidateHandlers(handler, machine); ValidateTransitions(handler, machine); + // special validation for monitors: + // ensure that each eventhandler is in the observe set. + ValidateSpecObservesList(handler, machine, job); + } + + private static void ValidateSpecObservesList(ITranslationErrorHandler handler, Machine machine, ICompilerConfiguration job) + { + if (machine.IsSpec) + { + foreach (var state in machine.AllStates()) + { + foreach (var pair in state.AllEventHandlers) + { + if (!machine.Observes.Events.Contains(pair.Key)) + { + job.Output.WriteWarning( + handler.SpecObservesSetIncompleteWarning(pair.Value.SourceLocation, pair.Key, machine)); + } + } + } + } } private static void ValidateHandlers(ITranslationErrorHandler handler, Machine machine) diff --git a/Tst/RegressionTests/Feature1SMLevelDecls/Correct/monitorobserves/observes.p b/Tst/RegressionTests/Feature1SMLevelDecls/Correct/monitorobserves/observes.p new file mode 100644 index 000000000..03855f714 --- /dev/null +++ b/Tst/RegressionTests/Feature1SMLevelDecls/Correct/monitorobserves/observes.p @@ -0,0 +1,14 @@ +event e1; +event e2; + +spec Invariant1 observes e1 { + start state Init { + on e2 goto Init; + } +} + +machine Main { + start state Init { + + } +} \ No newline at end of file From 5e7f6c68e976dc6064fb5dcb52778d715bda5c27 Mon Sep 17 00:00:00 2001 From: Eric Hua Date: Mon, 15 Apr 2024 08:33:18 -0700 Subject: [PATCH 2/5] Create custom converter for JSON serialization in .NET8 (#717) * Create custom converter for JSON serialization in .NET8 * Add check for different dictionary type for null replacement --------- Co-authored-by: Eric Hua --- .../SystematicTesting/TestingEngine.cs | 31 +++++++++++++++++-- 1 file changed, 28 insertions(+), 3 deletions(-) diff --git a/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs b/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs index 0c7fb0bca..3a54d5e47 100644 --- a/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs +++ b/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs @@ -97,9 +97,25 @@ public class TestingEngine { DefaultIgnoreCondition = JsonIgnoreCondition.WhenWritingNull, PropertyNamingPolicy = JsonNamingPolicy.CamelCase, - WriteIndented = true + WriteIndented = true, + Converters = { new EncodingConverter() } }; + internal class EncodingConverter : JsonConverter + { + public override Encoding Read(ref Utf8JsonReader reader, Type typeToConvert, JsonSerializerOptions options) + { + var name = reader.GetString(); + if (name == null) + return null; + return Encoding.GetEncoding(name); + } + public override void Write(Utf8JsonWriter writer, Encoding value, JsonSerializerOptions options) + { + writer.WriteStringValue(value.WebName); + } + } + /// /// The profiler. /// @@ -618,9 +634,18 @@ public object RecursivelyReplaceNullWithString(object obj) { if (obj == null) { return "null"; } - if (obj is Dictionary dictionary) { + if (obj is Dictionary dictionaryStr) { var newDictionary = new Dictionary(); - foreach (var item in dictionary) { + foreach (var item in dictionaryStr) { + var newVal = RecursivelyReplaceNullWithString(item.Value); + if (newVal != null) + newDictionary[item.Key] = newVal; + } + return newDictionary; + } + else if (obj is Dictionary dictionaryInt) { + var newDictionary = new Dictionary(); + foreach (var item in dictionaryInt) { var newVal = RecursivelyReplaceNullWithString(item.Value); if (newVal != null) newDictionary[item.Key] = newVal; From db2776377247520e6bbad415583702fa0a569ec4 Mon Sep 17 00:00:00 2001 From: Ao Li Date: Wed, 8 May 2024 16:37:27 -0400 Subject: [PATCH 3/5] udpate. --- Src/PChecker/CheckerCore/SystematicTesting/TestReport.cs | 2 +- .../CheckerCore/SystematicTesting/TestingEngine.cs | 7 +++++-- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/Src/PChecker/CheckerCore/SystematicTesting/TestReport.cs b/Src/PChecker/CheckerCore/SystematicTesting/TestReport.cs index 24fd70057..36b59c305 100644 --- a/Src/PChecker/CheckerCore/SystematicTesting/TestReport.cs +++ b/Src/PChecker/CheckerCore/SystematicTesting/TestReport.cs @@ -105,7 +105,7 @@ public class TestReport /// Set of hashes of timelines discovered by the scheduler. /// [DataMember] - public HashSet ExploredTimelines = new(); + public Dictionary ExploredTimelines = new(); /// /// Number of schedulings that satisfies the pattern. diff --git a/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs b/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs index 18042472c..f426c8788 100644 --- a/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs +++ b/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs @@ -706,6 +706,8 @@ private void RunNextIteration(int schedule) var seconds = watch.Elapsed.TotalSeconds; Logger.WriteLine($"Elapsed: {seconds}, " + $"# timelines: {TestReport.ExploredTimelines.Count}"); + var mostVisited = TestReport.ExploredTimelines.Values.Max(); + Logger.WriteLine($"Most visited: {mostVisited}"); if (Strategy is IFeedbackGuidedStrategy s) { s.DumpStats(Logger); @@ -1038,8 +1040,9 @@ private void GatherTestingStatistics(ControlledRuntime runtime, TimelineObserver var coverageInfo = runtime.GetCoverageInfo(); report.CoverageInfo.Merge(coverageInfo); TestReport.Merge(report); - - TestReport.ExploredTimelines.Add(timelineObserver.GetTimelineHash()); + var timelineHash = timelineObserver.GetTimelineHash(); + TestReport.ExploredTimelines[timelineHash] = + TestReport.ExploredTimelines.GetValueOrDefault(timelineHash, 0) + 1; // Also save the graph snapshot of the last iteration, if there is one. Graph = coverageInfo.CoverageGraph; // Also save the graph snapshot of the last schedule, if there is one. From e0dfaa4e71b9342a778d86409f75f3d7907ac98b Mon Sep 17 00:00:00 2001 From: Ao Li Date: Fri, 10 May 2024 16:07:46 -0400 Subject: [PATCH 4/5] update. --- Src/PChecker/CheckerCore/CheckerConfiguration.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Src/PChecker/CheckerCore/CheckerConfiguration.cs b/Src/PChecker/CheckerCore/CheckerConfiguration.cs index 57706a2b4..b1f183180 100644 --- a/Src/PChecker/CheckerCore/CheckerConfiguration.cs +++ b/Src/PChecker/CheckerCore/CheckerConfiguration.cs @@ -229,7 +229,7 @@ public int MaxSchedulingSteps /// Defaults to true. /// [DataMember] - public bool IsJsonLogEnabled { get; set; } = true; + public bool IsJsonLogEnabled { get; set; } = false; /// /// If specified, requests a custom runtime log to be used instead of the default. From 81ca950768175d45fc0d11aa012a4a7b4cbe5a77 Mon Sep 17 00:00:00 2001 From: Ao Li Date: Mon, 13 May 2024 15:22:54 -0400 Subject: [PATCH 5/5] update. --- Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs | 2 -- 1 file changed, 2 deletions(-) diff --git a/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs b/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs index f426c8788..5d8088d73 100644 --- a/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs +++ b/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs @@ -706,8 +706,6 @@ private void RunNextIteration(int schedule) var seconds = watch.Elapsed.TotalSeconds; Logger.WriteLine($"Elapsed: {seconds}, " + $"# timelines: {TestReport.ExploredTimelines.Count}"); - var mostVisited = TestReport.ExploredTimelines.Values.Max(); - Logger.WriteLine($"Most visited: {mostVisited}"); if (Strategy is IFeedbackGuidedStrategy s) { s.DumpStats(Logger);