From a4765e1bd6f66b4571760f60883270df02025882 Mon Sep 17 00:00:00 2001 From: rustanleino Date: Thu, 4 Feb 2010 22:14:26 +0000 Subject: Dafny: Added if-then-else expressions (replacing and extending the previous boolean-only if-then-else expressions) Dafny: Added 'class' functions and methods (i.e., functions and methods with a receiver parameter) Dafny grammar changes: Tthe 'use' keyword now goes before 'function' (akin to 'ghost' and 'class'), and quantifier triggers now go before the '::' Dafny: Check for division-by-zero for both '/' and '%' --- Binaries/DafnyPrelude.bpl | 8 + Source/Dafny/Dafny.atg | 113 ++++----- Source/Dafny/DafnyAst.ssc | 19 +- Source/Dafny/Parser.ssc | 590 ++++++++++++++++++++++---------------------- Source/Dafny/Printer.ssc | 90 ++++--- Source/Dafny/Resolver.ssc | 71 +++++- Source/Dafny/Scanner.ssc | 64 ++--- Source/Dafny/Translator.ssc | 132 ++++++---- Test/dafny0/Answer | 34 ++- Test/dafny0/Simple.dfy | 8 + Test/dafny0/SmallTests.dfy | 23 ++ Test/dafny0/Use.dfy | 6 +- Util/Emacs/dafny-mode.el | 2 +- Util/latex/dafny.sty | 2 +- 14 files changed, 661 insertions(+), 501 deletions(-) diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 60de3d84..50433b54 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -152,6 +152,14 @@ axiom (forall s: Seq T, n: int, j: int :: { Seq#Index(Seq#Drop(s,n), j) } 0 <= n && 0 <= j && j < Seq#Length(s)-n ==> Seq#Index(Seq#Drop(s,n), j) == Seq#Index(s, j+n)); +// --------------------------------------------------------------- +// -- If then else ----------------------------------------------- +// --------------------------------------------------------------- + +function $ite(bool, T, T): T; +axiom (forall g: bool, a,b: T :: { $ite(g,a,b) } + (g ==> $ite(g,a,b) == a) && (!g ==> $ite(g,a,b) == b)); + // --------------------------------------------------------------- // -- Boxing and unboxing ---------------------------------------- // --------------------------------------------------------------- diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index a6eba750..9e30ab85 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -27,6 +27,12 @@ static Attributes.Argument! dummyAttrArg = new Attributes.Argument("dummyAttrArg static Scope! parseVarScope = new Scope(); static int anonymousIds = 0; +struct MemberModifiers { + public bool IsGhost; + public bool IsClass; + public bool IsUse; +} + // helper routine for parsing call statements private static void RecordCallLhs(IdentifierExpr! e, List! lhs, @@ -135,11 +141,15 @@ ClassDecl ClassMemberDecl! mm> = (. Method! m; Function! f; + MemberModifiers mmod = new MemberModifiers(); .) - ( FieldDecl - | FunctionDecl (. mm.Add(f); .) - | MethodDecl (. mm.Add(m); .) - | FrameDecl + { "ghost" (. mmod.IsGhost = true; .) + | "class" (. mmod.IsClass = true; .) + | "use" (. mmod.IsUse = true; .) + } + ( FieldDecl + | FunctionDecl (. mm.Add(f); .) + | MethodDecl (. mm.Add(m); .) ) . @@ -176,15 +186,17 @@ DatatypeMemberDecl! ctors> ";" . -FieldDecl! mm> +FieldDecl! mm> = (. Attributes attrs = null; Token! id; Type! ty; .) - [ "ghost" ] "var" + (. if (mmod.IsUse) { SemErr(token, "fields cannot be declared 'use'"); } + if (mmod.IsClass) { SemErr(token, "fields cannot be declared 'class'"); } + .) { Attribute } - IdentType (. mm.Add(new Field(id, id.val, ty, attrs)); .) - { "," IdentType (. mm.Add(new Field(id, id.val, ty, attrs)); .) + IdentType (. mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); .) + { "," IdentType (. mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); .) } ";" . @@ -237,21 +249,9 @@ GenericParameters! typeArgs> ">" . -FrameDecl -= (. Token! id; - Attributes attrs = null; - .) - "frame" - { Attribute } - Ident - "{" - /* TBD */ - "}" - . - /*------------------------------------------------------------------------*/ -MethodDecl +MethodDecl = (. Token! id; Attributes attrs = null; List! typeArgs = new List(); @@ -263,6 +263,9 @@ MethodDecl Statement! bb; Statement body = null; .) "method" + (. if (mmod.IsGhost) { SemErr(token, "methods cannot be declared 'ghost'"); } + if (mmod.IsUse) { SemErr(token, "methods cannot be declared 'use'"); } + .) { Attribute } Ident [ GenericParameters ] @@ -277,7 +280,7 @@ MethodDecl ) (. parseVarScope.PopMarker(); - m = new Method(id, id.val, typeArgs, ins, outs, req, mod, ens, body, attrs); + m = new Method(id, id.val, mmod.IsClass, typeArgs, ins, outs, req, mod, ens, body, attrs); .) . @@ -369,7 +372,7 @@ GenericInstantiation! gt> /*------------------------------------------------------------------------*/ -FunctionDecl +FunctionDecl = (. Attributes attrs = null; Token! id; List typeArgs = new List(); @@ -379,11 +382,11 @@ FunctionDecl List reads = new List(); List decreases = new List(); Expression! bb; Expression body = null; - bool use = false; .) "function" + (. if (mmod.IsGhost) { SemErr(token, "functions cannot be declared 'ghost'"); } + .) { Attribute } - [ "use" (. use = true; .) ] Ident [ GenericParameters ] (. parseVarScope.PushMarker(); .) @@ -396,7 +399,7 @@ FunctionDecl FunctionBody (. body = bb; .) ) (. parseVarScope.PopMarker(); - f = new Function(id, id.val, use, typeArgs, formals, returnType, reqs, reads, decreases, body, attrs); + f = new Function(id, id.val, mmod.IsClass, mmod.IsUse, typeArgs, formals, returnType, reqs, reads, decreases, body, attrs); .) . @@ -434,33 +437,12 @@ PossiblyWildExpression FunctionBody = (. e = dummyExpr; .) "{" - ( IfThenElseExpr - | MatchExpression + ( MatchExpression | Expression ) "}" . -ExtendedExpr -= (. e = dummyExpr; .) - "{" - ( IfThenElseExpr - | Expression - ) - "}" - . - -IfThenElseExpr -= (. Token! x; Expression! e0; Expression! e1 = dummyExpr; .) - "if" (. x = token; .) - "(" Expression ")" - ExtendedExpr - "else" - ( IfThenElseExpr - | ExtendedExpr - ) (. e = new ITEExpr(x, e, e0, e1); .) - . - MatchExpression = (. Token! x; List cases = new List(); @@ -586,7 +568,7 @@ HavocStmt . LhsExpr -= Expression /* TODO: restrict LHS further */ += SelectExpression . VarDeclStmts! ss> @@ -773,8 +755,20 @@ UseStmt . /*------------------------------------------------------------------------*/ +Expression += (. Token! x; Expression! e0; Expression! e1 = dummyExpr; + e = dummyExpr; + .) + ( "if" (. x = token; .) + Expression + "then" Expression + "else" Expression (. e = new ITEExpr(x, e, e0, e1); .) + | EquivExpression + ) + . -Expression +/*------------------------------------------------------------------------*/ +EquivExpression = (. Token! x; Expression! e1; .) ImpliesExpression { EquivOp (. x = token; .) @@ -908,16 +902,6 @@ ConstAtomExpression | "|" (. x = token; .) Expression (. e = new UnaryExpr(x, UnaryExpr.Opcode.SeqLength, e); .) "|" - /* Note, the following open-curly-brace causes grammar ambiguities that result in two Coco warnings. - One of these is the confusion between BlockStmt and AssignStmt, the former starting with an open - curly brace and the latter starting with a left-hand side Expression, which syntactically can - start with an open curly brace. The other is the confusion between a quantifier's triggers/attributes - and the quantifier's body. The disamiguation I've chosen involves giving priority to BlockStmt - (since no semantically legal AssignStmt can have a set constructor as its left-hand side) and to - triggers/attributes (which, unfortunately, changes what programs are syntactically allowed, but there - is a simple workaround, which is for a user to put parentheses around any quantifier body that begins - with a set constructor. - */ | "{" (. x = token; elements = new List(); .) [ Expressions ] (. e = new SetDisplayExpr(x, elements); .) "}" @@ -1042,15 +1026,8 @@ QuantifierGuts { "," IdentTypeOptional (. bvars.Add(bv); parseVarScope.Push(bv.Name, bv.Name); .) } - QSep - /* The grammar is ambiguous in how to resolve triggers/attributes versus the expression body. - However, the loop generated by Coco for the next two lines of grammar declarations is still - fine--it will loop, picking up as many triggers/attributes it can before going on to parse an - expression. This seems good, because there's a simple workaround for quantifier bodies that - begin with a set constructor: simply put parentheses around the quantifier body. See also - the Note in production ConstAtomExpression. - */ { AttributeOrTrigger } + QSep Expression (. if (univ) { q = new ForallExpr(x, bvars, body, trigs, attrs); diff --git a/Source/Dafny/DafnyAst.ssc b/Source/Dafny/DafnyAst.ssc index 38c3b87d..01e55cfd 100644 --- a/Source/Dafny/DafnyAst.ssc +++ b/Source/Dafny/DafnyAst.ssc @@ -391,9 +391,11 @@ namespace Microsoft.Dafny } public class Field : MemberDecl { + public readonly bool IsGhost; public readonly Type! Type; - public Field(Token! tok, string! name, Type! type, Attributes attributes) { + public Field(Token! tok, string! name, bool isGhost, Type! type, Attributes attributes) { + IsGhost = isGhost; Type = type; base(tok, name, attributes); } @@ -458,7 +460,8 @@ namespace Microsoft.Dafny } public class Function : MemberDecl, TypeParameter.ParentType { - public readonly bool Use; + public readonly bool IsClass; + public readonly bool IsUse; public readonly List! TypeArgs; public readonly List! Formals; public readonly Type! ResultType; @@ -467,9 +470,10 @@ namespace Microsoft.Dafny public readonly List! Decreases; public readonly Expression Body; // an extended expression - public Function(Token! tok, string! name, bool use, [Captured] List! typeArgs, [Captured] List! formals, Type! resultType, + public Function(Token! tok, string! name, bool isClass, bool isUse, [Captured] List! typeArgs, [Captured] List! formals, Type! resultType, List! req, List! reads, List! decreases, Expression body, Attributes attributes) { - this.Use = use; + this.IsClass = isClass; + this.IsUse = isUse; this.TypeArgs = typeArgs; this.Formals = formals; this.ResultType = resultType; @@ -482,6 +486,7 @@ namespace Microsoft.Dafny } public class Method : MemberDecl, TypeParameter.ParentType { + public readonly bool IsClass; public readonly List! TypeArgs; public readonly List! Ins; public readonly List! Outs; @@ -491,11 +496,13 @@ namespace Microsoft.Dafny public readonly Statement Body; public Method(Token! tok, string! name, + bool isClass, [Captured] List! typeArgs, [Captured] List! ins, [Captured] List! outs, [Captured] List! req, [Captured] List! mod, [Captured] List! ens, [Captured] Statement body, Attributes attributes) { + this.IsClass = isClass; this.TypeArgs = typeArgs; this.Ins = ins; this.Outs = outs; @@ -977,7 +984,7 @@ namespace Microsoft.Dafny public class UseExpr : FunctionCallExpr { [NotDelayed] [Captured] public UseExpr(FunctionCallExpr! fce) - requires fce.Function != null && fce.Function.Use; + requires fce.Function != null && fce.Function.IsUse; { base(fce.tok, fce.Name, fce.Receiver, new List(fce.Args)); this.Function = fce.Function; @@ -1115,7 +1122,7 @@ namespace Microsoft.Dafny } } - public class ITEExpr : Expression { // an ITEExpr is an "extended expression" and is only allowed in certain places + public class ITEExpr : Expression { public readonly Expression! Test; public readonly Expression! Thn; public readonly Expression! Els; diff --git a/Source/Dafny/Parser.ssc b/Source/Dafny/Parser.ssc index 50079f11..76bb32bc 100644 --- a/Source/Dafny/Parser.ssc +++ b/Source/Dafny/Parser.ssc @@ -25,6 +25,12 @@ static Attributes.Argument! dummyAttrArg = new Attributes.Argument("dummyAttrArg static Scope! parseVarScope = new Scope(); static int anonymousIds = 0; +struct MemberModifiers { + public bool IsGhost; + public bool IsClass; + public bool IsUse; +} + // helper routine for parsing call statements private static void RecordCallLhs(IdentifierExpr! e, List! lhs, @@ -133,7 +139,7 @@ public static int Parse (List! classes) { static void Dafny() { ClassDecl! c; DatatypeDecl! dt; - while (t.kind == 4 || t.kind == 7) { + while (t.kind == 4 || t.kind == 9) { if (t.kind == 4) { ClassDecl(out c); theClasses.Add(c); @@ -156,7 +162,7 @@ public static int Parse (List! classes) { Attribute(ref attrs); } Ident(out id); - if (t.kind == 13) { + if (t.kind == 14) { GenericParameters(typeArgs); } Expect(5); @@ -173,12 +179,12 @@ public static int Parse (List! classes) { List typeArgs = new List(); List ctors = new List(); - Expect(7); + Expect(9); while (t.kind == 5) { Attribute(ref attrs); } Ident(out id); - if (t.kind == 13) { + if (t.kind == 14) { GenericParameters(typeArgs); } Expect(5); @@ -202,56 +208,67 @@ public static int Parse (List! classes) { static void GenericParameters(List! typeArgs) { Token! id; - Expect(13); + Expect(14); Ident(out id); typeArgs.Add(new TypeParameter(id, id.val)); - while (t.kind == 11) { + while (t.kind == 12) { Get(); Ident(out id); typeArgs.Add(new TypeParameter(id, id.val)); } - Expect(14); + Expect(15); } static void ClassMemberDecl(List! mm) { Method! m; Function! f; + MemberModifiers mmod = new MemberModifiers(); - if (t.kind == 9 || t.kind == 10) { - FieldDecl(mm); + while (t.kind == 4 || t.kind == 7 || t.kind == 8) { + if (t.kind == 7) { + Get(); + mmod.IsGhost = true; + } else if (t.kind == 4) { + Get(); + mmod.IsClass = true; + } else { + Get(); + mmod.IsUse = true; + } + } + if (t.kind == 11) { + FieldDecl(mmod, mm); } else if (t.kind == 29) { - FunctionDecl(out f); + FunctionDecl(mmod, out f); mm.Add(f); } else if (t.kind == 16) { - MethodDecl(out m); + MethodDecl(mmod, out m); mm.Add(m); - } else if (t.kind == 15) { - FrameDecl(); } else Error(94); } - static void FieldDecl(List! mm) { + static void FieldDecl(MemberModifiers mmod, List! mm) { Attributes attrs = null; Token! id; Type! ty; - if (t.kind == 9) { - Get(); - } - Expect(10); + Expect(11); + if (mmod.IsUse) { SemErr(token, "fields cannot be declared 'use'"); } + if (mmod.IsClass) { SemErr(token, "fields cannot be declared 'class'"); } + while (t.kind == 5) { Attribute(ref attrs); } IdentType(out id, out ty); - mm.Add(new Field(id, id.val, ty, attrs)); - while (t.kind == 11) { + mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); + while (t.kind == 12) { Get(); IdentType(out id, out ty); - mm.Add(new Field(id, id.val, ty, attrs)); + mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); } - Expect(8); + Expect(10); } - static void FunctionDecl(out Function! f) { + static void FunctionDecl(MemberModifiers mmod, out Function! f) { Attributes attrs = null; Token! id; List typeArgs = new List(); @@ -261,42 +278,39 @@ public static int Parse (List! classes) { List reads = new List(); List decreases = new List(); Expression! bb; Expression body = null; - bool use = false; Expect(29); + if (mmod.IsGhost) { SemErr(token, "functions cannot be declared 'ghost'"); } + while (t.kind == 5) { Attribute(ref attrs); } - if (t.kind == 30) { - Get(); - use = true; - } Ident(out id); - if (t.kind == 13) { + if (t.kind == 14) { GenericParameters(typeArgs); } parseVarScope.PushMarker(); Formals(true, formals); - Expect(12); + Expect(13); Type(out returnType); - if (t.kind == 8) { + if (t.kind == 10) { Get(); - while (t.kind == 20 || t.kind == 31 || t.kind == 32) { + while (t.kind == 20 || t.kind == 30 || t.kind == 31) { FunctionSpec(reqs, reads, decreases); } } else if (StartOf(2)) { - while (t.kind == 20 || t.kind == 31 || t.kind == 32) { + while (t.kind == 20 || t.kind == 30 || t.kind == 31) { FunctionSpec(reqs, reads, decreases); } FunctionBody(out bb); body = bb; } else Error(95); parseVarScope.PopMarker(); - f = new Function(id, id.val, use, typeArgs, formals, returnType, reqs, reads, decreases, body, attrs); + f = new Function(id, id.val, mmod.IsClass, mmod.IsUse, typeArgs, formals, returnType, reqs, reads, decreases, body, attrs); } - static void MethodDecl(out Method! m) { + static void MethodDecl(MemberModifiers mmod, out Method! m) { Token! id; Attributes attrs = null; List! typeArgs = new List(); @@ -308,11 +322,14 @@ public static int Parse (List! classes) { Statement! bb; Statement body = null; Expect(16); + if (mmod.IsGhost) { SemErr(token, "methods cannot be declared 'ghost'"); } + if (mmod.IsUse) { SemErr(token, "methods cannot be declared 'use'"); } + while (t.kind == 5) { Attribute(ref attrs); } Ident(out id); - if (t.kind == 13) { + if (t.kind == 14) { GenericParameters(typeArgs); } parseVarScope.PushMarker(); @@ -321,7 +338,7 @@ public static int Parse (List! classes) { Get(); Formals(false, outs); } - if (t.kind == 8) { + if (t.kind == 10) { Get(); while (StartOf(3)) { MethodSpec(req, mod, ens); @@ -334,23 +351,10 @@ public static int Parse (List! classes) { body = bb; } else Error(96); parseVarScope.PopMarker(); - m = new Method(id, id.val, typeArgs, ins, outs, req, mod, ens, body, attrs); + m = new Method(id, id.val, mmod.IsClass, typeArgs, ins, outs, req, mod, ens, body, attrs); } - static void FrameDecl() { - Token! id; - Attributes attrs = null; - - Expect(15); - while (t.kind == 5) { - Attribute(ref attrs); - } - Ident(out id); - Expect(5); - Expect(6); - } - static void DatatypeMemberDecl(List! ctors) { Attributes attrs = null; Token! id; @@ -361,7 +365,7 @@ public static int Parse (List! classes) { Attribute(ref attrs); } Ident(out id); - if (t.kind == 13) { + if (t.kind == 14) { GenericParameters(typeArgs); } parseVarScope.PushMarker(); @@ -371,7 +375,7 @@ public static int Parse (List! classes) { parseVarScope.PopMarker(); ctors.Add(new DatatypeCtor(id, id.val, typeArgs, formals, attrs)); - Expect(8); + Expect(10); } static void FormalsOptionalIds(List! formals) { @@ -380,7 +384,7 @@ public static int Parse (List! classes) { if (StartOf(5)) { TypeIdentOptional(out id, out name, out ty); formals.Add(new Formal(id, name, ty, true)); parseVarScope.Push(name, name); - while (t.kind == 11) { + while (t.kind == 12) { Get(); TypeIdentOptional(out id, out name, out ty); formals.Add(new Formal(id, name, ty, true)); parseVarScope.Push(name, name); @@ -391,7 +395,7 @@ public static int Parse (List! classes) { static void IdentType(out Token! id, out Type! ty) { Ident(out id); - Expect(12); + Expect(13); Type(out ty); } @@ -404,7 +408,7 @@ public static int Parse (List! classes) { Token! id; Type! ty; Type optType = null; Ident(out id); - if (t.kind == 12) { + if (t.kind == 13) { Get(); Type(out ty); optType = ty; @@ -415,7 +419,7 @@ public static int Parse (List! classes) { static void TypeIdentOptional(out Token! id, out string! identName, out Type! ty) { string name = null; TypeAndToken(out id, out ty); - if (t.kind == 12) { + if (t.kind == 13) { Get(); UserDefinedType udt = ty as UserDefinedType; if (udt != null && udt.TypeArgs.Count == 0) { @@ -473,7 +477,7 @@ public static int Parse (List! classes) { if (t.kind == 1) { IdentType(out id, out ty); formals.Add(new Formal(id, id.val, ty, incoming)); parseVarScope.Push(id.val, id.val); - while (t.kind == 11) { + while (t.kind == 12) { Get(); IdentType(out id, out ty); formals.Add(new Formal(id, id.val, ty, incoming)); parseVarScope.Push(id.val, id.val); @@ -490,13 +494,13 @@ public static int Parse (List! classes) { if (StartOf(6)) { Expression(out e); mod.Add(e); - while (t.kind == 11) { + while (t.kind == 12) { Get(); Expression(out e); mod.Add(e); } } - Expect(8); + Expect(10); } else if (t.kind == 19 || t.kind == 20 || t.kind == 21) { if (t.kind == 19) { Get(); @@ -505,12 +509,12 @@ public static int Parse (List! classes) { if (t.kind == 20) { Get(); Expression(out e); - Expect(8); + Expect(10); req.Add(new MaybeFreeExpression(e, isFree)); } else if (t.kind == 21) { Get(); Expression(out e); - Expect(8); + Expect(10); ens.Add(new MaybeFreeExpression(e, isFree)); } else Error(98); } else Error(99); @@ -532,28 +536,35 @@ public static int Parse (List! classes) { parseVarScope.PopMarker(); } - static void Expression(out Expression! e0) { - Token! x; Expression! e1; - ImpliesExpression(out e0); - while (t.kind == 53 || t.kind == 54) { - EquivOp(); + static void Expression(out Expression! e) { + Token! x; Expression! e0; Expression! e1 = dummyExpr; + e = dummyExpr; + + if (t.kind == 42) { + Get(); x = token; - ImpliesExpression(out e1); - e0 = new BinaryExpr(x, BinaryExpr.Opcode.Iff, e0, e1); - } + Expression(out e); + Expect(52); + Expression(out e0); + Expect(43); + Expression(out e1); + e = new ITEExpr(x, e, e0, e1); + } else if (StartOf(8)) { + EquivExpression(out e); + } else Error(100); } static void GenericInstantiation(List! gt) { Type! ty; - Expect(13); + Expect(14); Type(out ty); gt.Add(ty); - while (t.kind == 11) { + while (t.kind == 12) { Get(); Type(out ty); gt.Add(ty); } - Expect(14); + Expect(15); } static void ReferenceType(out Token! tok, out Type! ty) { @@ -566,11 +577,11 @@ public static int Parse (List! classes) { } else if (t.kind == 1) { Ident(out tok); gt = new List(); - if (t.kind == 13) { + if (t.kind == 14) { GenericInstantiation(gt); } ty = new UserDefinedType(tok, tok.val, gt); - } else Error(100); + } else Error(101); } static void FunctionSpec(List! reqs, List! reads, List! decreases) { @@ -578,31 +589,29 @@ public static int Parse (List! classes) { if (t.kind == 20) { Get(); Expression(out e); - Expect(8); + Expect(10); reqs.Add(e); - } else if (t.kind == 31) { + } else if (t.kind == 30) { Get(); - if (StartOf(8)) { + if (StartOf(9)) { PossiblyWildExpressions(reads); } - Expect(8); - } else if (t.kind == 32) { + Expect(10); + } else if (t.kind == 31) { Get(); Expressions(decreases); - Expect(8); - } else Error(101); + Expect(10); + } else Error(102); } static void FunctionBody(out Expression! e) { e = dummyExpr; Expect(5); - if (t.kind == 34) { - IfThenElseExpr(out e); - } else if (t.kind == 36) { + if (t.kind == 33) { MatchExpression(out e); } else if (StartOf(6)) { Expression(out e); - } else Error(102); + } else Error(103); Expect(6); } @@ -610,7 +619,7 @@ public static int Parse (List! classes) { Expression! e; PossiblyWildExpression(out e); args.Add(e); - while (t.kind == 11) { + while (t.kind == 12) { Get(); PossiblyWildExpression(out e); args.Add(e); @@ -621,7 +630,7 @@ public static int Parse (List! classes) { Expression! e; Expression(out e); args.Add(e); - while (t.kind == 11) { + while (t.kind == 12) { Get(); Expression(out e); args.Add(e); @@ -630,62 +639,34 @@ public static int Parse (List! classes) { static void PossiblyWildExpression(out Expression! e) { e = dummyExpr; - if (t.kind == 33) { + if (t.kind == 32) { Get(); e = new WildcardExpr(token); } else if (StartOf(6)) { Expression(out e); - } else Error(103); - } - - static void IfThenElseExpr(out Expression! e) { - Token! x; Expression! e0; Expression! e1 = dummyExpr; - Expect(34); - x = token; - Expect(22); - Expression(out e); - Expect(23); - ExtendedExpr(out e0); - Expect(35); - if (t.kind == 34) { - IfThenElseExpr(out e1); - } else if (t.kind == 5) { - ExtendedExpr(out e1); } else Error(104); - e = new ITEExpr(x, e, e0, e1); } static void MatchExpression(out Expression! e) { Token! x; List cases = new List(); - Expect(36); + Expect(33); x = token; Expression(out e); if (t.kind == 5) { Get(); CaseExpressions(cases); Expect(6); - } else if (t.kind == 6 || t.kind == 37) { + } else if (t.kind == 6 || t.kind == 34) { CaseExpressions(cases); } else Error(105); e = new MatchExpr(x, e, cases); } - static void ExtendedExpr(out Expression! e) { - e = dummyExpr; - Expect(5); - if (t.kind == 34) { - IfThenElseExpr(out e); - } else if (StartOf(6)) { - Expression(out e); - } else Error(106); - Expect(6); - } - static void CaseExpressions(List! cases) { MatchCase! c; - while (t.kind == 37) { + while (t.kind == 34) { CaseExpression(out c); cases.Add(c); } @@ -696,7 +677,7 @@ public static int Parse (List! classes) { List arguments = new List(); Expression! body; - Expect(37); + Expect(34); x = token; parseVarScope.PushMarker(); Ident(out id); if (t.kind == 22) { @@ -704,7 +685,7 @@ public static int Parse (List! classes) { Ident(out arg); arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy())); parseVarScope.Push(arg.val, arg.val); - while (t.kind == 11) { + while (t.kind == 12) { Get(); Ident(out arg); arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy())); @@ -712,7 +693,7 @@ public static int Parse (List! classes) { } Expect(23); } - Expect(38); + Expect(35); Expression(out body); c = new MatchCase(x, id.val, arguments, body); parseVarScope.PopMarker(); @@ -724,12 +705,12 @@ public static int Parse (List! classes) { BlockStmt(out s); ss.Add(s); } - if (StartOf(9)) { + if (StartOf(10)) { OneStmt(out s); ss.Add(s); - } else if (t.kind == 9 || t.kind == 10) { + } else if (t.kind == 7 || t.kind == 11) { VarDeclStmts(ss); - } else Error(107); + } else Error(106); } static void OneStmt(out Statement! s) { @@ -737,112 +718,112 @@ public static int Parse (List! classes) { s = dummyStmt; /* to please the compiler */ switch (t.kind) { - case 51: { + case 50: { AssertStmt(out s); break; } - case 52: { + case 51: { AssumeStmt(out s); break; } - case 30: { + case 8: { UseStmt(out s); break; } - case 1: case 2: case 5: case 22: case 50: case 71: case 74: case 75: case 76: case 77: case 78: case 79: case 81: case 82: case 85: case 86: { + case 1: case 22: case 85: case 86: { AssignStmt(out s); break; } - case 44: { + case 41: { HavocStmt(out s); break; } - case 47: { + case 46: { CallStmt(out s); break; } - case 34: { + case 42: { IfStmt(out s); break; } - case 45: { + case 44: { WhileStmt(out s); break; } - case 48: { + case 47: { ForeachStmt(out s); break; } - case 39: { + case 36: { Get(); x = token; Ident(out id); - Expect(12); + Expect(13); s = new LabelStmt(x, id.val); break; } - case 40: { + case 37: { Get(); x = token; if (t.kind == 1) { Ident(out id); label = id.val; } - Expect(8); + Expect(10); s = new BreakStmt(x, label); break; } - case 41: { + case 38: { Get(); x = token; - Expect(8); + Expect(10); s = new ReturnStmt(x); break; } - default: Error(108); break; + default: Error(107); break; } } static void VarDeclStmts(List! ss) { VarDecl! d; - if (t.kind == 9) { + if (t.kind == 7) { Get(); } - Expect(10); + Expect(11); IdentTypeRhs(out d); ss.Add(d); parseVarScope.Push(d.Name, d.Name); - while (t.kind == 11) { + while (t.kind == 12) { Get(); IdentTypeRhs(out d); ss.Add(d); parseVarScope.Push(d.Name, d.Name); } - Expect(8); + Expect(10); } static void AssertStmt(out Statement! s) { Token! x; Expression! e; - Expect(51); + Expect(50); x = token; Expression(out e); - Expect(8); + Expect(10); s = new AssertStmt(x, e); } static void AssumeStmt(out Statement! s) { Token! x; Expression! e; - Expect(52); + Expect(51); x = token; Expression(out e); - Expect(8); + Expect(10); s = new AssumeStmt(x, e); } static void UseStmt(out Statement! s) { Token! x; Expression! e; - Expect(30); + Expect(8); x = token; Expression(out e); - Expect(8); + Expect(10); s = new UseStmt(x, e); } @@ -854,7 +835,7 @@ public static int Parse (List! classes) { s = dummyStmt; LhsExpr(out lhs); - Expect(42); + Expect(39); x = token; AssignRhs(out rhs, out ty); if (rhs != null) { @@ -864,15 +845,15 @@ public static int Parse (List! classes) { s = new AssignStmt(x, lhs, ty); } - Expect(8); + Expect(10); } static void HavocStmt(out Statement! s) { Token! x; Expression! lhs; - Expect(44); + Expect(41); x = token; LhsExpr(out lhs); - Expect(8); + Expect(10); s = new AssignStmt(x, lhs); } @@ -882,11 +863,11 @@ public static int Parse (List! classes) { List lhs = new List(); List newVars = new List(); - Expect(47); + Expect(46); x = token; CallStmtSubExpr(out e); - if (t.kind == 11 || t.kind == 42) { - if (t.kind == 11) { + if (t.kind == 12 || t.kind == 39) { + if (t.kind == 12) { Get(); e = ConvertToLocal(e); if (e is IdentifierExpr) { @@ -899,12 +880,12 @@ public static int Parse (List! classes) { Ident(out id); RecordCallLhs(new IdentifierExpr(id, id.val), lhs, newVars); - while (t.kind == 11) { + while (t.kind == 12) { Get(); Ident(out id); RecordCallLhs(new IdentifierExpr(id, id.val), lhs, newVars); } - Expect(42); + Expect(39); CallStmtSubExpr(out e); } else { Get(); @@ -920,7 +901,7 @@ public static int Parse (List! classes) { CallStmtSubExpr(out e); } } - Expect(8); + Expect(10); if (e is FunctionCallExpr) { FunctionCallExpr fce = (FunctionCallExpr)e; s = new CallStmt(x, newVars, lhs, fce.Receiver, fce.Name, fce.Args); // this actually does an ownership transfer of fce.Args @@ -938,19 +919,19 @@ public static int Parse (List! classes) { Statement! s; Statement els = null; - Expect(34); + Expect(42); x = token; Guard(out guard); BlockStmt(out thn); - if (t.kind == 35) { + if (t.kind == 43) { Get(); - if (t.kind == 34) { + if (t.kind == 42) { IfStmt(out s); els = s; } else if (t.kind == 5) { BlockStmt(out s); els = s; - } else Error(109); + } else Error(108); } ifStmt = new IfStmt(x, guard, thn, els); } @@ -963,25 +944,25 @@ public static int Parse (List! classes) { List decreases = new List(); Statement! body; - Expect(45); + Expect(44); x = token; Guard(out guard); assume guard == null || Owner.None(guard); - while (t.kind == 19 || t.kind == 32 || t.kind == 46) { - if (t.kind == 19 || t.kind == 46) { + while (t.kind == 19 || t.kind == 31 || t.kind == 45) { + if (t.kind == 19 || t.kind == 45) { isFree = false; if (t.kind == 19) { Get(); isFree = true; } - Expect(46); + Expect(45); Expression(out e); invariants.Add(new MaybeFreeExpression(e, isFree)); - Expect(8); + Expect(10); } else { Get(); PossiblyWildExpressions(decreases); - Expect(8); + Expect(10); } } BlockStmt(out body); @@ -997,31 +978,31 @@ public static int Parse (List! classes) { AssignStmt bodyAssign = null; parseVarScope.PushMarker(); - Expect(48); + Expect(47); x = token; range = new LiteralExpr(x, true); ty = new InferredTypeProxy(); Expect(22); Ident(out boundVar); - if (t.kind == 12) { + if (t.kind == 13) { Get(); Type(out ty); } - Expect(49); + Expect(48); Expression(out collection); parseVarScope.Push(boundVar.val, boundVar.val); - if (t.kind == 50) { + if (t.kind == 49) { Get(); Expression(out range); } Expect(23); Expect(5); - while (t.kind == 30 || t.kind == 51 || t.kind == 52) { - if (t.kind == 51) { + while (t.kind == 8 || t.kind == 50 || t.kind == 51) { + if (t.kind == 50) { AssertStmt(out s); if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); } - } else if (t.kind == 52) { + } else if (t.kind == 51) { AssumeStmt(out s); if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); } } else { @@ -1029,49 +1010,61 @@ public static int Parse (List! classes) { if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); } } } - if (StartOf(6)) { + if (StartOf(11)) { AssignStmt(out s); if (s is AssignStmt) { bodyAssign = (AssignStmt)s; } - } else if (t.kind == 44) { + } else if (t.kind == 41) { HavocStmt(out s); if (s is AssignStmt) { bodyAssign = (AssignStmt)s; } - } else Error(110); + } else Error(109); Expect(6); s = new ForeachStmt(x, new BoundVar(boundVar, boundVar.val, ty), collection, range, bodyPrefix, bodyAssign); parseVarScope.PopMarker(); } static void LhsExpr(out Expression! e) { - Expression(out e); + SelectExpression(out e); } static void AssignRhs(out Expression e, out Type ty) { Token! x; Expression! ee; Type! tt; e = null; ty = null; - if (t.kind == 43) { + if (t.kind == 40) { Get(); ReferenceType(out x, out tt); ty = tt; } else if (StartOf(6)) { Expression(out ee); e = ee; - } else Error(111); + } else Error(110); if (e == null && ty == null) { e = dummyExpr; } } + static void SelectExpression(out Expression! e) { + Token! id; e = dummyExpr; + if (t.kind == 1) { + IdentOrFuncExpression(out e); + } else if (t.kind == 22 || t.kind == 85 || t.kind == 86) { + ObjectExpression(out e); + } else Error(111); + while (t.kind == 80 || t.kind == 82) { + SelectOrCallSuffix(ref e); + } + } + static void IdentTypeRhs(out VarDecl! d) { Token! id; Type! ty; Expression! e; Expression rhs = null; Type newType = null; Type optionalType = null; DeterminedAssignmentRhs optionalRhs = null; Ident(out id); - if (t.kind == 12) { + if (t.kind == 13) { Get(); Type(out ty); optionalType = ty; } - if (t.kind == 42) { + if (t.kind == 39) { Get(); AssignRhs(out rhs, out newType); } @@ -1090,7 +1083,7 @@ public static int Parse (List! classes) { static void Guard(out Expression e) { Expression! ee; e = null; Expect(22); - if (t.kind == 33) { + if (t.kind == 32) { Get(); e = null; } else if (StartOf(6)) { @@ -1113,6 +1106,17 @@ public static int Parse (List! classes) { } } + static void EquivExpression(out Expression! e0) { + Token! x; Expression! e1; + ImpliesExpression(out e0); + while (t.kind == 53 || t.kind == 54) { + EquivOp(); + x = token; + ImpliesExpression(out e1); + e0 = new BinaryExpr(x, BinaryExpr.Opcode.Iff, e0, e1); + } + } + static void ImpliesExpression(out Expression! e0) { Token! x; Expression! e1; LogicalExpression(out e0); @@ -1135,7 +1139,7 @@ public static int Parse (List! classes) { static void LogicalExpression(out Expression! e0) { Token! x; Expression! e1; RelationalExpression(out e0); - if (StartOf(10)) { + if (StartOf(12)) { if (t.kind == 57 || t.kind == 58) { AndOp(); x = token; @@ -1173,7 +1177,7 @@ public static int Parse (List! classes) { static void RelationalExpression(out Expression! e0) { Token! x; Expression! e1; BinaryExpr.Opcode op; Term(out e0); - if (StartOf(11)) { + if (StartOf(13)) { RelOp(out x, out op); Term(out e1); e0 = new BinaryExpr(x, op, e0, e1); @@ -1214,12 +1218,12 @@ public static int Parse (List! classes) { x = token; op = BinaryExpr.Opcode.Eq; break; } - case 13: { + case 14: { Get(); x = token; op = BinaryExpr.Opcode.Lt; break; } - case 14: { + case 15: { Get(); x = token; op = BinaryExpr.Opcode.Gt; break; @@ -1244,7 +1248,7 @@ public static int Parse (List! classes) { x = token; op = BinaryExpr.Opcode.Disjoint; break; } - case 49: { + case 48: { Get(); x = token; op = BinaryExpr.Opcode.In; break; @@ -1276,7 +1280,7 @@ public static int Parse (List! classes) { static void Factor(out Expression! e0) { Token! x; Expression! e1; BinaryExpr.Opcode op; UnaryExpression(out e0); - while (t.kind == 33 || t.kind == 72 || t.kind == 73) { + while (t.kind == 32 || t.kind == 72 || t.kind == 73) { MulOp(out x, out op); UnaryExpression(out e1); e0 = new BinaryExpr(x, op, e0, e1); @@ -1306,16 +1310,16 @@ public static int Parse (List! classes) { x = token; UnaryExpression(out e); e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e); - } else if (StartOf(12)) { + } else if (StartOf(11)) { SelectExpression(out e); - } else if (StartOf(13)) { + } else if (StartOf(14)) { ConstAtomExpression(out e); } else Error(120); } static void MulOp(out Token! x, out BinaryExpr.Opcode op) { x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/; - if (t.kind == 33) { + if (t.kind == 32) { Get(); x = token; op = BinaryExpr.Opcode.Mul; } else if (t.kind == 72) { @@ -1335,18 +1339,6 @@ public static int Parse (List! classes) { } else Error(122); } - static void SelectExpression(out Expression! e) { - Token! id; e = dummyExpr; - if (t.kind == 1) { - IdentOrFuncExpression(out e); - } else if (t.kind == 22 || t.kind == 85 || t.kind == 86) { - ObjectExpression(out e); - } else Error(123); - while (t.kind == 80 || t.kind == 82) { - SelectOrCallSuffix(ref e); - } - } - static void ConstAtomExpression(out Expression! e) { Token! x, dtName, id; BigInteger n; List! elements; e = dummyExpr; @@ -1398,12 +1390,12 @@ public static int Parse (List! classes) { e = new FreshExpr(x, e); break; } - case 50: { + case 49: { Get(); x = token; Expression(out e); e = new UnaryExpr(x, UnaryExpr.Opcode.SeqLength, e); - Expect(50); + Expect(49); break; } case 5: { @@ -1426,7 +1418,7 @@ public static int Parse (List! classes) { Expect(83); break; } - default: Error(124); break; + default: Error(123); break; } } @@ -1477,13 +1469,13 @@ public static int Parse (List! classes) { e = new OldExpr(x, e); } else if (t.kind == 22) { Get(); - if (StartOf(14)) { + if (StartOf(15)) { QuantifierGuts(out e); } else if (StartOf(6)) { Expression(out e); - } else Error(125); + } else Error(124); Expect(23); - } else Error(126); + } else Error(125); } static void SelectOrCallSuffix(ref Expression! e) { @@ -1510,7 +1502,7 @@ public static int Parse (List! classes) { if (StartOf(6)) { Expression(out ee); e0 = ee; - if (t.kind == 42 || t.kind == 84) { + if (t.kind == 39 || t.kind == 84) { if (t.kind == 84) { Get(); anyDots = true; @@ -1528,7 +1520,7 @@ public static int Parse (List! classes) { Get(); Expression(out ee); anyDots = true; e1 = ee; - } else Error(127); + } else Error(126); assert !anyDots ==> e0 != null; if (anyDots) { assert e0 != null || e1 != null; @@ -1542,7 +1534,7 @@ public static int Parse (List! classes) { } Expect(83); - } else Error(128); + } else Error(127); } static void QuantifierGuts(out Expression! q) { @@ -1561,19 +1553,19 @@ public static int Parse (List! classes) { } else if (t.kind == 89 || t.kind == 90) { Exists(); x = token; - } else Error(129); + } else Error(128); parseVarScope.PushMarker(); IdentTypeOptional(out bv); bvars.Add(bv); parseVarScope.Push(bv.Name, bv.Name); - while (t.kind == 11) { + while (t.kind == 12) { Get(); IdentTypeOptional(out bv); bvars.Add(bv); parseVarScope.Push(bv.Name, bv.Name); } - QSep(); while (t.kind == 5) { AttributeOrTrigger(ref attrs, ref trigs); } + QSep(); Expression(out body); if (univ) { q = new ForallExpr(x, bvars, body, trigs, attrs); @@ -1589,7 +1581,7 @@ public static int Parse (List! classes) { Get(); } else if (t.kind == 88) { Get(); - } else Error(130); + } else Error(129); } static void Exists() { @@ -1597,43 +1589,43 @@ public static int Parse (List! classes) { Get(); } else if (t.kind == 90) { Get(); - } else Error(131); - } - - static void QSep() { - if (t.kind == 91) { - Get(); - } else if (t.kind == 92) { - Get(); - } else Error(132); + } else Error(130); } static void AttributeOrTrigger(ref Attributes attrs, ref Triggers trigs) { List es = new List(); Expect(5); - if (t.kind == 12) { + if (t.kind == 13) { AttributeBody(ref attrs); } else if (StartOf(6)) { es = new List(); Expressions(es); trigs = new Triggers(es, trigs); - } else Error(133); + } else Error(131); Expect(6); } + static void QSep() { + if (t.kind == 91) { + Get(); + } else if (t.kind == 92) { + Get(); + } else Error(132); + } + static void AttributeBody(ref Attributes attrs) { string aName; List aArgs = new List(); Attributes.Argument! aArg; - Expect(12); + Expect(13); Expect(1); aName = token.val; - if (StartOf(15)) { + if (StartOf(16)) { AttributeArg(out aArg); aArgs.Add(aArg); - while (t.kind == 11) { + while (t.kind == 12) { Get(); AttributeArg(out aArg); aArgs.Add(aArg); @@ -1650,7 +1642,7 @@ public static int Parse (List! classes) { } else if (StartOf(6)) { Expression(out e); arg = new Attributes.Argument(e); - } else Error(134); + } else Error(133); } @@ -1676,15 +1668,15 @@ public static int Parse (List! classes) { case 4: s = "class expected"; break; case 5: s = "{ expected"; break; case 6: s = "} expected"; break; - case 7: s = "datatype expected"; break; - case 8: s = "; expected"; break; - case 9: s = "ghost expected"; break; - case 10: s = "var expected"; break; - case 11: s = ", expected"; break; - case 12: s = ": expected"; break; - case 13: s = "< expected"; break; - case 14: s = "> expected"; break; - case 15: s = "frame expected"; break; + case 7: s = "ghost expected"; break; + case 8: s = "use expected"; break; + case 9: s = "datatype expected"; break; + case 10: s = "; expected"; break; + case 11: s = "var expected"; break; + case 12: s = ", expected"; break; + case 13: s = ": expected"; break; + case 14: s = "< expected"; break; + case 15: s = "> expected"; break; case 16: s = "method expected"; break; case 17: s = "returns expected"; break; case 18: s = "modifies expected"; break; @@ -1699,29 +1691,29 @@ public static int Parse (List! classes) { case 27: s = "seq expected"; break; case 28: s = "object expected"; break; case 29: s = "function expected"; break; - case 30: s = "use expected"; break; - case 31: s = "reads expected"; break; - case 32: s = "decreases expected"; break; - case 33: s = "* expected"; break; - case 34: s = "if expected"; break; - case 35: s = "else expected"; break; - case 36: s = "match expected"; break; - case 37: s = "case expected"; break; - case 38: s = "=> expected"; break; - case 39: s = "label expected"; break; - case 40: s = "break expected"; break; - case 41: s = "return expected"; break; - case 42: s = ":= expected"; break; - case 43: s = "new expected"; break; - case 44: s = "havoc expected"; break; - case 45: s = "while expected"; break; - case 46: s = "invariant expected"; break; - case 47: s = "call expected"; break; - case 48: s = "foreach expected"; break; - case 49: s = "in expected"; break; - case 50: s = "| expected"; break; - case 51: s = "assert expected"; break; - case 52: s = "assume expected"; break; + case 30: s = "reads expected"; break; + case 31: s = "decreases expected"; break; + case 32: s = "* expected"; break; + case 33: s = "match expected"; break; + case 34: s = "case expected"; break; + case 35: s = "=> expected"; break; + case 36: s = "label expected"; break; + case 37: s = "break expected"; break; + case 38: s = "return expected"; break; + case 39: s = ":= expected"; break; + case 40: s = "new expected"; break; + case 41: s = "havoc expected"; break; + case 42: s = "if expected"; break; + case 43: s = "else expected"; break; + case 44: s = "while expected"; break; + case 45: s = "invariant expected"; break; + case 46: s = "call expected"; break; + case 47: s = "foreach expected"; break; + case 48: s = "in expected"; break; + case 49: s = "| expected"; break; + case 50: s = "assert expected"; break; + case 51: s = "assume expected"; break; + case 52: s = "then expected"; break; case 53: s = "<==> expected"; break; case 54: s = "\\u21d4 expected"; break; case 55: s = "==> expected"; break; @@ -1769,18 +1761,18 @@ public static int Parse (List! classes) { case 97: s = "invalid TypeAndToken"; break; case 98: s = "invalid MethodSpec"; break; case 99: s = "invalid MethodSpec"; break; - case 100: s = "invalid ReferenceType"; break; - case 101: s = "invalid FunctionSpec"; break; - case 102: s = "invalid FunctionBody"; break; - case 103: s = "invalid PossiblyWildExpression"; break; - case 104: s = "invalid IfThenElseExpr"; break; + case 100: s = "invalid Expression"; break; + case 101: s = "invalid ReferenceType"; break; + case 102: s = "invalid FunctionSpec"; break; + case 103: s = "invalid FunctionBody"; break; + case 104: s = "invalid PossiblyWildExpression"; break; case 105: s = "invalid MatchExpression"; break; - case 106: s = "invalid ExtendedExpr"; break; - case 107: s = "invalid Stmt"; break; - case 108: s = "invalid OneStmt"; break; - case 109: s = "invalid IfStmt"; break; - case 110: s = "invalid ForeachStmt"; break; - case 111: s = "invalid AssignRhs"; break; + case 106: s = "invalid Stmt"; break; + case 107: s = "invalid OneStmt"; break; + case 108: s = "invalid IfStmt"; break; + case 109: s = "invalid ForeachStmt"; break; + case 110: s = "invalid AssignRhs"; break; + case 111: s = "invalid SelectExpression"; break; case 112: s = "invalid Guard"; break; case 113: s = "invalid CallStmtSubExpr"; break; case 114: s = "invalid EquivOp"; break; @@ -1792,18 +1784,17 @@ public static int Parse (List! classes) { case 120: s = "invalid UnaryExpression"; break; case 121: s = "invalid MulOp"; break; case 122: s = "invalid NegOp"; break; - case 123: s = "invalid SelectExpression"; break; - case 124: s = "invalid ConstAtomExpression"; break; + case 123: s = "invalid ConstAtomExpression"; break; + case 124: s = "invalid ObjectExpression"; break; case 125: s = "invalid ObjectExpression"; break; - case 126: s = "invalid ObjectExpression"; break; + case 126: s = "invalid SelectOrCallSuffix"; break; case 127: s = "invalid SelectOrCallSuffix"; break; - case 128: s = "invalid SelectOrCallSuffix"; break; - case 129: s = "invalid QuantifierGuts"; break; - case 130: s = "invalid Forall"; break; - case 131: s = "invalid Exists"; break; + case 128: s = "invalid QuantifierGuts"; break; + case 129: s = "invalid Forall"; break; + case 130: s = "invalid Exists"; break; + case 131: s = "invalid AttributeOrTrigger"; break; case 132: s = "invalid QSep"; break; - case 133: s = "invalid AttributeOrTrigger"; break; - case 134: s = "invalid AttributeArg"; break; + case 133: s = "invalid AttributeArg"; break; default: s = "error " + n; break; } @@ -1812,21 +1803,22 @@ public static int Parse (List! classes) { static bool[,]! set = { {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x}, - {x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x}, - {x,x,x,x, x,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,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, T,x,x,T, T,x,x,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x}, + {x,x,x,x, x,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,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,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x}, {x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x}, {x,T,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,T,T,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,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,T,T,T, x,T,T,x, x,T,T,x, x,x,x,x, x,x,x}, - {x,T,T,x, x,T,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,T,x, x,x,T,x, x,x,x,T, T,T,x,x, T,T,x,T, T,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,T,T,T, x,T,T,x, x,T,T,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,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,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,T,T,T, x,T,T,x, x,T,T,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,T,x, x,x,x,x, x,x,T,x, x,x,T,x, x,x,x,T, T,T,x,x, T,T,x,T, T,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,T,T,T, x,T,T,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,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,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,T,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x}, + {x,T,T,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,T,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,T, x,x,T,T, T,T,T,T, x,T,T,x, x,T,T,x, x,x,x,x, x,x,x}, + {x,T,x,x, x,T,x,T, T,x,x,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, T,T,T,x, x,T,T,x, T,x,T,T, 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,T,T,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,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,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,T,T,T, x,T,T,x, x,T,T,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,T,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,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,T,T,T, x,T,T,x, x,T,T,x, x,x,x,x, x,x,x}, + {x,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, T,T,T,x, x,T,T,x, T,x,T,T, 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,T,T,x, x,x,x,x, x,x,x}, {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,T,x, x,x,x,x, x,x,x}, - {x,x,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,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, T,T,T,T, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x}, + {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x}, + {x,x,x,x, x,x,x,x, x,x,x,x, x,x,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, T,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x}, + {x,x,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,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, T,T,T,T, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x}, {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,x, x,x,x}, - {x,T,T,T, 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,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,T,T,T, x,T,T,x, x,T,T,x, x,x,x,x, x,x,x} + {x,T,T,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,T,T,T, x,T,T,x, x,T,T,x, x,x,x,x, x,x,x} }; diff --git a/Source/Dafny/Printer.ssc b/Source/Dafny/Printer.ssc index d0a6b3c9..89b9f62e 100644 --- a/Source/Dafny/Printer.ssc +++ b/Source/Dafny/Printer.ssc @@ -34,7 +34,7 @@ namespace Microsoft.Dafny { } public void PrintClass(ClassDecl! c) { - PrintClassMethodHelper("class", c.Attributes, "", c.Name, c.TypeArgs); + PrintClassMethodHelper("class", c.Attributes, c.Name, c.TypeArgs); if (c.Members.Count == 0) { wr.WriteLine(" { }"); } else { @@ -61,12 +61,11 @@ namespace Microsoft.Dafny { } } - void PrintClassMethodHelper(string! kind, Attributes attrs, string! modifiers, string! name, List! typeArgs) { + void PrintClassMethodHelper(string! kind, Attributes attrs, string! name, List! typeArgs) { if (kind.Length != 0) { wr.Write("{0} ", kind); } PrintAttributes(attrs); - wr.Write(modifiers); wr.Write(name); if (typeArgs.Count != 0) { wr.Write("<"); @@ -80,7 +79,7 @@ namespace Microsoft.Dafny { } public void PrintDatatype(DatatypeDecl! dt) { - PrintClassMethodHelper("datatype", dt.Attributes, "", dt.Name, dt.TypeArgs); + PrintClassMethodHelper("datatype", dt.Attributes, dt.Name, dt.TypeArgs); if (dt.Ctors.Count == 0) { wr.WriteLine(" { }"); } else { @@ -114,6 +113,9 @@ namespace Microsoft.Dafny { public void PrintField(Field! field) { Indent(IndentAmount); + if (field.IsGhost) { + wr.Write("ghost "); + } wr.Write("var "); PrintAttributes(field.Attributes); wr.Write("{0}: ", field.Name); @@ -123,7 +125,10 @@ namespace Microsoft.Dafny { public void PrintFunction(Function! f) { Indent(IndentAmount); - PrintClassMethodHelper("function", f.Attributes, f.Use ? "use " : "", f.Name, f.TypeArgs); + string k = "function"; + if (f.IsUse) { k = "use " + k; } + if (f.IsClass) { k = "class " + k; } + PrintClassMethodHelper(k, f.Attributes, f.Name, f.TypeArgs); PrintFormals(f.Formals); wr.Write(": "); PrintType(f.ResultType); @@ -152,14 +157,16 @@ namespace Microsoft.Dafny { } if (f.Body != null) { Indent(IndentAmount); - PrintExtendedExpr(f.Body, IndentAmount); - wr.WriteLine(); + wr.WriteLine("{"); + PrintExtendedExpr(f.Body, IndentAmount + IndentAmount); + Indent(IndentAmount); + wr.WriteLine("}"); } } public void PrintCtor(DatatypeCtor! ctor) { Indent(IndentAmount); - PrintClassMethodHelper("", ctor.Attributes, "", ctor.Name, ctor.TypeArgs); + PrintClassMethodHelper("", ctor.Attributes, ctor.Name, ctor.TypeArgs); if (ctor.Formals.Count != 0) { PrintFormals(ctor.Formals); } @@ -181,7 +188,9 @@ namespace Microsoft.Dafny { public void PrintMethod(Method! method) { Indent(IndentAmount); - PrintClassMethodHelper("method", method.Attributes, "", method.Name, method.TypeArgs); + string k = "method"; + if (method.IsClass) { k = "class " + k; } + PrintClassMethodHelper(k, method.Attributes, method.Name, method.TypeArgs); PrintFormals(method.Ins); if (method.Outs.Count != 0) { if (method.Ins.Count + method.Outs.Count <= 3) { @@ -431,27 +440,32 @@ namespace Microsoft.Dafny { // ----------------------------- PrintExpression ----------------------------- public void PrintExtendedExpr(Expression! expr, int indent) { - wr.WriteLine("{"); - int ind = indent + IndentAmount; - Indent(ind); + Indent(indent); if (expr is ITEExpr) { - Expression els = expr; // bogus assignment, just to please the compiler - for (ITEExpr ite = (ITEExpr)expr; ite != null; ite = els as ITEExpr) { - wr.Write("if ("); + while (true) { + ITEExpr ite = (ITEExpr)expr; + wr.Write("if "); PrintExpression(ite.Test); - wr.Write(") "); - PrintExtendedExpr(ite.Thn, ind); - wr.Write(" else "); - els = ite.Els; + wr.WriteLine(" then"); + PrintExtendedExpr(ite.Thn, indent + IndentAmount); + expr = ite.Els; + if (expr is ITEExpr) { + Indent(indent); wr.Write("else "); + } else { + Indent(indent); wr.WriteLine("else"); + Indent(indent + IndentAmount); + PrintExpression(expr); + wr.WriteLine(); + return; + } } - PrintExtendedExpr(els, ind); } else if (expr is MatchExpr) { MatchExpr me = (MatchExpr)expr; wr.Write("match "); PrintExpression(me.Source); bool needsCurlies = exists{MatchCase mc in me.Cases; mc.Body is MatchExpr}; wr.WriteLine(needsCurlies ? " {" : ""); - int caseInd = ind + (needsCurlies ? IndentAmount : 0); + int caseInd = indent + (needsCurlies ? IndentAmount : 0); foreach (MatchCase mc in me.Cases) { Indent(caseInd); wr.Write("case {0}", mc.Id); @@ -464,20 +478,16 @@ namespace Microsoft.Dafny { wr.Write(")"); } wr.WriteLine(" =>"); - Indent(caseInd + IndentAmount); - PrintExpression(mc.Body); - wr.WriteLine(); + PrintExtendedExpr(mc.Body, caseInd + IndentAmount); } if (needsCurlies) { - Indent(ind); + Indent(indent); wr.WriteLine("}"); } } else { - PrintExpression(expr, ind); + PrintExpression(expr, indent); wr.WriteLine(); } - Indent(indent); - wr.Write("}"); } public void PrintExpression(Expression! expr) { @@ -552,7 +562,7 @@ namespace Microsoft.Dafny { (fragileContext && opBindingStrength == contextBindingStrength); if (parensNeeded) { wr.Write("("); } - PrintExpr(e.Seq, 00, false, indent); // BOGUS: fix me + PrintExpr(e.Seq, 0x00, false, indent); // BOGUS: fix me wr.Write("["); if (e.SelectOne) { assert e.E0 != null; @@ -674,12 +684,12 @@ namespace Microsoft.Dafny { case BinaryExpr.Opcode.Imp: opBindingStrength = 0x10; fragileLeftContext = true; break; case BinaryExpr.Opcode.Iff: - opBindingStrength = 0x00; break; + opBindingStrength = 0x08; break; default: assert false; // unexpected binary operator } - int opBS = opBindingStrength & 0xF0; - int ctxtBS = contextBindingStrength & 0xF0; + int opBS = opBindingStrength & 0xF8; + int ctxtBS = contextBindingStrength & 0xF8; bool parensNeeded = opBS < ctxtBS || (opBS == ctxtBS && (opBindingStrength != contextBindingStrength || fragileContext)); @@ -729,7 +739,21 @@ namespace Microsoft.Dafny { wr.Write("*"); } else if (expr is ITEExpr) { - assert false; // ITE is an extended expression and should be printed only using PrintExtendedExpr + ITEExpr ite = (ITEExpr)expr; + // determine if parens are needed + int opBindingStrength = 0x00; + bool parensNeeded = opBindingStrength < contextBindingStrength || + (fragileContext && opBindingStrength == contextBindingStrength); + + if (parensNeeded) { wr.Write("("); } + wr.Write("if "); + PrintExpression(ite.Test); + wr.Write(" then "); + PrintExpression(ite.Thn); + wr.Write(" else "); + PrintExpr(ite.Els, opBindingStrength, false, indent); + if (parensNeeded) { wr.Write(")"); } + } else if (expr is MatchExpr) { assert false; // MatchExpr is an extended expression and should be printed only using PrintExtendedExpr } else { diff --git a/Source/Dafny/Resolver.ssc b/Source/Dafny/Resolver.ssc index 31f51424..8bbc1d29 100644 --- a/Source/Dafny/Resolver.ssc +++ b/Source/Dafny/Resolver.ssc @@ -243,6 +243,9 @@ namespace Microsoft.Dafny { /// void ResolveFunction(Function! f) { scope.PushMarker(); + if (f.IsClass) { + scope.AllowInstance = false; + } foreach (Formal p in f.Formals) { scope.Push(p.Name, p); } @@ -310,6 +313,9 @@ namespace Microsoft.Dafny { void ResolveMethod(Method! m) { // Add in-parameters to the scope, but don't care about any duplication errors, since they have already been reported scope.PushMarker(); + if (m.IsClass) { + scope.AllowInstance = false; + } foreach (Formal p in m.Ins) { scope.Push(p.Name, p); } @@ -647,7 +653,7 @@ namespace Microsoft.Dafny { } } FunctionCallExpr fce = expr as FunctionCallExpr; - if (fce == null || fce.Function == null || !fce.Function.Use) { + if (fce == null || fce.Function == null || !fce.Function.IsUse) { Error(s.Expr, "use statement must indicate a function declared as use"); } } else if (stmt is PredicateStmt) { @@ -767,7 +773,7 @@ namespace Microsoft.Dafny { } } // resolve receiver - ResolveExpression(s.Receiver, true); + ResolveReceiver(s.Receiver, true); assert s.Receiver.Type != null; // follows from postcondition of ResolveExpression // resolve arguments foreach (Expression e in s.Args) { @@ -790,6 +796,12 @@ namespace Microsoft.Dafny { Error(s, "wrong number of method result arguments (got {0}, expected {1})", s.Lhs.Count, method.Outs.Count); } else { assert ctype != null; // follows from postcondition of ResolveMember + if (!scope.AllowInstance && !method.IsClass && s.Receiver is ThisExpr) { + // The call really needs an instance, but that instance is given as 'this', which is not + // available in this context. For more details, see comment in the resolution of a + // FunctionCallExpr. + Error(s.Receiver, "'this' is not allowed in a 'class' context"); + } // build the type substitution map Dictionary subst = new Dictionary(); for (int i = 0; i < ctype.TypeArgs.Count; i++) { @@ -1031,7 +1043,10 @@ namespace Microsoft.Dafny { } } else if (expr is ThisExpr) { - expr.Type = GetThisType(expr.tok, currentClass); + if (!scope.AllowInstance) { + Error(expr, "'this' is not allowed in a 'class' context"); + } + expr.Type = GetThisType(expr.tok, currentClass); // do this regardless of scope.AllowInstance, for better error reporting } else if (expr is IdentifierExpr) { IdentifierExpr e = (IdentifierExpr)expr; @@ -1185,7 +1200,7 @@ namespace Microsoft.Dafny { } else if (expr is FunctionCallExpr) { FunctionCallExpr e = (FunctionCallExpr)expr; - ResolveExpression(e.Receiver, twoState); + ResolveReceiver(e.Receiver, twoState); assert e.Receiver.Type != null; // follows from postcondition of ResolveExpression UserDefinedType ctype; MemberDecl member = ResolveMember(expr.tok, e.Receiver.Type, e.Name, out ctype); @@ -1200,6 +1215,16 @@ namespace Microsoft.Dafny { Error(expr, "wrong number of function arguments (got {0}, expected {1})", e.Args.Count, function.Formals.Count); } else { assert ctype != null; // follows from postcondition of ResolveMember + if (!scope.AllowInstance && !function.IsClass && e.Receiver is ThisExpr) { + // The call really needs an instance, but that instance is given as 'this', which is not + // available in this context. In most cases, occurrences of 'this' inside e.Receiver would + // have been caught in the recursive call to resolve e.Receiver, but not the specific case + // of e.Receiver being 'this' (explicitly or implicitly), for that case needs to be allowed + // in the event that a class function calls another class function (and note that we need the + // type of the receiver in order to find the method, so we could not have made this check + // earlier). + Error(e.Receiver, "'this' is not allowed in a 'class' context"); + } // build the type substitution map Dictionary subst = new Dictionary(); for (int i = 0; i < ctype.TypeArgs.Count; i++) { @@ -1403,7 +1428,6 @@ namespace Microsoft.Dafny { } else if (expr is ITEExpr) { ITEExpr e = (ITEExpr)expr; - assert !twoState; ResolveExpression(e.Test, twoState); assert e.Test.Type != null; // follows from postcondition of ResolveExpression ResolveExpression(e.Thn, twoState); @@ -1413,13 +1437,11 @@ namespace Microsoft.Dafny { if (!UnifyTypes(e.Test.Type, Type.Bool)) { Error(expr, "guard condition in if-then-else expression must be a boolean (instead got {0})", e.Test.Type); } - if (!UnifyTypes(e.Thn.Type, Type.Bool)) { - Error(expr, "the then branch of an if-then-else expression must be a boolean (instead got {0})", e.Thn.Type); - } - if (!UnifyTypes(e.Els.Type, Type.Bool)) { - Error(expr, "the else branch of an if-then-else expression must be a boolean (instead got {0})", e.Els.Type); + if (UnifyTypes(e.Thn.Type, e.Els.Type)) { + expr.Type = e.Thn.Type; + } else { + Error(expr, "the two branches of an if-then-else expression must have the same type (got {0} and {1})", e.Thn.Type, e.Els.Type); } - expr.Type = Type.Bool; } else if (expr is MatchExpr) { MatchExpr me = (MatchExpr)expr; @@ -1516,6 +1538,19 @@ namespace Microsoft.Dafny { } } + void ResolveReceiver(Expression! expr, bool twoState) + requires currentClass != null; + ensures expr.Type != null; + { + if (expr is ThisExpr) { + // Allow 'this' here, regardless of scope.AllowInstance. The caller is responsible for + // making sure 'this' does not really get used when it's not available. + expr.Type = GetThisType(expr.tok, currentClass); + } else { + ResolveExpression(expr, twoState); + } + } + /// /// Note: this method is allowed to be called even if "type" does not make sense for "op", as might be the case if /// resolution of the binary expression failed. If so, an arbitrary resolved opcode is returned. @@ -1615,7 +1650,18 @@ namespace Microsoft.Dafny { [Rep] readonly List! names = new List(); // a null means a marker [Rep] readonly List! things = new List(); invariant names.Count == things.Count; + int scopeSizeWhereInstancesWereDisallowed = -1; + invariant -1 <= scopeSizeWhereInstancesWereDisallowed && scopeSizeWhereInstancesWereDisallowed <= names.Count; + public bool AllowInstance { + get { return scopeSizeWhereInstancesWereDisallowed == -1; } + set + requires AllowInstance && !value; // only allowed to change from true to false (that's all that's currently needed in Dafny); Pop is what can make the change in the other direction + { + scopeSizeWhereInstancesWereDisallowed = names.Count; + } + } + public void PushMarker() { names.Add(null); things.Add(null); @@ -1631,6 +1677,9 @@ namespace Microsoft.Dafny { } names.RemoveRange(n, names.Count - n); things.RemoveRange(n, things.Count - n); + if (names.Count < scopeSizeWhereInstancesWereDisallowed) { + scopeSizeWhereInstancesWereDisallowed = -1; + } } // Pushes name-->var association and returns "true", if name has not already been pushed since the last marker. diff --git a/Source/Dafny/Scanner.ssc b/Source/Dafny/Scanner.ssc index c134acf9..921ef4f6 100644 --- a/Source/Dafny/Scanner.ssc +++ b/Source/Dafny/Scanner.ssc @@ -276,10 +276,10 @@ public class Scanner { static void CheckLiteral() { switch (t.val) { case "class": t.kind = 4; break; - case "datatype": t.kind = 7; break; - case "ghost": t.kind = 9; break; - case "var": t.kind = 10; break; - case "frame": t.kind = 15; break; + case "ghost": t.kind = 7; break; + case "use": t.kind = 8; break; + case "datatype": t.kind = 9; break; + case "var": t.kind = 11; break; case "method": t.kind = 16; break; case "returns": t.kind = 17; break; case "modifies": t.kind = 18; break; @@ -292,25 +292,25 @@ public class Scanner { case "seq": t.kind = 27; break; case "object": t.kind = 28; break; case "function": t.kind = 29; break; - case "use": t.kind = 30; break; - case "reads": t.kind = 31; break; - case "decreases": t.kind = 32; break; - case "if": t.kind = 34; break; - case "else": t.kind = 35; break; - case "match": t.kind = 36; break; - case "case": t.kind = 37; break; - case "label": t.kind = 39; break; - case "break": t.kind = 40; break; - case "return": t.kind = 41; break; - case "new": t.kind = 43; break; - case "havoc": t.kind = 44; break; - case "while": t.kind = 45; break; - case "invariant": t.kind = 46; break; - case "call": t.kind = 47; break; - case "foreach": t.kind = 48; break; - case "in": t.kind = 49; break; - case "assert": t.kind = 51; break; - case "assume": t.kind = 52; break; + case "reads": t.kind = 30; break; + case "decreases": t.kind = 31; break; + case "match": t.kind = 33; break; + case "case": t.kind = 34; break; + case "label": t.kind = 36; break; + case "break": t.kind = 37; break; + case "return": t.kind = 38; break; + case "new": t.kind = 40; break; + case "havoc": t.kind = 41; break; + case "if": t.kind = 42; break; + case "else": t.kind = 43; break; + case "while": t.kind = 44; break; + case "invariant": t.kind = 45; break; + case "call": t.kind = 46; break; + case "foreach": t.kind = 47; break; + case "in": t.kind = 48; break; + case "assert": t.kind = 50; break; + case "assume": t.kind = 51; break; + case "then": t.kind = 52; break; case "false": t.kind = 76; break; case "true": t.kind = 77; break; case "null": t.kind = 78; break; @@ -352,36 +352,36 @@ public class Scanner { case 6: {t.kind = 6; goto done;} case 7: - {t.kind = 8; goto done;} + {t.kind = 10; goto done;} case 8: - {t.kind = 11; goto done;} + {t.kind = 12; goto done;} case 9: if (ch == '=') {buf.Append(ch); NextCh(); goto case 17;} else if (ch == ':') {buf.Append(ch); NextCh(); goto case 52;} - else {t.kind = 12; goto done;} + else {t.kind = 13; goto done;} case 10: if (ch == '=') {buf.Append(ch); NextCh(); goto case 19;} - else {t.kind = 13; goto done;} + else {t.kind = 14; goto done;} case 11: if (ch == '=') {buf.Append(ch); NextCh(); goto case 31;} - else {t.kind = 14; goto done;} + else {t.kind = 15; goto done;} case 12: {t.kind = 22; goto done;} case 13: {t.kind = 23; goto done;} case 14: - {t.kind = 33; goto done;} + {t.kind = 32; goto done;} case 15: if (ch == '>') {buf.Append(ch); NextCh(); goto case 16;} else if (ch == '=') {buf.Append(ch); NextCh(); goto case 23;} else {t.kind = noSym; goto done;} case 16: - {t.kind = 38; goto done;} + {t.kind = 35; goto done;} case 17: - {t.kind = 42; goto done;} + {t.kind = 39; goto done;} case 18: if (ch == '|') {buf.Append(ch); NextCh(); goto case 29;} - else {t.kind = 50; goto done;} + else {t.kind = 49; goto done;} case 19: if (ch == '=') {buf.Append(ch); NextCh(); goto case 20;} else {t.kind = 62; goto done;} diff --git a/Source/Dafny/Translator.ssc b/Source/Dafny/Translator.ssc index 85a09b1f..4a8d7ebf 100644 --- a/Source/Dafny/Translator.ssc +++ b/Source/Dafny/Translator.ssc @@ -439,10 +439,17 @@ namespace Microsoft.Dafny { Bpl.BoundVariable bv = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, predef.HeapVarName, predef.HeapType)); formals.Add(bv); args.Add(new Bpl.IdentifierExpr(f.tok, bv)); - Bpl.BoundVariable bvThis = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "this", predef.RefType)); - formals.Add(bvThis); - Bpl.Expr bvThisIdExpr = new Bpl.IdentifierExpr(f.tok, bvThis); - args.Add(bvThisIdExpr); + Bpl.BoundVariable bvThis; + Bpl.Expr bvThisIdExpr; + if (f.IsClass) { + bvThis = null; + bvThisIdExpr = null; + } else { + bvThis = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "this", predef.RefType)); + formals.Add(bvThis); + bvThisIdExpr = new Bpl.IdentifierExpr(f.tok, bvThis); + args.Add(bvThisIdExpr); + } DatatypeValue r = null; if (specializationReplacementFormals != null) { assert ctor != null; // follows from if guard and the precondition @@ -468,16 +475,18 @@ namespace Microsoft.Dafny { } } - Bpl.Expr ante = Bpl.Expr.And( - Bpl.Expr.Neq(bvThisIdExpr, predef.Null), - FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, etran.HeapExpr)); + Bpl.Expr ante = FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, etran.HeapExpr); + if (!f.IsClass) { + assert bvThisIdExpr != null; // set to non-null value above when !f.IsClass + ante = Bpl.Expr.And(Bpl.Expr.Neq(bvThisIdExpr, predef.Null), ante); + } foreach (Expression req in f.Req) { ante = Bpl.Expr.And(ante, etran.TrExpr(req)); } Bpl.FunctionCall funcID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullName, TrType(f.ResultType))); Bpl.Expr funcAppl = new Bpl.NAryExpr(f.tok, funcID, args); Bpl.Trigger tr; - if (f.Use) { + if (f.IsUse) { Bpl.FunctionCall useID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullName + "#use", TrType(f.ResultType))); Bpl.Expr useAppl = new Bpl.NAryExpr(f.tok, useID, args); ante = Bpl.Expr.And(useAppl, ante); @@ -727,16 +736,21 @@ namespace Microsoft.Dafny { Bpl.VariableSeq bvars = new Bpl.VariableSeq(); Bpl.ExprSeq f0args = new Bpl.ExprSeq(); Bpl.ExprSeq f1args = new Bpl.ExprSeq(); - Bpl.BoundVariable thVar = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "this", predef.RefType)); - Bpl.Expr th = new Bpl.IdentifierExpr(f.tok, thVar); - bvars.Add(h0Var); bvars.Add(h1Var); bvars.Add(thVar); - f0args.Add(h0); f0args.Add(th); - f1args.Add(h1); f1args.Add(th); + bvars.Add(h0Var); bvars.Add(h1Var); + f0args.Add(h0); + f1args.Add(h1); + if (!f.IsClass) { + Bpl.BoundVariable thVar = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "this", predef.RefType)); + Bpl.Expr th = new Bpl.IdentifierExpr(f.tok, thVar); + bvars.Add(thVar); + f0args.Add(th); + f1args.Add(th); - Type thisType = Resolver.GetThisType(f.tok, (!)f.EnclosingClass); - Bpl.Expr wh = Bpl.Expr.And(Bpl.Expr.Neq(th, predef.Null), - Bpl.Expr.And(etran0.GoodRef(f.tok, th, thisType), etran1.GoodRef(f.tok, th, thisType))); - wellFormed = Bpl.Expr.And(wellFormed, wh); + Type thisType = Resolver.GetThisType(f.tok, (!)f.EnclosingClass); + Bpl.Expr wh = Bpl.Expr.And(Bpl.Expr.Neq(th, predef.Null), + Bpl.Expr.And(etran0.GoodRef(f.tok, th, thisType), etran1.GoodRef(f.tok, th, thisType))); + wellFormed = Bpl.Expr.And(wellFormed, wh); + } foreach (Formal p in f.Formals) { Bpl.BoundVariable bv = new Bpl.BoundVariable(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, TrType(p.Type))); @@ -744,7 +758,7 @@ namespace Microsoft.Dafny { Bpl.Expr formal = new Bpl.IdentifierExpr(p.tok, bv); f0args.Add(formal); f1args.Add(formal); - wh = GetWhereClause(p.tok, formal, p.Type, etran0); + Bpl.Expr wh = GetWhereClause(p.tok, formal, p.Type, etran0); if (wh != null) { wellFormed = Bpl.Expr.And(wellFormed, wh); } wh = GetWhereClause(p.tok, formal, p.Type, etran1); if (wh != null) { wellFormed = Bpl.Expr.And(wellFormed, wh); } @@ -816,14 +830,16 @@ namespace Microsoft.Dafny { ExpressionTranslator etran = new ExpressionTranslator(this, predef, f.tok); // parameters of the procedure Bpl.VariableSeq inParams = new Bpl.VariableSeq(); - Bpl.Expr wh = Bpl.Expr.And( - Bpl.Expr.Neq(new Bpl.IdentifierExpr(f.tok, "this", predef.RefType), predef.Null), - etran.GoodRef(f.tok, new Bpl.IdentifierExpr(f.tok, "this", predef.RefType), Resolver.GetThisType(f.tok, (!)f.EnclosingClass))); - Bpl.Formal thVar = new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, "this", predef.RefType, wh), true); - inParams.Add(thVar); + if (!f.IsClass) { + Bpl.Expr wh = Bpl.Expr.And( + Bpl.Expr.Neq(new Bpl.IdentifierExpr(f.tok, "this", predef.RefType), predef.Null), + etran.GoodRef(f.tok, new Bpl.IdentifierExpr(f.tok, "this", predef.RefType), Resolver.GetThisType(f.tok, (!)f.EnclosingClass))); + Bpl.Formal thVar = new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, "this", predef.RefType, wh), true); + inParams.Add(thVar); + } foreach (Formal p in f.Formals) { Bpl.Type varType = TrType(p.Type); - wh = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, p.UniqueName, varType), p.Type, etran); + Bpl.Expr wh = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, p.UniqueName, varType), p.Type, etran); inParams.Add(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, varType, wh), true)); } Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(f.TypeArgs); @@ -901,8 +917,9 @@ namespace Microsoft.Dafny { return total; } else if (expr is FunctionCallExpr) { FunctionCallExpr e = (FunctionCallExpr)expr; + assert e.Function != null; // follows from the fact that expr has been successfully resolved Bpl.Expr r = IsTotal(e.Receiver, etran); - if (!(e.Receiver is ThisExpr)) { + if (!e.Function.IsClass && !(e.Receiver is ThisExpr)) { r = BplAnd(r, Bpl.Expr.Neq(etran.TrExpr(e.Receiver), predef.Null)); } // TODO: check reads permissions and check preconditions @@ -1046,7 +1063,9 @@ namespace Microsoft.Dafny { assert e.Function != null; // follows from the fact that expr has been successfully resolved // check well-formedness of receiver CheckWellformed(e.Receiver, func, Position.Neither, locals, builder, etran); - CheckNonNull(expr.tok, e.Receiver, builder, etran); + if (!e.Function.IsClass && !(e.Receiver is ThisExpr)) { + CheckNonNull(expr.tok, e.Receiver, builder, etran); + } // check well-formedness of the other parameters foreach (Expression arg in e.Args) { CheckWellformed(arg, func, Position.Neither, locals, builder, etran); @@ -1164,6 +1183,11 @@ namespace Microsoft.Dafny { builder.Add(new Bpl.IfCmd(expr.tok, Bpl.Expr.Not(etran.TrExpr(e.E0)), b.Collect(expr.tok), null, null)); } break; + case BinaryExpr.ResolvedOpcode.Div: + case BinaryExpr.ResolvedOpcode.Mod: + CheckWellformed(e.E1, func, pos, locals, builder, etran); + builder.Add(Assert(expr.tok, Bpl.Expr.Neq(etran.TrExpr(e.E1), Bpl.Expr.Literal(0)), "possible division by zero")); + break; default: CheckWellformed(e.E1, func, pos, locals, builder, etran); break; @@ -1319,7 +1343,9 @@ namespace Microsoft.Dafny { Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(f.TypeArgs); Bpl.VariableSeq args = new Bpl.VariableSeq(); args.Add(new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, "$heap", predef.HeapType), true)); - args.Add(new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, "this", predef.RefType), true)); + if (!f.IsClass) { + args.Add(new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, "this", predef.RefType), true)); + } foreach (Formal p in f.Formals) { args.Add(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, TrType(p.Type)), true)); } @@ -1328,7 +1354,7 @@ namespace Microsoft.Dafny { functions.Add(f, func); - if (f.Use) { + if (f.IsUse) { Bpl.Formal boolRes = new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, Bpl.TypedIdent.NoName, Bpl.Type.Bool), false); useF = new Bpl.Function(f.tok, f.FullName + "#use", args, boolRes); } @@ -1347,19 +1373,21 @@ namespace Microsoft.Dafny { Bpl.VariableSeq inParams = new Bpl.VariableSeq(); Bpl.VariableSeq outParams = new Bpl.VariableSeq(); - Bpl.Expr wh = Bpl.Expr.And( - Bpl.Expr.Neq(new Bpl.IdentifierExpr(m.tok, "this", predef.RefType), predef.Null), - etran.GoodRef(m.tok, new Bpl.IdentifierExpr(m.tok, "this", predef.RefType), Resolver.GetThisType(m.tok, (!)m.EnclosingClass))); - Bpl.Formal thVar = new Bpl.Formal(m.tok, new Bpl.TypedIdent(m.tok, "this", predef.RefType, wh), true); - inParams.Add(thVar); + if (!m.IsClass) { + Bpl.Expr wh = Bpl.Expr.And( + Bpl.Expr.Neq(new Bpl.IdentifierExpr(m.tok, "this", predef.RefType), predef.Null), + etran.GoodRef(m.tok, new Bpl.IdentifierExpr(m.tok, "this", predef.RefType), Resolver.GetThisType(m.tok, (!)m.EnclosingClass))); + Bpl.Formal thVar = new Bpl.Formal(m.tok, new Bpl.TypedIdent(m.tok, "this", predef.RefType, wh), true); + inParams.Add(thVar); + } foreach (Formal p in m.Ins) { Bpl.Type varType = TrType(p.Type); - wh = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, p.UniqueName, varType), p.Type, etran); + Bpl.Expr wh = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, p.UniqueName, varType), p.Type, etran); inParams.Add(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, varType, wh), true)); } foreach (Formal p in m.Outs) { Bpl.Type varType = TrType(p.Type); - wh = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, p.UniqueName, varType), p.Type, etran); + Bpl.Expr wh = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, p.UniqueName, varType), p.Type, etran); outParams.Add(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, varType, wh), false)); } @@ -1666,17 +1694,20 @@ namespace Microsoft.Dafny { TrStmt(local, builder, locals, etran); } Bpl.ExprSeq ins = new Bpl.ExprSeq(); - ins.Add(etran.TrExpr(s.Receiver)); + assert s.Method != null; // follows from the fact that stmt has been successfully resolved + if (!s.Method.IsClass) { + ins.Add(etran.TrExpr(s.Receiver)); + } for (int i = 0; i < s.Args.Count; i++) { Expression e = s.Args[i]; - Type t = ((!)s.Method).Ins[i].Type; + Type t = s.Method.Ins[i].Type; ins.Add(etran.CondApplyBox(stmt.Tok, etran.TrExpr(e), (!)e.Type, t)); } Bpl.IdentifierExprSeq outs = new Bpl.IdentifierExprSeq(); List tmpOuts = new List(s.Lhs.Count); for (int i = 0; i < s.Lhs.Count; i++) { Expression e = s.Lhs[i]; - if (ExpressionTranslator.ModeledAsBoxType(((!)s.Method).Outs[i].Type) && !ExpressionTranslator.ModeledAsBoxType((!)e.Type)) { + if (ExpressionTranslator.ModeledAsBoxType(s.Method.Outs[i].Type) && !ExpressionTranslator.ModeledAsBoxType((!)e.Type)) { // we need an Unbox Bpl.LocalVariable var = new Bpl.LocalVariable(stmt.Tok, new Bpl.TypedIdent(stmt.Tok, "$tmp#" + otherTmpVarCount, predef.BoxType)); otherTmpVarCount++; @@ -1690,7 +1721,7 @@ namespace Microsoft.Dafny { } } - Bpl.CallCmd call = new Bpl.CallCmd(stmt.Tok, ((!)s.Method).FullName, ins, outs); + Bpl.CallCmd call = new Bpl.CallCmd(stmt.Tok, s.Method.FullName, ins, outs); builder.Add(call); for (int i = 0; i < s.Lhs.Count; i++) { Bpl.IdentifierExpr tmpVarIdE = tmpOuts[i]; @@ -2293,7 +2324,9 @@ namespace Microsoft.Dafny { Bpl.IdentifierExpr id = new Bpl.IdentifierExpr(expr.tok, nm, translator.TrType((!)e.Type)); Bpl.ExprSeq args = new Bpl.ExprSeq(); args.Add(HeapExpr); - args.Add(TrExpr(e.Receiver)); + if (!e.Function.IsClass) { + args.Add(TrExpr(e.Receiver)); + } for (int i = 0; i < e.Args.Count; i++) { Expression ee = e.Args[i]; Type t = e.Function.Formals[i].Type; @@ -2487,9 +2520,7 @@ namespace Microsoft.Dafny { Bpl.Expr g = TrExpr(e.Test); Bpl.Expr thn = TrExpr(e.Thn); Bpl.Expr els = TrExpr(e.Els); - Bpl.Expr yea = Bpl.Expr.Imp(g, thn); - Bpl.Expr nay = Bpl.Expr.Imp(Bpl.Expr.Not(g), els); - return Bpl.Expr.And(yea, nay); + return translator.FunctionCall(expr.tok, BuiltinFunction.IfThenElse, translator.TrType((!)expr.Type), g, thn, els); } else { assert false; // unexpected expression @@ -2513,7 +2544,9 @@ namespace Microsoft.Dafny { Bpl.IdentifierExpr id = new Bpl.IdentifierExpr(e.tok, ((!)e.Function).FullName + "#use", translator.TrType((!)e.Type)); Bpl.ExprSeq args = new Bpl.ExprSeq(); args.Add(HeapExpr); - args.Add(TrExpr(e.Receiver)); + if (!e.Function.IsClass) { + args.Add(TrExpr(e.Receiver)); + } foreach (Expression ee in e.Args) { args.Add(TrExpr(ee)); } @@ -2734,6 +2767,8 @@ namespace Microsoft.Dafny { SeqEqual, SeqSameUntil, + IfThenElse, + Box, Unbox, @@ -2842,6 +2877,11 @@ namespace Microsoft.Dafny { assert args.Length == 3; assert typeInstantiation == null; return FunctionCall(tok, "Seq#SameUntil", Bpl.Type.Bool, args); + + case BuiltinFunction.IfThenElse: + assert args.Length == 3; + assert typeInstantiation != null; + return FunctionCall(tok, "$ite", typeInstantiation, args); case BuiltinFunction.Box: assert args.Length == 1; @@ -2993,7 +3033,7 @@ namespace Microsoft.Dafny { Expression body = Substitute(fexp.Function.Body, fexp.Receiver, substMap); foreach (Expression se in SplitExpr(body, false)) { assert fexp != null && fexp.Function != null; // already checked above, but the compiler seems to have forgotten that - if (fexp.Function.Use) { + if (fexp.Function.IsUse) { BinaryExpr imp = new BinaryExpr(expr.tok, BinaryExpr.Opcode.Imp, new UseExpr(fexp), se); imp.ResolvedOp = BinaryExpr.ResolvedOpcode.Imp; imp.Type = Type.Bool; @@ -3003,7 +3043,7 @@ namespace Microsoft.Dafny { } } assert fexp != null && fexp.Function != null; // already checked above, but the compiler seems to have forgotten that - if (fexp.Function.Use) { + if (fexp.Function.IsUse) { UnaryExpr ue = new UnaryExpr(expr.tok, UnaryExpr.Opcode.Not, new UseExpr(fexp)); ue.Type = Type.Bool; BinaryExpr imp = new BinaryExpr(expr.tok, BinaryExpr.Opcode.Imp, ue, expr); diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 043a4cfd..d1584333 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -30,6 +30,21 @@ class MyClass { assert v[x] != null ==> null !in v[2 .. x][1..][5 := v[this.x]][..10]; } } + + function F(x: int, y: int, h: WildData, k: WildData): WildData + { + if x < 0 then + h + else if x == 0 then + if if h == k then true else false then + h + else if y == 0 then + k + else + h + else + k + } } datatype List { @@ -70,8 +85,25 @@ TypeTests.dfy(12,4): Error: incorrect type of method out-parameter 1 (expected C SmallTests.dfy(30,7): Error: RHS expression must be well defined Execution trace: (0,0): anon0 +SmallTests.dfy(61,36): Error: possible division by zero +Execution trace: + (0,0): anon0 + (0,0): anon10_Then +SmallTests.dfy(62,51): Error: possible division by zero +Execution trace: + (0,0): anon0 + (0,0): anon10_Else + (0,0): anon3 + (0,0): anon11_Else +SmallTests.dfy(63,22): Error: target object may be null +Execution trace: + (0,0): anon0 + (0,0): anon10_Then + (0,0): anon3 + (0,0): anon11_Then + (0,0): anon6 -Dafny program verifier finished with 4 verified, 1 error +Dafny program verifier finished with 6 verified, 4 errors -------------------- Queue.dfy -------------------- diff --git a/Test/dafny0/Simple.dfy b/Test/dafny0/Simple.dfy index a224ed91..c5599529 100644 --- a/Test/dafny0/Simple.dfy +++ b/Test/dafny0/Simple.dfy @@ -27,6 +27,14 @@ class MyClass { assert v[x] != null ==> null !in v[2..x][1..][5 := v[this.x]][..10]; } } + + function F(x: int, y: int, h: WildData, k: WildData): WildData + { + if x < 0 then h else + if (x == 0) then + if if h==k then true else false then h else if y == 0 then k else h + else k + } } // some datatype stuff: diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy index 17f0168a..6ac9879d 100644 --- a/Test/dafny0/SmallTests.dfy +++ b/Test/dafny0/SmallTests.dfy @@ -43,4 +43,27 @@ class Node { t := s[..j] + [b] + s[j+1..]; } } + + method Max0(x: int, y: int) returns (r: int) + ensures r == (if x < y then y else x); + { + if (x < y) { r := y; } else { r := x; } + } + + method Max1(x: int, y: int) returns (r: int) + ensures r == x || r == y; + ensures x <= r && y <= r; + { + r := if x < y then y else x; + } + + function PoorlyDefined(x: int): int + requires if next == null then 5/x < 20 else true; // ill-defined then branch + requires if next == null then true else 0 <= 5/x; // ill-defined then branch + requires if next.next == null then true else true; // ill-defined guard + requires 10/x != 8; // this is well-defined, because we get here only if x is non-0 + reads this; + { + 12 + } } diff --git a/Test/dafny0/Use.dfy b/Test/dafny0/Use.dfy index 1d2d264f..8b7eafc1 100644 --- a/Test/dafny0/Use.dfy +++ b/Test/dafny0/Use.dfy @@ -1,7 +1,7 @@ class T { var x: int; - function use F(y: int): int { + use function F(y: int): int { 2*y } @@ -12,7 +12,7 @@ class T { assert F(7) == 14; // error (definition not engaged) } - function use G(y: int): bool { + use function G(y: int): bool { 0 <= y } @@ -25,7 +25,7 @@ class T { assert G(7); // error (definition not engaged) } - function use H(): int + use function H(): int reads this; { x diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el index d8fe3052..3b10c560 100644 --- a/Util/Emacs/dafny-mode.el +++ b/Util/Emacs/dafny-mode.el @@ -35,7 +35,7 @@ "invariant" "decreases" )) . font-lock-builtin-face) `(,(dafny-regexp-opt '( - "assert" "assume" "break" "call" "else" "havoc" "if" "label" "return" "while" + "assert" "assume" "break" "call" "then" "else" "havoc" "if" "label" "return" "while" "old" "forall" "exists" "new" "foreach" "in" "this" "fresh" "use" "match" "case" "false" "true" "null")) . font-lock-keyword-face) `(,(dafny-regexp-opt '("bool" "int" "object" "set" "seq")) . font-lock-type-face) diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty index f88c3b54..23ea36fb 100644 --- a/Util/latex/dafny.sty +++ b/Util/latex/dafny.sty @@ -13,7 +13,7 @@ % expressions match,case,false,true,null,old,fresh,this, % statements - assert,assume,new,havoc,call,if,else,while,invariant,break,return,foreach, + assert,assume,new,havoc,call,if,then,else,while,invariant,break,return,foreach, }, literate=% {:}{$\colon$}1 -- cgit v1.2.3