Fix the code generation error for static functions called from Monito…

…rs (#530) * Fixing the problem around allowing functions with side effects inside a monitor * Added more regressions for the static function in monitors * Fixed the regression that was failing
p-org · Nov 29, 2022 · 88ab781 · 88ab781
1 parent 007ab2f
commit 88ab781
Show file tree

Hide file tree

Showing 13 changed files with 169 additions and 33 deletions.
diff --git a/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs b/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs
@@ -208,8 +208,7 @@ private void WriteDecl(CompilationContext context, StringWriter output, IPDecl d
                     break;
 
                 case TypeDef typeDef:
-                    ForeignType foreignType = typeDef.Type as ForeignType;
-                    if (foreignType != null)
+                    if (typeDef.Type is ForeignType foreignType)
                     {
                         WriteForeignType(context, output, foreignType);
                     }
@@ -705,15 +704,32 @@ private void WriteFunction(CompilationContext context, StringWriter output, Func
                         $"{GetCSharpType(param.Type)} {context.Names.GetNameForDecl(param)}"));
             }
 
-            if (isStatic)
+            if (isStatic) // then we need to generate two versions of the function
             {
+                // for machine
                 string seperator = functionParameters == "" ? "" : ", ";
-                functionParameters += string.Concat(seperator, "PMachine currentMachine");
+                var functionParameters_machine = functionParameters + string.Concat(seperator, "PMachine currentMachine");
+                context.WriteLine(output,
+                    $"public {staticKeyword}{asyncKeyword}{returnType} {functionName}({functionParameters_machine})");
+                WriteFunctionBody(context, output, function);
+
+                // for monitor
+                if (!(function.CanCreate == true || function.CanSend == true || function.IsNondeterministic == true || function.CanReceive == true))
+                {
+                    var functionParameters_monitor = functionParameters + string.Concat(seperator, "PMonitor currentMachine");
+                    context.WriteLine(output,
+                        $"public {staticKeyword}{asyncKeyword}{returnType} {functionName}({functionParameters_monitor})");
+                    WriteFunctionBody(context, output, function);
+                }
+
             }
-
-            context.WriteLine(output,
-                $"public {staticKeyword}{asyncKeyword}{returnType} {functionName}({functionParameters})");
-            WriteFunctionBody(context, output, function);
+            else
+            {
+                context.WriteLine(output,
+                    $"public {staticKeyword}{asyncKeyword}{returnType} {functionName}({functionParameters})");
+                WriteFunctionBody(context, output, function);   
+            }
+
         }
 
         private void WriteFunctionBody(CompilationContext context, StringWriter output, Function function)

diff --git a/Src/PCompiler/CompilerCore/DefaultTranslationErrorHandler.cs b/Src/PCompiler/CompilerCore/DefaultTranslationErrorHandler.cs
@@ -161,6 +161,12 @@ public Exception IllegalChooseSubExprType(PParser.ChooseExprContext context, PLa
             return IssueError(context, $"choose expects a parameter of type int (max value) or a collection type (seq, set, or map) got a parameter of type {subExprType}");
         }
 
+        public Exception IllegalFunctionUsedInSpecMachine(Function function, Machine callerOwner)
+        {
+            return IssueError(function.SourceLocation,
+                $"Method {DeclarationName(function)} is non-deterministic or has side-effects (new or send or receive), hence cannot be used in spec machine {DeclarationName(callerOwner)}.");
+        }
+
         public Exception EmittedNullEvent(IPExpr evtExpr)
         {
             return IssueError(evtExpr.SourceLocation, "cannot send null events");
@@ -177,13 +183,6 @@ public Exception ChangedStateMidTransition(ParserRuleContext location, Function
                 $"Method {DeclarationName(method)} is used as a transition function, but might change state here.");
         }
 
-        public Exception NonDeterministicFunctionInSpecMachine(Function machineFunction)
-        {
-            return IssueError(machineFunction.SourceLocation,
-                $"Method {DeclarationName(machineFunction)} is non-deterministic, but used in spec machine.");
-        }
-
-
         public Exception InvalidPrintFormat(PParser.PrintStmtContext context, IToken symbol)
         {
             return IssueError(context,

diff --git a/Src/PCompiler/CompilerCore/ITranslationErrorHandler.cs b/Src/PCompiler/CompilerCore/ITranslationErrorHandler.cs
@@ -56,8 +56,6 @@ public interface ITranslationErrorHandler
 
         Exception ChangedStateMidTransition(ParserRuleContext location, Function method);
 
-        Exception NonDeterministicFunctionInSpecMachine(Function machineFunction);
-
         Exception InvalidPrintFormat(PParser.PrintStmtContext context, IToken symbol);
 
         Exception InvalidStringExprFormat(PParser.FormatedStringContext context, IToken symbol);
@@ -120,5 +118,6 @@ public interface ITranslationErrorHandler
         Exception MoreThanOneParameterForHandlers(ParserRuleContext sourceLocation, int count);
 
         Exception IllegalChooseSubExprType(PParser.ChooseExprContext context, PLanguageType subExprType);
+        Exception IllegalFunctionUsedInSpecMachine(Function function, Machine callerOwner);
     }
 }
