From dcaef29ffbe2570632e7368d27377fb9ac282d7b Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 22 Apr 2011 22:57:58 -0700 Subject: Dafny: include source location for array types supplied in input --- Source/Dafny/Dafny.atg | 4 ++-- Source/Dafny/DafnyAst.cs | 9 +++++---- Source/Dafny/Parser.cs | 4 ++-- 3 files changed, 9 insertions(+), 8 deletions(-) diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 23582495..c630d67e 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -555,7 +555,7 @@ ReferenceType if (tok.val.Length != 5) { dims = int.Parse(tok.val.Substring(5)); } - ty = theBuiltIns.ArrayType(dims, gt[0], true); + ty = theBuiltIns.ArrayType(tok, dims, gt[0], true); .) | Ident (. gt = new List(); .) [ GenericInstantiation ] (. ty = new UserDefinedType(tok, tok.val, gt); .) @@ -808,7 +808,7 @@ AssignRhs<.out List ee, out Type ty, out CallStmt initCall, Expressi [ "[" (. ee = new List(); .) Expressions "]" (. // make sure an array class with this dimensionality exists - UserDefinedType tmp = theBuiltIns.ArrayType(ee.Count, new IntType(), true); + UserDefinedType tmp = theBuiltIns.ArrayType(x, ee.Count, new IntType(), true); .) | "." Ident "(" (. args = new List(); .) diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index d923e5dc..f76f24de 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -40,20 +40,21 @@ namespace Microsoft.Dafny { ClassDecl obj = new ClassDecl(Token.NoToken, "object", SystemModule, new List(), new List(), null); SystemModule.TopLevelDecls.Add(obj); // add one-dimensional arrays, since they may arise during type checking - UserDefinedType tmp = ArrayType(1, Type.Int, true); + UserDefinedType tmp = ArrayType(Token.NoToken, 1, Type.Int, true); } public UserDefinedType ArrayType(int dims, Type arg) { - return ArrayType(dims, arg, false); + return ArrayType(Token.NoToken, dims, arg, false); } - public UserDefinedType ArrayType(int dims, Type arg, bool allowCreationOfNewClass) { + public UserDefinedType ArrayType(IToken tok, int dims, Type arg, bool allowCreationOfNewClass) { + Contract.Requires(tok != null); Contract.Requires(1 <= dims); Contract.Requires(arg != null); Contract.Ensures(Contract.Result() != null); List typeArgs = new List(); typeArgs.Add(arg); - UserDefinedType udt = new UserDefinedType(Token.NoToken, ArrayClassName(dims), typeArgs); + UserDefinedType udt = new UserDefinedType(tok, ArrayClassName(dims), typeArgs); if (allowCreationOfNewClass && !arrayTypeDecls.ContainsKey(dims)) { ArrayClassDecl arrayClass = new ArrayClassDecl(dims, SystemModule); for (int d = 0; d < dims; d++) { diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 180f15ab..e2a45ceb 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -877,7 +877,7 @@ List/*!*/ decreases) { if (tok.val.Length != 5) { dims = int.Parse(tok.val.Substring(5)); } - ty = theBuiltIns.ArrayType(dims, gt[0], true); + ty = theBuiltIns.ArrayType(tok, dims, gt[0], true); } else if (la.kind == 1) { Ident(out tok); @@ -1419,7 +1419,7 @@ List/*!*/ decreases) { ee = new List(); Expressions(ee); Expect(53); - UserDefinedType tmp = theBuiltIns.ArrayType(ee.Count, new IntType(), true); + UserDefinedType tmp = theBuiltIns.ArrayType(x, ee.Count, new IntType(), true); } else { Get(); -- cgit v1.2.3 From 27241e69516368f116baea922938d1cb10570d85 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Wed, 11 May 2011 17:25:34 -0700 Subject: Dafny: * added missing error checking for ghost-vs-physical contexts (e.g., use of the "old" keyword) * check that arrays are not null when accessed * added dafny1/FindZero.dfy test case --- Source/Dafny/Resolver.cs | 13 ++++++++++++- Source/Dafny/Translator.cs | 3 +++ Test/dafny0/Answer | 9 ++++++--- Test/dafny0/Modules0.dfy | 15 +++++++++++++++ Test/dafny0/NatTypes.dfy | 2 +- Test/dafny1/Answer | 4 ++++ Test/dafny1/FindZero.dfy | 30 ++++++++++++++++++++++++++++++ Test/dafny1/runtest.bat | 2 +- 8 files changed, 72 insertions(+), 6 deletions(-) create mode 100644 Test/dafny1/FindZero.dfy diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 22a58a39..ba28d531 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -837,7 +837,11 @@ namespace Microsoft.Dafny { #if !NO_CHEAP_OBJECT_WORKAROUND if (a is ObjectType || b is ObjectType) { // TODO: remove this temporary hack - // allow anything with object; this is BOGUS + var other = a is ObjectType ? b : a; + if (other is BoolType || other is IntType || other is SetType || other is SeqType || other.IsDatatype) { + return false; + } + // allow anything else with object; this is BOGUS return true; } #endif @@ -2019,6 +2023,8 @@ namespace Microsoft.Dafny { OldExpr e = (OldExpr)expr; if (!twoState) { Error(expr, "old expressions are not allowed in this context"); + } else if (!specContext) { + Error(expr, "old expressions are allowed only in specification and ghost contexts"); } ResolveExpression(e.E, twoState, specContext); expr.Type = e.E.Type; @@ -2027,6 +2033,8 @@ namespace Microsoft.Dafny { FreshExpr e = (FreshExpr)expr; if (!twoState) { Error(expr, "fresh expressions are not allowed in this context"); + } else if (!specContext) { + Error(expr, "fresh expressions are allowed only in specification and ghost contexts"); } ResolveExpression(e.E, twoState, specContext); // the type of e.E must be either an object or a collection of objects @@ -2047,6 +2055,9 @@ namespace Microsoft.Dafny { } else if (expr is AllocatedExpr) { AllocatedExpr e = (AllocatedExpr)expr; ResolveExpression(e.E, twoState, specContext); + if (!specContext) { + Error(expr, "allocated expressions are allowed only in specification and ghost contexts"); + } // e.E can be of any type expr.Type = Type.Bool; diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 2bb5a51e..557fcaf0 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -1785,6 +1785,9 @@ namespace Microsoft.Dafny { bool isSequence = e.Seq.Type is SeqType; CheckWellformed(e.Seq, options, locals, builder, etran); Bpl.Expr seq = etran.TrExpr(e.Seq); + if (e.Seq.Type.IsArrayType) { + builder.Add(Assert(e.Seq.tok, Bpl.Expr.Neq(seq, predef.Null), "array may be null")); + } Bpl.Expr e0 = null; if (e.E0 != null) { e0 = etran.TrExpr(e.E0); diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 1ac8fc1c..afa88a47 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -483,9 +483,12 @@ Modules0.dfy(62,6): Error: inter-module calls must follow the module import rela Modules0.dfy(72,6): Error: inter-module calls must follow the module import relation (so module X0 must transitively import X1) Modules0.dfy(91,4): Error: inter-module calls must follow the module import relation (so module _default must transitively import YY) Modules0.dfy(116,16): Error: ghost variables are allowed only in specification contexts -Modules0.dfy(133,10): Error: match source expression 'tree' has already been used as a match source expression in this context -Modules0.dfy(172,12): Error: match source expression 'l' has already been used as a match source expression in this context -10 resolution/type errors detected in Modules0.dfy +Modules0.dfy(130,11): Error: old expressions are allowed only in specification and ghost contexts +Modules0.dfy(131,11): Error: fresh expressions are allowed only in specification and ghost contexts +Modules0.dfy(132,11): Error: allocated expressions are allowed only in specification and ghost contexts +Modules0.dfy(148,10): Error: match source expression 'tree' has already been used as a match source expression in this context +Modules0.dfy(187,12): Error: match source expression 'l' has already been used as a match source expression in this context +13 resolution/type errors detected in Modules0.dfy -------------------- Modules1.dfy -------------------- Modules1.dfy(55,3): Error: decreases expression must be bounded below by 0 diff --git a/Test/dafny0/Modules0.dfy b/Test/dafny0/Modules0.dfy index adce71a8..59052ac2 100644 --- a/Test/dafny0/Modules0.dfy +++ b/Test/dafny0/Modules0.dfy @@ -121,6 +121,21 @@ class Ghosty { ghost method Theorem(a: int) { } } +var SomeField: int; + +method SpecialFunctions() + modifies this; +{ + SomeField := SomeField + 4; + var a := old(SomeField); // error: old can only be used in ghost contexts + var b := fresh(this); // error: fresh can only be used in ghost contexts + var c := allocated(this); // error: allocated can only be used in ghost contexts + if (fresh(this)) { // this guard makes the if statement a ghost statement + ghost var x := old(SomeField); // this is a ghost context, so it's okay + ghost var y := allocated(this); // this is a ghost context, so it's okay + } +} + // ---------------------- illegal match expressions --------------- datatype Tree { Nil; Cons(int, Tree, Tree); } diff --git a/Test/dafny0/NatTypes.dfy b/Test/dafny0/NatTypes.dfy index 93bd4b65..6b7ce9b9 100644 --- a/Test/dafny0/NatTypes.dfy +++ b/Test/dafny0/NatTypes.dfy @@ -60,7 +60,7 @@ datatype List { Cons(nat, T, List); } -method MatchIt(list: List) returns (k: nat) +method MatchIt(list: List