Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Paramtest #1

Open
wants to merge 15 commits into
base: master
Choose a base branch
from
3 changes: 0 additions & 3 deletions .gitmodules
Original file line number Diff line number Diff line change
@@ -1,3 +0,0 @@
[submodule "Ext/libhandler"]
path = Ext/libhandler
url = https://github.com/koka-lang/libhandler.git
127 changes: 117 additions & 10 deletions Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,12 @@ public class CSharpCodeGenerator : 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)
{
Expand Down Expand Up @@ -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);
}

Expand Down Expand Up @@ -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);
Expand Down Expand Up @@ -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)
{
Expand All @@ -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);
Expand Down Expand Up @@ -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();");
Expand Down Expand Up @@ -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:
Expand Down Expand Up @@ -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)
Expand Down
2 changes: 2 additions & 0 deletions Src/PCompiler/CompilerCore/Backend/ICodeGenerator.cs
Original file line number Diff line number Diff line change
Expand Up @@ -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>
Expand Down
18 changes: 18 additions & 0 deletions Src/PCompiler/CompilerCore/DefaultTranslationErrorHandler.cs
Original file line number Diff line number Diff line change
Expand Up @@ -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)
{
Expand Down
6 changes: 6 additions & 0 deletions Src/PCompiler/CompilerCore/ITranslationErrorHandler.cs
Original file line number Diff line number Diff line change
Expand Up @@ -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);

Expand Down
2 changes: 2 additions & 0 deletions Src/PCompiler/CompilerCore/Parser/PLexer.g4
Original file line number Diff line number Diff line change
Expand Up @@ -59,6 +59,7 @@ THIS : 'this' ;
TYPE : 'type' ;
VALUES : 'values' ;
VAR : 'var' ;
CONSTANT : 'constant' ;
WHILE : 'while' ;
WITH : 'with' ;
CHOOSE : 'choose' ;
Expand All @@ -69,6 +70,7 @@ CHOOSE : 'choose' ;
MODULE : 'module' ;
IMPLEMENTATION : 'implementation' ;
TEST : 'test' ;
PARAMTEST : 'paramtest' ;
REFINES : 'refines' ;

// module constructors
Expand Down
14 changes: 13 additions & 1 deletion Src/PCompiler/CompilerCore/Parser/PParser.g4
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -192,7 +194,7 @@ expr : primitive # PrimitiveExpr
| CHOOSE LPAREN expr? RPAREN # ChooseExpr
| formatedString # StringExpr
;

formatedString : StringLiteral
| FORMAT LPAREN StringLiteral (COMMA rvalueList)? RPAREN
;
Expand Down Expand Up @@ -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
;

Expand Down
Original file line number Diff line number Diff line change
@@ -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;

Expand All @@ -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>();

Expand Down Expand Up @@ -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);
Expand Down
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
using Antlr4.Runtime;
using System.Collections.Generic;

namespace Plang.Compiler.TypeChecker.AST.Declarations
{
Expand All @@ -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; }
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ public NamedTupleExpr(ParserRuleContext sourceLocation, IReadOnlyList<IPExpr> tu
}

public IReadOnlyList<IPExpr> TupleFields { get; }

public ParserRuleContext SourceLocation { get; }

public PLanguageType Type { get; }
Expand Down
Loading