diff --git a/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/Function.cs b/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/Function.cs
@@ -96,6 +96,10 @@ public void RemoveCallee(Function callee)
         public bool? CanChangeState { get; set; }
         public bool? CanRaiseEvent { get; set; }
         public bool? CanReceive { get; set; }
+
+        public bool? CanSend { get; set; }
+
+        public bool? CanCreate { get; set; }
         public bool? IsNondeterministic { get; set; }
 
         public IEnumerable<Function> Callers => callers;

diff --git a/Src/PCompiler/CompilerCore/TypeChecker/Analyzer.cs b/Src/PCompiler/CompilerCore/TypeChecker/Analyzer.cs
@@ -42,22 +42,40 @@ public static class Analyzer
                 CreatePropagation(fn => fn.CanReceive, (fn, value) => fn.CanReceive = value,
                     true),
                 CreatePropagation(fn => fn.CanChangeState, (fn, value) => fn.CanChangeState = value,
-                    true));
+                    true),
+                CreatePropagation(fn => fn.CanCreate, (fn, value) => fn.CanCreate = value,
+                    true),
+                CreatePropagation(fn => fn.CanSend, (fn, value) => fn.CanSend = value,
+                    true),
+                CreatePropagation(fn => fn.IsNondeterministic, (fn, value) => fn.IsNondeterministic = value,
+                    true)
+                );
 
             // Step 5: Verify capability restrictions
-            foreach (Function machineFunction in allFunctions)
+            foreach (var function in allFunctions)
             {
-                // TODO: is this checked earlier?
-                if (machineFunction.Owner?.IsSpec == true && machineFunction.IsNondeterministic == true)
+                // This can been checked before but just doing it again for safety!
+                if (function.Owner?.IsSpec == true && (function.IsNondeterministic == true || function.CanCreate == true || function.CanSend == true|| function.CanReceive == true))
                 {
-                    throw handler.NonDeterministicFunctionInSpecMachine(machineFunction);
+                    throw handler.IllegalFunctionUsedInSpecMachine(function, function.Owner);
                 }
-
-                if ((machineFunction.CanChangeState == true || machineFunction.CanRaiseEvent == true) &&
-                    (machineFunction.Role.HasFlag(FunctionRole.TransitionFunction) ||
-                     machineFunction.Role.HasFlag(FunctionRole.ExitHandler)))
+
+                // A static function if it has side effects or is non-deterministic then it cannot be called from a spec machine
+                if (function.Owner == null && (function.IsNondeterministic == true || function.CanCreate == true || function.CanSend == true|| function.CanReceive == true))
+                {
+                    foreach (var caller in function.Callers)
+                    {
+                        if (caller.Owner?.IsSpec == true)
+                        {
+                            throw handler.IllegalFunctionUsedInSpecMachine(function, caller.Owner);
+                        }
+                    }
+                }
+                if ((function.CanChangeState == true || function.CanRaiseEvent == true) &&
+                    (function.Role.HasFlag(FunctionRole.TransitionFunction) ||
+                     function.Role.HasFlag(FunctionRole.ExitHandler)))
                 {
-                    throw handler.ChangedStateMidTransition(machineFunction.SourceLocation, machineFunction);
+                    throw handler.ChangedStateMidTransition(function.SourceLocation, function);
                 }
             }
 

diff --git a/Src/PCompiler/CompilerCore/TypeChecker/ExprVisitor.cs b/Src/PCompiler/CompilerCore/TypeChecker/ExprVisitor.cs
@@ -172,6 +172,9 @@ public override IPExpr VisitCtorExpr(PParser.CtorExprContext context)
 
             IPExpr[] arguments = TypeCheckingUtils.VisitRvalueList(context.rvalueList(), this).ToArray();
             TypeCheckingUtils.ValidatePayloadTypes(handler, context, @interface.PayloadType, arguments);
+
+            method.CanCreate = true;
+
             return new CtorExpr(context, @interface, arguments);
         }
 

