From 67c07706d2b4ee941954301a0c18abfcf253384c Mon Sep 17 00:00:00 2001 From: mikebarnett Date: Tue, 22 Jun 2010 17:58:58 +0000 Subject: Updated the frame files to work with the latest Coco/R. This entails *not* having them in this repository because of license issues. Instead, they must be downloaded from http://boogiepartners.codeplex.com/ and then copied into the appropriate directories. Lots of code changes to compensate for the new frame files. --- Source/Core/Absy.ssc | 15 +- Source/Core/AbsyCmd.ssc | 16 +- Source/Core/BoogiePL.atg | 244 +++++---- Source/Core/Core.sscproj | 4 + Source/Core/Makefile | 7 +- Source/Core/Parser.ssc | 1234 +++++++++++++++++++++++------------------- Source/Core/ParserHelper.ssc | 116 ++++ Source/Core/Scanner.ssc | 1095 ++++++++++++++++++++----------------- Source/Core/parser.frame | 103 ---- Source/Core/scanner.frame | 377 ------------- 10 files changed, 1536 insertions(+), 1675 deletions(-) create mode 100644 Source/Core/ParserHelper.ssc delete mode 100644 Source/Core/parser.frame delete mode 100644 Source/Core/scanner.frame (limited to 'Source/Core') diff --git a/Source/Core/Absy.ssc b/Source/Core/Absy.ssc index 6b4cae62..07723e4d 100644 --- a/Source/Core/Absy.ssc +++ b/Source/Core/Absy.ssc @@ -1680,17 +1680,26 @@ namespace Microsoft.Boogie VariableSeq! inParams, VariableSeq! outParams, VariableSeq! localVariables, [Captured] StmtList! structuredStmts) { - this(tok, name, typeParams, inParams, outParams, localVariables, structuredStmts, null); + this(tok, name, typeParams, inParams, outParams, localVariables, structuredStmts, null, new Errors()); } public Implementation(IToken! tok, string! name, TypeVariableSeq! typeParams, VariableSeq! inParams, VariableSeq! outParams, - VariableSeq! localVariables, [Captured] StmtList! structuredStmts, QKeyValue kv) + VariableSeq! localVariables, [Captured] StmtList! structuredStmts, + Errors! errorHandler) + { + this(tok, name, typeParams, inParams, outParams, localVariables, structuredStmts, null, errorHandler); + } + + public Implementation(IToken! tok, string! name, TypeVariableSeq! typeParams, + VariableSeq! inParams, VariableSeq! outParams, + VariableSeq! localVariables, [Captured] StmtList! structuredStmts, QKeyValue kv, + Errors! errorHandler) : base(tok, name, typeParams, inParams, outParams) { LocVars = localVariables; StructuredStmts = structuredStmts; - BigBlocksResolutionContext ctx = new BigBlocksResolutionContext(structuredStmts); + BigBlocksResolutionContext ctx = new BigBlocksResolutionContext(structuredStmts, errorHandler); Blocks = ctx.Blocks; BlockPredecessorsComputed = false; scc = null; diff --git a/Source/Core/AbsyCmd.ssc b/Source/Core/AbsyCmd.ssc index bf80116c..d682029e 100644 --- a/Source/Core/AbsyCmd.ssc +++ b/Source/Core/AbsyCmd.ssc @@ -202,9 +202,11 @@ namespace Microsoft.Boogie string! prefix = "anon"; int anon = 0; Set allLabels = new Set(); + Errors! errorHandler; - public BigBlocksResolutionContext(StmtList! stmtList) { + public BigBlocksResolutionContext(StmtList! stmtList, Errors! errorHandler) { this.stmtList = stmtList; + this.errorHandler = errorHandler; } public List! Blocks { @@ -212,7 +214,7 @@ namespace Microsoft.Boogie if (blocks == null) { blocks = new List(); - int startErrorCount = BoogiePL.Errors.count; + int startErrorCount = this.errorHandler.count; // Check that there are no goto's into the middle of a block, and no break statement to a non-enclosing loop. // Also, determine a good value for "prefix". CheckLegalLabels(stmtList, null, null); @@ -223,7 +225,7 @@ namespace Microsoft.Boogie // determine successor blocks RecordSuccessors(stmtList, null); - if (BoogiePL.Errors.count == startErrorCount) { + if (this.errorHandler.count == startErrorCount) { // generate blocks from the big blocks CreateBlocks(stmtList, null); } @@ -270,7 +272,7 @@ namespace Microsoft.Boogie } } if (!found) { - BoogiePL.Errors.SemErr(g.tok, "Error: goto label '" + lbl + "' is undefined or out of reach"); + this.errorHandler.SemErr(g.tok, "Error: goto label '" + lbl + "' is undefined or out of reach"); } } } @@ -299,7 +301,7 @@ namespace Microsoft.Boogie bcmd.BreakEnclosure = bb; } else { // the label of bb refers to the first statement of bb, which in which case is a simple statement, not an if/while statement - BoogiePL.Errors.SemErr(bcmd.tok, "Error: break label '" + bcmd.Label + "' must designate an enclosing statement"); + this.errorHandler.SemErr(bcmd.tok, "Error: break label '" + bcmd.Label + "' must designate an enclosing statement"); } found = true; // don't look any further, since we've found a matching label break; @@ -307,9 +309,9 @@ namespace Microsoft.Boogie } if (!found) { if (bcmd.Label == null) { - BoogiePL.Errors.SemErr(bcmd.tok, "Error: break statement is not inside a loop"); + this.errorHandler.SemErr(bcmd.tok, "Error: break statement is not inside a loop"); } else { - BoogiePL.Errors.SemErr(bcmd.tok, "Error: break label '" + bcmd.Label + "' must designate an enclosing statement"); + this.errorHandler.SemErr(bcmd.tok, "Error: break label '" + bcmd.Label + "' must designate an enclosing statement"); } } } diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index aded331b..896dc0e5 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -7,6 +7,8 @@ using PureCollections; using System.Collections; using System.Collections.Generic; +using System.IO; +using System.Text; using Microsoft.Boogie; using Microsoft.Basetypes; using Bpl = Microsoft.Boogie; @@ -33,22 +35,24 @@ static StructuredCmd! dummyStructuredCmd = new BreakCmd(Token.NoToken, null); ///the parsed program. /// public static int Parse (string! filename, out /*maybe null*/ Program program) /* throws System.IO.IOException */ { - using (System.IO.StreamReader reader = new System.IO.StreamReader(filename)) { - Buffer.Fill(reader); - Scanner.Init(filename); - return Parse(out program); - } -} -/// -///Returns the number of parsing errors encountered. If 0, "program" returns as -///the parsed program. -///Note: first initialize the Scanner. -/// -public static int Parse (out /*maybe null*/ Program program) { + + FileStream stream = new FileStream(filename, FileMode.Open, FileAccess.Read, FileShare.Read); +// Scanner scanner = new Scanner(stream); + + string s = ParserHelper.Fill(stream,new List()); + byte[]! buffer = (!) UTF8Encoding.Default.GetBytes(s); + MemoryStream ms = new MemoryStream(buffer,false); + Errors errors = new Errors(); + Scanner scanner = new Scanner(ms, errors, filename); + +/* + Scanner scanner = new Scanner(filename); +*/ + Parser parser = new Parser(scanner, errors); Pgm = new Program(); // reset the global variable - Parse(); - if (Errors.count == 0) + parser.Parse(); + if (parser.errors.count == 0) { program = Pgm; return 0; @@ -56,22 +60,50 @@ public static int Parse (out /*maybe null*/ Program program) { else { program = null; - return Errors.count; + return parser.errors.count; } +/* + using (System.IO.StreamReader reader = new System.IO.StreamReader(filename)) { + Buffer.Fill(reader); + Scanner.Init(filename); + return Parse(out program); + } +*/ } - +/// +///Returns the number of parsing errors encountered. If 0, "program" returns as +///the parsed program. +///Note: first initialize the Scanner. +/// +//public static int Parse (out /*maybe null*/ Program program) { +// Pgm = new Program(); // reset the global variable +// Parse(); +// if (Errors.count == 0) +// { +// program = Pgm; +// return 0; +// } +// else +// { +// program = null; +// return Errors.count; +// } +//} + +/* public static int ParseProposition (string! text, out Expr! expression) { Buffer.Fill(text); Scanner.Init(string.Format("\"{0}\"", text)); Errors.SynErr = new ErrorProc(SynErr); - t = new Token(); + la = new Token(); Get(); Proposition(out expression); return Errors.count; } +*/ // Class to represent the bounds of a bitvector expression t[a:b]. // Objects of this class only exist during parsing and are directly @@ -228,7 +260,7 @@ IdsTypeWhere [ "where" Expression (. if (allowWhereClauses) { wh = nne; } else { - SemErr("where clause not allowed here"); + this.SemErr("where clause not allowed here"); } .) ] @@ -267,8 +299,8 @@ TypeArgs TypeAtom = (. ty = dummyType; .) - ( "int" (. ty = new BasicType(token, SimpleType.Int); .) - | "bool" (. ty = new BasicType(token, SimpleType.Bool); .) + ( "int" (. ty = new BasicType(t, SimpleType.Int); .) + | "bool" (. ty = new BasicType(t, SimpleType.Bool); .) /* note: bitvectors are handled in UnresolvedTypeIdentifier */ | "(" @@ -285,7 +317,7 @@ MapType TypeVariableSeq! typeParameters = new TypeVariableSeq(); .) [ TypeParams (. tok = nnTok; .) ] - "[" (. if (tok == null) tok = token; .) + "[" (. if (tok == null) tok = t; .) [ Types ] "]" Type @@ -296,7 +328,7 @@ MapType TypeParams = (. TokenSeq! typeParamToks; .) - "<" (. tok = token; .) + "<" (. tok = t; .) Idents ">" (. @@ -321,7 +353,7 @@ Consts bool u = false; QKeyValue kv = null; bool ChildrenComplete = false; List Parents = null; .) - "const" (. y = token; .) + "const" (. y = t; .) { Attribute } [ "unique" (. u = true; .) ] @@ -349,7 +381,7 @@ Consts ";" . -OrderSpec Parents> +OrderSpec<.out bool ChildrenComplete, out List Parents.> = (. ChildrenComplete = false; Parents = null; bool u; @@ -401,7 +433,7 @@ Function (. if (retTyd == null) { // construct a dummy type for the case of syntax error - tyd = new TypedIdent(token, "", new BasicType(token, SimpleType.Int)); + tyd = new TypedIdent(t, "", new BasicType(t, SimpleType.Int)); } else { tyd = retTyd; } @@ -421,7 +453,7 @@ Function TypedIdent! curr = ((!)arguments[i]).TypedIdent; if (curr.Name == "") { if (prevType == null) { - SemErr(curr.tok, "the type of the last parameter is unspecified"); + this.errors.SemErr(curr.tok, "the type of the last parameter is unspecified"); break; } Type ty = curr.Type; @@ -430,7 +462,7 @@ Function curr.Name = ((!)(ty as UnresolvedTypeIdentifier)).Name; curr.Type = prevType; } else { - SemErr(curr.tok, "expecting an identifier as parameter name"); + this.errors.SemErr(curr.tok, "expecting an identifier as parameter name"); } } else { prevType = curr.Type; @@ -479,7 +511,7 @@ VarOrType ((!)(ty as UnresolvedTypeIdentifier)).Arguments.Length == 0) { varName = ((!)(ty as UnresolvedTypeIdentifier)).Name; } else { - SemErr("expected identifier before ':'"); + this.SemErr("expected identifier before ':'"); } .) Type @@ -492,12 +524,12 @@ Axiom = (. Expr! e; QKeyValue kv = null; .) "axiom" { Attribute } - (. IToken! x = token; .) + (. IToken! x = t; .) Proposition ";" (. m = new Axiom(x,e, null, kv); .) . /*------------------------------------------------------------------------*/ -UserDefinedTypes! ts> +UserDefinedTypes<.out List! ts.> = (. Declaration! decl; QKeyValue kv = null; ts = new List (); .) "type" { Attribute } @@ -552,7 +584,7 @@ Procedure (. // here we attach kv only to the Procedure, not its implementation impl = new Implementation(x, x.val, typeParams, - Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, null); + Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, null, this.errors); .) ) (. proc = new Procedure(x, x.val, typeParams, ins, outs, pre, mods, post, kv); .) @@ -571,7 +603,7 @@ Implementation "implementation" ProcSignature ImplBody - (. impl = new Implementation(x, x.val, typeParams, ins, outs, locals, stmtList, kv); .) + (. impl = new Implementation(x, x.val, typeParams, ins, outs, locals, stmtList, kv, this.errors); .) . @@ -602,14 +634,14 @@ Spec SpecPrePost = (. Expr! e; VariableSeq! locals; BlockSeq! blocks; Token tok = null; QKeyValue kv = null; .) - ( "requires" (. tok = token; .) + ( "requires" (. tok = t; .) { Attribute } (Proposition ";" (. pre.Add(new Requires(tok, free, e, null, kv)); .) | SpecBody ";" (. pre.Add(new Requires(tok, free, new BlockExpr(locals, blocks), null, kv)); .) ) - | "ensures" (. tok = token; .) + | "ensures" (. tok = t; .) { Attribute } (Proposition ";" (. post.Add(new Ensures(tok, free, e, null, kv)); .) | @@ -645,16 +677,16 @@ SpecBlock cs.Add(c); } else { assert label != null; - SemErr("SpecBlock's can only have one label"); + this.SemErr("SpecBlock's can only have one label"); } .) } - ( "goto" (. y = token; .) + ( "goto" (. y = t; .) Idents (. foreach (IToken! s in xs) { 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(token,e)); .) + (. b = new Block(x,x.val,cs,new ReturnExprCmd(t,e)); .) ) ";" . @@ -724,9 +756,9 @@ StmtList ) } "}" - (. IToken! endCurly = token; + (. IToken! endCurly = t; if (startToken == null && bigblocks.Count == 0) { - startToken = token; cs = new CmdSeq(); + startToken = t; cs = new CmdSeq(); } if (startToken != null) { assert cs != null; @@ -743,11 +775,11 @@ TransferCmd Token y; TokenSeq! xs; StringSeq ss = new StringSeq(); .) - ( "goto" (. y = token; .) + ( "goto" (. y = t; .) Idents (. foreach (IToken! s in xs) { ss.Add(s.val); } tc = new GotoCmd(y, ss); .) - | "return" (. tc = new ReturnCmd(token); .) + | "return" (. tc = new ReturnCmd(t); .) ) ";" . @@ -768,7 +800,7 @@ IfCmd IfCmd! elseIf; IfCmd elseIfOption = null; StmtList! els; StmtList elseOption = null; .) - "if" (. x = token; .) + "if" (. x = t; .) Guard "{" StmtList [ "else" @@ -786,9 +818,9 @@ WhileCmd List invariants = new List(); StmtList! body; .) - "while" (. x = token; .) + "while" (. x = t; .) Guard (. assume guard == null || Owner.None(guard); .) - { (. isFree = false; z = t/*lookahead token*/; .) + { (. isFree = false; z = la/*lookahead token*/; .) [ "free" (. isFree = true; .) ] "invariant" @@ -817,7 +849,7 @@ BreakCmd = (. IToken! x; IToken! y; string breakLabel = null; .) - "break" (. x = token; .) + "break" (. x = t; .) [ Ident (. breakLabel = y.val; .) ] ";" (. bcmd = new BreakCmd(x, breakLabel); .) . @@ -834,14 +866,14 @@ LabelOrCmd QKeyValue kv = null; .) ( LabelOrAssign - | "assert" (. x = token; .) + | "assert" (. x = t; .) { Attribute } Proposition (. c = new AssertCmd(x,e, kv); .) ";" - | "assume" (. x = token; .) + | "assume" (. x = t; .) Proposition (. c = new AssumeCmd(x,e); .) ";" - | "havoc" (. x = token; .) + | "havoc" (. x = t; .) Idents ";" (. ids = new IdentifierExprSeq(); foreach (IToken! y in xs) { ids.Add(new IdentifierExpr(y, y.val)); @@ -862,7 +894,7 @@ LabelOrAssign List! lhss; List! rhss; .) - Ident (. x = token; .) + Ident (. x = t; .) ( ":" (. c = null; label = x; .) | MapAssignIndexes (. lhss = new List (); @@ -871,7 +903,7 @@ LabelOrAssign Ident MapAssignIndexes (. lhss.Add(lhs); .) } - ":=" (. x = token; /* use location of := */ .) + ":=" (. x = t; /* use location of := */ .) Expression (. rhss = new List (); rhss.Add(e0); .) { "," @@ -890,7 +922,7 @@ MapAssignIndexes Expr! e0; .) { - "[" (. x = token; + "[" (. x = t; indexes = new List (); .) [ Expression (. indexes.Add(e0); .) @@ -913,7 +945,7 @@ CallCmd Expr en; List args; c = dummyCmd; .) - "call" (. x = token; .) + "call" (. x = t; .) { Attribute } ( Ident ( "(" @@ -1033,7 +1065,7 @@ Expressions Expression = (. IToken! x; Expr! e1; .) ImpliesExpression - { EquivOp (. x = token; .) + { EquivOp (. x = t; .) ImpliesExpression (. e0 = Expr.Binary(x, BinaryOperator.Opcode.Iff, e0, e1); .) } @@ -1046,19 +1078,19 @@ ImpliesExpression = (. IToken! x; Expr! e1; .) LogicalExpression [ - ImpliesOp (. x = token; .) + ImpliesOp (. x = t; .) /* recurse because implication is right-associative */ ImpliesExpression (. e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e0, e1); .) | ExpliesOp (. if (noExplies) - SemErr("illegal mixture of ==> and <==, use parentheses to disambiguate"); - x = token; .) + 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 = token; .) + ExpliesOp (. x = t; .) LogicalExpression (. e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e1, e0); .) } @@ -1072,17 +1104,17 @@ ExpliesOp = "<==" | '\u21d0'. LogicalExpression = (. IToken! x; Expr! e1; BinaryOperator.Opcode op; .) RelationalExpression - [ AndOp (. x = token; .) + [ AndOp (. x = t; .) RelationalExpression (. e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1); .) - { AndOp (. x = token; .) + { AndOp (. x = t; .) RelationalExpression (. e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1); .) } - | OrOp (. x = token; .) + | OrOp (. x = t; .) RelationalExpression (. e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1); .) - { OrOp (. x = token; .) + { OrOp (. x = t; .) RelationalExpression (. e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1); .) } @@ -1103,16 +1135,16 @@ RelationalExpression RelOp = (. x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; .) - ( "==" (. x = token; op=BinaryOperator.Opcode.Eq; .) - | "<" (. x = token; op=BinaryOperator.Opcode.Lt; .) - | ">" (. x = token; op=BinaryOperator.Opcode.Gt; .) - | "<=" (. x = token; op=BinaryOperator.Opcode.Le; .) - | ">=" (. x = token; op=BinaryOperator.Opcode.Ge; .) - | "!=" (. x = token; op=BinaryOperator.Opcode.Neq; .) - | "<:" (. x = token; op=BinaryOperator.Opcode.Subtype; .) - | '\u2260' (. x = token; op=BinaryOperator.Opcode.Neq; .) - | '\u2264' (. x = token; op=BinaryOperator.Opcode.Le; .) - | '\u2265' (. x = token; op=BinaryOperator.Opcode.Ge; .) + ( "==" (. 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; .) ) . @@ -1120,7 +1152,7 @@ RelOp BvTerm = (. IToken! x; Expr! e1; .) Term - { "++" (. x = token; .) + { "++" (. x = t; .) Term (. e0 = new BvConcatExpr(x, e0, e1); .) } . @@ -1137,8 +1169,8 @@ Term AddOp = (. x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; .) - ( "+" (. x = token; op=BinaryOperator.Opcode.Add; .) - | "-" (. x = token; op=BinaryOperator.Opcode.Sub; .) + ( "+" (. x = t; op=BinaryOperator.Opcode.Add; .) + | "-" (. x = t; op=BinaryOperator.Opcode.Sub; .) ) . @@ -1153,9 +1185,9 @@ Factor MulOp = (. x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; .) - ( "*" (. x = token; op=BinaryOperator.Opcode.Mul; .) - | "/" (. x = token; op=BinaryOperator.Opcode.Div; .) - | "%" (. x = token; op=BinaryOperator.Opcode.Mod; .) + ( "*" (. x = t; op=BinaryOperator.Opcode.Mul; .) + | "/" (. x = t; op=BinaryOperator.Opcode.Div; .) + | "%" (. x = t; op=BinaryOperator.Opcode.Mod; .) ) . @@ -1164,9 +1196,9 @@ UnaryExpression = (. IToken! x; e = dummyExpr; .) - ( "-" (. x = token; .) + ( "-" (. x = t; .) UnaryExpression (. e = Expr.Binary(x, BinaryOperator.Opcode.Sub, new LiteralExpr(x, BigNum.ZERO), e); .) - | NegOp (. x = token; .) + | NegOp (. x = t; .) UnaryExpression (. e = Expr.Unary(x, UnaryOperator.Opcode.Not, e); .) | CoercionExpression ) @@ -1189,14 +1221,14 @@ CoercionExpression BigNum bn; .) ArrayExpression - { ":" (. x = token; .) + { ":" (. 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) { - SemErr("arguments of extract need to be integer literals"); + 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); @@ -1214,7 +1246,7 @@ ArrayExpression ExprSeq! allArgs = dummyExprSeq; .) AtomExpression - { "[" (. x = token; allArgs = new ExprSeq (); + { "[" (. x = t; allArgs = new ExprSeq (); allArgs.Add(e); store = false; bvExtract = false; .) [ @@ -1226,13 +1258,13 @@ ArrayExpression .) { "," Expression (. if (bvExtract || e1 is BvBounds) - SemErr("bitvectors only have one dimension"); + this.SemErr("bitvectors only have one dimension"); allArgs.Add(e1); .) } [ ":=" Expression (. if (bvExtract || e1 is BvBounds) - SemErr("assignment to bitvectors is not possible"); + this.SemErr("assignment to bitvectors is not possible"); allArgs.Add(e1); store = true; .) ] @@ -1262,10 +1294,10 @@ AtomExpression QKeyValue kv; e = dummyExpr; .) - ( "false" (. e = new LiteralExpr(token, false); .) - | "true" (. e = new LiteralExpr(token, true); .) - | Nat (. e = new LiteralExpr(token, bn); .) - | BvLit (. e = new LiteralExpr(token, bn, n); .) + ( "false" (. e = new LiteralExpr(t, false); .) + | "true" (. e = new LiteralExpr(t, true); .) + | Nat (. e = new LiteralExpr(t, bn); .) + | BvLit (. e = new LiteralExpr(t, bn, n); .) | Ident (. id = new IdentifierExpr(x, x.val); e = id; .) [ "(" @@ -1275,23 +1307,23 @@ AtomExpression ")" ] - | "old" (. x = token; .) + | "old" (. x = t; .) "(" Expression ")" (. e = new OldExpr(x, e); .) | "(" ( Expression (. if (e is BvBounds) - SemErr("parentheses around bitvector bounds " + + this.SemErr("parentheses around bitvector bounds " + "are not allowed"); .) - | Forall (. x = token; .) + | Forall (. x = t; .) QuantifierBody (. if (typeParams.Length + ds.Length > 0) e = new ForallExpr(x, typeParams, ds, kv, trig, e); .) - | Exists (. x = token; .) + | Exists (. x = t; .) QuantifierBody (. if (typeParams.Length + ds.Length > 0) e = new ExistsExpr(x, typeParams, ds, kv, trig, e); .) - | Lambda (. x = token; .) + | Lambda (. x = t; .) QuantifierBody (. if (trig != null) SemErr("triggers not allowed in lambda expressions"); @@ -1305,7 +1337,7 @@ AtomExpression Attribute = (. Trigger trig = null; .) - AttributeOrTrigger (. if (trig != null) SemErr("only attributes, not triggers, allowed here"); .) + AttributeOrTrigger (. if (trig != null) this.SemErr("only attributes, not triggers, allowed here"); .) . AttributeOrTrigger @@ -1313,9 +1345,9 @@ AttributeOrTrigger string key; string value; List parameters; object! param; .) - "{" (. tok = token; .) + "{" (. tok = t; .) ( - ":" ident (. key = token.val; parameters = new List(); .) + ":" ident (. key = t.val; parameters = new List(); .) [ AttributeParameter (. parameters.Add(param); .) { "," AttributeParameter (. parameters.Add(param); .) } @@ -1329,7 +1361,7 @@ AttributeOrTrigger trig.AddLast(new Trigger(tok, false, new ExprSeq(e), null)); } } else { - SemErr("the 'nopats' quantifier attribute expects a string-literal parameter"); + this.SemErr("the 'nopats' quantifier attribute expects a string-literal parameter"); } } else { if (kv==null) { @@ -1356,7 +1388,7 @@ AttributeParameter = (. o = "error"; Expr! e; .) - ( string (. o = token.val.Substring(1, token.val.Length-2); .) + ( string (. o = t.val.Substring(1, t.val.Length-2); .) | Expression (. o = e; .) ) . @@ -1365,7 +1397,7 @@ IfThenElseExpression = (. IToken! tok; Expr! e0, e1, e2; e = dummyExpr; .) - "if" (. tok = token; .) Expression "then" Expression "else" Expression + "if" (. tok = t; .) Expression "then" Expression "else" Expression (. e = new NAryExpr(tok, new IfThenElse(tok), new ExprSeq(e0, e1, e2)); .) . @@ -1396,7 +1428,7 @@ QSep = "::" | '\u2022'. /*------------------------------------------------------------------------*/ Ident = - ident (. x = token; + ident (. x = t; if (x.val.StartsWith("\\")) x.val = x.val.Substring(1); .) @@ -1407,9 +1439,9 @@ Nat = digits (. try { - n = BigNum.FromString(token.val); + n = BigNum.FromString(t.val); } catch (FormatException) { - SemErr("incorrectly formatted number"); + this.SemErr("incorrectly formatted number"); n = BigNum.ZERO; } .) @@ -1420,14 +1452,14 @@ BvLit = bvlit (. - int pos = token.val.IndexOf("bv"); - string a = token.val.Substring(0, pos); - string b = token.val.Substring(pos + 2); + int pos = t.val.IndexOf("bv"); + string a = t.val.Substring(0, pos); + string b = t.val.Substring(pos + 2); try { n = BigNum.FromString(a); m = Convert.ToInt32(b); } catch (FormatException) { - SemErr("incorrectly formatted bitvector"); + this.SemErr("incorrectly formatted bitvector"); n = BigNum.ZERO; m = 0; } diff --git a/Source/Core/Core.sscproj b/Source/Core/Core.sscproj index 91bbaf47..4929e1c7 100644 --- a/Source/Core/Core.sscproj +++ b/Source/Core/Core.sscproj @@ -170,6 +170,10 @@ SubType="Code" RelPath="parser.ssc" /> + public static int Parse (string! filename, out /*maybe null*/ Program program) /* throws System.IO.IOException */ { - using (System.IO.StreamReader reader = new System.IO.StreamReader(filename)) { - Buffer.Fill(reader); - Scanner.Init(filename); - return Parse(out program); - } -} -/// -///Returns the number of parsing errors encountered. If 0, "program" returns as -///the parsed program. -///Note: first initialize the Scanner. -/// -public static int Parse (out /*maybe null*/ Program program) { + + FileStream stream = new FileStream(filename, FileMode.Open, FileAccess.Read, FileShare.Read); +// Scanner scanner = new Scanner(stream); + + string s = ParserHelper.Fill(stream,new List()); + byte[]! buffer = (!) UTF8Encoding.Default.GetBytes(s); + MemoryStream ms = new MemoryStream(buffer,false); + Errors errors = new Errors(); + Scanner scanner = new Scanner(ms, errors, filename); + +/* + Scanner scanner = new Scanner(filename); +*/ + Parser parser = new Parser(scanner, errors); Pgm = new Program(); // reset the global variable - Parse(); - if (Errors.count == 0) + parser.Parse(); + if (parser.errors.count == 0) { program = Pgm; return 0; @@ -60,22 +79,50 @@ public static int Parse (out /*maybe null*/ Program program) { else { program = null; - return Errors.count; + return parser.errors.count; } +/* + using (System.IO.StreamReader reader = new System.IO.StreamReader(filename)) { + Buffer.Fill(reader); + Scanner.Init(filename); + return Parse(out program); + } +*/ } - +/// +///Returns the number of parsing errors encountered. If 0, "program" returns as +///the parsed program. +///Note: first initialize the Scanner. +/// +//public static int Parse (out /*maybe null*/ Program program) { +// Pgm = new Program(); // reset the global variable +// Parse(); +// if (Errors.count == 0) +// { +// program = Pgm; +// return 0; +// } +// else +// { +// program = null; +// return Errors.count; +// } +//} + +/* public static int ParseProposition (string! text, out Expr! expression) { Buffer.Fill(text); Scanner.Init(string.Format("\"{0}\"", text)); Errors.SynErr = new ErrorProc(SynErr); - t = new Token(); + la = new Token(); Get(); Proposition(out expression); return Errors.count; } +*/ // Class to represent the bounds of a bitvector expression t[a:b]. // Objects of this class only exist during parsing and are directly @@ -103,61 +150,72 @@ private class BvBounds : Expr { /*--------------------------------------------------------------------------*/ - static void Error(int n) { - if (errDist >= minErrDist) Errors.SynErr(n, t.filename, t.line, t.col); - errDist = 0; + public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors) { + this.scanner = scanner; + this.errors = errors; + Token! tok = new Token(); + tok.val = ""; + this.la = tok; + this.t = new Token(); // just to satisfy its non-null constraint } - - public static void SemErr(string! msg) { - if (errDist >= minErrDist) Errors.SemErr(token.filename, token.line, token.col, msg); + + void SynErr (int n) { + if (errDist >= minErrDist) errors.SynErr(la.filename, la.line, la.col, n); errDist = 0; } - public static void SemErr(IToken! tok, string! msg) { - Errors.SemErr(tok.filename, tok.line, tok.col, msg); + public void SemErr (string! msg) { + if (errDist >= minErrDist) errors.SemErr(t, msg); + errDist = 0; + } + + public void SemErr(IToken! tok, string! msg) { + errors.SemErr(tok, msg); } - static void Get() { + void Get () { for (;;) { - token = t; - t = Scanner.Scan(); - if (t.kind<=maxT) {errDist++; return;} + t = la; + la = scanner.Scan(); + if (la.kind <= maxT) { ++errDist; break; } - t = token; + la = t; } } - static void Expect(int n) { - if (t.kind==n) Get(); else Error(n); + void Expect (int n) { + if (la.kind==n) Get(); else { SynErr(n); } } - static bool StartOf(int s) { - return set[s, t.kind]; + bool StartOf (int s) { + return set[s, la.kind]; } - static void ExpectWeak(int n, int follow) { - if (t.kind == n) Get(); + void ExpectWeak (int n, int follow) { + if (la.kind == n) Get(); else { - Error(n); + SynErr(n); while (!StartOf(follow)) Get(); } } - - static bool WeakSeparator(int n, int syFol, int repFol) { - bool[] s = new bool[maxT+1]; - if (t.kind == n) {Get(); return true;} - else if (StartOf(repFol)) return false; + + + bool WeakSeparator(int n, int syFol, int repFol) { + int kind = la.kind; + if (kind == n) {Get(); return true;} + else if (StartOf(repFol)) {return false;} else { - for (int i=0; i <= maxT; i++) { - s[i] = set[syFol, i] || set[repFol, i] || set[0, i]; + SynErr(n); + while (!(set[syFol, kind] || set[repFol, kind] || set[0, kind])) { + Get(); + kind = la.kind; } - Error(n); - while (!s[t.kind]) Get(); return StartOf(syFol); } } + - static void BoogiePL() { + void BoogiePL() { VariableSeq! vs; DeclarationSeq! ds; Axiom! ax; @@ -167,7 +225,7 @@ private class BvBounds : Expr { Implementation! nnim; while (StartOf(1)) { - switch (t.kind) { + switch (la.kind) { case 19: { Consts(out vs); foreach (Bpl.Variable! v in vs) { Pgm.TopLevelDeclarations.Add(v); } @@ -214,46 +272,48 @@ private class BvBounds : Expr { Expect(0); } - static void Consts(out VariableSeq! ds) { + void Consts(out VariableSeq! ds) { IToken! y; TypedIdentSeq! xs; ds = new VariableSeq(); bool u = false; QKeyValue kv = null; bool ChildrenComplete = false; List Parents = null; Expect(19); - y = token; - while (t.kind == 25) { + y = t; + while (la.kind == 25) { Attribute(ref kv); } - if (t.kind == 20) { + if (la.kind == 20) { Get(); u = true; } IdsType(out xs); - if (t.kind == 21) { + if (la.kind == 21) { OrderSpec(out ChildrenComplete, out Parents); } bool makeClone = false; foreach(TypedIdent! x in xs) { - // ensure that no sharing is introduced - List ParentsClone; - if (makeClone && Parents != null) { - ParentsClone = new List (); - foreach (ConstantParent! p in Parents) - 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)); - } + // ensure that no sharing is introduced + List ParentsClone; + if (makeClone && Parents != null) { + ParentsClone = new List (); + foreach (ConstantParent! p in Parents) + ParentsClone.Add(new ConstantParent ( + new IdentifierExpr (p.Parent.tok, p.Parent.Name), + p.Unique)); + } else { + ParentsClone = Parents; + } + makeClone = true; + + ds.Add(new Constant(y, x, u, ParentsClone, ChildrenComplete, kv)); + } + Expect(7); } - static void Function(out DeclarationSeq! ds) { + void Function(out DeclarationSeq! ds) { ds = new DeclarationSeq(); IToken! z; IToken! typeParamTok; TypeVariableSeq! typeParams = new TypeVariableSeq(); @@ -266,46 +326,46 @@ private class BvBounds : Expr { Expr! tmp; Expect(23); - while (t.kind == 25) { + while (la.kind == 25) { Attribute(ref kv); } Ident(out z); - if (t.kind == 17) { + if (la.kind == 17) { TypeParams(out typeParamTok, out typeParams); } Expect(8); if (StartOf(2)) { VarOrType(out tyd); arguments.Add(new Formal(tyd.tok, tyd, true)); - while (t.kind == 11) { + while (la.kind == 11) { Get(); VarOrType(out tyd); arguments.Add(new Formal(tyd.tok, tyd, true)); } } Expect(9); - if (t.kind == 24) { + if (la.kind == 24) { Get(); Expect(8); VarOrType(out tyd); Expect(9); retTyd = tyd; - } else if (t.kind == 10) { + } else if (la.kind == 10) { Get(); Type(out retTy); retTyd = new TypedIdent(retTy.tok, "", retTy); - } else Error(89); - if (t.kind == 25) { + } else SynErr(89); + if (la.kind == 25) { Get(); Expression(out tmp); definition = tmp; Expect(26); - } else if (t.kind == 7) { + } else if (la.kind == 7) { Get(); - } else Error(90); + } else SynErr(90); if (retTyd == null) { // construct a dummy type for the case of syntax error - tyd = new TypedIdent(token, "", new BasicType(token, SimpleType.Int)); + tyd = new TypedIdent(t, "", new BasicType(t, SimpleType.Int)); } else { tyd = retTyd; } @@ -325,7 +385,7 @@ private class BvBounds : Expr { TypedIdent! curr = ((!)arguments[i]).TypedIdent; if (curr.Name == "") { if (prevType == null) { - SemErr(curr.tok, "the type of the last parameter is unspecified"); + this.errors.SemErr(curr.tok, "the type of the last parameter is unspecified"); break; } Type ty = curr.Type; @@ -334,7 +394,7 @@ private class BvBounds : Expr { curr.Name = ((!)(ty as UnresolvedTypeIdentifier)).Name; curr.Type = prevType; } else { - SemErr(curr.tok, "expecting an identifier as parameter name"); + this.errors.SemErr(curr.tok, "expecting an identifier as parameter name"); } } else { prevType = curr.Type; @@ -359,44 +419,44 @@ private class BvBounds : Expr { foreach (TypeVariable! t in typeParams) quantifiedTypeVars.Add(new TypeVariable (Token.NoToken, t.Name)); - Expr call = new NAryExpr(z, new FunctionCall(new IdentifierExpr(z, z.val)), callArgs); - // specify the type of the function, because it might be that - // type parameters only occur in the output type - call = Expr.CoerceType(z, call, (Type)tyd.Type.Clone()); - Expr def = Expr.Eq(call, definition); - if (quantifiedTypeVars.Length != 0 || dummies.Length != 0) { - def = new ForallExpr(z, quantifiedTypeVars, dummies, - kv, - new Trigger(z, true, new ExprSeq(call), null), - def); - } - ds.Add(new Axiom(z, def, "autogenerated definition axiom", null)); - } - } - - } - - static void Axiom(out Axiom! m) { + Expr call = new NAryExpr(z, new FunctionCall(new IdentifierExpr(z, z.val)), callArgs); + // specify the type of the function, because it might be that + // type parameters only occur in the output type + call = Expr.CoerceType(z, call, (Type)tyd.Type.Clone()); + Expr def = Expr.Eq(call, definition); + if (quantifiedTypeVars.Length != 0 || dummies.Length != 0) { + def = new ForallExpr(z, quantifiedTypeVars, dummies, + kv, + new Trigger(z, true, new ExprSeq(call), null), + def); + } + ds.Add(new Axiom(z, def, "autogenerated definition axiom", null)); + } + } + + } + + void Axiom(out Axiom! m) { Expr! e; QKeyValue kv = null; Expect(27); - while (t.kind == 25) { + while (la.kind == 25) { Attribute(ref kv); } - IToken! x = token; + IToken! x = t; Proposition(out e); Expect(7); m = new Axiom(x,e, null, kv); } - static void UserDefinedTypes(out List! ts) { + void UserDefinedTypes(out List! ts) { Declaration! decl; QKeyValue kv = null; ts = new List (); Expect(28); - while (t.kind == 25) { + while (la.kind == 25) { Attribute(ref kv); } UserDefinedType(out decl, kv); ts.Add(decl); - while (t.kind == 11) { + while (la.kind == 11) { Get(); UserDefinedType(out decl, kv); ts.Add(decl); @@ -404,10 +464,10 @@ private class BvBounds : Expr { Expect(7); } - static void GlobalVars(out VariableSeq! ds) { + void GlobalVars(out VariableSeq! ds) { TypedIdentSeq! tyds = new TypedIdentSeq(); ds = new VariableSeq(); QKeyValue kv = null; Expect(6); - while (t.kind == 25) { + while (la.kind == 25) { Attribute(ref kv); } IdsTypeWheres(true, tyds); @@ -418,21 +478,22 @@ private class BvBounds : Expr { } - static void Procedure(out Procedure! proc, out /*maybe null*/ Implementation impl) { + void Procedure(out Procedure! proc, out /*maybe null*/ Implementation impl) { IToken! x; TypeVariableSeq! typeParams; VariableSeq! ins, outs; RequiresSeq! pre = new RequiresSeq(); IdentifierExprSeq! mods = new IdentifierExprSeq(); EnsuresSeq! post = new EnsuresSeq(); - VariableSeq! locals = new VariableSeq(); - StmtList! stmtList; - QKeyValue kv = null; - impl = null; + VariableSeq! locals = new VariableSeq(); + StmtList! stmtList; + QKeyValue kv = null; + impl = null; + Expect(30); ProcSignature(true, out x, out typeParams, out ins, out outs, out kv); - if (t.kind == 7) { + if (la.kind == 7) { Get(); while (StartOf(3)) { Spec(pre, mods, post); @@ -442,15 +503,14 @@ private class BvBounds : Expr { Spec(pre, mods, post); } ImplBody(out locals, out stmtList); - // here we attach kv only to the Procedure, not its implementation impl = new Implementation(x, x.val, typeParams, - Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, null); + Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, null, this.errors); - } else Error(91); + } else SynErr(91); proc = new Procedure(x, x.val, typeParams, ins, outs, pre, mods, post, kv); } - static void Implementation(out Implementation! impl) { + void Implementation(out Implementation! impl) { IToken! x; TypeVariableSeq! typeParams; VariableSeq! ins, outs; @@ -461,27 +521,27 @@ private class BvBounds : Expr { Expect(31); 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); + impl = new Implementation(x, x.val, typeParams, ins, outs, locals, stmtList, kv, this.errors); } - static void Attribute(ref QKeyValue kv) { + void Attribute(ref QKeyValue kv) { Trigger trig = null; AttributeOrTrigger(ref kv, ref trig); - if (trig != null) SemErr("only attributes, not triggers, allowed here"); + if (trig != null) this.SemErr("only attributes, not triggers, allowed here"); } - static void IdsTypeWheres(bool allowWhereClauses, TypedIdentSeq! tyds) { + void IdsTypeWheres(bool allowWhereClauses, TypedIdentSeq! tyds) { IdsTypeWhere(allowWhereClauses, tyds); - while (t.kind == 11) { + while (la.kind == 11) { Get(); IdsTypeWhere(allowWhereClauses, tyds); } } - static void LocalVars(VariableSeq! ds) { + void LocalVars(VariableSeq! ds) { TypedIdentSeq! tyds = new TypedIdentSeq(); QKeyValue kv = null; Expect(6); - while (t.kind == 25) { + while (la.kind == 25) { Attribute(ref kv); } IdsTypeWheres(true, tyds); @@ -492,10 +552,10 @@ private class BvBounds : Expr { } - static void ProcFormals(bool incoming, bool allowWhereClauses, out VariableSeq! ds) { + void ProcFormals(bool incoming, bool allowWhereClauses, out VariableSeq! ds) { TypedIdentSeq! tyds = new TypedIdentSeq(); ds = new VariableSeq(); Expect(8); - if (t.kind == 1) { + if (la.kind == 1) { IdsTypeWheres(allowWhereClauses, tyds); } Expect(9); @@ -505,7 +565,7 @@ private class BvBounds : Expr { } - static void BoundVars(IToken! x, out VariableSeq! ds) { + void BoundVars(IToken! x, out VariableSeq! ds) { TypedIdentSeq! tyds = new TypedIdentSeq(); ds = new VariableSeq(); IdsTypeWheres(false, tyds); foreach (TypedIdent! tyd in tyds) { @@ -514,7 +574,7 @@ private class BvBounds : Expr { } - static void IdsType(out TypedIdentSeq! tyds) { + void IdsType(out TypedIdentSeq! tyds) { TokenSeq! ids; Bpl.Type! ty; Idents(out ids); Expect(10); @@ -526,45 +586,45 @@ private class BvBounds : Expr { } - static void Idents(out TokenSeq! xs) { + void Idents(out TokenSeq! xs) { IToken! id; xs = new TokenSeq(); Ident(out id); xs.Add(id); - while (t.kind == 11) { + while (la.kind == 11) { Get(); Ident(out id); xs.Add(id); } } - static void Type(out Bpl.Type! ty) { + void Type(out Bpl.Type! ty) { IToken! tok; ty = dummyType; - if (t.kind == 8 || t.kind == 13 || t.kind == 14) { + if (la.kind == 8 || la.kind == 13 || la.kind == 14) { TypeAtom(out ty); - } else if (t.kind == 1) { + } else if (la.kind == 1) { Ident(out tok); TypeSeq! args = new TypeSeq (); if (StartOf(2)) { TypeArgs(args); } ty = new UnresolvedTypeIdentifier (tok, tok.val, args); - } else if (t.kind == 15 || t.kind == 17) { + } else if (la.kind == 15 || la.kind == 17) { MapType(out ty); - } else Error(92); + } else SynErr(92); } - static void IdsTypeWhere(bool allowWhereClauses, TypedIdentSeq! tyds) { + void IdsTypeWhere(bool allowWhereClauses, TypedIdentSeq! tyds) { TokenSeq! ids; Bpl.Type! ty; Expr wh = null; Expr! nne; Idents(out ids); Expect(10); Type(out ty); - if (t.kind == 12) { + if (la.kind == 12) { Get(); Expression(out nne); if (allowWhereClauses) { wh = nne; } else { - SemErr("where clause not allowed here"); + this.SemErr("where clause not allowed here"); } } @@ -574,74 +634,74 @@ private class BvBounds : Expr { } - static void Expression(out Expr! e0) { + void Expression(out Expr! e0) { IToken! x; Expr! e1; ImpliesExpression(false, out e0); - while (t.kind == 52 || t.kind == 53) { + while (la.kind == 52 || la.kind == 53) { EquivOp(); - x = token; + x = t; ImpliesExpression(false, out e1); e0 = Expr.Binary(x, BinaryOperator.Opcode.Iff, e0, e1); } } - static void TypeAtom(out Bpl.Type! ty) { + void TypeAtom(out Bpl.Type! ty) { ty = dummyType; - if (t.kind == 13) { + if (la.kind == 13) { Get(); - ty = new BasicType(token, SimpleType.Int); - } else if (t.kind == 14) { + ty = new BasicType(t, SimpleType.Int); + } else if (la.kind == 14) { Get(); - ty = new BasicType(token, SimpleType.Bool); - } else if (t.kind == 8) { + ty = new BasicType(t, SimpleType.Bool); + } else if (la.kind == 8) { Get(); Type(out ty); Expect(9); - } else Error(93); + } else SynErr(93); } - static void Ident(out IToken! x) { + void Ident(out IToken! x) { Expect(1); - x = token; + x = t; if (x.val.StartsWith("\\")) x.val = x.val.Substring(1); } - static void TypeArgs(TypeSeq! ts) { + void TypeArgs(TypeSeq! ts) { IToken! tok; Type! ty; - if (t.kind == 8 || t.kind == 13 || t.kind == 14) { + if (la.kind == 8 || la.kind == 13 || la.kind == 14) { TypeAtom(out ty); ts.Add(ty); if (StartOf(2)) { TypeArgs(ts); } - } else if (t.kind == 1) { + } else if (la.kind == 1) { Ident(out tok); TypeSeq! args = new TypeSeq (); ts.Add(new UnresolvedTypeIdentifier (tok, tok.val, args)); if (StartOf(2)) { TypeArgs(ts); } - } else if (t.kind == 15 || t.kind == 17) { + } else if (la.kind == 15 || la.kind == 17) { MapType(out ty); ts.Add(ty); - } else Error(94); + } else SynErr(94); } - static void MapType(out Bpl.Type! ty) { + void MapType(out Bpl.Type! ty) { IToken tok = null; IToken! nnTok; TypeSeq! arguments = new TypeSeq(); Type! result; TypeVariableSeq! typeParameters = new TypeVariableSeq(); - if (t.kind == 17) { + if (la.kind == 17) { TypeParams(out nnTok, out typeParameters); tok = nnTok; } Expect(15); - if (tok == null) tok = token; + if (tok == null) tok = t; if (StartOf(2)) { Types(arguments); } @@ -651,10 +711,10 @@ private class BvBounds : Expr { } - static void TypeParams(out IToken! tok, out Bpl.TypeVariableSeq! typeParams) { + void TypeParams(out IToken! tok, out Bpl.TypeVariableSeq! typeParams) { TokenSeq! typeParamToks; Expect(17); - tok = token; + tok = t; Idents(out typeParamToks); Expect(18); typeParams = new TypeVariableSeq (); @@ -663,18 +723,18 @@ private class BvBounds : Expr { } - static void Types(TypeSeq! ts) { + void Types(TypeSeq! ts) { Bpl.Type! ty; Type(out ty); ts.Add(ty); - while (t.kind == 11) { + while (la.kind == 11) { Get(); Type(out ty); ts.Add(ty); } } - static void OrderSpec(out bool ChildrenComplete, out List Parents) { + void OrderSpec(out bool ChildrenComplete, out List Parents) { ChildrenComplete = false; Parents = null; bool u; @@ -682,18 +742,18 @@ private class BvBounds : Expr { Expect(21); Parents = new List (); u = false; - if (t.kind == 1 || t.kind == 20) { - if (t.kind == 20) { + if (la.kind == 1 || la.kind == 20) { + if (la.kind == 20) { Get(); u = true; } Ident(out parent); Parents.Add(new ConstantParent ( new IdentifierExpr(parent, parent.val), u)); - while (t.kind == 11) { + while (la.kind == 11) { Get(); u = false; - if (t.kind == 20) { + if (la.kind == 20) { Get(); u = true; } @@ -702,23 +762,23 @@ private class BvBounds : Expr { new IdentifierExpr(parent, parent.val), u)); } } - if (t.kind == 22) { + if (la.kind == 22) { Get(); ChildrenComplete = true; } } - static void VarOrType(out TypedIdent! tyd) { + void VarOrType(out TypedIdent! tyd) { string! varName = ""; Bpl.Type! ty; IToken! tok; Type(out ty); tok = ty.tok; - if (t.kind == 10) { + if (la.kind == 10) { Get(); if (ty is UnresolvedTypeIdentifier && ((!)(ty as UnresolvedTypeIdentifier)).Arguments.Length == 0) { varName = ((!)(ty as UnresolvedTypeIdentifier)).Name; } else { - SemErr("expected identifier before ':'"); + this.SemErr("expected identifier before ':'"); } Type(out ty); @@ -726,18 +786,18 @@ private class BvBounds : Expr { tyd = new TypedIdent(tok, varName, ty); } - static void Proposition(out Expr! e) { + void Proposition(out Expr! e) { Expression(out e); } - static void UserDefinedType(out Declaration! decl, QKeyValue kv) { + void UserDefinedType(out Declaration! decl, QKeyValue kv) { IToken! id; IToken! id2; TokenSeq! paramTokens = new TokenSeq (); Type! body = dummyType; bool synonym = false; Ident(out id); - if (t.kind == 1) { + if (la.kind == 1) { WhiteSpaceIdents(out paramTokens); } - if (t.kind == 29) { + if (la.kind == 29) { Get(); Type(out body); synonym = true; @@ -753,39 +813,39 @@ private class BvBounds : Expr { } - static void WhiteSpaceIdents(out TokenSeq! xs) { + void WhiteSpaceIdents(out TokenSeq! xs) { IToken! id; xs = new TokenSeq(); Ident(out id); xs.Add(id); - while (t.kind == 1) { + while (la.kind == 1) { Ident(out id); xs.Add(id); } } - static void ProcSignature(bool allowWhereClausesOnFormals, out IToken! name, out TypeVariableSeq! typeParams, + void ProcSignature(bool allowWhereClausesOnFormals, out IToken! name, out TypeVariableSeq! typeParams, out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { IToken! typeParamTok; typeParams = new TypeVariableSeq(); outs = new VariableSeq(); kv = null; - while (t.kind == 25) { + while (la.kind == 25) { Attribute(ref kv); } Ident(out name); - if (t.kind == 17) { + if (la.kind == 17) { TypeParams(out typeParamTok, out typeParams); } ProcFormals(true, allowWhereClausesOnFormals, out ins); - if (t.kind == 24) { + if (la.kind == 24) { Get(); ProcFormals(false, allowWhereClausesOnFormals, out outs); } } - static void Spec(RequiresSeq! pre, IdentifierExprSeq! mods, EnsuresSeq! post) { + void Spec(RequiresSeq! pre, IdentifierExprSeq! mods, EnsuresSeq! post) { TokenSeq! ms; - if (t.kind == 32) { + if (la.kind == 32) { Get(); - if (t.kind == 1) { + if (la.kind == 1) { Idents(out ms); foreach (IToken! m in ms) { mods.Add(new IdentifierExpr(m, m.val)); @@ -793,74 +853,74 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { } Expect(7); - } else if (t.kind == 33) { + } else if (la.kind == 33) { Get(); SpecPrePost(true, pre, post); - } else if (t.kind == 34 || t.kind == 35) { + } else if (la.kind == 34 || la.kind == 35) { SpecPrePost(false, pre, post); - } else Error(95); + } else SynErr(95); } - static void ImplBody(out VariableSeq! locals, out StmtList! stmtList) { + void ImplBody(out VariableSeq! locals, out StmtList! stmtList) { locals = new VariableSeq(); Expect(25); - while (t.kind == 6) { + while (la.kind == 6) { LocalVars(locals); } StmtList(out stmtList); } - static void SpecPrePost(bool free, RequiresSeq! pre, EnsuresSeq! post) { + void SpecPrePost(bool free, RequiresSeq! pre, EnsuresSeq! post) { Expr! e; VariableSeq! locals; BlockSeq! blocks; Token tok = null; QKeyValue kv = null; - if (t.kind == 34) { + if (la.kind == 34) { Get(); - tok = token; - while (t.kind == 25) { + tok = t; + while (la.kind == 25) { Attribute(ref kv); } if (StartOf(5)) { Proposition(out e); Expect(7); pre.Add(new Requires(tok, free, e, null, kv)); - } else if (t.kind == 36) { + } else if (la.kind == 36) { SpecBody(out locals, out blocks); Expect(7); pre.Add(new Requires(tok, free, new BlockExpr(locals, blocks), null, kv)); - } else Error(96); - } else if (t.kind == 35) { + } else SynErr(96); + } else if (la.kind == 35) { Get(); - tok = token; - while (t.kind == 25) { + tok = t; + while (la.kind == 25) { Attribute(ref kv); } if (StartOf(5)) { Proposition(out e); Expect(7); post.Add(new Ensures(tok, free, e, null, kv)); - } else if (t.kind == 36) { + } else if (la.kind == 36) { SpecBody(out locals, out blocks); Expect(7); post.Add(new Ensures(tok, free, new BlockExpr(locals, blocks), null, kv)); - } else Error(97); - } else Error(98); + } else SynErr(97); + } else SynErr(98); } - static void SpecBody(out VariableSeq! locals, out BlockSeq! blocks) { + void SpecBody(out VariableSeq! locals, out BlockSeq! blocks) { locals = new VariableSeq(); Block! b; Expect(36); - while (t.kind == 6) { + while (la.kind == 6) { LocalVars(locals); } SpecBlock(out b); blocks = new BlockSeq(b); - while (t.kind == 1) { + while (la.kind == 1) { SpecBlock(out b); blocks.Add(b); } Expect(37); } - static void SpecBlock(out Block! b) { + void SpecBlock(out Block! b) { IToken! x; IToken! y; Cmd c; IToken label; CmdSeq cs = new CmdSeq(); @@ -878,26 +938,26 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { cs.Add(c); } else { assert label != null; - SemErr("SpecBlock's can only have one label"); + this.SemErr("SpecBlock's can only have one label"); } } - if (t.kind == 38) { + if (la.kind == 38) { Get(); - y = token; + y = t; Idents(out xs); foreach (IToken! s in xs) { ss.Add(s.val); } b = new Block(x,x.val,cs,new GotoCmd(y,ss)); - } else if (t.kind == 39) { + } else if (la.kind == 39) { Get(); Expression(out e); - b = new Block(x,x.val,cs,new ReturnExprCmd(token,e)); - } else Error(99); + b = new Block(x,x.val,cs,new ReturnExprCmd(t,e)); + } else SynErr(99); Expect(7); } - static void LabelOrCmd(out Cmd c, out IToken label) { + void LabelOrCmd(out Cmd c, out IToken label) { IToken! x; Expr! e; TokenSeq! xs; IdentifierExprSeq ids; @@ -905,26 +965,26 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { Cmd! cn; QKeyValue kv = null; - if (t.kind == 1) { + if (la.kind == 1) { LabelOrAssign(out c, out label); - } else if (t.kind == 46) { + } else if (la.kind == 46) { Get(); - x = token; - while (t.kind == 25) { + x = t; + while (la.kind == 25) { Attribute(ref kv); } Proposition(out e); c = new AssertCmd(x,e, kv); Expect(7); - } else if (t.kind == 47) { + } else if (la.kind == 47) { Get(); - x = token; + x = t; Proposition(out e); c = new AssumeCmd(x,e); Expect(7); - } else if (t.kind == 48) { + } else if (la.kind == 48) { Get(); - x = token; + x = t; Idents(out xs); Expect(7); ids = new IdentifierExprSeq(); @@ -933,14 +993,14 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { } c = new HavocCmd(x,ids); - } else if (t.kind == 50) { + } else if (la.kind == 50) { CallCmd(out cn); Expect(7); c = cn; - } else Error(100); + } else SynErr(100); } - static void StmtList(out StmtList! stmtList) { + void StmtList(out StmtList! stmtList) { List bigblocks = new List(); /* built-up state for the current BigBlock: */ IToken startToken = null; string currentLabel = null; @@ -974,7 +1034,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { cs = new CmdSeq(); } - } else if (t.kind == 40 || t.kind == 42 || t.kind == 45) { + } else if (la.kind == 40 || la.kind == 42 || la.kind == 45) { StructuredCmd(out ecn); ec = ecn; if (startToken == null) { startToken = ec.tok; cs = new CmdSeq(); } @@ -995,55 +1055,56 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { } } Expect(26); - IToken! endCurly = token; + IToken! endCurly = t; if (startToken == null && bigblocks.Count == 0) { - startToken = token; cs = new CmdSeq(); + startToken = t; cs = new CmdSeq(); } if (startToken != null) { assert cs != null; b = new BigBlock(startToken, currentLabel, cs, null, null); bigblocks.Add(b); } - stmtList = new StmtList(bigblocks, endCurly); + stmtList = new StmtList(bigblocks, endCurly); + } - static void StructuredCmd(out StructuredCmd! ec) { + void StructuredCmd(out StructuredCmd! ec) { ec = dummyStructuredCmd; assume ec.IsPeerConsistent; IfCmd! ifcmd; WhileCmd! wcmd; BreakCmd! bcmd; - if (t.kind == 40) { + if (la.kind == 40) { IfCmd(out ifcmd); ec = ifcmd; - } else if (t.kind == 42) { + } else if (la.kind == 42) { WhileCmd(out wcmd); ec = wcmd; - } else if (t.kind == 45) { + } else if (la.kind == 45) { BreakCmd(out bcmd); ec = bcmd; - } else Error(101); + } else SynErr(101); } - static void TransferCmd(out TransferCmd! tc) { + void TransferCmd(out TransferCmd! tc) { tc = dummyTransferCmd; Token y; TokenSeq! xs; StringSeq ss = new StringSeq(); - if (t.kind == 38) { + if (la.kind == 38) { Get(); - y = token; + y = t; Idents(out xs); foreach (IToken! s in xs) { ss.Add(s.val); } tc = new GotoCmd(y, ss); - } else if (t.kind == 39) { + } else if (la.kind == 39) { Get(); - tc = new ReturnCmd(token); - } else Error(102); + tc = new ReturnCmd(t); + } else SynErr(102); Expect(7); } - static void IfCmd(out IfCmd! ifcmd) { + void IfCmd(out IfCmd! ifcmd) { IToken! x; Expr guard; StmtList! thn; @@ -1051,37 +1112,37 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { StmtList! els; StmtList elseOption = null; Expect(40); - x = token; + x = t; Guard(out guard); Expect(25); StmtList(out thn); - if (t.kind == 41) { + if (la.kind == 41) { Get(); - if (t.kind == 40) { + if (la.kind == 40) { IfCmd(out elseIf); elseIfOption = elseIf; - } else if (t.kind == 25) { + } else if (la.kind == 25) { Get(); StmtList(out els); elseOption = els; - } else Error(103); + } else SynErr(103); } ifcmd = new IfCmd(x, guard, thn, elseIfOption, elseOption); } - static void WhileCmd(out WhileCmd! wcmd) { + void WhileCmd(out WhileCmd! wcmd) { IToken! x; Token z; Expr guard; Expr! e; bool isFree; List invariants = new List(); StmtList! body; Expect(42); - x = token; + x = t; Guard(out guard); assume guard == null || Owner.None(guard); - while (t.kind == 33 || t.kind == 43) { - isFree = false; z = t/*lookahead token*/; - if (t.kind == 33) { + while (la.kind == 33 || la.kind == 43) { + isFree = false; z = la/*lookahead token*/; + if (la.kind == 33) { Get(); isFree = true; } @@ -1100,13 +1161,13 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { wcmd = new WhileCmd(x, guard, invariants, body); } - static void BreakCmd(out BreakCmd! bcmd) { + void BreakCmd(out BreakCmd! bcmd) { IToken! x; IToken! y; string breakLabel = null; Expect(45); - x = token; - if (t.kind == 1) { + x = t; + if (la.kind == 1) { Ident(out y); breakLabel = y.val; } @@ -1114,20 +1175,20 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { bcmd = new BreakCmd(x, breakLabel); } - static void Guard(out Expr e) { + void Guard(out Expr e) { Expr! ee; e = null; Expect(8); - if (t.kind == 44) { + if (la.kind == 44) { Get(); e = null; } else if (StartOf(5)) { Expression(out ee); e = ee; - } else Error(104); + } else SynErr(104); Expect(9); } - static void LabelOrAssign(out Cmd c, out IToken label) { + void LabelOrAssign(out Cmd c, out IToken label) { IToken! id; IToken! x; Expr! e, e0; c = dummyCmd; label = null; AssignLhs! lhs; @@ -1135,36 +1196,36 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { List! rhss; Ident(out id); - x = token; - if (t.kind == 10) { + x = t; + if (la.kind == 10) { Get(); c = null; label = x; - } else if (t.kind == 11 || t.kind == 15 || t.kind == 49) { + } else if (la.kind == 11 || la.kind == 15 || la.kind == 49) { MapAssignIndexes(id, out lhs); lhss = new List (); lhss.Add(lhs); - while (t.kind == 11) { + while (la.kind == 11) { Get(); Ident(out id); MapAssignIndexes(id, out lhs); lhss.Add(lhs); } Expect(49); - x = token; /* use location of := */ + x = t; /* use location of := */ Expression(out e0); rhss = new List (); rhss.Add(e0); - while (t.kind == 11) { + while (la.kind == 11) { Get(); Expression(out e0); rhss.Add(e0); } Expect(7); c = new AssignCmd(x, lhss, rhss); - } else Error(105); + } else SynErr(105); } - static void CallCmd(out Cmd! c) { + void CallCmd(out Cmd! c) { IToken! x; IToken! first; IToken p; List! ids = new List(); List! es = new List(); @@ -1173,18 +1234,18 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { c = dummyCmd; Expect(50); - x = token; - while (t.kind == 25) { + x = t; + while (la.kind == 25) { Attribute(ref kv); } - if (t.kind == 1) { + if (la.kind == 1) { Ident(out first); - if (t.kind == 8) { + if (la.kind == 8) { Get(); if (StartOf(8)) { CallForallArg(out en); es.Add(en); - while (t.kind == 11) { + while (la.kind == 11) { Get(); CallForallArg(out en); es.Add(en); @@ -1192,9 +1253,9 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { } Expect(9); c = new CallCmd(x, first.val, es, ids, kv); - } else if (t.kind == 11 || t.kind == 49) { + } else if (la.kind == 11 || la.kind == 49) { ids.Add(new IdentifierExpr(first, first.val)); - if (t.kind == 11) { + if (la.kind == 11) { Get(); CallOutIdent(out p); if (p==null) { @@ -1203,7 +1264,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { ids.Add(new IdentifierExpr(p, p.val)); } - while (t.kind == 11) { + while (la.kind == 11) { Get(); CallOutIdent(out p); if (p==null) { @@ -1220,7 +1281,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { if (StartOf(8)) { CallForallArg(out en); es.Add(en); - while (t.kind == 11) { + while (la.kind == 11) { Get(); CallForallArg(out en); es.Add(en); @@ -1228,8 +1289,8 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { } Expect(9); c = new CallCmd(x, first.val, es, ids, kv); - } else Error(106); - } else if (t.kind == 51) { + } else SynErr(106); + } else if (la.kind == 51) { Get(); Ident(out first); Expect(8); @@ -1237,7 +1298,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { if (StartOf(8)) { CallForallArg(out en); args.Add(en); - while (t.kind == 11) { + while (la.kind == 11) { Get(); CallForallArg(out en); args.Add(en); @@ -1245,10 +1306,10 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { } Expect(9); c = new CallForallCmd(x, first.val, args, kv); - } else if (t.kind == 44) { + } else if (la.kind == 44) { Get(); ids.Add(null); - if (t.kind == 11) { + if (la.kind == 11) { Get(); CallOutIdent(out p); if (p==null) { @@ -1257,7 +1318,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { ids.Add(new IdentifierExpr(p, p.val)); } - while (t.kind == 11) { + while (la.kind == 11) { Get(); CallOutIdent(out p); if (p==null) { @@ -1274,7 +1335,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { if (StartOf(8)) { CallForallArg(out en); es.Add(en); - while (t.kind == 11) { + while (la.kind == 11) { Get(); CallForallArg(out en); es.Add(en); @@ -1282,10 +1343,10 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { } Expect(9); c = new CallCmd(x, first.val, es, ids, kv); - } else Error(107); + } else SynErr(107); } - static void MapAssignIndexes(IToken! assignedVariable, out AssignLhs! lhs) { + void MapAssignIndexes(IToken! assignedVariable, out AssignLhs! lhs) { IToken! x; AssignLhs! runningLhs = new SimpleAssignLhs(assignedVariable, @@ -1293,14 +1354,14 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { List! indexes; Expr! e0; - while (t.kind == 15) { + while (la.kind == 15) { Get(); - x = token; + x = t; indexes = new List (); if (StartOf(5)) { Expression(out e0); indexes.Add(e0); - while (t.kind == 11) { + while (la.kind == 11) { Get(); Expression(out e0); indexes.Add(e0); @@ -1313,60 +1374,60 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { lhs = runningLhs; } - static void CallForallArg(out Expr exprOptional) { + void CallForallArg(out Expr exprOptional) { exprOptional = null; Expr! e; - if (t.kind == 44) { + if (la.kind == 44) { Get(); } else if (StartOf(5)) { Expression(out e); exprOptional = e; - } else Error(108); + } else SynErr(108); } - static void CallOutIdent(out IToken id) { + void CallOutIdent(out IToken id) { id = null; IToken! p; - if (t.kind == 44) { + if (la.kind == 44) { Get(); - } else if (t.kind == 1) { + } else if (la.kind == 1) { Ident(out p); id = p; - } else Error(109); + } else SynErr(109); } - static void Expressions(out ExprSeq! es) { + void Expressions(out ExprSeq! es) { Expr! e; es = new ExprSeq(); Expression(out e); es.Add(e); - while (t.kind == 11) { + while (la.kind == 11) { Get(); Expression(out e); es.Add(e); } } - static void ImpliesExpression(bool noExplies, out Expr! e0) { + void ImpliesExpression(bool noExplies, out Expr! e0) { IToken! x; Expr! e1; LogicalExpression(out e0); if (StartOf(9)) { - if (t.kind == 54 || t.kind == 55) { + if (la.kind == 54 || la.kind == 55) { ImpliesOp(); - x = token; + x = t; ImpliesExpression(true, out e1); e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e0, e1); } else { ExpliesOp(); if (noExplies) - SemErr("illegal mixture of ==> and <==, use parentheses to disambiguate"); - x = token; + this.SemErr("illegal mixture of ==> and <==, use parentheses to disambiguate"); + x = t; LogicalExpression(out e1); e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e1, e0); - while (t.kind == 56 || t.kind == 57) { + while (la.kind == 56 || la.kind == 57) { ExpliesOp(); - x = token; + x = t; LogicalExpression(out e1); e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e1, e0); } @@ -1374,37 +1435,37 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { } } - static void EquivOp() { - if (t.kind == 52) { + void EquivOp() { + if (la.kind == 52) { Get(); - } else if (t.kind == 53) { + } else if (la.kind == 53) { Get(); - } else Error(110); + } else SynErr(110); } - static void LogicalExpression(out Expr! e0) { + void LogicalExpression(out Expr! e0) { IToken! x; Expr! e1; BinaryOperator.Opcode op; RelationalExpression(out e0); if (StartOf(10)) { - if (t.kind == 58 || t.kind == 59) { + if (la.kind == 58 || la.kind == 59) { AndOp(); - x = token; + x = t; RelationalExpression(out e1); e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1); - while (t.kind == 58 || t.kind == 59) { + while (la.kind == 58 || la.kind == 59) { AndOp(); - x = token; + x = t; RelationalExpression(out e1); e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1); } } else { OrOp(); - x = token; + x = t; RelationalExpression(out e1); e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1); - while (t.kind == 60 || t.kind == 61) { + while (la.kind == 60 || la.kind == 61) { OrOp(); - x = token; + x = t; RelationalExpression(out e1); e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1); } @@ -1412,23 +1473,23 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { } } - static void ImpliesOp() { - if (t.kind == 54) { + void ImpliesOp() { + if (la.kind == 54) { Get(); - } else if (t.kind == 55) { + } else if (la.kind == 55) { Get(); - } else Error(111); + } else SynErr(111); } - static void ExpliesOp() { - if (t.kind == 56) { + void ExpliesOp() { + if (la.kind == 56) { Get(); - } else if (t.kind == 57) { + } else if (la.kind == 57) { Get(); - } else Error(112); + } else SynErr(112); } - static void RelationalExpression(out Expr! e0) { + void RelationalExpression(out Expr! e0) { IToken! x; Expr! e1; BinaryOperator.Opcode op; BvTerm(out e0); if (StartOf(11)) { @@ -1438,197 +1499,197 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { } } - static void AndOp() { - if (t.kind == 58) { + void AndOp() { + if (la.kind == 58) { Get(); - } else if (t.kind == 59) { + } else if (la.kind == 59) { Get(); - } else Error(113); + } else SynErr(113); } - static void OrOp() { - if (t.kind == 60) { + void OrOp() { + if (la.kind == 60) { Get(); - } else if (t.kind == 61) { + } else if (la.kind == 61) { Get(); - } else Error(114); + } else SynErr(114); } - static void BvTerm(out Expr! e0) { + void BvTerm(out Expr! e0) { IToken! x; Expr! e1; Term(out e0); - while (t.kind == 70) { + while (la.kind == 70) { Get(); - x = token; + x = t; Term(out e1); e0 = new BvConcatExpr(x, e0, e1); } } - static void RelOp(out IToken! x, out BinaryOperator.Opcode op) { + void RelOp(out IToken! x, out BinaryOperator.Opcode op) { x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; - switch (t.kind) { + switch (la.kind) { case 62: { Get(); - x = token; op=BinaryOperator.Opcode.Eq; + x = t; op=BinaryOperator.Opcode.Eq; break; } case 17: { Get(); - x = token; op=BinaryOperator.Opcode.Lt; + x = t; op=BinaryOperator.Opcode.Lt; break; } case 18: { Get(); - x = token; op=BinaryOperator.Opcode.Gt; + x = t; op=BinaryOperator.Opcode.Gt; break; } case 63: { Get(); - x = token; op=BinaryOperator.Opcode.Le; + x = t; op=BinaryOperator.Opcode.Le; break; } case 64: { Get(); - x = token; op=BinaryOperator.Opcode.Ge; + x = t; op=BinaryOperator.Opcode.Ge; break; } case 65: { Get(); - x = token; op=BinaryOperator.Opcode.Neq; + x = t; op=BinaryOperator.Opcode.Neq; break; } case 66: { Get(); - x = token; op=BinaryOperator.Opcode.Subtype; + x = t; op=BinaryOperator.Opcode.Subtype; break; } case 67: { Get(); - x = token; op=BinaryOperator.Opcode.Neq; + x = t; op=BinaryOperator.Opcode.Neq; break; } case 68: { Get(); - x = token; op=BinaryOperator.Opcode.Le; + x = t; op=BinaryOperator.Opcode.Le; break; } case 69: { Get(); - x = token; op=BinaryOperator.Opcode.Ge; + x = t; op=BinaryOperator.Opcode.Ge; break; } - default: Error(115); break; + default: SynErr(115); break; } } - static void Term(out Expr! e0) { + void Term(out Expr! e0) { IToken! x; Expr! e1; BinaryOperator.Opcode op; Factor(out e0); - while (t.kind == 71 || t.kind == 72) { + while (la.kind == 71 || la.kind == 72) { AddOp(out x, out op); Factor(out e1); e0 = Expr.Binary(x, op, e0, e1); } } - static void Factor(out Expr! e0) { + void Factor(out Expr! e0) { IToken! x; Expr! e1; BinaryOperator.Opcode op; UnaryExpression(out e0); - while (t.kind == 44 || t.kind == 73 || t.kind == 74) { + while (la.kind == 44 || la.kind == 73 || la.kind == 74) { MulOp(out x, out op); UnaryExpression(out e1); e0 = Expr.Binary(x, op, e0, e1); } } - static void AddOp(out IToken! x, out BinaryOperator.Opcode op) { + void AddOp(out IToken! x, out BinaryOperator.Opcode op) { x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; - if (t.kind == 71) { + if (la.kind == 71) { Get(); - x = token; op=BinaryOperator.Opcode.Add; - } else if (t.kind == 72) { + x = t; op=BinaryOperator.Opcode.Add; + } else if (la.kind == 72) { Get(); - x = token; op=BinaryOperator.Opcode.Sub; - } else Error(116); + x = t; op=BinaryOperator.Opcode.Sub; + } else SynErr(116); } - static void UnaryExpression(out Expr! e) { + void UnaryExpression(out Expr! e) { IToken! x; e = dummyExpr; - if (t.kind == 72) { + if (la.kind == 72) { Get(); - x = token; + x = t; UnaryExpression(out e); e = Expr.Binary(x, BinaryOperator.Opcode.Sub, new LiteralExpr(x, BigNum.ZERO), e); - } else if (t.kind == 75 || t.kind == 76) { + } else if (la.kind == 75 || la.kind == 76) { NegOp(); - x = token; + x = t; UnaryExpression(out e); e = Expr.Unary(x, UnaryOperator.Opcode.Not, e); } else if (StartOf(12)) { CoercionExpression(out e); - } else Error(117); + } else SynErr(117); } - static void MulOp(out IToken! x, out BinaryOperator.Opcode op) { + void MulOp(out IToken! x, out BinaryOperator.Opcode op) { x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; - if (t.kind == 44) { + if (la.kind == 44) { Get(); - x = token; op=BinaryOperator.Opcode.Mul; - } else if (t.kind == 73) { + x = t; op=BinaryOperator.Opcode.Mul; + } else if (la.kind == 73) { Get(); - x = token; op=BinaryOperator.Opcode.Div; - } else if (t.kind == 74) { + x = t; op=BinaryOperator.Opcode.Div; + } else if (la.kind == 74) { Get(); - x = token; op=BinaryOperator.Opcode.Mod; - } else Error(118); + x = t; op=BinaryOperator.Opcode.Mod; + } else SynErr(118); } - static void NegOp() { - if (t.kind == 75) { + void NegOp() { + if (la.kind == 75) { Get(); - } else if (t.kind == 76) { + } else if (la.kind == 76) { Get(); - } else Error(119); + } else SynErr(119); } - static void CoercionExpression(out Expr! e) { + void CoercionExpression(out Expr! e) { IToken! x; Type! coercedTo; BigNum bn; ArrayExpression(out e); - while (t.kind == 10) { + while (la.kind == 10) { Get(); - x = token; + x = t; if (StartOf(2)) { Type(out coercedTo); e = Expr.CoerceType(x, e, coercedTo); - } else if (t.kind == 3) { + } else if (la.kind == 3) { Nat(out bn); if (!(e is LiteralExpr) || !((LiteralExpr)e).isBigNum) { - SemErr("arguments of extract need to be integer literals"); + this.SemErr("arguments of extract need to be integer literals"); e = new BvBounds(x, bn, BigNum.ZERO); } else { e = new BvBounds(x, bn, ((LiteralExpr)e).asBigNum); } - } else Error(120); + } else SynErr(120); } } - static void ArrayExpression(out Expr! e) { + void ArrayExpression(out Expr! e) { IToken! x; Expr! index0 = dummyExpr; Expr! e1; bool store; bool bvExtract; ExprSeq! allArgs = dummyExprSeq; AtomExpression(out e); - while (t.kind == 15) { + while (la.kind == 15) { Get(); - x = token; allArgs = new ExprSeq (); + x = t; allArgs = new ExprSeq (); allArgs.Add(e); store = false; bvExtract = false; if (StartOf(13)) { @@ -1639,19 +1700,19 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { else allArgs.Add(index0); - while (t.kind == 11) { + while (la.kind == 11) { Get(); Expression(out e1); if (bvExtract || e1 is BvBounds) - SemErr("bitvectors only have one dimension"); + this.SemErr("bitvectors only have one dimension"); allArgs.Add(e1); } - if (t.kind == 49) { + if (la.kind == 49) { Get(); Expression(out e1); if (bvExtract || e1 is BvBounds) - SemErr("assignment to bitvectors is not possible"); + this.SemErr("assignment to bitvectors is not possible"); allArgs.Add(e1); store = true; } @@ -1674,18 +1735,18 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { } } - static void Nat(out BigNum n) { + void Nat(out BigNum n) { Expect(3); try { - n = BigNum.FromString(token.val); + n = BigNum.FromString(t.val); } catch (FormatException) { - SemErr("incorrectly formatted number"); + this.SemErr("incorrectly formatted number"); n = BigNum.ZERO; } } - static void AtomExpression(out Expr! e) { + void AtomExpression(out Expr! e) { IToken! x; int n; BigNum bn; ExprSeq! es; VariableSeq! ds; Trigger trig; TypeVariableSeq! typeParams; @@ -1694,45 +1755,45 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { QKeyValue kv; e = dummyExpr; - switch (t.kind) { + switch (la.kind) { case 77: { Get(); - e = new LiteralExpr(token, false); + e = new LiteralExpr(t, false); break; } case 78: { Get(); - e = new LiteralExpr(token, true); + e = new LiteralExpr(t, true); break; } case 3: { Nat(out bn); - e = new LiteralExpr(token, bn); + e = new LiteralExpr(t, bn); break; } case 2: { BvLit(out bn, out n); - e = new LiteralExpr(token, bn, n); + e = new LiteralExpr(t, bn, n); break; } case 1: { Ident(out x); id = new IdentifierExpr(x, x.val); e = id; - if (t.kind == 8) { + if (la.kind == 8) { Get(); if (StartOf(5)) { Expressions(out es); e = new NAryExpr(x, new FunctionCall(id), es); - } else if (t.kind == 9) { + } else if (la.kind == 9) { e = new NAryExpr(x, new FunctionCall(id), new ExprSeq()); - } else Error(121); + } else SynErr(121); Expect(9); } break; } case 79: { Get(); - x = token; + x = t; Expect(8); Expression(out e); Expect(9); @@ -1744,29 +1805,29 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { if (StartOf(5)) { Expression(out e); if (e is BvBounds) - SemErr("parentheses around bitvector bounds " + + this.SemErr("parentheses around bitvector bounds " + "are not allowed"); - } else if (t.kind == 51 || t.kind == 81) { + } else if (la.kind == 51 || la.kind == 81) { Forall(); - x = token; + x = t; QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e); if (typeParams.Length + ds.Length > 0) e = new ForallExpr(x, typeParams, ds, kv, trig, e); - } else if (t.kind == 82 || t.kind == 83) { + } else if (la.kind == 82 || la.kind == 83) { Exists(); - x = token; + x = t; QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e); if (typeParams.Length + ds.Length > 0) e = new ExistsExpr(x, typeParams, ds, kv, trig, e); - } else if (t.kind == 84 || t.kind == 85) { + } else if (la.kind == 84 || la.kind == 85) { Lambda(); - x = token; + x = t; QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e); if (trig != null) SemErr("triggers not allowed in lambda expressions"); if (typeParams.Length + ds.Length > 0) e = new LambdaExpr(x, typeParams, ds, kv, e); - } else Error(122); + } else SynErr(122); Expect(9); break; } @@ -1774,78 +1835,78 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { IfThenElseExpression(out e); break; } - default: Error(123); break; + default: SynErr(123); break; } } - static void BvLit(out BigNum n, out int m) { + void BvLit(out BigNum n, out int m) { Expect(2); - int pos = token.val.IndexOf("bv"); - string a = token.val.Substring(0, pos); - string b = token.val.Substring(pos + 2); + int pos = t.val.IndexOf("bv"); + string a = t.val.Substring(0, pos); + string b = t.val.Substring(pos + 2); try { n = BigNum.FromString(a); m = Convert.ToInt32(b); } catch (FormatException) { - SemErr("incorrectly formatted bitvector"); + this.SemErr("incorrectly formatted bitvector"); n = BigNum.ZERO; m = 0; } } - static void Forall() { - if (t.kind == 51) { + void Forall() { + if (la.kind == 51) { Get(); - } else if (t.kind == 81) { + } else if (la.kind == 81) { Get(); - } else Error(124); + } else SynErr(124); } - static void QuantifierBody(IToken! q, out TypeVariableSeq! typeParams, out VariableSeq! ds, + void QuantifierBody(IToken! q, out TypeVariableSeq! typeParams, out VariableSeq! ds, out QKeyValue kv, out Trigger trig, out Expr! body) { trig = null; typeParams = new TypeVariableSeq (); IToken! tok; Expr! e; ExprSeq! es; kv = null; string key; string value; ds = new VariableSeq (); - if (t.kind == 17) { + if (la.kind == 17) { TypeParams(out tok, out typeParams); - if (t.kind == 1) { + if (la.kind == 1) { BoundVars(q, out ds); } - } else if (t.kind == 1) { + } else if (la.kind == 1) { BoundVars(q, out ds); - } else Error(125); + } else SynErr(125); QSep(); - while (t.kind == 25) { + while (la.kind == 25) { AttributeOrTrigger(ref kv, ref trig); } Expression(out body); } - static void Exists() { - if (t.kind == 82) { + void Exists() { + if (la.kind == 82) { Get(); - } else if (t.kind == 83) { + } else if (la.kind == 83) { Get(); - } else Error(126); + } else SynErr(126); } - static void Lambda() { - if (t.kind == 84) { + void Lambda() { + if (la.kind == 84) { Get(); - } else if (t.kind == 85) { + } else if (la.kind == 85) { Get(); - } else Error(127); + } else SynErr(127); } - static void IfThenElseExpression(out Expr! e) { + void IfThenElseExpression(out Expr! e) { IToken! tok; Expr! e0, e1, e2; e = dummyExpr; Expect(40); - tok = token; + tok = t; Expression(out e0); Expect(80); Expression(out e1); @@ -1854,21 +1915,21 @@ out QKeyValue kv, out Trigger trig, out Expr! body) { e = new NAryExpr(tok, new IfThenElse(tok), new ExprSeq(e0, e1, e2)); } - static void AttributeOrTrigger(ref QKeyValue kv, ref Trigger trig) { + void AttributeOrTrigger(ref QKeyValue kv, ref Trigger trig) { IToken! tok; Expr! e; ExprSeq! es; string key; string value; List parameters; object! param; Expect(25); - tok = token; - if (t.kind == 10) { + tok = t; + if (la.kind == 10) { Get(); Expect(1); - key = token.val; parameters = new List(); + key = t.val; parameters = new List(); if (StartOf(14)) { AttributeParameter(out param); parameters.Add(param); - while (t.kind == 11) { + while (la.kind == 11) { Get(); AttributeParameter(out param); parameters.Add(param); @@ -1883,7 +1944,7 @@ out QKeyValue kv, out Trigger trig, out Expr! body) { trig.AddLast(new Trigger(tok, false, new ExprSeq(e), null)); } } else { - SemErr("the 'nopats' quantifier attribute expects a string-literal parameter"); + this.SemErr("the 'nopats' quantifier attribute expects a string-literal parameter"); } } else { if (kv==null) { @@ -1896,7 +1957,7 @@ out QKeyValue kv, out Trigger trig, out Expr! body) { } else if (StartOf(5)) { Expression(out e); es = new ExprSeq(e); - while (t.kind == 11) { + while (la.kind == 11) { Get(); Expression(out e); es.Add(e); @@ -1907,46 +1968,73 @@ out QKeyValue kv, out Trigger trig, out Expr! body) { trig.AddLast(new Trigger(tok, true, es, null)); } - } else Error(128); + } else SynErr(128); Expect(26); } - static void AttributeParameter(out object! o) { + void AttributeParameter(out object! o) { o = "error"; Expr! e; - if (t.kind == 4) { + if (la.kind == 4) { Get(); - o = token.val.Substring(1, token.val.Length-2); + o = t.val.Substring(1, t.val.Length-2); } else if (StartOf(5)) { Expression(out e); o = e; - } else Error(129); + } else SynErr(129); } - static void QSep() { - if (t.kind == 86) { + void QSep() { + if (la.kind == 86) { Get(); - } else if (t.kind == 87) { + } else if (la.kind == 87) { Get(); - } else Error(130); + } else SynErr(130); } - public static void Parse() { - Errors.SynErr = new ErrorProc(SynErr); - t = new Token(); + public void Parse() { + la = new Token(); + la.val = ""; Get(); BoogiePL(); + Expect(0); } + + 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,T,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,T,x,x, x,x,x,x, T,x,x,x, x,T,T,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, + {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,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,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x}, + {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,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,T,T, T,x,T,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,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,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, T,x,x,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,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,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,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,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,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,T,T,T, x,x,x,x, x,x,x,x, x,x}, + {x,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,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, T,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x}, + {x,T,T,T, T,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,x,x,x, x,x,x,x, 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,T,T, x,x,x,x, x,x,x,x, x,x} - [Microsoft.Contracts.Verify(false)] - static void SynErr(int n, string filename, int line, int col) { - Errors.count++; - Console.Write("{0}({1},{2}): syntax error: ", filename, line, col); + }; +} // end Parser + + +public class Errors { + public int count = 0; // number of errors detected + public System.IO.TextWriter! errorStream = Console.Out; // error messages go to this stream +// public string errMsgFormat = "-- line {0} col {1}: {2}"; // 0=line, 1=column, 2=text + public string! errMsgFormat4 = "{0}({1},{2}): Error: {3}"; // 0=line, 1=column, 2=text + public string! errMsgFormat = "-- line {0} col {1}: {2}"; // 0=line, 1=column, 2=text + + public void SynErr (string filename, int line, int col, int n) { string s; + Console.Write("{0}({1},{2}): syntax error: ", filename, line, col); switch (n) { case 0: s = "EOF expected"; break; case 1: s = "ident expected"; break; @@ -1954,88 +2042,88 @@ out QKeyValue kv, out Trigger trig, out Expr! body) { case 3: s = "digits expected"; break; case 4: s = "string expected"; break; case 5: s = "float expected"; break; - case 6: s = "var expected"; break; - case 7: s = "; 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 = "where expected"; break; - case 13: s = "int expected"; break; - case 14: s = "bool expected"; break; - case 15: s = "[ expected"; break; - case 16: s = "] expected"; break; - case 17: s = "< expected"; break; - case 18: s = "> expected"; break; - case 19: s = "const expected"; break; - case 20: s = "unique expected"; break; - case 21: s = "extends expected"; break; - case 22: s = "complete expected"; break; - case 23: s = "function expected"; break; - case 24: s = "returns expected"; break; - case 25: s = "{ expected"; break; - case 26: s = "} expected"; break; - case 27: s = "axiom expected"; break; - case 28: s = "type expected"; break; - case 29: s = "= expected"; break; - case 30: s = "procedure expected"; break; - case 31: s = "implementation expected"; break; - case 32: s = "modifies expected"; break; - case 33: s = "free expected"; break; - case 34: s = "requires expected"; break; - case 35: s = "ensures expected"; break; - case 36: s = "{{ expected"; break; - case 37: s = "}} 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 = ":= expected"; break; - case 50: s = "call expected"; break; - case 51: s = "forall expected"; break; - case 52: s = "<==> expected"; break; - case 53: s = "\\u21d4 expected"; break; - case 54: s = "==> expected"; break; - case 55: s = "\\u21d2 expected"; break; - case 56: s = "<== expected"; break; - case 57: s = "\\u21d0 expected"; break; - case 58: s = "&& expected"; break; - case 59: s = "\\u2227 expected"; break; - case 60: s = "|| expected"; break; - case 61: s = "\\u2228 expected"; break; - case 62: s = "== expected"; break; - case 63: s = "<= expected"; break; - case 64: s = ">= expected"; break; - case 65: s = "!= expected"; break; - case 66: s = "<: expected"; break; - case 67: s = "\\u2260 expected"; break; - case 68: s = "\\u2264 expected"; break; - case 69: s = "\\u2265 expected"; break; - case 70: s = "++ expected"; break; - case 71: s = "+ expected"; break; - case 72: s = "- expected"; break; - case 73: s = "/ expected"; break; - case 74: s = "% expected"; break; - case 75: s = "! expected"; break; - case 76: s = "\\u00ac expected"; break; - case 77: s = "false expected"; break; - case 78: s = "true expected"; break; - case 79: s = "old expected"; break; - case 80: s = "then expected"; break; - case 81: s = "\\u2200 expected"; break; - case 82: s = "exists expected"; break; - case 83: s = "\\u2203 expected"; break; - case 84: s = "lambda expected"; break; - case 85: s = "\\u03bb expected"; break; - case 86: s = ":: expected"; break; - case 87: s = "\\u2022 expected"; break; + case 6: s = "\"var\" expected"; break; + case 7: s = "\";\" 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 = "\"where\" expected"; break; + case 13: s = "\"int\" expected"; break; + case 14: s = "\"bool\" expected"; break; + case 15: s = "\"[\" expected"; break; + case 16: s = "\"]\" expected"; break; + case 17: s = "\"<\" expected"; break; + case 18: s = "\">\" expected"; break; + case 19: s = "\"const\" expected"; break; + case 20: s = "\"unique\" expected"; break; + case 21: s = "\"extends\" expected"; break; + case 22: s = "\"complete\" expected"; break; + case 23: s = "\"function\" expected"; break; + case 24: s = "\"returns\" expected"; break; + case 25: s = "\"{\" expected"; break; + case 26: s = "\"}\" expected"; break; + case 27: s = "\"axiom\" expected"; break; + case 28: s = "\"type\" expected"; break; + case 29: s = "\"=\" expected"; break; + case 30: s = "\"procedure\" expected"; break; + case 31: s = "\"implementation\" expected"; break; + case 32: s = "\"modifies\" expected"; break; + case 33: s = "\"free\" expected"; break; + case 34: s = "\"requires\" expected"; break; + case 35: s = "\"ensures\" expected"; break; + case 36: s = "\"{{\" expected"; break; + case 37: s = "\"}}\" 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 = "\":=\" expected"; break; + case 50: s = "\"call\" expected"; break; + case 51: s = "\"forall\" expected"; break; + case 52: s = "\"<==>\" expected"; break; + case 53: s = "\"\\u21d4\" expected"; break; + case 54: s = "\"==>\" expected"; break; + case 55: s = "\"\\u21d2\" expected"; break; + case 56: s = "\"<==\" expected"; break; + case 57: s = "\"\\u21d0\" expected"; break; + case 58: s = "\"&&\" expected"; break; + case 59: s = "\"\\u2227\" expected"; break; + case 60: s = "\"||\" expected"; break; + case 61: s = "\"\\u2228\" expected"; break; + case 62: s = "\"==\" expected"; break; + case 63: s = "\"<=\" expected"; break; + case 64: s = "\">=\" expected"; break; + case 65: s = "\"!=\" expected"; break; + case 66: s = "\"<:\" expected"; break; + case 67: s = "\"\\u2260\" expected"; break; + case 68: s = "\"\\u2264\" expected"; break; + case 69: s = "\"\\u2265\" expected"; break; + case 70: s = "\"++\" expected"; break; + case 71: s = "\"+\" expected"; break; + case 72: s = "\"-\" expected"; break; + case 73: s = "\"/\" expected"; break; + case 74: s = "\"%\" expected"; break; + case 75: s = "\"!\" expected"; break; + case 76: s = "\"\\u00ac\" expected"; break; + case 77: s = "\"false\" expected"; break; + case 78: s = "\"true\" expected"; break; + case 79: s = "\"old\" expected"; break; + case 80: s = "\"then\" expected"; break; + case 81: s = "\"\\u2200\" expected"; break; + case 82: s = "\"exists\" expected"; break; + case 83: s = "\"\\u2203\" expected"; break; + case 84: s = "\"lambda\" expected"; break; + case 85: s = "\"\\u03bb\" expected"; break; + case 86: s = "\"::\" expected"; break; + case 87: s = "\"\\u2022\" expected"; break; case 88: s = "??? expected"; break; case 89: s = "invalid Function"; break; case 90: s = "invalid Function"; break; @@ -2082,30 +2170,42 @@ out QKeyValue kv, out Trigger trig, out Expr! body) { default: s = "error " + n; break; } - Console.WriteLine(s); - } - - static 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,T,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,T,x,x, x,x,x,x, T,x,x,x, x,T,T,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, - {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,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,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x}, - {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,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,T,T, T,x,T,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,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,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, T,x,x,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,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,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,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,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,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,T,T,T, x,x,x,x, x,x,x,x, x,x}, - {x,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,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, T,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x}, - {x,T,T,T, T,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,x,x,x, x,x,x,x, 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,T,T, x,x,x,x, x,x,x,x, x,x} + //errorStream.WriteLine(errMsgFormat, line, col, s); + errorStream.WriteLine(s); + count++; + } - }; + public void SemErr (int line, int col, string! s) { + errorStream.WriteLine(errMsgFormat, line, col, s); + count++; + } - [Microsoft.Contracts.Verify(false)] - static Parser() {} -} // end Parser + public void SemErr (string filename, int line, int col, string! s) { + errorStream.WriteLine(errMsgFormat4, filename, line, col, s); + count++; + } + + public void SemErr (string s) { + errorStream.WriteLine(s); + count++; + } + + public void SemErr(IToken! tok, string! msg) { // semantic errors + SemErr(tok.filename, tok.line, tok.col, msg); + } + + public void Warning (int line, int col, string s) { + errorStream.WriteLine(errMsgFormat, line, col, s); + } + + public void Warning(string s) { + errorStream.WriteLine(s); + } +} // Errors + + +public class FatalError: Exception { + public FatalError(string m): base(m) {} +} -} // end namespace +} \ No newline at end of file diff --git a/Source/Core/ParserHelper.ssc b/Source/Core/ParserHelper.ssc new file mode 100644 index 00000000..ee01880a --- /dev/null +++ b/Source/Core/ParserHelper.ssc @@ -0,0 +1,116 @@ +using System.Text; +using System.Collections.Generic; +using System.IO; +namespace Microsoft.Boogie { +public static class ParserHelper { + struct ReadState { + public bool hasSeenElse; + public bool mayStillIncludeAnotherAlternative; + public ReadState(bool hasSeenElse, bool mayStillIncludeAnotherAlternative) { + this.hasSeenElse = hasSeenElse; + this.mayStillIncludeAnotherAlternative = mayStillIncludeAnotherAlternative; + } + } + // "arg" is assumed to be trimmed + private static bool IfdefConditionSaysToInclude(string! arg, List! defines) { + bool sense = true; + while (arg.StartsWith("!")) { + sense = !sense; + arg = arg.Substring(1).TrimStart(); + } + return defines.Contains(arg) == sense; + } + + public static string! Fill(FileStream! fileStream, List! defines) { + StreamReader! reader = new StreamReader(fileStream); + return Fill(reader, defines); + } + public static string! Fill(TextReader! reader, List! defines) { + StringBuilder sb = new StringBuilder(); + List! readState = new List(); // readState.Count is the current nesting level of #if's + int ignoreCutoff = -1; // -1 means we're not ignoring; for 0<=n, n means we're ignoring because of something at nesting level n + while (true) + //invariant -1 <= ignoreCutoff && ignoreCutoff < readState.Count; + { + string s = reader.ReadLine(); + if (s == null) { + if (readState.Count != 0) { + sb.AppendLine("#MalformedInput: missing #endif"); + } + break; + } + string t = s.Trim(); + if (t.StartsWith("#if")) { + ReadState rs = new ReadState(false, false); + if (ignoreCutoff != -1) { + // we're already in a state of ignoring, so continue to ignore + } else if (IfdefConditionSaysToInclude(t.Substring(3).TrimStart(), defines)) { + // include this branch + } else { + ignoreCutoff = readState.Count; // start ignoring + rs.mayStillIncludeAnotherAlternative = true; // allow some later "elsif" or "else" branch to be included + } + readState.Add(rs); + sb.AppendLine(); // ignore the #if line + + } else if (t.StartsWith("#elsif")) { + ReadState rs; + if (readState.Count == 0 || (rs = readState[readState.Count-1]).hasSeenElse) { + sb.AppendLine("#MalformedInput: misplaced #elsif"); // malformed input + break; + } + if (ignoreCutoff == -1) { + // we had included the previous branch + //assert !rs.mayStillIncludeAnotherAlternative; + ignoreCutoff = readState.Count-1; // start ignoring + } else if (rs.mayStillIncludeAnotherAlternative && IfdefConditionSaysToInclude(t.Substring(6).TrimStart(), defines)) { + // include this branch, but no subsequent branch at this level + ignoreCutoff = -1; + rs.mayStillIncludeAnotherAlternative = false; + readState[readState.Count-1] = rs; + } + sb.AppendLine(); // ignore the #elsif line + + } else if (t == "#else") { + ReadState rs; + if (readState.Count == 0 || (rs = readState[readState.Count-1]).hasSeenElse) { + sb.AppendLine("#MalformedInput: misplaced #else"); // malformed input + break; + } + rs.hasSeenElse = true; + if (ignoreCutoff == -1) { + // we had included the previous branch + //assert !rs.mayStillIncludeAnotherAlternative; + ignoreCutoff = readState.Count-1; // start ignoring + } else if (rs.mayStillIncludeAnotherAlternative) { + // include this branch + ignoreCutoff = -1; + rs.mayStillIncludeAnotherAlternative = false; + } + readState[readState.Count-1] = rs; + sb.AppendLine(); // ignore the #else line + + } else if (t == "#endif") { + if (readState.Count == 0) { + sb.AppendLine("#MalformedInput: misplaced #endif"); // malformed input + break; + } + readState.RemoveAt(readState.Count-1); // pop + if (ignoreCutoff == readState.Count) { + // we had ignored the branch that ends here; so, now we start including again + ignoreCutoff = -1; + } + sb.AppendLine(); // ignore the #endif line + + } else if (ignoreCutoff == -1) { + sb.AppendLine(s); // included line + + } else { + sb.AppendLine(); // ignore the line + } + } + + return sb.ToString(); + } +} +} \ No newline at end of file diff --git a/Source/Core/Scanner.ssc b/Source/Core/Scanner.ssc index a6f2c0a4..3765574e 100644 --- a/Source/Core/Scanner.ssc +++ b/Source/Core/Scanner.ssc @@ -1,3 +1,4 @@ + using System; using System.IO; using System.Collections; @@ -5,7 +6,6 @@ using System.Collections.Generic; using System.Text; using Microsoft.Contracts; - namespace Microsoft.Boogie { [Immutable] @@ -19,26 +19,30 @@ namespace Microsoft.Boogie { bool IsValid { get; } } - + [Immutable] public class Token : IToken { - int _kind; // token kind + public int _kind; // token kind string _filename; // token file - int _pos; // token position in the source text (starting at 0) - int _col; // token column (starting at 0) - int _line; // token line (starting at 1) - string/*!*/ _val = "foo"; // token value - + public int _pos; // token position in the source text (starting at 0) + public int _col; // token column (starting at 1) + public int _line; // token line (starting at 1) + public string/*!*/ _val; // token value + public Token next; // ML 2005-03-11 Tokens are kept in linked list + public static IToken! NoToken = new Token(); - public Token(); + public Token() { + this._val = "anything so that it is nonnull"; + } public Token(int linenum, int colnum) { this._line = linenum; this._col = colnum; + this._val = "anything so that it is nonnull"; base(); } - public int kind { + public int kind { get { return this._kind; } set { this._kind = value; } } @@ -47,7 +51,7 @@ namespace Microsoft.Boogie { get { return this._filename; } set { this._filename = value; } } - + public int pos{ get { return this._pos; } set { this._pos = value; } @@ -67,394 +71,435 @@ namespace Microsoft.Boogie { get { return this._val; } set { this._val = value; } } - + public bool IsValid { get { return this._filename != null; } } - } + } -namespace BoogiePL { - -using Microsoft.Boogie; - +//----------------------------------------------------------------------------------- +// Buffer +//----------------------------------------------------------------------------------- public class Buffer { - static string/*!*/ buf; - static int bufLen; - static int pos; - public const int eof = '\uffff'; + // This Buffer supports the following cases: + // 1) seekable stream (file) + // a) whole stream in buffer + // b) part of stream in buffer + // 2) non seekable stream (network, console) - public static void Fill(TextReader! reader) { - List defines = new List(); - Fill(reader, defines); - } - - struct ReadState { - public bool hasSeenElse; - public bool mayStillIncludeAnotherAlternative; - public ReadState(bool hasSeenElse, bool mayStillIncludeAnotherAlternative) { - this.hasSeenElse = hasSeenElse; - this.mayStillIncludeAnotherAlternative = mayStillIncludeAnotherAlternative; - } - } - - public static void Fill(TextReader! reader, List! defines) { - StringBuilder sb = new StringBuilder(); - List! readState = new List(); // readState.Count is the current nesting level of #if's - int ignoreCutoff = -1; // -1 means we're not ignoring; for 0<=n, n means we're ignoring because of something at nesting level n - while (true) - invariant -1 <= ignoreCutoff && ignoreCutoff < readState.Count; - { - string s = reader.ReadLine(); - if (s == null) { - if (readState.Count != 0) { - sb.AppendLine("#MalformedInput: missing #endif"); - } - break; - } - string t = s.Trim(); - if (t.StartsWith("#if")) { - ReadState rs = new ReadState(false, false); - if (ignoreCutoff != -1) { - // we're already in a state of ignoring, so continue to ignore - } else if (IfdefConditionSaysToInclude(t.Substring(3).TrimStart(), defines)) { - // include this branch - } else { - ignoreCutoff = readState.Count; // start ignoring - rs.mayStillIncludeAnotherAlternative = true; // allow some later "elsif" or "else" branch to be included - } - readState.Add(rs); - sb.AppendLine(); // ignore the #if line - - } else if (t.StartsWith("#elsif")) { - ReadState rs; - if (readState.Count == 0 || (rs = readState[readState.Count-1]).hasSeenElse) { - sb.AppendLine("#MalformedInput: misplaced #elsif"); // malformed input - break; - } - if (ignoreCutoff == -1) { - // we had included the previous branch - assert !rs.mayStillIncludeAnotherAlternative; - ignoreCutoff = readState.Count-1; // start ignoring - } else if (rs.mayStillIncludeAnotherAlternative && IfdefConditionSaysToInclude(t.Substring(6).TrimStart(), defines)) { - // include this branch, but no subsequent branch at this level - ignoreCutoff = -1; - rs.mayStillIncludeAnotherAlternative = false; - readState[readState.Count-1] = rs; - } - sb.AppendLine(); // ignore the #elsif line - - } else if (t == "#else") { - ReadState rs; - if (readState.Count == 0 || (rs = readState[readState.Count-1]).hasSeenElse) { - sb.AppendLine("#MalformedInput: misplaced #else"); // malformed input - break; - } - rs.hasSeenElse = true; - if (ignoreCutoff == -1) { - // we had included the previous branch - assert !rs.mayStillIncludeAnotherAlternative; - ignoreCutoff = readState.Count-1; // start ignoring - } else if (rs.mayStillIncludeAnotherAlternative) { - // include this branch - ignoreCutoff = -1; - rs.mayStillIncludeAnotherAlternative = false; - } - readState[readState.Count-1] = rs; - sb.AppendLine(); // ignore the #else line - - } else if (t == "#endif") { - if (readState.Count == 0) { - sb.AppendLine("#MalformedInput: misplaced #endif"); // malformed input - break; - } - readState.RemoveAt(readState.Count-1); // pop - if (ignoreCutoff == readState.Count) { - // we had ignored the branch that ends here; so, now we start including again - ignoreCutoff = -1; - } - sb.AppendLine(); // ignore the #endif line - - } else if (ignoreCutoff == -1) { - sb.AppendLine(s); // included line - - } else { - sb.AppendLine(); // ignore the line - } - } - - Fill(sb.ToString()); - } + public const int EOF = 65535 + 1; // char.MaxValue + 1; + const int MIN_BUFFER_LENGTH = 1024; // 1KB + const int MAX_BUFFER_LENGTH = MIN_BUFFER_LENGTH * 64; // 64KB + byte[]! buf; // input buffer + int bufStart; // position of first byte in buffer relative to input stream + int bufLen; // length of buffer + int fileLen; // length of input stream (may change if the stream is no file) + int bufPos; // current position in buffer + Stream! stream; // input stream (seekable) + bool isUserStream; // was the stream opened by the user? + + [NotDelayed] + public Buffer (Stream! s, bool isUserStream) { + stream = s; this.isUserStream = isUserStream; + + int fl, bl; + if (s.CanSeek) { + fl = (int) s.Length; + bl = fl < MAX_BUFFER_LENGTH ? fl : MAX_BUFFER_LENGTH; // Math.Min(fileLen, MAX_BUFFER_LENGTH); + bufStart = Int32.MaxValue; // nothing in the buffer so far + } else { + fl = bl = bufStart = 0; + } - // "arg" is assumed to be trimmed - private static bool IfdefConditionSaysToInclude(string! arg, List! defines) { - bool sense = true; - while (arg.StartsWith("!")) { - sense = !sense; - arg = arg.Substring(1).TrimStart(); - } - return defines.Contains(arg) == sense; - } - - public static void Fill(string! text) { - buf = text; - bufLen = buf.Length; - pos = 0; - } - - public static int Read() { - if (pos < bufLen) { - return buf[pos++]; - } else { - return eof; - } - } + buf = new byte[(bl>0) ? bl : MIN_BUFFER_LENGTH]; + fileLen = fl; bufLen = bl; + base(); + if (fileLen > 0) Pos = 0; // setup buffer to position 0 (start) + else bufPos = 0; // index 0 is already after the file, thus Pos = 0 is invalid + if (bufLen == fileLen && s.CanSeek) Close(); + } + + protected Buffer(Buffer! b) { // called in UTF8Buffer constructor + buf = b.buf; + bufStart = b.bufStart; + bufLen = b.bufLen; + fileLen = b.fileLen; + bufPos = b.bufPos; + stream = b.stream; + // keep destructor from closing the stream + //b.stream = null; + isUserStream = b.isUserStream; + // keep destructor from closing the stream + b.isUserStream = true; + } - public static string/*!*/ ReadToEOL() { - int x = buf.IndexOf('\n', pos); - if (x == -1) { - string s = buf.Substring(pos); - pos = buf.Length; - return s; - } else { - string s = buf.Substring(pos, x+1 - pos); // also include the '\n' - pos = x+1; - return s; - } - } + ~Buffer() { Close(); } + + protected void Close() { + if (!isUserStream && stream != null) { + stream.Close(); + //stream = null; + } + } + + public virtual int Read () { + if (bufPos < bufLen) { + return buf[bufPos++]; + } else if (Pos < fileLen) { + Pos = Pos; // shift buffer start to Pos + return buf[bufPos++]; + } else if (stream != null && !stream.CanSeek && ReadNextStreamChunk() > 0) { + return buf[bufPos++]; + } else { + return EOF; + } + } - public static int Pos { - get { return pos; } - set { - if (value < 0) pos = 0; else if (value >= bufLen) pos = bufLen; else pos = value; - } - } -} + public int Peek () { + int curPos = Pos; + int ch = Read(); + Pos = curPos; + return ch; + } + + public string! GetString (int beg, int end) { + int len = 0; + char[] buf = new char[end - beg]; + int oldPos = Pos; + Pos = beg; + while (Pos < end) buf[len++] = (char) Read(); + Pos = oldPos; + return new String(buf, 0, len); + } + public int Pos { + get { return bufPos + bufStart; } + set { + if (value >= fileLen && stream != null && !stream.CanSeek) { + // Wanted position is after buffer and the stream + // is not seek-able e.g. network or console, + // thus we have to read the stream manually till + // the wanted position is in sight. + while (value >= fileLen && ReadNextStreamChunk() > 0); + } + if (value < 0 || value > fileLen) { + throw new FatalError("buffer out of bounds access, position: " + value); + } + if (value >= bufStart && value < bufStart + bufLen) { // already in buffer + bufPos = value - bufStart; + } else if (stream != null) { // must be swapped in + stream.Seek(value, SeekOrigin.Begin); + bufLen = stream.Read(buf, 0, buf.Length); + bufStart = value; bufPos = 0; + } else { + // set the position to the end of the file, Pos will return fileLen. + bufPos = fileLen - bufStart; + } + } + } + + // Read the next chunk of bytes from the stream, increases the buffer + // if needed and updates the fields fileLen and bufLen. + // Returns the number of bytes read. + private int ReadNextStreamChunk() { + int free = buf.Length - bufLen; + if (free == 0) { + // in the case of a growing input stream + // we can neither seek in the stream, nor can we + // foresee the maximum length, thus we must adapt + // the buffer size on demand. + byte[] newBuf = new byte[bufLen * 2]; + Array.Copy(buf, newBuf, bufLen); + buf = newBuf; + free = bufLen; + } + int read = stream.Read(buf, bufLen, free); + if (read > 0) { + fileLen = bufLen = (bufLen + read); + return read; + } + // end of stream reached + return 0; + } +} + +//----------------------------------------------------------------------------------- +// UTF8Buffer +//----------------------------------------------------------------------------------- +public class UTF8Buffer: Buffer { + public UTF8Buffer(Buffer! b): base(b) {} + + public override int Read() { + int ch; + do { + ch = base.Read(); + // until we find a utf8 start (0xxxxxxx or 11xxxxxx) + } while ((ch >= 128) && ((ch & 0xC0) != 0xC0) && (ch != EOF)); + if (ch < 128 || ch == EOF) { + // nothing to do, first 127 chars are the same in ascii and utf8 + // 0xxxxxxx or end of file character + } else if ((ch & 0xF0) == 0xF0) { + // 11110xxx 10xxxxxx 10xxxxxx 10xxxxxx + int c1 = ch & 0x07; ch = base.Read(); + int c2 = ch & 0x3F; ch = base.Read(); + int c3 = ch & 0x3F; ch = base.Read(); + int c4 = ch & 0x3F; + ch = (((((c1 << 6) | c2) << 6) | c3) << 6) | c4; + } else if ((ch & 0xE0) == 0xE0) { + // 1110xxxx 10xxxxxx 10xxxxxx + int c1 = ch & 0x0F; ch = base.Read(); + int c2 = ch & 0x3F; ch = base.Read(); + int c3 = ch & 0x3F; + ch = (((c1 << 6) | c2) << 6) | c3; + } else if ((ch & 0xC0) == 0xC0) { + // 110xxxxx 10xxxxxx + int c1 = ch & 0x1F; ch = base.Read(); + int c2 = ch & 0x3F; + ch = (c1 << 6) | c2; + } + return ch; + } +} + +//----------------------------------------------------------------------------------- +// Scanner +//----------------------------------------------------------------------------------- public class Scanner { - const char EOF = '\0'; - const char CR = '\r'; - const char LF = '\n'; - [Microsoft.Contracts.Verify(false)] + const char EOL = '\n'; + const int eofSym = 0; /* pdt */ + const int maxT = 88; + const int noSym = 88; + + + public Buffer! buffer; // scanner buffer + + Token! t; // current token + int ch; // current input character + int pos; // byte position of current character + int col; // column number of current character + int line; // line number of current character + int oldEols; // EOLs that appeared in a comment; + static readonly Hashtable! start; // maps first token character to start state + + Token! tokens; // list of tokens already peeked (first token is a dummy) + Token! pt; // current peek token + + char[]! tval = new char[128]; // text of current token + int tlen; // length of current token + + private string! Filename; + private Errors! errorHandler; + static Scanner() { - start[0] = 58; - start[33] = 41; - start[34] = 6; - start[35] = 2; - start[36] = 2; - start[37] = 51; - start[38] = 34; - start[39] = 2; - start[40] = 11; - start[41] = 12; - start[42] = 24; - start[43] = 47; - start[44] = 14; - start[45] = 49; - start[46] = 2; - start[47] = 50; - start[48] = 9; - start[49] = 9; - start[50] = 9; - start[51] = 9; - start[52] = 9; - start[53] = 9; - start[54] = 9; - start[55] = 9; - start[56] = 9; - start[57] = 9; - start[58] = 13; - start[59] = 10; - start[60] = 17; - start[61] = 21; - start[62] = 18; - start[63] = 2; - start[65] = 2; - start[66] = 2; - start[67] = 2; - start[68] = 2; - start[69] = 2; - start[70] = 2; - start[71] = 2; - start[72] = 2; - start[73] = 2; - start[74] = 2; - start[75] = 2; - start[76] = 2; - start[77] = 2; - start[78] = 2; - start[79] = 2; - start[80] = 2; - start[81] = 2; - start[82] = 2; - start[83] = 2; - start[84] = 2; - start[85] = 2; - start[86] = 2; - start[87] = 2; - start[88] = 2; - start[89] = 2; - start[90] = 2; - start[91] = 15; - start[92] = 1; - start[93] = 16; - start[94] = 2; - start[95] = 2; - start[96] = 2; - start[97] = 2; - start[98] = 2; - start[99] = 2; - start[100] = 2; - start[101] = 2; - start[102] = 2; - start[103] = 2; - start[104] = 2; - start[105] = 2; - start[106] = 2; - start[107] = 2; - start[108] = 2; - start[109] = 2; - start[110] = 2; - start[111] = 2; - start[112] = 2; - start[113] = 2; - start[114] = 2; - start[115] = 2; - start[116] = 2; - start[117] = 2; - start[118] = 2; - start[119] = 2; - start[120] = 2; - start[121] = 2; - start[122] = 2; - start[123] = 19; - start[124] = 37; - start[125] = 20; - start[126] = 2; - start[172] = 52; - start[955] = 55; - start[8226] = 57; - start[8656] = 33; - start[8658] = 32; - start[8660] = 29; - start[8704] = 53; - start[8707] = 54; - start[8743] = 36; - start[8744] = 39; - start[8800] = 44; - start[8804] = 45; - start[8805] = 46; + start = new Hashtable(128); + for (int i = 35; i <= 36; ++i) start[i] = 2; + for (int i = 39; i <= 39; ++i) start[i] = 2; + for (int i = 46; i <= 46; ++i) start[i] = 2; + for (int i = 63; i <= 63; ++i) start[i] = 2; + 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] = 9; + for (int i = 34; i <= 34; ++i) start[i] = 6; + start[92] = 1; + start[59] = 10; + start[40] = 11; + start[41] = 12; + start[58] = 47; + start[44] = 13; + start[91] = 14; + start[93] = 15; + start[60] = 48; + start[62] = 49; + start[123] = 50; + start[125] = 51; + start[61] = 52; + start[42] = 18; + start[8660] = 21; + start[8658] = 23; + start[8656] = 24; + start[38] = 25; + start[8743] = 27; + start[124] = 28; + start[8744] = 30; + start[33] = 53; + start[8800] = 34; + start[8804] = 35; + start[8805] = 36; + start[43] = 54; + start[45] = 38; + start[47] = 39; + start[37] = 40; + start[172] = 41; + start[8704] = 42; + start[8707] = 43; + start[955] = 44; + start[8226] = 46; + start[Buffer.EOF] = -1; + } - const int noSym = 88; - static short[] start = new short[16385]; - - - static Token/*!*/ t; // current token - static char ch; // current input character - static int pos; // column number of current character - static int line; // line number of current character - static int lineStart; // start position of current line - static Queue! oldEols; // EOLs that appeared in a comment; - static BitArray/*!*/ ignore; // set of characters to be ignored by the scanner - static string Filename; - - /// - ///Initializes the scanner. Note: first fill the Buffer. - /// - ///File name used for error reporting - public static void Init (string filename) { - Filename = filename; - pos = -1; line = 1; lineStart = 0; - oldEols = new Queue(); - NextCh(); - ignore = new BitArray(16384); - ignore[9] = true; ignore[10] = true; ignore[13] = true; ignore[32] = true; - - } - - private static void NextCh() { - if (oldEols.Count > 0) { - ch = (char) ((!)oldEols.Dequeue()); - } else { - while (true) { - ch = (char)Buffer.Read(); pos++; - if (ch == Buffer.eof) { - ch = EOF; - } else if (ch == LF) { - line++; - lineStart = pos + 1; - - } else if (ch == '#' && pos == lineStart) { - int prLine = line; - int prColumn = pos - lineStart; // which is 0 - - string hashLine = Buffer.ReadToEOL(); pos += hashLine.Length; - line++; - lineStart = pos + 1; - - hashLine = hashLine.TrimEnd(null); - if (hashLine.StartsWith("line ") || hashLine == "line") { - // parse #line pragma: #line num [filename] - string h = hashLine.Substring(4).TrimStart(null); - int x = h.IndexOf(' '); - if (x == -1) { - x = h.Length; // this will be convenient below when we look for a filename - } - try { - int li = int.Parse(h.Substring(0, x)); - - h = h.Substring(x).Trim(); - - // act on #line - line = li; - if (h.Length != 0) { - // a filename was specified - Filename = h; - } - continue; // successfully parsed and acted on the #line pragma - - } catch (FormatException) { - // just fall down through to produce an error message - } - Errors.SemErr(Filename, prLine, prColumn, "Malformed (#line num [filename]) pragma: #" + hashLine); - continue; - } - - Errors.SemErr(Filename, prLine, prColumn, "Unrecognized pragma: #" + hashLine); - continue; - } - return; - } - } - } - - - static bool Comment0() { - int level = 1, line0 = line, lineStart0 = lineStart; + + [NotDelayed] + public Scanner (string! fileName, Errors! errorHandler) { + this.errorHandler = errorHandler; + pt = tokens = new Token(); // first token is a dummy + t = new Token(); // dummy because t is a non-null field + try { + Stream stream = new FileStream(fileName, FileMode.Open, FileAccess.Read, FileShare.Read); + buffer = new Buffer(stream, false); + Filename = fileName; + base(); + Init(); + } catch (IOException) { + throw new FatalError("Cannot open file " + fileName); + } + } + + [NotDelayed] + public Scanner (Stream! s, Errors! errorHandler, string! fileName) { + pt = tokens = new Token(); // first token is a dummy + t = new Token(); // dummy because t is a non-null field + buffer = new Buffer(s, true); + this.errorHandler = errorHandler; + this.Filename = fileName; + base(); + Init(); + } + + void Init() { + pos = -1; line = 1; col = 0; + oldEols = 0; + NextCh(); + if (ch == 0xEF) { // check optional byte order mark for UTF-8 + NextCh(); int ch1 = ch; + NextCh(); int ch2 = ch; + if (ch1 != 0xBB || ch2 != 0xBF) { + throw new FatalError(String.Format("illegal byte order mark: EF {0,2:X} {1,2:X}", ch1, ch2)); + } + buffer = new UTF8Buffer(buffer); col = 0; + NextCh(); + } + pt = tokens = new Token(); // first token is a dummy + } + + string! ReadToEOL(){ + int p = buffer.Pos; + int ch = buffer.Read(); + // replace isolated '\r' by '\n' in order to make + // eol handling uniform across Windows, Unix and Mac + if (ch == '\r' && buffer.Peek() != '\n') ch = EOL; + while (ch != EOL && ch != Buffer.EOF){ + ch = buffer.Read(); + // replace isolated '\r' by '\n' in order to make + // eol handling uniform across Windows, Unix and Mac + if (ch == '\r' && buffer.Peek() != '\n') ch = EOL; + } + string! s = buffer.GetString(p, buffer.Pos); + return s; + } + + void NextCh() { + if (oldEols > 0) { ch = EOL; oldEols--; } + else { +// pos = buffer.Pos; +// ch = buffer.Read(); col++; +// // replace isolated '\r' by '\n' in order to make +// // eol handling uniform across Windows, Unix and Mac +// if (ch == '\r' && buffer.Peek() != '\n') ch = EOL; +// if (ch == EOL) { line++; col = 0; } + + while (true) { + pos = buffer.Pos; + ch = buffer.Read(); col++; + // replace isolated '\r' by '\n' in order to make + // eol handling uniform across Windows, Unix and Mac + if (ch == '\r' && buffer.Peek() != '\n') ch = EOL; + if (ch == EOL) { + line++; col = 0; + } else if (ch == '#' && col == 1) { + int prLine = line; + int prColumn = 0; + + string! hashLine = ReadToEOL(); + col = 0; + line++; + + hashLine = hashLine.TrimEnd(null); + if (hashLine.StartsWith("line ") || hashLine == "line") { + // parse #line pragma: #line num [filename] + string h = hashLine.Substring(4).TrimStart(null); + int x = h.IndexOf(' '); + if (x == -1) { + x = h.Length; // this will be convenient below when we look for a filename + } + try { + int li = int.Parse(h.Substring(0, x)); + + h = h.Substring(x).Trim(); + + // act on #line + line = li; + if (h.Length != 0) { + // a filename was specified + Filename = h; + } + continue; // successfully parsed and acted on the #line pragma + + } catch (FormatException) { + // just fall down through to produce an error message + } + this.errorHandler.SemErr(Filename, prLine, prColumn, "Malformed (#line num [filename]) pragma: #" + hashLine); + continue; + } + + this.errorHandler.SemErr(Filename, prLine, prColumn, "Unrecognized pragma: #" + hashLine); + continue; + } + return; + } + + + } + + } + + void AddCh() { + if (tlen >= tval.Length) { + char[] newBuf = new char[2 * tval.Length]; + Array.Copy(tval, 0, newBuf, 0, tval.Length); + tval = newBuf; + } + if (ch != Buffer.EOF) { + tval[tlen++] = (char) ch; + NextCh(); + } + } + + + + bool Comment0() { + int level = 1, pos0 = pos, line0 = line, col0 = col; NextCh(); if (ch == '/') { NextCh(); for(;;) { if (ch == 10) { level--; - if (level == 0) { - while(line0 < line) {oldEols.Enqueue('\r'); oldEols.Enqueue('\n'); line0++;} - NextCh(); return true; - } + if (level == 0) { oldEols = line - line0; NextCh(); return true; } NextCh(); - } else if (ch == EOF) return false; + } else if (ch == Buffer.EOF) return false; else NextCh(); } } else { - if (ch==CR) {line--; lineStart = lineStart0;} - pos = pos - 2; Buffer.Pos = pos+1; NextCh(); + buffer.Pos = pos0; NextCh(); line = line0; col = col0; } return false; } - - static bool Comment1() { - int level = 1, line0 = line, lineStart0 = lineStart; + + bool Comment1() { + int level = 1, pos0 = pos, line0 = line, col0 = col; NextCh(); if (ch == '*') { NextCh(); @@ -463,10 +508,7 @@ public class Scanner { NextCh(); if (ch == '/') { level--; - if (level == 0) { - while(line0 < line) {oldEols.Enqueue('\r'); oldEols.Enqueue('\n'); line0++;} - NextCh(); return true; - } + if (level == 0) { oldEols = line - line0; NextCh(); return true; } NextCh(); } } else if (ch == '/') { @@ -474,19 +516,18 @@ public class Scanner { if (ch == '*') { level++; NextCh(); } - } else if (ch == EOF) return false; + } else if (ch == Buffer.EOF) return false; else NextCh(); } } else { - if (ch==CR) {line--; lineStart = lineStart0;} - pos = pos - 2; Buffer.Pos = pos+1; NextCh(); + buffer.Pos = pos0; NextCh(); line = line0; col = col0; } return false; } - - static void CheckLiteral() { - switch (t.val) { + + void CheckLiteral() { + switch (t.val) { case "var": t.kind = 6; break; case "where": t.kind = 12; break; case "int": t.kind = 13; break; @@ -524,197 +565,229 @@ public class Scanner { case "exists": t.kind = 82; break; case "lambda": t.kind = 84; break; default: break; + } + } - } - } - - public static Token/*!*/ Scan() { - while (ignore[ch]) { NextCh(); } - if (ch == '/' && Comment0() || ch == '/' && Comment1() ) return Scan(); - t = new Token(); - t.pos = pos; t.col = pos - lineStart + 1; t.line = line; t.filename = Filename; - int state = (/*^ (!) ^*/ start)[ch]; - StringBuilder buf = new StringBuilder(16); - buf.Append(ch); NextCh(); - - switch (state) { - case 0: {t.kind = noSym; goto done;} // NextCh already done + Token! NextToken() { + while (ch == ' ' || + ch >= 9 && ch <= 10 || ch == 13 + ) NextCh(); + if (ch == '/' && Comment0() ||ch == '/' && Comment1()) return NextToken(); + int recKind = noSym; + int recEnd = pos; + t = new Token(); + t.pos = pos; t.col = col; t.line = line; + t.filename = this.Filename; + int state; + if (start.ContainsKey(ch)) { state = (int) (!) start[ch]; } + else { state = 0; } + tlen = 0; AddCh(); + + switch (state) { + case -1: { t.kind = eofSym; break; } // NextCh already done + case 0: { + if (recKind != noSym) { + tlen = recEnd - t.pos; + SetScannerBehindT(); + } + t.kind = recKind; break; + } // NextCh already done case 1: - if ((ch >= '#' && ch <= '$' || ch == 39 || ch == '.' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch >= '^' && ch <= 'z' || ch == '~')) {buf.Append(ch); NextCh(); goto case 2;} - else {t.kind = noSym; goto done;} + if (ch >= '#' && ch <= '$' || ch == 39 || ch == '.' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch >= '^' && ch <= 'z' || ch == '~') {AddCh(); goto case 2;} + else {goto case 0;} case 2: - if ((ch >= '#' && ch <= '$' || ch == 39 || ch == '.' || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch >= '^' && ch <= 'z' || ch == '~')) {buf.Append(ch); NextCh(); goto case 2;} - else {t.kind = 1; t.val = buf.ToString(); CheckLiteral(); return t;} + recEnd = pos; recKind = 1; + if (ch >= '#' && ch <= '$' || ch == 39 || ch == '.' || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch >= '^' && ch <= 'z' || ch == '~') {AddCh(); goto case 2;} + else {t.kind = 1; t.val = new String(tval, 0, tlen); CheckLiteral(); return t;} case 3: - if (ch == 'v') {buf.Append(ch); NextCh(); goto case 4;} - else {t.kind = noSym; goto done;} + if (ch == 'v') {AddCh(); goto case 4;} + else {goto case 0;} case 4: - if ((ch >= '0' && ch <= '9')) {buf.Append(ch); NextCh(); goto case 5;} - else {t.kind = noSym; goto done;} + if (ch >= '0' && ch <= '9') {AddCh(); goto case 5;} + else {goto case 0;} case 5: - if ((ch >= '0' && ch <= '9')) {buf.Append(ch); NextCh(); goto case 5;} - else {t.kind = 2; goto done;} + recEnd = pos; recKind = 2; + if (ch >= '0' && ch <= '9') {AddCh(); goto case 5;} + else {t.kind = 2; break;} case 6: - if ((ch == '"')) {buf.Append(ch); NextCh(); goto case 7;} - else if ((ch >= ' ' && ch <= '!' || ch >= '#' && ch <= '~')) {buf.Append(ch); NextCh(); goto case 6;} - else {t.kind = noSym; goto done;} + if (ch == '"') {AddCh(); goto case 7;} + else if (ch >= ' ' && ch <= '!' || ch >= '#' && ch <= '~') {AddCh(); goto case 6;} + else {goto case 0;} case 7: - {t.kind = 4; goto done;} + {t.kind = 4; break;} case 8: - if ((ch >= '0' && ch <= '9')) {buf.Append(ch); NextCh(); goto case 8;} - else {t.kind = 5; goto done;} + recEnd = pos; recKind = 5; + if (ch >= '0' && ch <= '9') {AddCh(); goto case 8;} + else {t.kind = 5; break;} case 9: - if ((ch >= '0' && ch <= '9')) {buf.Append(ch); NextCh(); goto case 9;} - else if (ch == 'b') {buf.Append(ch); NextCh(); goto case 3;} - else if (ch == '.') {buf.Append(ch); NextCh(); goto case 8;} - else {t.kind = 3; goto done;} + recEnd = pos; recKind = 3; + if (ch >= '0' && ch <= '9') {AddCh(); goto case 9;} + else if (ch == 'b') {AddCh(); goto case 3;} + else if (ch == '.') {AddCh(); goto case 8;} + else {t.kind = 3; break;} case 10: - {t.kind = 7; goto done;} + {t.kind = 7; break;} case 11: - {t.kind = 8; goto done;} + {t.kind = 8; break;} case 12: - {t.kind = 9; goto done;} + {t.kind = 9; break;} case 13: - if (ch == '=') {buf.Append(ch); NextCh(); goto case 25;} - else if (ch == ':') {buf.Append(ch); NextCh(); goto case 56;} - else {t.kind = 10; goto done;} + {t.kind = 11; break;} case 14: - {t.kind = 11; goto done;} + {t.kind = 15; break;} case 15: - {t.kind = 15; goto done;} + {t.kind = 16; break;} case 16: - {t.kind = 16; goto done;} + {t.kind = 36; break;} case 17: - if (ch == '=') {buf.Append(ch); NextCh(); goto case 26;} - else if (ch == ':') {buf.Append(ch); NextCh(); goto case 43;} - else {t.kind = 17; goto done;} + {t.kind = 37; break;} case 18: - if (ch == '=') {buf.Append(ch); NextCh(); goto case 40;} - else {t.kind = 18; goto done;} + {t.kind = 44; break;} case 19: - if (ch == '{') {buf.Append(ch); NextCh(); goto case 22;} - else {t.kind = 25; goto done;} + {t.kind = 49; break;} case 20: - if (ch == '}') {buf.Append(ch); NextCh(); goto case 23;} - else {t.kind = 26; goto done;} + {t.kind = 52; break;} case 21: - if (ch == '=') {buf.Append(ch); NextCh(); goto case 30;} - else {t.kind = 29; goto done;} + {t.kind = 53; break;} case 22: - {t.kind = 36; goto done;} + {t.kind = 54; break;} case 23: - {t.kind = 37; goto done;} + {t.kind = 55; break;} case 24: - {t.kind = 44; goto done;} + {t.kind = 57; break;} case 25: - {t.kind = 49; goto done;} + if (ch == '&') {AddCh(); goto case 26;} + else {goto case 0;} case 26: - if (ch == '=') {buf.Append(ch); NextCh(); goto case 27;} - else {t.kind = 63; goto done;} + {t.kind = 58; break;} case 27: - if (ch == '>') {buf.Append(ch); NextCh(); goto case 28;} - else {t.kind = 56; goto done;} + {t.kind = 59; break;} case 28: - {t.kind = 52; goto done;} + if (ch == '|') {AddCh(); goto case 29;} + else {goto case 0;} case 29: - {t.kind = 53; goto done;} + {t.kind = 60; break;} case 30: - if (ch == '>') {buf.Append(ch); NextCh(); goto case 31;} - else {t.kind = 62; goto done;} + {t.kind = 61; break;} case 31: - {t.kind = 54; goto done;} + {t.kind = 64; break;} case 32: - {t.kind = 55; goto done;} + {t.kind = 65; break;} case 33: - {t.kind = 57; goto done;} + {t.kind = 66; break;} case 34: - if (ch == '&') {buf.Append(ch); NextCh(); goto case 35;} - else {t.kind = noSym; goto done;} + {t.kind = 67; break;} case 35: - {t.kind = 58; goto done;} + {t.kind = 68; break;} case 36: - {t.kind = 59; goto done;} + {t.kind = 69; break;} case 37: - if (ch == '|') {buf.Append(ch); NextCh(); goto case 38;} - else {t.kind = noSym; goto done;} + {t.kind = 70; break;} case 38: - {t.kind = 60; goto done;} + {t.kind = 72; break;} case 39: - {t.kind = 61; goto done;} + {t.kind = 73; break;} case 40: - {t.kind = 64; goto done;} + {t.kind = 74; break;} case 41: - if (ch == '=') {buf.Append(ch); NextCh(); goto case 42;} - else {t.kind = 75; goto done;} + {t.kind = 76; break;} case 42: - {t.kind = 65; goto done;} + {t.kind = 81; break;} case 43: - {t.kind = 66; goto done;} + {t.kind = 83; break;} case 44: - {t.kind = 67; goto done;} + {t.kind = 85; break;} case 45: - {t.kind = 68; goto done;} + {t.kind = 86; break;} case 46: - {t.kind = 69; goto done;} + {t.kind = 87; break;} case 47: - if (ch == '+') {buf.Append(ch); NextCh(); goto case 48;} - else {t.kind = 71; goto done;} + recEnd = pos; recKind = 10; + if (ch == '=') {AddCh(); goto case 19;} + else if (ch == ':') {AddCh(); goto case 45;} + else {t.kind = 10; break;} case 48: - {t.kind = 70; goto done;} + recEnd = pos; recKind = 17; + if (ch == '=') {AddCh(); goto case 55;} + else if (ch == ':') {AddCh(); goto case 33;} + else {t.kind = 17; break;} case 49: - {t.kind = 72; goto done;} + recEnd = pos; recKind = 18; + if (ch == '=') {AddCh(); goto case 31;} + else {t.kind = 18; break;} case 50: - {t.kind = 73; goto done;} + recEnd = pos; recKind = 25; + if (ch == '{') {AddCh(); goto case 16;} + else {t.kind = 25; break;} case 51: - {t.kind = 74; goto done;} + recEnd = pos; recKind = 26; + if (ch == '}') {AddCh(); goto case 17;} + else {t.kind = 26; break;} case 52: - {t.kind = 76; goto done;} + recEnd = pos; recKind = 29; + if (ch == '=') {AddCh(); goto case 56;} + else {t.kind = 29; break;} case 53: - {t.kind = 81; goto done;} + recEnd = pos; recKind = 75; + if (ch == '=') {AddCh(); goto case 32;} + else {t.kind = 75; break;} case 54: - {t.kind = 83; goto done;} + recEnd = pos; recKind = 71; + if (ch == '+') {AddCh(); goto case 37;} + else {t.kind = 71; break;} case 55: - {t.kind = 85; goto done;} + recEnd = pos; recKind = 63; + if (ch == '=') {AddCh(); goto case 57;} + else {t.kind = 63; break;} case 56: - {t.kind = 86; goto done;} + recEnd = pos; recKind = 62; + if (ch == '>') {AddCh(); goto case 22;} + else {t.kind = 62; break;} case 57: - {t.kind = 87; goto done;} - case 58: {t.kind = 0; goto done;} - } - done: - t.val = buf.ToString(); - return t; - } + recEnd = pos; recKind = 56; + if (ch == '>') {AddCh(); goto case 20;} + else {t.kind = 56; break;} -} // end Scanner + } + t.val = new String(tval, 0, tlen); + return t; + } + + private void SetScannerBehindT() { + buffer.Pos = t.pos; + NextCh(); + line = t.line; col = t.col; + for (int i = 0; i < tlen; i++) NextCh(); + } + + // get the next token (possibly a token already seen during peeking) + public Token! Scan () { + if (tokens.next == null) { + return NextToken(); + } else { + pt = tokens = tokens.next; + return tokens; + } + } + // peek for the next token, ignore pragmas + public Token! Peek () { + do { + if (pt.next == null) { + pt.next = NextToken(); + } + pt = pt.next; + } while (pt.kind > maxT); // skip pragmas + + return pt; + } -public delegate void ErrorProc(int n, string filename, int line, int col); + // make sure that peeking starts at the current scan position + public void ResetPeek () { pt = tokens; } -public class Errors { - public static int count = 0; // number of errors detected - public static ErrorProc/*!*/ SynErr; // syntactic errors - - public static void SemErr(string filename, int line, int col, string! msg) { // semantic errors - ConsoleColor color = Console.ForegroundColor; - Console.ForegroundColor = ConsoleColor.Red; - Console.WriteLine("{0}({1},{2}): Error: {3}", filename, line, col, msg); - Console.ForegroundColor = color; - count++; - } - - public static void SemErr(IToken! tok, string! msg) { // semantic errors - SemErr(tok.filename, tok.line, tok.col, msg); - } - - public static void Exception (string s) { - ConsoleColor color = Console.ForegroundColor; - Console.ForegroundColor = ConsoleColor.Red; - Console.WriteLine(s); - Console.ForegroundColor = color; - System.Environment.Exit(0); - } +} // end Scanner + +public delegate void ErrorProc(int n, string filename, int line, int col); -} // Errors -} // end namespace +} \ No newline at end of file diff --git a/Source/Core/parser.frame b/Source/Core/parser.frame deleted file mode 100644 index c7818e57..00000000 --- a/Source/Core/parser.frame +++ /dev/null @@ -1,103 +0,0 @@ - -using System; -using Microsoft.Contracts; - -namespace -->namespace { - -public class Parser { --->constants - const bool T = true; - const bool x = false; - const int minErrDist = 2; - - static Token/*!*/ token; // last recognized token - static Token/*!*/ t; // lookahead token - static int errDist = minErrDist; - - -->declarations - - static void Error(int n) { - if (errDist >= minErrDist) Errors.SynErr(n, t.filename, t.line, t.col); - errDist = 0; - } - - public static void SemErr(string! msg) { - if (errDist >= minErrDist) Errors.SemErr(token.filename, token.line, token.col, msg); - errDist = 0; - } - - public static void SemErr(IToken! tok, string! msg) { - Errors.SemErr(tok.filename, tok.line, tok.col, msg); - } - - static void Get() { - for (;;) { - token = t; - t = Scanner.Scan(); - if (t.kind<=maxT) {errDist++; return;} --->pragmas - t = token; - } - } - - static void Expect(int n) { - if (t.kind==n) Get(); else Error(n); - } - - static bool StartOf(int s) { - return set[s, t.kind]; - } - - static void ExpectWeak(int n, int follow) { - if (t.kind == n) Get(); - else { - Error(n); - while (!StartOf(follow)) Get(); - } - } - - static bool WeakSeparator(int n, int syFol, int repFol) { - bool[] s = new bool[maxT+1]; - if (t.kind == n) {Get(); return true;} - else if (StartOf(repFol)) return false; - else { - for (int i=0; i <= maxT; i++) { - s[i] = set[syFol, i] || set[repFol, i] || set[0, i]; - } - Error(n); - while (!s[t.kind]) Get(); - return StartOf(syFol); - } - } - --->productions - - public static void Parse() { - Errors.SynErr = new ErrorProc(SynErr); - t = new Token(); - Get(); --->parseRoot - } - - [Microsoft.Contracts.Verify(false)] - static void SynErr(int n, string filename, int line, int col) { - Errors.count++; - Console.Write("{0}({1},{2}): syntax error: ", filename, line, col); - string s; - switch (n) { --->errors - default: s = "error " + n; break; - } - Console.WriteLine(s); - } - - static bool[,]! set = { --->initialization - }; - - [Microsoft.Contracts.Verify(false)] - static Parser() {} -} // end Parser - -} // end namespace -$$$ diff --git a/Source/Core/scanner.frame b/Source/Core/scanner.frame deleted file mode 100644 index b9a2ce02..00000000 --- a/Source/Core/scanner.frame +++ /dev/null @@ -1,377 +0,0 @@ -using System; -using System.IO; -using System.Collections; -using System.Collections.Generic; -using System.Text; -using Microsoft.Contracts; - - -namespace Microsoft.Boogie { - - [Immutable] - public interface IToken { - int kind {get; set; } // token kind - string filename {get; set; } // token file - int pos {get; set; } // token position in the source text (starting at 0) - int col {get; set; } // token column (starting at 0) - int line {get; set; } // token line (starting at 1) - string/*!*/ val {get; set; } // token value - - bool IsValid { get; } - } - - [Immutable] - public class Token : IToken { - int _kind; // token kind - string _filename; // token file - int _pos; // token position in the source text (starting at 0) - int _col; // token column (starting at 0) - int _line; // token line (starting at 1) - string/*!*/ _val = "foo"; // token value - - public static IToken! NoToken = new Token(); - - public Token(); - public Token(int linenum, int colnum) { - this._line = linenum; - this._col = colnum; - base(); - } - - public int kind { - get { return this._kind; } - set { this._kind = value; } - } - - public string filename{ - get { return this._filename; } - set { this._filename = value; } - } - - public int pos{ - get { return this._pos; } - set { this._pos = value; } - } - - public int col{ - get { return this._col; } - set { this._col = value; } - } - - public int line{ - get { return this._line; } - set { this._line = value; } - } - - public string/*!*/ val{ - get { return this._val; } - set { this._val = value; } - } - - public bool IsValid { get { return this._filename != null; } } - } - -} - -namespace -->namespace { - -using Microsoft.Boogie; - -public class Buffer { - static string/*!*/ buf; - static int bufLen; - static int pos; - public const int eof = '\uffff'; - - public static void Fill(TextReader! reader) { - List defines = new List(); - Fill(reader, defines); - } - - struct ReadState { - public bool hasSeenElse; - public bool mayStillIncludeAnotherAlternative; - public ReadState(bool hasSeenElse, bool mayStillIncludeAnotherAlternative) { - this.hasSeenElse = hasSeenElse; - this.mayStillIncludeAnotherAlternative = mayStillIncludeAnotherAlternative; - } - } - - public static void Fill(TextReader! reader, List! defines) { - StringBuilder sb = new StringBuilder(); - List! readState = new List(); // readState.Count is the current nesting level of #if's - int ignoreCutoff = -1; // -1 means we're not ignoring; for 0<=n, n means we're ignoring because of something at nesting level n - while (true) - invariant -1 <= ignoreCutoff && ignoreCutoff < readState.Count; - { - string s = reader.ReadLine(); - if (s == null) { - if (readState.Count != 0) { - sb.AppendLine("#MalformedInput: missing #endif"); - } - break; - } - string t = s.Trim(); - if (t.StartsWith("#if")) { - ReadState rs = new ReadState(false, false); - if (ignoreCutoff != -1) { - // we're already in a state of ignoring, so continue to ignore - } else if (IfdefConditionSaysToInclude(t.Substring(3).TrimStart(), defines)) { - // include this branch - } else { - ignoreCutoff = readState.Count; // start ignoring - rs.mayStillIncludeAnotherAlternative = true; // allow some later "elsif" or "else" branch to be included - } - readState.Add(rs); - sb.AppendLine(); // ignore the #if line - - } else if (t.StartsWith("#elsif")) { - ReadState rs; - if (readState.Count == 0 || (rs = readState[readState.Count-1]).hasSeenElse) { - sb.AppendLine("#MalformedInput: misplaced #elsif"); // malformed input - break; - } - if (ignoreCutoff == -1) { - // we had included the previous branch - assert !rs.mayStillIncludeAnotherAlternative; - ignoreCutoff = readState.Count-1; // start ignoring - } else if (rs.mayStillIncludeAnotherAlternative && IfdefConditionSaysToInclude(t.Substring(6).TrimStart(), defines)) { - // include this branch, but no subsequent branch at this level - ignoreCutoff = -1; - rs.mayStillIncludeAnotherAlternative = false; - readState[readState.Count-1] = rs; - } - sb.AppendLine(); // ignore the #elsif line - - } else if (t == "#else") { - ReadState rs; - if (readState.Count == 0 || (rs = readState[readState.Count-1]).hasSeenElse) { - sb.AppendLine("#MalformedInput: misplaced #else"); // malformed input - break; - } - rs.hasSeenElse = true; - if (ignoreCutoff == -1) { - // we had included the previous branch - assert !rs.mayStillIncludeAnotherAlternative; - ignoreCutoff = readState.Count-1; // start ignoring - } else if (rs.mayStillIncludeAnotherAlternative) { - // include this branch - ignoreCutoff = -1; - rs.mayStillIncludeAnotherAlternative = false; - } - readState[readState.Count-1] = rs; - sb.AppendLine(); // ignore the #else line - - } else if (t == "#endif") { - if (readState.Count == 0) { - sb.AppendLine("#MalformedInput: misplaced #endif"); // malformed input - break; - } - readState.RemoveAt(readState.Count-1); // pop - if (ignoreCutoff == readState.Count) { - // we had ignored the branch that ends here; so, now we start including again - ignoreCutoff = -1; - } - sb.AppendLine(); // ignore the #endif line - - } else if (ignoreCutoff == -1) { - sb.AppendLine(s); // included line - - } else { - sb.AppendLine(); // ignore the line - } - } - - Fill(sb.ToString()); - } - - // "arg" is assumed to be trimmed - private static bool IfdefConditionSaysToInclude(string! arg, List! defines) { - bool sense = true; - while (arg.StartsWith("!")) { - sense = !sense; - arg = arg.Substring(1).TrimStart(); - } - return defines.Contains(arg) == sense; - } - - public static void Fill(string! text) { - buf = text; - bufLen = buf.Length; - pos = 0; - } - - public static int Read() { - if (pos < bufLen) { - return buf[pos++]; - } else { - return eof; - } - } - - public static string/*!*/ ReadToEOL() { - int x = buf.IndexOf('\n', pos); - if (x == -1) { - string s = buf.Substring(pos); - pos = buf.Length; - return s; - } else { - string s = buf.Substring(pos, x+1 - pos); // also include the '\n' - pos = x+1; - return s; - } - } - - public static int Pos { - get { return pos; } - set { - if (value < 0) pos = 0; else if (value >= bufLen) pos = bufLen; else pos = value; - } - } -} - - - -public class Scanner { - const char EOF = '\0'; - const char CR = '\r'; - const char LF = '\n'; - [Microsoft.Contracts.Verify(false)] --->declarations - - static Token/*!*/ t; // current token - static char ch; // current input character - static int pos; // column number of current character - static int line; // line number of current character - static int lineStart; // start position of current line - static Queue! oldEols; // EOLs that appeared in a comment; - static BitArray/*!*/ ignore; // set of characters to be ignored by the scanner - static string Filename; - - /// - ///Initializes the scanner. Note: first fill the Buffer. - /// - ///File name used for error reporting - public static void Init (string filename) { - Filename = filename; - pos = -1; line = 1; lineStart = 0; - oldEols = new Queue(); - NextCh(); --->initialization - } - - private static void NextCh() { - if (oldEols.Count > 0) { - ch = (char) ((!)oldEols.Dequeue()); - } else { - while (true) { - ch = (char)Buffer.Read(); pos++; - if (ch == Buffer.eof) { - ch = EOF; - } else if (ch == LF) { - line++; - lineStart = pos + 1; - - } else if (ch == '#' && pos == lineStart) { - int prLine = line; - int prColumn = pos - lineStart; // which is 0 - - string hashLine = Buffer.ReadToEOL(); pos += hashLine.Length; - line++; - lineStart = pos + 1; - - hashLine = hashLine.TrimEnd(null); - if (hashLine.StartsWith("line ") || hashLine == "line") { - // parse #line pragma: #line num [filename] - string h = hashLine.Substring(4).TrimStart(null); - int x = h.IndexOf(' '); - if (x == -1) { - x = h.Length; // this will be convenient below when we look for a filename - } - try { - int li = int.Parse(h.Substring(0, x)); - - h = h.Substring(x).Trim(); - - // act on #line - line = li; - if (h.Length != 0) { - // a filename was specified - Filename = h; - } - continue; // successfully parsed and acted on the #line pragma - - } catch (FormatException) { - // just fall down through to produce an error message - } - Errors.SemErr(Filename, prLine, prColumn, "Malformed (#line num [filename]) pragma: #" + hashLine); - continue; - } - - Errors.SemErr(Filename, prLine, prColumn, "Unrecognized pragma: #" + hashLine); - continue; - } - return; - } - } - } - --->comment - - static void CheckLiteral() { - switch (t.val) { --->literals - } - } - - public static Token/*!*/ Scan() { - while (ignore[ch]) { NextCh(); } --->scan1 - t = new Token(); - t.pos = pos; t.col = pos - lineStart + 1; t.line = line; t.filename = Filename; - int state = (/*^ (!) ^*/ start)[ch]; - StringBuilder buf = new StringBuilder(16); - buf.Append(ch); NextCh(); - - switch (state) { - case 0: {t.kind = noSym; goto done;} // NextCh already done --->scan2 - } - done: - t.val = buf.ToString(); - return t; - } - -} // end Scanner - - -public delegate void ErrorProc(int n, string filename, int line, int col); - -public class Errors { - public static int count = 0; // number of errors detected - public static ErrorProc/*!*/ SynErr; // syntactic errors - - public static void SemErr(string filename, int line, int col, string! msg) { // semantic errors - ConsoleColor color = Console.ForegroundColor; - Console.ForegroundColor = ConsoleColor.Red; - Console.WriteLine("{0}({1},{2}): Error: {3}", filename, line, col, msg); - Console.ForegroundColor = color; - count++; - } - - public static void SemErr(IToken! tok, string! msg) { // semantic errors - SemErr(tok.filename, tok.line, tok.col, msg); - } - - public static void Exception (string s) { - ConsoleColor color = Console.ForegroundColor; - Console.ForegroundColor = ConsoleColor.Red; - Console.WriteLine(s); - Console.ForegroundColor = color; - System.Environment.Exit(0); - } - -} // Errors - -} // end namespace -$$$ -- cgit v1.2.3