diff options
| -rw-r--r-- | Source/Dafny/Compiler.cs | 8 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 29 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 1 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 64 | ||||
| -rw-r--r-- | Test/dafny0/ControlStructures.dfy.expect | 4 | ||||
| -rw-r--r-- | Test/dafny0/snapshots/runtest.snapshot.expect | 14 |
6 files changed, 63 insertions, 57 deletions
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index 07b6b67d..a69ac677 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -30,10 +30,10 @@ namespace Microsoft.Dafny { class UniqueNameGenerator : IUniqueNameGenerator
{
- int nameCount;
+ int currentId = -1;
public int GenerateId(string name)
{
- return nameCount++;
+ return System.Threading.Interlocked.Increment(ref currentId);
}
}
@@ -1165,7 +1165,7 @@ namespace Microsoft.Dafny { } else if (stmt is BreakStmt) {
var s = (BreakStmt)stmt;
Indent(indent);
- wr.WriteLine("goto after_{0};", s.TargetStmt.Labels.Data.UniqueId);
+ wr.WriteLine("goto after_{0};", s.TargetStmt.Labels.Data.AssignUniqueId("after_", VariableNameGenerator));
} else if (stmt is ProduceStmt) {
var s = (ProduceStmt)stmt;
if (s.hiddenUpdate != null)
@@ -1945,7 +1945,7 @@ namespace Microsoft.Dafny { TrStmt(ss, indent + IndentAmount);
if (ss.Labels != null) {
Indent(indent); // labels are not indented as much as the statements
- wr.WriteLine("after_{0}: ;", ss.Labels.Data.UniqueId);
+ wr.WriteLine("after_{0}: ;", ss.Labels.Data.AssignUniqueId("after_", VariableNameGenerator));
}
}
}
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index e8f10cf0..28f88f57 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -1452,11 +1452,11 @@ namespace Microsoft.Dafny { return Name;
}
- int nameCount;
+ int currentId;
public int GenerateId(string name)
{
- return nameCount++;
+ return System.Threading.Interlocked.Increment(ref currentId);
}
}
@@ -3321,14 +3321,19 @@ namespace Microsoft.Dafny { {
public readonly IToken Tok;
public readonly string Name;
- public readonly int UniqueId;
- static int nodes = 0;
-
+ int uniqueId = -1;
+ public int AssignUniqueId(string prefix, FreshVariableNameGenerator nameGen)
+ {
+ if (uniqueId < 0)
+ {
+ uniqueId = nameGen.FreshVariableCount(prefix);
+ }
+ return uniqueId;
+ }
public Label(IToken tok, string label) {
Contract.Requires(tok != null);
Tok = tok;
Name = label;
- UniqueId = nodes++;
}
}
@@ -6442,11 +6447,15 @@ namespace Microsoft.Dafny { public abstract class QuantifierExpr : ComprehensionExpr, TypeParameter.ParentType {
public List<TypeParameter> TypeArgs;
- private static int quantCount = 0;
- private readonly int quantUnique;
+ private static int currentQuantId = -1;
+ static int FreshQuantId()
+ {
+ return System.Threading.Interlocked.Increment(ref currentQuantId);
+ }
+ private readonly int UniqueId;
public string FullName {
get {
- return "q$" + quantUnique;
+ return "q$" + UniqueId;
}
}
public String Refresh(string prefix, FreshVariableNameGenerator freshVarNameGen) {
@@ -6468,7 +6477,7 @@ namespace Microsoft.Dafny { Contract.Requires(cce.NonNullElements(bvars));
Contract.Requires(term != null);
this.TypeArgs = tvars;
- this.quantUnique = quantCount++;
+ this.UniqueId = FreshQuantId();
}
public abstract Expression LogicalBody();
}
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index eab4fd08..f7cda6d1 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -75,6 +75,7 @@ namespace Microsoft.Dafny ModuleSignature moduleInfo = null;
int tempVarCount = 0;
+ // TODO(wuestholz): Can we get rid of this?
int FreshTempVarCount()
{
return ++tempVarCount;
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index ba5ae281..81e3ecd0 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -15,7 +15,7 @@ using Microsoft.Boogie; namespace Microsoft.Dafny {
- public class FreshVariableNameGenerator
+ public class FreshVariableNameGenerator : IUniqueNameGenerator
{
readonly Dictionary<string, int> PrefixToCount = new Dictionary<string, int>();
@@ -55,6 +55,11 @@ namespace Microsoft.Dafny { PrefixToCount[prefix] = old + 1;
return old;
}
+
+ public int GenerateId(string name)
+ {
+ return FreshVariableCount(name);
+ }
}
public class Translator {
@@ -1701,8 +1706,8 @@ namespace Microsoft.Dafny { Contract.Requires(proc != null);
Contract.Requires(sink != null && predef != null);
Contract.Requires(iter.Body != null);
- Contract.Requires(currentModule == null && codeContext == null && yieldCountVariable == null && loopHeapVarCount == 0 && _tmpIEs.Count == 0);
- Contract.Ensures(currentModule == null && codeContext == null && yieldCountVariable == null && loopHeapVarCount == 0 && _tmpIEs.Count == 0);
+ Contract.Requires(currentModule == null && codeContext == null && yieldCountVariable == null && _tmpIEs.Count == 0);
+ Contract.Ensures(currentModule == null && codeContext == null && yieldCountVariable == null && _tmpIEs.Count == 0);
currentModule = iter.Module;
codeContext = iter;
@@ -1760,7 +1765,6 @@ namespace Microsoft.Dafny { {
currentModule = null;
codeContext = null;
- loopHeapVarCount = 0;
FreshVarNameGenerator.Reset();
_tmpIEs.Clear();
}
@@ -2579,13 +2583,7 @@ namespace Microsoft.Dafny { ICallable codeContext = null; // the method/iterator whose implementation is currently being translated or the function whose specification is being checked for well-formedness
Bpl.LocalVariable yieldCountVariable = null; // non-null when an iterator body is being translated
bool assertAsAssume = false; // generate assume statements instead of assert statements
-
- int loopHeapVarCount = 0;
- int FreshLoopHeadVarCount()
- {
- return loopHeapVarCount++;
- }
-
+
public readonly FreshVariableNameGenerator FreshVarNameGenerator = new FreshVariableNameGenerator();
Dictionary<string, Bpl.IdentifierExpr> _tmpIEs = new Dictionary<string, Bpl.IdentifierExpr>();
@@ -2659,8 +2657,8 @@ namespace Microsoft.Dafny { Contract.Requires(proc != null);
Contract.Requires(sink != null && predef != null);
Contract.Requires(wellformednessProc || m.Body != null);
- Contract.Requires(currentModule == null && codeContext == null && loopHeapVarCount == 0 && _tmpIEs.Count == 0);
- Contract.Ensures(currentModule == null && codeContext == null && loopHeapVarCount == 0 && _tmpIEs.Count == 0);
+ Contract.Requires(currentModule == null && codeContext == null && _tmpIEs.Count == 0);
+ Contract.Ensures(currentModule == null && codeContext == null && _tmpIEs.Count == 0);
currentModule = m.EnclosingClass.Module;
codeContext = m;
@@ -2874,8 +2872,8 @@ namespace Microsoft.Dafny { Contract.Requires(sink != null && predef != null);
Contract.Requires(f.OverriddenFunction != null);
Contract.Requires(f.Formals.Count == f.OverriddenFunction.Formals.Count);
- Contract.Requires(currentModule == null && codeContext == null && loopHeapVarCount == 0 && _tmpIEs.Count == 0);
- Contract.Ensures(currentModule == null && codeContext == null && loopHeapVarCount == 0 && _tmpIEs.Count == 0);
+ Contract.Requires(currentModule == null && codeContext == null && _tmpIEs.Count == 0);
+ Contract.Ensures(currentModule == null && codeContext == null && _tmpIEs.Count == 0);
#region first procedure, no impl yet
//Function nf = new Function(f.tok, "OverrideCheck_" + f.Name, f.IsStatic, f.IsGhost, f.TypeArgs, f.OpenParen, f.Formals, f.ResultType, f.Req, f.Reads, f.Ens, f.Decreases, f.Body, f.Attributes, f.SignatureEllipsis);
@@ -3207,8 +3205,8 @@ namespace Microsoft.Dafny { Contract.Requires(m.Ins.Count == m.OverriddenMethod.Ins.Count);
Contract.Requires(m.Outs.Count == m.OverriddenMethod.Outs.Count);
//Contract.Requires(wellformednessProc || m.Body != null);
- Contract.Requires(currentModule == null && codeContext == null && loopHeapVarCount == 0 && _tmpIEs.Count == 0);
- Contract.Ensures(currentModule == null && codeContext == null && loopHeapVarCount == 0 && _tmpIEs.Count == 0);
+ Contract.Requires(currentModule == null && codeContext == null && _tmpIEs.Count == 0);
+ Contract.Ensures(currentModule == null && codeContext == null && _tmpIEs.Count == 0);
currentModule = m.EnclosingClass.Module;
codeContext = m;
@@ -5387,9 +5385,9 @@ namespace Microsoft.Dafny { var lhs_args = new List<Bpl.Expr>();
var rhs_args = new List<Bpl.Expr>();
- var i = 0;
+ var ng = new FreshVariableNameGenerator();
foreach (var fm in f.Formals) {
- var fe = BplBoundVar("x#" + i++, predef.BoxType, bvars);
+ var fe = BplBoundVar(ng.FreshVariableName("x#"), predef.BoxType, bvars);
lhs_args.Add(fe);
var be = UnboxIfBoxed(fe, fm.Type);
rhs_args.Add(be);
@@ -6841,7 +6839,7 @@ namespace Microsoft.Dafny { } else if (stmt is BreakStmt) {
AddComment(builder, stmt, "break statement");
var s = (BreakStmt)stmt;
- builder.Add(new GotoCmd(s.Tok, new List<String> { "after_" + s.TargetStmt.Labels.Data.UniqueId }));
+ builder.Add(new GotoCmd(s.Tok, new List<String> { "after_" + s.TargetStmt.Labels.Data.AssignUniqueId("after_", FreshVarNameGenerator) }));
} else if (stmt is ReturnStmt) {
var s = (ReturnStmt)stmt;
AddComment(builder, stmt, "return statement");
@@ -7082,9 +7080,9 @@ namespace Microsoft.Dafny { // check that the modifies is a subset
CheckFrameSubset(s.Tok, s.Mod.Expressions, null, null, etran, builder, "modify statement may violate context's modifies clause", null);
// cause the change of the heap according to the given frame
- int modifyId = FreshLoopHeadVarCount();
- string modifyFrameName = "#_Frame#" + modifyId;
- var preModifyHeapVar = new Bpl.LocalVariable(s.Tok, new Bpl.TypedIdent(s.Tok, "$PreModifyHeap" + modifyId, predef.HeapType));
+ var suffix = FreshVarNameGenerator.FreshVariableName("modify#");
+ string modifyFrameName = "$Frame$" + suffix;
+ var preModifyHeapVar = new Bpl.LocalVariable(s.Tok, new Bpl.TypedIdent(s.Tok, "$PreModifyHeap$" + suffix, predef.HeapType));
locals.Add(preModifyHeapVar);
DefineFrame(s.Tok, s.Mod.Expressions, builder, locals, modifyFrameName);
if (s.Body == null) {
@@ -7325,7 +7323,7 @@ namespace Microsoft.Dafny { foreach (Statement ss in stmts) {
TrStmt(ss, builder, locals, etran);
if (ss.Labels != null) {
- builder.AddLabelCmd("after_" + ss.Labels.Data.UniqueId);
+ builder.AddLabelCmd("after_" + ss.Labels.Data.AssignUniqueId("after_", FreshVarNameGenerator));
}
}
}
@@ -8178,16 +8176,16 @@ namespace Microsoft.Dafny { Contract.Requires(locals != null);
Contract.Requires(etran != null);
- int loopId = FreshLoopHeadVarCount();
+ var suffix = FreshVarNameGenerator.FreshVariableName("loop#");
var theDecreases = s.Decreases.Expressions;
- Bpl.LocalVariable preLoopHeapVar = new Bpl.LocalVariable(s.Tok, new Bpl.TypedIdent(s.Tok, "$PreLoopHeap" + loopId, predef.HeapType));
+ Bpl.LocalVariable preLoopHeapVar = new Bpl.LocalVariable(s.Tok, new Bpl.TypedIdent(s.Tok, "$PreLoopHeap$" + suffix, predef.HeapType));
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;
+ string loopFrameName = "$Frame$" + suffix;
if (s.Mod.Expressions != null)
updatedFrameEtran = new ExpressionTranslator(etran, loopFrameName);
else
@@ -8201,11 +8199,11 @@ namespace Microsoft.Dafny { List<Bpl.Expr> initDecr = null;
if (!Contract.Exists(theDecreases, e => e is WildcardExpr)) {
- initDecr = RecordDecreasesValue(theDecreases, builder, locals, etran, "$decr" + loopId + "$init$");
+ initDecr = RecordDecreasesValue(theDecreases, builder, locals, etran, "$decr_init$" + suffix);
}
// the variable w is used to coordinate the definedness checking of the loop invariant
- Bpl.LocalVariable wVar = new Bpl.LocalVariable(s.Tok, new Bpl.TypedIdent(s.Tok, "$w" + loopId, Bpl.Type.Bool));
+ Bpl.LocalVariable wVar = new Bpl.LocalVariable(s.Tok, new Bpl.TypedIdent(s.Tok, "$w$" + suffix, Bpl.Type.Bool));
Bpl.IdentifierExpr w = new Bpl.IdentifierExpr(s.Tok, wVar);
locals.Add(wVar);
// havoc w;
@@ -8293,7 +8291,7 @@ namespace Microsoft.Dafny { // omit termination checking for this loop
bodyTr(loopBodyBuilder, updatedFrameEtran);
} else {
- List<Bpl.Expr> oldBfs = RecordDecreasesValue(theDecreases, loopBodyBuilder, locals, etran, "$decr" + loopId + "$");
+ List<Bpl.Expr> oldBfs = RecordDecreasesValue(theDecreases, loopBodyBuilder, locals, etran, "$decr$" + suffix);
// time for the actual loop body
bodyTr(loopBodyBuilder, updatedFrameEtran);
// check definedness of decreases expressions
@@ -8658,18 +8656,16 @@ namespace Microsoft.Dafny { Contract.Requires(builder != null);
Contract.Requires(decreases != null);
List<Bpl.Expr> oldBfs = new List<Bpl.Expr>();
- int c = 0;
+ var ng = new FreshVariableNameGenerator();
foreach (Expression e in decreases) {
Contract.Assert(e != null);
- Bpl.LocalVariable bfVar = new Bpl.LocalVariable(e.tok, new Bpl.TypedIdent(e.tok, varPrefix + c, TrType(cce.NonNull(e.Type))));
+ Bpl.LocalVariable bfVar = new Bpl.LocalVariable(e.tok, new Bpl.TypedIdent(e.tok, ng.FreshVariableName(varPrefix), TrType(cce.NonNull(e.Type))));
locals.Add(bfVar);
Bpl.IdentifierExpr bf = new Bpl.IdentifierExpr(e.tok, bfVar);
oldBfs.Add(bf);
// record value of each decreases expression at beginning of the loop iteration
Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(e.tok, bf, etran.TrExpr(e));
builder.Add(cmd);
-
- c++;
}
return oldBfs;
}
diff --git a/Test/dafny0/ControlStructures.dfy.expect b/Test/dafny0/ControlStructures.dfy.expect index 633fc692..bc4cb97d 100644 --- a/Test/dafny0/ControlStructures.dfy.expect +++ b/Test/dafny0/ControlStructures.dfy.expect @@ -68,7 +68,7 @@ Execution trace: ControlStructures.dfy(213,9): anon70_Else
ControlStructures.dfy(213,9): anon71_Else
(0,0): anon72_Then
- (0,0): after_4
+ (0,0): after_2
ControlStructures.dfy(224,7): anon74_LoopHead
(0,0): anon74_LoopBody
ControlStructures.dfy(224,7): anon75_Else
@@ -109,7 +109,7 @@ Execution trace: ControlStructures.dfy(213,9): anon70_Else
ControlStructures.dfy(213,9): anon71_Else
(0,0): anon72_Then
- (0,0): after_4
+ (0,0): after_2
ControlStructures.dfy(224,7): anon74_LoopHead
(0,0): anon74_LoopBody
ControlStructures.dfy(224,7): anon75_Else
diff --git a/Test/dafny0/snapshots/runtest.snapshot.expect b/Test/dafny0/snapshots/runtest.snapshot.expect index d61f92ac..59ee1721 100644 --- a/Test/dafny0/snapshots/runtest.snapshot.expect +++ b/Test/dafny0/snapshots/runtest.snapshot.expect @@ -128,27 +128,27 @@ Dafny program verifier finished with 1 verified, 2 errors -------------------- Snapshots5.dfy --------------------
Processing command (at Snapshots5.v0.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
>>> DoNothingToAssert
-Processing command (at Snapshots5.v0.dfy(10,40)) assert (forall b#1: bool :: true ==> b#1 || !b#1) || 0 != 0;
+Processing command (at Snapshots5.v0.dfy(10,40)) assert (forall b#2: bool :: true ==> b#2 || !b#2) || 0 != 0;
>>> DoNothingToAssert
Processing command (at Snapshots5.v0.dfy(12,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
>>> DoNothingToAssert
-Processing command (at Snapshots5.v0.dfy(13,38)) assert (forall b#3: bool :: true ==> b#3 || !b#3) || 3 != 3;
+Processing command (at Snapshots5.v0.dfy(13,38)) assert (forall b#4: bool :: true ==> b#4 || !b#4) || 3 != 3;
>>> DoNothingToAssert
-Processing command (at Snapshots5.v0.dfy(20,40)) assert (forall b#5: bool :: true ==> b#5 || !b#5) || 1 != 1;
+Processing command (at Snapshots5.v0.dfy(20,40)) assert (forall b#6: bool :: true ==> b#6 || !b#6) || 1 != 1;
>>> DoNothingToAssert
Dafny program verifier finished with 3 verified, 0 errors
Processing command (at Snapshots5.v1.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
>>> MarkAsFullyVerified
-Processing command (at Snapshots5.v1.dfy(10,40)) assert (forall b#1: bool :: true ==> b#1 || !b#1) || 0 != 0;
+Processing command (at Snapshots5.v1.dfy(10,40)) assert (forall b#2: bool :: true ==> b#2 || !b#2) || 0 != 0;
>>> MarkAsFullyVerified
Processing command (at Snapshots5.v1.dfy(12,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
>>> MarkAsFullyVerified
-Processing command (at Snapshots5.v1.dfy(13,38)) assert (forall b#3: bool :: true ==> b#3 || !b#3) || 3 != 3;
+Processing command (at Snapshots5.v1.dfy(13,38)) assert (forall b#4: bool :: true ==> b#4 || !b#4) || 3 != 3;
>>> MarkAsFullyVerified
-Processing command (at Snapshots5.v1.dfy(20,40)) assert (exists b#5: bool :: b#5 || !b#5) || 4 != 4;
+Processing command (at Snapshots5.v1.dfy(20,40)) assert (exists b#6: bool :: b#6 || !b#6) || 4 != 4;
>>> DoNothingToAssert
-Processing command (at Snapshots5.v1.dfy(22,38)) assert (exists b#7: bool :: b#7 || !b#7) || 5 != 5;
+Processing command (at Snapshots5.v1.dfy(22,38)) assert (exists b#8: bool :: b#8 || !b#8) || 5 != 5;
>>> DoNothingToAssert
Dafny program verifier finished with 3 verified, 0 errors
|