Skip to content

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

New issue

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

Sign up for GitHub

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

Already on GitHub? Sign in to your account

Merged
merged 4 commits into from
May 22, 2025
Merged

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

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
4a6884c
save fixes
AD1024 May 21, 2025
af7a82b
retrigger checks
AD1024 May 21, 2025
8995a16
Merge branch 'dev_p3.0/pverifier' into pverifier-compiler-fix
AD1024 May 21, 2025
b4280c7
fill in proof block at the end of scope construction
AD1024 May 21, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
63 changes: 63 additions & 0 deletions Src/PCompiler/CompilerCore/TypeChecker/Analyzer.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
{
Expand Down Expand Up @@ -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)
{
Expand Down Expand Up @@ -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)
{
Expand Down Expand Up @@ -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;
}
Expand Down
189 changes: 3 additions & 186 deletions Src/PCompiler/CompilerCore/TypeChecker/DeclarationVisitor.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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;
}

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

Expand Down
Loading
Loading