diff --git a/.github/workflows/macosci.yml b/.github/workflows/macosci.yml index dd612f646..541814648 100644 --- a/.github/workflows/macosci.yml +++ b/.github/workflows/macosci.yml @@ -24,4 +24,10 @@ jobs: - name: Build run: dotnet build --configuration Release - name: Test - run: dotnet test --configuration Release + run: dotnet test --configuration Release --blame-crash --blame-hang --blame-hang-timeout 300s --logger:"console;verbosity=detailed" + - name: Upload Test Results + uses: actions/upload-artifact@v4 + if: always() # This ensures it runs even after test failure + with: + name: test-results + path: Tst/UnitTests/TestResults/**/*.xml diff --git a/Src/PChecker/CheckerCore/Checker.cs b/Src/PChecker/CheckerCore/Checker.cs index 07df575a2..bf0d4c07e 100644 --- a/Src/PChecker/CheckerCore/Checker.cs +++ b/Src/PChecker/CheckerCore/Checker.cs @@ -1,8 +1,8 @@ using System; using PChecker.IO.Debugging; using PChecker.IO.Logging; -using PChecker.SystematicTesting; using PChecker.Testing; +using PChecker.SystematicTesting; namespace PChecker; @@ -51,7 +51,12 @@ public static void Run(CheckerConfiguration configuration) switch (configuration.Mode) { case CheckerMode.BugFinding: - TestingProcess.Create(configuration).Run(); + var testingEngine = TestingProcess.Create(configuration); + if (configuration.ListTestCases) + { + break; + } + testingEngine.Run(); break; case CheckerMode.PEx: ExhaustiveEngine.Create(configuration).Run(); diff --git a/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs b/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs index 4aef7b527..458375e49 100644 --- a/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs +++ b/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs @@ -176,7 +176,7 @@ public static TestingEngine Create(CheckerConfiguration checkerConfiguration) => /// /// Creates a new systematic testing engine. /// - public static TestingEngine Create(CheckerConfiguration checkerConfiguration, Assembly assembly) + private static TestingEngine Create(CheckerConfiguration checkerConfiguration, Assembly assembly) { if (checkerConfiguration.ListTestCases) { @@ -190,7 +190,7 @@ public static TestingEngine Create(CheckerConfiguration checkerConfiguration, As Console.Out.WriteLine($"{mi.DeclaringType.Name}"); } - Environment.Exit(0); + return null; } catch { diff --git a/Src/PCompiler/CompilerCore/Backend/PChecker/PCheckerCodeGenerator.cs b/Src/PCompiler/CompilerCore/Backend/PChecker/PCheckerCodeGenerator.cs index 8be0dd182..32f80158d 100644 --- a/Src/PCompiler/CompilerCore/Backend/PChecker/PCheckerCodeGenerator.cs +++ b/Src/PCompiler/CompilerCore/Backend/PChecker/PCheckerCodeGenerator.cs @@ -1,5 +1,6 @@ using System; using System.Collections.Generic; +using System.ComponentModel.Design; using System.IO; using System.Linq; using System.Reflection; @@ -21,7 +22,8 @@ public class PCheckerCodeGenerator : ICodeGenerator /// This compiler has a compilation stage. /// public bool HasCompilationStage => true; - private static List _globalParams = []; + [ThreadStatic] + private static List _globalParams; private string GetGlobalParamAndLocalVariableName(CompilationContext context, Variable v) { @@ -346,6 +348,7 @@ private static void WriteForeignType(CompilationContext context, StringWriter ou // For normal test, the assignment is empty dictionary private void WriteSafetyTestDecl(CompilationContext context, StringWriter output, SafetyTest safety, Dictionary assignment) { + // Console.WriteLine($"dic: {string.Join(',', dic.ToList())}"); WriteNameSpacePrologue(context, output); var name = ParamAssignment.RenameSafetyTestByAssignment(context.Names.GetNameForDecl(safety), assignment); context.WriteLine(output, $"public class {name} {{"); diff --git a/Src/PCompiler/CompilerCore/TypeChecker/ParamAssignment.cs b/Src/PCompiler/CompilerCore/TypeChecker/ParamAssignment.cs index bc01adb46..cc24a482a 100644 --- a/Src/PCompiler/CompilerCore/TypeChecker/ParamAssignment.cs +++ b/Src/PCompiler/CompilerCore/TypeChecker/ParamAssignment.cs @@ -110,6 +110,11 @@ private static Dictionary IndexDic2Dic(List globalPa foreach (var (k, i) in indexDic) { var values = paramExprDic[k]; + if (!globalParams.Any(v => v.Name == k)) + { + throw new Exception($"Variable name '{k}' not found in globalParams. " + + $"GlobalParams are: [{string.Join(", ", globalParams.Select(v => v.Name))}]"); + } var variable = globalParams.First(v => v.Name == k); if (i >= values.Count) throw new ArgumentException("Index out of range in global variable config."); dic[variable] = values[i]; diff --git a/Src/PCompiler/CompilerCore/TypeChecker/ParamVisitor.cs b/Src/PCompiler/CompilerCore/TypeChecker/ParamVisitor.cs index 81b8c728e..a787fc4bf 100644 --- a/Src/PCompiler/CompilerCore/TypeChecker/ParamVisitor.cs +++ b/Src/PCompiler/CompilerCore/TypeChecker/ParamVisitor.cs @@ -46,16 +46,25 @@ public override IPExpr VisitSeqLiteralBody([NotNull] PParser.SeqLiteralBodyConte if (context.primitive() != null) { var values = context.primitive().Select(Visit).ToList(); - if (values.Count == 0) return new SeqLiteralExpr(context, values, PrimitiveType.Int); - // Console.WriteLine($"value[0] = {values[0].GetType()}"); + + if (values.Count == 2 && + values[0] is IntLiteralExpr first && + values[1] is IntLiteralExpr second && + first.Value == second.Value) + { + throw handler.InternalError(context, new Exception("Invalid range: start and end must not be equal (e.g., [2, 2] is not allowed)")); } + + if (values.Count == 0) + return new SeqLiteralExpr(context, values, PrimitiveType.Int); + var type = values[0].Type; foreach (var v in values.Where(v => !v.Type.Equals(type))) { throw handler.TypeMismatch(v.SourceLocation, v.Type, type); } + return new SeqLiteralExpr(context, values, new SequenceType(type)); - - } + } if (context.seqLiteral() != null) { return Visit(context.seqLiteral()); diff --git a/Src/PCompiler/PCommandLine/CommandLine.cs b/Src/PCompiler/PCommandLine/CommandLine.cs index c127e0bd8..a871b91b0 100644 --- a/Src/PCompiler/PCommandLine/CommandLine.cs +++ b/Src/PCompiler/PCommandLine/CommandLine.cs @@ -17,7 +17,7 @@ public static class CommandLine private static readonly object ConsoleLock = new object(); - private static void Main(string[] args) + public static void Main(string[] args) { // Save these so we can force output to happen even if TestingProcess has re-routed it. StdOut = Console.Out; diff --git a/Src/PEx/src/test/java/pex/TestPEx.java b/Src/PEx/src/test/java/pex/TestPEx.java index b21f56b08..20b2baba9 100644 --- a/Src/PEx/src/test/java/pex/TestPEx.java +++ b/Src/PEx/src/test/java/pex/TestPEx.java @@ -187,7 +187,11 @@ Collection loadTests(String testDirPath) { pathKeys.sort(String.CASE_INSENSITIVE_ORDER); if (testDir.contains("Correct")) { + for (String key : pathKeys) { + if (key.contains("ParamTest")) { + continue; + } runDynamicTest(0, paths.get(key), key, dynamicTests); } } else if (testDir.contains("DynamicError")) { diff --git a/Tst/CorrectLogs/bugs2/Main.coverage.txt b/Tst/CorrectLogs/bugs2/bug2.coverage.txt similarity index 100% rename from Tst/CorrectLogs/bugs2/Main.coverage.txt rename to Tst/CorrectLogs/bugs2/bug2.coverage.txt diff --git a/Tst/CorrectLogs/bugs2/Main_0_0.trace.json b/Tst/CorrectLogs/bugs2/bug2_0_0.trace.json similarity index 90% rename from Tst/CorrectLogs/bugs2/Main_0_0.trace.json rename to Tst/CorrectLogs/bugs2/bug2_0_0.trace.json index 0d8eca9d6..b8bcdad83 100644 --- a/Tst/CorrectLogs/bugs2/Main_0_0.trace.json +++ b/Tst/CorrectLogs/bugs2/bug2_0_0.trace.json @@ -1,15 +1,4 @@ -[ - { - "type": "CreateStateMachine", - "details": { - "log": "Main(1) was created by task \u00272\u0027.", - "id": "Main(1)", - "payload": "null", - "clock": { - "Main(1)": 1 - } - } - }, + [ { "type": "StateTransition", "details": { diff --git a/Tst/CorrectLogs/bugs2/Main_0_0.txt b/Tst/CorrectLogs/bugs2/bug2_0_0.txt similarity index 90% rename from Tst/CorrectLogs/bugs2/Main_0_0.txt rename to Tst/CorrectLogs/bugs2/bug2_0_0.txt index 82bedc2ab..d474d8c9d 100644 --- a/Tst/CorrectLogs/bugs2/Main_0_0.txt +++ b/Tst/CorrectLogs/bugs2/bug2_0_0.txt @@ -1,5 +1,3 @@ - Running test 'DefaultImpl'. - Main(1) was created by task '2'. Main(1) enters state 'S'. 'Main(1)' raised event 'x with payload ()' in state 'S'. 'Main(1)' raised event 'a with payload (3)' in state 'S'. diff --git a/Tst/RegressionTests/Feature1SMLevelDecls/Correct/ParamTest/ExpectedParametricTests.txt b/Tst/RegressionTests/Feature1SMLevelDecls/Correct/ParamTest/ExpectedParametricTests.txt new file mode 100644 index 000000000..eb985a274 --- /dev/null +++ b/Tst/RegressionTests/Feature1SMLevelDecls/Correct/ParamTest/ExpectedParametricTests.txt @@ -0,0 +1,69 @@ +BasicNonParametricTest +FullCartesianProductParametricTest___g1_1__g2_3__g3_5__g4_7 +FullCartesianProductParametricTest___g1_2__g2_3__g3_5__g4_7 +FullCartesianProductParametricTest___g1_1__g2_4__g3_5__g4_7 +FullCartesianProductParametricTest___g1_2__g2_4__g3_5__g4_7 +FullCartesianProductParametricTest___g1_1__g2_3__g3_6__g4_7 +FullCartesianProductParametricTest___g1_2__g2_3__g3_6__g4_7 +FullCartesianProductParametricTest___g1_1__g2_4__g3_6__g4_7 +FullCartesianProductParametricTest___g1_2__g2_4__g3_6__g4_7 +FullCartesianProductParametricTest___g1_1__g2_3__g3_5__g4_8 +FullCartesianProductParametricTest___g1_2__g2_3__g3_5__g4_8 +FullCartesianProductParametricTest___g1_1__g2_4__g3_5__g4_8 +FullCartesianProductParametricTest___g1_2__g2_4__g3_5__g4_8 +FullCartesianProductParametricTest___g1_1__g2_3__g3_6__g4_8 +FullCartesianProductParametricTest___g1_2__g2_3__g3_6__g4_8 +FullCartesianProductParametricTest___g1_1__g2_4__g3_6__g4_8 +FullCartesianProductParametricTest___g1_2__g2_4__g3_6__g4_8 +ParametricTestWithAssumption___g1_1__g2_3__g3_5__g4_7 +ParametricTestWithAssumption___g1_2__g2_3__g3_5__g4_7 +ParametricTestWithAssumption___g1_1__g2_4__g3_5__g4_7 +ParametricTestWithAssumption___g1_2__g2_4__g3_5__g4_7 +ParametricTestWithAssumption___g1_1__g2_3__g3_6__g4_7 +ParametricTestWithAssumption___g1_2__g2_3__g3_6__g4_7 +ParametricTestWithAssumption___g1_1__g2_4__g3_6__g4_7 +ParametricTestWithAssumption___g1_2__g2_4__g3_6__g4_7 +ParametricTestWithAssumption___g1_1__g2_3__g3_5__g4_8 +ParametricTestWithAssumption___g1_2__g2_3__g3_5__g4_8 +ParametricTestWithAssumption___g1_1__g2_4__g3_5__g4_8 +ParametricTestWithAssumption___g1_2__g2_4__g3_5__g4_8 +ParametricTestWithAssumption___g1_1__g2_3__g3_6__g4_8 +ParametricTestWithAssumption___g1_2__g2_3__g3_6__g4_8 +ParametricTestWithAssumption___g1_1__g2_4__g3_6__g4_8 +ParametricTestWithAssumption___g1_2__g2_4__g3_6__g4_8 +ParametricTestWithBoolAssumption___g1_1__g2_3__g3_5__g4_7__b1_False +ParametricTestWithBoolAssumption___g1_2__g2_3__g3_5__g4_7__b1_False +ParametricTestWithBoolAssumption___g1_1__g2_4__g3_5__g4_7__b1_False +ParametricTestWithBoolAssumption___g1_2__g2_4__g3_5__g4_7__b1_False +ParametricTestWithBoolAssumption___g1_1__g2_3__g3_6__g4_7__b1_False +ParametricTestWithBoolAssumption___g1_2__g2_3__g3_6__g4_7__b1_False +ParametricTestWithBoolAssumption___g1_1__g2_4__g3_6__g4_7__b1_False +ParametricTestWithBoolAssumption___g1_2__g2_4__g3_6__g4_7__b1_False +ParametricTestWithBoolAssumption___g1_1__g2_3__g3_5__g4_8__b1_False +ParametricTestWithBoolAssumption___g1_2__g2_3__g3_5__g4_8__b1_False +ParametricTestWithBoolAssumption___g1_1__g2_4__g3_5__g4_8__b1_False +ParametricTestWithBoolAssumption___g1_2__g2_4__g3_5__g4_8__b1_False +ParametricTestWithBoolAssumption___g1_1__g2_3__g3_6__g4_8__b1_False +ParametricTestWithBoolAssumption___g1_2__g2_3__g3_6__g4_8__b1_False +ParametricTestWithBoolAssumption___g1_1__g2_4__g3_6__g4_8__b1_False +ParametricTestWithBoolAssumption___g1_2__g2_4__g3_6__g4_8__b1_False +TWise1CoverageTest___g1_1__g2_3__g3_5__g4_7__b1_True +TWise1CoverageTest___g1_2__g2_4__g3_6__g4_8__b1_False +TWise2CoverageTest___g1_1__g2_3__g3_5__g4_7__b1_True +TWise2CoverageTest___g1_2__g2_4__g3_6__g4_8__b1_True +TWise2CoverageTest___g1_2__g2_4__g3_5__g4_7__b1_False +TWise2CoverageTest___g1_1__g2_3__g3_6__g4_8__b1_False +TWise2CoverageTest___g1_2__g2_3__g3_6__g4_7__b1_True +TWise2CoverageTest___g1_1__g2_4__g3_5__g4_8__b1_True +TWise3CoverageTest___g1_1__g2_3__g3_5__g4_7__b1_True +TWise3CoverageTest___g1_2__g2_4__g3_6__g4_7__b1_True +TWise3CoverageTest___g1_2__g2_3__g3_5__g4_8__b1_False +TWise3CoverageTest___g1_1__g2_4__g3_6__g4_8__b1_False +TWise3CoverageTest___g1_1__g2_4__g3_5__g4_8__b1_True +TWise3CoverageTest___g1_2__g2_3__g3_6__g4_8__b1_True +TWise3CoverageTest___g1_2__g2_4__g3_5__g4_7__b1_False +TWise3CoverageTest___g1_1__g2_3__g3_6__g4_7__b1_False +TWise3CoverageTest___g1_2__g2_3__g3_5__g4_7__b1_True +TWise3CoverageTest___g1_1__g2_4__g3_6__g4_7__b1_True +TWise3CoverageTest___g1_1__g2_3__g3_5__g4_8__b1_False +TWise3CoverageTest___g1_2__g2_4__g3_6__g4_8__b1_False \ No newline at end of file diff --git a/Tst/RegressionTests/Feature1SMLevelDecls/Correct/ParamTest/ParamTest.p b/Tst/RegressionTests/Feature1SMLevelDecls/Correct/ParamTest/ParamTest.p new file mode 100644 index 000000000..104066832 --- /dev/null +++ b/Tst/RegressionTests/Feature1SMLevelDecls/Correct/ParamTest/ParamTest.p @@ -0,0 +1,33 @@ +param g1 : int; +param g2 : int; +param g3 : int; +param g4 : int; + +machine Main { + var M: machine; + start state Init { + entry { + print format("global varaible g1 = {0}", g1); + print format("global varaible g2 = {0}", g2); + print format("global varaible g3 = {0}", g3); + print format("global varaible g4 = {0}", g4); + } + } +} + + +test BasicNonParametricTest [main=Main]:{Main}; + +test param (g1 in [1, 2], g2 in [3, 4], g3 in [5, 6], g4 in [7, 8]) FullCartesianProductParametricTest [main=Main]:{Main}; + +test param (g1 in [1, 2], g2 in [3, 4], g3 in [5, 6], g4 in [7, 8]) assume (g1 + g2 < g3 + g4) ParametricTestWithAssumption [main=Main]:{Main}; + +param b1: bool; + +test param (g1 in [1, 2], g2 in [3, 4], g3 in [5, 6], g4 in [7, 8], b1 in [true, false]) assume (b1 == (g1 + g2 > g3 + g4)) ParametricTestWithBoolAssumption [main=Main]:{Main}; + +test param (g1 in [1, 2], g2 in [3, 4], g3 in [5, 6], g4 in [7, 8], b1 in [true, false]) (1 wise) TWise1CoverageTest [main=Main]:{Main}; + +test param (g1 in [1, 2], g2 in [3, 4], g3 in [5, 6], g4 in [7, 8], b1 in [true, false]) (2 wise) TWise2CoverageTest [main=Main]:{Main}; + +test param (g1 in [1, 2], g2 in [3, 4], g3 in [5, 6], g4 in [7, 8], b1 in [true, false]) (3 wise) TWise3CoverageTest [main=Main]:{Main}; \ No newline at end of file diff --git a/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/ParamTest2/ExpectedParametricTests.txt b/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/ParamTest2/ExpectedParametricTests.txt new file mode 100644 index 000000000..798e59677 --- /dev/null +++ b/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/ParamTest2/ExpectedParametricTests.txt @@ -0,0 +1 @@ +TestParam___g1_1__g2_3 \ No newline at end of file diff --git a/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/ParamTest2/ParamTest2.p b/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/ParamTest2/ParamTest2.p new file mode 100644 index 000000000..c4fc5b68d --- /dev/null +++ b/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/ParamTest2/ParamTest2.p @@ -0,0 +1,17 @@ +param g1 : int; +param g2 : int; + + +machine Main { + var M: machine; + start state Init { + entry { + print format("global varaible g1 = {0}", g1); + print format("global varaible g2 = {0}", g2); + assert g1 != 1 && g2 != 3 ; + } + } +} + + +test param (g1 in [1], g2 in [3]) TestParam [main=Main]:{Main}; \ No newline at end of file diff --git a/Tst/RegressionTests/Feature1SMLevelDecls/StaticError/ParamTest3/ParamTest3.p b/Tst/RegressionTests/Feature1SMLevelDecls/StaticError/ParamTest3/ParamTest3.p new file mode 100644 index 000000000..4b41ef189 --- /dev/null +++ b/Tst/RegressionTests/Feature1SMLevelDecls/StaticError/ParamTest3/ParamTest3.p @@ -0,0 +1,13 @@ +param g1 : int; + +machine Main { + var M: machine; + start state Init { + entry { + print format("global varaible g1 = {0}", g1); + } + } +} + +test param (g1 in [2, 2]) Test1 [main=Main]:{Main}; + diff --git a/Tst/RegressionTests/Feature1SMLevelDecls/StaticError/ParamTest4/ParamTest4.p b/Tst/RegressionTests/Feature1SMLevelDecls/StaticError/ParamTest4/ParamTest4.p new file mode 100644 index 000000000..a1a875816 --- /dev/null +++ b/Tst/RegressionTests/Feature1SMLevelDecls/StaticError/ParamTest4/ParamTest4.p @@ -0,0 +1,13 @@ +param g1 : int; + +machine Main { + var M: machine; + start state Init { + entry { + print format("global varaible g1 = {0}", g1); + } + } +} + + +test param (g1 in [1, 2]) (0 wise) TWise0CoverageTest [main=Main]:{Main}; \ No newline at end of file diff --git a/Tst/TestParamTester/1_ClientServer/PTst/TestDriver.p b/Tst/TestParamTester/1_ClientServer/PTst/TestDriver.p index 3d2168e51..6bb747c3f 100644 --- a/Tst/TestParamTester/1_ClientServer/PTst/TestDriver.p +++ b/Tst/TestParamTester/1_ClientServer/PTst/TestDriver.p @@ -37,7 +37,7 @@ fun CreateRandomInitialAccounts(numAccounts: int) : map[int, int] var i: int; var bankBalance: map[int, int]; while(i < numAccounts) { - bankBalance[i] = choose(10) + 10; // min 10 in the account + bankBalance[i] = choose(100) + 10; // min 10 in the account i = i + 1; } return bankBalance; diff --git a/Tst/UnitTests/PCheckerLogGeneratorTests.cs b/Tst/UnitTests/PCheckerLogGeneratorTests.cs index 243b720da..7077d3e40 100644 --- a/Tst/UnitTests/PCheckerLogGeneratorTests.cs +++ b/Tst/UnitTests/PCheckerLogGeneratorTests.cs @@ -26,10 +26,10 @@ public void TestLogGenerator() var tempDir = Directory.CreateDirectory(testLogGeneratorPath); var srcPath = new FileInfo(Path.Combine(Constants.SolutionDirectory, "Tst", "RegressionTests", "Feature1SMLevelDecls", "DynamicError", "bug2", "bug2.p")); - var dllPath = Path.Combine(Constants.ScratchParentDirectory, "TestLogGenerator", "PChecker", "net8.0", "Main.dll"); + var runner = new PCheckerRunner([srcPath]); + var dllPath = Path.Combine(Constants.ScratchParentDirectory, "TestLogGenerator", "PChecker", "net8.0", "bug2.dll"); var expectedPath = Path.Combine(Constants.SolutionDirectory, "Tst", "CorrectLogs", "bugs2"); - var runner = new PCheckerRunner([srcPath]); runner.DoCompile(tempDir); var configuration = new PCheckerOptions().Parse([dllPath, "-o", tempDir.ToString()]); @@ -53,7 +53,7 @@ private void AssertLog(string generatedDir, string expectedDir) string generatedFilePath = Path.Combine(generatedDir, fileName); string expectedFilePath = Path.Combine(expectedDir, fileName); - if (fileName == "Main_0_0.trace.json") + if (fileName == "bug2_0_0.trace.json") { // Perform "Is JSON Included" check for this specific file if (!IsJsonContentIncluded(generatedFilePath, expectedFilePath)) @@ -61,6 +61,17 @@ private void AssertLog(string generatedDir, string expectedDir) Assert.Fail($"Test Failed \nContent of {expectedFilePath} is not fully included in {generatedFilePath}"); } } + else if (fileName == "bug2_0_0.txt") + { + // Perform "Is text included" check for this specific file + var expectedContent = File.ReadAllText(expectedFilePath); + var generatedContent = File.ReadAllText(generatedFilePath); + + if (!generatedContent.Contains(expectedContent)) + { + Assert.Fail($"Test Failed \nExpected content from {expectedFilePath} not found in {generatedFilePath}"); + } + } else { // Perform exact match for other files @@ -128,4 +139,4 @@ private static bool IsSubset(JToken subset, JToken superset) return false; } -} \ No newline at end of file +} diff --git a/Tst/UnitTests/Runners/PCheckerRunner.cs b/Tst/UnitTests/Runners/PCheckerRunner.cs index 974a8e818..0a3668a00 100644 --- a/Tst/UnitTests/Runners/PCheckerRunner.cs +++ b/Tst/UnitTests/Runners/PCheckerRunner.cs @@ -2,7 +2,12 @@ using System.Collections.Generic; using System.IO; using System.Linq; +using System.Reflection; +using System.Runtime.Loader; using System.Threading; +using PChecker; +using PChecker.SystematicTesting; +using Plang; using Plang.Compiler; using UnitTests.Core; @@ -10,24 +15,39 @@ namespace UnitTests.Runners { internal class PCheckerRunner : ICompilerTestRunner { + private static readonly object CheckerLock = new object(); + private static readonly object RunTestLock = new object(); private readonly FileInfo[] nativeSources; private readonly FileInfo[] sources; + private readonly string sourceDirectoryName; public PCheckerRunner(FileInfo[] sources) { this.sources = sources; nativeSources = new FileInfo[] { }; + this.sourceDirectoryName = GetSourceDirectoryName(sources); } public PCheckerRunner(FileInfo[] sources, FileInfo[] nativeSources) { this.sources = sources; this.nativeSources = nativeSources; + this.sourceDirectoryName = GetSourceDirectoryName(sources); + } + + private string GetSourceDirectoryName(FileInfo[] sources) + { + var pFile = sources.FirstOrDefault(f => f.Extension == ".p"); + if (pFile?.Directory != null) + { + return pFile.Directory.Name; + } + // Fallback to GUID if no .p file found or no directory + return $"Test_{Guid.NewGuid():N}"; } private void FileCopy(string src, string target, bool overwrite) { - // during parallel testing we might get "The process cannot access the file because it is being used by another process." var retries = 5; while (retries-- > 0) { @@ -52,123 +72,208 @@ private void FileCopy(string src, string target, bool overwrite) stdout = ""; stderr = ""; - // path to generated code DirectoryInfo scratchDirectoryGenerated = Directory.CreateDirectory(Path.Combine(scratchDirectory.FullName, "PChecker")); - // Do not want to use the auto-generated Test.cs file - CreateFileWithMainFunction(scratchDirectoryGenerated); - // Do not want to use the auto-generated csproj file - CreateCSProjFile(scratchDirectoryGenerated); - // copy the foreign code to the folder + foreach (var nativeFile in nativeSources) { FileCopy(nativeFile.FullName, Path.Combine(scratchDirectoryGenerated.FullName, nativeFile.Name), true); } var exitCode = DoCompile(scratchDirectory); - - if (exitCode == 0) + if (exitCode != 0) { - exitCode = RunPChecker(scratchDirectoryGenerated.FullName, - Path.Combine(scratchDirectoryGenerated.FullName, "./net8.0/Main.dll"), out var testStdout, out var testStderr); - stdout += testStdout; - stderr += testStderr; + return exitCode; } - else + + + // Step 2: Parametric tests + string dllPath = Path.Combine(scratchDirectoryGenerated.FullName, $"./net8.0/{sourceDirectoryName}.dll"); + var pFile = sources.FirstOrDefault(f => f.Extension == ".p"); + var sourceDirectory = pFile?.Directory; + if (sourceDirectory.Name.ToLowerInvariant().Contains("param")) { - // compilation returned unexpected error - exitCode = 2; + var expectedFile = Path.Combine(sourceDirectory.FullName, "ExpectedParametricTests.txt"); + return ValidateParametricTestOutput(dllPath, expectedFile, out stdout, out stderr); } + // Step 3: Check + var config = CheckerConfiguration.Create() + .WithTestingIterations(1000) + .WithMaxSchedulingSteps(1000); + + exitCode = RunCheckerInProcess(config, dllPath, "DefaultImpl", out var testStdout, out var testStderr); + stdout += testStdout; + stderr += testStderr; return exitCode; - } - private void CreateCSProjFile(DirectoryInfo scratchDirectory) - { - const string csprojTemplate = @" - - - net8.0 - - Exe - - latest - . - - - - -"; - using var outputFile = new StreamWriter(Path.Combine(scratchDirectory.FullName, "Main.csproj"), false); - outputFile.WriteLine(csprojTemplate); } - private void CreateFileWithMainFunction(DirectoryInfo dir) + private int ValidateParametricTestOutput(string dllPath, string expectedFilePath, out string stdout, out string stderr) { - var testCode = @" -using PChecker; -using PChecker.SystematicTesting; -using System; -using System.Linq; + stdout = string.Empty; + stderr = string.Empty; -namespace PImplementation -{ - public class _TestRegression { - public static void Main(string[] args) - { - CheckerConfiguration checkerConfiguration = CheckerConfiguration.Create().WithTestingIterations(1000); - checkerConfiguration.WithMaxSchedulingSteps(1000); - TestingEngine engine = TestingEngine.Create(checkerConfiguration, DefaultImpl.Execute); - engine.Run(); - string bug = engine.TestReport.BugReports.FirstOrDefault(); - if (bug != null) + if (!File.Exists(expectedFilePath)) { - Console.WriteLine(bug); - Environment.Exit(1); + stderr = $"ExpectedParametricTests.txt not found at: {expectedFilePath}."; + return 1; } - Environment.Exit(0); - - // for debugging: - /* For replaying a bug and single stepping - CheckerConfiguration checkerConfiguration = CheckerConfiguration.Create(); - checkerConfiguration.WithVerbosityEnabled(true); - // update the path to the schedule file. - checkerConfiguration.WithReplayStrategy(""AfterNewUpdate.schedule""); - TestingEngine engine = TestingEngine.Create(checkerConfiguration, DefaultImpl.Execute); - engine.Run(); - string bug = engine.TestReport.BugReports.FirstOrDefault(); - if (bug != null) + + // Step 1: Run with --list-tests to get console output + var listArgs = new[] { - Console.WriteLine(bug); + "check", + dllPath, + "--list-tests" + }; + + var exitCode = RunCommandLineWithArgs(listArgs, out var checkerOut, out var checkerErr); + stdout += checkerOut; + stderr += checkerErr; + + if (exitCode != 0) + { + stderr += "\nFailed to list parametric tests."; + return exitCode; } - */ - } - } -}"; - using (var outputFile = new StreamWriter(Path.Combine(dir.FullName, "Test.cs"), false)) + + // Step 2: Load expected lines (ignoring empty lines and comments) + var expectedLines = File.ReadAllLines(expectedFilePath) + .Select(line => line.Trim()) + .Where(line => !string.IsNullOrEmpty(line) && !line.StartsWith("#")) + .ToList(); + + // Step 3: Verify each expected line appears somewhere in the checker output + var missing = expectedLines + .Where(expected => !checkerOut.Contains(expected)) + .ToList(); + + if (missing.Any()) { - outputFile.WriteLine(testCode); + stderr += "\nSome expected lines were not found in the output:"; + stderr += $"\nMissing: {string.Join(", ", missing)}"; + return 1; + } + + + if (expectedLines.Count != 1) + { return 0; } + + var config = CheckerConfiguration.Create() + .WithTestingIterations(1000) + .WithMaxSchedulingSteps(1000); + config.TestCaseName = expectedLines[0]; + + exitCode = RunCheckerInProcess(config, dllPath, "DefaultImpl", out var testStdout, out var testStderr); + stdout += testStdout; + stderr += testStderr; + return exitCode; } - private int RunPChecker(string directory, string dllPath, out string stdout, out string stderr) + public int RunCommandLineWithArgs(string[] args, out string stdout, out string stderr) { - return ProcessHelper.RunWithOutput(directory, out stdout, out stderr, "dotnet", dllPath); + stdout = string.Empty; + stderr = string.Empty; + + lock (CheckerLock) + { + var originalOut = Console.Out; + var originalErr = Console.Error; + var originalExitCode = Environment.ExitCode; + Environment.ExitCode = 0; + + using var stdOutWriter = new StringWriter(); + using var stdErrWriter = new StringWriter(); + + Console.SetOut(stdOutWriter); + Console.SetError(stdErrWriter); + try + { + CommandLine.Main(args); + + stdout = stdOutWriter.ToString(); + stderr = stdErrWriter.ToString(); + + return Environment.ExitCode; + } + catch (Exception ex) + { + stderr = $"Error during PChecker execution: {ex.Message}\nStack Trace: {ex.StackTrace}"; + return 1; + } + finally + { + Console.SetOut(originalOut); + Console.SetError(originalErr); + Environment.ExitCode = originalExitCode; + } + } } + public int RunCheckerInProcess(CheckerConfiguration configuration, string testAssemblyPath, string testMethodName, out string stdout, out string stderr) + { + stdout = ""; + stderr = ""; + + try + { + lock (CheckerLock) + { + var exitCode = 0; + var context = new AssemblyLoadContext($"ALC_{Guid.NewGuid():N}", isCollectible: true); + Assembly assembly = context.LoadFromAssemblyPath(testAssemblyPath); + + Type testClass = assembly.GetType($"PImplementation.{testMethodName}"); + if (testClass == null) + throw new Exception($"Test class not found: PImplementation.{testMethodName}"); + + MethodInfo executeMethod = testClass.GetMethod("Execute", BindingFlags.Public | BindingFlags.Static); + if (executeMethod == null) + throw new Exception($"Execute method not found in: {testClass.FullName}"); + + var del = (Action)Delegate.CreateDelegate(typeof(Action), executeMethod); + var engine = TestingEngine.Create(configuration, del); + engine.Run(); + + string bug = engine.TestReport.BugReports.FirstOrDefault(); + if (bug != null) + { + stdout += bug; + exitCode = 1; + } + + context.Unload(); + GC.Collect(); + GC.WaitForPendingFinalizers(); + + return exitCode; + } + } + catch (Exception ex) + { + stderr = $"Error running Checker: {ex.Message}"; + stdout = $"Stack Trace: {ex.StackTrace}"; + Console.WriteLine(stderr); + Console.WriteLine(stdout); + Console.Out.Flush(); + return 1; + } + } public int DoCompile(DirectoryInfo scratchDirectory) { var compiler = new Compiler(); var outputStream = new TestExecutionStream(scratchDirectory); - var compilerConfiguration = new CompilerConfiguration(outputStream, scratchDirectory, new List{CompilerOutput.PChecker}, sources.Select(x => x.FullName).ToList(), "Main", scratchDirectory); + var compilerConfiguration = new CompilerConfiguration(outputStream, scratchDirectory, new List{CompilerOutput.PChecker}, sources.Select(x => x.FullName).ToList(), sourceDirectoryName, scratchDirectory); try { return compiler.Compile(compilerConfiguration); } catch (Exception ex) { - compilerConfiguration.Output.WriteError($":\n {ex.Message}\n"); + compilerConfiguration.Output.WriteError($":\n {ex.Message} {ex.StackTrace}\n"); return 1; } } } -} \ No newline at end of file +} diff --git a/Tst/UnitTests/TestAssertions.cs b/Tst/UnitTests/TestAssertions.cs index 81924cb71..da3cce19c 100644 --- a/Tst/UnitTests/TestAssertions.cs +++ b/Tst/UnitTests/TestAssertions.cs @@ -1,5 +1,6 @@ using System; using System.IO; +using System.Threading; using NUnit.Framework; using UnitTests.Core; @@ -13,7 +14,7 @@ public static void AssertTestCase(CompilerTestCase testCase) { Console.WriteLine("Test failed!\n"); WriteOutput(stdout, stderr, exitCode); - Assert.Fail($"EXIT: {exitCode}\n{stderr}"); + Assert.Fail($"EXIT: {exitCode}\n{stderr}\n{stdout}"); } Console.WriteLine("Test succeeded!\n"); @@ -33,7 +34,22 @@ public static void SafeDeleteDirectory(DirectoryInfo toDelete) { if (toDelete.Exists) { - toDelete.Delete(true); + for (int i = 0; i < 5; i++) + { + try + { + toDelete.Delete(true); + break; + } + catch (IOException) + { + Thread.Sleep(200); + } + catch (UnauthorizedAccessException) + { + Thread.Sleep(200); + } + } } return;