summaryrefslogtreecommitdiff
path: root/Source/Core/BoogiePL.atg
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Core/BoogiePL.atg')
-rw-r--r--Source/Core/BoogiePL.atg3022
1 files changed, 1511 insertions, 1511 deletions
diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg
index 644a5d3d..091ceeb0 100644
--- a/Source/Core/BoogiePL.atg
+++ b/Source/Core/BoogiePL.atg
@@ -1,1511 +1,1511 @@
-
-/*---------------------------------------------------------------------------
-// BoogiePL -
-//--------------------------------------------------------------------------*/
-
-/*using System;*/
-using System.Collections;
-using System.Collections.Generic;
-using System.IO;
-using System.Text;
-using Microsoft.Boogie;
-using Microsoft.Basetypes;
-using Bpl = Microsoft.Boogie;
-
-
-COMPILER BoogiePL
-
-/*--------------------------------------------------------------------------*/
-
-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) {
- 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(); }
-}
-
-/*--------------------------------------------------------------------------*/
-CHARACTERS
- letter = "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz".
- digit = "0123456789".
- special = "'~#$^_.?`".
- glyph = "`~!@#$%^&*()-_=+[{]}|;:',<.>/?\\".
-
- cr = '\r'.
- lf = '\n'.
- tab = '\t'.
-
- space = ' '.
- quote = '"'.
-
- newLine = cr + lf.
- regularStringChar = ANY - quote - newLine.
-
- nondigit = letter + special.
- nonquote = letter + digit + space + glyph.
-
-
-/*------------------------------------------------------------------------*/
-TOKENS
- ident = [ '\\' ] nondigit {nondigit | digit}.
- bvlit = digit {digit} 'b' 'v' digit {digit}.
- digits = digit {digit}.
-
- string = quote { regularStringChar | "\\\"" } quote.
-
- decimal = digit {digit} 'e' [ '-' ] digit {digit} .
- float = digit {digit} '.' digit {digit} [ 'e' [ '-' ] digit {digit} ] .
-
-COMMENTS FROM "/*" TO "*/" NESTED
-COMMENTS FROM "//" TO lf
-
-IGNORE cr + lf + tab
-
-
-/*------------------------------------------------------------------------*/
-PRODUCTIONS
-
-
-/*------------------------------------------------------------------------*/
-BoogiePL
-= (. List<Variable>/*!*/ vs;
- List<Declaration>/*!*/ ds;
- Axiom/*!*/ ax;
- List<Declaration/*!*/>/*!*/ ts;
- Procedure/*!*/ pr;
- Implementation im;
- Implementation/*!*/ nnim;
- .)
- { Consts<out vs> (. foreach(Bpl.Variable/*!*/ v in vs){
- Contract.Assert(v != null);
- Pgm.AddTopLevelDeclaration(v);
- }
- .)
- | Function<out ds> (. foreach(Bpl.Declaration/*!*/ d in ds){
- Contract.Assert(d != null);
- Pgm.AddTopLevelDeclaration(d);
- }
- .)
- | Axiom<out ax> (. Pgm.AddTopLevelDeclaration(ax); .)
- | UserDefinedTypes<out ts> (. foreach(Declaration/*!*/ td in ts){
- Contract.Assert(td != null);
- Pgm.AddTopLevelDeclaration(td);
- }
- .)
- | GlobalVars<out vs> (. foreach(Bpl.Variable/*!*/ v in vs){
- Contract.Assert(v != null);
- Pgm.AddTopLevelDeclaration(v);
- }
- .)
- | Procedure<out pr, out im> (. Pgm.AddTopLevelDeclaration(pr);
- if (im != null) {
- Pgm.AddTopLevelDeclaration(im);
- }
- .)
- | Implementation<out nnim> (. Pgm.AddTopLevelDeclaration(nnim); .)
- }
- EOF
- .
-
-/*------------------------------------------------------------------------*/
-GlobalVars<.out List<Variable>/*!*/ ds.>
-= (.
- Contract.Ensures(Contract.ValueAtReturn(out ds) != null);
- QKeyValue kv = null;
- ds = new List<Variable>();
- var dsx = ds;
- .)
- "var"
- { Attribute<ref kv> }
- IdsTypeWheres<true, "global variables", delegate(TypedIdent tyd) { dsx.Add(new GlobalVariable(tyd.tok, tyd, kv)); } > ";"
- .
-
-LocalVars<.List<Variable>/*!*/ ds.>
-= (.
- Contract.Ensures(Contract.ValueAtReturn(out ds) != null);
- QKeyValue kv = null;
- .)
- "var"
- { Attribute<ref kv> }
- IdsTypeWheres<true, "local variables", delegate(TypedIdent tyd) { ds.Add(new LocalVariable(tyd.tok, tyd, kv)); } > ";"
- .
-
-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";
- .)
- "("
- [ AttrsIdsTypeWheres<allowWhereClauses, allowWhereClauses, context, delegate(TypedIdent tyd, QKeyValue kv) { dsx.Add(new Formal(tyd.tok, tyd, incoming, kv)); }>
- ]
- ")"
- .
-
-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)); } >
- .
-
-/*------------------------------------------------------------------------*/
-/* IdsType is used with const declarations */
-IdsType<.out List<TypedIdent>/*!*/ tyds.>
-= (. Contract.Ensures(Contract.ValueAtReturn(out tyds) != null); List<IToken>/*!*/ ids; Bpl.Type/*!*/ ty; .)
- Idents<out ids> ":" 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));
- }
- .)
- .
-
-/* AttrsIdsTypeWheres is used with the declarations of formals and bound variables */
-AttrsIdsTypeWheres<. bool allowAttributes, bool allowWhereClauses, string context, System.Action<TypedIdent, QKeyValue> action .>
-=
- AttributesIdsTypeWhere<allowAttributes, allowWhereClauses, context, action>
- { "," AttributesIdsTypeWhere<allowAttributes, allowWhereClauses, context, action> }
- .
-
-IdsTypeWheres<. bool allowWhereClauses, string context, System.Action<TypedIdent> action .>
-=
- IdsTypeWhere<allowWhereClauses, context, action>
- { "," IdsTypeWhere<allowWhereClauses, context, action> }
- .
-
-AttributesIdsTypeWhere<. bool allowAttributes, bool allowWhereClauses, string context, System.Action<TypedIdent, QKeyValue> action .>
-= (. QKeyValue kv = null; .)
- { Attribute<ref kv> (. if (!allowAttributes) {
- kv = null;
- this.SemErr("attributes are not allowed on " + context);
- }
- .)
- }
- IdsTypeWhere<allowWhereClauses, context, delegate(TypedIdent tyd) { action(tyd, kv); }>
- .
-
-/* context is allowed to be null if allowWhereClauses is true */
-IdsTypeWhere<. bool allowWhereClauses, string context, System.Action<TypedIdent> action .>
-= (. List<IToken>/*!*/ ids; Bpl.Type/*!*/ ty; Expr wh = null; Expr/*!*/ nne; .)
- Idents<out ids> ":" Type<out ty>
- [ "where" 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));
- }
- .)
- .
-
-/*------------------------------------------------------------------------*/
-Type<out Bpl.Type/*!*/ ty>
-= (.Contract.Ensures(Contract.ValueAtReturn(out ty) != null); IToken/*!*/ tok; ty = dummyType; .)
- (
- TypeAtom<out ty>
- |
- Ident<out tok> (. List<Bpl.Type>/*!*/ args = new List<Bpl.Type> (); .)
- [ TypeArgs<args> ] (. ty = new UnresolvedTypeIdentifier (tok, tok.val, args); .)
- |
- MapType<out ty>
- )
- .
-
-TypeArgs<.List<Bpl.Type>/*!*/ ts.>
-= (.Contract.Requires(ts != null); IToken/*!*/ tok; Bpl.Type/*!*/ ty; .)
- (
- TypeAtom<out ty> (. ts.Add(ty); .)
- [ TypeArgs<ts> ]
- |
- Ident<out tok> (. List<Bpl.Type>/*!*/ args = new List<Bpl.Type> ();
- ts.Add(new UnresolvedTypeIdentifier (tok, tok.val, args)); .)
- [ TypeArgs<ts> ]
- |
- MapType<out ty> (. ts.Add(ty); .)
- )
- .
-
-TypeAtom<out Bpl.Type/*!*/ ty>
-= (.Contract.Ensures(Contract.ValueAtReturn(out ty) != null); ty = dummyType; .)
- ( "int" (. ty = new BasicType(t, SimpleType.Int); .)
- | "real" (. ty = new BasicType(t, SimpleType.Real); .)
- | "bool" (. ty = new BasicType(t, SimpleType.Bool); .)
- /* note: bitvectors are handled in UnresolvedTypeIdentifier */
- |
- "("
- Type<out ty>
- ")"
- )
- .
-
-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>();
- .)
- [ TypeParams<out nnTok, out typeParameters> (. tok = nnTok; .) ]
- "[" (. if (tok == null) tok = t; .)
- [ Types<arguments> ]
- "]"
- Type<out result>
- (.
- ty = new MapType(tok, typeParameters, arguments, result);
- .)
- .
-
-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; .)
- "<" (. tok = t; .)
- Idents<out typeParamToks>
- ">"
- (.
- typeParams = new List<TypeVariable> ();
- foreach(Token/*!*/ id in typeParamToks){
- Contract.Assert(id != null);
- typeParams.Add(new TypeVariable(id, id.val));}
- .)
- .
-
-Types<.List<Bpl.Type>/*!*/ ts.>
-= (. Contract.Requires(ts != null); Bpl.Type/*!*/ ty; .)
- Type<out ty> (. ts.Add(ty); .)
- { "," Type<out ty> (. ts.Add(ty); .)
- }
- .
-
-
-/*------------------------------------------------------------------------*/
-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; .)
- "const" (. y = t; .)
- { Attribute<ref kv> }
- [ "unique" (. u = true; .)
- ]
- IdsType<out xs>
- [ 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));
- }
- .)
- ";"
- .
-
-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; .)
- "extends" (. Parents = new List<ConstantParent/*!*/> ();
- u = false; .)
- [
- [ "unique" (. u = true; .)
- ]
- Ident<out parent> (. Parents.Add(new ConstantParent (
- new IdentifierExpr(parent, parent.val), u)); .)
- {
- "," (. u = false; .)
- [ "unique" (. u = true; .)
- ]
- Ident<out parent> (. Parents.Add(new ConstantParent (
- new IdentifierExpr(parent, parent.val), u)); .)
- }
- ]
- [ "complete" (. ChildrenComplete = true; .)
- ]
- .
-
-/*------------------------------------------------------------------------*/
-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;
- .)
- "function" { Attribute<ref kv> } Ident<out z>
- [ TypeParams<out typeParamTok, out typeParams> ]
- "("
- [ VarOrType<out tyd, out argKv> (. arguments.Add(new Formal(tyd.tok, tyd, true, argKv)); .)
- { "," VarOrType<out tyd, out argKv> (. arguments.Add(new Formal(tyd.tok, tyd, true, argKv)); .)
- } ] ")"
- (. argKv = null; .)
- (
- "returns" "(" VarOrType<out retTyd, out argKv> ")"
- |
- ":" Type<out retTy> (. retTyd = new TypedIdent(retTy.tok, TypedIdent.NoName, retTy); .)
- )
- ( "{" Expression<out tmp> (. definition = tmp; .) "}" | ";" )
- (.
- 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));
- }
- }
- .)
- .
-
-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;
- .)
- { Attribute<ref kv> }
- Type<out ty> (. tok = ty.tok; .)
- [ ":" (. 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); .)
- .
-
-/*------------------------------------------------------------------------*/
-Axiom<out Axiom/*!*/ m>
-= (.Contract.Ensures(Contract.ValueAtReturn(out m) != null); Expr/*!*/ e; QKeyValue kv = null; .)
- "axiom"
- { Attribute<ref kv> }
- (. IToken/*!*/ x = t; .)
- Proposition<out e> ";" (. m = new Axiom(x,e, null, kv); .)
- .
-
-/*------------------------------------------------------------------------*/
-UserDefinedTypes<.out List<Declaration/*!*/>/*!*/ ts.>
-= (. Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out ts))); Declaration/*!*/ decl; QKeyValue kv = null; ts = new List<Declaration/*!*/> (); .)
- "type"
- { Attribute<ref kv> }
- UserDefinedType<out decl, kv> (. ts.Add(decl); .)
- { "," UserDefinedType<out decl, kv> (. ts.Add(decl); .) }
- ";"
- .
-
-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>
- [ WhiteSpaceIdents<out paramTokens> ]
- [
- "=" 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);
- }
- .)
- .
-
-
-/*------------------------------------------------------------------------*/
-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;
- .)
-
- "procedure"
- ProcSignature<true, out x, out typeParams, out ins, out outs, out kv>
- ( ";"
- { Spec<pre, mods, post> }
- | { 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);
- .)
- )
- (. proc = new Procedure(x, x.val, typeParams, ins, outs, pre, mods, post, kv); .)
- .
-
-
-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;
- .)
-
- "implementation"
- 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); .)
- .
-
-
-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; .)
- { Attribute<ref kv> }
- Ident<out name>
- [ TypeParams<out typeParamTok, out typeParams> ]
- ProcFormals<true, allowWhereClausesOnFormals, out ins>
- [ "returns" ProcFormals<false, allowWhereClausesOnFormals, out outs> ]
- .
-
-
-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; .)
- ( "modifies"
- [ Idents<out ms> (. foreach(IToken/*!*/ m in ms){
- Contract.Assert(m != null);
- mods.Add(new IdentifierExpr(m, m.val));
- }
- .)
- ] ";"
- | "free" SpecPrePost<true, pre, post>
- | SpecPrePost<false, pre, post>
- )
- .
-
-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; .)
- ( "requires" (. tok = t; .)
- { Attribute<ref kv> }
- Proposition<out e> ";" (. pre.Add(new Requires(tok, free, e, null, kv)); .)
- | "ensures" (. tok = t; .)
- { Attribute<ref kv> }
- Proposition<out e> ";" (. post.Add(new Ensures(tok, free, e, null, kv)); .)
- )
- .
-
-/*------------------------------------------------------------------------*/
-
-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>(); .)
- "{"
- { LocalVars<locals> }
- StmtList<out stmtList>
- .
-
-/* the StmtList also reads the final curly brace */
-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;
- .)
-
- {
- ( 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>();
- }
- .)
-
- | 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;
- .)
-
- | 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;
- .)
-
- )
- }
- "}"
- (. 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);
- .)
- .
-
-TransferCmd<out TransferCmd/*!*/ tc>
-= (. Contract.Ensures(Contract.ValueAtReturn(out tc) != null); tc = dummyTransferCmd;
- Token y; List<IToken>/*!*/ xs;
- List<String> ss = new List<String>();
- .)
- ( "goto" (. y = t; .)
- Idents<out xs> (. foreach(IToken/*!*/ s in xs){
- Contract.Assert(s != null);
- ss.Add(s.val); }
- tc = new GotoCmd(y, ss);
- .)
- | "return" (. tc = new ReturnCmd(t); .)
- ) ";"
- .
-
-StructuredCmd<out StructuredCmd/*!*/ ec>
-= (. Contract.Ensures(Contract.ValueAtReturn(out ec) != null); ec = dummyStructuredCmd; Contract.Assume(cce.IsPeerConsistent(ec));
- IfCmd/*!*/ ifcmd; WhileCmd/*!*/ wcmd; BreakCmd/*!*/ bcmd;
- .)
- ( IfCmd<out ifcmd> (. ec = ifcmd; .)
- | WhileCmd<out wcmd> (. ec = wcmd; .)
- | BreakCmd<out bcmd> (. ec = bcmd; .)
- )
- .
-
-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;
- .)
- "if" (. x = t; .)
- Guard<out guard>
- "{" StmtList<out thn>
- [ "else"
- ( IfCmd<out elseIf> (. elseIfOption = elseIf; .)
- | "{"
- StmtList<out els> (. elseOption = els; .)
- )
- ]
- (. ifcmd = new IfCmd(x, guard, thn, elseIfOption, elseOption); .)
- .
-
-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;
- .)
- "while" (. x = t; .)
- Guard<out guard> (. Contract.Assume(guard == null || cce.Owner.None(guard)); .)
- { (. isFree = false; z = la/*lookahead token*/; .)
- [ "free" (. isFree = true; .)
- ]
- "invariant"
- { 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;
- .)
- ";"
- }
- "{"
- StmtList<out body> (. wcmd = new WhileCmd(x, guard, invariants, body); .)
- .
-
-Guard<out Expr e>
-= (. Expr/*!*/ ee; e = null; .)
- "("
- ( "*" (. e = null; .)
- | Expression<out ee> (. e = ee; .)
- )
- ")"
- .
-
-BreakCmd<out BreakCmd/*!*/ bcmd>
-= (.Contract.Ensures(Contract.ValueAtReturn(out bcmd) != null); IToken/*!*/ x; IToken/*!*/ y;
- string breakLabel = null;
- .)
- "break" (. x = t; .)
- [ Ident<out y> (. breakLabel = y.val; .)
- ] ";" (. bcmd = new BreakCmd(x, breakLabel); .)
- .
-
-/*------------------------------------------------------------------------*/
-
-LabelOrCmd<out Cmd c, out IToken label>
-/* ensures (c == null) != (label != null) */
-= (. IToken/*!*/ x; Expr/*!*/ e;
- List<IToken>/*!*/ xs;
- List<IdentifierExpr> ids;
- c = dummyCmd; label = null;
- Cmd/*!*/ cn;
- QKeyValue kv = null;
- .)
- ( LabelOrAssign<out c, out label>
- | "assert" (. x = t; .)
- { Attribute<ref kv> }
- Proposition<out e> (. c = new AssertCmd(x, e, kv); .)
- ";"
- | "assume" (. x = t; .)
- { Attribute<ref kv> }
- Proposition<out e> (. c = new AssumeCmd(x, e, kv); .)
- ";"
- | "havoc" (. x = t; .)
- Idents<out xs> ";" (. 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);
- .)
- | CallCmd<out cn> ";" (. c = cn; .)
- | ParCallCmd<out cn> (. c = cn; .)
- | "yield" (. x = t; .)
- ";" (. c = new YieldCmd(x); .)
- )
- .
-
-/*------------------------------------------------------------------------*/
-
-LabelOrAssign<out Cmd c, out IToken label>
-/* ensures (c == null) != (label != null) */
-= (. 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; .)
- ( ":" (. c = null; label = x; .)
-
- | (. lhss = new List<AssignLhs/*!*/>(); .)
- (. lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val)); .)
-
- { MapAssignIndex<out y, out indexes> (. lhs = new MapAssignLhs(y, lhs, indexes); .) }
- (. lhss.Add(lhs); .)
-
- { ","
- Ident<out id>
- (. lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val)); .)
- { MapAssignIndex<out y, out indexes> (. lhs = new MapAssignLhs(y, lhs, indexes); .) }
- (. lhss.Add(lhs); .)
- }
-
- ":=" (. x = t; /* use location of := */ .)
- Expression<out e0> (. rhss = new List<Expr/*!*/> ();
- rhss.Add(e0); .)
- { ","
- Expression<out e0> (. rhss.Add(e0); .)
- }
- ";" (. c = new AssignCmd(x, lhss, rhss); .)
- )
- .
-
-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;
- .)
- "[" (. x = t; .)
- [
- Expression<out e> (. indexes.Add(e); .)
- { ","
- Expression<out e> (. indexes.Add(e); .)
- }
- ]
- "]"
- .
-
-/*------------------------------------------------------------------------*/
-CallCmd<out Cmd c>
-= (. Contract.Ensures(Contract.ValueAtReturn(out c) != null);
- IToken x;
- bool isAsync = false;
- bool isFree = false;
- QKeyValue kv = null;
- c = null;
- .)
- [ "async" (. isAsync = true; .)
- ]
- [ "free" (. isFree = true; .)
- ]
- "call" (. x = t; .)
- { Attribute<ref kv> }
- CallParams<isAsync, isFree, kv, x, out c> (. .)
- .
-
-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>();
- .)
- "par" (. x = t; .)
- { Attribute<ref kv> }
- CallParams<false, false, kv, x, out c> (. callCmds.Add((CallCmd)c); .)
- { "|" CallParams<false, false, kv, x, out c> (. callCmds.Add((CallCmd)c); .)
- }
- ";" (. d = new ParCallCmd(x, callCmds, kv); .)
- .
-
-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>
- ( "("
- [ Expression<out en> (. es.Add(en); .)
- { "," Expression<out en> (. es.Add(en); .)
- }
- ]
- ")" (. c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync; .)
- |
- (. ids.Add(new IdentifierExpr(first, first.val)); .)
- [ "," Ident<out p> (. ids.Add(new IdentifierExpr(p, p.val)); .)
- { "," Ident<out p> (. ids.Add(new IdentifierExpr(p, p.val)); .)
- }
- ] ":="
- Ident<out first> "("
- [ Expression<out en> (. es.Add(en); .)
- { "," Expression<out en> (. es.Add(en); .)
- }
- ]
- ")" (. c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync; .)
- )
- .
-
-/*------------------------------------------------------------------------*/
-Proposition<out Expr/*!*/ e>
-=(.Contract.Ensures(Contract.ValueAtReturn(out e) != null);.)
- Expression<out e>
- .
-
-/*------------------------------------------------------------------------*/
-Idents<.out List<IToken>/*!*/ xs.>
-= (.Contract.Ensures(Contract.ValueAtReturn(out xs) != null); IToken/*!*/ id; xs = new List<IToken>(); .)
- Ident<out id> (. xs.Add(id); .)
- { "," Ident<out id> (. xs.Add(id); .)
- }
- .
-
-/*------------------------------------------------------------------------*/
-WhiteSpaceIdents<.out List<IToken>/*!*/ xs.>
-= (. Contract.Ensures(Contract.ValueAtReturn(out xs) != null); IToken/*!*/ id; xs = new List<IToken>(); .)
- Ident<out id> (. xs.Add(id); .)
- { Ident<out id> (. xs.Add(id); .)
- }
- .
-
-/*------------------------------------------------------------------------*/
-Expressions<.out List<Expr>/*!*/ es.>
-= (. Contract.Ensures(Contract.ValueAtReturn(out es) != null); Expr/*!*/ e; es = new List<Expr>(); .)
- Expression<out e> (. es.Add(e); .)
- { "," Expression<out e> (. es.Add(e); .)
- }
- .
-
-/*------------------------------------------------------------------------*/
-Expression<.out Expr/*!*/ e0.>
-= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; .)
- ImpliesExpression<false, out e0>
- { EquivOp (. x = t; .)
- ImpliesExpression<false, out e1>
- (. e0 = Expr.Binary(x, BinaryOperator.Opcode.Iff, e0, e1); .)
- }
- .
-
-EquivOp = "<==>" | '\u21d4'.
-
-/*------------------------------------------------------------------------*/
-ImpliesExpression<bool noExplies, out Expr/*!*/ e0>
-= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; .)
- LogicalExpression<out e0>
- [
- ImpliesOp (. x = t; .)
- /* recurse because implication is right-associative */
- ImpliesExpression<true, out e1>
- (. e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e0, e1); .)
- |
- 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); .)
- /* loop because explies is left-associative */
- {
- ExpliesOp (. x = t; .)
- LogicalExpression<out e1>
- (. e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e1, e0); .)
- }
- ]
- .
-
-ImpliesOp = "==>" | '\u21d2'.
-ExpliesOp = "<==" | '\u21d0'.
-
-/*------------------------------------------------------------------------*/
-LogicalExpression<out Expr/*!*/ e0>
-= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; .)
- RelationalExpression<out e0>
- [ AndOp (. x = t; .)
- RelationalExpression<out e1>
- (. e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1); .)
- { AndOp (. x = t; .)
- RelationalExpression<out e1>
- (. e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1); .)
- }
- | OrOp (. x = t; .)
- RelationalExpression<out e1>
- (. e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1); .)
- { OrOp (. x = t; .)
- RelationalExpression<out e1>
- (. e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1); .)
- }
- ]
- .
-
-AndOp = "&&" | '\u2227'.
-OrOp = "||" | '\u2228'.
-
-/*------------------------------------------------------------------------*/
-RelationalExpression<out Expr/*!*/ e0>
-= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; BinaryOperator.Opcode op; .)
- BvTerm<out e0>
- [ RelOp<out x, out op>
- BvTerm<out e1> (. e0 = Expr.Binary(x, op, e0, e1); .)
- ]
- .
-
-RelOp<out IToken/*!*/ x, out BinaryOperator.Opcode op>
-= (.Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; .)
- ( "==" (. x = t; op=BinaryOperator.Opcode.Eq; .)
- | "<" (. x = t; op=BinaryOperator.Opcode.Lt; .)
- | ">" (. x = t; op=BinaryOperator.Opcode.Gt; .)
- | "<=" (. x = t; op=BinaryOperator.Opcode.Le; .)
- | ">=" (. x = t; op=BinaryOperator.Opcode.Ge; .)
- | "!=" (. x = t; op=BinaryOperator.Opcode.Neq; .)
- | "<:" (. x = t; op=BinaryOperator.Opcode.Subtype; .)
- | '\u2260' (. x = t; op=BinaryOperator.Opcode.Neq; .)
- | '\u2264' (. x = t; op=BinaryOperator.Opcode.Le; .)
- | '\u2265' (. x = t; op=BinaryOperator.Opcode.Ge; .)
- )
- .
-
-/*------------------------------------------------------------------------*/
-BvTerm<out Expr/*!*/ e0>
-= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; .)
- Term<out e0>
- { "++" (. x = t; .)
- Term<out e1> (. e0 = new BvConcatExpr(x, e0, e1); .)
- }
- .
-
-
-/*------------------------------------------------------------------------*/
-Term<out Expr/*!*/ e0>
-= (.Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; BinaryOperator.Opcode op; .)
- Factor<out e0>
- { AddOp<out x, out op>
- Factor<out e1> (. e0 = Expr.Binary(x, op, e0, e1); .)
- }
- .
-
-AddOp<out IToken/*!*/ x, out BinaryOperator.Opcode op>
-= (.Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; .)
- ( "+" (. x = t; op=BinaryOperator.Opcode.Add; .)
- | "-" (. x = t; op=BinaryOperator.Opcode.Sub; .)
- )
- .
-
-/*------------------------------------------------------------------------*/
-Factor<out Expr/*!*/ e0>
-= (.Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; BinaryOperator.Opcode op; .)
- Power<out e0>
- { MulOp<out x, out op>
- Power<out e1> (. e0 = Expr.Binary(x, op, e0, e1); .)
- }
- .
-
-MulOp<out IToken/*!*/ x, out BinaryOperator.Opcode op>
-= (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; .)
- ( "*" (. x = t; op=BinaryOperator.Opcode.Mul; .)
- | "div" (. x = t; op=BinaryOperator.Opcode.Div; .)
- | "mod" (. x = t; op=BinaryOperator.Opcode.Mod; .)
- | "/" (. x = t; op=BinaryOperator.Opcode.RealDiv; .)
- )
- .
-
-/*------------------------------------------------------------------------*/
-Power<out Expr/*!*/ e0>
-= (.Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; .)
- UnaryExpression<out e0>
- [
- "**" (. x = t; .)
- /* recurse because exponentation is right-associative */
- Power<out e1> (. e0 = Expr.Binary(x, BinaryOperator.Opcode.Pow, e0, e1); .)
- ]
- .
-
-/*------------------------------------------------------------------------*/
-UnaryExpression<out Expr/*!*/ e>
-= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;
- e = dummyExpr;
- .)
- ( "-" (. x = t; .)
- UnaryExpression<out e> (. e = Expr.Unary(x, UnaryOperator.Opcode.Neg, e); .)
- | NegOp (. x = t; .)
- UnaryExpression<out e> (. e = Expr.Unary(x, UnaryOperator.Opcode.Not, e); .)
- | CoercionExpression<out e>
- )
- .
-
-NegOp = "!" | '\u00ac'.
-
-/*------------------------------------------------------------------------*/
-
-/* This production creates ambiguities, because types can start with "<"
- (polymorphic map types), but can also be followed by "<" (inequalities).
- Coco deals with these ambiguities in a reasonable way by preferring to read
- further types (type arguments) over relational symbols. E.g., "5 : C < 0"
- will cause a parse error because "<" is treated as the beginning of a
- map type. */
-
-CoercionExpression<out Expr/*!*/ e>
-= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;
- Bpl.Type/*!*/ coercedTo;
- BigNum bn;
- .)
- ArrayExpression<out e>
- { ":" (. x = t; .)
- (
- Type<out coercedTo> (. e = Expr.CoerceType(x, e, coercedTo); .)
- |
- Nat<out bn> /* This means that we really look at a bitvector
- expression t[a:b] */
- (. 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);
- }
- .)
- )
- }
- .
-
-/*------------------------------------------------------------------------*/
-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>
- { "[" (. x = t; allArgs = new List<Expr> ();
- allArgs.Add(e);
- store = false; bvExtract = false; .)
- [
- Expression<out index0>
- (. if (index0 is BvBounds)
- bvExtract = true;
- else
- allArgs.Add(index0);
- .)
- { "," Expression<out e1>
- (. if (bvExtract || e1 is BvBounds)
- this.SemErr("bitvectors only have one dimension");
- allArgs.Add(e1);
- .)
- }
- [ ":=" Expression<out e1>
- (. if (bvExtract || e1 is BvBounds)
- this.SemErr("assignment to bitvectors is not possible");
- allArgs.Add(e1); store = true;
- .)
- ]
- | ":=" Expression<out e1> (. allArgs.Add(e1); store = true; .)
- ]
- "]"
- (. 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);
- .)
- }
- .
-
-
-/*------------------------------------------------------------------------*/
-AtomExpression<out Expr/*!*/ e>
-= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; int n; BigNum bn; BigDec bd;
- List<Expr>/*!*/ es; List<Variable>/*!*/ ds; Trigger trig;
- List<TypeVariable>/*!*/ typeParams;
- IdentifierExpr/*!*/ id;
- QKeyValue kv;
- e = dummyExpr;
- List<Variable>/*!*/ locals;
- List<Block/*!*/>/*!*/ blocks;
- .)
- ( "false" (. e = new LiteralExpr(t, false); .)
- | "true" (. e = new LiteralExpr(t, true); .)
- | Nat<out bn> (. e = new LiteralExpr(t, bn); .)
- | Dec<out bd> (. e = new LiteralExpr(t, bd); .)
- | BvLit<out bn, out n> (. e = new LiteralExpr(t, bn, n); .)
-
- | Ident<out x> (. id = new IdentifierExpr(x, x.val); e = id; .)
- [ "("
- ( Expressions<out es> (. e = new NAryExpr(x, new FunctionCall(id), es); .)
- | /* empty */ (. e = new NAryExpr(x, new FunctionCall(id), new List<Expr>()); .)
- )
- ")"
- ]
-
- | "old" (. x = t; .)
- "("
- Expression<out e>
- ")" (. e = new OldExpr(x, e); .)
-
- | "int" (. x = t; .)
- "("
- Expression<out e>
- ")" (. e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToInt), new List<Expr>{ e }); .)
-
- | "real" (. x = t; .)
- "("
- Expression<out e>
- ")" (. e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToReal), new List<Expr>{ e }); .)
-
- | "(" ( Expression<out e> (. if (e is BvBounds)
- this.SemErr("parentheses around bitvector bounds " +
- "are not allowed"); .)
- | 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); .)
- | 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); .)
- | 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); .)
- )
- ")"
- | IfThenElseExpression<out e>
- | CodeExpression<out locals, out blocks> (. e = new CodeExpr(locals, blocks); .)
- )
- .
-
-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/*!*/>();
- .)
- "|{"
- { LocalVars<locals> }
- SpecBlock<out b> (. blocks.Add(b); .)
- { SpecBlock<out b> (. blocks.Add(b); .)
- }
- "}|"
- .
-
-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> ":"
- { 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");
- }
- .)
- }
- ( "goto" (. 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));
- .)
- | "return" Expression<out e>
- (. b = new Block(x,x.val,cs,new ReturnExprCmd(t,e)); .)
- )
- ";"
- .
-
-Attribute<ref QKeyValue kv>
-= (. Trigger trig = null; .)
- AttributeOrTrigger<ref kv, ref trig> (. if (trig != null) this.SemErr("only attributes, not triggers, allowed here"); .)
-.
-
-AttributeOrTrigger<ref QKeyValue kv, ref Trigger trig>
-= (. IToken/*!*/ tok; Expr/*!*/ e; List<Expr>/*!*/ es;
- string key;
- List<object/*!*/> parameters; object/*!*/ param;
- .)
- "{" (. tok = t; .)
- (
- ":" ident (. key = t.val; parameters = new List<object/*!*/>(); .)
- [ AttributeParameter<out param> (. parameters.Add(param); .)
- { "," 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));
- }
- }
- .)
- |
- Expression<out e> (. es = new List<Expr> { e }; .)
- { "," 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));
- }
- .)
- )
- "}"
- .
-
-AttributeParameter<out object/*!*/ o>
-= (. Contract.Ensures(Contract.ValueAtReturn(out o) != null);
- o = "error";
- Expr/*!*/ e;
- .)
- ( string (. o = t.val.Substring(1, t.val.Length-2); .)
- | Expression<out e> (. o = e; .)
- )
- .
-
-IfThenElseExpression<out Expr/*!*/ e>
-= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null);
- IToken/*!*/ tok;
- Expr/*!*/ e0, e1, e2;
- e = dummyExpr; .)
- "if" (. tok = t; .) Expression<out e0> "then" Expression<out e1> "else" Expression<out e2>
- (. e = new NAryExpr(tok, new IfThenElse(tok), new List<Expr>{ e0, e1, e2 }); .)
- .
-
-
-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> ();
- .)
- (
- TypeParams<out tok, out typeParams>
- [ BoundVars<q, out ds> ]
- |
- BoundVars<q, out ds>
- )
- QSep
- { AttributeOrTrigger<ref kv, ref trig> }
- Expression<out body>
- .
-
-Forall = "forall" | '\u2200'.
-Exists = "exists" | '\u2203'.
-Lambda = "lambda" | '\u03bb'.
-QSep = "::" | '\u2022'.
-
-/*------------------------------------------------------------------------*/
-Ident<out IToken/*!*/ x>
-=(.Contract.Ensures(Contract.ValueAtReturn(out x) != null);.)
- ident (. x = t;
- if (x.val.StartsWith("\\"))
- x.val = x.val.Substring(1);
- .)
- .
-
-/*------------------------------------------------------------------------*/
-Nat<out BigNum n>
-=
- digits
- (. try {
- n = BigNum.FromString(t.val);
- } catch (FormatException) {
- this.SemErr("incorrectly formatted number");
- n = BigNum.ZERO;
- }
- .)
- .
-
-/*------------------------------------------------------------------------*/
-Dec<out BigDec n>
-= (. string s = ""; .)
- (
- decimal (. s = t.val; .)
- |
- float (. s = t.val; .)
- )
- (. try {
- n = BigDec.FromString(s);
- } catch (FormatException) {
- this.SemErr("incorrectly formatted number");
- n = BigDec.ZERO;
- }
- .)
- .
-
-/*------------------------------------------------------------------------*/
-BvLit<out BigNum n, out int m>
-=
- bvlit
- (.
- 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;
- }
- .)
- .
-END BoogiePL.
+
+/*---------------------------------------------------------------------------
+// BoogiePL -
+//--------------------------------------------------------------------------*/
+
+/*using System;*/
+using System.Collections;
+using System.Collections.Generic;
+using System.IO;
+using System.Text;
+using Microsoft.Boogie;
+using Microsoft.Basetypes;
+using Bpl = Microsoft.Boogie;
+
+
+COMPILER BoogiePL
+
+/*--------------------------------------------------------------------------*/
+
+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) {
+ 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(); }
+}
+
+/*--------------------------------------------------------------------------*/
+CHARACTERS
+ letter = "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz".
+ digit = "0123456789".
+ special = "'~#$^_.?`".
+ glyph = "`~!@#$%^&*()-_=+[{]}|;:',<.>/?\\".
+
+ cr = '\r'.
+ lf = '\n'.
+ tab = '\t'.
+
+ space = ' '.
+ quote = '"'.
+
+ newLine = cr + lf.
+ regularStringChar = ANY - quote - newLine.
+
+ nondigit = letter + special.
+ nonquote = letter + digit + space + glyph.
+
+
+/*------------------------------------------------------------------------*/
+TOKENS
+ ident = [ '\\' ] nondigit {nondigit | digit}.
+ bvlit = digit {digit} 'b' 'v' digit {digit}.
+ digits = digit {digit}.
+
+ string = quote { regularStringChar | "\\\"" } quote.
+
+ decimal = digit {digit} 'e' [ '-' ] digit {digit} .
+ float = digit {digit} '.' digit {digit} [ 'e' [ '-' ] digit {digit} ] .
+
+COMMENTS FROM "/*" TO "*/" NESTED
+COMMENTS FROM "//" TO lf
+
+IGNORE cr + lf + tab
+
+
+/*------------------------------------------------------------------------*/
+PRODUCTIONS
+
+
+/*------------------------------------------------------------------------*/
+BoogiePL
+= (. List<Variable>/*!*/ vs;
+ List<Declaration>/*!*/ ds;
+ Axiom/*!*/ ax;
+ List<Declaration/*!*/>/*!*/ ts;
+ Procedure/*!*/ pr;
+ Implementation im;
+ Implementation/*!*/ nnim;
+ .)
+ { Consts<out vs> (. foreach(Bpl.Variable/*!*/ v in vs){
+ Contract.Assert(v != null);
+ Pgm.AddTopLevelDeclaration(v);
+ }
+ .)
+ | Function<out ds> (. foreach(Bpl.Declaration/*!*/ d in ds){
+ Contract.Assert(d != null);
+ Pgm.AddTopLevelDeclaration(d);
+ }
+ .)
+ | Axiom<out ax> (. Pgm.AddTopLevelDeclaration(ax); .)
+ | UserDefinedTypes<out ts> (. foreach(Declaration/*!*/ td in ts){
+ Contract.Assert(td != null);
+ Pgm.AddTopLevelDeclaration(td);
+ }
+ .)
+ | GlobalVars<out vs> (. foreach(Bpl.Variable/*!*/ v in vs){
+ Contract.Assert(v != null);
+ Pgm.AddTopLevelDeclaration(v);
+ }
+ .)
+ | Procedure<out pr, out im> (. Pgm.AddTopLevelDeclaration(pr);
+ if (im != null) {
+ Pgm.AddTopLevelDeclaration(im);
+ }
+ .)
+ | Implementation<out nnim> (. Pgm.AddTopLevelDeclaration(nnim); .)
+ }
+ EOF
+ .
+
+/*------------------------------------------------------------------------*/
+GlobalVars<.out List<Variable>/*!*/ ds.>
+= (.
+ Contract.Ensures(Contract.ValueAtReturn(out ds) != null);
+ QKeyValue kv = null;
+ ds = new List<Variable>();
+ var dsx = ds;
+ .)
+ "var"
+ { Attribute<ref kv> }
+ IdsTypeWheres<true, "global variables", delegate(TypedIdent tyd) { dsx.Add(new GlobalVariable(tyd.tok, tyd, kv)); } > ";"
+ .
+
+LocalVars<.List<Variable>/*!*/ ds.>
+= (.
+ Contract.Ensures(Contract.ValueAtReturn(out ds) != null);
+ QKeyValue kv = null;
+ .)
+ "var"
+ { Attribute<ref kv> }
+ IdsTypeWheres<true, "local variables", delegate(TypedIdent tyd) { ds.Add(new LocalVariable(tyd.tok, tyd, kv)); } > ";"
+ .
+
+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";
+ .)
+ "("
+ [ AttrsIdsTypeWheres<allowWhereClauses, allowWhereClauses, context, delegate(TypedIdent tyd, QKeyValue kv) { dsx.Add(new Formal(tyd.tok, tyd, incoming, kv)); }>
+ ]
+ ")"
+ .
+
+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)); } >
+ .
+
+/*------------------------------------------------------------------------*/
+/* IdsType is used with const declarations */
+IdsType<.out List<TypedIdent>/*!*/ tyds.>
+= (. Contract.Ensures(Contract.ValueAtReturn(out tyds) != null); List<IToken>/*!*/ ids; Bpl.Type/*!*/ ty; .)
+ Idents<out ids> ":" 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));
+ }
+ .)
+ .
+
+/* AttrsIdsTypeWheres is used with the declarations of formals and bound variables */
+AttrsIdsTypeWheres<. bool allowAttributes, bool allowWhereClauses, string context, System.Action<TypedIdent, QKeyValue> action .>
+=
+ AttributesIdsTypeWhere<allowAttributes, allowWhereClauses, context, action>
+ { "," AttributesIdsTypeWhere<allowAttributes, allowWhereClauses, context, action> }
+ .
+
+IdsTypeWheres<. bool allowWhereClauses, string context, System.Action<TypedIdent> action .>
+=
+ IdsTypeWhere<allowWhereClauses, context, action>
+ { "," IdsTypeWhere<allowWhereClauses, context, action> }
+ .
+
+AttributesIdsTypeWhere<. bool allowAttributes, bool allowWhereClauses, string context, System.Action<TypedIdent, QKeyValue> action .>
+= (. QKeyValue kv = null; .)
+ { Attribute<ref kv> (. if (!allowAttributes) {
+ kv = null;
+ this.SemErr("attributes are not allowed on " + context);
+ }
+ .)
+ }
+ IdsTypeWhere<allowWhereClauses, context, delegate(TypedIdent tyd) { action(tyd, kv); }>
+ .
+
+/* context is allowed to be null if allowWhereClauses is true */
+IdsTypeWhere<. bool allowWhereClauses, string context, System.Action<TypedIdent> action .>
+= (. List<IToken>/*!*/ ids; Bpl.Type/*!*/ ty; Expr wh = null; Expr/*!*/ nne; .)
+ Idents<out ids> ":" Type<out ty>
+ [ "where" 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));
+ }
+ .)
+ .
+
+/*------------------------------------------------------------------------*/
+Type<out Bpl.Type/*!*/ ty>
+= (.Contract.Ensures(Contract.ValueAtReturn(out ty) != null); IToken/*!*/ tok; ty = dummyType; .)
+ (
+ TypeAtom<out ty>
+ |
+ Ident<out tok> (. List<Bpl.Type>/*!*/ args = new List<Bpl.Type> (); .)
+ [ TypeArgs<args> ] (. ty = new UnresolvedTypeIdentifier (tok, tok.val, args); .)
+ |
+ MapType<out ty>
+ )
+ .
+
+TypeArgs<.List<Bpl.Type>/*!*/ ts.>
+= (.Contract.Requires(ts != null); IToken/*!*/ tok; Bpl.Type/*!*/ ty; .)
+ (
+ TypeAtom<out ty> (. ts.Add(ty); .)
+ [ TypeArgs<ts> ]
+ |
+ Ident<out tok> (. List<Bpl.Type>/*!*/ args = new List<Bpl.Type> ();
+ ts.Add(new UnresolvedTypeIdentifier (tok, tok.val, args)); .)
+ [ TypeArgs<ts> ]
+ |
+ MapType<out ty> (. ts.Add(ty); .)
+ )
+ .
+
+TypeAtom<out Bpl.Type/*!*/ ty>
+= (.Contract.Ensures(Contract.ValueAtReturn(out ty) != null); ty = dummyType; .)
+ ( "int" (. ty = new BasicType(t, SimpleType.Int); .)
+ | "real" (. ty = new BasicType(t, SimpleType.Real); .)
+ | "bool" (. ty = new BasicType(t, SimpleType.Bool); .)
+ /* note: bitvectors are handled in UnresolvedTypeIdentifier */
+ |
+ "("
+ Type<out ty>
+ ")"
+ )
+ .
+
+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>();
+ .)
+ [ TypeParams<out nnTok, out typeParameters> (. tok = nnTok; .) ]
+ "[" (. if (tok == null) tok = t; .)
+ [ Types<arguments> ]
+ "]"
+ Type<out result>
+ (.
+ ty = new MapType(tok, typeParameters, arguments, result);
+ .)
+ .
+
+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; .)
+ "<" (. tok = t; .)
+ Idents<out typeParamToks>
+ ">"
+ (.
+ typeParams = new List<TypeVariable> ();
+ foreach(Token/*!*/ id in typeParamToks){
+ Contract.Assert(id != null);
+ typeParams.Add(new TypeVariable(id, id.val));}
+ .)
+ .
+
+Types<.List<Bpl.Type>/*!*/ ts.>
+= (. Contract.Requires(ts != null); Bpl.Type/*!*/ ty; .)
+ Type<out ty> (. ts.Add(ty); .)
+ { "," Type<out ty> (. ts.Add(ty); .)
+ }
+ .
+
+
+/*------------------------------------------------------------------------*/
+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; .)
+ "const" (. y = t; .)
+ { Attribute<ref kv> }
+ [ "unique" (. u = true; .)
+ ]
+ IdsType<out xs>
+ [ 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));
+ }
+ .)
+ ";"
+ .
+
+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; .)
+ "extends" (. Parents = new List<ConstantParent/*!*/> ();
+ u = false; .)
+ [
+ [ "unique" (. u = true; .)
+ ]
+ Ident<out parent> (. Parents.Add(new ConstantParent (
+ new IdentifierExpr(parent, parent.val), u)); .)
+ {
+ "," (. u = false; .)
+ [ "unique" (. u = true; .)
+ ]
+ Ident<out parent> (. Parents.Add(new ConstantParent (
+ new IdentifierExpr(parent, parent.val), u)); .)
+ }
+ ]
+ [ "complete" (. ChildrenComplete = true; .)
+ ]
+ .
+
+/*------------------------------------------------------------------------*/
+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;
+ .)
+ "function" { Attribute<ref kv> } Ident<out z>
+ [ TypeParams<out typeParamTok, out typeParams> ]
+ "("
+ [ VarOrType<out tyd, out argKv> (. arguments.Add(new Formal(tyd.tok, tyd, true, argKv)); .)
+ { "," VarOrType<out tyd, out argKv> (. arguments.Add(new Formal(tyd.tok, tyd, true, argKv)); .)
+ } ] ")"
+ (. argKv = null; .)
+ (
+ "returns" "(" VarOrType<out retTyd, out argKv> ")"
+ |
+ ":" Type<out retTy> (. retTyd = new TypedIdent(retTy.tok, TypedIdent.NoName, retTy); .)
+ )
+ ( "{" Expression<out tmp> (. definition = tmp; .) "}" | ";" )
+ (.
+ 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));
+ }
+ }
+ .)
+ .
+
+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;
+ .)
+ { Attribute<ref kv> }
+ Type<out ty> (. tok = ty.tok; .)
+ [ ":" (. 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); .)
+ .
+
+/*------------------------------------------------------------------------*/
+Axiom<out Axiom/*!*/ m>
+= (.Contract.Ensures(Contract.ValueAtReturn(out m) != null); Expr/*!*/ e; QKeyValue kv = null; .)
+ "axiom"
+ { Attribute<ref kv> }
+ (. IToken/*!*/ x = t; .)
+ Proposition<out e> ";" (. m = new Axiom(x,e, null, kv); .)
+ .
+
+/*------------------------------------------------------------------------*/
+UserDefinedTypes<.out List<Declaration/*!*/>/*!*/ ts.>
+= (. Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out ts))); Declaration/*!*/ decl; QKeyValue kv = null; ts = new List<Declaration/*!*/> (); .)
+ "type"
+ { Attribute<ref kv> }
+ UserDefinedType<out decl, kv> (. ts.Add(decl); .)
+ { "," UserDefinedType<out decl, kv> (. ts.Add(decl); .) }
+ ";"
+ .
+
+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>
+ [ WhiteSpaceIdents<out paramTokens> ]
+ [
+ "=" 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);
+ }
+ .)
+ .
+
+
+/*------------------------------------------------------------------------*/
+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;
+ .)
+
+ "procedure"
+ ProcSignature<true, out x, out typeParams, out ins, out outs, out kv>
+ ( ";"
+ { Spec<pre, mods, post> }
+ | { 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);
+ .)
+ )
+ (. proc = new Procedure(x, x.val, typeParams, ins, outs, pre, mods, post, kv); .)
+ .
+
+
+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;
+ .)
+
+ "implementation"
+ 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); .)
+ .
+
+
+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; .)
+ { Attribute<ref kv> }
+ Ident<out name>
+ [ TypeParams<out typeParamTok, out typeParams> ]
+ ProcFormals<true, allowWhereClausesOnFormals, out ins>
+ [ "returns" ProcFormals<false, allowWhereClausesOnFormals, out outs> ]
+ .
+
+
+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; .)
+ ( "modifies"
+ [ Idents<out ms> (. foreach(IToken/*!*/ m in ms){
+ Contract.Assert(m != null);
+ mods.Add(new IdentifierExpr(m, m.val));
+ }
+ .)
+ ] ";"
+ | "free" SpecPrePost<true, pre, post>
+ | SpecPrePost<false, pre, post>
+ )
+ .
+
+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; .)
+ ( "requires" (. tok = t; .)
+ { Attribute<ref kv> }
+ Proposition<out e> ";" (. pre.Add(new Requires(tok, free, e, null, kv)); .)
+ | "ensures" (. tok = t; .)
+ { Attribute<ref kv> }
+ Proposition<out e> ";" (. post.Add(new Ensures(tok, free, e, null, kv)); .)
+ )
+ .
+
+/*------------------------------------------------------------------------*/
+
+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>(); .)
+ "{"
+ { LocalVars<locals> }
+ StmtList<out stmtList>
+ .
+
+/* the StmtList also reads the final curly brace */
+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;
+ .)
+
+ {
+ ( 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>();
+ }
+ .)
+
+ | 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;
+ .)
+
+ | 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;
+ .)
+
+ )
+ }
+ "}"
+ (. 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);
+ .)
+ .
+
+TransferCmd<out TransferCmd/*!*/ tc>
+= (. Contract.Ensures(Contract.ValueAtReturn(out tc) != null); tc = dummyTransferCmd;
+ Token y; List<IToken>/*!*/ xs;
+ List<String> ss = new List<String>();
+ .)
+ ( "goto" (. y = t; .)
+ Idents<out xs> (. foreach(IToken/*!*/ s in xs){
+ Contract.Assert(s != null);
+ ss.Add(s.val); }
+ tc = new GotoCmd(y, ss);
+ .)
+ | "return" (. tc = new ReturnCmd(t); .)
+ ) ";"
+ .
+
+StructuredCmd<out StructuredCmd/*!*/ ec>
+= (. Contract.Ensures(Contract.ValueAtReturn(out ec) != null); ec = dummyStructuredCmd; Contract.Assume(cce.IsPeerConsistent(ec));
+ IfCmd/*!*/ ifcmd; WhileCmd/*!*/ wcmd; BreakCmd/*!*/ bcmd;
+ .)
+ ( IfCmd<out ifcmd> (. ec = ifcmd; .)
+ | WhileCmd<out wcmd> (. ec = wcmd; .)
+ | BreakCmd<out bcmd> (. ec = bcmd; .)
+ )
+ .
+
+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;
+ .)
+ "if" (. x = t; .)
+ Guard<out guard>
+ "{" StmtList<out thn>
+ [ "else"
+ ( IfCmd<out elseIf> (. elseIfOption = elseIf; .)
+ | "{"
+ StmtList<out els> (. elseOption = els; .)
+ )
+ ]
+ (. ifcmd = new IfCmd(x, guard, thn, elseIfOption, elseOption); .)
+ .
+
+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;
+ .)
+ "while" (. x = t; .)
+ Guard<out guard> (. Contract.Assume(guard == null || cce.Owner.None(guard)); .)
+ { (. isFree = false; z = la/*lookahead token*/; .)
+ [ "free" (. isFree = true; .)
+ ]
+ "invariant"
+ { 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;
+ .)
+ ";"
+ }
+ "{"
+ StmtList<out body> (. wcmd = new WhileCmd(x, guard, invariants, body); .)
+ .
+
+Guard<out Expr e>
+= (. Expr/*!*/ ee; e = null; .)
+ "("
+ ( "*" (. e = null; .)
+ | Expression<out ee> (. e = ee; .)
+ )
+ ")"
+ .
+
+BreakCmd<out BreakCmd/*!*/ bcmd>
+= (.Contract.Ensures(Contract.ValueAtReturn(out bcmd) != null); IToken/*!*/ x; IToken/*!*/ y;
+ string breakLabel = null;
+ .)
+ "break" (. x = t; .)
+ [ Ident<out y> (. breakLabel = y.val; .)
+ ] ";" (. bcmd = new BreakCmd(x, breakLabel); .)
+ .
+
+/*------------------------------------------------------------------------*/
+
+LabelOrCmd<out Cmd c, out IToken label>
+/* ensures (c == null) != (label != null) */
+= (. IToken/*!*/ x; Expr/*!*/ e;
+ List<IToken>/*!*/ xs;
+ List<IdentifierExpr> ids;
+ c = dummyCmd; label = null;
+ Cmd/*!*/ cn;
+ QKeyValue kv = null;
+ .)
+ ( LabelOrAssign<out c, out label>
+ | "assert" (. x = t; .)
+ { Attribute<ref kv> }
+ Proposition<out e> (. c = new AssertCmd(x, e, kv); .)
+ ";"
+ | "assume" (. x = t; .)
+ { Attribute<ref kv> }
+ Proposition<out e> (. c = new AssumeCmd(x, e, kv); .)
+ ";"
+ | "havoc" (. x = t; .)
+ Idents<out xs> ";" (. 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);
+ .)
+ | CallCmd<out cn> ";" (. c = cn; .)
+ | ParCallCmd<out cn> (. c = cn; .)
+ | "yield" (. x = t; .)
+ ";" (. c = new YieldCmd(x); .)
+ )
+ .
+
+/*------------------------------------------------------------------------*/
+
+LabelOrAssign<out Cmd c, out IToken label>
+/* ensures (c == null) != (label != null) */
+= (. 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; .)
+ ( ":" (. c = null; label = x; .)
+
+ | (. lhss = new List<AssignLhs/*!*/>(); .)
+ (. lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val)); .)
+
+ { MapAssignIndex<out y, out indexes> (. lhs = new MapAssignLhs(y, lhs, indexes); .) }
+ (. lhss.Add(lhs); .)
+
+ { ","
+ Ident<out id>
+ (. lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val)); .)
+ { MapAssignIndex<out y, out indexes> (. lhs = new MapAssignLhs(y, lhs, indexes); .) }
+ (. lhss.Add(lhs); .)
+ }
+
+ ":=" (. x = t; /* use location of := */ .)
+ Expression<out e0> (. rhss = new List<Expr/*!*/> ();
+ rhss.Add(e0); .)
+ { ","
+ Expression<out e0> (. rhss.Add(e0); .)
+ }
+ ";" (. c = new AssignCmd(x, lhss, rhss); .)
+ )
+ .
+
+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;
+ .)
+ "[" (. x = t; .)
+ [
+ Expression<out e> (. indexes.Add(e); .)
+ { ","
+ Expression<out e> (. indexes.Add(e); .)
+ }
+ ]
+ "]"
+ .
+
+/*------------------------------------------------------------------------*/
+CallCmd<out Cmd c>
+= (. Contract.Ensures(Contract.ValueAtReturn(out c) != null);
+ IToken x;
+ bool isAsync = false;
+ bool isFree = false;
+ QKeyValue kv = null;
+ c = null;
+ .)
+ [ "async" (. isAsync = true; .)
+ ]
+ [ "free" (. isFree = true; .)
+ ]
+ "call" (. x = t; .)
+ { Attribute<ref kv> }
+ CallParams<isAsync, isFree, kv, x, out c> (. .)
+ .
+
+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>();
+ .)
+ "par" (. x = t; .)
+ { Attribute<ref kv> }
+ CallParams<false, false, kv, x, out c> (. callCmds.Add((CallCmd)c); .)
+ { "|" CallParams<false, false, kv, x, out c> (. callCmds.Add((CallCmd)c); .)
+ }
+ ";" (. d = new ParCallCmd(x, callCmds, kv); .)
+ .
+
+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>
+ ( "("
+ [ Expression<out en> (. es.Add(en); .)
+ { "," Expression<out en> (. es.Add(en); .)
+ }
+ ]
+ ")" (. c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync; .)
+ |
+ (. ids.Add(new IdentifierExpr(first, first.val)); .)
+ [ "," Ident<out p> (. ids.Add(new IdentifierExpr(p, p.val)); .)
+ { "," Ident<out p> (. ids.Add(new IdentifierExpr(p, p.val)); .)
+ }
+ ] ":="
+ Ident<out first> "("
+ [ Expression<out en> (. es.Add(en); .)
+ { "," Expression<out en> (. es.Add(en); .)
+ }
+ ]
+ ")" (. c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync; .)
+ )
+ .
+
+/*------------------------------------------------------------------------*/
+Proposition<out Expr/*!*/ e>
+=(.Contract.Ensures(Contract.ValueAtReturn(out e) != null);.)
+ Expression<out e>
+ .
+
+/*------------------------------------------------------------------------*/
+Idents<.out List<IToken>/*!*/ xs.>
+= (.Contract.Ensures(Contract.ValueAtReturn(out xs) != null); IToken/*!*/ id; xs = new List<IToken>(); .)
+ Ident<out id> (. xs.Add(id); .)
+ { "," Ident<out id> (. xs.Add(id); .)
+ }
+ .
+
+/*------------------------------------------------------------------------*/
+WhiteSpaceIdents<.out List<IToken>/*!*/ xs.>
+= (. Contract.Ensures(Contract.ValueAtReturn(out xs) != null); IToken/*!*/ id; xs = new List<IToken>(); .)
+ Ident<out id> (. xs.Add(id); .)
+ { Ident<out id> (. xs.Add(id); .)
+ }
+ .
+
+/*------------------------------------------------------------------------*/
+Expressions<.out List<Expr>/*!*/ es.>
+= (. Contract.Ensures(Contract.ValueAtReturn(out es) != null); Expr/*!*/ e; es = new List<Expr>(); .)
+ Expression<out e> (. es.Add(e); .)
+ { "," Expression<out e> (. es.Add(e); .)
+ }
+ .
+
+/*------------------------------------------------------------------------*/
+Expression<.out Expr/*!*/ e0.>
+= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; .)
+ ImpliesExpression<false, out e0>
+ { EquivOp (. x = t; .)
+ ImpliesExpression<false, out e1>
+ (. e0 = Expr.Binary(x, BinaryOperator.Opcode.Iff, e0, e1); .)
+ }
+ .
+
+EquivOp = "<==>" | '\u21d4'.
+
+/*------------------------------------------------------------------------*/
+ImpliesExpression<bool noExplies, out Expr/*!*/ e0>
+= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; .)
+ LogicalExpression<out e0>
+ [
+ ImpliesOp (. x = t; .)
+ /* recurse because implication is right-associative */
+ ImpliesExpression<true, out e1>
+ (. e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e0, e1); .)
+ |
+ 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); .)
+ /* loop because explies is left-associative */
+ {
+ ExpliesOp (. x = t; .)
+ LogicalExpression<out e1>
+ (. e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e1, e0); .)
+ }
+ ]
+ .
+
+ImpliesOp = "==>" | '\u21d2'.
+ExpliesOp = "<==" | '\u21d0'.
+
+/*------------------------------------------------------------------------*/
+LogicalExpression<out Expr/*!*/ e0>
+= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; .)
+ RelationalExpression<out e0>
+ [ AndOp (. x = t; .)
+ RelationalExpression<out e1>
+ (. e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1); .)
+ { AndOp (. x = t; .)
+ RelationalExpression<out e1>
+ (. e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1); .)
+ }
+ | OrOp (. x = t; .)
+ RelationalExpression<out e1>
+ (. e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1); .)
+ { OrOp (. x = t; .)
+ RelationalExpression<out e1>
+ (. e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1); .)
+ }
+ ]
+ .
+
+AndOp = "&&" | '\u2227'.
+OrOp = "||" | '\u2228'.
+
+/*------------------------------------------------------------------------*/
+RelationalExpression<out Expr/*!*/ e0>
+= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; BinaryOperator.Opcode op; .)
+ BvTerm<out e0>
+ [ RelOp<out x, out op>
+ BvTerm<out e1> (. e0 = Expr.Binary(x, op, e0, e1); .)
+ ]
+ .
+
+RelOp<out IToken/*!*/ x, out BinaryOperator.Opcode op>
+= (.Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; .)
+ ( "==" (. x = t; op=BinaryOperator.Opcode.Eq; .)
+ | "<" (. x = t; op=BinaryOperator.Opcode.Lt; .)
+ | ">" (. x = t; op=BinaryOperator.Opcode.Gt; .)
+ | "<=" (. x = t; op=BinaryOperator.Opcode.Le; .)
+ | ">=" (. x = t; op=BinaryOperator.Opcode.Ge; .)
+ | "!=" (. x = t; op=BinaryOperator.Opcode.Neq; .)
+ | "<:" (. x = t; op=BinaryOperator.Opcode.Subtype; .)
+ | '\u2260' (. x = t; op=BinaryOperator.Opcode.Neq; .)
+ | '\u2264' (. x = t; op=BinaryOperator.Opcode.Le; .)
+ | '\u2265' (. x = t; op=BinaryOperator.Opcode.Ge; .)
+ )
+ .
+
+/*------------------------------------------------------------------------*/
+BvTerm<out Expr/*!*/ e0>
+= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; .)
+ Term<out e0>
+ { "++" (. x = t; .)
+ Term<out e1> (. e0 = new BvConcatExpr(x, e0, e1); .)
+ }
+ .
+
+
+/*------------------------------------------------------------------------*/
+Term<out Expr/*!*/ e0>
+= (.Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; BinaryOperator.Opcode op; .)
+ Factor<out e0>
+ { AddOp<out x, out op>
+ Factor<out e1> (. e0 = Expr.Binary(x, op, e0, e1); .)
+ }
+ .
+
+AddOp<out IToken/*!*/ x, out BinaryOperator.Opcode op>
+= (.Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; .)
+ ( "+" (. x = t; op=BinaryOperator.Opcode.Add; .)
+ | "-" (. x = t; op=BinaryOperator.Opcode.Sub; .)
+ )
+ .
+
+/*------------------------------------------------------------------------*/
+Factor<out Expr/*!*/ e0>
+= (.Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; BinaryOperator.Opcode op; .)
+ Power<out e0>
+ { MulOp<out x, out op>
+ Power<out e1> (. e0 = Expr.Binary(x, op, e0, e1); .)
+ }
+ .
+
+MulOp<out IToken/*!*/ x, out BinaryOperator.Opcode op>
+= (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; .)
+ ( "*" (. x = t; op=BinaryOperator.Opcode.Mul; .)
+ | "div" (. x = t; op=BinaryOperator.Opcode.Div; .)
+ | "mod" (. x = t; op=BinaryOperator.Opcode.Mod; .)
+ | "/" (. x = t; op=BinaryOperator.Opcode.RealDiv; .)
+ )
+ .
+
+/*------------------------------------------------------------------------*/
+Power<out Expr/*!*/ e0>
+= (.Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; .)
+ UnaryExpression<out e0>
+ [
+ "**" (. x = t; .)
+ /* recurse because exponentation is right-associative */
+ Power<out e1> (. e0 = Expr.Binary(x, BinaryOperator.Opcode.Pow, e0, e1); .)
+ ]
+ .
+
+/*------------------------------------------------------------------------*/
+UnaryExpression<out Expr/*!*/ e>
+= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;
+ e = dummyExpr;
+ .)
+ ( "-" (. x = t; .)
+ UnaryExpression<out e> (. e = Expr.Unary(x, UnaryOperator.Opcode.Neg, e); .)
+ | NegOp (. x = t; .)
+ UnaryExpression<out e> (. e = Expr.Unary(x, UnaryOperator.Opcode.Not, e); .)
+ | CoercionExpression<out e>
+ )
+ .
+
+NegOp = "!" | '\u00ac'.
+
+/*------------------------------------------------------------------------*/
+
+/* This production creates ambiguities, because types can start with "<"
+ (polymorphic map types), but can also be followed by "<" (inequalities).
+ Coco deals with these ambiguities in a reasonable way by preferring to read
+ further types (type arguments) over relational symbols. E.g., "5 : C < 0"
+ will cause a parse error because "<" is treated as the beginning of a
+ map type. */
+
+CoercionExpression<out Expr/*!*/ e>
+= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;
+ Bpl.Type/*!*/ coercedTo;
+ BigNum bn;
+ .)
+ ArrayExpression<out e>
+ { ":" (. x = t; .)
+ (
+ Type<out coercedTo> (. e = Expr.CoerceType(x, e, coercedTo); .)
+ |
+ Nat<out bn> /* This means that we really look at a bitvector
+ expression t[a:b] */
+ (. 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);
+ }
+ .)
+ )
+ }
+ .
+
+/*------------------------------------------------------------------------*/
+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>
+ { "[" (. x = t; allArgs = new List<Expr> ();
+ allArgs.Add(e);
+ store = false; bvExtract = false; .)
+ [
+ Expression<out index0>
+ (. if (index0 is BvBounds)
+ bvExtract = true;
+ else
+ allArgs.Add(index0);
+ .)
+ { "," Expression<out e1>
+ (. if (bvExtract || e1 is BvBounds)
+ this.SemErr("bitvectors only have one dimension");
+ allArgs.Add(e1);
+ .)
+ }
+ [ ":=" Expression<out e1>
+ (. if (bvExtract || e1 is BvBounds)
+ this.SemErr("assignment to bitvectors is not possible");
+ allArgs.Add(e1); store = true;
+ .)
+ ]
+ | ":=" Expression<out e1> (. allArgs.Add(e1); store = true; .)
+ ]
+ "]"
+ (. 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);
+ .)
+ }
+ .
+
+
+/*------------------------------------------------------------------------*/
+AtomExpression<out Expr/*!*/ e>
+= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; int n; BigNum bn; BigDec bd;
+ List<Expr>/*!*/ es; List<Variable>/*!*/ ds; Trigger trig;
+ List<TypeVariable>/*!*/ typeParams;
+ IdentifierExpr/*!*/ id;
+ QKeyValue kv;
+ e = dummyExpr;
+ List<Variable>/*!*/ locals;
+ List<Block/*!*/>/*!*/ blocks;
+ .)
+ ( "false" (. e = new LiteralExpr(t, false); .)
+ | "true" (. e = new LiteralExpr(t, true); .)
+ | Nat<out bn> (. e = new LiteralExpr(t, bn); .)
+ | Dec<out bd> (. e = new LiteralExpr(t, bd); .)
+ | BvLit<out bn, out n> (. e = new LiteralExpr(t, bn, n); .)
+
+ | Ident<out x> (. id = new IdentifierExpr(x, x.val); e = id; .)
+ [ "("
+ ( Expressions<out es> (. e = new NAryExpr(x, new FunctionCall(id), es); .)
+ | /* empty */ (. e = new NAryExpr(x, new FunctionCall(id), new List<Expr>()); .)
+ )
+ ")"
+ ]
+
+ | "old" (. x = t; .)
+ "("
+ Expression<out e>
+ ")" (. e = new OldExpr(x, e); .)
+
+ | "int" (. x = t; .)
+ "("
+ Expression<out e>
+ ")" (. e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToInt), new List<Expr>{ e }); .)
+
+ | "real" (. x = t; .)
+ "("
+ Expression<out e>
+ ")" (. e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToReal), new List<Expr>{ e }); .)
+
+ | "(" ( Expression<out e> (. if (e is BvBounds)
+ this.SemErr("parentheses around bitvector bounds " +
+ "are not allowed"); .)
+ | 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); .)
+ | 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); .)
+ | 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); .)
+ )
+ ")"
+ | IfThenElseExpression<out e>
+ | CodeExpression<out locals, out blocks> (. e = new CodeExpr(locals, blocks); .)
+ )
+ .
+
+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/*!*/>();
+ .)
+ "|{"
+ { LocalVars<locals> }
+ SpecBlock<out b> (. blocks.Add(b); .)
+ { SpecBlock<out b> (. blocks.Add(b); .)
+ }
+ "}|"
+ .
+
+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> ":"
+ { 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");
+ }
+ .)
+ }
+ ( "goto" (. 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));
+ .)
+ | "return" Expression<out e>
+ (. b = new Block(x,x.val,cs,new ReturnExprCmd(t,e)); .)
+ )
+ ";"
+ .
+
+Attribute<ref QKeyValue kv>
+= (. Trigger trig = null; .)
+ AttributeOrTrigger<ref kv, ref trig> (. if (trig != null) this.SemErr("only attributes, not triggers, allowed here"); .)
+.
+
+AttributeOrTrigger<ref QKeyValue kv, ref Trigger trig>
+= (. IToken/*!*/ tok; Expr/*!*/ e; List<Expr>/*!*/ es;
+ string key;
+ List<object/*!*/> parameters; object/*!*/ param;
+ .)
+ "{" (. tok = t; .)
+ (
+ ":" ident (. key = t.val; parameters = new List<object/*!*/>(); .)
+ [ AttributeParameter<out param> (. parameters.Add(param); .)
+ { "," 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));
+ }
+ }
+ .)
+ |
+ Expression<out e> (. es = new List<Expr> { e }; .)
+ { "," 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));
+ }
+ .)
+ )
+ "}"
+ .
+
+AttributeParameter<out object/*!*/ o>
+= (. Contract.Ensures(Contract.ValueAtReturn(out o) != null);
+ o = "error";
+ Expr/*!*/ e;
+ .)
+ ( string (. o = t.val.Substring(1, t.val.Length-2); .)
+ | Expression<out e> (. o = e; .)
+ )
+ .
+
+IfThenElseExpression<out Expr/*!*/ e>
+= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null);
+ IToken/*!*/ tok;
+ Expr/*!*/ e0, e1, e2;
+ e = dummyExpr; .)
+ "if" (. tok = t; .) Expression<out e0> "then" Expression<out e1> "else" Expression<out e2>
+ (. e = new NAryExpr(tok, new IfThenElse(tok), new List<Expr>{ e0, e1, e2 }); .)
+ .
+
+
+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> ();
+ .)
+ (
+ TypeParams<out tok, out typeParams>
+ [ BoundVars<q, out ds> ]
+ |
+ BoundVars<q, out ds>
+ )
+ QSep
+ { AttributeOrTrigger<ref kv, ref trig> }
+ Expression<out body>
+ .
+
+Forall = "forall" | '\u2200'.
+Exists = "exists" | '\u2203'.
+Lambda = "lambda" | '\u03bb'.
+QSep = "::" | '\u2022'.
+
+/*------------------------------------------------------------------------*/
+Ident<out IToken/*!*/ x>
+=(.Contract.Ensures(Contract.ValueAtReturn(out x) != null);.)
+ ident (. x = t;
+ if (x.val.StartsWith("\\"))
+ x.val = x.val.Substring(1);
+ .)
+ .
+
+/*------------------------------------------------------------------------*/
+Nat<out BigNum n>
+=
+ digits
+ (. try {
+ n = BigNum.FromString(t.val);
+ } catch (FormatException) {
+ this.SemErr("incorrectly formatted number");
+ n = BigNum.ZERO;
+ }
+ .)
+ .
+
+/*------------------------------------------------------------------------*/
+Dec<out BigDec n>
+= (. string s = ""; .)
+ (
+ decimal (. s = t.val; .)
+ |
+ float (. s = t.val; .)
+ )
+ (. try {
+ n = BigDec.FromString(s);
+ } catch (FormatException) {
+ this.SemErr("incorrectly formatted number");
+ n = BigDec.ZERO;
+ }
+ .)
+ .
+
+/*------------------------------------------------------------------------*/
+BvLit<out BigNum n, out int m>
+=
+ bvlit
+ (.
+ 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;
+ }
+ .)
+ .
+END BoogiePL.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 03:11:44 +0000