diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index dcca7e5e4..7eb23e4fc 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 IEnumerable DefinitionAxioms { get; } + [ContractInvariantMethod] void ObjectInvariant() { @@ -2483,33 +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) + IEnumerable parents = null, bool childrenComplete = false, + QKeyValue kv = null, + IEnumerable definitionAxioms = null) : base(tok, typedIdent, kv) { Contract.Requires(tok != null); @@ -2520,12 +2514,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 ?? Enumerable.Empty(); } - public override bool IsMutable - { - get { return false; } - } + public override bool IsMutable => false; public override void Emit(TokenTextWriter stream, int level) { @@ -3301,22 +3293,16 @@ public class Function : DeclWithFormals public NAryExpr DefinitionBody; // Only set if the function is declared with {:define} public Axiom DefinitionAxiom; - public IList otherDefinitionAxioms; + public IList otherDefinitionAxioms = new List(); + public IEnumerable DefinitionAxioms => + (DefinitionAxiom == null ? Enumerable.Empty() : new[]{ DefinitionAxiom }).Concat(otherDefinitionAxioms); - public IEnumerable OtherDefinitionAxioms - { - get { return otherDefinitionAxioms; } - } + public IEnumerable OtherDefinitionAxioms => otherDefinitionAxioms; public void AddOtherDefinitionAxiom(Axiom axiom) { Contract.Requires(axiom != null); - if (otherDefinitionAxioms == null) - { - otherDefinitionAxioms = new List(); - } - otherDefinitionAxioms.Add(axiom); } 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/BoogiePL.atg b/Source/Core/BoogiePL.atg index f5e74eaa3..3c478a3d8 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; .) @@ -407,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); @@ -424,11 +427,14 @@ Consts<.out List/*!*/ ds.> ParentsClone = Parents; } makeClone = true; - - ds.Add(new Constant(y, x, u, ParentsClone, ChildrenComplete, kv)); + + var constant = new Constant(y, x, u, ParentsClone, ChildrenComplete, kv, axioms); + ds.Add(constant); + } + foreach(var axiom in axioms) { + ds.Add(axiom); } .) - ";" . OrderSpec<.out bool ChildrenComplete, out List Parents.> @@ -462,6 +468,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 +476,7 @@ Function<.out List/*!*/ ds.> QKeyValue kv = null; Expr definition = null; Expr/*!*/ tmp; + Axiom ax; .) "function" { Attribute } Ident [ TypeParams ] @@ -482,7 +490,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 +501,15 @@ Function<.out List/*!*/ ds.> } Function/*!*/ func = new Function(z, z.val, typeParams, arguments, new Formal(retTyd.tok, retTyd, false, argKv), null, kv); + foreach(var axiom in axioms) { + ds.Add(axiom); + func.AddOtherDefinitionAxiom(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/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index b131887c7..d271d65b6 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -523,10 +523,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) { @@ -592,7 +589,80 @@ 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 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 edges in both directions between the declaration of A and the axiom declaration. + * So if either declaration is live, both declarations are live. + */ + Automatic, + + /** + * 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 UsesDecls over Automatic pruning is that the latter can miss pruning opportunities. + * Consider the following program: + * + * ``` + * function F(int): int; + * function G(int): 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) uses { + * axiom forall x: int :: G(x) == F(x) + 1 + * } + * + * procedure FMultipliesByTwo(x: int) + * ensures F(x) - x == x + * { } + * ``` + * + * And apply UsesDecls pruning, then G and its axiom will be removed when verifying FMultipliesByTwo. + * + * 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 UsesDecls pruning. + */ + UsesDecls + } + public PruneMode Prune = PruneMode.None; public enum InstrumentationPlaces { @@ -1681,6 +1751,12 @@ protected override bool ParseOption(string name, CommandLineOptionEngine.Command ps.GetNumericArgument(ref KInductionDepth); return true; + case "prune": + int number = 0; + ps.GetNumericArgument(ref number); + Prune = (PruneMode)number; + return true; + case "emitDebugInformation": ps.GetNumericArgument(ref emitDebugInformation); return true; @@ -1738,7 +1814,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) ) { @@ -2323,8 +2398,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 '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. 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) diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index a2078a7d4..ed801d05b 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,9 +318,20 @@ void Consts(out List/*!*/ ds) { u = true; } IdsType(out xs); - if (la.kind == 24) { + 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); @@ -336,11 +349,14 @@ void Consts(out List/*!*/ ds) { ParentsClone = Parents; } makeClone = true; - - ds.Add(new Constant(y, x, u, ParentsClone, ChildrenComplete, kv)); + + var constant = new Constant(y, x, u, ParentsClone, ChildrenComplete, kv, axioms); + ds.Add(constant); + } + foreach(var axiom in axioms) { + ds.Add(axiom); } - Expect(9); } void Function(out List/*!*/ ds) { @@ -349,6 +365,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 +373,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 +395,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 +404,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); + foreach(var axiom in axioms) { + ds.Add(axiom); + func.AddOtherDefinitionAxiom(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 +495,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 +507,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 +528,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 +548,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 +563,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 +575,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 +600,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 +614,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 +674,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 +715,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 +822,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 +845,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 +858,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 +889,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 +921,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 +929,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 +937,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 +948,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 +967,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 +1021,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 +1041,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 +1069,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 +1080,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 +1091,7 @@ void LabelOrCmd(out Cmd c, out IToken label) { Expect(9); break; } - case 49: { + case 50: { Get(); x = t; Idents(out xs); @@ -1065,25 +1105,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 +1131,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 +1148,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 +1157,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 +1171,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 +1197,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 +1221,7 @@ void WhileCmd(out WhileCmd/*!*/ wcmd) { Expect(9); } - Expect(28); + Expect(25); StmtList(out body); wcmd = new WhileCmd(x, guard, invariants, body); } @@ -1190,7 +1230,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 +1243,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 +1267,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 +1285,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 +1300,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 +1310,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 +1330,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 +1370,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 +1387,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 +1399,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 +1413,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 +1431,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 +1443,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 +1454,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 +1481,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 +1492,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 +1518,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 +1547,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 +1562,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 +1623,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 +1645,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 +1708,7 @@ void CoercionExpression(out Expr/*!*/ e) { e = new BvBounds(x, bn, ((LiteralExpr)e).asBigNum); } - } else SynErr(133); + } else SynErr(135); } } @@ -1700,7 +1740,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 +1789,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 +1808,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 +1817,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 +1826,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 +1835,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 +1879,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 +1918,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 +1940,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 +1965,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 +2005,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 +2022,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 +2069,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 +2078,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 +2090,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 +2104,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 +2114,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 +2138,7 @@ void SpecBlock(out Block/*!*/ b) { } } - if (la.kind == 39) { + if (la.kind == 40) { Get(); y = t; Idents(out xs); @@ -2107,11 +2147,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 +2160,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 +2208,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 +2223,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 +2260,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 +2324,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/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/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 105102d99..809e83ba4 100644 --- a/Source/Core/Prune/DependencyEvaluator.cs +++ b/Source/Core/Prune/DependencyEvaluator.cs @@ -33,7 +33,7 @@ private static bool ExcludeDep(Declaration declaration) protected void AddIncoming(Declaration newIncoming) { if (!ExcludeDep(newIncoming)) { - incomingSets.Add(new[] { newIncoming }); + AddIncoming(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/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 ef0ac507a..1ee1fc83e 100644 --- a/Source/Core/Prune/Prune.cs +++ b/Source/Core/Prune/Prune.cs @@ -5,21 +5,17 @@ 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; } - 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) { @@ -107,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; } @@ -118,8 +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)); - 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/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/Directory.Build.props b/Source/Directory.Build.props index 1a6a1ba69..a4dd17768 100644 --- a/Source/Directory.Build.props +++ b/Source/Directory.Build.props @@ -2,7 +2,7 @@ - 2.9.6 + 2.10.0 net5.0 false Boogie diff --git a/Source/Graph/Graph.cs b/Source/Graph/Graph.cs index 6ebe87f43..b58a05ee6 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 IEnumerable{object} diff --git a/Source/UnitTests/ExecutionEngineTests/ProofIsolation.cs b/Source/UnitTests/ExecutionEngineTests/ProofIsolation.cs index eff206bd7..725fcd49e 100644 --- a/Source/UnitTests/ExecutionEngineTests/ProofIsolation.cs +++ b/Source/UnitTests/ExecutionEngineTests/ProofIsolation.cs @@ -150,7 +150,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/test0/Prune.bpl b/Test/pruning/Automatic.bpl similarity index 76% rename from Test/test0/Prune.bpl rename to Test/pruning/Automatic.bpl index 25af3fc1e..d2ac51e1c 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 16 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 new file mode 100644 index 000000000..d22a26ab1 --- /dev/null +++ b/Test/pruning/Basic.bpl @@ -0,0 +1,29 @@ +// RUN: %parallel-boogie /prune:2 /errorTrace:0 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +const unique four: int; +const unique ProducerConst: bool uses { + axiom four == 4; +} + +function ConsumerFunc(x: int): int; + +function ProducerFunc(x: int): bool uses { + axiom (forall x: int :: ConsumerFunc(x) == 3); +} + +procedure hasAxioms() + requires ProducerFunc(2); + requires ProducerConst; + ensures ConsumerFunc(4) == 3; + ensures four == 4; +{ + +} + +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 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/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 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