Fix unhandled exception when accessing machine fields (fixes #920)

Src/PCompiler/CompilerCore/TypeChecker/Analyzer.cs

@@ -184,7 +184,7 @@ public static Scope AnalyzeCompilationUnit(ICompilerConfiguration config,
 
         private static IPExpr PopulateExpr(Function func, ParserRuleContext ctx, PLanguageType type, ITranslationErrorHandler handler)
         {
-            var exprVisitor = new ExprVisitor(func, handler);
+            var exprVisitor = new ExprVisitor(func, handler, isPVerifier: true);
             var body = exprVisitor.Visit(ctx);
             if (!type.IsSameTypeAs(body.Type))
             {

Src/PCompiler/CompilerCore/TypeChecker/ExprVisitor.cs

@@ -15,19 +15,22 @@ public class ExprVisitor : PParserBaseVisitor<IPExpr>
     {
         private readonly ITranslationErrorHandler handler;
         private readonly Function method;
+        private readonly bool isPVerifier;
         private Scope table;
 
-        public ExprVisitor(Function method, ITranslationErrorHandler handler)
+        public ExprVisitor(Function method, ITranslationErrorHandler handler, bool isPVerifier = false)
         {
             table = method.Scope;
             this.method = method;
             this.handler = handler;
+            this.isPVerifier = isPVerifier;
         }
 
-        public ExprVisitor(Scope scope, ITranslationErrorHandler handler)
+        public ExprVisitor(Scope scope, ITranslationErrorHandler handler, bool isPVerifier = false)
         {
             table = scope;
             this.handler = handler;
+            this.isPVerifier = isPVerifier;
         }
 
         public override IPExpr VisitPrimitiveExpr(PParser.PrimitiveExprContext context)
@@ -65,7 +68,7 @@ public override IPExpr VisitNamedTupleAccessExpr(PParser.NamedTupleAccessExprCon
 
                     return new NamedTupleAccessExpr(context, subExpr, entry);
 
-                case PermissionType {Origin: Machine} permission:
+                case PermissionType {Origin: Machine} permission when isPVerifier:
                     var machine = (Machine) permission.Origin;
 
                     if (!machine.LookupEntry(fieldName, out var field))
@@ -74,7 +77,7 @@ public override IPExpr VisitNamedTupleAccessExpr(PParser.NamedTupleAccessExprCon
                     }
                     return new MachineAccessExpr(context, machine, subExpr, field);
 
-                case PermissionType {Origin: Interface} permission:
+                case PermissionType {Origin: Interface} permission when isPVerifier:
                     var pname = permission.Origin.Name;
 
                     if (!table.Lookup(pname, out Machine m))
@@ -88,7 +91,7 @@ public override IPExpr VisitNamedTupleAccessExpr(PParser.NamedTupleAccessExprCon
                     }
                     return new MachineAccessExpr(context, m, subExpr, mfield);
 
-                case PermissionType {Origin: NamedEventSet} permission:
+                case PermissionType {Origin: NamedEventSet} permission when isPVerifier:
 
                     var pevents = ((NamedEventSet)permission.Origin).Events.ToList();
 
@@ -107,7 +110,7 @@ public override IPExpr VisitNamedTupleAccessExpr(PParser.NamedTupleAccessExprCon
 
                     throw handler.MissingEventField(context.field, pevents.First());
 
-                case PrimitiveType pt when pt.IsSameTypeAs(PrimitiveType.Machine):
+                case PrimitiveType pt when pt.IsSameTypeAs(PrimitiveType.Machine) && isPVerifier:
                     Machine spec;
 
                     switch (subExpr)

Src/PCompiler/CompilerCore/TypeChecker/ProofBlockVisitor.cs

@@ -60,7 +60,7 @@ public override object VisitProveUsingCmd(PParser.ProveUsingCmdContext context)
             var proofCmd = (ProofCommand)nodesToDeclarations.Get(context);
             var temporaryFunction = new Function(proofCmd.Name, context);
             temporaryFunction.Scope = CurrentScope.MakeChildScope();
-            var exprVisitor = new ExprVisitor(temporaryFunction, Handler);
+            var exprVisitor = new ExprVisitor(temporaryFunction, Handler, isPVerifier: true);
             List<IPExpr> premises = [];
             List<IPExpr> goals = [];
             List<IPExpr> excepts = context._excludes.Select(exprVisitor.Visit).ToList();

Src/PCompiler/CompilerCore/TypeChecker/StatementVisitor.cs

@@ -26,7 +26,7 @@ public StatementVisitor(ICompilerConfiguration config, Machine machine, Function
             this.machine = machine;
             this.method = method;
             table = method.Scope;
-            exprVisitor = new ExprVisitor(method, config.Handler);
+            exprVisitor = new ExprVisitor(method, config.Handler, config.OutputLanguages.Contains(CompilerOutput.PVerifier));
         }
 
         public override IPStmt VisitFunctionBody(PParser.FunctionBodyContext context)

Tst/RegressionTests/Feature3Exprs/StaticError/MachineFieldAccess/MachineFieldAccess.p

@@ -0,0 +1,28 @@
+// Test case for GitHub issue #920
+// Accessing a field of a machine reference should produce a compile error
+// rather than an unhandled ArgumentOutOfRangeException
+
+event eStart;
+
+machine Server {
+    var database: int;
+
+    start state Init {
+        entry {
+            database = 42;
+        }
+    }
+}
+
+machine Client {
+    var server: Server;
+    var x: int;
+
+    start state Init {
+        entry (s: Server) {
+            server = s;
+            // This should produce a static error - cannot access machine fields
+            x = server.database;
+        }
+    }
+}

Tst/RegressionTests/Feature3Exprs/StaticError/MachineFieldAccessInExpr/MachineFieldAccessInExpr.p

@@ -0,0 +1,27 @@
+// Test case for GitHub issue #920 - machine field access in expressions
+// Using machine field access in arithmetic expressions should produce a compile error
+
+event eStart;
+
+machine Counter {
+    var count: int;
+
+    start state Init {
+        entry {
+            count = 10;
+        }
+    }
+}
+
+machine Client {
+    var counter: Counter;
+    var result: int;
+
+    start state Init {
+        entry (c: Counter) {
+            counter = c;
+            // This should produce a static error - machine field access in expression
+            result = counter.count + 5;
+        }
+    }
+}

Tst/RegressionTests/Feature3Exprs/StaticError/MachineFieldAccessNested/MachineFieldAccessNested.p

@@ -0,0 +1,37 @@
+// Test case for GitHub issue #920 - nested machine field access
+// Accessing fields through a chain of machine references should produce a compile error
+
+event eInit: Server;
+
+machine Database {
+    var storedValue: int;
+
+    start state Init {
+        entry {
+            storedValue = 100;
+        }
+    }
+}
+
+machine Server {
+    var database: Database;
+
+    start state Init {
+        entry {
+            database = new Database();
+        }
+    }
+}
+
+machine Client {
+    var server: Server;
+    var x: int;
+
+    start state Init {
+        entry (s: Server) {
+            server = s;
+            // This should produce a static error - nested machine field access
+            x = server.database.storedValue;
+        }
+    }
+}