From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 23:14:18 -0600 Subject: Merging complete. Everything looks good *crosses fingers* --- Source/Core/BoogiePL.atg | 3022 +++++++++++++++++++++++----------------------- 1 file changed, 1511 insertions(+), 1511 deletions(-) (limited to 'Source/Core/BoogiePL.atg') 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/*!*/ dummyExprSeq; -readonly TransferCmd/*!*/ dummyTransferCmd; -readonly StructuredCmd/*!*/ dummyStructuredCmd; - -/// -///Returns the number of parsing errors encountered. If 0, "program" returns as -///the parsed program. -/// -public static int Parse (string/*!*/ filename, /*maybe null*/ List 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(); - } - - 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(), new ReturnCmd(Token.NoToken)); - dummyType = new BasicType(Token.NoToken, SimpleType.Bool); - dummyExprSeq = new List (); - 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() != 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/*!*/ 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/*!*/ vs; - List/*!*/ ds; - Axiom/*!*/ ax; - List/*!*/ ts; - Procedure/*!*/ pr; - Implementation im; - Implementation/*!*/ nnim; - .) - { Consts (. foreach(Bpl.Variable/*!*/ v in vs){ - Contract.Assert(v != null); - Pgm.AddTopLevelDeclaration(v); - } - .) - | Function (. foreach(Bpl.Declaration/*!*/ d in ds){ - Contract.Assert(d != null); - Pgm.AddTopLevelDeclaration(d); - } - .) - | Axiom (. Pgm.AddTopLevelDeclaration(ax); .) - | UserDefinedTypes (. foreach(Declaration/*!*/ td in ts){ - Contract.Assert(td != null); - Pgm.AddTopLevelDeclaration(td); - } - .) - | GlobalVars (. foreach(Bpl.Variable/*!*/ v in vs){ - Contract.Assert(v != null); - Pgm.AddTopLevelDeclaration(v); - } - .) - | Procedure (. Pgm.AddTopLevelDeclaration(pr); - if (im != null) { - Pgm.AddTopLevelDeclaration(im); - } - .) - | Implementation (. Pgm.AddTopLevelDeclaration(nnim); .) - } - EOF - . - -/*------------------------------------------------------------------------*/ -GlobalVars<.out List/*!*/ ds.> -= (. - Contract.Ensures(Contract.ValueAtReturn(out ds) != null); - QKeyValue kv = null; - ds = new List(); - var dsx = ds; - .) - "var" - { Attribute } - IdsTypeWheres ";" - . - -LocalVars<.List/*!*/ ds.> -= (. - Contract.Ensures(Contract.ValueAtReturn(out ds) != null); - QKeyValue kv = null; - .) - "var" - { Attribute } - IdsTypeWheres ";" - . - -ProcFormals<.bool incoming, bool allowWhereClauses, out List/*!*/ ds.> -= (. Contract.Ensures(Contract.ValueAtReturn(out ds) != null); - ds = new List(); - var dsx = ds; - var context = allowWhereClauses ? "procedure formals" : "the 'implementation' copies of formals"; - .) - "(" - [ AttrsIdsTypeWheres - ] - ")" - . - -BoundVars<.IToken/*!*/ x, out List/*!*/ ds.> -= (. - Contract.Requires(x != null); - Contract.Ensures(Contract.ValueAtReturn(out ds) != null); - List/*!*/ tyds = new List(); - ds = new List(); - var dsx = ds; - .) - AttrsIdsTypeWheres - . - -/*------------------------------------------------------------------------*/ -/* IdsType is used with const declarations */ -IdsType<.out List/*!*/ tyds.> -= (. Contract.Ensures(Contract.ValueAtReturn(out tyds) != null); List/*!*/ ids; Bpl.Type/*!*/ ty; .) - Idents ":" Type - (. tyds = new List(); - 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 action .> -= - AttributesIdsTypeWhere - { "," AttributesIdsTypeWhere } - . - -IdsTypeWheres<. bool allowWhereClauses, string context, System.Action action .> -= - IdsTypeWhere - { "," IdsTypeWhere } - . - -AttributesIdsTypeWhere<. bool allowAttributes, bool allowWhereClauses, string context, System.Action action .> -= (. QKeyValue kv = null; .) - { Attribute (. if (!allowAttributes) { - kv = null; - this.SemErr("attributes are not allowed on " + context); - } - .) - } - IdsTypeWhere - . - -/* context is allowed to be null if allowWhereClauses is true */ -IdsTypeWhere<. bool allowWhereClauses, string context, System.Action action .> -= (. List/*!*/ ids; Bpl.Type/*!*/ ty; Expr wh = null; Expr/*!*/ nne; .) - Idents ":" Type - [ "where" Expression (. 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 -= (.Contract.Ensures(Contract.ValueAtReturn(out ty) != null); IToken/*!*/ tok; ty = dummyType; .) - ( - TypeAtom - | - Ident (. List/*!*/ args = new List (); .) - [ TypeArgs ] (. ty = new UnresolvedTypeIdentifier (tok, tok.val, args); .) - | - MapType - ) - . - -TypeArgs<.List/*!*/ ts.> -= (.Contract.Requires(ts != null); IToken/*!*/ tok; Bpl.Type/*!*/ ty; .) - ( - TypeAtom (. ts.Add(ty); .) - [ TypeArgs ] - | - Ident (. List/*!*/ args = new List (); - ts.Add(new UnresolvedTypeIdentifier (tok, tok.val, args)); .) - [ TypeArgs ] - | - MapType (. ts.Add(ty); .) - ) - . - -TypeAtom -= (.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 - ")" - ) - . - -MapType -= (.Contract.Ensures(Contract.ValueAtReturn(out ty) != null); IToken tok = null; - IToken/*!*/ nnTok; - List/*!*/ arguments = new List(); - Bpl.Type/*!*/ result; - List/*!*/ typeParameters = new List(); - .) - [ TypeParams (. tok = nnTok; .) ] - "[" (. if (tok == null) tok = t; .) - [ Types ] - "]" - Type - (. - ty = new MapType(tok, typeParameters, arguments, result); - .) - . - -TypeParams<.out IToken/*!*/ tok, out List/*!*/ typeParams.> -= (.Contract.Ensures(Contract.ValueAtReturn(out tok) != null); Contract.Ensures(Contract.ValueAtReturn(out typeParams) != null); List/*!*/ typeParamToks; .) - "<" (. tok = t; .) - Idents - ">" - (. - typeParams = new List (); - foreach(Token/*!*/ id in typeParamToks){ - Contract.Assert(id != null); - typeParams.Add(new TypeVariable(id, id.val));} - .) - . - -Types<.List/*!*/ ts.> -= (. Contract.Requires(ts != null); Bpl.Type/*!*/ ty; .) - Type (. ts.Add(ty); .) - { "," Type (. ts.Add(ty); .) - } - . - - -/*------------------------------------------------------------------------*/ -Consts<.out List/*!*/ ds.> -= (. Contract.Ensures(Contract.ValueAtReturn(out ds) != null); IToken/*!*/ y; List/*!*/ xs; - ds = new List(); - bool u = false; QKeyValue kv = null; - bool ChildrenComplete = false; - List Parents = null; .) - "const" (. y = t; .) - { Attribute } - [ "unique" (. u = true; .) - ] - IdsType - [ OrderSpec ] - (. bool makeClone = false; - foreach(TypedIdent/*!*/ x in xs){ - Contract.Assert(x != null); - - // ensure that no sharing is introduced - List ParentsClone; - if (makeClone && Parents != null) { - ParentsClone = new List (); - 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 Parents.> -= (.Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out Parents),true)); ChildrenComplete = false; - Parents = null; - bool u; - IToken/*!*/ parent; .) - "extends" (. Parents = new List (); - u = false; .) - [ - [ "unique" (. u = true; .) - ] - Ident (. Parents.Add(new ConstantParent ( - new IdentifierExpr(parent, parent.val), u)); .) - { - "," (. u = false; .) - [ "unique" (. u = true; .) - ] - Ident (. Parents.Add(new ConstantParent ( - new IdentifierExpr(parent, parent.val), u)); .) - } - ] - [ "complete" (. ChildrenComplete = true; .) - ] - . - -/*------------------------------------------------------------------------*/ -Function<.out List/*!*/ ds.> -= (. Contract.Ensures(Contract.ValueAtReturn(out ds) != null); - ds = new List(); IToken/*!*/ z; - IToken/*!*/ typeParamTok; - var typeParams = new List(); - var arguments = new List(); - TypedIdent/*!*/ tyd; - TypedIdent retTyd = null; - Bpl.Type/*!*/ retTy; - QKeyValue argKv = null; - QKeyValue kv = null; - Expr definition = null; - Expr/*!*/ tmp; - .) - "function" { Attribute } Ident - [ TypeParams ] - "(" - [ VarOrType (. arguments.Add(new Formal(tyd.tok, tyd, true, argKv)); .) - { "," VarOrType (. arguments.Add(new Formal(tyd.tok, tyd, true, argKv)); .) - } ] ")" - (. argKv = null; .) - ( - "returns" "(" VarOrType ")" - | - ":" Type (. retTyd = new TypedIdent(retTy.tok, TypedIdent.NoName, retTy); .) - ) - ( "{" Expression (. 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 -= (. - Contract.Ensures(Contract.ValueAtReturn(out tyd) != null); - string/*!*/ varName = TypedIdent.NoName; - Bpl.Type/*!*/ ty; - IToken/*!*/ tok; - kv = null; - .) - { Attribute } - Type (. 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 - ] - (. tyd = new TypedIdent(tok, varName, ty); .) - . - -/*------------------------------------------------------------------------*/ -Axiom -= (.Contract.Ensures(Contract.ValueAtReturn(out m) != null); Expr/*!*/ e; QKeyValue kv = null; .) - "axiom" - { Attribute } - (. IToken/*!*/ x = t; .) - Proposition ";" (. m = new Axiom(x,e, null, kv); .) - . - -/*------------------------------------------------------------------------*/ -UserDefinedTypes<.out List/*!*/ ts.> -= (. Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out ts))); Declaration/*!*/ decl; QKeyValue kv = null; ts = new List (); .) - "type" - { Attribute } - UserDefinedType (. ts.Add(decl); .) - { "," UserDefinedType (. ts.Add(decl); .) } - ";" - . - -UserDefinedType -= (. Contract.Ensures(Contract.ValueAtReturn(out decl) != null); IToken/*!*/ id; List/*!*/ paramTokens = new List (); - Bpl.Type/*!*/ body = dummyType; bool synonym = false; .) - Ident - [ WhiteSpaceIdents ] - [ - "=" Type - (. synonym = true; .) - ] - (. - if (synonym) { - List/*!*/ typeParams = new List(); - 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 -= (. Contract.Ensures(Contract.ValueAtReturn(out proc) != null); IToken/*!*/ x; - List/*!*/ typeParams; - List/*!*/ ins, outs; - List/*!*/ pre = new List(); - List/*!*/ mods = new List(); - List/*!*/ post = new List(); - - List/*!*/ locals = new List(); - StmtList/*!*/ stmtList; - QKeyValue kv = null; - impl = null; - .) - - "procedure" - ProcSignature - ( ";" - { Spec } - | { Spec } - ImplBody - (. - 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 -= (. Contract.Ensures(Contract.ValueAtReturn(out impl) != null); IToken/*!*/ x; - List/*!*/ typeParams; - List/*!*/ ins, outs; - List/*!*/ locals; - StmtList/*!*/ stmtList; - QKeyValue kv; - .) - - "implementation" - ProcSignature - ImplBody - (. impl = new Implementation(x, x.val, typeParams, ins, outs, locals, stmtList, kv, this.errors); .) - . - - -ProcSignature<.bool allowWhereClausesOnFormals, out IToken/*!*/ name, out List/*!*/ typeParams, - out List/*!*/ ins, out List/*!*/ 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(); - outs = new List(); kv = null; .) - { Attribute } - Ident - [ TypeParams ] - ProcFormals - [ "returns" ProcFormals ] - . - - -Spec<.List/*!*/ pre, List/*!*/ mods, List/*!*/ post.> -= (.Contract.Requires(pre != null); Contract.Requires(mods != null); Contract.Requires(post != null); List/*!*/ ms; .) - ( "modifies" - [ Idents (. foreach(IToken/*!*/ m in ms){ - Contract.Assert(m != null); - mods.Add(new IdentifierExpr(m, m.val)); - } - .) - ] ";" - | "free" SpecPrePost - | SpecPrePost - ) - . - -SpecPrePost<.bool free, List/*!*/ pre, List/*!*/ post.> -= (. Contract.Requires(pre != null); Contract.Requires(post != null); Expr/*!*/ e; Token tok = null; QKeyValue kv = null; .) - ( "requires" (. tok = t; .) - { Attribute } - Proposition ";" (. pre.Add(new Requires(tok, free, e, null, kv)); .) - | "ensures" (. tok = t; .) - { Attribute } - Proposition ";" (. post.Add(new Ensures(tok, free, e, null, kv)); .) - ) - . - -/*------------------------------------------------------------------------*/ - -ImplBody<.out List/*!*/ locals, out StmtList/*!*/ stmtList.> -= (. Contract.Ensures(Contract.ValueAtReturn(out locals) != null); Contract.Ensures(Contract.ValueAtReturn(out stmtList) != null); locals = new List(); .) - "{" - { LocalVars } - StmtList - . - -/* the StmtList also reads the final curly brace */ -StmtList -= (. Contract.Ensures(Contract.ValueAtReturn(out stmtList) != null); List bigblocks = new List(); - /* built-up state for the current BigBlock: */ - IToken startToken = null; string currentLabel = null; - List 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 - (. if (c != null) { - // LabelOrCmd read a Cmd - Contract.Assert(label == null); - if (startToken == null) { startToken = c.tok; cs = new List(); } - 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(); - } - .) - - | StructuredCmd - (. ec = ecn; - if (startToken == null) { startToken = ec.tok; cs = new List(); } - Contract.Assert(cs != null); - b = new BigBlock(startToken, currentLabel, cs, ec, null); - bigblocks.Add(b); - startToken = null; currentLabel = null; cs = null; - .) - - | TransferCmd - (. tc = tcn; - if (startToken == null) { startToken = tc.tok; cs = new List(); } - 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(); - } - if (startToken != null) { - Contract.Assert(cs != null); - b = new BigBlock(startToken, currentLabel, cs, null, null); - bigblocks.Add(b); - } - - stmtList = new StmtList(bigblocks, endCurly); - .) - . - -TransferCmd -= (. Contract.Ensures(Contract.ValueAtReturn(out tc) != null); tc = dummyTransferCmd; - Token y; List/*!*/ xs; - List ss = new List(); - .) - ( "goto" (. y = t; .) - Idents (. foreach(IToken/*!*/ s in xs){ - Contract.Assert(s != null); - ss.Add(s.val); } - tc = new GotoCmd(y, ss); - .) - | "return" (. tc = new ReturnCmd(t); .) - ) ";" - . - -StructuredCmd -= (. Contract.Ensures(Contract.ValueAtReturn(out ec) != null); ec = dummyStructuredCmd; Contract.Assume(cce.IsPeerConsistent(ec)); - IfCmd/*!*/ ifcmd; WhileCmd/*!*/ wcmd; BreakCmd/*!*/ bcmd; - .) - ( IfCmd (. ec = ifcmd; .) - | WhileCmd (. ec = wcmd; .) - | BreakCmd (. ec = bcmd; .) - ) - . - -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 - "{" StmtList - [ "else" - ( IfCmd (. elseIfOption = elseIf; .) - | "{" - StmtList (. elseOption = els; .) - ) - ] - (. ifcmd = new IfCmd(x, guard, thn, elseIfOption, elseOption); .) - . - -WhileCmd -= (. Contract.Ensures(Contract.ValueAtReturn(out wcmd) != null); IToken/*!*/ x; Token z; - Expr guard; Expr/*!*/ e; bool isFree; - List invariants = new List(); - StmtList/*!*/ body; - QKeyValue kv = null; - .) - "while" (. x = t; .) - Guard (. Contract.Assume(guard == null || cce.Owner.None(guard)); .) - { (. isFree = false; z = la/*lookahead token*/; .) - [ "free" (. isFree = true; .) - ] - "invariant" - { Attribute } - Expression (. if (isFree) { - invariants.Add(new AssumeCmd(z, e, kv)); - } else { - invariants.Add(new AssertCmd(z, e, kv)); - } - kv = null; - .) - ";" - } - "{" - StmtList (. wcmd = new WhileCmd(x, guard, invariants, body); .) - . - -Guard -= (. Expr/*!*/ ee; e = null; .) - "(" - ( "*" (. e = null; .) - | Expression (. e = ee; .) - ) - ")" - . - -BreakCmd -= (.Contract.Ensures(Contract.ValueAtReturn(out bcmd) != null); IToken/*!*/ x; IToken/*!*/ y; - string breakLabel = null; - .) - "break" (. x = t; .) - [ Ident (. breakLabel = y.val; .) - ] ";" (. bcmd = new BreakCmd(x, breakLabel); .) - . - -/*------------------------------------------------------------------------*/ - -LabelOrCmd -/* ensures (c == null) != (label != null) */ -= (. IToken/*!*/ x; Expr/*!*/ e; - List/*!*/ xs; - List ids; - c = dummyCmd; label = null; - Cmd/*!*/ cn; - QKeyValue kv = null; - .) - ( LabelOrAssign - | "assert" (. x = t; .) - { Attribute } - Proposition (. c = new AssertCmd(x, e, kv); .) - ";" - | "assume" (. x = t; .) - { Attribute } - Proposition (. c = new AssumeCmd(x, e, kv); .) - ";" - | "havoc" (. x = t; .) - Idents ";" (. ids = new List(); - foreach(IToken/*!*/ y in xs){ - Contract.Assert(y != null); - ids.Add(new IdentifierExpr(y, y.val)); - } - c = new HavocCmd(x,ids); - .) - | CallCmd ";" (. c = cn; .) - | ParCallCmd (. c = cn; .) - | "yield" (. x = t; .) - ";" (. c = new YieldCmd(x); .) - ) - . - -/*------------------------------------------------------------------------*/ - -LabelOrAssign -/* ensures (c == null) != (label != null) */ -= (. IToken/*!*/ id; IToken/*!*/ x, y; Expr/*!*/ e0; - c = dummyCmd; label = null; - AssignLhs/*!*/ lhs; - List/*!*/ lhss; - List/*!*/ rhss; - List/*!*/ indexes; - .) - Ident (. x = t; .) - ( ":" (. c = null; label = x; .) - - | (. lhss = new List(); .) - (. lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val)); .) - - { MapAssignIndex (. lhs = new MapAssignLhs(y, lhs, indexes); .) } - (. lhss.Add(lhs); .) - - { "," - Ident - (. lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val)); .) - { MapAssignIndex (. lhs = new MapAssignLhs(y, lhs, indexes); .) } - (. lhss.Add(lhs); .) - } - - ":=" (. x = t; /* use location of := */ .) - Expression (. rhss = new List (); - rhss.Add(e0); .) - { "," - Expression (. rhss.Add(e0); .) - } - ";" (. c = new AssignCmd(x, lhss, rhss); .) - ) - . - -MapAssignIndex<.out IToken/*!*/ x, out List/*!*/ indexes.> -= (.Contract.Ensures(Contract.ValueAtReturn(out x) != null); Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out indexes))); indexes = new List (); - Expr/*!*/ e; - .) - "[" (. x = t; .) - [ - Expression (. indexes.Add(e); .) - { "," - Expression (. indexes.Add(e); .) - } - ] - "]" - . - -/*------------------------------------------------------------------------*/ -CallCmd -= (. 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 } - CallParams (. .) - . - -ParCallCmd -= (. Contract.Ensures(Contract.ValueAtReturn(out d) != null); - IToken x; - QKeyValue kv = null; - Cmd c = null; - List callCmds = new List(); - .) - "par" (. x = t; .) - { Attribute } - CallParams (. callCmds.Add((CallCmd)c); .) - { "|" CallParams (. callCmds.Add((CallCmd)c); .) - } - ";" (. d = new ParCallCmd(x, callCmds, kv); .) - . - -CallParams -= (. - List ids = new List(); - List es = new List(); - Expr en; - IToken first; - IToken p; - c = null; - .) - Ident - ( "(" - [ Expression (. es.Add(en); .) - { "," Expression (. 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 (. ids.Add(new IdentifierExpr(p, p.val)); .) - { "," Ident (. ids.Add(new IdentifierExpr(p, p.val)); .) - } - ] ":=" - Ident "(" - [ Expression (. es.Add(en); .) - { "," Expression (. es.Add(en); .) - } - ] - ")" (. c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync; .) - ) - . - -/*------------------------------------------------------------------------*/ -Proposition -=(.Contract.Ensures(Contract.ValueAtReturn(out e) != null);.) - Expression - . - -/*------------------------------------------------------------------------*/ -Idents<.out List/*!*/ xs.> -= (.Contract.Ensures(Contract.ValueAtReturn(out xs) != null); IToken/*!*/ id; xs = new List(); .) - Ident (. xs.Add(id); .) - { "," Ident (. xs.Add(id); .) - } - . - -/*------------------------------------------------------------------------*/ -WhiteSpaceIdents<.out List/*!*/ xs.> -= (. Contract.Ensures(Contract.ValueAtReturn(out xs) != null); IToken/*!*/ id; xs = new List(); .) - Ident (. xs.Add(id); .) - { Ident (. xs.Add(id); .) - } - . - -/*------------------------------------------------------------------------*/ -Expressions<.out List/*!*/ es.> -= (. Contract.Ensures(Contract.ValueAtReturn(out es) != null); Expr/*!*/ e; es = new List(); .) - Expression (. es.Add(e); .) - { "," Expression (. es.Add(e); .) - } - . - -/*------------------------------------------------------------------------*/ -Expression<.out Expr/*!*/ e0.> -= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; .) - ImpliesExpression - { EquivOp (. x = t; .) - ImpliesExpression - (. e0 = Expr.Binary(x, BinaryOperator.Opcode.Iff, e0, e1); .) - } - . - -EquivOp = "<==>" | '\u21d4'. - -/*------------------------------------------------------------------------*/ -ImpliesExpression -= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; .) - LogicalExpression - [ - ImpliesOp (. x = t; .) - /* recurse because implication is right-associative */ - ImpliesExpression - (. 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 - (. e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e1, e0); .) - /* loop because explies is left-associative */ - { - ExpliesOp (. x = t; .) - LogicalExpression - (. e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e1, e0); .) - } - ] - . - -ImpliesOp = "==>" | '\u21d2'. -ExpliesOp = "<==" | '\u21d0'. - -/*------------------------------------------------------------------------*/ -LogicalExpression -= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; .) - RelationalExpression - [ AndOp (. x = t; .) - RelationalExpression - (. e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1); .) - { AndOp (. x = t; .) - RelationalExpression - (. e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1); .) - } - | OrOp (. x = t; .) - RelationalExpression - (. e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1); .) - { OrOp (. x = t; .) - RelationalExpression - (. e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1); .) - } - ] - . - -AndOp = "&&" | '\u2227'. -OrOp = "||" | '\u2228'. - -/*------------------------------------------------------------------------*/ -RelationalExpression -= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; BinaryOperator.Opcode op; .) - BvTerm - [ RelOp - BvTerm (. e0 = Expr.Binary(x, op, e0, e1); .) - ] - . - -RelOp -= (.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 -= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; .) - Term - { "++" (. x = t; .) - Term (. e0 = new BvConcatExpr(x, e0, e1); .) - } - . - - -/*------------------------------------------------------------------------*/ -Term -= (.Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; BinaryOperator.Opcode op; .) - Factor - { AddOp - Factor (. e0 = Expr.Binary(x, op, e0, e1); .) - } - . - -AddOp -= (.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 -= (.Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; BinaryOperator.Opcode op; .) - Power - { MulOp - Power (. e0 = Expr.Binary(x, op, e0, e1); .) - } - . - -MulOp -= (. 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 -= (.Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; .) - UnaryExpression - [ - "**" (. x = t; .) - /* recurse because exponentation is right-associative */ - Power (. e0 = Expr.Binary(x, BinaryOperator.Opcode.Pow, e0, e1); .) - ] - . - -/*------------------------------------------------------------------------*/ -UnaryExpression -= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; - e = dummyExpr; - .) - ( "-" (. x = t; .) - UnaryExpression (. e = Expr.Unary(x, UnaryOperator.Opcode.Neg, e); .) - | NegOp (. x = t; .) - UnaryExpression (. e = Expr.Unary(x, UnaryOperator.Opcode.Not, e); .) - | CoercionExpression - ) - . - -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 -= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; - Bpl.Type/*!*/ coercedTo; - BigNum bn; - .) - ArrayExpression - { ":" (. x = t; .) - ( - Type (. e = Expr.CoerceType(x, e, coercedTo); .) - | - Nat /* 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 -= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; - Expr/*!*/ index0 = dummyExpr; Expr/*!*/ e1; - bool store; bool bvExtract; - List/*!*/ allArgs = dummyExprSeq; - .) - AtomExpression - { "[" (. x = t; allArgs = new List (); - allArgs.Add(e); - store = false; bvExtract = false; .) - [ - Expression - (. if (index0 is BvBounds) - bvExtract = true; - else - allArgs.Add(index0); - .) - { "," Expression - (. if (bvExtract || e1 is BvBounds) - this.SemErr("bitvectors only have one dimension"); - allArgs.Add(e1); - .) - } - [ ":=" Expression - (. if (bvExtract || e1 is BvBounds) - this.SemErr("assignment to bitvectors is not possible"); - allArgs.Add(e1); store = true; - .) - ] - | ":=" Expression (. 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 -= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; int n; BigNum bn; BigDec bd; - List/*!*/ es; List/*!*/ ds; Trigger trig; - List/*!*/ typeParams; - IdentifierExpr/*!*/ id; - QKeyValue kv; - e = dummyExpr; - List/*!*/ locals; - List/*!*/ blocks; - .) - ( "false" (. e = new LiteralExpr(t, false); .) - | "true" (. e = new LiteralExpr(t, true); .) - | Nat (. e = new LiteralExpr(t, bn); .) - | Dec (. e = new LiteralExpr(t, bd); .) - | BvLit (. e = new LiteralExpr(t, bn, n); .) - - | Ident (. id = new IdentifierExpr(x, x.val); e = id; .) - [ "(" - ( Expressions (. e = new NAryExpr(x, new FunctionCall(id), es); .) - | /* empty */ (. e = new NAryExpr(x, new FunctionCall(id), new List()); .) - ) - ")" - ] - - | "old" (. x = t; .) - "(" - Expression - ")" (. e = new OldExpr(x, e); .) - - | "int" (. x = t; .) - "(" - Expression - ")" (. e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToInt), new List{ e }); .) - - | "real" (. x = t; .) - "(" - Expression - ")" (. e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToReal), new List{ e }); .) - - | "(" ( Expression (. if (e is BvBounds) - this.SemErr("parentheses around bitvector bounds " + - "are not allowed"); .) - | Forall (. x = t; .) - QuantifierBody - (. if (typeParams.Count + ds.Count > 0) - e = new ForallExpr(x, typeParams, ds, kv, trig, e); .) - | Exists (. x = t; .) - QuantifierBody - (. if (typeParams.Count + ds.Count > 0) - e = new ExistsExpr(x, typeParams, ds, kv, trig, e); .) - | Lambda (. x = t; .) - QuantifierBody - (. 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 - | CodeExpression (. e = new CodeExpr(locals, blocks); .) - ) - . - -CodeExpression<.out List/*!*/ locals, out List/*!*/ blocks.> -= (. Contract.Ensures(Contract.ValueAtReturn(out locals) != null); Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out blocks))); locals = new List(); Block/*!*/ b; - blocks = new List(); - .) - "|{" - { LocalVars } - SpecBlock (. blocks.Add(b); .) - { SpecBlock (. blocks.Add(b); .) - } - "}|" - . - -SpecBlock -= (. Contract.Ensures(Contract.ValueAtReturn(out b) != null); IToken/*!*/ x; IToken/*!*/ y; - Cmd c; IToken label; - List cs = new List(); - List/*!*/ xs; - List ss = new List(); - b = dummyBlock; - Expr/*!*/ e; - .) - Ident ":" - { LabelOrCmd - (. 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 (. 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 - (. b = new Block(x,x.val,cs,new ReturnExprCmd(t,e)); .) - ) - ";" - . - -Attribute -= (. Trigger trig = null; .) - AttributeOrTrigger (. if (trig != null) this.SemErr("only attributes, not triggers, allowed here"); .) -. - -AttributeOrTrigger -= (. IToken/*!*/ tok; Expr/*!*/ e; List/*!*/ es; - string key; - List parameters; object/*!*/ param; - .) - "{" (. tok = t; .) - ( - ":" ident (. key = t.val; parameters = new List(); .) - [ AttributeParameter (. parameters.Add(param); .) - { "," AttributeParameter (. 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 { e }, null); - } else { - trig.AddLast(new Trigger(tok, false, new List { 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 (. es = new List { e }; .) - { "," Expression (. es.Add(e); .) - } (. if (trig==null) { - trig = new Trigger(tok, true, es, null); - } else { - trig.AddLast(new Trigger(tok, true, es, null)); - } - .) - ) - "}" - . - -AttributeParameter -= (. Contract.Ensures(Contract.ValueAtReturn(out o) != null); - o = "error"; - Expr/*!*/ e; - .) - ( string (. o = t.val.Substring(1, t.val.Length-2); .) - | Expression (. o = e; .) - ) - . - -IfThenElseExpression -= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); - IToken/*!*/ tok; - Expr/*!*/ e0, e1, e2; - e = dummyExpr; .) - "if" (. tok = t; .) Expression "then" Expression "else" Expression - (. e = new NAryExpr(tok, new IfThenElse(tok), new List{ e0, e1, e2 }); .) - . - - -QuantifierBody<.IToken/*!*/ q, out List/*!*/ typeParams, out List/*!*/ 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 (); - IToken/*!*/ tok; - kv = null; - ds = new List (); - .) - ( - TypeParams - [ BoundVars ] - | - BoundVars - ) - QSep - { AttributeOrTrigger } - Expression - . - -Forall = "forall" | '\u2200'. -Exists = "exists" | '\u2203'. -Lambda = "lambda" | '\u03bb'. -QSep = "::" | '\u2022'. - -/*------------------------------------------------------------------------*/ -Ident -=(.Contract.Ensures(Contract.ValueAtReturn(out x) != null);.) - ident (. x = t; - if (x.val.StartsWith("\\")) - x.val = x.val.Substring(1); - .) - . - -/*------------------------------------------------------------------------*/ -Nat -= - digits - (. try { - n = BigNum.FromString(t.val); - } catch (FormatException) { - this.SemErr("incorrectly formatted number"); - n = BigNum.ZERO; - } - .) - . - -/*------------------------------------------------------------------------*/ -Dec -= (. 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 -= - 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/*!*/ dummyExprSeq; +readonly TransferCmd/*!*/ dummyTransferCmd; +readonly StructuredCmd/*!*/ dummyStructuredCmd; + +/// +///Returns the number of parsing errors encountered. If 0, "program" returns as +///the parsed program. +/// +public static int Parse (string/*!*/ filename, /*maybe null*/ List 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(); + } + + 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(), new ReturnCmd(Token.NoToken)); + dummyType = new BasicType(Token.NoToken, SimpleType.Bool); + dummyExprSeq = new List (); + 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() != 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/*!*/ 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/*!*/ vs; + List/*!*/ ds; + Axiom/*!*/ ax; + List/*!*/ ts; + Procedure/*!*/ pr; + Implementation im; + Implementation/*!*/ nnim; + .) + { Consts (. foreach(Bpl.Variable/*!*/ v in vs){ + Contract.Assert(v != null); + Pgm.AddTopLevelDeclaration(v); + } + .) + | Function (. foreach(Bpl.Declaration/*!*/ d in ds){ + Contract.Assert(d != null); + Pgm.AddTopLevelDeclaration(d); + } + .) + | Axiom (. Pgm.AddTopLevelDeclaration(ax); .) + | UserDefinedTypes (. foreach(Declaration/*!*/ td in ts){ + Contract.Assert(td != null); + Pgm.AddTopLevelDeclaration(td); + } + .) + | GlobalVars (. foreach(Bpl.Variable/*!*/ v in vs){ + Contract.Assert(v != null); + Pgm.AddTopLevelDeclaration(v); + } + .) + | Procedure (. Pgm.AddTopLevelDeclaration(pr); + if (im != null) { + Pgm.AddTopLevelDeclaration(im); + } + .) + | Implementation (. Pgm.AddTopLevelDeclaration(nnim); .) + } + EOF + . + +/*------------------------------------------------------------------------*/ +GlobalVars<.out List/*!*/ ds.> += (. + Contract.Ensures(Contract.ValueAtReturn(out ds) != null); + QKeyValue kv = null; + ds = new List(); + var dsx = ds; + .) + "var" + { Attribute } + IdsTypeWheres ";" + . + +LocalVars<.List/*!*/ ds.> += (. + Contract.Ensures(Contract.ValueAtReturn(out ds) != null); + QKeyValue kv = null; + .) + "var" + { Attribute } + IdsTypeWheres ";" + . + +ProcFormals<.bool incoming, bool allowWhereClauses, out List/*!*/ ds.> += (. Contract.Ensures(Contract.ValueAtReturn(out ds) != null); + ds = new List(); + var dsx = ds; + var context = allowWhereClauses ? "procedure formals" : "the 'implementation' copies of formals"; + .) + "(" + [ AttrsIdsTypeWheres + ] + ")" + . + +BoundVars<.IToken/*!*/ x, out List/*!*/ ds.> += (. + Contract.Requires(x != null); + Contract.Ensures(Contract.ValueAtReturn(out ds) != null); + List/*!*/ tyds = new List(); + ds = new List(); + var dsx = ds; + .) + AttrsIdsTypeWheres + . + +/*------------------------------------------------------------------------*/ +/* IdsType is used with const declarations */ +IdsType<.out List/*!*/ tyds.> += (. Contract.Ensures(Contract.ValueAtReturn(out tyds) != null); List/*!*/ ids; Bpl.Type/*!*/ ty; .) + Idents ":" Type + (. tyds = new List(); + 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 action .> += + AttributesIdsTypeWhere + { "," AttributesIdsTypeWhere } + . + +IdsTypeWheres<. bool allowWhereClauses, string context, System.Action action .> += + IdsTypeWhere + { "," IdsTypeWhere } + . + +AttributesIdsTypeWhere<. bool allowAttributes, bool allowWhereClauses, string context, System.Action action .> += (. QKeyValue kv = null; .) + { Attribute (. if (!allowAttributes) { + kv = null; + this.SemErr("attributes are not allowed on " + context); + } + .) + } + IdsTypeWhere + . + +/* context is allowed to be null if allowWhereClauses is true */ +IdsTypeWhere<. bool allowWhereClauses, string context, System.Action action .> += (. List/*!*/ ids; Bpl.Type/*!*/ ty; Expr wh = null; Expr/*!*/ nne; .) + Idents ":" Type + [ "where" Expression (. 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 += (.Contract.Ensures(Contract.ValueAtReturn(out ty) != null); IToken/*!*/ tok; ty = dummyType; .) + ( + TypeAtom + | + Ident (. List/*!*/ args = new List (); .) + [ TypeArgs ] (. ty = new UnresolvedTypeIdentifier (tok, tok.val, args); .) + | + MapType + ) + . + +TypeArgs<.List/*!*/ ts.> += (.Contract.Requires(ts != null); IToken/*!*/ tok; Bpl.Type/*!*/ ty; .) + ( + TypeAtom (. ts.Add(ty); .) + [ TypeArgs ] + | + Ident (. List/*!*/ args = new List (); + ts.Add(new UnresolvedTypeIdentifier (tok, tok.val, args)); .) + [ TypeArgs ] + | + MapType (. ts.Add(ty); .) + ) + . + +TypeAtom += (.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 + ")" + ) + . + +MapType += (.Contract.Ensures(Contract.ValueAtReturn(out ty) != null); IToken tok = null; + IToken/*!*/ nnTok; + List/*!*/ arguments = new List(); + Bpl.Type/*!*/ result; + List/*!*/ typeParameters = new List(); + .) + [ TypeParams (. tok = nnTok; .) ] + "[" (. if (tok == null) tok = t; .) + [ Types ] + "]" + Type + (. + ty = new MapType(tok, typeParameters, arguments, result); + .) + . + +TypeParams<.out IToken/*!*/ tok, out List/*!*/ typeParams.> += (.Contract.Ensures(Contract.ValueAtReturn(out tok) != null); Contract.Ensures(Contract.ValueAtReturn(out typeParams) != null); List/*!*/ typeParamToks; .) + "<" (. tok = t; .) + Idents + ">" + (. + typeParams = new List (); + foreach(Token/*!*/ id in typeParamToks){ + Contract.Assert(id != null); + typeParams.Add(new TypeVariable(id, id.val));} + .) + . + +Types<.List/*!*/ ts.> += (. Contract.Requires(ts != null); Bpl.Type/*!*/ ty; .) + Type (. ts.Add(ty); .) + { "," Type (. ts.Add(ty); .) + } + . + + +/*------------------------------------------------------------------------*/ +Consts<.out List/*!*/ ds.> += (. Contract.Ensures(Contract.ValueAtReturn(out ds) != null); IToken/*!*/ y; List/*!*/ xs; + ds = new List(); + bool u = false; QKeyValue kv = null; + bool ChildrenComplete = false; + List Parents = null; .) + "const" (. y = t; .) + { Attribute } + [ "unique" (. u = true; .) + ] + IdsType + [ OrderSpec ] + (. bool makeClone = false; + foreach(TypedIdent/*!*/ x in xs){ + Contract.Assert(x != null); + + // ensure that no sharing is introduced + List ParentsClone; + if (makeClone && Parents != null) { + ParentsClone = new List (); + 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 Parents.> += (.Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out Parents),true)); ChildrenComplete = false; + Parents = null; + bool u; + IToken/*!*/ parent; .) + "extends" (. Parents = new List (); + u = false; .) + [ + [ "unique" (. u = true; .) + ] + Ident (. Parents.Add(new ConstantParent ( + new IdentifierExpr(parent, parent.val), u)); .) + { + "," (. u = false; .) + [ "unique" (. u = true; .) + ] + Ident (. Parents.Add(new ConstantParent ( + new IdentifierExpr(parent, parent.val), u)); .) + } + ] + [ "complete" (. ChildrenComplete = true; .) + ] + . + +/*------------------------------------------------------------------------*/ +Function<.out List/*!*/ ds.> += (. Contract.Ensures(Contract.ValueAtReturn(out ds) != null); + ds = new List(); IToken/*!*/ z; + IToken/*!*/ typeParamTok; + var typeParams = new List(); + var arguments = new List(); + TypedIdent/*!*/ tyd; + TypedIdent retTyd = null; + Bpl.Type/*!*/ retTy; + QKeyValue argKv = null; + QKeyValue kv = null; + Expr definition = null; + Expr/*!*/ tmp; + .) + "function" { Attribute } Ident + [ TypeParams ] + "(" + [ VarOrType (. arguments.Add(new Formal(tyd.tok, tyd, true, argKv)); .) + { "," VarOrType (. arguments.Add(new Formal(tyd.tok, tyd, true, argKv)); .) + } ] ")" + (. argKv = null; .) + ( + "returns" "(" VarOrType ")" + | + ":" Type (. retTyd = new TypedIdent(retTy.tok, TypedIdent.NoName, retTy); .) + ) + ( "{" Expression (. 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 += (. + Contract.Ensures(Contract.ValueAtReturn(out tyd) != null); + string/*!*/ varName = TypedIdent.NoName; + Bpl.Type/*!*/ ty; + IToken/*!*/ tok; + kv = null; + .) + { Attribute } + Type (. 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 + ] + (. tyd = new TypedIdent(tok, varName, ty); .) + . + +/*------------------------------------------------------------------------*/ +Axiom += (.Contract.Ensures(Contract.ValueAtReturn(out m) != null); Expr/*!*/ e; QKeyValue kv = null; .) + "axiom" + { Attribute } + (. IToken/*!*/ x = t; .) + Proposition ";" (. m = new Axiom(x,e, null, kv); .) + . + +/*------------------------------------------------------------------------*/ +UserDefinedTypes<.out List/*!*/ ts.> += (. Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out ts))); Declaration/*!*/ decl; QKeyValue kv = null; ts = new List (); .) + "type" + { Attribute } + UserDefinedType (. ts.Add(decl); .) + { "," UserDefinedType (. ts.Add(decl); .) } + ";" + . + +UserDefinedType += (. Contract.Ensures(Contract.ValueAtReturn(out decl) != null); IToken/*!*/ id; List/*!*/ paramTokens = new List (); + Bpl.Type/*!*/ body = dummyType; bool synonym = false; .) + Ident + [ WhiteSpaceIdents ] + [ + "=" Type + (. synonym = true; .) + ] + (. + if (synonym) { + List/*!*/ typeParams = new List(); + 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 += (. Contract.Ensures(Contract.ValueAtReturn(out proc) != null); IToken/*!*/ x; + List/*!*/ typeParams; + List/*!*/ ins, outs; + List/*!*/ pre = new List(); + List/*!*/ mods = new List(); + List/*!*/ post = new List(); + + List/*!*/ locals = new List(); + StmtList/*!*/ stmtList; + QKeyValue kv = null; + impl = null; + .) + + "procedure" + ProcSignature + ( ";" + { Spec } + | { Spec } + ImplBody + (. + 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 += (. Contract.Ensures(Contract.ValueAtReturn(out impl) != null); IToken/*!*/ x; + List/*!*/ typeParams; + List/*!*/ ins, outs; + List/*!*/ locals; + StmtList/*!*/ stmtList; + QKeyValue kv; + .) + + "implementation" + ProcSignature + ImplBody + (. impl = new Implementation(x, x.val, typeParams, ins, outs, locals, stmtList, kv, this.errors); .) + . + + +ProcSignature<.bool allowWhereClausesOnFormals, out IToken/*!*/ name, out List/*!*/ typeParams, + out List/*!*/ ins, out List/*!*/ 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(); + outs = new List(); kv = null; .) + { Attribute } + Ident + [ TypeParams ] + ProcFormals + [ "returns" ProcFormals ] + . + + +Spec<.List/*!*/ pre, List/*!*/ mods, List/*!*/ post.> += (.Contract.Requires(pre != null); Contract.Requires(mods != null); Contract.Requires(post != null); List/*!*/ ms; .) + ( "modifies" + [ Idents (. foreach(IToken/*!*/ m in ms){ + Contract.Assert(m != null); + mods.Add(new IdentifierExpr(m, m.val)); + } + .) + ] ";" + | "free" SpecPrePost + | SpecPrePost + ) + . + +SpecPrePost<.bool free, List/*!*/ pre, List/*!*/ post.> += (. Contract.Requires(pre != null); Contract.Requires(post != null); Expr/*!*/ e; Token tok = null; QKeyValue kv = null; .) + ( "requires" (. tok = t; .) + { Attribute } + Proposition ";" (. pre.Add(new Requires(tok, free, e, null, kv)); .) + | "ensures" (. tok = t; .) + { Attribute } + Proposition ";" (. post.Add(new Ensures(tok, free, e, null, kv)); .) + ) + . + +/*------------------------------------------------------------------------*/ + +ImplBody<.out List/*!*/ locals, out StmtList/*!*/ stmtList.> += (. Contract.Ensures(Contract.ValueAtReturn(out locals) != null); Contract.Ensures(Contract.ValueAtReturn(out stmtList) != null); locals = new List(); .) + "{" + { LocalVars } + StmtList + . + +/* the StmtList also reads the final curly brace */ +StmtList += (. Contract.Ensures(Contract.ValueAtReturn(out stmtList) != null); List bigblocks = new List(); + /* built-up state for the current BigBlock: */ + IToken startToken = null; string currentLabel = null; + List 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 + (. if (c != null) { + // LabelOrCmd read a Cmd + Contract.Assert(label == null); + if (startToken == null) { startToken = c.tok; cs = new List(); } + 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(); + } + .) + + | StructuredCmd + (. ec = ecn; + if (startToken == null) { startToken = ec.tok; cs = new List(); } + Contract.Assert(cs != null); + b = new BigBlock(startToken, currentLabel, cs, ec, null); + bigblocks.Add(b); + startToken = null; currentLabel = null; cs = null; + .) + + | TransferCmd + (. tc = tcn; + if (startToken == null) { startToken = tc.tok; cs = new List(); } + 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(); + } + if (startToken != null) { + Contract.Assert(cs != null); + b = new BigBlock(startToken, currentLabel, cs, null, null); + bigblocks.Add(b); + } + + stmtList = new StmtList(bigblocks, endCurly); + .) + . + +TransferCmd += (. Contract.Ensures(Contract.ValueAtReturn(out tc) != null); tc = dummyTransferCmd; + Token y; List/*!*/ xs; + List ss = new List(); + .) + ( "goto" (. y = t; .) + Idents (. foreach(IToken/*!*/ s in xs){ + Contract.Assert(s != null); + ss.Add(s.val); } + tc = new GotoCmd(y, ss); + .) + | "return" (. tc = new ReturnCmd(t); .) + ) ";" + . + +StructuredCmd += (. Contract.Ensures(Contract.ValueAtReturn(out ec) != null); ec = dummyStructuredCmd; Contract.Assume(cce.IsPeerConsistent(ec)); + IfCmd/*!*/ ifcmd; WhileCmd/*!*/ wcmd; BreakCmd/*!*/ bcmd; + .) + ( IfCmd (. ec = ifcmd; .) + | WhileCmd (. ec = wcmd; .) + | BreakCmd (. ec = bcmd; .) + ) + . + +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 + "{" StmtList + [ "else" + ( IfCmd (. elseIfOption = elseIf; .) + | "{" + StmtList (. elseOption = els; .) + ) + ] + (. ifcmd = new IfCmd(x, guard, thn, elseIfOption, elseOption); .) + . + +WhileCmd += (. Contract.Ensures(Contract.ValueAtReturn(out wcmd) != null); IToken/*!*/ x; Token z; + Expr guard; Expr/*!*/ e; bool isFree; + List invariants = new List(); + StmtList/*!*/ body; + QKeyValue kv = null; + .) + "while" (. x = t; .) + Guard (. Contract.Assume(guard == null || cce.Owner.None(guard)); .) + { (. isFree = false; z = la/*lookahead token*/; .) + [ "free" (. isFree = true; .) + ] + "invariant" + { Attribute } + Expression (. if (isFree) { + invariants.Add(new AssumeCmd(z, e, kv)); + } else { + invariants.Add(new AssertCmd(z, e, kv)); + } + kv = null; + .) + ";" + } + "{" + StmtList (. wcmd = new WhileCmd(x, guard, invariants, body); .) + . + +Guard += (. Expr/*!*/ ee; e = null; .) + "(" + ( "*" (. e = null; .) + | Expression (. e = ee; .) + ) + ")" + . + +BreakCmd += (.Contract.Ensures(Contract.ValueAtReturn(out bcmd) != null); IToken/*!*/ x; IToken/*!*/ y; + string breakLabel = null; + .) + "break" (. x = t; .) + [ Ident (. breakLabel = y.val; .) + ] ";" (. bcmd = new BreakCmd(x, breakLabel); .) + . + +/*------------------------------------------------------------------------*/ + +LabelOrCmd +/* ensures (c == null) != (label != null) */ += (. IToken/*!*/ x; Expr/*!*/ e; + List/*!*/ xs; + List ids; + c = dummyCmd; label = null; + Cmd/*!*/ cn; + QKeyValue kv = null; + .) + ( LabelOrAssign + | "assert" (. x = t; .) + { Attribute } + Proposition (. c = new AssertCmd(x, e, kv); .) + ";" + | "assume" (. x = t; .) + { Attribute } + Proposition (. c = new AssumeCmd(x, e, kv); .) + ";" + | "havoc" (. x = t; .) + Idents ";" (. ids = new List(); + foreach(IToken/*!*/ y in xs){ + Contract.Assert(y != null); + ids.Add(new IdentifierExpr(y, y.val)); + } + c = new HavocCmd(x,ids); + .) + | CallCmd ";" (. c = cn; .) + | ParCallCmd (. c = cn; .) + | "yield" (. x = t; .) + ";" (. c = new YieldCmd(x); .) + ) + . + +/*------------------------------------------------------------------------*/ + +LabelOrAssign +/* ensures (c == null) != (label != null) */ += (. IToken/*!*/ id; IToken/*!*/ x, y; Expr/*!*/ e0; + c = dummyCmd; label = null; + AssignLhs/*!*/ lhs; + List/*!*/ lhss; + List/*!*/ rhss; + List/*!*/ indexes; + .) + Ident (. x = t; .) + ( ":" (. c = null; label = x; .) + + | (. lhss = new List(); .) + (. lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val)); .) + + { MapAssignIndex (. lhs = new MapAssignLhs(y, lhs, indexes); .) } + (. lhss.Add(lhs); .) + + { "," + Ident + (. lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val)); .) + { MapAssignIndex (. lhs = new MapAssignLhs(y, lhs, indexes); .) } + (. lhss.Add(lhs); .) + } + + ":=" (. x = t; /* use location of := */ .) + Expression (. rhss = new List (); + rhss.Add(e0); .) + { "," + Expression (. rhss.Add(e0); .) + } + ";" (. c = new AssignCmd(x, lhss, rhss); .) + ) + . + +MapAssignIndex<.out IToken/*!*/ x, out List/*!*/ indexes.> += (.Contract.Ensures(Contract.ValueAtReturn(out x) != null); Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out indexes))); indexes = new List (); + Expr/*!*/ e; + .) + "[" (. x = t; .) + [ + Expression (. indexes.Add(e); .) + { "," + Expression (. indexes.Add(e); .) + } + ] + "]" + . + +/*------------------------------------------------------------------------*/ +CallCmd += (. 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 } + CallParams (. .) + . + +ParCallCmd += (. Contract.Ensures(Contract.ValueAtReturn(out d) != null); + IToken x; + QKeyValue kv = null; + Cmd c = null; + List callCmds = new List(); + .) + "par" (. x = t; .) + { Attribute } + CallParams (. callCmds.Add((CallCmd)c); .) + { "|" CallParams (. callCmds.Add((CallCmd)c); .) + } + ";" (. d = new ParCallCmd(x, callCmds, kv); .) + . + +CallParams += (. + List ids = new List(); + List es = new List(); + Expr en; + IToken first; + IToken p; + c = null; + .) + Ident + ( "(" + [ Expression (. es.Add(en); .) + { "," Expression (. 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 (. ids.Add(new IdentifierExpr(p, p.val)); .) + { "," Ident (. ids.Add(new IdentifierExpr(p, p.val)); .) + } + ] ":=" + Ident "(" + [ Expression (. es.Add(en); .) + { "," Expression (. es.Add(en); .) + } + ] + ")" (. c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync; .) + ) + . + +/*------------------------------------------------------------------------*/ +Proposition +=(.Contract.Ensures(Contract.ValueAtReturn(out e) != null);.) + Expression + . + +/*------------------------------------------------------------------------*/ +Idents<.out List/*!*/ xs.> += (.Contract.Ensures(Contract.ValueAtReturn(out xs) != null); IToken/*!*/ id; xs = new List(); .) + Ident (. xs.Add(id); .) + { "," Ident (. xs.Add(id); .) + } + . + +/*------------------------------------------------------------------------*/ +WhiteSpaceIdents<.out List/*!*/ xs.> += (. Contract.Ensures(Contract.ValueAtReturn(out xs) != null); IToken/*!*/ id; xs = new List(); .) + Ident (. xs.Add(id); .) + { Ident (. xs.Add(id); .) + } + . + +/*------------------------------------------------------------------------*/ +Expressions<.out List/*!*/ es.> += (. Contract.Ensures(Contract.ValueAtReturn(out es) != null); Expr/*!*/ e; es = new List(); .) + Expression (. es.Add(e); .) + { "," Expression (. es.Add(e); .) + } + . + +/*------------------------------------------------------------------------*/ +Expression<.out Expr/*!*/ e0.> += (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; .) + ImpliesExpression + { EquivOp (. x = t; .) + ImpliesExpression + (. e0 = Expr.Binary(x, BinaryOperator.Opcode.Iff, e0, e1); .) + } + . + +EquivOp = "<==>" | '\u21d4'. + +/*------------------------------------------------------------------------*/ +ImpliesExpression += (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; .) + LogicalExpression + [ + ImpliesOp (. x = t; .) + /* recurse because implication is right-associative */ + ImpliesExpression + (. 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 + (. e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e1, e0); .) + /* loop because explies is left-associative */ + { + ExpliesOp (. x = t; .) + LogicalExpression + (. e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e1, e0); .) + } + ] + . + +ImpliesOp = "==>" | '\u21d2'. +ExpliesOp = "<==" | '\u21d0'. + +/*------------------------------------------------------------------------*/ +LogicalExpression += (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; .) + RelationalExpression + [ AndOp (. x = t; .) + RelationalExpression + (. e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1); .) + { AndOp (. x = t; .) + RelationalExpression + (. e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1); .) + } + | OrOp (. x = t; .) + RelationalExpression + (. e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1); .) + { OrOp (. x = t; .) + RelationalExpression + (. e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1); .) + } + ] + . + +AndOp = "&&" | '\u2227'. +OrOp = "||" | '\u2228'. + +/*------------------------------------------------------------------------*/ +RelationalExpression += (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; BinaryOperator.Opcode op; .) + BvTerm + [ RelOp + BvTerm (. e0 = Expr.Binary(x, op, e0, e1); .) + ] + . + +RelOp += (.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 += (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; .) + Term + { "++" (. x = t; .) + Term (. e0 = new BvConcatExpr(x, e0, e1); .) + } + . + + +/*------------------------------------------------------------------------*/ +Term += (.Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; BinaryOperator.Opcode op; .) + Factor + { AddOp + Factor (. e0 = Expr.Binary(x, op, e0, e1); .) + } + . + +AddOp += (.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 += (.Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; BinaryOperator.Opcode op; .) + Power + { MulOp + Power (. e0 = Expr.Binary(x, op, e0, e1); .) + } + . + +MulOp += (. 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 += (.Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; .) + UnaryExpression + [ + "**" (. x = t; .) + /* recurse because exponentation is right-associative */ + Power (. e0 = Expr.Binary(x, BinaryOperator.Opcode.Pow, e0, e1); .) + ] + . + +/*------------------------------------------------------------------------*/ +UnaryExpression += (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; + e = dummyExpr; + .) + ( "-" (. x = t; .) + UnaryExpression (. e = Expr.Unary(x, UnaryOperator.Opcode.Neg, e); .) + | NegOp (. x = t; .) + UnaryExpression (. e = Expr.Unary(x, UnaryOperator.Opcode.Not, e); .) + | CoercionExpression + ) + . + +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 += (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; + Bpl.Type/*!*/ coercedTo; + BigNum bn; + .) + ArrayExpression + { ":" (. x = t; .) + ( + Type (. e = Expr.CoerceType(x, e, coercedTo); .) + | + Nat /* 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 += (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; + Expr/*!*/ index0 = dummyExpr; Expr/*!*/ e1; + bool store; bool bvExtract; + List/*!*/ allArgs = dummyExprSeq; + .) + AtomExpression + { "[" (. x = t; allArgs = new List (); + allArgs.Add(e); + store = false; bvExtract = false; .) + [ + Expression + (. if (index0 is BvBounds) + bvExtract = true; + else + allArgs.Add(index0); + .) + { "," Expression + (. if (bvExtract || e1 is BvBounds) + this.SemErr("bitvectors only have one dimension"); + allArgs.Add(e1); + .) + } + [ ":=" Expression + (. if (bvExtract || e1 is BvBounds) + this.SemErr("assignment to bitvectors is not possible"); + allArgs.Add(e1); store = true; + .) + ] + | ":=" Expression (. 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 += (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; int n; BigNum bn; BigDec bd; + List/*!*/ es; List/*!*/ ds; Trigger trig; + List/*!*/ typeParams; + IdentifierExpr/*!*/ id; + QKeyValue kv; + e = dummyExpr; + List/*!*/ locals; + List/*!*/ blocks; + .) + ( "false" (. e = new LiteralExpr(t, false); .) + | "true" (. e = new LiteralExpr(t, true); .) + | Nat (. e = new LiteralExpr(t, bn); .) + | Dec (. e = new LiteralExpr(t, bd); .) + | BvLit (. e = new LiteralExpr(t, bn, n); .) + + | Ident (. id = new IdentifierExpr(x, x.val); e = id; .) + [ "(" + ( Expressions (. e = new NAryExpr(x, new FunctionCall(id), es); .) + | /* empty */ (. e = new NAryExpr(x, new FunctionCall(id), new List()); .) + ) + ")" + ] + + | "old" (. x = t; .) + "(" + Expression + ")" (. e = new OldExpr(x, e); .) + + | "int" (. x = t; .) + "(" + Expression + ")" (. e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToInt), new List{ e }); .) + + | "real" (. x = t; .) + "(" + Expression + ")" (. e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToReal), new List{ e }); .) + + | "(" ( Expression (. if (e is BvBounds) + this.SemErr("parentheses around bitvector bounds " + + "are not allowed"); .) + | Forall (. x = t; .) + QuantifierBody + (. if (typeParams.Count + ds.Count > 0) + e = new ForallExpr(x, typeParams, ds, kv, trig, e); .) + | Exists (. x = t; .) + QuantifierBody + (. if (typeParams.Count + ds.Count > 0) + e = new ExistsExpr(x, typeParams, ds, kv, trig, e); .) + | Lambda (. x = t; .) + QuantifierBody + (. 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 + | CodeExpression (. e = new CodeExpr(locals, blocks); .) + ) + . + +CodeExpression<.out List/*!*/ locals, out List/*!*/ blocks.> += (. Contract.Ensures(Contract.ValueAtReturn(out locals) != null); Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out blocks))); locals = new List(); Block/*!*/ b; + blocks = new List(); + .) + "|{" + { LocalVars } + SpecBlock (. blocks.Add(b); .) + { SpecBlock (. blocks.Add(b); .) + } + "}|" + . + +SpecBlock += (. Contract.Ensures(Contract.ValueAtReturn(out b) != null); IToken/*!*/ x; IToken/*!*/ y; + Cmd c; IToken label; + List cs = new List(); + List/*!*/ xs; + List ss = new List(); + b = dummyBlock; + Expr/*!*/ e; + .) + Ident ":" + { LabelOrCmd + (. 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 (. 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 + (. b = new Block(x,x.val,cs,new ReturnExprCmd(t,e)); .) + ) + ";" + . + +Attribute += (. Trigger trig = null; .) + AttributeOrTrigger (. if (trig != null) this.SemErr("only attributes, not triggers, allowed here"); .) +. + +AttributeOrTrigger += (. IToken/*!*/ tok; Expr/*!*/ e; List/*!*/ es; + string key; + List parameters; object/*!*/ param; + .) + "{" (. tok = t; .) + ( + ":" ident (. key = t.val; parameters = new List(); .) + [ AttributeParameter (. parameters.Add(param); .) + { "," AttributeParameter (. 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 { e }, null); + } else { + trig.AddLast(new Trigger(tok, false, new List { 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 (. es = new List { e }; .) + { "," Expression (. es.Add(e); .) + } (. if (trig==null) { + trig = new Trigger(tok, true, es, null); + } else { + trig.AddLast(new Trigger(tok, true, es, null)); + } + .) + ) + "}" + . + +AttributeParameter += (. Contract.Ensures(Contract.ValueAtReturn(out o) != null); + o = "error"; + Expr/*!*/ e; + .) + ( string (. o = t.val.Substring(1, t.val.Length-2); .) + | Expression (. o = e; .) + ) + . + +IfThenElseExpression += (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); + IToken/*!*/ tok; + Expr/*!*/ e0, e1, e2; + e = dummyExpr; .) + "if" (. tok = t; .) Expression "then" Expression "else" Expression + (. e = new NAryExpr(tok, new IfThenElse(tok), new List{ e0, e1, e2 }); .) + . + + +QuantifierBody<.IToken/*!*/ q, out List/*!*/ typeParams, out List/*!*/ 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 (); + IToken/*!*/ tok; + kv = null; + ds = new List (); + .) + ( + TypeParams + [ BoundVars ] + | + BoundVars + ) + QSep + { AttributeOrTrigger } + Expression + . + +Forall = "forall" | '\u2200'. +Exists = "exists" | '\u2203'. +Lambda = "lambda" | '\u03bb'. +QSep = "::" | '\u2022'. + +/*------------------------------------------------------------------------*/ +Ident +=(.Contract.Ensures(Contract.ValueAtReturn(out x) != null);.) + ident (. x = t; + if (x.val.StartsWith("\\")) + x.val = x.val.Substring(1); + .) + . + +/*------------------------------------------------------------------------*/ +Nat += + digits + (. try { + n = BigNum.FromString(t.val); + } catch (FormatException) { + this.SemErr("incorrectly formatted number"); + n = BigNum.ZERO; + } + .) + . + +/*------------------------------------------------------------------------*/ +Dec += (. 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 += + 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. -- cgit v1.2.3 From f3f704edfb2cd1021d811050c72694767710217f Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Tue, 19 Jul 2016 11:14:41 -0600 Subject: Added and briefly tested the updated syntax. NaN/oo not supported yet --- Source/AbsInt/IntervalDomain.cs | 6 +- Source/Basetypes/BigFloat.cs | 982 +++++++++++++++++++++------------------- Source/Core/AbsyExpr.cs | 12 +- Source/Core/AbsyType.cs | 8 +- Source/Core/BoogiePL.atg | 25 +- Source/Core/Parser.cs | 889 ++++++++++++++++++------------------ Source/Core/Scanner.cs | 385 ++++++++-------- Test/floats/float0.bpl | 8 +- Test/floats/float1.bpl | 24 +- 9 files changed, 1213 insertions(+), 1126 deletions(-) (limited to 'Source/Core/BoogiePL.atg') diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs index 9d37476f..1d35b735 100644 --- a/Source/AbsInt/IntervalDomain.cs +++ b/Source/AbsInt/IntervalDomain.cs @@ -695,10 +695,10 @@ namespace Microsoft.Boogie.AbstractInterpretation Lo = floor; Hi = ceiling; } else if (node.Val is BigFloat) { - BigNum floor, ceiling; + BigInteger floor, ceiling; ((BigFloat)node.Val).FloorCeiling(out floor, out ceiling); - Lo = floor.ToBigInteger; - Hi = ceiling.ToBigInteger; + Lo = floor; + Hi = ceiling; } else if (node.Val is bool) { if ((bool)node.Val) { // true diff --git a/Source/Basetypes/BigFloat.cs b/Source/Basetypes/BigFloat.cs index 3c4cc40a..5f711e70 100644 --- a/Source/Basetypes/BigFloat.cs +++ b/Source/Basetypes/BigFloat.cs @@ -1,475 +1,507 @@ -//----------------------------------------------------------------------------- -// -// Copyright (C) Microsoft Corporation. All Rights Reserved. -// -//----------------------------------------------------------------------------- - -using System; -using System.Collections.Generic; -using System.Linq; -using System.Text; -using System.Diagnostics.Contracts; -using System.Diagnostics; - -namespace Microsoft.Basetypes -{ - using BIM = System.Numerics.BigInteger; - - /// - /// A representation of a 32-bit floating point value - /// Note that this value has a 1-bit sign, 8-bit exponent, and 24-bit significand - /// - public struct BigFloat - { - //Please note that this code outline is copy-pasted from BigDec.cs - - // the internal representation - [Rep] - internal readonly BigNum significand; //Note that the significand arrangement matches standard fp arrangement (most significant bit is farthest left) - [Rep] - internal readonly int significandSize; - [Rep] - internal readonly BigNum exponent; //The value of the exponent is always positive as per fp representation requirements - [Rep] - internal readonly int exponentSize; //The bit size of the exponent - [Rep] - internal readonly String value; //Only used with second syntax - [Rep] - internal readonly bool isNeg; - - public BigNum Significand { - get { - return significand; - } - } - - public BigNum Exponent { - get { - return exponent; - } - } - - public int SignificandSize { - get { - return significandSize; - } - } - - public int ExponentSize { - get { - return exponentSize; - } - } - - public bool IsNegative { - get { - return this.isNeg; - } - } - - public String Value { - get { - return value; - } - } - - public static BigFloat ZERO(int exponentSize, int significandSize) { return new BigFloat(false, BigNum.ZERO, BigNum.ZERO, exponentSize, significandSize); } //Does not include negative zero - - private static readonly BigNum two = new BigNum(2); - private static readonly BigNum one = new BigNum(1); - private static BigNum two_n(int n) { - BigNum toReturn = one; - for (int i = 0; i < n; i++) - toReturn = toReturn * two; - return toReturn; - } - - - //////////////////////////////////////////////////////////////////////////// - // Constructors - - //Please note that these constructors will be called throughout boogie - //For a complete summary of where this class has been added, simply view constructor references - - [Pure] - public static BigFloat FromInt(int v) { - return new BigFloat(v.ToString(), 8, 24); - } - - public static BigFloat FromInt(int v, int exponentSize, int significandSize) - { - return new BigFloat(v.ToString(), exponentSize, significandSize); - } - - public static BigFloat FromBigInt(BIM v) { - return new BigFloat(v.ToString(), 8, 24); - } - - public static BigFloat FromBigInt(BIM v, int exponentSize, int significandSize) - { - return new BigFloat(v.ToString(), exponentSize, significandSize); - } - - public static BigFloat FromBigDec(BigDec v) - { - return new BigFloat(v.ToDecimalString(), 8, 24); - } - - public static BigFloat FromBigDec(BigDec v, int exponentSize, int significandSize) - { - return new BigFloat(v.ToDecimalString(), exponentSize, significandSize); - } - - [Pure] - public static BigFloat FromString(String v, int exp, int sig) { //String must be - return new BigFloat(v, exp, sig); - } - - public BigFloat(bool sign, BigNum exponent, BigNum significand, int exponentSize, int significandSize) { - this.exponentSize = exponentSize; - this.exponent = exponent; - this.significand = significand; - this.significandSize = significandSize+1; - this.isNeg = sign; - this.value = ""; - } - - public BigFloat(String value, int exponentSize, int significandSize) { - this.exponentSize = exponentSize; - this.significandSize = significandSize; - this.exponent = BigNum.ZERO; - this.significand = BigNum.ZERO; - this.value = value; - this.isNeg = value[0] == '-'; - } - - private BigNum maxsignificand() - { - BigNum result = one; - for (int i = 0; i < significandSize; i++) - result = result * two; - return result - one; - } - private int maxExponent() { return (int)Math.Pow(2, exponentSize) - 1; } - - - - //////////////////////////////////////////////////////////////////////////// - // Basic object operations - - [Pure] - [Reads(ReadsAttribute.Reads.Nothing)] - public override bool Equals(object obj) { - if (obj == null) - return false; - if (!(obj is BigFloat)) - return false; - - return (this == (BigFloat)obj); - } - - [Pure] - public override int GetHashCode() { - return significand.GetHashCode() * 13 + Exponent.GetHashCode(); - } - - [Pure] - public override string/*!*/ ToString() { - Contract.Ensures(Contract.Result() != null); - return value=="" ? String.Format("{0}x2^{1}", significand.ToString(), Exponent.ToString()) : value; - } - - - //////////////////////////////////////////////////////////////////////////// - // Conversion operations - - /// - /// NOTE: THIS METHOD MAY NOT WORK AS EXPECTED!!! - /// Converts the given decimal value (provided as a string) to the nearest floating point approximation - /// the returned fp assumes the given significand and exponent size - /// - /// - /// - /// - /// - public static BigFloat Round(String value, int exponentSize, int significandSize) - { - int i = value.IndexOf('.'); - if (i == -1) - return Round(BigNum.FromString(value), BigNum.ZERO, exponentSize, significandSize); - return Round(i == 0 ? BigNum.ZERO : BigNum.FromString(value.Substring(0, i)), BigNum.FromString(value.Substring(i + 1, value.Length - i - 1)), exponentSize, significandSize); - } - - /// - /// NOTE: THIS METHOD MAY NOT WORK AS EXPECTED!!!! - /// Converts value.dec_value to a the closest float approximation with the given significandSize, exponentSize - /// Returns the result of this calculation - /// - /// - /// - /// - /// - /// - public static BigFloat Round(BigNum value, BigNum dec_value, int exponentSize, int significandSize) - { - int exp = 0; - BigNum one = new BigNum(1); - BigNum ten = new BigNum(10); - BigNum dec_max = new BigNum(0); //represents the order of magnitude of dec_value for carrying during calculations - - //First, determine the exponent - while (value > one) { //Divide by two, increment exponent by 1 - if (!(value % two).IsZero) { //Add "1.0" to the decimal - dec_max = new BigNum(10); - while (dec_max < dec_value) - dec_max = dec_max * ten; - dec_value = dec_value + dec_max; - } - value = value / two; - if (!(dec_value % ten).IsZero) - dec_value = dec_value * ten; //Creates excess zeroes to avoid losing data during division - dec_value = dec_value / two; - exp++; - } - if (value.IsZero && !dec_value.IsZero) { - dec_max = new BigNum(10); - while (dec_max < dec_value) - dec_max = dec_max * ten; - while (value.IsZero) {//Multiply by two, decrement exponent by 1 - dec_value = dec_value * two; - if (dec_value >= dec_max) { - dec_value = dec_value - dec_max; - value = value + one; - } - exp--; - } - } - - //Second, calculate the significand - value = new BigNum(0); //remove implicit bit - dec_max = new BigNum(10); - while (dec_max < dec_value) - dec_max = dec_max * ten; - for (int i = significandSize; i > 0 && !dec_value.IsZero; i--) { //Multiply by two until the significand is fully calculated - dec_value = dec_value * two; - if (dec_value >= dec_max) { - dec_value = dec_value - dec_max; - value = value + two_n(i); //Note that i is decrementing so that the most significant bit is left-most in the representation - } - } - - return new BigFloat(false, BigNum.ZERO, BigNum.FromString(value.ToString()), exponentSize, significandSize); //Sign not actually checked... - } - - // ``floor`` rounds towards negative infinity (like SMT-LIBv2's to_int). - /// - /// NOTE: THIS PROBABLY WON'T GIVE USEFUL OUTPUT!!! - /// Computes the floor and ceiling of this BigFloat. Note the choice of rounding towards negative - /// infinity rather than zero for floor is because SMT-LIBv2's to_int function floors this way. - /// - /// The Floor (rounded towards negative infinity) - /// Ceiling (rounded towards positive infinity) - public void FloorCeiling(out BigNum floor, out BigNum ceiling) { - //TODO: fix for fp functionality - BigNum n = Significand; - BigNum e = Exponent; - if (n.IsZero) { - floor = ceiling = n; - } else if (BigNum.ZERO <= e) { - // it's an integer - for (; BigNum.ZERO < e; e = e - one) - { - n = n * two; - } - floor = ceiling = n; - } else { - // it's a non-zero integer, so the ceiling is one more than the floor - for (; BigNum.ZERO < e && !n.IsZero; e = e + one) - { - n = n / two; // Division rounds towards negative infinity - } - - if (!IsNegative) { - floor = n; - ceiling = n + one; - } else { - ceiling = n; - floor = n - one; - } - } - Debug.Assert(floor <= ceiling, "Invariant was not maintained"); - } - - [Pure] - public String ToDecimalString(int maxDigits) { - //TODO: fix for fp functionality - { - throw new NotImplementedException(); - } - } - - public String ToBVString(){ - if (this.IsSpecialType) { - return "_ " + this.value + " " + this.exponentSize + " " + this.significandSize; - } - else if (this.Value == "") { - return "fp (_ bv" + (this.isNeg ? "1" : "0") + " 1) (_ bv" + this.exponent + " " + this.exponentSize + ") (_ bv" + this.significand + " " + (this.significandSize-1) + ")"; - } - else { - return "(_ to_fp " + this.exponentSize + " " + this.significandSize + ") (_ bv" + this.value + " " + (this.exponentSize + this.significandSize).ToString() + ")"; - } - } - - [Pure] - public string ToDecimalString() { - Contract.Ensures(Contract.Result() != null); - return value=="" ? String.Format("{0}x2^{1}", significand.ToString(), Exponent.ToString()) : value; - } - - [Pure] - public static string Zeros(int n) { - //TODO: fix for fp functionality - Contract.Requires(0 <= n); - if (n <= 10) { - var tenZeros = "0000000000"; - return tenZeros.Substring(0, n); - } else { - var d = n / 2; - var s = Zeros(d); - if (n % 2 == 0) { - return s + s; - } else { - return s + s + "0"; - } - } - } - - - //////////////////////////////////////////////////////////////////////////// - // Basic arithmetic operations - - [Pure] - public BigFloat Abs { - get { - return new BigFloat(true, Exponent, Significand, ExponentSize, SignificandSize); - } - } - - [Pure] - public BigFloat Negate { - get { - if (value != "") - return value[0] == '-' ? new BigFloat(value.Remove(0, 1), ExponentSize, significandSize) : new BigFloat("-" + value, ExponentSize, significandSize); - return new BigFloat(!isNeg, Exponent, Significand, ExponentSize, SignificandSize); - } - } - - [Pure] - public static BigFloat operator -(BigFloat x) { - return x.Negate; - } - - [Pure] - public static BigFloat operator +(BigFloat x, BigFloat y) { - //TODO: Modify for correct fp functionality - Contract.Requires(x.ExponentSize == y.ExponentSize); - Contract.Requires(x.significandSize == y.significandSize); - BigNum m1 = x.significand; - BigNum e1 = x.Exponent; - BigNum m2 = y.significand; - BigNum e2 = y.Exponent; - m1 = m1 + two_n(x.significandSize + 1); //Add implicit bit - m2 = m2 + two_n(y.significandSize + 1); - if (e2 > e1) { - m1 = y.significand; - e1 = y.Exponent; - m2 = x.significand; - e2 = x.Exponent; - } - - while (e2 < e1) { - m2 = m2 / two; - e2 = e2 + one; - } - - return new BigFloat(false, e1, m1 + m2, x.significandSize, x.ExponentSize); - } - - [Pure] - public static BigFloat operator -(BigFloat x, BigFloat y) { - return x + y.Negate; - } - - [Pure] - public static BigFloat operator *(BigFloat x, BigFloat y) { - Contract.Requires(x.ExponentSize == y.ExponentSize); - Contract.Requires(x.significandSize == y.significandSize); - return new BigFloat(x.isNeg ^ y.isNeg, x.Exponent + y.Exponent, x.significand * y.significand, x.significandSize, x.ExponentSize); - } - - - //////////////////////////////////////////////////////////////////////////// - // Some basic comparison operations - - public bool IsSpecialType { - get { - if (value == "") - return false; - return (value.Equals("NaN") || value.Equals("+oo") || value.Equals("-oo") || value.Equals("zero") || value.Equals("-zero")); - } - } - - public bool IsPositive { - get { - return !IsNegative; - } - } - - public bool IsZero { - get { - return significand.Equals(BigNum.ZERO) && Exponent == BigNum.ZERO; - } - } - - [Pure] - public int CompareTo(BigFloat that) { - if (this.exponent > that.exponent) - return 1; - if (this.exponent < that.exponent) - return -1; - if (this.significand == that.significand) - return 0; - return this.significand > that.significand ? 1 : -1; - } - - [Pure] - public static bool operator ==(BigFloat x, BigFloat y) { - return x.CompareTo(y) == 0; - } - - [Pure] - public static bool operator !=(BigFloat x, BigFloat y) { - return x.CompareTo(y) != 0; - } - - [Pure] - public static bool operator <(BigFloat x, BigFloat y) { - return x.CompareTo(y) < 0; - } - - [Pure] - public static bool operator >(BigFloat x, BigFloat y) { - return x.CompareTo(y) > 0; - } - - [Pure] - public static bool operator <=(BigFloat x, BigFloat y) { - return x.CompareTo(y) <= 0; - } - - [Pure] - public static bool operator >=(BigFloat x, BigFloat y) { - return x.CompareTo(y) >= 0; - } - } -} +//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- + +using System; +using System.Collections.Generic; +using System.Linq; +using System.Text; +using System.Diagnostics.Contracts; +using System.Diagnostics; + +namespace Microsoft.Basetypes +{ + using BIM = System.Numerics.BigInteger; + + /// + /// A representation of a 32-bit floating point value + /// Note that this value has a 1-bit sign, 8-bit exponent, and 24-bit significand + /// + public struct BigFloat + { + //Please note that this code outline is copy-pasted from BigDec.cs + + // the internal representation + [Rep] + internal readonly BIM significand; //Note that the significand arrangement matches standard fp arrangement (most significant bit is farthest left) + [Rep] + internal readonly int significandSize; + [Rep] + internal readonly BIM exponent; //The value of the exponent is always positive as per fp representation requirements + [Rep] + internal readonly int exponentSize; //The bit size of the exponent + [Rep] + internal readonly String value; //Only used with second syntax + [Rep] + internal readonly bool isNeg; + + public BIM Significand { + get { + return significand; + } + } + + public BIM Exponent { + get { + return exponent; + } + } + + public int SignificandSize { + get { + return significandSize; + } + } + + public int ExponentSize { + get { + return exponentSize; + } + } + + public bool IsNegative { + get { + return this.isNeg; + } + } + + public String Value { + get { + return value; + } + } + + public static BigFloat ZERO = new BigFloat(false, BIM.Zero, BIM.Zero, 24, 8); //Does not include negative zero + + private static readonly BIM two = new BIM(2); + private static readonly BIM one = new BIM(1); + private static BIM two_n(int n) { + BIM toReturn = one; + for (int i = 0; i < n; i++) + toReturn = toReturn * two; + return toReturn; + } + + + //////////////////////////////////////////////////////////////////////////// + // Constructors + + //Please note that these constructors will be called throughout boogie + //For a complete summary of where this class has been added, simply view constructor references + + [Pure] + public static BigFloat FromInt(int v) { + return new BigFloat(v.ToString(), 24, 8); + } + + public static BigFloat FromInt(int v, int significandSize, int exponentSize) + { + return new BigFloat(v.ToString(), significandSize, exponentSize); + } + + public static BigFloat FromBigInt(BIM v) { + return new BigFloat(v.ToString(), 24, 8); + } + + public static BigFloat FromBigInt(BIM v, int significandSize, int exponentSize) + { + return new BigFloat(v.ToString(), significandSize, exponentSize); + } + + public static BigFloat FromBigDec(BigDec v) + { + return new BigFloat(v.ToDecimalString(), 24, 8); + } + + public static BigFloat FromBigDec(BigDec v, int significandSize, int exponentSize) + { + return new BigFloat(v.ToDecimalString(), significandSize, exponentSize); + } + + [Pure] + public static BigFloat FromString(String s) { + /* + * String must be either of the format *e*f*e* + * or of the special value formats: 0NaN*e* 0nan*e* 0+oo*e* 0-oo*e* + * Where * indicates an integer value (digit) + */ + BIM sig, exp; + int sigSize, expSize; + bool isNeg; + + if (s.IndexOf('f') == -1) { + String val = s; + sigSize = int.Parse(s.Substring(4, s.IndexOf('e')-4)); + expSize = int.Parse(s.Substring(s.IndexOf('e') + 1)); + if (sigSize <= 0 || expSize <= 0) + throw new FormatException("Significand and Exponent sizes must be greater than 0"); + return new BigFloat(val, sigSize, expSize); + } + + sig = BIM.Parse(s.Substring(0, s.IndexOf('e'))); + exp = BIM.Parse(s.Substring(s.IndexOf('e') + 1, s.IndexOf('f') - s.IndexOf('e') - 1)); + sigSize = int.Parse(s.Substring(s.IndexOf('f') + 1, s.IndexOf('e', s.IndexOf('e') + 1) - s.IndexOf('f') - 1)); + expSize = int.Parse(s.Substring(s.IndexOf('e', s.IndexOf('e') + 1) + 1)); + + if (sigSize <= 0 || expSize <= 0) + throw new FormatException("Significand and Exponent sizes must be greater than 0"); + + sigSize = sigSize - 1; //Get rid of sign bit + isNeg = sig < 0; + sig = BIM.Abs(sig); + exp = exp + BIM.Pow(new BIM(2), expSize-1) - BIM.One; + + if (exp < 0 || exp >= BIM.Pow(new BIM(2), expSize)) + throw new FormatException("The given exponent " + exp + " cannot fit in the bit size " + expSize); + + if (sig >= BIM.Pow(new BIM(2), sigSize)) + throw new FormatException("The given significand " + sig + " cannot fit in the bit size " + (sigSize+1)); + + return new BigFloat(isNeg, sig, exp, sigSize, expSize); + } + + public BigFloat(bool isNeg, BIM significand, BIM exponent, int significandSize, int exponentSize) { + this.exponentSize = exponentSize; + this.exponent = exponent; + this.significand = significand; + this.significandSize = significandSize+1; + this.isNeg = isNeg; + this.value = ""; + } + + public BigFloat(String value, int significandSize, int exponentSize) { + this.exponentSize = exponentSize; + this.significandSize = significandSize; + this.exponent = BIM.Zero; + this.significand = BIM.Zero; + this.value = value; + if (value.Equals("nan")) + this.value = "NaN"; + this.isNeg = value[0] == '-'; + } + + private BIM maxsignificand() + { + BIM result = one; + for (int i = 0; i < significandSize; i++) + result = result * two; + return result - one; + } + private int maxExponent() { return (int)Math.Pow(2, exponentSize) - 1; } + + + + //////////////////////////////////////////////////////////////////////////// + // Basic object operations + + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public override bool Equals(object obj) { + if (obj == null) + return false; + if (!(obj is BigFloat)) + return false; + + return (this == (BigFloat)obj); + } + + [Pure] + public override int GetHashCode() { + return significand.GetHashCode() * 13 + Exponent.GetHashCode(); + } + + [Pure] + public override string/*!*/ ToString() { + Contract.Ensures(Contract.Result() != null); + return value=="" ? String.Format("{0}x2^{1}", significand.ToString(), Exponent.ToString()) : value; + } + + + //////////////////////////////////////////////////////////////////////////// + // Conversion operations + + /// + /// NOTE: THIS METHOD MAY NOT WORK AS EXPECTED!!! + /// Converts the given decimal value (provided as a string) to the nearest floating point approximation + /// the returned fp assumes the given significand and exponent size + /// + /// + /// + /// + /// + public static BigFloat Round(String value, int exponentSize, int significandSize) + { + int i = value.IndexOf('.'); + if (i == -1) + return Round(BIM.Parse(value), BIM.Zero, exponentSize, significandSize); + return Round(i == 0 ? BIM.Zero : BIM.Parse(value.Substring(0, i)), BIM.Parse(value.Substring(i + 1, value.Length - i - 1)), exponentSize, significandSize); + } + + /// + /// NOTE: THIS METHOD MAY NOT WORK AS EXPECTED!!!! + /// Converts value.dec_value to a the closest float approximation with the given significandSize, exponentSize + /// Returns the result of this calculation + /// + /// + /// + /// + /// + /// + public static BigFloat Round(BIM value, BIM dec_value, int exponentSize, int significandSize) + { + int exp = 0; + BIM one = new BIM(1); + BIM ten = new BIM(10); + BIM dec_max = new BIM(0); //represents the order of magnitude of dec_value for carrying during calculations + + //First, determine the exponent + while (value > one) { //Divide by two, increment exponent by 1 + if (!(value % two).IsZero) { //Add "1.0" to the decimal + dec_max = new BIM(10); + while (dec_max < dec_value) + dec_max = dec_max * ten; + dec_value = dec_value + dec_max; + } + value = value / two; + if (!(dec_value % ten).IsZero) + dec_value = dec_value * ten; //Creates excess zeroes to avoid losing data during division + dec_value = dec_value / two; + exp++; + } + if (value.IsZero && !dec_value.IsZero) { + dec_max = new BIM(10); + while (dec_max < dec_value) + dec_max = dec_max * ten; + while (value.IsZero) {//Multiply by two, decrement exponent by 1 + dec_value = dec_value * two; + if (dec_value >= dec_max) { + dec_value = dec_value - dec_max; + value = value + one; + } + exp--; + } + } + + //Second, calculate the significand + value = new BIM(0); //remove implicit bit + dec_max = new BIM(10); + while (dec_max < dec_value) + dec_max = dec_max * ten; + for (int i = significandSize; i > 0 && !dec_value.IsZero; i--) { //Multiply by two until the significand is fully calculated + dec_value = dec_value * two; + if (dec_value >= dec_max) { + dec_value = dec_value - dec_max; + value = value + two_n(i); //Note that i is decrementing so that the most significant bit is left-most in the representation + } + } + + return new BigFloat(false, BIM.Zero, BIM.Parse(value.ToString()), exponentSize, significandSize); //Sign not actually checked... + } + + // ``floor`` rounds towards negative infinity (like SMT-LIBv2's to_int). + /// + /// NOTE: This may give wrong results, it hasn't been tested extensively + /// If you're getting weird bugs, you may want to check this function out... + /// Computes the floor and ceiling of this BigFloat. Note the choice of rounding towards negative + /// infinity rather than zero for floor is because SMT-LIBv2's to_int function floors this way. + /// + /// The Floor (rounded towards negative infinity) + /// Ceiling (rounded towards positive infinity) + public void FloorCeiling(out BIM floor, out BIM ceiling) + { + BIM two = new BIM(2); + + BIM sig = Significand + BIM.Pow(two, SignificandSize); //Add hidden bit + BIM exp = Exponent - BIM.Pow(two, ExponentSize); + sig = sig >> ExponentSize; + + while (exp > BIM.Zero) { + exp--; + sig = sig >> 1; + } + + if (isNeg) { + ceiling = -sig + 1; + floor = -sig; + } + else { + ceiling = sig + 1; + floor = sig; + } + } + + [Pure] + public String ToDecimalString(int maxDigits) { + //TODO: fix for fp functionality + { + throw new NotImplementedException(); + } + } + + public String ToBVString(){ + if (this.IsSpecialType) { + return "_ " + this.value + " " + this.exponentSize + " " + this.significandSize; + } + else if (this.Value == "") { + return "fp (_ bv" + (this.isNeg ? "1" : "0") + " 1) (_ bv" + this.exponent + " " + this.exponentSize + ") (_ bv" + this.significand + " " + (this.significandSize-1) + ")"; + } + else { + return "(_ to_fp " + this.exponentSize + " " + this.significandSize + ") (_ bv" + this.value + " " + (this.exponentSize + this.significandSize).ToString() + ")"; + } + } + + [Pure] + public string ToDecimalString() { + Contract.Ensures(Contract.Result() != null); + return value=="" ? String.Format("{0}x2^{1}", significand.ToString(), Exponent.ToString()) : value; + } + + [Pure] + public static string Zeros(int n) { + //TODO: fix for fp functionality + Contract.Requires(0 <= n); + if (n <= 10) { + var tenZeros = "0000000000"; + return tenZeros.Substring(0, n); + } else { + var d = n / 2; + var s = Zeros(d); + if (n % 2 == 0) { + return s + s; + } else { + return s + s + "0"; + } + } + } + + + //////////////////////////////////////////////////////////////////////////// + // Basic arithmetic operations + + [Pure] + public BigFloat Abs { + get { + return new BigFloat(true, Exponent, Significand, ExponentSize, SignificandSize); + } + } + + [Pure] + public BigFloat Negate { + get { + if (value != "") + return value[0] == '-' ? new BigFloat(value.Remove(0, 1), ExponentSize, significandSize) : new BigFloat("-" + value, ExponentSize, significandSize); + return new BigFloat(!isNeg, Exponent, Significand, ExponentSize, SignificandSize); + } + } + + [Pure] + public static BigFloat operator -(BigFloat x) { + return x.Negate; + } + + [Pure] + public static BigFloat operator +(BigFloat x, BigFloat y) { + //TODO: Modify for correct fp functionality + Contract.Requires(x.ExponentSize == y.ExponentSize); + Contract.Requires(x.significandSize == y.significandSize); + BIM m1 = x.significand; + BIM e1 = x.Exponent; + BIM m2 = y.significand; + BIM e2 = y.Exponent; + m1 = m1 + two_n(x.significandSize + 1); //Add implicit bit + m2 = m2 + two_n(y.significandSize + 1); + if (e2 > e1) { + m1 = y.significand; + e1 = y.Exponent; + m2 = x.significand; + e2 = x.Exponent; + } + + while (e2 < e1) { + m2 = m2 / two; + e2 = e2 + one; + } + + return new BigFloat(false, e1, m1 + m2, x.significandSize, x.ExponentSize); + } + + [Pure] + public static BigFloat operator -(BigFloat x, BigFloat y) { + return x + y.Negate; + } + + [Pure] + public static BigFloat operator *(BigFloat x, BigFloat y) { + Contract.Requires(x.ExponentSize == y.ExponentSize); + Contract.Requires(x.significandSize == y.significandSize); + return new BigFloat(x.isNeg ^ y.isNeg, x.Exponent + y.Exponent, x.significand * y.significand, x.significandSize, x.ExponentSize); + } + + + //////////////////////////////////////////////////////////////////////////// + // Some basic comparison operations + + public bool IsSpecialType { + get { + if (value == "") + return false; + return (value.Equals("NaN") || value.Equals("+oo") || value.Equals("-oo") || value.Equals("zero") || value.Equals("-zero")); + } + } + + public bool IsPositive { + get { + return !IsNegative; + } + } + + public bool IsZero { + get { + return significand.Equals(BigNum.ZERO) && Exponent == BIM.Zero; + } + } + + [Pure] + public int CompareTo(BigFloat that) { + if (this.exponent > that.exponent) + return 1; + if (this.exponent < that.exponent) + return -1; + if (this.significand == that.significand) + return 0; + return this.significand > that.significand ? 1 : -1; + } + + [Pure] + public static bool operator ==(BigFloat x, BigFloat y) { + return x.CompareTo(y) == 0; + } + + [Pure] + public static bool operator !=(BigFloat x, BigFloat y) { + return x.CompareTo(y) != 0; + } + + [Pure] + public static bool operator <(BigFloat x, BigFloat y) { + return x.CompareTo(y) < 0; + } + + [Pure] + public static bool operator >(BigFloat x, BigFloat y) { + return x.CompareTo(y) > 0; + } + + [Pure] + public static bool operator <=(BigFloat x, BigFloat y) { + return x.CompareTo(y) <= 0; + } + + [Pure] + public static bool operator >=(BigFloat x, BigFloat y) { + return x.CompareTo(y) >= 0; + } + } +} diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index bc2b4391..409254d0 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -584,7 +584,7 @@ namespace Microsoft.Boogie { { Contract.Requires(tok != null); Val = v; - Type = Type.GetFloatType(v.ExponentSize, v.SignificandSize); + Type = Type.GetFloatType(v.SignificandSize, v.ExponentSize); if (immutable) CachedHashCode = ComputeHashCode(); } @@ -662,7 +662,7 @@ namespace Microsoft.Boogie { return Type.Real; } else if (Val is BigFloat) { BigFloat temp = (BigFloat)Val; - return Type.GetFloatType(temp.ExponentSize, temp.SignificandSize); + return Type.GetFloatType(temp.SignificandSize, temp.ExponentSize); } else if (Val is BvConst) { return Type.GetBvType(((BvConst)Val).Bits); } else { @@ -1724,10 +1724,10 @@ namespace Microsoft.Boogie { return Type.Real; } if (arg0type.IsFloat && arg0type.Unify(arg1type)) { - return Type.GetFloatType(arg0.Type.FloatExponent, arg0.Type.FloatSignificand); + return Type.GetFloatType(arg0.Type.FloatSignificand, arg0.Type.FloatExponent); } if (arg1type.IsFloat && arg1type.Unify(arg0type)) { - return Type.GetFloatType(arg1.Type.FloatExponent, arg1.Type.FloatSignificand); + return Type.GetFloatType(arg1.Type.FloatSignificand, arg1.Type.FloatExponent); } goto BAD_TYPE; case Opcode.Div: @@ -1742,10 +1742,10 @@ namespace Microsoft.Boogie { return Type.Real; } if (arg0type.IsFloat && arg0type.Unify(arg1type)) { - return Type.GetFloatType(arg0.Type.FloatExponent, arg0.Type.FloatSignificand); + return Type.GetFloatType(arg0.Type.FloatSignificand, arg0.Type.FloatExponent); } if (arg1type.IsFloat && arg1type.Unify(arg0type)) { - return Type.GetFloatType(arg1.Type.FloatExponent, arg1.Type.FloatSignificand); + return Type.GetFloatType(arg1.Type.FloatSignificand, arg1.Type.FloatExponent); } goto BAD_TYPE; case Opcode.Pow: diff --git a/Source/Core/AbsyType.cs b/Source/Core/AbsyType.cs index 08cf37cc..ab6ef5e9 100644 --- a/Source/Core/AbsyType.cs +++ b/Source/Core/AbsyType.cs @@ -386,12 +386,12 @@ namespace Microsoft.Boogie { } } - static public FloatType GetFloatType(int exp, int man) { + static public FloatType GetFloatType(int sig, int exp) { Contract.Requires(0 <= exp); - Contract.Requires(0 <= man); + Contract.Requires(0 <= sig); Contract.Ensures(Contract.Result() != null); - return new FloatType(exp, man); + return new FloatType(sig, exp); } //------------ Match formal argument types on actual argument types @@ -1094,7 +1094,7 @@ namespace Microsoft.Boogie { public override string ToString() { Contract.Ensures(Contract.Result() != null); - return "float (" + Exponent + " " + Significand + ")"; + return "float" + Significand + "e" + Exponent; } //----------- Equality ---------------------------------- diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index 091ceeb0..31823110 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -144,7 +144,8 @@ TOKENS string = quote { regularStringChar | "\\\"" } quote. decimal = digit {digit} 'e' [ '-' ] digit {digit} . - float = digit {digit} '.' digit {digit} [ 'e' [ '-' ] digit {digit} ] . + dec_float = digit {digit} '.' digit {digit} [ 'e' [ '-' ] digit {digit} ] . + float = digit {digit} 'e' digit {digit} 'f' digit {digit} 'e' digit {digit} . COMMENTS FROM "/*" TO "*/" NESTED COMMENTS FROM "//" TO lf @@ -330,7 +331,7 @@ TypeAtom ( "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 */ + /* note: bitvectors and floats are handled in UnresolvedTypeIdentifier */ | "(" Type @@ -1252,7 +1253,7 @@ ArrayExpression /*------------------------------------------------------------------------*/ AtomExpression -= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; int n; BigNum bn; BigDec bd; += (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; int n; BigNum bn; BigDec bd; BigFloat bf; List/*!*/ es; List/*!*/ ds; Trigger trig; List/*!*/ typeParams; IdentifierExpr/*!*/ id; @@ -1265,6 +1266,7 @@ AtomExpression | "true" (. e = new LiteralExpr(t, true); .) | Nat (. e = new LiteralExpr(t, bn); .) | Dec (. e = new LiteralExpr(t, bd); .) + | Float (. e = new LiteralExpr(t, bf); .) | BvLit (. e = new LiteralExpr(t, bn, n); .) | Ident (. id = new IdentifierExpr(x, x.val); e = id; .) @@ -1479,7 +1481,7 @@ Dec ( decimal (. s = t.val; .) | - float (. s = t.val; .) + dec_float (. s = t.val; .) ) (. try { n = BigDec.FromString(s); @@ -1508,4 +1510,19 @@ BvLit } .) . + +Float += (. string s = ""; .) + ( + float (. s = t.val; .) + ) + (. try { + n = BigFloat.FromString(s); + } catch (FormatException) { + this.SemErr("incorrectly formatted number"); + n = BigFloat.ZERO; + } + .) + . + END BoogiePL. diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index 78823b61..a5e2921e 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -23,8 +23,9 @@ public class Parser { public const int _digits = 3; public const int _string = 4; public const int _decimal = 5; - public const int _float = 6; - public const int maxT = 96; + public const int _dec_float = 6; + public const int _float = 7; + public const int maxT = 97; const bool T = true; const bool x = false; @@ -117,7 +118,7 @@ private class BvBounds : Expr { public BigNum Lower; public BigNum Upper; public BvBounds(IToken/*!*/ tok, BigNum lower, BigNum upper) - : base(tok, /*immutable*/ false) { + : base(tok, /*immutable=*/ false) { Contract.Requires(tok != null); this.Lower = lower; this.Upper = upper; @@ -132,8 +133,7 @@ private class BvBounds : Expr { Contract.Assert(false);throw new cce.UnreachableException(); } public override void ComputeFreeVariables(GSet/*!*/ freeVars) { Contract.Assert(false);throw new cce.UnreachableException(); } - public override int ComputeHashCode() - { + public override int ComputeHashCode() { return base.GetHashCode(); } } @@ -220,7 +220,7 @@ private class BvBounds : Expr { while (StartOf(1)) { switch (la.kind) { - case 21: { + case 22: { Consts(out vs); foreach(Bpl.Variable/*!*/ v in vs){ Contract.Assert(v != null); @@ -229,7 +229,7 @@ private class BvBounds : Expr { break; } - case 25: { + case 26: { Function(out ds); foreach(Bpl.Declaration/*!*/ d in ds){ Contract.Assert(d != null); @@ -238,12 +238,12 @@ private class BvBounds : Expr { break; } - case 29: { + case 30: { Axiom(out ax); Pgm.AddTopLevelDeclaration(ax); break; } - case 30: { + case 31: { UserDefinedTypes(out ts); foreach(Declaration/*!*/ td in ts){ Contract.Assert(td != null); @@ -252,7 +252,7 @@ private class BvBounds : Expr { break; } - case 7: { + case 8: { GlobalVars(out vs); foreach(Bpl.Variable/*!*/ v in vs){ Contract.Assert(v != null); @@ -261,7 +261,7 @@ private class BvBounds : Expr { break; } - case 32: { + case 33: { Procedure(out pr, out im); Pgm.AddTopLevelDeclaration(pr); if (im != null) { @@ -270,7 +270,7 @@ private class BvBounds : Expr { break; } - case 33: { + case 34: { Implementation(out nnim); Pgm.AddTopLevelDeclaration(nnim); break; @@ -286,17 +286,17 @@ private class BvBounds : Expr { bool u = false; QKeyValue kv = null; bool ChildrenComplete = false; List Parents = null; - Expect(21); + Expect(22); y = t; - while (la.kind == 27) { + while (la.kind == 28) { Attribute(ref kv); } - if (la.kind == 22) { + if (la.kind == 23) { Get(); u = true; } IdsType(out xs); - if (la.kind == 23) { + if (la.kind == 24) { OrderSpec(out ChildrenComplete, out Parents); } bool makeClone = false; @@ -320,7 +320,7 @@ private class BvBounds : Expr { ds.Add(new Constant(y, x, u, ParentsClone, ChildrenComplete, kv)); } - Expect(8); + Expect(9); } void Function(out List/*!*/ ds) { @@ -337,44 +337,44 @@ private class BvBounds : Expr { Expr definition = null; Expr/*!*/ tmp; - Expect(25); - while (la.kind == 27) { + Expect(26); + while (la.kind == 28) { Attribute(ref kv); } Ident(out z); - if (la.kind == 19) { + if (la.kind == 20) { TypeParams(out typeParamTok, out typeParams); } - Expect(9); + Expect(10); if (StartOf(2)) { VarOrType(out tyd, out argKv); arguments.Add(new Formal(tyd.tok, tyd, true, argKv)); - while (la.kind == 12) { + while (la.kind == 13) { Get(); VarOrType(out tyd, out argKv); arguments.Add(new Formal(tyd.tok, tyd, true, argKv)); } } - Expect(10); + Expect(11); argKv = null; - if (la.kind == 26) { + if (la.kind == 27) { Get(); - Expect(9); - VarOrType(out retTyd, out argKv); Expect(10); - } else if (la.kind == 11) { + VarOrType(out retTyd, out argKv); + Expect(11); + } else if (la.kind == 12) { Get(); Type(out retTy); retTyd = new TypedIdent(retTy.tok, TypedIdent.NoName, retTy); - } else SynErr(97); - if (la.kind == 27) { + } else SynErr(98); + if (la.kind == 28) { Get(); Expression(out tmp); definition = tmp; - Expect(28); - } else if (la.kind == 8) { + Expect(29); + } else if (la.kind == 9) { Get(); - } else SynErr(98); + } else SynErr(99); if (retTyd == null) { // construct a dummy type for the case of syntax error retTyd = new TypedIdent(t, TypedIdent.NoName, new BasicType(t, SimpleType.Int)); @@ -429,30 +429,30 @@ private class BvBounds : Expr { void Axiom(out Axiom/*!*/ m) { Contract.Ensures(Contract.ValueAtReturn(out m) != null); Expr/*!*/ e; QKeyValue kv = null; - Expect(29); - while (la.kind == 27) { + Expect(30); + while (la.kind == 28) { Attribute(ref kv); } IToken/*!*/ x = t; Proposition(out e); - Expect(8); + Expect(9); m = new Axiom(x,e, null, kv); } void UserDefinedTypes(out List/*!*/ ts) { Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out ts))); Declaration/*!*/ decl; QKeyValue kv = null; ts = new List (); - Expect(30); - while (la.kind == 27) { + Expect(31); + while (la.kind == 28) { Attribute(ref kv); } UserDefinedType(out decl, kv); ts.Add(decl); - while (la.kind == 12) { + while (la.kind == 13) { Get(); UserDefinedType(out decl, kv); ts.Add(decl); } - Expect(8); + Expect(9); } void GlobalVars(out List/*!*/ ds) { @@ -461,12 +461,12 @@ private class BvBounds : Expr { ds = new List(); var dsx = ds; - Expect(7); - while (la.kind == 27) { + Expect(8); + while (la.kind == 28) { Attribute(ref kv); } IdsTypeWheres(true, "global variables", delegate(TypedIdent tyd) { dsx.Add(new GlobalVariable(tyd.tok, tyd, kv)); } ); - Expect(8); + Expect(9); } void Procedure(out Procedure/*!*/ proc, out /*maybe null*/ Implementation impl) { @@ -482,9 +482,9 @@ private class BvBounds : Expr { QKeyValue kv = null; impl = null; - Expect(32); + Expect(33); ProcSignature(true, out x, out typeParams, out ins, out outs, out kv); - if (la.kind == 8) { + if (la.kind == 9) { Get(); while (StartOf(3)) { Spec(pre, mods, post); @@ -497,7 +497,7 @@ private class BvBounds : Expr { impl = new Implementation(x, x.val, typeParams, Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, kv == null ? null : (QKeyValue)kv.Clone(), this.errors); - } else SynErr(99); + } else SynErr(100); proc = new Procedure(x, x.val, typeParams, ins, outs, pre, mods, post, kv); } @@ -509,7 +509,7 @@ private class BvBounds : Expr { StmtList/*!*/ stmtList; QKeyValue kv; - Expect(33); + Expect(34); 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); @@ -523,7 +523,7 @@ private class BvBounds : Expr { void IdsTypeWheres(bool allowWhereClauses, string context, System.Action action ) { IdsTypeWhere(allowWhereClauses, context, action); - while (la.kind == 12) { + while (la.kind == 13) { Get(); IdsTypeWhere(allowWhereClauses, context, action); } @@ -533,12 +533,12 @@ private class BvBounds : Expr { Contract.Ensures(Contract.ValueAtReturn(out ds) != null); QKeyValue kv = null; - Expect(7); - while (la.kind == 27) { + Expect(8); + while (la.kind == 28) { Attribute(ref kv); } IdsTypeWheres(true, "local variables", delegate(TypedIdent tyd) { ds.Add(new LocalVariable(tyd.tok, tyd, kv)); } ); - Expect(8); + Expect(9); } void ProcFormals(bool incoming, bool allowWhereClauses, out List/*!*/ ds) { @@ -547,16 +547,16 @@ private class BvBounds : Expr { var dsx = ds; var context = allowWhereClauses ? "procedure formals" : "the 'implementation' copies of formals"; - Expect(9); - if (la.kind == 1 || la.kind == 27) { + Expect(10); + if (la.kind == 1 || la.kind == 28) { AttrsIdsTypeWheres(allowWhereClauses, allowWhereClauses, context, delegate(TypedIdent tyd, QKeyValue kv) { dsx.Add(new Formal(tyd.tok, tyd, incoming, kv)); }); } - Expect(10); + Expect(11); } void AttrsIdsTypeWheres(bool allowAttributes, bool allowWhereClauses, string context, System.Action action ) { AttributesIdsTypeWhere(allowAttributes, allowWhereClauses, context, action); - while (la.kind == 12) { + while (la.kind == 13) { Get(); AttributesIdsTypeWhere(allowAttributes, allowWhereClauses, context, action); } @@ -575,7 +575,7 @@ private class BvBounds : Expr { void IdsType(out List/*!*/ tyds) { Contract.Ensures(Contract.ValueAtReturn(out tyds) != null); List/*!*/ ids; Bpl.Type/*!*/ ty; Idents(out ids); - Expect(11); + Expect(12); Type(out ty); tyds = new List(); foreach(Token/*!*/ id in ids){ @@ -589,7 +589,7 @@ private class BvBounds : Expr { Contract.Ensures(Contract.ValueAtReturn(out xs) != null); IToken/*!*/ id; xs = new List(); Ident(out id); xs.Add(id); - while (la.kind == 12) { + while (la.kind == 13) { Get(); Ident(out id); xs.Add(id); @@ -607,14 +607,14 @@ private class BvBounds : Expr { TypeArgs(args); } ty = new UnresolvedTypeIdentifier (tok, tok.val, args); - } else if (la.kind == 17 || la.kind == 19) { + } else if (la.kind == 18 || la.kind == 20) { MapType(out ty); - } else SynErr(100); + } else SynErr(101); } void AttributesIdsTypeWhere(bool allowAttributes, bool allowWhereClauses, string context, System.Action action ) { QKeyValue kv = null; - while (la.kind == 27) { + while (la.kind == 28) { Attribute(ref kv); if (!allowAttributes) { kv = null; @@ -628,9 +628,9 @@ private class BvBounds : Expr { void IdsTypeWhere(bool allowWhereClauses, string context, System.Action action ) { List/*!*/ ids; Bpl.Type/*!*/ ty; Expr wh = null; Expr/*!*/ nne; Idents(out ids); - Expect(11); + Expect(12); Type(out ty); - if (la.kind == 13) { + if (la.kind == 14) { Get(); Expression(out nne); if (!allowWhereClauses) { @@ -650,7 +650,7 @@ private class BvBounds : Expr { void Expression(out Expr/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; ImpliesExpression(false, out e0); - while (la.kind == 55 || la.kind == 56) { + while (la.kind == 56 || la.kind == 57) { EquivOp(); x = t; ImpliesExpression(false, out e1); @@ -660,20 +660,20 @@ private class BvBounds : Expr { void TypeAtom(out Bpl.Type/*!*/ ty) { Contract.Ensures(Contract.ValueAtReturn(out ty) != null); ty = dummyType; - if (la.kind == 14) { + if (la.kind == 15) { Get(); ty = new BasicType(t, SimpleType.Int); - } else if (la.kind == 15) { + } else if (la.kind == 16) { Get(); ty = new BasicType(t, SimpleType.Real); - } else if (la.kind == 16) { + } else if (la.kind == 17) { Get(); ty = new BasicType(t, SimpleType.Bool); - } else if (la.kind == 9) { + } else if (la.kind == 10) { Get(); Type(out ty); - Expect(10); - } else SynErr(101); + Expect(11); + } else SynErr(102); } void Ident(out IToken/*!*/ x) { @@ -700,10 +700,10 @@ private class BvBounds : Expr { if (StartOf(6)) { TypeArgs(ts); } - } else if (la.kind == 17 || la.kind == 19) { + } else if (la.kind == 18 || la.kind == 20) { MapType(out ty); ts.Add(ty); - } else SynErr(102); + } else SynErr(103); } void MapType(out Bpl.Type/*!*/ ty) { @@ -713,16 +713,16 @@ private class BvBounds : Expr { Bpl.Type/*!*/ result; List/*!*/ typeParameters = new List(); - if (la.kind == 19) { + if (la.kind == 20) { TypeParams(out nnTok, out typeParameters); tok = nnTok; } - Expect(17); + Expect(18); if (tok == null) tok = t; if (StartOf(6)) { Types(arguments); } - Expect(18); + Expect(19); Type(out result); ty = new MapType(tok, typeParameters, arguments, result); @@ -730,10 +730,10 @@ private class BvBounds : Expr { void TypeParams(out IToken/*!*/ tok, out List/*!*/ typeParams) { Contract.Ensures(Contract.ValueAtReturn(out tok) != null); Contract.Ensures(Contract.ValueAtReturn(out typeParams) != null); List/*!*/ typeParamToks; - Expect(19); + Expect(20); tok = t; Idents(out typeParamToks); - Expect(20); + Expect(21); typeParams = new List (); foreach(Token/*!*/ id in typeParamToks){ Contract.Assert(id != null); @@ -745,7 +745,7 @@ private class BvBounds : Expr { Contract.Requires(ts != null); Bpl.Type/*!*/ ty; Type(out ty); ts.Add(ty); - while (la.kind == 12) { + while (la.kind == 13) { Get(); Type(out ty); ts.Add(ty); @@ -757,21 +757,21 @@ private class BvBounds : Expr { Parents = null; bool u; IToken/*!*/ parent; - Expect(23); + Expect(24); Parents = new List (); u = false; - if (la.kind == 1 || la.kind == 22) { - if (la.kind == 22) { + if (la.kind == 1 || la.kind == 23) { + if (la.kind == 23) { Get(); u = true; } Ident(out parent); Parents.Add(new ConstantParent ( new IdentifierExpr(parent, parent.val), u)); - while (la.kind == 12) { + while (la.kind == 13) { Get(); u = false; - if (la.kind == 22) { + if (la.kind == 23) { Get(); u = true; } @@ -780,7 +780,7 @@ private class BvBounds : Expr { new IdentifierExpr(parent, parent.val), u)); } } - if (la.kind == 24) { + if (la.kind == 25) { Get(); ChildrenComplete = true; } @@ -793,12 +793,12 @@ private class BvBounds : Expr { IToken/*!*/ tok; kv = null; - while (la.kind == 27) { + while (la.kind == 28) { Attribute(ref kv); } Type(out ty); tok = ty.tok; - if (la.kind == 11) { + if (la.kind == 12) { Get(); var uti = ty as UnresolvedTypeIdentifier; if (uti != null && uti.Arguments.Count == 0) { @@ -824,7 +824,7 @@ private class BvBounds : Expr { if (la.kind == 1) { WhiteSpaceIdents(out paramTokens); } - if (la.kind == 31) { + if (la.kind == 32) { Get(); Type(out body); synonym = true; @@ -856,15 +856,15 @@ out List/*!*/ ins, out List/*!*/ 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(); outs = new List(); kv = null; - while (la.kind == 27) { + while (la.kind == 28) { Attribute(ref kv); } Ident(out name); - if (la.kind == 19) { + if (la.kind == 20) { TypeParams(out typeParamTok, out typeParams); } ProcFormals(true, allowWhereClausesOnFormals, out ins); - if (la.kind == 26) { + if (la.kind == 27) { Get(); ProcFormals(false, allowWhereClausesOnFormals, out outs); } @@ -872,7 +872,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { void Spec(List/*!*/ pre, List/*!*/ mods, List/*!*/ post) { Contract.Requires(pre != null); Contract.Requires(mods != null); Contract.Requires(post != null); List/*!*/ ms; - if (la.kind == 34) { + if (la.kind == 35) { Get(); if (la.kind == 1) { Idents(out ms); @@ -882,19 +882,19 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { } } - Expect(8); - } else if (la.kind == 35) { + Expect(9); + } else if (la.kind == 36) { Get(); SpecPrePost(true, pre, post); - } else if (la.kind == 36 || la.kind == 37) { + } else if (la.kind == 37 || la.kind == 38) { SpecPrePost(false, pre, post); - } else SynErr(103); + } else SynErr(104); } void ImplBody(out List/*!*/ locals, out StmtList/*!*/ stmtList) { Contract.Ensures(Contract.ValueAtReturn(out locals) != null); Contract.Ensures(Contract.ValueAtReturn(out stmtList) != null); locals = new List(); - Expect(27); - while (la.kind == 7) { + Expect(28); + while (la.kind == 8) { LocalVars(locals); } StmtList(out stmtList); @@ -902,25 +902,25 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { void SpecPrePost(bool free, List/*!*/ pre, List/*!*/ post) { Contract.Requires(pre != null); Contract.Requires(post != null); Expr/*!*/ e; Token tok = null; QKeyValue kv = null; - if (la.kind == 36) { + if (la.kind == 37) { Get(); tok = t; - while (la.kind == 27) { + while (la.kind == 28) { Attribute(ref kv); } Proposition(out e); - Expect(8); + Expect(9); pre.Add(new Requires(tok, free, e, null, kv)); - } else if (la.kind == 37) { + } else if (la.kind == 38) { Get(); tok = t; - while (la.kind == 27) { + while (la.kind == 28) { Attribute(ref kv); } Proposition(out e); - Expect(8); + Expect(9); post.Add(new Ensures(tok, free, e, null, kv)); - } else SynErr(104); + } else SynErr(105); } void StmtList(out StmtList/*!*/ stmtList) { @@ -957,7 +957,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { cs = new List(); } - } else if (la.kind == 40 || la.kind == 42 || la.kind == 45) { + } else if (la.kind == 41 || la.kind == 43 || la.kind == 46) { StructuredCmd(out ecn); ec = ecn; if (startToken == null) { startToken = ec.tok; cs = new List(); } @@ -977,7 +977,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { } } - Expect(28); + Expect(29); IToken/*!*/ endCurly = t; if (startToken == null && bigblocks.Count == 0) { startToken = t; cs = new List(); @@ -1005,33 +1005,33 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { LabelOrAssign(out c, out label); break; } - case 46: { + case 47: { Get(); x = t; - while (la.kind == 27) { + while (la.kind == 28) { Attribute(ref kv); } Proposition(out e); c = new AssertCmd(x, e, kv); - Expect(8); + Expect(9); break; } - case 47: { + case 48: { Get(); x = t; - while (la.kind == 27) { + while (la.kind == 28) { Attribute(ref kv); } Proposition(out e); c = new AssumeCmd(x, e, kv); - Expect(8); + Expect(9); break; } - case 48: { + case 49: { Get(); x = t; Idents(out xs); - Expect(8); + Expect(9); ids = new List(); foreach(IToken/*!*/ y in xs){ Contract.Assert(y != null); @@ -1041,25 +1041,25 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { break; } - case 35: case 51: case 52: { + case 36: case 52: case 53: { CallCmd(out cn); - Expect(8); + Expect(9); c = cn; break; } - case 53: { + case 54: { ParCallCmd(out cn); c = cn; break; } - case 49: { + case 50: { Get(); x = t; - Expect(8); + Expect(9); c = new YieldCmd(x); break; } - default: SynErr(105); break; + default: SynErr(106); break; } } @@ -1067,16 +1067,16 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { Contract.Ensures(Contract.ValueAtReturn(out ec) != null); ec = dummyStructuredCmd; Contract.Assume(cce.IsPeerConsistent(ec)); IfCmd/*!*/ ifcmd; WhileCmd/*!*/ wcmd; BreakCmd/*!*/ bcmd; - if (la.kind == 40) { + if (la.kind == 41) { IfCmd(out ifcmd); ec = ifcmd; - } else if (la.kind == 42) { + } else if (la.kind == 43) { WhileCmd(out wcmd); ec = wcmd; - } else if (la.kind == 45) { + } else if (la.kind == 46) { BreakCmd(out bcmd); ec = bcmd; - } else SynErr(106); + } else SynErr(107); } void TransferCmd(out TransferCmd/*!*/ tc) { @@ -1084,7 +1084,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { Token y; List/*!*/ xs; List ss = new List(); - if (la.kind == 38) { + if (la.kind == 39) { Get(); y = t; Idents(out xs); @@ -1093,11 +1093,11 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { ss.Add(s.val); } tc = new GotoCmd(y, ss); - } else if (la.kind == 39) { + } else if (la.kind == 40) { Get(); tc = new ReturnCmd(t); - } else SynErr(107); - Expect(8); + } else SynErr(108); + Expect(9); } void IfCmd(out IfCmd/*!*/ ifcmd) { @@ -1107,21 +1107,21 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { IfCmd/*!*/ elseIf; IfCmd elseIfOption = null; StmtList/*!*/ els; StmtList elseOption = null; - Expect(40); + Expect(41); x = t; Guard(out guard); - Expect(27); + Expect(28); StmtList(out thn); - if (la.kind == 41) { + if (la.kind == 42) { Get(); - if (la.kind == 40) { + if (la.kind == 41) { IfCmd(out elseIf); elseIfOption = elseIf; - } else if (la.kind == 27) { + } else if (la.kind == 28) { Get(); StmtList(out els); elseOption = els; - } else SynErr(108); + } else SynErr(109); } ifcmd = new IfCmd(x, guard, thn, elseIfOption, elseOption); } @@ -1133,18 +1133,18 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { StmtList/*!*/ body; QKeyValue kv = null; - Expect(42); + Expect(43); x = t; Guard(out guard); Contract.Assume(guard == null || cce.Owner.None(guard)); - while (la.kind == 35 || la.kind == 43) { + while (la.kind == 36 || la.kind == 44) { isFree = false; z = la/*lookahead token*/; - if (la.kind == 35) { + if (la.kind == 36) { Get(); isFree = true; } - Expect(43); - while (la.kind == 27) { + Expect(44); + while (la.kind == 28) { Attribute(ref kv); } Expression(out e); @@ -1155,9 +1155,9 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { } kv = null; - Expect(8); + Expect(9); } - Expect(27); + Expect(28); StmtList(out body); wcmd = new WhileCmd(x, guard, invariants, body); } @@ -1166,27 +1166,27 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { Contract.Ensures(Contract.ValueAtReturn(out bcmd) != null); IToken/*!*/ x; IToken/*!*/ y; string breakLabel = null; - Expect(45); + Expect(46); x = t; if (la.kind == 1) { Ident(out y); breakLabel = y.val; } - Expect(8); + Expect(9); bcmd = new BreakCmd(x, breakLabel); } void Guard(out Expr e) { Expr/*!*/ ee; e = null; - Expect(9); - if (la.kind == 44) { + Expect(10); + if (la.kind == 45) { Get(); e = null; } else if (StartOf(9)) { Expression(out ee); e = ee; - } else SynErr(109); - Expect(10); + } else SynErr(110); + Expect(11); } void LabelOrAssign(out Cmd c, out IToken label) { @@ -1199,40 +1199,40 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { Ident(out id); x = t; - if (la.kind == 11) { + if (la.kind == 12) { Get(); c = null; label = x; - } else if (la.kind == 12 || la.kind == 17 || la.kind == 50) { + } else if (la.kind == 13 || la.kind == 18 || la.kind == 51) { lhss = new List(); lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val)); - while (la.kind == 17) { + while (la.kind == 18) { MapAssignIndex(out y, out indexes); lhs = new MapAssignLhs(y, lhs, indexes); } lhss.Add(lhs); - while (la.kind == 12) { + while (la.kind == 13) { Get(); Ident(out id); lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val)); - while (la.kind == 17) { + while (la.kind == 18) { MapAssignIndex(out y, out indexes); lhs = new MapAssignLhs(y, lhs, indexes); } lhss.Add(lhs); } - Expect(50); + Expect(51); x = t; /* use location of := */ Expression(out e0); rhss = new List (); rhss.Add(e0); - while (la.kind == 12) { + while (la.kind == 13) { Get(); Expression(out e0); rhss.Add(e0); } - Expect(8); + Expect(9); c = new AssignCmd(x, lhss, rhss); - } else SynErr(110); + } else SynErr(111); } void CallCmd(out Cmd c) { @@ -1243,17 +1243,17 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { QKeyValue kv = null; c = null; - if (la.kind == 51) { + if (la.kind == 52) { Get(); isAsync = true; } - if (la.kind == 35) { + if (la.kind == 36) { Get(); isFree = true; } - Expect(52); + Expect(53); x = t; - while (la.kind == 27) { + while (la.kind == 28) { Attribute(ref kv); } CallParams(isAsync, isFree, kv, x, out c); @@ -1267,19 +1267,19 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { Cmd c = null; List callCmds = new List(); - Expect(53); + Expect(54); x = t; - while (la.kind == 27) { + while (la.kind == 28) { Attribute(ref kv); } CallParams(false, false, kv, x, out c); callCmds.Add((CallCmd)c); - while (la.kind == 54) { + while (la.kind == 55) { Get(); CallParams(false, false, kv, x, out c); callCmds.Add((CallCmd)c); } - Expect(8); + Expect(9); d = new ParCallCmd(x, callCmds, kv); } @@ -1287,18 +1287,18 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { Contract.Ensures(Contract.ValueAtReturn(out x) != null); Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out indexes))); indexes = new List (); Expr/*!*/ e; - Expect(17); + Expect(18); x = t; if (StartOf(9)) { Expression(out e); indexes.Add(e); - while (la.kind == 12) { + while (la.kind == 13) { Get(); Expression(out e); indexes.Add(e); } } - Expect(18); + Expect(19); } void CallParams(bool isAsync, bool isFree, QKeyValue kv, IToken x, out Cmd c) { @@ -1310,53 +1310,53 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { c = null; Ident(out first); - if (la.kind == 9) { + if (la.kind == 10) { Get(); if (StartOf(9)) { Expression(out en); es.Add(en); - while (la.kind == 12) { + while (la.kind == 13) { Get(); Expression(out en); es.Add(en); } } - Expect(10); + Expect(11); c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync; - } else if (la.kind == 12 || la.kind == 50) { + } else if (la.kind == 13 || la.kind == 51) { ids.Add(new IdentifierExpr(first, first.val)); - if (la.kind == 12) { + if (la.kind == 13) { Get(); Ident(out p); ids.Add(new IdentifierExpr(p, p.val)); - while (la.kind == 12) { + while (la.kind == 13) { Get(); Ident(out p); ids.Add(new IdentifierExpr(p, p.val)); } } - Expect(50); + Expect(51); Ident(out first); - Expect(9); + Expect(10); if (StartOf(9)) { Expression(out en); es.Add(en); - while (la.kind == 12) { + while (la.kind == 13) { Get(); Expression(out en); es.Add(en); } } - Expect(10); + Expect(11); c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync; - } else SynErr(111); + } else SynErr(112); } void Expressions(out List/*!*/ es) { Contract.Ensures(Contract.ValueAtReturn(out es) != null); Expr/*!*/ e; es = new List(); Expression(out e); es.Add(e); - while (la.kind == 12) { + while (la.kind == 13) { Get(); Expression(out e); es.Add(e); @@ -1367,7 +1367,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; LogicalExpression(out e0); if (StartOf(10)) { - if (la.kind == 57 || la.kind == 58) { + if (la.kind == 58 || la.kind == 59) { ImpliesOp(); x = t; ImpliesExpression(true, out e1); @@ -1379,7 +1379,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { x = t; LogicalExpression(out e1); e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e1, e0); - while (la.kind == 59 || la.kind == 60) { + while (la.kind == 60 || la.kind == 61) { ExpliesOp(); x = t; LogicalExpression(out e1); @@ -1390,23 +1390,23 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { } void EquivOp() { - if (la.kind == 55) { + if (la.kind == 56) { Get(); - } else if (la.kind == 56) { + } else if (la.kind == 57) { Get(); - } else SynErr(112); + } else SynErr(113); } void LogicalExpression(out Expr/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; RelationalExpression(out e0); if (StartOf(11)) { - if (la.kind == 61 || la.kind == 62) { + if (la.kind == 62 || la.kind == 63) { AndOp(); x = t; RelationalExpression(out e1); e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1); - while (la.kind == 61 || la.kind == 62) { + while (la.kind == 62 || la.kind == 63) { AndOp(); x = t; RelationalExpression(out e1); @@ -1417,7 +1417,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { x = t; RelationalExpression(out e1); e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1); - while (la.kind == 63 || la.kind == 64) { + while (la.kind == 64 || la.kind == 65) { OrOp(); x = t; RelationalExpression(out e1); @@ -1428,19 +1428,19 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { } void ImpliesOp() { - if (la.kind == 57) { + if (la.kind == 58) { Get(); - } else if (la.kind == 58) { + } else if (la.kind == 59) { Get(); - } else SynErr(113); + } else SynErr(114); } void ExpliesOp() { - if (la.kind == 59) { + if (la.kind == 60) { Get(); - } else if (la.kind == 60) { + } else if (la.kind == 61) { Get(); - } else SynErr(114); + } else SynErr(115); } void RelationalExpression(out Expr/*!*/ e0) { @@ -1454,25 +1454,25 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { } void AndOp() { - if (la.kind == 61) { + if (la.kind == 62) { Get(); - } else if (la.kind == 62) { + } else if (la.kind == 63) { Get(); - } else SynErr(115); + } else SynErr(116); } void OrOp() { - if (la.kind == 63) { + if (la.kind == 64) { Get(); - } else if (la.kind == 64) { + } else if (la.kind == 65) { Get(); - } else SynErr(116); + } else SynErr(117); } void BvTerm(out Expr/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; Term(out e0); - while (la.kind == 73) { + while (la.kind == 74) { Get(); x = t; Term(out e1); @@ -1483,64 +1483,64 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { void RelOp(out IToken/*!*/ x, out BinaryOperator.Opcode op) { Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; switch (la.kind) { - case 65: { + case 66: { Get(); x = t; op=BinaryOperator.Opcode.Eq; break; } - case 19: { + case 20: { Get(); x = t; op=BinaryOperator.Opcode.Lt; break; } - case 20: { + case 21: { Get(); x = t; op=BinaryOperator.Opcode.Gt; break; } - case 66: { + case 67: { Get(); x = t; op=BinaryOperator.Opcode.Le; break; } - case 67: { + case 68: { Get(); x = t; op=BinaryOperator.Opcode.Ge; break; } - case 68: { + case 69: { Get(); x = t; op=BinaryOperator.Opcode.Neq; break; } - case 69: { + case 70: { Get(); x = t; op=BinaryOperator.Opcode.Subtype; break; } - case 70: { + case 71: { Get(); x = t; op=BinaryOperator.Opcode.Neq; break; } - case 71: { + case 72: { Get(); x = t; op=BinaryOperator.Opcode.Le; break; } - case 72: { + case 73: { Get(); x = t; op=BinaryOperator.Opcode.Ge; break; } - default: SynErr(117); break; + default: SynErr(118); break; } } void Term(out Expr/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; BinaryOperator.Opcode op; Factor(out e0); - while (la.kind == 74 || la.kind == 75) { + while (la.kind == 75 || la.kind == 76) { AddOp(out x, out op); Factor(out e1); e0 = Expr.Binary(x, op, e0, e1); @@ -1559,19 +1559,19 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { void AddOp(out IToken/*!*/ x, out BinaryOperator.Opcode op) { Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; - if (la.kind == 74) { + if (la.kind == 75) { Get(); x = t; op=BinaryOperator.Opcode.Add; - } else if (la.kind == 75) { + } else if (la.kind == 76) { Get(); x = t; op=BinaryOperator.Opcode.Sub; - } else SynErr(118); + } else SynErr(119); } void Power(out Expr/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; UnaryExpression(out e0); - if (la.kind == 79) { + if (la.kind == 80) { Get(); x = t; Power(out e1); @@ -1581,46 +1581,46 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { void MulOp(out IToken/*!*/ x, out BinaryOperator.Opcode op) { Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; - if (la.kind == 44) { + if (la.kind == 45) { Get(); x = t; op=BinaryOperator.Opcode.Mul; - } else if (la.kind == 76) { + } else if (la.kind == 77) { Get(); x = t; op=BinaryOperator.Opcode.Div; - } else if (la.kind == 77) { + } else if (la.kind == 78) { Get(); x = t; op=BinaryOperator.Opcode.Mod; - } else if (la.kind == 78) { + } else if (la.kind == 79) { Get(); x = t; op=BinaryOperator.Opcode.RealDiv; - } else SynErr(119); + } else SynErr(120); } void UnaryExpression(out Expr/*!*/ e) { Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; e = dummyExpr; - if (la.kind == 75) { + if (la.kind == 76) { Get(); x = t; UnaryExpression(out e); e = Expr.Unary(x, UnaryOperator.Opcode.Neg, e); - } else if (la.kind == 80 || la.kind == 81) { + } else if (la.kind == 81 || la.kind == 82) { NegOp(); x = t; UnaryExpression(out e); e = Expr.Unary(x, UnaryOperator.Opcode.Not, e); } else if (StartOf(14)) { CoercionExpression(out e); - } else SynErr(120); + } else SynErr(121); } void NegOp() { - if (la.kind == 80) { + if (la.kind == 81) { Get(); - } else if (la.kind == 81) { + } else if (la.kind == 82) { Get(); - } else SynErr(121); + } else SynErr(122); } void CoercionExpression(out Expr/*!*/ e) { @@ -1629,7 +1629,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { BigNum bn; ArrayExpression(out e); - while (la.kind == 11) { + while (la.kind == 12) { Get(); x = t; if (StartOf(6)) { @@ -1644,7 +1644,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { e = new BvBounds(x, bn, ((LiteralExpr)e).asBigNum); } - } else SynErr(122); + } else SynErr(123); } } @@ -1655,7 +1655,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { List/*!*/ allArgs = dummyExprSeq; AtomExpression(out e); - while (la.kind == 17) { + while (la.kind == 18) { Get(); x = t; allArgs = new List (); allArgs.Add(e); @@ -1668,7 +1668,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { else allArgs.Add(index0); - while (la.kind == 12) { + while (la.kind == 13) { Get(); Expression(out e1); if (bvExtract || e1 is BvBounds) @@ -1676,7 +1676,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { allArgs.Add(e1); } - if (la.kind == 50) { + if (la.kind == 51) { Get(); Expression(out e1); if (bvExtract || e1 is BvBounds) @@ -1690,7 +1690,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { allArgs.Add(e1); store = true; } } - Expect(18); + Expect(19); if (store) e = new NAryExpr(x, new MapStore(x, allArgs.Count - 2), allArgs); else if (bvExtract) @@ -1715,7 +1715,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { } void AtomExpression(out Expr/*!*/ e) { - Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; int n; BigNum bn; BigDec bd; + Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; int n; BigNum bn; BigDec bd; BigFloat bf; List/*!*/ es; List/*!*/ ds; Trigger trig; List/*!*/ typeParams; IdentifierExpr/*!*/ id; @@ -1725,12 +1725,12 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { List/*!*/ blocks; switch (la.kind) { - case 82: { + case 83: { Get(); e = new LiteralExpr(t, false); break; } - case 83: { + case 84: { Get(); e = new LiteralExpr(t, true); break; @@ -1745,6 +1745,11 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { e = new LiteralExpr(t, bd); break; } + case 7: { + Float(out bf); + e = new LiteralExpr(t, bf); + break; + } case 2: { BvLit(out bn, out n); e = new LiteralExpr(t, bn, n); @@ -1753,65 +1758,65 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { case 1: { Ident(out x); id = new IdentifierExpr(x, x.val); e = id; - if (la.kind == 9) { + if (la.kind == 10) { Get(); if (StartOf(9)) { Expressions(out es); e = new NAryExpr(x, new FunctionCall(id), es); - } else if (la.kind == 10) { + } else if (la.kind == 11) { e = new NAryExpr(x, new FunctionCall(id), new List()); - } else SynErr(123); - Expect(10); + } else SynErr(124); + Expect(11); } break; } - case 84: { + case 85: { Get(); x = t; - Expect(9); - Expression(out e); Expect(10); + Expression(out e); + Expect(11); e = new OldExpr(x, e); break; } - case 14: { + case 15: { Get(); x = t; - Expect(9); - Expression(out e); Expect(10); + Expression(out e); + Expect(11); e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToInt), new List{ e }); break; } - case 15: { + case 16: { Get(); x = t; - Expect(9); - Expression(out e); Expect(10); + Expression(out e); + Expect(11); e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToReal), new List{ e }); break; } - case 9: { + case 10: { Get(); if (StartOf(9)) { Expression(out e); if (e is BvBounds) this.SemErr("parentheses around bitvector bounds " + "are not allowed"); - } else if (la.kind == 88 || la.kind == 89) { + } else if (la.kind == 89 || la.kind == 90) { Forall(); x = t; QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e); if (typeParams.Count + ds.Count > 0) e = new ForallExpr(x, typeParams, ds, kv, trig, e); - } else if (la.kind == 90 || la.kind == 91) { + } else if (la.kind == 91 || la.kind == 92) { Exists(); x = t; QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e); if (typeParams.Count + ds.Count > 0) e = new ExistsExpr(x, typeParams, ds, kv, trig, e); - } else if (la.kind == 92 || la.kind == 93) { + } else if (la.kind == 93 || la.kind == 94) { Lambda(); x = t; QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e); @@ -1819,20 +1824,20 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { SemErr("triggers not allowed in lambda expressions"); if (typeParams.Count + ds.Count > 0) e = new LambdaExpr(x, typeParams, ds, kv, e); - } else SynErr(124); - Expect(10); + } else SynErr(125); + Expect(11); break; } - case 40: { + case 41: { IfThenElseExpression(out e); break; } - case 85: { + case 86: { CodeExpression(out locals, out blocks); e = new CodeExpr(locals, blocks); break; } - default: SynErr(125); break; + default: SynErr(126); break; } } @@ -1844,7 +1849,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { } else if (la.kind == 6) { Get(); s = t.val; - } else SynErr(126); + } else SynErr(127); try { n = BigDec.FromString(s); } catch (FormatException) { @@ -1854,6 +1859,19 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { } + void Float(out BigFloat n) { + string s = ""; + Expect(7); + s = t.val; + try { + n = BigFloat.FromString(s); + } catch (FormatException e) { + this.SemErr("incorrectly formatted floating point: " + e.Message); + n = BigFloat.ZERO; + } + + } + void BvLit(out BigNum n, out int m) { Expect(2); int pos = t.val.IndexOf("bv"); @@ -1871,11 +1889,11 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { } void Forall() { - if (la.kind == 88) { + if (la.kind == 89) { Get(); - } else if (la.kind == 89) { + } else if (la.kind == 90) { Get(); - } else SynErr(127); + } else SynErr(128); } void QuantifierBody(IToken/*!*/ q, out List/*!*/ typeParams, out List/*!*/ ds, @@ -1886,35 +1904,35 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { kv = null; ds = new List (); - if (la.kind == 19) { + if (la.kind == 20) { TypeParams(out tok, out typeParams); - if (la.kind == 1 || la.kind == 27) { + if (la.kind == 1 || la.kind == 28) { BoundVars(q, out ds); } - } else if (la.kind == 1 || la.kind == 27) { + } else if (la.kind == 1 || la.kind == 28) { BoundVars(q, out ds); - } else SynErr(128); + } else SynErr(129); QSep(); - while (la.kind == 27) { + while (la.kind == 28) { AttributeOrTrigger(ref kv, ref trig); } Expression(out body); } void Exists() { - if (la.kind == 90) { + if (la.kind == 91) { Get(); - } else if (la.kind == 91) { + } else if (la.kind == 92) { Get(); - } else SynErr(129); + } else SynErr(130); } void Lambda() { - if (la.kind == 92) { + if (la.kind == 93) { Get(); - } else if (la.kind == 93) { + } else if (la.kind == 94) { Get(); - } else SynErr(130); + } else SynErr(131); } void IfThenElseExpression(out Expr/*!*/ e) { @@ -1922,12 +1940,12 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { IToken/*!*/ tok; Expr/*!*/ e0, e1, e2; e = dummyExpr; - Expect(40); + Expect(41); tok = t; Expression(out e0); - Expect(87); + Expect(88); Expression(out e1); - Expect(41); + Expect(42); Expression(out e2); e = new NAryExpr(tok, new IfThenElse(tok), new List{ e0, e1, e2 }); } @@ -1936,8 +1954,8 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { Contract.Ensures(Contract.ValueAtReturn(out locals) != null); Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out blocks))); locals = new List(); Block/*!*/ b; blocks = new List(); - Expect(85); - while (la.kind == 7) { + Expect(86); + while (la.kind == 8) { LocalVars(locals); } SpecBlock(out b); @@ -1946,7 +1964,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { SpecBlock(out b); blocks.Add(b); } - Expect(86); + Expect(87); } void SpecBlock(out Block/*!*/ b) { @@ -1959,7 +1977,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { Expr/*!*/ e; Ident(out x); - Expect(11); + Expect(12); while (StartOf(8)) { LabelOrCmd(out c, out label); if (c != null) { @@ -1971,7 +1989,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { } } - if (la.kind == 38) { + if (la.kind == 39) { Get(); y = t; Idents(out xs); @@ -1980,12 +1998,12 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { ss.Add(s.val); } b = new Block(x,x.val,cs,new GotoCmd(y,ss)); - } else if (la.kind == 39) { + } else if (la.kind == 40) { Get(); Expression(out e); b = new Block(x,x.val,cs,new ReturnExprCmd(t,e)); - } else SynErr(131); - Expect(8); + } else SynErr(132); + Expect(9); } void AttributeOrTrigger(ref QKeyValue kv, ref Trigger trig) { @@ -1993,16 +2011,16 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { string key; List parameters; object/*!*/ param; - Expect(27); + Expect(28); tok = t; - if (la.kind == 11) { + if (la.kind == 12) { Get(); Expect(1); key = t.val; parameters = new List(); if (StartOf(16)) { AttributeParameter(out param); parameters.Add(param); - while (la.kind == 12) { + while (la.kind == 13) { Get(); AttributeParameter(out param); parameters.Add(param); @@ -2030,7 +2048,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { } else if (StartOf(9)) { Expression(out e); es = new List { e }; - while (la.kind == 12) { + while (la.kind == 13) { Get(); Expression(out e); es.Add(e); @@ -2041,8 +2059,8 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { trig.AddLast(new Trigger(tok, true, es, null)); } - } else SynErr(132); - Expect(28); + } else SynErr(133); + Expect(29); } void AttributeParameter(out object/*!*/ o) { @@ -2056,15 +2074,15 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { } else if (StartOf(9)) { Expression(out e); o = e; - } else SynErr(133); + } else SynErr(134); } void QSep() { - if (la.kind == 94) { + if (la.kind == 95) { Get(); - } else if (la.kind == 95) { + } else if (la.kind == 96) { Get(); - } else SynErr(134); + } else SynErr(135); } @@ -2080,23 +2098,23 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { } static readonly bool[,]/*!*/ set = { - {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, - {x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,T,x,x, x,T,T,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, - {x,T,x,x, x,x,x,x, x,T,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, - {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, - {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, - {x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, - {x,T,x,x, x,x,x,x, x,T,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, - {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,x,T,x, x,T,T,T, T,T,x,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, - {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, - {x,T,T,T, x,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x}, - {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, - {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, - {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, - {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, - {x,T,T,T, x,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x}, - {x,T,T,T, x,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x}, - {x,T,T,T, T,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x} + {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x}, + {x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,T,x, x,x,T,T, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x}, + {x,T,x,x, x,x,x,x, x,x,T,x, x,x,x,T, T,T,T,x, T,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x}, + {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x}, + {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x}, + {x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x}, + {x,T,x,x, x,x,x,x, x,x,T,x, x,x,x,T, T,T,T,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x}, + {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,x,T, x,x,T,T, T,T,T,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x}, + {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,T, T,T,T,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x}, + {x,T,T,T, x,T,T,T, x,x,T,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x}, + {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x}, + {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x}, + {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x}, + {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x}, + {x,T,T,T, x,T,T,T, x,x,T,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x}, + {x,T,T,T, x,T,T,T, x,x,T,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x}, + {x,T,T,T, T,T,T,T, x,x,T,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x} }; } // end Parser @@ -2127,135 +2145,136 @@ public class Errors { case 3: s = "digits expected"; break; case 4: s = "string expected"; break; case 5: s = "decimal expected"; break; - case 6: s = "float expected"; break; - case 7: s = "\"var\" expected"; break; - case 8: s = "\";\" expected"; break; - case 9: s = "\"(\" expected"; break; - case 10: s = "\")\" expected"; break; - case 11: s = "\":\" expected"; break; - case 12: s = "\",\" expected"; break; - case 13: s = "\"where\" expected"; break; - case 14: s = "\"int\" expected"; break; - case 15: s = "\"real\" expected"; break; - case 16: s = "\"bool\" expected"; break; - case 17: s = "\"[\" expected"; break; - case 18: s = "\"]\" expected"; break; - case 19: s = "\"<\" expected"; break; - case 20: s = "\">\" expected"; break; - case 21: s = "\"const\" expected"; break; - case 22: s = "\"unique\" expected"; break; - case 23: s = "\"extends\" expected"; break; - case 24: s = "\"complete\" expected"; break; - case 25: s = "\"function\" expected"; break; - case 26: s = "\"returns\" expected"; break; - case 27: s = "\"{\" expected"; break; - case 28: s = "\"}\" expected"; break; - case 29: s = "\"axiom\" expected"; break; - case 30: s = "\"type\" expected"; break; - case 31: s = "\"=\" expected"; break; - case 32: s = "\"procedure\" expected"; break; - case 33: s = "\"implementation\" expected"; break; - case 34: s = "\"modifies\" expected"; break; - case 35: s = "\"free\" expected"; break; - case 36: s = "\"requires\" expected"; break; - case 37: s = "\"ensures\" expected"; break; - case 38: s = "\"goto\" expected"; break; - case 39: s = "\"return\" expected"; break; - case 40: s = "\"if\" expected"; break; - case 41: s = "\"else\" expected"; break; - case 42: s = "\"while\" expected"; break; - case 43: s = "\"invariant\" expected"; break; - case 44: s = "\"*\" expected"; break; - case 45: s = "\"break\" expected"; break; - case 46: s = "\"assert\" expected"; break; - case 47: s = "\"assume\" expected"; break; - case 48: s = "\"havoc\" expected"; break; - case 49: s = "\"yield\" expected"; break; - case 50: s = "\":=\" expected"; break; - case 51: s = "\"async\" expected"; break; - case 52: s = "\"call\" expected"; break; - case 53: s = "\"par\" expected"; break; - case 54: s = "\"|\" expected"; break; - case 55: s = "\"<==>\" expected"; break; - case 56: s = "\"\\u21d4\" expected"; break; - case 57: s = "\"==>\" expected"; break; - case 58: s = "\"\\u21d2\" expected"; break; - case 59: s = "\"<==\" expected"; break; - case 60: s = "\"\\u21d0\" expected"; break; - case 61: s = "\"&&\" expected"; break; - case 62: s = "\"\\u2227\" expected"; break; - case 63: s = "\"||\" expected"; break; - case 64: s = "\"\\u2228\" expected"; break; - case 65: s = "\"==\" expected"; break; - case 66: s = "\"<=\" expected"; break; - case 67: s = "\">=\" expected"; break; - case 68: s = "\"!=\" expected"; break; - case 69: s = "\"<:\" expected"; break; - case 70: s = "\"\\u2260\" expected"; break; - case 71: s = "\"\\u2264\" expected"; break; - case 72: s = "\"\\u2265\" expected"; break; - case 73: s = "\"++\" expected"; break; - case 74: s = "\"+\" expected"; break; - case 75: s = "\"-\" expected"; break; - case 76: s = "\"div\" expected"; break; - case 77: s = "\"mod\" expected"; break; - case 78: s = "\"/\" expected"; break; - case 79: s = "\"**\" expected"; break; - case 80: s = "\"!\" expected"; break; - case 81: s = "\"\\u00ac\" expected"; break; - case 82: s = "\"false\" expected"; break; - case 83: s = "\"true\" expected"; break; - case 84: s = "\"old\" expected"; break; - case 85: s = "\"|{\" expected"; break; - case 86: s = "\"}|\" expected"; break; - case 87: s = "\"then\" expected"; break; - case 88: s = "\"forall\" expected"; break; - case 89: s = "\"\\u2200\" expected"; break; - case 90: s = "\"exists\" expected"; break; - case 91: s = "\"\\u2203\" expected"; break; - case 92: s = "\"lambda\" expected"; break; - case 93: s = "\"\\u03bb\" expected"; break; - case 94: s = "\"::\" expected"; break; - case 95: s = "\"\\u2022\" expected"; break; - case 96: s = "??? expected"; break; - case 97: s = "invalid Function"; break; + case 6: s = "dec_float expected"; break; + case 7: s = "float expected"; break; + case 8: s = "\"var\" expected"; break; + case 9: s = "\";\" expected"; break; + case 10: s = "\"(\" expected"; break; + case 11: s = "\")\" expected"; break; + case 12: s = "\":\" expected"; break; + case 13: s = "\",\" expected"; break; + case 14: s = "\"where\" expected"; break; + case 15: s = "\"int\" expected"; break; + case 16: s = "\"real\" expected"; break; + case 17: s = "\"bool\" expected"; break; + case 18: s = "\"[\" expected"; break; + case 19: s = "\"]\" expected"; break; + case 20: s = "\"<\" expected"; break; + case 21: s = "\">\" expected"; break; + case 22: s = "\"const\" expected"; break; + case 23: s = "\"unique\" expected"; break; + case 24: s = "\"extends\" expected"; break; + case 25: s = "\"complete\" expected"; break; + case 26: s = "\"function\" expected"; break; + case 27: s = "\"returns\" expected"; break; + case 28: s = "\"{\" expected"; break; + case 29: s = "\"}\" expected"; break; + case 30: s = "\"axiom\" expected"; break; + case 31: s = "\"type\" expected"; break; + case 32: s = "\"=\" expected"; break; + case 33: s = "\"procedure\" expected"; break; + case 34: s = "\"implementation\" expected"; break; + case 35: s = "\"modifies\" expected"; break; + case 36: s = "\"free\" expected"; break; + case 37: s = "\"requires\" expected"; break; + case 38: s = "\"ensures\" expected"; break; + case 39: s = "\"goto\" expected"; break; + case 40: s = "\"return\" expected"; break; + case 41: s = "\"if\" expected"; break; + case 42: s = "\"else\" expected"; break; + case 43: s = "\"while\" expected"; break; + case 44: s = "\"invariant\" expected"; break; + case 45: s = "\"*\" expected"; break; + case 46: s = "\"break\" expected"; break; + case 47: s = "\"assert\" expected"; break; + case 48: s = "\"assume\" expected"; break; + case 49: s = "\"havoc\" expected"; break; + case 50: s = "\"yield\" expected"; break; + case 51: s = "\":=\" expected"; break; + case 52: s = "\"async\" expected"; break; + case 53: s = "\"call\" expected"; break; + case 54: s = "\"par\" expected"; break; + case 55: s = "\"|\" expected"; break; + case 56: s = "\"<==>\" expected"; break; + case 57: s = "\"\\u21d4\" expected"; break; + case 58: s = "\"==>\" expected"; break; + case 59: s = "\"\\u21d2\" expected"; break; + case 60: s = "\"<==\" expected"; break; + case 61: s = "\"\\u21d0\" expected"; break; + case 62: s = "\"&&\" expected"; break; + case 63: s = "\"\\u2227\" expected"; break; + case 64: s = "\"||\" expected"; break; + case 65: s = "\"\\u2228\" expected"; break; + case 66: s = "\"==\" expected"; break; + case 67: s = "\"<=\" expected"; break; + case 68: s = "\">=\" expected"; break; + case 69: s = "\"!=\" expected"; break; + case 70: s = "\"<:\" expected"; break; + case 71: s = "\"\\u2260\" expected"; break; + case 72: s = "\"\\u2264\" expected"; break; + case 73: s = "\"\\u2265\" expected"; break; + case 74: s = "\"++\" expected"; break; + case 75: s = "\"+\" expected"; break; + case 76: s = "\"-\" expected"; break; + case 77: s = "\"div\" expected"; break; + case 78: s = "\"mod\" expected"; break; + case 79: s = "\"/\" expected"; break; + case 80: s = "\"**\" expected"; break; + case 81: s = "\"!\" expected"; break; + case 82: s = "\"\\u00ac\" expected"; break; + case 83: s = "\"false\" expected"; break; + case 84: s = "\"true\" expected"; break; + case 85: s = "\"old\" expected"; break; + case 86: s = "\"|{\" expected"; break; + case 87: s = "\"}|\" expected"; break; + case 88: s = "\"then\" expected"; break; + case 89: s = "\"forall\" expected"; break; + case 90: s = "\"\\u2200\" expected"; break; + case 91: s = "\"exists\" expected"; break; + case 92: s = "\"\\u2203\" expected"; break; + case 93: s = "\"lambda\" expected"; break; + case 94: s = "\"\\u03bb\" expected"; break; + case 95: s = "\"::\" expected"; break; + case 96: s = "\"\\u2022\" expected"; break; + case 97: s = "??? expected"; break; case 98: s = "invalid Function"; break; - case 99: s = "invalid Procedure"; break; - case 100: s = "invalid Type"; break; - case 101: s = "invalid TypeAtom"; break; - case 102: s = "invalid TypeArgs"; break; - case 103: s = "invalid Spec"; break; - case 104: s = "invalid SpecPrePost"; break; - case 105: s = "invalid LabelOrCmd"; break; - case 106: s = "invalid StructuredCmd"; break; - case 107: s = "invalid TransferCmd"; break; - case 108: s = "invalid IfCmd"; break; - case 109: s = "invalid Guard"; break; - case 110: s = "invalid LabelOrAssign"; break; - case 111: s = "invalid CallParams"; break; - case 112: s = "invalid EquivOp"; break; - case 113: s = "invalid ImpliesOp"; break; - case 114: s = "invalid ExpliesOp"; break; - case 115: s = "invalid AndOp"; break; - case 116: s = "invalid OrOp"; break; - case 117: s = "invalid RelOp"; break; - case 118: s = "invalid AddOp"; break; - case 119: s = "invalid MulOp"; break; - case 120: s = "invalid UnaryExpression"; break; - case 121: s = "invalid NegOp"; break; - case 122: s = "invalid CoercionExpression"; break; - case 123: s = "invalid AtomExpression"; break; + case 99: s = "invalid Function"; break; + case 100: s = "invalid Procedure"; break; + case 101: s = "invalid Type"; break; + case 102: s = "invalid TypeAtom"; break; + case 103: s = "invalid TypeArgs"; break; + case 104: s = "invalid Spec"; break; + case 105: s = "invalid SpecPrePost"; break; + case 106: s = "invalid LabelOrCmd"; break; + case 107: s = "invalid StructuredCmd"; break; + case 108: s = "invalid TransferCmd"; break; + case 109: s = "invalid IfCmd"; break; + case 110: s = "invalid Guard"; break; + case 111: s = "invalid LabelOrAssign"; break; + case 112: s = "invalid CallParams"; break; + case 113: s = "invalid EquivOp"; break; + case 114: s = "invalid ImpliesOp"; break; + case 115: s = "invalid ExpliesOp"; break; + case 116: s = "invalid AndOp"; break; + case 117: s = "invalid OrOp"; break; + case 118: s = "invalid RelOp"; break; + case 119: s = "invalid AddOp"; break; + case 120: s = "invalid MulOp"; break; + case 121: s = "invalid UnaryExpression"; break; + case 122: s = "invalid NegOp"; break; + case 123: s = "invalid CoercionExpression"; break; case 124: s = "invalid AtomExpression"; break; case 125: s = "invalid AtomExpression"; break; - case 126: s = "invalid Dec"; break; - case 127: s = "invalid Forall"; break; - case 128: s = "invalid QuantifierBody"; break; - case 129: s = "invalid Exists"; break; - case 130: s = "invalid Lambda"; break; - case 131: s = "invalid SpecBlock"; break; - case 132: s = "invalid AttributeOrTrigger"; break; - case 133: s = "invalid AttributeParameter"; break; - case 134: s = "invalid QSep"; break; + case 126: s = "invalid AtomExpression"; break; + case 127: s = "invalid Dec"; break; + case 128: s = "invalid Forall"; break; + case 129: s = "invalid QuantifierBody"; break; + case 130: s = "invalid Exists"; break; + case 131: s = "invalid Lambda"; break; + case 132: s = "invalid SpecBlock"; break; + case 133: s = "invalid AttributeOrTrigger"; break; + case 134: s = "invalid AttributeParameter"; break; + case 135: s = "invalid QSep"; break; default: s = "error " + n; break; } diff --git a/Source/Core/Scanner.cs b/Source/Core/Scanner.cs index e068fc4b..1185963f 100644 --- a/Source/Core/Scanner.cs +++ b/Source/Core/Scanner.cs @@ -211,8 +211,8 @@ public class UTF8Buffer: Buffer { public class Scanner { const char EOL = '\n'; const int eofSym = 0; /* pdt */ - const int maxT = 96; - const int noSym = 96; + const int maxT = 97; + const int noSym = 97; [ContractInvariantMethod] @@ -267,41 +267,41 @@ public class Scanner { for (int i = 65; i <= 90; ++i) start[i] = 2; for (int i = 94; i <= 122; ++i) start[i] = 2; for (int i = 126; i <= 126; ++i) start[i] = 2; - for (int i = 48; i <= 57; ++i) start[i] = 16; + for (int i = 48; i <= 57; ++i) start[i] = 19; for (int i = 34; i <= 34; ++i) start[i] = 6; start[92] = 1; - start[59] = 19; - start[40] = 20; - start[41] = 21; - start[58] = 55; - start[44] = 22; - start[91] = 23; - start[93] = 24; - start[60] = 56; - start[62] = 57; - start[123] = 25; - start[125] = 58; - start[61] = 59; - start[42] = 60; - start[124] = 61; - start[8660] = 28; - start[8658] = 30; - start[8656] = 31; - start[38] = 32; - start[8743] = 34; - start[8744] = 36; - start[33] = 62; - start[8800] = 40; - start[8804] = 41; - start[8805] = 42; - start[43] = 63; - start[45] = 44; - start[47] = 45; - start[172] = 47; - start[8704] = 50; - start[8707] = 51; - start[955] = 52; - start[8226] = 54; + start[59] = 24; + start[40] = 25; + start[41] = 26; + start[58] = 60; + start[44] = 27; + start[91] = 28; + start[93] = 29; + start[60] = 61; + start[62] = 62; + start[123] = 30; + start[125] = 63; + start[61] = 64; + start[42] = 65; + start[124] = 66; + start[8660] = 33; + start[8658] = 35; + start[8656] = 36; + start[38] = 37; + start[8743] = 39; + start[8744] = 41; + start[33] = 67; + start[8800] = 45; + start[8804] = 46; + start[8805] = 47; + start[43] = 68; + start[45] = 49; + start[47] = 50; + start[172] = 52; + start[8704] = 55; + start[8707] = 56; + start[955] = 57; + start[8226] = 59; start[Buffer.EOF] = -1; } @@ -503,48 +503,48 @@ public class Scanner { void CheckLiteral() { switch (t.val) { - case "var": t.kind = 7; break; - case "where": t.kind = 13; break; - case "int": t.kind = 14; break; - case "real": t.kind = 15; break; - case "bool": t.kind = 16; break; - case "const": t.kind = 21; break; - case "unique": t.kind = 22; break; - case "extends": t.kind = 23; break; - case "complete": t.kind = 24; break; - case "function": t.kind = 25; break; - case "returns": t.kind = 26; break; - case "axiom": t.kind = 29; break; - case "type": t.kind = 30; break; - case "procedure": t.kind = 32; break; - case "implementation": t.kind = 33; break; - case "modifies": t.kind = 34; break; - case "free": t.kind = 35; break; - case "requires": t.kind = 36; break; - case "ensures": t.kind = 37; break; - case "goto": t.kind = 38; break; - case "return": t.kind = 39; break; - case "if": t.kind = 40; break; - case "else": t.kind = 41; break; - case "while": t.kind = 42; break; - case "invariant": t.kind = 43; break; - case "break": t.kind = 45; break; - case "assert": t.kind = 46; break; - case "assume": t.kind = 47; break; - case "havoc": t.kind = 48; break; - case "yield": t.kind = 49; break; - case "async": t.kind = 51; break; - case "call": t.kind = 52; break; - case "par": t.kind = 53; break; - case "div": t.kind = 76; break; - case "mod": t.kind = 77; break; - case "false": t.kind = 82; break; - case "true": t.kind = 83; break; - case "old": t.kind = 84; break; - case "then": t.kind = 87; break; - case "forall": t.kind = 88; break; - case "exists": t.kind = 90; break; - case "lambda": t.kind = 92; break; + case "var": t.kind = 8; break; + case "where": t.kind = 14; break; + case "int": t.kind = 15; break; + case "real": t.kind = 16; break; + case "bool": t.kind = 17; break; + case "const": t.kind = 22; break; + case "unique": t.kind = 23; break; + case "extends": t.kind = 24; break; + case "complete": t.kind = 25; break; + case "function": t.kind = 26; break; + case "returns": t.kind = 27; break; + case "axiom": t.kind = 30; break; + case "type": t.kind = 31; break; + case "procedure": t.kind = 33; break; + case "implementation": t.kind = 34; break; + case "modifies": t.kind = 35; break; + case "free": t.kind = 36; break; + case "requires": t.kind = 37; break; + case "ensures": t.kind = 38; break; + case "goto": t.kind = 39; break; + case "return": t.kind = 40; break; + case "if": t.kind = 41; break; + case "else": t.kind = 42; break; + case "while": t.kind = 43; break; + case "invariant": t.kind = 44; break; + case "break": t.kind = 46; break; + case "assert": t.kind = 47; break; + case "assume": t.kind = 48; break; + case "havoc": t.kind = 49; break; + case "yield": t.kind = 50; break; + case "async": t.kind = 52; break; + case "call": t.kind = 53; break; + case "par": t.kind = 54; break; + case "div": t.kind = 77; break; + case "mod": t.kind = 78; break; + case "false": t.kind = 83; break; + case "true": t.kind = 84; break; + case "old": t.kind = 85; break; + case "then": t.kind = 88; break; + case "forall": t.kind = 89; break; + case "exists": t.kind = 91; break; + case "lambda": t.kind = 93; break; default: break; } } @@ -597,182 +597,201 @@ public class Scanner { case 6: if (ch == '"') {AddCh(); goto case 7;} else if (ch <= 9 || ch >= 11 && ch <= 12 || ch >= 14 && ch <= '!' || ch >= '#' && ch <= '[' || ch >= ']' && ch <= 65535) {AddCh(); goto case 6;} - else if (ch == 92) {AddCh(); goto case 17;} + else if (ch == 92) {AddCh(); goto case 20;} else {goto case 0;} case 7: {t.kind = 4; break;} case 8: - if (ch >= '0' && ch <= '9') {AddCh(); goto case 10;} - else if (ch == '-') {AddCh(); goto case 9;} + if (ch >= '0' && ch <= '9') {AddCh(); goto case 9;} else {goto case 0;} case 9: - if (ch >= '0' && ch <= '9') {AddCh(); goto case 10;} - else {goto case 0;} - case 10: recEnd = pos; recKind = 5; - if (ch >= '0' && ch <= '9') {AddCh(); goto case 10;} + if (ch >= '0' && ch <= '9') {AddCh(); goto case 9;} else {t.kind = 5; break;} - case 11: - if (ch >= '0' && ch <= '9') {AddCh(); goto case 12;} + case 10: + if (ch >= '0' && ch <= '9') {AddCh(); goto case 11;} else {goto case 0;} - case 12: + case 11: recEnd = pos; recKind = 6; - if (ch >= '0' && ch <= '9') {AddCh(); goto case 12;} - else if (ch == 'e') {AddCh(); goto case 13;} + if (ch >= '0' && ch <= '9') {AddCh(); goto case 11;} + else if (ch == 'e') {AddCh(); goto case 12;} else {t.kind = 6; break;} + case 12: + if (ch >= '0' && ch <= '9') {AddCh(); goto case 14;} + else if (ch == '-') {AddCh(); goto case 13;} + else {goto case 0;} case 13: - if (ch >= '0' && ch <= '9') {AddCh(); goto case 15;} - else if (ch == '-') {AddCh(); goto case 14;} + if (ch >= '0' && ch <= '9') {AddCh(); goto case 14;} else {goto case 0;} case 14: - if (ch >= '0' && ch <= '9') {AddCh(); goto case 15;} - else {goto case 0;} - case 15: recEnd = pos; recKind = 6; - if (ch >= '0' && ch <= '9') {AddCh(); goto case 15;} + if (ch >= '0' && ch <= '9') {AddCh(); goto case 14;} else {t.kind = 6; break;} + case 15: + if (ch >= '0' && ch <= '9') {AddCh(); goto case 16;} + else {goto case 0;} case 16: - recEnd = pos; recKind = 3; if (ch >= '0' && ch <= '9') {AddCh(); goto case 16;} + else if (ch == 'e') {AddCh(); goto case 17;} + else {goto case 0;} + case 17: + if (ch >= '0' && ch <= '9') {AddCh(); goto case 18;} + else {goto case 0;} + case 18: + recEnd = pos; recKind = 7; + if (ch >= '0' && ch <= '9') {AddCh(); goto case 18;} + else {t.kind = 7; break;} + case 19: + recEnd = pos; recKind = 3; + if (ch >= '0' && ch <= '9') {AddCh(); goto case 19;} else if (ch == 'b') {AddCh(); goto case 3;} - else if (ch == 'e') {AddCh(); goto case 8;} - else if (ch == '.') {AddCh(); goto case 11;} + else if (ch == 'e') {AddCh(); goto case 21;} + else if (ch == '.') {AddCh(); goto case 10;} else {t.kind = 3; break;} - case 17: - if (ch == '"') {AddCh(); goto case 18;} + case 20: + if (ch == '"') {AddCh(); goto case 22;} else if (ch <= 9 || ch >= 11 && ch <= 12 || ch >= 14 && ch <= '!' || ch >= '#' && ch <= '[' || ch >= ']' && ch <= 65535) {AddCh(); goto case 6;} - else if (ch == 92) {AddCh(); goto case 17;} + else if (ch == 92) {AddCh(); goto case 20;} else {goto case 0;} - case 18: + case 21: + if (ch >= '0' && ch <= '9') {AddCh(); goto case 23;} + else if (ch == '-') {AddCh(); goto case 8;} + else {goto case 0;} + case 22: recEnd = pos; recKind = 4; if (ch == '"') {AddCh(); goto case 7;} else if (ch <= 9 || ch >= 11 && ch <= 12 || ch >= 14 && ch <= '!' || ch >= '#' && ch <= '[' || ch >= ']' && ch <= 65535) {AddCh(); goto case 6;} - else if (ch == 92) {AddCh(); goto case 17;} + else if (ch == 92) {AddCh(); goto case 20;} else {t.kind = 4; break;} - case 19: - {t.kind = 8; break;} - case 20: - {t.kind = 9; break;} - case 21: - {t.kind = 10; break;} - case 22: - {t.kind = 12; break;} case 23: - {t.kind = 17; break;} + recEnd = pos; recKind = 5; + if (ch >= '0' && ch <= '9') {AddCh(); goto case 23;} + else if (ch == 'f') {AddCh(); goto case 15;} + else {t.kind = 5; break;} case 24: - {t.kind = 18; break;} + {t.kind = 9; break;} case 25: - {t.kind = 27; break;} + {t.kind = 10; break;} case 26: - {t.kind = 50; break;} + {t.kind = 11; break;} case 27: - {t.kind = 55; break;} + {t.kind = 13; break;} case 28: - {t.kind = 56; break;} + {t.kind = 18; break;} case 29: - {t.kind = 57; break;} + {t.kind = 19; break;} case 30: - {t.kind = 58; break;} + {t.kind = 28; break;} case 31: - {t.kind = 60; break;} + {t.kind = 51; break;} case 32: - if (ch == '&') {AddCh(); goto case 33;} - else {goto case 0;} + {t.kind = 56; break;} case 33: - {t.kind = 61; break;} + {t.kind = 57; break;} case 34: - {t.kind = 62; break;} + {t.kind = 58; break;} case 35: - {t.kind = 63; break;} + {t.kind = 59; break;} case 36: - {t.kind = 64; break;} + {t.kind = 61; break;} case 37: - {t.kind = 67; break;} + if (ch == '&') {AddCh(); goto case 38;} + else {goto case 0;} case 38: - {t.kind = 68; break;} + {t.kind = 62; break;} case 39: - {t.kind = 69; break;} + {t.kind = 63; break;} case 40: - {t.kind = 70; break;} + {t.kind = 64; break;} case 41: - {t.kind = 71; break;} + {t.kind = 65; break;} case 42: - {t.kind = 72; break;} + {t.kind = 68; break;} case 43: - {t.kind = 73; break;} + {t.kind = 69; break;} case 44: - {t.kind = 75; break;} + {t.kind = 70; break;} case 45: - {t.kind = 78; break;} + {t.kind = 71; break;} case 46: - {t.kind = 79; break;} + {t.kind = 72; break;} case 47: - {t.kind = 81; break;} + {t.kind = 73; break;} case 48: - {t.kind = 85; break;} + {t.kind = 74; break;} case 49: - {t.kind = 86; break;} + {t.kind = 76; break;} case 50: - {t.kind = 89; break;} + {t.kind = 79; break;} case 51: - {t.kind = 91; break;} + {t.kind = 80; break;} case 52: - {t.kind = 93; break;} + {t.kind = 82; break;} case 53: - {t.kind = 94; break;} + {t.kind = 86; break;} case 54: - {t.kind = 95; break;} + {t.kind = 87; break;} case 55: - recEnd = pos; recKind = 11; - if (ch == '=') {AddCh(); goto case 26;} - else if (ch == ':') {AddCh(); goto case 53;} - else {t.kind = 11; break;} + {t.kind = 90; break;} case 56: - recEnd = pos; recKind = 19; - if (ch == '=') {AddCh(); goto case 64;} - else if (ch == ':') {AddCh(); goto case 39;} - else {t.kind = 19; break;} + {t.kind = 92; break;} case 57: - recEnd = pos; recKind = 20; - if (ch == '=') {AddCh(); goto case 37;} - else {t.kind = 20; break;} + {t.kind = 94; break;} case 58: - recEnd = pos; recKind = 28; - if (ch == '|') {AddCh(); goto case 49;} - else {t.kind = 28; break;} + {t.kind = 95; break;} case 59: - recEnd = pos; recKind = 31; - if (ch == '=') {AddCh(); goto case 65;} - else {t.kind = 31; break;} + {t.kind = 96; break;} case 60: - recEnd = pos; recKind = 44; - if (ch == '*') {AddCh(); goto case 46;} - else {t.kind = 44; break;} + recEnd = pos; recKind = 12; + if (ch == '=') {AddCh(); goto case 31;} + else if (ch == ':') {AddCh(); goto case 58;} + else {t.kind = 12; break;} case 61: - recEnd = pos; recKind = 54; - if (ch == '|') {AddCh(); goto case 35;} - else if (ch == '{') {AddCh(); goto case 48;} - else {t.kind = 54; break;} + recEnd = pos; recKind = 20; + if (ch == '=') {AddCh(); goto case 69;} + else if (ch == ':') {AddCh(); goto case 44;} + else {t.kind = 20; break;} case 62: - recEnd = pos; recKind = 80; - if (ch == '=') {AddCh(); goto case 38;} - else {t.kind = 80; break;} + recEnd = pos; recKind = 21; + if (ch == '=') {AddCh(); goto case 42;} + else {t.kind = 21; break;} case 63: - recEnd = pos; recKind = 74; - if (ch == '+') {AddCh(); goto case 43;} - else {t.kind = 74; break;} + recEnd = pos; recKind = 29; + if (ch == '|') {AddCh(); goto case 54;} + else {t.kind = 29; break;} case 64: - recEnd = pos; recKind = 66; - if (ch == '=') {AddCh(); goto case 66;} - else {t.kind = 66; break;} + recEnd = pos; recKind = 32; + if (ch == '=') {AddCh(); goto case 70;} + else {t.kind = 32; break;} case 65: - recEnd = pos; recKind = 65; - if (ch == '>') {AddCh(); goto case 29;} - else {t.kind = 65; break;} + recEnd = pos; recKind = 45; + if (ch == '*') {AddCh(); goto case 51;} + else {t.kind = 45; break;} case 66: - recEnd = pos; recKind = 59; - if (ch == '>') {AddCh(); goto case 27;} - else {t.kind = 59; break;} + recEnd = pos; recKind = 55; + if (ch == '|') {AddCh(); goto case 40;} + else if (ch == '{') {AddCh(); goto case 53;} + else {t.kind = 55; break;} + case 67: + recEnd = pos; recKind = 81; + if (ch == '=') {AddCh(); goto case 43;} + else {t.kind = 81; break;} + case 68: + recEnd = pos; recKind = 75; + if (ch == '+') {AddCh(); goto case 48;} + else {t.kind = 75; break;} + case 69: + recEnd = pos; recKind = 67; + if (ch == '=') {AddCh(); goto case 71;} + else {t.kind = 67; break;} + case 70: + recEnd = pos; recKind = 66; + if (ch == '>') {AddCh(); goto case 34;} + else {t.kind = 66; break;} + case 71: + recEnd = pos; recKind = 60; + if (ch == '>') {AddCh(); goto case 32;} + else {t.kind = 60; break;} } t.val = new String(tval, 0, tlen); diff --git a/Test/floats/float0.bpl b/Test/floats/float0.bpl index 1a642835..d7faa4b0 100644 --- a/Test/floats/float0.bpl +++ b/Test/floats/float0.bpl @@ -4,11 +4,11 @@ procedure foo(x : real) returns (r : float8e24) { r := 15; // Error r := 15.0; // Error - r := fp(false, 1bv8, 0bv22); // Error - r := fp<8, 23>(1bv31); // Error + r := 0e1f22e8; // Error + r := 1e0f23e8; // Error r := x; // Error - r := fp<8, 23>(1bv31) + fp<8, 23>(1bv31); // Error - r := fp<8, 24>(1bv32) + fp<8, 23>(1bv31); // Error + r := 1e0f23e8 + 1e0f23e8; // Error + r := 1e0f24e8 + 1e0f23e8; // Error return; } \ No newline at end of file diff --git a/Test/floats/float1.bpl b/Test/floats/float1.bpl index 9ed62579..2b901c94 100644 --- a/Test/floats/float1.bpl +++ b/Test/floats/float1.bpl @@ -1,13 +1,13 @@ -// RUN: %boogie -proverWarnings:1 "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -procedure foo(x : float<8, 24>) returns (r : float<8, 24>) -{ - r := fp(false, 1bv8, 0bv23); - r := fp<8, 24>(1bv32); - r := x; - r := x + fp<8, 24>(1bv32); - r := fp<8, 24>(1bv32) + fp<8, 24>(1bv32); - assert(r == fp<8, 24>(2bv32)); - - return; +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure foo(x : float24e8) returns (r : float24e8) +{ + r := 0e1f24e8; + r := 1e0f24e8; + r := x; + r := x + 1e0f24e8; + r := 0e0f24e8 + 0e0f24e8; + assert(r == 0e1f24e8); + + return; } \ No newline at end of file -- cgit v1.2.3 From 86c78db45fad37209663bf87547a50a880760051 Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Tue, 19 Jul 2016 16:39:54 -0600 Subject: fixed an issue with parsing floating points --- Source/Core/BoogiePL.atg | 12 +- Source/Core/Parser.cs | 5 +- Source/Core/Scanner.cs | 363 ++++++++++++++++++++++++++++++----------------- Test/floats/float3.bpl | 4 +- Test/floats/float4.bpl | 3 +- 5 files changed, 249 insertions(+), 138 deletions(-) (limited to 'Source/Core/BoogiePL.atg') diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index 31823110..f74f8bff 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -145,7 +145,11 @@ TOKENS decimal = digit {digit} 'e' [ '-' ] digit {digit} . dec_float = digit {digit} '.' digit {digit} [ 'e' [ '-' ] digit {digit} ] . - float = digit {digit} 'e' digit {digit} 'f' digit {digit} 'e' digit {digit} . + float = [ '-' ] digit {digit} 'e' [ '-' ] digit {digit} 'f' digit {digit} 'e' digit {digit} + | '0' 'N' 'a' 'N' digit {digit} 'e' digit {digit} + | '0' 'n' 'a' 'n' digit {digit} 'e' digit {digit} + | '0' '+' 'o' 'o' digit {digit} 'e' digit {digit} + | '0' '-' 'o' 'o' digit {digit} 'e' digit {digit} . COMMENTS FROM "/*" TO "*/" NESTED COMMENTS FROM "//" TO lf @@ -1292,7 +1296,7 @@ AtomExpression Expression ")" (. e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToReal), new List{ e }); .) - | "(" ( Expression (. if (e is BvBounds) + | "(" ( Expression (. if (e is BvBounds) this.SemErr("parentheses around bitvector bounds " + "are not allowed"); .) | Forall (. x = t; .) @@ -1518,8 +1522,8 @@ Float ) (. try { n = BigFloat.FromString(s); - } catch (FormatException) { - this.SemErr("incorrectly formatted number"); + } catch (FormatException e) { + this.SemErr("incorrectly formatted floating point, " + e.Message); n = BigFloat.ZERO; } .) diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index a5e2921e..c91de177 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -133,7 +133,8 @@ private class BvBounds : Expr { Contract.Assert(false);throw new cce.UnreachableException(); } public override void ComputeFreeVariables(GSet/*!*/ freeVars) { Contract.Assert(false);throw new cce.UnreachableException(); } - public override int ComputeHashCode() { + public override int ComputeHashCode() + { return base.GetHashCode(); } } @@ -1866,7 +1867,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { try { n = BigFloat.FromString(s); } catch (FormatException e) { - this.SemErr("incorrectly formatted floating point: " + e.Message); + this.SemErr("incorrectly formatted floating point, " + e.Message); n = BigFloat.ZERO; } diff --git a/Source/Core/Scanner.cs b/Source/Core/Scanner.cs index 1185963f..46a3c419 100644 --- a/Source/Core/Scanner.cs +++ b/Source/Core/Scanner.cs @@ -267,41 +267,42 @@ public class Scanner { for (int i = 65; i <= 90; ++i) start[i] = 2; for (int i = 94; i <= 122; ++i) start[i] = 2; for (int i = 126; i <= 126; ++i) start[i] = 2; - for (int i = 48; i <= 57; ++i) start[i] = 19; + for (int i = 49; i <= 57; ++i) start[i] = 45; for (int i = 34; i <= 34; ++i) start[i] = 6; start[92] = 1; - start[59] = 24; - start[40] = 25; - start[41] = 26; - start[58] = 60; - start[44] = 27; - start[91] = 28; - start[93] = 29; - start[60] = 61; - start[62] = 62; - start[123] = 30; - start[125] = 63; - start[61] = 64; - start[42] = 65; - start[124] = 66; - start[8660] = 33; - start[8658] = 35; - start[8656] = 36; - start[38] = 37; - start[8743] = 39; - start[8744] = 41; - start[33] = 67; - start[8800] = 45; - start[8804] = 46; - start[8805] = 47; - start[43] = 68; - start[45] = 49; - start[47] = 50; - start[172] = 52; - start[8704] = 55; - start[8707] = 56; - start[955] = 57; - start[8226] = 59; + start[45] = 87; + start[48] = 46; + start[59] = 52; + start[40] = 53; + start[41] = 54; + start[58] = 88; + start[44] = 55; + start[91] = 56; + start[93] = 57; + start[60] = 89; + start[62] = 90; + start[123] = 58; + start[125] = 91; + start[61] = 92; + start[42] = 93; + start[124] = 94; + start[8660] = 61; + start[8658] = 63; + start[8656] = 64; + start[38] = 65; + start[8743] = 67; + start[8744] = 69; + start[33] = 95; + start[8800] = 73; + start[8804] = 74; + start[8805] = 75; + start[43] = 96; + start[47] = 77; + start[172] = 79; + start[8704] = 82; + start[8707] = 83; + start[955] = 84; + start[8226] = 86; start[Buffer.EOF] = -1; } @@ -597,7 +598,7 @@ public class Scanner { case 6: if (ch == '"') {AddCh(); goto case 7;} else if (ch <= 9 || ch >= 11 && ch <= 12 || ch >= 14 && ch <= '!' || ch >= '#' && ch <= '[' || ch >= ']' && ch <= 65535) {AddCh(); goto case 6;} - else if (ch == 92) {AddCh(); goto case 20;} + else if (ch == 92) {AddCh(); goto case 47;} else {goto case 0;} case 7: {t.kind = 4; break;} @@ -605,192 +606,296 @@ public class Scanner { if (ch >= '0' && ch <= '9') {AddCh(); goto case 9;} else {goto case 0;} case 9: - recEnd = pos; recKind = 5; + recEnd = pos; recKind = 6; if (ch >= '0' && ch <= '9') {AddCh(); goto case 9;} - else {t.kind = 5; break;} + else if (ch == 'e') {AddCh(); goto case 10;} + else {t.kind = 6; break;} case 10: - if (ch >= '0' && ch <= '9') {AddCh(); goto case 11;} + if (ch >= '0' && ch <= '9') {AddCh(); goto case 12;} + else if (ch == '-') {AddCh(); goto case 11;} else {goto case 0;} case 11: + if (ch >= '0' && ch <= '9') {AddCh(); goto case 12;} + else {goto case 0;} + case 12: recEnd = pos; recKind = 6; - if (ch >= '0' && ch <= '9') {AddCh(); goto case 11;} - else if (ch == 'e') {AddCh(); goto case 12;} + if (ch >= '0' && ch <= '9') {AddCh(); goto case 12;} else {t.kind = 6; break;} - case 12: - if (ch >= '0' && ch <= '9') {AddCh(); goto case 14;} - else if (ch == '-') {AddCh(); goto case 13;} - else {goto case 0;} case 13: - if (ch >= '0' && ch <= '9') {AddCh(); goto case 14;} + if (ch >= '0' && ch <= '9') {AddCh(); goto case 13;} + else if (ch == 'e') {AddCh(); goto case 14;} else {goto case 0;} case 14: - recEnd = pos; recKind = 6; - if (ch >= '0' && ch <= '9') {AddCh(); goto case 14;} - else {t.kind = 6; break;} + if (ch >= '0' && ch <= '9') {AddCh(); goto case 16;} + else if (ch == '-') {AddCh(); goto case 15;} + else {goto case 0;} case 15: if (ch >= '0' && ch <= '9') {AddCh(); goto case 16;} else {goto case 0;} case 16: if (ch >= '0' && ch <= '9') {AddCh(); goto case 16;} - else if (ch == 'e') {AddCh(); goto case 17;} + else if (ch == 'f') {AddCh(); goto case 17;} else {goto case 0;} case 17: if (ch >= '0' && ch <= '9') {AddCh(); goto case 18;} else {goto case 0;} case 18: - recEnd = pos; recKind = 7; if (ch >= '0' && ch <= '9') {AddCh(); goto case 18;} - else {t.kind = 7; break;} + else if (ch == 'e') {AddCh(); goto case 19;} + else {goto case 0;} case 19: + if (ch >= '0' && ch <= '9') {AddCh(); goto case 20;} + else {goto case 0;} + case 20: + recEnd = pos; recKind = 7; + if (ch >= '0' && ch <= '9') {AddCh(); goto case 20;} + else {t.kind = 7; break;} + case 21: + if (ch == 'a') {AddCh(); goto case 22;} + else {goto case 0;} + case 22: + if (ch == 'N') {AddCh(); goto case 23;} + else {goto case 0;} + case 23: + if (ch >= '0' && ch <= '9') {AddCh(); goto case 24;} + else {goto case 0;} + case 24: + if (ch >= '0' && ch <= '9') {AddCh(); goto case 24;} + else if (ch == 'e') {AddCh(); goto case 25;} + else {goto case 0;} + case 25: + if (ch >= '0' && ch <= '9') {AddCh(); goto case 26;} + else {goto case 0;} + case 26: + recEnd = pos; recKind = 7; + if (ch >= '0' && ch <= '9') {AddCh(); goto case 26;} + else {t.kind = 7; break;} + case 27: + if (ch == 'a') {AddCh(); goto case 28;} + else {goto case 0;} + case 28: + if (ch == 'n') {AddCh(); goto case 29;} + else {goto case 0;} + case 29: + if (ch >= '0' && ch <= '9') {AddCh(); goto case 30;} + else {goto case 0;} + case 30: + if (ch >= '0' && ch <= '9') {AddCh(); goto case 30;} + else if (ch == 'e') {AddCh(); goto case 31;} + else {goto case 0;} + case 31: + if (ch >= '0' && ch <= '9') {AddCh(); goto case 32;} + else {goto case 0;} + case 32: + recEnd = pos; recKind = 7; + if (ch >= '0' && ch <= '9') {AddCh(); goto case 32;} + else {t.kind = 7; break;} + case 33: + if (ch == 'o') {AddCh(); goto case 34;} + else {goto case 0;} + case 34: + if (ch == 'o') {AddCh(); goto case 35;} + else {goto case 0;} + case 35: + if (ch >= '0' && ch <= '9') {AddCh(); goto case 36;} + else {goto case 0;} + case 36: + if (ch >= '0' && ch <= '9') {AddCh(); goto case 36;} + else if (ch == 'e') {AddCh(); goto case 37;} + else {goto case 0;} + case 37: + if (ch >= '0' && ch <= '9') {AddCh(); goto case 38;} + else {goto case 0;} + case 38: + recEnd = pos; recKind = 7; + if (ch >= '0' && ch <= '9') {AddCh(); goto case 38;} + else {t.kind = 7; break;} + case 39: + if (ch == 'o') {AddCh(); goto case 40;} + else {goto case 0;} + case 40: + if (ch == 'o') {AddCh(); goto case 41;} + else {goto case 0;} + case 41: + if (ch >= '0' && ch <= '9') {AddCh(); goto case 42;} + else {goto case 0;} + case 42: + if (ch >= '0' && ch <= '9') {AddCh(); goto case 42;} + else if (ch == 'e') {AddCh(); goto case 43;} + else {goto case 0;} + case 43: + if (ch >= '0' && ch <= '9') {AddCh(); goto case 44;} + else {goto case 0;} + case 44: + recEnd = pos; recKind = 7; + if (ch >= '0' && ch <= '9') {AddCh(); goto case 44;} + else {t.kind = 7; break;} + case 45: recEnd = pos; recKind = 3; - if (ch >= '0' && ch <= '9') {AddCh(); goto case 19;} + if (ch >= '0' && ch <= '9') {AddCh(); goto case 45;} else if (ch == 'b') {AddCh(); goto case 3;} - else if (ch == 'e') {AddCh(); goto case 21;} - else if (ch == '.') {AddCh(); goto case 10;} + else if (ch == 'e') {AddCh(); goto case 48;} + else if (ch == '.') {AddCh(); goto case 8;} else {t.kind = 3; break;} - case 20: - if (ch == '"') {AddCh(); goto case 22;} + case 46: + recEnd = pos; recKind = 3; + if (ch >= '0' && ch <= '9') {AddCh(); goto case 45;} + else if (ch == 'b') {AddCh(); goto case 3;} + else if (ch == 'e') {AddCh(); goto case 48;} + else if (ch == '.') {AddCh(); goto case 8;} + else if (ch == 'N') {AddCh(); goto case 21;} + else if (ch == 'n') {AddCh(); goto case 27;} + else if (ch == '+') {AddCh(); goto case 33;} + else if (ch == '-') {AddCh(); goto case 39;} + else {t.kind = 3; break;} + case 47: + if (ch == '"') {AddCh(); goto case 49;} else if (ch <= 9 || ch >= 11 && ch <= 12 || ch >= 14 && ch <= '!' || ch >= '#' && ch <= '[' || ch >= ']' && ch <= 65535) {AddCh(); goto case 6;} - else if (ch == 92) {AddCh(); goto case 20;} + else if (ch == 92) {AddCh(); goto case 47;} else {goto case 0;} - case 21: - if (ch >= '0' && ch <= '9') {AddCh(); goto case 23;} - else if (ch == '-') {AddCh(); goto case 8;} + case 48: + if (ch >= '0' && ch <= '9') {AddCh(); goto case 50;} + else if (ch == '-') {AddCh(); goto case 51;} else {goto case 0;} - case 22: + case 49: recEnd = pos; recKind = 4; if (ch == '"') {AddCh(); goto case 7;} else if (ch <= 9 || ch >= 11 && ch <= 12 || ch >= 14 && ch <= '!' || ch >= '#' && ch <= '[' || ch >= ']' && ch <= 65535) {AddCh(); goto case 6;} - else if (ch == 92) {AddCh(); goto case 20;} + else if (ch == 92) {AddCh(); goto case 47;} else {t.kind = 4; break;} - case 23: + case 50: recEnd = pos; recKind = 5; - if (ch >= '0' && ch <= '9') {AddCh(); goto case 23;} - else if (ch == 'f') {AddCh(); goto case 15;} + if (ch >= '0' && ch <= '9') {AddCh(); goto case 50;} + else if (ch == 'f') {AddCh(); goto case 17;} else {t.kind = 5; break;} - case 24: + case 51: + if (ch >= '0' && ch <= '9') {AddCh(); goto case 50;} + else {goto case 0;} + case 52: {t.kind = 9; break;} - case 25: + case 53: {t.kind = 10; break;} - case 26: + case 54: {t.kind = 11; break;} - case 27: + case 55: {t.kind = 13; break;} - case 28: + case 56: {t.kind = 18; break;} - case 29: + case 57: {t.kind = 19; break;} - case 30: + case 58: {t.kind = 28; break;} - case 31: + case 59: {t.kind = 51; break;} - case 32: + case 60: {t.kind = 56; break;} - case 33: + case 61: {t.kind = 57; break;} - case 34: + case 62: {t.kind = 58; break;} - case 35: + case 63: {t.kind = 59; break;} - case 36: + case 64: {t.kind = 61; break;} - case 37: - if (ch == '&') {AddCh(); goto case 38;} + case 65: + if (ch == '&') {AddCh(); goto case 66;} else {goto case 0;} - case 38: + case 66: {t.kind = 62; break;} - case 39: + case 67: {t.kind = 63; break;} - case 40: + case 68: {t.kind = 64; break;} - case 41: + case 69: {t.kind = 65; break;} - case 42: + case 70: {t.kind = 68; break;} - case 43: + case 71: {t.kind = 69; break;} - case 44: + case 72: {t.kind = 70; break;} - case 45: + case 73: {t.kind = 71; break;} - case 46: + case 74: {t.kind = 72; break;} - case 47: + case 75: {t.kind = 73; break;} - case 48: + case 76: {t.kind = 74; break;} - case 49: - {t.kind = 76; break;} - case 50: + case 77: {t.kind = 79; break;} - case 51: + case 78: {t.kind = 80; break;} - case 52: + case 79: {t.kind = 82; break;} - case 53: + case 80: {t.kind = 86; break;} - case 54: + case 81: {t.kind = 87; break;} - case 55: + case 82: {t.kind = 90; break;} - case 56: + case 83: {t.kind = 92; break;} - case 57: + case 84: {t.kind = 94; break;} - case 58: + case 85: {t.kind = 95; break;} - case 59: + case 86: {t.kind = 96; break;} - case 60: + case 87: + recEnd = pos; recKind = 76; + if (ch >= '0' && ch <= '9') {AddCh(); goto case 13;} + else {t.kind = 76; break;} + case 88: recEnd = pos; recKind = 12; - if (ch == '=') {AddCh(); goto case 31;} - else if (ch == ':') {AddCh(); goto case 58;} + if (ch == '=') {AddCh(); goto case 59;} + else if (ch == ':') {AddCh(); goto case 85;} else {t.kind = 12; break;} - case 61: + case 89: recEnd = pos; recKind = 20; - if (ch == '=') {AddCh(); goto case 69;} - else if (ch == ':') {AddCh(); goto case 44;} + if (ch == '=') {AddCh(); goto case 97;} + else if (ch == ':') {AddCh(); goto case 72;} else {t.kind = 20; break;} - case 62: + case 90: recEnd = pos; recKind = 21; - if (ch == '=') {AddCh(); goto case 42;} + if (ch == '=') {AddCh(); goto case 70;} else {t.kind = 21; break;} - case 63: + case 91: recEnd = pos; recKind = 29; - if (ch == '|') {AddCh(); goto case 54;} + if (ch == '|') {AddCh(); goto case 81;} else {t.kind = 29; break;} - case 64: + case 92: recEnd = pos; recKind = 32; - if (ch == '=') {AddCh(); goto case 70;} + if (ch == '=') {AddCh(); goto case 98;} else {t.kind = 32; break;} - case 65: + case 93: recEnd = pos; recKind = 45; - if (ch == '*') {AddCh(); goto case 51;} + if (ch == '*') {AddCh(); goto case 78;} else {t.kind = 45; break;} - case 66: + case 94: recEnd = pos; recKind = 55; - if (ch == '|') {AddCh(); goto case 40;} - else if (ch == '{') {AddCh(); goto case 53;} + if (ch == '|') {AddCh(); goto case 68;} + else if (ch == '{') {AddCh(); goto case 80;} else {t.kind = 55; break;} - case 67: + case 95: recEnd = pos; recKind = 81; - if (ch == '=') {AddCh(); goto case 43;} + if (ch == '=') {AddCh(); goto case 71;} else {t.kind = 81; break;} - case 68: + case 96: recEnd = pos; recKind = 75; - if (ch == '+') {AddCh(); goto case 48;} + if (ch == '+') {AddCh(); goto case 76;} else {t.kind = 75; break;} - case 69: + case 97: recEnd = pos; recKind = 67; - if (ch == '=') {AddCh(); goto case 71;} + if (ch == '=') {AddCh(); goto case 99;} else {t.kind = 67; break;} - case 70: + case 98: recEnd = pos; recKind = 66; - if (ch == '>') {AddCh(); goto case 34;} + if (ch == '>') {AddCh(); goto case 62;} else {t.kind = 66; break;} - case 71: + case 99: recEnd = pos; recKind = 60; - if (ch == '>') {AddCh(); goto case 32;} + if (ch == '>') {AddCh(); goto case 60;} else {t.kind = 60; break;} } diff --git a/Test/floats/float3.bpl b/Test/floats/float3.bpl index 31de7ca8..e4de8b3b 100644 --- a/Test/floats/float3.bpl +++ b/Test/floats/float3.bpl @@ -8,10 +8,10 @@ procedure main() returns () { z := x + y; z := x - y; z := x * y; - assume(y != 0e-128f24e8); + assume(y != 0e-127f24e8); z := x / y; - z := (0e0f24e8 + 0e0f24e8 + 0e-128f24e8); + z := (0e0f24e8 + 0e0f24e8 + 0e-127f24e8); assert(z == 0e1f24e8); z := 0e1f24e8 - 0e0f24e8; diff --git a/Test/floats/float4.bpl b/Test/floats/float4.bpl index a1608572..816d8446 100644 --- a/Test/floats/float4.bpl +++ b/Test/floats/float4.bpl @@ -1,10 +1,11 @@ // RUN: %boogie -proverWarnings:1 "%s" > "%t" // RUN: %diff "%s.expect" "%t" -procedure foo() returns (r : float32) { +procedure foo() returns (r : float8e24) { r := 0NaN8e24; r := 0nan8e24; r := 0+oo8e24; r := 0-oo8e24; + r := -5e-3f8e24; return; } \ No newline at end of file -- cgit v1.2.3