diff options
| author |  Michal Moskal <michal@moskal.me> | 2011-12-07 11:14:46 -0800 |
|---|---|---|
| committer | Michal Moskal <michal@moskal.me> | 2011-12-07 11:14:46 -0800 |
| commit | d58f452f518d5b14b32534d909b6436a3577576b (patch) | |
| tree | 3bcb4cc62af26a6a10bd651e2fa1a1a5fd01a900 /Source | |
| parent | be9a2d297ccd8900cccc750c15a9c02c9e23a83b (diff) | |
| parent | 5023898ea9b2204593bf0cc685cb57be7fade17c (diff) | |
Merge
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.cs | 2 | ||||
| -rw-r--r-- | Source/Core/Absy.cs | 1 | ||||
| -rw-r--r-- | Source/Dafny/Compiler.cs | 2 | ||||
| -rw-r--r-- | Source/Dafny/Dafny.atg | 57 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 4 | ||||
| -rw-r--r-- | Source/Dafny/Parser.cs | 474 | ||||
| -rw-r--r-- | Source/Dafny/Scanner.cs | 111 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 2 | ||||
| -rw-r--r-- | Source/DafnyDriver/DafnyDriver.cs | 2 | ||||
| -rw-r--r-- | Source/GPUVerify/GPUVerifier.cs | 260 | ||||
| -rw-r--r-- | Source/GPUVerify/INonLocalState.cs | 2 | ||||
| -rw-r--r-- | Source/GPUVerify/Main.cs | 6 | ||||
| -rw-r--r-- | Source/GPUVerify/NonLocalStateLists.cs | 10 | ||||
| -rw-r--r-- | Source/GPUVerify/RaceInstrumenterBase.cs | 4 | ||||
| -rw-r--r-- | Source/Houdini/Houdini.cs | 67 |
15 files changed, 555 insertions, 449 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 58731f10..eab8bc36 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -390,6 +390,8 @@ namespace Microsoft.Boogie { // Coalesce blocks
if (CommandLineOptions.Clo.CoalesceBlocks) {
+ if (CommandLineOptions.Clo.Trace)
+ Console.WriteLine("Coalescing blocks...");
Microsoft.Boogie.BlockCoalescer.CoalesceBlocks(program);
}
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 18a0441a..d6a2a74d 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -2018,6 +2018,7 @@ namespace Microsoft.Boogie { stream.WriteLine(this, level, "// " + Comment);
}
stream.Write(this, level, "{0}requires ", Free ? "free " : "");
+ Cmd.EmitAttributes(stream, Attributes);
this.Condition.Emit(stream);
stream.WriteLine(";");
}
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index d0e0cb0e..b49c011f 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -1367,7 +1367,7 @@ namespace Microsoft.Dafny { Type elType = cce.NonNull((MultiSetType)e.Type).Arg;
wr.Write("{0}<{1}>.FromElements", DafnyMultiSetClass, TypeName(elType));
TrExprList(e.Elements);
-
+
} else if (expr is SeqDisplayExpr) {
SeqDisplayExpr e = (SeqDisplayExpr)expr;
Type elType = cce.NonNull((SeqType)e.Type).Arg;
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<ModuleDecl/*!*/ module, out ClassDecl/*!*/ c> List<MemberDecl/*!*/> members = new List<MemberDecl/*!*/>();
IToken bodyStart;
.)
+ SYNC
"class"
{ Attribute<ref attrs> }
Ident<out id>
@@ -234,6 +235,7 @@ DatatypeDecl<ModuleDecl/*!*/ module, out DatatypeDecl/*!*/ dt> List<DatatypeCtor/*!*/> ctors = new List<DatatypeCtor/*!*/>();
IToken bodyStart = Token.NoToken; // dummy assignment
.)
+ SYNC
"datatype"
{ Attribute<ref attrs> }
Ident<out id>
@@ -241,7 +243,7 @@ DatatypeDecl<ModuleDecl/*!*/ module, out DatatypeDecl/*!*/ dt> "=" (. bodyStart = t; .)
DatatypeMemberDecl<ctors>
{ "|" DatatypeMemberDecl<ctors> }
- ";"
+ 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<MemberDecl/*!*/>/*!*/ 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<MemberDecl/*!*/>/*!*/ mm.> IdentType<out id, out ty> (. mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); .)
{ "," IdentType<out id, out ty> (. mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); .)
}
- ";"
+ SYNC ";"
.
CouplingInvDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.>
= (. Contract.Requires(cce.NonNullElements(mm));
@@ -379,6 +382,7 @@ MethodDecl<MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m> IToken bodyStart = Token.NoToken;
IToken bodyEnd = Token.NoToken;
.)
+ SYNC
( "method"
| "constructor" (. if (allowConstructor) {
isConstructor = true;
@@ -423,16 +427,17 @@ MethodSpec<.List<MaybeFreeExpression/*!*/>/*!*/ req, List<FrameExpression/*!*/>/ = (. 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<out fe> (. mod.Add(fe); .)
{ "," FrameExpression<out fe> (. mod.Add(fe); .)
}
- ] ";"
+ ] SYNC ";"
| [ "free" (. isFree = true; .)
]
- ( "requires" Expression<out e> ";" (. req.Add(new MaybeFreeExpression(e, isFree)); .)
- | "ensures" Expression<out e> ";" (. ens.Add(new MaybeFreeExpression(e, isFree)); .)
+ ( "requires" Expression<out e> SYNC ";" (. req.Add(new MaybeFreeExpression(e, isFree)); .)
+ | "ensures" Expression<out e> SYNC ";" (. ens.Add(new MaybeFreeExpression(e, isFree)); .)
)
- | "decreases" DecreasesList<decreases, false> ";"
+ | "decreases" DecreasesList<decreases, false> SYNC ";"
)
.
Formals<.bool incoming, bool allowGhostKeyword, List<Formal/*!*/>/*!*/ formals.>
@@ -555,13 +560,15 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f> FunctionSpec<.List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/>/*!*/ decreases.>
= (. Contract.Requires(cce.NonNullElements(reqs)); Contract.Requires(cce.NonNullElements(reads)); Contract.Requires(cce.NonNullElements(decreases));
Expression/*!*/ e; FrameExpression/*!*/ fe; .)
- ( "requires" Expression<out e> ";" (. reqs.Add(e); .)
+ (
+ SYNC
+ "requires" Expression<out e> SYNC ";" (. reqs.Add(e); .)
| "reads" [ PossiblyWildFrameExpression<out fe> (. reads.Add(fe); .)
{ "," PossiblyWildFrameExpression<out fe> (. reads.Add(fe); .)
}
- ] ";"
- | "ensures" Expression<out e> ";" (. ens.Add(e); .)
- | "decreases" DecreasesList<decreases, false> ";"
+ ] SYNC ";"
+ | "ensures" Expression<out e> SYNC ";" (. ens.Add(e); .)
+ | "decreases" DecreasesList<decreases, false> SYNC ";"
)
.
PossiblyWildExpression<out Expression/*!*/ e>
@@ -622,6 +629,7 @@ OneStmt<out Statement/*!*/ s> int breakCount;
.)
/* This list does not contain BlockStmt, see comment above in Stmt production. */
+ SYNC
( BlockStmt<out s, out bodyStart, out bodyEnd>
| AssertStmt<out s>
| AssumeStmt<out s>
@@ -640,6 +648,7 @@ OneStmt<out Statement/*!*/ s> | { "break" (. breakCount++; .)
}
)
+ SYNC
";" (. s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount); .)
| ReturnStmt<out s>
)
@@ -814,25 +823,29 @@ WhileStmt<out Statement/*!*/ stmt> )
.
LoopSpec<.out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*/> decreases, out List<FrameExpression/*!*/> mod.>
-= (. bool isFree; Expression/*!*/ e; FrameExpression/*!*/ fe;
+= (. FrameExpression/*!*/ fe;
invariants = new List<MaybeFreeExpression/*!*/>();
+ MaybeFreeExpression invariant = null;
decreases = new List<Expression/*!*/>();
mod = null;
.)
- { (. isFree = false; .)
- [ "free" (. isFree = true; .)
- ]
- "invariant"
- Expression<out e> (. invariants.Add(new MaybeFreeExpression(e, isFree)); .)
- ";"
- | "decreases" DecreasesList<decreases, true> ";"
- | "modifies" (. mod = mod ?? new List<FrameExpression>(); .)
+ {
+ Invariant<out invariant> SYNC ";" (. invariants.Add(invariant); .)
+ | SYNC "decreases" DecreasesList<decreases, true> SYNC ";"
+ | SYNC "modifies" (. mod = mod ?? new List<FrameExpression>(); .)
[ FrameExpression<out fe> (. mod.Add(fe); .)
{ "," FrameExpression<out fe> (. mod.Add(fe); .)
}
- ] ";"
+ ] SYNC ";"
}
.
+Invariant<out MaybeFreeExpression/*!*/ invariant>
+= (. bool isFree = false; Expression/*!*/ e; invariant = null; .)
+ SYNC
+ ["free" (. isFree = true; .)
+ ]
+ "invariant" Expression<out e> (. invariant = new MaybeFreeExpression(e, isFree); .)
+ .
DecreasesList<.List<Expression/*!*/> decreases, bool allowWildcard.>
= (. Expression/*!*/ e; .)
PossiblyWildExpression<out e> (. if (!allowWildcard && e is WildcardExpr) {
@@ -1310,8 +1323,8 @@ Suffix<ref Expression/*!*/ e> }
)
| ".." (. anyDots = true; .)
- [ Expression<out ee> (. e1 = ee; .)
- ]
+ [ Expression<out ee> (. e1 = ee; .)
+ ]
)
(. if (multipleIndices != null) {
e = new MultiSelectExpr(x, e, multipleIndices);
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 8272736c..99ebe8da 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -262,7 +262,7 @@ namespace Microsoft.Dafny { this.Arg = arg;
}
}
-
+
public class SetType : CollectionType {
public SetType(Type arg) : base(arg) {
Contract.Requires(arg != null);
@@ -2149,7 +2149,7 @@ namespace Microsoft.Dafny { get { return Elements; }
}
}
-
+
public class SetDisplayExpr : DisplayExpression {
public SetDisplayExpr(IToken tok, List<Expression/*!*/>/*!*/ elements)
: base(tok, elements) {
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<ModuleDecl/*! if (errDist >= 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<ModuleDecl/*! la = t;
}
}
-
+
void Expect (int n) {
if (la.kind==n) Get(); else { SynErr(n); }
}
-
+
bool StartOf (int s) {
return set[s, la.kind];
}
-
+
void ExpectWeak (int n, int follow) {
if (la.kind == n) Get();
else {
@@ -182,7 +182,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! }
}
-
+
void Dafny() {
ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt;
Attributes attrs; IToken/*!*/ id; List<string/*!*/> theImports;
@@ -191,13 +191,13 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! // to support multiple files, create a default module only if theModules doesn't already contain one
DefaultModuleDecl defaultModule = null;
foreach (ModuleDecl mdecl in theModules) {
- defaultModule = mdecl as DefaultModuleDecl;
- if (defaultModule != null) { break; }
+ defaultModule = mdecl as DefaultModuleDecl;
+ if (defaultModule != null) { break; }
}
bool defaultModuleCreatedHere = false;
if (defaultModule == null) {
- defaultModuleCreatedHere = true;
- defaultModule = new DefaultModuleDecl();
+ defaultModuleCreatedHere = true;
+ defaultModule = new DefaultModuleDecl();
}
while (StartOf(1)) {
@@ -241,14 +241,14 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! defaultModule.TopLevelDecls.Add(new DefaultClassDecl(defaultModule, membersDefaultClass));
theModules.Add(defaultModule);
} else {
- // find the default class in the default module, then append membersDefaultClass to its member list
- foreach (TopLevelDecl topleveldecl in defaultModule.TopLevelDecls) {
- DefaultClassDecl defaultClass = topleveldecl as DefaultClassDecl;
- if (defaultClass != null) {
- defaultClass.Members.AddRange(membersDefaultClass);
- break;
- }
- }
+ // find the default class in the default module, then append membersDefaultClass to its member list
+ foreach (TopLevelDecl topleveldecl in defaultModule.TopLevelDecls) {
+ DefaultClassDecl defaultClass = topleveldecl as DefaultClassDecl;
+ if (defaultClass != null) {
+ defaultClass.Members.AddRange(membersDefaultClass);
+ break;
+ }
+ }
}
Expect(0);
@@ -288,6 +288,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! List<MemberDecl/*!*/> members = new List<MemberDecl/*!*/>();
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<ModuleDecl/*! if (optionalId == null)
c = new ClassDecl(id, id.val, module, typeArgs, members, attrs);
else
- c = new ClassRefinementDecl(id, id.val, module, typeArgs, members, attrs, optionalId);
+ c = new ClassRefinementDecl(id, id.val, module, typeArgs, members, attrs, optionalId);
c.BodyStartTok = bodyStart;
c.BodyEndTok = t;
@@ -325,6 +326,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! List<DatatypeCtor/*!*/> ctors = new List<DatatypeCtor/*!*/>();
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<ModuleDecl/*! Get();
DatatypeMemberDecl(ctors);
}
+ while (!(la.kind == 0 || la.kind == 17)) {SynErr(107); Get();}
Expect(17);
dt = new DatatypeDecl(id, id.val, module, typeArgs, ctors, attrs);
dt.BodyStartTok = bodyStart;
@@ -375,7 +378,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! mm.Add(m);
} else if (la.kind == 20) {
CouplingInvDecl(mmod, mm);
- } else SynErr(105);
+ } else SynErr(108);
}
void GenericParameters(List<TypeParameter/*!*/>/*!*/ typeArgs) {
@@ -397,6 +400,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! Attributes attrs = null;
IToken/*!*/ id; Type/*!*/ ty;
+ while (!(la.kind == 0 || la.kind == 18)) {SynErr(109); Get();}
Expect(18);
if (mmod.IsUnlimited) { SemErr(t, "fields cannot be declared 'unlimited'"); }
if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); }
@@ -411,6 +415,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! IdentType(out id, out ty);
mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs));
}
+ while (!(la.kind == 0 || la.kind == 17)) {SynErr(110); Get();}
Expect(17);
}
@@ -477,6 +482,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! IToken bodyStart = Token.NoToken;
IToken bodyEnd = Token.NoToken;
+ while (!(StartOf(4))) {SynErr(111); Get();}
if (la.kind == 25) {
Get();
} else if (la.kind == 26) {
@@ -484,21 +490,21 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! if (allowConstructor) {
isConstructor = true;
} else {
- SemErr(t, "constructors are only allowed in classes");
+ SemErr(t, "constructors are only allowed in classes");
}
} else if (la.kind == 10) {
Get();
isRefinement = true;
- } else SynErr(106);
+ } else SynErr(112);
if (mmod.IsUnlimited) { SemErr(t, "methods cannot be declared 'unlimited'"); }
if (isConstructor) {
- if (mmod.IsGhost) {
- SemErr(t, "constructors cannot be declared 'ghost'");
- }
- if (mmod.IsStatic) {
- SemErr(t, "constructors cannot be declared 'static'");
- }
+ if (mmod.IsGhost) {
+ SemErr(t, "constructors cannot be declared 'ghost'");
+ }
+ if (mmod.IsStatic) {
+ SemErr(t, "constructors cannot be declared 'static'");
+ }
}
while (la.kind == 7) {
@@ -514,7 +520,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! if (isConstructor) { SemErr(t, "constructors cannot have out-parameters"); }
Formals(false, !mmod.IsGhost, outs);
}
- while (StartOf(4)) {
+ while (StartOf(5)) {
MethodSpec(req, mod, ens, dec);
}
if (la.kind == 7) {
@@ -524,9 +530,9 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! if (isRefinement)
m = new MethodRefinement(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);
else if (isConstructor)
- m = new Constructor(id, id.val, typeArgs, ins, req, mod, ens, dec, body, attrs);
+ m = new Constructor(id, id.val, typeArgs, ins, req, mod, ens, dec, body, attrs);
else
- m = new Method(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);
+ m = new Method(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);
m.BodyStartTok = bodyStart;
m.BodyEndTok = bodyEnd;
@@ -579,7 +585,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! void FormalsOptionalIds(List<Formal/*!*/>/*!*/ 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<ModuleDecl/*! Get();
UserDefinedType udt = ty as UserDefinedType;
if (udt != null && udt.TypeArgs.Count == 0) {
- name = udt.Name;
+ name = udt.Name;
} else {
- SemErr(id, "invalid formal-parameter name in datatype constructor");
+ SemErr(id, "invalid formal-parameter name in datatype constructor");
}
Type(out ty);
@@ -666,7 +672,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! if (name != null) {
identName = name;
} else {
- identName = "#" + anonymousIds++;
+ identName = "#" + anonymousIds++;
}
}
@@ -728,7 +734,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! ReferenceType(out tok, out ty);
break;
}
- default: SynErr(107); break;
+ default: SynErr(113); break;
}
}
@@ -752,9 +758,10 @@ List<Expression/*!*/>/*!*/ 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<Expression/*!*/>/*!*/ 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<Expression/*!*/>/*!*/ 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<Expression/*!*/>/*!*/ decreases) { Expect(7);
bodyStart = t;
- while (StartOf(7)) {
+ while (StartOf(9)) {
Stmt(body);
}
Expect(8);
@@ -818,7 +829,7 @@ List<Expression/*!*/>/*!*/ 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<Expression/*!*/>/*!*/ 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<Expression/*!*/>/*!*/ 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<Expression/*!*/>/*!*/ decreases) { GenericInstantiation(gt);
}
ty = new UserDefinedType(tok, tok.val, gt);
- } else SynErr(110);
+ } else SynErr(121);
}
void FunctionSpec(List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/>/*!*/ 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<Expression/*!*/>/*!*/ 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<Expression/*!*/>/*!*/ 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<Expression/*!*/>/*!*/ 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<Statement/*!*/>/*!*/ ss) {
@@ -952,6 +968,7 @@ List<Expression/*!*/>/*!*/ 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<Expression/*!*/>/*!*/ 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<Expression/*!*/>/*!*/ decreases) { ReturnStmt(out s);
break;
}
- default: SynErr(115); break;
+ default: SynErr(133); break;
}
}
@@ -1093,7 +1111,7 @@ List<Expression/*!*/>/*!*/ 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<Expression/*!*/>/*!*/ decreases) { Expect(17);
UpdateStmt update;
if (rhss.Count == 0) {
- update = null;
+ update = null;
} else {
- var ies = new List<Expression>();
- foreach (var lhs in lhss) {
- ies.Add(new AutoGhostIdentifierExpr(lhs.Tok, lhs.Name));
- }
- update = new UpdateStmt(assignTok, ies, rhss);
+ var ies = new List<Expression>();
+ 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<Expression/*!*/>/*!*/ 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<Expression/*!*/>/*!*/ 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<Expression/*!*/>/*!*/ decreases) { Expect(48);
returnTok = t;
- if (StartOf(10)) {
+ if (StartOf(13)) {
Rhs(out r, null);
rhss = new List<AssignmentRhs>(); rhss.Add(r);
while (la.kind == 19) {
@@ -1298,7 +1316,7 @@ List<Expression/*!*/>/*!*/ decreases) { Ident(out x);
Expect(33);
args = new List<Expression/*!*/>();
- if (StartOf(6)) {
+ if (StartOf(8)) {
Expressions(args);
}
Expect(34);
@@ -1309,7 +1327,7 @@ List<Expression/*!*/>/*!*/ 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<Expression/*!*/>/*!*/ 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<Expression/*!*/>/*!*/ 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<Expression/*!*/>/*!*/ args) {
@@ -1360,10 +1378,10 @@ List<Expression/*!*/>/*!*/ 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<Expression/*!*/>/*!*/ decreases) { Expression(out e);
Expect(58);
body = new List<Statement>();
- while (StartOf(7)) {
+ while (StartOf(9)) {
Stmt(body);
}
alternatives.Add(new GuardedAlternative(x, e, body));
@@ -1389,30 +1407,29 @@ List<Expression/*!*/>/*!*/ decreases) { }
void LoopSpec(out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*/> decreases, out List<FrameExpression/*!*/> mod) {
- bool isFree; Expression/*!*/ e; FrameExpression/*!*/ fe;
+ FrameExpression/*!*/ fe;
invariants = new List<MaybeFreeExpression/*!*/>();
+ MaybeFreeExpression invariant = null;
decreases = new List<Expression/*!*/>();
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<FrameExpression>();
- if (StartOf(6)) {
+ if (StartOf(8)) {
FrameExpression(out fe);
mod.Add(fe);
while (la.kind == 19) {
@@ -1421,11 +1438,24 @@ List<Expression/*!*/>/*!*/ 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<Expression/*!*/>/*!*/ 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<Expression/*!*/>/*!*/ 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<BoundVar/*!*/> bvars, out Attributes attrs, out Expression range) {
@@ -1514,13 +1544,13 @@ List<Expression/*!*/>/*!*/ 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<Expression/*!*/>/*!*/ decreases) { Get();
} else if (la.kind == 69) {
Get();
- } else SynErr(125);
+ } else SynErr(149);
}
void RelationalExpression(out Expression/*!*/ e) {
@@ -1561,23 +1591,23 @@ List<Expression/*!*/>/*!*/ decreases) { List<Expression> chain = null;
List<BinaryExpr.Opcode> 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<Expression>();
ops = new List<BinaryExpr.Opcode>();
@@ -1631,11 +1661,11 @@ List<Expression/*!*/>/*!*/ 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<Expression/*!*/>/*!*/ decreases) { Get();
} else if (la.kind == 71) {
Get();
- } else SynErr(126);
+ } else SynErr(150);
}
void OrOp() {
@@ -1658,7 +1688,7 @@ List<Expression/*!*/>/*!*/ decreases) { Get();
} else if (la.kind == 73) {
Get();
- } else SynErr(127);
+ } else SynErr(151);
}
void Term(out Expression/*!*/ e0) {
@@ -1727,10 +1757,10 @@ List<Expression/*!*/>/*!*/ 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<Expression/*!*/>/*!*/ decreases) { x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- default: SynErr(128); break;
+ default: SynErr(152); break;
}
}
@@ -1772,7 +1802,7 @@ List<Expression/*!*/>/*!*/ 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<Expression/*!*/>/*!*/ decreases) { }
break;
}
- default: SynErr(130); break;
+ default: SynErr(154); break;
}
}
@@ -1833,7 +1863,7 @@ List<Expression/*!*/>/*!*/ 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<Expression/*!*/>/*!*/ decreases) { Get();
} else if (la.kind == 88) {
Get();
- } else SynErr(132);
+ } else SynErr(156);
}
void EndlessExpression(out Expression e) {
@@ -1918,7 +1948,7 @@ List<Expression/*!*/>/*!*/ decreases) { e = new LetExpr(x, letVars, letRHSs, e);
break;
}
- default: SynErr(133); break;
+ default: SynErr(157); break;
}
}
@@ -1937,7 +1967,7 @@ List<Expression/*!*/>/*!*/ decreases) { if (la.kind == 33) {
Get();
openParen = t; args = new List<Expression>();
- if (StartOf(6)) {
+ if (StartOf(8)) {
Expressions(args);
}
Expect(34);
@@ -1957,7 +1987,7 @@ List<Expression/*!*/>/*!*/ decreases) { if (la.kind == 33) {
Get();
args = new List<Expression/*!*/>(); func = true;
- if (StartOf(6)) {
+ if (StartOf(8)) {
Expressions(args);
}
Expect(34);
@@ -1967,13 +1997,13 @@ List<Expression/*!*/>/*!*/ 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<Expression/*!*/>/*!*/ 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<Expression/*!*/>/*!*/ decreases) { if (la.kind == 7) {
Get();
x = t; elements = new List<Expression/*!*/>();
- if (StartOf(6)) {
+ if (StartOf(8)) {
Expressions(elements);
}
e = new SetDisplayExpr(x, elements);
@@ -2043,12 +2073,12 @@ List<Expression/*!*/>/*!*/ decreases) { } else if (la.kind == 51) {
Get();
x = t; elements = new List<Expression/*!*/>();
- 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<Expression/*!*/>/*!*/ decreases) { if (la.kind == 7) {
Get();
elements = new List<Expression/*!*/>();
- if (StartOf(6)) {
+ if (StartOf(8)) {
Expressions(elements);
}
e = new MultiSetDisplayExpr(x, elements);
@@ -2072,9 +2102,9 @@ List<Expression/*!*/>/*!*/ 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<Expression/*!*/>/*!*/ decreases) { Expect(34);
break;
}
- default: SynErr(139); break;
+ default: SynErr(163); break;
}
}
@@ -2160,8 +2190,8 @@ List<Expression/*!*/>/*!*/ 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<Expression/*!*/>/*!*/ 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<Expression/*!*/>/*!*/ decreases) { Get();
} else if (la.kind == 99) {
Get();
- } else SynErr(141);
+ } else SynErr(165);
}
void Exists() {
@@ -2272,7 +2302,7 @@ List<Expression/*!*/>/*!*/ decreases) { Get();
} else if (la.kind == 101) {
Get();
- } else SynErr(142);
+ } else SynErr(166);
}
void QSep() {
@@ -2280,7 +2310,7 @@ List<Expression/*!*/>/*!*/ decreases) { Get();
} else if (la.kind == 103) {
Get();
- } else SynErr(143);
+ } else SynErr(167);
}
void AttributeBody(ref Attributes attrs) {
@@ -2291,7 +2321,7 @@ List<Expression/*!*/>/*!*/ 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<Expression/*!*/>/*!*/ 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<Expression/*!*/>/*!*/ 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<string>() != 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<string>() != 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<Token>() != null);
@@ -787,7 +792,7 @@ void objectInvariant(){ }
pt = pt.next;
} while (pt.kind > maxT); // skip pragmas
-
+
return pt;
}
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index d1e41663..5f382eb6 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -1499,7 +1499,7 @@ namespace Microsoft.Dafny { Bpl.Expr.Eq(Bpl.Expr.Literal(mod.CallGraph.GetSCCRepresentativeId(f)), etran.FunctionContextHeight()));
req.Add(Requires(f.tok, true, context, null, null));
Bpl.Procedure proc = new Bpl.Procedure(f.tok, "CheckWellformed$$" + f.FullName, typeParams, inParams, new Bpl.VariableSeq(),
- req, new Bpl.IdentifierExprSeq(), new Bpl.EnsuresSeq());
+ req, new Bpl.IdentifierExprSeq(), new Bpl.EnsuresSeq(), etran.TrAttributes(f.Attributes, null));
sink.TopLevelDeclarations.Add(proc);
VariableSeq implInParams = Bpl.Formal.StripWhereClauses(proc.InParams);
diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index 80e24356..6cc225d9 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -368,7 +368,7 @@ namespace Microsoft.Dafny }
}
- /// <summary>
+ /// <summary>
/// Resolve, type check, infer invariants for, and verify the given Boogie program.
/// The intention is that this Boogie program has been produced by translation from something
/// else. Hence, any resolution errors and type checking errors are due to errors in
diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs index 5e33e78d..f1d06590 100644 --- a/Source/GPUVerify/GPUVerifier.cs +++ b/Source/GPUVerify/GPUVerifier.cs @@ -37,29 +37,29 @@ namespace GPUVerify private const string _Y_name = "_Y";
private const string _Z_name = "_Z";
- private Constant _TILE_SIZE_X = null;
- private Constant _TILE_SIZE_Y = null;
- private Constant _TILE_SIZE_Z = null;
+ private Constant _GROUP_SIZE_X = null;
+ private Constant _GROUP_SIZE_Y = null;
+ private Constant _GROUP_SIZE_Z = null;
- private const string _TILE_SIZE_X_name = "_TILE_SIZE_X";
- private const string _TILE_SIZE_Y_name = "_TILE_SIZE_Y";
- private const string _TILE_SIZE_Z_name = "_TILE_SIZE_Z";
+ private const string _GROUP_SIZE_X_name = "_GROUP_SIZE_X";
+ private const string _GROUP_SIZE_Y_name = "_GROUP_SIZE_Y";
+ private const string _GROUP_SIZE_Z_name = "_GROUP_SIZE_Z";
- private Constant _TILE_X = null;
- private Constant _TILE_Y = null;
- private Constant _TILE_Z = null;
+ private Constant _GROUP_X = null;
+ private Constant _GROUP_Y = null;
+ private Constant _GROUP_Z = null;
- private const string _TILE_X_name = "_TILE_X";
- private const string _TILE_Y_name = "_TILE_Y";
- private const string _TILE_Z_name = "_TILE_Z";
+ private const string _GROUP_X_name = "_GROUP_X";
+ private const string _GROUP_Y_name = "_GROUP_Y";
+ private const string _GROUP_Z_name = "_GROUP_Z";
- private Constant _NUM_TILES_X = null;
- private Constant _NUM_TILES_Y = null;
- private Constant _NUM_TILES_Z = null;
+ private Constant _NUM_GROUPS_X = null;
+ private Constant _NUM_GROUPS_Y = null;
+ private Constant _NUM_GROUPS_Z = null;
- private const string _NUM_TILES_X_name = "_NUM_TILES_X";
- private const string _NUM_TILES_Y_name = "_NUM_TILES_Y";
- private const string _NUM_TILES_Z_name = "_NUM_TILES_Z";
+ private const string _NUM_GROUPS_X_name = "_NUM_GROUPS_X";
+ private const string _NUM_GROUPS_Y_name = "_NUM_GROUPS_Y";
+ private const string _NUM_GROUPS_Z_name = "_NUM_GROUPS_Z";
public IRaceInstrumenter RaceInstrumenter;
@@ -113,6 +113,11 @@ namespace GPUVerify continue;
}
+ if (decl is Implementation)
+ {
+ continue;
+ }
+
if (decl is Procedure)
{
if (attributedProcedure == null)
@@ -143,9 +148,9 @@ namespace GPUVerify {
foreach (LocalVariable LV in KernelImplementation.LocVars)
{
- if (QKeyValue.FindBoolAttribute(LV.Attributes, "tile_static"))
+ if (QKeyValue.FindBoolAttribute(LV.Attributes, "group_shared"))
{
- Error(LV.tok, "Local variable must not be marked 'tile_static' -- promote the variable to global scope");
+ Error(LV.tok, "Local variable must not be marked 'group_shared' -- promote the variable to global scope");
}
}
}
@@ -158,11 +163,11 @@ namespace GPUVerify {
if (!ReservedNames.Contains((D as Variable).Name))
{
- if (QKeyValue.FindBoolAttribute(D.Attributes, "tile_static"))
+ if (QKeyValue.FindBoolAttribute(D.Attributes, "group_shared"))
{
- NonLocalState.getTileStaticVariables().Add(D as Variable);
+ NonLocalState.getGroupSharedVariables().Add(D as Variable);
}
- else
+ else if(QKeyValue.FindBoolAttribute(D.Attributes, "global"))
{
NonLocalState.getGlobalVariables().Add(D as Variable);
}
@@ -186,50 +191,50 @@ namespace GPUVerify CheckSpecialConstantType(C);
_Z = C;
}
- if (C.Name.Equals(_TILE_SIZE_X_name))
+ if (C.Name.Equals(_GROUP_SIZE_X_name))
{
CheckSpecialConstantType(C);
- _TILE_SIZE_X = C;
+ _GROUP_SIZE_X = C;
}
- if (C.Name.Equals(_TILE_SIZE_Y_name))
+ if (C.Name.Equals(_GROUP_SIZE_Y_name))
{
CheckSpecialConstantType(C);
- _TILE_SIZE_Y = C;
+ _GROUP_SIZE_Y = C;
}
- if (C.Name.Equals(_TILE_SIZE_Z_name))
+ if (C.Name.Equals(_GROUP_SIZE_Z_name))
{
CheckSpecialConstantType(C);
- _TILE_SIZE_Z = C;
+ _GROUP_SIZE_Z = C;
}
- if (C.Name.Equals(_TILE_X_name))
+ if (C.Name.Equals(_GROUP_X_name))
{
CheckSpecialConstantType(C);
- _TILE_X = C;
+ _GROUP_X = C;
}
- if (C.Name.Equals(_TILE_Y_name))
+ if (C.Name.Equals(_GROUP_Y_name))
{
CheckSpecialConstantType(C);
- _TILE_Y = C;
+ _GROUP_Y = C;
}
- if (C.Name.Equals(_TILE_Z_name))
+ if (C.Name.Equals(_GROUP_Z_name))
{
CheckSpecialConstantType(C);
- _TILE_Z = C;
+ _GROUP_Z = C;
}
- if (C.Name.Equals(_NUM_TILES_X_name))
+ if (C.Name.Equals(_NUM_GROUPS_X_name))
{
CheckSpecialConstantType(C);
- _NUM_TILES_X = C;
+ _NUM_GROUPS_X = C;
}
- if (C.Name.Equals(_NUM_TILES_Y_name))
+ if (C.Name.Equals(_NUM_GROUPS_Y_name))
{
CheckSpecialConstantType(C);
- _NUM_TILES_Y = C;
+ _NUM_GROUPS_Y = C;
}
- if (C.Name.Equals(_NUM_TILES_Z_name))
+ if (C.Name.Equals(_NUM_GROUPS_Z_name))
{
CheckSpecialConstantType(C);
- _NUM_TILES_Z = C;
+ _NUM_GROUPS_Z = C;
}
}
@@ -866,49 +871,49 @@ namespace GPUVerify return _Z != null;
}
- public bool KernelHasTileIdX()
+ public bool KernelHasGroupIdX()
{
- return _TILE_X != null;
+ return _GROUP_X != null;
}
- public bool KernelHasTileIdY()
+ public bool KernelHasGroupIdY()
{
- return _TILE_Y != null;
+ return _GROUP_Y != null;
}
- public bool KernelHasTileIdZ()
+ public bool KernelHasGroupIdZ()
{
- return _TILE_Z != null;
+ return _GROUP_Z != null;
}
- public bool KernelHasNumTilesX()
+ public bool KernelHasNumGroupsX()
{
- return _NUM_TILES_X != null;
+ return _NUM_GROUPS_X != null;
}
- public bool KernelHasNumTilesY()
+ public bool KernelHasNumGroupsY()
{
- return _NUM_TILES_Y != null;
+ return _NUM_GROUPS_Y != null;
}
- public bool KernelHasNumTilesZ()
+ public bool KernelHasNumGroupsZ()
{
- return _NUM_TILES_Z != null;
+ return _NUM_GROUPS_Z != null;
}
- public bool KernelHasTileSizeX()
+ public bool KernelHasGroupSizeX()
{
- return _TILE_SIZE_X != null;
+ return _GROUP_SIZE_X != null;
}
- public bool KernelHasTileSizeY()
+ public bool KernelHasGroupSizeY()
{
- return _TILE_SIZE_Y != null;
+ return _GROUP_SIZE_Y != null;
}
- public bool KernelHasTileSizeZ()
+ public bool KernelHasGroupSizeZ()
{
- return _TILE_SIZE_Z != null;
+ return _GROUP_SIZE_Z != null;
}
public bool KernelHasId(string dimension)
@@ -1129,17 +1134,17 @@ namespace GPUVerify if (GetTypeOfId(dimension).Equals(Microsoft.Boogie.Type.GetBvType(32)))
{
- Proc.Requires.Add(new Requires(false, MakeBitVectorBinaryBoolean("BV32_GT", new IdentifierExpr(tok, GetTileSize(dimension)), ZeroBV(tok))));
- Proc.Requires.Add(new Requires(false, MakeBitVectorBinaryBoolean("BV32_GT", new IdentifierExpr(tok, GetNumTiles(dimension)), ZeroBV(tok))));
- Proc.Requires.Add(new Requires(false, MakeBitVectorBinaryBoolean("BV32_GEQ", new IdentifierExpr(tok, GetTileId(dimension)), ZeroBV(tok))));
- Proc.Requires.Add(new Requires(false, MakeBitVectorBinaryBoolean("BV32_LT", new IdentifierExpr(tok, GetTileId(dimension)), new IdentifierExpr(tok, GetNumTiles(dimension)))));
+ Proc.Requires.Add(new Requires(false, MakeBitVectorBinaryBoolean("BV32_GT", new IdentifierExpr(tok, GetGroupSize(dimension)), ZeroBV(tok))));
+ Proc.Requires.Add(new Requires(false, MakeBitVectorBinaryBoolean("BV32_GT", new IdentifierExpr(tok, GetNumGroups(dimension)), ZeroBV(tok))));
+ Proc.Requires.Add(new Requires(false, MakeBitVectorBinaryBoolean("BV32_GEQ", new IdentifierExpr(tok, GetGroupId(dimension)), ZeroBV(tok))));
+ Proc.Requires.Add(new Requires(false, MakeBitVectorBinaryBoolean("BV32_LT", new IdentifierExpr(tok, GetGroupId(dimension)), new IdentifierExpr(tok, GetNumGroups(dimension)))));
}
else
{
- Proc.Requires.Add(new Requires(false, Expr.Gt(new IdentifierExpr(tok, GetTileSize(dimension)), Zero(tok))));
- Proc.Requires.Add(new Requires(false, Expr.Gt(new IdentifierExpr(tok, GetNumTiles(dimension)), Zero(tok))));
- Proc.Requires.Add(new Requires(false, Expr.Ge(new IdentifierExpr(tok, GetTileId(dimension)), Zero(tok))));
- Proc.Requires.Add(new Requires(false, Expr.Lt(new IdentifierExpr(tok, GetTileId(dimension)), new IdentifierExpr(tok, GetNumTiles(dimension)))));
+ Proc.Requires.Add(new Requires(false, Expr.Gt(new IdentifierExpr(tok, GetGroupSize(dimension)), Zero(tok))));
+ Proc.Requires.Add(new Requires(false, Expr.Gt(new IdentifierExpr(tok, GetNumGroups(dimension)), Zero(tok))));
+ Proc.Requires.Add(new Requires(false, Expr.Ge(new IdentifierExpr(tok, GetGroupId(dimension)), Zero(tok))));
+ Proc.Requires.Add(new Requires(false, Expr.Lt(new IdentifierExpr(tok, GetGroupId(dimension)), new IdentifierExpr(tok, GetNumGroups(dimension)))));
}
}
@@ -1159,8 +1164,8 @@ namespace GPUVerify MakeBitVectorBinaryBoolean("BV32_GEQ", new IdentifierExpr(tok, MakeThreadId(tok, dimension, 2)), ZeroBV(tok))
),
Expr.And(
- MakeBitVectorBinaryBoolean("BV32_LT", new IdentifierExpr(tok, MakeThreadId(tok, dimension, 1)), new IdentifierExpr(tok, GetTileSize(dimension))),
- MakeBitVectorBinaryBoolean("BV32_LT", new IdentifierExpr(tok, MakeThreadId(tok, dimension, 2)), new IdentifierExpr(tok, GetTileSize(dimension)))
+ MakeBitVectorBinaryBoolean("BV32_LT", new IdentifierExpr(tok, MakeThreadId(tok, dimension, 1)), new IdentifierExpr(tok, GetGroupSize(dimension))),
+ MakeBitVectorBinaryBoolean("BV32_LT", new IdentifierExpr(tok, MakeThreadId(tok, dimension, 2)), new IdentifierExpr(tok, GetGroupSize(dimension)))
))
:
Expr.And(
@@ -1169,8 +1174,8 @@ namespace GPUVerify Expr.Ge(new IdentifierExpr(tok, MakeThreadId(tok, dimension, 2)), Zero(tok))
),
Expr.And(
- Expr.Lt(new IdentifierExpr(tok, MakeThreadId(tok, dimension, 1)), new IdentifierExpr(tok, GetTileSize(dimension))),
- Expr.Lt(new IdentifierExpr(tok, MakeThreadId(tok, dimension, 2)), new IdentifierExpr(tok, GetTileSize(dimension)))
+ Expr.Lt(new IdentifierExpr(tok, MakeThreadId(tok, dimension, 1)), new IdentifierExpr(tok, GetGroupSize(dimension))),
+ Expr.Lt(new IdentifierExpr(tok, MakeThreadId(tok, dimension, 2)), new IdentifierExpr(tok, GetGroupSize(dimension)))
));
AssumeThreadIdsInRange = (null == AssumeThreadIdsInRange) ? AssumeThreadIdsInRangeInDimension : Expr.And(AssumeThreadIdsInRange, AssumeThreadIdsInRangeInDimension);
@@ -1185,22 +1190,22 @@ namespace GPUVerify }), new LocalVariable(lhs.tok, new TypedIdent(lhs.tok, "result", Microsoft.Boogie.Type.Bool)))), new ExprSeq(new Expr[] { lhs, rhs }));
}
- private Constant GetTileSize(string dimension)
+ private Constant GetGroupSize(string dimension)
{
Contract.Requires(dimension.Equals("X") || dimension.Equals("Y") || dimension.Equals("Z"));
- if (dimension.Equals("X")) return _TILE_SIZE_X;
- if (dimension.Equals("Y")) return _TILE_SIZE_Y;
- if (dimension.Equals("Z")) return _TILE_SIZE_Z;
+ if (dimension.Equals("X")) return _GROUP_SIZE_X;
+ if (dimension.Equals("Y")) return _GROUP_SIZE_Y;
+ if (dimension.Equals("Z")) return _GROUP_SIZE_Z;
Debug.Assert(false);
return null;
}
- private Constant GetNumTiles(string dimension)
+ private Constant GetNumGroups(string dimension)
{
Contract.Requires(dimension.Equals("X") || dimension.Equals("Y") || dimension.Equals("Z"));
- if (dimension.Equals("X")) return _NUM_TILES_X;
- if (dimension.Equals("Y")) return _NUM_TILES_Y;
- if (dimension.Equals("Z")) return _NUM_TILES_Z;
+ if (dimension.Equals("X")) return _NUM_GROUPS_X;
+ if (dimension.Equals("Y")) return _NUM_GROUPS_Y;
+ if (dimension.Equals("Z")) return _NUM_GROUPS_Z;
Debug.Assert(false);
return null;
}
@@ -1217,12 +1222,12 @@ namespace GPUVerify return new Constant(tok, new TypedIdent(tok, "_" + dimension + "$" + number, GetTypeOfId(dimension)));
}
- private Constant GetTileId(string dimension)
+ private Constant GetGroupId(string dimension)
{
Contract.Requires(dimension.Equals("X") || dimension.Equals("Y") || dimension.Equals("Z"));
- if (dimension.Equals("X")) return _TILE_X;
- if (dimension.Equals("Y")) return _TILE_Y;
- if (dimension.Equals("Z")) return _TILE_Z;
+ if (dimension.Equals("X")) return _GROUP_X;
+ if (dimension.Equals("Y")) return _GROUP_Y;
+ if (dimension.Equals("Z")) return _GROUP_Z;
Debug.Assert(false);
return null;
}
@@ -1436,7 +1441,7 @@ namespace GPUVerify foreach (Variable v in impl.LocVars)
{
- Debug.Assert(!NonLocalState.getTileStaticVariables().Contains(v));
+ Debug.Assert(!NonLocalState.getGroupSharedVariables().Contains(v));
NewLocVars.Add(v);
}
@@ -2184,22 +2189,22 @@ namespace GPUVerify Error(KernelProcedure.tok, "Kernel must declare global constant '" + _X_name + "'");
}
- if (!KernelHasTileSizeX())
+ if (!KernelHasGroupSizeX())
{
- Error(KernelProcedure.tok, "Kernel must declare global constant '" + _TILE_SIZE_X_name + "'");
+ Error(KernelProcedure.tok, "Kernel must declare global constant '" + _GROUP_SIZE_X_name + "'");
}
- if (!KernelHasNumTilesX())
+ if (!KernelHasNumGroupsX())
{
- Error(KernelProcedure.tok, "Kernel must declare global constant '" + _NUM_TILES_X_name + "'");
+ Error(KernelProcedure.tok, "Kernel must declare global constant '" + _NUM_GROUPS_X_name + "'");
}
- if (!KernelHasTileIdX())
+ if (!KernelHasGroupIdX())
{
- Error(KernelProcedure.tok, "Kernel must declare global constant '" + _TILE_X_name + "'");
+ Error(KernelProcedure.tok, "Kernel must declare global constant '" + _GROUP_X_name + "'");
}
- if (KernelHasIdY() || KernelHasTileSizeY() || KernelHasNumTilesY() || KernelHasTileIdY())
+ if (KernelHasIdY() || KernelHasGroupSizeY() || KernelHasNumGroupsY() || KernelHasGroupIdY())
{
if (!KernelHasIdY())
@@ -2207,24 +2212,24 @@ namespace GPUVerify Error(KernelProcedure.tok, "2D kernel must declare global constant '" + _Y_name + "'");
}
- if (!KernelHasTileSizeY())
+ if (!KernelHasGroupSizeY())
{
- Error(KernelProcedure.tok, "2D kernel must declare global constant '" + _TILE_SIZE_Y_name + "'");
+ Error(KernelProcedure.tok, "2D kernel must declare global constant '" + _GROUP_SIZE_Y_name + "'");
}
- if (!KernelHasNumTilesY())
+ if (!KernelHasNumGroupsY())
{
- Error(KernelProcedure.tok, "2D kernel must declare global constant '" + _NUM_TILES_Y_name + "'");
+ Error(KernelProcedure.tok, "2D kernel must declare global constant '" + _NUM_GROUPS_Y_name + "'");
}
- if (!KernelHasTileIdY())
+ if (!KernelHasGroupIdY())
{
- Error(KernelProcedure.tok, "2D kernel must declare global constant '" + _TILE_Y_name + "'");
+ Error(KernelProcedure.tok, "2D kernel must declare global constant '" + _GROUP_Y_name + "'");
}
}
- if (KernelHasIdZ() || KernelHasTileSizeZ() || KernelHasNumTilesZ() || KernelHasTileIdZ())
+ if (KernelHasIdZ() || KernelHasGroupSizeZ() || KernelHasNumGroupsZ() || KernelHasGroupIdZ())
{
if (!KernelHasIdY())
@@ -2232,19 +2237,19 @@ namespace GPUVerify Error(KernelProcedure.tok, "3D kernel must declare global constant '" + _Y_name + "'");
}
- if (!KernelHasTileSizeY())
+ if (!KernelHasGroupSizeY())
{
- Error(KernelProcedure.tok, "3D kernel must declare global constant '" + _TILE_SIZE_Y_name + "'");
+ Error(KernelProcedure.tok, "3D kernel must declare global constant '" + _GROUP_SIZE_Y_name + "'");
}
- if (!KernelHasNumTilesY())
+ if (!KernelHasNumGroupsY())
{
- Error(KernelProcedure.tok, "3D kernel must declare global constant '" + _NUM_TILES_Y_name + "'");
+ Error(KernelProcedure.tok, "3D kernel must declare global constant '" + _NUM_GROUPS_Y_name + "'");
}
- if (!KernelHasTileIdY())
+ if (!KernelHasGroupIdY())
{
- Error(KernelProcedure.tok, "3D kernel must declare global constant '" + _TILE_Y_name + "'");
+ Error(KernelProcedure.tok, "3D kernel must declare global constant '" + _GROUP_Y_name + "'");
}
if (!KernelHasIdZ())
@@ -2252,19 +2257,19 @@ namespace GPUVerify Error(KernelProcedure.tok, "3D kernel must declare global constant '" + _Z_name + "'");
}
- if (!KernelHasTileSizeZ())
+ if (!KernelHasGroupSizeZ())
{
- Error(KernelProcedure.tok, "3D kernel must declare global constant '" + _TILE_SIZE_Z_name + "'");
+ Error(KernelProcedure.tok, "3D kernel must declare global constant '" + _GROUP_SIZE_Z_name + "'");
}
- if (!KernelHasNumTilesZ())
+ if (!KernelHasNumGroupsZ())
{
- Error(KernelProcedure.tok, "3D kernel must declare global constant '" + _NUM_TILES_Z_name + "'");
+ Error(KernelProcedure.tok, "3D kernel must declare global constant '" + _NUM_GROUPS_Z_name + "'");
}
- if (!KernelHasTileIdZ())
+ if (!KernelHasGroupIdZ())
{
- Error(KernelProcedure.tok, "3D kernel must declare global constant '" + _TILE_Z_name + "'");
+ Error(KernelProcedure.tok, "3D kernel must declare global constant '" + _GROUP_Z_name + "'");
}
}
@@ -2272,41 +2277,6 @@ namespace GPUVerify return ErrorCount;
}
- private bool HasNamedConstant(string dimension, string Name)
- {
- foreach (Declaration d in Program.TopLevelDeclarations)
- {
- if (d is Variable && (d as Variable).Name.Equals(Name + dimension))
- {
- Variable v = d as Variable;
- if (v is Constant && IsIntOrBv32(v.TypedIdent.Type))
- {
- return true;
- }
- else
- {
- Error(v.tok, "Declaration '" + Name + dimension + "' must be a constant integer");
- }
- }
- }
- return false;
- }
-
- private bool HasTileId(string dimension)
- {
- return HasNamedConstant(dimension, "_tile_");
- }
-
- private bool HasNumTiles(string dimension)
- {
- return HasNamedConstant(dimension, "NUM_TILES_");
- }
-
- private bool HasTileSize(string dimension)
- {
- return HasNamedConstant(dimension, "TILE_SIZE_");
- }
-
public static bool IsThreadLocalIdConstant(Variable variable)
{
return variable is Constant && (variable.Name.Equals(_X_name) || variable.Name.Equals(_Y_name) || variable.Name.Equals(_Z_name));
diff --git a/Source/GPUVerify/INonLocalState.cs b/Source/GPUVerify/INonLocalState.cs index 0e03d685..c6211dab 100644 --- a/Source/GPUVerify/INonLocalState.cs +++ b/Source/GPUVerify/INonLocalState.cs @@ -11,7 +11,7 @@ namespace GPUVerify ICollection<Variable> getGlobalVariables();
- ICollection<Variable> getTileStaticVariables();
+ ICollection<Variable> getGroupSharedVariables();
ICollection<Variable> getAllNonLocalVariables();
diff --git a/Source/GPUVerify/Main.cs b/Source/GPUVerify/Main.cs index e38aabea..1be30dc9 100644 --- a/Source/GPUVerify/Main.cs +++ b/Source/GPUVerify/Main.cs @@ -97,11 +97,11 @@ namespace GPUVerify Variable newG = findClonedVar(v, newGp.NonLocalState.getGlobalVariables());
- Variable newT = findClonedVar(v, newGp.NonLocalState.getTileStaticVariables());
+ Variable newT = findClonedVar(v, newGp.NonLocalState.getGroupSharedVariables());
Contract.Assert(newG == null || newT == null);
ri.NonLocalStateToCheck.getGlobalVariables().Clear();
- ri.NonLocalStateToCheck.getTileStaticVariables().Clear();
+ ri.NonLocalStateToCheck.getGroupSharedVariables().Clear();
ri.onlyLog1 = a1;
ri.onlyLog2 = a2;
@@ -112,7 +112,7 @@ namespace GPUVerify if (newT != null)
{
- ri.NonLocalStateToCheck.getTileStaticVariables().Add(newT);
+ ri.NonLocalStateToCheck.getGroupSharedVariables().Add(newT);
}
newGp.doit();
diff --git a/Source/GPUVerify/NonLocalStateLists.cs b/Source/GPUVerify/NonLocalStateLists.cs index a4b5e154..c47cddd5 100644 --- a/Source/GPUVerify/NonLocalStateLists.cs +++ b/Source/GPUVerify/NonLocalStateLists.cs @@ -10,12 +10,12 @@ namespace GPUVerify class NonLocalStateLists : INonLocalState
{
private List<Variable> GlobalVariables;
- private List<Variable> TileStaticVariables;
+ private List<Variable> GroupSharedVariables;
public NonLocalStateLists()
{
GlobalVariables = new List<Variable>();
- TileStaticVariables = new List<Variable>();
+ GroupSharedVariables = new List<Variable>();
}
public ICollection<Variable> getGlobalVariables()
@@ -23,16 +23,16 @@ namespace GPUVerify return GlobalVariables;
}
- public ICollection<Variable> getTileStaticVariables()
+ public ICollection<Variable> getGroupSharedVariables()
{
- return TileStaticVariables;
+ return GroupSharedVariables;
}
public ICollection<Variable> getAllNonLocalVariables()
{
List<Variable> all = new List<Variable>();
all.AddRange(GlobalVariables);
- all.AddRange(TileStaticVariables);
+ all.AddRange(GroupSharedVariables);
return all;
}
diff --git a/Source/GPUVerify/RaceInstrumenterBase.cs b/Source/GPUVerify/RaceInstrumenterBase.cs index 4f2f76be..692f1288 100644 --- a/Source/GPUVerify/RaceInstrumenterBase.cs +++ b/Source/GPUVerify/RaceInstrumenterBase.cs @@ -38,9 +38,9 @@ namespace GPUVerify {
NonLocalStateToCheck.getGlobalVariables().Add(v);
}
- foreach(Variable v in verifier.NonLocalState.getTileStaticVariables())
+ foreach(Variable v in verifier.NonLocalState.getGroupSharedVariables())
{
- NonLocalStateToCheck.getTileStaticVariables().Add(v);
+ NonLocalStateToCheck.getGroupSharedVariables().Add(v);
}
}
diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index ed3d1afc..6cd961ac 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -255,25 +255,48 @@ namespace Microsoft.Boogie.Houdini { private Checker checker;
private Graph<Implementation> callGraph;
private bool continueAtError;
+ private HashSet<Implementation> vcgenFailures;
public Houdini(Program program, bool continueAtError) {
this.program = program;
- this.callGraph = BuildCallGraph();
this.continueAtError = continueAtError;
+
+ if (CommandLineOptions.Clo.Trace)
+ Console.WriteLine("Collecting existential constants...");
this.houdiniConstants = CollectExistentialConstants();
+
+ if (CommandLineOptions.Clo.Trace)
+ Console.WriteLine("Building call graph...");
+ this.callGraph = BuildCallGraph();
+ if (CommandLineOptions.Clo.Trace)
+ Console.WriteLine("Number of implementations = {0}", callGraph.Nodes.Count);
+
Inline();
+
this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
this.checker = new Checker(vcgen, program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, CommandLineOptions.Clo.ProverKillTime);
+ vcgenFailures = new HashSet<Implementation>();
Dictionary<Implementation, HoudiniSession> houdiniSessions = new Dictionary<Implementation, HoudiniSession>();
+ if (CommandLineOptions.Clo.Trace)
+ Console.WriteLine("Beginning VC generation for Houdini...");
foreach (Implementation impl in callGraph.Nodes) {
- // make a different simplify log file for each function
- String simplifyLog = null;
- if (CommandLineOptions.Clo.SimplifyLogFilePath != null) {
- simplifyLog = impl.ToString() + CommandLineOptions.Clo.SimplifyLogFilePath;
+ try {
+ if (CommandLineOptions.Clo.Trace)
+ Console.WriteLine("Generating VC for {0}", impl.Name);
+ // make a different simplify log file for each function
+ String simplifyLog = null;
+ if (CommandLineOptions.Clo.SimplifyLogFilePath != null) {
+ simplifyLog = impl.ToString() + CommandLineOptions.Clo.SimplifyLogFilePath;
+ }
+ HoudiniSession session = new HoudiniSession(vcgen, checker, program, impl, simplifyLog, CommandLineOptions.Clo.SimplifyLogFileAppend);
+ houdiniSessions.Add(impl, session);
+ }
+ catch (VCGenException) {
+ if (CommandLineOptions.Clo.Trace)
+ Console.WriteLine("VC generation failed");
+ vcgenFailures.Add(impl);
}
- HoudiniSession session = new HoudiniSession(vcgen, checker, program, impl, simplifyLog, CommandLineOptions.Clo.SimplifyLogFileAppend);
- houdiniSessions.Add(impl, session);
}
this.houdiniSessions = new ReadOnlyDictionary<Implementation, HoudiniSession>(houdiniSessions);
}
@@ -281,17 +304,43 @@ namespace Microsoft.Boogie.Houdini { private void Inline() {
if (CommandLineOptions.Clo.InlineDepth < 0)
return;
+
foreach (Implementation impl in callGraph.Nodes) {
impl.OriginalBlocks = impl.Blocks;
impl.OriginalLocVars = impl.LocVars;
}
foreach (Implementation impl in callGraph.Nodes) {
+ CommandLineOptions.Inlining savedOption = CommandLineOptions.Clo.ProcedureInlining;
+ CommandLineOptions.Clo.ProcedureInlining = CommandLineOptions.Inlining.Spec;
Inliner.ProcessImplementationForHoudini(program, impl);
+ CommandLineOptions.Clo.ProcedureInlining = savedOption;
}
foreach (Implementation impl in callGraph.Nodes) {
impl.OriginalBlocks = null;
impl.OriginalLocVars = null;
}
+
+ Graph<Implementation> oldCallGraph = callGraph;
+ callGraph = new Graph<Implementation>();
+ foreach (Implementation impl in oldCallGraph.Nodes) {
+ callGraph.AddSource(impl);
+ }
+ foreach (Tuple<Implementation, Implementation> edge in oldCallGraph.Edges) {
+ callGraph.AddEdge(edge.Item1, edge.Item2);
+ }
+ int count = CommandLineOptions.Clo.InlineDepth;
+ while (count > 0) {
+ foreach (Implementation impl in oldCallGraph.Nodes) {
+ List<Implementation> newNodes = new List<Implementation>();
+ foreach (Implementation succ in callGraph.Successors(impl)) {
+ newNodes.AddRange(oldCallGraph.Successors(succ));
+ }
+ foreach (Implementation newNode in newNodes) {
+ callGraph.AddEdge(impl, newNode);
+ }
+ }
+ count--;
+ }
}
private ReadOnlyDictionary<string, IdentifierExpr> CollectExistentialConstants() {
@@ -349,6 +398,7 @@ namespace Microsoft.Boogie.Houdini { sccs.Compute();
foreach (SCC<Implementation> scc in sccs) {
foreach (Implementation impl in scc) {
+ if (vcgenFailures.Contains(impl)) continue;
queue.Enqueue(impl);
}
}
@@ -806,6 +856,9 @@ namespace Microsoft.Boogie.Houdini { public HoudiniOutcome PerformHoudiniInference() {
HoudiniState current = new HoudiniState(BuildWorkList(program), BuildAssignment(houdiniConstants.Keys));
this.NotifyStart(program, houdiniConstants.Keys.Count);
+ foreach (Implementation impl in vcgenFailures) {
+ current.addToBlackList(impl.Name);
+ }
while (current.WorkQueue.Count > 0) {
bool exceptional = false;
|