diff options
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 76 | ||||
| -rw-r--r-- | Source/Dafny/Translator.ssc | 268 |
2 files changed, 319 insertions, 25 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 7ff940b5..fde82b93 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -176,10 +176,84 @@ type Field alpha; type HeapType = <alpha>[ref,Field alpha]alpha;
function $IsGoodHeap(HeapType) returns (bool);
-var $Heap: HeapType where $IsGoodHeap($Heap);
+var $Heap: HeapType where $IsGoodHeap($Heap) && #cev_var_update(#cev_pc, cev_implicit, #loc.$Heap, $Heap);
+const unique #loc.$Heap: $token;
const unique alloc: Field bool;
function $HeapSucc(HeapType, HeapType) returns (bool);
axiom (forall h: HeapType, k: HeapType :: { $HeapSucc(h,k) }
$HeapSucc(h,k) ==> (forall o: ref :: { k[o,alloc] } h[o,alloc] ==> k[o,alloc]));
+
+// ---------------------------------------------------------------
+
+type $token;
+function $file_name_is(id:int, tok:$token) returns(bool);
+
+
+type cf_event;
+type var_locglob;
+
+const unique conditional_moment : cf_event;
+const unique took_then_branch : cf_event;
+const unique took_else_branch : cf_event;
+
+const unique loop_register : cf_event;
+const unique loop_entered : cf_event;
+const unique loop_exited : cf_event;
+
+const unique cev_local : var_locglob;
+const unique cev_global : var_locglob;
+const unique cev_parameter : var_locglob;
+const unique cev_implicit : var_locglob;
+
+
+function #cev_init(n:int) returns(bool);
+
+function #cev_save_position(n:int) returns($token);
+
+function #cev_var_intro<T,U>(n:int, locorglob:var_locglob, name:$token, val:T, typ: U) returns(bool);
+
+function #cev_var_update<T>(n:int, locorglob:var_locglob, name:$token, val:T) returns(bool);
+
+function #cev_control_flow_event(n:int, tag : cf_event) returns(bool);
+
+function #cev_function_call(n:int) returns(bool);
+
+
+
+var #cev_pc: int;
+
+procedure CevVarIntro<T>(pos: $token, locorglob: var_locglob, name: $token, val: T);
+ modifies #cev_pc;
+ ensures #cev_var_intro(old(#cev_pc), locorglob, name, val, 0);
+ ensures #cev_save_position(old(#cev_pc)) == pos;
+ ensures #cev_pc == old(#cev_pc) + 1;
+
+procedure CevUpdateHere<T>(name: $token, val: T);
+ ensures #cev_var_update(#cev_pc, cev_global/*BOGUS*/, name, val);
+
+procedure CevStep(pos: $token);
+ modifies #cev_pc;
+ ensures #cev_save_position(old(#cev_pc)) == pos;
+ ensures #cev_pc == old(#cev_pc) + 1;
+
+// CevUpdate == CevUpdateHere + CevStep
+procedure CevUpdate<T>(pos: $token, name: $token, val: T);
+ modifies #cev_pc;
+ ensures #cev_var_update(old(#cev_pc), cev_global/*BOGUS*/, name, val);
+ ensures #cev_save_position(old(#cev_pc)) == pos;
+ ensures #cev_pc == old(#cev_pc) + 1;
+
+procedure CevEvent(pos: $token, tag: cf_event);
+ modifies #cev_pc;
+ ensures #cev_control_flow_event(old(#cev_pc), tag);
+ ensures #cev_save_position(old(#cev_pc)) == pos;
+ ensures #cev_pc == old(#cev_pc) + 1;
+
+procedure CevPreLoop(pos: $token) returns (oldPC: int);
+ ensures #cev_control_flow_event(#cev_pc, loop_register);
+ ensures #cev_save_position(#cev_pc) == pos;
+ ensures oldPC == #cev_pc;
+
+// ---------------------------------------------------------------
diff --git a/Source/Dafny/Translator.ssc b/Source/Dafny/Translator.ssc index 0b56372d..e4cc1d24 100644 --- a/Source/Dafny/Translator.ssc +++ b/Source/Dafny/Translator.ssc @@ -14,12 +14,17 @@ using Bpl = Microsoft.Boogie; namespace Microsoft.Dafny {
public class Translator {
+ [NotDelayed]
public Translator() {
Bpl.Program boogieProgram = ReadPrelude();
if (boogieProgram != null) {
sink = boogieProgram;
predef = FindPredefinedDecls(boogieProgram);
}
+ base();
+ if (predef != null) {
+ cevVariables.Add(predef.HeapVarName, predef.CevHeapName);
+ }
}
// translation state
@@ -27,11 +32,54 @@ namespace Microsoft.Dafny { readonly Dictionary<Field!,Bpl.Constant!>! fields = new Dictionary<Field!,Bpl.Constant!>();
readonly Dictionary<Function!,Bpl.Function!>! functions = new Dictionary<Function!,Bpl.Function!>();
readonly Dictionary<Method!,Bpl.Procedure!>! methods = new Dictionary<Method!,Bpl.Procedure!>();
+
+ // Machinery for providing information to the Counterexample Visualizer
+ readonly Dictionary<string!,int>! cevFilenames = new Dictionary<string!,int>();
+ readonly Dictionary<Token!,Bpl.Constant!>! cevLocations = new Dictionary<Token!,Bpl.Constant!>();
+ readonly Dictionary<string!,Bpl.Constant!>! cevVariables = new Dictionary<string!,Bpl.Constant!>();
+ Bpl.Expr! CevLocation(Token! tok)
+ requires predef != null && sink != null;
+ {
+ Bpl.Constant c;
+ if (cevLocations.TryGetValue(tok, out c)) {
+ assert c != null;
+ } else {
+ int fileId;
+ string filename = "#file^" + (tok.filename == null ? ".dfy" : tok.filename);
+ if (!cevFilenames.TryGetValue(filename, out fileId)) {
+ fileId = cevFilenames.Count;
+ cevFilenames.Add(filename, fileId);
+ Bpl.Constant fn = new Bpl.Constant(tok, new Bpl.TypedIdent(tok, filename, predef.CevTokenType), true);
+ sink.TopLevelDeclarations.Add(fn);
+ sink.TopLevelDeclarations.Add(new Bpl.Axiom(tok, FunctionCall(tok, "$file_name_is", Bpl.Type.Bool, Bpl.Expr.Literal(fileId), new Bpl.IdentifierExpr(tok, fn))));
+ }
+ c = new Bpl.Constant(tok, new Bpl.TypedIdent(tok, string.Format("#tok${0}^{1}.{2}", fileId, tok.line, tok.col), predef.CevTokenType), true);
+ cevLocations.Add(tok, c);
+ sink.TopLevelDeclarations.Add(c);
+ }
+ return new Bpl.IdentifierExpr(tok, c);
+ }
+ Bpl.Expr! CevVariable(Bpl.IToken! tok, string! name)
+ requires predef != null && sink != null;
+ {
+ Bpl.Constant c;
+ if (cevVariables.TryGetValue(name, out c)) {
+ assert c != null;
+ } else {
+ c = new Bpl.Constant(tok, new Bpl.TypedIdent(tok, string.Format("#loc.{0}", name), predef.CevTokenType), true);
+ cevVariables.Add(name, c);
+ sink.TopLevelDeclarations.Add(c);
+ }
+ return new Bpl.IdentifierExpr(tok, c);
+ }
readonly Bpl.Program sink;
readonly PredefinedDecls predef;
internal class PredefinedDecls {
public readonly Bpl.Type! RefType;
+ public readonly Bpl.Type! CevTokenType;
+ public readonly Bpl.Type! CevVariableKind;
+ public readonly Bpl.Type! CevEventType;
private readonly Bpl.TypeCtorDecl! seqTypeCtor;
public Bpl.Type! SeqType(Token! tok, Bpl.Type! ty) {
return new Bpl.CtorType(Token.NoToken, seqTypeCtor, new Bpl.TypeSeq(ty));
@@ -41,6 +89,8 @@ namespace Microsoft.Dafny { return new Bpl.CtorType(tok, fieldName, new Bpl.TypeSeq(ty));
}
public readonly Bpl.Type! HeapType;
+ public readonly string! HeapVarName;
+ public readonly Bpl.Constant! CevHeapName;
public readonly Bpl.Type! ClassNameType;
public readonly Bpl.Expr! Null;
private readonly Bpl.Constant! allocField;
@@ -48,13 +98,19 @@ namespace Microsoft.Dafny { return new Bpl.IdentifierExpr(tok, allocField);
}
- public PredefinedDecls(Bpl.TypeCtorDecl! refType, Bpl.TypeCtorDecl! seqTypeCtor, Bpl.TypeCtorDecl! fieldNameType,
- Bpl.GlobalVariable! heap, Bpl.TypeCtorDecl! classNameType, Bpl.Constant! allocField) {
+ public PredefinedDecls(Bpl.TypeCtorDecl! refType, Bpl.TypeCtorDecl! cevTokenType, Bpl.TypeCtorDecl! cevVariableKind, Bpl.TypeCtorDecl! cevEventType,
+ Bpl.TypeCtorDecl! seqTypeCtor, Bpl.TypeCtorDecl! fieldNameType,
+ Bpl.GlobalVariable! heap, Bpl.TypeCtorDecl! classNameType, Bpl.Constant! allocField, Bpl.Constant! cevHeapNameConst) {
Bpl.CtorType refT = new Bpl.CtorType(Token.NoToken, refType, new Bpl.TypeSeq());
this.RefType = refT;
+ this.CevTokenType = new Bpl.CtorType(Token.NoToken, cevTokenType, new Bpl.TypeSeq());
+ this.CevVariableKind = new Bpl.CtorType(Token.NoToken, cevVariableKind, new Bpl.TypeSeq());
+ this.CevEventType = new Bpl.CtorType(Token.NoToken, cevEventType, new Bpl.TypeSeq());
this.seqTypeCtor = seqTypeCtor;
this.fieldName = fieldNameType;
this.HeapType = heap.TypedIdent.Type;
+ this.HeapVarName = heap.Name;
+ this.CevHeapName = cevHeapNameConst;
this.ClassNameType = new Bpl.CtorType(Token.NoToken, classNameType, new Bpl.TypeSeq());
this.allocField = allocField;
this.Null = new Bpl.IdentifierExpr(Token.NoToken, "null", refT);
@@ -68,11 +124,15 @@ namespace Microsoft.Dafny { }
Bpl.TypeCtorDecl refType = null;
+ Bpl.TypeCtorDecl cevTokenType = null;
+ Bpl.TypeCtorDecl cevVariableKind = null;
+ Bpl.TypeCtorDecl cevEventType = null;
Bpl.TypeCtorDecl seqTypeCtor = null;
Bpl.TypeCtorDecl fieldNameType = null;
Bpl.TypeCtorDecl classNameType = null;
Bpl.GlobalVariable heap = null;
Bpl.Constant allocField = null;
+ Bpl.Constant cevHeapNameConst = null;
foreach (Bpl.Declaration d in prog.TopLevelDeclarations) {
if (d is Bpl.TypeCtorDecl) {
Bpl.TypeCtorDecl dt = (Bpl.TypeCtorDecl)d;
@@ -84,11 +144,19 @@ namespace Microsoft.Dafny { classNameType = dt;
} else if (dt.Name == "ref") {
refType = dt;
+ } else if (dt.Name == "$token") {
+ cevTokenType = dt;
+ } else if (dt.Name == "var_locglob") {
+ cevVariableKind = dt;
+ } else if (dt.Name == "cf_event") {
+ cevEventType = dt;
}
} else if (d is Bpl.Constant) {
Bpl.Constant c = (Bpl.Constant)d;
if (c.Name == "alloc") {
allocField = c;
+ } else if (c.Name == "#loc.$Heap") {
+ cevHeapNameConst = c;
}
} else if (d is Bpl.GlobalVariable) {
Bpl.GlobalVariable v = (Bpl.GlobalVariable)d;
@@ -105,12 +173,20 @@ namespace Microsoft.Dafny { Console.WriteLine("Error: Dafny prelude is missing declaration of type ClassName");
} else if (refType == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of type ref");
+ } else if (cevTokenType == null) {
+ Console.WriteLine("Error: Dafny prelude is missing declaration of type $token");
+ } else if (cevVariableKind == null) {
+ Console.WriteLine("Error: Dafny prelude is missing declaration of type var_locglob");
+ } else if (cevEventType == null) {
+ Console.WriteLine("Error: Dafny prelude is missing declaration of type cf_event");
} else if (heap == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of $Heap");
} else if (allocField == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of constant alloc");
+ } else if (cevHeapNameConst == null) {
+ Console.WriteLine("Error: Dafny prelude is missing declaration of constant #loc.$Heap");
} else {
- return new PredefinedDecls(refType, seqTypeCtor, fieldNameType, heap, classNameType, allocField);
+ return new PredefinedDecls(refType, cevTokenType, cevVariableKind, cevEventType, seqTypeCtor, fieldNameType, heap, classNameType, allocField, cevHeapNameConst);
}
return null;
}
@@ -195,7 +271,7 @@ namespace Microsoft.Dafny { // sound after that, then it would also have been sound just before the allocation.
Bpl.VariableSeq formals = new Bpl.VariableSeq();
Bpl.ExprSeq args = new Bpl.ExprSeq();
- Bpl.BoundVariable bv = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$Heap", predef.HeapType));
+ Bpl.BoundVariable bv = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, predef.HeapVarName, predef.HeapType));
formals.Add(bv);
args.Add(new Bpl.IdentifierExpr(f.tok, bv));
Bpl.BoundVariable bvThis = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "this", predef.RefType));
@@ -369,7 +445,29 @@ namespace Microsoft.Dafny { Bpl.VariableSeq localVariables = new Bpl.VariableSeq();
- Bpl.StmtList stmts = TrStmt2StmtList(m.Body, localVariables, new ExpressionTranslator(this, predef, m.tok));
+ Bpl.StmtListBuilder builder = new Bpl.StmtListBuilder();
+ foreach (Bpl.Variable p in proc.InParams) {
+ assert p != null;
+ builder.Add(new Bpl.CallCmd(p.tok, "CevVarIntro",
+ new Bpl.ExprSeq(
+ CevLocation((Dafny.Token)p.tok),
+ new Bpl.IdentifierExpr(p.tok, "cev_parameter", predef.CevVariableKind),
+ CevVariable(p.tok, p.Name),
+ new Bpl.IdentifierExpr(p.tok, p)),
+ new Bpl.IdentifierExprSeq()));
+ }
+ foreach (Bpl.Variable p in proc.OutParams) {
+ assert p != null;
+ builder.Add(new Bpl.CallCmd(p.tok, "CevVarIntro",
+ new Bpl.ExprSeq(
+ CevLocation((Dafny.Token)p.tok),
+ new Bpl.IdentifierExpr(p.tok, "cev_parameter", predef.CevVariableKind),
+ CevVariable(p.tok, p.Name),
+ new Bpl.IdentifierExpr(p.tok, p)),
+ new Bpl.IdentifierExprSeq()));
+ }
+
+ Bpl.StmtList stmts = TrStmt2StmtList(builder, m.Body, localVariables, new ExpressionTranslator(this, predef, m.tok));
Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(m.TypeArgs);
Bpl.Implementation impl = new Bpl.Implementation(m.tok, proc.Name,
typeParams,
@@ -888,6 +986,7 @@ namespace Microsoft.Dafny { Bpl.IdentifierExprSeq mod = new Bpl.IdentifierExprSeq();
Bpl.EnsuresSeq ens = new Bpl.EnsuresSeq();
mod.Add(etran.HeapExpr);
+ mod.Add(Bpl.Expr.Ident("#cev_pc", Bpl.Type.Int));
string comment = "user-defined preconditions";
foreach (MaybeFreeExpression p in m.Req) {
Bpl.RequiresSeq pieces = new Bpl.RequiresSeq();
@@ -915,9 +1014,9 @@ namespace Microsoft.Dafny { }
}
if (pieces.Length == 1) {
- ens.Add(Ensures(p.E.tok, false, etran.TrExpr(p.E), comment, null));
+ ens.Add(Ensures(p.E.tok, false, etran.TrExpr(p.E), null, comment));
} else {
- ens.Add(Ensures(p.E.tok, true, etran.TrExpr(p.E), comment, null));
+ ens.Add(Ensures(p.E.tok, true, etran.TrExpr(p.E), null, comment));
ens.AddRange(pieces);
}
comment = null;
@@ -927,6 +1026,21 @@ namespace Microsoft.Dafny { ens.Add(Ensures(tri.tok, tri.IsFree, tri.Expr, tri.ErrorMessage, tri.Comment));
}
+ // CEV information
+ // free requires #cev_pc == 0;
+ req.Add(Requires(m.tok, true, Bpl.Expr.Eq(Bpl.Expr.Ident("#cev_pc", Bpl.Type.Int), Bpl.Expr.Literal(0)), null, "CEV information"));
+ // free requires #cev_init(0);
+ req.Add(Requires(m.tok, true, FunctionCall(m.tok, BuiltinFunction.CevInit, null, Bpl.Expr.Literal(0)), null, null));
+ // free requires #cev_var_intro(0, cev_implicit, #loc.$Heap, $Heap, 0);
+ req.Add(Requires(m.tok, true, FunctionCall(m.tok, BuiltinFunction.CevVarIntro, null,
+ Bpl.Expr.Literal(0),
+ new Bpl.IdentifierExpr(m.tok, "cev_implicit", predef.CevVariableKind),
+ CevVariable(m.tok, predef.HeapVarName),
+ etran.HeapExpr,
+ Bpl.Expr.Literal(0)), null, null));
+ // free requires #cev_save_position(0) == #tok.Tok;
+ req.Add(Requires(m.tok, true, Bpl.Expr.Eq(FunctionCall(m.tok, BuiltinFunction.CevProgramLocation, null, Bpl.Expr.Literal(0)), CevLocation(m.tok)), null, null));
+
Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(m.TypeArgs);
proc = new Bpl.Procedure(m.tok, m.FullName, typeParams, inParams, outParams, req, mod, ens);
@@ -1076,7 +1190,12 @@ namespace Microsoft.Dafny { Bpl.StmtList! TrStmt2StmtList(Statement! block, Bpl.VariableSeq! locals, ExpressionTranslator! etran)
requires currentMethod != null && predef != null;
{
- Bpl.StmtListBuilder builder = new Bpl.StmtListBuilder();
+ return TrStmt2StmtList(new Bpl.StmtListBuilder(), block, locals, etran);
+ }
+
+ Bpl.StmtList! TrStmt2StmtList(Bpl.StmtListBuilder! builder, Statement! block, Bpl.VariableSeq! locals, ExpressionTranslator! etran)
+ requires currentMethod != null && predef != null;
+ {
TrStmt(block, builder, locals, etran);
return builder.Collect(block.Tok); // TODO: would be nice to have an end-curly location for "block"
}
@@ -1119,11 +1238,27 @@ namespace Microsoft.Dafny { AddComment(builder, stmt, "assignment statement");
AssignStmt s = (AssignStmt)stmt;
TrAssignment(stmt.Tok, s.Lhs, s.Rhs, builder, locals, etran);
+ if (s.Lhs is IdentifierExpr) {
+ Bpl.IdentifierExpr v = etran.TrVar(stmt.Tok, (!)((IdentifierExpr)s.Lhs).Var);
+ builder.Add(new Bpl.CallCmd(stmt.Tok, "CevUpdate",
+ new Bpl.ExprSeq(CevLocation(stmt.Tok), CevVariable(stmt.Tok, v.Name), v),
+ new Bpl.IdentifierExprSeq()));
+ } else {
+ builder.Add(new Bpl.CallCmd(stmt.Tok, "CevUpdate",
+ new Bpl.ExprSeq(CevLocation(stmt.Tok), CevVariable(stmt.Tok, predef.HeapVarName), etran.HeapExpr),
+ new Bpl.IdentifierExprSeq()));
+ }
} else if (stmt is VarDecl) {
AddComment(builder, stmt, "var-declaration statement");
VarDecl s = (VarDecl)stmt;
Bpl.Type varType = TrType(s.Type);
Bpl.Expr wh = GetWhereClause(stmt.Tok, new Bpl.IdentifierExpr(stmt.Tok, s.UniqueName, varType), s.Type, etran);
+ Bpl.Expr cevWh = FunctionCall(stmt.Tok, BuiltinFunction.CevVarUpdate, null,
+ Bpl.Expr.Ident("#cev_pc", Bpl.Type.Int),
+ new Bpl.IdentifierExpr(stmt.Tok, "cev_local", predef.CevVariableKind),
+ CevVariable(stmt.Tok, s.UniqueName),
+ new Bpl.IdentifierExpr(stmt.Tok, s.UniqueName, varType));
+ wh = wh == null ? cevWh : Bpl.Expr.And(wh, cevWh);
Bpl.LocalVariable var = new Bpl.LocalVariable(stmt.Tok, new Bpl.TypedIdent(stmt.Tok, s.UniqueName, varType, wh));
locals.Add(var);
if (s.Rhs != null) {
@@ -1131,6 +1266,13 @@ namespace Microsoft.Dafny { ide.Var = s; ide.Type = s.Type; // ... and resolve it right here
TrAssignment(stmt.Tok, ide, s.Rhs, builder, locals, etran);
}
+ builder.Add(new Bpl.CallCmd(stmt.Tok, "CevVarIntro",
+ new Bpl.ExprSeq(
+ CevLocation(stmt.Tok),
+ new Bpl.IdentifierExpr(stmt.Tok, "cev_local", predef.CevVariableKind),
+ CevVariable(stmt.Tok, var.Name),
+ new Bpl.IdentifierExpr(stmt.Tok, var)),
+ new Bpl.IdentifierExprSeq()));
} else if (stmt is CallStmt) {
AddComment(builder, stmt, "call statement");
@@ -1164,14 +1306,21 @@ namespace Microsoft.Dafny { builder.Add(call);
for (int i = 0; i < s.Lhs.Count; i++) {
Bpl.IdentifierExpr tmpVarIdE = tmpOuts[i];
+ IdentifierExpr e = s.Lhs[i];
+ Bpl.IdentifierExpr lhs = (Bpl.IdentifierExpr)etran.TrExpr(e); // TODO: is this cast always justified?
if (tmpVarIdE != null) {
- IdentifierExpr e = s.Lhs[i];
// e := UnBox(tmpVar);
- Bpl.IdentifierExpr lhs = (Bpl.IdentifierExpr)etran.TrExpr(e); // TODO: is this cast always justified?
Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(stmt.Tok, lhs, FunctionSpecial(stmt.Tok, BuiltinFunction.Unbox, TrType((!)e.Type), tmpVarIdE));
builder.Add(cmd);
}
- }
+ builder.Add(new Bpl.CallCmd(stmt.Tok, "CevUpdateHere",
+ new Bpl.ExprSeq(CevVariable(stmt.Tok, e.Name), lhs),
+ new Bpl.IdentifierExprSeq()));
+ }
+ builder.Add(new Bpl.CallCmd(stmt.Tok, "CevUpdateHere",
+ new Bpl.ExprSeq(CevVariable(stmt.Tok, predef.HeapVarName), etran.HeapExpr),
+ new Bpl.IdentifierExprSeq()));
+ builder.Add(new Bpl.CallCmd(stmt.Tok, "CevStep", new Bpl.ExprSeq(CevLocation(stmt.Tok)), new Bpl.IdentifierExprSeq()));
} else if (stmt is BlockStmt) {
foreach (Statement ss in ((BlockStmt)stmt).Body) {
@@ -1180,12 +1329,29 @@ namespace Microsoft.Dafny { } else if (stmt is IfStmt) {
AddComment(builder, stmt, "if statement");
IfStmt s = (IfStmt)stmt;
+ builder.Add(new Bpl.CallCmd(s.Tok, "CevEvent",
+ new Bpl.ExprSeq(CevLocation(s.Tok), new Bpl.IdentifierExpr(s.Tok, "conditional_moment", predef.CevEventType)),
+ new Bpl.IdentifierExprSeq()));
Bpl.Expr guard = s.Guard == null ? null : etran.TrExpr(s.Guard);
- Bpl.StmtList thn = TrStmt2StmtList(s.Thn, locals, etran);
- Bpl.StmtList els = null;
+ Bpl.StmtListBuilder b = new Bpl.StmtListBuilder();
+ b.Add(new Bpl.CallCmd(s.Thn.Tok, "CevEvent",
+ new Bpl.ExprSeq(CevLocation(s.Thn.Tok), new Bpl.IdentifierExpr(s.Thn.Tok, "took_then_branch", predef.CevEventType)),
+ new Bpl.IdentifierExprSeq()));
+ Bpl.StmtList thn = TrStmt2StmtList(b, s.Thn, locals, etran);
+ Bpl.StmtList els;
Bpl.IfCmd elsIf = null;
- if (s.Els != null) {
- els = TrStmt2StmtList(s.Els, locals, etran);
+ if (s.Els == null) {
+ b = new Bpl.StmtListBuilder();
+ b.Add(new Bpl.CallCmd(s.Tok, "CevEvent",
+ new Bpl.ExprSeq(CevLocation(s.Tok), new Bpl.IdentifierExpr(s.Tok, "took_else_branch", predef.CevEventType)),
+ new Bpl.IdentifierExprSeq()));
+ els = b.Collect(s.Tok);
+ } else {
+ b = new Bpl.StmtListBuilder();
+ b.Add(new Bpl.CallCmd(s.Els.Tok, "CevEvent",
+ new Bpl.ExprSeq(CevLocation(s.Els.Tok), new Bpl.IdentifierExpr(s.Els.Tok, "took_else_branch", predef.CevEventType)),
+ new Bpl.IdentifierExprSeq()));
+ els = TrStmt2StmtList(b, s.Els, locals, etran);
if (els.BigBlocks.Count == 1) {
Bpl.BigBlock bb = els.BigBlocks[0];
if (bb.LabelName == null && bb.simpleCmds.Length == 0 && bb.ec is Bpl.IfCmd) {
@@ -1205,6 +1371,15 @@ namespace Microsoft.Dafny { Bpl.IdentifierExpr preLoopHeap = new Bpl.IdentifierExpr(stmt.Tok, preLoopHeapVar);
ExpressionTranslator etranPreLoop = new ExpressionTranslator(this, predef, preLoopHeap);
builder.Add(Bpl.Cmd.SimpleAssign(stmt.Tok, preLoopHeap, etran.HeapExpr)); // TODO: does this screw up labeled breaks for this loop?
+
+ // CEV information
+ Bpl.LocalVariable preLoopCevPCVar = new Bpl.LocalVariable(stmt.Tok, new Bpl.TypedIdent(stmt.Tok, "$PreLoopCevPC" + loopHeapVarCount, Bpl.Type.Int));
+ locals.Add(preLoopCevPCVar);
+ Bpl.IdentifierExpr preLoopCevPC = new Bpl.IdentifierExpr(stmt.Tok, preLoopCevPCVar);
+ // call preLoopCevPC := CevPreLoop(loc);
+ builder.Add(new Bpl.CallCmd(stmt.Tok, "CevPreLoop",
+ new Bpl.ExprSeq(CevLocation(stmt.Tok)),
+ new Bpl.IdentifierExprSeq(preLoopCevPC))); // TODO: does this screw up labeled breaks for this loop?
Bpl.Expr guard = s.Guard == null ? null : etran.TrExpr(s.Guard);
List<Bpl.PredicateCmd!> invariants = new List<Bpl.PredicateCmd!>();
@@ -1228,13 +1403,25 @@ namespace Microsoft.Dafny { invariants.Add(Assert(stmt.Tok, tri.Expr, tri.ErrorMessage));
}
}
+
+ // CEV information
+ invariants.Add(new Bpl.AssumeCmd(stmt.Tok, Bpl.Expr.Le(preLoopCevPC, Bpl.Expr.Ident("#cev_pc", Bpl.Type.Int))));
+ foreach (Formal p in currentMethod.Outs) {
+ Bpl.Expr wh = FunctionCall(stmt.Tok, BuiltinFunction.CevVarUpdate, null,
+ Bpl.Expr.Ident("#cev_pc", Bpl.Type.Int),
+ new Bpl.IdentifierExpr(stmt.Tok, "cev_parameter", predef.CevVariableKind),
+ CevVariable(stmt.Tok, p.UniqueName),
+ etran.TrVar(stmt.Tok, p));
+ invariants.Add(new Bpl.AssumeCmd(stmt.Tok, wh));
+ }
- Bpl.StmtList body;
+ Bpl.StmtListBuilder loopBodyBuilder = new Bpl.StmtListBuilder();
+ loopBodyBuilder.Add(new Bpl.CallCmd(stmt.Tok, "CevEvent",
+ new Bpl.ExprSeq(CevLocation(stmt.Tok), new Bpl.IdentifierExpr(stmt.Tok, "loop_entered", predef.CevEventType)),
+ new Bpl.IdentifierExprSeq()));
if (s.Decreases.Count == 0) {
- body = TrStmt2StmtList(s.Body, locals, etran);
+ TrStmt(s.Body, loopBodyBuilder, locals, etran);
} else {
- Bpl.StmtListBuilder loopBodyBuilder = new Bpl.StmtListBuilder();
-
List<Bpl.IdentifierExpr!> oldBfs = new List<Bpl.IdentifierExpr!>();
int c = 0;
foreach (Expression e in s.Decreases) {
@@ -1325,11 +1512,13 @@ namespace Microsoft.Dafny { }
assert decrCheck != null; // follows from loop invariant and the fact that s.Decreases.Count != 0
loopBodyBuilder.Add(Assert(stmt.Tok, decrCheck, "decreases expression might not decrease"));
-
- body = loopBodyBuilder.Collect(stmt.Tok);
}
+ Bpl.StmtList body = loopBodyBuilder.Collect(stmt.Tok);
builder.Add(new Bpl.WhileCmd(stmt.Tok, guard, invariants, body));
+ builder.Add(new Bpl.CallCmd(stmt.Tok, "CevEvent",
+ new Bpl.ExprSeq(CevLocation(stmt.Tok), new Bpl.IdentifierExpr(stmt.Tok, "loop_exited", predef.CevEventType)),
+ new Bpl.IdentifierExprSeq()));
loopHeapVarCount++;
} else if (stmt is ForeachStmt) {
@@ -1415,6 +1604,11 @@ namespace Microsoft.Dafny { qq = new Bpl.ForallExpr(stmt.Tok, new Bpl.VariableSeq(oVar), body);
builder.Add(new Bpl.AssumeCmd(stmt.Tok, qq));
+ // CEV information
+ builder.Add(new Bpl.CallCmd(stmt.Tok, "CevUpdate",
+ new Bpl.ExprSeq(CevLocation(stmt.Tok), CevVariable(stmt.Tok, predef.HeapVarName), etran.HeapExpr),
+ new Bpl.IdentifierExprSeq()));
+
} else {
assert false; // unexpected statement
}
@@ -1545,7 +1739,7 @@ namespace Microsoft.Dafny { public ExpressionTranslator(Translator! translator, PredefinedDecls! predef, Token! heapToken) {
this.translator = translator;
this.predef = predef;
- HeapExpr = new Bpl.IdentifierExpr(heapToken, "$Heap", predef.HeapType);
+ HeapExpr = new Bpl.IdentifierExpr(heapToken, predef.HeapVarName, predef.HeapType);
}
public ExpressionTranslator(Translator! translator, PredefinedDecls! predef, Bpl.Expr! heap) {
@@ -1861,7 +2055,7 @@ namespace Microsoft.Dafny { return !(t is BoolType || t is IntType || t is CollectionType);
}
- public Bpl.Expr! TrVar(Token! tok, IVariable! var) {
+ public Bpl.IdentifierExpr! TrVar(Token! tok, IVariable! var) {
return new Bpl.IdentifierExpr(tok, var.UniqueName, translator.TrType(var.Type));
}
@@ -2043,7 +2237,13 @@ namespace Microsoft.Dafny { DynamicType, // allocated type
TypeParams, // type parameters to allocated type
- TypeTuple
+ TypeTuple,
+
+ // CEV
+ CevInit,
+ CevVarIntro,
+ CevVarUpdate,
+ CevProgramLocation
}
Bpl.NAryExpr! FunctionCall(Token! tok, BuiltinFunction f, Bpl.Type typeInstantiation, params Bpl.Expr[]! args)
@@ -2148,14 +2348,34 @@ namespace Microsoft.Dafny { case BuiltinFunction.DynamicType:
assert args.Length == 1;
+ assert typeInstantiation == null;
return FunctionCall(tok, "dtype", predef.ClassNameType, args);
case BuiltinFunction.TypeParams:
assert args.Length == 2;
+ assert typeInstantiation == null;
return FunctionCall(tok, "TypeParams", predef.ClassNameType, args);
case BuiltinFunction.TypeTuple:
assert args.Length == 2;
+ assert typeInstantiation == null;
return FunctionCall(tok, "TypeTuple", predef.ClassNameType, args);
+ case BuiltinFunction.CevInit:
+ assert args.Length == 1;
+ assert typeInstantiation == null;
+ return FunctionCall(tok, "#cev_init", Bpl.Type.Bool, args);
+ case BuiltinFunction.CevVarIntro:
+ assert args.Length == 5;
+ assert typeInstantiation == null;
+ return FunctionCall(tok, "#cev_var_intro", Bpl.Type.Bool, args);
+ case BuiltinFunction.CevVarUpdate:
+ assert args.Length == 4;
+ assert typeInstantiation == null;
+ return FunctionCall(tok, "#cev_var_update", Bpl.Type.Bool, args);
+ case BuiltinFunction.CevProgramLocation:
+ assert args.Length == 1;
+ assert typeInstantiation == null;
+ return FunctionCall(tok, "#cev_save_position", predef.CevTokenType, args);
+
default:
assert false; // unexpected built-in function
}
|