summaryrefslogtreecommitdiff
path: root/Source/Core/Parser.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Core/Parser.cs')
-rw-r--r--Source/Core/Parser.cs4848
1 files changed, 2424 insertions, 2424 deletions
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index 7982f594..1f8d17d6 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -1,2425 +1,2425 @@
-using System.Collections;
-using System.Collections.Generic;
-using System.IO;
-using System.Text;
-using Microsoft.Boogie;
-using Microsoft.Basetypes;
-using Bpl = Microsoft.Boogie;
-
-
-
-
-using System;
-using System.Diagnostics.Contracts;
-
-namespace Microsoft.Boogie {
-
-
-
-public class Parser {
- public const int _EOF = 0;
- public const int _ident = 1;
- public const int _bvlit = 2;
- public const int _digits = 3;
- public const int _string = 4;
- public const int _decimal = 5;
- public const int _float = 6;
- public const int _fp = 97;
- public const int maxT = 98;
-
- const bool T = true;
- const bool x = false;
- const int minErrDist = 2;
-
- public Scanner/*!*/ scanner;
- public Errors/*!*/ errors;
-
- public Token/*!*/ t; // last recognized token
- public Token/*!*/ la; // lookahead token
- int errDist = minErrDist;
-
-readonly Program/*!*/ Pgm;
-
-readonly Expr/*!*/ dummyExpr;
-readonly Cmd/*!*/ dummyCmd;
-readonly Block/*!*/ dummyBlock;
-readonly Bpl.Type/*!*/ dummyType;
-readonly List<Expr>/*!*/ dummyExprSeq;
-readonly TransferCmd/*!*/ dummyTransferCmd;
-readonly StructuredCmd/*!*/ dummyStructuredCmd;
-
-///<summary>
-///Returns the number of parsing errors encountered. If 0, "program" returns as
-///the parsed program.
-///</summary>
-public static int Parse (string/*!*/ filename, /*maybe null*/ List<string/*!*/> defines, out /*maybe null*/ Program program, bool useBaseName=false) /* throws System.IO.IOException */ {
- Contract.Requires(filename != null);
- Contract.Requires(cce.NonNullElements(defines,true));
-
- if (defines == null) {
- defines = new List<string/*!*/>();
- }
-
- if (filename == "stdin.bpl") {
- var s = ParserHelper.Fill(Console.In, defines);
- return Parse(s, filename, out program, useBaseName);
- } else {
- FileStream stream = new FileStream(filename, FileMode.Open, FileAccess.Read, FileShare.Read);
- var s = ParserHelper.Fill(stream, defines);
- var ret = Parse(s, filename, out program, useBaseName);
- stream.Close();
- return ret;
- }
-}
-
-
-public static int Parse (string s, string/*!*/ filename, out /*maybe null*/ Program program, bool useBaseName=false) /* throws System.IO.IOException */ {
- Contract.Requires(s != null);
- Contract.Requires(filename != null);
-
- byte[]/*!*/ buffer = cce.NonNull(UTF8Encoding.Default.GetBytes(s));
- MemoryStream ms = new MemoryStream(buffer,false);
- Errors errors = new Errors();
- Scanner scanner = new Scanner(ms, errors, filename, useBaseName);
-
- Parser parser = new Parser(scanner, errors, false);
- parser.Parse();
- if (parser.errors.count == 0)
- {
- program = parser.Pgm;
- program.ProcessDatatypeConstructors();
- return 0;
- }
- else
- {
- program = null;
- return parser.errors.count;
- }
-}
-
-public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, bool disambiguation)
- : this(scanner, errors)
-{
- // initialize readonly fields
- Pgm = new Program();
- dummyExpr = new LiteralExpr(Token.NoToken, false);
- dummyCmd = new AssumeCmd(Token.NoToken, dummyExpr);
- dummyBlock = new Block(Token.NoToken, "dummyBlock", new List<Cmd>(), new ReturnCmd(Token.NoToken));
- dummyType = new BasicType(Token.NoToken, SimpleType.Bool);
- dummyExprSeq = new List<Expr> ();
- dummyTransferCmd = new ReturnCmd(Token.NoToken);
- dummyStructuredCmd = new BreakCmd(Token.NoToken, null);
-}
-
-// Class to represent the bounds of a bitvector expression t[a:b].
-// Objects of this class only exist during parsing and are directly
-// turned into BvExtract before they get anywhere else
-private class BvBounds : Expr {
- public BigNum Lower;
- public BigNum Upper;
- public BvBounds(IToken/*!*/ tok, BigNum lower, BigNum upper)
- : base(tok, /*immutable=*/ false) {
- Contract.Requires(tok != null);
- this.Lower = lower;
- this.Upper = upper;
- }
- public override Bpl.Type/*!*/ ShallowType { get {Contract.Ensures(Contract.Result<Bpl.Type>() != null); return Bpl.Type.Int; } }
- public override void Resolve(ResolutionContext/*!*/ rc) {
- // Contract.Requires(rc != null);
- rc.Error(this, "bitvector bounds in illegal position");
- }
- public override void Emit(TokenTextWriter/*!*/ stream,
- int contextBindingStrength, bool fragileContext) {
- Contract.Assert(false);throw new cce.UnreachableException();
- }
- public override void ComputeFreeVariables(GSet<object>/*!*/ freeVars) { Contract.Assert(false);throw new cce.UnreachableException(); }
- public override int ComputeHashCode() {
- return base.GetHashCode();
- }
-}
-
-/*--------------------------------------------------------------------------*/
-
-
- public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors) {
- this.scanner = scanner;
- this.errors = errors;
- Token/*!*/ tok = new Token();
- tok.val = "";
- this.la = tok;
- this.t = new Token(); // just to satisfy its non-null constraint
- }
-
- void SynErr (int n) {
- if (errDist >= minErrDist) errors.SynErr(la.filename, la.line, la.col, n);
- errDist = 0;
- }
-
- public void SemErr (string/*!*/ msg) {
- Contract.Requires(msg != null);
- if (errDist >= minErrDist) errors.SemErr(t, msg);
- errDist = 0;
- }
-
- public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {
- Contract.Requires(tok != null);
- Contract.Requires(msg != null);
- errors.SemErr(tok, msg);
- }
-
- void Get () {
- for (;;) {
- t = la;
- la = scanner.Scan();
- if (la.kind <= maxT) { ++errDist; break; }
-
- la = t;
- }
- }
-
- void Expect (int n) {
- if (la.kind==n) Get(); else { SynErr(n); }
- }
-
- bool StartOf (int s) {
- return set[s, la.kind];
- }
-
- void ExpectWeak (int n, int follow) {
- if (la.kind == n) Get();
- else {
- SynErr(n);
- while (!StartOf(follow)) Get();
- }
- }
-
-
- bool WeakSeparator(int n, int syFol, int repFol) {
- int kind = la.kind;
- if (kind == n) {Get(); return true;}
- else if (StartOf(repFol)) {return false;}
- else {
- SynErr(n);
- while (!(set[syFol, kind] || set[repFol, kind] || set[0, kind])) {
- Get();
- kind = la.kind;
- }
- return StartOf(syFol);
- }
- }
-
-
- void BoogiePL() {
- List<Variable>/*!*/ vs;
- List<Declaration>/*!*/ ds;
- Axiom/*!*/ ax;
- List<Declaration/*!*/>/*!*/ ts;
- Procedure/*!*/ pr;
- Implementation im;
- Implementation/*!*/ nnim;
-
- while (StartOf(1)) {
- switch (la.kind) {
- case 21: {
- Consts(out vs);
- foreach(Bpl.Variable/*!*/ v in vs){
- Contract.Assert(v != null);
- Pgm.AddTopLevelDeclaration(v);
- }
-
- break;
- }
- case 25: {
- Function(out ds);
- foreach(Bpl.Declaration/*!*/ d in ds){
- Contract.Assert(d != null);
- Pgm.AddTopLevelDeclaration(d);
- }
-
- break;
- }
- case 29: {
- Axiom(out ax);
- Pgm.AddTopLevelDeclaration(ax);
- break;
- }
- case 30: {
- UserDefinedTypes(out ts);
- foreach(Declaration/*!*/ td in ts){
- Contract.Assert(td != null);
- Pgm.AddTopLevelDeclaration(td);
- }
-
- break;
- }
- case 7: {
- GlobalVars(out vs);
- foreach(Bpl.Variable/*!*/ v in vs){
- Contract.Assert(v != null);
- Pgm.AddTopLevelDeclaration(v);
- }
-
- break;
- }
- case 32: {
- Procedure(out pr, out im);
- Pgm.AddTopLevelDeclaration(pr);
- if (im != null) {
- Pgm.AddTopLevelDeclaration(im);
- }
-
- break;
- }
- case 33: {
- Implementation(out nnim);
- Pgm.AddTopLevelDeclaration(nnim);
- break;
- }
- }
- }
- Expect(0);
- }
-
- void Consts(out List<Variable>/*!*/ ds) {
- Contract.Ensures(Contract.ValueAtReturn(out ds) != null); IToken/*!*/ y; List<TypedIdent>/*!*/ xs;
- ds = new List<Variable>();
- bool u = false; QKeyValue kv = null;
- bool ChildrenComplete = false;
- List<ConstantParent/*!*/> Parents = null;
- Expect(21);
- y = t;
- while (la.kind == 27) {
- Attribute(ref kv);
- }
- if (la.kind == 22) {
- Get();
- u = true;
- }
- IdsType(out xs);
- if (la.kind == 23) {
- OrderSpec(out ChildrenComplete, out Parents);
- }
- bool makeClone = false;
- foreach(TypedIdent/*!*/ x in xs){
- Contract.Assert(x != null);
-
- // ensure that no sharing is introduced
- List<ConstantParent/*!*/> ParentsClone;
- if (makeClone && Parents != null) {
- ParentsClone = new List<ConstantParent/*!*/> ();
- foreach (ConstantParent/*!*/ p in Parents){
- Contract.Assert(p != null);
- ParentsClone.Add(new ConstantParent (
- new IdentifierExpr (p.Parent.tok, p.Parent.Name),
- p.Unique));}
- } else {
- ParentsClone = Parents;
- }
- makeClone = true;
-
- ds.Add(new Constant(y, x, u, ParentsClone, ChildrenComplete, kv));
- }
-
- Expect(8);
- }
-
- void Function(out List<Declaration>/*!*/ ds) {
- Contract.Ensures(Contract.ValueAtReturn(out ds) != null);
- ds = new List<Declaration>(); IToken/*!*/ z;
- IToken/*!*/ typeParamTok;
- var typeParams = new List<TypeVariable>();
- var arguments = new List<Variable>();
- TypedIdent/*!*/ tyd;
- TypedIdent retTyd = null;
- Bpl.Type/*!*/ retTy;
- QKeyValue argKv = null;
- QKeyValue kv = null;
- Expr definition = null;
- Expr/*!*/ tmp;
-
- Expect(25);
- while (la.kind == 27) {
- Attribute(ref kv);
- }
- Ident(out z);
- if (la.kind == 19) {
- TypeParams(out typeParamTok, out typeParams);
- }
- Expect(9);
- if (StartOf(2)) {
- VarOrType(out tyd, out argKv);
- arguments.Add(new Formal(tyd.tok, tyd, true, argKv));
- while (la.kind == 12) {
- Get();
- VarOrType(out tyd, out argKv);
- arguments.Add(new Formal(tyd.tok, tyd, true, argKv));
- }
- }
- Expect(10);
- argKv = null;
- if (la.kind == 26) {
- Get();
- Expect(9);
- VarOrType(out retTyd, out argKv);
- Expect(10);
- } else if (la.kind == 11) {
- Get();
- Type(out retTy);
- retTyd = new TypedIdent(retTy.tok, TypedIdent.NoName, retTy);
- } else SynErr(99);
- if (la.kind == 27) {
- Get();
- Expression(out tmp);
- definition = tmp;
- Expect(28);
- } else if (la.kind == 8) {
- Get();
- } else SynErr(100);
- 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);
- Contract.Assert(func != null);
- ds.Add(func);
- bool allUnnamed = true;
- foreach(Formal/*!*/ f in arguments){
- Contract.Assert(f != null);
- if (f.TypedIdent.HasName) {
- allUnnamed = false;
- break;
- }
- }
- if (!allUnnamed) {
- Bpl.Type prevType = null;
- for (int i = arguments.Count; 0 <= --i; ) {
- TypedIdent/*!*/ curr = cce.NonNull(arguments[i]).TypedIdent;
- if (curr.HasName) {
- // the argument was given as both an identifier and a type
- prevType = curr.Type;
- } else {
- // the argument was given as just one "thing", which syntactically parsed as a type
- if (prevType == null) {
- this.errors.SemErr(curr.tok, "the type of the last parameter is unspecified");
- break;
- }
- Bpl.Type ty = curr.Type;
- var uti = ty as UnresolvedTypeIdentifier;
- if (uti != null && uti.Arguments.Count == 0) {
- // the given "thing" was just an identifier, so let's use it as the name of the parameter
- curr.Name = uti.Name;
- curr.Type = prevType;
- } else {
- this.errors.SemErr(curr.tok, "expecting an identifier as parameter name");
- }
- }
- }
- }
- if (definition != null) {
- // generate either an axiom or a function body
- if (QKeyValue.FindBoolAttribute(kv, "inline")) {
- func.Body = definition;
- } else {
- ds.Add(func.CreateDefinitionAxiom(definition, kv));
- }
- }
-
- }
-
- void Axiom(out Axiom/*!*/ m) {
- Contract.Ensures(Contract.ValueAtReturn(out m) != null); Expr/*!*/ e; QKeyValue kv = null;
- Expect(29);
- while (la.kind == 27) {
- Attribute(ref kv);
- }
- IToken/*!*/ x = t;
- Proposition(out e);
- Expect(8);
- m = new Axiom(x,e, null, kv);
- }
-
- void UserDefinedTypes(out List<Declaration/*!*/>/*!*/ ts) {
- Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out ts))); Declaration/*!*/ decl; QKeyValue kv = null; ts = new List<Declaration/*!*/> ();
- Expect(30);
- while (la.kind == 27) {
- Attribute(ref kv);
- }
- UserDefinedType(out decl, kv);
- ts.Add(decl);
- while (la.kind == 12) {
- Get();
- UserDefinedType(out decl, kv);
- ts.Add(decl);
- }
- Expect(8);
- }
-
- void GlobalVars(out List<Variable>/*!*/ ds) {
- Contract.Ensures(Contract.ValueAtReturn(out ds) != null);
- QKeyValue kv = null;
- ds = new List<Variable>();
- var dsx = ds;
-
- Expect(7);
- while (la.kind == 27) {
- Attribute(ref kv);
- }
- IdsTypeWheres(true, "global variables", delegate(TypedIdent tyd) { dsx.Add(new GlobalVariable(tyd.tok, tyd, kv)); } );
- Expect(8);
- }
-
- void Procedure(out Procedure/*!*/ proc, out /*maybe null*/ Implementation impl) {
- Contract.Ensures(Contract.ValueAtReturn(out proc) != null); IToken/*!*/ x;
- List<TypeVariable>/*!*/ typeParams;
- List<Variable>/*!*/ ins, outs;
- List<Requires>/*!*/ pre = new List<Requires>();
- List<IdentifierExpr>/*!*/ mods = new List<IdentifierExpr>();
- List<Ensures>/*!*/ post = new List<Ensures>();
-
- List<Variable>/*!*/ locals = new List<Variable>();
- StmtList/*!*/ stmtList;
- QKeyValue kv = null;
- impl = null;
-
- Expect(32);
- ProcSignature(true, out x, out typeParams, out ins, out outs, out kv);
- if (la.kind == 8) {
- Get();
- while (StartOf(3)) {
- Spec(pre, mods, post);
- }
- } else if (StartOf(4)) {
- while (StartOf(3)) {
- Spec(pre, mods, post);
- }
- ImplBody(out locals, out stmtList);
- impl = new Implementation(x, x.val, typeParams,
- Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, kv == null ? null : (QKeyValue)kv.Clone(), this.errors);
-
- } else SynErr(99);
- proc = new Procedure(x, x.val, typeParams, ins, outs, pre, mods, post, kv);
- }
-
- void Implementation(out Implementation/*!*/ impl) {
- Contract.Ensures(Contract.ValueAtReturn(out impl) != null); IToken/*!*/ x;
- List<TypeVariable>/*!*/ typeParams;
- List<Variable>/*!*/ ins, outs;
- List<Variable>/*!*/ locals;
- StmtList/*!*/ stmtList;
- QKeyValue kv;
-
- Expect(33);
- 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);
- }
-
- void Attribute(ref QKeyValue kv) {
- Trigger trig = null;
- AttributeOrTrigger(ref kv, ref trig);
- if (trig != null) this.SemErr("only attributes, not triggers, allowed here");
- }
-
- void IdsTypeWheres(bool allowWhereClauses, string context, System.Action<TypedIdent> action ) {
- IdsTypeWhere(allowWhereClauses, context, action);
- while (la.kind == 12) {
- Get();
- IdsTypeWhere(allowWhereClauses, context, action);
- }
- }
-
- void LocalVars(List<Variable>/*!*/ ds) {
- Contract.Ensures(Contract.ValueAtReturn(out ds) != null);
- QKeyValue kv = null;
-
- Expect(7);
- while (la.kind == 27) {
- Attribute(ref kv);
- }
- IdsTypeWheres(true, "local variables", delegate(TypedIdent tyd) { ds.Add(new LocalVariable(tyd.tok, tyd, kv)); } );
- Expect(8);
- }
-
- void ProcFormals(bool incoming, bool allowWhereClauses, out List<Variable>/*!*/ ds) {
- Contract.Ensures(Contract.ValueAtReturn(out ds) != null);
- ds = new List<Variable>();
- var dsx = ds;
- var context = allowWhereClauses ? "procedure formals" : "the 'implementation' copies of formals";
-
- Expect(9);
- if (la.kind == 1 || la.kind == 27) {
- AttrsIdsTypeWheres(allowWhereClauses, allowWhereClauses, context, delegate(TypedIdent tyd, QKeyValue kv) { dsx.Add(new Formal(tyd.tok, tyd, incoming, kv)); });
- }
- Expect(10);
- }
-
- void AttrsIdsTypeWheres(bool allowAttributes, bool allowWhereClauses, string context, System.Action<TypedIdent, QKeyValue> action ) {
- AttributesIdsTypeWhere(allowAttributes, allowWhereClauses, context, action);
- while (la.kind == 12) {
- Get();
- AttributesIdsTypeWhere(allowAttributes, allowWhereClauses, context, action);
- }
- }
-
- void BoundVars(IToken/*!*/ x, out List<Variable>/*!*/ ds) {
- Contract.Requires(x != null);
- Contract.Ensures(Contract.ValueAtReturn(out ds) != null);
- List<TypedIdent>/*!*/ tyds = new List<TypedIdent>();
- ds = new List<Variable>();
- var dsx = ds;
-
- AttrsIdsTypeWheres(true, false, "bound variables", delegate(TypedIdent tyd, QKeyValue kv) { dsx.Add(new BoundVariable(tyd.tok, tyd, kv)); } );
- }
-
- void IdsType(out List<TypedIdent>/*!*/ tyds) {
- Contract.Ensures(Contract.ValueAtReturn(out tyds) != null); List<IToken>/*!*/ ids; Bpl.Type/*!*/ ty;
- Idents(out ids);
- Expect(11);
- Type(out ty);
- tyds = new List<TypedIdent>();
- foreach(Token/*!*/ id in ids){
- Contract.Assert(id != null);
- tyds.Add(new TypedIdent(id, id.val, ty, null));
- }
-
- }
-
- void Idents(out List<IToken>/*!*/ xs) {
- Contract.Ensures(Contract.ValueAtReturn(out xs) != null); IToken/*!*/ id; xs = new List<IToken>();
- Ident(out id);
- xs.Add(id);
- while (la.kind == 12) {
- Get();
- Ident(out id);
- xs.Add(id);
- }
- }
-
- void Type(out Bpl.Type/*!*/ ty) {
- Contract.Ensures(Contract.ValueAtReturn(out ty) != null); IToken/*!*/ tok; ty = dummyType;
- if (StartOf(5)) {
- TypeAtom(out ty);
- } else if (la.kind == 1) {
- Ident(out tok);
- List<Bpl.Type>/*!*/ args = new List<Bpl.Type> ();
- if (StartOf(6)) {
- TypeArgs(args);
- }
- ty = new UnresolvedTypeIdentifier (tok, tok.val, args);
- } else if (la.kind == 17 || la.kind == 19) {
- MapType(out ty);
- } else SynErr(100);
- }
-
- void AttributesIdsTypeWhere(bool allowAttributes, bool allowWhereClauses, string context, System.Action<TypedIdent, QKeyValue> action ) {
- QKeyValue kv = null;
- while (la.kind == 27) {
- Attribute(ref kv);
- if (!allowAttributes) {
- kv = null;
- this.SemErr("attributes are not allowed on " + context);
- }
-
- }
- IdsTypeWhere(allowWhereClauses, context, delegate(TypedIdent tyd) { action(tyd, kv); });
- }
-
- void IdsTypeWhere(bool allowWhereClauses, string context, System.Action<TypedIdent> action ) {
- List<IToken>/*!*/ ids; Bpl.Type/*!*/ ty; Expr wh = null; Expr/*!*/ nne;
- Idents(out ids);
- Expect(11);
- Type(out ty);
- if (la.kind == 13) {
- Get();
- Expression(out nne);
- if (!allowWhereClauses) {
- this.SemErr("where clause not allowed on " + context);
- } else {
- wh = nne;
- }
-
- }
- foreach(Token/*!*/ id in ids){
- Contract.Assert(id != null);
- action(new TypedIdent(id, id.val, ty, wh));
- }
-
- }
-
- void Expression(out Expr/*!*/ e0) {
- Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1;
- ImpliesExpression(false, out e0);
- while (la.kind == 55 || la.kind == 56) {
- EquivOp();
- x = t;
- ImpliesExpression(false, out e1);
- e0 = Expr.Binary(x, BinaryOperator.Opcode.Iff, e0, e1);
- }
- }
-
- void TypeAtom(out Bpl.Type/*!*/ ty) {
- Contract.Ensures(Contract.ValueAtReturn(out ty) != null); ty = dummyType;
- if (la.kind == 14) {
- Get();
- ty = new BasicType(t, SimpleType.Int);
- } else if (la.kind == 15) {
- Get();
- ty = new BasicType(t, SimpleType.Real);
- } else if (la.kind == 98) {
- Get();
- ty = FType();
- } else if (la.kind == 16) {
- Get();
- ty = new BasicType(t, SimpleType.Bool);
- } else if (la.kind == 9) {
- Get();
- Type(out ty);
- Expect(10);
- } else SynErr(101);
- }
-
- FloatType FType() {
- if (t.val.Length > 5) {
- switch (Int32.Parse(t.val.Substring(5))) {
- case 16:
- return new FloatType(t, 5, 11);
- case 32:
- return new FloatType(t, 8, 24);
- case 64:
- return new FloatType(t, 11, 53);
- case 128:
- return new FloatType(t, 15, 113);
- default:
- SynErr(3);
- return new FloatType(t, 0, 0);
- }
- }
- else {
- try {
- Expect(19); //<
- Expect(3); //int
- int exp = Int32.Parse(t.val);
- Expect(12); //,
- Expect(3); //int
- int man = Int32.Parse(t.val);
- Expect(20); //>
- return new FloatType(t, exp, man);
- }
- catch (Exception) {
- return new FloatType(t, 0, 0);
- }
- }
- }
-
- void Ident(out IToken/*!*/ x) {
- Contract.Ensures(Contract.ValueAtReturn(out x) != null);
- Expect(1);
- x = t;
- if (x.val.StartsWith("\\"))
- x.val = x.val.Substring(1);
-
- }
-
- void TypeArgs(List<Bpl.Type>/*!*/ ts) {
- Contract.Requires(ts != null); IToken/*!*/ tok; Bpl.Type/*!*/ ty;
- if (StartOf(5)) {
- TypeAtom(out ty);
- ts.Add(ty);
- if (StartOf(6)) {
- TypeArgs(ts);
- }
- } else if (la.kind == 1) {
- Ident(out tok);
- List<Bpl.Type>/*!*/ args = new List<Bpl.Type> ();
- ts.Add(new UnresolvedTypeIdentifier (tok, tok.val, args));
- if (StartOf(6)) {
- TypeArgs(ts);
- }
- } else if (la.kind == 17 || la.kind == 19) {
- MapType(out ty);
- ts.Add(ty);
- } else SynErr(102);
- }
-
- void MapType(out Bpl.Type/*!*/ ty) {
- Contract.Ensures(Contract.ValueAtReturn(out ty) != null); IToken tok = null;
- IToken/*!*/ nnTok;
- List<Bpl.Type>/*!*/ arguments = new List<Bpl.Type>();
- Bpl.Type/*!*/ result;
- List<TypeVariable>/*!*/ typeParameters = new List<TypeVariable>();
-
- if (la.kind == 19) {
- TypeParams(out nnTok, out typeParameters);
- tok = nnTok;
- }
- Expect(17);
- if (tok == null) tok = t;
- if (StartOf(6)) {
- Types(arguments);
- }
- Expect(18);
- Type(out result);
- ty = new MapType(tok, typeParameters, arguments, result);
-
- }
-
- void TypeParams(out IToken/*!*/ tok, out List<TypeVariable>/*!*/ typeParams) {
- Contract.Ensures(Contract.ValueAtReturn(out tok) != null); Contract.Ensures(Contract.ValueAtReturn(out typeParams) != null); List<IToken>/*!*/ typeParamToks;
- Expect(19);
- tok = t;
- Idents(out typeParamToks);
- Expect(20);
- typeParams = new List<TypeVariable> ();
- foreach(Token/*!*/ id in typeParamToks){
- Contract.Assert(id != null);
- typeParams.Add(new TypeVariable(id, id.val));}
-
- }
-
- void Types(List<Bpl.Type>/*!*/ ts) {
- Contract.Requires(ts != null); Bpl.Type/*!*/ ty;
- Type(out ty);
- ts.Add(ty);
- while (la.kind == 12) {
- Get();
- Type(out ty);
- ts.Add(ty);
- }
- }
-
- void OrderSpec(out bool ChildrenComplete, out List<ConstantParent/*!*/> Parents) {
- Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out Parents),true)); ChildrenComplete = false;
- Parents = null;
- bool u;
- IToken/*!*/ parent;
- Expect(23);
- Parents = new List<ConstantParent/*!*/> ();
- u = false;
- if (la.kind == 1 || la.kind == 22) {
- if (la.kind == 22) {
- Get();
- u = true;
- }
- Ident(out parent);
- Parents.Add(new ConstantParent (
- new IdentifierExpr(parent, parent.val), u));
- while (la.kind == 12) {
- Get();
- u = false;
- if (la.kind == 22) {
- Get();
- u = true;
- }
- Ident(out parent);
- Parents.Add(new ConstantParent (
- new IdentifierExpr(parent, parent.val), u));
- }
- }
- if (la.kind == 24) {
- Get();
- ChildrenComplete = true;
- }
- }
-
- void VarOrType(out TypedIdent/*!*/ tyd, out QKeyValue kv) {
- Contract.Ensures(Contract.ValueAtReturn(out tyd) != null);
- string/*!*/ varName = TypedIdent.NoName;
- Bpl.Type/*!*/ ty;
- IToken/*!*/ tok;
- kv = null;
-
- while (la.kind == 27) {
- Attribute(ref kv);
- }
- Type(out ty);
- tok = ty.tok;
- if (la.kind == 11) {
- Get();
- var uti = ty as UnresolvedTypeIdentifier;
- if (uti != null && uti.Arguments.Count == 0) {
- varName = uti.Name;
- } else {
- this.SemErr("expected identifier before ':'");
- }
-
- Type(out ty);
- }
- tyd = new TypedIdent(tok, varName, ty);
- }
-
- void Proposition(out Expr/*!*/ e) {
- Contract.Ensures(Contract.ValueAtReturn(out e) != null);
- Expression(out e);
- }
-
- void UserDefinedType(out Declaration/*!*/ decl, QKeyValue kv) {
- Contract.Ensures(Contract.ValueAtReturn(out decl) != null); IToken/*!*/ id; List<IToken>/*!*/ paramTokens = new List<IToken> ();
- Bpl.Type/*!*/ body = dummyType; bool synonym = false;
- Ident(out id);
- if (la.kind == 1) {
- WhiteSpaceIdents(out paramTokens);
- }
- if (la.kind == 31) {
- Get();
- Type(out body);
- synonym = true;
- }
- if (synonym) {
- List<TypeVariable>/*!*/ typeParams = new List<TypeVariable>();
- foreach(Token/*!*/ t in paramTokens){
- Contract.Assert(t != null);
- typeParams.Add(new TypeVariable(t, t.val));}
- decl = new TypeSynonymDecl(id, id.val, typeParams, body, kv);
- } else {
- decl = new TypeCtorDecl(id, id.val, paramTokens.Count, kv);
- }
-
- }
-
- void WhiteSpaceIdents(out List<IToken>/*!*/ xs) {
- Contract.Ensures(Contract.ValueAtReturn(out xs) != null); IToken/*!*/ id; xs = new List<IToken>();
- Ident(out id);
- xs.Add(id);
- while (la.kind == 1) {
- Ident(out id);
- xs.Add(id);
- }
- }
-
- void ProcSignature(bool allowWhereClausesOnFormals, out IToken/*!*/ name, out List<TypeVariable>/*!*/ typeParams,
-out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
- 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<TypeVariable>();
- outs = new List<Variable>(); kv = null;
- while (la.kind == 27) {
- Attribute(ref kv);
- }
- Ident(out name);
- if (la.kind == 19) {
- TypeParams(out typeParamTok, out typeParams);
- }
- ProcFormals(true, allowWhereClausesOnFormals, out ins);
- if (la.kind == 26) {
- Get();
- ProcFormals(false, allowWhereClausesOnFormals, out outs);
- }
- }
-
- void Spec(List<Requires>/*!*/ pre, List<IdentifierExpr>/*!*/ mods, List<Ensures>/*!*/ post) {
- Contract.Requires(pre != null); Contract.Requires(mods != null); Contract.Requires(post != null); List<IToken>/*!*/ ms;
- if (la.kind == 34) {
- Get();
- if (la.kind == 1) {
- Idents(out ms);
- foreach(IToken/*!*/ m in ms){
- Contract.Assert(m != null);
- mods.Add(new IdentifierExpr(m, m.val));
- }
-
- }
- Expect(8);
- } else if (la.kind == 35) {
- Get();
- SpecPrePost(true, pre, post);
- } else if (la.kind == 36 || la.kind == 37) {
- SpecPrePost(false, pre, post);
- } else SynErr(103);
- }
-
- void ImplBody(out List<Variable>/*!*/ locals, out StmtList/*!*/ stmtList) {
- Contract.Ensures(Contract.ValueAtReturn(out locals) != null); Contract.Ensures(Contract.ValueAtReturn(out stmtList) != null); locals = new List<Variable>();
- Expect(27);
- while (la.kind == 7) {
- LocalVars(locals);
- }
- StmtList(out stmtList);
- }
-
- void SpecPrePost(bool free, List<Requires>/*!*/ pre, List<Ensures>/*!*/ post) {
- Contract.Requires(pre != null); Contract.Requires(post != null); Expr/*!*/ e; Token tok = null; QKeyValue kv = null;
- if (la.kind == 36) {
- Get();
- tok = t;
- while (la.kind == 27) {
- Attribute(ref kv);
- }
- Proposition(out e);
- Expect(8);
- pre.Add(new Requires(tok, free, e, null, kv));
- } else if (la.kind == 37) {
- Get();
- tok = t;
- while (la.kind == 27) {
- Attribute(ref kv);
- }
- Proposition(out e);
- Expect(8);
- post.Add(new Ensures(tok, free, e, null, kv));
- } else SynErr(104);
- }
-
- void StmtList(out StmtList/*!*/ stmtList) {
- Contract.Ensures(Contract.ValueAtReturn(out stmtList) != null); List<BigBlock/*!*/> bigblocks = new List<BigBlock/*!*/>();
- /* built-up state for the current BigBlock: */
- IToken startToken = null; string currentLabel = null;
- List<Cmd> cs = null; /* invariant: startToken != null ==> cs != null */
- /* temporary variables: */
- IToken label; Cmd c; BigBlock b;
- StructuredCmd ec = null; StructuredCmd/*!*/ ecn;
- TransferCmd tc = null; TransferCmd/*!*/ tcn;
-
- while (StartOf(7)) {
- if (StartOf(8)) {
- LabelOrCmd(out c, out label);
- if (c != null) {
- // LabelOrCmd read a Cmd
- Contract.Assert(label == null);
- if (startToken == null) { startToken = c.tok; cs = new List<Cmd>(); }
- Contract.Assert(cs != null);
- cs.Add(c);
- } else {
- // LabelOrCmd read a label
- Contract.Assert(label != null);
- if (startToken != null) {
- Contract.Assert(cs != null);
- // dump the built-up state into a BigBlock
- b = new BigBlock(startToken, currentLabel, cs, null, null);
- bigblocks.Add(b);
- cs = null;
- }
- startToken = label;
- currentLabel = label.val;
- cs = new List<Cmd>();
- }
-
- } else if (la.kind == 40 || la.kind == 42 || la.kind == 45) {
- StructuredCmd(out ecn);
- ec = ecn;
- if (startToken == null) { startToken = ec.tok; cs = new List<Cmd>(); }
- Contract.Assert(cs != null);
- b = new BigBlock(startToken, currentLabel, cs, ec, null);
- bigblocks.Add(b);
- startToken = null; currentLabel = null; cs = null;
-
- } else {
- TransferCmd(out tcn);
- tc = tcn;
- if (startToken == null) { startToken = tc.tok; cs = new List<Cmd>(); }
- Contract.Assert(cs != null);
- b = new BigBlock(startToken, currentLabel, cs, null, tc);
- bigblocks.Add(b);
- startToken = null; currentLabel = null; cs = null;
-
- }
- }
- Expect(28);
- IToken/*!*/ endCurly = t;
- if (startToken == null && bigblocks.Count == 0) {
- startToken = t; cs = new List<Cmd>();
- }
- if (startToken != null) {
- Contract.Assert(cs != null);
- b = new BigBlock(startToken, currentLabel, cs, null, null);
- bigblocks.Add(b);
- }
-
- stmtList = new StmtList(bigblocks, endCurly);
-
- }
-
- void LabelOrCmd(out Cmd c, out IToken label) {
- IToken/*!*/ x; Expr/*!*/ e;
- List<IToken>/*!*/ xs;
- List<IdentifierExpr> ids;
- c = dummyCmd; label = null;
- Cmd/*!*/ cn;
- QKeyValue kv = null;
-
- switch (la.kind) {
- case 1: {
- LabelOrAssign(out c, out label);
- break;
- }
- case 46: {
- Get();
- x = t;
- while (la.kind == 27) {
- Attribute(ref kv);
- }
- Proposition(out e);
- c = new AssertCmd(x, e, kv);
- Expect(8);
- break;
- }
- case 47: {
- Get();
- x = t;
- while (la.kind == 27) {
- Attribute(ref kv);
- }
- Proposition(out e);
- c = new AssumeCmd(x, e, kv);
- Expect(8);
- break;
- }
- case 48: {
- Get();
- x = t;
- Idents(out xs);
- Expect(8);
- ids = new List<IdentifierExpr>();
- foreach(IToken/*!*/ y in xs){
- Contract.Assert(y != null);
- ids.Add(new IdentifierExpr(y, y.val));
- }
- c = new HavocCmd(x,ids);
-
- break;
- }
- case 35: case 51: case 52: {
- CallCmd(out cn);
- Expect(8);
- c = cn;
- break;
- }
- case 53: {
- ParCallCmd(out cn);
- c = cn;
- break;
- }
- case 49: {
- Get();
- x = t;
- Expect(8);
- c = new YieldCmd(x);
- break;
- }
- default: SynErr(105); break;
- }
- }
-
- 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 == 40) {
- IfCmd(out ifcmd);
- ec = ifcmd;
- } else if (la.kind == 42) {
- WhileCmd(out wcmd);
- ec = wcmd;
- } else if (la.kind == 45) {
- BreakCmd(out bcmd);
- ec = bcmd;
- } else SynErr(106);
- }
-
- void TransferCmd(out TransferCmd/*!*/ tc) {
- Contract.Ensures(Contract.ValueAtReturn(out tc) != null); tc = dummyTransferCmd;
- Token y; List<IToken>/*!*/ xs;
- List<String> ss = new List<String>();
-
- if (la.kind == 38) {
- Get();
- y = t;
- Idents(out xs);
- foreach(IToken/*!*/ s in xs){
- Contract.Assert(s != null);
- ss.Add(s.val); }
- tc = new GotoCmd(y, ss);
-
- } else if (la.kind == 39) {
- Get();
- tc = new ReturnCmd(t);
- } else SynErr(107);
- Expect(8);
- }
-
- void IfCmd(out IfCmd/*!*/ ifcmd) {
- Contract.Ensures(Contract.ValueAtReturn(out ifcmd) != null); IToken/*!*/ x;
- Expr guard;
- StmtList/*!*/ thn;
- IfCmd/*!*/ elseIf; IfCmd elseIfOption = null;
- StmtList/*!*/ els; StmtList elseOption = null;
-
- Expect(40);
- x = t;
- Guard(out guard);
- Expect(27);
- StmtList(out thn);
- if (la.kind == 41) {
- Get();
- if (la.kind == 40) {
- IfCmd(out elseIf);
- elseIfOption = elseIf;
- } else if (la.kind == 27) {
- Get();
- StmtList(out els);
- elseOption = els;
- } else SynErr(108);
- }
- ifcmd = new IfCmd(x, guard, thn, elseIfOption, elseOption);
- }
-
- void WhileCmd(out WhileCmd/*!*/ wcmd) {
- Contract.Ensures(Contract.ValueAtReturn(out wcmd) != null); IToken/*!*/ x; Token z;
- Expr guard; Expr/*!*/ e; bool isFree;
- List<PredicateCmd/*!*/> invariants = new List<PredicateCmd/*!*/>();
- StmtList/*!*/ body;
- QKeyValue kv = null;
-
- Expect(42);
- x = t;
- Guard(out guard);
- Contract.Assume(guard == null || cce.Owner.None(guard));
- while (la.kind == 35 || la.kind == 43) {
- isFree = false; z = la/*lookahead token*/;
- if (la.kind == 35) {
- Get();
- isFree = true;
- }
- Expect(43);
- while (la.kind == 27) {
- Attribute(ref kv);
- }
- Expression(out e);
- if (isFree) {
- invariants.Add(new AssumeCmd(z, e, kv));
- } else {
- invariants.Add(new AssertCmd(z, e, kv));
- }
- kv = null;
-
- Expect(8);
- }
- Expect(27);
- StmtList(out body);
- wcmd = new WhileCmd(x, guard, invariants, body);
- }
-
- void BreakCmd(out BreakCmd/*!*/ bcmd) {
- Contract.Ensures(Contract.ValueAtReturn(out bcmd) != null); IToken/*!*/ x; IToken/*!*/ y;
- string breakLabel = null;
-
- Expect(45);
- x = t;
- if (la.kind == 1) {
- Ident(out y);
- breakLabel = y.val;
- }
- Expect(8);
- bcmd = new BreakCmd(x, breakLabel);
- }
-
- void Guard(out Expr e) {
- Expr/*!*/ ee; e = null;
- Expect(9);
- if (la.kind == 44) {
- Get();
- e = null;
- } else if (StartOf(9)) {
- Expression(out ee);
- e = ee;
- } else SynErr(109);
- Expect(10);
- }
-
- void LabelOrAssign(out Cmd c, out IToken label) {
- IToken/*!*/ id; IToken/*!*/ x, y; Expr/*!*/ e0;
- c = dummyCmd; label = null;
- AssignLhs/*!*/ lhs;
- List<AssignLhs/*!*/>/*!*/ lhss;
- List<Expr/*!*/>/*!*/ rhss;
- List<Expr/*!*/>/*!*/ indexes;
-
- Ident(out id);
- x = t;
- if (la.kind == 11) {
- Get();
- c = null; label = x;
- } else if (la.kind == 12 || la.kind == 17 || la.kind == 50) {
- lhss = new List<AssignLhs/*!*/>();
- lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val));
- while (la.kind == 17) {
- MapAssignIndex(out y, out indexes);
- lhs = new MapAssignLhs(y, lhs, indexes);
- }
- lhss.Add(lhs);
- while (la.kind == 12) {
- Get();
- Ident(out id);
- lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val));
- while (la.kind == 17) {
- MapAssignIndex(out y, out indexes);
- lhs = new MapAssignLhs(y, lhs, indexes);
- }
- lhss.Add(lhs);
- }
- Expect(50);
- x = t; /* use location of := */
- Expression(out e0);
- rhss = new List<Expr/*!*/> ();
- rhss.Add(e0);
- while (la.kind == 12) {
- Get();
- Expression(out e0);
- rhss.Add(e0);
- }
- Expect(8);
- c = new AssignCmd(x, lhss, rhss);
- } else SynErr(110);
- }
-
- void CallCmd(out Cmd c) {
- Contract.Ensures(Contract.ValueAtReturn(out c) != null);
- IToken x;
- bool isAsync = false;
- bool isFree = false;
- QKeyValue kv = null;
- c = null;
-
- if (la.kind == 51) {
- Get();
- isAsync = true;
- }
- if (la.kind == 35) {
- Get();
- isFree = true;
- }
- Expect(52);
- x = t;
- while (la.kind == 27) {
- Attribute(ref kv);
- }
- CallParams(isAsync, isFree, kv, x, out c);
-
- }
-
- void ParCallCmd(out Cmd d) {
- Contract.Ensures(Contract.ValueAtReturn(out d) != null);
- IToken x;
- QKeyValue kv = null;
- Cmd c = null;
- List<CallCmd> callCmds = new List<CallCmd>();
-
- Expect(53);
- x = t;
- while (la.kind == 27) {
- Attribute(ref kv);
- }
- CallParams(false, false, kv, x, out c);
- callCmds.Add((CallCmd)c);
- while (la.kind == 54) {
- Get();
- CallParams(false, false, kv, x, out c);
- callCmds.Add((CallCmd)c);
- }
- Expect(8);
- d = new ParCallCmd(x, callCmds, kv);
- }
-
- void MapAssignIndex(out IToken/*!*/ x, out List<Expr/*!*/>/*!*/ indexes) {
- Contract.Ensures(Contract.ValueAtReturn(out x) != null); Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out indexes))); indexes = new List<Expr/*!*/> ();
- Expr/*!*/ e;
-
- Expect(17);
- x = t;
- if (StartOf(9)) {
- Expression(out e);
- indexes.Add(e);
- while (la.kind == 12) {
- Get();
- Expression(out e);
- indexes.Add(e);
- }
- }
- Expect(18);
- }
-
- void CallParams(bool isAsync, bool isFree, QKeyValue kv, IToken x, out Cmd c) {
- List<IdentifierExpr> ids = new List<IdentifierExpr>();
- List<Expr> es = new List<Expr>();
- Expr en;
- IToken first;
- IToken p;
- c = null;
-
- Ident(out first);
- if (la.kind == 9) {
- Get();
- if (StartOf(9)) {
- Expression(out en);
- es.Add(en);
- while (la.kind == 12) {
- Get();
- Expression(out en);
- es.Add(en);
- }
- }
- Expect(10);
- c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync;
- } else if (la.kind == 12 || la.kind == 50) {
- ids.Add(new IdentifierExpr(first, first.val));
- if (la.kind == 12) {
- Get();
- Ident(out p);
- ids.Add(new IdentifierExpr(p, p.val));
- while (la.kind == 12) {
- Get();
- Ident(out p);
- ids.Add(new IdentifierExpr(p, p.val));
- }
- }
- Expect(50);
- Ident(out first);
- Expect(9);
- if (StartOf(9)) {
- Expression(out en);
- es.Add(en);
- while (la.kind == 12) {
- Get();
- Expression(out en);
- es.Add(en);
- }
- }
- Expect(10);
- c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync;
- } else SynErr(111);
- }
-
- void Expressions(out List<Expr>/*!*/ es) {
- Contract.Ensures(Contract.ValueAtReturn(out es) != null); Expr/*!*/ e; es = new List<Expr>();
- Expression(out e);
- es.Add(e);
- while (la.kind == 12) {
- Get();
- Expression(out e);
- es.Add(e);
- }
- }
-
- 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 == 57 || la.kind == 58) {
- ImpliesOp();
- x = t;
- ImpliesExpression(true, out e1);
- e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e0, e1);
- } else {
- ExpliesOp();
- if (noExplies)
- this.SemErr("illegal mixture of ==> and <==, use parentheses to disambiguate");
- x = t;
- LogicalExpression(out e1);
- e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e1, e0);
- while (la.kind == 59 || la.kind == 60) {
- ExpliesOp();
- x = t;
- LogicalExpression(out e1);
- e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e1, e0);
- }
- }
- }
- }
-
- void EquivOp() {
- if (la.kind == 55) {
- Get();
- } else if (la.kind == 56) {
- Get();
- } else SynErr(112);
- }
-
- 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 == 61 || la.kind == 62) {
- AndOp();
- x = t;
- RelationalExpression(out e1);
- e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1);
- while (la.kind == 61 || la.kind == 62) {
- AndOp();
- x = t;
- RelationalExpression(out e1);
- e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1);
- }
- } else {
- OrOp();
- x = t;
- RelationalExpression(out e1);
- e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1);
- while (la.kind == 63 || la.kind == 64) {
- OrOp();
- x = t;
- RelationalExpression(out e1);
- e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1);
- }
- }
- }
- }
-
- void ImpliesOp() {
- if (la.kind == 57) {
- Get();
- } else if (la.kind == 58) {
- Get();
- } else SynErr(113);
- }
-
- void ExpliesOp() {
- if (la.kind == 59) {
- Get();
- } else if (la.kind == 60) {
- Get();
- } else SynErr(114);
- }
-
- void RelationalExpression(out Expr/*!*/ e0) {
- Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; BinaryOperator.Opcode op;
- BvTerm(out e0);
- if (StartOf(12)) {
- RelOp(out x, out op);
- BvTerm(out e1);
- e0 = Expr.Binary(x, op, e0, e1);
- }
- }
-
- void AndOp() {
- if (la.kind == 61) {
- Get();
- } else if (la.kind == 62) {
- Get();
- } else SynErr(115);
- }
-
- void OrOp() {
- if (la.kind == 63) {
- Get();
- } else if (la.kind == 64) {
- Get();
- } else SynErr(116);
- }
-
- void BvTerm(out Expr/*!*/ e0) {
- Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1;
- Term(out e0);
- while (la.kind == 73) {
- Get();
- x = t;
- Term(out e1);
- e0 = new BvConcatExpr(x, e0, e1);
- }
- }
-
- 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 65: {
- Get();
- x = t; op=BinaryOperator.Opcode.Eq;
- break;
- }
- case 19: {
- Get();
- x = t; op=BinaryOperator.Opcode.Lt;
- break;
- }
- case 20: {
- Get();
- x = t; op=BinaryOperator.Opcode.Gt;
- break;
- }
- case 66: {
- Get();
- x = t; op=BinaryOperator.Opcode.Le;
- break;
- }
- case 67: {
- Get();
- x = t; op=BinaryOperator.Opcode.Ge;
- break;
- }
- case 68: {
- Get();
- x = t; op=BinaryOperator.Opcode.Neq;
- break;
- }
- case 69: {
- Get();
- x = t; op=BinaryOperator.Opcode.Subtype;
- break;
- }
- case 70: {
- Get();
- x = t; op=BinaryOperator.Opcode.Neq;
- break;
- }
- case 71: {
- Get();
- x = t; op=BinaryOperator.Opcode.Le;
- break;
- }
- case 72: {
- Get();
- x = t; op=BinaryOperator.Opcode.Ge;
- break;
- }
- default: SynErr(117); 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 == 74 || la.kind == 75) {
- AddOp(out x, out op);
- Factor(out e1);
- e0 = Expr.Binary(x, op, e0, e1);
- }
- }
-
- void Factor(out Expr/*!*/ e0) {
- Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; BinaryOperator.Opcode op;
- Power(out e0);
- while (StartOf(13)) {
- MulOp(out x, out op);
- Power(out e1);
- e0 = Expr.Binary(x, op, e0, e1);
- }
- }
-
- 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 == 74) {
- Get();
- x = t; op=BinaryOperator.Opcode.Add;
- } else if (la.kind == 75) {
- Get();
- x = t; op=BinaryOperator.Opcode.Sub;
- } else SynErr(118);
- }
-
- void Power(out Expr/*!*/ e0) {
- Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1;
- UnaryExpression(out e0);
- if (la.kind == 79) {
- Get();
- x = t;
- Power(out e1);
- e0 = Expr.Binary(x, BinaryOperator.Opcode.Pow, e0, e1);
- }
- }
-
- 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 == 44) {
- Get();
- x = t; op=BinaryOperator.Opcode.Mul;
- } else if (la.kind == 76) {
- Get();
- x = t; op=BinaryOperator.Opcode.Div;
- } else if (la.kind == 77) {
- Get();
- x = t; op=BinaryOperator.Opcode.Mod;
- } else if (la.kind == 78) {
- Get();
- x = t; op=BinaryOperator.Opcode.RealDiv;
- } else SynErr(119);
- }
-
- void UnaryExpression(out Expr/*!*/ e) {
- Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;
- e = dummyExpr;
-
- if (la.kind == 75) {
- Get();
- x = t;
- UnaryExpression(out e);
- e = Expr.Unary(x, UnaryOperator.Opcode.Neg, e);
- } else if (la.kind == 80 || la.kind == 81) {
- NegOp();
- x = t;
- UnaryExpression(out e);
- e = Expr.Unary(x, UnaryOperator.Opcode.Not, e);
- } else if (StartOf(14)) {
- CoercionExpression(out e);
- } else SynErr(120);
- }
-
- void NegOp() {
- if (la.kind == 80) {
- Get();
- } else if (la.kind == 81) {
- Get();
- } else SynErr(123);
- }
-
- void CoercionExpression(out Expr/*!*/ e) {
- Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;
- Bpl.Type/*!*/ coercedTo;
- BigNum bn;
-
- ArrayExpression(out e);
- while (la.kind == 11) {
- Get();
- x = t;
- if (StartOf(6)) {
- Type(out coercedTo);
- e = Expr.CoerceType(x, e, coercedTo);
- } else if (la.kind == 3) {
- Nat(out bn);
- if (!(e is LiteralExpr) || !((LiteralExpr)e).isBigNum) {
- this.SemErr("arguments of extract need to be integer literals");
- e = new BvBounds(x, bn, BigNum.ZERO);
- } else {
- e = new BvBounds(x, bn, ((LiteralExpr)e).asBigNum);
- }
-
- } else SynErr(124);
- }
- }
-
- void ArrayExpression(out Expr/*!*/ e) {
- Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;
- Expr/*!*/ index0 = dummyExpr; Expr/*!*/ e1;
- bool store; bool bvExtract;
- List<Expr>/*!*/ allArgs = dummyExprSeq;
-
- AtomExpression(out e);
- while (la.kind == 17) {
- Get();
- x = t; allArgs = new List<Expr> ();
- allArgs.Add(e);
- store = false; bvExtract = false;
- if (StartOf(15)) {
- if (StartOf(9)) {
- Expression(out index0);
- if (index0 is BvBounds)
- bvExtract = true;
- else
- allArgs.Add(index0);
-
- while (la.kind == 12) {
- Get();
- Expression(out e1);
- if (bvExtract || e1 is BvBounds)
- this.SemErr("bitvectors only have one dimension");
- allArgs.Add(e1);
-
- }
- if (la.kind == 50) {
- Get();
- Expression(out e1);
- if (bvExtract || e1 is BvBounds)
- this.SemErr("assignment to bitvectors is not possible");
- allArgs.Add(e1); store = true;
-
- }
- } else {
- Get();
- Expression(out e1);
- allArgs.Add(e1); store = true;
- }
- }
- Expect(18);
- if (store)
- e = new NAryExpr(x, new MapStore(x, allArgs.Count - 2), allArgs);
- else if (bvExtract)
- e = new BvExtractExpr(x, e,
- ((BvBounds)index0).Upper.ToIntSafe,
- ((BvBounds)index0).Lower.ToIntSafe);
- else
- e = new NAryExpr(x, new MapSelect(x, allArgs.Count - 1), allArgs);
-
- }
- }
-
- void Nat(out BigNum n) {
- Expect(3);
- try {
- n = BigNum.FromString(t.val);
- } catch (FormatException) {
- this.SemErr("incorrectly formatted number");
- n = BigNum.ZERO;
- }
-
- }
-
- void AtomExpression(out Expr/*!*/ e) {
- Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; int n; BigNum bn; BigDec bd; BigFloat fp;
- List<Expr>/*!*/ es; List<Variable>/*!*/ ds; Trigger trig;
- List<TypeVariable>/*!*/ typeParams;
- IdentifierExpr/*!*/ id;
- QKeyValue kv;
- e = dummyExpr;
- List<Variable>/*!*/ locals;
- List<Block/*!*/>/*!*/ blocks;
-
- switch (la.kind) {
- case 82: {
- Get();
- e = new LiteralExpr(t, false);
- break;
- }
- case 83: {
- Get();
- e = new LiteralExpr(t, true);
- break;
- }
- case 3: {
- Nat(out bn);
- e = new LiteralExpr(t, bn);
- break;
- }
- case 5: case 6: {
- Dec(out bd);
- e = new LiteralExpr(t, bd);
- break;
- }
- case 97: {
- Float(out fp);
- e = new LiteralExpr(t, fp);
- break;
- }
- case 2: {
- BvLit(out bn, out n);
- e = new LiteralExpr(t, bn, n);
- break;
- }
- case 1: {
- Ident(out x);
- id = new IdentifierExpr(x, x.val); e = id;
- if (la.kind == 9) {
- Get();
- if (StartOf(9)) {
- Expressions(out es);
- e = new NAryExpr(x, new FunctionCall(id), es);
- } else if (la.kind == 10) {
- e = new NAryExpr(x, new FunctionCall(id), new List<Expr>());
- } else SynErr(125);
- Expect(10);
- }
- break;
- }
- case 84: {
- Get();
- x = t;
- Expect(9);
- Expression(out e);
- Expect(10);
- e = new OldExpr(x, e);
- break;
- }
- case 14: {
- Get();
- x = t;
- Expect(9);
- Expression(out e);
- Expect(10);
- e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToInt), new List<Expr>{ e });
- break;
- }
- case 15: {
- Get();
- x = t;
- Expect(9);
- Expression(out e);
- Expect(10);
- e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToReal), new List<Expr>{ e });
- break;
- }
- case 98: {
- Get();
- x = t;
- Expect(19);
- Expression(out e);
- Expect(20);
- e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToFloat), new List<Expr> { e });
- break;
- }
- case 9: {
- Get();
- if (StartOf(9)) {
- Expression(out e);
- if (e is BvBounds)
- this.SemErr("parentheses around bitvector bounds " +
- "are not allowed");
- } else if (la.kind == 88 || la.kind == 89) {
- 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 == 90 || la.kind == 91) {
- 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 == 92 || la.kind == 93) {
- Lambda();
- x = t;
- QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);
- if (trig != null)
- SemErr("triggers not allowed in lambda expressions");
- if (typeParams.Count + ds.Count > 0)
- e = new LambdaExpr(x, typeParams, ds, kv, e);
- } else SynErr(126);
- Expect(10);
- break;
- }
- case 40: {
- IfThenElseExpression(out e);
- break;
- }
- case 85: {
- CodeExpression(out locals, out blocks);
- e = new CodeExpr(locals, blocks);
- break;
- }
- default: SynErr(127); break;
- }
- }
-
- void Dec(out BigDec n) {
- string s = "";
- if (la.kind == 5) {
- Get();
- s = t.val;
- } else if (la.kind == 6) {
- Get();
- s = t.val;
- } else SynErr(128);
- try {
- n = BigDec.FromString(s);
- } catch (FormatException) {
- this.SemErr("incorrectly formatted number");
- n = BigDec.ZERO;
- }
-
- }
-
- /// <summary>
- /// Creates a floating point from the current token value
- /// </summary>
- /// <param name="n"></param>
- void Float(out BigFloat n)
- {
- try
- {
- if (la.kind == 97) {
- bool negative = false;
- int exp, sig, size;
- BigNum exp_val, sig_val, value;
- //Expected format = float(sign exp_val sig_val) || float<exp sig>(value)
- Get(); //Skip the float token
- if (la.val == "(") {
- Get();
- if (la.val == "false")
- negative = false;
- else if (la.val == "true")
- negative = true;
- else
- throw new FormatException();
- Get();
- Expect(12); //,
- BvLit(out exp_val, out exp);
- Expect(12);
- BvLit(out sig_val, out sig);
- n = new BigFloat(negative, exp_val, sig_val, exp, sig);
- Expect(10); //)
- }
- else if (la.val == "<") {
- Get();
- Expect(3);
- exp = Int32.Parse(t.val);
- Expect(12);
- Expect(3);
- sig = Int32.Parse(t.val);
- Expect(20); //>
- Expect(9); //(
- if (la.kind == 1) { //NaN
- Get();
- n = new BigFloat(t.val, exp, sig);
- }
- else if (la.kind == 74 || la.kind == 75) { //+ or -
- Get();
- String s = t.val;
- Get();
- n = new BigFloat(s + t.val, exp, sig);
- }
- else {
- BvLit(out value, out size);
- n = new BigFloat(value.ToString(), exp, sig);
- }
- Expect(10); //)
- }
- else {
- throw new FormatException();
- }
- }
- else {
- n = BigFloat.ZERO(8, 24);
- SynErr(137);
- }
- }
- catch (FormatException)
- {
- this.SemErr("incorrectly formatted floating point");
- n = BigFloat.ZERO(8, 24);
- }
- }
-
- void BvLit(out BigNum n, out int m) {
- Expect(2);
- int pos = t.val.IndexOf("bv");
- string a = t.val.Substring(0, pos);
- string b = t.val.Substring(pos + 2);
- try {
- n = BigNum.FromString(a);
- m = Convert.ToInt32(b);
- } catch (FormatException) {
- this.SemErr("incorrectly formatted bitvector");
- n = BigNum.ZERO;
- m = 0;
- }
-
- }
-
- void Forall() {
- if (la.kind == 88) {
- Get();
- } else if (la.kind == 89) {
- Get();
- } else SynErr(129);
- }
-
- void QuantifierBody(IToken/*!*/ q, out List<TypeVariable>/*!*/ typeParams, out List<Variable>/*!*/ ds,
-out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
- Contract.Requires(q != null); Contract.Ensures(Contract.ValueAtReturn(out typeParams) != null); Contract.Ensures(Contract.ValueAtReturn(out ds) != null); Contract.Ensures(Contract.ValueAtReturn(out body) != null);
- trig = null; typeParams = new List<TypeVariable> ();
- IToken/*!*/ tok;
- kv = null;
- ds = new List<Variable> ();
-
- if (la.kind == 19) {
- TypeParams(out tok, out typeParams);
- if (la.kind == 1 || la.kind == 27) {
- BoundVars(q, out ds);
- }
- } else if (la.kind == 1 || la.kind == 27) {
- BoundVars(q, out ds);
- } else SynErr(130);
- QSep();
- while (la.kind == 27) {
- AttributeOrTrigger(ref kv, ref trig);
- }
- Expression(out body);
- }
-
- void Exists() {
- if (la.kind == 90) {
- Get();
- } else if (la.kind == 91) {
- Get();
- } else SynErr(131);
- }
-
- void Lambda() {
- if (la.kind == 92) {
- Get();
- } else if (la.kind == 93) {
- Get();
- } else SynErr(132);
- }
-
- void IfThenElseExpression(out Expr/*!*/ e) {
- Contract.Ensures(Contract.ValueAtReturn(out e) != null);
- IToken/*!*/ tok;
- Expr/*!*/ e0, e1, e2;
- e = dummyExpr;
- Expect(40);
- tok = t;
- Expression(out e0);
- Expect(87);
- Expression(out e1);
- Expect(41);
- Expression(out e2);
- e = new NAryExpr(tok, new IfThenElse(tok), new List<Expr>{ e0, e1, e2 });
- }
-
- void CodeExpression(out List<Variable>/*!*/ locals, out List<Block/*!*/>/*!*/ blocks) {
- Contract.Ensures(Contract.ValueAtReturn(out locals) != null); Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out blocks))); locals = new List<Variable>(); Block/*!*/ b;
- blocks = new List<Block/*!*/>();
-
- Expect(85);
- while (la.kind == 7) {
- LocalVars(locals);
- }
- SpecBlock(out b);
- blocks.Add(b);
- while (la.kind == 1) {
- SpecBlock(out b);
- blocks.Add(b);
- }
- Expect(86);
- }
-
- void SpecBlock(out Block/*!*/ b) {
- Contract.Ensures(Contract.ValueAtReturn(out b) != null); IToken/*!*/ x; IToken/*!*/ y;
- Cmd c; IToken label;
- List<Cmd> cs = new List<Cmd>();
- List<IToken>/*!*/ xs;
- List<String> ss = new List<String>();
- b = dummyBlock;
- Expr/*!*/ e;
-
- Ident(out x);
- Expect(11);
- while (StartOf(8)) {
- LabelOrCmd(out c, out label);
- if (c != null) {
- Contract.Assert(label == null);
- cs.Add(c);
- } else {
- Contract.Assert(label != null);
- SemErr("SpecBlock's can only have one label");
- }
-
- }
- if (la.kind == 38) {
- Get();
- y = t;
- Idents(out xs);
- foreach(IToken/*!*/ s in xs){
- Contract.Assert(s != null);
- ss.Add(s.val); }
- b = new Block(x,x.val,cs,new GotoCmd(y,ss));
-
- } else if (la.kind == 39) {
- Get();
- Expression(out e);
- b = new Block(x,x.val,cs,new ReturnExprCmd(t,e));
- } else SynErr(133);
- Expect(8);
- }
-
- void AttributeOrTrigger(ref QKeyValue kv, ref Trigger trig) {
- IToken/*!*/ tok; Expr/*!*/ e; List<Expr>/*!*/ es;
- string key;
- List<object/*!*/> parameters; object/*!*/ param;
-
- Expect(27);
- tok = t;
- if (la.kind == 11) {
- Get();
- Expect(1);
- key = t.val; parameters = new List<object/*!*/>();
- if (StartOf(16)) {
- AttributeParameter(out param);
- parameters.Add(param);
- while (la.kind == 12) {
- Get();
- AttributeParameter(out param);
- parameters.Add(param);
- }
- }
- if (key == "nopats") {
- if (parameters.Count == 1 && parameters[0] is Expr) {
- e = (Expr)parameters[0];
- if(trig==null){
- trig = new Trigger(tok, false, new List<Expr> { e }, null);
- } else {
- trig.AddLast(new Trigger(tok, false, new List<Expr> { e }, null));
- }
- } else {
- this.SemErr("the 'nopats' quantifier attribute expects a string-literal parameter");
- }
- } else {
- if (kv==null) {
- kv = new QKeyValue(tok, key, parameters, null);
- } else {
- kv.AddLast(new QKeyValue(tok, key, parameters, null));
- }
- }
-
- } else if (StartOf(9)) {
- Expression(out e);
- es = new List<Expr> { e };
- while (la.kind == 12) {
- Get();
- Expression(out e);
- es.Add(e);
- }
- if (trig==null) {
- trig = new Trigger(tok, true, es, null);
- } else {
- trig.AddLast(new Trigger(tok, true, es, null));
- }
-
- } else SynErr(134);
- Expect(28);
- }
-
- void AttributeParameter(out object/*!*/ o) {
- Contract.Ensures(Contract.ValueAtReturn(out o) != null);
- o = "error";
- Expr/*!*/ e;
-
- if (la.kind == 4) {
- Get();
- o = t.val.Substring(1, t.val.Length-2);
- } else if (StartOf(9)) {
- Expression(out e);
- o = e;
- } else SynErr(135);
- }
-
- void QSep() {
- if (la.kind == 94) {
- Get();
- } else if (la.kind == 95) {
- Get();
- } else SynErr(136);
- }
-
-
-
- public void Parse() {
- la = new Token();
- la.val = "";
- Get();
- BoogiePL();
- Expect(0);
-
- Expect(0);
- }
-
- static readonly bool[,]/*!*/ set = { //grid is 17 x 100
- {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,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,T,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,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,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,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,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,T,x},
- {x,T,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,T,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,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,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,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,T,T,T, x,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,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,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,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,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, 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,T,T,T, x,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,x,x, x,x,x,x, x,x,x,x, x,T,x,x},
- {x,T,T,T, x,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,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,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,x,x, x,x,x,x, x,x,x,x, x,x,x,x}
-
- };
-} // end Parser
-
-
-public class Errors {
- public int count = 0; // number of errors detected
- public System.IO.TextWriter/*!*/ errorStream = Console.Out; // error messages go to this stream
- public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text
- public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text
-
- public void SynErr(string filename, int line, int col, int n) {
- SynErr(filename, line, col, GetSyntaxErrorString(n));
- }
-
- public virtual void SynErr(string filename, int line, int col, string/*!*/ msg) {
- Contract.Requires(msg != null);
- errorStream.WriteLine(errMsgFormat, filename, line, col, msg);
- count++;
- }
-
- /// <summary>
- /// Returns a string corresponding to the syntax error of the given type
- /// Note that many of these errors (0-98) correspond to token types (e.g. the la token)
- /// </summary>
- /// <param name="n"></param>
- /// <returns></returns>
- string GetSyntaxErrorString(int n) {
- string s;
- switch (n) {
- case 0: s = "EOF expected"; break;
- case 1: s = "ident expected"; break;
- case 2: s = "bvlit expected"; break;
- case 3: s = "digits expected"; break;
- case 4: s = "string expected"; break;
- case 5: s = "decimal expected"; break;
- case 6: s = "float expected"; break;
- case 7: s = "\"var\" expected"; break;
- case 8: s = "\";\" expected"; break;
- case 9: s = "\"(\" expected"; break;
- case 10: s = "\")\" expected"; break;
- case 11: s = "\":\" expected"; break;
- case 12: s = "\",\" expected"; break;
- case 13: s = "\"where\" expected"; break;
- case 14: s = "\"int\" expected"; break;
- case 15: s = "\"real\" expected"; break;
- case 16: s = "\"bool\" expected"; break;
- case 17: s = "\"[\" expected"; break;
- case 18: s = "\"]\" expected"; break;
- case 19: s = "\"<\" expected"; break;
- case 20: s = "\">\" expected"; break;
- case 21: s = "\"const\" expected"; break;
- case 22: s = "\"unique\" expected"; break;
- case 23: s = "\"extends\" expected"; break;
- case 24: s = "\"complete\" expected"; break;
- case 25: s = "\"function\" expected"; break;
- case 26: s = "\"returns\" expected"; break;
- case 27: s = "\"{\" expected"; break;
- case 28: s = "\"}\" expected"; break;
- case 29: s = "\"axiom\" expected"; break;
- case 30: s = "\"type\" expected"; break;
- case 31: s = "\"=\" expected"; break;
- case 32: s = "\"procedure\" expected"; break;
- case 33: s = "\"implementation\" expected"; break;
- case 34: s = "\"modifies\" expected"; break;
- case 35: s = "\"free\" expected"; break;
- case 36: s = "\"requires\" expected"; break;
- case 37: s = "\"ensures\" expected"; break;
- case 38: s = "\"goto\" expected"; break;
- case 39: s = "\"return\" expected"; break;
- case 40: s = "\"if\" expected"; break;
- case 41: s = "\"else\" expected"; break;
- case 42: s = "\"while\" expected"; break;
- case 43: s = "\"invariant\" expected"; break;
- case 44: s = "\"*\" expected"; break;
- case 45: s = "\"break\" expected"; break;
- case 46: s = "\"assert\" expected"; break;
- case 47: s = "\"assume\" expected"; break;
- case 48: s = "\"havoc\" expected"; break;
- case 49: s = "\"yield\" expected"; break;
- case 50: s = "\":=\" expected"; break;
- case 51: s = "\"async\" expected"; break;
- case 52: s = "\"call\" expected"; break;
- case 53: s = "\"par\" expected"; break;
- case 54: s = "\"|\" expected"; break;
- case 55: s = "\"<==>\" expected"; break;
- case 56: s = "\"\\u21d4\" expected"; break;
- case 57: s = "\"==>\" expected"; break;
- case 58: s = "\"\\u21d2\" expected"; break;
- case 59: s = "\"<==\" expected"; break;
- case 60: s = "\"\\u21d0\" expected"; break;
- case 61: s = "\"&&\" expected"; break;
- case 62: s = "\"\\u2227\" expected"; break;
- case 63: s = "\"||\" expected"; break;
- case 64: s = "\"\\u2228\" expected"; break;
- case 65: s = "\"==\" 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 = "\"\\u2260\" expected"; break;
- case 71: s = "\"\\u2264\" expected"; break;
- case 72: s = "\"\\u2265\" expected"; break;
- case 73: s = "\"++\" expected"; break;
- case 74: s = "\"+\" expected"; break;
- case 75: s = "\"-\" expected"; break;
- case 76: s = "\"div\" expected"; break;
- case 77: s = "\"mod\" expected"; break;
- case 78: s = "\"/\" expected"; break;
- case 79: s = "\"**\" expected"; break;
- case 80: s = "\"!\" expected"; break;
- case 81: s = "\"\\u00ac\" expected"; break;
- case 82: s = "\"false\" expected"; break;
- case 83: s = "\"true\" expected"; break;
- case 84: s = "\"old\" expected"; break;
- case 85: s = "\"|{\" expected"; break;
- case 86: s = "\"}|\" expected"; break;
- case 87: s = "\"then\" expected"; break;
- case 88: s = "\"forall\" expected"; break;
- case 89: s = "\"\\u2200\" expected"; break;
- case 90: s = "\"exists\" expected"; break;
- case 91: s = "\"\\u2203\" expected"; break;
- case 92: s = "\"lambda\" expected"; break;
- case 93: s = "\"\\u03bb\" expected"; break;
- case 94: s = "\"::\" expected"; break;
- case 95: s = "\"\\u2022\" expected"; break;
- case 96: s = "??? expected"; break;
- case 97: s = "fp expected"; break;
- case 98: s = "\"float\" expected"; break;
- case 99: s = "invalid Function"; break;
- case 100: s = "invalid Function"; break;
- case 101: s = "invalid Procedure"; break;
- case 102: s = "invalid Type"; break;
- case 103: s = "invalid TypeAtom"; break;
- case 104: s = "invalid TypeArgs"; break;
- case 105: s = "invalid Spec"; break;
- case 106: s = "invalid SpecPrePost"; break;
- case 107: s = "invalid LabelOrCmd"; break;
- case 108: s = "invalid StructuredCmd"; break;
- case 109: s = "invalid TransferCmd"; break;
- case 110: s = "invalid IfCmd"; break;
- case 111: s = "invalid Guard"; break;
- case 112: s = "invalid LabelOrAssign"; break;
- case 113: s = "invalid CallParams"; break;
- case 114: s = "invalid EquivOp"; break;
- case 115: s = "invalid ImpliesOp"; break;
- case 116: s = "invalid ExpliesOp"; break;
- case 117: s = "invalid AndOp"; break;
- case 118: s = "invalid OrOp"; break;
- case 119: s = "invalid RelOp"; break;
- case 120: s = "invalid AddOp"; break;
- case 121: s = "invalid MulOp"; break;
- case 122: s = "invalid UnaryExpression"; break;
- case 123: s = "invalid NegOp"; break;
- case 124: s = "invalid CoercionExpression"; break;
- case 125: s = "invalid AtomExpression"; break;
- case 126: s = "invalid AtomExpression"; break;
- case 127: s = "invalid AtomExpression"; break;
- case 128: s = "invalid Dec"; break;
- case 129: s = "invalid Forall"; break;
- case 130: s = "invalid QuantifierBody"; break;
- case 131: s = "invalid Exists"; break;
- case 132: s = "invalid Lambda"; break;
- case 133: s = "invalid SpecBlock"; break;
- case 134: s = "invalid AttributeOrTrigger"; break;
- case 135: s = "invalid AttributeParameter"; break;
- case 136: s = "invalid QSep"; break;
- case 137: s = "invalid Float"; break;
-
- default: s = "error " + n; break;
- }
- return s;
- }
-
- public void SemErr(IToken/*!*/ tok, string/*!*/ msg) { // semantic errors
- Contract.Requires(tok != null);
- Contract.Requires(msg != null);
- SemErr(tok.filename, tok.line, tok.col, msg);
- }
-
- public virtual void SemErr(string filename, int line, int col, string/*!*/ msg) {
- Contract.Requires(msg != null);
- errorStream.WriteLine(errMsgFormat, filename, line, col, msg);
- count++;
- }
-
- public void Warning(IToken/*!*/ tok, string/*!*/ msg) { // warnings
- Contract.Requires(tok != null);
- Contract.Requires(msg != null);
- Warning(tok.filename, tok.line, tok.col, msg);
- }
-
- public virtual void Warning(string filename, int line, int col, string msg) {
- Contract.Requires(msg != null);
- errorStream.WriteLine(warningMsgFormat, filename, line, col, msg);
- }
-} // Errors
-
-
-public class FatalError: Exception {
- public FatalError(string m): base(m) {}
-}
-
-
+using System.Collections;
+using System.Collections.Generic;
+using System.IO;
+using System.Text;
+using Microsoft.Boogie;
+using Microsoft.Basetypes;
+using Bpl = Microsoft.Boogie;
+
+
+
+
+using System;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Boogie {
+
+
+
+public class Parser {
+ public const int _EOF = 0;
+ public const int _ident = 1;
+ public const int _bvlit = 2;
+ public const int _digits = 3;
+ public const int _string = 4;
+ public const int _decimal = 5;
+ public const int _float = 6;
+ public const int _fp = 97;
+ public const int maxT = 98;
+
+ const bool T = true;
+ const bool x = false;
+ const int minErrDist = 2;
+
+ public Scanner/*!*/ scanner;
+ public Errors/*!*/ errors;
+
+ public Token/*!*/ t; // last recognized token
+ public Token/*!*/ la; // lookahead token
+ int errDist = minErrDist;
+
+readonly Program/*!*/ Pgm;
+
+readonly Expr/*!*/ dummyExpr;
+readonly Cmd/*!*/ dummyCmd;
+readonly Block/*!*/ dummyBlock;
+readonly Bpl.Type/*!*/ dummyType;
+readonly List<Expr>/*!*/ dummyExprSeq;
+readonly TransferCmd/*!*/ dummyTransferCmd;
+readonly StructuredCmd/*!*/ dummyStructuredCmd;
+
+///<summary>
+///Returns the number of parsing errors encountered. If 0, "program" returns as
+///the parsed program.
+///</summary>
+public static int Parse (string/*!*/ filename, /*maybe null*/ List<string/*!*/> defines, out /*maybe null*/ Program program, bool useBaseName=false) /* throws System.IO.IOException */ {
+ Contract.Requires(filename != null);
+ Contract.Requires(cce.NonNullElements(defines,true));
+
+ if (defines == null) {
+ defines = new List<string/*!*/>();
+ }
+
+ if (filename == "stdin.bpl") {
+ var s = ParserHelper.Fill(Console.In, defines);
+ return Parse(s, filename, out program, useBaseName);
+ } else {
+ FileStream stream = new FileStream(filename, FileMode.Open, FileAccess.Read, FileShare.Read);
+ var s = ParserHelper.Fill(stream, defines);
+ var ret = Parse(s, filename, out program, useBaseName);
+ stream.Close();
+ return ret;
+ }
+}
+
+
+public static int Parse (string s, string/*!*/ filename, out /*maybe null*/ Program program, bool useBaseName=false) /* throws System.IO.IOException */ {
+ Contract.Requires(s != null);
+ Contract.Requires(filename != null);
+
+ byte[]/*!*/ buffer = cce.NonNull(UTF8Encoding.Default.GetBytes(s));
+ MemoryStream ms = new MemoryStream(buffer,false);
+ Errors errors = new Errors();
+ Scanner scanner = new Scanner(ms, errors, filename, useBaseName);
+
+ Parser parser = new Parser(scanner, errors, false);
+ parser.Parse();
+ if (parser.errors.count == 0)
+ {
+ program = parser.Pgm;
+ program.ProcessDatatypeConstructors();
+ return 0;
+ }
+ else
+ {
+ program = null;
+ return parser.errors.count;
+ }
+}
+
+public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, bool disambiguation)
+ : this(scanner, errors)
+{
+ // initialize readonly fields
+ Pgm = new Program();
+ dummyExpr = new LiteralExpr(Token.NoToken, false);
+ dummyCmd = new AssumeCmd(Token.NoToken, dummyExpr);
+ dummyBlock = new Block(Token.NoToken, "dummyBlock", new List<Cmd>(), new ReturnCmd(Token.NoToken));
+ dummyType = new BasicType(Token.NoToken, SimpleType.Bool);
+ dummyExprSeq = new List<Expr> ();
+ dummyTransferCmd = new ReturnCmd(Token.NoToken);
+ dummyStructuredCmd = new BreakCmd(Token.NoToken, null);
+}
+
+// Class to represent the bounds of a bitvector expression t[a:b].
+// Objects of this class only exist during parsing and are directly
+// turned into BvExtract before they get anywhere else
+private class BvBounds : Expr {
+ public BigNum Lower;
+ public BigNum Upper;
+ public BvBounds(IToken/*!*/ tok, BigNum lower, BigNum upper)
+ : base(tok, /*immutable=*/ false) {
+ Contract.Requires(tok != null);
+ this.Lower = lower;
+ this.Upper = upper;
+ }
+ public override Bpl.Type/*!*/ ShallowType { get {Contract.Ensures(Contract.Result<Bpl.Type>() != null); return Bpl.Type.Int; } }
+ public override void Resolve(ResolutionContext/*!*/ rc) {
+ // Contract.Requires(rc != null);
+ rc.Error(this, "bitvector bounds in illegal position");
+ }
+ public override void Emit(TokenTextWriter/*!*/ stream,
+ int contextBindingStrength, bool fragileContext) {
+ Contract.Assert(false);throw new cce.UnreachableException();
+ }
+ public override void ComputeFreeVariables(GSet<object>/*!*/ freeVars) { Contract.Assert(false);throw new cce.UnreachableException(); }
+ public override int ComputeHashCode() {
+ return base.GetHashCode();
+ }
+}
+
+/*--------------------------------------------------------------------------*/
+
+
+ public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors) {
+ this.scanner = scanner;
+ this.errors = errors;
+ Token/*!*/ tok = new Token();
+ tok.val = "";
+ this.la = tok;
+ this.t = new Token(); // just to satisfy its non-null constraint
+ }
+
+ void SynErr (int n) {
+ if (errDist >= minErrDist) errors.SynErr(la.filename, la.line, la.col, n);
+ errDist = 0;
+ }
+
+ public void SemErr (string/*!*/ msg) {
+ Contract.Requires(msg != null);
+ if (errDist >= minErrDist) errors.SemErr(t, msg);
+ errDist = 0;
+ }
+
+ public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {
+ Contract.Requires(tok != null);
+ Contract.Requires(msg != null);
+ errors.SemErr(tok, msg);
+ }
+
+ void Get () {
+ for (;;) {
+ t = la;
+ la = scanner.Scan();
+ if (la.kind <= maxT) { ++errDist; break; }
+
+ la = t;
+ }
+ }
+
+ void Expect (int n) {
+ if (la.kind==n) Get(); else { SynErr(n); }
+ }
+
+ bool StartOf (int s) {
+ return set[s, la.kind];
+ }
+
+ void ExpectWeak (int n, int follow) {
+ if (la.kind == n) Get();
+ else {
+ SynErr(n);
+ while (!StartOf(follow)) Get();
+ }
+ }
+
+
+ bool WeakSeparator(int n, int syFol, int repFol) {
+ int kind = la.kind;
+ if (kind == n) {Get(); return true;}
+ else if (StartOf(repFol)) {return false;}
+ else {
+ SynErr(n);
+ while (!(set[syFol, kind] || set[repFol, kind] || set[0, kind])) {
+ Get();
+ kind = la.kind;
+ }
+ return StartOf(syFol);
+ }
+ }
+
+
+ void BoogiePL() {
+ List<Variable>/*!*/ vs;
+ List<Declaration>/*!*/ ds;
+ Axiom/*!*/ ax;
+ List<Declaration/*!*/>/*!*/ ts;
+ Procedure/*!*/ pr;
+ Implementation im;
+ Implementation/*!*/ nnim;
+
+ while (StartOf(1)) {
+ switch (la.kind) {
+ case 21: {
+ Consts(out vs);
+ foreach(Bpl.Variable/*!*/ v in vs){
+ Contract.Assert(v != null);
+ Pgm.AddTopLevelDeclaration(v);
+ }
+
+ break;
+ }
+ case 25: {
+ Function(out ds);
+ foreach(Bpl.Declaration/*!*/ d in ds){
+ Contract.Assert(d != null);
+ Pgm.AddTopLevelDeclaration(d);
+ }
+
+ break;
+ }
+ case 29: {
+ Axiom(out ax);
+ Pgm.AddTopLevelDeclaration(ax);
+ break;
+ }
+ case 30: {
+ UserDefinedTypes(out ts);
+ foreach(Declaration/*!*/ td in ts){
+ Contract.Assert(td != null);
+ Pgm.AddTopLevelDeclaration(td);
+ }
+
+ break;
+ }
+ case 7: {
+ GlobalVars(out vs);
+ foreach(Bpl.Variable/*!*/ v in vs){
+ Contract.Assert(v != null);
+ Pgm.AddTopLevelDeclaration(v);
+ }
+
+ break;
+ }
+ case 32: {
+ Procedure(out pr, out im);
+ Pgm.AddTopLevelDeclaration(pr);
+ if (im != null) {
+ Pgm.AddTopLevelDeclaration(im);
+ }
+
+ break;
+ }
+ case 33: {
+ Implementation(out nnim);
+ Pgm.AddTopLevelDeclaration(nnim);
+ break;
+ }
+ }
+ }
+ Expect(0);
+ }
+
+ void Consts(out List<Variable>/*!*/ ds) {
+ Contract.Ensures(Contract.ValueAtReturn(out ds) != null); IToken/*!*/ y; List<TypedIdent>/*!*/ xs;
+ ds = new List<Variable>();
+ bool u = false; QKeyValue kv = null;
+ bool ChildrenComplete = false;
+ List<ConstantParent/*!*/> Parents = null;
+ Expect(21);
+ y = t;
+ while (la.kind == 27) {
+ Attribute(ref kv);
+ }
+ if (la.kind == 22) {
+ Get();
+ u = true;
+ }
+ IdsType(out xs);
+ if (la.kind == 23) {
+ OrderSpec(out ChildrenComplete, out Parents);
+ }
+ bool makeClone = false;
+ foreach(TypedIdent/*!*/ x in xs){
+ Contract.Assert(x != null);
+
+ // ensure that no sharing is introduced
+ List<ConstantParent/*!*/> ParentsClone;
+ if (makeClone && Parents != null) {
+ ParentsClone = new List<ConstantParent/*!*/> ();
+ foreach (ConstantParent/*!*/ p in Parents){
+ Contract.Assert(p != null);
+ ParentsClone.Add(new ConstantParent (
+ new IdentifierExpr (p.Parent.tok, p.Parent.Name),
+ p.Unique));}
+ } else {
+ ParentsClone = Parents;
+ }
+ makeClone = true;
+
+ ds.Add(new Constant(y, x, u, ParentsClone, ChildrenComplete, kv));
+ }
+
+ Expect(8);
+ }
+
+ void Function(out List<Declaration>/*!*/ ds) {
+ Contract.Ensures(Contract.ValueAtReturn(out ds) != null);
+ ds = new List<Declaration>(); IToken/*!*/ z;
+ IToken/*!*/ typeParamTok;
+ var typeParams = new List<TypeVariable>();
+ var arguments = new List<Variable>();
+ TypedIdent/*!*/ tyd;
+ TypedIdent retTyd = null;
+ Bpl.Type/*!*/ retTy;
+ QKeyValue argKv = null;
+ QKeyValue kv = null;
+ Expr definition = null;
+ Expr/*!*/ tmp;
+
+ Expect(25);
+ while (la.kind == 27) {
+ Attribute(ref kv);
+ }
+ Ident(out z);
+ if (la.kind == 19) {
+ TypeParams(out typeParamTok, out typeParams);
+ }
+ Expect(9);
+ if (StartOf(2)) {
+ VarOrType(out tyd, out argKv);
+ arguments.Add(new Formal(tyd.tok, tyd, true, argKv));
+ while (la.kind == 12) {
+ Get();
+ VarOrType(out tyd, out argKv);
+ arguments.Add(new Formal(tyd.tok, tyd, true, argKv));
+ }
+ }
+ Expect(10);
+ argKv = null;
+ if (la.kind == 26) {
+ Get();
+ Expect(9);
+ VarOrType(out retTyd, out argKv);
+ Expect(10);
+ } else if (la.kind == 11) {
+ Get();
+ Type(out retTy);
+ retTyd = new TypedIdent(retTy.tok, TypedIdent.NoName, retTy);
+ } else SynErr(99);
+ if (la.kind == 27) {
+ Get();
+ Expression(out tmp);
+ definition = tmp;
+ Expect(28);
+ } else if (la.kind == 8) {
+ Get();
+ } else SynErr(100);
+ 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);
+ Contract.Assert(func != null);
+ ds.Add(func);
+ bool allUnnamed = true;
+ foreach(Formal/*!*/ f in arguments){
+ Contract.Assert(f != null);
+ if (f.TypedIdent.HasName) {
+ allUnnamed = false;
+ break;
+ }
+ }
+ if (!allUnnamed) {
+ Bpl.Type prevType = null;
+ for (int i = arguments.Count; 0 <= --i; ) {
+ TypedIdent/*!*/ curr = cce.NonNull(arguments[i]).TypedIdent;
+ if (curr.HasName) {
+ // the argument was given as both an identifier and a type
+ prevType = curr.Type;
+ } else {
+ // the argument was given as just one "thing", which syntactically parsed as a type
+ if (prevType == null) {
+ this.errors.SemErr(curr.tok, "the type of the last parameter is unspecified");
+ break;
+ }
+ Bpl.Type ty = curr.Type;
+ var uti = ty as UnresolvedTypeIdentifier;
+ if (uti != null && uti.Arguments.Count == 0) {
+ // the given "thing" was just an identifier, so let's use it as the name of the parameter
+ curr.Name = uti.Name;
+ curr.Type = prevType;
+ } else {
+ this.errors.SemErr(curr.tok, "expecting an identifier as parameter name");
+ }
+ }
+ }
+ }
+ if (definition != null) {
+ // generate either an axiom or a function body
+ if (QKeyValue.FindBoolAttribute(kv, "inline")) {
+ func.Body = definition;
+ } else {
+ ds.Add(func.CreateDefinitionAxiom(definition, kv));
+ }
+ }
+
+ }
+
+ void Axiom(out Axiom/*!*/ m) {
+ Contract.Ensures(Contract.ValueAtReturn(out m) != null); Expr/*!*/ e; QKeyValue kv = null;
+ Expect(29);
+ while (la.kind == 27) {
+ Attribute(ref kv);
+ }
+ IToken/*!*/ x = t;
+ Proposition(out e);
+ Expect(8);
+ m = new Axiom(x,e, null, kv);
+ }
+
+ void UserDefinedTypes(out List<Declaration/*!*/>/*!*/ ts) {
+ Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out ts))); Declaration/*!*/ decl; QKeyValue kv = null; ts = new List<Declaration/*!*/> ();
+ Expect(30);
+ while (la.kind == 27) {
+ Attribute(ref kv);
+ }
+ UserDefinedType(out decl, kv);
+ ts.Add(decl);
+ while (la.kind == 12) {
+ Get();
+ UserDefinedType(out decl, kv);
+ ts.Add(decl);
+ }
+ Expect(8);
+ }
+
+ void GlobalVars(out List<Variable>/*!*/ ds) {
+ Contract.Ensures(Contract.ValueAtReturn(out ds) != null);
+ QKeyValue kv = null;
+ ds = new List<Variable>();
+ var dsx = ds;
+
+ Expect(7);
+ while (la.kind == 27) {
+ Attribute(ref kv);
+ }
+ IdsTypeWheres(true, "global variables", delegate(TypedIdent tyd) { dsx.Add(new GlobalVariable(tyd.tok, tyd, kv)); } );
+ Expect(8);
+ }
+
+ void Procedure(out Procedure/*!*/ proc, out /*maybe null*/ Implementation impl) {
+ Contract.Ensures(Contract.ValueAtReturn(out proc) != null); IToken/*!*/ x;
+ List<TypeVariable>/*!*/ typeParams;
+ List<Variable>/*!*/ ins, outs;
+ List<Requires>/*!*/ pre = new List<Requires>();
+ List<IdentifierExpr>/*!*/ mods = new List<IdentifierExpr>();
+ List<Ensures>/*!*/ post = new List<Ensures>();
+
+ List<Variable>/*!*/ locals = new List<Variable>();
+ StmtList/*!*/ stmtList;
+ QKeyValue kv = null;
+ impl = null;
+
+ Expect(32);
+ ProcSignature(true, out x, out typeParams, out ins, out outs, out kv);
+ if (la.kind == 8) {
+ Get();
+ while (StartOf(3)) {
+ Spec(pre, mods, post);
+ }
+ } else if (StartOf(4)) {
+ while (StartOf(3)) {
+ Spec(pre, mods, post);
+ }
+ ImplBody(out locals, out stmtList);
+ impl = new Implementation(x, x.val, typeParams,
+ Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, kv == null ? null : (QKeyValue)kv.Clone(), this.errors);
+
+ } else SynErr(99);
+ proc = new Procedure(x, x.val, typeParams, ins, outs, pre, mods, post, kv);
+ }
+
+ void Implementation(out Implementation/*!*/ impl) {
+ Contract.Ensures(Contract.ValueAtReturn(out impl) != null); IToken/*!*/ x;
+ List<TypeVariable>/*!*/ typeParams;
+ List<Variable>/*!*/ ins, outs;
+ List<Variable>/*!*/ locals;
+ StmtList/*!*/ stmtList;
+ QKeyValue kv;
+
+ Expect(33);
+ 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);
+ }
+
+ void Attribute(ref QKeyValue kv) {
+ Trigger trig = null;
+ AttributeOrTrigger(ref kv, ref trig);
+ if (trig != null) this.SemErr("only attributes, not triggers, allowed here");
+ }
+
+ void IdsTypeWheres(bool allowWhereClauses, string context, System.Action<TypedIdent> action ) {
+ IdsTypeWhere(allowWhereClauses, context, action);
+ while (la.kind == 12) {
+ Get();
+ IdsTypeWhere(allowWhereClauses, context, action);
+ }
+ }
+
+ void LocalVars(List<Variable>/*!*/ ds) {
+ Contract.Ensures(Contract.ValueAtReturn(out ds) != null);
+ QKeyValue kv = null;
+
+ Expect(7);
+ while (la.kind == 27) {
+ Attribute(ref kv);
+ }
+ IdsTypeWheres(true, "local variables", delegate(TypedIdent tyd) { ds.Add(new LocalVariable(tyd.tok, tyd, kv)); } );
+ Expect(8);
+ }
+
+ void ProcFormals(bool incoming, bool allowWhereClauses, out List<Variable>/*!*/ ds) {
+ Contract.Ensures(Contract.ValueAtReturn(out ds) != null);
+ ds = new List<Variable>();
+ var dsx = ds;
+ var context = allowWhereClauses ? "procedure formals" : "the 'implementation' copies of formals";
+
+ Expect(9);
+ if (la.kind == 1 || la.kind == 27) {
+ AttrsIdsTypeWheres(allowWhereClauses, allowWhereClauses, context, delegate(TypedIdent tyd, QKeyValue kv) { dsx.Add(new Formal(tyd.tok, tyd, incoming, kv)); });
+ }
+ Expect(10);
+ }
+
+ void AttrsIdsTypeWheres(bool allowAttributes, bool allowWhereClauses, string context, System.Action<TypedIdent, QKeyValue> action ) {
+ AttributesIdsTypeWhere(allowAttributes, allowWhereClauses, context, action);
+ while (la.kind == 12) {
+ Get();
+ AttributesIdsTypeWhere(allowAttributes, allowWhereClauses, context, action);
+ }
+ }
+
+ void BoundVars(IToken/*!*/ x, out List<Variable>/*!*/ ds) {
+ Contract.Requires(x != null);
+ Contract.Ensures(Contract.ValueAtReturn(out ds) != null);
+ List<TypedIdent>/*!*/ tyds = new List<TypedIdent>();
+ ds = new List<Variable>();
+ var dsx = ds;
+
+ AttrsIdsTypeWheres(true, false, "bound variables", delegate(TypedIdent tyd, QKeyValue kv) { dsx.Add(new BoundVariable(tyd.tok, tyd, kv)); } );
+ }
+
+ void IdsType(out List<TypedIdent>/*!*/ tyds) {
+ Contract.Ensures(Contract.ValueAtReturn(out tyds) != null); List<IToken>/*!*/ ids; Bpl.Type/*!*/ ty;
+ Idents(out ids);
+ Expect(11);
+ Type(out ty);
+ tyds = new List<TypedIdent>();
+ foreach(Token/*!*/ id in ids){
+ Contract.Assert(id != null);
+ tyds.Add(new TypedIdent(id, id.val, ty, null));
+ }
+
+ }
+
+ void Idents(out List<IToken>/*!*/ xs) {
+ Contract.Ensures(Contract.ValueAtReturn(out xs) != null); IToken/*!*/ id; xs = new List<IToken>();
+ Ident(out id);
+ xs.Add(id);
+ while (la.kind == 12) {
+ Get();
+ Ident(out id);
+ xs.Add(id);
+ }
+ }
+
+ void Type(out Bpl.Type/*!*/ ty) {
+ Contract.Ensures(Contract.ValueAtReturn(out ty) != null); IToken/*!*/ tok; ty = dummyType;
+ if (StartOf(5)) {
+ TypeAtom(out ty);
+ } else if (la.kind == 1) {
+ Ident(out tok);
+ List<Bpl.Type>/*!*/ args = new List<Bpl.Type> ();
+ if (StartOf(6)) {
+ TypeArgs(args);
+ }
+ ty = new UnresolvedTypeIdentifier (tok, tok.val, args);
+ } else if (la.kind == 17 || la.kind == 19) {
+ MapType(out ty);
+ } else SynErr(100);
+ }
+
+ void AttributesIdsTypeWhere(bool allowAttributes, bool allowWhereClauses, string context, System.Action<TypedIdent, QKeyValue> action ) {
+ QKeyValue kv = null;
+ while (la.kind == 27) {
+ Attribute(ref kv);
+ if (!allowAttributes) {
+ kv = null;
+ this.SemErr("attributes are not allowed on " + context);
+ }
+
+ }
+ IdsTypeWhere(allowWhereClauses, context, delegate(TypedIdent tyd) { action(tyd, kv); });
+ }
+
+ void IdsTypeWhere(bool allowWhereClauses, string context, System.Action<TypedIdent> action ) {
+ List<IToken>/*!*/ ids; Bpl.Type/*!*/ ty; Expr wh = null; Expr/*!*/ nne;
+ Idents(out ids);
+ Expect(11);
+ Type(out ty);
+ if (la.kind == 13) {
+ Get();
+ Expression(out nne);
+ if (!allowWhereClauses) {
+ this.SemErr("where clause not allowed on " + context);
+ } else {
+ wh = nne;
+ }
+
+ }
+ foreach(Token/*!*/ id in ids){
+ Contract.Assert(id != null);
+ action(new TypedIdent(id, id.val, ty, wh));
+ }
+
+ }
+
+ void Expression(out Expr/*!*/ e0) {
+ Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1;
+ ImpliesExpression(false, out e0);
+ while (la.kind == 55 || la.kind == 56) {
+ EquivOp();
+ x = t;
+ ImpliesExpression(false, out e1);
+ e0 = Expr.Binary(x, BinaryOperator.Opcode.Iff, e0, e1);
+ }
+ }
+
+ void TypeAtom(out Bpl.Type/*!*/ ty) {
+ Contract.Ensures(Contract.ValueAtReturn(out ty) != null); ty = dummyType;
+ if (la.kind == 14) {
+ Get();
+ ty = new BasicType(t, SimpleType.Int);
+ } else if (la.kind == 15) {
+ Get();
+ ty = new BasicType(t, SimpleType.Real);
+ } else if (la.kind == 98) {
+ Get();
+ ty = FType();
+ } else if (la.kind == 16) {
+ Get();
+ ty = new BasicType(t, SimpleType.Bool);
+ } else if (la.kind == 9) {
+ Get();
+ Type(out ty);
+ Expect(10);
+ } else SynErr(101);
+ }
+
+ FloatType FType() {
+ if (t.val.Length > 5) {
+ switch (Int32.Parse(t.val.Substring(5))) {
+ case 16:
+ return new FloatType(t, 5, 11);
+ case 32:
+ return new FloatType(t, 8, 24);
+ case 64:
+ return new FloatType(t, 11, 53);
+ case 128:
+ return new FloatType(t, 15, 113);
+ default:
+ SynErr(3);
+ return new FloatType(t, 0, 0);
+ }
+ }
+ else {
+ try {
+ Expect(19); //<
+ Expect(3); //int
+ int exp = Int32.Parse(t.val);
+ Expect(12); //,
+ Expect(3); //int
+ int man = Int32.Parse(t.val);
+ Expect(20); //>
+ return new FloatType(t, exp, man);
+ }
+ catch (Exception) {
+ return new FloatType(t, 0, 0);
+ }
+ }
+ }
+
+ void Ident(out IToken/*!*/ x) {
+ Contract.Ensures(Contract.ValueAtReturn(out x) != null);
+ Expect(1);
+ x = t;
+ if (x.val.StartsWith("\\"))
+ x.val = x.val.Substring(1);
+
+ }
+
+ void TypeArgs(List<Bpl.Type>/*!*/ ts) {
+ Contract.Requires(ts != null); IToken/*!*/ tok; Bpl.Type/*!*/ ty;
+ if (StartOf(5)) {
+ TypeAtom(out ty);
+ ts.Add(ty);
+ if (StartOf(6)) {
+ TypeArgs(ts);
+ }
+ } else if (la.kind == 1) {
+ Ident(out tok);
+ List<Bpl.Type>/*!*/ args = new List<Bpl.Type> ();
+ ts.Add(new UnresolvedTypeIdentifier (tok, tok.val, args));
+ if (StartOf(6)) {
+ TypeArgs(ts);
+ }
+ } else if (la.kind == 17 || la.kind == 19) {
+ MapType(out ty);
+ ts.Add(ty);
+ } else SynErr(102);
+ }
+
+ void MapType(out Bpl.Type/*!*/ ty) {
+ Contract.Ensures(Contract.ValueAtReturn(out ty) != null); IToken tok = null;
+ IToken/*!*/ nnTok;
+ List<Bpl.Type>/*!*/ arguments = new List<Bpl.Type>();
+ Bpl.Type/*!*/ result;
+ List<TypeVariable>/*!*/ typeParameters = new List<TypeVariable>();
+
+ if (la.kind == 19) {
+ TypeParams(out nnTok, out typeParameters);
+ tok = nnTok;
+ }
+ Expect(17);
+ if (tok == null) tok = t;
+ if (StartOf(6)) {
+ Types(arguments);
+ }
+ Expect(18);
+ Type(out result);
+ ty = new MapType(tok, typeParameters, arguments, result);
+
+ }
+
+ void TypeParams(out IToken/*!*/ tok, out List<TypeVariable>/*!*/ typeParams) {
+ Contract.Ensures(Contract.ValueAtReturn(out tok) != null); Contract.Ensures(Contract.ValueAtReturn(out typeParams) != null); List<IToken>/*!*/ typeParamToks;
+ Expect(19);
+ tok = t;
+ Idents(out typeParamToks);
+ Expect(20);
+ typeParams = new List<TypeVariable> ();
+ foreach(Token/*!*/ id in typeParamToks){
+ Contract.Assert(id != null);
+ typeParams.Add(new TypeVariable(id, id.val));}
+
+ }
+
+ void Types(List<Bpl.Type>/*!*/ ts) {
+ Contract.Requires(ts != null); Bpl.Type/*!*/ ty;
+ Type(out ty);
+ ts.Add(ty);
+ while (la.kind == 12) {
+ Get();
+ Type(out ty);
+ ts.Add(ty);
+ }
+ }
+
+ void OrderSpec(out bool ChildrenComplete, out List<ConstantParent/*!*/> Parents) {
+ Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out Parents),true)); ChildrenComplete = false;
+ Parents = null;
+ bool u;
+ IToken/*!*/ parent;
+ Expect(23);
+ Parents = new List<ConstantParent/*!*/> ();
+ u = false;
+ if (la.kind == 1 || la.kind == 22) {
+ if (la.kind == 22) {
+ Get();
+ u = true;
+ }
+ Ident(out parent);
+ Parents.Add(new ConstantParent (
+ new IdentifierExpr(parent, parent.val), u));
+ while (la.kind == 12) {
+ Get();
+ u = false;
+ if (la.kind == 22) {
+ Get();
+ u = true;
+ }
+ Ident(out parent);
+ Parents.Add(new ConstantParent (
+ new IdentifierExpr(parent, parent.val), u));
+ }
+ }
+ if (la.kind == 24) {
+ Get();
+ ChildrenComplete = true;
+ }
+ }
+
+ void VarOrType(out TypedIdent/*!*/ tyd, out QKeyValue kv) {
+ Contract.Ensures(Contract.ValueAtReturn(out tyd) != null);
+ string/*!*/ varName = TypedIdent.NoName;
+ Bpl.Type/*!*/ ty;
+ IToken/*!*/ tok;
+ kv = null;
+
+ while (la.kind == 27) {
+ Attribute(ref kv);
+ }
+ Type(out ty);
+ tok = ty.tok;
+ if (la.kind == 11) {
+ Get();
+ var uti = ty as UnresolvedTypeIdentifier;
+ if (uti != null && uti.Arguments.Count == 0) {
+ varName = uti.Name;
+ } else {
+ this.SemErr("expected identifier before ':'");
+ }
+
+ Type(out ty);
+ }
+ tyd = new TypedIdent(tok, varName, ty);
+ }
+
+ void Proposition(out Expr/*!*/ e) {
+ Contract.Ensures(Contract.ValueAtReturn(out e) != null);
+ Expression(out e);
+ }
+
+ void UserDefinedType(out Declaration/*!*/ decl, QKeyValue kv) {
+ Contract.Ensures(Contract.ValueAtReturn(out decl) != null); IToken/*!*/ id; List<IToken>/*!*/ paramTokens = new List<IToken> ();
+ Bpl.Type/*!*/ body = dummyType; bool synonym = false;
+ Ident(out id);
+ if (la.kind == 1) {
+ WhiteSpaceIdents(out paramTokens);
+ }
+ if (la.kind == 31) {
+ Get();
+ Type(out body);
+ synonym = true;
+ }
+ if (synonym) {
+ List<TypeVariable>/*!*/ typeParams = new List<TypeVariable>();
+ foreach(Token/*!*/ t in paramTokens){
+ Contract.Assert(t != null);
+ typeParams.Add(new TypeVariable(t, t.val));}
+ decl = new TypeSynonymDecl(id, id.val, typeParams, body, kv);
+ } else {
+ decl = new TypeCtorDecl(id, id.val, paramTokens.Count, kv);
+ }
+
+ }
+
+ void WhiteSpaceIdents(out List<IToken>/*!*/ xs) {
+ Contract.Ensures(Contract.ValueAtReturn(out xs) != null); IToken/*!*/ id; xs = new List<IToken>();
+ Ident(out id);
+ xs.Add(id);
+ while (la.kind == 1) {
+ Ident(out id);
+ xs.Add(id);
+ }
+ }
+
+ void ProcSignature(bool allowWhereClausesOnFormals, out IToken/*!*/ name, out List<TypeVariable>/*!*/ typeParams,
+out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
+ 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<TypeVariable>();
+ outs = new List<Variable>(); kv = null;
+ while (la.kind == 27) {
+ Attribute(ref kv);
+ }
+ Ident(out name);
+ if (la.kind == 19) {
+ TypeParams(out typeParamTok, out typeParams);
+ }
+ ProcFormals(true, allowWhereClausesOnFormals, out ins);
+ if (la.kind == 26) {
+ Get();
+ ProcFormals(false, allowWhereClausesOnFormals, out outs);
+ }
+ }
+
+ void Spec(List<Requires>/*!*/ pre, List<IdentifierExpr>/*!*/ mods, List<Ensures>/*!*/ post) {
+ Contract.Requires(pre != null); Contract.Requires(mods != null); Contract.Requires(post != null); List<IToken>/*!*/ ms;
+ if (la.kind == 34) {
+ Get();
+ if (la.kind == 1) {
+ Idents(out ms);
+ foreach(IToken/*!*/ m in ms){
+ Contract.Assert(m != null);
+ mods.Add(new IdentifierExpr(m, m.val));
+ }
+
+ }
+ Expect(8);
+ } else if (la.kind == 35) {
+ Get();
+ SpecPrePost(true, pre, post);
+ } else if (la.kind == 36 || la.kind == 37) {
+ SpecPrePost(false, pre, post);
+ } else SynErr(103);
+ }
+
+ void ImplBody(out List<Variable>/*!*/ locals, out StmtList/*!*/ stmtList) {
+ Contract.Ensures(Contract.ValueAtReturn(out locals) != null); Contract.Ensures(Contract.ValueAtReturn(out stmtList) != null); locals = new List<Variable>();
+ Expect(27);
+ while (la.kind == 7) {
+ LocalVars(locals);
+ }
+ StmtList(out stmtList);
+ }
+
+ void SpecPrePost(bool free, List<Requires>/*!*/ pre, List<Ensures>/*!*/ post) {
+ Contract.Requires(pre != null); Contract.Requires(post != null); Expr/*!*/ e; Token tok = null; QKeyValue kv = null;
+ if (la.kind == 36) {
+ Get();
+ tok = t;
+ while (la.kind == 27) {
+ Attribute(ref kv);
+ }
+ Proposition(out e);
+ Expect(8);
+ pre.Add(new Requires(tok, free, e, null, kv));
+ } else if (la.kind == 37) {
+ Get();
+ tok = t;
+ while (la.kind == 27) {
+ Attribute(ref kv);
+ }
+ Proposition(out e);
+ Expect(8);
+ post.Add(new Ensures(tok, free, e, null, kv));
+ } else SynErr(104);
+ }
+
+ void StmtList(out StmtList/*!*/ stmtList) {
+ Contract.Ensures(Contract.ValueAtReturn(out stmtList) != null); List<BigBlock/*!*/> bigblocks = new List<BigBlock/*!*/>();
+ /* built-up state for the current BigBlock: */
+ IToken startToken = null; string currentLabel = null;
+ List<Cmd> cs = null; /* invariant: startToken != null ==> cs != null */
+ /* temporary variables: */
+ IToken label; Cmd c; BigBlock b;
+ StructuredCmd ec = null; StructuredCmd/*!*/ ecn;
+ TransferCmd tc = null; TransferCmd/*!*/ tcn;
+
+ while (StartOf(7)) {
+ if (StartOf(8)) {
+ LabelOrCmd(out c, out label);
+ if (c != null) {
+ // LabelOrCmd read a Cmd
+ Contract.Assert(label == null);
+ if (startToken == null) { startToken = c.tok; cs = new List<Cmd>(); }
+ Contract.Assert(cs != null);
+ cs.Add(c);
+ } else {
+ // LabelOrCmd read a label
+ Contract.Assert(label != null);
+ if (startToken != null) {
+ Contract.Assert(cs != null);
+ // dump the built-up state into a BigBlock
+ b = new BigBlock(startToken, currentLabel, cs, null, null);
+ bigblocks.Add(b);
+ cs = null;
+ }
+ startToken = label;
+ currentLabel = label.val;
+ cs = new List<Cmd>();
+ }
+
+ } else if (la.kind == 40 || la.kind == 42 || la.kind == 45) {
+ StructuredCmd(out ecn);
+ ec = ecn;
+ if (startToken == null) { startToken = ec.tok; cs = new List<Cmd>(); }
+ Contract.Assert(cs != null);
+ b = new BigBlock(startToken, currentLabel, cs, ec, null);
+ bigblocks.Add(b);
+ startToken = null; currentLabel = null; cs = null;
+
+ } else {
+ TransferCmd(out tcn);
+ tc = tcn;
+ if (startToken == null) { startToken = tc.tok; cs = new List<Cmd>(); }
+ Contract.Assert(cs != null);
+ b = new BigBlock(startToken, currentLabel, cs, null, tc);
+ bigblocks.Add(b);
+ startToken = null; currentLabel = null; cs = null;
+
+ }
+ }
+ Expect(28);
+ IToken/*!*/ endCurly = t;
+ if (startToken == null && bigblocks.Count == 0) {
+ startToken = t; cs = new List<Cmd>();
+ }
+ if (startToken != null) {
+ Contract.Assert(cs != null);
+ b = new BigBlock(startToken, currentLabel, cs, null, null);
+ bigblocks.Add(b);
+ }
+
+ stmtList = new StmtList(bigblocks, endCurly);
+
+ }
+
+ void LabelOrCmd(out Cmd c, out IToken label) {
+ IToken/*!*/ x; Expr/*!*/ e;
+ List<IToken>/*!*/ xs;
+ List<IdentifierExpr> ids;
+ c = dummyCmd; label = null;
+ Cmd/*!*/ cn;
+ QKeyValue kv = null;
+
+ switch (la.kind) {
+ case 1: {
+ LabelOrAssign(out c, out label);
+ break;
+ }
+ case 46: {
+ Get();
+ x = t;
+ while (la.kind == 27) {
+ Attribute(ref kv);
+ }
+ Proposition(out e);
+ c = new AssertCmd(x, e, kv);
+ Expect(8);
+ break;
+ }
+ case 47: {
+ Get();
+ x = t;
+ while (la.kind == 27) {
+ Attribute(ref kv);
+ }
+ Proposition(out e);
+ c = new AssumeCmd(x, e, kv);
+ Expect(8);
+ break;
+ }
+ case 48: {
+ Get();
+ x = t;
+ Idents(out xs);
+ Expect(8);
+ ids = new List<IdentifierExpr>();
+ foreach(IToken/*!*/ y in xs){
+ Contract.Assert(y != null);
+ ids.Add(new IdentifierExpr(y, y.val));
+ }
+ c = new HavocCmd(x,ids);
+
+ break;
+ }
+ case 35: case 51: case 52: {
+ CallCmd(out cn);
+ Expect(8);
+ c = cn;
+ break;
+ }
+ case 53: {
+ ParCallCmd(out cn);
+ c = cn;
+ break;
+ }
+ case 49: {
+ Get();
+ x = t;
+ Expect(8);
+ c = new YieldCmd(x);
+ break;
+ }
+ default: SynErr(105); break;
+ }
+ }
+
+ 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 == 40) {
+ IfCmd(out ifcmd);
+ ec = ifcmd;
+ } else if (la.kind == 42) {
+ WhileCmd(out wcmd);
+ ec = wcmd;
+ } else if (la.kind == 45) {
+ BreakCmd(out bcmd);
+ ec = bcmd;
+ } else SynErr(106);
+ }
+
+ void TransferCmd(out TransferCmd/*!*/ tc) {
+ Contract.Ensures(Contract.ValueAtReturn(out tc) != null); tc = dummyTransferCmd;
+ Token y; List<IToken>/*!*/ xs;
+ List<String> ss = new List<String>();
+
+ if (la.kind == 38) {
+ Get();
+ y = t;
+ Idents(out xs);
+ foreach(IToken/*!*/ s in xs){
+ Contract.Assert(s != null);
+ ss.Add(s.val); }
+ tc = new GotoCmd(y, ss);
+
+ } else if (la.kind == 39) {
+ Get();
+ tc = new ReturnCmd(t);
+ } else SynErr(107);
+ Expect(8);
+ }
+
+ void IfCmd(out IfCmd/*!*/ ifcmd) {
+ Contract.Ensures(Contract.ValueAtReturn(out ifcmd) != null); IToken/*!*/ x;
+ Expr guard;
+ StmtList/*!*/ thn;
+ IfCmd/*!*/ elseIf; IfCmd elseIfOption = null;
+ StmtList/*!*/ els; StmtList elseOption = null;
+
+ Expect(40);
+ x = t;
+ Guard(out guard);
+ Expect(27);
+ StmtList(out thn);
+ if (la.kind == 41) {
+ Get();
+ if (la.kind == 40) {
+ IfCmd(out elseIf);
+ elseIfOption = elseIf;
+ } else if (la.kind == 27) {
+ Get();
+ StmtList(out els);
+ elseOption = els;
+ } else SynErr(108);
+ }
+ ifcmd = new IfCmd(x, guard, thn, elseIfOption, elseOption);
+ }
+
+ void WhileCmd(out WhileCmd/*!*/ wcmd) {
+ Contract.Ensures(Contract.ValueAtReturn(out wcmd) != null); IToken/*!*/ x; Token z;
+ Expr guard; Expr/*!*/ e; bool isFree;
+ List<PredicateCmd/*!*/> invariants = new List<PredicateCmd/*!*/>();
+ StmtList/*!*/ body;
+ QKeyValue kv = null;
+
+ Expect(42);
+ x = t;
+ Guard(out guard);
+ Contract.Assume(guard == null || cce.Owner.None(guard));
+ while (la.kind == 35 || la.kind == 43) {
+ isFree = false; z = la/*lookahead token*/;
+ if (la.kind == 35) {
+ Get();
+ isFree = true;
+ }
+ Expect(43);
+ while (la.kind == 27) {
+ Attribute(ref kv);
+ }
+ Expression(out e);
+ if (isFree) {
+ invariants.Add(new AssumeCmd(z, e, kv));
+ } else {
+ invariants.Add(new AssertCmd(z, e, kv));
+ }
+ kv = null;
+
+ Expect(8);
+ }
+ Expect(27);
+ StmtList(out body);
+ wcmd = new WhileCmd(x, guard, invariants, body);
+ }
+
+ void BreakCmd(out BreakCmd/*!*/ bcmd) {
+ Contract.Ensures(Contract.ValueAtReturn(out bcmd) != null); IToken/*!*/ x; IToken/*!*/ y;
+ string breakLabel = null;
+
+ Expect(45);
+ x = t;
+ if (la.kind == 1) {
+ Ident(out y);
+ breakLabel = y.val;
+ }
+ Expect(8);
+ bcmd = new BreakCmd(x, breakLabel);
+ }
+
+ void Guard(out Expr e) {
+ Expr/*!*/ ee; e = null;
+ Expect(9);
+ if (la.kind == 44) {
+ Get();
+ e = null;
+ } else if (StartOf(9)) {
+ Expression(out ee);
+ e = ee;
+ } else SynErr(109);
+ Expect(10);
+ }
+
+ void LabelOrAssign(out Cmd c, out IToken label) {
+ IToken/*!*/ id; IToken/*!*/ x, y; Expr/*!*/ e0;
+ c = dummyCmd; label = null;
+ AssignLhs/*!*/ lhs;
+ List<AssignLhs/*!*/>/*!*/ lhss;
+ List<Expr/*!*/>/*!*/ rhss;
+ List<Expr/*!*/>/*!*/ indexes;
+
+ Ident(out id);
+ x = t;
+ if (la.kind == 11) {
+ Get();
+ c = null; label = x;
+ } else if (la.kind == 12 || la.kind == 17 || la.kind == 50) {
+ lhss = new List<AssignLhs/*!*/>();
+ lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val));
+ while (la.kind == 17) {
+ MapAssignIndex(out y, out indexes);
+ lhs = new MapAssignLhs(y, lhs, indexes);
+ }
+ lhss.Add(lhs);
+ while (la.kind == 12) {
+ Get();
+ Ident(out id);
+ lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val));
+ while (la.kind == 17) {
+ MapAssignIndex(out y, out indexes);
+ lhs = new MapAssignLhs(y, lhs, indexes);
+ }
+ lhss.Add(lhs);
+ }
+ Expect(50);
+ x = t; /* use location of := */
+ Expression(out e0);
+ rhss = new List<Expr/*!*/> ();
+ rhss.Add(e0);
+ while (la.kind == 12) {
+ Get();
+ Expression(out e0);
+ rhss.Add(e0);
+ }
+ Expect(8);
+ c = new AssignCmd(x, lhss, rhss);
+ } else SynErr(110);
+ }
+
+ void CallCmd(out Cmd c) {
+ Contract.Ensures(Contract.ValueAtReturn(out c) != null);
+ IToken x;
+ bool isAsync = false;
+ bool isFree = false;
+ QKeyValue kv = null;
+ c = null;
+
+ if (la.kind == 51) {
+ Get();
+ isAsync = true;
+ }
+ if (la.kind == 35) {
+ Get();
+ isFree = true;
+ }
+ Expect(52);
+ x = t;
+ while (la.kind == 27) {
+ Attribute(ref kv);
+ }
+ CallParams(isAsync, isFree, kv, x, out c);
+
+ }
+
+ void ParCallCmd(out Cmd d) {
+ Contract.Ensures(Contract.ValueAtReturn(out d) != null);
+ IToken x;
+ QKeyValue kv = null;
+ Cmd c = null;
+ List<CallCmd> callCmds = new List<CallCmd>();
+
+ Expect(53);
+ x = t;
+ while (la.kind == 27) {
+ Attribute(ref kv);
+ }
+ CallParams(false, false, kv, x, out c);
+ callCmds.Add((CallCmd)c);
+ while (la.kind == 54) {
+ Get();
+ CallParams(false, false, kv, x, out c);
+ callCmds.Add((CallCmd)c);
+ }
+ Expect(8);
+ d = new ParCallCmd(x, callCmds, kv);
+ }
+
+ void MapAssignIndex(out IToken/*!*/ x, out List<Expr/*!*/>/*!*/ indexes) {
+ Contract.Ensures(Contract.ValueAtReturn(out x) != null); Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out indexes))); indexes = new List<Expr/*!*/> ();
+ Expr/*!*/ e;
+
+ Expect(17);
+ x = t;
+ if (StartOf(9)) {
+ Expression(out e);
+ indexes.Add(e);
+ while (la.kind == 12) {
+ Get();
+ Expression(out e);
+ indexes.Add(e);
+ }
+ }
+ Expect(18);
+ }
+
+ void CallParams(bool isAsync, bool isFree, QKeyValue kv, IToken x, out Cmd c) {
+ List<IdentifierExpr> ids = new List<IdentifierExpr>();
+ List<Expr> es = new List<Expr>();
+ Expr en;
+ IToken first;
+ IToken p;
+ c = null;
+
+ Ident(out first);
+ if (la.kind == 9) {
+ Get();
+ if (StartOf(9)) {
+ Expression(out en);
+ es.Add(en);
+ while (la.kind == 12) {
+ Get();
+ Expression(out en);
+ es.Add(en);
+ }
+ }
+ Expect(10);
+ c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync;
+ } else if (la.kind == 12 || la.kind == 50) {
+ ids.Add(new IdentifierExpr(first, first.val));
+ if (la.kind == 12) {
+ Get();
+ Ident(out p);
+ ids.Add(new IdentifierExpr(p, p.val));
+ while (la.kind == 12) {
+ Get();
+ Ident(out p);
+ ids.Add(new IdentifierExpr(p, p.val));
+ }
+ }
+ Expect(50);
+ Ident(out first);
+ Expect(9);
+ if (StartOf(9)) {
+ Expression(out en);
+ es.Add(en);
+ while (la.kind == 12) {
+ Get();
+ Expression(out en);
+ es.Add(en);
+ }
+ }
+ Expect(10);
+ c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync;
+ } else SynErr(111);
+ }
+
+ void Expressions(out List<Expr>/*!*/ es) {
+ Contract.Ensures(Contract.ValueAtReturn(out es) != null); Expr/*!*/ e; es = new List<Expr>();
+ Expression(out e);
+ es.Add(e);
+ while (la.kind == 12) {
+ Get();
+ Expression(out e);
+ es.Add(e);
+ }
+ }
+
+ 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 == 57 || la.kind == 58) {
+ ImpliesOp();
+ x = t;
+ ImpliesExpression(true, out e1);
+ e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e0, e1);
+ } else {
+ ExpliesOp();
+ if (noExplies)
+ this.SemErr("illegal mixture of ==> and <==, use parentheses to disambiguate");
+ x = t;
+ LogicalExpression(out e1);
+ e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e1, e0);
+ while (la.kind == 59 || la.kind == 60) {
+ ExpliesOp();
+ x = t;
+ LogicalExpression(out e1);
+ e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e1, e0);
+ }
+ }
+ }
+ }
+
+ void EquivOp() {
+ if (la.kind == 55) {
+ Get();
+ } else if (la.kind == 56) {
+ Get();
+ } else SynErr(112);
+ }
+
+ 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 == 61 || la.kind == 62) {
+ AndOp();
+ x = t;
+ RelationalExpression(out e1);
+ e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1);
+ while (la.kind == 61 || la.kind == 62) {
+ AndOp();
+ x = t;
+ RelationalExpression(out e1);
+ e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1);
+ }
+ } else {
+ OrOp();
+ x = t;
+ RelationalExpression(out e1);
+ e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1);
+ while (la.kind == 63 || la.kind == 64) {
+ OrOp();
+ x = t;
+ RelationalExpression(out e1);
+ e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1);
+ }
+ }
+ }
+ }
+
+ void ImpliesOp() {
+ if (la.kind == 57) {
+ Get();
+ } else if (la.kind == 58) {
+ Get();
+ } else SynErr(113);
+ }
+
+ void ExpliesOp() {
+ if (la.kind == 59) {
+ Get();
+ } else if (la.kind == 60) {
+ Get();
+ } else SynErr(114);
+ }
+
+ void RelationalExpression(out Expr/*!*/ e0) {
+ Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; BinaryOperator.Opcode op;
+ BvTerm(out e0);
+ if (StartOf(12)) {
+ RelOp(out x, out op);
+ BvTerm(out e1);
+ e0 = Expr.Binary(x, op, e0, e1);
+ }
+ }
+
+ void AndOp() {
+ if (la.kind == 61) {
+ Get();
+ } else if (la.kind == 62) {
+ Get();
+ } else SynErr(115);
+ }
+
+ void OrOp() {
+ if (la.kind == 63) {
+ Get();
+ } else if (la.kind == 64) {
+ Get();
+ } else SynErr(116);
+ }
+
+ void BvTerm(out Expr/*!*/ e0) {
+ Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1;
+ Term(out e0);
+ while (la.kind == 73) {
+ Get();
+ x = t;
+ Term(out e1);
+ e0 = new BvConcatExpr(x, e0, e1);
+ }
+ }
+
+ 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 65: {
+ Get();
+ x = t; op=BinaryOperator.Opcode.Eq;
+ break;
+ }
+ case 19: {
+ Get();
+ x = t; op=BinaryOperator.Opcode.Lt;
+ break;
+ }
+ case 20: {
+ Get();
+ x = t; op=BinaryOperator.Opcode.Gt;
+ break;
+ }
+ case 66: {
+ Get();
+ x = t; op=BinaryOperator.Opcode.Le;
+ break;
+ }
+ case 67: {
+ Get();
+ x = t; op=BinaryOperator.Opcode.Ge;
+ break;
+ }
+ case 68: {
+ Get();
+ x = t; op=BinaryOperator.Opcode.Neq;
+ break;
+ }
+ case 69: {
+ Get();
+ x = t; op=BinaryOperator.Opcode.Subtype;
+ break;
+ }
+ case 70: {
+ Get();
+ x = t; op=BinaryOperator.Opcode.Neq;
+ break;
+ }
+ case 71: {
+ Get();
+ x = t; op=BinaryOperator.Opcode.Le;
+ break;
+ }
+ case 72: {
+ Get();
+ x = t; op=BinaryOperator.Opcode.Ge;
+ break;
+ }
+ default: SynErr(117); 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 == 74 || la.kind == 75) {
+ AddOp(out x, out op);
+ Factor(out e1);
+ e0 = Expr.Binary(x, op, e0, e1);
+ }
+ }
+
+ void Factor(out Expr/*!*/ e0) {
+ Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; BinaryOperator.Opcode op;
+ Power(out e0);
+ while (StartOf(13)) {
+ MulOp(out x, out op);
+ Power(out e1);
+ e0 = Expr.Binary(x, op, e0, e1);
+ }
+ }
+
+ 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 == 74) {
+ Get();
+ x = t; op=BinaryOperator.Opcode.Add;
+ } else if (la.kind == 75) {
+ Get();
+ x = t; op=BinaryOperator.Opcode.Sub;
+ } else SynErr(118);
+ }
+
+ void Power(out Expr/*!*/ e0) {
+ Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1;
+ UnaryExpression(out e0);
+ if (la.kind == 79) {
+ Get();
+ x = t;
+ Power(out e1);
+ e0 = Expr.Binary(x, BinaryOperator.Opcode.Pow, e0, e1);
+ }
+ }
+
+ 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 == 44) {
+ Get();
+ x = t; op=BinaryOperator.Opcode.Mul;
+ } else if (la.kind == 76) {
+ Get();
+ x = t; op=BinaryOperator.Opcode.Div;
+ } else if (la.kind == 77) {
+ Get();
+ x = t; op=BinaryOperator.Opcode.Mod;
+ } else if (la.kind == 78) {
+ Get();
+ x = t; op=BinaryOperator.Opcode.RealDiv;
+ } else SynErr(119);
+ }
+
+ void UnaryExpression(out Expr/*!*/ e) {
+ Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;
+ e = dummyExpr;
+
+ if (la.kind == 75) {
+ Get();
+ x = t;
+ UnaryExpression(out e);
+ e = Expr.Unary(x, UnaryOperator.Opcode.Neg, e);
+ } else if (la.kind == 80 || la.kind == 81) {
+ NegOp();
+ x = t;
+ UnaryExpression(out e);
+ e = Expr.Unary(x, UnaryOperator.Opcode.Not, e);
+ } else if (StartOf(14)) {
+ CoercionExpression(out e);
+ } else SynErr(120);
+ }
+
+ void NegOp() {
+ if (la.kind == 80) {
+ Get();
+ } else if (la.kind == 81) {
+ Get();
+ } else SynErr(123);
+ }
+
+ void CoercionExpression(out Expr/*!*/ e) {
+ Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;
+ Bpl.Type/*!*/ coercedTo;
+ BigNum bn;
+
+ ArrayExpression(out e);
+ while (la.kind == 11) {
+ Get();
+ x = t;
+ if (StartOf(6)) {
+ Type(out coercedTo);
+ e = Expr.CoerceType(x, e, coercedTo);
+ } else if (la.kind == 3) {
+ Nat(out bn);
+ if (!(e is LiteralExpr) || !((LiteralExpr)e).isBigNum) {
+ this.SemErr("arguments of extract need to be integer literals");
+ e = new BvBounds(x, bn, BigNum.ZERO);
+ } else {
+ e = new BvBounds(x, bn, ((LiteralExpr)e).asBigNum);
+ }
+
+ } else SynErr(124);
+ }
+ }
+
+ void ArrayExpression(out Expr/*!*/ e) {
+ Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;
+ Expr/*!*/ index0 = dummyExpr; Expr/*!*/ e1;
+ bool store; bool bvExtract;
+ List<Expr>/*!*/ allArgs = dummyExprSeq;
+
+ AtomExpression(out e);
+ while (la.kind == 17) {
+ Get();
+ x = t; allArgs = new List<Expr> ();
+ allArgs.Add(e);
+ store = false; bvExtract = false;
+ if (StartOf(15)) {
+ if (StartOf(9)) {
+ Expression(out index0);
+ if (index0 is BvBounds)
+ bvExtract = true;
+ else
+ allArgs.Add(index0);
+
+ while (la.kind == 12) {
+ Get();
+ Expression(out e1);
+ if (bvExtract || e1 is BvBounds)
+ this.SemErr("bitvectors only have one dimension");
+ allArgs.Add(e1);
+
+ }
+ if (la.kind == 50) {
+ Get();
+ Expression(out e1);
+ if (bvExtract || e1 is BvBounds)
+ this.SemErr("assignment to bitvectors is not possible");
+ allArgs.Add(e1); store = true;
+
+ }
+ } else {
+ Get();
+ Expression(out e1);
+ allArgs.Add(e1); store = true;
+ }
+ }
+ Expect(18);
+ if (store)
+ e = new NAryExpr(x, new MapStore(x, allArgs.Count - 2), allArgs);
+ else if (bvExtract)
+ e = new BvExtractExpr(x, e,
+ ((BvBounds)index0).Upper.ToIntSafe,
+ ((BvBounds)index0).Lower.ToIntSafe);
+ else
+ e = new NAryExpr(x, new MapSelect(x, allArgs.Count - 1), allArgs);
+
+ }
+ }
+
+ void Nat(out BigNum n) {
+ Expect(3);
+ try {
+ n = BigNum.FromString(t.val);
+ } catch (FormatException) {
+ this.SemErr("incorrectly formatted number");
+ n = BigNum.ZERO;
+ }
+
+ }
+
+ void AtomExpression(out Expr/*!*/ e) {
+ Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; int n; BigNum bn; BigDec bd; BigFloat fp;
+ List<Expr>/*!*/ es; List<Variable>/*!*/ ds; Trigger trig;
+ List<TypeVariable>/*!*/ typeParams;
+ IdentifierExpr/*!*/ id;
+ QKeyValue kv;
+ e = dummyExpr;
+ List<Variable>/*!*/ locals;
+ List<Block/*!*/>/*!*/ blocks;
+
+ switch (la.kind) {
+ case 82: {
+ Get();
+ e = new LiteralExpr(t, false);
+ break;
+ }
+ case 83: {
+ Get();
+ e = new LiteralExpr(t, true);
+ break;
+ }
+ case 3: {
+ Nat(out bn);
+ e = new LiteralExpr(t, bn);
+ break;
+ }
+ case 5: case 6: {
+ Dec(out bd);
+ e = new LiteralExpr(t, bd);
+ break;
+ }
+ case 97: {
+ Float(out fp);
+ e = new LiteralExpr(t, fp);
+ break;
+ }
+ case 2: {
+ BvLit(out bn, out n);
+ e = new LiteralExpr(t, bn, n);
+ break;
+ }
+ case 1: {
+ Ident(out x);
+ id = new IdentifierExpr(x, x.val); e = id;
+ if (la.kind == 9) {
+ Get();
+ if (StartOf(9)) {
+ Expressions(out es);
+ e = new NAryExpr(x, new FunctionCall(id), es);
+ } else if (la.kind == 10) {
+ e = new NAryExpr(x, new FunctionCall(id), new List<Expr>());
+ } else SynErr(125);
+ Expect(10);
+ }
+ break;
+ }
+ case 84: {
+ Get();
+ x = t;
+ Expect(9);
+ Expression(out e);
+ Expect(10);
+ e = new OldExpr(x, e);
+ break;
+ }
+ case 14: {
+ Get();
+ x = t;
+ Expect(9);
+ Expression(out e);
+ Expect(10);
+ e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToInt), new List<Expr>{ e });
+ break;
+ }
+ case 15: {
+ Get();
+ x = t;
+ Expect(9);
+ Expression(out e);
+ Expect(10);
+ e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToReal), new List<Expr>{ e });
+ break;
+ }
+ case 98: {
+ Get();
+ x = t;
+ Expect(19);
+ Expression(out e);
+ Expect(20);
+ e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToFloat), new List<Expr> { e });
+ break;
+ }
+ case 9: {
+ Get();
+ if (StartOf(9)) {
+ Expression(out e);
+ if (e is BvBounds)
+ this.SemErr("parentheses around bitvector bounds " +
+ "are not allowed");
+ } else if (la.kind == 88 || la.kind == 89) {
+ 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 == 90 || la.kind == 91) {
+ 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 == 92 || la.kind == 93) {
+ Lambda();
+ x = t;
+ QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);
+ if (trig != null)
+ SemErr("triggers not allowed in lambda expressions");
+ if (typeParams.Count + ds.Count > 0)
+ e = new LambdaExpr(x, typeParams, ds, kv, e);
+ } else SynErr(126);
+ Expect(10);
+ break;
+ }
+ case 40: {
+ IfThenElseExpression(out e);
+ break;
+ }
+ case 85: {
+ CodeExpression(out locals, out blocks);
+ e = new CodeExpr(locals, blocks);
+ break;
+ }
+ default: SynErr(127); break;
+ }
+ }
+
+ void Dec(out BigDec n) {
+ string s = "";
+ if (la.kind == 5) {
+ Get();
+ s = t.val;
+ } else if (la.kind == 6) {
+ Get();
+ s = t.val;
+ } else SynErr(128);
+ try {
+ n = BigDec.FromString(s);
+ } catch (FormatException) {
+ this.SemErr("incorrectly formatted number");
+ n = BigDec.ZERO;
+ }
+
+ }
+
+ /// <summary>
+ /// Creates a floating point from the current token value
+ /// </summary>
+ /// <param name="n"></param>
+ void Float(out BigFloat n)
+ {
+ try
+ {
+ if (la.kind == 97) {
+ bool negative = false;
+ int exp, sig, size;
+ BigNum exp_val, sig_val, value;
+ //Expected format = float(sign exp_val sig_val) || float<exp sig>(value)
+ Get(); //Skip the float token
+ if (la.val == "(") {
+ Get();
+ if (la.val == "false")
+ negative = false;
+ else if (la.val == "true")
+ negative = true;
+ else
+ throw new FormatException();
+ Get();
+ Expect(12); //,
+ BvLit(out exp_val, out exp);
+ Expect(12);
+ BvLit(out sig_val, out sig);
+ n = new BigFloat(negative, exp_val, sig_val, exp, sig);
+ Expect(10); //)
+ }
+ else if (la.val == "<") {
+ Get();
+ Expect(3);
+ exp = Int32.Parse(t.val);
+ Expect(12);
+ Expect(3);
+ sig = Int32.Parse(t.val);
+ Expect(20); //>
+ Expect(9); //(
+ if (la.kind == 1) { //NaN
+ Get();
+ n = new BigFloat(t.val, exp, sig);
+ }
+ else if (la.kind == 74 || la.kind == 75) { //+ or -
+ Get();
+ String s = t.val;
+ Get();
+ n = new BigFloat(s + t.val, exp, sig);
+ }
+ else {
+ BvLit(out value, out size);
+ n = new BigFloat(value.ToString(), exp, sig);
+ }
+ Expect(10); //)
+ }
+ else {
+ throw new FormatException();
+ }
+ }
+ else {
+ n = BigFloat.ZERO(8, 24);
+ SynErr(137);
+ }
+ }
+ catch (FormatException)
+ {
+ this.SemErr("incorrectly formatted floating point");
+ n = BigFloat.ZERO(8, 24);
+ }
+ }
+
+ void BvLit(out BigNum n, out int m) {
+ Expect(2);
+ int pos = t.val.IndexOf("bv");
+ string a = t.val.Substring(0, pos);
+ string b = t.val.Substring(pos + 2);
+ try {
+ n = BigNum.FromString(a);
+ m = Convert.ToInt32(b);
+ } catch (FormatException) {
+ this.SemErr("incorrectly formatted bitvector");
+ n = BigNum.ZERO;
+ m = 0;
+ }
+
+ }
+
+ void Forall() {
+ if (la.kind == 88) {
+ Get();
+ } else if (la.kind == 89) {
+ Get();
+ } else SynErr(129);
+ }
+
+ void QuantifierBody(IToken/*!*/ q, out List<TypeVariable>/*!*/ typeParams, out List<Variable>/*!*/ ds,
+out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
+ Contract.Requires(q != null); Contract.Ensures(Contract.ValueAtReturn(out typeParams) != null); Contract.Ensures(Contract.ValueAtReturn(out ds) != null); Contract.Ensures(Contract.ValueAtReturn(out body) != null);
+ trig = null; typeParams = new List<TypeVariable> ();
+ IToken/*!*/ tok;
+ kv = null;
+ ds = new List<Variable> ();
+
+ if (la.kind == 19) {
+ TypeParams(out tok, out typeParams);
+ if (la.kind == 1 || la.kind == 27) {
+ BoundVars(q, out ds);
+ }
+ } else if (la.kind == 1 || la.kind == 27) {
+ BoundVars(q, out ds);
+ } else SynErr(130);
+ QSep();
+ while (la.kind == 27) {
+ AttributeOrTrigger(ref kv, ref trig);
+ }
+ Expression(out body);
+ }
+
+ void Exists() {
+ if (la.kind == 90) {
+ Get();
+ } else if (la.kind == 91) {
+ Get();
+ } else SynErr(131);
+ }
+
+ void Lambda() {
+ if (la.kind == 92) {
+ Get();
+ } else if (la.kind == 93) {
+ Get();
+ } else SynErr(132);
+ }
+
+ void IfThenElseExpression(out Expr/*!*/ e) {
+ Contract.Ensures(Contract.ValueAtReturn(out e) != null);
+ IToken/*!*/ tok;
+ Expr/*!*/ e0, e1, e2;
+ e = dummyExpr;
+ Expect(40);
+ tok = t;
+ Expression(out e0);
+ Expect(87);
+ Expression(out e1);
+ Expect(41);
+ Expression(out e2);
+ e = new NAryExpr(tok, new IfThenElse(tok), new List<Expr>{ e0, e1, e2 });
+ }
+
+ void CodeExpression(out List<Variable>/*!*/ locals, out List<Block/*!*/>/*!*/ blocks) {
+ Contract.Ensures(Contract.ValueAtReturn(out locals) != null); Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out blocks))); locals = new List<Variable>(); Block/*!*/ b;
+ blocks = new List<Block/*!*/>();
+
+ Expect(85);
+ while (la.kind == 7) {
+ LocalVars(locals);
+ }
+ SpecBlock(out b);
+ blocks.Add(b);
+ while (la.kind == 1) {
+ SpecBlock(out b);
+ blocks.Add(b);
+ }
+ Expect(86);
+ }
+
+ void SpecBlock(out Block/*!*/ b) {
+ Contract.Ensures(Contract.ValueAtReturn(out b) != null); IToken/*!*/ x; IToken/*!*/ y;
+ Cmd c; IToken label;
+ List<Cmd> cs = new List<Cmd>();
+ List<IToken>/*!*/ xs;
+ List<String> ss = new List<String>();
+ b = dummyBlock;
+ Expr/*!*/ e;
+
+ Ident(out x);
+ Expect(11);
+ while (StartOf(8)) {
+ LabelOrCmd(out c, out label);
+ if (c != null) {
+ Contract.Assert(label == null);
+ cs.Add(c);
+ } else {
+ Contract.Assert(label != null);
+ SemErr("SpecBlock's can only have one label");
+ }
+
+ }
+ if (la.kind == 38) {
+ Get();
+ y = t;
+ Idents(out xs);
+ foreach(IToken/*!*/ s in xs){
+ Contract.Assert(s != null);
+ ss.Add(s.val); }
+ b = new Block(x,x.val,cs,new GotoCmd(y,ss));
+
+ } else if (la.kind == 39) {
+ Get();
+ Expression(out e);
+ b = new Block(x,x.val,cs,new ReturnExprCmd(t,e));
+ } else SynErr(133);
+ Expect(8);
+ }
+
+ void AttributeOrTrigger(ref QKeyValue kv, ref Trigger trig) {
+ IToken/*!*/ tok; Expr/*!*/ e; List<Expr>/*!*/ es;
+ string key;
+ List<object/*!*/> parameters; object/*!*/ param;
+
+ Expect(27);
+ tok = t;
+ if (la.kind == 11) {
+ Get();
+ Expect(1);
+ key = t.val; parameters = new List<object/*!*/>();
+ if (StartOf(16)) {
+ AttributeParameter(out param);
+ parameters.Add(param);
+ while (la.kind == 12) {
+ Get();
+ AttributeParameter(out param);
+ parameters.Add(param);
+ }
+ }
+ if (key == "nopats") {
+ if (parameters.Count == 1 && parameters[0] is Expr) {
+ e = (Expr)parameters[0];
+ if(trig==null){
+ trig = new Trigger(tok, false, new List<Expr> { e }, null);
+ } else {
+ trig.AddLast(new Trigger(tok, false, new List<Expr> { e }, null));
+ }
+ } else {
+ this.SemErr("the 'nopats' quantifier attribute expects a string-literal parameter");
+ }
+ } else {
+ if (kv==null) {
+ kv = new QKeyValue(tok, key, parameters, null);
+ } else {
+ kv.AddLast(new QKeyValue(tok, key, parameters, null));
+ }
+ }
+
+ } else if (StartOf(9)) {
+ Expression(out e);
+ es = new List<Expr> { e };
+ while (la.kind == 12) {
+ Get();
+ Expression(out e);
+ es.Add(e);
+ }
+ if (trig==null) {
+ trig = new Trigger(tok, true, es, null);
+ } else {
+ trig.AddLast(new Trigger(tok, true, es, null));
+ }
+
+ } else SynErr(134);
+ Expect(28);
+ }
+
+ void AttributeParameter(out object/*!*/ o) {
+ Contract.Ensures(Contract.ValueAtReturn(out o) != null);
+ o = "error";
+ Expr/*!*/ e;
+
+ if (la.kind == 4) {
+ Get();
+ o = t.val.Substring(1, t.val.Length-2);
+ } else if (StartOf(9)) {
+ Expression(out e);
+ o = e;
+ } else SynErr(135);
+ }
+
+ void QSep() {
+ if (la.kind == 94) {
+ Get();
+ } else if (la.kind == 95) {
+ Get();
+ } else SynErr(136);
+ }
+
+
+
+ public void Parse() {
+ la = new Token();
+ la.val = "";
+ Get();
+ BoogiePL();
+ Expect(0);
+
+ Expect(0);
+ }
+
+ static readonly bool[,]/*!*/ set = { //grid is 17 x 100
+ {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,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,T,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,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,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,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,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,T,x},
+ {x,T,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,T,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,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,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,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,T,T,T, x,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,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,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,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,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, 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,T,T,T, x,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,x,x, x,x,x,x, x,x,x,x, x,T,x,x},
+ {x,T,T,T, x,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,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+ {x,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,x,x, x,x,x,x, x,x,x,x, x,x,x,x}
+
+ };
+} // end Parser
+
+
+public class Errors {
+ public int count = 0; // number of errors detected
+ public System.IO.TextWriter/*!*/ errorStream = Console.Out; // error messages go to this stream
+ public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text
+ public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text
+
+ public void SynErr(string filename, int line, int col, int n) {
+ SynErr(filename, line, col, GetSyntaxErrorString(n));
+ }
+
+ public virtual void SynErr(string filename, int line, int col, string/*!*/ msg) {
+ Contract.Requires(msg != null);
+ errorStream.WriteLine(errMsgFormat, filename, line, col, msg);
+ count++;
+ }
+
+ /// <summary>
+ /// Returns a string corresponding to the syntax error of the given type
+ /// Note that many of these errors (0-98) correspond to token types (e.g. the la token)
+ /// </summary>
+ /// <param name="n"></param>
+ /// <returns></returns>
+ string GetSyntaxErrorString(int n) {
+ string s;
+ switch (n) {
+ case 0: s = "EOF expected"; break;
+ case 1: s = "ident expected"; break;
+ case 2: s = "bvlit expected"; break;
+ case 3: s = "digits expected"; break;
+ case 4: s = "string expected"; break;
+ case 5: s = "decimal expected"; break;
+ case 6: s = "float expected"; break;
+ case 7: s = "\"var\" expected"; break;
+ case 8: s = "\";\" expected"; break;
+ case 9: s = "\"(\" expected"; break;
+ case 10: s = "\")\" expected"; break;
+ case 11: s = "\":\" expected"; break;
+ case 12: s = "\",\" expected"; break;
+ case 13: s = "\"where\" expected"; break;
+ case 14: s = "\"int\" expected"; break;
+ case 15: s = "\"real\" expected"; break;
+ case 16: s = "\"bool\" expected"; break;
+ case 17: s = "\"[\" expected"; break;
+ case 18: s = "\"]\" expected"; break;
+ case 19: s = "\"<\" expected"; break;
+ case 20: s = "\">\" expected"; break;
+ case 21: s = "\"const\" expected"; break;
+ case 22: s = "\"unique\" expected"; break;
+ case 23: s = "\"extends\" expected"; break;
+ case 24: s = "\"complete\" expected"; break;
+ case 25: s = "\"function\" expected"; break;
+ case 26: s = "\"returns\" expected"; break;
+ case 27: s = "\"{\" expected"; break;
+ case 28: s = "\"}\" expected"; break;
+ case 29: s = "\"axiom\" expected"; break;
+ case 30: s = "\"type\" expected"; break;
+ case 31: s = "\"=\" expected"; break;
+ case 32: s = "\"procedure\" expected"; break;
+ case 33: s = "\"implementation\" expected"; break;
+ case 34: s = "\"modifies\" expected"; break;
+ case 35: s = "\"free\" expected"; break;
+ case 36: s = "\"requires\" expected"; break;
+ case 37: s = "\"ensures\" expected"; break;
+ case 38: s = "\"goto\" expected"; break;
+ case 39: s = "\"return\" expected"; break;
+ case 40: s = "\"if\" expected"; break;
+ case 41: s = "\"else\" expected"; break;
+ case 42: s = "\"while\" expected"; break;
+ case 43: s = "\"invariant\" expected"; break;
+ case 44: s = "\"*\" expected"; break;
+ case 45: s = "\"break\" expected"; break;
+ case 46: s = "\"assert\" expected"; break;
+ case 47: s = "\"assume\" expected"; break;
+ case 48: s = "\"havoc\" expected"; break;
+ case 49: s = "\"yield\" expected"; break;
+ case 50: s = "\":=\" expected"; break;
+ case 51: s = "\"async\" expected"; break;
+ case 52: s = "\"call\" expected"; break;
+ case 53: s = "\"par\" expected"; break;
+ case 54: s = "\"|\" expected"; break;
+ case 55: s = "\"<==>\" expected"; break;
+ case 56: s = "\"\\u21d4\" expected"; break;
+ case 57: s = "\"==>\" expected"; break;
+ case 58: s = "\"\\u21d2\" expected"; break;
+ case 59: s = "\"<==\" expected"; break;
+ case 60: s = "\"\\u21d0\" expected"; break;
+ case 61: s = "\"&&\" expected"; break;
+ case 62: s = "\"\\u2227\" expected"; break;
+ case 63: s = "\"||\" expected"; break;
+ case 64: s = "\"\\u2228\" expected"; break;
+ case 65: s = "\"==\" 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 = "\"\\u2260\" expected"; break;
+ case 71: s = "\"\\u2264\" expected"; break;
+ case 72: s = "\"\\u2265\" expected"; break;
+ case 73: s = "\"++\" expected"; break;
+ case 74: s = "\"+\" expected"; break;
+ case 75: s = "\"-\" expected"; break;
+ case 76: s = "\"div\" expected"; break;
+ case 77: s = "\"mod\" expected"; break;
+ case 78: s = "\"/\" expected"; break;
+ case 79: s = "\"**\" expected"; break;
+ case 80: s = "\"!\" expected"; break;
+ case 81: s = "\"\\u00ac\" expected"; break;
+ case 82: s = "\"false\" expected"; break;
+ case 83: s = "\"true\" expected"; break;
+ case 84: s = "\"old\" expected"; break;
+ case 85: s = "\"|{\" expected"; break;
+ case 86: s = "\"}|\" expected"; break;
+ case 87: s = "\"then\" expected"; break;
+ case 88: s = "\"forall\" expected"; break;
+ case 89: s = "\"\\u2200\" expected"; break;
+ case 90: s = "\"exists\" expected"; break;
+ case 91: s = "\"\\u2203\" expected"; break;
+ case 92: s = "\"lambda\" expected"; break;
+ case 93: s = "\"\\u03bb\" expected"; break;
+ case 94: s = "\"::\" expected"; break;
+ case 95: s = "\"\\u2022\" expected"; break;
+ case 96: s = "??? expected"; break;
+ case 97: s = "fp expected"; break;
+ case 98: s = "\"float\" expected"; break;
+ case 99: s = "invalid Function"; break;
+ case 100: s = "invalid Function"; break;
+ case 101: s = "invalid Procedure"; break;
+ case 102: s = "invalid Type"; break;
+ case 103: s = "invalid TypeAtom"; break;
+ case 104: s = "invalid TypeArgs"; break;
+ case 105: s = "invalid Spec"; break;
+ case 106: s = "invalid SpecPrePost"; break;
+ case 107: s = "invalid LabelOrCmd"; break;
+ case 108: s = "invalid StructuredCmd"; break;
+ case 109: s = "invalid TransferCmd"; break;
+ case 110: s = "invalid IfCmd"; break;
+ case 111: s = "invalid Guard"; break;
+ case 112: s = "invalid LabelOrAssign"; break;
+ case 113: s = "invalid CallParams"; break;
+ case 114: s = "invalid EquivOp"; break;
+ case 115: s = "invalid ImpliesOp"; break;
+ case 116: s = "invalid ExpliesOp"; break;
+ case 117: s = "invalid AndOp"; break;
+ case 118: s = "invalid OrOp"; break;
+ case 119: s = "invalid RelOp"; break;
+ case 120: s = "invalid AddOp"; break;
+ case 121: s = "invalid MulOp"; break;
+ case 122: s = "invalid UnaryExpression"; break;
+ case 123: s = "invalid NegOp"; break;
+ case 124: s = "invalid CoercionExpression"; break;
+ case 125: s = "invalid AtomExpression"; break;
+ case 126: s = "invalid AtomExpression"; break;
+ case 127: s = "invalid AtomExpression"; break;
+ case 128: s = "invalid Dec"; break;
+ case 129: s = "invalid Forall"; break;
+ case 130: s = "invalid QuantifierBody"; break;
+ case 131: s = "invalid Exists"; break;
+ case 132: s = "invalid Lambda"; break;
+ case 133: s = "invalid SpecBlock"; break;
+ case 134: s = "invalid AttributeOrTrigger"; break;
+ case 135: s = "invalid AttributeParameter"; break;
+ case 136: s = "invalid QSep"; break;
+ case 137: s = "invalid Float"; break;
+
+ default: s = "error " + n; break;
+ }
+ return s;
+ }
+
+ public void SemErr(IToken/*!*/ tok, string/*!*/ msg) { // semantic errors
+ Contract.Requires(tok != null);
+ Contract.Requires(msg != null);
+ SemErr(tok.filename, tok.line, tok.col, msg);
+ }
+
+ public virtual void SemErr(string filename, int line, int col, string/*!*/ msg) {
+ Contract.Requires(msg != null);
+ errorStream.WriteLine(errMsgFormat, filename, line, col, msg);
+ count++;
+ }
+
+ public void Warning(IToken/*!*/ tok, string/*!*/ msg) { // warnings
+ Contract.Requires(tok != null);
+ Contract.Requires(msg != null);
+ Warning(tok.filename, tok.line, tok.col, msg);
+ }
+
+ public virtual void Warning(string filename, int line, int col, string msg) {
+ Contract.Requires(msg != null);
+ errorStream.WriteLine(warningMsgFormat, filename, line, col, msg);
+ }
+} // Errors
+
+
+public class FatalError: Exception {
+ public FatalError(string m): base(m) {}
+}
+
+
} \ No newline at end of file
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 03:58:30 +0000