diff options
Diffstat (limited to 'Source/Core/BoogiePL.atg')
-rw-r--r-- | Source/Core/BoogiePL.atg | 3022 |
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. |