summaryrefslogtreecommitdiff
path: root/Source/Dafny
diff options
context:
space:
mode:
authorGravatar rustanleino <unknown>2010-05-21 18:38:47 +0000
committerGravatar rustanleino <unknown>2010-05-21 18:38:47 +0000
commit2fc9a47b200589fae14f698e7546553a0b31aec2 (patch)
treeae0fd61bcd66c4f92833c33f82de518a718bfb7c /Source/Dafny
parent9657b7042a5a55fe96bc9b7560c473876d7efa60 (diff)
Dafny:
* Added arrays * Beefed up set axiomatization to know more things about set displays * Added a simple heuristic that can infer some simple decreases clauses for loops * Added Dafny solutions to a couple of VACID benchmarks
Diffstat (limited to 'Source/Dafny')
-rw-r--r--Source/Dafny/Compiler.ssc94
-rw-r--r--Source/Dafny/Dafny.atg29
-rw-r--r--Source/Dafny/DafnyAst.ssc71
-rw-r--r--Source/Dafny/Parser.ssc611
-rw-r--r--Source/Dafny/Printer.ssc8
-rw-r--r--Source/Dafny/Resolver.ssc208
-rw-r--r--Source/Dafny/Scanner.ssc201
-rw-r--r--Source/Dafny/Translator.ssc215
8 files changed, 928 insertions, 509 deletions
diff --git a/Source/Dafny/Compiler.ssc b/Source/Dafny/Compiler.ssc
index 155927c4..c7dc73eb 100644
--- a/Source/Dafny/Compiler.ssc
+++ b/Source/Dafny/Compiler.ssc
@@ -386,6 +386,9 @@ namespace Microsoft.Dafny {
return "BigInteger";
} else if (type is ObjectType) {
return "object";
+ } else if (type.IsArrayType) {
+ Type elType = UserDefinedType.ArrayElementType(type);
+ return TypeName(elType) + "[]";
} else if (type is UserDefinedType) {
UserDefinedType udt = (UserDefinedType)type;
string s = udt.Name;
@@ -507,13 +510,54 @@ namespace Microsoft.Dafny {
wr.WriteLine("return;");
} else if (stmt is AssignStmt) {
AssignStmt s = (AssignStmt)stmt;
- Indent(indent);
- TrExpr(s.Lhs);
- if (!(s.Rhs is HavocRhs)) {
- wr.Write(" = ");
- TrAssignmentRhs(s.Rhs);
+ if (s.Lhs is SeqSelectExpr && !((SeqSelectExpr)s.Lhs).SelectOne) {
+ SeqSelectExpr sel = (SeqSelectExpr)s.Lhs;
+ // Generate the following:
+ // tmpArr = sel.Seq;
+ // tmpLow = sel.E0; // or 0 if sel.E0==null
+ // tmpHigh = sel.Eq; // or arr.Length if sel.E1==null
+ // tmpRhs = s.Rhs;
+ // for (int tmpI = tmpLow; tmpI < tmpHigh; tmpI++) {
+ // tmpArr[tmpI] = tmpRhs;
+ // }
+ string arr = "_arr" + tmpVarCount;
+ string low = "_low" + tmpVarCount;
+ string high = "_high" + tmpVarCount;
+ string rhs = "_rhs" + tmpVarCount;
+ string i = "_i" + tmpVarCount;
+ tmpVarCount++;
+ Indent(indent); wr.Write("{0} {1} = ", TypeName((!)sel.Seq.Type), arr); TrExpr(sel.Seq); wr.WriteLine(";");
+ Indent(indent); wr.Write("int {0} = ", low);
+ if (sel.E0 == null) {
+ wr.Write("0");
+ } else {
+ TrExpr(sel.E0);
+ }
+ wr.WriteLine(";");
+ Indent(indent); wr.Write("int {0} = ", high);
+ if (sel.E1 == null) {
+ wr.Write("new BigInteger(arr.Length)");
+ } else {
+ TrExpr(sel.E1);
+ }
+ wr.WriteLine(";");
+ Indent(indent); wr.Write("{0} {1} = ", TypeName((!)sel.Type), rhs); TrAssignmentRhs(s.Rhs); wr.WriteLine(";");
+ Indent(indent);
+ wr.WriteLine("for (BigInteger {0} = {1}; {0} < {2}; {0}++) {{", i, low, high);
+ Indent(indent + IndentAmount);
+ wr.WriteLine("{0}[(int)({1})] = {2};", arr, i, rhs);
+ Indent(indent);
+ wr.WriteLine(";");
+
+ } else {
+ Indent(indent);
+ TrExpr(s.Lhs);
+ if (!(s.Rhs is HavocRhs)) {
+ wr.Write(" = ");
+ TrAssignmentRhs(s.Rhs);
+ }
+ wr.WriteLine(";");
}
- wr.WriteLine(";");
} else if (stmt is VarDecl) {
TrVarDecl((VarDecl)stmt, true, indent);
@@ -686,7 +730,21 @@ namespace Microsoft.Dafny {
} else {
TypeRhs tp = (TypeRhs)rhs;
- wr.Write("new {0}()", TypeName(tp.Type));
+ if (tp.ArraySize == null) {
+ wr.Write("new {0}()", TypeName(tp.EType));
+ } else {
+ if (tp.EType is IntType || tp.EType.IsTypeParameter) {
+ // Because the default constructor for BigInteger does not generate a valid BigInteger, we have
+ // to excplicitly initialize the elements of an integer array. This is all done in a helper routine.
+ wr.Write("Dafny.Helpers.InitNewArray<{0}>(", TypeName(tp.EType));
+ TrExpr(tp.ArraySize);
+ wr.Write(")");
+ } else {
+ wr.Write("new {0}[(int)", TypeName(tp.EType));
+ TrExpr(tp.ArraySize);
+ wr.Write("]");
+ }
+ }
}
}
@@ -827,9 +885,15 @@ namespace Microsoft.Dafny {
} else if (expr is SeqSelectExpr) {
SeqSelectExpr e = (SeqSelectExpr)expr;
TrParenExpr(e.Seq);
- if (e.SelectOne) {
- assert e.E0 != null;
- assert e.E1 == null;
+ assert e.Seq.Type != null;
+ if (e.Seq.Type.IsArrayType) {
+ assert e.SelectOne;
+ assert e.E0 != null && e.E1 == null;
+ wr.Write("[(int)");
+ TrParenExpr(e.E0);
+ wr.Write("]");
+ } else if (e.SelectOne) {
+ assert e.E0 != null && e.E1 == null;
TrParenExpr(".Select", e.E0);
} else {
if (e.E1 != null) {
@@ -902,8 +966,14 @@ namespace Microsoft.Dafny {
TrParenExpr(e.E);
break;
case UnaryExpr.Opcode.SeqLength:
- TrParenExpr(e.E);
- wr.Write(".Length");
+ if (((!)e.E.Type).IsArrayType) {
+ wr.Write("new BigInteger(");
+ TrParenExpr(e.E);
+ wr.Write(".Length)");
+ } else {
+ TrParenExpr(e.E);
+ wr.Write(".Length");
+ }
break;
default:
assert false; // unexpected unary expression
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 9d232294..6b46aa4f 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -397,6 +397,12 @@ ReferenceType<out Token! tok, out Type! ty>
List<Type!>! gt;
.)
( "object" (. tok = token; ty = new ObjectType(); .)
+ | "array" (. tok = token; gt = new List<Type!>(); .)
+ GenericInstantiation<gt> (. if (gt.Count != 1) {
+ SemErr("array type expects exactly one type argument");
+ }
+ ty = UserDefinedType.ArrayType(tok, gt[0]);
+ .)
| Ident<out tok> (. gt = new List<Type!>(); .)
[ GenericInstantiation<gt> ] (. ty = new UserDefinedType(tok, tok.val, gt); .)
)
@@ -590,22 +596,26 @@ AssignStmt<out Statement! s>
.)
LhsExpr<out lhs>
":=" (. x = token; .)
- AssignRhs<out rhs, out ty> (. if (rhs != null) {
+ AssignRhs<out rhs, out ty> (. if (ty == null) {
+ assert rhs != null;
s = new AssignStmt(x, lhs, rhs);
- } else {
- assert ty != null;
+ } else if (rhs == null) {
s = new AssignStmt(x, lhs, ty);
+ } else {
+ s = new AssignStmt(x, lhs, ty, rhs);
}
.)
";"
.
AssignRhs<out Expression e, out Type ty>
-/* ensures e == null <==> ty == null; */
+/* ensures e != null || ty != null; */
= (. Token! x; Expression! ee; Type! tt;
e = null; ty = null;
.)
- ( "new" ReferenceType<out x, out tt> (. ty = tt; .)
+ ( "new" TypeAndToken<out x, out tt> (. ty = tt; .)
+ [ "[" Expression<out ee> "]" (. e = ee; .)
+ ]
| Expression<out ee> (. e = ee; .)
) (. if (e == null && ty == null) { e = dummyExpr; } .)
.
@@ -642,11 +652,14 @@ IdentTypeRhs<out VarDecl! d, bool isGhost>
[ ":="
AssignRhs<out rhs, out newType>
]
- (. if (rhs != null) {
- assert newType == null;
+ (. if (newType == null && rhs != null) {
optionalRhs = new ExprRhs(rhs);
} else if (newType != null) {
- optionalRhs = new TypeRhs(newType);
+ if (rhs == null) {
+ optionalRhs = new TypeRhs(newType);
+ } else {
+ optionalRhs = new TypeRhs(newType, rhs);
+ }
} else if (optionalType == null) {
optionalType = new InferredTypeProxy();
}
diff --git a/Source/Dafny/DafnyAst.ssc b/Source/Dafny/DafnyAst.ssc
index 55e76d30..cea08862 100644
--- a/Source/Dafny/DafnyAst.ssc
+++ b/Source/Dafny/DafnyAst.ssc
@@ -68,6 +68,12 @@ namespace Microsoft.Dafny
}
}
}
+ public bool IsArrayType {
+ get {
+ UserDefinedType udt = UserDefinedType.DenotesClass(this);
+ return udt != null && ((ClassDecl!)udt.ResolvedClass).Name == "array"; // the cast to non-null is guaranteed by postcondition of DenotesClass
+ }
+ }
public bool IsDatatype {
get {
return AsDatatype != null;
@@ -140,7 +146,7 @@ namespace Microsoft.Dafny
return "seq<" + Arg + ">";
}
}
-
+
public class UserDefinedType : Type {
public readonly Token! tok;
public readonly string! Name;
@@ -148,6 +154,22 @@ namespace Microsoft.Dafny
public TopLevelDecl ResolvedClass; // filled in by resolution, if Name denotes a class/datatype and TypeArgs match the type parameters of that class/datatype
public TypeParameter ResolvedParam; // filled in by resolution, if Name denotes an enclosing type parameter and TypeArgs is the empty list
+
+ public static UserDefinedType! ArrayType(Token! tok, Type! arg) {
+ List<Type!> typeArgs = new List<Type!>();
+ typeArgs.Add(arg);
+ UserDefinedType udt = new UserDefinedType(tok, "array", typeArgs);
+ udt.ResolvedClass = arrayTypeDecl;
+ return udt;
+ }
+ static TopLevelDecl! arrayTypeDecl;
+ static UserDefinedType() {
+ List<TypeParameter!> typeArgs = new List<TypeParameter!>();
+ typeArgs.Add(new TypeParameter(Token.NoToken, "arg"));
+ ModuleDecl systemModule = new ModuleDecl(Token.NoToken, "_System", new List<string!>(), null);
+ arrayTypeDecl = new ClassDecl(Token.NoToken, "array", systemModule, typeArgs, new List<MemberDecl!>(), null);
+ }
+
public UserDefinedType(Token! tok, string! name, [Captured] List<Type!>! typeArgs) {
this.tok = tok;
@@ -201,6 +223,19 @@ namespace Microsoft.Dafny
}
}
+ /// <summary>
+ /// If type denotes a resolved class type, then return that class type.
+ /// Otherwise, return null.
+ /// </summary>
+ public static Type! ArrayElementType(Type! type)
+ requires type.IsArrayType;
+ {
+ UserDefinedType udt = DenotesClass(type);
+ assert udt != null;
+ assert udt.TypeArgs.Count == 1; // holds true of all array types
+ return udt.TypeArgs[0];
+ }
+
[Pure] public override string! ToString() {
string s = Name;
if (TypeArgs.Count != 0) {
@@ -253,23 +288,23 @@ namespace Microsoft.Dafny
}
/// <summary>
- /// This proxy stands for object or any class type.
+ /// This proxy stands for object or any class/array type.
/// </summary>
public class ObjectTypeProxy : RestrictedTypeProxy {
public override int OrderID { get { return 0; } }
}
/// <summary>
- /// This proxy stands for object or any class type or a set or sequence of object or a class type.
+ /// This proxy stands for object or any class/array type or a set/sequence of object or a class/array type.
/// </summary>
public class ObjectsTypeProxy : RestrictedTypeProxy {
public override int OrderID { get { return 1; } }
}
/// <summary>
- /// This proxy stands for either:
+ /// This proxy stands for:
/// set(Arg) or seq(Arg)
- /// </summary>
+ /// </summary>
public class CollectionTypeProxy : RestrictedTypeProxy {
public readonly Type! Arg;
public CollectionTypeProxy(Type! arg) {
@@ -293,6 +328,18 @@ namespace Microsoft.Dafny
public override int OrderID { get { return 3; } }
}
+ /// <summary>
+ /// This proxy stands for:
+ /// seq(Arg) or array(Arg)
+ /// </summary>
+ public class IndexableTypeProxy : RestrictedTypeProxy {
+ public readonly Type! Arg;
+ public IndexableTypeProxy(Type! arg) {
+ Arg = arg;
+ }
+ public override int OrderID { get { return 4; } }
+ }
+
// ------------------------------------------------------------------------------------------------------
public abstract class Declaration {
@@ -708,9 +755,14 @@ namespace Microsoft.Dafny
}
public class TypeRhs : DeterminedAssignmentRhs {
- public readonly Type! Type;
+ public readonly Type! EType;
+ public readonly Expression ArraySize;
public TypeRhs(Type! type) {
- Type = type;
+ EType = type;
+ }
+ public TypeRhs(Type! type, Expression! arraySize) {
+ EType = type;
+ ArraySize = arraySize;
}
}
@@ -730,6 +782,11 @@ namespace Microsoft.Dafny
this.Rhs = new TypeRhs(type);
base(tok);
}
+ public AssignStmt(Token! tok, Expression! lhs, Type! type, Expression! arraySize) { // array alloc statement
+ this.Lhs = lhs;
+ this.Rhs = new TypeRhs(type, arraySize);
+ base(tok);
+ }
public AssignStmt(Token! tok, Expression! lhs) { // havoc
this.Lhs = lhs;
this.Rhs = new HavocRhs();
diff --git a/Source/Dafny/Parser.ssc b/Source/Dafny/Parser.ssc
index 7b28ec2c..2499821c 100644
--- a/Source/Dafny/Parser.ssc
+++ b/Source/Dafny/Parser.ssc
@@ -6,7 +6,7 @@ using Microsoft.Contracts;
namespace Microsoft.Dafny {
public class Parser {
- const int maxT = 99;
+ const int maxT = 100;
const bool T = true;
const bool x = false;
@@ -280,13 +280,13 @@ public static int Parse (List<ModuleDecl!>! modules) {
}
if (t.kind == 14) {
FieldDecl(mmod, mm);
- } else if (t.kind == 33) {
+ } else if (t.kind == 34) {
FunctionDecl(mmod, out f);
mm.Add(f);
} else if (t.kind == 19) {
MethodDecl(mmod, out m);
mm.Add(m);
- } else Error(100);
+ } else Error(101);
}
static void GenericParameters(List<TypeParameter!>! typeArgs) {
@@ -335,7 +335,7 @@ public static int Parse (List<ModuleDecl!>! modules) {
Expression! bb; Expression body = null;
bool isFunctionMethod = false;
- Expect(33);
+ Expect(34);
if (t.kind == 19) {
Get();
isFunctionMethod = true;
@@ -355,16 +355,16 @@ public static int Parse (List<ModuleDecl!>! modules) {
Type(out returnType);
if (t.kind == 13) {
Get();
- while (t.kind == 23 || t.kind == 25 || t.kind == 34) {
+ while (t.kind == 23 || t.kind == 25 || t.kind == 35) {
FunctionSpec(reqs, reads, decreases);
}
} else if (StartOf(3)) {
- while (t.kind == 23 || t.kind == 25 || t.kind == 34) {
+ while (t.kind == 23 || t.kind == 25 || t.kind == 35) {
FunctionSpec(reqs, reads, decreases);
}
FunctionBody(out bb);
body = bb;
- } else Error(101);
+ } else Error(102);
parseVarScope.PopMarker();
f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUnlimited, typeArgs, formals, returnType, reqs, reads, decreases, body, attrs);
@@ -409,7 +409,7 @@ public static int Parse (List<ModuleDecl!>! modules) {
}
BlockStmt(out bb);
body = (BlockStmt)bb;
- } else Error(102);
+ } else Error(103);
parseVarScope.PopMarker();
m = new Method(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);
@@ -539,9 +539,9 @@ public static int Parse (List<ModuleDecl!>! modules) {
}
ty = new SeqType(gt[0]);
- } else if (t.kind == 1 || t.kind == 32) {
+ } else if (t.kind == 1 || t.kind == 32 || t.kind == 33) {
ReferenceType(out tok, out ty);
- } else Error(103);
+ } else Error(104);
}
static void Formals(bool incoming, bool allowGhosts, List<Formal!>! formals) {
@@ -590,12 +590,12 @@ List<Expression!>! decreases) {
Expression(out e);
Expect(13);
ens.Add(new MaybeFreeExpression(e, isFree));
- } else Error(104);
+ } else Error(105);
} else if (t.kind == 25) {
Get();
Expressions(decreases);
Expect(13);
- } else Error(105);
+ } else Error(106);
}
static void BlockStmt(out Statement! block) {
@@ -617,7 +617,7 @@ List<Expression!>! decreases) {
static void FrameExpression(out FrameExpression! fe) {
Expression! e; Token! id; string fieldName = null;
Expression(out e);
- if (t.kind == 36) {
+ if (t.kind == 37) {
Get();
Ident(out id);
fieldName = id.val;
@@ -629,18 +629,18 @@ List<Expression!>! decreases) {
Token! x; Expression! e0; Expression! e1 = dummyExpr;
e = dummyExpr;
- if (t.kind == 46) {
+ if (t.kind == 49) {
Get();
x = token;
Expression(out e);
- Expect(58);
+ Expect(61);
Expression(out e0);
- Expect(47);
+ Expect(50);
Expression(out e1);
e = new ITEExpr(x, e, e0, e1);
} else if (StartOf(9)) {
EquivExpression(out e);
- } else Error(106);
+ } else Error(107);
}
static void Expressions(List<Expression!>! args) {
@@ -674,6 +674,15 @@ List<Expression!>! decreases) {
if (t.kind == 32) {
Get();
tok = token; ty = new ObjectType();
+ } else if (t.kind == 33) {
+ Get();
+ tok = token; gt = new List<Type!>();
+ GenericInstantiation(gt);
+ if (gt.Count != 1) {
+ SemErr("array type expects exactly one type argument");
+ }
+ ty = UserDefinedType.ArrayType(tok, gt[0]);
+
} else if (t.kind == 1) {
Ident(out tok);
gt = new List<Type!>();
@@ -681,7 +690,7 @@ List<Expression!>! decreases) {
GenericInstantiation(gt);
}
ty = new UserDefinedType(tok, tok.val, gt);
- } else Error(107);
+ } else Error(108);
}
static void FunctionSpec(List<Expression!>! reqs, List<FrameExpression!>! reads, List<Expression!>! decreases) {
@@ -691,7 +700,7 @@ List<Expression!>! decreases) {
Expression(out e);
Expect(13);
reqs.Add(e);
- } else if (t.kind == 34) {
+ } else if (t.kind == 35) {
Get();
if (StartOf(10)) {
PossiblyWildFrameExpression(out fe);
@@ -707,48 +716,48 @@ List<Expression!>! decreases) {
Get();
Expressions(decreases);
Expect(13);
- } else Error(108);
+ } else Error(109);
}
static void FunctionBody(out Expression! e) {
e = dummyExpr;
Expect(6);
- if (t.kind == 37) {
+ if (t.kind == 38) {
MatchExpression(out e);
} else if (StartOf(7)) {
Expression(out e);
- } else Error(109);
+ } else Error(110);
Expect(7);
}
static void PossiblyWildFrameExpression(out FrameExpression! fe) {
fe = dummyFrameExpr;
- if (t.kind == 35) {
+ if (t.kind == 36) {
Get();
fe = new FrameExpression(new WildcardExpr(token), null);
} else if (StartOf(7)) {
FrameExpression(out fe);
- } else Error(110);
+ } else Error(111);
}
static void PossiblyWildExpression(out Expression! e) {
e = dummyExpr;
- if (t.kind == 35) {
+ if (t.kind == 36) {
Get();
e = new WildcardExpr(token);
} else if (StartOf(7)) {
Expression(out e);
- } else Error(111);
+ } else Error(112);
}
static void MatchExpression(out Expression! e) {
Token! x; MatchCaseExpr! c;
List<MatchCaseExpr!> cases = new List<MatchCaseExpr!>();
- Expect(37);
+ Expect(38);
x = token;
Expression(out e);
- while (t.kind == 38) {
+ while (t.kind == 39) {
CaseExpression(out c);
cases.Add(c);
}
@@ -760,7 +769,7 @@ List<Expression!>! decreases) {
List<BoundVar!> arguments = new List<BoundVar!>();
Expression! body;
- Expect(38);
+ Expect(39);
x = token; parseVarScope.PushMarker();
Ident(out id);
if (t.kind == 26) {
@@ -776,7 +785,7 @@ List<Expression!>! decreases) {
}
Expect(27);
}
- Expect(39);
+ Expect(40);
Expression(out body);
c = new MatchCaseExpr(x, id.val, arguments, body);
parseVarScope.PopMarker();
@@ -793,7 +802,7 @@ List<Expression!>! decreases) {
ss.Add(s);
} else if (t.kind == 9 || t.kind == 14) {
VarDeclStmts(ss);
- } else Error(112);
+ } else Error(113);
}
static void OneStmt(out Statement! s) {
@@ -801,51 +810,51 @@ List<Expression!>! decreases) {
s = dummyStmt; /* to please the compiler */
switch (t.kind) {
- case 54: {
+ case 57: {
AssertStmt(out s);
break;
}
- case 55: {
+ case 58: {
AssumeStmt(out s);
break;
}
- case 56: {
+ case 59: {
UseStmt(out s);
break;
}
- case 57: {
+ case 60: {
PrintStmt(out s);
break;
}
- case 1: case 26: case 91: case 92: {
+ case 1: case 26: case 92: case 93: {
AssignStmt(out s);
break;
}
- case 45: {
+ case 48: {
HavocStmt(out s);
break;
}
- case 50: {
+ case 53: {
CallStmt(out s);
break;
}
- case 46: {
+ case 49: {
IfStmt(out s);
break;
}
- case 48: {
+ case 51: {
WhileStmt(out s);
break;
}
- case 37: {
+ case 38: {
MatchStmt(out s);
break;
}
- case 51: {
+ case 54: {
ForeachStmt(out s);
break;
}
- case 40: {
+ case 41: {
Get();
x = token;
Ident(out id);
@@ -853,7 +862,7 @@ List<Expression!>! decreases) {
s = new LabelStmt(x, id.val);
break;
}
- case 41: {
+ case 42: {
Get();
x = token;
if (t.kind == 1) {
@@ -864,14 +873,14 @@ List<Expression!>! decreases) {
s = new BreakStmt(x, label);
break;
}
- case 42: {
+ case 43: {
Get();
x = token;
Expect(13);
s = new ReturnStmt(x);
break;
}
- default: Error(113); break;
+ default: Error(114); break;
}
}
@@ -894,7 +903,7 @@ List<Expression!>! decreases) {
static void AssertStmt(out Statement! s) {
Token! x; Expression! e;
- Expect(54);
+ Expect(57);
x = token;
Expression(out e);
Expect(13);
@@ -903,7 +912,7 @@ List<Expression!>! decreases) {
static void AssumeStmt(out Statement! s) {
Token! x; Expression! e;
- Expect(55);
+ Expect(58);
x = token;
Expression(out e);
Expect(13);
@@ -912,7 +921,7 @@ List<Expression!>! decreases) {
static void UseStmt(out Statement! s) {
Token! x; Expression! e;
- Expect(56);
+ Expect(59);
x = token;
Expression(out e);
Expect(13);
@@ -923,7 +932,7 @@ List<Expression!>! decreases) {
Token! x; Attributes.Argument! arg;
List<Attributes.Argument!> args = new List<Attributes.Argument!>();
- Expect(57);
+ Expect(60);
x = token;
AttributeArg(out arg);
args.Add(arg);
@@ -944,14 +953,16 @@ List<Expression!>! decreases) {
s = dummyStmt;
LhsExpr(out lhs);
- Expect(43);
+ Expect(44);
x = token;
AssignRhs(out rhs, out ty);
- if (rhs != null) {
+ if (ty == null) {
+ assert rhs != null;
s = new AssignStmt(x, lhs, rhs);
- } else {
- assert ty != null;
+ } else if (rhs == null) {
s = new AssignStmt(x, lhs, ty);
+ } else {
+ s = new AssignStmt(x, lhs, ty, rhs);
}
Expect(13);
@@ -959,7 +970,7 @@ List<Expression!>! decreases) {
static void HavocStmt(out Statement! s) {
Token! x; Expression! lhs;
- Expect(45);
+ Expect(48);
x = token;
LhsExpr(out lhs);
Expect(13);
@@ -972,10 +983,10 @@ List<Expression!>! decreases) {
List<IdentifierExpr!> lhs = new List<IdentifierExpr!>();
List<AutoVarDecl!> newVars = new List<AutoVarDecl!>();
- Expect(50);
+ Expect(53);
x = token;
CallStmtSubExpr(out e);
- if (t.kind == 15 || t.kind == 43) {
+ if (t.kind == 15 || t.kind == 44) {
if (t.kind == 15) {
Get();
e = ConvertToLocal(e);
@@ -994,7 +1005,7 @@ List<Expression!>! decreases) {
Ident(out id);
RecordCallLhs(new IdentifierExpr(id, id.val), lhs, newVars);
}
- Expect(43);
+ Expect(44);
CallStmtSubExpr(out e);
} else {
Get();
@@ -1028,19 +1039,19 @@ List<Expression!>! decreases) {
Statement! s;
Statement els = null;
- Expect(46);
+ Expect(49);
x = token;
Guard(out guard);
BlockStmt(out thn);
- if (t.kind == 47) {
+ if (t.kind == 50) {
Get();
- if (t.kind == 46) {
+ if (t.kind == 49) {
IfStmt(out s);
els = s;
} else if (t.kind == 6) {
BlockStmt(out s);
els = s;
- } else Error(114);
+ } else Error(115);
}
ifStmt = new IfStmt(x, guard, thn, els);
}
@@ -1053,18 +1064,18 @@ List<Expression!>! decreases) {
List<Expression!> decreases = new List<Expression!>();
Statement! body;
- Expect(48);
+ Expect(51);
x = token;
Guard(out guard);
assume guard == null || Owner.None(guard);
- while (t.kind == 22 || t.kind == 25 || t.kind == 49) {
- if (t.kind == 22 || t.kind == 49) {
+ while (t.kind == 22 || t.kind == 25 || t.kind == 52) {
+ if (t.kind == 22 || t.kind == 52) {
isFree = false;
if (t.kind == 22) {
Get();
isFree = true;
}
- Expect(49);
+ Expect(52);
Expression(out e);
invariants.Add(new MaybeFreeExpression(e, isFree));
Expect(13);
@@ -1087,11 +1098,11 @@ List<Expression!>! decreases) {
static void MatchStmt(out Statement! s) {
Token x; Expression! e; MatchCaseStmt! c;
List<MatchCaseStmt!> cases = new List<MatchCaseStmt!>();
- Expect(37);
+ Expect(38);
x = token;
Expression(out e);
Expect(6);
- while (t.kind == 38) {
+ while (t.kind == 39) {
CaseStatement(out c);
cases.Add(c);
}
@@ -1108,7 +1119,7 @@ List<Expression!>! decreases) {
AssignStmt bodyAssign = null;
parseVarScope.PushMarker();
- Expect(51);
+ Expect(54);
x = token;
range = new LiteralExpr(x, true);
ty = new InferredTypeProxy();
@@ -1119,20 +1130,20 @@ List<Expression!>! decreases) {
Get();
Type(out ty);
}
- Expect(52);
+ Expect(55);
Expression(out collection);
parseVarScope.Push(boundVar.val, boundVar.val);
- if (t.kind == 53) {
+ if (t.kind == 56) {
Get();
Expression(out range);
}
Expect(27);
Expect(6);
- while (t.kind == 54 || t.kind == 55 || t.kind == 56) {
- if (t.kind == 54) {
+ while (t.kind == 57 || t.kind == 58 || t.kind == 59) {
+ if (t.kind == 57) {
AssertStmt(out s);
if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); }
- } else if (t.kind == 55) {
+ } else if (t.kind == 58) {
AssumeStmt(out s);
if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); }
} else {
@@ -1143,10 +1154,10 @@ List<Expression!>! decreases) {
if (StartOf(12)) {
AssignStmt(out s);
if (s is AssignStmt) { bodyAssign = (AssignStmt)s; }
- } else if (t.kind == 45) {
+ } else if (t.kind == 48) {
HavocStmt(out s);
if (s is AssignStmt) { bodyAssign = (AssignStmt)s; }
- } else Error(115);
+ } else Error(116);
Expect(7);
if (bodyAssign != null) {
s = new ForeachStmt(x, new BoundVar(boundVar, boundVar.val, ty), collection, range, bodyPrefix, bodyAssign);
@@ -1165,14 +1176,20 @@ List<Expression!>! decreases) {
Token! x; Expression! ee; Type! tt;
e = null; ty = null;
- if (t.kind == 44) {
+ if (t.kind == 45) {
Get();
- ReferenceType(out x, out tt);
+ TypeAndToken(out x, out tt);
ty = tt;
+ if (t.kind == 46) {
+ Get();
+ Expression(out ee);
+ Expect(47);
+ e = ee;
+ }
} else if (StartOf(7)) {
Expression(out ee);
e = ee;
- } else Error(116);
+ } else Error(117);
if (e == null && ty == null) { e = dummyExpr; }
}
@@ -1180,10 +1197,10 @@ List<Expression!>! decreases) {
Token! id; e = dummyExpr;
if (t.kind == 1) {
IdentOrFuncExpression(out e);
- } else if (t.kind == 26 || t.kind == 91 || t.kind == 92) {
+ } else if (t.kind == 26 || t.kind == 92 || t.kind == 93) {
ObjectExpression(out e);
- } else Error(117);
- while (t.kind == 86 || t.kind == 88) {
+ } else Error(118);
+ while (t.kind == 46 || t.kind == 89) {
SelectOrCallSuffix(ref e);
}
}
@@ -1199,15 +1216,18 @@ List<Expression!>! decreases) {
Type(out ty);
optionalType = ty;
}
- if (t.kind == 43) {
+ if (t.kind == 44) {
Get();
AssignRhs(out rhs, out newType);
}
- if (rhs != null) {
- assert newType == null;
+ if (newType == null && rhs != null) {
optionalRhs = new ExprRhs(rhs);
} else if (newType != null) {
- optionalRhs = new TypeRhs(newType);
+ if (rhs == null) {
+ optionalRhs = new TypeRhs(newType);
+ } else {
+ optionalRhs = new TypeRhs(newType, rhs);
+ }
} else if (optionalType == null) {
optionalType = new InferredTypeProxy();
}
@@ -1218,13 +1238,13 @@ List<Expression!>! decreases) {
static void Guard(out Expression e) {
Expression! ee; e = null;
Expect(26);
- if (t.kind == 35) {
+ if (t.kind == 36) {
Get();
e = null;
} else if (StartOf(7)) {
Expression(out ee);
e = ee;
- } else Error(118);
+ } else Error(119);
Expect(27);
}
@@ -1233,7 +1253,7 @@ List<Expression!>! decreases) {
List<BoundVar!> arguments = new List<BoundVar!>();
List<Statement!> body = new List<Statement!>();
- Expect(38);
+ Expect(39);
x = token; parseVarScope.PushMarker();
Ident(out id);
if (t.kind == 26) {
@@ -1249,7 +1269,7 @@ List<Expression!>! decreases) {
}
Expect(27);
}
- Expect(39);
+ Expect(40);
parseVarScope.PushMarker();
while (StartOf(8)) {
Stmt(body);
@@ -1263,11 +1283,11 @@ List<Expression!>! decreases) {
e = dummyExpr;
if (t.kind == 1) {
IdentOrFuncExpression(out e);
- } else if (t.kind == 26 || t.kind == 91 || t.kind == 92) {
+ } else if (t.kind == 26 || t.kind == 92 || t.kind == 93) {
ObjectExpression(out e);
SelectOrCallSuffix(ref e);
- } else Error(119);
- while (t.kind == 86 || t.kind == 88) {
+ } else Error(120);
+ while (t.kind == 46 || t.kind == 89) {
SelectOrCallSuffix(ref e);
}
}
@@ -1280,13 +1300,13 @@ List<Expression!>! decreases) {
} else if (StartOf(7)) {
Expression(out e);
arg = new Attributes.Argument(e);
- } else Error(120);
+ } else Error(121);
}
static void EquivExpression(out Expression! e0) {
Token! x; Expression! e1;
ImpliesExpression(out e0);
- while (t.kind == 59 || t.kind == 60) {
+ while (t.kind == 62 || t.kind == 63) {
EquivOp();
x = token;
ImpliesExpression(out e1);
@@ -1297,7 +1317,7 @@ List<Expression!>! decreases) {
static void ImpliesExpression(out Expression! e0) {
Token! x; Expression! e1;
LogicalExpression(out e0);
- if (t.kind == 61 || t.kind == 62) {
+ if (t.kind == 64 || t.kind == 65) {
ImpliesOp();
x = token;
ImpliesExpression(out e1);
@@ -1306,23 +1326,23 @@ List<Expression!>! decreases) {
}
static void EquivOp() {
- if (t.kind == 59) {
+ if (t.kind == 62) {
Get();
- } else if (t.kind == 60) {
+ } else if (t.kind == 63) {
Get();
- } else Error(121);
+ } else Error(122);
}
static void LogicalExpression(out Expression! e0) {
Token! x; Expression! e1;
RelationalExpression(out e0);
if (StartOf(13)) {
- if (t.kind == 63 || t.kind == 64) {
+ if (t.kind == 66 || t.kind == 67) {
AndOp();
x = token;
RelationalExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1);
- while (t.kind == 63 || t.kind == 64) {
+ while (t.kind == 66 || t.kind == 67) {
AndOp();
x = token;
RelationalExpression(out e1);
@@ -1333,7 +1353,7 @@ List<Expression!>! decreases) {
x = token;
RelationalExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1);
- while (t.kind == 65 || t.kind == 66) {
+ while (t.kind == 68 || t.kind == 69) {
OrOp();
x = token;
RelationalExpression(out e1);
@@ -1344,11 +1364,11 @@ List<Expression!>! decreases) {
}
static void ImpliesOp() {
- if (t.kind == 61) {
+ if (t.kind == 64) {
Get();
- } else if (t.kind == 62) {
+ } else if (t.kind == 65) {
Get();
- } else Error(122);
+ } else Error(123);
}
static void RelationalExpression(out Expression! e0) {
@@ -1362,25 +1382,25 @@ List<Expression!>! decreases) {
}
static void AndOp() {
- if (t.kind == 63) {
+ if (t.kind == 66) {
Get();
- } else if (t.kind == 64) {
+ } else if (t.kind == 67) {
Get();
- } else Error(123);
+ } else Error(124);
}
static void OrOp() {
- if (t.kind == 65) {
+ if (t.kind == 68) {
Get();
- } else if (t.kind == 66) {
+ } else if (t.kind == 69) {
Get();
- } else Error(124);
+ } else Error(125);
}
static void Term(out Expression! e0) {
Token! x; Expression! e1; BinaryExpr.Opcode op;
Factor(out e0);
- while (t.kind == 76 || t.kind == 77) {
+ while (t.kind == 79 || t.kind == 80) {
AddOp(out x, out op);
Factor(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -1390,7 +1410,7 @@ List<Expression!>! decreases) {
static void RelOp(out Token! x, out BinaryExpr.Opcode op) {
x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/;
switch (t.kind) {
- case 67: {
+ case 70: {
Get();
x = token; op = BinaryExpr.Opcode.Eq;
break;
@@ -1405,59 +1425,59 @@ List<Expression!>! decreases) {
x = token; op = BinaryExpr.Opcode.Gt;
break;
}
- case 68: {
+ case 71: {
Get();
x = token; op = BinaryExpr.Opcode.Le;
break;
}
- case 69: {
+ case 72: {
Get();
x = token; op = BinaryExpr.Opcode.Ge;
break;
}
- case 70: {
+ case 73: {
Get();
x = token; op = BinaryExpr.Opcode.Neq;
break;
}
- case 71: {
+ case 74: {
Get();
x = token; op = BinaryExpr.Opcode.Disjoint;
break;
}
- case 52: {
+ case 55: {
Get();
x = token; op = BinaryExpr.Opcode.In;
break;
}
- case 72: {
+ case 75: {
Get();
x = token; op = BinaryExpr.Opcode.NotIn;
break;
}
- case 73: {
+ case 76: {
Get();
x = token; op = BinaryExpr.Opcode.Neq;
break;
}
- case 74: {
+ case 77: {
Get();
x = token; op = BinaryExpr.Opcode.Le;
break;
}
- case 75: {
+ case 78: {
Get();
x = token; op = BinaryExpr.Opcode.Ge;
break;
}
- default: Error(125); break;
+ default: Error(126); break;
}
}
static void Factor(out Expression! e0) {
Token! x; Expression! e1; BinaryExpr.Opcode op;
UnaryExpression(out e0);
- while (t.kind == 35 || t.kind == 78 || t.kind == 79) {
+ while (t.kind == 36 || t.kind == 81 || t.kind == 82) {
MulOp(out x, out op);
UnaryExpression(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -1466,23 +1486,23 @@ List<Expression!>! decreases) {
static void AddOp(out Token! x, out BinaryExpr.Opcode op) {
x = Token.NoToken; op=BinaryExpr.Opcode.Add/*(dummy)*/;
- if (t.kind == 76) {
+ if (t.kind == 79) {
Get();
x = token; op = BinaryExpr.Opcode.Add;
- } else if (t.kind == 77) {
+ } else if (t.kind == 80) {
Get();
x = token; op = BinaryExpr.Opcode.Sub;
- } else Error(126);
+ } else Error(127);
}
static void UnaryExpression(out Expression! e) {
Token! x; e = dummyExpr;
- if (t.kind == 77) {
+ if (t.kind == 80) {
Get();
x = token;
UnaryExpression(out e);
e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e);
- } else if (t.kind == 80 || t.kind == 81) {
+ } else if (t.kind == 83 || t.kind == 84) {
NegOp();
x = token;
UnaryExpression(out e);
@@ -1491,29 +1511,29 @@ List<Expression!>! decreases) {
SelectExpression(out e);
} else if (StartOf(15)) {
ConstAtomExpression(out e);
- } else Error(127);
+ } else Error(128);
}
static void MulOp(out Token! x, out BinaryExpr.Opcode op) {
x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/;
- if (t.kind == 35) {
+ if (t.kind == 36) {
Get();
x = token; op = BinaryExpr.Opcode.Mul;
- } else if (t.kind == 78) {
+ } else if (t.kind == 81) {
Get();
x = token; op = BinaryExpr.Opcode.Div;
- } else if (t.kind == 79) {
+ } else if (t.kind == 82) {
Get();
x = token; op = BinaryExpr.Opcode.Mod;
- } else Error(128);
+ } else Error(129);
}
static void NegOp() {
- if (t.kind == 80) {
+ if (t.kind == 83) {
Get();
- } else if (t.kind == 81) {
+ } else if (t.kind == 84) {
Get();
- } else Error(129);
+ } else Error(130);
}
static void ConstAtomExpression(out Expression! e) {
@@ -1521,17 +1541,17 @@ List<Expression!>! decreases) {
e = dummyExpr;
switch (t.kind) {
- case 82: {
+ case 85: {
Get();
e = new LiteralExpr(token, false);
break;
}
- case 83: {
+ case 86: {
Get();
e = new LiteralExpr(token, true);
break;
}
- case 84: {
+ case 87: {
Get();
e = new LiteralExpr(token);
break;
@@ -1541,11 +1561,11 @@ List<Expression!>! decreases) {
e = new LiteralExpr(token, n);
break;
}
- case 85: {
+ case 88: {
Get();
x = token;
Ident(out dtName);
- Expect(86);
+ Expect(89);
Ident(out id);
elements = new List<Expression!>();
if (t.kind == 26) {
@@ -1558,7 +1578,7 @@ List<Expression!>! decreases) {
e = new DatatypeValue(token, dtName.val, id.val, elements);
break;
}
- case 87: {
+ case 90: {
Get();
x = token;
Expect(26);
@@ -1567,12 +1587,12 @@ List<Expression!>! decreases) {
e = new FreshExpr(x, e);
break;
}
- case 53: {
+ case 56: {
Get();
x = token;
Expression(out e);
e = new UnaryExpr(x, UnaryExpr.Opcode.SeqLength, e);
- Expect(53);
+ Expect(56);
break;
}
case 6: {
@@ -1585,17 +1605,17 @@ List<Expression!>! decreases) {
Expect(7);
break;
}
- case 88: {
+ case 46: {
Get();
x = token; elements = new List<Expression!>();
if (StartOf(7)) {
Expressions(elements);
}
e = new SeqDisplayExpr(x, elements);
- Expect(89);
+ Expect(47);
break;
}
- default: Error(130); break;
+ default: Error(131); break;
}
}
@@ -1634,10 +1654,10 @@ List<Expression!>! decreases) {
static void ObjectExpression(out Expression! e) {
Token! x; e = dummyExpr;
- if (t.kind == 91) {
+ if (t.kind == 92) {
Get();
e = new ThisExpr(token);
- } else if (t.kind == 92) {
+ } else if (t.kind == 93) {
Get();
x = token;
Expect(26);
@@ -1650,9 +1670,9 @@ List<Expression!>! decreases) {
QuantifierGuts(out e);
} else if (StartOf(7)) {
Expression(out e);
- } else Error(131);
+ } else Error(132);
Expect(27);
- } else Error(132);
+ } else Error(133);
}
static void SelectOrCallSuffix(ref Expression! e) {
@@ -1660,7 +1680,7 @@ List<Expression!>! decreases) {
Expression e0 = null; Expression e1 = null; Expression! ee; bool anyDots = false;
bool func = false;
- if (t.kind == 86) {
+ if (t.kind == 89) {
Get();
Ident(out id);
if (t.kind == 26) {
@@ -1673,14 +1693,14 @@ List<Expression!>! decreases) {
e = new FunctionCallExpr(id, id.val, e, args);
}
if (!func) { e = new FieldSelectExpr(id, e, id.val); }
- } else if (t.kind == 88) {
+ } else if (t.kind == 46) {
Get();
x = token;
if (StartOf(7)) {
Expression(out ee);
e0 = ee;
- if (t.kind == 43 || t.kind == 90) {
- if (t.kind == 90) {
+ if (t.kind == 44 || t.kind == 91) {
+ if (t.kind == 91) {
Get();
anyDots = true;
if (StartOf(7)) {
@@ -1693,11 +1713,11 @@ List<Expression!>! decreases) {
e1 = ee;
}
}
- } else if (t.kind == 90) {
+ } else if (t.kind == 91) {
Get();
Expression(out ee);
anyDots = true; e1 = ee;
- } else Error(133);
+ } else Error(134);
if (!anyDots && e0 == null) {
/* a parsing error occurred */
e0 = dummyExpr;
@@ -1714,8 +1734,8 @@ List<Expression!>! decreases) {
e = new SeqUpdateExpr(x, e, e0, e1);
}
- Expect(89);
- } else Error(134);
+ Expect(47);
+ } else Error(135);
}
static void QuantifierGuts(out Expression! q) {
@@ -1728,13 +1748,13 @@ List<Expression!>! decreases) {
Triggers trigs = null;
Expression! body;
- if (t.kind == 93 || t.kind == 94) {
+ if (t.kind == 94 || t.kind == 95) {
Forall();
x = token; univ = true;
- } else if (t.kind == 95 || t.kind == 96) {
+ } else if (t.kind == 96 || t.kind == 97) {
Exists();
x = token;
- } else Error(135);
+ } else Error(136);
parseVarScope.PushMarker();
IdentTypeOptional(out bv);
bvars.Add(bv); parseVarScope.Push(bv.Name, bv.Name);
@@ -1758,19 +1778,19 @@ List<Expression!>! decreases) {
}
static void Forall() {
- if (t.kind == 93) {
+ if (t.kind == 94) {
Get();
- } else if (t.kind == 94) {
+ } else if (t.kind == 95) {
Get();
- } else Error(136);
+ } else Error(137);
}
static void Exists() {
- if (t.kind == 95) {
+ if (t.kind == 96) {
Get();
- } else if (t.kind == 96) {
+ } else if (t.kind == 97) {
Get();
- } else Error(137);
+ } else Error(138);
}
static void AttributeOrTrigger(ref Attributes attrs, ref Triggers trigs) {
@@ -1783,16 +1803,16 @@ List<Expression!>! decreases) {
es = new List<Expression!>();
Expressions(es);
trigs = new Triggers(es, trigs);
- } else Error(138);
+ } else Error(139);
Expect(7);
}
static void QSep() {
- if (t.kind == 97) {
+ if (t.kind == 98) {
Get();
- } else if (t.kind == 98) {
+ } else if (t.kind == 99) {
Get();
- } else Error(139);
+ } else Error(140);
}
static void AttributeBody(ref Attributes attrs) {
@@ -1864,113 +1884,114 @@ List<Expression!>! decreases) {
case 30: s = "set expected"; break;
case 31: s = "seq expected"; break;
case 32: s = "object expected"; break;
- case 33: s = "function expected"; break;
- case 34: s = "reads expected"; break;
- case 35: s = "* expected"; break;
- case 36: s = "` expected"; break;
- case 37: s = "match expected"; break;
- case 38: s = "case expected"; break;
- case 39: s = "=> expected"; break;
- case 40: s = "label expected"; break;
- case 41: s = "break expected"; break;
- case 42: s = "return expected"; break;
- case 43: s = ":= expected"; break;
- case 44: s = "new expected"; break;
- case 45: s = "havoc expected"; break;
- case 46: s = "if expected"; break;
- case 47: s = "else expected"; break;
- case 48: s = "while expected"; break;
- case 49: s = "invariant expected"; break;
- case 50: s = "call expected"; break;
- case 51: s = "foreach expected"; break;
- case 52: s = "in expected"; break;
- case 53: s = "| expected"; break;
- case 54: s = "assert expected"; break;
- case 55: s = "assume expected"; break;
- case 56: s = "use expected"; break;
- case 57: s = "print expected"; break;
- case 58: s = "then expected"; break;
- case 59: s = "<==> expected"; break;
- case 60: s = "\\u21d4 expected"; break;
- case 61: s = "==> expected"; break;
- case 62: s = "\\u21d2 expected"; break;
- case 63: s = "&& expected"; break;
- case 64: s = "\\u2227 expected"; break;
- case 65: s = "|| expected"; break;
- case 66: s = "\\u2228 expected"; break;
- case 67: s = "== expected"; break;
- case 68: s = "<= expected"; break;
- case 69: s = ">= expected"; break;
- case 70: s = "!= expected"; break;
- case 71: s = "!! expected"; break;
- case 72: s = "!in expected"; break;
- case 73: s = "\\u2260 expected"; break;
- case 74: s = "\\u2264 expected"; break;
- case 75: s = "\\u2265 expected"; break;
- case 76: s = "+ expected"; break;
- case 77: s = "- expected"; break;
- case 78: s = "/ expected"; break;
- case 79: s = "% expected"; break;
- case 80: s = "! expected"; break;
- case 81: s = "\\u00ac expected"; break;
- case 82: s = "false expected"; break;
- case 83: s = "true expected"; break;
- case 84: s = "null expected"; break;
- case 85: s = "# expected"; break;
- case 86: s = ". expected"; break;
- case 87: s = "fresh expected"; break;
- case 88: s = "[ expected"; break;
- case 89: s = "] expected"; break;
- case 90: s = ".. expected"; break;
- case 91: s = "this expected"; break;
- case 92: s = "old expected"; break;
- case 93: s = "forall expected"; break;
- case 94: s = "\\u2200 expected"; break;
- case 95: s = "exists expected"; break;
- case 96: s = "\\u2203 expected"; break;
- case 97: s = ":: expected"; break;
- case 98: s = "\\u2022 expected"; break;
- case 99: s = "??? expected"; break;
- case 100: s = "invalid ClassMemberDecl"; break;
- case 101: s = "invalid FunctionDecl"; break;
- case 102: s = "invalid MethodDecl"; break;
- case 103: s = "invalid TypeAndToken"; break;
- case 104: s = "invalid MethodSpec"; break;
+ case 33: s = "array expected"; break;
+ case 34: s = "function expected"; break;
+ case 35: s = "reads expected"; break;
+ case 36: s = "* expected"; break;
+ case 37: s = "` expected"; break;
+ case 38: s = "match expected"; break;
+ case 39: s = "case expected"; break;
+ case 40: s = "=> expected"; break;
+ case 41: s = "label expected"; break;
+ case 42: s = "break expected"; break;
+ case 43: s = "return expected"; break;
+ case 44: s = ":= expected"; break;
+ case 45: s = "new expected"; break;
+ case 46: s = "[ expected"; break;
+ case 47: s = "] expected"; break;
+ case 48: s = "havoc expected"; break;
+ case 49: s = "if expected"; break;
+ case 50: s = "else expected"; break;
+ case 51: s = "while expected"; break;
+ case 52: s = "invariant expected"; break;
+ case 53: s = "call expected"; break;
+ case 54: s = "foreach expected"; break;
+ case 55: s = "in expected"; break;
+ case 56: s = "| expected"; break;
+ case 57: s = "assert expected"; break;
+ case 58: s = "assume expected"; break;
+ case 59: s = "use expected"; break;
+ case 60: s = "print expected"; break;
+ case 61: s = "then expected"; break;
+ case 62: s = "<==> expected"; break;
+ case 63: s = "\\u21d4 expected"; break;
+ case 64: s = "==> expected"; break;
+ case 65: s = "\\u21d2 expected"; break;
+ case 66: s = "&& expected"; break;
+ case 67: s = "\\u2227 expected"; break;
+ case 68: s = "|| expected"; break;
+ case 69: s = "\\u2228 expected"; break;
+ case 70: s = "== expected"; break;
+ case 71: s = "<= expected"; break;
+ case 72: s = ">= expected"; break;
+ case 73: s = "!= expected"; break;
+ case 74: s = "!! expected"; break;
+ case 75: s = "!in expected"; break;
+ case 76: s = "\\u2260 expected"; break;
+ case 77: s = "\\u2264 expected"; break;
+ case 78: s = "\\u2265 expected"; break;
+ case 79: s = "+ expected"; break;
+ case 80: s = "- expected"; break;
+ case 81: s = "/ expected"; break;
+ case 82: s = "% expected"; break;
+ case 83: s = "! expected"; break;
+ case 84: s = "\\u00ac expected"; break;
+ case 85: s = "false expected"; break;
+ case 86: s = "true expected"; break;
+ case 87: s = "null expected"; break;
+ case 88: s = "# expected"; break;
+ case 89: s = ". expected"; break;
+ case 90: s = "fresh expected"; break;
+ case 91: s = ".. expected"; break;
+ case 92: s = "this expected"; break;
+ case 93: s = "old expected"; break;
+ case 94: s = "forall expected"; break;
+ case 95: s = "\\u2200 expected"; break;
+ case 96: s = "exists expected"; break;
+ case 97: s = "\\u2203 expected"; break;
+ case 98: s = ":: expected"; break;
+ case 99: s = "\\u2022 expected"; break;
+ case 100: s = "??? expected"; break;
+ case 101: s = "invalid ClassMemberDecl"; break;
+ case 102: s = "invalid FunctionDecl"; break;
+ case 103: s = "invalid MethodDecl"; break;
+ case 104: s = "invalid TypeAndToken"; break;
case 105: s = "invalid MethodSpec"; break;
- case 106: s = "invalid Expression"; break;
- case 107: s = "invalid ReferenceType"; break;
- case 108: s = "invalid FunctionSpec"; break;
- case 109: s = "invalid FunctionBody"; break;
- case 110: s = "invalid PossiblyWildFrameExpression"; break;
- case 111: s = "invalid PossiblyWildExpression"; break;
- case 112: s = "invalid Stmt"; break;
- case 113: s = "invalid OneStmt"; break;
- case 114: s = "invalid IfStmt"; break;
- case 115: s = "invalid ForeachStmt"; break;
- case 116: s = "invalid AssignRhs"; break;
- case 117: s = "invalid SelectExpression"; break;
- case 118: s = "invalid Guard"; break;
- case 119: s = "invalid CallStmtSubExpr"; break;
- case 120: s = "invalid AttributeArg"; break;
- case 121: s = "invalid EquivOp"; break;
- case 122: s = "invalid ImpliesOp"; break;
- case 123: s = "invalid AndOp"; break;
- case 124: s = "invalid OrOp"; break;
- case 125: s = "invalid RelOp"; break;
- case 126: s = "invalid AddOp"; break;
- case 127: s = "invalid UnaryExpression"; break;
- case 128: s = "invalid MulOp"; break;
- case 129: s = "invalid NegOp"; break;
- case 130: s = "invalid ConstAtomExpression"; break;
- case 131: s = "invalid ObjectExpression"; break;
+ case 106: s = "invalid MethodSpec"; break;
+ case 107: s = "invalid Expression"; break;
+ case 108: s = "invalid ReferenceType"; break;
+ case 109: s = "invalid FunctionSpec"; break;
+ case 110: s = "invalid FunctionBody"; break;
+ case 111: s = "invalid PossiblyWildFrameExpression"; break;
+ case 112: s = "invalid PossiblyWildExpression"; break;
+ case 113: s = "invalid Stmt"; break;
+ case 114: s = "invalid OneStmt"; break;
+ case 115: s = "invalid IfStmt"; break;
+ case 116: s = "invalid ForeachStmt"; break;
+ case 117: s = "invalid AssignRhs"; break;
+ case 118: s = "invalid SelectExpression"; break;
+ case 119: s = "invalid Guard"; break;
+ case 120: s = "invalid CallStmtSubExpr"; break;
+ case 121: s = "invalid AttributeArg"; break;
+ case 122: s = "invalid EquivOp"; break;
+ case 123: s = "invalid ImpliesOp"; break;
+ case 124: s = "invalid AndOp"; break;
+ case 125: s = "invalid OrOp"; break;
+ case 126: s = "invalid RelOp"; break;
+ case 127: s = "invalid AddOp"; break;
+ case 128: s = "invalid UnaryExpression"; break;
+ case 129: s = "invalid MulOp"; break;
+ case 130: s = "invalid NegOp"; break;
+ case 131: s = "invalid ConstAtomExpression"; break;
case 132: s = "invalid ObjectExpression"; break;
- case 133: s = "invalid SelectOrCallSuffix"; break;
+ case 133: s = "invalid ObjectExpression"; break;
case 134: s = "invalid SelectOrCallSuffix"; break;
- case 135: s = "invalid QuantifierGuts"; break;
- case 136: s = "invalid Forall"; break;
- case 137: s = "invalid Exists"; break;
- case 138: s = "invalid AttributeOrTrigger"; break;
- case 139: s = "invalid QSep"; break;
+ case 135: s = "invalid SelectOrCallSuffix"; break;
+ case 136: s = "invalid QuantifierGuts"; break;
+ case 137: s = "invalid Forall"; break;
+ case 138: s = "invalid Exists"; break;
+ case 139: s = "invalid AttributeOrTrigger"; break;
+ case 140: s = "invalid QSep"; break;
default: s = "error " + n; break;
}
@@ -1978,24 +1999,24 @@ List<Expression!>! decreases) {
}
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,x, T,x,x,x, T,T,T,T, T,x,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,x,x,x, x,x,x,x, x,T,T,T, x,x,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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,T, x,T,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,T,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,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,T,x, x,T,x,x, x,x,T,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, T,T,T,x, x,T,T,x, T,x,T,T, 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,T, T,x,x,x, x,x,x,x, x},
- {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,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,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,x,x,T, 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,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, 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,T,x,x, T,T,T,x, x,T,T,x, T,x,T,T, 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,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,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,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,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,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,x,x,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,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,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,x, x,x,x,x, x,T,T,T, T,x,x,x, x},
- {x,T,T,T, 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,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,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}
+ {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, T,x,x,x, T,T,T,T, T,x,T,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,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,T,T,T, x,x,T,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,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,T, x,T,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,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,T,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,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, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, T,x,T,x, T,T,x,x, x,x,x,x, x,x},
+ {x,T,x,x, x,x,T,x, x,T,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, x,x,x,x, T,T,x,T, x,T,T,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, T,T,x,x, x,x,x,x, x,x},
+ {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, T,x,T,x, T,T,x,x, x,x,x,x, x,x},
+ {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,T,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,x,x, T,x,x,T, T,T,T,T, T,x,T,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,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, x,x,x,x, T,T,x,T, x,T,T,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, 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,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, T,T,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, 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,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,T, x,x,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,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,T,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,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,x,x,x, x,x,x,x, x,x,x,x, x,x,T,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,x,x, T,x,x,T, T,T,T,T, T,x,T,x, T,T,x,x, x,x,x,x, x,x}
};
diff --git a/Source/Dafny/Printer.ssc b/Source/Dafny/Printer.ssc
index 755c10b2..bf07e122 100644
--- a/Source/Dafny/Printer.ssc
+++ b/Source/Dafny/Printer.ssc
@@ -510,8 +510,14 @@ namespace Microsoft.Dafny {
if (rhs is ExprRhs) {
PrintExpression(((ExprRhs)rhs).Expr);
} else if (rhs is TypeRhs) {
+ TypeRhs t = (TypeRhs)rhs;
wr.Write("new ");
- PrintType(((TypeRhs)rhs).Type);
+ PrintType(t.EType);
+ if (t.ArraySize != null) {
+ wr.Write("[");
+ PrintExpression(t.ArraySize);
+ wr.Write("]");
+ }
} else {
assert false; // unexpected RHS
}
diff --git a/Source/Dafny/Resolver.ssc b/Source/Dafny/Resolver.ssc
index 0222b606..6e16aff6 100644
--- a/Source/Dafny/Resolver.ssc
+++ b/Source/Dafny/Resolver.ssc
@@ -577,7 +577,7 @@ namespace Microsoft.Dafny {
} else {
Error(t.tok, "Type parameter expects no type arguments: {0}", t.Name);
}
- } else {
+ } else if (t.ResolvedClass == null) { // this test is becausee 'array' is already resolved; TODO: an alternative would be to pre-populate 'classes' with built-in references types like 'array' (and perhaps in the future 'string')
TopLevelDecl d;
if (!classes.TryGetValue(t.Name, out d)) {
Error(t.tok, "Undeclared top-level type or type parameter: {0}", t.Name);
@@ -725,7 +725,7 @@ namespace Microsoft.Dafny {
} else {
return false;
}
-
+
} else if (proxy is OperationTypeProxy) {
OperationTypeProxy opProxy = (OperationTypeProxy)proxy;
if (t is IntType || t is SetType || (opProxy.AllowSeq && t is SeqType)) {
@@ -733,7 +733,22 @@ namespace Microsoft.Dafny {
} else {
return false;
}
-
+
+ } else if (proxy is IndexableTypeProxy) {
+ IndexableTypeProxy iProxy = (IndexableTypeProxy)proxy;
+ if (t is SeqType) {
+ if (!UnifyTypes(iProxy.Arg, ((SeqType)t).Arg)) {
+ return false;
+ }
+ } else if (t.IsArrayType) {
+ Type elType = UserDefinedType.ArrayElementType(t);
+ if (!UnifyTypes(iProxy.Arg, elType)) {
+ return false;
+ }
+ } else {
+ return false;
+ }
+
} else {
assert false; // unexpected proxy type
}
@@ -759,6 +774,11 @@ namespace Microsoft.Dafny {
// unify a and b by redirecting b to a, since a gives the stronger requirement
b.T = a;
return true;
+ } else if (b is IndexableTypeProxy) {
+ // the intersection of ObjectTypeProxy and IndexableTypeProxy is an array type
+ a.T = UserDefinedType.ArrayType(Token.NoToken, ((IndexableTypeProxy)b).Arg);
+ b.T = a.T;
+ return true;
} else {
return false;
}
@@ -770,8 +790,8 @@ namespace Microsoft.Dafny {
return true;
} else if (b is CollectionTypeProxy) {
// fine provided b's collection-element-type can be unified with object or a class type
- a.T = new ObjectTypeProxy();
- return UnifyTypes(a.T, ((CollectionTypeProxy)b).Arg);
+ a.T = b;
+ return UnifyTypes(((CollectionTypeProxy)b).Arg, new ObjectTypeProxy());
} else if (b is OperationTypeProxy) {
// fine; restrict a to sets of object/class, and restrict b to set/seq of object/class
if (((OperationTypeProxy)b).AllowSeq) {
@@ -782,6 +802,14 @@ namespace Microsoft.Dafny {
b.T = a.T;
}
return true;
+ } else if (b is IndexableTypeProxy) {
+ IndexableTypeProxy pb = (IndexableTypeProxy)b;
+ // the intersection of ObjectsTypeProxy and IndexableTypeProxy is
+ // EITHER a sequence of ObjectTypeProxy OR an array of anything
+ // TODO: here, only the first of the two cases is supported
+ b.T = new SeqType(pb.Arg);
+ a.T = b.T;
+ return UnifyTypes(pb.Arg, new ObjectTypeProxy());
} else {
assert false; // unexpected restricted-proxy type
}
@@ -799,18 +827,42 @@ namespace Microsoft.Dafny {
b.T = a.T;
}
return true;
+ } else if (b is IndexableTypeProxy) {
+ CollectionTypeProxy pa = (CollectionTypeProxy)a;
+ IndexableTypeProxy pb = (IndexableTypeProxy)b;
+ // strengthen a and b to a sequence type
+ a.T = new SeqType(pa.Arg);
+ b.T = new SeqType(pb.Arg);
+ return UnifyTypes(pa.Arg, pb.Arg);
} else {
assert false; // unexpected restricted-proxy type
}
} else if (a is OperationTypeProxy) {
- assert b is OperationTypeProxy; // else we we have unexpected restricted-proxy type
- if (((OperationTypeProxy)a).AllowSeq ==> ((OperationTypeProxy)b).AllowSeq) {
- b.T = a;
+ OperationTypeProxy pa = (OperationTypeProxy)a;
+ if (b is OperationTypeProxy) {
+ if (pa.AllowSeq ==> ((OperationTypeProxy)b).AllowSeq) {
+ b.T = a;
+ } else {
+ a.T = b; // b has the stronger requirement
+ }
+ return true;
} else {
- a.T = b; // b has the stronger requirement
+ IndexableTypeProxy pb = (IndexableTypeProxy)b; // cast justification: lse we have unexpected restricted-proxy type
+ if (pa.AllowSeq) {
+ // strengthen a and b to a sequence type
+ b.T = new SeqType(pb.Arg);
+ a.T = b.T;
+ return true;
+ } else {
+ return false;
+ }
}
- return true;
+
+ } else if (a is IndexableTypeProxy) {
+ assert b is IndexableTypeProxy; // else we have unexpected restricted-proxy type
+ a.T = b;
+ return UnifyTypes(((IndexableTypeProxy)a).Arg, ((IndexableTypeProxy)b).Arg);
} else {
assert false; // unexpected restricted-proxy type
@@ -863,11 +915,15 @@ namespace Microsoft.Dafny {
} else if (stmt is AssignStmt) {
AssignStmt s = (AssignStmt)stmt;
int prevErrorCount = ErrorCount;
- ResolveExpression(s.Lhs, true, true); // allow ghosts for now, but see FieldSelectExpr LHS case below
+ if (s.Lhs is SeqSelectExpr) {
+ ResolveSeqSelectExpr((SeqSelectExpr)s.Lhs, true, false, true);
+ } else {
+ ResolveExpression(s.Lhs, true, true); // allow ghosts for now, but see FieldSelectExpr LHS case below
+ }
bool lhsResolvedSuccessfully = ErrorCount == prevErrorCount;
assert s.Lhs.Type != null; // follows from postcondition of ResolveExpression
// check that LHS denotes a mutable variable or a field
- bool lvalueIsGhost = true;
+ bool lvalueIsGhost = false;
if (s.Lhs is IdentifierExpr) {
IVariable var = ((IdentifierExpr)s.Lhs).Var;
if (var == null) {
@@ -899,6 +955,23 @@ namespace Microsoft.Dafny {
}
}
}
+ } else if (s.Lhs is SeqSelectExpr) {
+ SeqSelectExpr lhs = (SeqSelectExpr)s.Lhs;
+ // LHS is fine, provided the "sequence" is really an array
+ if (lhsResolvedSuccessfully) {
+ assert lhs.Seq.Type != null;
+ Type elementType = new InferredTypeProxy();
+ if (!UnifyTypes(lhs.Seq.Type, UserDefinedType.ArrayType(Token.NoToken, elementType))) {
+ Error(lhs.Seq, "LHS of array assignment must denote an array element (found {0})", lhs.Seq.Type);
+ }
+ if (specContextOnly) {
+ Error(stmt, "Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)");
+ }
+ }
+ if (!(s.Rhs is ExprRhs)) {
+ Error(stmt, "Assignment to array element must have an expression RHS; try using a temporary local variable");
+ }
+
} else {
Error(stmt, "LHS of assignment must denote a mutable variable or field");
}
@@ -908,16 +981,19 @@ namespace Microsoft.Dafny {
ExprRhs rr = (ExprRhs)s.Rhs;
ResolveExpression(rr.Expr, true, lvalueIsGhost);
assert rr.Expr.Type != null; // follows from postcondition of ResolveExpression
- if (!UnifyTypes(s.Lhs.Type, rr.Expr.Type)) {
+ Type lhsType = s.Lhs.Type;
+ if (s.Lhs is SeqSelectExpr && !((SeqSelectExpr)s.Lhs).SelectOne) {
+ assert lhsType.IsArrayType;
+ lhsType = UserDefinedType.ArrayElementType(lhsType);
+ }
+ if (!UnifyTypes(lhsType, rr.Expr.Type)) {
Error(stmt, "RHS (of type {0}) not assignable to LHS (of type {1})", rr.Expr.Type, s.Lhs.Type);
}
} else if (s.Rhs is TypeRhs) {
TypeRhs rr = (TypeRhs)s.Rhs;
- ResolveType(rr.Type);
- if (!rr.Type.IsRefType) {
- Error(stmt, "new can be applied only to reference types (got {0})", rr.Type);
- } else if (!UnifyTypes(s.Lhs.Type, rr.Type)) {
- Error(stmt, "type {0} is not assignable to LHS (of type {1})", rr.Type, s.Lhs.Type);
+ Type t = ResolveTypeRhs(rr, stmt, lvalueIsGhost);
+ if (!UnifyTypes(s.Lhs.Type, t)) {
+ Error(stmt, "type {0} is not assignable to LHS (of type {1})", t, s.Lhs.Type);
}
} else if (s.Rhs is HavocRhs) {
// nothing else to do
@@ -940,11 +1016,7 @@ namespace Microsoft.Dafny {
rhsType = rr.Expr.Type;
} else if (s.Rhs is TypeRhs) {
TypeRhs rr = (TypeRhs)s.Rhs;
- ResolveType(rr.Type);
- if (!rr.Type.IsRefType) {
- Error(stmt, "new can be applied only to reference types (got {0})", rr.Type);
- }
- rhsType = rr.Type;
+ rhsType = ResolveTypeRhs(rr, stmt, s.IsGhost);
} else {
assert false; // unexpected RHS
}
@@ -1264,6 +1336,24 @@ namespace Microsoft.Dafny {
assert false;
}
}
+
+ Type! ResolveTypeRhs(TypeRhs! rr, Statement! stmt, bool specContext) {
+ ResolveType(rr.EType);
+ if (rr.ArraySize == null) {
+ if (!rr.EType.IsRefType) {
+ Error(stmt, "new can be applied only to reference types (got {0})", rr.EType);
+ }
+ } else {
+ ResolveExpression(rr.ArraySize, true, specContext);
+ if (rr.ArraySize.Type is IntType) {
+ // all is good
+ return UserDefinedType.ArrayType(stmt.Tok, rr.EType);
+ } else {
+ Error(stmt, "new must use an integer expression for the array size (got {0})", rr.ArraySize.Type);
+ }
+ }
+ return rr.EType;
+ }
MemberDecl ResolveMember(Token! tok, Type! receiverType, string! memberName, out UserDefinedType ctype)
ensures result != null ==> ctype != null && ctype.ResolvedClass != null;
@@ -1499,35 +1589,7 @@ namespace Microsoft.Dafny {
} else if (expr is SeqSelectExpr) {
SeqSelectExpr e = (SeqSelectExpr)expr;
- bool seqErr = false;
- ResolveExpression(e.Seq, twoState, specContext);
- assert e.Seq.Type != null; // follows from postcondition of ResolveExpression
- Type elementType = new InferredTypeProxy();
- if (!UnifyTypes(e.Seq.Type, new SeqType(elementType))) {
- Error(expr, "sequence selection requires a sequence (got {0})", e.Seq.Type);
- seqErr = true;
- }
- if (e.E0 != null) {
- ResolveExpression(e.E0, twoState, specContext);
- assert e.E0.Type != null; // follows from postcondition of ResolveExpression
- if (!UnifyTypes(e.E0.Type, Type.Int)) {
- Error(e.E0, "sequence selection requires integer indices (got {0})", e.E0.Type);
- }
- }
- if (e.E1 != null) {
- ResolveExpression(e.E1, twoState, specContext);
- assert e.E1.Type != null; // follows from postcondition of ResolveExpression
- if (!UnifyTypes(e.E1.Type, Type.Int)) {
- Error(e.E1, "sequence selection requires integer indices (got {0})", e.E1.Type);
- }
- }
- if (!seqErr) {
- if (e.SelectOne) {
- expr.Type = elementType;
- } else {
- expr.Type = e.Seq.Type;
- }
- }
+ ResolveSeqSelectExpr(e, twoState, specContext, false);
} else if (expr is SeqUpdateExpr) {
SeqUpdateExpr e = (SeqUpdateExpr)expr;
@@ -1665,8 +1727,8 @@ namespace Microsoft.Dafny {
expr.Type = Type.Bool;
break;
case UnaryExpr.Opcode.SeqLength:
- if (!UnifyTypes(e.E.Type, new SeqType(new InferredTypeProxy()))) {
- Error(expr, "sequence-length operator expects a sequence argument (instead got {0})", e.E.Type);
+ if (!UnifyTypes(e.E.Type, new IndexableTypeProxy(new InferredTypeProxy()))) {
+ Error(expr, "length operator expects a sequence or array argument (instead got {0})", e.E.Type);
}
expr.Type = Type.Int;
break;
@@ -1933,6 +1995,44 @@ namespace Microsoft.Dafny {
}
}
+ void ResolveSeqSelectExpr(SeqSelectExpr! e, bool twoState, bool specContext, bool allowNonUnitArraySelection) {
+ bool seqErr = false;
+ ResolveExpression(e.Seq, twoState, specContext);
+ assert e.Seq.Type != null; // follows from postcondition of ResolveExpression
+ Type elementType = new InferredTypeProxy();
+ Type expectedType;
+ if (e.SelectOne || allowNonUnitArraySelection) {
+ expectedType = new IndexableTypeProxy(elementType);
+ } else {
+ expectedType = new SeqType(elementType);
+ }
+ if (!UnifyTypes(e.Seq.Type, expectedType)) {
+ Error(e, "sequence/array selection requires a sequence or array (got {0})", e.Seq.Type);
+ seqErr = true;
+ }
+ if (e.E0 != null) {
+ ResolveExpression(e.E0, twoState, specContext);
+ assert e.E0.Type != null; // follows from postcondition of ResolveExpression
+ if (!UnifyTypes(e.E0.Type, Type.Int)) {
+ Error(e.E0, "sequence/array selection requires integer indices (got {0})", e.E0.Type);
+ }
+ }
+ if (e.E1 != null) {
+ ResolveExpression(e.E1, twoState, specContext);
+ assert e.E1.Type != null; // follows from postcondition of ResolveExpression
+ if (!UnifyTypes(e.E1.Type, Type.Int)) {
+ Error(e.E1, "sequence/array selection requires integer indices (got {0})", e.E1.Type);
+ }
+ }
+ if (!seqErr) {
+ if (e.SelectOne) {
+ e.Type = elementType;
+ } else {
+ e.Type = e.Seq.Type;
+ }
+ }
+ }
+
/// <summary>
/// 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.
diff --git a/Source/Dafny/Scanner.ssc b/Source/Dafny/Scanner.ssc
index cf759f84..5fdeefed 100644
--- a/Source/Dafny/Scanner.ssc
+++ b/Source/Dafny/Scanner.ssc
@@ -31,20 +31,20 @@ public class Scanner {
[Microsoft.Contracts.Verify(false)]
static Scanner() {
start[0] = 55;
- start[33] = 33;
+ start[33] = 35;
start[34] = 3;
- start[35] = 46;
- start[37] = 44;
- start[38] = 27;
+ start[35] = 48;
+ start[37] = 46;
+ start[38] = 29;
start[39] = 1;
start[40] = 12;
start[41] = 13;
start[42] = 14;
- start[43] = 41;
+ start[43] = 43;
start[44] = 8;
- start[45] = 42;
- start[46] = 47;
- start[47] = 43;
+ start[45] = 44;
+ start[46] = 49;
+ start[47] = 45;
start[48] = 2;
start[49] = 2;
start[50] = 2;
@@ -87,9 +87,9 @@ public class Scanner {
start[88] = 1;
start[89] = 1;
start[90] = 1;
- start[91] = 48;
+ start[91] = 19;
start[92] = 1;
- start[93] = 49;
+ start[93] = 20;
start[95] = 1;
start[96] = 15;
start[97] = 1;
@@ -119,21 +119,21 @@ public class Scanner {
start[121] = 1;
start[122] = 1;
start[123] = 5;
- start[124] = 19;
+ start[124] = 21;
start[125] = 6;
- start[172] = 45;
+ start[172] = 47;
start[8226] = 54;
- start[8658] = 26;
- start[8660] = 23;
+ start[8658] = 28;
+ start[8660] = 25;
start[8704] = 51;
start[8707] = 52;
- start[8743] = 29;
- start[8744] = 31;
- start[8800] = 38;
- start[8804] = 39;
- start[8805] = 40;
+ start[8743] = 31;
+ start[8744] = 33;
+ start[8800] = 40;
+ start[8804] = 41;
+ start[8805] = 42;
}
- const int noSym = 99;
+ const int noSym = 100;
static short[] start = new short[16385];
@@ -295,35 +295,36 @@ public class Scanner {
case "set": t.kind = 30; break;
case "seq": t.kind = 31; break;
case "object": t.kind = 32; break;
- case "function": t.kind = 33; break;
- case "reads": t.kind = 34; break;
- case "match": t.kind = 37; break;
- case "case": t.kind = 38; break;
- case "label": t.kind = 40; break;
- case "break": t.kind = 41; break;
- case "return": t.kind = 42; break;
- case "new": t.kind = 44; break;
- case "havoc": t.kind = 45; break;
- case "if": t.kind = 46; break;
- case "else": t.kind = 47; break;
- case "while": t.kind = 48; break;
- case "invariant": t.kind = 49; break;
- case "call": t.kind = 50; break;
- case "foreach": t.kind = 51; break;
- case "in": t.kind = 52; break;
- case "assert": t.kind = 54; break;
- case "assume": t.kind = 55; break;
- case "use": t.kind = 56; break;
- case "print": t.kind = 57; break;
- case "then": t.kind = 58; break;
- case "false": t.kind = 82; break;
- case "true": t.kind = 83; break;
- case "null": t.kind = 84; break;
- case "fresh": t.kind = 87; break;
- case "this": t.kind = 91; break;
- case "old": t.kind = 92; break;
- case "forall": t.kind = 93; break;
- case "exists": t.kind = 95; break;
+ case "array": t.kind = 33; break;
+ case "function": t.kind = 34; break;
+ case "reads": t.kind = 35; break;
+ case "match": t.kind = 38; break;
+ case "case": t.kind = 39; break;
+ case "label": t.kind = 41; break;
+ case "break": t.kind = 42; break;
+ case "return": t.kind = 43; break;
+ case "new": t.kind = 45; break;
+ case "havoc": t.kind = 48; break;
+ case "if": t.kind = 49; break;
+ case "else": t.kind = 50; break;
+ case "while": t.kind = 51; break;
+ case "invariant": t.kind = 52; break;
+ case "call": t.kind = 53; break;
+ case "foreach": t.kind = 54; break;
+ case "in": t.kind = 55; break;
+ case "assert": t.kind = 57; break;
+ case "assume": t.kind = 58; break;
+ case "use": t.kind = 59; break;
+ case "print": t.kind = 60; break;
+ case "then": t.kind = 61; break;
+ case "false": t.kind = 85; break;
+ case "true": t.kind = 86; break;
+ case "null": t.kind = 87; break;
+ case "fresh": t.kind = 90; break;
+ case "this": t.kind = 92; break;
+ case "old": t.kind = 93; break;
+ case "forall": t.kind = 94; break;
+ case "exists": t.kind = 96; break;
default: break;
}
@@ -365,109 +366,109 @@ public class Scanner {
else if (ch == ':') {buf.Append(ch); NextCh(); goto case 53;}
else {t.kind = 16; goto done;}
case 10:
- if (ch == '=') {buf.Append(ch); NextCh(); goto case 20;}
+ if (ch == '=') {buf.Append(ch); NextCh(); goto case 22;}
else {t.kind = 17; goto done;}
case 11:
- if (ch == '=') {buf.Append(ch); NextCh(); goto case 32;}
+ if (ch == '=') {buf.Append(ch); NextCh(); goto case 34;}
else {t.kind = 18; goto done;}
case 12:
{t.kind = 26; goto done;}
case 13:
{t.kind = 27; goto done;}
case 14:
- {t.kind = 35; goto done;}
- case 15:
{t.kind = 36; goto done;}
+ case 15:
+ {t.kind = 37; goto done;}
case 16:
if (ch == '>') {buf.Append(ch); NextCh(); goto case 17;}
- else if (ch == '=') {buf.Append(ch); NextCh(); goto case 24;}
+ else if (ch == '=') {buf.Append(ch); NextCh(); goto case 26;}
else {t.kind = noSym; goto done;}
case 17:
- {t.kind = 39; goto done;}
+ {t.kind = 40; goto done;}
case 18:
- {t.kind = 43; goto done;}
+ {t.kind = 44; goto done;}
case 19:
- if (ch == '|') {buf.Append(ch); NextCh(); goto case 30;}
- else {t.kind = 53; goto done;}
+ {t.kind = 46; goto done;}
case 20:
- if (ch == '=') {buf.Append(ch); NextCh(); goto case 21;}
- else {t.kind = 68; goto done;}
+ {t.kind = 47; goto done;}
case 21:
- if (ch == '>') {buf.Append(ch); NextCh(); goto case 22;}
- else {t.kind = noSym; goto done;}
+ if (ch == '|') {buf.Append(ch); NextCh(); goto case 32;}
+ else {t.kind = 56; goto done;}
case 22:
- {t.kind = 59; goto done;}
+ if (ch == '=') {buf.Append(ch); NextCh(); goto case 23;}
+ else {t.kind = 71; goto done;}
case 23:
- {t.kind = 60; goto done;}
+ if (ch == '>') {buf.Append(ch); NextCh(); goto case 24;}
+ else {t.kind = noSym; goto done;}
case 24:
- if (ch == '>') {buf.Append(ch); NextCh(); goto case 25;}
- else {t.kind = 67; goto done;}
+ {t.kind = 62; goto done;}
case 25:
- {t.kind = 61; goto done;}
+ {t.kind = 63; goto done;}
case 26:
- {t.kind = 62; goto done;}
+ if (ch == '>') {buf.Append(ch); NextCh(); goto case 27;}
+ else {t.kind = 70; goto done;}
case 27:
- if (ch == '&') {buf.Append(ch); NextCh(); goto case 28;}
- else {t.kind = noSym; goto done;}
+ {t.kind = 64; goto done;}
case 28:
- {t.kind = 63; goto done;}
+ {t.kind = 65; goto done;}
case 29:
- {t.kind = 64; goto done;}
+ if (ch == '&') {buf.Append(ch); NextCh(); goto case 30;}
+ else {t.kind = noSym; goto done;}
case 30:
- {t.kind = 65; goto done;}
- case 31:
{t.kind = 66; goto done;}
+ case 31:
+ {t.kind = 67; goto done;}
case 32:
- {t.kind = 69; goto done;}
+ {t.kind = 68; goto done;}
case 33:
- if (ch == '=') {buf.Append(ch); NextCh(); goto case 34;}
- else if (ch == '!') {buf.Append(ch); NextCh(); goto case 35;}
- else if (ch == 'i') {buf.Append(ch); NextCh(); goto case 36;}
- else {t.kind = 80; goto done;}
+ {t.kind = 69; goto done;}
case 34:
- {t.kind = 70; goto done;}
+ {t.kind = 72; goto done;}
case 35:
- {t.kind = 71; goto done;}
+ if (ch == '=') {buf.Append(ch); NextCh(); goto case 36;}
+ else if (ch == '!') {buf.Append(ch); NextCh(); goto case 37;}
+ else if (ch == 'i') {buf.Append(ch); NextCh(); goto case 38;}
+ else {t.kind = 83; goto done;}
case 36:
- if (ch == 'n') {buf.Append(ch); NextCh(); goto case 37;}
- else {t.kind = noSym; goto done;}
+ {t.kind = 73; goto done;}
case 37:
- {t.kind = 72; goto done;}
+ {t.kind = 74; goto done;}
case 38:
- {t.kind = 73; goto done;}
+ if (ch == 'n') {buf.Append(ch); NextCh(); goto case 39;}
+ else {t.kind = noSym; goto done;}
case 39:
- {t.kind = 74; goto done;}
- case 40:
{t.kind = 75; goto done;}
- case 41:
+ case 40:
{t.kind = 76; goto done;}
- case 42:
+ case 41:
{t.kind = 77; goto done;}
- case 43:
+ case 42:
{t.kind = 78; goto done;}
- case 44:
+ case 43:
{t.kind = 79; goto done;}
+ case 44:
+ {t.kind = 80; goto done;}
case 45:
{t.kind = 81; goto done;}
case 46:
- {t.kind = 85; goto done;}
+ {t.kind = 82; goto done;}
case 47:
- if (ch == '.') {buf.Append(ch); NextCh(); goto case 50;}
- else {t.kind = 86; goto done;}
+ {t.kind = 84; goto done;}
case 48:
{t.kind = 88; goto done;}
case 49:
- {t.kind = 89; goto done;}
+ if (ch == '.') {buf.Append(ch); NextCh(); goto case 50;}
+ else {t.kind = 89; goto done;}
case 50:
- {t.kind = 90; goto done;}
+ {t.kind = 91; goto done;}
case 51:
- {t.kind = 94; goto done;}
+ {t.kind = 95; goto done;}
case 52:
- {t.kind = 96; goto done;}
- case 53:
{t.kind = 97; goto done;}
- case 54:
+ case 53:
{t.kind = 98; goto done;}
+ case 54:
+ {t.kind = 99; goto done;}
case 55: {t.kind = 0; goto done;}
}
done:
diff --git a/Source/Dafny/Translator.ssc b/Source/Dafny/Translator.ssc
index c079db7e..778096e9 100644
--- a/Source/Dafny/Translator.ssc
+++ b/Source/Dafny/Translator.ssc
@@ -104,6 +104,7 @@ namespace Microsoft.Dafny {
public readonly string! HeapVarName;
public readonly Bpl.Constant! CevHeapName;
public readonly Bpl.Type! ClassNameType;
+ public readonly Bpl.Type! FieldCategoryType;
public readonly Bpl.Type! DatatypeType;
public readonly Bpl.Type! DtCtorId;
public readonly Bpl.Expr! Null;
@@ -114,7 +115,8 @@ namespace Microsoft.Dafny {
public PredefinedDecls(Bpl.TypeCtorDecl! refType, Bpl.TypeCtorDecl! boxType, Bpl.TypeCtorDecl! cevTokenType, Bpl.TypeCtorDecl! cevVariableKind, Bpl.TypeCtorDecl! cevEventType,
Bpl.TypeSynonymDecl! setTypeCtor, Bpl.TypeCtorDecl! seqTypeCtor, Bpl.TypeCtorDecl! fieldNameType,
- Bpl.GlobalVariable! heap, Bpl.TypeCtorDecl! classNameType, Bpl.TypeCtorDecl! datatypeType, Bpl.TypeCtorDecl! dtCtorId,
+ Bpl.GlobalVariable! heap, Bpl.TypeCtorDecl! classNameType, Bpl.TypeCtorDecl! fieldCategoryType,
+ Bpl.TypeCtorDecl! datatypeType, Bpl.TypeCtorDecl! dtCtorId,
Bpl.Constant! allocField, Bpl.Constant! cevHeapNameConst) {
Bpl.CtorType refT = new Bpl.CtorType(Token.NoToken, refType, new Bpl.TypeSeq());
this.RefType = refT;
@@ -129,6 +131,7 @@ namespace Microsoft.Dafny {
this.HeapVarName = heap.Name;
this.CevHeapName = cevHeapNameConst;
this.ClassNameType = new Bpl.CtorType(Token.NoToken, classNameType, new Bpl.TypeSeq());
+ this.FieldCategoryType = new Bpl.CtorType(Token.NoToken, fieldCategoryType, new Bpl.TypeSeq());
this.DatatypeType = new Bpl.CtorType(Token.NoToken, datatypeType, new Bpl.TypeSeq());
this.DtCtorId = new Bpl.CtorType(Token.NoToken, dtCtorId, new Bpl.TypeSeq());
this.allocField = allocField;
@@ -150,6 +153,7 @@ namespace Microsoft.Dafny {
Bpl.TypeCtorDecl seqTypeCtor = null;
Bpl.TypeCtorDecl fieldNameType = null;
Bpl.TypeCtorDecl classNameType = null;
+ Bpl.TypeCtorDecl fieldCategoryType = null;
Bpl.TypeCtorDecl datatypeType = null;
Bpl.TypeCtorDecl dtCtorId = null;
Bpl.TypeCtorDecl boxType = null;
@@ -165,6 +169,8 @@ namespace Microsoft.Dafny {
fieldNameType = dt;
} else if (dt.Name == "ClassName") {
classNameType = dt;
+ } else if (dt.Name == "FieldCategory") {
+ fieldCategoryType = dt;
} else if (dt.Name == "DatatypeType") {
datatypeType = dt;
} else if (dt.Name == "DtCtorId") {
@@ -207,6 +213,8 @@ namespace Microsoft.Dafny {
Console.WriteLine("Error: Dafny prelude is missing declaration of type Field");
} else if (classNameType == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of type ClassName");
+ } else if (fieldCategoryType == null) {
+ Console.WriteLine("Error: Dafny prelude is missing declaration of type FieldCategory");
} else if (datatypeType == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of type DatatypeType");
} else if (dtCtorId == null) {
@@ -229,7 +237,7 @@ namespace Microsoft.Dafny {
Console.WriteLine("Error: Dafny prelude is missing declaration of constant #loc.$Heap");
} else {
return new PredefinedDecls(refType, boxType, cevTokenType, cevVariableKind, cevEventType,
- setTypeCtor, seqTypeCtor, fieldNameType, heap, classNameType, datatypeType, dtCtorId,
+ setTypeCtor, seqTypeCtor, fieldNameType, heap, classNameType, fieldCategoryType, datatypeType, dtCtorId,
allocField, cevHeapNameConst);
}
return null;
@@ -623,7 +631,7 @@ namespace Microsoft.Dafny {
Bpl.Expr oDotFsubI = FunctionCall(f.tok, BuiltinFunction.SeqIndex, predef.BoxType, oDotF, i);
Bpl.Expr unbox = FunctionCall(f.tok, BuiltinFunction.Unbox, predef.RefType, oDotFsubI);
- Bpl.Expr range = InSeqRange(f.tok, i, oDotF, null, false);
+ Bpl.Expr range = InSeqRange(f.tok, i, oDotF, true, null, false);
Bpl.Trigger tr = new Bpl.Trigger(f.tok, true, new Bpl.ExprSeq(oDotFsubI));
@@ -652,16 +660,17 @@ namespace Microsoft.Dafny {
}
}
- Bpl.Expr! InSeqRange(Token! tok, Bpl.Expr! index, Bpl.Expr! seq, Bpl.Expr lowerBound, bool includeUpperBound) {
+ Bpl.Expr! InSeqRange(Token! tok, Bpl.Expr! index, Bpl.Expr! seq, bool isSequence, Bpl.Expr lowerBound, bool includeUpperBound) {
if (lowerBound == null) {
lowerBound = Bpl.Expr.Literal(0);
}
Bpl.Expr lower = Bpl.Expr.Le(lowerBound, index);
+ Bpl.Expr length = FunctionCall(tok, isSequence ? BuiltinFunction.SeqLength : BuiltinFunction.ArrayLength, null, seq);
Bpl.Expr upper;
if (includeUpperBound) {
- upper = Bpl.Expr.Le(index, FunctionCall(tok, BuiltinFunction.SeqLength, null, seq));
+ upper = Bpl.Expr.Le(index, length);
} else {
- upper = Bpl.Expr.Lt(index, FunctionCall(tok, BuiltinFunction.SeqLength, null, seq));
+ upper = Bpl.Expr.Lt(index, length);
}
return Bpl.Expr.And(lower, upper);
}
@@ -975,7 +984,7 @@ namespace Microsoft.Dafny {
Bpl.Expr boxO = FunctionCall(tok, BuiltinFunction.Box, null, o);
Bpl.Variable iVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$i", Bpl.Type.Int));
Bpl.Expr i = new Bpl.IdentifierExpr(tok, iVar);
- Bpl.Expr iBounds = InSeqRange(tok, i, etran.TrExpr(e), null, false);
+ Bpl.Expr iBounds = InSeqRange(tok, i, etran.TrExpr(e), true, null, false);
Bpl.Expr XsubI = FunctionCall(tok, BuiltinFunction.SeqIndex, predef.BoxType, etran.TrExpr(e), i);
// TODO: the equality in the next line should be changed to one that understands extensionality
disjunct = new Bpl.ExistsExpr(tok, new Bpl.VariableSeq(iVar), Bpl.Expr.Imp(iBounds, Bpl.Expr.Eq(XsubI, boxO)));
@@ -1083,17 +1092,18 @@ namespace Microsoft.Dafny {
}
} else if (expr is SeqSelectExpr) {
SeqSelectExpr e = (SeqSelectExpr)expr;
+ bool isSequence = e.Seq.Type is SeqType;
Bpl.Expr total = IsTotal(e.Seq, etran);
Bpl.Expr seq = etran.TrExpr(e.Seq);
Bpl.Expr e0 = null;
if (e.E0 != null) {
e0 = etran.TrExpr(e.E0);
total = BplAnd(total, IsTotal(e.E0, etran));
- total = BplAnd(total, InSeqRange(expr.tok, e0, seq, null, !e.SelectOne));
+ total = BplAnd(total, InSeqRange(expr.tok, e0, seq, isSequence, null, !e.SelectOne));
}
if (e.E1 != null) {
total = BplAnd(total, IsTotal(e.E1, etran));
- total = BplAnd(total, InSeqRange(expr.tok, etran.TrExpr(e.E1), seq, e0, true));
+ total = BplAnd(total, InSeqRange(expr.tok, etran.TrExpr(e.E1), seq, isSequence, e0, true));
}
return total;
} else if (expr is SeqUpdateExpr) {
@@ -1102,7 +1112,7 @@ namespace Microsoft.Dafny {
Bpl.Expr seq = etran.TrExpr(e.Seq);
Bpl.Expr index = etran.TrExpr(e.Index);
total = BplAnd(total, IsTotal(e.Index, etran));
- total = BplAnd(total, InSeqRange(expr.tok, index, seq, null, false));
+ total = BplAnd(total, InSeqRange(expr.tok, index, seq, true, null, false));
total = BplAnd(total, IsTotal(e.Value, etran));
return total;
} else if (expr is FunctionCallExpr) {
@@ -1137,7 +1147,11 @@ namespace Microsoft.Dafny {
return IsTotal(e.E, etran);
} else if (expr is UnaryExpr) {
UnaryExpr e = (UnaryExpr)expr;
- return IsTotal(e.E, etran);
+ Bpl.Expr t = IsTotal(e.E, etran);
+ if (e.Op == UnaryExpr.Opcode.SeqLength && !(e.E.Type is SeqType)) {
+ return Bpl.Expr.And(t, Bpl.Expr.Neq(etran.TrExpr(e.E), predef.Null));
+ }
+ return t;
} else if (expr is BinaryExpr) {
BinaryExpr e = (BinaryExpr)expr;
Bpl.Expr t0 = IsTotal(e.E0, etran);
@@ -1240,17 +1254,23 @@ namespace Microsoft.Dafny {
}
} else if (expr is SeqSelectExpr) {
SeqSelectExpr e = (SeqSelectExpr)expr;
+ bool isSequence = e.Seq.Type is SeqType;
CheckWellformed(e.Seq, func, Position.Neither, locals, builder, etran);
Bpl.Expr seq = etran.TrExpr(e.Seq);
Bpl.Expr e0 = null;
if (e.E0 != null) {
e0 = etran.TrExpr(e.E0);
CheckWellformed(e.E0, func, Position.Neither, locals, builder, etran);
- builder.Add(Assert(expr.tok, InSeqRange(expr.tok, e0, seq, null, !e.SelectOne), "index out of range"));
+ builder.Add(Assert(expr.tok, InSeqRange(expr.tok, e0, seq, isSequence, null, !e.SelectOne), "index out of range"));
}
if (e.E1 != null) {
CheckWellformed(e.E1, func, Position.Neither, locals, builder, etran);
- builder.Add(Assert(expr.tok, InSeqRange(expr.tok, etran.TrExpr(e.E1), seq, e0, true), "end-of-range beyond length of sequence"));
+ builder.Add(Assert(expr.tok, InSeqRange(expr.tok, etran.TrExpr(e.E1), seq, isSequence, e0, true), "end-of-range beyond length of " + (isSequence ? "sequence" : "array")));
+ }
+ if (func != null && ((!)e.Seq.Type).IsArrayType) {
+ assert e.E0 != null;
+ Bpl.Expr fieldName = FunctionCall(expr.tok, BuiltinFunction.IndexField, null, etran.TrExpr(e.E0));
+ builder.Add(Assert(expr.tok, Bpl.Expr.SelectTok(expr.tok, etran.TheFrame(expr.tok), seq, fieldName), "insufficient reads clause to read array element"));
}
} else if (expr is SeqUpdateExpr) {
SeqUpdateExpr e = (SeqUpdateExpr)expr;
@@ -1258,7 +1278,7 @@ namespace Microsoft.Dafny {
Bpl.Expr seq = etran.TrExpr(e.Seq);
Bpl.Expr index = etran.TrExpr(e.Index);
CheckWellformed(e.Index, func, Position.Neither, locals, builder, etran);
- builder.Add(Assert(expr.tok, InSeqRange(expr.tok, index, seq, null, false), "index out of range"));
+ builder.Add(Assert(expr.tok, InSeqRange(expr.tok, index, seq, true, null, false), "index out of range"));
CheckWellformed(e.Value, func, Position.Neither, locals, builder, etran);
} else if (expr is FunctionCallExpr) {
FunctionCallExpr e = (FunctionCallExpr)expr;
@@ -1325,6 +1345,9 @@ namespace Microsoft.Dafny {
} else if (expr is UnaryExpr) {
UnaryExpr e = (UnaryExpr)expr;
CheckWellformed(e.E, func, e.Op == UnaryExpr.Opcode.Not ? Negate(pos) : Position.Neither, locals, builder, etran);
+ if (e.Op == UnaryExpr.Opcode.SeqLength && !(e.E.Type is SeqType)) {
+ CheckNonNull(expr.tok, e.E, builder, etran);
+ }
} else if (expr is BinaryExpr) {
BinaryExpr e = (BinaryExpr)expr;
CheckWellformed(e.E0, func, e.ResolvedOp == BinaryExpr.ResolvedOpcode.Imp ? Negate(pos) : pos, locals, builder, etran);
@@ -1423,8 +1446,6 @@ namespace Microsoft.Dafny {
if (classes.TryGetValue(cl, out cc)) {
assert cc != null;
} else {
- // TODO: make the following a function when the class has type parameters, so that different instantiations
- // of a class can be distinguished
cc = new Bpl.Constant(cl.tok, new Bpl.TypedIdent(cl.tok, "class." + cl.Name, predef.ClassNameType), true);
classes.Add(cl, cc);
}
@@ -1485,11 +1506,14 @@ namespace Microsoft.Dafny {
if (fields.TryGetValue(f, out fc)) {
assert fc != null;
} else {
+ // const unique f: Field ty;
Bpl.Type ty = predef.FieldName(f.tok, TrType(f.Type));
fc = new Bpl.Constant(f.tok, new Bpl.TypedIdent(f.tok, f.FullName, ty), true);
fields.Add(f, fc);
- // axiom DeclType(f) == C;
- Bpl.Axiom ax = new Bpl.Axiom(f.tok, Bpl.Expr.Eq(FunctionCall(f.tok, BuiltinFunction.DeclType, ty, Bpl.Expr.Ident(fc)), new Bpl.IdentifierExpr(f.tok, GetClass((!)f.EnclosingClass))));
+ // axiom FCat(f) == $NamedField && DeclType(f) == C;
+ Bpl.Expr fcat = Bpl.Expr.Eq(FunctionCall(f.tok, BuiltinFunction.FCat, ty, Bpl.Expr.Ident(fc)), new Bpl.IdentifierExpr(f.tok, "$NamedField", predef.FieldCategoryType));
+ Bpl.Expr declType = Bpl.Expr.Eq(FunctionCall(f.tok, BuiltinFunction.DeclType, ty, Bpl.Expr.Ident(fc)), new Bpl.IdentifierExpr(f.tok, GetClass((!)f.EnclosingClass)));
+ Bpl.Axiom ax = new Bpl.Axiom(f.tok, Bpl.Expr.And(fcat, declType));
sink.TopLevelDeclarations.Add(ax);
}
return fc;
@@ -1849,6 +1873,8 @@ namespace Microsoft.Dafny {
builder.Add(new Bpl.CallCmd(stmt.Tok, "CevUpdate",
new Bpl.ExprSeq(CevLocation(stmt.Tok), CevVariable(stmt.Tok, v.Name), v),
new Bpl.IdentifierExprSeq()));
+ } else if (s.Lhs is SeqSelectExpr) {
+ // TODO: CEV
} else {
builder.Add(new Bpl.CallCmd(stmt.Tok, "CevUpdateHeap",
new Bpl.ExprSeq(CevLocation(stmt.Tok), CevVariable(stmt.Tok, predef.HeapVarName), etran.HeapExpr),
@@ -2013,6 +2039,30 @@ namespace Microsoft.Dafny {
int loopId = loopHeapVarCount;
loopHeapVarCount++;
+ // use simple heuristics to create a default decreases clause, if none is given
+ List<Expression!> theDecreases = s.Decreases;
+ if (theDecreases.Count == 0) {
+ Expression guess = null;
+ BinaryExpr bin = s.Guard as BinaryExpr;
+ if (bin != null) {
+ switch (bin.ResolvedOp) {
+ case BinaryExpr.ResolvedOpcode.Lt:
+ case BinaryExpr.ResolvedOpcode.Le:
+ guess = IntSub(s.Tok, bin.E1, bin.E0);
+ break;
+ case BinaryExpr.ResolvedOpcode.Ge:
+ case BinaryExpr.ResolvedOpcode.Gt:
+ guess = IntSub(s.Tok, bin.E0, bin.E1);
+ break;
+ default:
+ break;
+ }
+ }
+ if (guess != null) {
+ theDecreases.Add(guess);
+ }
+ }
+
Bpl.LocalVariable preLoopHeapVar = new Bpl.LocalVariable(stmt.Tok, new Bpl.TypedIdent(stmt.Tok, "$PreLoopHeap" + loopId, predef.HeapType));
locals.Add(preLoopHeapVar);
Bpl.IdentifierExpr preLoopHeap = new Bpl.IdentifierExpr(stmt.Tok, preLoopHeapVar);
@@ -2055,7 +2105,7 @@ namespace Microsoft.Dafny {
}
}
// check definedness of decreases clause
- foreach (Expression e in s.Decreases) {
+ foreach (Expression e in theDecreases) {
invDefinednessBuilder.Add(Assert(e.tok, IsTotal(e, etran), "decreases expression must be well defined at top of each loop iteration")); // totality check
}
// include boilerplate invariants
@@ -2104,13 +2154,13 @@ namespace Microsoft.Dafny {
new Bpl.ExprSeq(CevLocation(stmt.Tok), new Bpl.IdentifierExpr(stmt.Tok, "loop_entered", predef.CevEventType)),
new Bpl.IdentifierExprSeq()));
// termination checking
- if (exists{Expression e in s.Decreases; e is WildcardExpr}) {
+ if (exists{Expression e in theDecreases; e is WildcardExpr}) {
// omit termination checking for this loop
TrStmt(s.Body, loopBodyBuilder, locals, etran);
} else {
List<Bpl.Expr!> oldBfs = new List<Bpl.Expr!>();
int c = 0;
- foreach (Expression e in s.Decreases) {
+ foreach (Expression e in theDecreases) {
Bpl.LocalVariable bfVar = new Bpl.LocalVariable(e.tok, new Bpl.TypedIdent(e.tok, "$decr" + loopId + "$" + c, TrType((!)e.Type)));
locals.Add(bfVar);
Bpl.IdentifierExpr bf = new Bpl.IdentifierExpr(e.tok, bfVar);
@@ -2127,7 +2177,7 @@ namespace Microsoft.Dafny {
List<Token!> toks = new List<Token!>();
List<Type!> types = new List<Type!>();
List<Bpl.Expr!> decrs = new List<Bpl.Expr!>();
- foreach (Expression e in s.Decreases) {
+ foreach (Expression e in theDecreases) {
toks.Add(e.tok);
types.Add((!)e.Type);
decrs.Add(etran.TrExpr(e));
@@ -2171,7 +2221,7 @@ namespace Microsoft.Dafny {
Bpl.BoundVariable iVar = new Bpl.BoundVariable(stmt.Tok, new Bpl.TypedIdent(stmt.Tok, "$i", Bpl.Type.Int));
Bpl.IdentifierExpr i = new Bpl.IdentifierExpr(stmt.Tok, iVar);
Bpl.Expr S = etran.TrExpr(s.Collection);
- Bpl.Expr range = InSeqRange(stmt.Tok, i, S, null, false);
+ Bpl.Expr range = InSeqRange(stmt.Tok, i, S, true, null, false);
Bpl.Expr Si = FunctionCall(stmt.Tok, BuiltinFunction.SeqIndex, predef.BoxType, S, i);
Bpl.Trigger tr = new Bpl.Trigger(stmt.Tok, true, new Bpl.ExprSeq(Si));
// TODO: in the next line, the == should be replaced by something that understands extensionality, for sets and sequences
@@ -2312,6 +2362,15 @@ namespace Microsoft.Dafny {
}
}
+ static Expression! IntSub(Token! tok, Expression! e0, Expression! e1)
+ requires e0.Type is IntType && e1.Type is IntType;
+ {
+ BinaryExpr s = new BinaryExpr(tok, BinaryExpr.Opcode.Sub, e0, e1);
+ s.ResolvedOp = BinaryExpr.ResolvedOpcode.Sub;
+ s.Type = Type.Int;
+ return s;
+ }
+
void CheckCallTermination(Token! tok, List<Expression!>! contextDecreases, List<Expression!>! calleeDecreases,
Expression receiverReplacement, Dictionary<IVariable,Expression!>! substMap,
ExpressionTranslator! etran, Bpl.StmtListBuilder! builder)
@@ -2489,7 +2548,7 @@ namespace Microsoft.Dafny {
Bpl.Expr xSubI = FunctionCall(tok, BuiltinFunction.SeqIndex, predef.BoxType, x, i);
Bpl.Expr unbox = FunctionCall(tok, BuiltinFunction.Unbox, predef.RefType, xSubI);
- Bpl.Expr range = InSeqRange(tok, i, x, null, false);
+ Bpl.Expr range = InSeqRange(tok, i, x, true, null, false);
Bpl.Trigger tr = new Bpl.Trigger(tok, true, new Bpl.ExprSeq(xSubI));
@@ -2523,7 +2582,7 @@ namespace Microsoft.Dafny {
Bpl.IdentifierExpr bLhs = (Bpl.IdentifierExpr)etran.TrExpr(lhs); // TODO: is this cast always justified?
Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(tok, bLhs, bRhs);
builder.Add(cmd);
- } else {
+ } else if (lhs is FieldSelectExpr) {
FieldSelectExpr fse = (FieldSelectExpr)lhs;
assert fse.Field != null;
// check that the enclosing modifies clause allows this object to be written: assert $_Frame[obj];
@@ -2535,6 +2594,38 @@ namespace Microsoft.Dafny {
builder.Add(cmd);
// assume $IsGoodHeap($Heap);
builder.Add(AssumeGoodHeap(tok, etran));
+ } else {
+ SeqSelectExpr sel = (SeqSelectExpr)lhs;
+ assert sel.Seq.Type != null && sel.Seq.Type.IsArrayType;
+ bRhs = etran.BoxIfNecessary(tok, bRhs, UserDefinedType.ArrayElementType(sel.Seq.Type));
+ if (sel.SelectOne) {
+ assert sel.E0 != null;
+ Bpl.Expr fieldName = FunctionCall(tok, BuiltinFunction.IndexField, null, etran.TrExpr(sel.E0));
+ // check that the enclosing modifies clause allows this object to be written: assert $_Frame[obj,index];
+ builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.TheFrame(tok), etran.TrExpr(sel.Seq), fieldName), "assignment may update an array not in the enclosing method's modifies clause"));
+
+ Bpl.IdentifierExpr h = (Bpl.IdentifierExpr!)etran.HeapExpr; // TODO: is this cast always justified?
+ Bpl.Cmd cmd = Bpl.Cmd.MapAssign(tok, h, etran.TrExpr(sel.Seq), fieldName, bRhs);
+ builder.Add(cmd);
+ // assume $IsGoodHeap($Heap);
+ builder.Add(AssumeGoodHeap(tok, etran));
+ } else {
+ Bpl.Expr low = sel.E0 == null ? Bpl.Expr.Literal(0) : etran.TrExpr(sel.E0);
+ Bpl.Expr high = sel.E1 == null ? FunctionCall(tok, BuiltinFunction.ArrayLength, null, etran.TrExpr(sel.Seq)) : etran.TrExpr(sel.E1);
+ // check frame:
+ // assert (forall i: int :: low <= i && i < high ==> $_Frame[arr,i]);
+ Bpl.Variable iVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$i", Bpl.Type.Int));
+ Bpl.IdentifierExpr ie = new Bpl.IdentifierExpr(tok, iVar);
+ Bpl.Expr ante = Bpl.Expr.And(Bpl.Expr.Le(low, ie), Bpl.Expr.Lt(ie, high));
+ Bpl.Expr fieldName = FunctionCall(tok, BuiltinFunction.IndexField, null, ie);
+ Bpl.Expr cons = Bpl.Expr.SelectTok(tok, etran.TheFrame(tok), etran.TrExpr(sel.Seq), fieldName);
+ Bpl.Expr q = new Bpl.ForallExpr(tok, new Bpl.VariableSeq(iVar), Bpl.Expr.Imp(ante, cons));
+ builder.Add(Assert(tok, q, "assignment may update an array not in the enclosing method's modifies clause"));
+ // do the update: call UpdateArrayRange(arr, low, high, rhs);
+ builder.Add(new Bpl.CallCmd(tok, "UpdateArrayRange",
+ new Bpl.ExprSeq(etran.TrExpr(sel.Seq), low, high, bRhs),
+ new Bpl.IdentifierExprSeq()));
+ }
}
} else if (rhs is HavocRhs) {
@@ -2544,13 +2635,35 @@ namespace Microsoft.Dafny {
} else {
assert rhs is TypeRhs; // otherwise, an unexpected AssignmentRhs
+ TypeRhs tRhs = (TypeRhs)rhs;
assert lhs is IdentifierExpr; // for this kind of RHS, the LHS is restricted to be a simple variable
+ if (tRhs.ArraySize != null) {
+ CheckWellformed(tRhs.ArraySize, null, Position.Positive, locals, builder, etran);
+ builder.Add(Assert(tok, Bpl.Expr.Le(Bpl.Expr.Literal(0), etran.TrExpr(tRhs.ArraySize)), "array size might be negative"));
+ }
+
Bpl.IdentifierExpr nw = GetNewVar_IdExpr(tok, locals);
builder.Add(new Bpl.HavocCmd(tok, new Bpl.IdentifierExprSeq(nw)));
// assume $nw != null && !$Heap[$nw, alloc] && dtype($nw) == RHS;
Bpl.Expr nwNotNull = Bpl.Expr.Neq(nw, predef.Null);
- builder.Add(new Bpl.AssumeCmd(tok, Bpl.Expr.And(nwNotNull, etran.GoodRef_Class(tok, nw, (UserDefinedType)((TypeRhs)rhs).Type, true))));
+ Bpl.Expr rightType;
+ if (tRhs.ArraySize != null) {
+ // array allocation
+ List<Type!> typeArgs = new List<Type!>();
+ typeArgs.Add(tRhs.EType);
+ rightType = etran.GoodRef_Ref(tok, nw, new Bpl.IdentifierExpr(tok, "class.array", predef.ClassNameType), typeArgs, true);
+ } else if (tRhs.EType is ObjectType) {
+ rightType = etran.GoodRef_Ref(tok, nw, new Bpl.IdentifierExpr(tok, "class.object", predef.ClassNameType), new List<Type!>(), true);
+ } else {
+ rightType = etran.GoodRef_Class(tok, nw, (UserDefinedType)tRhs.EType, true);
+ }
+ builder.Add(new Bpl.AssumeCmd(tok, Bpl.Expr.And(nwNotNull, rightType)));
+ if (tRhs.ArraySize != null) {
+ // assume Array#Length($nw) == arraySize;
+ Bpl.Expr arrayLength = FunctionCall(tok, BuiltinFunction.ArrayLength, null, nw);
+ builder.Add(new Bpl.AssumeCmd(tok, Bpl.Expr.Eq(arrayLength, etran.TrExpr(tRhs.ArraySize))));
+ }
// $Heap[$nw, alloc] := true;
Bpl.Expr alloc = predef.Alloc(tok);
Bpl.Cmd cmd = Bpl.Cmd.MapAssign(tok, (Bpl.IdentifierExpr/*TODO: this cast is dubious*/)etran.HeapExpr, nw, alloc, Bpl.Expr.True);
@@ -2685,13 +2798,26 @@ namespace Microsoft.Dafny {
} else if (expr is SeqSelectExpr) {
SeqSelectExpr e = (SeqSelectExpr)expr;
Bpl.Expr seq = TrExpr(e.Seq);
- Type elmtType = ((SeqType!)e.Seq.Type).Arg;
+ Type elmtType;
+ assert e.Seq.Type != null; // the expression has been successfully resolved
+ if (e.Seq.Type.IsArrayType) {
+ assert e.SelectOne; // resolution enforces that a non-unit array selections is allowed only as an assignment LHS
+ elmtType = UserDefinedType.ArrayElementType(e.Seq.Type);
+ } else {
+ elmtType = ((SeqType)e.Seq.Type).Arg;
+ }
Bpl.Type elType = translator.TrType(elmtType);
Bpl.Expr e0 = e.E0 == null ? null : TrExpr(e.E0);
Bpl.Expr e1 = e.E1 == null ? null : TrExpr(e.E1);
if (e.SelectOne) {
assert e1 == null;
- Bpl.Expr x = translator.FunctionCall(expr.tok, BuiltinFunction.SeqIndex, predef.BoxType, seq, e0);
+ Bpl.Expr x;
+ if (e.Seq.Type.IsArrayType) {
+ Bpl.Expr fieldName = translator.FunctionCall(expr.tok, BuiltinFunction.IndexField, null, e0);
+ x = Bpl.Expr.SelectTok(expr.tok, HeapExpr, TrExpr(e.Seq), fieldName);
+ } else {
+ x = translator.FunctionCall(expr.tok, BuiltinFunction.SeqIndex, predef.BoxType, seq, e0);
+ }
if (!ModeledAsBoxType(elmtType)) {
x = translator.FunctionCall(expr.tok, BuiltinFunction.Unbox, elType, x);
}
@@ -2773,7 +2899,7 @@ namespace Microsoft.Dafny {
// TODO: trigger?
Bpl.Variable iVar = new Bpl.BoundVariable(expr.tok, new Bpl.TypedIdent(expr.tok, "$i", Bpl.Type.Int));
Bpl.Expr i = new Bpl.IdentifierExpr(expr.tok, iVar);
- Bpl.Expr iBounds = translator.InSeqRange(expr.tok, i, TrExpr(e.E), null, false);
+ Bpl.Expr iBounds = translator.InSeqRange(expr.tok, i, TrExpr(e.E), true, null, false);
Bpl.Expr XsubI = translator.FunctionCall(expr.tok, BuiltinFunction.SeqIndex, predef.RefType, TrExpr(e.E), i);
Bpl.Expr oIsFresh = Bpl.Expr.Not(IsAlloced(expr.tok, XsubI, oldHeap));
Bpl.Expr xsubiNotNull = Bpl.Expr.Neq(translator.FunctionCall(expr.tok, BuiltinFunction.Unbox, predef.RefType, XsubI), predef.Null);
@@ -2793,7 +2919,11 @@ namespace Microsoft.Dafny {
case UnaryExpr.Opcode.Not:
return Bpl.Expr.Not(arg);
case UnaryExpr.Opcode.SeqLength:
- return translator.FunctionCall(expr.tok, BuiltinFunction.SeqLength, null, arg);
+ if (e.E.Type is SeqType) {
+ return translator.FunctionCall(expr.tok, BuiltinFunction.SeqLength, null, arg);
+ } else {
+ return translator.FunctionCall(expr.tok, BuiltinFunction.ArrayLength, null, arg);
+ }
default:
assert false; // unexpected unary expression
}
@@ -3087,6 +3217,10 @@ namespace Microsoft.Dafny {
public Bpl.Expr! GoodRef_Class(Token! tok, Bpl.Expr! e, UserDefinedType! type, bool isNew)
requires type.ResolvedClass is ClassDecl;
{
+ return GoodRef_Ref(tok, e, new Bpl.IdentifierExpr(tok, translator.GetClass(type.ResolvedClass)), type.TypeArgs, isNew);
+ }
+
+ public Bpl.Expr! GoodRef_Ref(Token! tok, Bpl.Expr! e, Bpl.Expr! type, List<Type!>! typeArgs, bool isNew) {
// Heap[e, alloc]
Bpl.Expr r = IsAlloced(tok, e);
if (isNew) {
@@ -3095,12 +3229,12 @@ namespace Microsoft.Dafny {
// dtype(e) == C
Bpl.Expr dtypeFunc = translator.FunctionCall(tok, BuiltinFunction.DynamicType, null, e);
- Bpl.Expr dtype = Bpl.Expr.Eq(dtypeFunc, new Bpl.IdentifierExpr(tok, translator.GetClass(type.ResolvedClass)));
+ Bpl.Expr dtype = Bpl.Expr.Eq(dtypeFunc, type);
r = Bpl.Expr.And(r, dtype);
// dtypeParams(e, #) == T
int n = 0;
- foreach (Type arg in type.TypeArgs) {
+ foreach (Type arg in typeArgs) {
Bpl.Expr tpFunc = translator.FunctionCall(tok, BuiltinFunction.TypeParams, null, e, Bpl.Expr.Literal(n));
Bpl.Expr ta = translator.GetTypeExpr(tok, arg);
if (ta != null) {
@@ -3180,6 +3314,9 @@ namespace Microsoft.Dafny {
SeqEqual,
SeqSameUntil,
+ ArrayLength,
+ IndexField,
+
IfThenElse,
Box,
@@ -3192,6 +3329,7 @@ namespace Microsoft.Dafny {
TypeParams, // type parameters to allocated type
TypeTuple,
DeclType,
+ FCat, // field category (indexed or named)
DatatypeCtorId,
DtRank,
@@ -3291,6 +3429,15 @@ namespace Microsoft.Dafny {
assert typeInstantiation == null;
return FunctionCall(tok, "Seq#SameUntil", Bpl.Type.Bool, args);
+ case BuiltinFunction.ArrayLength:
+ assert args.Length == 1;
+ assert typeInstantiation == null;
+ return FunctionCall(tok, "Array#Length", Bpl.Type.Int, args);
+ case BuiltinFunction.IndexField:
+ assert args.Length == 1;
+ assert typeInstantiation == null;
+ return FunctionCall(tok, "IndexField", predef.FieldName(tok, predef.BoxType), args);
+
case BuiltinFunction.IfThenElse:
assert args.Length == 3;
assert typeInstantiation != null;
@@ -3330,6 +3477,10 @@ namespace Microsoft.Dafny {
assert args.Length == 1;
assert typeInstantiation != null;
return FunctionCall(tok, "DeclType", predef.ClassNameType, args);
+ case BuiltinFunction.FCat:
+ assert args.Length == 1;
+ assert typeInstantiation != null;
+ return FunctionCall(tok, "FCat", predef.FieldCategoryType, args);
case BuiltinFunction.DatatypeCtorId:
assert args.Length == 1;
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-18 06:08:37 +0000