From d28df0fd0ded0d2777d2f4fe01d913cc53b60abf Mon Sep 17 00:00:00 2001 From: Remy Willems <> Date: Mon, 8 Nov 2021 12:41:20 +0100 Subject: [PATCH 01/23] Fix typo in name --- Source/Core/Prune/AxiomVisitor.cs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Source/Core/Prune/AxiomVisitor.cs b/Source/Core/Prune/AxiomVisitor.cs index 98cfca003..b5452440a 100644 --- a/Source/Core/Prune/AxiomVisitor.cs +++ b/Source/Core/Prune/AxiomVisitor.cs @@ -32,12 +32,12 @@ public override Expr VisitExpr(Expr node) { AddIncoming(f.Func); AddOutgoing(f.Func); } else if (node is NAryExpr n) { - var appliable = n.Fun; - if (appliable is UnaryOperator op) { + var applicable = n.Fun; + if (applicable is UnaryOperator op) { Contract.Assert(op.Op == UnaryOperator.Opcode.Neg || op.Op == UnaryOperator.Opcode.Not); Contract.Assert(n.Args.Count() == 1); n.Args[0].pos = Expr.NegatePosition(n.Args[0].pos); - } else if (appliable is BinaryOperator bin) { + } else if (applicable is BinaryOperator bin) { Contract.Assert(n.Args.Count() == 2); if (bin.Op == BinaryOperator.Opcode.And || bin.Op == BinaryOperator.Opcode.Or) { From 62f6e6b37e364c8495e7fb13ba5f8ae27ee97377 Mon Sep 17 00:00:00 2001 From: Remy Willems <> Date: Mon, 8 Nov 2021 12:42:03 +0100 Subject: [PATCH 02/23] Fix bug in testcase, causing it to always give the same result regardless of pruning --- Test/test0/Prune.bpl | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Test/test0/Prune.bpl b/Test/test0/Prune.bpl index 330374089..0895a997d 100644 --- a/Test/test0/Prune.bpl +++ b/Test/test0/Prune.bpl @@ -20,7 +20,7 @@ axiom (forall x: int :: procedure I1(x : int) returns (y: int) requires R(x); - ensures Q(f1(y)); // this post-condition doesn't prove because f1 is attributed as exclude_dep and + ensures Q(f1(x)); // this post-condition doesn't prove because f1 is attributed as exclude_dep and // is thus removed from the outgoing set of I1. // This makes the axiom on line 23 unreachable from I1, which is thus pruned away. { From ce74b0a9d9c65cea6e612b7b0ef9299bc29bc301 Mon Sep 17 00:00:00 2001 From: Remy Willems <> Date: Mon, 8 Nov 2021 12:43:24 +0100 Subject: [PATCH 03/23] Fix bugs related to triggers with multiple conditions --- Source/Core/Prune/AxiomVisitor.cs | 2 +- Source/Core/Prune/DependencyEvaluator.cs | 4 +--- Source/Graph/Graph.cs | 7 +++---- 3 files changed, 5 insertions(+), 8 deletions(-) diff --git a/Source/Core/Prune/AxiomVisitor.cs b/Source/Core/Prune/AxiomVisitor.cs index b5452440a..ad3495fe6 100644 --- a/Source/Core/Prune/AxiomVisitor.cs +++ b/Source/Core/Prune/AxiomVisitor.cs @@ -21,7 +21,7 @@ private void VisitTriggerCustom(Trigger t) { var triggerList = t.Tr.ToList(); triggerList.ForEach(e => e.pos = Expr.Position.Neither); triggerList.ForEach(e => visitor.VisitExpr(e)); - AddIncoming(visitor.incomingSets.SelectMany(x => x).ToArray()); + AddIncoming(visitor.outgoing.ToArray()); } public override Expr VisitExpr(Expr node) { diff --git a/Source/Core/Prune/DependencyEvaluator.cs b/Source/Core/Prune/DependencyEvaluator.cs index ab0130b32..1f42c1423 100644 --- a/Source/Core/Prune/DependencyEvaluator.cs +++ b/Source/Core/Prune/DependencyEvaluator.cs @@ -39,9 +39,7 @@ protected void AddIncoming(Declaration newIncoming) protected void AddOutgoing(Declaration newOutgoing) { - if (!ExcludeDep(newOutgoing)) { - outgoing.Add(newOutgoing); - } + outgoing.Add(newOutgoing); } protected void AddIncoming(Declaration[] declarations) diff --git a/Source/Graph/Graph.cs b/Source/Graph/Graph.cs index 2286f4a3e..ba7bafd1a 100644 --- a/Source/Graph/Graph.cs +++ b/Source/Graph/Graph.cs @@ -1182,13 +1182,12 @@ public static IEnumerable FindReachableNodesInGraphWithMergeNodes(Dictio continue; } - if (node is IReadOnlySet mergeNode) { - if (!visitedEdges.IsSupersetOf(mergeNode)) { + if (node is IEnumerable objects) { + if (!visitedEdges.IsSupersetOf(objects)) { continue; } - } else { - visitedEdges.Add(node); } + visitedEdges.Add(node); var outgoing = edges.GetValueOrDefault(node) ?? new List(); foreach (var x in outgoing) From 3b60a4a530574fdafc1948d36bd6c855f717126f Mon Sep 17 00:00:00 2001 From: Remy Willems <> Date: Tue, 9 Nov 2021 15:54:20 +0100 Subject: [PATCH 04/23] Fix bug --- Source/Core/Prune/AxiomVisitor.cs | 7 +++---- Source/Core/Prune/DependencyEvaluator.cs | 6 ++++-- Source/Core/Prune/TriggerVisitor.cs | 19 +++++++++++++++++++ 3 files changed, 26 insertions(+), 6 deletions(-) create mode 100644 Source/Core/Prune/TriggerVisitor.cs diff --git a/Source/Core/Prune/AxiomVisitor.cs b/Source/Core/Prune/AxiomVisitor.cs index ad3495fe6..b4f33b673 100644 --- a/Source/Core/Prune/AxiomVisitor.cs +++ b/Source/Core/Prune/AxiomVisitor.cs @@ -1,5 +1,4 @@ using System; -using System.Collections.Generic; using System.Diagnostics.Contracts; using System.Linq; @@ -17,11 +16,11 @@ public static DependencyEvaluator GetAxiomDependencies(Axiom axiom) } private void VisitTriggerCustom(Trigger t) { - var visitor = new AxiomVisitor((Axiom)declaration); + var visitor = new TriggerVisitor(); var triggerList = t.Tr.ToList(); - triggerList.ForEach(e => e.pos = Expr.Position.Neither); triggerList.ForEach(e => visitor.VisitExpr(e)); - AddIncoming(visitor.outgoing.ToArray()); + var incomingSet = visitor.Declarations.ToArray(); + AddIncoming(incomingSet); } public override Expr VisitExpr(Expr node) { diff --git a/Source/Core/Prune/DependencyEvaluator.cs b/Source/Core/Prune/DependencyEvaluator.cs index 1f42c1423..64b3f3a89 100644 --- a/Source/Core/Prune/DependencyEvaluator.cs +++ b/Source/Core/Prune/DependencyEvaluator.cs @@ -25,7 +25,7 @@ public class DependencyEvaluator : ReadOnlyVisitor public List incomingSets = new(); public HashSet types = new(); - private static bool ExcludeDep(Declaration declaration) + public static bool ExcludeDep(Declaration declaration) { return declaration.Attributes != null && QKeyValue.FindBoolAttribute(declaration.Attributes, "exclude_dep"); } @@ -39,7 +39,9 @@ protected void AddIncoming(Declaration newIncoming) protected void AddOutgoing(Declaration newOutgoing) { - outgoing.Add(newOutgoing); + if (!ExcludeDep(newOutgoing)) { + outgoing.Add(newOutgoing); + } } protected void AddIncoming(Declaration[] declarations) diff --git a/Source/Core/Prune/TriggerVisitor.cs b/Source/Core/Prune/TriggerVisitor.cs new file mode 100644 index 000000000..8cc5afa30 --- /dev/null +++ b/Source/Core/Prune/TriggerVisitor.cs @@ -0,0 +1,19 @@ +using System.Collections.Generic; + +namespace Microsoft.Boogie +{ + class TriggerVisitor : ReadOnlyVisitor + { + public readonly ISet Declarations = new HashSet(); + + public override Expr VisitExpr(Expr node) + { + if (node is IdentifierExpr iExpr && iExpr.Decl is Constant c) { + Declarations.Add(c); + } else if (node is NAryExpr e && e.Fun is FunctionCall f) { + Declarations.Add(f.Func); + } + return base.VisitExpr(node); + } + } +} \ No newline at end of file From 89f0ad9dcdfdc0de7809ab0bc2683ce3e50163b9 Mon Sep 17 00:00:00 2001 From: Remy Willems <> Date: Tue, 2 Nov 2021 15:08:35 +0100 Subject: [PATCH 05/23] Added uses to parser --- Source/Core/Absy.cs | 13 +- Source/Core/BoogiePL.atg | 33 +- Source/Core/Parser.cs | 719 ++++++++++++++++++---------------- Source/Core/Prune/Prune.cs | 3 +- Source/Core/Scanner.cs | 191 ++++----- Source/Graph/Graph.cs | 4 +- Test/pruning/basic.bpl | 19 + Test/pruning/basic.bpl.expect | 2 + 8 files changed, 537 insertions(+), 447 deletions(-) create mode 100644 Test/pruning/basic.bpl create mode 100644 Test/pruning/basic.bpl.expect diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index dcca7e5e4..f695dc15e 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -1779,6 +1779,11 @@ public override void Emit(TokenTextWriter stream, int level) public class Axiom : Declaration { + public override string ToString() + { + return "Axiom: " + expression.ToString(); + } + private Expr /*!*/ expression; @@ -2472,6 +2477,8 @@ public class Constant : Variable // that the parental situation is unconstrained. public readonly ReadOnlyCollection Parents; + public IList NewDefinitionAxioms; + [ContractInvariantMethod] void ObjectInvariant() { @@ -3301,12 +3308,10 @@ public class Function : DeclWithFormals public NAryExpr DefinitionBody; // Only set if the function is declared with {:define} public Axiom DefinitionAxiom; + public IList NewDefinitionAxioms; public IList otherDefinitionAxioms; - public IEnumerable OtherDefinitionAxioms - { - get { return otherDefinitionAxioms; } - } + public IEnumerable OtherDefinitionAxioms => otherDefinitionAxioms; public void AddOtherDefinitionAxiom(Axiom axiom) { diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index f5e74eaa3..abc21e382 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -185,7 +185,7 @@ BoogiePL Implementation im; Implementation/*!*/ nnim; .) - { Consts (. foreach(Bpl.Variable/*!*/ v in vs){ + { Consts (. foreach(Bpl.Declaration/*!*/ v in ds){ Contract.Assert(v != null); Pgm.AddTopLevelDeclaration(v); } @@ -395,9 +395,11 @@ Types<.List/*!*/ ts.> /*------------------------------------------------------------------------*/ -Consts<.out List/*!*/ ds.> +Consts<.out List/*!*/ ds.> = (. Contract.Ensures(Contract.ValueAtReturn(out ds) != null); IToken/*!*/ y; List/*!*/ xs; - ds = new List(); + ds = new List(); + var axioms = new List(); + Axiom ax; bool u = false; QKeyValue kv = null; bool ChildrenComplete = false; List Parents = null; .) @@ -424,11 +426,16 @@ Consts<.out List/*!*/ ds.> ParentsClone = Parents; } makeClone = true; - - ds.Add(new Constant(y, x, u, ParentsClone, ChildrenComplete, kv)); + + foreach(var axiom in axioms) { + ds.Add(axiom); + } + var constant = new Constant(y, x, u, ParentsClone, ChildrenComplete, kv); + constant.NewDefinitionAxioms = axioms; + ds.Add(constant); } .) - ";" + ( ";" | "uses" "{" { Axiom(. axioms.Add(ax); .) } "}") . OrderSpec<.out bool ChildrenComplete, out List Parents.> @@ -462,6 +469,7 @@ Function<.out List/*!*/ ds.> IToken/*!*/ typeParamTok; var typeParams = new List(); var arguments = new List(); + var axioms = new List(); TypedIdent/*!*/ tyd; TypedIdent retTyd = null; Bpl.Type/*!*/ retTy; @@ -469,6 +477,7 @@ Function<.out List/*!*/ ds.> QKeyValue kv = null; Expr definition = null; Expr/*!*/ tmp; + Axiom ax; .) "function" { Attribute } Ident [ TypeParams ] @@ -482,7 +491,10 @@ Function<.out List/*!*/ ds.> | ":" Type (. retTyd = new TypedIdent(retTy.tok, TypedIdent.NoName, retTy); .) ) - ( "{" Expression (. definition = tmp; .) "}" | ";" ) + ( "{" Expression (. definition = tmp; .) "}" [ "uses" "{" { Axiom(. axioms.Add(ax); .) } "}" ] | + "uses" "{" { Axiom(. axioms.Add(ax); .) } "}" | + ";" + ) (. if (retTyd == null) { // construct a dummy type for the case of syntax error @@ -490,10 +502,15 @@ Function<.out List/*!*/ ds.> } Function/*!*/ func = new Function(z, z.val, typeParams, arguments, new Formal(retTyd.tok, retTyd, false, argKv), null, kv); + func.NewDefinitionAxioms = axioms; + foreach(var axiom in axioms) { + ds.Add(axiom); + } + Contract.Assert(func != null); ds.Add(func); bool allUnnamed = true; - foreach(Formal/*!*/ f in arguments){ + foreach(Formal/*!*/ f in arguments) { Contract.Assert(f != null); if (f.TypedIdent.HasName) { allUnnamed = false; diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index a2078a7d4..dcfb0c96b 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -35,7 +35,7 @@ public class Parser { public const int _decimal = 5; public const int _dec_float = 6; public const int _float = 7; - public const int maxT = 107; + public const int maxT = 108; const bool _T = true; const bool _x = false; @@ -241,15 +241,15 @@ void BoogiePL() { while (StartOf(1)) { switch (la.kind) { case 22: { - Consts(out vs); - foreach(Bpl.Variable/*!*/ v in vs){ + Consts(out ds); + foreach(Bpl.Declaration/*!*/ v in ds){ Contract.Assert(v != null); Pgm.AddTopLevelDeclaration(v); } break; } - case 26: { + case 29: { Function(out ds); foreach(Bpl.Declaration/*!*/ d in ds){ Contract.Assert(d != null); @@ -258,12 +258,12 @@ void BoogiePL() { break; } - case 30: { + case 31: { Axiom(out ax); Pgm.AddTopLevelDeclaration(ax); break; } - case 31: { + case 32: { UserDefinedTypes(out ts); foreach(Declaration/*!*/ td in ts){ Contract.Assert(td != null); @@ -281,7 +281,7 @@ void BoogiePL() { break; } - case 33: { + case 34: { Procedure(out pr, out im); Pgm.AddTopLevelDeclaration(pr); if (im != null) { @@ -290,7 +290,7 @@ void BoogiePL() { break; } - case 34: { + case 35: { Implementation(out nnim); Pgm.AddTopLevelDeclaration(nnim); break; @@ -300,15 +300,17 @@ void BoogiePL() { Expect(0); } - void Consts(out List/*!*/ ds) { + void Consts(out List/*!*/ ds) { Contract.Ensures(Contract.ValueAtReturn(out ds) != null); IToken/*!*/ y; List/*!*/ xs; - ds = new List(); + ds = new List(); + var axioms = new List(); + Axiom ax; bool u = false; QKeyValue kv = null; bool ChildrenComplete = false; List Parents = null; Expect(22); y = t; - while (la.kind == 28) { + while (la.kind == 25) { Attribute(ref kv); } if (la.kind == 23) { @@ -316,7 +318,7 @@ void Consts(out List/*!*/ ds) { u = true; } IdsType(out xs); - if (la.kind == 24) { + if (la.kind == 27) { OrderSpec(out ChildrenComplete, out Parents); } bool makeClone = false; @@ -336,11 +338,26 @@ void Consts(out List/*!*/ ds) { ParentsClone = Parents; } makeClone = true; - - ds.Add(new Constant(y, x, u, ParentsClone, ChildrenComplete, kv)); + + foreach(var axiom in axioms) { + ds.Add(axiom); + } + var constant = new Constant(y, x, u, ParentsClone, ChildrenComplete, kv); + constant.NewDefinitionAxioms = axioms; + ds.Add(constant); } - Expect(9); + if (la.kind == 9) { + Get(); + } else if (la.kind == 24) { + Get(); + Expect(25); + while (la.kind == 31) { + Axiom(out ax); + axioms.Add(ax); + } + Expect(26); + } else SynErr(109); } void Function(out List/*!*/ ds) { @@ -349,6 +366,7 @@ void Function(out List/*!*/ ds) { IToken/*!*/ typeParamTok; var typeParams = new List(); var arguments = new List(); + var axioms = new List(); TypedIdent/*!*/ tyd; TypedIdent retTyd = null; Bpl.Type/*!*/ retTy; @@ -356,9 +374,10 @@ void Function(out List/*!*/ ds) { QKeyValue kv = null; Expr definition = null; Expr/*!*/ tmp; + Axiom ax; - Expect(26); - while (la.kind == 28) { + Expect(29); + while (la.kind == 25) { Attribute(ref kv); } Ident(out z); @@ -377,7 +396,7 @@ void Function(out List/*!*/ ds) { } Expect(11); argKv = null; - if (la.kind == 27) { + if (la.kind == 30) { Get(); Expect(10); VarOrType(out retTyd, out argKv); @@ -386,25 +405,47 @@ void Function(out List/*!*/ ds) { Get(); Type(out retTy); retTyd = new TypedIdent(retTy.tok, TypedIdent.NoName, retTy); - } else SynErr(108); - if (la.kind == 28) { + } else SynErr(110); + if (la.kind == 25) { Get(); Expression(out tmp); definition = tmp; - Expect(29); + Expect(26); + if (la.kind == 24) { + Get(); + Expect(25); + while (la.kind == 31) { + Axiom(out ax); + axioms.Add(ax); + } + Expect(26); + } + } else if (la.kind == 24) { + Get(); + Expect(25); + while (la.kind == 31) { + Axiom(out ax); + axioms.Add(ax); + } + Expect(26); } else if (la.kind == 9) { Get(); - } else SynErr(109); + } else SynErr(111); if (retTyd == null) { // construct a dummy type for the case of syntax error retTyd = new TypedIdent(t, TypedIdent.NoName, new BasicType(t, SimpleType.Int)); } Function/*!*/ func = new Function(z, z.val, typeParams, arguments, new Formal(retTyd.tok, retTyd, false, argKv), null, kv); + func.NewDefinitionAxioms = axioms; + foreach(var axiom in axioms) { + ds.Add(axiom); + } + Contract.Assert(func != null); ds.Add(func); bool allUnnamed = true; - foreach(Formal/*!*/ f in arguments){ + foreach(Formal/*!*/ f in arguments) { Contract.Assert(f != null); if (f.TypedIdent.HasName) { allUnnamed = false; @@ -455,8 +496,8 @@ void Function(out List/*!*/ ds) { void Axiom(out Axiom/*!*/ m) { Contract.Ensures(Contract.ValueAtReturn(out m) != null); Expr/*!*/ e; QKeyValue kv = null; - Expect(30); - while (la.kind == 28) { + Expect(31); + while (la.kind == 25) { Attribute(ref kv); } IToken/*!*/ x = t; @@ -467,8 +508,8 @@ void Axiom(out Axiom/*!*/ m) { void UserDefinedTypes(out List/*!*/ ts) { Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out ts))); Declaration/*!*/ decl; QKeyValue kv = null; ts = new List (); - Expect(31); - while (la.kind == 28) { + Expect(32); + while (la.kind == 25) { Attribute(ref kv); } UserDefinedType(out decl, kv); @@ -488,7 +529,7 @@ void GlobalVars(out List/*!*/ ds) { var dsx = ds; Expect(8); - while (la.kind == 28) { + while (la.kind == 25) { Attribute(ref kv); } IdsTypeWheres(true, "global variables", delegate(TypedIdent tyd) { dsx.Add(new GlobalVariable(tyd.tok, tyd, kv)); } ); @@ -508,7 +549,7 @@ void Procedure(out Procedure/*!*/ proc, out /*maybe null*/ Implementation impl) QKeyValue kv = null; impl = null; - Expect(33); + Expect(34); ProcSignature(true, out x, out typeParams, out ins, out outs, out kv); if (la.kind == 9) { Get(); @@ -523,7 +564,7 @@ void Procedure(out Procedure/*!*/ proc, out /*maybe null*/ Implementation impl) impl = new Implementation(x, x.val, typeParams.ConvertAll(tp => new TypeVariable(tp.tok, tp.Name)), Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, kv == null ? null : (QKeyValue)kv.Clone(), this.errors); - } else SynErr(110); + } else SynErr(112); proc = new Procedure(x, x.val, typeParams, ins, outs, pre, mods, post, kv); } @@ -535,7 +576,7 @@ void Implementation(out Implementation/*!*/ impl) { StmtList/*!*/ stmtList; QKeyValue kv; - Expect(34); + Expect(35); ProcSignature(false, out x, out typeParams, out ins, out outs, out kv); ImplBody(out locals, out stmtList); impl = new Implementation(x, x.val, typeParams, ins, outs, locals, stmtList, kv, this.errors); @@ -560,7 +601,7 @@ void LocalVars(List/*!*/ ds) { QKeyValue kv = null; Expect(8); - while (la.kind == 28) { + while (la.kind == 25) { Attribute(ref kv); } IdsTypeWheres(true, "local variables", delegate(TypedIdent tyd) { ds.Add(new LocalVariable(tyd.tok, tyd, kv)); } ); @@ -574,7 +615,7 @@ void ProcFormals(bool incoming, bool allowWhereClauses, out List/*!*/ var context = allowWhereClauses ? "procedure formals" : "the 'implementation' copies of formals"; Expect(10); - if (la.kind == 1 || la.kind == 28) { + if (la.kind == 1 || la.kind == 25) { AttrsIdsTypeWheres(allowWhereClauses, allowWhereClauses, context, delegate(TypedIdent tyd, QKeyValue kv) { dsx.Add(new Formal(tyd.tok, tyd, incoming, kv)); }); } Expect(11); @@ -634,12 +675,12 @@ void Type(out Bpl.Type/*!*/ ty) { ty = new UnresolvedTypeIdentifier (tok, tok.val, args); } else if (la.kind == 18 || la.kind == 20) { MapType(out ty); - } else SynErr(111); + } else SynErr(113); } void AttributesIdsTypeWhere(bool allowAttributes, bool allowWhereClauses, string context, System.Action action ) { QKeyValue kv = null; - while (la.kind == 28) { + while (la.kind == 25) { Attribute(ref kv); if (!allowAttributes) { kv = null; @@ -675,7 +716,7 @@ void IdsTypeWhere(bool allowWhereClauses, string context, System.Action/*!*/ ts) { } else if (la.kind == 18 || la.kind == 20) { MapType(out ty); ts.Add(ty); - } else SynErr(113); + } else SynErr(115); } void MapType(out Bpl.Type/*!*/ ty) { @@ -782,7 +823,7 @@ void OrderSpec(out bool ChildrenComplete, out List Parents) Parents = null; bool u; IToken/*!*/ parent; - Expect(24); + Expect(27); Parents = new List (); u = false; if (la.kind == 1 || la.kind == 23) { @@ -805,7 +846,7 @@ void OrderSpec(out bool ChildrenComplete, out List Parents) new IdentifierExpr(parent, parent.val), u)); } } - if (la.kind == 25) { + if (la.kind == 28) { Get(); ChildrenComplete = true; } @@ -818,7 +859,7 @@ void VarOrType(out TypedIdent/*!*/ tyd, out QKeyValue kv) { IToken/*!*/ tok; kv = null; - while (la.kind == 28) { + while (la.kind == 25) { Attribute(ref kv); } Type(out ty); @@ -849,7 +890,7 @@ void UserDefinedType(out Declaration/*!*/ decl, QKeyValue kv) { if (la.kind == 1) { WhiteSpaceIdents(out paramTokens); } - if (la.kind == 32) { + if (la.kind == 33) { Get(); Type(out body); synonym = true; @@ -881,7 +922,7 @@ void ProcSignature(bool allowWhereClausesOnFormals, out IToken/*!*/ name, out Li Contract.Ensures(Contract.ValueAtReturn(out name) != null); Contract.Ensures(Contract.ValueAtReturn(out typeParams) != null); Contract.Ensures(Contract.ValueAtReturn(out ins) != null); Contract.Ensures(Contract.ValueAtReturn(out outs) != null); IToken/*!*/ typeParamTok; typeParams = new List(); outs = new List(); kv = null; - while (la.kind == 28) { + while (la.kind == 25) { Attribute(ref kv); } Ident(out name); @@ -889,7 +930,7 @@ void ProcSignature(bool allowWhereClausesOnFormals, out IToken/*!*/ name, out Li TypeParams(out typeParamTok, out typeParams); } ProcFormals(true, allowWhereClausesOnFormals, out ins); - if (la.kind == 27) { + if (la.kind == 30) { Get(); ProcFormals(false, allowWhereClausesOnFormals, out outs); } @@ -897,7 +938,7 @@ void ProcSignature(bool allowWhereClausesOnFormals, out IToken/*!*/ name, out Li void Spec(List/*!*/ pre, List/*!*/ mods, List/*!*/ post) { Contract.Requires(pre != null); Contract.Requires(mods != null); Contract.Requires(post != null); List/*!*/ ms; - if (la.kind == 35) { + if (la.kind == 36) { Get(); if (la.kind == 1) { Idents(out ms); @@ -908,17 +949,17 @@ void Spec(List/*!*/ pre, List/*!*/ mods, List } Expect(9); - } else if (la.kind == 36) { + } else if (la.kind == 37) { Get(); SpecPrePost(true, pre, post); - } else if (la.kind == 37 || la.kind == 38) { + } else if (la.kind == 38 || la.kind == 39) { SpecPrePost(false, pre, post); - } else SynErr(114); + } else SynErr(116); } void ImplBody(out List/*!*/ locals, out StmtList/*!*/ stmtList) { Contract.Ensures(Contract.ValueAtReturn(out locals) != null); Contract.Ensures(Contract.ValueAtReturn(out stmtList) != null); locals = new List(); - Expect(28); + Expect(25); while (la.kind == 8) { LocalVars(locals); } @@ -927,25 +968,25 @@ void ImplBody(out List/*!*/ locals, out StmtList/*!*/ stmtList) { void SpecPrePost(bool free, List/*!*/ pre, List/*!*/ post) { Contract.Requires(pre != null); Contract.Requires(post != null); Expr/*!*/ e; Token tok = null; QKeyValue kv = null; - if (la.kind == 37) { + if (la.kind == 38) { Get(); tok = t; - while (la.kind == 28) { + while (la.kind == 25) { Attribute(ref kv); } Proposition(out e); Expect(9); pre.Add(new Requires(tok, free, e, null, kv)); - } else if (la.kind == 38) { + } else if (la.kind == 39) { Get(); tok = t; - while (la.kind == 28) { + while (la.kind == 25) { Attribute(ref kv); } Proposition(out e); Expect(9); post.Add(new Ensures(tok, free, e, null, kv)); - } else SynErr(115); + } else SynErr(117); } void StmtList(out StmtList/*!*/ stmtList) { @@ -981,7 +1022,7 @@ void StmtList(out StmtList/*!*/ stmtList) { cs = new List(); } - } else if (la.kind == 41 || la.kind == 43 || la.kind == 46) { + } else if (la.kind == 42 || la.kind == 44 || la.kind == 47) { StructuredCmd(out ecn); ec = ecn; if (startToken == null) { startToken = ec.tok; cs = new List(); } @@ -1001,7 +1042,7 @@ void StmtList(out StmtList/*!*/ stmtList) { } } - Expect(29); + Expect(26); IToken/*!*/ endCurly = t; if (startToken == null && bigblocks.Count == 0) { startToken = t; cs = new List(); @@ -1029,10 +1070,10 @@ void LabelOrCmd(out Cmd c, out IToken label) { LabelOrAssign(out c, out label); break; } - case 47: { + case 48: { Get(); x = t; - while (la.kind == 28) { + while (la.kind == 25) { Attribute(ref kv); } Proposition(out e); @@ -1040,10 +1081,10 @@ void LabelOrCmd(out Cmd c, out IToken label) { Expect(9); break; } - case 48: { + case 49: { Get(); x = t; - while (la.kind == 28) { + while (la.kind == 25) { Attribute(ref kv); } Proposition(out e); @@ -1051,7 +1092,7 @@ void LabelOrCmd(out Cmd c, out IToken label) { Expect(9); break; } - case 49: { + case 50: { Get(); x = t; Idents(out xs); @@ -1065,25 +1106,25 @@ void LabelOrCmd(out Cmd c, out IToken label) { break; } - case 36: case 52: case 53: { + case 37: case 53: case 54: { CallCmd(out cn); Expect(9); c = cn; break; } - case 54: { + case 55: { ParCallCmd(out cn); c = cn; break; } - case 50: { + case 51: { Get(); x = t; Expect(9); c = new YieldCmd(x); break; } - default: SynErr(116); break; + default: SynErr(118); break; } } @@ -1091,16 +1132,16 @@ void StructuredCmd(out StructuredCmd/*!*/ ec) { Contract.Ensures(Contract.ValueAtReturn(out ec) != null); ec = dummyStructuredCmd; Contract.Assume(cce.IsPeerConsistent(ec)); IfCmd/*!*/ ifcmd; WhileCmd/*!*/ wcmd; BreakCmd/*!*/ bcmd; - if (la.kind == 41) { + if (la.kind == 42) { IfCmd(out ifcmd); ec = ifcmd; - } else if (la.kind == 43) { + } else if (la.kind == 44) { WhileCmd(out wcmd); ec = wcmd; - } else if (la.kind == 46) { + } else if (la.kind == 47) { BreakCmd(out bcmd); ec = bcmd; - } else SynErr(117); + } else SynErr(119); } void TransferCmd(out TransferCmd/*!*/ tc) { @@ -1108,7 +1149,7 @@ void TransferCmd(out TransferCmd/*!*/ tc) { Token y; List/*!*/ xs; List ss = new List(); - if (la.kind == 39) { + if (la.kind == 40) { Get(); y = t; Idents(out xs); @@ -1117,10 +1158,10 @@ void TransferCmd(out TransferCmd/*!*/ tc) { ss.Add(s.val); } tc = new GotoCmd(y, ss); - } else if (la.kind == 40) { + } else if (la.kind == 41) { Get(); tc = new ReturnCmd(t); - } else SynErr(118); + } else SynErr(120); Expect(9); } @@ -1131,21 +1172,21 @@ void IfCmd(out IfCmd/*!*/ ifcmd) { IfCmd/*!*/ elseIf; IfCmd elseIfOption = null; StmtList/*!*/ els; StmtList elseOption = null; - Expect(41); + Expect(42); x = t; Guard(out guard); - Expect(28); + Expect(25); StmtList(out thn); - if (la.kind == 42) { + if (la.kind == 43) { Get(); - if (la.kind == 41) { + if (la.kind == 42) { IfCmd(out elseIf); elseIfOption = elseIf; - } else if (la.kind == 28) { + } else if (la.kind == 25) { Get(); StmtList(out els); elseOption = els; - } else SynErr(119); + } else SynErr(121); } ifcmd = new IfCmd(x, guard, thn, elseIfOption, elseOption); } @@ -1157,18 +1198,18 @@ void WhileCmd(out WhileCmd/*!*/ wcmd) { StmtList/*!*/ body; QKeyValue kv = null; - Expect(43); + Expect(44); x = t; Guard(out guard); Contract.Assume(guard == null || cce.Owner.None(guard)); - while (la.kind == 36 || la.kind == 44) { + while (la.kind == 37 || la.kind == 45) { isFree = false; z = la/*lookahead token*/; - if (la.kind == 36) { + if (la.kind == 37) { Get(); isFree = true; } - Expect(44); - while (la.kind == 28) { + Expect(45); + while (la.kind == 25) { Attribute(ref kv); } Expression(out e); @@ -1181,7 +1222,7 @@ void WhileCmd(out WhileCmd/*!*/ wcmd) { Expect(9); } - Expect(28); + Expect(25); StmtList(out body); wcmd = new WhileCmd(x, guard, invariants, body); } @@ -1190,7 +1231,7 @@ void BreakCmd(out BreakCmd/*!*/ bcmd) { Contract.Ensures(Contract.ValueAtReturn(out bcmd) != null); IToken/*!*/ x; IToken/*!*/ y; string breakLabel = null; - Expect(46); + Expect(47); x = t; if (la.kind == 1) { Ident(out y); @@ -1203,13 +1244,13 @@ void BreakCmd(out BreakCmd/*!*/ bcmd) { void Guard(out Expr e) { Expr/*!*/ ee; e = null; Expect(10); - if (la.kind == 45) { + if (la.kind == 46) { Get(); e = null; } else if (StartOf(9)) { Expression(out ee); e = ee; - } else SynErr(120); + } else SynErr(122); Expect(11); } @@ -1227,7 +1268,7 @@ void LabelOrAssign(out Cmd c, out IToken label) { if (la.kind == 12) { Get(); c = null; label = x; - } else if (la.kind == 13 || la.kind == 18 || la.kind == 51) { + } else if (la.kind == 13 || la.kind == 18 || la.kind == 52) { lhss = new List(); lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val)); while (la.kind == 18) { @@ -1245,9 +1286,9 @@ void LabelOrAssign(out Cmd c, out IToken label) { } lhss.Add(lhs); } - Expect(51); + Expect(52); x = t; /* use location of := */ - while (la.kind == 28) { + while (la.kind == 25) { Attribute(ref kv); } Expression(out e0); @@ -1260,7 +1301,7 @@ void LabelOrAssign(out Cmd c, out IToken label) { } Expect(9); c = new AssignCmd(x, lhss, rhss, kv); - } else SynErr(121); + } else SynErr(123); } void CallCmd(out Cmd c) { @@ -1270,15 +1311,15 @@ void CallCmd(out Cmd c) { bool isFree = false; c = null; - if (la.kind == 52) { + if (la.kind == 53) { Get(); isAsync = true; } - if (la.kind == 36) { + if (la.kind == 37) { Get(); isFree = true; } - Expect(53); + Expect(54); x = t; CallParams(isAsync, isFree, x, out c); @@ -1290,11 +1331,11 @@ void ParCallCmd(out Cmd d) { Cmd c = null; List callCmds = new List(); - Expect(54); + Expect(55); x = t; CallParams(false, false, x, out c); callCmds.Add((CallCmd)c); - while (la.kind == 55) { + while (la.kind == 56) { Get(); CallParams(false, false, x, out c); callCmds.Add((CallCmd)c); @@ -1330,7 +1371,7 @@ void CallParams(bool isAsync, bool isFree, IToken x, out Cmd c) { IToken p; c = null; - while (la.kind == 28) { + while (la.kind == 25) { Attribute(ref kv); } Ident(out first); @@ -1347,7 +1388,7 @@ void CallParams(bool isAsync, bool isFree, IToken x, out Cmd c) { } Expect(11); c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync; - } else if (la.kind == 13 || la.kind == 51) { + } else if (la.kind == 13 || la.kind == 52) { ids.Add(new IdentifierExpr(first, first.val)); if (la.kind == 13) { Get(); @@ -1359,7 +1400,7 @@ void CallParams(bool isAsync, bool isFree, IToken x, out Cmd c) { ids.Add(new IdentifierExpr(p, p.val)); } } - Expect(51); + Expect(52); Ident(out first); Expect(10); if (StartOf(9)) { @@ -1373,7 +1414,7 @@ void CallParams(bool isAsync, bool isFree, IToken x, out Cmd c) { } Expect(11); c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync; - } else SynErr(122); + } else SynErr(124); } void Expressions(out List/*!*/ es) { @@ -1391,7 +1432,7 @@ void ImpliesExpression(bool noExplies, out Expr/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; LogicalExpression(out e0); if (StartOf(10)) { - if (la.kind == 58 || la.kind == 59) { + if (la.kind == 59 || la.kind == 60) { ImpliesOp(); x = t; ImpliesExpression(true, out e1); @@ -1403,7 +1444,7 @@ void ImpliesExpression(bool noExplies, out Expr/*!*/ e0) { x = t; LogicalExpression(out e1); e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e1, e0); - while (la.kind == 60 || la.kind == 61) { + while (la.kind == 61 || la.kind == 62) { ExpliesOp(); x = t; LogicalExpression(out e1); @@ -1414,23 +1455,23 @@ void ImpliesExpression(bool noExplies, out Expr/*!*/ e0) { } void EquivOp() { - if (la.kind == 56) { + if (la.kind == 57) { Get(); - } else if (la.kind == 57) { + } else if (la.kind == 58) { Get(); - } else SynErr(123); + } else SynErr(125); } void LogicalExpression(out Expr/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; RelationalExpression(out e0); if (StartOf(11)) { - if (la.kind == 62 || la.kind == 63) { + if (la.kind == 63 || la.kind == 64) { AndOp(); x = t; RelationalExpression(out e1); e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1); - while (la.kind == 62 || la.kind == 63) { + while (la.kind == 63 || la.kind == 64) { AndOp(); x = t; RelationalExpression(out e1); @@ -1441,7 +1482,7 @@ void LogicalExpression(out Expr/*!*/ e0) { x = t; RelationalExpression(out e1); e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1); - while (la.kind == 64 || la.kind == 65) { + while (la.kind == 65 || la.kind == 66) { OrOp(); x = t; RelationalExpression(out e1); @@ -1452,19 +1493,19 @@ void LogicalExpression(out Expr/*!*/ e0) { } void ImpliesOp() { - if (la.kind == 58) { + if (la.kind == 59) { Get(); - } else if (la.kind == 59) { + } else if (la.kind == 60) { Get(); - } else SynErr(124); + } else SynErr(126); } void ExpliesOp() { - if (la.kind == 60) { + if (la.kind == 61) { Get(); - } else if (la.kind == 61) { + } else if (la.kind == 62) { Get(); - } else SynErr(125); + } else SynErr(127); } void RelationalExpression(out Expr/*!*/ e0) { @@ -1478,25 +1519,25 @@ void RelationalExpression(out Expr/*!*/ e0) { } void AndOp() { - if (la.kind == 62) { + if (la.kind == 63) { Get(); - } else if (la.kind == 63) { + } else if (la.kind == 64) { Get(); - } else SynErr(126); + } else SynErr(128); } void OrOp() { - if (la.kind == 64) { + if (la.kind == 65) { Get(); - } else if (la.kind == 65) { + } else if (la.kind == 66) { Get(); - } else SynErr(127); + } else SynErr(129); } void BvTerm(out Expr/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; Term(out e0); - while (la.kind == 74) { + while (la.kind == 75) { Get(); x = t; Term(out e1); @@ -1507,7 +1548,7 @@ void BvTerm(out Expr/*!*/ e0) { void RelOp(out IToken/*!*/ x, out BinaryOperator.Opcode op) { Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; switch (la.kind) { - case 66: { + case 67: { Get(); x = t; op=BinaryOperator.Opcode.Eq; break; @@ -1522,49 +1563,49 @@ void RelOp(out IToken/*!*/ x, out BinaryOperator.Opcode op) { x = t; op=BinaryOperator.Opcode.Gt; break; } - case 67: { + case 68: { Get(); x = t; op=BinaryOperator.Opcode.Le; break; } - case 68: { + case 69: { Get(); x = t; op=BinaryOperator.Opcode.Ge; break; } - case 69: { + case 70: { Get(); x = t; op=BinaryOperator.Opcode.Neq; break; } - case 70: { + case 71: { Get(); x = t; op=BinaryOperator.Opcode.Subtype; break; } - case 71: { + case 72: { Get(); x = t; op=BinaryOperator.Opcode.Neq; break; } - case 72: { + case 73: { Get(); x = t; op=BinaryOperator.Opcode.Le; break; } - case 73: { + case 74: { Get(); x = t; op=BinaryOperator.Opcode.Ge; break; } - default: SynErr(128); break; + default: SynErr(130); break; } } void Term(out Expr/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; BinaryOperator.Opcode op; Factor(out e0); - while (la.kind == 75 || la.kind == 76) { + while (la.kind == 76 || la.kind == 77) { AddOp(out x, out op); Factor(out e1); e0 = Expr.Binary(x, op, e0, e1); @@ -1583,19 +1624,19 @@ void Factor(out Expr/*!*/ e0) { void AddOp(out IToken/*!*/ x, out BinaryOperator.Opcode op) { Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; - if (la.kind == 75) { + if (la.kind == 76) { Get(); x = t; op=BinaryOperator.Opcode.Add; - } else if (la.kind == 76) { + } else if (la.kind == 77) { Get(); x = t; op=BinaryOperator.Opcode.Sub; - } else SynErr(129); + } else SynErr(131); } void Power(out Expr/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; UnaryExpression(out e0); - if (la.kind == 80) { + if (la.kind == 81) { Get(); x = t; Power(out e1); @@ -1605,46 +1646,46 @@ void Power(out Expr/*!*/ e0) { void MulOp(out IToken/*!*/ x, out BinaryOperator.Opcode op) { Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; - if (la.kind == 45) { + if (la.kind == 46) { Get(); x = t; op=BinaryOperator.Opcode.Mul; - } else if (la.kind == 77) { + } else if (la.kind == 78) { Get(); x = t; op=BinaryOperator.Opcode.Div; - } else if (la.kind == 78) { + } else if (la.kind == 79) { Get(); x = t; op=BinaryOperator.Opcode.Mod; - } else if (la.kind == 79) { + } else if (la.kind == 80) { Get(); x = t; op=BinaryOperator.Opcode.RealDiv; - } else SynErr(130); + } else SynErr(132); } void UnaryExpression(out Expr/*!*/ e) { Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; e = dummyExpr; - if (la.kind == 76) { + if (la.kind == 77) { Get(); x = t; UnaryExpression(out e); e = Expr.Unary(x, UnaryOperator.Opcode.Neg, e); - } else if (la.kind == 81 || la.kind == 82) { + } else if (la.kind == 82 || la.kind == 83) { NegOp(); x = t; UnaryExpression(out e); e = Expr.Unary(x, UnaryOperator.Opcode.Not, e); } else if (StartOf(14)) { CoercionExpression(out e); - } else SynErr(131); + } else SynErr(133); } void NegOp() { - if (la.kind == 81) { + if (la.kind == 82) { Get(); - } else if (la.kind == 82) { + } else if (la.kind == 83) { Get(); - } else SynErr(132); + } else SynErr(134); } void CoercionExpression(out Expr/*!*/ e) { @@ -1668,7 +1709,7 @@ void CoercionExpression(out Expr/*!*/ e) { e = new BvBounds(x, bn, ((LiteralExpr)e).asBigNum); } - } else SynErr(133); + } else SynErr(135); } } @@ -1700,7 +1741,7 @@ void ArrayExpression(out Expr/*!*/ e) { allArgs.Add(e1); } - if (la.kind == 51) { + if (la.kind == 52) { Get(); Expression(out e1); if (bvExtract || e1 is BvBounds) @@ -1749,18 +1790,18 @@ void AtomExpression(out Expr/*!*/ e) { List/*!*/ blocks; switch (la.kind) { - case 83: { + case 84: { Get(); e = new LiteralExpr(t, false); break; } - case 84: { + case 85: { Get(); e = new LiteralExpr(t, true); break; } - case 85: case 86: { - if (la.kind == 85) { + case 86: case 87: { + if (la.kind == 86) { Get(); } else { Get(); @@ -1768,8 +1809,8 @@ void AtomExpression(out Expr/*!*/ e) { e = new LiteralExpr(t, RoundingMode.RNE); break; } - case 87: case 88: { - if (la.kind == 87) { + case 88: case 89: { + if (la.kind == 88) { Get(); } else { Get(); @@ -1777,8 +1818,8 @@ void AtomExpression(out Expr/*!*/ e) { e = new LiteralExpr(t, RoundingMode.RNA); break; } - case 89: case 90: { - if (la.kind == 89) { + case 90: case 91: { + if (la.kind == 90) { Get(); } else { Get(); @@ -1786,8 +1827,8 @@ void AtomExpression(out Expr/*!*/ e) { e = new LiteralExpr(t, RoundingMode.RTP); break; } - case 91: case 92: { - if (la.kind == 91) { + case 92: case 93: { + if (la.kind == 92) { Get(); } else { Get(); @@ -1795,8 +1836,8 @@ void AtomExpression(out Expr/*!*/ e) { e = new LiteralExpr(t, RoundingMode.RTN); break; } - case 93: case 94: { - if (la.kind == 93) { + case 94: case 95: { + if (la.kind == 94) { Get(); } else { Get(); @@ -1839,12 +1880,12 @@ void AtomExpression(out Expr/*!*/ e) { e = new NAryExpr(x, new FunctionCall(id), es); } else if (la.kind == 11) { e = new NAryExpr(x, new FunctionCall(id), new List()); - } else SynErr(134); + } else SynErr(136); Expect(11); } break; } - case 95: { + case 96: { Get(); x = t; Expect(10); @@ -1878,19 +1919,19 @@ void AtomExpression(out Expr/*!*/ e) { if (e is BvBounds) this.SemErr("parentheses around bitvector bounds " + "are not allowed"); - } else if (la.kind == 99 || la.kind == 100) { + } else if (la.kind == 100 || la.kind == 101) { Forall(); x = t; QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e); if (typeParams.Count + ds.Count > 0) e = new ForallExpr(x, typeParams, ds, kv, trig, e); - } else if (la.kind == 101 || la.kind == 102) { + } else if (la.kind == 102 || la.kind == 103) { Exists(); x = t; QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e); if (typeParams.Count + ds.Count > 0) e = new ExistsExpr(x, typeParams, ds, kv, trig, e); - } else if (la.kind == 103 || la.kind == 104) { + } else if (la.kind == 104 || la.kind == 105) { Lambda(); x = t; QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e); @@ -1900,20 +1941,20 @@ void AtomExpression(out Expr/*!*/ e) { e = new LambdaExpr(x, typeParams, ds, kv, e); } else if (la.kind == 8) { LetExpr(out e); - } else SynErr(135); + } else SynErr(137); Expect(11); break; } - case 41: { + case 42: { IfThenElseExpression(out e); break; } - case 96: { + case 97: { CodeExpression(out locals, out blocks); e = new CodeExpr(locals, blocks); break; } - default: SynErr(136); break; + default: SynErr(138); break; } } @@ -1925,7 +1966,7 @@ void Dec(out BigDec n) { } else if (la.kind == 6) { Get(); s = t.val; - } else SynErr(137); + } else SynErr(139); try { n = BigDec.FromString(s); } catch (FormatException) { @@ -1965,11 +2006,11 @@ void BvLit(out BigNum n, out int m) { } void Forall() { - if (la.kind == 99) { + if (la.kind == 100) { Get(); - } else if (la.kind == 100) { + } else if (la.kind == 101) { Get(); - } else SynErr(138); + } else SynErr(140); } void QuantifierBody(IToken/*!*/ q, out List/*!*/ typeParams, out List/*!*/ ds, @@ -1982,33 +2023,33 @@ void QuantifierBody(IToken/*!*/ q, out List/*!*/ typeParams, out L if (la.kind == 20) { TypeParams(out tok, out typeParams); - if (la.kind == 1 || la.kind == 28) { + if (la.kind == 1 || la.kind == 25) { BoundVars(out ds); } - } else if (la.kind == 1 || la.kind == 28) { + } else if (la.kind == 1 || la.kind == 25) { BoundVars(out ds); - } else SynErr(139); + } else SynErr(141); QSep(); - while (la.kind == 28) { + while (la.kind == 25) { AttributeOrTrigger(ref kv, ref trig); } Expression(out body); } void Exists() { - if (la.kind == 101) { + if (la.kind == 102) { Get(); - } else if (la.kind == 102) { + } else if (la.kind == 103) { Get(); - } else SynErr(140); + } else SynErr(142); } void Lambda() { - if (la.kind == 103) { + if (la.kind == 104) { Get(); - } else if (la.kind == 104) { + } else if (la.kind == 105) { Get(); - } else SynErr(141); + } else SynErr(143); } void LetExpr(out Expr/*!*/ letexpr) { @@ -2029,7 +2070,7 @@ void LetExpr(out Expr/*!*/ letexpr) { LetVar(out v); ds.Add(v); } - Expect(51); + Expect(52); Expression(out e0); rhss.Add(e0); while (la.kind == 13) { @@ -2038,7 +2079,7 @@ void LetExpr(out Expr/*!*/ letexpr) { rhss.Add(e0); } Expect(9); - while (la.kind == 28) { + while (la.kind == 25) { Attribute(ref kv); } Expression(out body); @@ -2050,12 +2091,12 @@ void IfThenElseExpression(out Expr/*!*/ e) { IToken/*!*/ tok; Expr/*!*/ e0, e1, e2; e = dummyExpr; - Expect(41); + Expect(42); tok = t; Expression(out e0); - Expect(98); + Expect(99); Expression(out e1); - Expect(42); + Expect(43); Expression(out e2); e = new NAryExpr(tok, new IfThenElse(tok), new List{ e0, e1, e2 }); } @@ -2064,7 +2105,7 @@ void CodeExpression(out List/*!*/ locals, out List/*!*/ bl Contract.Ensures(Contract.ValueAtReturn(out locals) != null); Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out blocks))); locals = new List(); Block/*!*/ b; blocks = new List(); - Expect(96); + Expect(97); while (la.kind == 8) { LocalVars(locals); } @@ -2074,7 +2115,7 @@ void CodeExpression(out List/*!*/ locals, out List/*!*/ bl SpecBlock(out b); blocks.Add(b); } - Expect(97); + Expect(98); } void SpecBlock(out Block/*!*/ b) { @@ -2098,7 +2139,7 @@ void SpecBlock(out Block/*!*/ b) { } } - if (la.kind == 39) { + if (la.kind == 40) { Get(); y = t; Idents(out xs); @@ -2107,11 +2148,11 @@ void SpecBlock(out Block/*!*/ b) { ss.Add(s.val); } b = new Block(x,x.val,cs,new GotoCmd(y,ss)); - } else if (la.kind == 40) { + } else if (la.kind == 41) { Get(); Expression(out e); b = new Block(x,x.val,cs,new ReturnExprCmd(t,e)); - } else SynErr(142); + } else SynErr(144); Expect(9); } @@ -2120,7 +2161,7 @@ void AttributeOrTrigger(ref QKeyValue kv, ref Trigger trig) { string key; List parameters; object/*!*/ param; - Expect(28); + Expect(25); tok = t; if (la.kind == 12) { Get(); @@ -2168,8 +2209,8 @@ void AttributeOrTrigger(ref QKeyValue kv, ref Trigger trig) { trig.AddLast(new Trigger(tok, true, es, null)); } - } else SynErr(143); - Expect(29); + } else SynErr(145); + Expect(26); } void AttributeParameter(out object/*!*/ o) { @@ -2183,22 +2224,22 @@ void AttributeParameter(out object/*!*/ o) { } else if (StartOf(9)) { Expression(out e); o = e; - } else SynErr(144); + } else SynErr(146); } void QSep() { - if (la.kind == 105) { + if (la.kind == 106) { Get(); - } else if (la.kind == 106) { + } else if (la.kind == 107) { Get(); - } else SynErr(145); + } else SynErr(147); } void LetVar(out Variable/*!*/ v) { QKeyValue kv = null; IToken id; - while (la.kind == 28) { + while (la.kind == 25) { Attribute(ref kv); } Ident(out id); @@ -2220,22 +2261,22 @@ public void Parse() { } static readonly bool[,]/*!*/ set = { - {_T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x}, - {_x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_T,_x, _x,_x,_T,_T, _x,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x}, - {_x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_T, _T,_T,_T,_x, _T,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x}, - {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x}, - {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x}, - {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x}, - {_x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_T, _T,_T,_T,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x}, - {_x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_T, _T,_T,_x,_T, _x,_x,_T,_T, _T,_T,_T,_x, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x}, - {_x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_x, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x}, - {_x,_T,_T,_T, _T,_T,_T,_T, _x,_x,_T,_x, _x,_x,_x,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x}, - {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x}, - {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x}, - {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x}, - {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x}, - {_x,_T,_T,_T, _T,_T,_T,_T, _x,_x,_T,_x, _x,_x,_x,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x}, - {_x,_T,_T,_T, _T,_T,_T,_T, _x,_x,_T,_x, _x,_x,_x,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x} + {_T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x}, + {_x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_T,_x,_T, _T,_x,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x}, + {_x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_T, _T,_T,_T,_x, _T,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x}, + {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x}, + {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x}, + {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x}, + {_x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_T, _T,_T,_T,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x}, + {_x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _T,_T,_T,_x, _T,_x,_x,_T, _T,_T,_T,_T, _x,_T,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x}, + {_x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_T,_T, _x,_T,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x}, + {_x,_T,_T,_T, _T,_T,_T,_T, _x,_x,_T,_x, _x,_x,_x,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x}, + {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x}, + {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x}, + {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x}, + {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x}, + {_x,_T,_T,_T, _T,_T,_T,_T, _x,_x,_T,_x, _x,_x,_x,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x}, + {_x,_T,_T,_T, _T,_T,_T,_T, _x,_x,_T,_x, _x,_x,_x,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x} }; } // end Parser @@ -2284,128 +2325,130 @@ string GetSyntaxErrorString(int n) { case 21: s = "\">\" expected"; break; case 22: s = "\"const\" expected"; break; case 23: s = "\"unique\" expected"; break; - case 24: s = "\"extends\" expected"; break; - case 25: s = "\"complete\" expected"; break; - case 26: s = "\"function\" expected"; break; - case 27: s = "\"returns\" expected"; break; - case 28: s = "\"{\" expected"; break; - case 29: s = "\"}\" expected"; break; - case 30: s = "\"axiom\" expected"; break; - case 31: s = "\"type\" expected"; break; - case 32: s = "\"=\" expected"; break; - case 33: s = "\"procedure\" expected"; break; - case 34: s = "\"implementation\" expected"; break; - case 35: s = "\"modifies\" expected"; break; - case 36: s = "\"free\" expected"; break; - case 37: s = "\"requires\" expected"; break; - case 38: s = "\"ensures\" expected"; break; - case 39: s = "\"goto\" expected"; break; - case 40: s = "\"return\" expected"; break; - case 41: s = "\"if\" expected"; break; - case 42: s = "\"else\" expected"; break; - case 43: s = "\"while\" expected"; break; - case 44: s = "\"invariant\" expected"; break; - case 45: s = "\"*\" expected"; break; - case 46: s = "\"break\" expected"; break; - case 47: s = "\"assert\" expected"; break; - case 48: s = "\"assume\" expected"; break; - case 49: s = "\"havoc\" expected"; break; - case 50: s = "\"yield\" expected"; break; - case 51: s = "\":=\" expected"; break; - case 52: s = "\"async\" expected"; break; - case 53: s = "\"call\" expected"; break; - case 54: s = "\"par\" expected"; break; - case 55: s = "\"|\" expected"; break; - case 56: s = "\"<==>\" expected"; break; - case 57: s = "\"\\u21d4\" expected"; break; - case 58: s = "\"==>\" expected"; break; - case 59: s = "\"\\u21d2\" expected"; break; - case 60: s = "\"<==\" expected"; break; - case 61: s = "\"\\u21d0\" expected"; break; - case 62: s = "\"&&\" expected"; break; - case 63: s = "\"\\u2227\" expected"; break; - case 64: s = "\"||\" expected"; break; - case 65: s = "\"\\u2228\" expected"; break; - case 66: s = "\"==\" expected"; break; - case 67: s = "\"<=\" expected"; break; - case 68: s = "\">=\" expected"; break; - case 69: s = "\"!=\" expected"; break; - case 70: s = "\"<:\" expected"; break; - case 71: s = "\"\\u2260\" expected"; break; - case 72: s = "\"\\u2264\" expected"; break; - case 73: s = "\"\\u2265\" expected"; break; - case 74: s = "\"++\" expected"; break; - case 75: s = "\"+\" expected"; break; - case 76: s = "\"-\" expected"; break; - case 77: s = "\"div\" expected"; break; - case 78: s = "\"mod\" expected"; break; - case 79: s = "\"/\" expected"; break; - case 80: s = "\"**\" expected"; break; - case 81: s = "\"!\" expected"; break; - case 82: s = "\"\\u00ac\" expected"; break; - case 83: s = "\"false\" expected"; break; - case 84: s = "\"true\" expected"; break; - case 85: s = "\"roundNearestTiesToEven\" expected"; break; - case 86: s = "\"RNE\" expected"; break; - case 87: s = "\"roundNearestTiesToAway\" expected"; break; - case 88: s = "\"RNA\" expected"; break; - case 89: s = "\"roundTowardPositive\" expected"; break; - case 90: s = "\"RTP\" expected"; break; - case 91: s = "\"roundTowardNegative\" expected"; break; - case 92: s = "\"RTN\" expected"; break; - case 93: s = "\"roundTowardZero\" expected"; break; - case 94: s = "\"RTZ\" expected"; break; - case 95: s = "\"old\" expected"; break; - case 96: s = "\"|{\" expected"; break; - case 97: s = "\"}|\" expected"; break; - case 98: s = "\"then\" expected"; break; - case 99: s = "\"forall\" expected"; break; - case 100: s = "\"\\u2200\" expected"; break; - case 101: s = "\"exists\" expected"; break; - case 102: s = "\"\\u2203\" expected"; break; - case 103: s = "\"lambda\" expected"; break; - case 104: s = "\"\\u03bb\" expected"; break; - case 105: s = "\"::\" expected"; break; - case 106: s = "\"\\u2022\" expected"; break; - case 107: s = "??? expected"; break; - case 108: s = "invalid Function"; break; - case 109: s = "invalid Function"; break; - case 110: s = "invalid Procedure"; break; - case 111: s = "invalid Type"; break; - case 112: s = "invalid TypeAtom"; break; - case 113: s = "invalid TypeArgs"; break; - case 114: s = "invalid Spec"; break; - case 115: s = "invalid SpecPrePost"; break; - case 116: s = "invalid LabelOrCmd"; break; - case 117: s = "invalid StructuredCmd"; break; - case 118: s = "invalid TransferCmd"; break; - case 119: s = "invalid IfCmd"; break; - case 120: s = "invalid Guard"; break; - case 121: s = "invalid LabelOrAssign"; break; - case 122: s = "invalid CallParams"; break; - case 123: s = "invalid EquivOp"; break; - case 124: s = "invalid ImpliesOp"; break; - case 125: s = "invalid ExpliesOp"; break; - case 126: s = "invalid AndOp"; break; - case 127: s = "invalid OrOp"; break; - case 128: s = "invalid RelOp"; break; - case 129: s = "invalid AddOp"; break; - case 130: s = "invalid MulOp"; break; - case 131: s = "invalid UnaryExpression"; break; - case 132: s = "invalid NegOp"; break; - case 133: s = "invalid CoercionExpression"; break; - case 134: s = "invalid AtomExpression"; break; - case 135: s = "invalid AtomExpression"; break; + case 24: s = "\"uses\" expected"; break; + case 25: s = "\"{\" expected"; break; + case 26: s = "\"}\" expected"; break; + case 27: s = "\"extends\" expected"; break; + case 28: s = "\"complete\" expected"; break; + case 29: s = "\"function\" expected"; break; + case 30: s = "\"returns\" expected"; break; + case 31: s = "\"axiom\" expected"; break; + case 32: s = "\"type\" expected"; break; + case 33: s = "\"=\" expected"; break; + case 34: s = "\"procedure\" expected"; break; + case 35: s = "\"implementation\" expected"; break; + case 36: s = "\"modifies\" expected"; break; + case 37: s = "\"free\" expected"; break; + case 38: s = "\"requires\" expected"; break; + case 39: s = "\"ensures\" expected"; break; + case 40: s = "\"goto\" expected"; break; + case 41: s = "\"return\" expected"; break; + case 42: s = "\"if\" expected"; break; + case 43: s = "\"else\" expected"; break; + case 44: s = "\"while\" expected"; break; + case 45: s = "\"invariant\" expected"; break; + case 46: s = "\"*\" expected"; break; + case 47: s = "\"break\" expected"; break; + case 48: s = "\"assert\" expected"; break; + case 49: s = "\"assume\" expected"; break; + case 50: s = "\"havoc\" expected"; break; + case 51: s = "\"yield\" expected"; break; + case 52: s = "\":=\" expected"; break; + case 53: s = "\"async\" expected"; break; + case 54: s = "\"call\" expected"; break; + case 55: s = "\"par\" expected"; break; + case 56: s = "\"|\" expected"; break; + case 57: s = "\"<==>\" expected"; break; + case 58: s = "\"\\u21d4\" expected"; break; + case 59: s = "\"==>\" expected"; break; + case 60: s = "\"\\u21d2\" expected"; break; + case 61: s = "\"<==\" expected"; break; + case 62: s = "\"\\u21d0\" expected"; break; + case 63: s = "\"&&\" expected"; break; + case 64: s = "\"\\u2227\" expected"; break; + case 65: s = "\"||\" expected"; break; + case 66: s = "\"\\u2228\" expected"; break; + case 67: s = "\"==\" expected"; break; + case 68: s = "\"<=\" expected"; break; + case 69: s = "\">=\" expected"; break; + case 70: s = "\"!=\" expected"; break; + case 71: s = "\"<:\" expected"; break; + case 72: s = "\"\\u2260\" expected"; break; + case 73: s = "\"\\u2264\" expected"; break; + case 74: s = "\"\\u2265\" expected"; break; + case 75: s = "\"++\" expected"; break; + case 76: s = "\"+\" expected"; break; + case 77: s = "\"-\" expected"; break; + case 78: s = "\"div\" expected"; break; + case 79: s = "\"mod\" expected"; break; + case 80: s = "\"/\" expected"; break; + case 81: s = "\"**\" expected"; break; + case 82: s = "\"!\" expected"; break; + case 83: s = "\"\\u00ac\" expected"; break; + case 84: s = "\"false\" expected"; break; + case 85: s = "\"true\" expected"; break; + case 86: s = "\"roundNearestTiesToEven\" expected"; break; + case 87: s = "\"RNE\" expected"; break; + case 88: s = "\"roundNearestTiesToAway\" expected"; break; + case 89: s = "\"RNA\" expected"; break; + case 90: s = "\"roundTowardPositive\" expected"; break; + case 91: s = "\"RTP\" expected"; break; + case 92: s = "\"roundTowardNegative\" expected"; break; + case 93: s = "\"RTN\" expected"; break; + case 94: s = "\"roundTowardZero\" expected"; break; + case 95: s = "\"RTZ\" expected"; break; + case 96: s = "\"old\" expected"; break; + case 97: s = "\"|{\" expected"; break; + case 98: s = "\"}|\" expected"; break; + case 99: s = "\"then\" expected"; break; + case 100: s = "\"forall\" expected"; break; + case 101: s = "\"\\u2200\" expected"; break; + case 102: s = "\"exists\" expected"; break; + case 103: s = "\"\\u2203\" expected"; break; + case 104: s = "\"lambda\" expected"; break; + case 105: s = "\"\\u03bb\" expected"; break; + case 106: s = "\"::\" expected"; break; + case 107: s = "\"\\u2022\" expected"; break; + case 108: s = "??? expected"; break; + case 109: s = "invalid Consts"; break; + case 110: s = "invalid Function"; break; + case 111: s = "invalid Function"; break; + case 112: s = "invalid Procedure"; break; + case 113: s = "invalid Type"; break; + case 114: s = "invalid TypeAtom"; break; + case 115: s = "invalid TypeArgs"; break; + case 116: s = "invalid Spec"; break; + case 117: s = "invalid SpecPrePost"; break; + case 118: s = "invalid LabelOrCmd"; break; + case 119: s = "invalid StructuredCmd"; break; + case 120: s = "invalid TransferCmd"; break; + case 121: s = "invalid IfCmd"; break; + case 122: s = "invalid Guard"; break; + case 123: s = "invalid LabelOrAssign"; break; + case 124: s = "invalid CallParams"; break; + case 125: s = "invalid EquivOp"; break; + case 126: s = "invalid ImpliesOp"; break; + case 127: s = "invalid ExpliesOp"; break; + case 128: s = "invalid AndOp"; break; + case 129: s = "invalid OrOp"; break; + case 130: s = "invalid RelOp"; break; + case 131: s = "invalid AddOp"; break; + case 132: s = "invalid MulOp"; break; + case 133: s = "invalid UnaryExpression"; break; + case 134: s = "invalid NegOp"; break; + case 135: s = "invalid CoercionExpression"; break; case 136: s = "invalid AtomExpression"; break; - case 137: s = "invalid Dec"; break; - case 138: s = "invalid Forall"; break; - case 139: s = "invalid QuantifierBody"; break; - case 140: s = "invalid Exists"; break; - case 141: s = "invalid Lambda"; break; - case 142: s = "invalid SpecBlock"; break; - case 143: s = "invalid AttributeOrTrigger"; break; - case 144: s = "invalid AttributeParameter"; break; - case 145: s = "invalid QSep"; break; + case 137: s = "invalid AtomExpression"; break; + case 138: s = "invalid AtomExpression"; break; + case 139: s = "invalid Dec"; break; + case 140: s = "invalid Forall"; break; + case 141: s = "invalid QuantifierBody"; break; + case 142: s = "invalid Exists"; break; + case 143: s = "invalid Lambda"; break; + case 144: s = "invalid SpecBlock"; break; + case 145: s = "invalid AttributeOrTrigger"; break; + case 146: s = "invalid AttributeParameter"; break; + case 147: s = "invalid QSep"; break; default: s = "error " + n; break; } diff --git a/Source/Core/Prune/Prune.cs b/Source/Core/Prune/Prune.cs index ef0ac507a..122296e6b 100644 --- a/Source/Core/Prune/Prune.cs +++ b/Source/Core/Prune/Prune.cs @@ -118,7 +118,8 @@ public static IEnumerable GetLiveDeclarations(Program program, List // an implementation only has outgoing edges. var reachableDeclarations = GraphAlgorithms.FindReachableNodesInGraphWithMergeNodes(program.DeclarationDependencies, blocksNode.outgoing).ToHashSet(); - var result = program.TopLevelDeclarations.Where(d => d is not Constant && d is not Axiom && d is not Function || reachableDeclarations.Contains(d)); + var result = program.TopLevelDeclarations.Where(d => d is not Constant && d is not Axiom && d is not Function || reachableDeclarations.Contains(d)).ToList(); + var removedDeclarations = program.TopLevelDeclarations.Except(result).ToList(); return result; } } diff --git a/Source/Core/Scanner.cs b/Source/Core/Scanner.cs index 67946a82e..14f2374c0 100644 --- a/Source/Core/Scanner.cs +++ b/Source/Core/Scanner.cs @@ -220,8 +220,8 @@ public override int Read() { public class Scanner { const char EOL = '\n'; const int eofSym = 0; /* pdt */ - const int maxT = 107; - const int noSym = 107; + const int maxT = 108; + const int noSym = 108; [ContractInvariantMethod] @@ -520,51 +520,52 @@ void CheckLiteral() { case "bool": t.kind = 17; break; case "const": t.kind = 22; break; case "unique": t.kind = 23; break; - case "extends": t.kind = 24; break; - case "complete": t.kind = 25; break; - case "function": t.kind = 26; break; - case "returns": t.kind = 27; break; - case "axiom": t.kind = 30; break; - case "type": t.kind = 31; break; - case "procedure": t.kind = 33; break; - case "implementation": t.kind = 34; break; - case "modifies": t.kind = 35; break; - case "free": t.kind = 36; break; - case "requires": t.kind = 37; break; - case "ensures": t.kind = 38; break; - case "goto": t.kind = 39; break; - case "return": t.kind = 40; break; - case "if": t.kind = 41; break; - case "else": t.kind = 42; break; - case "while": t.kind = 43; break; - case "invariant": t.kind = 44; break; - case "break": t.kind = 46; break; - case "assert": t.kind = 47; break; - case "assume": t.kind = 48; break; - case "havoc": t.kind = 49; break; - case "yield": t.kind = 50; break; - case "async": t.kind = 52; break; - case "call": t.kind = 53; break; - case "par": t.kind = 54; break; - case "div": t.kind = 77; break; - case "mod": t.kind = 78; break; - case "false": t.kind = 83; break; - case "true": t.kind = 84; break; - case "roundNearestTiesToEven": t.kind = 85; break; - case "RNE": t.kind = 86; break; - case "roundNearestTiesToAway": t.kind = 87; break; - case "RNA": t.kind = 88; break; - case "roundTowardPositive": t.kind = 89; break; - case "RTP": t.kind = 90; break; - case "roundTowardNegative": t.kind = 91; break; - case "RTN": t.kind = 92; break; - case "roundTowardZero": t.kind = 93; break; - case "RTZ": t.kind = 94; break; - case "old": t.kind = 95; break; - case "then": t.kind = 98; break; - case "forall": t.kind = 99; break; - case "exists": t.kind = 101; break; - case "lambda": t.kind = 103; break; + case "uses": t.kind = 24; break; + case "extends": t.kind = 27; break; + case "complete": t.kind = 28; break; + case "function": t.kind = 29; break; + case "returns": t.kind = 30; break; + case "axiom": t.kind = 31; break; + case "type": t.kind = 32; break; + case "procedure": t.kind = 34; break; + case "implementation": t.kind = 35; break; + case "modifies": t.kind = 36; break; + case "free": t.kind = 37; break; + case "requires": t.kind = 38; break; + case "ensures": t.kind = 39; break; + case "goto": t.kind = 40; break; + case "return": t.kind = 41; break; + case "if": t.kind = 42; break; + case "else": t.kind = 43; break; + case "while": t.kind = 44; break; + case "invariant": t.kind = 45; break; + case "break": t.kind = 47; break; + case "assert": t.kind = 48; break; + case "assume": t.kind = 49; break; + case "havoc": t.kind = 50; break; + case "yield": t.kind = 51; break; + case "async": t.kind = 53; break; + case "call": t.kind = 54; break; + case "par": t.kind = 55; break; + case "div": t.kind = 78; break; + case "mod": t.kind = 79; break; + case "false": t.kind = 84; break; + case "true": t.kind = 85; break; + case "roundNearestTiesToEven": t.kind = 86; break; + case "RNE": t.kind = 87; break; + case "roundNearestTiesToAway": t.kind = 88; break; + case "RNA": t.kind = 89; break; + case "roundTowardPositive": t.kind = 90; break; + case "RTP": t.kind = 91; break; + case "roundTowardNegative": t.kind = 92; break; + case "RTN": t.kind = 93; break; + case "roundTowardZero": t.kind = 94; break; + case "RTZ": t.kind = 95; break; + case "old": t.kind = 96; break; + case "then": t.kind = 99; break; + case "forall": t.kind = 100; break; + case "exists": t.kind = 102; break; + case "lambda": t.kind = 104; break; default: break; } } @@ -846,68 +847,68 @@ void CheckLiteral() { case 66: {t.kind = 19; break;} case 67: - {t.kind = 28; break;} + {t.kind = 25; break;} case 68: - {t.kind = 51; break;} + {t.kind = 52; break;} case 69: - {t.kind = 56; break;} - case 70: {t.kind = 57; break;} - case 71: + case 70: {t.kind = 58; break;} - case 72: + case 71: {t.kind = 59; break;} + case 72: + {t.kind = 60; break;} case 73: - {t.kind = 61; break;} + {t.kind = 62; break;} case 74: if (ch == '&') {AddCh(); goto case 75;} else {goto case 0;} case 75: - {t.kind = 62; break;} - case 76: {t.kind = 63; break;} - case 77: + case 76: {t.kind = 64; break;} - case 78: + case 77: {t.kind = 65; break;} + case 78: + {t.kind = 66; break;} case 79: - {t.kind = 68; break;} - case 80: {t.kind = 69; break;} - case 81: + case 80: {t.kind = 70; break;} - case 82: + case 81: {t.kind = 71; break;} - case 83: + case 82: {t.kind = 72; break;} - case 84: + case 83: {t.kind = 73; break;} - case 85: + case 84: {t.kind = 74; break;} + case 85: + {t.kind = 75; break;} case 86: - {t.kind = 79; break;} - case 87: {t.kind = 80; break;} + case 87: + {t.kind = 81; break;} case 88: - {t.kind = 82; break;} + {t.kind = 83; break;} case 89: - {t.kind = 96; break;} - case 90: {t.kind = 97; break;} + case 90: + {t.kind = 98; break;} case 91: - {t.kind = 100; break;} + {t.kind = 101; break;} case 92: - {t.kind = 102; break;} + {t.kind = 103; break;} case 93: - {t.kind = 104; break;} - case 94: {t.kind = 105; break;} - case 95: + case 94: {t.kind = 106; break;} + case 95: + {t.kind = 107; break;} case 96: - recEnd = pos; recKind = 76; + recEnd = pos; recKind = 77; if (ch == '0') {AddCh(); goto case 16;} - else {t.kind = 76; break;} + else {t.kind = 77; break;} case 97: recEnd = pos; recKind = 12; if (ch == '=') {AddCh(); goto case 68;} @@ -923,42 +924,42 @@ void CheckLiteral() { if (ch == '=') {AddCh(); goto case 79;} else {t.kind = 21; break;} case 100: - recEnd = pos; recKind = 29; + recEnd = pos; recKind = 26; if (ch == '|') {AddCh(); goto case 90;} - else {t.kind = 29; break;} + else {t.kind = 26; break;} case 101: - recEnd = pos; recKind = 32; + recEnd = pos; recKind = 33; if (ch == '=') {AddCh(); goto case 107;} - else {t.kind = 32; break;} + else {t.kind = 33; break;} case 102: - recEnd = pos; recKind = 45; + recEnd = pos; recKind = 46; if (ch == '*') {AddCh(); goto case 87;} - else {t.kind = 45; break;} + else {t.kind = 46; break;} case 103: - recEnd = pos; recKind = 55; + recEnd = pos; recKind = 56; if (ch == '|') {AddCh(); goto case 77;} else if (ch == '{') {AddCh(); goto case 89;} - else {t.kind = 55; break;} + else {t.kind = 56; break;} case 104: - recEnd = pos; recKind = 81; + recEnd = pos; recKind = 82; if (ch == '=') {AddCh(); goto case 80;} - else {t.kind = 81; break;} + else {t.kind = 82; break;} case 105: - recEnd = pos; recKind = 75; + recEnd = pos; recKind = 76; if (ch == '+') {AddCh(); goto case 85;} - else {t.kind = 75; break;} + else {t.kind = 76; break;} case 106: - recEnd = pos; recKind = 67; + recEnd = pos; recKind = 68; if (ch == '=') {AddCh(); goto case 108;} - else {t.kind = 67; break;} + else {t.kind = 68; break;} case 107: - recEnd = pos; recKind = 66; + recEnd = pos; recKind = 67; if (ch == '>') {AddCh(); goto case 71;} - else {t.kind = 66; break;} + else {t.kind = 67; break;} case 108: - recEnd = pos; recKind = 60; + recEnd = pos; recKind = 61; if (ch == '>') {AddCh(); goto case 69;} - else {t.kind = 60; break;} + else {t.kind = 61; break;} } t.val = new String(tval, 0, tlen); diff --git a/Source/Graph/Graph.cs b/Source/Graph/Graph.cs index ba7bafd1a..1bd34b5d5 100644 --- a/Source/Graph/Graph.cs +++ b/Source/Graph/Graph.cs @@ -1166,7 +1166,6 @@ public ICollection Reachable() public static class GraphAlgorithms { - /** * A merge node is a node that has multiple incoming edges, and which cannot be traversed unless all incoming edges have been traversed. * A merge node is represented by an object of type IReadOnlySet{object} @@ -1192,6 +1191,9 @@ public static IEnumerable FindReachableNodesInGraphWithMergeNodes(Dictio var outgoing = edges.GetValueOrDefault(node) ?? new List(); foreach (var x in outgoing) { + if (x.ToString().Contains("Agnes2")) { + Console.Write(""); + } todo.Push(x); } } diff --git a/Test/pruning/basic.bpl b/Test/pruning/basic.bpl new file mode 100644 index 000000000..4c789b182 --- /dev/null +++ b/Test/pruning/basic.bpl @@ -0,0 +1,19 @@ +// RUN: %parallel-boogie "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +type Ty; +const unique TBool : Ty; + +type TyTag; +function Tag(Ty) : TyTag; + +const unique TagBool : TyTag uses { + axiom Tag(TBool) == TagBool; +} + +type Box; +function $Box(T): Box; + +function {:identity} Lit(x: T): T { x } uses { + axiom (forall x: T :: { $Box(Lit(x)) } $Box(Lit(x)) == Lit($Box(x)) ); +} \ No newline at end of file diff --git a/Test/pruning/basic.bpl.expect b/Test/pruning/basic.bpl.expect new file mode 100644 index 000000000..cc5cde4d7 --- /dev/null +++ b/Test/pruning/basic.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 0 verified, 0 errors From 9ec71942b73fba078192c79e3c507168c3b9e3f1 Mon Sep 17 00:00:00 2001 From: Remy Willems <> Date: Tue, 2 Nov 2021 15:22:05 +0100 Subject: [PATCH 06/23] Track outgoing edges from explicit uses clauses --- Source/Core/Absy.cs | 13 ++++++------- Source/Core/BoogiePL.atg | 2 +- Source/Core/Prune/AxiomVisitor.cs | 2 +- Source/Core/Prune/DependencyEvaluator.cs | 17 +++++++++++++++++ Source/Core/Prune/FunctionVisitor.cs | 5 ++++- Source/Core/Prune/Prune.cs | 7 ++++--- 6 files changed, 33 insertions(+), 13 deletions(-) diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index f695dc15e..1e018a7a0 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -2477,7 +2477,7 @@ public class Constant : Variable // that the parental situation is unconstrained. public readonly ReadOnlyCollection Parents; - public IList NewDefinitionAxioms; + public readonly IReadOnlyList DefinitionAxioms { get; } [ContractInvariantMethod] void ObjectInvariant() @@ -2516,7 +2516,8 @@ public Constant(IToken /*!*/ tok, TypedIdent /*!*/ typedIdent, bool unique) public Constant(IToken /*!*/ tok, TypedIdent /*!*/ typedIdent, bool unique, IEnumerable parents, bool childrenComplete, - QKeyValue kv) + QKeyValue kv, + IReadOnlyList definitionAxioms) : base(tok, typedIdent, kv) { Contract.Requires(tok != null); @@ -2527,12 +2528,10 @@ public Constant(IToken /*!*/ tok, TypedIdent /*!*/ typedIdent, this.Unique = unique; this.Parents = parents == null ? null : new ReadOnlyCollection(parents.ToList()); this.ChildrenComplete = childrenComplete; + this.DefinitionAxioms = definitionAxioms; } - public override bool IsMutable - { - get { return false; } - } + public override bool IsMutable => false; public override void Emit(TokenTextWriter stream, int level) { @@ -3308,8 +3307,8 @@ public class Function : DeclWithFormals public NAryExpr DefinitionBody; // Only set if the function is declared with {:define} public Axiom DefinitionAxiom; - public IList NewDefinitionAxioms; public IList otherDefinitionAxioms; + public IEnumerable DefinitionAxioms => new []{ DefinitionAxiom}.Concat(otherDefinitionAxioms); public IEnumerable OtherDefinitionAxioms => otherDefinitionAxioms; diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index abc21e382..238faaf6d 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -502,9 +502,9 @@ Function<.out List/*!*/ ds.> } Function/*!*/ func = new Function(z, z.val, typeParams, arguments, new Formal(retTyd.tok, retTyd, false, argKv), null, kv); - func.NewDefinitionAxioms = axioms; foreach(var axiom in axioms) { ds.Add(axiom); + func.AddOtherDefinitionAxiom(axiom); } Contract.Assert(func != null); diff --git a/Source/Core/Prune/AxiomVisitor.cs b/Source/Core/Prune/AxiomVisitor.cs index b4f33b673..be0687a72 100644 --- a/Source/Core/Prune/AxiomVisitor.cs +++ b/Source/Core/Prune/AxiomVisitor.cs @@ -8,7 +8,7 @@ internal class AxiomVisitor : DependencyEvaluator { public AxiomVisitor (Axiom a) : base(a) {} - public static DependencyEvaluator GetAxiomDependencies(Axiom axiom) + public static DependencyEvaluator GetDependencies(Axiom axiom) { var result = new AxiomVisitor(axiom); result.Visit(axiom); diff --git a/Source/Core/Prune/DependencyEvaluator.cs b/Source/Core/Prune/DependencyEvaluator.cs index 64b3f3a89..f59a11173 100644 --- a/Source/Core/Prune/DependencyEvaluator.cs +++ b/Source/Core/Prune/DependencyEvaluator.cs @@ -54,4 +54,21 @@ protected DependencyEvaluator(Declaration declaration) this.declaration = declaration; } } + + class ConstantVisitor : DependencyEvaluator + { + protected ConstantVisitor(Declaration declaration) : base(declaration) + { + } + + public static DependencyEvaluator GetDependencies(Constant constant) + { + var result = new ConstantVisitor(constant); + foreach (var definitionAxiom in constant.DefinitionAxioms) { + result.AddOutgoing(definitionAxiom); + } + result.Visit(constant); + return result; + } + } } \ No newline at end of file diff --git a/Source/Core/Prune/FunctionVisitor.cs b/Source/Core/Prune/FunctionVisitor.cs index 70b6daed0..5ed808fe3 100644 --- a/Source/Core/Prune/FunctionVisitor.cs +++ b/Source/Core/Prune/FunctionVisitor.cs @@ -6,9 +6,12 @@ public FunctionVisitor(Function func) : base(func) { } - public static DependencyEvaluator GetFunctionDependencies(Function function) + public static DependencyEvaluator GetDependencies(Function function) { var result = new FunctionVisitor(function); + foreach (var definitionAxiom in function.DefinitionAxioms) { + result.AddOutgoing(definitionAxiom); + } result.Visit(function); return result; } diff --git a/Source/Core/Prune/Prune.cs b/Source/Core/Prune/Prune.cs index 122296e6b..c686582cd 100644 --- a/Source/Core/Prune/Prune.cs +++ b/Source/Core/Prune/Prune.cs @@ -17,9 +17,10 @@ public static Dictionary> ComputeDeclarationDependencies(Pr { return null; } - var axiomNodes = program.Axioms.Select(AxiomVisitor.GetAxiomDependencies); - var functionNodes = program.Functions.Select(FunctionVisitor.GetFunctionDependencies); - var nodes = axiomNodes.Concat(functionNodes).ToList(); + var axiomNodes = program.Axioms.Select(AxiomVisitor.GetDependencies); + var functionNodes = program.Functions.Select(FunctionVisitor.GetDependencies); + var constantNodes = program.Constants.Select(ConstantVisitor.GetDependencies); + var nodes = axiomNodes.Concat(functionNodes).Concat(constantNodes).ToList(); var edges = new Dictionary>(); foreach (var node in nodes) { From 5c811823fb274269586b8b4f50415feedaf108e3 Mon Sep 17 00:00:00 2001 From: Remy Willems <> Date: Tue, 2 Nov 2021 17:26:21 +0100 Subject: [PATCH 07/23] Add testcase and fix some bugs --- Source/Core/Absy.cs | 12 +++------ Source/Core/BoogiePL.atg | 11 ++++---- Source/Core/CommandLineOptions.cs | 17 +++++++++--- Source/Core/Parser.cs | 27 +++++++++---------- Source/Core/Prune/DependencyEvaluator.cs | 6 +++-- Source/Core/Prune/Prune.cs | 9 ++----- .../ExecutionEngineTests/ProofIsolation.cs | 2 +- Source/VCGeneration/CheckerPool.cs | 2 +- Test/pruning/basic.bpl | 14 ++++++---- Test/pruning/basic.bpl.expect | 2 +- 10 files changed, 53 insertions(+), 49 deletions(-) diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 1e018a7a0..84ca7a82d 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -2477,7 +2477,7 @@ public class Constant : Variable // that the parental situation is unconstrained. public readonly ReadOnlyCollection Parents; - public readonly IReadOnlyList DefinitionAxioms { get; } + public IReadOnlyList DefinitionAxioms { get; } [ContractInvariantMethod] void ObjectInvariant() @@ -3307,8 +3307,9 @@ public class Function : DeclWithFormals public NAryExpr DefinitionBody; // Only set if the function is declared with {:define} public Axiom DefinitionAxiom; - public IList otherDefinitionAxioms; - public IEnumerable DefinitionAxioms => new []{ DefinitionAxiom}.Concat(otherDefinitionAxioms); + public IList otherDefinitionAxioms = new List(); + public IEnumerable DefinitionAxioms => + (DefinitionAxiom == null ? Enumerable.Empty() : new[]{ DefinitionAxiom }).Concat(otherDefinitionAxioms); public IEnumerable OtherDefinitionAxioms => otherDefinitionAxioms; @@ -3316,11 +3317,6 @@ public void AddOtherDefinitionAxiom(Axiom axiom) { Contract.Requires(axiom != null); - if (otherDefinitionAxioms == null) - { - otherDefinitionAxioms = new List(); - } - otherDefinitionAxioms.Add(axiom); } diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index 238faaf6d..a9477140f 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -409,6 +409,7 @@ Consts<.out List/*!*/ ds.> ] IdsType [ OrderSpec ] + ( ";" | "uses" "{" { Axiom(. axioms.Add(ax); .) } "}") (. bool makeClone = false; foreach(TypedIdent/*!*/ x in xs){ Contract.Assert(x != null); @@ -427,15 +428,13 @@ Consts<.out List/*!*/ ds.> } makeClone = true; - foreach(var axiom in axioms) { - ds.Add(axiom); - } - var constant = new Constant(y, x, u, ParentsClone, ChildrenComplete, kv); - constant.NewDefinitionAxioms = axioms; + var constant = new Constant(y, x, u, ParentsClone, ChildrenComplete, kv, axioms); ds.Add(constant); } + foreach(var axiom in axioms) { + ds.Add(axiom); + } .) - ( ";" | "uses" "{" { Axiom(. axioms.Add(ax); .) } "}") . OrderSpec<.out bool ChildrenComplete, out List Parents.> diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 820a4a17b..e3db618b0 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -569,7 +569,9 @@ public bool PrintInstrumented { public bool InstrumentWithAsserts = false; public string ProverPreamble { get; set; }= null; public bool WarnNotEliminatedVars = false; - public bool PruneFunctionsAndAxioms = false; + + public enum PruneMode { None, Automatic, UsesClauses } + public PruneMode Prune = PruneMode.None; public enum InstrumentationPlaces { @@ -1656,6 +1658,12 @@ protected override bool ParseOption(string name, CommandLineOptionEngine.Command case "kInductionDepth": ps.GetNumericArgument(ref KInductionDepth); return true; + + case "prune": + int number = 0; + ps.GetNumericArgument(ref number); + Prune = (PruneMode)number; + return true; default: bool optionValue = false; @@ -1710,7 +1718,6 @@ protected override bool ParseOption(string name, CommandLineOptionEngine.Command ps.CheckBooleanFlag("trustInductiveSequentialization", ref trustInductiveSequentialization) || ps.CheckBooleanFlag("useBaseNameForFileName", ref UseBaseNameForFileName) || ps.CheckBooleanFlag("freeVarLambdaLifting", ref FreeVarLambdaLifting) || - ps.CheckBooleanFlag("pruneFunctionsAndAxioms", ref PruneFunctionsAndAxioms) || ps.CheckBooleanFlag("warnNotEliminatedVars", ref WarnNotEliminatedVars) ) { @@ -2291,8 +2298,10 @@ Use the SMT theory of arrays (as opposed to axioms). Supported only for monomorphic programs. /reflectAdd In the VC, generate an auxiliary symbol, elsewhere defined to be +, instead of +. - /pruneFunctionsAndAxioms - Prune declarations for each implementation + /prune: + 0 (default) - none + 1 - automatic pruning + 2 - aggressive pruning. Requires binding axioms to functions and constants using 'using' /relaxFocus Process foci in a bottom-up fashion. This way only generates a linear number of splits. The default way (top-down) is more aggressive and it may create an exponential number of splits. diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index dcfb0c96b..4aa4c42a1 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -321,6 +321,17 @@ void Consts(out List/*!*/ ds) { if (la.kind == 27) { OrderSpec(out ChildrenComplete, out Parents); } + if (la.kind == 9) { + Get(); + } else if (la.kind == 24) { + Get(); + Expect(25); + while (la.kind == 31) { + Axiom(out ax); + axioms.Add(ax); + } + Expect(26); + } else SynErr(109); bool makeClone = false; foreach(TypedIdent/*!*/ x in xs){ Contract.Assert(x != null); @@ -342,22 +353,10 @@ void Consts(out List/*!*/ ds) { foreach(var axiom in axioms) { ds.Add(axiom); } - var constant = new Constant(y, x, u, ParentsClone, ChildrenComplete, kv); - constant.NewDefinitionAxioms = axioms; + var constant = new Constant(y, x, u, ParentsClone, ChildrenComplete, kv, axioms); ds.Add(constant); } - if (la.kind == 9) { - Get(); - } else if (la.kind == 24) { - Get(); - Expect(25); - while (la.kind == 31) { - Axiom(out ax); - axioms.Add(ax); - } - Expect(26); - } else SynErr(109); } void Function(out List/*!*/ ds) { @@ -437,9 +436,9 @@ void Function(out List/*!*/ ds) { } Function/*!*/ func = new Function(z, z.val, typeParams, arguments, new Formal(retTyd.tok, retTyd, false, argKv), null, kv); - func.NewDefinitionAxioms = axioms; foreach(var axiom in axioms) { ds.Add(axiom); + func.AddOtherDefinitionAxiom(axiom); } Contract.Assert(func != null); diff --git a/Source/Core/Prune/DependencyEvaluator.cs b/Source/Core/Prune/DependencyEvaluator.cs index f59a11173..4f915016b 100644 --- a/Source/Core/Prune/DependencyEvaluator.cs +++ b/Source/Core/Prune/DependencyEvaluator.cs @@ -32,7 +32,7 @@ public static bool ExcludeDep(Declaration declaration) protected void AddIncoming(Declaration newIncoming) { - if (!ExcludeDep(newIncoming)) { + if (CommandLineOptions.Clo.Prune == CommandLineOptions.PruneMode.Automatic && !ExcludeDep(newIncoming)) { incomingSets.Add(new[] { newIncoming }); } } @@ -46,7 +46,9 @@ protected void AddOutgoing(Declaration newOutgoing) protected void AddIncoming(Declaration[] declarations) { - incomingSets.Add(declarations); + if (CommandLineOptions.Clo.Prune == CommandLineOptions.PruneMode.Automatic) { + incomingSets.Add(declarations); + } } protected DependencyEvaluator(Declaration declaration) diff --git a/Source/Core/Prune/Prune.cs b/Source/Core/Prune/Prune.cs index c686582cd..36ee7bb05 100644 --- a/Source/Core/Prune/Prune.cs +++ b/Source/Core/Prune/Prune.cs @@ -5,15 +5,10 @@ namespace Microsoft.Boogie { public class Prune { - private static bool ExcludeDep(Declaration d) - { - return d.Attributes != null && - QKeyValue.FindBoolAttribute(d.Attributes, "exclude_dep"); - } public static Dictionary> ComputeDeclarationDependencies(Program program) { - if (!CommandLineOptions.Clo.PruneFunctionsAndAxioms) + if (CommandLineOptions.Clo.Prune == CommandLineOptions.PruneMode.None) { return null; } @@ -108,7 +103,7 @@ bool DeadWhereAssumption(Cmd c) */ public static IEnumerable GetLiveDeclarations(Program program, List blocks) { - if (program.DeclarationDependencies == null || blocks == null || !CommandLineOptions.Clo.PruneFunctionsAndAxioms) + if (program.DeclarationDependencies == null || blocks == null || CommandLineOptions.Clo.Prune == CommandLineOptions.PruneMode.None) { return program.TopLevelDeclarations; } diff --git a/Source/UnitTests/ExecutionEngineTests/ProofIsolation.cs b/Source/UnitTests/ExecutionEngineTests/ProofIsolation.cs index e1eee27b2..2769c67f2 100644 --- a/Source/UnitTests/ExecutionEngineTests/ProofIsolation.cs +++ b/Source/UnitTests/ExecutionEngineTests/ProofIsolation.cs @@ -121,7 +121,7 @@ procedure M2(x: int, coloredBarrel: Barrel2 RGBColor2) {procedure1} {procedure2}"; CommandLineOptions.Install(new CommandLineOptions()); - CommandLineOptions.Clo.PruneFunctionsAndAxioms = true; + CommandLineOptions.Clo.Prune = CommandLineOptions.PruneMode.Automatic; CommandLineOptions.Clo.Parse(new string[]{}); ExecutionEngine.printer = new ConsolePrinter(); diff --git a/Source/VCGeneration/CheckerPool.cs b/Source/VCGeneration/CheckerPool.cs index c73a30d78..b32ae657b 100644 --- a/Source/VCGeneration/CheckerPool.cs +++ b/Source/VCGeneration/CheckerPool.cs @@ -82,7 +82,7 @@ public void Dispose() void PrepareChecker(Program program, Split split, Checker checker) { - if (checker.WillingToHandle(program) && !options.PruneFunctionsAndAxioms) + if (checker.WillingToHandle(program) && options.Prune == CommandLineOptions.PruneMode.None) { checker.GetReady(); return; diff --git a/Test/pruning/basic.bpl b/Test/pruning/basic.bpl index 4c789b182..043049f6d 100644 --- a/Test/pruning/basic.bpl +++ b/Test/pruning/basic.bpl @@ -1,4 +1,4 @@ -// RUN: %parallel-boogie "%s" > "%t" +// RUN: %parallel-boogie /prune:2 "%s" > "%t" // RUN: %diff "%s.expect" "%t" type Ty; @@ -11,9 +11,13 @@ const unique TagBool : TyTag uses { axiom Tag(TBool) == TagBool; } -type Box; -function $Box(T): Box; +function Magic(x: T): T uses { + axiom (forall x: T :: Magic(x) == 3); +} -function {:identity} Lit(x: T): T { x } uses { - axiom (forall x: T :: { $Box(Lit(x)) } $Box(Lit(x)) == Lit($Box(x)) ); +procedure test() + ensures Magic(4) == 3; + ensures TagBool == Tag(TBool); +{ + } \ No newline at end of file diff --git a/Test/pruning/basic.bpl.expect b/Test/pruning/basic.bpl.expect index cc5cde4d7..37fad75c9 100644 --- a/Test/pruning/basic.bpl.expect +++ b/Test/pruning/basic.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 0 verified, 0 errors +Boogie program verifier finished with 1 verified, 0 errors From 6a192fbbef8b87b9cb8fcf8efa85d02adf8bfaff Mon Sep 17 00:00:00 2001 From: Remy Willems <> Date: Fri, 5 Nov 2021 15:57:16 +0100 Subject: [PATCH 08/23] Fix bug related to definnition axioms --- Source/Core/Absy.cs | 28 +++++++--------------------- 1 file changed, 7 insertions(+), 21 deletions(-) diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 84ca7a82d..7eb23e4fc 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -2477,7 +2477,7 @@ public class Constant : Variable // that the parental situation is unconstrained. public readonly ReadOnlyCollection Parents; - public IReadOnlyList DefinitionAxioms { get; } + public IEnumerable DefinitionAxioms { get; } [ContractInvariantMethod] void ObjectInvariant() @@ -2490,34 +2490,20 @@ void ObjectInvariant() public readonly bool ChildrenComplete; public Constant(IToken /*!*/ tok, TypedIdent /*!*/ typedIdent) - : base(tok, typedIdent) + : this(tok, typedIdent, true) { - Contract.Requires(tok != null); - Contract.Requires(typedIdent != null); - Contract.Requires(typedIdent.Name != null && (!typedIdent.HasName || typedIdent.Name.Length > 0)); - Contract.Requires(typedIdent.WhereExpr == null); - this.Unique = true; - this.Parents = null; - this.ChildrenComplete = false; } public Constant(IToken /*!*/ tok, TypedIdent /*!*/ typedIdent, bool unique) - : base(tok, typedIdent) + : this(tok, typedIdent, unique, null, false, null, new List()) { - Contract.Requires(tok != null); - Contract.Requires(typedIdent != null); - Contract.Requires(typedIdent.Name != null && typedIdent.Name.Length > 0); - Contract.Requires(typedIdent.WhereExpr == null); - this.Unique = unique; - this.Parents = null; - this.ChildrenComplete = false; } public Constant(IToken /*!*/ tok, TypedIdent /*!*/ typedIdent, bool unique, - IEnumerable parents, bool childrenComplete, - QKeyValue kv, - IReadOnlyList definitionAxioms) + IEnumerable parents = null, bool childrenComplete = false, + QKeyValue kv = null, + IEnumerable definitionAxioms = null) : base(tok, typedIdent, kv) { Contract.Requires(tok != null); @@ -2528,7 +2514,7 @@ public Constant(IToken /*!*/ tok, TypedIdent /*!*/ typedIdent, this.Unique = unique; this.Parents = parents == null ? null : new ReadOnlyCollection(parents.ToList()); this.ChildrenComplete = childrenComplete; - this.DefinitionAxioms = definitionAxioms; + this.DefinitionAxioms = definitionAxioms ?? Enumerable.Empty(); } public override bool IsMutable => false; From e2eb2f26009846ea05b20b7664663fbc84550092 Mon Sep 17 00:00:00 2001 From: Remy Willems <> Date: Fri, 5 Nov 2021 15:56:49 +0100 Subject: [PATCH 09/23] Tiny refactorings --- Source/Core/AbsyQuant.cs | 2 +- Source/Core/CommandLineOptions.cs | 5 +---- Source/Core/LambdaHelper.cs | 2 +- 3 files changed, 3 insertions(+), 6 deletions(-) diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs index d37aa18c5..1e027b7c5 100644 --- a/Source/Core/AbsyQuant.cs +++ b/Source/Core/AbsyQuant.cs @@ -51,7 +51,7 @@ public List /*!*/ public Expr /*!*/ Body { - get { return _Body; } + get => _Body; set { if (Immutable) diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index e3db618b0..178bfe696 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -509,10 +509,7 @@ protected CommandLineOptions(string toolName, string descriptiveName) private static CommandLineOptions clo; - public static CommandLineOptions /*!*/ Clo - { - get { return clo; } - } + public static CommandLineOptions /*!*/ Clo => clo; public static void Install(CommandLineOptions options) { diff --git a/Source/Core/LambdaHelper.cs b/Source/Core/LambdaHelper.cs index 8e082b35e..b5b182aef 100644 --- a/Source/Core/LambdaHelper.cs +++ b/Source/Core/LambdaHelper.cs @@ -109,7 +109,7 @@ void ObjectInvariant() string FreshLambdaFunctionName() { - return string.Format("lambda#{0}", lambdaid++); + return $"lambda#{lambdaid++}"; } public override Expr VisitLambdaExpr(LambdaExpr lambda) From d77e4e63f7bcd049f50533f589cc16d70e4f36f5 Mon Sep 17 00:00:00 2001 From: Remy Willems <> Date: Mon, 8 Nov 2021 11:47:21 +0100 Subject: [PATCH 10/23] Fix text --- Source/Core/CommandLineOptions.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 178bfe696..324e51fd1 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -2298,7 +2298,7 @@ Use the SMT theory of arrays (as opposed to axioms). Supported /prune: 0 (default) - none 1 - automatic pruning - 2 - aggressive pruning. Requires binding axioms to functions and constants using 'using' + 2 - aggressive pruning. Requires binding axioms to functions and constants using 'uses' /relaxFocus Process foci in a bottom-up fashion. This way only generates a linear number of splits. The default way (top-down) is more aggressive and it may create an exponential number of splits. From 4ee7da57f2fce4771f451f719061a9a83ea687f7 Mon Sep 17 00:00:00 2001 From: Remy Willems <> Date: Mon, 8 Nov 2021 11:51:28 +0100 Subject: [PATCH 11/23] Cleanup --- Source/Core/Prune/ConstantVisitor.cs | 19 +++++++++++++++++++ Source/Core/Prune/DependencyEvaluator.cs | 17 ----------------- Source/Core/Prune/Prune.cs | 4 +--- Source/Graph/Graph.cs | 3 --- 4 files changed, 20 insertions(+), 23 deletions(-) create mode 100644 Source/Core/Prune/ConstantVisitor.cs diff --git a/Source/Core/Prune/ConstantVisitor.cs b/Source/Core/Prune/ConstantVisitor.cs new file mode 100644 index 000000000..52fc67831 --- /dev/null +++ b/Source/Core/Prune/ConstantVisitor.cs @@ -0,0 +1,19 @@ +namespace Microsoft.Boogie +{ + class ConstantVisitor : DependencyEvaluator + { + protected ConstantVisitor(Declaration declaration) : base(declaration) + { + } + + public static DependencyEvaluator GetDependencies(Constant constant) + { + var result = new ConstantVisitor(constant); + foreach (var definitionAxiom in constant.DefinitionAxioms) { + result.AddOutgoing(definitionAxiom); + } + result.Visit(constant); + return result; + } + } +} \ No newline at end of file diff --git a/Source/Core/Prune/DependencyEvaluator.cs b/Source/Core/Prune/DependencyEvaluator.cs index 4f915016b..4bcd1e3c1 100644 --- a/Source/Core/Prune/DependencyEvaluator.cs +++ b/Source/Core/Prune/DependencyEvaluator.cs @@ -56,21 +56,4 @@ protected DependencyEvaluator(Declaration declaration) this.declaration = declaration; } } - - class ConstantVisitor : DependencyEvaluator - { - protected ConstantVisitor(Declaration declaration) : base(declaration) - { - } - - public static DependencyEvaluator GetDependencies(Constant constant) - { - var result = new ConstantVisitor(constant); - foreach (var definitionAxiom in constant.DefinitionAxioms) { - result.AddOutgoing(definitionAxiom); - } - result.Visit(constant); - return result; - } - } } \ No newline at end of file diff --git a/Source/Core/Prune/Prune.cs b/Source/Core/Prune/Prune.cs index 36ee7bb05..1ee1fc83e 100644 --- a/Source/Core/Prune/Prune.cs +++ b/Source/Core/Prune/Prune.cs @@ -114,9 +114,7 @@ public static IEnumerable GetLiveDeclarations(Program program, List // an implementation only has outgoing edges. var reachableDeclarations = GraphAlgorithms.FindReachableNodesInGraphWithMergeNodes(program.DeclarationDependencies, blocksNode.outgoing).ToHashSet(); - var result = program.TopLevelDeclarations.Where(d => d is not Constant && d is not Axiom && d is not Function || reachableDeclarations.Contains(d)).ToList(); - var removedDeclarations = program.TopLevelDeclarations.Except(result).ToList(); - return result; + return program.TopLevelDeclarations.Where(d => d is not Constant && d is not Axiom && d is not Function || reachableDeclarations.Contains(d)); } } } \ No newline at end of file diff --git a/Source/Graph/Graph.cs b/Source/Graph/Graph.cs index 1bd34b5d5..ad5d4c703 100644 --- a/Source/Graph/Graph.cs +++ b/Source/Graph/Graph.cs @@ -1191,9 +1191,6 @@ public static IEnumerable FindReachableNodesInGraphWithMergeNodes(Dictio var outgoing = edges.GetValueOrDefault(node) ?? new List(); foreach (var x in outgoing) { - if (x.ToString().Contains("Agnes2")) { - Console.Write(""); - } todo.Push(x); } } From 67af2e0c00726a113fc35d25165d355971378a75 Mon Sep 17 00:00:00 2001 From: Remy Willems <> Date: Mon, 8 Nov 2021 15:53:11 +0100 Subject: [PATCH 12/23] Improve testcase --- Test/pruning/basic.bpl | 30 ++++++++++++++++++------------ 1 file changed, 18 insertions(+), 12 deletions(-) diff --git a/Test/pruning/basic.bpl b/Test/pruning/basic.bpl index 043049f6d..a92074a84 100644 --- a/Test/pruning/basic.bpl +++ b/Test/pruning/basic.bpl @@ -1,23 +1,29 @@ -// RUN: %parallel-boogie /prune:2 "%s" > "%t" +// RUN: %parallel-boogie /prune:2 /errorTrace:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" -type Ty; -const unique TBool : Ty; +const unique four : int; +const unique ProducerConst : bool uses { + axiom four == 4; +} -type TyTag; -function Tag(Ty) : TyTag; +function ConsumerFunc(x: int): int; -const unique TagBool : TyTag uses { - axiom Tag(TBool) == TagBool; +function ProducerFunc(x: int): bool uses { + axiom (forall x: int :: ConsumerFunc(x) == 3); } -function Magic(x: T): T uses { - axiom (forall x: T :: Magic(x) == 3); +procedure hasAxioms() + requires ProducerFunc(2); + requires ProducerConst; + ensures ConsumerFunc(4) == 3; + ensures four == 4; +{ + } -procedure test() - ensures Magic(4) == 3; - ensures TagBool == Tag(TBool); +procedure doesNotHaveAxioms() + ensures ConsumerFunc(4) == 3; // The ConsumerFunc axiom is pruned away, so this fails to verify + ensures four == 4; // The ProducerConstant axiom is pruned away, so this fails to verify { } \ No newline at end of file From 524772c2765cf2cf9ec26a5b88133de5f81e495f Mon Sep 17 00:00:00 2001 From: Remy Willems <> Date: Tue, 9 Nov 2021 16:11:45 +0100 Subject: [PATCH 13/23] Fix tests --- .../Prune.bpl => pruning/Automatic.bpl} | 10 +--- Test/pruning/Automatic.bpl.expect | 6 +++ Test/pruning/{basic.bpl => Basic.bpl} | 0 Test/pruning/Basic.bpl.expect | 6 +++ Test/pruning/Focus.bpl | 47 +++++++++++++++++++ Test/pruning/Focus.bpl.expect | 3 ++ Test/pruning/basic.bpl.expect | 2 - Test/test0/Focus.bpl | 33 ------------- Test/test0/Focus.bpl.expect | 7 --- Test/test0/Prune.bpl.expect | 11 ----- 10 files changed, 63 insertions(+), 62 deletions(-) rename Test/{test0/Prune.bpl => pruning/Automatic.bpl} (76%) create mode 100644 Test/pruning/Automatic.bpl.expect rename Test/pruning/{basic.bpl => Basic.bpl} (100%) create mode 100644 Test/pruning/Basic.bpl.expect create mode 100644 Test/pruning/Focus.bpl create mode 100644 Test/pruning/Focus.bpl.expect delete mode 100644 Test/pruning/basic.bpl.expect delete mode 100644 Test/test0/Focus.bpl delete mode 100644 Test/test0/Focus.bpl.expect delete mode 100644 Test/test0/Prune.bpl.expect diff --git a/Test/test0/Prune.bpl b/Test/pruning/Automatic.bpl similarity index 76% rename from Test/test0/Prune.bpl rename to Test/pruning/Automatic.bpl index 0895a997d..ec114e927 100644 --- a/Test/test0/Prune.bpl +++ b/Test/pruning/Automatic.bpl @@ -1,4 +1,4 @@ -// RUN: %parallel-boogie /pruneFunctionsAndAxioms "%s" > "%t" +// RUN: %parallel-boogie /prune:1 /errorTrace:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" function {:exclude_dep} f1 (x: int) : int; @@ -24,14 +24,6 @@ procedure I1(x : int) returns (y: int) // is thus removed from the outgoing set of I1. // This makes the axiom on line 23 unreachable from I1, which is thus pruned away. { - var i: int where false; - - if (x > 0) { - havoc i; // mentioning i in this branch results in assuming false because of the where clause. - // Thus, the post-condition proves for this path. - } else { - assume {:focus} true; // i is not mentioned in this branch so the where clause is not assumed for it. - } } procedure I2(x : int) returns (y: int) diff --git a/Test/pruning/Automatic.bpl.expect b/Test/pruning/Automatic.bpl.expect new file mode 100644 index 000000000..6ea6e0575 --- /dev/null +++ b/Test/pruning/Automatic.bpl.expect @@ -0,0 +1,6 @@ +Automatic.bpl(27,1): Error: A postcondition might not hold on this return path. +Automatic.bpl(23,3): Related location: This is the postcondition that might not hold. +Automatic.bpl(57,1): Error: A postcondition might not hold on this return path. +Automatic.bpl(55,3): Related location: This is the postcondition that might not hold. + +Boogie program verifier finished with 1 verified, 2 errors diff --git a/Test/pruning/basic.bpl b/Test/pruning/Basic.bpl similarity index 100% rename from Test/pruning/basic.bpl rename to Test/pruning/Basic.bpl diff --git a/Test/pruning/Basic.bpl.expect b/Test/pruning/Basic.bpl.expect new file mode 100644 index 000000000..815724294 --- /dev/null +++ b/Test/pruning/Basic.bpl.expect @@ -0,0 +1,6 @@ +Basic.bpl(29,1): Error: A postcondition might not hold on this return path. +Basic.bpl(25,3): Related location: This is the postcondition that might not hold. +Basic.bpl(29,1): Error: A postcondition might not hold on this return path. +Basic.bpl(26,3): Related location: This is the postcondition that might not hold. + +Boogie program verifier finished with 1 verified, 2 errors diff --git a/Test/pruning/Focus.bpl b/Test/pruning/Focus.bpl new file mode 100644 index 000000000..9ea7e6bec --- /dev/null +++ b/Test/pruning/Focus.bpl @@ -0,0 +1,47 @@ +// RUN: %parallel-boogie /vcsDumpSplits /errorTrace:0 "%s" > "%t" +// RUN: mv %/S/Ex.split* %/S/Output/ +// RUN: %diff "%s.expect" "%t" +// RUN: %diff ./Output/Ex.split.0.bpl ./Output/Ex.split.0.bpl +// RUN: %diff ./Output/Ex.split.1.bpl ./Output/Ex.split.1.bpl +// RUN: %diff ./Output/Ex.split.2.bpl ./Output/Ex.split.2.bpl +// RUN: %diff ./Output/Ex.split.3.bpl ./Output/Ex.split.3.bpl +// RUN: %diff ./Output/Ex.split.4.bpl ./Output/Ex.split.4.bpl +// RUN: %diff ./Output/Ex.split.5.bpl ./Output/Ex.split.5.bpl + +procedure Ex() returns (y: int) + ensures y >= 0; +{ + var x: int; + x := 5; + y := 0; + while (x > 0) + invariant x + y == 5; + invariant x*x <= 25; + { + x := x - 1; + assert {:split_here} (x+y) * (x+y) > 16; // should not lead to more than one split. + assert {:focus} (x+y) * (x+y) > 25; + y := y + 1; + if (x < 3) { + assert 2 < 2; + assert {:focus} y*y > 4; + } + else { + assert 2 < 2; + } + assert {:focus} (x+y) * (x+y) == 25; + } +} + +procedure focusInconsistency(x : int) returns (y: int) + ensures false; +{ + var i: int where false; + + if (x > 0) { + havoc i; // mentioning i in this branch results in assuming false because of the where clause. + // Thus, the post-condition proves for this path. + } else { + assume {:focus} true; // i is not mentioned in this branch so the where clause is not assumed for it. + } +} diff --git a/Test/pruning/Focus.bpl.expect b/Test/pruning/Focus.bpl.expect new file mode 100644 index 000000000..d75e72f55 --- /dev/null +++ b/Test/pruning/Focus.bpl.expect @@ -0,0 +1,3 @@ +Focus.bpl(22,5): Error: This assertion might not hold. + +Boogie program verifier finished with 1 verified, 1 error diff --git a/Test/pruning/basic.bpl.expect b/Test/pruning/basic.bpl.expect deleted file mode 100644 index 37fad75c9..000000000 --- a/Test/pruning/basic.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/test0/Focus.bpl b/Test/test0/Focus.bpl deleted file mode 100644 index e5c72eb67..000000000 --- a/Test/test0/Focus.bpl +++ /dev/null @@ -1,33 +0,0 @@ -// RUN: %parallel-boogie /vcsDumpSplits "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -// RUN: %diff Ex.split.0.bpl Ex.split.0.bpl -// RUN: %diff Ex.split.1.bpl Ex.split.1.bpl -// RUN: %diff Ex.split.2.bpl Ex.split.2.bpl -// RUN: %diff Ex.split.3.bpl Ex.split.3.bpl -// RUN: %diff Ex.split.4.bpl Ex.split.4.bpl -// RUN: %diff Ex.split.5.bpl Ex.split.5.bpl - -procedure Ex() returns (y: int) - ensures y >= 0; -{ - var x: int; - x := 5; - y := 0; - while (x > 0) - invariant x + y == 5; - invariant x*x <= 25; - { - x := x - 1; - assert {:split_here} (x+y) * (x+y) > 16; // should not lead to more than one split. - assert {:focus} (x+y) * (x+y) > 25; - y := y + 1; - if (x < 3) { - assert 2 < 2; - assert {:focus} y*y > 4; - } - else { - assert 2 < 2; - } - assert {:focus} (x+y) * (x+y) == 25; - } -} diff --git a/Test/test0/Focus.bpl.expect b/Test/test0/Focus.bpl.expect deleted file mode 100644 index 6c717cbc2..000000000 --- a/Test/test0/Focus.bpl.expect +++ /dev/null @@ -1,7 +0,0 @@ -Focus.bpl(21,5): Error: This assertion might not hold. -Execution trace: - Focus.bpl(14,5): anon0 - Focus.bpl(16,3): anon5_LoopHead - Focus.bpl(20,7): anon5_LoopBody - -Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test0/Prune.bpl.expect b/Test/test0/Prune.bpl.expect deleted file mode 100644 index 7c04fc0c1..000000000 --- a/Test/test0/Prune.bpl.expect +++ /dev/null @@ -1,11 +0,0 @@ -Prune.bpl(35,1): Error: A postcondition might not hold on this return path. -Prune.bpl(23,3): Related location: This is the postcondition that might not hold. -Execution trace: - Prune.bpl(29,3): anon0 - Prune.bpl(33,5): anon3_Else -Prune.bpl(65,1): Error: A postcondition might not hold on this return path. -Prune.bpl(63,3): Related location: This is the postcondition that might not hold. -Execution trace: - Prune.bpl(65,1): anon0 - -Boogie program verifier finished with 1 verified, 2 errors From fc5665f262f398d7bbcbf1e75d6ca29cb55d6584 Mon Sep 17 00:00:00 2001 From: Remy Willems <> Date: Tue, 9 Nov 2021 16:42:30 +0100 Subject: [PATCH 14/23] Update parser --- Source/Core/Parser.cs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index 4aa4c42a1..ed801d05b 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -350,12 +350,12 @@ void Consts(out List/*!*/ ds) { } makeClone = true; - foreach(var axiom in axioms) { - ds.Add(axiom); - } var constant = new Constant(y, x, u, ParentsClone, ChildrenComplete, kv, axioms); ds.Add(constant); } + foreach(var axiom in axioms) { + ds.Add(axiom); + } } From edcf8786fc1c3cf70d2cd1512a05feec9f97df62 Mon Sep 17 00:00:00 2001 From: Remy Willems <> Date: Tue, 9 Nov 2021 18:23:08 +0100 Subject: [PATCH 15/23] Update test --- Test/test0/WhereParsing2.bpl.expect | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Test/test0/WhereParsing2.bpl.expect b/Test/test0/WhereParsing2.bpl.expect index 17484299e..9932f556a 100644 --- a/Test/test0/WhereParsing2.bpl.expect +++ b/Test/test0/WhereParsing2.bpl.expect @@ -1,2 +1,2 @@ -WhereParsing2.bpl(3,14): error: ";" expected +WhereParsing2.bpl(3,14): error: invalid Consts 1 parse errors detected in WhereParsing2.bpl From 1c9691e4574cb0ae228ef3cc8cd3f9d37d36575c Mon Sep 17 00:00:00 2001 From: Remy Willems <> Date: Thu, 11 Nov 2021 13:02:04 +0100 Subject: [PATCH 16/23] Code review --- Source/Core/Prune/DependencyEvaluator.cs | 4 ++-- Source/Graph/Graph.cs | 2 +- Test/test0/Prune.bpl | 4 ++-- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/Source/Core/Prune/DependencyEvaluator.cs b/Source/Core/Prune/DependencyEvaluator.cs index 64b3f3a89..105102d99 100644 --- a/Source/Core/Prune/DependencyEvaluator.cs +++ b/Source/Core/Prune/DependencyEvaluator.cs @@ -24,8 +24,8 @@ public class DependencyEvaluator : ReadOnlyVisitor public readonly HashSet outgoing = new(); // an edge can either be a function or a constant. public List incomingSets = new(); public HashSet types = new(); - - public static bool ExcludeDep(Declaration declaration) + + private static bool ExcludeDep(Declaration declaration) { return declaration.Attributes != null && QKeyValue.FindBoolAttribute(declaration.Attributes, "exclude_dep"); } diff --git a/Source/Graph/Graph.cs b/Source/Graph/Graph.cs index ba7bafd1a..6ebe87f43 100644 --- a/Source/Graph/Graph.cs +++ b/Source/Graph/Graph.cs @@ -1169,7 +1169,7 @@ public static class GraphAlgorithms /** * A merge node is a node that has multiple incoming edges, and which cannot be traversed unless all incoming edges have been traversed. - * A merge node is represented by an object of type IReadOnlySet{object} + * A merge node is represented by an object of type IEnumerable{object} */ public static IEnumerable FindReachableNodesInGraphWithMergeNodes(Dictionary> edges, IEnumerable roots) { diff --git a/Test/test0/Prune.bpl b/Test/test0/Prune.bpl index 0895a997d..25af3fc1e 100644 --- a/Test/test0/Prune.bpl +++ b/Test/test0/Prune.bpl @@ -22,7 +22,7 @@ procedure I1(x : int) returns (y: int) requires R(x); ensures Q(f1(x)); // this post-condition doesn't prove because f1 is attributed as exclude_dep and // is thus removed from the outgoing set of I1. - // This makes the axiom on line 23 unreachable from I1, which is thus pruned away. + // This makes the axiom on line 16 unreachable from I1, which is thus pruned away. { var i: int where false; @@ -36,7 +36,7 @@ procedure I1(x : int) returns (y: int) procedure I2(x : int) returns (y: int) requires R(x); - ensures Q(f2(x)); // proved using the axiom on line 23 + ensures Q(f2(x)); // proved using the axiom on line 16 { } From 1634080cae7e25c99f1b5e0c4ac0424264c1cb3a Mon Sep 17 00:00:00 2001 From: Remy Willems <> Date: Thu, 11 Nov 2021 14:24:32 +0100 Subject: [PATCH 17/23] Refactoring --- Source/Core/Prune/DependencyEvaluator.cs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Source/Core/Prune/DependencyEvaluator.cs b/Source/Core/Prune/DependencyEvaluator.cs index 4bcd1e3c1..8e4a75813 100644 --- a/Source/Core/Prune/DependencyEvaluator.cs +++ b/Source/Core/Prune/DependencyEvaluator.cs @@ -32,8 +32,8 @@ public static bool ExcludeDep(Declaration declaration) protected void AddIncoming(Declaration newIncoming) { - if (CommandLineOptions.Clo.Prune == CommandLineOptions.PruneMode.Automatic && !ExcludeDep(newIncoming)) { - incomingSets.Add(new[] { newIncoming }); + if (!ExcludeDep(newIncoming)) { + AddIncoming(new[] { newIncoming }); } } From 56b011f654f2dc49a2715e74b04d5908324991c4 Mon Sep 17 00:00:00 2001 From: Remy Willems <> Date: Mon, 15 Nov 2021 10:05:22 +0100 Subject: [PATCH 18/23] Add documentation to PruneMode --- Source/Core/CommandLineOptions.cs | 68 ++++++++++++++++++++++++++++++- 1 file changed, 67 insertions(+), 1 deletion(-) diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 324e51fd1..b0e22ebf4 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -567,7 +567,73 @@ public bool PrintInstrumented { public string ProverPreamble { get; set; }= null; public bool WarnNotEliminatedVars = false; - public enum PruneMode { None, Automatic, UsesClauses } + public enum PruneMode { + None, + + /** + * Automatic pruning will remove any declarations that are guaranteed not to be useful for verifying the current implementation. + * Automatic pruning detects incoming edges in axioms, for example: + * + * function A(int) returns (int); + * axiom A(3) == 2; + * + * Will detect both an incoming and an outgoing edge from and to A, in the axiom. So if either the axiom of the function A is live, the other is also live. + */ + Automatic, + + /** + * UsesClauses pruning will not detect any incoming edges in axioms, + * and instead depends on uses clauses in the input program + * to determine the outgoing edges of functions and constants. + * + * The reason to use UsesClauses is that Automatic pruning mode can miss opportunities for pruning. + * Consider the following program: + * + * ``` + * function F(int) returns (int); + * function G(int) returns (int); + * + * // declaration axiom for F + * axiom forall x: int :: F(x) == x * 2 + * + * // declaration axiom for G + * axiom forall x: int :: G(x) == F(x) + 1 + * + * procedure FMultipliesByTwo(x: int) + * ensures F(x) - x == x + * { } + * ``` + * + * Automatic pruning will not remove any declarations when verifying the procedure FMultipliesByTwo, + * since it refers to F, which refers to the declaration axiom of G through an incoming edge in the axiom, + * which also has an outgoing edge to G. + * + * If we rewrite the previous program to + * + * ``` + * function F(int) returns (int) uses { + * axiom forall x: int :: F(x) == x * 2 + * } + * function G(int) returns (int) { + * axiom forall x: int :: G(x) == F(x) + 1 + * } + * + * procedure FMultipliesByTwo(x: int) + * ensures F(x) - x == x + * { } + * ``` + * + * And apply UsesClauses pruning, then G and its axiom will be removed when verifying FMultipliesByTwo. + * + * An alternative to using UsesClauses pruning, is to add an {:exclude_dep} attributes to a function or constant, + * which prevents axioms from detecting incoming edges from that declaration. + * To add outgoing edges to the function or constant, uses clauses should be used. + * + * Using Automatic pruning in combination with {:exclude_dep} can be useful if this provides good enough pruning, + * or to migrate from Automatic to UsesClauses pruning. + */ + UsesClauses + } public PruneMode Prune = PruneMode.None; public enum InstrumentationPlaces From b6d5e73ff11ea93c9cd25091e732c0b49e95c26b Mon Sep 17 00:00:00 2001 From: Remy Willems <> Date: Tue, 16 Nov 2021 11:26:20 +0100 Subject: [PATCH 19/23] Small refactorings, and bumped minor version number because of the additional reserved keyword 'uses' --- Source/Core/BoogiePL.atg | 6 +++--- Source/Core/CommandLineOptions.cs | 10 ++++++---- Source/Directory.Build.props | 2 +- Test/pruning/Basic.bpl | 4 ++-- 4 files changed, 12 insertions(+), 10 deletions(-) diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index a9477140f..3c478a3d8 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -490,9 +490,9 @@ Function<.out List/*!*/ ds.> | ":" Type (. retTyd = new TypedIdent(retTy.tok, TypedIdent.NoName, retTy); .) ) - ( "{" Expression (. definition = tmp; .) "}" [ "uses" "{" { Axiom(. axioms.Add(ax); .) } "}" ] | - "uses" "{" { Axiom(. axioms.Add(ax); .) } "}" | - ";" + ( "{" Expression (. definition = tmp; .) "}" [ "uses" "{" { Axiom(. axioms.Add(ax); .) } "}" ] + | "uses" "{" { Axiom(. axioms.Add(ax); .) } "}" + | ";" ) (. if (retTyd == null) { diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index b0e22ebf4..2fe749ef1 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -571,10 +571,12 @@ public enum PruneMode { None, /** - * Automatic pruning will remove any declarations that are guaranteed not to be useful for verifying the current implementation. + * Automatic pruning will remove any declarations that do not reference, directly or indirectly, and are not referenced by, the implementation being verified, + * and declarations which cannot be used for verifying the current implementation, such as axioms with triggers that can not be satisfied. + * * Automatic pruning detects incoming edges in axioms, for example: * - * function A(int) returns (int); + * function A(int): int; * axiom A(3) == 2; * * Will detect both an incoming and an outgoing edge from and to A, in the axiom. So if either the axiom of the function A is live, the other is also live. @@ -590,8 +592,8 @@ public enum PruneMode { * Consider the following program: * * ``` - * function F(int) returns (int); - * function G(int) returns (int); + * function F(int): int; + * function G(int): int; * * // declaration axiom for F * axiom forall x: int :: F(x) == x * 2 diff --git a/Source/Directory.Build.props b/Source/Directory.Build.props index 1a6a1ba69..e9b72044f 100644 --- a/Source/Directory.Build.props +++ b/Source/Directory.Build.props @@ -2,7 +2,7 @@ - 2.9.6 + 2.10.6 net5.0 false Boogie diff --git a/Test/pruning/Basic.bpl b/Test/pruning/Basic.bpl index a92074a84..d22a26ab1 100644 --- a/Test/pruning/Basic.bpl +++ b/Test/pruning/Basic.bpl @@ -1,8 +1,8 @@ // RUN: %parallel-boogie /prune:2 /errorTrace:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" -const unique four : int; -const unique ProducerConst : bool uses { +const unique four: int; +const unique ProducerConst: bool uses { axiom four == 4; } From 4ece71954a47514626863df62a730b6227e6b7c6 Mon Sep 17 00:00:00 2001 From: Remy Willems <> Date: Wed, 17 Nov 2021 00:14:25 +0100 Subject: [PATCH 20/23] Update version number --- Source/Directory.Build.props | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/Directory.Build.props b/Source/Directory.Build.props index e9b72044f..a4dd17768 100644 --- a/Source/Directory.Build.props +++ b/Source/Directory.Build.props @@ -2,7 +2,7 @@ - 2.10.6 + 2.10.0 net5.0 false Boogie From 09177ee750e609686d2cee47694328cdf93e339f Mon Sep 17 00:00:00 2001 From: Remy Willems <> Date: Mon, 22 Nov 2021 16:05:39 +0100 Subject: [PATCH 21/23] Documentation improvements --- Source/Core/CommandLineOptions.cs | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 2fe749ef1..4907e5992 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -571,15 +571,18 @@ public enum PruneMode { None, /** - * Automatic pruning will remove any declarations that do not reference, directly or indirectly, and are not referenced by, the implementation being verified, - * and declarations which cannot be used for verifying the current implementation, such as axioms with triggers that can not be satisfied. + * Automatic pruning will remove any declarations that do not reference, + * directly or indirectly, and are not referenced by, the implementation being verified, + * and declarations which cannot be used for verifying the current implementation, + * such as axioms with triggers that can not be satisfied. * * Automatic pruning detects incoming edges in axioms, for example: * * function A(int): int; * axiom A(3) == 2; * - * Will detect both an incoming and an outgoing edge from and to A, in the axiom. So if either the axiom of the function A is live, the other is also live. + * Will detect edges in both directions between the declaration of A and the axiom declaration. + * So if either declaration is live, both declarations are live. */ Automatic, @@ -616,7 +619,7 @@ public enum PruneMode { * function F(int) returns (int) uses { * axiom forall x: int :: F(x) == x * 2 * } - * function G(int) returns (int) { + * function G(int) returns (int) uses { * axiom forall x: int :: G(x) == F(x) + 1 * } * @@ -627,12 +630,12 @@ public enum PruneMode { * * And apply UsesClauses pruning, then G and its axiom will be removed when verifying FMultipliesByTwo. * - * An alternative to using UsesClauses pruning, is to add an {:exclude_dep} attributes to a function or constant, + * An alternative to using UsesClauses pruning, is to add an {:exclude_dep} attribute to a function or constant, * which prevents axioms from detecting incoming edges from that declaration. * To add outgoing edges to the function or constant, uses clauses should be used. * * Using Automatic pruning in combination with {:exclude_dep} can be useful if this provides good enough pruning, - * or to migrate from Automatic to UsesClauses pruning. + * or to migrate from None to UsesClauses pruning. */ UsesClauses } From c9f3d270b9ef7ae78175b5f6a10cab63dcfdbf40 Mon Sep 17 00:00:00 2001 From: Remy Willems <> Date: Mon, 22 Nov 2021 16:10:27 +0100 Subject: [PATCH 22/23] Update text --- Source/Core/CommandLineOptions.cs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index f36feb484..c85c8a8f9 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -610,11 +610,11 @@ public enum PruneMode { Automatic, /** - * UsesClauses pruning will not detect any incoming edges in axioms, - * and instead depends on uses clauses in the input program - * to determine the outgoing edges of functions and constants. + * UsesClauses pruning will not automatically detect incoming edges in axioms. + * Instead it depends on uses clauses in the input program to determine the outgoing edges of functions and constants. + * Outgoing edges in axioms are still detected automatically. * - * The reason to use UsesClauses is that Automatic pruning mode can miss opportunities for pruning. + * The reason to use UsesClauses over Automatic pruning is that the latter can miss pruning opportunities. * Consider the following program: * * ``` From 4042f5db7a5b873010b105ff24ebc175f3fde742 Mon Sep 17 00:00:00 2001 From: Remy Willems <> Date: Wed, 24 Nov 2021 11:56:00 +0100 Subject: [PATCH 23/23] Rename UsesClauses to usesDecls --- Source/Core/CommandLineOptions.cs | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index c85c8a8f9..d271d65b6 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -610,11 +610,11 @@ public enum PruneMode { Automatic, /** - * UsesClauses pruning will not automatically detect incoming edges in axioms. + * UsesDecls pruning will not automatically detect incoming edges in axioms. * Instead it depends on uses clauses in the input program to determine the outgoing edges of functions and constants. * Outgoing edges in axioms are still detected automatically. * - * The reason to use UsesClauses over Automatic pruning is that the latter can miss pruning opportunities. + * The reason to use UsesDecls over Automatic pruning is that the latter can miss pruning opportunities. * Consider the following program: * * ``` @@ -651,16 +651,16 @@ public enum PruneMode { * { } * ``` * - * And apply UsesClauses pruning, then G and its axiom will be removed when verifying FMultipliesByTwo. + * And apply UsesDecls pruning, then G and its axiom will be removed when verifying FMultipliesByTwo. * - * An alternative to using UsesClauses pruning, is to add an {:exclude_dep} attribute to a function or constant, + * An alternative to using UsesDecls pruning, is to add an {:exclude_dep} attribute to a function or constant, * which prevents axioms from detecting incoming edges from that declaration. * To add outgoing edges to the function or constant, uses clauses should be used. * * Using Automatic pruning in combination with {:exclude_dep} can be useful if this provides good enough pruning, - * or to migrate from None to UsesClauses pruning. + * or to migrate from None to UsesDecls pruning. */ - UsesClauses + UsesDecls } public PruneMode Prune = PruneMode.None;