[fix] Postpone type checking of invariants, axioms, init-conditions and pure functions (#865)

* save fixes

* retrigger checks

* fill in proof block at the end of scope construction

Author: AD1024

Src/PCompiler/CompilerCore/TypeChecker/Analyzer.cs

@@ -1,9 +1,11 @@
 using System;
 using System.Collections.Generic;
 using System.Linq;
+using Antlr4.Runtime;
 using Antlr4.Runtime.Tree;
 using Plang.Compiler.TypeChecker.AST;
 using Plang.Compiler.TypeChecker.AST.Declarations;
+using Plang.Compiler.TypeChecker.Types;
 
 namespace Plang.Compiler.TypeChecker
 {
@@ -32,6 +34,50 @@ public static Scope AnalyzeCompilationUnit(ICompilerConfiguration config,
                 FunctionValidator.CheckAllPathsReturn(handler, machineFunction);
             }
 
+            // Step 3b: for PVerifier, fill in body of Invariants, Axioms, Init conditions and Pure functions
+            foreach (var inv in globalScope.Invariants)
+            {
+                var ctx = (PParser.InvariantDeclContext) inv.SourceLocation;
+                var temporaryFunction = new Function(inv.Name, inv.SourceLocation)
+                {
+                    Scope = globalScope
+                };
+                inv.Body = PopulateExpr(temporaryFunction, ctx.body, PrimitiveType.Bool, handler);
+            }
+
+            foreach (var axiom in globalScope.Axioms)
+            {
+                var ctx = (PParser.AxiomDeclContext) axiom.SourceLocation;
+                var temporaryFunction = new Function(axiom.Name, axiom.SourceLocation)
+                {
+                    Scope = globalScope
+                };
+                axiom.Body = PopulateExpr(temporaryFunction, ctx.body, PrimitiveType.Bool, handler);
+            }
+
+            foreach (var initCond in globalScope.AssumeOnStarts)
+            {
+                var ctx = (PParser.AssumeOnStartDeclContext)initCond.SourceLocation;
+                var temporaryFunction = new Function(initCond.Name, initCond.SourceLocation)
+                {
+                    Scope = globalScope
+                };
+                initCond.Body = PopulateExpr(temporaryFunction, ctx.body, PrimitiveType.Bool, handler); 
+            }
+
+            foreach (var pure in globalScope.Pures)
+            {
+                var temporaryFunction = new Function(pure.Name, pure.SourceLocation)
+                {
+                    Scope = pure.Scope
+                };
+                var context = (PParser.PureDeclContext) pure.SourceLocation;
+                if (context.body is not null)
+                {
+                    pure.Body = PopulateExpr(temporaryFunction, context.body, pure.Signature.ReturnType, handler);
+                }
+            }
+
             // Step 2b: Validate no static handlers
             foreach (var machine in globalScope.Machines)
             {
@@ -120,6 +166,17 @@ public static Scope AnalyzeCompilationUnit(ICompilerConfiguration config,
             return globalScope;
         }
 
+        private static IPExpr PopulateExpr(Function func, ParserRuleContext ctx, PLanguageType type, ITranslationErrorHandler handler)
+        {
+            var exprVisitor = new ExprVisitor(func, handler);
+            var body = exprVisitor.Visit(ctx);
+            if (!type.IsSameTypeAs(body.Type))
+            {
+                throw handler.TypeMismatch(ctx, body.Type, type);
+            }
+            return body;
+        }
+
         private static Propagation<T> CreatePropagation<T>(Func<Function, T> getter, Action<Function, T> setter,
             T value)
         {
@@ -180,6 +237,12 @@ private static Scope BuildGlobalScope(ICompilerConfiguration config, PParser.Pro
             {
                 DeclarationVisitor.PopulateDeclarations(config.Handler, globalScope, programUnit, nodesToDeclarations);
             }
+
+            // Step 3: fill in proof blocks
+            foreach (var proofBlock in globalScope.ProofBlocks)
+            {
+                ProofBlockVisitor.PopulateProofBlocks(config.Handler, globalScope, proofBlock.SourceLocation, nodesToDeclarations);
+            }
 
             return globalScope;
         }

Src/PCompiler/CompilerCore/TypeChecker/DeclarationVisitor.cs

@@ -48,7 +48,7 @@ public static void PopulateDeclarations(
         public override object VisitEventDecl(PParser.EventDeclContext context)
         {
             // EVENT name=Iden
-            var pEvent = (Event) nodesToDeclarations.Get(context);
+            var pEvent = (Event)nodesToDeclarations.Get(context);
 
             // cardinality?
             var hasAssume = context.cardinality()?.ASSUME() != null;
@@ -633,63 +633,21 @@ public override object VisitPureDecl(PParser.PureDeclContext context)
             // (COLON type)?
             pure.Signature.ReturnType = ResolveType(context.type());
 
-            if (context.body is not null)
-            {
-                var exprVisitor = new ExprVisitor(temporaryFunction, Handler);
-                var body = exprVisitor.Visit(context.body);
-                
-                if (!pure.Signature.ReturnType.IsSameTypeAs(body.Type))
-                {
-                    throw Handler.TypeMismatch(context.body, body.Type, pure.Signature.ReturnType);
-                }
-
-                pure.Body = body;
-            }
-            
+            // body will be handled in a later stage
             return pure;
         }
 
         public override object VisitInvariantDecl(PParser.InvariantDeclContext context)
         {
             // INVARIANT name=Iden body=Expr
             var inv = (Invariant) nodesToDeclarations.Get(context);
-            
-            var temporaryFunction = new Function(inv.Name, context);
-            temporaryFunction.Scope = CurrentScope.MakeChildScope();
-            
-            var exprVisitor = new ExprVisitor(temporaryFunction, Handler);
-            
-            var body = exprVisitor.Visit(context.body);
-            
-            if (!PrimitiveType.Bool.IsSameTypeAs(body.Type))
-            {
-                throw Handler.TypeMismatch(context.body, body.Type, PrimitiveType.Bool);
-            }
-
-            inv.Body = body;
-            
             return inv;
         }
 
         public override object VisitAxiomDecl(PParser.AxiomDeclContext context)
         {
             // Axiom body=Expr
             var inv = (Axiom) nodesToDeclarations.Get(context);
-            
-            var temporaryFunction = new Function(inv.Name, context);
-            temporaryFunction.Scope = CurrentScope.MakeChildScope();
-            
-            var exprVisitor = new ExprVisitor(temporaryFunction, Handler);
-            
-            var body = exprVisitor.Visit(context.body);
-            
-            if (!PrimitiveType.Bool.IsSameTypeAs(body.Type))
-            {
-                throw Handler.TypeMismatch(context.body, body.Type, PrimitiveType.Bool);
-            }
-
-            inv.Body = body;
-            
             return inv;
         }
 
@@ -699,153 +657,12 @@ public override object VisitInvariantGroupDecl(PParser.InvariantGroupDeclContext
             invGroup.Invariants = context.invariantDecl().Select(Visit).Cast<Invariant>().ToList();
             return invGroup;
         }
-
-        private List<Invariant> ToInvariant(IPExpr e, ParserRuleContext context)
-        {
-            if (e is InvariantGroupRefExpr invGroupRef) return invGroupRef.Invariants;
-            if (e is InvariantRefExpr invRef) return [invRef.Invariant];
-            if (!PrimitiveType.Bool.IsSameTypeAs(e.Type.Canonicalize()))
-            {
-                throw Handler.TypeMismatch(context, e.Type, PrimitiveType.Bool);
-            }
-            Invariant inv = new Invariant($"tmp_inv_{Guid.NewGuid()}", e, context);
-            return [inv];
-        }
-
-        public override object VisitProofBlock(PParser.ProofBlockContext context)
-        {
-            var proofBlock = (ProofBlock) nodesToDeclarations.Get(context);
-            proofBlock.Commands = context.proofBody().proofItem().Select(Visit).Cast<ProofCommand>().ToList();
-            proofBlock.Commands.ForEach(x => x.ProofBlock = proofBlock.Name);
-            return proofBlock;
-        }
-
-        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);
-            List<IPExpr> premises = [];
-            List<IPExpr> goals = [];
-            List<IPExpr> excepts = context._excludes.Select(exprVisitor.Visit).ToList();
-            if (context.premisesAll == null)
-            {
-                premises = context._premises.Select(exprVisitor.Visit).ToList();
-            }
-            else
-            {
-                premises = CurrentScope.AllDecls.OfType<Invariant>().Select(x => (IPExpr) new InvariantRefExpr(x, context)).ToList();
-            }
-            
-            if (context.goalsAll == null && context.goalsDefault == null)
-            {
-                goals = context._targets.Select(exprVisitor.Visit).ToList();
-            }
-            else if (context.goalsDefault != null)
-            {
-                goals = [new InvariantRefExpr(new Invariant(context), context)];
-            }
-            else
-            {
-                goals = CurrentScope.AllDecls.OfType<Invariant>().Select(x => (IPExpr) new InvariantRefExpr(x, context)).ToList();
-            }
-            
-            if (premises.Count == context._premises.Count)
-            {
-                proofCmd.Premises = premises.Zip(context._premises, (x, y) => ToInvariant(x, y)).SelectMany(x => x).ToList();
-            }
-            else
-            {
-                proofCmd.Premises = premises.SelectMany(x => ToInvariant(x, context)).ToList();
-            }
-            
-            if (goals.Count == context._targets.Count)
-            {
-                proofCmd.Goals = goals.Zip(context._targets, (x, y) => ToInvariant(x, y)).SelectMany(x => x).ToList();
-            }
-            else
-            {
-                proofCmd.Goals = goals.SelectMany(x => ToInvariant(x, context)).ToList();
-            }
-            
-            proofCmd.Excepts = excepts.Zip(context._excludes, (x, y) => ToInvariant(x, y)).SelectMany(x => x).ToList();
-            proofCmd.Premises = proofCmd.Premises.Except(proofCmd.Excepts).ToList();
-            proofCmd.Goals = proofCmd.Goals.Except(proofCmd.Excepts).ToList();
-            
-            // prove A using B, ..., C means A -> B, ..., A -> C
-            // If there is a cycle in the graph formed by all prove-using commands, then we should throw an error. 
-            // We could do this incrementally but the number of prove-using commands will probably be very small anyway
-            // so we are just going to do a topological sort every time (https://gist.github.com/Sup3rc4l1fr4g1l1571c3xp14l1d0c10u5/3341dba6a53d7171fe3397d13d00ee3f)
-            // TODO: using _ to pick out sub invariants?
-            var nodes = new System.Collections.Generic.HashSet<string>();
-            var edges = new System.Collections.Generic.HashSet<(string, string)>();
-            foreach (var cmd in CurrentScope.ProofCommands)
-            {
-                if (cmd.Goals is null) continue;
-                foreach (var source in cmd.Goals.Select(inv => inv.Name))
-                {
-                    if (cmd.Premises is null) continue;
-                    foreach (var target in cmd.Premises.Select(inv => inv.Name))
-                    {
-                        nodes.Add(source);
-                        nodes.Add(target);
-                        edges.Add((source, target));
-                    }
-                }
-            }
-            
-            // Set of all nodes with no incoming edges
-            var S = new System.Collections.Generic.HashSet<string>(nodes.Where(n => edges.All(e => e.Item2.Equals(n) == false)));
-
-            // while S is non-empty do
-            while (S.Any()) {
-
-                //  remove a node n from S
-                var n = S.First();
-                S.Remove(n);
-
-                // for each node m with an edge e from n to m do
-                foreach (var e in edges.Where(e => e.Item1.Equals(n)).ToList()) {
-                    var m = e.Item2;
-
-                    // remove edge e from the graph
-                    edges.Remove(e);
-
-                    // if m has no other incoming edges then
-                    if (edges.All(me => me.Item2.Equals(m) == false)) {
-                        S.Add(m);
-                    }
-                }
-            }
-            
-            // if graph has edges then
-            if (edges.Any()) {
-                throw Handler.CyclicProof(proofCmd.SourceLocation, proofCmd);
-            }
-            
-            return proofCmd;
-        }
 
         public override object VisitAssumeOnStartDecl(PParser.AssumeOnStartDeclContext context)
         {
             // assume on start: body=Expr
             var assume = (AssumeOnStart) nodesToDeclarations.Get(context);
-            
-            var temporaryFunction = new Function(assume.Name, context);
-            temporaryFunction.Scope = CurrentScope.MakeChildScope();
-            
-            var exprVisitor = new ExprVisitor(temporaryFunction, Handler);
-            
-            var body = exprVisitor.Visit(context.body);
-            
-            if (!PrimitiveType.Bool.IsSameTypeAs(body.Type))
-            {
-                throw Handler.TypeMismatch(context.body, body.Type, PrimitiveType.Bool);
-            }
-
-            assume.Body = body;
-            
+            // body will be handled in a later stage
             return assume;
         }