diff --git a/.gitmodules b/.gitmodules index 52ba41cabf..e69de29bb2 100644 --- 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 index 42c60c8a16..8055b2e8b4 100644 --- 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"; + /// /// Generate target language source files from a P project. /// diff --git a/Src/PCompiler/CompilerCore/Backend/PChecker/PCheckerCodeGenerator.cs b/Src/PCompiler/CompilerCore/Backend/PChecker/PCheckerCodeGenerator.cs index 96d3d9a2e0..709201e659 100644 --- 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. /// public bool HasCompilationStage => true; + private List _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,7 +262,10 @@ 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}"); @@ -259,6 +273,26 @@ private void WriteDecl(CompilationContext context, StringWriter output, IPDecl d } } + 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 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 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(); + 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> 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()); + 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(); + 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 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 index a9b99eee6e..50c303a3d7 100644 --- 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 index 5aea56f1d9..54002810b2 100644 --- 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 index 8f7511ac8d..c46715ecde 100644 --- 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 index dc00fca475..0512533c66 100644 --- 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 index 69ed97c4ad..9d728b8ba2 100644 --- 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 callees = new HashSet(); private readonly HashSet callers = new HashSet(); + private readonly List _globalConstantVariables = []; private readonly List localVariables = new List(); private readonly List createsInterfaces = new List(); @@ -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 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 index 4a3fce639f..515e424978 100644 --- 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> 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 index 915f15ba05..4b1757f359 100644 --- 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 } } \ No newline at end of file diff --git a/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/NamedTupleExpr.cs b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/NamedTupleExpr.cs index 5d993f36ea..297449361f 100644 --- 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 tu } public IReadOnlyList TupleFields { get; } - + public ParserRuleContext SourceLocation { get; } public PLanguageType Type { get; } diff --git a/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/SeqLiteralExpr.cs b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/SeqLiteralExpr.cs new file mode 100644 index 0000000000..759f2ed115 --- /dev/null +++ b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/SeqLiteralExpr.cs @@ -0,0 +1,15 @@ +using Antlr4.Runtime; +using Plang.Compiler.TypeChecker.Types; +using System.Collections.Generic; + +namespace Plang.Compiler.TypeChecker.AST.Expressions +{ + public class SeqLiteralExpr(ParserRuleContext sourceLocation, List values, PLanguageType type) + : IExprTerm + { + public List Value { get; } = values; + + public ParserRuleContext SourceLocation { get; } = sourceLocation; + public PLanguageType Type { get; } = type; + } +} \ No newline at end of file diff --git a/Src/PCompiler/CompilerCore/TypeChecker/Analyzer.cs b/Src/PCompiler/CompilerCore/TypeChecker/Analyzer.cs index d9679b59d9..75d0168e40 100644 --- a/Src/PCompiler/CompilerCore/TypeChecker/Analyzer.cs +++ b/Src/PCompiler/CompilerCore/TypeChecker/Analyzer.cs @@ -26,12 +26,14 @@ public static Scope AnalyzeCompilationUnit(ICompilerConfiguration config, // Step 3: Fill function bodies var allFunctions = globalScope.GetAllMethods().ToList(); + // var globalConstantVariables = globalScope.GetVariables(); foreach (var machineFunction in allFunctions) { FunctionBodyVisitor.PopulateMethod(config, machineFunction); + // machineFunction.AddGlobalConstantVariables(handler, globalConstantVariables); FunctionValidator.CheckAllPathsReturn(handler, machineFunction); } - + // Step 2: Validate no static handlers foreach (var machine in globalScope.Machines) { @@ -174,7 +176,7 @@ private static Scope BuildGlobalScope(ICompilerConfiguration config, PParser.Pro { DeclarationStubVisitor.PopulateStubs(globalScope, programUnit, nodesToDeclarations); } - + // Step 2: Validate declarations and fill with types foreach (var programUnit in programUnits) { diff --git a/Src/PCompiler/CompilerCore/TypeChecker/DeclarationStubVisitor.cs b/Src/PCompiler/CompilerCore/TypeChecker/DeclarationStubVisitor.cs index 77782e7308..21965587a4 100644 --- a/Src/PCompiler/CompilerCore/TypeChecker/DeclarationStubVisitor.cs +++ b/Src/PCompiler/CompilerCore/TypeChecker/DeclarationStubVisitor.cs @@ -29,6 +29,21 @@ public static void PopulateStubs( var visitor = new DeclarationStubVisitor(globalScope, nodesToDeclarations); visitor.Visit(context); } + + #region GlobalConstantVariables + + public override object VisitGlobalValDecl(PParser.GlobalValDeclContext context) + { + foreach (var varName in context.idenList()._names) + { + var decl = CurrentScope.Put(varName.GetText(), varName, VariableRole.GlobalConstant); + nodesToDeclarations.Put(varName, decl); + } + + return null; + } + + #endregion GlobalConstantVariables #region Events @@ -218,6 +233,17 @@ public override object VisitSafetyTestDecl([NotNull] PParser.SafetyTestDeclConte } return null; } + + public override object VisitParametricSafetyTestDecl([NotNull] PParser.ParametricSafetyTestDeclContext context) + { + var symbolName = context.testName.GetText(); + var decl = CurrentScope.Put(symbolName, context); + if (decl == null) return null; + decl.Main = context.mainMachine?.GetText(); + nodesToDeclarations.Put(context, decl); + return null ; + } + public override object VisitRefinementTestDecl([NotNull] PParser.RefinementTestDeclContext context) { diff --git a/Src/PCompiler/CompilerCore/TypeChecker/DeclarationVisitor.cs b/Src/PCompiler/CompilerCore/TypeChecker/DeclarationVisitor.cs index f29e8eb273..1fd9fa82ba 100644 --- a/Src/PCompiler/CompilerCore/TypeChecker/DeclarationVisitor.cs +++ b/Src/PCompiler/CompilerCore/TypeChecker/DeclarationVisitor.cs @@ -16,13 +16,18 @@ public class DeclarationVisitor : PParserBaseVisitor private readonly StackProperty currentMachine = new StackProperty(); private readonly StackProperty currentScope; private readonly ParseTreeProperty nodesToDeclarations; - + private IDictionary globalConstantVariables = new Dictionary(); + private DeclarationVisitor( ITranslationErrorHandler handler, Scope topLevelScope, ParseTreeProperty nodesToDeclarations) { Handler = handler; + foreach (var variable in topLevelScope.Variables) + { + globalConstantVariables.Add(variable.Name, variable); + } currentScope = new StackProperty(topLevelScope); this.nodesToDeclarations = nodesToDeclarations; } @@ -41,6 +46,35 @@ public static void PopulateDeclarations( visitor.Visit(context); } + private void CheckGlobalConstantVariableRedeclare(Variable decl) + { + if (globalConstantVariables.TryGetValue(decl.Name, out var existingDecl)) + { + throw Handler.RedeclareGlobalConstantVariable(decl.SourceLocation, decl, existingDecl); + } + } + + #region GlobalConstantVariables + + public override object VisitGlobalValDecl(PParser.GlobalValDeclContext context) + { + // COLON type + var variableType = ResolveType(context.type()); + // Console.WriteLine("variableType:" + variableType); + + // VAR idenList + foreach (var t in context.idenList()._names) + { + var variable = (Variable) nodesToDeclarations.Get(t); + variable.Type = variableType; + currentScope.Value.Update(variable); + } + // SEMI + return globalConstantVariables; + } + + #endregion GlobalConstantVariables + #region Events public override object VisitEventDecl(PParser.EventDeclContext context) @@ -389,6 +423,8 @@ public override object VisitVarDecl(PParser.VarDeclContext context) for (var i = 0; i < varNameCtxs.Count; i++) { var variable = (Variable) nodesToDeclarations.Get(varNameCtxs[i]); + // Console.WriteLine("Local Variable:" + variable.Name); + CheckGlobalConstantVariableRedeclare(variable); variable.Type = variableType; variables[i] = variable; } diff --git a/Src/PCompiler/CompilerCore/TypeChecker/ExprVisitor.cs b/Src/PCompiler/CompilerCore/TypeChecker/ExprVisitor.cs index ff6d1e2d0d..91bcfd6d5b 100644 --- a/Src/PCompiler/CompilerCore/TypeChecker/ExprVisitor.cs +++ b/Src/PCompiler/CompilerCore/TypeChecker/ExprVisitor.cs @@ -502,6 +502,8 @@ public override IPExpr VisitPrimitive(PParser.PrimitiveContext context) if (context.iden() != null) { var symbolName = context.iden().GetText(); + // Console.WriteLine("Looking up " + symbolName); + // Console.WriteLine("Table: " + String.Join(", ", table.GetVariables().Select(x =>x.Name).ToArray())); if (table.Lookup(symbolName, out Variable variable)) { return new VariableAccessExpr(context, variable); @@ -516,7 +518,7 @@ public override IPExpr VisitPrimitive(PParser.PrimitiveContext context) { return new EventRefExpr(context, evt); } - + throw handler.MissingDeclaration(context.iden(), "variable, enum element, or event", symbolName); } @@ -659,7 +661,7 @@ public override IPExpr VisitStringExpr(PParser.StringExprContext context) public override IPExpr VisitVarLvalue(PParser.VarLvalueContext context) { var varName = context.name.GetText(); - if (!table.Lookup(varName, out Variable variable)) + if (!table.LookupLvalue(handler, varName, context, out Variable variable)) { throw handler.MissingDeclaration(context, "variable", varName); } diff --git a/Src/PCompiler/CompilerCore/TypeChecker/FunctionBodyVisitor.cs b/Src/PCompiler/CompilerCore/TypeChecker/FunctionBodyVisitor.cs index 2cb0b21eb3..063d857327 100644 --- a/Src/PCompiler/CompilerCore/TypeChecker/FunctionBodyVisitor.cs +++ b/Src/PCompiler/CompilerCore/TypeChecker/FunctionBodyVisitor.cs @@ -53,6 +53,9 @@ public override object VisitFunctionBody(PParser.FunctionBodyContext context) { Visit(varDeclContext); } + + // Then we validate this scope doesn't redeclare the global constant variables + method.Scope.ValidateGlobalConstantVariablesUnique(config.Handler); // Build the statement trees var statementVisitor = new StatementVisitor(config, machine, method); diff --git a/Src/PCompiler/CompilerCore/TypeChecker/ModuleExprVisitor.cs b/Src/PCompiler/CompilerCore/TypeChecker/ModuleExprVisitor.cs index 74e4e7220d..d4b0a49d4e 100644 --- a/Src/PCompiler/CompilerCore/TypeChecker/ModuleExprVisitor.cs +++ b/Src/PCompiler/CompilerCore/TypeChecker/ModuleExprVisitor.cs @@ -5,7 +5,9 @@ using Antlr4.Runtime.Misc; using Plang.Compiler.TypeChecker.AST; using Plang.Compiler.TypeChecker.AST.Declarations; +using Plang.Compiler.TypeChecker.AST.Expressions; using Plang.Compiler.TypeChecker.AST.ModuleExprs; +using Plang.Compiler.TypeChecker.Types; namespace Plang.Compiler.TypeChecker { @@ -16,6 +18,7 @@ public static void PopulateAllModuleExprs( Scope globalScope) { var modExprVisitor = new ModuleExprVisitor(handler, globalScope); + var paramExprVisitor = new ParamExprVisitor(handler); // first do all the named modules foreach (var mod in globalScope.NamedModules) @@ -27,10 +30,37 @@ public static void PopulateAllModuleExprs( // all the test declarations foreach (var test in globalScope.SafetyTests) { - var context = (PParser.SafetyTestDeclContext)test.SourceLocation; - test.ModExpr = modExprVisitor.Visit(context.modExpr()); + if (test.ParamExpr == null) + { + var context = (PParser.ParametricSafetyTestDeclContext)test.SourceLocation; + test.ModExpr = modExprVisitor.Visit(context.modExpr()); + var expr = (NamedTupleExpr)paramExprVisitor.Visit(context.globalParam); + var names = ((NamedTupleType)expr.Type).Names.ToList(); + var values = expr.TupleFields.ToList(); + IDictionary> dic = new Dictionary>(); + foreach (var (name, value) in names.Zip(values)) + { + var v = globalScope.Variables.FirstOrDefault(x => x.Name == name); + if (v == null) + { + throw handler.UndeclaredGlobalConstantVariable(context.globalParam, name); + } + var expectedType = new SequenceType(v.Type); + if (!value.Type.Equals(expectedType)) + { + throw handler.TypeMismatch(value.SourceLocation, value.Type, expectedType); + } + dic[name] = ((SeqLiteralExpr)value).Value; + } + test.ParamExpr = dic; + } + else + { + var context = (PParser.SafetyTestDeclContext)test.SourceLocation; + test.ModExpr = modExprVisitor.Visit(context.modExpr()); + } } - + foreach (var test in globalScope.RefinementTests) { var context = (PParser.RefinementTestDeclContext)test.SourceLocation; diff --git a/Src/PCompiler/CompilerCore/TypeChecker/ParamVisitor.cs b/Src/PCompiler/CompilerCore/TypeChecker/ParamVisitor.cs new file mode 100644 index 0000000000..81b8c728e4 --- /dev/null +++ b/Src/PCompiler/CompilerCore/TypeChecker/ParamVisitor.cs @@ -0,0 +1,108 @@ +using System; +using System.Collections.Generic; +using System.Linq; +using Antlr4.Runtime.Misc; +using Plang.Compiler.TypeChecker.AST; +using Plang.Compiler.TypeChecker.AST.Expressions; +using Plang.Compiler.TypeChecker.Types; + +namespace Plang.Compiler.TypeChecker +{ + + internal class ParamExprVisitor(ITranslationErrorHandler handler) : PParserBaseVisitor + { + public override IPExpr VisitParam([NotNull] PParser.ParamContext context) + { + return Visit(context.paramBody()); + } + + public override IPExpr VisitParamBody([NotNull] PParser.ParamBodyContext context) + { + var fields = context.seqLiteral().Select(Visit).ToArray(); + var entries = new NamedTupleEntry[fields.Length]; + var names = new List(); + for (var i = 0; i < fields.Length; i++) + { + var entryName = context.iden()[i].GetText(); + if (names.Contains(entryName)) + { + throw handler.DuplicateNamedTupleEntry(context.iden()[i], entryName); + } + names.Add(entryName); + entries[i] = new NamedTupleEntry { Name = entryName, FieldNo = i, Type = fields[i].Type }; + } + + var type = new NamedTupleType(entries); + return new NamedTupleExpr(context, fields, type); + } + + public override IPExpr VisitSeqLiteral([NotNull] PParser.SeqLiteralContext context) + { + return Visit(context.seqLiteralBody()); + } + + public override IPExpr VisitSeqLiteralBody([NotNull] PParser.SeqLiteralBodyContext context) + { + 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()}"); + 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()); + } + throw handler.InternalError(context, new ArgumentOutOfRangeException(nameof(context), "unknown primitive literal")); + } + + public override IPExpr VisitPrimitive(PParser.PrimitiveContext context) + { + + if (context.floatLiteral() != null) + { + return Visit(context.floatLiteral()); + } + + if (context.BoolLiteral() != null) + { + return new BoolLiteralExpr(context, context.BoolLiteral().GetText().Equals("true")); + } + + if (context.IntLiteral() != null) + { + return new IntLiteralExpr(context, int.Parse(context.IntLiteral().GetText())); + } + + if (context.NullLiteral() != null) + { + return new NullLiteralExpr(context); + } + + throw handler.InternalError(context, new ArgumentOutOfRangeException(nameof(context), "unknown primitive literal")); + } + + public override IPExpr VisitExpFloat(PParser.ExpFloatContext context) + { + throw new NotImplementedException("float(x,y) syntax"); + } + + public override IPExpr VisitDecimalFloat(PParser.DecimalFloatContext context) + { + var value = double.Parse($"{context.pre?.Text ?? ""}.{context.post.Text}"); + return new FloatLiteralExpr(context, value); + } + public override IPExpr VisitInt([NotNull] PParser.IntContext context) + { + return new IntLiteralExpr(context, int.Parse(context.IntLiteral().GetText())); + } + + } +} \ No newline at end of file diff --git a/Src/PCompiler/CompilerCore/TypeChecker/Scope.cs b/Src/PCompiler/CompilerCore/TypeChecker/Scope.cs index da78441999..a7d46c8f3e 100644 --- a/Src/PCompiler/CompilerCore/TypeChecker/Scope.cs +++ b/Src/PCompiler/CompilerCore/TypeChecker/Scope.cs @@ -3,10 +3,12 @@ using System.Diagnostics; using System.IO; using System.Linq; +using System.Linq.Expressions; using Antlr4.Runtime; using Plang.Compiler.TypeChecker.AST; using Plang.Compiler.TypeChecker.AST.Declarations; using Plang.Compiler.TypeChecker.AST.States; +using Plang.Compiler.TypeChecker.AST.Expressions; using Plang.Compiler.TypeChecker.Types; namespace Plang.Compiler.TypeChecker @@ -32,7 +34,7 @@ public class Scope private readonly IDictionary states = new Dictionary(); private readonly IDictionary tuples = new Dictionary(); private readonly IDictionary typedefs = new Dictionary(); - private readonly IDictionary variables = new Dictionary(); + private readonly IDictionary _variables = new Dictionary(); private Scope(ICompilerConfiguration config, Scope parent = null) { @@ -76,7 +78,7 @@ private Scope(ICompilerConfiguration config, Scope parent = null) public IEnumerable States => states.Values; public IEnumerable Tuples => tuples.Values; public IEnumerable Typedefs => typedefs.Values; - public IEnumerable Variables => variables.Values; + public IEnumerable Variables => _variables.Values; public IEnumerable SafetyTests => safetyTests.Values; public IEnumerable RefinementTests => refinementTests.Values; public IEnumerable Implementations => implementations.Values; @@ -183,7 +185,7 @@ public bool Get(string name, out TypeDef tree) public bool Get(string name, out Variable tree) { - return variables.TryGetValue(name, out tree); + return _variables.TryGetValue(name, out tree); } public bool Get(string name, out SafetyTest tree) @@ -567,8 +569,8 @@ public EnumElem Put(string name, PParser.NumberedEnumElemContext tree) public Variable Put(string name, ParserRuleContext tree, VariableRole role) { var variable = new Variable(name, tree, role); - CheckConflicts(variable, Namespace(variables)); - variables.Add(name, variable); + CheckConflicts(variable, Namespace(_variables)); + _variables.Add(name, variable); return variable; } @@ -611,6 +613,25 @@ public SafetyTest Put(string name, PParser.SafetyTestDeclContext tree) } } + var safetyTest = new SafetyTest(tree, name); + safetyTest.ParamExpr = new Dictionary>(); + CheckConflicts(safetyTest, + Namespace(implementations), + Namespace(safetyTests), + Namespace(refinementTests)); + safetyTests.Add(name, safetyTest); + return safetyTest; + } + + public SafetyTest Put(string name, PParser.ParametricSafetyTestDeclContext tree) + { + // check if test is from an imported project, if so, return null + var filePath = config.LocationResolver.GetLocation(tree).File.FullName; + if (config.ProjectDependencies.Any(dependencyPath => filePath.StartsWith(dependencyPath))) + { + return null; + } + var safetyTest = new SafetyTest(tree, name); CheckConflicts(safetyTest, Namespace(implementations), @@ -658,5 +679,69 @@ private static TableReader Namespace(IDictionary table) where T : } #endregion Conflict API + + #region Global Constant Variables + + public void Update(Variable v) + { + Variable vv; + if (_variables.TryGetValue(v.Name, out vv)) + { + _variables[v.Name] = v; + } + return; + } + + public List GetGlobalVariables() + { + return _variables.Values.Where(v => v.Role == VariableRole.GlobalConstant).ToList(); + } + + public void ValidateGlobalConstantVariablesUnique(ITranslationErrorHandler handler) + { + var current = this; + IDictionary allVariables = new Dictionary(); + while (current != null) + { + foreach (var v in current._variables.Values) { + if (allVariables.Keys.Contains(v.Name)) + { + if (v.Role == VariableRole.GlobalConstant) + { + var vv = allVariables[v.Name]; + throw handler.DuplicateDeclaration(vv.SourceLocation, vv, v); + } + } + allVariables[v.Name] = v; + } + current = current.Parent; + } + return; + } + + public bool LookupLvalue(ITranslationErrorHandler handler, string name, ParserRuleContext pos, out Variable tree) + { + var current = this; + while (current != null) + { + if (current.Get(name, out tree)) + { + if (tree.Role == VariableRole.GlobalConstant) + { + throw handler.ModifyGlobalConstantVariable(pos, tree); + } + return true; + } + + current = current.Parent; + } + + tree = null; + return false; + } + + #endregion Global Constant Variables + + } } \ No newline at end of file diff --git a/Src/PCompiler/PCommandLine/CommandLine.cs b/Src/PCompiler/PCommandLine/CommandLine.cs index 14c01e6b5e..c127e0bd80 100644 --- a/Src/PCompiler/PCommandLine/CommandLine.cs +++ b/Src/PCompiler/PCommandLine/CommandLine.cs @@ -144,4 +144,4 @@ public static void RunCompiler(string[] args) compiler.Compile(configuration); } } -} \ No newline at end of file +} diff --git a/Tst/TestParamTester/.gitignore b/Tst/TestParamTester/.gitignore new file mode 100644 index 0000000000..161a65f6d8 --- /dev/null +++ b/Tst/TestParamTester/.gitignore @@ -0,0 +1,7 @@ +*.out +*.err +portfolio/ +Test.cs +pom.xml +*.csproj +PCheckerOutput/ diff --git a/Tst/TestParamTester/1_ClientServer/.gitignore b/Tst/TestParamTester/1_ClientServer/.gitignore new file mode 100644 index 0000000000..161a65f6d8 --- /dev/null +++ b/Tst/TestParamTester/1_ClientServer/.gitignore @@ -0,0 +1,7 @@ +*.out +*.err +portfolio/ +Test.cs +pom.xml +*.csproj +PCheckerOutput/ diff --git a/Tst/TestParamTester/1_ClientServer/1_ClientServer.sln b/Tst/TestParamTester/1_ClientServer/1_ClientServer.sln new file mode 100644 index 0000000000..d1b53efe1d --- /dev/null +++ b/Tst/TestParamTester/1_ClientServer/1_ClientServer.sln @@ -0,0 +1,30 @@ + +Microsoft Visual Studio Solution File, Format Version 12.00 +# Visual Studio Version 17 +VisualStudioVersion = 17.5.002.0 +MinimumVisualStudioVersion = 10.0.40219.1 +Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = "PGenerated", "PGenerated", "{A4B0FE06-DF66-47F7-B1E0-4334AE0C9924}" +EndProject +Project("{9A19103F-16F7-4668-BE54-9A1E7A4F7556}") = "ClientServer", "PGenerated\CSharp\ClientServer.csproj", "{9151E286-95CD-4FD1-838B-3346B8BDC1DB}" +EndProject +Global + GlobalSection(SolutionConfigurationPlatforms) = preSolution + Debug|Any CPU = Debug|Any CPU + Release|Any CPU = Release|Any CPU + EndGlobalSection + GlobalSection(ProjectConfigurationPlatforms) = postSolution + {9151E286-95CD-4FD1-838B-3346B8BDC1DB}.Debug|Any CPU.ActiveCfg = Debug|Any CPU + {9151E286-95CD-4FD1-838B-3346B8BDC1DB}.Debug|Any CPU.Build.0 = Debug|Any CPU + {9151E286-95CD-4FD1-838B-3346B8BDC1DB}.Release|Any CPU.ActiveCfg = Release|Any CPU + {9151E286-95CD-4FD1-838B-3346B8BDC1DB}.Release|Any CPU.Build.0 = Release|Any CPU + EndGlobalSection + GlobalSection(SolutionProperties) = preSolution + HideSolutionNode = FALSE + EndGlobalSection + GlobalSection(NestedProjects) = preSolution + {9151E286-95CD-4FD1-838B-3346B8BDC1DB} = {A4B0FE06-DF66-47F7-B1E0-4334AE0C9924} + EndGlobalSection + GlobalSection(ExtensibilityGlobals) = postSolution + SolutionGuid = {CFC55A7C-D468-43CA-B3ED-D1299442372F} + EndGlobalSection +EndGlobal diff --git a/Tst/TestParamTester/1_ClientServer/ClientServer.pproj b/Tst/TestParamTester/1_ClientServer/ClientServer.pproj new file mode 100644 index 0000000000..3cb5ef4297 --- /dev/null +++ b/Tst/TestParamTester/1_ClientServer/ClientServer.pproj @@ -0,0 +1,10 @@ + + +ClientServer + + ./PSrc/ + ./PSpec/ + ./PTst/ + +./PGenerated/ + diff --git a/Tst/TestParamTester/1_ClientServer/PSpec/BankBalanceCorrect.p b/Tst/TestParamTester/1_ClientServer/PSpec/BankBalanceCorrect.p new file mode 100644 index 0000000000..34e63b2680 --- /dev/null +++ b/Tst/TestParamTester/1_ClientServer/PSpec/BankBalanceCorrect.p @@ -0,0 +1,115 @@ +/***************************************************** +This file defines two P specifications + +BankBalanceIsAlwaysCorrect (safety property): +BankBalanceIsAlwaysCorrect checks the global invariant that the account-balance communicated +to the client by the bank is always correct and the bank never removes more money from the account +than that withdrawn by the client! Also, if the bank denies a withdraw request then it is only because +the withdrawal would reduce the account balance to below 10. + +GuaranteedWithDrawProgress (liveness property): +GuaranteedWithDrawProgress checks the liveness (or progress) property that all withdraw requests +submitted by the client are eventually responded. + +Note: stating that "BankBalanceIsAlwaysCorrect checks that if the bank denies a withdraw request +then the request would reduce the balance to below 10 (< 10)" is equivalent to state that "if there is enough money in the account - at least 10 (>= 10), then the request must not error". +Hence, the two properties BankBalanceIsAlwaysCorrect and GuaranteedWithDrawProgress together ensure that every withdraw request if allowed will eventually succeed and the bank cannot block correct withdrawal requests. +*****************************************************/ + +// event: initialize the monitor with the initial account balances for all clients when the system starts +event eSpec_BankBalanceIsAlwaysCorrect_Init: map[int, int]; + +/**************************************************** +BankBalanceIsAlwaysCorrect checks the global invariant that the account balance communicated +to the client by the bank is always correct and there is no error on the banks side with the +implementation of the withdraw logic. + +For checking this property the spec machine observes the withdraw request (eWithDrawReq) and response (eWithDrawResp). +- On receiving the eWithDrawReq, it adds the request in the pending-withdraws-map so that on receiving a +response for this withdraw we can assert that the amount of money deducted from the account is same as +what was requested by the client. + +- On receiving the eWithDrawResp, we look up the corresponding withdraw request and check that: the +new account balance is correct and if the withdraw failed it is because the withdraw will make the account +balance go below 10 dollars which is against the bank policies! +****************************************************/ +spec BankBalanceIsAlwaysCorrect observes eWithDrawReq, eWithDrawResp, eSpec_BankBalanceIsAlwaysCorrect_Init { + // keep track of the bank balance for each client: map from accountId to bank balance. + var bankBalance: map[int, int]; + // keep track of the pending withdraw requests that have not been responded yet. + // map from reqId -> withdraw request + var pendingWithDraws: map[int, tWithDrawReq]; + + start state Init { + on eSpec_BankBalanceIsAlwaysCorrect_Init goto WaitForWithDrawReqAndResp with (balance: map[int, int]){ + bankBalance = balance; + } + } + + state WaitForWithDrawReqAndResp { + on eWithDrawReq do (req: tWithDrawReq) { + assert req.accountId in bankBalance, + format ("Unknown accountId {0} in the withdraw request. Valid accountIds = {1}", + req.accountId, keys(bankBalance)); + pendingWithDraws[req.rId] = req; + } + + on eWithDrawResp do (resp: tWithDrawResp) { + assert resp.accountId in bankBalance, + format ("Unknown accountId {0} in the withdraw response!", resp.accountId); + assert resp.rId in pendingWithDraws, + format ("Unknown rId {0} in the withdraw response!", resp.rId); + assert resp.balance >= 10, + "Bank balance in all accounts must always be greater than or equal to 10!!"; + + if(resp.status == WITHDRAW_SUCCESS) + { + assert resp.balance == bankBalance[resp.accountId] - pendingWithDraws[resp.rId].amount, + format ("Bank balance for the account {0} is {1} and not the expected value {2}, Bank is lying!", + resp.accountId, resp.balance, bankBalance[resp.accountId] - pendingWithDraws[resp.rId].amount); + // update the new account balance + bankBalance[resp.accountId] = resp.balance; + } + else + { + // bank can only reject a request if it will drop the balance below 10 + assert bankBalance[resp.accountId] - pendingWithDraws[resp.rId].amount < 10, + format ("Bank must accept the withdraw request for {0}, bank balance is {1}!", + pendingWithDraws[resp.rId].amount, bankBalance[resp.accountId]); + // if withdraw failed then the account balance must remain the same + assert bankBalance[resp.accountId] == resp.balance, + format ("Withdraw failed BUT the account balance changed! actual: {0}, bank said: {1}", + bankBalance[resp.accountId], resp.balance); + } + } + } +} + +/************************************************************************** +GuaranteedWithDrawProgress checks the liveness (or progress) property that all withdraw requests +submitted by the client are eventually responded. +***************************************************************************/ +spec GuaranteedWithDrawProgress observes eWithDrawReq, eWithDrawResp { + // keep track of the pending withdraw requests + var pendingWDReqs: set[int]; + + start state NopendingRequests { + on eWithDrawReq goto PendingReqs with (req: tWithDrawReq) { + pendingWDReqs += (req.rId); + } + } + + hot state PendingReqs { + on eWithDrawResp do (resp: tWithDrawResp) { + assert resp.rId in pendingWDReqs, + format ("unexpected rId: {0} received, expected one of {1}", resp.rId, pendingWDReqs); + pendingWDReqs -= (resp.rId); + if(sizeof(pendingWDReqs) == 0) // all requests have been responded + goto NopendingRequests; + } + + on eWithDrawReq goto PendingReqs with (req: tWithDrawReq){ + pendingWDReqs += (req.rId); + } + } +} diff --git a/Tst/TestParamTester/1_ClientServer/PSrc/AbstractBankServer.p b/Tst/TestParamTester/1_ClientServer/PSrc/AbstractBankServer.p new file mode 100644 index 0000000000..fea5042e68 --- /dev/null +++ b/Tst/TestParamTester/1_ClientServer/PSrc/AbstractBankServer.p @@ -0,0 +1,37 @@ +/********************************************************* +The AbstractBankServer provides an abstract implementation of the BankServer where it abstract away +the interaction between the BankServer and Database. +The AbstractBankServer machine is used to demonstrate how one can replace a complex component in P +with its abstraction that hides a lot of its internal complexity. +In this case, instead of storing the balance in a separate database the abstraction store the information +locally and abstracts away the complexity of bank server interaction with the database. +For the client, it still exposes the same interface/behavior. Hence, when checking the correctness +of the client it doesnt matter whether we use BankServer or the AbstractBankServer +**********************************************************/ + +machine AbstractBankServer +{ + // account balance: map from account-id to balance + var balance: map[int, int]; + start state WaitForWithdrawRequests { + entry (init_balance: map[int, int]) + { + balance = init_balance; + } + + on eWithDrawReq do (wReq: tWithDrawReq) { + assert wReq.accountId in balance, "Invalid accountId received in the withdraw request!"; + if(balance[wReq.accountId] - wReq.amount > 10) /* hint: bug */ + { + balance[wReq.accountId] = balance[wReq.accountId] - wReq.amount; + send wReq.source, eWithDrawResp, + (status = WITHDRAW_SUCCESS, accountId = wReq.accountId, balance = balance[wReq.accountId], rId = wReq.rId); + } + else + { + send wReq.source, eWithDrawResp, + (status = WITHDRAW_ERROR, accountId = wReq.accountId, balance = balance[wReq.accountId], rId = wReq.rId); + } + } + } +} \ No newline at end of file diff --git a/Tst/TestParamTester/1_ClientServer/PSrc/Client.p b/Tst/TestParamTester/1_ClientServer/PSrc/Client.p new file mode 100644 index 0000000000..f01c3d8e8a --- /dev/null +++ b/Tst/TestParamTester/1_ClientServer/PSrc/Client.p @@ -0,0 +1,96 @@ +/* User Defined Types */ + +// payload type associated with the eWithDrawReq, where `source`: client sending the withdraw request, +// `accountId`: account to withdraw from, `amount`: amount to withdraw, and `rId`: unique +// request Id associated with each request. +type tWithDrawReq = (source: Client, accountId: int, amount: int, rId:int); + +// payload type associated with the eWithDrawResp, where `status`: response status (below), +// `accountId`: account withdrawn from, `balance`: bank balance after withdrawal, and +// `rId`: request id for which this is the response. +type tWithDrawResp = (status: tWithDrawRespStatus, accountId: int, balance: int, rId: int); + +// enum representing the response status for the withdraw request +enum tWithDrawRespStatus { + WITHDRAW_SUCCESS, + WITHDRAW_ERROR +} + +// event: withdraw request (from client to bank server) +event eWithDrawReq : tWithDrawReq; +// event: withdraw response (from bank server to client) +event eWithDrawResp: tWithDrawResp; + +constant global1 : int; + +machine Client +{ + var server : BankServer; + var accountId: int; + var nextReqId : int; + var numOfWithdrawOps: int; + var currentBalance: int; + + start state Init { + + entry (input : (serv : BankServer, accountId: int, balance : int)) + { + print format("global varaible global1 = {0}", global1); + print format("global varaible global2 = {0}", global2); + server = input.serv; + currentBalance = input.balance; + accountId = input.accountId; + // hacky: we would like request id's to be unique across all requests from clients + nextReqId = accountId*100 + 1; // each client has a unique account id + goto WithdrawMoney; + } + } + + state WithdrawMoney { + entry { + // If current balance is <= 10 then we need more deposits before any more withdrawal + if(currentBalance <= 10) + goto NoMoneyToWithDraw; + + // send withdraw request to the bank for a random amount between (1 to current balance + 1) + send server, eWithDrawReq, (source = this, accountId = accountId, amount = WithdrawAmount(), rId = nextReqId); + nextReqId = nextReqId + 1; + } + + on eWithDrawResp do (resp: tWithDrawResp) { + // bank always ensures that a client has atleast 10 dollars in the account + assert resp.balance >= 10, "Bank balance must be greater than 10!!"; + if(resp.status == WITHDRAW_SUCCESS) // withdraw succeeded + { + print format ("Withdrawal with rId = {0} succeeded, new account balance = {1}", resp.rId, resp.balance); + currentBalance = resp.balance; + } + else // withdraw failed + { + // if withdraw failed then the account balance must remain the same + assert currentBalance == resp.balance, + format ("Withdraw failed BUT the account balance changed! client thinks: {0}, bank balance: {1}", currentBalance, resp.balance); + print format ("Withdrawal with rId = {0} failed, account balance = {1}", resp.rId, resp.balance); + } + + if(currentBalance > 10) + { + print format ("Still have account balance = {0}, lets try and withdraw more", currentBalance); + goto WithdrawMoney; + } + } + } + + // function that returns a random integer between (1 to current balance + 1) + fun WithdrawAmount() : int { + return choose(currentBalance) + 1; + } + + state NoMoneyToWithDraw { + entry { + // if I am here then the amount of money in my account should be exactly 10 + assert currentBalance == 10, "Hmm, I still have money that I can withdraw but I have reached NoMoneyToWithDraw state!"; + print format ("No Money to withdraw, waiting for more deposits!"); + } + } +} diff --git a/Tst/TestParamTester/1_ClientServer/PSrc/ClientServerModules.p b/Tst/TestParamTester/1_ClientServer/PSrc/ClientServerModules.p new file mode 100644 index 0000000000..f17c40d517 --- /dev/null +++ b/Tst/TestParamTester/1_ClientServer/PSrc/ClientServerModules.p @@ -0,0 +1,8 @@ +// Client module +module Client = { Client }; + +// Bank module +module Bank = { BankServer, Database }; + +// Abstract Bank Server module +module AbstractBank = { AbstractBankServer -> BankServer }; \ No newline at end of file diff --git a/Tst/TestParamTester/1_ClientServer/PSrc/Server.p b/Tst/TestParamTester/1_ClientServer/PSrc/Server.p new file mode 100644 index 0000000000..ec1ef87879 --- /dev/null +++ b/Tst/TestParamTester/1_ClientServer/PSrc/Server.p @@ -0,0 +1,95 @@ +/** Events used to communicate between the bank server and the backend database **/ +// event: send update the database, i.e. the `balance` associated with the `accountId` +event eUpdateQuery: (accountId: int, balance: int); +// event: send a read request for the `accountId`. +event eReadQuery: (accountId: int); +// event: send a response (`balance`) corresponding to the read request for an `accountId` +event eReadQueryResp: (accountId: int, balance: int); + +/************************************************************* +The BankServer machine uses a database machine as a service to store the bank balance for all its clients. +On receiving an eWithDrawReq (withdraw requests) from a client, it reads the current balance for the account, +if there is enough money in the account then it updates the new balance in the database after withdrawal +and sends a response back to the client. +*************************************************************/ + +constant global2 : int; + +machine BankServer +{ + var database: Database; + + start state Init { + entry (initialBalance: map[int, int]){ + database = new Database((server = this, initialBalance = initialBalance)); + goto WaitForWithdrawRequests; + } + } + + state WaitForWithdrawRequests { + on eWithDrawReq do (wReq: tWithDrawReq) { + var currentBalance: int; + var response: tWithDrawResp; + + // read the current account balance from the database + currentBalance = ReadBankBalance(database, wReq.accountId); + // if there is enough money in account after withdrawal + if(currentBalance - wReq.amount >= 10) + { + UpdateBankBalance(database, wReq.accountId, currentBalance - wReq.amount); + response = (status = WITHDRAW_SUCCESS, accountId = wReq.accountId, balance = currentBalance - wReq.amount, rId = wReq.rId); + } + else // not enough money after withdraw + { + response = (status = WITHDRAW_ERROR, accountId = wReq.accountId, balance = currentBalance, rId = wReq.rId); + } + + // send response to the client + send wReq.source, eWithDrawResp, response; + } + } +} + +/*************************************************************** +The Database machine acts as a helper service for the Bank server and stores the bank balance for +each account. There are two API's or functions to interact with the Database: +ReadBankBalance and UpdateBankBalance. +****************************************************************/ +machine Database +{ + var server: BankServer; + var balance: map[int, int]; + start state Init { + entry(input: (server : BankServer, initialBalance: map[int, int])){ + server = input.server; + balance = input.initialBalance; + } + on eUpdateQuery do (query: (accountId: int, balance: int)) { + assert query.accountId in balance, "Invalid accountId received in the update query!"; + balance[query.accountId] = query.balance; + } + on eReadQuery do (query: (accountId: int)) + { + assert query.accountId in balance, "Invalid accountId received in the read query!"; + send server, eReadQueryResp, (accountId = query.accountId, balance = balance[query.accountId]); + } + } +} + +// Function to read the bank balance corresponding to the accountId +fun ReadBankBalance(database: Database, accountId: int) : int { + var currentBalance: int; + send database, eReadQuery, (accountId = accountId,); + receive { + case eReadQueryResp: (resp: (accountId: int, balance: int)) { + currentBalance = resp.balance; + } + } + return currentBalance; +} + +// Function to update the account balance for the account Id +fun UpdateBankBalance(database: Database, accId: int, bal: int) +{ + send database, eUpdateQuery, (accountId = accId, balance = bal); +} \ No newline at end of file diff --git a/Tst/TestParamTester/1_ClientServer/PTst/TestDriver.p b/Tst/TestParamTester/1_ClientServer/PTst/TestDriver.p new file mode 100644 index 0000000000..f2e4e23260 --- /dev/null +++ b/Tst/TestParamTester/1_ClientServer/PTst/TestDriver.p @@ -0,0 +1,70 @@ + +// Test driver that checks the system with a single Client. +machine TestWithSingleClient +{ + start state Init { + entry { + // since client + SetupClientServerSystem(1); + } + } +} + +// Test driver that checks the system with multiple Clients. +machine TestWithMultipleClients +{ + start state Init { + entry { + // multiple clients between (2, 4) + SetupClientServerSystem(choose(3) + 2); + } + } +} + +constant globalnumClients: int; + +machine TestWithConfig { + start state Init { + entry { + SetupClientServerSystem(globalnumClients); + } + } +} + +// creates a random map from accountId's to account balance of size `numAccounts` +fun CreateRandomInitialAccounts(numAccounts: int) : map[int, int] +{ + var i: int; + var bankBalance: map[int, int]; + while(i < numAccounts) { + bankBalance[i] = choose(100) + 10; // min 10 in the account + i = i + 1; + } + return bankBalance; +} + +// setup the client server system with one bank server and `numClients` clients. +fun SetupClientServerSystem(numClients: int) +{ + var i: int; + var server: BankServer; + var accountIds: seq[int]; + var initAccBalance: map[int, int]; + + // randomly initialize the account balance for all clients + initAccBalance = CreateRandomInitialAccounts(numClients); + // create bank server with the init account balance + server = new BankServer(initAccBalance); + + // before client starts sending any messages make sure we + // initialize the monitors or specifications + announce eSpec_BankBalanceIsAlwaysCorrect_Init, initAccBalance; + + accountIds = keys(initAccBalance); + + // create the clients + while(i < sizeof(accountIds)) { + new Client((serv = server, accountId = accountIds[i], balance = initAccBalance[accountIds[i]])); + i = i + 1; + } +} \ No newline at end of file diff --git a/Tst/TestParamTester/1_ClientServer/PTst/Testscript.p b/Tst/TestParamTester/1_ClientServer/PTst/Testscript.p new file mode 100644 index 0000000000..8959f43fab --- /dev/null +++ b/Tst/TestParamTester/1_ClientServer/PTst/Testscript.p @@ -0,0 +1,66 @@ +/* This file contains three different model checking scenarios */ + +// assert the properties for the single client and single server scenario +test tcSingleClient [main=TestWithSingleClient]: + assert BankBalanceIsAlwaysCorrect, GuaranteedWithDrawProgress in + (union Client, Bank, { TestWithSingleClient }); + +// assert the properties for the two clients and single server scenario +test tcMultipleClients [main=TestWithMultipleClients]: + assert BankBalanceIsAlwaysCorrect, GuaranteedWithDrawProgress in + (union Client, Bank, { TestWithMultipleClients }); + +// assert the properties for the single client and single server scenario but with abstract server + test tcAbstractServer [main=TestWithSingleClient]: + assert BankBalanceIsAlwaysCorrect, GuaranteedWithDrawProgress in + (union Client, AbstractBank, { TestWithSingleClient }); + +paramtest (globalnumClients in [2, 3, 4], global1 in [1,2], global2 in [4, 5]) aaaa1 [main=TestWithConfig]: + assert BankBalanceIsAlwaysCorrect, GuaranteedWithDrawProgress in + (union Client, Bank, { TestWithConfig }); + +paramtest (globalnumClients in [1]) aaa2 [main=TestWithConfig]: + assert BankBalanceIsAlwaysCorrect, GuaranteedWithDrawProgress in + (union Client, Bank, { TestWithConfig }); + +constant dummyGv : bool; +paramtest (globalnumClients in [1], dummyGv in [true, false]) aaa3 [main=TestWithConfig]: + assert BankBalanceIsAlwaysCorrect, GuaranteedWithDrawProgress in + (union Client, Bank, { TestWithConfig }); + +constant rich1: float; +constant rich2: any; + +paramtest (globalnumClients in [1], rich1 in [3.0, 2.1], rich2 in [null]) aaa4 [main=TestWithConfig]: + assert BankBalanceIsAlwaysCorrect, GuaranteedWithDrawProgress in + (union Client, Bank, { TestWithConfig }); + +// Syntax error +// paramtest () wrong1 [main=TestWithSingleClient]: +// assert BankBalanceIsAlwaysCorrect, GuaranteedWithDrawProgress in +// (union Client, Bank, { TestWithSingleClient }); + +// Syntax error +// paramtest (globalnumClients in []) wrong2 [main=TestWithSingleClient]: +// assert BankBalanceIsAlwaysCorrect, GuaranteedWithDrawProgress in +// (union Client, Bank, { TestWithSingleClient }); + +// Duplicate Assign +// paramtest (globalnumClients in [1], globalnumClients in [1]) wrong3 [main=TestWithSingleClient]: +// assert BankBalanceIsAlwaysCorrect, GuaranteedWithDrawProgress in +// (union Client, Bank, { TestWithSingleClient }); + +// Undelared global variable +// paramtest (x in [1], globalnumClients in [1]) wrong4 [main=TestWithSingleClient]: +// assert BankBalanceIsAlwaysCorrect, GuaranteedWithDrawProgress in +// (union Client, Bank, { TestWithSingleClient }); + +// Type mismatch +// paramtest (globalnumClients in [1], dummyGv in [2, 3]) wrong5 [main=TestWithSingleClient]: +// assert BankBalanceIsAlwaysCorrect, GuaranteedWithDrawProgress in +// (union Client, Bank, { TestWithSingleClient }); + +// Type mismatch +// paramtest (globalnumClients in [1], dummyGv in [true, 3]) wrong6 [main=TestWithConfig]: +// assert BankBalanceIsAlwaysCorrect, GuaranteedWithDrawProgress in +// (union Client, Bank, { TestWithConfig }); \ No newline at end of file diff --git a/Tst/TestParamTester/1_ClientServer/portfolio-config.json b/Tst/TestParamTester/1_ClientServer/portfolio-config.json new file mode 100644 index 0000000000..96f0722a4e --- /dev/null +++ b/Tst/TestParamTester/1_ClientServer/portfolio-config.json @@ -0,0 +1,66 @@ +{ + "pproj": { + "help" : "Name of the .pproj file in the project directory", + "default" : "ClientServer.pproj", + "metavar" : "F" + }, + + "dll": { + "help" : "Path to generated .dll file, relative to project directory", + "default" : "PGenerated/CSharp/net8.0/ClientServer.dll", + "metavar" : "F" + }, + + "partitions": { + "help" : "Number of runs for parallel analysis, per method", + "default" : 2, + "metavar" : "N" + }, + + "timeout": { + "help" : "Timeout for checker run in seconds, per method per partition", + "default" : 30, + "metavar" : "N" + }, + + "schedules": { + "help" : "Number of schedules, per method per partition", + "default" : 100000, + "metavar" : "N" + }, + + "max-steps": { + "help" : "Max number of scheduling points in execution", + "default" : 10000, + "metavar" : "N" + }, + + "methods": { + "help" : "Suffixes of test methods to execute", + "metavar" : "M", + "default" : [ + "tcSingleClient", + "tcMultipleClients", + "tcAbstractServer" + ] + }, + + "polling-interval": { + "help" : "How frequently to check for job completion, in seconds", + "metavar" : "N", + "default" : 10 + }, + + "verbose": { + "help" : "Verbose output", + "default" : false, + "action" : "store_true" + }, + + "psym-jar": { + "help" : "Path to generated PSym .jar file, relative to project directory", + "default" : "PGenerated/Symbolic/target/ClientServer-jar-with-dependencies.jar", + "metavar" : "F" + } + +}