Skip to content

Commit 70df7a6

Browse files
zhezhouzzankushdesai
zhezhouzz
and
ankushdesai
authored
Pex param test (#855)
* Add global constant varaibles; TODO backend * Updated BuildGlobalScope * add global variable * fix global variable types * Allow multiple tests * Add int list literal syntax * add parametric test * Quick-fix * fix bad quick-fix * add rich syntax * Small merge error * Param (#833) * update assumption * fix: add deps back * refactor: constant -> param * fix * clean the code * unify normal/param/assume tests * clean the code * rename * merging safety test parser rules * clean the code * Update github CI action v2 to v3 * iUpdate github CI action v2 to v3 on ubuntu * rename variable "param" into "parameter" to avoid keyword conflicts * T-wise combinatorial test (#837) * add twise * clean the code * Solved Concerns from Lewis: + new allow twise number be 1 + unify twise number valid condition + add unit test * add new test case * unit test for ParamAssignment.IterateAssignments * merge * fix duplicate declears bug --------- Co-authored-by: Ankush Desai <[email protected]>
1 parent a03febc commit 70df7a6

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

42 files changed

+1520
-53
lines changed

‎.gitmodules

Lines changed: 0 additions & 3 deletions
This file was deleted.

‎Src/PCompiler/CompilerCore/Backend/ICodeGenerator.cs

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,8 @@ namespace Plang.Compiler.Backend
66
{
77
public interface ICodeGenerator
88
{
9+
public const string GlobalConfigName = "GlobalConfig";
10+
911
/// <summary>
1012
/// Generate target language source files from a P project.
1113
/// </summary>

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

Lines changed: 64 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,12 @@ public class PCheckerCodeGenerator : ICodeGenerator
2121
/// This compiler has a compilation stage.
2222
/// </summary>
2323
public bool HasCompilationStage => true;
24+
private static List<Variable> _globalParams = [];
25+
26+
private string GetGlobalParamAndLocalVariableName(CompilationContext context, Variable v)
27+
{
28+
return _globalParams.Contains(v) ? $"({ICodeGenerator.GlobalConfigName}.{v.Name})" : context.Names.GetNameForDecl(v);
29+
}
2430

2531
public void Compile(ICompilerConfiguration job)
2632
{
@@ -89,6 +95,10 @@ private CompiledFile GenerateSource(CompilationContext context, Scope globalScop
8995

9096
WriteSourcePrologue(context, source.Stream);
9197

98+
_globalParams = globalScope.GetGlobalVariables();
99+
100+
DeclareGlobalParams(context, source.Stream);
101+
92102
// write the top level declarations
93103
foreach (var decl in globalScope.AllDecls)
94104
{
@@ -242,22 +252,46 @@ private void WriteDecl(CompilationContext context, StringWriter output, IPDecl d
242252
break;
243253

244254
case SafetyTest safety:
245-
WriteSafetyTestDecl(context, output, safety);
255+
ParamAssignment.IterateAssignments(safety, _globalParams,
256+
assignment => WriteSafetyTestDecl(context, output, safety, assignment));
246257
break;
247258

248259
case Interface _:
249260
break;
250261

251262
case EnumElem _:
252263
break;
253-
264+
265+
case Variable _:
266+
break;
267+
254268
default:
255269
declName = context.Names.GetNameForDecl(decl);
256270
context.WriteLine(output, $"// TODO: {decl.GetType().Name} {declName}");
257271
break;
258272
}
259273
}
260274

275+
private void DeclareGlobalParams(CompilationContext context, StringWriter output)
276+
{
277+
WriteNameSpacePrologue(context, output);
278+
context.WriteLine(output, $"public static class {ICodeGenerator.GlobalConfigName}");
279+
context.WriteLine(output, "{");
280+
foreach (var v in _globalParams)
281+
{
282+
if (v.Role != VariableRole.GlobalParams)
283+
{
284+
throw context.Handler.InternalError(v.SourceLocation, new ArgumentException("The role of global variable is not global."));
285+
}
286+
context.Write(output,
287+
$" public static {GetCSharpType(v.Type, true)} {context.Names.GetNameForDecl(v)} = ");
288+
context.Write(output, $"{GetDefaultValue(v.Type)}");
289+
context.WriteLine(output, $";");
290+
}
291+
context.WriteLine(output, "}");
292+
WriteNameSpaceEpilogue(context, output);
293+
}
294+
261295
private void WriteMonitor(CompilationContext context, StringWriter output, Machine machine)
262296
{
263297
WriteNameSpacePrologue(context, output);
@@ -308,17 +342,19 @@ private static void WriteForeignType(CompilationContext context, StringWriter ou
308342
var declName = foreignType.CanonicalRepresentation;
309343
context.WriteLine(output, $"// TODO: Implement the Foreign Type {declName}");
310344
}
311-
312-
private void WriteSafetyTestDecl(CompilationContext context, StringWriter output, SafetyTest safety)
345+
346+
// For normal test, the assignment is empty dictionary
347+
private void WriteSafetyTestDecl(CompilationContext context, StringWriter output, SafetyTest safety, Dictionary<Variable, IPExpr> assignment)
313348
{
314349
WriteNameSpacePrologue(context, output);
315-
316-
context.WriteLine(output, $"public class {context.Names.GetNameForDecl(safety)} {{");
350+
var name = ParamAssignment.RenameSafetyTestByAssignment(context.Names.GetNameForDecl(safety), assignment);
351+
context.WriteLine(output, $"public class {name} {{");
352+
WriteInitializeGlobalParams(context, output, assignment);
317353
WriteInitializeLinkMap(context, output, safety.ModExpr.ModuleInfo.LinkMap);
318354
WriteInitializeInterfaceDefMap(context, output, safety.ModExpr.ModuleInfo.InterfaceDef);
319355
WriteInitializeMonitorObserves(context, output, safety.ModExpr.ModuleInfo.MonitorMap.Keys);
320356
WriteInitializeMonitorMap(context, output, safety.ModExpr.ModuleInfo.MonitorMap);
321-
WriteTestFunction(context, output, safety.Main);
357+
WriteTestFunction(context, output, safety.Main, true);
322358
context.WriteLine(output, "}");
323359

324360
WriteNameSpaceEpilogue(context, output);
@@ -333,7 +369,7 @@ private void WriteImplementationDecl(CompilationContext context, StringWriter ou
333369
WriteInitializeInterfaceDefMap(context, output, impl.ModExpr.ModuleInfo.InterfaceDef);
334370
WriteInitializeMonitorObserves(context, output, impl.ModExpr.ModuleInfo.MonitorMap.Keys);
335371
WriteInitializeMonitorMap(context, output, impl.ModExpr.ModuleInfo.MonitorMap);
336-
WriteTestFunction(context, output, impl.Main);
372+
WriteTestFunction(context, output, impl.Main, false);
337373
context.WriteLine(output, "}");
338374

339375
WriteNameSpaceEpilogue(context, output);
@@ -381,11 +417,27 @@ private void WriteInitializeEnums(CompilationContext context, StringWriter outpu
381417
WriteNameSpaceEpilogue(context, output);
382418
}
383419

384-
private void WriteTestFunction(CompilationContext context, StringWriter output, string main)
420+
private const string InitGlobalParamsFunctionName = "InitializeGlobalParams";
421+
422+
private void WriteInitializeGlobalParams(CompilationContext context, StringWriter output, IDictionary<Variable, IPExpr> dic)
423+
{
424+
context.WriteLine(output, $"public static void {InitGlobalParamsFunctionName}() {{");
425+
foreach (var (v, value) in dic)
426+
{
427+
var varName = GetGlobalParamAndLocalVariableName(context, v);
428+
context.Write(output, $" {varName} = ");
429+
WriteExpr(context, output, value);
430+
context.WriteLine(output, $";");
431+
}
432+
context.WriteLine(output, "}");
433+
}
434+
435+
private void WriteTestFunction(CompilationContext context, StringWriter output, string main, bool ifInitGlobalParams)
385436
{
386437
context.WriteLine(output);
387438
context.WriteLine(output, "[PChecker.SystematicTesting.Test]");
388439
context.WriteLine(output, "public static void Execute(ControlledRuntime runtime) {");
440+
if (ifInitGlobalParams) { context.WriteLine(output, $"{InitGlobalParamsFunctionName}();"); }
389441
context.WriteLine(output, "runtime.RegisterLog(new PCheckerLogTextFormatter());");
390442
context.WriteLine(output, "runtime.RegisterLog(new PCheckerLogJsonFormatter());");
391443
context.WriteLine(output, "PModule.runtime = runtime;");
@@ -1175,7 +1227,8 @@ private void WriteLValue(CompilationContext context, StringWriter output, IPExpr
11751227
break;
11761228

11771229
case VariableAccessExpr variableAccessExpr:
1178-
context.Write(output, context.Names.GetNameForDecl(variableAccessExpr.Variable));
1230+
var varName = GetGlobalParamAndLocalVariableName(context, variableAccessExpr.Variable);
1231+
context.Write(output, varName);
11791232
break;
11801233

11811234
default:
@@ -1515,7 +1568,7 @@ private void WriteClone(CompilationContext context, StringWriter output, IExprTe
15151568
return;
15161569
}
15171570

1518-
var varName = context.Names.GetNameForDecl(variableRef.Variable);
1571+
var varName = GetGlobalParamAndLocalVariableName(context, variableRef.Variable);
15191572
context.Write(output, $"(({GetCSharpType(variableRef.Type)})((IPValue){varName})?.Clone())");
15201573
}
15211574

‎Src/PCompiler/CompilerCore/Backend/PEx/PExCodeGenerator.cs

Lines changed: 66 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -28,6 +28,12 @@ public IEnumerable<CompiledFile> GenerateCode(ICompilerConfiguration job, Scope
2828
/// This compiler has a compilation stage.
2929
/// </summary>
3030
public bool HasCompilationStage => true;
31+
private static List<Variable> _globalParams = [];
32+
33+
private string GetGlobalParamAndLocalVariableName(Variable v)
34+
{
35+
return _globalParams.Contains(v) ? $"({ICodeGenerator.GlobalConfigName}.{v.Name})" : CompilationContext.GetVar(v.Name);
36+
}
3137

3238
public void Compile(ICompilerConfiguration job)
3339
{
@@ -103,6 +109,10 @@ private CompiledFile GenerateSource(CompilationContext context, Scope globalScop
103109
context.WriteLine(source.Stream);
104110

105111
context.WriteLine(source.Stream);
112+
113+
_globalParams = globalScope.GetGlobalVariables();
114+
115+
DeclareGlobalParams(context, source.Stream);
106116

107117
//WriteMachineTagDefs(context, source.Stream, globalScope.Machines);
108118

@@ -118,7 +128,7 @@ private CompiledFile GenerateSource(CompilationContext context, Scope globalScop
118128
WriteDecl(context, source.Stream, decl);
119129
}
120130

121-
if (!hasSafetyTest) WriteMainDriver(context, source.Stream, globalScope, decls);
131+
if (!hasSafetyTest) WriteImplementationDecl(context, source.Stream, globalScope, decls);
122132

123133
context.WriteLine(source.Stream, "PTestDriver testDriver = null;");
124134
context.WriteLine(source.Stream, "@Generated");
@@ -131,20 +141,36 @@ private CompiledFile GenerateSource(CompilationContext context, Scope globalScop
131141

132142
return source;
133143
}
144+
145+
private const string InitGlobalParamsFunctionName = "InitializeGlobalParams";
146+
147+
private void WriteInitializeGlobalParams(CompilationContext context, StringWriter output, IDictionary<Variable, IPExpr> dic)
148+
{
149+
context.WriteLine(output, $"public static void {InitGlobalParamsFunctionName}() {{");
150+
foreach (var (v, value) in dic)
151+
{
152+
var varName = GetGlobalParamAndLocalVariableName(v);
153+
context.Write(output, $" {varName} = ");
154+
WriteExpr(context, output, value);
155+
context.WriteLine(output, $";");
156+
}
157+
context.WriteLine(output, "}");
158+
}
134159

135-
private void WriteDriver(CompilationContext context, StringWriter output, string startMachine,
136-
IEnumerable<IPDecl> decls, IDictionary<Interface, Machine> interfaceDef = null)
160+
private void WriteTestFunction(CompilationContext context, StringWriter output, string startMachine,
161+
IEnumerable<IPDecl> decls, bool ifInitGlobalParams, IDictionary<Interface, Machine> interfaceDef = null)
137162
{
138-
WriteDriverConfigure(context, output, startMachine, decls, interfaceDef);
163+
WriteTestFunctionConfigure(context, output, startMachine, decls, interfaceDef, ifInitGlobalParams);
139164
context.WriteLine(output);
140165
}
141166

142-
private void WriteDriverConfigure(CompilationContext context, StringWriter output, string startMachine,
143-
IEnumerable<IPDecl> decls, IDictionary<Interface, Machine> interfaceDef)
167+
private void WriteTestFunctionConfigure(CompilationContext context, StringWriter output, string startMachine,
168+
IEnumerable<IPDecl> decls, IDictionary<Interface, Machine> interfaceDef, bool ifInitGlobalParams)
144169
{
145170
context.WriteLine(output);
146171
context.WriteLine(output, "@Generated");
147172
context.WriteLine(output, "public void configure() {");
173+
if (ifInitGlobalParams) { context.WriteLine(output, $" {InitGlobalParamsFunctionName}();"); }
148174

149175
context.WriteLine(output, $" mainMachine = {startMachine}.class;");
150176

@@ -182,7 +208,7 @@ private void WriteDriverConfigure(CompilationContext context, StringWriter outpu
182208
context.WriteLine(output, "}");
183209
}
184210

185-
private void WriteMainDriver(CompilationContext context, StringWriter output, Scope globalScope,
211+
private void WriteImplementationDecl(CompilationContext context, StringWriter output, Scope globalScope,
186212
IEnumerable<IPDecl> decls)
187213
{
188214
Machine mainMachine = null;
@@ -204,7 +230,7 @@ private void WriteMainDriver(CompilationContext context, StringWriter output, Sc
204230

205231
context.WriteLine(output, "@Generated");
206232
context.WriteLine(output, "public static class test_DefaultImpl extends PTestDriver {");
207-
WriteDriver(context, output, mainMachine.Name, decls);
233+
WriteTestFunction(context, output, mainMachine.Name, decls, false);
208234
context.WriteLine(output, "}");
209235
context.WriteLine(output);
210236
}
@@ -235,19 +261,44 @@ private void WriteDecl(CompilationContext context, StringWriter output, IPDecl d
235261
WriteEvent(context, output, ev);
236262
break;
237263
case SafetyTest safety:
238-
WriteSafetyTestDecl(context, output, safety);
264+
ParamAssignment.IterateAssignments(safety, _globalParams,
265+
assignment => WriteSafetyTestDecl(context, output, safety, assignment));
266+
break;
267+
case Variable _:
239268
break;
240269
default:
241270
context.WriteLine(output, $"// Skipping {decl.GetType().Name} '{decl.Name}'\n");
242271
break;
243272
}
244273
}
245-
246-
private void WriteSafetyTestDecl(CompilationContext context, StringWriter output, SafetyTest safety)
274+
275+
private void DeclareGlobalParams(CompilationContext context, StringWriter output)
276+
{
277+
context.WriteLine(output, "@Generated");
278+
context.WriteLine(output, $"public static class {ICodeGenerator.GlobalConfigName}");
279+
context.WriteLine(output, "{");
280+
foreach (var v in _globalParams)
281+
{
282+
if (v.Role != VariableRole.GlobalParams)
283+
{
284+
throw context.Handler.InternalError(v.SourceLocation, new ArgumentException("The role of global variable is not global."));
285+
}
286+
context.Write(output,
287+
$" public static {GetPExType(v.Type)} {v.Name} = ");
288+
context.Write(output, $"{GetDefaultValue(v.Type)}");
289+
context.WriteLine(output, $";");
290+
}
291+
context.WriteLine(output, "}");
292+
context.WriteLine(output);
293+
}
294+
295+
private void WriteSafetyTestDecl(CompilationContext context, StringWriter output, SafetyTest safety, Dictionary<Variable, IPExpr> assignment)
247296
{
248297
context.WriteLine(output, "@Generated");
249-
context.WriteLine(output, $"public static class {context.GetNameForDecl(safety)} extends PTestDriver {{");
250-
WriteDriver(context, output, safety.Main, safety.ModExpr.ModuleInfo.MonitorMap.Keys,
298+
var name = ParamAssignment.RenameSafetyTestByAssignment(context.GetNameForDecl(safety), assignment);
299+
context.WriteLine(output, $"public static class {name} extends PTestDriver {{");
300+
WriteInitializeGlobalParams(context, output, assignment);
301+
WriteTestFunction(context, output, safety.Main, safety.ModExpr.ModuleInfo.MonitorMap.Keys, true,
251302
safety.ModExpr.ModuleInfo.InterfaceDef);
252303
context.WriteLine(output, "}");
253304
context.WriteLine(output);
@@ -1416,8 +1467,7 @@ private void WriteWithLValueMutationContext(
14161467
);
14171468
break;
14181469
case VariableAccessExpr variableAccessExpr:
1419-
var name = variableAccessExpr.Variable.Name;
1420-
var unguarded = CompilationContext.GetVar(name);
1470+
var unguarded = GetGlobalParamAndLocalVariableName(variableAccessExpr.Variable);
14211471
var guardedTemp = context.FreshTempVar();
14221472

14231473
context.Write(output, $"{GetPExType(variableAccessExpr.Type)} {guardedTemp}");
@@ -1685,7 +1735,7 @@ private void WriteExpr(CompilationContext context, StringWriter output, IPExpr e
16851735
break;
16861736
}
16871737
case VariableAccessExpr variableAccessExpr:
1688-
context.Write(output, $"{CompilationContext.GetVar(variableAccessExpr.Variable.Name)}");
1738+
context.Write(output, $"{GetGlobalParamAndLocalVariableName(variableAccessExpr.Variable)}");
16891739
break;
16901740
case FunCallExpr _:
16911741
throw new InvalidOperationException(

‎Src/PCompiler/CompilerCore/DefaultTranslationErrorHandler.cs

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@
22
using System.IO;
33
using System.Linq;
44
using Antlr4.Runtime;
5+
using Antlr4.Runtime.Tree;
56
using Plang.Compiler.TypeChecker;
67
using Plang.Compiler.TypeChecker.AST;
78
using Plang.Compiler.TypeChecker.AST.Declarations;
@@ -52,6 +53,30 @@ public Exception DuplicateDeclaration(ParserRuleContext location, IPDecl duplica
5253
return IssueError(location,
5354
$"'{duplicate.Name}' duplicates declaration '{existing.Name}' at {locationResolver.GetLocation(existing.SourceLocation)}");
5455
}
56+
57+
public Exception RedeclareGlobalParam(ParserRuleContext location, IPDecl duplicate, IPDecl existing)
58+
{
59+
return IssueError(location,
60+
$"'{duplicate.Name}' redeclares a global param '{existing.Name}' at {locationResolver.GetLocation(existing.SourceLocation)}");
61+
}
62+
63+
public Exception UndeclaredGlobalParam(ParserRuleContext location, string name)
64+
{
65+
return IssueError(location,
66+
$"'global param {name}' is not undeclared");
67+
}
68+
69+
public Exception ModifyGlobalParam(ParserRuleContext location, IPDecl existing)
70+
{
71+
return IssueError(location,
72+
$"try to modify a global param '{existing.Name}' at {locationResolver.GetLocation(existing.SourceLocation)}");
73+
}
74+
75+
public Exception InvalidTwise(ParserRuleContext location, IPDecl testDecl, string errMsg)
76+
{
77+
return IssueError(location,
78+
$"invalid twise number at {locationResolver.GetLocation(testDecl.SourceLocation)}: {errMsg}");
79+
}
5580

5681
public Exception IncorrectArgumentCount(ParserRuleContext location, int actualCount, int expectedCount)
5782
{

‎Src/PCompiler/CompilerCore/ITranslationErrorHandler.cs

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
using System;
22
using System.IO;
33
using Antlr4.Runtime;
4+
using Antlr4.Runtime.Tree;
45
using Plang.Compiler.TypeChecker.AST;
56
using Plang.Compiler.TypeChecker.AST.Declarations;
67
using Plang.Compiler.TypeChecker.AST.States;
@@ -23,6 +24,14 @@ Exception DuplicateStartState(
2324
Exception DuplicateStateEntry(ParserRuleContext location, Function existingHandler, State state);
2425

2526
Exception DuplicateDeclaration(ParserRuleContext location, IPDecl duplicate, IPDecl existing);
27+
28+
Exception RedeclareGlobalParam(ParserRuleContext location, IPDecl duplicate, IPDecl existing);
29+
30+
Exception UndeclaredGlobalParam(ParserRuleContext location, string name);
31+
32+
Exception ModifyGlobalParam(ParserRuleContext location, IPDecl existing);
33+
34+
Exception InvalidTwise(ParserRuleContext location, IPDecl testDecl, string errMsg);
2635

2736
Exception IncorrectArgumentCount(ParserRuleContext location, int actualCount, int expectedCount);
2837

0 commit comments

Comments
 (0)