From a537984b725aaf2b8250fa8000662d32334e10f1 Mon Sep 17 00:00:00 2001 From: wuestholz Date: Tue, 6 Dec 2011 23:20:12 +0100 Subject: Dafny: Made some minor changes to the grammar. --- Source/Dafny/Dafny.atg | 57 +++--- Source/Dafny/Parser.cs | 474 +++++++++++++++++++++++++++--------------------- Source/Dafny/Scanner.cs | 111 ++++++------ 3 files changed, 361 insertions(+), 281 deletions(-) diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 2eaaca7f..7019a22b 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -191,6 +191,7 @@ ClassDecl List members = new List(); IToken bodyStart; .) + SYNC "class" { Attribute } Ident @@ -234,6 +235,7 @@ DatatypeDecl List ctors = new List(); IToken bodyStart = Token.NoToken; // dummy assignment .) + SYNC "datatype" { Attribute } Ident @@ -241,7 +243,7 @@ DatatypeDecl "=" (. bodyStart = t; .) DatatypeMemberDecl { "|" DatatypeMemberDecl } - ";" + SYNC ";" (. dt = new DatatypeDecl(id, id.val, module, typeArgs, ctors, attrs); dt.BodyStartTok = bodyStart; dt.BodyEndTok = t; @@ -263,6 +265,7 @@ FieldDecl<.MemberModifiers mmod, List/*!*/ mm.> Attributes attrs = null; IToken/*!*/ id; Type/*!*/ ty; .) + SYNC "var" (. if (mmod.IsUnlimited) { SemErr(t, "fields cannot be declared 'unlimited'"); } if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); } @@ -271,7 +274,7 @@ FieldDecl<.MemberModifiers mmod, List/*!*/ mm.> IdentType (. mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); .) { "," IdentType (. mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); .) } - ";" + SYNC ";" . CouplingInvDecl<.MemberModifiers mmod, List/*!*/ mm.> = (. Contract.Requires(cce.NonNullElements(mm)); @@ -379,6 +382,7 @@ MethodDecl IToken bodyStart = Token.NoToken; IToken bodyEnd = Token.NoToken; .) + SYNC ( "method" | "constructor" (. if (allowConstructor) { isConstructor = true; @@ -423,16 +427,17 @@ MethodSpec<.List/*!*/ req, List/ = (. Contract.Requires(cce.NonNullElements(req)); Contract.Requires(cce.NonNullElements(mod)); Contract.Requires(cce.NonNullElements(ens)); Contract.Requires(cce.NonNullElements(decreases)); Expression/*!*/ e; FrameExpression/*!*/ fe; bool isFree = false; .) + SYNC ( "modifies" [ FrameExpression (. mod.Add(fe); .) { "," FrameExpression (. mod.Add(fe); .) } - ] ";" + ] SYNC ";" | [ "free" (. isFree = true; .) ] - ( "requires" Expression ";" (. req.Add(new MaybeFreeExpression(e, isFree)); .) - | "ensures" Expression ";" (. ens.Add(new MaybeFreeExpression(e, isFree)); .) + ( "requires" Expression SYNC ";" (. req.Add(new MaybeFreeExpression(e, isFree)); .) + | "ensures" Expression SYNC ";" (. ens.Add(new MaybeFreeExpression(e, isFree)); .) ) - | "decreases" DecreasesList ";" + | "decreases" DecreasesList SYNC ";" ) . Formals<.bool incoming, bool allowGhostKeyword, List/*!*/ formals.> @@ -555,13 +560,15 @@ FunctionDecl FunctionSpec<.List/*!*/ reqs, List/*!*/ reads, List/*!*/ ens, List/*!*/ decreases.> = (. Contract.Requires(cce.NonNullElements(reqs)); Contract.Requires(cce.NonNullElements(reads)); Contract.Requires(cce.NonNullElements(decreases)); Expression/*!*/ e; FrameExpression/*!*/ fe; .) - ( "requires" Expression ";" (. reqs.Add(e); .) + ( + SYNC + "requires" Expression SYNC ";" (. reqs.Add(e); .) | "reads" [ PossiblyWildFrameExpression (. reads.Add(fe); .) { "," PossiblyWildFrameExpression (. reads.Add(fe); .) } - ] ";" - | "ensures" Expression ";" (. ens.Add(e); .) - | "decreases" DecreasesList ";" + ] SYNC ";" + | "ensures" Expression SYNC ";" (. ens.Add(e); .) + | "decreases" DecreasesList SYNC ";" ) . PossiblyWildExpression @@ -622,6 +629,7 @@ OneStmt int breakCount; .) /* This list does not contain BlockStmt, see comment above in Stmt production. */ + SYNC ( BlockStmt | AssertStmt | AssumeStmt @@ -640,6 +648,7 @@ OneStmt | { "break" (. breakCount++; .) } ) + SYNC ";" (. s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount); .) | ReturnStmt ) @@ -814,25 +823,29 @@ WhileStmt ) . LoopSpec<.out List invariants, out List decreases, out List mod.> -= (. bool isFree; Expression/*!*/ e; FrameExpression/*!*/ fe; += (. FrameExpression/*!*/ fe; invariants = new List(); + MaybeFreeExpression invariant = null; decreases = new List(); mod = null; .) - { (. isFree = false; .) - [ "free" (. isFree = true; .) - ] - "invariant" - Expression (. invariants.Add(new MaybeFreeExpression(e, isFree)); .) - ";" - | "decreases" DecreasesList ";" - | "modifies" (. mod = mod ?? new List(); .) + { + Invariant SYNC ";" (. invariants.Add(invariant); .) + | SYNC "decreases" DecreasesList SYNC ";" + | SYNC "modifies" (. mod = mod ?? new List(); .) [ FrameExpression (. mod.Add(fe); .) { "," FrameExpression (. mod.Add(fe); .) } - ] ";" + ] SYNC ";" } . +Invariant += (. bool isFree = false; Expression/*!*/ e; invariant = null; .) + SYNC + ["free" (. isFree = true; .) + ] + "invariant" Expression (. invariant = new MaybeFreeExpression(e, isFree); .) + . DecreasesList<.List decreases, bool allowWildcard.> = (. Expression/*!*/ e; .) PossiblyWildExpression (. if (!allowWildcard && e is WildcardExpr) { @@ -1310,8 +1323,8 @@ Suffix } ) | ".." (. anyDots = true; .) - [ Expression (. e1 = ee; .) - ] + [ Expression (. e1 = ee; .) + ] ) (. if (multipleIndices != null) { e = new MultiSelectExpr(x, e, multipleIndices); diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 583fcc61..f723ad2c 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -23,7 +23,7 @@ public class Parser { const bool T = true; const bool x = false; const int minErrDist = 2; - + public Scanner/*!*/ scanner; public Errors/*!*/ errors; @@ -134,10 +134,10 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List= minErrDist) errors.SemErr(t, msg); errDist = 0; } - - public void SemErr(IToken/*!*/ tok, string/*!*/ msg) { - Contract.Requires(tok != null); - Contract.Requires(msg != null); + + public void SemErr(IToken/*!*/ tok, string/*!*/ msg) { + Contract.Requires(tok != null); + Contract.Requires(msg != null); errors.SemErr(tok, msg); } @@ -150,15 +150,15 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List theImports; @@ -191,13 +191,13 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List members = new List(); IToken bodyStart; + while (!(la.kind == 0 || la.kind == 9)) {SynErr(105); Get();} Expect(9); while (la.kind == 7) { Attribute(ref attrs); @@ -310,7 +311,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List ctors = new List(); IToken bodyStart = Token.NoToken; // dummy assignment + while (!(la.kind == 0 || la.kind == 14)) {SynErr(106); Get();} Expect(14); while (la.kind == 7) { Attribute(ref attrs); @@ -340,6 +342,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List/*!*/ typeArgs) { @@ -397,6 +400,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List/*!*/ formals) { Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; string/*!*/ name; bool isGhost; Expect(33); - if (StartOf(5)) { + if (StartOf(6)) { TypeIdentOptional(out id, out name, out ty, out isGhost); formals.Add(new Formal(id, name, ty, true, isGhost)); while (la.kind == 19) { @@ -656,9 +662,9 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List/*!*/ decreases) { Contract.Requires(cce.NonNullElements(req)); Contract.Requires(cce.NonNullElements(mod)); Contract.Requires(cce.NonNullElements(ens)); Contract.Requires(cce.NonNullElements(decreases)); Expression/*!*/ e; FrameExpression/*!*/ fe; bool isFree = false; + while (!(StartOf(7))) {SynErr(114); Get();} if (la.kind == 28) { Get(); - if (StartOf(6)) { + if (StartOf(8)) { FrameExpression(out fe); mod.Add(fe); while (la.kind == 19) { @@ -763,6 +770,7 @@ List/*!*/ decreases) { mod.Add(fe); } } + while (!(la.kind == 0 || la.kind == 17)) {SynErr(115); Get();} Expect(17); } else if (la.kind == 29 || la.kind == 30 || la.kind == 31) { if (la.kind == 29) { @@ -772,19 +780,22 @@ List/*!*/ decreases) { if (la.kind == 30) { Get(); Expression(out e); + while (!(la.kind == 0 || la.kind == 17)) {SynErr(116); Get();} Expect(17); req.Add(new MaybeFreeExpression(e, isFree)); } else if (la.kind == 31) { Get(); Expression(out e); + while (!(la.kind == 0 || la.kind == 17)) {SynErr(117); Get();} Expect(17); ens.Add(new MaybeFreeExpression(e, isFree)); - } else SynErr(108); + } else SynErr(118); } else if (la.kind == 32) { Get(); DecreasesList(decreases, false); + while (!(la.kind == 0 || la.kind == 17)) {SynErr(119); Get();} Expect(17); - } else SynErr(109); + } else SynErr(120); } void BlockStmt(out Statement/*!*/ block, out IToken bodyStart, out IToken bodyEnd) { @@ -793,7 +804,7 @@ List/*!*/ decreases) { Expect(7); bodyStart = t; - while (StartOf(7)) { + while (StartOf(9)) { Stmt(body); } Expect(8); @@ -818,7 +829,7 @@ List/*!*/ decreases) { if (!allowWildcard && e is WildcardExpr) { SemErr(e.tok, "'decreases *' is only allowed on loops"); } else { - decreases.Add(e); + decreases.Add(e); } while (la.kind == 19) { @@ -827,7 +838,7 @@ List/*!*/ decreases) { if (!allowWildcard && e is WildcardExpr) { SemErr(e.tok, "'decreases *' is only allowed on loops"); } else { - decreases.Add(e); + decreases.Add(e); } } @@ -863,7 +874,7 @@ List/*!*/ decreases) { } int dims = 1; if (tok.val.Length != 5) { - dims = int.Parse(tok.val.Substring(5)); + dims = int.Parse(tok.val.Substring(5)); } ty = theBuiltIns.ArrayType(tok, dims, gt[0], true); @@ -874,20 +885,22 @@ List/*!*/ decreases) { GenericInstantiation(gt); } ty = new UserDefinedType(tok, tok.val, gt); - } else SynErr(110); + } else SynErr(121); } void FunctionSpec(List/*!*/ reqs, List/*!*/ reads, List/*!*/ ens, List/*!*/ decreases) { Contract.Requires(cce.NonNullElements(reqs)); Contract.Requires(cce.NonNullElements(reads)); Contract.Requires(cce.NonNullElements(decreases)); Expression/*!*/ e; FrameExpression/*!*/ fe; if (la.kind == 30) { + while (!(la.kind == 0 || la.kind == 30)) {SynErr(122); Get();} Get(); Expression(out e); + while (!(la.kind == 0 || la.kind == 17)) {SynErr(123); Get();} Expect(17); reqs.Add(e); } else if (la.kind == 43) { Get(); - if (StartOf(8)) { + if (StartOf(10)) { PossiblyWildFrameExpression(out fe); reads.Add(fe); while (la.kind == 19) { @@ -896,17 +909,20 @@ List/*!*/ decreases) { reads.Add(fe); } } + while (!(la.kind == 0 || la.kind == 17)) {SynErr(124); Get();} Expect(17); } else if (la.kind == 31) { Get(); Expression(out e); + while (!(la.kind == 0 || la.kind == 17)) {SynErr(125); Get();} Expect(17); ens.Add(e); } else if (la.kind == 32) { Get(); DecreasesList(decreases, false); + while (!(la.kind == 0 || la.kind == 17)) {SynErr(126); Get();} Expect(17); - } else SynErr(111); + } else SynErr(127); } void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) { @@ -923,9 +939,9 @@ List/*!*/ decreases) { if (la.kind == 44) { Get(); fe = new FrameExpression(new WildcardExpr(t), null); - } else if (StartOf(6)) { + } else if (StartOf(8)) { FrameExpression(out fe); - } else SynErr(112); + } else SynErr(128); } void PossiblyWildExpression(out Expression/*!*/ e) { @@ -934,9 +950,9 @@ List/*!*/ decreases) { if (la.kind == 44) { Get(); e = new WildcardExpr(t); - } else if (StartOf(6)) { + } else if (StartOf(8)) { Expression(out e); - } else SynErr(113); + } else SynErr(129); } void Stmt(List/*!*/ ss) { @@ -952,6 +968,7 @@ List/*!*/ decreases) { IToken bodyStart, bodyEnd; int breakCount; + while (!(StartOf(11))) {SynErr(130); Get();} switch (la.kind) { case 7: { BlockStmt(out s, out bodyStart, out bodyEnd); @@ -1013,7 +1030,8 @@ List/*!*/ decreases) { Get(); breakCount++; } - } else SynErr(114); + } else SynErr(131); + while (!(la.kind == 0 || la.kind == 17)) {SynErr(132); Get();} Expect(17); s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount); break; @@ -1022,7 +1040,7 @@ List/*!*/ decreases) { ReturnStmt(out s); break; } - default: SynErr(115); break; + default: SynErr(133); break; } } @@ -1093,7 +1111,7 @@ List/*!*/ decreases) { } else if (la.kind == 22) { Get(); SemErr(t, "invalid statement (did you forget the 'label' keyword?)"); - } else SynErr(116); + } else SynErr(134); s = new UpdateStmt(x, lhss, rhss); } @@ -1134,13 +1152,13 @@ List/*!*/ decreases) { Expect(17); UpdateStmt update; if (rhss.Count == 0) { - update = null; + update = null; } else { - var ies = new List(); - foreach (var lhs in lhss) { - ies.Add(new AutoGhostIdentifierExpr(lhs.Tok, lhs.Name)); - } - update = new UpdateStmt(assignTok, ies, rhss); + var ies = new List(); + foreach (var lhs in lhss) { + ies.Add(new AutoGhostIdentifierExpr(lhs.Tok, lhs.Name)); + } + update = new UpdateStmt(assignTok, ies, rhss); } s = new VarDeclStmt(x, lhss, update); @@ -1169,13 +1187,13 @@ List/*!*/ decreases) { } else if (la.kind == 7) { BlockStmt(out s, out bodyStart, out bodyEnd); els = s; - } else SynErr(117); + } else SynErr(135); } ifStmt = new IfStmt(x, guard, thn, els); } else if (la.kind == 7) { AlternativeBlock(out alternatives); ifStmt = new AlternativeStmt(x, alternatives); - } else SynErr(118); + } else SynErr(136); } void WhileStmt(out Statement/*!*/ stmt) { @@ -1197,11 +1215,11 @@ List/*!*/ decreases) { LoopSpec(out invariants, out decreases, out mod); BlockStmt(out body, out bodyStart, out bodyEnd); stmt = new WhileStmt(x, guard, invariants, decreases, mod, body); - } else if (StartOf(9)) { + } else if (StartOf(12)) { LoopSpec(out invariants, out decreases, out mod); AlternativeBlock(out alternatives); stmt = new AlternativeLoopStmt(x, invariants, decreases, mod, alternatives); - } else SynErr(119); + } else SynErr(137); } void MatchStmt(out Statement/*!*/ s) { @@ -1260,7 +1278,7 @@ List/*!*/ decreases) { Expect(48); returnTok = t; - if (StartOf(10)) { + if (StartOf(13)) { Rhs(out r, null); rhss = new List(); rhss.Add(r); while (la.kind == 19) { @@ -1298,7 +1316,7 @@ List/*!*/ decreases) { Ident(out x); Expect(33); args = new List(); - if (StartOf(6)) { + if (StartOf(8)) { Expressions(args); } Expect(34); @@ -1309,7 +1327,7 @@ List/*!*/ decreases) { if (ee != null) { r = new TypeRhs(newToken, ty, ee); } else { - r = new TypeRhs(newToken, ty, initCall); + r = new TypeRhs(newToken, ty, initCall); } } else if (la.kind == 54) { @@ -1320,10 +1338,10 @@ List/*!*/ decreases) { } else if (la.kind == 44) { Get(); r = new HavocRhs(t); - } else if (StartOf(6)) { + } else if (StartOf(8)) { Expression(out e); r = new ExprRhs(e); - } else SynErr(120); + } else SynErr(138); } void Lhs(out Expression e) { @@ -1334,13 +1352,13 @@ List/*!*/ decreases) { while (la.kind == 51 || la.kind == 53) { Suffix(ref e); } - } else if (StartOf(11)) { + } else if (StartOf(14)) { ConstAtomExpression(out e); Suffix(ref e); while (la.kind == 51 || la.kind == 53) { Suffix(ref e); } - } else SynErr(121); + } else SynErr(139); } void Expressions(List/*!*/ args) { @@ -1360,10 +1378,10 @@ List/*!*/ decreases) { if (la.kind == 44) { Get(); e = null; - } else if (StartOf(6)) { + } else if (StartOf(8)) { Expression(out ee); e = ee; - } else SynErr(122); + } else SynErr(140); Expect(34); } @@ -1380,7 +1398,7 @@ List/*!*/ decreases) { Expression(out e); Expect(58); body = new List(); - while (StartOf(7)) { + while (StartOf(9)) { Stmt(body); } alternatives.Add(new GuardedAlternative(x, e, body)); @@ -1389,30 +1407,29 @@ List/*!*/ decreases) { } void LoopSpec(out List invariants, out List decreases, out List mod) { - bool isFree; Expression/*!*/ e; FrameExpression/*!*/ fe; + FrameExpression/*!*/ fe; invariants = new List(); + MaybeFreeExpression invariant = null; decreases = new List(); mod = null; - while (StartOf(12)) { + while (StartOf(15)) { if (la.kind == 29 || la.kind == 60) { - isFree = false; - if (la.kind == 29) { - Get(); - isFree = true; - } - Expect(60); - Expression(out e); - invariants.Add(new MaybeFreeExpression(e, isFree)); + Invariant(out invariant); + while (!(la.kind == 0 || la.kind == 17)) {SynErr(141); Get();} Expect(17); + invariants.Add(invariant); } else if (la.kind == 32) { + while (!(la.kind == 0 || la.kind == 32)) {SynErr(142); Get();} Get(); DecreasesList(decreases, true); + while (!(la.kind == 0 || la.kind == 17)) {SynErr(143); Get();} Expect(17); } else { + while (!(la.kind == 0 || la.kind == 28)) {SynErr(144); Get();} Get(); mod = mod ?? new List(); - if (StartOf(6)) { + if (StartOf(8)) { FrameExpression(out fe); mod.Add(fe); while (la.kind == 19) { @@ -1421,11 +1438,24 @@ List/*!*/ decreases) { mod.Add(fe); } } + while (!(la.kind == 0 || la.kind == 17)) {SynErr(145); Get();} Expect(17); } } } + void Invariant(out MaybeFreeExpression/*!*/ invariant) { + bool isFree = false; Expression/*!*/ e; invariant = null; + while (!(la.kind == 0 || la.kind == 29 || la.kind == 60)) {SynErr(146); Get();} + if (la.kind == 29) { + Get(); + isFree = true; + } + Expect(60); + Expression(out e); + invariant = new MaybeFreeExpression(e, isFree); + } + void CaseStatement(out MatchCaseStmt/*!*/ c) { Contract.Ensures(Contract.ValueAtReturn(out c) != null); IToken/*!*/ x, id; @@ -1448,7 +1478,7 @@ List/*!*/ decreases) { Expect(34); } Expect(58); - while (StartOf(7)) { + while (StartOf(9)) { Stmt(body); } c = new MatchCaseStmt(x, id.val, arguments, body); @@ -1459,10 +1489,10 @@ List/*!*/ decreases) { if (la.kind == 4) { Get(); arg = new Attributes.Argument(t, t.val.Substring(1, t.val.Length-2)); - } else if (StartOf(6)) { + } else if (StartOf(8)) { Expression(out e); arg = new Attributes.Argument(t, e); - } else SynErr(123); + } else SynErr(147); } void QuantifierDomain(out List bvars, out Attributes attrs, out Expression range) { @@ -1514,13 +1544,13 @@ List/*!*/ decreases) { Get(); } else if (la.kind == 67) { Get(); - } else SynErr(124); + } else SynErr(148); } void LogicalExpression(out Expression/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; RelationalExpression(out e0); - if (StartOf(13)) { + if (StartOf(16)) { if (la.kind == 70 || la.kind == 71) { AndOp(); x = t; @@ -1552,7 +1582,7 @@ List/*!*/ decreases) { Get(); } else if (la.kind == 69) { Get(); - } else SynErr(125); + } else SynErr(149); } void RelationalExpression(out Expression/*!*/ e) { @@ -1561,23 +1591,23 @@ List/*!*/ decreases) { List chain = null; List ops = null; int kind = 0; // 0 ("uncommitted") indicates chain of ==, possibly with one != - // 1 ("ascending") indicates chain of ==, <, <=, possibly with one != - // 2 ("descending") indicates chain of ==, >, >=, possibly with one != - // 3 ("illegal") indicates illegal chain - // 4 ("disjoint") indicates chain of disjoint set operators + // 1 ("ascending") indicates chain of ==, <, <=, possibly with one != + // 2 ("descending") indicates chain of ==, >, >=, possibly with one != + // 3 ("illegal") indicates illegal chain + // 4 ("disjoint") indicates chain of disjoint set operators bool hasSeenNeq = false; Term(out e0); e = e0; - if (StartOf(14)) { + if (StartOf(17)) { RelOp(out x, out op); firstOpTok = x; Term(out e1); e = new BinaryExpr(x, op, e0, e1); if (op == BinaryExpr.Opcode.Disjoint) - acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, e0, e1); // accumulate first two operands. + acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, e0, e1); // accumulate first two operands. - while (StartOf(14)) { + while (StartOf(17)) { if (chain == null) { chain = new List(); ops = new List(); @@ -1631,11 +1661,11 @@ List/*!*/ decreases) { Term(out e1); ops.Add(op); chain.Add(e1); if (op == BinaryExpr.Opcode.Disjoint) { - e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, acc, e1)); - acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, acc, e1); //e0 has already been added. + e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, acc, e1)); + acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, acc, e1); //e0 has already been added. } else - e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, e0, e1)); + e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, e0, e1)); } } @@ -1650,7 +1680,7 @@ List/*!*/ decreases) { Get(); } else if (la.kind == 71) { Get(); - } else SynErr(126); + } else SynErr(150); } void OrOp() { @@ -1658,7 +1688,7 @@ List/*!*/ decreases) { Get(); } else if (la.kind == 73) { Get(); - } else SynErr(127); + } else SynErr(151); } void Term(out Expression/*!*/ e0) { @@ -1727,10 +1757,10 @@ List/*!*/ decreases) { if (y == Token.NoToken) { SemErr(x, "invalid RelOp"); } else if (y.pos != x.pos + 1) { - SemErr(x, "invalid RelOp (perhaps you intended \"!in\" with no intervening whitespace?)"); + SemErr(x, "invalid RelOp (perhaps you intended \"!in\" with no intervening whitespace?)"); } else { - x.val = "!in"; - op = BinaryExpr.Opcode.NotIn; + x.val = "!in"; + op = BinaryExpr.Opcode.NotIn; } break; @@ -1750,7 +1780,7 @@ List/*!*/ decreases) { x = t; op = BinaryExpr.Opcode.Ge; break; } - default: SynErr(128); break; + default: SynErr(152); break; } } @@ -1772,7 +1802,7 @@ List/*!*/ decreases) { } else if (la.kind == 85) { Get(); x = t; op = BinaryExpr.Opcode.Sub; - } else SynErr(129); + } else SynErr(153); } void UnaryExpression(out Expression/*!*/ e) { @@ -1818,7 +1848,7 @@ List/*!*/ decreases) { } break; } - default: SynErr(130); break; + default: SynErr(154); break; } } @@ -1833,7 +1863,7 @@ List/*!*/ decreases) { } else if (la.kind == 87) { Get(); x = t; op = BinaryExpr.Opcode.Mod; - } else SynErr(131); + } else SynErr(155); } void NegOp() { @@ -1841,7 +1871,7 @@ List/*!*/ decreases) { Get(); } else if (la.kind == 88) { Get(); - } else SynErr(132); + } else SynErr(156); } void EndlessExpression(out Expression e) { @@ -1918,7 +1948,7 @@ List/*!*/ decreases) { e = new LetExpr(x, letVars, letRHSs, e); break; } - default: SynErr(133); break; + default: SynErr(157); break; } } @@ -1937,7 +1967,7 @@ List/*!*/ decreases) { if (la.kind == 33) { Get(); openParen = t; args = new List(); - if (StartOf(6)) { + if (StartOf(8)) { Expressions(args); } Expect(34); @@ -1957,7 +1987,7 @@ List/*!*/ decreases) { if (la.kind == 33) { Get(); args = new List(); func = true; - if (StartOf(6)) { + if (StartOf(8)) { Expressions(args); } Expect(34); @@ -1967,13 +1997,13 @@ List/*!*/ decreases) { } else if (la.kind == 51) { Get(); x = t; - if (StartOf(6)) { + if (StartOf(8)) { Expression(out ee); e0 = ee; if (la.kind == 97) { Get(); anyDots = true; - if (StartOf(6)) { + if (StartOf(8)) { Expression(out ee); e1 = ee; } @@ -1992,39 +2022,39 @@ List/*!*/ decreases) { multipleIndices.Add(ee); } - } else SynErr(134); + } else SynErr(158); } else if (la.kind == 97) { Get(); anyDots = true; - if (StartOf(6)) { + if (StartOf(8)) { Expression(out ee); e1 = ee; } - } else SynErr(135); + } else SynErr(159); if (multipleIndices != null) { e = new MultiSelectExpr(x, e, multipleIndices); // make sure an array class with this dimensionality exists UserDefinedType tmp = theBuiltIns.ArrayType(x, multipleIndices.Count, new IntType(), true); } else { - if (!anyDots && e0 == null) { - /* a parsing error occurred */ - e0 = dummyExpr; - } - Contract.Assert(anyDots || e0 != null); - if (anyDots) { - //Contract.Assert(e0 != null || e1 != null); - e = new SeqSelectExpr(x, false, e, e0, e1); - } else if (e1 == null) { - Contract.Assert(e0 != null); - e = new SeqSelectExpr(x, true, e, e0, null); - } else { - Contract.Assert(e0 != null); - e = new SeqUpdateExpr(x, e, e0, e1); - } + if (!anyDots && e0 == null) { + /* a parsing error occurred */ + e0 = dummyExpr; + } + Contract.Assert(anyDots || e0 != null); + if (anyDots) { + //Contract.Assert(e0 != null || e1 != null); + e = new SeqSelectExpr(x, false, e, e0, e1); + } else if (e1 == null) { + Contract.Assert(e0 != null); + e = new SeqSelectExpr(x, true, e, e0, null); + } else { + Contract.Assert(e0 != null); + e = new SeqUpdateExpr(x, e, e0, e1); + } } Expect(52); - } else SynErr(136); + } else SynErr(160); } void DisplayExpr(out Expression e) { @@ -2035,7 +2065,7 @@ List/*!*/ decreases) { if (la.kind == 7) { Get(); x = t; elements = new List(); - if (StartOf(6)) { + if (StartOf(8)) { Expressions(elements); } e = new SetDisplayExpr(x, elements); @@ -2043,12 +2073,12 @@ List/*!*/ decreases) { } else if (la.kind == 51) { Get(); x = t; elements = new List(); - if (StartOf(6)) { + if (StartOf(8)) { Expressions(elements); } e = new SeqDisplayExpr(x, elements); Expect(52); - } else SynErr(137); + } else SynErr(161); } void MultiSetExpr(out Expression e) { @@ -2061,7 +2091,7 @@ List/*!*/ decreases) { if (la.kind == 7) { Get(); elements = new List(); - if (StartOf(6)) { + if (StartOf(8)) { Expressions(elements); } e = new MultiSetDisplayExpr(x, elements); @@ -2072,9 +2102,9 @@ List/*!*/ decreases) { Expression(out e); e = new MultiSetFormingExpr(x, e); Expect(34); - } else if (StartOf(15)) { + } else if (StartOf(18)) { SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses."); - } else SynErr(138); + } else SynErr(162); } void ConstAtomExpression(out Expression/*!*/ e) { @@ -2151,7 +2181,7 @@ List/*!*/ decreases) { Expect(34); break; } - default: SynErr(139); break; + default: SynErr(163); break; } } @@ -2160,8 +2190,8 @@ List/*!*/ decreases) { try { n = BigInteger.Parse(t.val); } catch (System.FormatException) { - SemErr("incorrectly formatted number"); - n = BigInteger.Zero; + SemErr("incorrectly formatted number"); + n = BigInteger.Zero; } } @@ -2194,14 +2224,14 @@ List/*!*/ decreases) { } else if (la.kind == 100 || la.kind == 101) { Exists(); x = t; - } else SynErr(140); + } else SynErr(164); QuantifierDomain(out bvars, out attrs, out range); QSep(); Expression(out body); if (univ) { q = new ForallExpr(x, bvars, range, body, attrs); } else { - q = new ExistsExpr(x, bvars, range, body, attrs); + q = new ExistsExpr(x, bvars, range, body, attrs); } } @@ -2264,7 +2294,7 @@ List/*!*/ decreases) { Get(); } else if (la.kind == 99) { Get(); - } else SynErr(141); + } else SynErr(165); } void Exists() { @@ -2272,7 +2302,7 @@ List/*!*/ decreases) { Get(); } else if (la.kind == 101) { Get(); - } else SynErr(142); + } else SynErr(166); } void QSep() { @@ -2280,7 +2310,7 @@ List/*!*/ decreases) { Get(); } else if (la.kind == 103) { Get(); - } else SynErr(143); + } else SynErr(167); } void AttributeBody(ref Attributes attrs) { @@ -2291,7 +2321,7 @@ List/*!*/ decreases) { Expect(22); Expect(1); aName = t.val; - if (StartOf(16)) { + if (StartOf(19)) { AttributeArg(out aArg); aArgs.Add(aArg); while (la.kind == 19) { @@ -2307,23 +2337,27 @@ List/*!*/ decreases) { public void Parse() { la = new Token(); - la.val = ""; + la.val = ""; Get(); Dafny(); + Expect(0); - Expect(0); + 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, x,x,x,x, x,x,x,x, x,x}, + {T,T,T,x, x,x,x,T, x,T,T,T, x,x,T,x, T,T,T,x, x,x,x,x, x,T,T,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,T, x,x,x,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x}, {x,x,x,x, x,T,x,x, x,T,T,T, T,T,T,x, x,x,T,x, T,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,T,x, T,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, {x,x,x,x, x,x,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,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}, + {T,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,x,x,x, x,x,x,x, x,x}, {x,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, + {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,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,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x}, {x,T,T,x, x,x,x,T, x,x,x,T, x,x,x,x, T,x,T,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,T, T,x,x,x, x,x,x,T, x,x,x,T, 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,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x}, {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, T,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x}, + {T,T,T,x, x,x,x,T, x,x,x,T, x,x,x,x, T,x,T,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,T, T,x,x,x, x,x,x,T, x,x,x,T, 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,T,T,T, T,T,T,T, 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, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, T,x,x,x, x,x,T,T, x,x,T,T, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x}, {x,x,T,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,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, T,T,T,T, x,x,x,x, x,x,x,x, x,x}, @@ -2340,18 +2374,20 @@ List/*!*/ decreases) { public class Errors { public int count = 0; // number of errors detected public System.IO.TextWriter/*!*/ errorStream = Console.Out; // error messages go to this stream - public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text - public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text - + public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text + public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text + public void SynErr(string filename, int line, int col, int n) { - SynErr(filename, line, col, GetSyntaxErrorString(n)); - } - public virtual void SynErr(string filename, int line, int col, string msg) { - Contract.Requires(msg != null); + SynErr(filename, line, col, GetSyntaxErrorString(n)); + } + + public virtual void SynErr(string filename, int line, int col, string/*!*/ msg) { + Contract.Requires(msg != null); errorStream.WriteLine(errMsgFormat, filename, line, col, msg); count++; - } - string GetSyntaxErrorString(int n) { + } + + string GetSyntaxErrorString(int n) { string s; switch (n) { case 0: s = "EOF expected"; break; @@ -2459,49 +2495,73 @@ public class Errors { case 102: s = "\"::\" expected"; break; case 103: s = "\"\\u2022\" expected"; break; case 104: s = "??? expected"; break; - case 105: s = "invalid ClassMemberDecl"; break; - case 106: s = "invalid MethodDecl"; break; - case 107: s = "invalid TypeAndToken"; break; - case 108: s = "invalid MethodSpec"; break; - case 109: s = "invalid MethodSpec"; break; - case 110: s = "invalid ReferenceType"; break; - case 111: s = "invalid FunctionSpec"; break; - case 112: s = "invalid PossiblyWildFrameExpression"; break; - case 113: s = "invalid PossiblyWildExpression"; break; - case 114: s = "invalid OneStmt"; break; - case 115: s = "invalid OneStmt"; break; - case 116: s = "invalid UpdateStmt"; break; - case 117: s = "invalid IfStmt"; break; - case 118: s = "invalid IfStmt"; break; - case 119: s = "invalid WhileStmt"; break; - case 120: s = "invalid Rhs"; break; - case 121: s = "invalid Lhs"; break; - case 122: s = "invalid Guard"; break; - case 123: s = "invalid AttributeArg"; break; - case 124: s = "invalid EquivOp"; break; - case 125: s = "invalid ImpliesOp"; break; - case 126: s = "invalid AndOp"; break; - case 127: s = "invalid OrOp"; break; - case 128: s = "invalid RelOp"; break; - case 129: s = "invalid AddOp"; break; - case 130: s = "invalid UnaryExpression"; break; - case 131: s = "invalid MulOp"; break; - case 132: s = "invalid NegOp"; break; - case 133: s = "invalid EndlessExpression"; break; - case 134: s = "invalid Suffix"; break; - case 135: s = "invalid Suffix"; break; - case 136: s = "invalid Suffix"; break; - case 137: s = "invalid DisplayExpr"; break; - case 138: s = "invalid MultiSetExpr"; break; - case 139: s = "invalid ConstAtomExpression"; break; - case 140: s = "invalid QuantifierGuts"; break; - case 141: s = "invalid Forall"; break; - case 142: s = "invalid Exists"; break; - case 143: s = "invalid QSep"; break; + case 105: s = "this symbol not expected in ClassDecl"; break; + case 106: s = "this symbol not expected in DatatypeDecl"; break; + case 107: s = "this symbol not expected in DatatypeDecl"; break; + case 108: s = "invalid ClassMemberDecl"; break; + case 109: s = "this symbol not expected in FieldDecl"; break; + case 110: s = "this symbol not expected in FieldDecl"; break; + case 111: s = "this symbol not expected in MethodDecl"; break; + case 112: s = "invalid MethodDecl"; break; + case 113: s = "invalid TypeAndToken"; break; + case 114: s = "this symbol not expected in MethodSpec"; break; + case 115: s = "this symbol not expected in MethodSpec"; break; + case 116: s = "this symbol not expected in MethodSpec"; break; + case 117: s = "this symbol not expected in MethodSpec"; break; + case 118: s = "invalid MethodSpec"; break; + case 119: s = "this symbol not expected in MethodSpec"; break; + case 120: s = "invalid MethodSpec"; break; + case 121: s = "invalid ReferenceType"; break; + case 122: s = "this symbol not expected in FunctionSpec"; break; + case 123: s = "this symbol not expected in FunctionSpec"; break; + case 124: s = "this symbol not expected in FunctionSpec"; break; + case 125: s = "this symbol not expected in FunctionSpec"; break; + case 126: s = "this symbol not expected in FunctionSpec"; break; + case 127: s = "invalid FunctionSpec"; break; + case 128: s = "invalid PossiblyWildFrameExpression"; break; + case 129: s = "invalid PossiblyWildExpression"; break; + case 130: s = "this symbol not expected in OneStmt"; break; + case 131: s = "invalid OneStmt"; break; + case 132: s = "this symbol not expected in OneStmt"; break; + case 133: s = "invalid OneStmt"; break; + case 134: s = "invalid UpdateStmt"; break; + case 135: s = "invalid IfStmt"; break; + case 136: s = "invalid IfStmt"; break; + case 137: s = "invalid WhileStmt"; break; + case 138: s = "invalid Rhs"; break; + case 139: s = "invalid Lhs"; break; + case 140: s = "invalid Guard"; break; + case 141: s = "this symbol not expected in LoopSpec"; break; + case 142: s = "this symbol not expected in LoopSpec"; break; + case 143: s = "this symbol not expected in LoopSpec"; break; + case 144: s = "this symbol not expected in LoopSpec"; break; + case 145: s = "this symbol not expected in LoopSpec"; break; + case 146: s = "this symbol not expected in Invariant"; break; + case 147: s = "invalid AttributeArg"; break; + case 148: s = "invalid EquivOp"; break; + case 149: s = "invalid ImpliesOp"; break; + case 150: s = "invalid AndOp"; break; + case 151: s = "invalid OrOp"; break; + case 152: s = "invalid RelOp"; break; + case 153: s = "invalid AddOp"; break; + case 154: s = "invalid UnaryExpression"; break; + case 155: s = "invalid MulOp"; break; + case 156: s = "invalid NegOp"; break; + case 157: s = "invalid EndlessExpression"; break; + case 158: s = "invalid Suffix"; break; + case 159: s = "invalid Suffix"; break; + case 160: s = "invalid Suffix"; break; + case 161: s = "invalid DisplayExpr"; break; + case 162: s = "invalid MultiSetExpr"; break; + case 163: s = "invalid ConstAtomExpression"; break; + case 164: s = "invalid QuantifierGuts"; break; + case 165: s = "invalid Forall"; break; + case 166: s = "invalid Exists"; break; + case 167: s = "invalid QSep"; break; default: s = "error " + n; break; } - return s; + return s; } public void SemErr(IToken/*!*/ tok, string/*!*/ msg) { // semantic errors @@ -2509,8 +2569,9 @@ public class Errors { Contract.Requires(msg != null); SemErr(tok.filename, tok.line, tok.col, msg); } + public virtual void SemErr(string filename, int line, int col, string/*!*/ msg) { - Contract.Requires(msg != null); + Contract.Requires(msg != null); errorStream.WriteLine(errMsgFormat, filename, line, col, msg); count++; } @@ -2526,4 +2587,5 @@ public class FatalError: Exception { public FatalError(string m): base(m) {} } + } \ No newline at end of file diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs index 1ab06974..f0eb1937 100644 --- a/Source/Dafny/Scanner.cs +++ b/Source/Dafny/Scanner.cs @@ -19,7 +19,7 @@ public class Buffer { // a) whole stream in buffer // b) part of stream in buffer // 2) non seekable stream (network, console) - + 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 @@ -31,15 +31,17 @@ public class Buffer { Stream/*!*/ stream; // input stream (seekable) bool isUserStream; // was the stream opened by the user? -[ContractInvariantMethod] -void ObjectInvariant(){ - Contract.Invariant(buf != null); - Contract.Invariant(stream != null);} - [NotDelayed] - public Buffer (Stream/*!*/ s, bool isUserStream) :base() { + [ContractInvariantMethod] + void ObjectInvariant(){ + Contract.Invariant(buf != null); + Contract.Invariant(stream != null); + } + +// [NotDelayed] + public Buffer (Stream/*!*/ s, bool isUserStream) : base() { Contract.Requires(s != null); stream = s; this.isUserStream = isUserStream; - + int fl, bl; if (s.CanSeek) { fl = (int) s.Length; @@ -51,12 +53,12 @@ void ObjectInvariant(){ buf = new byte[(bl>0) ? bl : MIN_BUFFER_LENGTH]; fileLen = fl; bufLen = bl; - + 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 Contract.Requires(b != null); buf = b.buf; @@ -73,14 +75,14 @@ void ObjectInvariant(){ } ~Buffer() { Close(); } - + protected void Close() { if (!isUserStream && stream != null) { stream.Close(); //stream = null; } } - + public virtual int Read () { if (bufPos < bufLen) { return buf[bufPos++]; @@ -100,7 +102,7 @@ void ObjectInvariant(){ Pos = curPos; return ch; } - + public string/*!*/ GetString (int beg, int end) { Contract.Ensures(Contract.Result() != null); int len = 0; @@ -139,7 +141,7 @@ void ObjectInvariant(){ } } } - + // 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. @@ -213,22 +215,24 @@ public class Scanner { const int noSym = 104; -[ContractInvariantMethod] -void objectInvariant(){ - Contract.Invariant(buffer!=null); - Contract.Invariant(t != null); - Contract.Invariant(start != null); - Contract.Invariant(tokens != null); - Contract.Invariant(pt != null); - Contract.Invariant(tval != null); - Contract.Invariant(Filename != null); - Contract.Invariant(errorHandler != null); -} + [ContractInvariantMethod] + void objectInvariant(){ + Contract.Invariant(buffer!=null); + Contract.Invariant(t != null); + Contract.Invariant(start != null); + Contract.Invariant(tokens != null); + Contract.Invariant(pt != null); + Contract.Invariant(tval != null); + Contract.Invariant(Filename != null); + Contract.Invariant(errorHandler != null); + } + public Buffer/*!*/ buffer; // scanner buffer - + Token/*!*/ t; // current token int ch; // current input character int pos; // byte position of current character + int charPos; int col; // column number of current character int line; // line number of current character int oldEols; // EOLs that appeared in a comment; @@ -236,13 +240,13 @@ void objectInvariant(){ 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 = new Hashtable(128); for (int i = 39; i <= 39; ++i) start[i] = 1; @@ -290,9 +294,9 @@ void objectInvariant(){ start[Buffer.EOF] = -1; } - - [NotDelayed] - public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) :base(){ + +// [NotDelayed] + public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) : base() { Contract.Requires(fileName != null); Contract.Requires(errorHandler != null); this.errorHandler = errorHandler; @@ -302,15 +306,14 @@ void objectInvariant(){ Stream stream = new FileStream(fileName, FileMode.Open, FileAccess.Read, FileShare.Read); buffer = new Buffer(stream, false); Filename = fileName; - Init(); } catch (IOException) { throw new FatalError("Cannot open file " + fileName); } } - - [NotDelayed] - public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) :base(){ + +// [NotDelayed] + public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) : base() { Contract.Requires(s != null); Contract.Requires(errorHandler != null); Contract.Requires(fileName != null); @@ -319,10 +322,9 @@ void objectInvariant(){ buffer = new Buffer(s, true); this.errorHandler = errorHandler; this.Filename = fileName; - Init(); } - + void Init() { pos = -1; line = 1; col = 0; oldEols = 0; @@ -343,11 +345,11 @@ void objectInvariant(){ Contract.Ensures(Contract.Result() != null); int p = buffer.Pos; int ch = buffer.Read(); - // replace isolated '\r' by '\n' in order to make + // 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(); + 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; @@ -358,7 +360,7 @@ void objectInvariant(){ } void NextCh() { - if (oldEols > 0) { ch = EOL; oldEols--; } + if (oldEols > 0) { ch = EOL; oldEols--; } else { // pos = buffer.Pos; // ch = buffer.Read(); col++; @@ -366,9 +368,9 @@ void objectInvariant(){ // // 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; + pos = buffer.Pos; ch = buffer.Read(); col++; // replace isolated '\r' by '\n' in order to make // eol handling uniform across Windows, Unix and Mac @@ -418,7 +420,7 @@ void objectInvariant(){ return; } - + } } @@ -438,7 +440,7 @@ void objectInvariant(){ bool Comment0() { - int level = 1, pos0 = pos, line0 = line, col0 = col; + int level = 1, pos0 = pos, line0 = line, col0 = col, charPos0 = charPos; NextCh(); if (ch == '/') { NextCh(); @@ -451,13 +453,13 @@ void objectInvariant(){ else NextCh(); } } else { - buffer.Pos = pos0; NextCh(); line = line0; col = col0; + buffer.Pos = pos0; NextCh(); line = line0; col = col0; charPos = charPos0; } return false; } bool Comment1() { - int level = 1, pos0 = pos, line0 = line, col0 = col; + int level = 1, pos0 = pos, line0 = line, col0 = col, charPos0 = charPos; NextCh(); if (ch == '*') { NextCh(); @@ -478,7 +480,7 @@ void objectInvariant(){ else NextCh(); } } else { - buffer.Pos = pos0; NextCh(); line = line0; col = col0; + buffer.Pos = pos0; NextCh(); line = line0; col = col0; charPos = charPos0; } return false; } @@ -556,10 +558,13 @@ void objectInvariant(){ t.pos = pos; t.col = col; t.line = line; t.filename = this.Filename; int state; - if (start.ContainsKey(ch)) { state = (int) cce.NonNull( start[ch]); } + if (start.ContainsKey(ch)) { + Contract.Assert(start[ch] != null); + state = (int) start[ch]; + } else { state = 0; } tlen = 0; AddCh(); - + switch (state) { case -1: { t.kind = eofSym; break; } // NextCh already done case 0: { @@ -759,14 +764,14 @@ void objectInvariant(){ 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 () { Contract.Ensures(Contract.Result() != null); @@ -787,7 +792,7 @@ void objectInvariant(){ } pt = pt.next; } while (pt.kind > maxT); // skip pragmas - + return pt; } -- cgit v1.2.3 From 0309df8a19b721a6e4813d41170989e65eaa3794 Mon Sep 17 00:00:00 2001 From: Mike Barnett Date: Tue, 6 Dec 2011 20:39:59 -0800 Subject: Fixed bug when getting last source context in a method body. --- BCT/GetMeHere/AssertionInjector/Program.cs | 37 ++++++++++++++++++------------ 1 file changed, 22 insertions(+), 15 deletions(-) diff --git a/BCT/GetMeHere/AssertionInjector/Program.cs b/BCT/GetMeHere/AssertionInjector/Program.cs index 4e8c3926..3d6552cd 100644 --- a/BCT/GetMeHere/AssertionInjector/Program.cs +++ b/BCT/GetMeHere/AssertionInjector/Program.cs @@ -42,6 +42,8 @@ namespace AssertionInjector { string outputAssemblyPath; string outputPdbFileName; + var returnValue = errorValue; + using (var host = new PeReader.DefaultHost()) { IModule/*?*/ module = host.LoadUnitFrom(args[0]) as IModule; if (module == null || module == Dummy.Module || module == Dummy.Assembly) { @@ -64,6 +66,8 @@ namespace AssertionInjector { var localScopeProvider = new ILGenerator.LocalScopeProvider(pdbReader); var mutator = new GetMeHereInjector(host, pdbReader, fileName, lineNumber, columnNumber); module = mutator.Rewrite(module); + //Console.WriteLine("Emitted probe: {0}", mutator.emittedProbe); + if (mutator.emittedProbe) returnValue = 0; originalAssemblyPath = module.Location; var tempDir = Path.GetTempPath(); @@ -92,7 +96,7 @@ namespace AssertionInjector { return errorValue; } - return 0; // success + return returnValue; // success } } @@ -126,6 +130,7 @@ namespace AssertionInjector { Stack scopeStack = new Stack(); private NamespaceTypeDefinition getMeHereClass; private MethodDefinition getMeHereAssert; + public bool emittedProbe; public override void RewriteChildren(Module module) { base.RewriteChildren(module); @@ -157,7 +162,7 @@ namespace AssertionInjector { public override void RewriteChildren(MethodBody methodBody) { this.currentLocals = methodBody.LocalVariables; - + //Console.WriteLine("{0}", MemberHelper.GetMethodSignature(methodBody.MethodDefinition)); try { var operations = methodBody.Operations; if (operations == null || operations.Count == 0) return; @@ -174,16 +179,18 @@ namespace AssertionInjector { if (startLocation == null || startLocation.StartLine == 0x00feefee || !startLocation.Document.Name.Value.Equals(this.fileName)) return; - ys = this.pdbReader.GetClosestPrimarySourceLocationsFor(operations[operations.Count - 1].Location); - foreach (var y in ys) { - //Console.WriteLine("{0}:{1}({2},{3})", y.Document.Name.Value, MemberHelper.GetMethodSignature(methodBody.MethodDefinition, NameFormattingOptions.None), - // y.StartLine, y.StartColumn); - endLocation = y; - break; - } - - if (endLocation == null || endLocation.StartLine == 0x00feefee) return; - if (!(startLocation.StartLine <= this.lineNumber && this.lineNumber <= endLocation.StartLine)) return; + var lastIndex = operations.Count; + do { + lastIndex--; + ys = this.pdbReader.GetClosestPrimarySourceLocationsFor(operations[lastIndex].Location); + foreach (var y in ys) { + //Console.WriteLine("{0}:{1}({2},{3})", y.Document.Name.Value, MemberHelper.GetMethodSignature(methodBody.MethodDefinition, NameFormattingOptions.None), + // y.StartLine, y.StartColumn); + endLocation = y; + break; + } + } while (0 <= lastIndex && (endLocation == null || endLocation.StartLine == 0x00feefee)); + if (lastIndex == -1 || !(startLocation.StartLine <= this.lineNumber && this.lineNumber <= endLocation.StartLine)) return; ProcessOperations(methodBody, operations); @@ -280,7 +287,7 @@ namespace AssertionInjector { #endregion Pass 1: Make a label for each branch target #region Pass 2: Emit each operation, along with labels - bool emittedProbe = false; // don't do it more than once + this.emittedProbe = false; // don't do it more than once for (int i = 0; i < count; i++) { IOperation op = operations[i]; ILGeneratorLabel label; @@ -330,7 +337,7 @@ namespace AssertionInjector { #region Emit operation along with any injection - if (!emittedProbe) { + if (!this.emittedProbe) { IPrimarySourceLocation location = null; var locations = this.pdbReader.GetPrimarySourceLocationsFor(op.Location); foreach (var x in locations) { @@ -340,7 +347,7 @@ namespace AssertionInjector { } } if (location != null) { - emittedProbe = true; + this.emittedProbe = true; generator.Emit(OperationCode.Ldc_I4_0); generator.Emit(OperationCode.Call, this.getMeHereAssert); } -- cgit v1.2.3