diff options
Diffstat (limited to 'Source/Dafny/Compiler.cs')
| -rw-r--r-- | Source/Dafny/Compiler.cs | 170 |
1 files changed, 120 insertions, 50 deletions
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index 18721cf3..8715c047 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -25,6 +25,7 @@ namespace Microsoft.Dafny { }
TextWriter wr;
+ Method enclosingMethod; // non-null when a method body is being translated
public int ErrorCount;
void Error(string msg, params object[] args) {
@@ -633,7 +634,17 @@ namespace Microsoft.Dafny { if (m.Body == null) {
Error("Method {0} has no body", m.FullName);
} else {
+ if (m.IsTailRecursive) {
+ Indent(indent); wr.WriteLine("TAIL_CALL_START: ;");
+ if (!m.IsStatic) {
+ Indent(indent); wr.WriteLine("var _this = this;");
+ }
+ }
+ Contract.Assert(enclosingMethod == null);
+ enclosingMethod = m;
TrStmtList(m.Body.Body, indent);
+ Contract.Assert(enclosingMethod == m);
+ enclosingMethod = null;
}
Indent(indent); wr.WriteLine("}");
@@ -1408,66 +1419,125 @@ namespace Microsoft.Dafny { Contract.Requires(s != null);
Contract.Assert(s.Method != null); // follows from the fact that stmt has been successfully resolved
- var lvalues = new List<string>();
- Contract.Assert(s.Lhs.Count == s.Method.Outs.Count);
- for (int i = 0; i < s.Method.Outs.Count; i++) {
- Formal p = s.Method.Outs[i];
- if (!p.IsGhost) {
- lvalues.Add(CreateLvalue(s.Lhs[i], indent));
+ if (s.Method == enclosingMethod && enclosingMethod.IsTailRecursive) {
+ // compile call as tail-recursive
+
+ // assign the actual in-parameters to temporary variables
+ var inTmps = new List<string>();
+ for (int i = 0; i < s.Method.Ins.Count; i++) {
+ Formal p = s.Method.Ins[i];
+ if (!p.IsGhost) {
+ SpillLetVariableDecls(s.Args[i], indent);
+ }
}
- }
- var outTmps = new List<string>();
- for (int i = 0; i < s.Method.Outs.Count; i++) {
- Formal p = s.Method.Outs[i];
- if (!p.IsGhost) {
- string target = "_out" + tmpVarCount;
+ if (receiverReplacement != null) {
+ // TODO: What to do here? When does this happen, what does it mean?
+ } else if (!s.Method.IsStatic) {
+ SpillLetVariableDecls(s.Receiver, indent);
+
+ string inTmp = "_in" + tmpVarCount;
tmpVarCount++;
- outTmps.Add(target);
+ inTmps.Add(inTmp);
Indent(indent);
- wr.WriteLine("{0} {1};", TypeName(s.Lhs[i].Type), target);
+ wr.Write("var {0} = ", inTmp);
+ TrExpr(s.Receiver);
+ wr.WriteLine(";");
}
- }
- Contract.Assert(lvalues.Count == outTmps.Count);
-
- for (int i = 0; i < s.Method.Ins.Count; i++) {
- Formal p = s.Method.Ins[i];
- if (!p.IsGhost) {
- SpillLetVariableDecls(s.Args[i], indent);
+ for (int i = 0; i < s.Method.Ins.Count; i++) {
+ Formal p = s.Method.Ins[i];
+ if (!p.IsGhost) {
+ string inTmp = "_in" + tmpVarCount;
+ tmpVarCount++;
+ inTmps.Add(inTmp);
+ Indent(indent);
+ wr.Write("var {0} = ", inTmp);
+ TrExpr(s.Args[i]);
+ wr.WriteLine(";");
+ }
}
- }
- if (receiverReplacement != null) {
- Indent(indent);
- wr.Write("@" + receiverReplacement);
- } else if (s.Method.IsStatic) {
+ // Now, assign to the formals
+ int n = 0;
+ if (!s.Method.IsStatic) {
+ Indent(indent);
+ wr.WriteLine("_this = {0};", inTmps[n]);
+ n++;
+ }
+ foreach (var p in s.Method.Ins) {
+ if (!p.IsGhost) {
+ Indent(indent);
+ wr.WriteLine("{0} = {1};", p.CompileName, inTmps[n]);
+ n++;
+ }
+ }
+ Contract.Assert(n == inTmps.Count);
+ // finally, the jump back to the head of the method
Indent(indent);
- wr.Write(TypeName(cce.NonNull(s.Receiver.Type)));
+ wr.WriteLine("goto TAIL_CALL_START;");
+
} else {
- SpillLetVariableDecls(s.Receiver, indent);
- Indent(indent);
- TrParenExpr(s.Receiver);
- }
- wr.Write(".@{0}(", s.Method.CompileName);
+ // compile call as a regular call
+
+ var lvalues = new List<string>();
+ Contract.Assert(s.Lhs.Count == s.Method.Outs.Count);
+ for (int i = 0; i < s.Method.Outs.Count; i++) {
+ Formal p = s.Method.Outs[i];
+ if (!p.IsGhost) {
+ lvalues.Add(CreateLvalue(s.Lhs[i], indent));
+ }
+ }
+ var outTmps = new List<string>();
+ for (int i = 0; i < s.Method.Outs.Count; i++) {
+ Formal p = s.Method.Outs[i];
+ if (!p.IsGhost) {
+ string target = "_out" + tmpVarCount;
+ tmpVarCount++;
+ outTmps.Add(target);
+ Indent(indent);
+ wr.WriteLine("{0} {1};", TypeName(s.Lhs[i].Type), target);
+ }
+ }
+ Contract.Assert(lvalues.Count == outTmps.Count);
- string sep = "";
- for (int i = 0; i < s.Method.Ins.Count; i++) {
- Formal p = s.Method.Ins[i];
- if (!p.IsGhost) {
- wr.Write(sep);
- TrExpr(s.Args[i]);
- sep = ", ";
+ for (int i = 0; i < s.Method.Ins.Count; i++) {
+ Formal p = s.Method.Ins[i];
+ if (!p.IsGhost) {
+ SpillLetVariableDecls(s.Args[i], indent);
+ }
}
- }
+ if (receiverReplacement != null) {
+ Indent(indent);
+ wr.Write("@" + receiverReplacement);
+ } else if (s.Method.IsStatic) {
+ Indent(indent);
+ wr.Write(TypeName(cce.NonNull(s.Receiver.Type)));
+ } else {
+ SpillLetVariableDecls(s.Receiver, indent);
+ Indent(indent);
+ TrParenExpr(s.Receiver);
+ }
+ wr.Write(".@{0}(", s.Method.CompileName);
- foreach (var outTmp in outTmps) {
- wr.Write("{0}out {1}", sep, outTmp);
- sep = ", ";
- }
- wr.WriteLine(");");
+ string sep = "";
+ for (int i = 0; i < s.Method.Ins.Count; i++) {
+ Formal p = s.Method.Ins[i];
+ if (!p.IsGhost) {
+ wr.Write(sep);
+ TrExpr(s.Args[i]);
+ sep = ", ";
+ }
+ }
- // assign to the actual LHSs
- for (int j = 0; j < lvalues.Count; j++) {
- Indent(indent);
- wr.WriteLine("{0} = {1};", lvalues[j], outTmps[j]);
+ foreach (var outTmp in outTmps) {
+ wr.Write("{0}out {1}", sep, outTmp);
+ sep = ", ";
+ }
+ wr.WriteLine(");");
+
+ // assign to the actual LHSs
+ for (int j = 0; j < lvalues.Count; j++) {
+ Indent(indent);
+ wr.WriteLine("{0} = {1};", lvalues[j], outTmps[j]);
+ }
}
}
@@ -1651,7 +1721,7 @@ namespace Microsoft.Dafny { }
} else if (expr is ThisExpr) {
- wr.Write("this");
+ wr.Write(enclosingMethod != null && enclosingMethod.IsTailRecursive ? "_this" : "this");
} else if (expr is IdentifierExpr) {
IdentifierExpr e = (IdentifierExpr)expr;
|