Merge branch 'p-org-paramtest' into dev_p3.0/param_testcases

p-org · Dec 4, 2024 · 924eced · 924eced
2 parents d652bc0 + 658c304
commit 924eced
Show file tree

Hide file tree

Showing 33 changed files with 1,112 additions and 30 deletions.
diff --git a/.gitmodules b/.gitmodules
@@ -1,3 +0,0 @@
-[submodule "Ext/libhandler"]
-	path = Ext/libhandler
-	url = https://github.com/koka-lang/libhandler.git

diff --git a/Src/PCompiler/CompilerCore/Backend/ICodeGenerator.cs b/Src/PCompiler/CompilerCore/Backend/ICodeGenerator.cs
@@ -6,6 +6,8 @@ namespace Plang.Compiler.Backend
 {
     public interface ICodeGenerator
     {
+        public const string GlobalConfigName = "GlobalConfig";
+
         /// <summary>
         /// Generate target language source files from a P project.
         /// </summary>

diff --git a/Src/PCompiler/CompilerCore/Backend/PChecker/PCheckerCodeGenerator.cs b/Src/PCompiler/CompilerCore/Backend/PChecker/PCheckerCodeGenerator.cs
@@ -21,6 +21,12 @@ public class PCheckerCodeGenerator : ICodeGenerator
         /// This compiler has a compilation stage.
         /// </summary>
         public bool HasCompilationStage => true;
+        private List<Variable> _globalVariables = [];
+
+        private string GetGlobalAndLocalVariableName(CompilationContext context, Variable v)
+        {
+            return _globalVariables.Contains(v) ? $"({ICodeGenerator.GlobalConfigName}.{v.Name})" : context.Names.GetNameForDecl(v);
+        }
 
         public void Compile(ICompilerConfiguration job)
         {
@@ -91,9 +97,14 @@ private CompiledFile GenerateSource(CompilationContext context, Scope globalScop
 
             WriteSourcePrologue(context, source.Stream);
 
+            _globalVariables = globalScope.GetGlobalVariables();
+
+            DeclareGlobalConstantVariables(context, source.Stream);
+
             // write the top level declarations
             foreach (var decl in globalScope.AllDecls)
             {
+                // Console.WriteLine("top-level decl: " + decl.Name);
                 WriteDecl(context, source.Stream, decl);
             }
 
@@ -251,14 +262,37 @@ private void WriteDecl(CompilationContext context, StringWriter output, IPDecl d
 
                 case EnumElem _:
                     break;
-
+
+                case Variable _:
+                    break;
+
                 default:
                     declName = context.Names.GetNameForDecl(decl);
                     context.WriteLine(output, $"// TODO: {decl.GetType().Name} {declName}");
                     break;
             }
         }
 
+        private void DeclareGlobalConstantVariables(CompilationContext context, StringWriter output)
+        {
+            WriteNameSpacePrologue(context, output);
+            context.WriteLine(output, $"public static class {ICodeGenerator.GlobalConfigName}");
+            context.WriteLine(output, "{");
+            foreach (var v in _globalVariables)
+            {
+                if (v.Role != VariableRole.GlobalConstant)
+                {
+                    throw context.Handler.InternalError(v.SourceLocation, new ArgumentException("The role of global variable is not global."));
+                }
+                context.Write(output,
+                    $"  public static {GetCSharpType(v.Type, true)} {context.Names.GetNameForDecl(v)} = ");
+                context.Write(output, $"{GetDefaultValue(v.Type)}");
+                context.WriteLine(output, $";");
+            }
+            context.WriteLine(output, "}");
+            WriteNameSpaceEpilogue(context, output);
+        }
+
         private void WriteMonitor(CompilationContext context, StringWriter output, Machine machine)
         {
             WriteNameSpacePrologue(context, output);
@@ -310,20 +344,76 @@ private static void WriteForeignType(CompilationContext context, StringWriter ou
             context.WriteLine(output, $"// TODO: Implement the Foreign Type {declName}");
         }
 
-        private void WriteSafetyTestDecl(CompilationContext context, StringWriter output, SafetyTest safety)
+        private static string RenameSafetyTest(string name, IDictionary<string, int> indexDic)
         {
+            var postfix = $"{string.Join('_', indexDic.ToList().Select(p => $"{p.Key}_{p.Value}"))}";
+            return postfix.Length == 0 ? name : $"{name}__{postfix}";
+        }
+
+        private void WriteSingleSafetyTestDecl(CompilationContext context, StringWriter output, SafetyTest safety, IDictionary<string, int> indexDic)
+        {
+            // Console.WriteLine($"indexArr: {string.Join(',', indexDic.ToList())}");
             WriteNameSpacePrologue(context, output);
-
-            context.WriteLine(output, $"public class {context.Names.GetNameForDecl(safety)} {{");
+            var name = RenameSafetyTest(context.Names.GetNameForDecl(safety), indexDic);
+            context.WriteLine(output, $"public class {name} {{");
+            var dic = new Dictionary<Variable, IPExpr>();
+            foreach (var (k, i) in indexDic)
+            {
+                var values = safety.ParamExpr[k];
+                var variable = _globalVariables.First(v => v.Name == k);
+                if (i >= values.Count)
+                {
+                    throw context.Handler.InternalError(variable.SourceLocation, new ArgumentException("Index out of range in global variable config.")); 
+                }
+                dic[variable] = values[i];
+            }
+            WriteInitializeGlobalConstantVariables(context, output, dic);
             WriteInitializeLinkMap(context, output, safety.ModExpr.ModuleInfo.LinkMap);
             WriteInitializeInterfaceDefMap(context, output, safety.ModExpr.ModuleInfo.InterfaceDef);
             WriteInitializeMonitorObserves(context, output, safety.ModExpr.ModuleInfo.MonitorMap.Keys);
             WriteInitializeMonitorMap(context, output, safety.ModExpr.ModuleInfo.MonitorMap);
-            WriteTestFunction(context, output, safety.Main);
+            WriteTestFunction(context, output, safety.Main, true);
             context.WriteLine(output, "}");
 
             WriteNameSpaceEpilogue(context, output);
         }
+
+        private bool Next((string, int)[] indexArr, IDictionary<string, List<IPExpr>> globalConstants)
+        {
+            for (var i = 0; i < indexArr.Length; i++)
+            {
+                indexArr[i] = (indexArr[i].Item1, indexArr[i].Item2 + 1);
+                // Console.WriteLine($"globalConstants[globalVariables[{i}].Name].Count = {globalConstants[globalVariables[i].Name].Count}");
+                if (indexArr[i].Item2 < globalConstants[indexArr[i].Item1].Count) return true;
+                indexArr[i] = (indexArr[i].Item1, 0);
+            }
+            return false;
+        }
+
+        private void WriteSafetyTestDecl(CompilationContext context, StringWriter output, SafetyTest safety)
+        {
+            if (safety.ParamExpr.Count == 0)
+            {
+                WriteSingleSafetyTestDecl(context, output, safety, new Dictionary<string, int>());
+                return;
+            }
+            var globalConstants = safety.ParamExpr;
+            // Console.WriteLine($"safety.ParamExpr.Count = {safety.ParamExpr.Count}");
+            var indexArr = globalConstants.ToList().Zip(Enumerable.Repeat(0, safety.ParamExpr.Count), (x, y) => (x.Key, y)).ToArray();
+            // Console.WriteLine($"global: {string.Join(',', globalConstants.Values.Select(x => x.Count))}");
+            // Console.WriteLine($"indexArr: {string.Join(',', indexArr)}");
+
+            do
+            {
+                var indexDic = new Dictionary<string, int>();
+                for (var i = 0; i < indexArr.Length; i++)
+                {
+                    indexDic[indexArr[i].Item1] = indexArr[i].Item2;
+                }
+
+                WriteSingleSafetyTestDecl(context, output, safety, indexDic);
+            } while (Next(indexArr, globalConstants));
+        }
 
         private void WriteImplementationDecl(CompilationContext context, StringWriter output, Implementation impl)
         {
@@ -334,7 +424,7 @@ private void WriteImplementationDecl(CompilationContext context, StringWriter ou
             WriteInitializeInterfaceDefMap(context, output, impl.ModExpr.ModuleInfo.InterfaceDef);
             WriteInitializeMonitorObserves(context, output, impl.ModExpr.ModuleInfo.MonitorMap.Keys);
             WriteInitializeMonitorMap(context, output, impl.ModExpr.ModuleInfo.MonitorMap);
-            WriteTestFunction(context, output, impl.Main);
+            WriteTestFunction(context, output, impl.Main, false);
             context.WriteLine(output, "}");
 
             WriteNameSpaceEpilogue(context, output);
@@ -382,11 +472,27 @@ private void WriteInitializeEnums(CompilationContext context, StringWriter outpu
             WriteNameSpaceEpilogue(context, output);
         }
 
-        private void WriteTestFunction(CompilationContext context, StringWriter output, string main)
+        private const string InitGlobalConstantsVariablesFunctionName = "InitializeGlobalConstantVariables";
+
+        private void WriteInitializeGlobalConstantVariables(CompilationContext context, StringWriter output, IDictionary<Variable, IPExpr> dic)
+        {
+            context.WriteLine(output, $"public static void {InitGlobalConstantsVariablesFunctionName}() {{");
+            foreach (var (v, value) in dic)
+            {
+                var varName = GetGlobalAndLocalVariableName(context, v);
+                context.Write(output, $"  {varName} = ");
+                WriteExpr(context, output, value);
+                context.WriteLine(output, $";");
+            }
+            context.WriteLine(output, "}");
+        }
+
+        private void WriteTestFunction(CompilationContext context, StringWriter output, string main, bool ifInitGlobalVars)
         {
             context.WriteLine(output);
             context.WriteLine(output, "[PChecker.SystematicTesting.Test]");
             context.WriteLine(output, "public static void Execute(ControlledRuntime runtime) {");
+            if (ifInitGlobalVars) { context.WriteLine(output, $"{InitGlobalConstantsVariablesFunctionName}();"); }
             context.WriteLine(output, "PModule.runtime = runtime;");
             context.WriteLine(output, "PHelper.InitializeInterfaces();");
             context.WriteLine(output, "PHelper.InitializeEnums();");
@@ -1174,7 +1280,8 @@ private void WriteLValue(CompilationContext context, StringWriter output, IPExpr
                     break;
 
                 case VariableAccessExpr variableAccessExpr:
-                    context.Write(output, context.Names.GetNameForDecl(variableAccessExpr.Variable));
+                    var varName = GetGlobalAndLocalVariableName(context, variableAccessExpr.Variable);
+                    context.Write(output, varName);
                     break;
 
                 default:
@@ -1514,8 +1621,8 @@ private void WriteClone(CompilationContext context, StringWriter output, IExprTe
                 return;
             }
 
-            var varName = context.Names.GetNameForDecl(variableRef.Variable);
-            context.Write(output, $"(({GetCSharpType(variableRef.Type)})((IPValue){varName})?.Clone())");
+            var varName = GetGlobalAndLocalVariableName(context, variableRef.Variable);
+            context.Write(output, $"(({GetCSharpType(variableRef.Type)})((IPrtValue){varName})?.Clone())");
         }
 
         private string GetCSharpType(PLanguageType type, bool isVar = false)

diff --git a/Src/PCompiler/CompilerCore/DefaultTranslationErrorHandler.cs b/Src/PCompiler/CompilerCore/DefaultTranslationErrorHandler.cs
@@ -52,6 +52,24 @@ public Exception DuplicateDeclaration(ParserRuleContext location, IPDecl duplica
             return IssueError(location,
                 $"'{duplicate.Name}' duplicates declaration '{existing.Name}' at {locationResolver.GetLocation(existing.SourceLocation)}");
         }
+
+        public Exception RedeclareGlobalConstantVariable(ParserRuleContext location, IPDecl duplicate, IPDecl existing)
+        {
+            return IssueError(location,
+                $"'{duplicate.Name}' redeclares a global constant variable '{existing.Name}' at {locationResolver.GetLocation(existing.SourceLocation)}");
+        }
+
+        public Exception UndeclaredGlobalConstantVariable(ParserRuleContext location, string name)
+        {
+            return IssueError(location,
+                $"'global constant variable {name}' is not undeclared");
+        }
+
+        public Exception ModifyGlobalConstantVariable(ParserRuleContext location, IPDecl existing)
+        {
+            return IssueError(location,
+                $"try to modify a global constant variable '{existing.Name}' at {locationResolver.GetLocation(existing.SourceLocation)}");
+        }
 
         public Exception IncorrectArgumentCount(ParserRuleContext location, int actualCount, int expectedCount)
         {

diff --git a/Src/PCompiler/CompilerCore/ITranslationErrorHandler.cs b/Src/PCompiler/CompilerCore/ITranslationErrorHandler.cs
@@ -23,6 +23,12 @@ Exception DuplicateStartState(
         Exception DuplicateStateEntry(ParserRuleContext location, Function existingHandler, State state);
 
         Exception DuplicateDeclaration(ParserRuleContext location, IPDecl duplicate, IPDecl existing);
+
+        Exception RedeclareGlobalConstantVariable(ParserRuleContext location, IPDecl duplicate, IPDecl existing);
+
+        Exception UndeclaredGlobalConstantVariable(ParserRuleContext location, string name);
+
+        Exception ModifyGlobalConstantVariable(ParserRuleContext location, IPDecl existing);
 
         Exception IncorrectArgumentCount(ParserRuleContext location, int actualCount, int expectedCount);
 

diff --git a/Src/PCompiler/CompilerCore/Parser/PLexer.g4 b/Src/PCompiler/CompilerCore/Parser/PLexer.g4
@@ -59,6 +59,7 @@ THIS      : 'this' ;
 TYPE      : 'type' ;
 VALUES    : 'values' ;
 VAR       : 'var' ;
+CONSTANT       : 'constant' ;
 WHILE     : 'while' ;
 WITH      : 'with' ;
 CHOOSE    : 'choose' ;
@@ -69,6 +70,7 @@ CHOOSE    : 'choose' ;
 MODULE         : 'module' ;
 IMPLEMENTATION : 'implementation' ;
 TEST           : 'test' ;
+PARAMTEST      : 'paramtest' ;
 REFINES        : 'refines' ;
 
 // module constructors

diff --git a/Src/PCompiler/CompilerCore/Parser/PParser.g4 b/Src/PCompiler/CompilerCore/Parser/PParser.g4
@@ -60,8 +60,10 @@ topDecl : typeDefDecl
         | namedModuleDecl
         | testDecl
         | implementationDecl
+        | globalValDecl
         ;
 
+globalValDecl : CONSTANT idenList COLON type SEMI ;
 
 typeDefDecl : TYPE name=iden SEMI # ForeignTypeDef
             | TYPE name=iden ASSIGN type SEMI # PTypeDef
@@ -192,7 +194,7 @@ expr : primitive                                      # PrimitiveExpr
 	 | CHOOSE LPAREN expr? RPAREN					  # ChooseExpr
 	 | formatedString								  # StringExpr
      ;
-
+     
 formatedString	:	StringLiteral
 				|	FORMAT LPAREN StringLiteral (COMMA rvalueList)? RPAREN
 				;	
@@ -241,8 +243,18 @@ modExpr : LPAREN modExpr RPAREN												  # ParenModuleExpr
 bindExpr : (mName=iden | mName=iden RARROW iName=iden) ;
 
 namedModuleDecl : MODULE name=iden ASSIGN modExpr SEMI ;
+seqLiteralBody : primitive
+             | seqLiteral 
+             | primitive (COMMA primitive)+ 
+             ;
+seqLiteral : LBRACK seqLiteralBody RBRACK;
+paramBody : name=iden IN value=seqLiteral
+          | name=iden IN value=seqLiteral (COMMA names=iden IN value=seqLiteral)+
+          ;
+param : LPAREN paramBody RPAREN;
 
 testDecl : TEST testName=iden (LBRACK MAIN ASSIGN mainMachine=iden RBRACK) COLON modExpr SEMI                  # SafetyTestDecl
+         | PARAMTEST globalParam=param testName=iden (LBRACK MAIN ASSIGN mainMachine=iden RBRACK) COLON modExpr SEMI # ParametricSafetyTestDecl
          | TEST testName=iden (LBRACK MAIN ASSIGN mainMachine=iden RBRACK) COLON modExpr REFINES modExpr SEMI  # RefinementTestDecl
          ;
 

diff --git a/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/Function.cs b/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/Function.cs
@@ -1,6 +1,7 @@
 using System;
 using System.Collections.Generic;
 using System.Diagnostics;
+using System.Linq;
 using Antlr4.Runtime;
 using Plang.Compiler.TypeChecker.AST.Statements;
 
@@ -22,6 +23,7 @@ public class Function : IPDecl, IHasScope
     {
         private readonly HashSet<Function> callees = new HashSet<Function>();
         private readonly HashSet<Function> callers = new HashSet<Function>();
+        private readonly List<Variable> _globalConstantVariables = [];
         private readonly List<Variable> localVariables = new List<Variable>();
         private readonly List<Interface> createsInterfaces = new List<Interface>();
 
@@ -66,6 +68,24 @@ public Function(ParserRuleContext sourceNode) : this("", sourceNode)
         public string Name { get; set; }
         public ParserRuleContext SourceLocation { get; }
 
+        public void AddGlobalConstantVariables(ITranslationErrorHandler handler, List<Variable> gvars)
+        {
+            var localNames = localVariables.Select(x => x.Name);
+            // Console.WriteLine("localNames:" + localNames.ToArray());
+            foreach (var g in gvars)
+            {
+                var res = localVariables.Find(x => x.Name == g.Name);
+                if (res == null)
+                {
+                    _globalConstantVariables.Add(g);
+                }
+                else
+                {
+                    throw handler.RedeclareGlobalConstantVariable(res.SourceLocation, res, g);
+                }
+            }
+        }
+
         public void AddLocalVariable(Variable local)
         {
             localVariables.Add(local);

diff --git a/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/SafetyTest.cs b/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/SafetyTest.cs
@@ -1,4 +1,5 @@
 using Antlr4.Runtime;
+using System.Collections.Generic;
 
 namespace Plang.Compiler.TypeChecker.AST.Declarations
 {
@@ -12,6 +13,8 @@ public SafetyTest(ParserRuleContext sourceNode, string testName)
 
         public string Main { get; set; }
         public IPModuleExpr ModExpr { get; set; }
+
+        public IDictionary<string, List<IPExpr>> ParamExpr { get; set; }
         public string Name { get; }
         public ParserRuleContext SourceLocation { get; }
     }

diff --git a/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/Variable.cs b/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/Variable.cs
@@ -26,6 +26,7 @@ public enum VariableRole
         Local = 1 << 0,
         Param = 1 << 1,
         Field = 1 << 2,
-        Temp = 1 << 3
+        Temp = 1 << 3,
+        GlobalConstant = 1 << 4
     }
 }
diff --git a/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/NamedTupleExpr.cs b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/NamedTupleExpr.cs
@@ -14,7 +14,7 @@ public NamedTupleExpr(ParserRuleContext sourceLocation, IReadOnlyList<IPExpr> tu
         }
 
         public IReadOnlyList<IPExpr> TupleFields { get; }
-
+        
         public ParserRuleContext SourceLocation { get; }
 
         public PLanguageType Type { get; }
-Original file line number
+Diff line change
@@ Expand Up @@
             }
             public IReadOnlyList<IPExpr> TupleFields { get; }
             public ParserRuleContext SourceLocation { get; }
             public PLanguageType Type { get; }
@@ Expand Down @@