Skip to content

Commit c2b6b70

Browse files
author
Christine Zhou
committed
Modified regression tests to run in process, added test cases for parametric test
1 parent 5c77847 commit c2b6b70

File tree

19 files changed

+382
-107
lines changed

19 files changed

+382
-107
lines changed

‎.github/workflows/macosci.yml

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -24,4 +24,10 @@ jobs:
2424
- name: Build
2525
run: dotnet build --configuration Release
2626
- name: Test
27-
run: dotnet test --configuration Release
27+
run: dotnet test --configuration Release --blame-crash --blame-hang --blame-hang-timeout 300s --logger:"console;verbosity=detailed"
28+
- name: Upload Test Results
29+
uses: actions/upload-artifact@v4
30+
if: always() # This ensures it runs even after test failure
31+
with:
32+
name: test-results
33+
path: Tst/UnitTests/TestResults/**/*.xml

‎Src/PChecker/CheckerCore/Checker.cs

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@
33
using PChecker.IO.Logging;
44
using PChecker.SystematicTesting;
55
using PChecker.Testing;
6+
using PChecker.SystematicTesting;
67

78
namespace PChecker;
89

@@ -52,7 +53,12 @@ public static void Run(CheckerConfiguration configuration)
5253
switch (configuration.Mode)
5354
{
5455
case CheckerMode.BugFinding:
55-
TestingProcess.Create(configuration).Run();
56+
var testingEngine = TestingProcess.Create(configuration);
57+
if (configuration.ListTestCases)
58+
{
59+
break;
60+
}
61+
testingEngine.Run();
5662
break;
5763
case CheckerMode.Verification:
5864
case CheckerMode.Coverage:

‎Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -176,7 +176,7 @@ public static TestingEngine Create(CheckerConfiguration checkerConfiguration) =>
176176
/// <summary>
177177
/// Creates a new systematic testing engine.
178178
/// </summary>
179-
public static TestingEngine Create(CheckerConfiguration checkerConfiguration, Assembly assembly)
179+
private static TestingEngine Create(CheckerConfiguration checkerConfiguration, Assembly assembly)
180180
{
181181
if (checkerConfiguration.ListTestCases)
182182
{
@@ -190,7 +190,7 @@ public static TestingEngine Create(CheckerConfiguration checkerConfiguration, As
190190
Console.Out.WriteLine($"{mi.DeclaringType.Name}");
191191
}
192192

193-
Environment.Exit(0);
193+
return null;
194194
}
195195
catch
196196
{

‎Src/PCompiler/CompilerCore/Backend/PChecker/PCheckerCodeGenerator.cs

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,8 @@ public class PCheckerCodeGenerator : ICodeGenerator
2222
/// This compiler has a compilation stage.
2323
/// </summary>
2424
public bool HasCompilationStage => true;
25-
private static List<Variable> _globalParams = [];
25+
[ThreadStatic]
26+
private static List<Variable> _globalParams;
2627

2728
private string GetGlobalParamAndLocalVariableName(CompilationContext context, Variable v)
2829
{

‎Src/PCompiler/CompilerCore/TypeChecker/ParamAssignment.cs

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -110,6 +110,11 @@ private static Dictionary<Variable, IPExpr> IndexDic2Dic(List<Variable> globalPa
110110
foreach (var (k, i) in indexDic)
111111
{
112112
var values = paramExprDic[k];
113+
if (!globalParams.Any(v => v.Name == k))
114+
{
115+
throw new Exception($"Variable name '{k}' not found in globalParams. " +
116+
$"GlobalParams are: [{string.Join(", ", globalParams.Select(v => v.Name))}]");
117+
}
113118
var variable = globalParams.First(v => v.Name == k);
114119
if (i >= values.Count) throw new ArgumentException("Index out of range in global variable config.");
115120
dic[variable] = values[i];

‎Src/PCompiler/CompilerCore/TypeChecker/ParamVisitor.cs

Lines changed: 13 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -46,16 +46,25 @@ public override IPExpr VisitSeqLiteralBody([NotNull] PParser.SeqLiteralBodyConte
4646
if (context.primitive() != null)
4747
{
4848
var values = context.primitive().Select(Visit).ToList();
49-
if (values.Count == 0) return new SeqLiteralExpr(context, values, PrimitiveType.Int);
50-
// Console.WriteLine($"value[0] = {values[0].GetType()}");
49+
50+
if (values.Count == 2 &&
51+
values[0] is IntLiteralExpr first &&
52+
values[1] is IntLiteralExpr second &&
53+
first.Value == second.Value)
54+
{
55+
throw handler.InternalError(context, new Exception("Invalid range: start and end must not be equal (e.g., [2, 2] is not allowed)")); }
56+
57+
if (values.Count == 0)
58+
return new SeqLiteralExpr(context, values, PrimitiveType.Int);
59+
5160
var type = values[0].Type;
5261
foreach (var v in values.Where(v => !v.Type.Equals(type)))
5362
{
5463
throw handler.TypeMismatch(v.SourceLocation, v.Type, type);
5564
}
65+
5666
return new SeqLiteralExpr(context, values, new SequenceType(type));
57-
58-
}
67+
}
5968
if (context.seqLiteral() != null)
6069
{
6170
return Visit(context.seqLiteral());

‎Src/PCompiler/PCommandLine/CommandLine.cs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ public static class CommandLine
1717

1818
private static readonly object ConsoleLock = new object();
1919

20-
private static void Main(string[] args)
20+
public static void Main(string[] args)
2121
{
2222
// Save these so we can force output to happen even if TestingProcess has re-routed it.
2323
StdOut = Console.Out;

‎Tst/CorrectLogs/bugs2/Main.coverage.txt renamed to ‎Tst/CorrectLogs/bugs2/bug2.coverage.txt

File renamed without changes.

‎Tst/CorrectLogs/bugs2/Main_0_0.trace.json renamed to ‎Tst/CorrectLogs/bugs2/bug2_0_0.trace.json

Lines changed: 1 addition & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,4 @@
1-
[
2-
{
3-
"type": "CreateStateMachine",
4-
"details": {
5-
"log": "Main(1) was created by task \u00272\u0027.",
6-
"id": "Main(1)",
7-
"payload": "null",
8-
"clock": {
9-
"Main(1)": 1
10-
}
11-
}
12-
},
1+
[
132
{
143
"type": "StateTransition",
154
"details": {

‎Tst/CorrectLogs/bugs2/Main_0_0.txt renamed to ‎Tst/CorrectLogs/bugs2/bug2_0_0.txt

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
<TestLog> Running test 'DefaultImpl'.
2-
<CreateLog> Main(1) was created by task '2'.
31
<StateLog> Main(1) enters state 'S'.
42
<RaiseLog> 'Main(1)' raised event 'x with payload (<a,3,>)' in state 'S'.
53
<RaiseLog> 'Main(1)' raised event 'a with payload (3)' in state 'S'.

‎Tst/RegressionTests/Feature1SMLevelDecls/Correct/ParamTest/ExpectedParametricTests.txt

Lines changed: 69 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,69 @@
1+
BasicNonParametricTest
2+
FullCartesianProductParametricTest___g1_1__g2_3__g3_5__g4_7
3+
FullCartesianProductParametricTest___g1_2__g2_3__g3_5__g4_7
4+
FullCartesianProductParametricTest___g1_1__g2_4__g3_5__g4_7
5+
FullCartesianProductParametricTest___g1_2__g2_4__g3_5__g4_7
6+
FullCartesianProductParametricTest___g1_1__g2_3__g3_6__g4_7
7+
FullCartesianProductParametricTest___g1_2__g2_3__g3_6__g4_7
8+
FullCartesianProductParametricTest___g1_1__g2_4__g3_6__g4_7
9+
FullCartesianProductParametricTest___g1_2__g2_4__g3_6__g4_7
10+
FullCartesianProductParametricTest___g1_1__g2_3__g3_5__g4_8
11+
FullCartesianProductParametricTest___g1_2__g2_3__g3_5__g4_8
12+
FullCartesianProductParametricTest___g1_1__g2_4__g3_5__g4_8
13+
FullCartesianProductParametricTest___g1_2__g2_4__g3_5__g4_8
14+
FullCartesianProductParametricTest___g1_1__g2_3__g3_6__g4_8
15+
FullCartesianProductParametricTest___g1_2__g2_3__g3_6__g4_8
16+
FullCartesianProductParametricTest___g1_1__g2_4__g3_6__g4_8
17+
FullCartesianProductParametricTest___g1_2__g2_4__g3_6__g4_8
18+
ParametricTestWithAssumption___g1_1__g2_3__g3_5__g4_7
19+
ParametricTestWithAssumption___g1_2__g2_3__g3_5__g4_7
20+
ParametricTestWithAssumption___g1_1__g2_4__g3_5__g4_7
21+
ParametricTestWithAssumption___g1_2__g2_4__g3_5__g4_7
22+
ParametricTestWithAssumption___g1_1__g2_3__g3_6__g4_7
23+
ParametricTestWithAssumption___g1_2__g2_3__g3_6__g4_7
24+
ParametricTestWithAssumption___g1_1__g2_4__g3_6__g4_7
25+
ParametricTestWithAssumption___g1_2__g2_4__g3_6__g4_7
26+
ParametricTestWithAssumption___g1_1__g2_3__g3_5__g4_8
27+
ParametricTestWithAssumption___g1_2__g2_3__g3_5__g4_8
28+
ParametricTestWithAssumption___g1_1__g2_4__g3_5__g4_8
29+
ParametricTestWithAssumption___g1_2__g2_4__g3_5__g4_8
30+
ParametricTestWithAssumption___g1_1__g2_3__g3_6__g4_8
31+
ParametricTestWithAssumption___g1_2__g2_3__g3_6__g4_8
32+
ParametricTestWithAssumption___g1_1__g2_4__g3_6__g4_8
33+
ParametricTestWithAssumption___g1_2__g2_4__g3_6__g4_8
34+
ParametricTestWithBoolAssumption___g1_1__g2_3__g3_5__g4_7__b1_False
35+
ParametricTestWithBoolAssumption___g1_2__g2_3__g3_5__g4_7__b1_False
36+
ParametricTestWithBoolAssumption___g1_1__g2_4__g3_5__g4_7__b1_False
37+
ParametricTestWithBoolAssumption___g1_2__g2_4__g3_5__g4_7__b1_False
38+
ParametricTestWithBoolAssumption___g1_1__g2_3__g3_6__g4_7__b1_False
39+
ParametricTestWithBoolAssumption___g1_2__g2_3__g3_6__g4_7__b1_False
40+
ParametricTestWithBoolAssumption___g1_1__g2_4__g3_6__g4_7__b1_False
41+
ParametricTestWithBoolAssumption___g1_2__g2_4__g3_6__g4_7__b1_False
42+
ParametricTestWithBoolAssumption___g1_1__g2_3__g3_5__g4_8__b1_False
43+
ParametricTestWithBoolAssumption___g1_2__g2_3__g3_5__g4_8__b1_False
44+
ParametricTestWithBoolAssumption___g1_1__g2_4__g3_5__g4_8__b1_False
45+
ParametricTestWithBoolAssumption___g1_2__g2_4__g3_5__g4_8__b1_False
46+
ParametricTestWithBoolAssumption___g1_1__g2_3__g3_6__g4_8__b1_False
47+
ParametricTestWithBoolAssumption___g1_2__g2_3__g3_6__g4_8__b1_False
48+
ParametricTestWithBoolAssumption___g1_1__g2_4__g3_6__g4_8__b1_False
49+
ParametricTestWithBoolAssumption___g1_2__g2_4__g3_6__g4_8__b1_False
50+
TWise1CoverageTest___g1_1__g2_3__g3_5__g4_7__b1_True
51+
TWise1CoverageTest___g1_2__g2_4__g3_6__g4_8__b1_False
52+
TWise2CoverageTest___g1_1__g2_3__g3_5__g4_7__b1_True
53+
TWise2CoverageTest___g1_2__g2_4__g3_6__g4_8__b1_True
54+
TWise2CoverageTest___g1_2__g2_4__g3_5__g4_7__b1_False
55+
TWise2CoverageTest___g1_1__g2_3__g3_6__g4_8__b1_False
56+
TWise2CoverageTest___g1_2__g2_3__g3_6__g4_7__b1_True
57+
TWise2CoverageTest___g1_1__g2_4__g3_5__g4_8__b1_True
58+
TWise3CoverageTest___g1_1__g2_3__g3_5__g4_7__b1_True
59+
TWise3CoverageTest___g1_2__g2_4__g3_6__g4_7__b1_True
60+
TWise3CoverageTest___g1_2__g2_3__g3_5__g4_8__b1_False
61+
TWise3CoverageTest___g1_1__g2_4__g3_6__g4_8__b1_False
62+
TWise3CoverageTest___g1_1__g2_4__g3_5__g4_8__b1_True
63+
TWise3CoverageTest___g1_2__g2_3__g3_6__g4_8__b1_True
64+
TWise3CoverageTest___g1_2__g2_4__g3_5__g4_7__b1_False
65+
TWise3CoverageTest___g1_1__g2_3__g3_6__g4_7__b1_False
66+
TWise3CoverageTest___g1_2__g2_3__g3_5__g4_7__b1_True
67+
TWise3CoverageTest___g1_1__g2_4__g3_6__g4_7__b1_True
68+
TWise3CoverageTest___g1_1__g2_3__g3_5__g4_8__b1_False
69+
TWise3CoverageTest___g1_2__g2_4__g3_6__g4_8__b1_False

‎Tst/RegressionTests/Feature1SMLevelDecls/Correct/ParamTest/ParamTest.p

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
param g1 : int;
2+
param g2 : int;
3+
param g3 : int;
4+
param g4 : int;
5+
6+
machine Main {
7+
var M: machine;
8+
start state Init {
9+
entry {
10+
print format("global varaible g1 = {0}", g1);
11+
print format("global varaible g2 = {0}", g2);
12+
print format("global varaible g3 = {0}", g3);
13+
print format("global varaible g4 = {0}", g4);
14+
}
15+
}
16+
}
17+
18+
19+
test BasicNonParametricTest [main=Main]:{Main};
20+
21+
test param (g1 in [1, 2], g2 in [3, 4], g3 in [5, 6], g4 in [7, 8]) FullCartesianProductParametricTest [main=Main]:{Main};
22+
23+
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};
24+
25+
param b1: bool;
26+
27+
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};
28+
29+
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};
30+
31+
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};
32+
33+
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};

‎Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/ParamTest2/ExpectedParametricTests.txt

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
TestParam___g1_1__g2_3

‎Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/ParamTest2/ParamTest2.p

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
param g1 : int;
2+
param g2 : int;
3+
4+
5+
machine Main {
6+
var M: machine;
7+
start state Init {
8+
entry {
9+
print format("global varaible g1 = {0}", g1);
10+
print format("global varaible g2 = {0}", g2);
11+
assert g1 != 1 && g2 != 3 ;
12+
}
13+
}
14+
}
15+
16+
17+
test param (g1 in [1], g2 in [3]) TestParam [main=Main]:{Main};

‎Tst/RegressionTests/Feature1SMLevelDecls/StaticError/ParamTest3/ParamTest3.p

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
param g1 : int;
2+
3+
machine Main {
4+
var M: machine;
5+
start state Init {
6+
entry {
7+
print format("global varaible g1 = {0}", g1);
8+
}
9+
}
10+
}
11+
12+
test param (g1 in [2, 2]) Test1 [main=Main]:{Main};
13+

‎Tst/RegressionTests/Feature1SMLevelDecls/StaticError/ParamTest4/ParamTest4.p

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
param g1 : int;
2+
3+
machine Main {
4+
var M: machine;
5+
start state Init {
6+
entry {
7+
print format("global varaible g1 = {0}", g1);
8+
}
9+
}
10+
}
11+
12+
13+
test param (g1 in [1, 2]) (0 wise) TWise0CoverageTest [main=Main]:{Main};

‎Tst/UnitTests/PCheckerLogGeneratorTests.cs

Lines changed: 15 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -20,10 +20,10 @@ public void TestLogGenerator()
2020
var tempDir = Directory.CreateDirectory(Path.Combine(Constants.ScratchParentDirectory, "TestLogGenerator"));
2121
var srcPath = new FileInfo(Path.Combine(Constants.SolutionDirectory, "Tst", "RegressionTests",
2222
"Feature1SMLevelDecls", "DynamicError", "bug2", "bug2.p"));
23-
var dllPath = Path.Combine(Constants.ScratchParentDirectory, "TestLogGenerator", "CSharp", "net8.0", "Main.dll");
23+
var runner = new PCheckerRunner([srcPath]);
24+
var dllPath = Path.Combine(Constants.ScratchParentDirectory, "TestLogGenerator", "PChecker", "net8.0", "bug2.dll");
2425
var expectedPath = Path.Combine(Constants.SolutionDirectory, "Tst", "CorrectLogs", "bugs2");
2526

26-
var runner = new PCheckerRunner([srcPath]);
2727
runner.DoCompile(tempDir);
2828

2929
var configuration = new PCheckerOptions().Parse([dllPath, "-o", tempDir.ToString()]);
@@ -47,14 +47,25 @@ private void AssertLog(string generatedDir, string expectedDir)
4747
string generatedFilePath = Path.Combine(generatedDir, fileName);
4848
string expectedFilePath = Path.Combine(expectedDir, fileName);
4949

50-
if (fileName == "Main_0_0.trace.json")
50+
if (fileName == "bug2_0_0.trace.json")
5151
{
5252
// Perform "Is JSON Included" check for this specific file
5353
if (!IsJsonContentIncluded(generatedFilePath, expectedFilePath))
5454
{
5555
Assert.Fail($"Test Failed \nContent of {expectedFilePath} is not fully included in {generatedFilePath}");
5656
}
5757
}
58+
else if (fileName == "bug2_0_0.txt")
59+
{
60+
// Perform "Is text included" check for this specific file
61+
var expectedContent = File.ReadAllText(expectedFilePath);
62+
var generatedContent = File.ReadAllText(generatedFilePath);
63+
64+
if (!generatedContent.Contains(expectedContent))
65+
{
66+
Assert.Fail($"Test Failed \nExpected content from {expectedFilePath} not found in {generatedFilePath}");
67+
}
68+
}
5869
else
5970
{
6071
// Perform exact match for other files
@@ -122,4 +133,4 @@ private static bool IsSubset(JToken subset, JToken superset)
122133

123134
return false;
124135
}
125-
}
136+
}

0 commit comments

Comments
 (0)