diff --git a/Src/PCompiler/CompilerCore/TypeChecker/StatementVisitor.cs b/Src/PCompiler/CompilerCore/TypeChecker/StatementVisitor.cs
@@ -281,6 +281,7 @@ public override IPStmt VisitCtorStmt(PParser.CtorStmtContext context)
 
             List<IPExpr> args = TypeCheckingUtils.VisitRvalueList(context.rvalueList(), exprVisitor).ToList();
             TypeCheckingUtils.ValidatePayloadTypes(handler, context, targetInterface.PayloadType, args);
+            method.CanCreate = true;
             return new CtorStmt(context, targetInterface, args);
         }
 
@@ -369,6 +370,8 @@ public override IPStmt VisitSendStmt(PParser.SendStmtContext context)
                 TypeCheckingUtils.ValidatePayloadTypes(handler, context, eventRef.Value.PayloadType, args);
             }
 
+            method.CanSend = true;
+
             return new SendStmt(context, machineExpr, evtExpr, args);
         }
 

diff --git a/Src/PRuntimes/PCSharpRuntime/PMachine.cs b/Src/PRuntimes/PCSharpRuntime/PMachine.cs
@@ -108,12 +108,6 @@ public Task<Event> TryReceiveEvent(params Type[] events)
             throw new PNonStandardReturnException { ReturnKind = NonStandardReturn.Goto };
         }
 
-        public void TryPopState()
-        {
-            base.RaisePopStateEvent();
-            throw new PNonStandardReturnException { ReturnKind = NonStandardReturn.Pop };
-        }
-
         public int TryRandomInt(int maxValue)
         {
             return base.RandomInteger(maxValue);

diff --git a/Src/PRuntimes/PCSharpRuntime/PMonitor.cs b/Src/PRuntimes/PCSharpRuntime/PMonitor.cs
@@ -35,5 +35,15 @@ public void TryAssert(bool predicate, string s, params object[] args)
         {
             base.Assert(predicate, s, args);
         }
+
+        public void LogLine(string message)
+        {
+            Logger.WriteLine($"<PrintLog> {message}");
+        }
+
+        public void Log(string message)
+        {
+            Logger.Write($"{message}");
+        }
     }
 }
diff --git a/...Tests/Feature1SMLevelDecls/DynamicError/StaticFunctionInMonitor/StaticFunctionInMonitor.p b/...Tests/Feature1SMLevelDecls/DynamicError/StaticFunctionInMonitor/StaticFunctionInMonitor.p
@@ -0,0 +1,26 @@
+fun foo() {
+	var x: machine;
+	assert false;
+}
+
+event e1;
+
+spec M observes e1 {
+
+	start state Init {
+		entry {
+			foo();
+		}
+
+	}
+}
+
+machine Main {
+	start state Init {
+		entry {
+			send this, e1;
+		}
+	}
+}
+
+test DefaultImpl [main=Main]: assert M in {Main};
diff --git a/Tst/RegressionTests/Feature1SMLevelDecls/StaticError/SendInMonitor/SendInMonitor.p b/Tst/RegressionTests/Feature1SMLevelDecls/StaticError/SendInMonitor/SendInMonitor.p
@@ -0,0 +1,15 @@
+event e1;
+
+spec Main observes e1 {
+
+	fun foo(x: machine) {
+		send x, e1;
+	}
+
+	start state Init {
+		entry {
+			var x: machine;
+			send x, e1;
+		}
+	}
+}
diff --git a/...ressionTests/Feature1SMLevelDecls/StaticError/SideEffectsInMonitor/SideEffectsInMonitor.p b/...ressionTests/Feature1SMLevelDecls/StaticError/SideEffectsInMonitor/SideEffectsInMonitor.p
@@ -0,0 +1,23 @@
+event e1;
+
+spec M observes e1 {
+	start state Init {
+
+	}
+
+	fun foo(x: machine) {
+		send x, e1;
+
+		receive {
+			case e1: {}
+		}
+
+		new Main();
+	}
+}
+
+machine Main {
+	start state Init {
+
+	}
+}
diff --git a/...nTests/Feature1SMLevelDecls/StaticError/StaticFunctionInMonitor/StaticFunctionInMonitor.p b/...nTests/Feature1SMLevelDecls/StaticError/StaticFunctionInMonitor/StaticFunctionInMonitor.p
@@ -0,0 +1,26 @@
+fun foo() {
+	var x: machine;
+	send x, e1;
+}
+
+event e1;
+
+spec M observes e1 {
+
+	start state Init {
+		entry {
+			foo();
+		}
+
+	}
+}
+
+machine Main {
+	start state Init {
+		entry {
+			foo();
+		}
+	}
+}
+
+test X [main=Main]: assert M in {Main};