diff options
Diffstat (limited to 'Source/Dafny')
| -rw-r--r-- | Source/Dafny/Dafny.atg | 19 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 15 | ||||
| -rw-r--r-- | Source/Dafny/Parser.cs | 93 | ||||
| -rw-r--r-- | Source/Dafny/Printer.cs | 4 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 5 | ||||
| -rw-r--r-- | Source/Dafny/Scanner.cs | 102 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 178 |
7 files changed, 262 insertions, 154 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 071dbd64..033bc239 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -843,6 +843,7 @@ WhileStmt<out Statement/*!*/ stmt> Expression guard;
List<MaybeFreeExpression/*!*/> invariants = new List<MaybeFreeExpression/*!*/>();
List<Expression/*!*/> decreases = new List<Expression/*!*/>();
+ List<FrameExpression/*!*/> mod = null;
Statement/*!*/ body;
IToken bodyStart, bodyEnd;
List<GuardedAlternative> alternatives;
@@ -851,20 +852,21 @@ WhileStmt<out Statement/*!*/ stmt> "while" (. x = t; .)
(
Guard<out guard> (. Contract.Assume(guard == null || cce.Owner.None(guard)); .)
- LoopSpec<out invariants, out decreases>
+ LoopSpec<out invariants, out decreases, out mod>
BlockStmt<out body, out bodyStart, out bodyEnd>
- (. stmt = new WhileStmt(x, guard, invariants, decreases, body); .)
+ (. stmt = new WhileStmt(x, guard, invariants, decreases, mod, body); .)
|
- LoopSpec<out invariants, out decreases>
+ LoopSpec<out invariants, out decreases, out mod>
AlternativeBlock<out alternatives>
- (. stmt = new AlternativeLoopStmt(x, invariants, decreases, alternatives); .)
+ (. stmt = new AlternativeLoopStmt(x, invariants, decreases, mod, alternatives); .)
)
.
-LoopSpec<.out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*/> decreases.>
-= (. bool isFree; Expression/*!*/ e;
+LoopSpec<.out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*/> decreases, out List<FrameExpression/*!*/> mod.>
+= (. bool isFree; Expression/*!*/ e; FrameExpression/*!*/ fe;
invariants = new List<MaybeFreeExpression/*!*/>();
decreases = new List<Expression/*!*/>();
+ mod = null;
.)
{ (. isFree = false; .)
[ "free" (. isFree = true; .)
@@ -873,6 +875,11 @@ LoopSpec<.out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!* Expression<out e> (. invariants.Add(new MaybeFreeExpression(e, isFree)); .)
";"
| "decreases" DecreasesList<decreases, true> ";"
+ | "modifies" (. mod = mod ?? new List<FrameExpression>(); .)
+ [ FrameExpression<out fe> (. mod.Add(fe); .)
+ { "," FrameExpression<out fe> (. mod.Add(fe); .)
+ }
+ ] ";"
}
.
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 99cf791f..0fd83011 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -1660,20 +1660,25 @@ namespace Microsoft.Dafny { {
public readonly List<MaybeFreeExpression/*!*/>/*!*/ Invariants;
public readonly List<Expression/*!*/>/*!*/ Decreases;
+ public readonly List<FrameExpression/*!*/>/*!*/ Mod;
+ public readonly bool explictModifies;
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(cce.NonNullElements(Invariants));
Contract.Invariant(cce.NonNullElements(Decreases));
+ Contract.Invariant(Mod == null || cce.NonNullElements(Mod));
}
- public LoopStmt(IToken tok, List<MaybeFreeExpression/*!*/>/*!*/ invariants, List<Expression/*!*/>/*!*/ decreases)
+ public LoopStmt(IToken tok, List<MaybeFreeExpression/*!*/>/*!*/ invariants, List<Expression/*!*/>/*!*/ decreases, List<FrameExpression/*!*/>/*!*/ mod)
: base(tok)
{
Contract.Requires(tok != null);
Contract.Requires(cce.NonNullElements(invariants));
Contract.Requires(cce.NonNullElements(decreases));
+ Contract.Requires(mod == null || cce.NonNullElements(mod));
this.Invariants = invariants;
this.Decreases = decreases;
+ this.Mod = mod;
}
}
@@ -1687,9 +1692,9 @@ namespace Microsoft.Dafny { }
public WhileStmt(IToken tok, Expression guard,
- List<MaybeFreeExpression/*!*/>/*!*/ invariants, List<Expression/*!*/>/*!*/ decreases,
+ List<MaybeFreeExpression/*!*/>/*!*/ invariants, List<Expression/*!*/>/*!*/ decreases, List<FrameExpression/*!*/> mod,
Statement/*!*/ body)
- : base(tok, invariants, decreases) {
+ : base(tok, invariants, decreases, mod) {
Contract.Requires(tok != null);
Contract.Requires(body != null);
this.Guard = guard;
@@ -1705,9 +1710,9 @@ namespace Microsoft.Dafny { Contract.Invariant(Alternatives != null);
}
public AlternativeLoopStmt(IToken tok,
- List<MaybeFreeExpression/*!*/>/*!*/ invariants, List<Expression/*!*/>/*!*/ decreases,
+ List<MaybeFreeExpression/*!*/>/*!*/ invariants, List<Expression/*!*/>/*!*/ decreases, List<FrameExpression/*!*/> mod,
List<GuardedAlternative> alternatives)
- : base(tok, invariants, decreases) {
+ : base(tok, invariants, decreases, mod) {
Contract.Requires(tok != null);
Contract.Requires(alternatives != null);
this.Alternatives = alternatives;
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 41fc89c5..b77f5e65 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -25,7 +25,7 @@ public class Parser { const bool T = true;
const bool x = false;
const int minErrDist = 2;
-
+
public Scanner/*!*/ scanner;
public Errors/*!*/ errors;
@@ -144,10 +144,10 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! if (errDist >= minErrDist) errors.SemErr(t, msg);
errDist = 0;
}
-
- public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {
- Contract.Requires(tok != null);
- Contract.Requires(msg != null);
+
+ public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {
+ Contract.Requires(tok != null);
+ Contract.Requires(msg != null);
errors.SemErr(tok, msg);
}
@@ -160,15 +160,15 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! la = t;
}
}
-
+
void Expect (int n) {
if (la.kind==n) Get(); else { SynErr(n); }
}
-
+
bool StartOf (int s) {
return set[s, la.kind];
}
-
+
void ExpectWeak (int n, int follow) {
if (la.kind == n) Get();
else {
@@ -192,7 +192,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! }
}
-
+
void Dafny() {
ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt;
Attributes attrs; IToken/*!*/ id; List<string/*!*/> theImports;
@@ -1189,6 +1189,7 @@ List<Expression/*!*/>/*!*/ decreases) { Expression guard;
List<MaybeFreeExpression/*!*/> invariants = new List<MaybeFreeExpression/*!*/>();
List<Expression/*!*/> decreases = new List<Expression/*!*/>();
+ List<FrameExpression/*!*/> mod = null;
Statement/*!*/ body;
IToken bodyStart, bodyEnd;
List<GuardedAlternative> alternatives;
@@ -1199,13 +1200,13 @@ List<Expression/*!*/>/*!*/ decreases) { if (la.kind == 33) {
Guard(out guard);
Contract.Assume(guard == null || cce.Owner.None(guard));
- LoopSpec(out invariants, out decreases);
+ LoopSpec(out invariants, out decreases, out mod);
BlockStmt(out body, out bodyStart, out bodyEnd);
- stmt = new WhileStmt(x, guard, invariants, decreases, body);
+ stmt = new WhileStmt(x, guard, invariants, decreases, mod, body);
} else if (StartOf(11)) {
- LoopSpec(out invariants, out decreases);
+ LoopSpec(out invariants, out decreases, out mod);
AlternativeBlock(out alternatives);
- stmt = new AlternativeLoopStmt(x, invariants, decreases, alternatives);
+ stmt = new AlternativeLoopStmt(x, invariants, decreases, mod, alternatives);
} else SynErr(121);
}
@@ -1388,12 +1389,13 @@ List<Expression/*!*/>/*!*/ decreases) { Expect(8);
}
- void LoopSpec(out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*/> decreases) {
- bool isFree; Expression/*!*/ e;
+ void LoopSpec(out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*/> decreases, out List<FrameExpression/*!*/> mod) {
+ bool isFree; Expression/*!*/ e; FrameExpression/*!*/ fe;
invariants = new List<MaybeFreeExpression/*!*/>();
decreases = new List<Expression/*!*/>();
+ mod = null;
- while (la.kind == 29 || la.kind == 32 || la.kind == 59) {
+ while (StartOf(13)) {
if (la.kind == 29 || la.kind == 59) {
isFree = false;
if (la.kind == 29) {
@@ -1404,10 +1406,23 @@ List<Expression/*!*/>/*!*/ decreases) { Expression(out e);
invariants.Add(new MaybeFreeExpression(e, isFree));
Expect(17);
- } else {
+ } else if (la.kind == 32) {
Get();
DecreasesList(decreases, true);
Expect(17);
+ } else {
+ Get();
+ mod = mod ?? new List<FrameExpression>();
+ if (StartOf(8)) {
+ FrameExpression(out fe);
+ mod.Add(fe);
+ while (la.kind == 19) {
+ Get();
+ FrameExpression(out fe);
+ mod.Add(fe);
+ }
+ }
+ Expect(17);
}
}
}
@@ -1483,7 +1498,7 @@ List<Expression/*!*/>/*!*/ decreases) { void LogicalExpression(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
RelationalExpression(out e0);
- if (StartOf(13)) {
+ if (StartOf(14)) {
if (la.kind == 70 || la.kind == 71) {
AndOp();
x = t;
@@ -1531,12 +1546,12 @@ List<Expression/*!*/>/*!*/ decreases) { Term(out e0);
e = e0;
- if (StartOf(14)) {
+ if (StartOf(15)) {
RelOp(out x, out op);
firstOpTok = x;
Term(out e1);
e = new BinaryExpr(x, op, e0, e1);
- while (StartOf(14)) {
+ while (StartOf(15)) {
if (chain == null) {
chain = new List<Expression>();
ops = new List<BinaryExpr.Opcode>();
@@ -1788,7 +1803,7 @@ List<Expression/*!*/>/*!*/ decreases) { e = new ITEExpr(x, e, e0, e1);
} else if (la.kind == 60) {
MatchExpression(out e);
- } else if (StartOf(15)) {
+ } else if (StartOf(16)) {
QuantifierGuts(out e);
} else if (la.kind == 38) {
ComprehensionExpr(out e);
@@ -2163,7 +2178,7 @@ List<Expression/*!*/>/*!*/ decreases) { Expect(22);
Expect(1);
aName = t.val;
- if (StartOf(16)) {
+ if (StartOf(17)) {
AttributeArg(out aArg);
aArgs.Add(aArg);
while (la.kind == 19) {
@@ -2179,13 +2194,13 @@ List<Expression/*!*/>/*!*/ decreases) { public void Parse() {
la = new Token();
- la.val = "";
+ la.val = "";
Get();
Dafny();
- Expect(0);
+ Expect(0);
}
-
+
static readonly bool[,]/*!*/ set = {
{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
{x,x,x,x, x,T,x,x, x,T,T,T, T,T,T,x, x,x,T,x, T,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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},
@@ -2198,8 +2213,9 @@ List<Expression/*!*/>/*!*/ decreases) { {x,T,T,x, x,x,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,T,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,T,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,T,T,T, x,x,T,T, T,T,x,x, x,x},
{x,T,T,x, x,x,x,T, x,x,x,T, x,x,x,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,x,x, x,x,T,x, x,x,T,x, T,T,x,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x},
{x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,x,x,T, x,x,x,x, x,x,T,x, x,x,T,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,T,T,T, x,x,T,T, T,T,x,x, x,x},
- {x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,x,x,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,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
{x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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,T,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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},
@@ -2212,18 +2228,20 @@ List<Expression/*!*/>/*!*/ decreases) { public class Errors {
public int count = 0; // number of errors detected
public System.IO.TextWriter/*!*/ errorStream = Console.Out; // error messages go to this stream
- public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text
- public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text
-
+ public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text
+ public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text
+
public void SynErr(string filename, int line, int col, int n) {
- SynErr(filename, line, col, GetSyntaxErrorString(n));
- }
- public virtual void SynErr(string filename, int line, int col, string msg) {
- Contract.Requires(msg != null);
+ SynErr(filename, line, col, GetSyntaxErrorString(n));
+ }
+
+ public virtual void SynErr(string filename, int line, int col, string/*!*/ msg) {
+ Contract.Requires(msg != null);
errorStream.WriteLine(errMsgFormat, filename, line, col, msg);
count++;
- }
- string GetSyntaxErrorString(int n) {
+ }
+
+ string GetSyntaxErrorString(int n) {
string s;
switch (n) {
case 0: s = "EOF expected"; break;
@@ -2375,7 +2393,7 @@ public class Errors { default: s = "error " + n; break;
}
- return s;
+ return s;
}
public void SemErr(IToken/*!*/ tok, string/*!*/ msg) { // semantic errors
@@ -2383,8 +2401,9 @@ public class Errors { Contract.Requires(msg != null);
SemErr(tok.filename, tok.line, tok.col, msg);
}
+
public virtual void SemErr(string filename, int line, int col, string/*!*/ msg) {
- Contract.Requires(msg != null);
+ Contract.Requires(msg != null);
errorStream.WriteLine(errMsgFormat, filename, line, col, msg);
count++;
}
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index a8970f05..9970d61a 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -507,6 +507,10 @@ namespace Microsoft.Dafny { PrintSpec("invariant", s.Invariants, indent + IndentAmount);
PrintSpecLine("decreases", s.Decreases, indent + IndentAmount);
+ if (s.Mod != null)
+ {
+ PrintFrameSpecLine("modifies", s.Mod, indent + IndentAmount);
+ }
Indent(indent);
PrintStatement(s.Body, indent);
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 17309836..c0bf4392 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -1512,6 +1512,11 @@ namespace Microsoft.Dafny { }
// any type is fine
}
+ if(s.Mod != null) {
+ foreach (FrameExpression fe in s.Mod) {
+ ResolveFrameExpression(fe, "modifies");
+ }
+ }
s.IsGhost = bodyMustBeSpecOnly;
loopStack.Add(s); // push
if (s.Labels == null) { // otherwise, "s" is already in "inSpecOnlyContext" map
diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs index 19157a32..81f556c8 100644 --- a/Source/Dafny/Scanner.cs +++ b/Source/Dafny/Scanner.cs @@ -19,7 +19,7 @@ public class Buffer { // a) whole stream in buffer
// b) part of stream in buffer
// 2) non seekable stream (network, console)
-
+
public const int EOF = 65535 + 1; // char.MaxValue + 1;
const int MIN_BUFFER_LENGTH = 1024; // 1KB
const int MAX_BUFFER_LENGTH = MIN_BUFFER_LENGTH * 64; // 64KB
@@ -31,15 +31,17 @@ public class Buffer { Stream/*!*/ stream; // input stream (seekable)
bool isUserStream; // was the stream opened by the user?
-[ContractInvariantMethod]
-void ObjectInvariant(){
- Contract.Invariant(buf != null);
- Contract.Invariant(stream != null);}
- [NotDelayed]
- public Buffer (Stream/*!*/ s, bool isUserStream) :base() {
+ [ContractInvariantMethod]
+ void ObjectInvariant(){
+ Contract.Invariant(buf != null);
+ Contract.Invariant(stream != null);
+ }
+
+// [NotDelayed]
+ public Buffer (Stream/*!*/ s, bool isUserStream) : base() {
Contract.Requires(s != null);
stream = s; this.isUserStream = isUserStream;
-
+
int fl, bl;
if (s.CanSeek) {
fl = (int) s.Length;
@@ -51,12 +53,12 @@ void ObjectInvariant(){ buf = new byte[(bl>0) ? bl : MIN_BUFFER_LENGTH];
fileLen = fl; bufLen = bl;
-
+
if (fileLen > 0) Pos = 0; // setup buffer to position 0 (start)
else bufPos = 0; // index 0 is already after the file, thus Pos = 0 is invalid
if (bufLen == fileLen && s.CanSeek) Close();
}
-
+
protected Buffer(Buffer/*!*/ b) { // called in UTF8Buffer constructor
Contract.Requires(b != null);
buf = b.buf;
@@ -73,14 +75,14 @@ void ObjectInvariant(){ }
~Buffer() { Close(); }
-
+
protected void Close() {
if (!isUserStream && stream != null) {
stream.Close();
//stream = null;
}
}
-
+
public virtual int Read () {
if (bufPos < bufLen) {
return buf[bufPos++];
@@ -100,7 +102,7 @@ void ObjectInvariant(){ Pos = curPos;
return ch;
}
-
+
public string/*!*/ GetString (int beg, int end) {
Contract.Ensures(Contract.Result<string>() != null);
int len = 0;
@@ -139,7 +141,7 @@ void ObjectInvariant(){ }
}
}
-
+
// Read the next chunk of bytes from the stream, increases the buffer
// if needed and updates the fields fileLen and bufLen.
// Returns the number of bytes read.
@@ -213,19 +215,20 @@ public class Scanner { const int noSym = 104;
-[ContractInvariantMethod]
-void objectInvariant(){
- Contract.Invariant(buffer!=null);
- Contract.Invariant(t != null);
- Contract.Invariant(start != null);
- Contract.Invariant(tokens != null);
- Contract.Invariant(pt != null);
- Contract.Invariant(tval != null);
- Contract.Invariant(Filename != null);
- Contract.Invariant(errorHandler != null);
-}
+ [ContractInvariantMethod]
+ void objectInvariant(){
+ Contract.Invariant(buffer!=null);
+ Contract.Invariant(t != null);
+ Contract.Invariant(start != null);
+ Contract.Invariant(tokens != null);
+ Contract.Invariant(pt != null);
+ Contract.Invariant(tval != null);
+ Contract.Invariant(Filename != null);
+ Contract.Invariant(errorHandler != null);
+ }
+
public Buffer/*!*/ buffer; // scanner buffer
-
+
Token/*!*/ t; // current token
int ch; // current input character
int pos; // byte position of current character
@@ -236,13 +239,13 @@ void objectInvariant(){ Token/*!*/ tokens; // list of tokens already peeked (first token is a dummy)
Token/*!*/ pt; // current peek token
-
+
char[]/*!*/ tval = new char[128]; // text of current token
int tlen; // length of current token
-
+
private string/*!*/ Filename;
private Errors/*!*/ errorHandler;
-
+
static Scanner() {
start = new Hashtable(128);
for (int i = 39; i <= 39; ++i) start[i] = 1;
@@ -290,9 +293,9 @@ void objectInvariant(){ start[Buffer.EOF] = -1;
}
-
- [NotDelayed]
- public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) :base(){
+
+// [NotDelayed]
+ public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) : base() {
Contract.Requires(fileName != null);
Contract.Requires(errorHandler != null);
this.errorHandler = errorHandler;
@@ -302,15 +305,14 @@ void objectInvariant(){ Stream stream = new FileStream(fileName, FileMode.Open, FileAccess.Read, FileShare.Read);
buffer = new Buffer(stream, false);
Filename = fileName;
-
Init();
} catch (IOException) {
throw new FatalError("Cannot open file " + fileName);
}
}
-
- [NotDelayed]
- public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) :base(){
+
+// [NotDelayed]
+ public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) : base() {
Contract.Requires(s != null);
Contract.Requires(errorHandler != null);
Contract.Requires(fileName != null);
@@ -319,10 +321,9 @@ void objectInvariant(){ buffer = new Buffer(s, true);
this.errorHandler = errorHandler;
this.Filename = fileName;
-
Init();
}
-
+
void Init() {
pos = -1; line = 1; col = 0;
oldEols = 0;
@@ -343,11 +344,11 @@ void objectInvariant(){ Contract.Ensures(Contract.Result<string>() != null);
int p = buffer.Pos;
int ch = buffer.Read();
- // replace isolated '\r' by '\n' in order to make
+ // replace isolated '\r' by '\n' in order to make
// eol handling uniform across Windows, Unix and Mac
if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;
while (ch != EOL && ch != Buffer.EOF){
- ch = buffer.Read();
+ ch = buffer.Read();
// replace isolated '\r' by '\n' in order to make
// eol handling uniform across Windows, Unix and Mac
if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;
@@ -358,7 +359,7 @@ void objectInvariant(){ }
void NextCh() {
- if (oldEols > 0) { ch = EOL; oldEols--; }
+ if (oldEols > 0) { ch = EOL; oldEols--; }
else {
// pos = buffer.Pos;
// ch = buffer.Read(); col++;
@@ -366,9 +367,9 @@ void objectInvariant(){ // // eol handling uniform across Windows, Unix and Mac
// if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;
// if (ch == EOL) { line++; col = 0; }
-
+
while (true) {
- pos = buffer.Pos;
+ pos = buffer.Pos;
ch = buffer.Read(); col++;
// replace isolated '\r' by '\n' in order to make
// eol handling uniform across Windows, Unix and Mac
@@ -418,7 +419,7 @@ void objectInvariant(){ return;
}
-
+
}
}
@@ -555,10 +556,13 @@ void objectInvariant(){ t.pos = pos; t.col = col; t.line = line;
t.filename = this.Filename;
int state;
- if (start.ContainsKey(ch)) { state = (int) cce.NonNull( start[ch]); }
+ if (start.ContainsKey(ch)) {
+ Contract.Assert(start[ch] != null);
+ state = (int) start[ch];
+ }
else { state = 0; }
tlen = 0; AddCh();
-
+
switch (state) {
case -1: { t.kind = eofSym; break; } // NextCh already done
case 0: {
@@ -764,14 +768,14 @@ void objectInvariant(){ t.val = new String(tval, 0, tlen);
return t;
}
-
+
private void SetScannerBehindT() {
buffer.Pos = t.pos;
NextCh();
line = t.line; col = t.col;
for (int i = 0; i < tlen; i++) NextCh();
}
-
+
// get the next token (possibly a token already seen during peeking)
public Token/*!*/ Scan () {
Contract.Ensures(Contract.Result<Token>() != null);
@@ -792,7 +796,7 @@ void objectInvariant(){ }
pt = pt.next;
} while (pt.kind > maxT); // skip pragmas
-
+
return pt;
}
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 07e328a0..b2c46c8a 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -1003,7 +1003,7 @@ namespace Microsoft.Dafny { // play havoc with the heap according to the modifies clause
builder.Add(new Bpl.HavocCmd(m.tok, new Bpl.IdentifierExprSeq((Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr)));
// assume the usual two-state boilerplate information
- foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(m.tok, currentMethod, etran.Old, etran)) {
+ foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(m.tok, currentMethod.Mod, etran.Old, etran, etran.Old)) {
if (tri.IsFree) {
builder.Add(new Bpl.AssumeCmd(m.tok, tri.Expr));
}
@@ -1049,7 +1049,7 @@ namespace Microsoft.Dafny { Contract.Requires(predef != null);
// set up the information used to verify the method's modifies clause
- DefineFrame(m.tok, m.Mod, builder, localVariables);
+ DefineFrame(m.tok, m.Mod, builder, localVariables, null);
}
Bpl.Cmd CaptureState(IToken tok, string/*?*/ additionalInfo) {
@@ -1065,7 +1065,7 @@ namespace Microsoft.Dafny { return CaptureState(tok, null);
}
- void DefineFrame(IToken/*!*/ tok, List<FrameExpression/*!*/>/*!*/ frameClause, Bpl.StmtListBuilder/*!*/ builder, Bpl.VariableSeq/*!*/ localVariables){
+ void DefineFrame(IToken/*!*/ tok, List<FrameExpression/*!*/>/*!*/ frameClause, Bpl.StmtListBuilder/*!*/ builder, Bpl.VariableSeq/*!*/ localVariables, string name){
Contract.Requires(tok != null);
Contract.Requires(cce.NonNullElements(frameClause));
Contract.Requires(builder != null);
@@ -1074,9 +1074,9 @@ namespace Microsoft.Dafny { ExpressionTranslator etran = new ExpressionTranslator(this, predef, tok);
// Declare a local variable $_Frame: <alpha>[ref, Field alpha]bool
- Bpl.IdentifierExpr theFrame = etran.TheFrame(tok); // this is a throw-away expression, used only to extract the name and type of the $_Frame variable
+ Bpl.IdentifierExpr theFrame = etran.TheFrame(tok); // this is a throw-away expression, used only to extract the type of the $_Frame variable
Contract.Assert(theFrame.Type != null); // follows from the postcondition of TheFrame
- Bpl.LocalVariable frame = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, theFrame.Name, theFrame.Type));
+ Bpl.LocalVariable frame = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, name ?? theFrame.Name, theFrame.Type));
localVariables.Add(frame);
// $_Frame := (lambda<alpha> $o: ref, $f: Field alpha :: $o != null && $Heap[$o,alloc] ==> ($o,$f) in Modifies/Reads-Clause);
Bpl.TypeVariable alpha = new Bpl.TypeVariable(tok, "alpha");
@@ -1099,14 +1099,14 @@ namespace Microsoft.Dafny { {
Contract.Requires(tok != null);
Contract.Requires(cce.NonNullElements(calleeFrame));
- Contract.Requires(receiverReplacement != null);
- Contract.Requires(cce.NonNullDictionaryAndValues(substMap));
+ Contract.Requires((receiverReplacement == null) == (substMap == null));
+ Contract.Requires(substMap == null || cce.NonNullDictionaryAndValues(substMap));
Contract.Requires(etran != null);
Contract.Requires(builder != null);
Contract.Requires(errorMessage != null);
Contract.Requires(predef != null);
- // emit: assert (forall<alpha> o: ref, f: Field alpha :: o != null && $Heap[o,alloc] && (o,f) in calleeFrame ==> $_Frame[o,f]);
+ // emit: assert (forall<alpha> o: ref, f: Field alpha :: o != null && $Heap[o,alloc] && (o,f) in subFrame ==> $_Frame[o,f]);
Bpl.TypeVariable alpha = new Bpl.TypeVariable(tok, "alpha");
Bpl.BoundVariable oVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$o", predef.RefType));
Bpl.IdentifierExpr o = new Bpl.IdentifierExpr(tok, oVar);
@@ -1230,7 +1230,7 @@ namespace Microsoft.Dafny { Contract.Requires(f != null);
Contract.Requires(etran != null);
Contract.Requires(cce.NonNullElements(rw));
- Contract.Requires(cce.NonNullDictionaryAndValues(substMap));
+ Contract.Requires(substMap == null || cce.NonNullDictionaryAndValues(substMap));
Contract.Requires(predef != null);
Contract.Requires((receiverReplacement == null) == (substMap == null));
Contract.Ensures(Contract.Result<Bpl.Expr>() != null);
@@ -1241,8 +1241,8 @@ namespace Microsoft.Dafny { Bpl.Expr disjunction = null;
foreach (FrameExpression rwComponent in rw) {
Expression e = rwComponent.E;
- if (substMap != null) {
- Contract.Assert(receiverReplacement != null);
+ if (receiverReplacement != null) {
+ Contract.Assert(substMap != null);
e = Substitute(e, receiverReplacement, substMap);
}
Bpl.Expr disjunct;
@@ -1355,7 +1355,7 @@ namespace Microsoft.Dafny { }
Bpl.Expr funcAppl = new Bpl.NAryExpr(f.tok, funcID, args);
- DefineFrame(f.tok, f.Reads, bodyCheckBuilder, locals);
+ DefineFrame(f.tok, f.Reads, bodyCheckBuilder, locals, null);
CheckWellformedWithResult(f.Body, new WFOptions(f, null, true), funcAppl, f.ResultType, locals, bodyCheckBuilder, etran);
// check that postconditions hold
@@ -2539,7 +2539,7 @@ namespace Microsoft.Dafny { }
comment = null;
}
- if (!skipEnsures) foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(m.tok, m, etran.Old, etran)) {
+ if (!skipEnsures) foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(m.tok, m.Mod, etran.Old, etran, etran.Old)) {
ens.Add(Ensures(tri.tok, tri.IsFree, tri.Expr, tri.ErrorMessage, tri.Comment));
}
}
@@ -2766,15 +2766,15 @@ namespace Microsoft.Dafny { /// <summary>
/// There are 3 states of interest when generating two-state boilerplate:
- /// S0. the beginning of the method, which is where the modifies clause is interpreted
+ /// S0. the beginning of the method or loop, which is where the modifies clause is interpreted
/// S1. the pre-state of the two-state interval
/// S2. the post-state of the two-state interval
- /// This method assumes that etranPre denotes S1, etran denotes S2, and that etran.Old denotes S0.
+ /// This method assumes that etranPre denotes S1, etran denotes S2, and that etranMod denotes S0.
/// </summary>
- List<BoilerplateTriple/*!*/>/*!*/ GetTwoStateBoilerplate(IToken/*!*/ tok, Method/*!*/ method, ExpressionTranslator/*!*/ etranPre, ExpressionTranslator/*!*/ etran)
+ List<BoilerplateTriple/*!*/>/*!*/ GetTwoStateBoilerplate(IToken/*!*/ tok, List<FrameExpression/*!*/>/*!*/ modifiesClause, ExpressionTranslator/*!*/ etranPre, ExpressionTranslator/*!*/ etran, ExpressionTranslator/*!*/ etranMod)
{
Contract.Requires(tok != null);
- Contract.Requires(method != null);
+ Contract.Requires(modifiesClause != null);
Contract.Requires(etranPre != null);
Contract.Requires(etran != null);
Contract.Ensures(cce.NonNullElements(Contract.Result<List<BoilerplateTriple>>()));
@@ -2782,7 +2782,7 @@ namespace Microsoft.Dafny { List<BoilerplateTriple> boilerplate = new List<BoilerplateTriple>();
// the frame condition, which is free since it is checked with every heap update and call
- boilerplate.Add(new BoilerplateTriple(tok, true, FrameCondition(tok, method.Mod, etranPre, etran), null, "frame condition"));
+ boilerplate.Add(new BoilerplateTriple(tok, true, FrameCondition(tok, modifiesClause, etranPre, etran, etranMod), null, "frame condition"));
// HeapSucc(S1, S2)
Bpl.Expr heapSucc = FunctionCall(tok, BuiltinFunction.HeapSucc, null, etranPre.HeapExpr, etran.HeapExpr);
@@ -2792,13 +2792,13 @@ namespace Microsoft.Dafny { }
/// <summary>
- /// There are 3 states of interest when generating a freame condition:
- /// S0. the beginning of the method, which is where the modifies clause is interpreted
+ /// There are 3 states of interest when generating a frame condition:
+ /// S0. the beginning of the method/loop, which is where the modifies clause is interpreted
/// S1. the pre-state of the two-state interval
/// S2. the post-state of the two-state interval
- /// This method assumes that etranPre denotes S1, etran denotes S2, and that etran.Old denotes S0.
+ /// This method assumes that etranPre denotes S1, etran denotes S2, and that etranMod denotes S0.
/// </summary>
- Bpl.Expr/*!*/ FrameCondition(IToken/*!*/ tok, List<FrameExpression/*!*/>/*!*/ modifiesClause, ExpressionTranslator/*!*/ etranPre, ExpressionTranslator/*!*/ etran)
+ Bpl.Expr/*!*/ FrameCondition(IToken/*!*/ tok, List<FrameExpression/*!*/>/*!*/ modifiesClause, ExpressionTranslator/*!*/ etranPre, ExpressionTranslator/*!*/ etran, ExpressionTranslator/*!*/ etranMod)
{
Contract.Requires(tok != null);
Contract.Requires(etran != null);
@@ -2820,15 +2820,43 @@ namespace Microsoft.Dafny { Bpl.Expr heapOF = ExpressionTranslator.ReadHeap(tok, etran.HeapExpr, o, f);
Bpl.Expr preHeapOF = ExpressionTranslator.ReadHeap(tok, etranPre.HeapExpr, o, f);
- Bpl.Expr ante = Bpl.Expr.And(Bpl.Expr.Neq(o, predef.Null), etran.Old.IsAlloced(tok, o));
+ Bpl.Expr ante = Bpl.Expr.And(Bpl.Expr.Neq(o, predef.Null), etranMod.IsAlloced(tok, o));
Bpl.Expr consequent = Bpl.Expr.Eq(heapOF, preHeapOF);
- consequent = Bpl.Expr.Or(consequent, InRWClause(tok, o, f, modifiesClause, etran.Old, null, null));
+ consequent = Bpl.Expr.Or(consequent, InRWClause(tok, o, f, modifiesClause, etranMod, null, null));
Bpl.Trigger tr = new Bpl.Trigger(tok, true, new Bpl.ExprSeq(heapOF));
return new Bpl.ForallExpr(tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fVar), null, tr, Bpl.Expr.Imp(ante, consequent));
}
-
+ Bpl.Expr/*!*/ FrameConditionUsingDefinedFrame(IToken/*!*/ tok, ExpressionTranslator/*!*/ etranPre, ExpressionTranslator/*!*/ etran, ExpressionTranslator/*!*/ etranMod)
+ {
+ Contract.Requires(tok != null);
+ Contract.Requires(etran != null);
+ Contract.Requires(etranPre != null);
+ Contract.Requires(predef != null);
+ Contract.Ensures(Contract.Result<Bpl.Expr>() != null);
+
+ // generate:
+ // (forall<alpha> o: ref, f: Field alpha :: { $Heap[o,f] }
+ // o != null && old($Heap)[o,alloc] ==>
+ // $Heap[o,f] == PreHeap[o,f] ||
+ // $_Frame[o,f])
+ Bpl.TypeVariable alpha = new Bpl.TypeVariable(tok, "alpha");
+ Bpl.BoundVariable oVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$o", predef.RefType));
+ Bpl.IdentifierExpr o = new Bpl.IdentifierExpr(tok, oVar);
+ Bpl.BoundVariable fVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$f", predef.FieldName(tok, alpha)));
+ Bpl.IdentifierExpr f = new Bpl.IdentifierExpr(tok, fVar);
+
+ Bpl.Expr heapOF = ExpressionTranslator.ReadHeap(tok, etran.HeapExpr, o, f);
+ Bpl.Expr preHeapOF = ExpressionTranslator.ReadHeap(tok, etranPre.HeapExpr, o, f);
+ Bpl.Expr ante = Bpl.Expr.And(Bpl.Expr.Neq(o, predef.Null), etranPre.IsAlloced(tok, o));
+ Bpl.Expr consequent = Bpl.Expr.Eq(heapOF, preHeapOF);
+
+ consequent = Bpl.Expr.Or(consequent, Bpl.Expr.SelectTok(tok, etranMod.TheFrame(tok), o, f));
+
+ Bpl.Trigger tr = new Bpl.Trigger(tok, true, new Bpl.ExprSeq(heapOF));
+ return new Bpl.ForallExpr(tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fVar), null, tr, Bpl.Expr.Imp(ante, consequent));
+ }
// ----- Type ---------------------------------------------------------------------------------
Bpl.Type TrType(Type type)
@@ -3120,7 +3148,7 @@ namespace Microsoft.Dafny { AddComment(builder, stmt, "while statement");
var s = (WhileStmt)stmt;
TrLoop(s, s.Guard,
- delegate(Bpl.StmtListBuilder bld) { TrStmt(s.Body, bld, locals, etran); },
+ delegate(Bpl.StmtListBuilder bld, ExpressionTranslator e) { TrStmt(s.Body, bld, locals, e); },
builder, locals, etran);
} else if (stmt is AlternativeLoopStmt) {
@@ -3129,7 +3157,7 @@ namespace Microsoft.Dafny { var tru = new LiteralExpr(s.Tok, true);
tru.Type = Type.Bool; // resolve here
TrLoop(s, tru,
- delegate(Bpl.StmtListBuilder bld) { TrAlternatives(s.Alternatives, null, new Bpl.BreakCmd(s.Tok, null), bld, locals, etran); },
+ delegate(Bpl.StmtListBuilder bld, ExpressionTranslator e) { TrAlternatives(s.Alternatives, null, new Bpl.BreakCmd(s.Tok, null), bld, locals, e); },
builder, locals, etran);
} else if (stmt is ForeachStmt) {
@@ -3322,7 +3350,7 @@ namespace Microsoft.Dafny { }
}
- delegate void BodyTranslator(Bpl.StmtListBuilder builder);
+ delegate void BodyTranslator(Bpl.StmtListBuilder builder, ExpressionTranslator etran);
void TrLoop(LoopStmt s, Expression Guard, BodyTranslator bodyTr,
Bpl.StmtListBuilder builder, Bpl.VariableSeq locals, ExpressionTranslator etran) {
@@ -3343,6 +3371,17 @@ namespace Microsoft.Dafny { locals.Add(preLoopHeapVar);
Bpl.IdentifierExpr preLoopHeap = new Bpl.IdentifierExpr(s.Tok, preLoopHeapVar);
ExpressionTranslator etranPreLoop = new ExpressionTranslator(this, predef, preLoopHeap);
+ ExpressionTranslator updatedFrameEtran;
+ string loopFrameName = "#_Frame#" + loopId;
+ if(s.Mod != null)
+ updatedFrameEtran = new ExpressionTranslator(etran, loopFrameName);
+ else
+ updatedFrameEtran = etran;
+
+ if (s.Mod != null) { // check that the modifies is a strict subset
+ CheckFrameSubset(s.Tok, s.Mod, null, null, etran, builder, "loop modifies clause may violate context's modifies clause", null);
+ DefineFrame(s.Tok, s.Mod, builder, locals, loopFrameName);
+ }
builder.Add(Bpl.Cmd.SimpleAssign(s.Tok, preLoopHeap, etran.HeapExpr));
List<Bpl.Expr> initDecr = null;
@@ -3390,14 +3429,19 @@ namespace Microsoft.Dafny { TrStmt_CheckWellformed(e, invDefinednessBuilder, locals, etran, true);
}
// include boilerplate invariants
- foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(s.Tok, currentMethod, etranPreLoop, etran)) {
- if (tri.IsFree) {
- invariants.Add(new Bpl.AssumeCmd(s.Tok, tri.Expr));
- } else {
- Contract.Assert(tri.ErrorMessage != null); // follows from BoilerplateTriple invariant
- invariants.Add(Assert(s.Tok, tri.Expr, tri.ErrorMessage));
- }
+ foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(s.Tok, currentMethod.Mod, etranPreLoop, etran, etran.Old))
+ {
+ if (tri.IsFree) {
+ invariants.Add(new Bpl.AssumeCmd(s.Tok, tri.Expr));
+ }
+ else {
+ Contract.Assert(tri.ErrorMessage != null); // follows from BoilerplateTriple invariant
+ invariants.Add(Assert(s.Tok, tri.Expr, tri.ErrorMessage));
+ }
}
+ // add a free invariant which says that the heap hasn't changed outside of the modifies clause.
+ invariants.Add(new Bpl.AssumeCmd(s.Tok, FrameConditionUsingDefinedFrame(s.Tok, etranPreLoop, etran, updatedFrameEtran)));
+
// include a free invariant that says that all completed iterations so far have only decreased the termination metric
if (initDecr != null) {
List<IToken> toks = new List<IToken>();
@@ -3430,11 +3474,11 @@ namespace Microsoft.Dafny { // termination checking
if (Contract.Exists(theDecreases, e => e is WildcardExpr)) {
// omit termination checking for this loop
- bodyTr(loopBodyBuilder);
+ bodyTr(loopBodyBuilder, updatedFrameEtran);
} else {
List<Bpl.Expr> oldBfs = RecordDecreasesValue(theDecreases, loopBodyBuilder, locals, etran, "$decr" + loopId + "$");
// time for the actual loop body
- bodyTr(loopBodyBuilder);
+ bodyTr(loopBodyBuilder, updatedFrameEtran);
// check definedness of decreases expressions
List<IToken> toks = new List<IToken>();
List<Type> types = new List<Type>();
@@ -3585,8 +3629,8 @@ namespace Microsoft.Dafny { ins.Add(param);
}
- // Check modifies clause
- CheckFrameSubset(tok, method.Mod, receiver, substMap, etran, builder, "call may violate caller's modifies clause", null);
+ // Check modifies clause of a subcall is a subset of the current frame.
+ CheckFrameSubset(tok, method.Mod, receiver, substMap, etran, builder, "call may violate context's modifies clause", null);
// Check termination
ModuleDecl module = cce.NonNull(method.EnclosingClass).Module;
@@ -4133,7 +4177,7 @@ namespace Microsoft.Dafny { "$obj" + i, predef.RefType, builder, locals);
prevObj[i] = obj;
// check that the enclosing modifies clause allows this object to be written: assert $_Frame[obj]);
- builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.TheFrame(tok), obj, GetField(fse)), "assignment may update an object not in the enclosing method's modifies clause"));
+ builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.TheFrame(tok), obj, GetField(fse)), "assignment may update an object not in the enclosing context's modifies clause"));
// check that this LHS is not the same as any previous LHSs
for (int j = 0; j < i; j++) {
@@ -4164,7 +4208,7 @@ namespace Microsoft.Dafny { prevObj[i] = obj;
prevIndex[i] = fieldName;
// 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), obj, fieldName), "assignment may update an array element not in the enclosing method's modifies clause"));
+ builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.TheFrame(tok), obj, fieldName), "assignment may update an array element not in the enclosing context's modifies clause"));
// check that this LHS is not the same as any previous LHSs
for (int j = 0; j < i; j++) {
@@ -4195,7 +4239,7 @@ namespace Microsoft.Dafny { "$index" + i, predef.FieldName(mse.tok, predef.BoxType), builder, locals);
prevObj[i] = obj;
prevIndex[i] = fieldName;
- builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.TheFrame(tok), obj, fieldName), "assignment may update an array element not in the enclosing method's modifies clause"));
+ builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.TheFrame(tok), obj, fieldName), "assignment may update an array element not in the enclosing context's modifies clause"));
// check that this LHS is not the same as any previous LHSs
for (int j = 0; j < i; j++) {
@@ -4376,6 +4420,7 @@ namespace Microsoft.Dafny { public readonly PredefinedDecls predef;
public readonly Translator translator;
public readonly string This;
+ public readonly string modifiesFrame = "$_Frame"; // the name of the context's frame variable.
readonly Function applyLimited_CurrentFunction;
readonly int layerOffset = 0;
public int Statistics_FunctionCount = 0;
@@ -4420,18 +4465,34 @@ namespace Microsoft.Dafny { this.HeapExpr = heap;
this.This = thisVar;
}
-
- ExpressionTranslator(Translator translator, PredefinedDecls predef, Bpl.Expr heap, Function applyLimited_CurrentFunction, int layerOffset) {
- Contract.Requires(translator != null);
- Contract.Requires(predef != null);
- Contract.Requires(heap != null);
- Contract.Requires(applyLimited_CurrentFunction != null);
- this.translator = translator;
- this.predef = predef;
- this.HeapExpr = heap;
- this.applyLimited_CurrentFunction = applyLimited_CurrentFunction;
- this.This = "this";
- this.layerOffset = layerOffset;
+
+ ExpressionTranslator(Translator translator, PredefinedDecls predef, Bpl.Expr heap, Function applyLimited_CurrentFunction, int layerOffset)
+ {
+ Contract.Requires(translator != null);
+ Contract.Requires(predef != null);
+ Contract.Requires(heap != null);
+ Contract.Requires(applyLimited_CurrentFunction != null);
+ this.translator = translator;
+ this.predef = predef;
+ this.HeapExpr = heap;
+ this.applyLimited_CurrentFunction = applyLimited_CurrentFunction;
+ this.This = "this";
+ this.layerOffset = layerOffset;
+ }
+
+ public ExpressionTranslator(ExpressionTranslator etran, string modifiesFrame)
+ {
+ Contract.Requires(etran != null);
+ Contract.Requires(modifiesFrame != null);
+ this.translator = etran.translator;
+ this.HeapExpr = etran.HeapExpr;
+ this.predef = etran.predef;
+ this.This = etran.This;
+ this.applyLimited_CurrentFunction = etran.applyLimited_CurrentFunction;
+ this.layerOffset = etran.layerOffset;
+ this.Statistics_FunctionCount = etran.Statistics_FunctionCount;
+ this.oldEtran = etran.oldEtran;
+ this.modifiesFrame = modifiesFrame;
}
ExpressionTranslator oldEtran;
@@ -4476,7 +4537,7 @@ namespace Microsoft.Dafny { Bpl.TypeVariable alpha = new Bpl.TypeVariable(tok, "beta");
Bpl.Type fieldAlpha = predef.FieldName(tok, alpha);
Bpl.Type ty = new Bpl.MapType(tok, new Bpl.TypeVariableSeq(alpha), new Bpl.TypeSeq(predef.RefType, fieldAlpha), Bpl.Type.Bool);
- return new Bpl.IdentifierExpr(tok, "$_Frame", ty);
+ return new Bpl.IdentifierExpr(tok, this.modifiesFrame ?? "$_Frame", ty);
}
public Bpl.IdentifierExpr Tick() {
@@ -5941,11 +6002,12 @@ namespace Microsoft.Dafny { static Expression Substitute(Expression expr, Expression receiverReplacement, Dictionary<IVariable,Expression/*!*/>/*!*/ substMap) {
Contract.Requires(expr != null);
+ Contract.Requires(receiverReplacement != null);
Contract.Requires(cce.NonNullDictionaryAndValues(substMap));
Contract.Ensures(Contract.Result<Expression>() != null);
Expression newExpr = null; // set to non-null value only if substitution has any effect; if non-null, newExpr will be resolved at end
-
+
if (expr is LiteralExpr || expr is WildcardExpr || expr is BoogieWrapper) {
// nothing to substitute
} else if (expr is ThisExpr) {
@@ -6103,8 +6165,10 @@ namespace Microsoft.Dafny { static List<Expression/*!*/>/*!*/ SubstituteExprList(List<Expression/*!*/>/*!*/ elist,
Expression receiverReplacement, Dictionary<IVariable,Expression/*!*/>/*!*/ substMap) {
Contract.Requires(cce.NonNullElements(elist));
- Contract.Requires(cce.NonNullDictionaryAndValues(substMap));
+ Contract.Requires((receiverReplacement == null) == (substMap == null));
+ Contract.Requires(substMap == null || cce.NonNullDictionaryAndValues(substMap));
Contract.Ensures(cce.NonNullElements(Contract.Result<List<Expression>>()));
+
List<Expression> newElist = null; // initialized lazily
for (int i = 0; i < elist.Count; i++)
{cce.LoopInvariant( newElist == null || newElist.Count == i);
|