//-----------------------------------------------------------------------------
//
// Copyright (C) Microsoft Corporation. All Rights Reserved.
//
//-----------------------------------------------------------------------------
using System;
using System.Collections.Generic;
using System.Numerics;
using System.Diagnostics.Contracts;
using Bpl = Microsoft.Boogie;
using System.Text;
using Microsoft.Boogie;
namespace Microsoft.Dafny {
public class Translator {
[NotDelayed]
public Translator() {
Bpl.Program boogieProgram = ReadPrelude();
if (boogieProgram != null) {
sink = boogieProgram;
predef = FindPredefinedDecls(boogieProgram);
}
}
// translation state
readonly Dictionary/*!*/ classes = new Dictionary();
readonly Dictionary/*!*/ fields = new Dictionary();
readonly Dictionary/*!*/ fieldFunctions = new Dictionary();
[ContractInvariantMethod]
void ObjectInvariant()
{
Contract.Invariant(cce.NonNullDictionaryAndValues(classes));
Contract.Invariant(cce.NonNullDictionaryAndValues(fields));
Contract.Invariant(cce.NonNullDictionaryAndValues(fieldFunctions));
}
readonly Bpl.Program sink;
readonly PredefinedDecls predef;
internal class PredefinedDecls {
public readonly Bpl.Type RefType;
public readonly Bpl.Type BoxType;
public readonly Bpl.Type TickType;
private readonly Bpl.TypeSynonymDecl setTypeCtor;
private readonly Bpl.TypeSynonymDecl multiSetTypeCtor;
public readonly Bpl.Function ArrayLength;
private readonly Bpl.TypeCtorDecl seqTypeCtor;
readonly Bpl.TypeCtorDecl fieldName;
public readonly Bpl.Type HeapType;
public readonly string HeapVarName;
public readonly Bpl.Type ClassNameType;
public readonly Bpl.Type DatatypeType;
public readonly Bpl.Type DtCtorId;
public readonly Bpl.Expr Null;
private readonly Bpl.Constant allocField;
public readonly Bpl.Constant ClassDotArray;
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(RefType != null);
Contract.Invariant(BoxType != null);
Contract.Invariant(TickType != null);
Contract.Invariant(setTypeCtor != null);
Contract.Invariant(multiSetTypeCtor != null);
Contract.Invariant(ArrayLength != null);
Contract.Invariant(seqTypeCtor != null);
Contract.Invariant(fieldName != null);
Contract.Invariant(HeapType != null);
Contract.Invariant(HeapVarName != null);
Contract.Invariant(ClassNameType != null);
Contract.Invariant(DatatypeType != null);
Contract.Invariant(DtCtorId != null);
Contract.Invariant(Null != null);
Contract.Invariant(allocField != null);
Contract.Invariant(ClassDotArray != null);
}
public Bpl.Type SetType(IToken tok, Bpl.Type ty) {
Contract.Requires(tok != null);
Contract.Requires(ty != null);
Contract.Ensures(Contract.Result() != null);
return new Bpl.TypeSynonymAnnotation(Token.NoToken, setTypeCtor, new Bpl.TypeSeq(ty));
}
public Bpl.Type MultiSetType(IToken tok, Bpl.Type ty) {
Contract.Requires(tok != null);
Contract.Requires(ty != null);
Contract.Ensures(Contract.Result() != null);
return new Bpl.TypeSynonymAnnotation(Token.NoToken, multiSetTypeCtor, new Bpl.TypeSeq(ty));
}
public Bpl.Type SeqType(IToken tok, Bpl.Type ty) {
Contract.Requires(tok != null);
Contract.Requires(ty != null);
Contract.Ensures(Contract.Result() != null);
return new Bpl.CtorType(Token.NoToken, seqTypeCtor, new Bpl.TypeSeq(ty));
}
public Bpl.Type FieldName(IToken tok, Bpl.Type ty) {
Contract.Requires(tok != null);
Contract.Requires(ty != null);
Contract.Ensures(Contract.Result() != null);
return new Bpl.CtorType(tok, fieldName, new Bpl.TypeSeq(ty));
}
public Bpl.IdentifierExpr Alloc(IToken tok) {
Contract.Requires(tok != null);
Contract.Ensures(Contract.Result() != null);
return new Bpl.IdentifierExpr(tok, allocField);
}
public PredefinedDecls(Bpl.TypeCtorDecl refType, Bpl.TypeCtorDecl boxType, Bpl.TypeCtorDecl tickType,
Bpl.TypeSynonymDecl setTypeCtor, Bpl.TypeSynonymDecl multiSetTypeCtor, Bpl.Function arrayLength, Bpl.TypeCtorDecl seqTypeCtor, Bpl.TypeCtorDecl fieldNameType,
Bpl.GlobalVariable heap, Bpl.TypeCtorDecl classNameType,
Bpl.TypeCtorDecl datatypeType, Bpl.TypeCtorDecl dtCtorId,
Bpl.Constant allocField, Bpl.Constant classDotArray) {
#region Non-null preconditions on parameters
Contract.Requires(refType != null);
Contract.Requires(boxType != null);
Contract.Requires(tickType != null);
Contract.Requires(setTypeCtor != null);
Contract.Requires(multiSetTypeCtor != null);
Contract.Requires(seqTypeCtor != null);
Contract.Requires(fieldNameType != null);
Contract.Requires(heap != null);
Contract.Requires(classNameType != null);
Contract.Requires(datatypeType != null);
Contract.Requires(dtCtorId != null);
Contract.Requires(allocField != null);
Contract.Requires(classDotArray != null);
#endregion
Bpl.CtorType refT = new Bpl.CtorType(Token.NoToken, refType, new Bpl.TypeSeq());
this.RefType = refT;
this.BoxType = new Bpl.CtorType(Token.NoToken, boxType, new Bpl.TypeSeq());
this.TickType = new Bpl.CtorType(Token.NoToken, tickType, new Bpl.TypeSeq());
this.setTypeCtor = setTypeCtor;
this.multiSetTypeCtor = multiSetTypeCtor;
this.ArrayLength = arrayLength;
this.seqTypeCtor = seqTypeCtor;
this.fieldName = fieldNameType;
this.HeapType = heap.TypedIdent.Type;
this.HeapVarName = heap.Name;
this.ClassNameType = new Bpl.CtorType(Token.NoToken, classNameType, 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;
this.Null = new Bpl.IdentifierExpr(Token.NoToken, "null", refT);
this.ClassDotArray = classDotArray;
}
}
static PredefinedDecls FindPredefinedDecls(Bpl.Program prog) {
Contract.Requires(prog != null);
if (prog.Resolve() != 0) {
Console.WriteLine("Error: resolution errors encountered in Dafny prelude");
return null;
}
Bpl.TypeCtorDecl refType = null;
Bpl.TypeSynonymDecl setTypeCtor = null;
Bpl.TypeSynonymDecl multiSetTypeCtor = null;
Bpl.Function arrayLength = null;
Bpl.TypeCtorDecl seqTypeCtor = null;
Bpl.TypeCtorDecl fieldNameType = null;
Bpl.TypeCtorDecl classNameType = null;
Bpl.TypeCtorDecl datatypeType = null;
Bpl.TypeCtorDecl dtCtorId = null;
Bpl.TypeCtorDecl boxType = null;
Bpl.TypeCtorDecl tickType = null;
Bpl.GlobalVariable heap = null;
Bpl.Constant allocField = null;
Bpl.Constant classDotArray = null;
foreach (var d in prog.TopLevelDeclarations) {
if (d is Bpl.TypeCtorDecl) {
Bpl.TypeCtorDecl dt = (Bpl.TypeCtorDecl)d;
if (dt.Name == "Seq") {
seqTypeCtor = dt;
} else if (dt.Name == "Field") {
fieldNameType = dt;
} else if (dt.Name == "ClassName") {
classNameType = dt;
} else if (dt.Name == "DatatypeType") {
datatypeType = dt;
} else if (dt.Name == "DtCtorId") {
dtCtorId = dt;
} else if (dt.Name == "ref") {
refType = dt;
} else if (dt.Name == "BoxType") {
boxType = dt;
} else if (dt.Name == "TickType") {
tickType = dt;
}
} else if (d is Bpl.TypeSynonymDecl) {
Bpl.TypeSynonymDecl dt = (Bpl.TypeSynonymDecl)d;
if (dt.Name == "Set") {
setTypeCtor = dt;
}
if (dt.Name == "MultiSet") {
multiSetTypeCtor = dt;
}
} else if (d is Bpl.Constant) {
Bpl.Constant c = (Bpl.Constant)d;
if (c.Name == "alloc") {
allocField = c;
} else if (c.Name == "class.array") {
classDotArray = c;
}
} else if (d is Bpl.GlobalVariable) {
Bpl.GlobalVariable v = (Bpl.GlobalVariable)d;
if (v.Name == "$Heap") {
heap = v;
}
} else if (d is Bpl.Function) {
var f = (Bpl.Function)d;
if (f.Name == "array.Length")
arrayLength = f;
}
}
if (seqTypeCtor == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of type Seq");
} else if (setTypeCtor == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of type Set");
} else if (multiSetTypeCtor == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of type MultiSet");
} else if (arrayLength == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of function array.Length");
} else if (fieldNameType == null) {
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 (datatypeType == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of type DatatypeType");
} else if (dtCtorId == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of type DtCtorId");
} else if (refType == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of type ref");
} else if (boxType == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of type BoxType");
} else if (tickType == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of type TickType");
} 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 (classDotArray == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of class.array");
} else {
return new PredefinedDecls(refType, boxType, tickType,
setTypeCtor, multiSetTypeCtor, arrayLength, seqTypeCtor, fieldNameType, heap, classNameType, datatypeType, dtCtorId,
allocField, classDotArray);
}
return null;
}
static Bpl.Program ReadPrelude() {
string preludePath = DafnyOptions.O.DafnyPrelude;
if (preludePath == null)
{
//using (System.IO.Stream stream = cce.NonNull( System.Reflection.Assembly.GetExecutingAssembly().GetManifestResourceStream("DafnyPrelude.bpl")) // Use this once Spec#/VSIP supports designating a non-.resx project item as an embedded resource
string codebase = cce.NonNull(System.IO.Path.GetDirectoryName(cce.NonNull(System.Reflection.Assembly.GetExecutingAssembly().Location)));
preludePath = System.IO.Path.Combine(codebase, "DafnyPrelude.bpl");
}
Bpl.Program prelude;
int errorCount = Bpl.Parser.Parse(preludePath, null, out prelude);
if (prelude == null || errorCount > 0) {
return null;
} else {
return prelude;
}
/*
List defines = new List();
using (System.IO.Stream stream = new System.IO.FileStream(preludePath, System.IO.FileMode.Open, System.IO.FileAccess.Read))
{
BoogiePL.Buffer.Fill(new System.IO.StreamReader(stream), defines);
//BoogiePL.Scanner.Init("");
Bpl.Program prelude;
int errorCount = BoogiePL.Parser.Parse(out prelude);
if (prelude == null || errorCount > 0) {
return null;
} else {
return prelude;
}
}
*/
}
public Bpl.Program Translate(Program program) {
Contract.Requires(program != null);
Contract.Ensures(Contract.Result() != null);
if (sink == null || predef == null) {
// something went wrong during construction, which reads the prelude; an error has
// already been printed, so just return an empty program here (which is non-null)
return new Bpl.Program();
}
foreach (TopLevelDecl d in program.BuiltIns.SystemModule.TopLevelDecls) {
if (d is DatatypeDecl) {
AddDatatype((DatatypeDecl)d);
} else {
AddClassMembers((ClassDecl)d);
}
}
foreach (ModuleDecl m in program.Modules) {
foreach (TopLevelDecl d in m.TopLevelDecls) {
if (d is DatatypeDecl) {
AddDatatype((DatatypeDecl)d);
} else {
AddClassMembers((ClassDecl)d);
}
}
}
return sink;
}
void AddDatatype(DatatypeDecl dt)
{
Contract.Requires(dt != null);
Contract.Requires(sink != null && predef != null);
sink.TopLevelDeclarations.Add(GetClass(dt));
foreach (DatatypeCtor ctor in dt.Ctors) {
// Add: function #dt.ctor(paramTypes) returns (DatatypeType);
Bpl.VariableSeq argTypes = new Bpl.VariableSeq();
foreach (Formal arg in ctor.Formals) {
Bpl.Variable a = new Bpl.Formal(arg.tok, new Bpl.TypedIdent(arg.tok, Bpl.TypedIdent.NoName, TrType(arg.Type)), true);
argTypes.Add(a);
}
Bpl.Variable resType = new Bpl.Formal(ctor.tok, new Bpl.TypedIdent(ctor.tok, Bpl.TypedIdent.NoName, predef.DatatypeType), false);
Bpl.Function fn = new Bpl.Function(ctor.tok, ctor.FullName, argTypes, resType);
sink.TopLevelDeclarations.Add(fn);
// Add: axiom (forall params :: #dt.ctor(params)-has-the-expected-type);
Bpl.VariableSeq bvs;
List args;
CreateBoundVariables(ctor.Formals, out bvs, out args);
Bpl.Expr ct = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);
List tpArgs = new List(); // we use an empty list of type arguments, because we don't want Good_Datatype to produce any DtTypeParams predicates anyway
Bpl.Expr wh = new ExpressionTranslator(this, predef, ctor.tok).Good_Datatype(ctor.tok, ct, dt, tpArgs);
if (bvs.Length != 0) {
wh = new Bpl.ForallExpr(ctor.tok, bvs, wh);
}
sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, wh));
// Add: const unique ##dt.ctor: DtCtorId;
Bpl.Constant cid = new Bpl.Constant(ctor.tok, new Bpl.TypedIdent(ctor.tok, "#" + ctor.FullName, predef.DtCtorId), true);
sink.TopLevelDeclarations.Add(cid);
// Add: axiom (forall params :: DatatypeCtorId(#dt.ctor(params)) == ##dt.ctor);
CreateBoundVariables(ctor.Formals, out bvs, out args);
Bpl.Expr lhs = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);
lhs = FunctionCall(ctor.tok, BuiltinFunction.DatatypeCtorId, null, lhs);
Bpl.Expr q = Bpl.Expr.Eq(lhs, new Bpl.IdentifierExpr(ctor.tok, cid));
if (bvs.Length != 0) {
q = new Bpl.ForallExpr(ctor.tok, bvs, q);
}
sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, q));
// Add: axiom (forall d: DatatypeType :: dt.ctor?(d) ==> (exists params :: d == #dt.ctor(params));
CreateBoundVariables(ctor.Formals, out bvs, out args);
lhs = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);
var dBv = new Bpl.BoundVariable(ctor.tok, new Bpl.TypedIdent(ctor.tok, "d", predef.DatatypeType));
var dId = new Bpl.IdentifierExpr(ctor.tok, dBv.Name, predef.DatatypeType);
q = Bpl.Expr.Eq(dId, lhs);
if (bvs.Length != 0) {
q = new Bpl.ExistsExpr(ctor.tok, bvs, q);
}
q = Bpl.Expr.Imp(FunctionCall(ctor.tok, ctor.QueryField.FullName, Bpl.Type.Bool, dId), q);
q = new Bpl.ForallExpr(ctor.tok, new VariableSeq(dBv), q);
sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, q));
// Add: function dt.ctor?(this: DatatypeType): bool { DatatypeCtorId(this) == ##dt.ctor }
fn = GetReadonlyField(ctor.QueryField);
lhs = FunctionCall(ctor.tok, BuiltinFunction.DatatypeCtorId, null, new Bpl.IdentifierExpr(ctor.tok, fn.InParams[0].Name, predef.DatatypeType));
fn.Body = Bpl.Expr.Eq(lhs, new Bpl.IdentifierExpr(ctor.tok, cid)); // this uses the "cid" defined for the previous axiom
sink.TopLevelDeclarations.Add(fn);
// Add: axiom (forall params, h: HeapType ::
// { DtAlloc(#dt.ctor(params), h) }
// $IsGoodHeap(h) ==>
// (DtAlloc(#dt.ctor(params), h) <==> ...each param has its expected type...));
CreateBoundVariables(ctor.Formals, out bvs, out args);
lhs = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);
Bpl.BoundVariable hVar = new Bpl.BoundVariable(ctor.tok, new Bpl.TypedIdent(ctor.tok, "$h", predef.HeapType));
Bpl.Expr h = new Bpl.IdentifierExpr(ctor.tok, hVar);
bvs.Add(hVar); args.Add(h);
ExpressionTranslator etranH = new ExpressionTranslator(this, predef, h);
Bpl.Expr isGoodHeap = FunctionCall(ctor.tok, BuiltinFunction.IsGoodHeap, null, h);
lhs = FunctionCall(ctor.tok, BuiltinFunction.DtAlloc, null, lhs, h);
Bpl.Expr pt = Bpl.Expr.True;
int i = 0;
foreach (Formal arg in ctor.Formals) {
Bpl.Expr whp = GetWhereClause(arg.tok, args[i], arg.Type, etranH);
if (whp != null) {
pt = BplAnd(pt, whp);
}
i++;
}
Bpl.Trigger tr = new Bpl.Trigger(ctor.tok, true, new ExprSeq(lhs));
q = new Bpl.ForallExpr(ctor.tok, bvs, tr, Bpl.Expr.Imp(isGoodHeap, Bpl.Expr.Iff(lhs, pt)));
sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, q));
// Add injectivity axioms:
i = 0;
foreach (Formal arg in ctor.Formals) {
// function ##dt.ctor#i(DatatypeType) returns (Ti);
var sf = ctor.Destructors[i];
if (sf != null) {
fn = GetReadonlyField(sf);
} else {
Contract.Assert(!arg.HasName);
argTypes = new Bpl.VariableSeq();
argTypes.Add(new Bpl.Formal(ctor.tok, new Bpl.TypedIdent(ctor.tok, Bpl.TypedIdent.NoName, predef.DatatypeType), true));
resType = new Bpl.Formal(arg.tok, new Bpl.TypedIdent(arg.tok, Bpl.TypedIdent.NoName, TrType(arg.Type)), false);
string nm = "#" + ctor.FullName + "#" + i;
fn = new Bpl.Function(ctor.tok, nm, argTypes, resType);
}
sink.TopLevelDeclarations.Add(fn);
// axiom (forall params :: ##dt.ctor#i(#dt.ctor(params)) == params_i);
CreateBoundVariables(ctor.Formals, out bvs, out args);
lhs = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);
lhs = FunctionCall(ctor.tok, fn.Name, TrType(arg.Type), lhs);
q = new Bpl.ForallExpr(ctor.tok, bvs, Bpl.Expr.Eq(lhs, args[i]));
sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, q));
if (arg.Type.IsDatatype || arg.Type.IsTypeParameter) {
// for datatype: axiom (forall params :: DtRank(params_i) < DtRank(#dt.ctor(params)));
// for type-parameter type: axiom (forall params :: DtRank(Unbox(params_i)) < DtRank(#dt.ctor(params)));
CreateBoundVariables(ctor.Formals, out bvs, out args);
lhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null,
arg.Type.IsDatatype ? args[i] : FunctionCall(ctor.tok, BuiltinFunction.Unbox, predef.DatatypeType, args[i]));
Bpl.Expr rhs = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);
rhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, rhs);
q = new Bpl.ForallExpr(ctor.tok, bvs, Bpl.Expr.Lt(lhs, rhs));
sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, q));
} else if (arg.Type is SeqType) {
// axiom (forall params, i: int :: 0 <= i && i < |arg| ==> DtRank(arg[i]) < DtRank(#dt.ctor(params)));
// that is:
// axiom (forall params, i: int :: 0 <= i && i < |arg| ==> DtRank(Unbox(Seq#Index(arg,i))) < DtRank(#dt.ctor(params)));
CreateBoundVariables(ctor.Formals, out bvs, out args);
Bpl.Variable iVar = new Bpl.BoundVariable(arg.tok, new Bpl.TypedIdent(arg.tok, "i", Bpl.Type.Int));
bvs.Add(iVar);
Bpl.IdentifierExpr ie = new Bpl.IdentifierExpr(arg.tok, iVar);
Bpl.Expr ante = Bpl.Expr.And(
Bpl.Expr.Le(Bpl.Expr.Literal(0), ie),
Bpl.Expr.Lt(ie, FunctionCall(arg.tok, BuiltinFunction.SeqLength, null, args[i])));
lhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null,
FunctionCall(arg.tok, BuiltinFunction.Unbox, predef.DatatypeType,
FunctionCall(arg.tok, BuiltinFunction.SeqIndex, predef.DatatypeType, args[i], ie)));
Bpl.Expr rhs = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);
rhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, rhs);
q = new Bpl.ForallExpr(ctor.tok, bvs, Bpl.Expr.Imp(ante, Bpl.Expr.Lt(lhs, rhs)));
sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, q));
} else if (arg.Type is SetType) {
// axiom (forall params, d: Datatype :: arg[d] ==> DtRank(d) < DtRank(#dt.ctor(params)));
// that is:
// axiom (forall params, d: Datatype :: arg[Box(d)] ==> DtRank(d) < DtRank(#dt.ctor(params)));
CreateBoundVariables(ctor.Formals, out bvs, out args);
Bpl.Variable dVar = new Bpl.BoundVariable(arg.tok, new Bpl.TypedIdent(arg.tok, "d", predef.DatatypeType));
bvs.Add(dVar);
Bpl.IdentifierExpr ie = new Bpl.IdentifierExpr(arg.tok, dVar);
Bpl.Expr ante = Bpl.Expr.SelectTok(arg.tok, args[i], FunctionCall(arg.tok, BuiltinFunction.Box, null, ie));
lhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, ie);
Bpl.Expr rhs = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);
rhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, rhs);
q = new Bpl.ForallExpr(ctor.tok, bvs, Bpl.Expr.Imp(ante, Bpl.Expr.Lt(lhs, rhs)));
sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, q));
} else if (arg.Type is MultiSetType) {
// axiom (forall params, d: Datatype :: 0 < arg[d] ==> DtRank(d) < DtRank(#dt.ctor(params)));
// that is:
// axiom (forall params, d: Datatype :: 0 < arg[Box(d)] ==> DtRank(d) < DtRank(#dt.ctor(params)));
CreateBoundVariables(ctor.Formals, out bvs, out args);
Bpl.Variable dVar = new Bpl.BoundVariable(arg.tok, new Bpl.TypedIdent(arg.tok, "d", predef.DatatypeType));
bvs.Add(dVar);
Bpl.IdentifierExpr ie = new Bpl.IdentifierExpr(arg.tok, dVar);
Bpl.Expr ante = Bpl.Expr.Gt(Bpl.Expr.SelectTok(arg.tok, args[i], FunctionCall(arg.tok, BuiltinFunction.Box, null, ie)), Bpl.Expr.Literal(0));
lhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, ie);
Bpl.Expr rhs = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);
rhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, rhs);
q = new Bpl.ForallExpr(ctor.tok, bvs, Bpl.Expr.Imp(ante, Bpl.Expr.Lt(lhs, rhs)));
sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, q));
}
i++;
}
}
// Add:
// function $IsA#Dt(d: DatatypeType): bool {
// Dt.Ctor0?(d) || Dt.Ctor1?(d) || ...
// }
var cases_dBv = new Bpl.Formal(dt.tok, new Bpl.TypedIdent(dt.tok, "d", predef.DatatypeType), true);
var cases_dId = new Bpl.IdentifierExpr(dt.tok, cases_dBv.Name, predef.DatatypeType);
Bpl.Expr cases_body = null;
foreach (DatatypeCtor ctor in dt.Ctors) {
var disj = FunctionCall(ctor.tok, ctor.QueryField.FullName, Bpl.Type.Bool, cases_dId);
cases_body = cases_body == null ? disj : Bpl.Expr.Or(cases_body, disj);
}
var cases_resType = new Bpl.Formal(dt.tok, new Bpl.TypedIdent(dt.tok, Bpl.TypedIdent.NoName, Bpl.Type.Bool), false);
var cases_fn = new Bpl.Function(dt.tok, "$IsA#" + dt.Name, new Bpl.VariableSeq(cases_dBv), cases_resType);
cases_fn.Body = cases_body;
sink.TopLevelDeclarations.Add(cases_fn);
}
void CreateBoundVariables(List/*!*/ formals, out Bpl.VariableSeq/*!*/ bvs, out List/*!*/ args)
{
Contract.Requires(formals != null);
Contract.Ensures(Contract.ValueAtReturn(out bvs).Length == Contract.ValueAtReturn(out args).Count);
Contract.Ensures(Contract.ValueAtReturn(out bvs) != null);
Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out args)));
bvs = new Bpl.VariableSeq();
args = new List();
foreach (Formal arg in formals) {
Contract.Assert(arg != null);
var nm = string.Format("a{0}#{1}", bvs.Length, otherTmpVarCount);
otherTmpVarCount++;
Bpl.Variable bv = new Bpl.BoundVariable(arg.tok, new Bpl.TypedIdent(arg.tok, nm, TrType(arg.Type)));
bvs.Add(bv);
args.Add(new Bpl.IdentifierExpr(arg.tok, bv));
}
}
void AddClassMembers(ClassDecl c)
{
Contract.Requires(sink != null && predef != null);
Contract.Requires(c != null);
if (c.Name == "array") {
classes.Add(c, predef.ClassDotArray);
} else {
sink.TopLevelDeclarations.Add(GetClass(c));
}
foreach (MemberDecl member in c.Members) {
if (member is Field) {
Field f = (Field)member;
if (f.IsMutable) {
Bpl.Constant fc = GetField(f);
sink.TopLevelDeclarations.Add(fc);
} else {
Bpl.Function ff = GetReadonlyField(f);
if (ff != predef.ArrayLength)
sink.TopLevelDeclarations.Add(ff);
}
AddAllocationAxiom(f);
} else if (member is Function) {
Function f = (Function)member;
AddFunction(f);
if (f.IsRecursive && !f.IsUnlimited) {
AddLimitedAxioms(f, 2);
AddLimitedAxioms(f, 1);
}
for (int layerOffset = 0; layerOffset < 2; layerOffset++) {
var body = f.Body == null ? null : f.Body.Resolved;
if (body is MatchExpr) {
AddFunctionAxiomCase(f, (MatchExpr)body, null, layerOffset);
Bpl.Axiom axPost = FunctionAxiom(f, null, f.Ens, null, layerOffset);
sink.TopLevelDeclarations.Add(axPost);
} else {
Bpl.Axiom ax = FunctionAxiom(f, body, f.Ens, null, layerOffset);
sink.TopLevelDeclarations.Add(ax);
}
if (!f.IsRecursive || f.IsUnlimited) { break; }
}
AddFrameAxiom(f);
AddWellformednessCheck(f);
} else if (member is Method) {
Method m = (Method)member;
// wellformedness check for method specification
Bpl.Procedure proc = AddMethod(m, true, false);
sink.TopLevelDeclarations.Add(proc);
AddMethodImpl(m, proc, true);
// the method itself
proc = AddMethod(m, false, false);
sink.TopLevelDeclarations.Add(proc);
if (m.Body != null) {
// ...and its implementation
AddMethodImpl(m, proc, false);
}
// refinement condition
if (member is MethodRefinement) {
AddMethodRefinement((MethodRefinement)member);
}
} else if (member is CouplingInvariant) {
// TODO: define a well-foundedness condition to check
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected member
}
}
}
void AddFunctionAxiomCase(Function f, MatchExpr me, Specialization prev, int layerOffset) {
Contract.Requires(f != null);
Contract.Requires(me != null);
Contract.Requires(layerOffset == 0 || layerOffset == 1);
IVariable formal = ((IdentifierExpr)me.Source.Resolved).Var; // correctness of casts follows from what resolution checks
foreach (MatchCaseExpr mc in me.Cases) {
Contract.Assert(mc.Ctor != null); // the field is filled in by resolution
Specialization s = new Specialization(formal, mc, prev);
var body = mc.Body.Resolved;
if (body is MatchExpr) {
AddFunctionAxiomCase(f, (MatchExpr)body, s, layerOffset);
} else {
Bpl.Axiom ax = FunctionAxiom(f, body, new List(), s, layerOffset);
sink.TopLevelDeclarations.Add(ax);
}
}
}
class Specialization
{
public readonly List Formals;
public readonly List ReplacementExprs;
public readonly List ReplacementFormals;
public readonly Dictionary SubstMap;
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(cce.NonNullElements(Formals));
Contract.Invariant(cce.NonNullElements(ReplacementExprs));
Contract.Invariant(Formals.Count == ReplacementExprs.Count);
Contract.Invariant(cce.NonNullElements(ReplacementFormals));
Contract.Invariant(SubstMap != null);
}
public Specialization(IVariable formal, MatchCase mc, Specialization prev) {
Contract.Requires(formal is Formal || formal is BoundVar);
Contract.Requires(mc != null);
Contract.Requires(prev == null || formal is BoundVar || !prev.Formals.Contains((Formal)formal));
List rArgs = new List();
foreach (BoundVar p in mc.Arguments) {
IdentifierExpr ie = new IdentifierExpr(p.tok, p.UniqueName);
ie.Var = p; ie.Type = ie.Var.Type; // resolve it here
rArgs.Add(ie);
}
// create and resolve datatype value
var r = new DatatypeValue(mc.tok, mc.Ctor.EnclosingDatatype.Name, mc.Ctor.Name, rArgs);
r.Ctor = mc.Ctor;
r.Type = new UserDefinedType(mc.tok, mc.Ctor.EnclosingDatatype.Name, new List()/*this is not right, but it seems like it won't matter here*/);
Dictionary substMap = new Dictionary();
substMap.Add(formal, r);
// Fill in the fields
Formals = new List();
ReplacementExprs = new List();
ReplacementFormals = new List();
SubstMap = new Dictionary();
if (prev != null) {
Formals.AddRange(prev.Formals);
foreach (var e in prev.ReplacementExprs) {
ReplacementExprs.Add(Substitute(e, null, substMap));
}
foreach (var rf in prev.ReplacementFormals) {
if (rf != formal) {
ReplacementFormals.Add(rf);
}
}
foreach (var entry in prev.SubstMap) {
SubstMap.Add(entry.Key, Substitute(entry.Value, null, substMap));
}
}
if (formal is Formal) {
Formals.Add((Formal)formal);
ReplacementExprs.Add(r);
}
ReplacementFormals.AddRange(mc.Arguments);
SubstMap.Add(formal, r);
}
}
Bpl.Axiom/*!*/ FunctionAxiom(Function/*!*/ f, Expression body, List/*!*/ ens, Specialization specialization, int layerOffset) {
Contract.Requires(f != null);
Contract.Requires(ens != null);
Contract.Requires(layerOffset == 0 || (layerOffset == 1 && f.IsRecursive && !f.IsUnlimited));
Contract.Requires(predef != null);
Contract.Requires(f.EnclosingClass != null);
ExpressionTranslator etran = new ExpressionTranslator(this, predef, f.tok);
// axiom
// mh < ModuleContextHeight ||
// (mh == ModuleContextHeight && (fh <= FunctionContextHeight || InMethodContext))
// ==>
// (forall $Heap, formals ::
// { f(args) }
// f#canCall(args) ||
// ( (mh != ModuleContextHeight || fh != FunctionContextHeight || InMethodContext) &&
// $IsHeap($Heap) && this != null && formals-have-the-expected-types &&
// Pre($Heap,args))
// ==>
// body-can-make-its-calls && // generated only for layerOffset==0
// f(args) == body &&
// ens && // generated only for layerOffset==0
// f(args)-has-the-expected-type); // generated only for layerOffset==0
//
// The variables "formals" are the formals of function "f"; except, if a specialization is provided, then
// "specialization.Formals" (which are expected to be among the formals of "f") are excluded and replaced by
// "specialization.ReplacementFormals".
// The list "args" is the list of formals of function "f"; except, if a specialization is provided, then
// each of the "specialization.Formals" is replaced by the corresponding expression in "specialization.ReplacementExprs".
// If a specialization is provided, occurrences of "specialization.Formals" in "body", "f.Req", and "f.Ens"
// are also replaced by those corresponding expressions.
//
// The translation of "body" uses the #limited form whenever the callee is in the same SCC of the call graph.
//
// if layerOffset==1, then the names f#2 and f are used instead of f and f#limited.
//
// Note, an antecedent $Heap[this,alloc] is intentionally left out: including it would only weaken
// the axiom. Moreover, leaving it out does not introduce any soundness problem, because the Dafny
// allocation statement changes only an allocation bit and then re-assumes $IsGoodHeap; so if it is
// 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, predef.HeapVarName, predef.HeapType));
formals.Add(bv);
args.Add(new Bpl.IdentifierExpr(f.tok, bv));
// ante: $IsHeap($Heap) && this != null && formals-have-the-expected-types &&
Bpl.Expr ante = FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, etran.HeapExpr);
Bpl.BoundVariable bvThis;
Bpl.Expr bvThisIdExpr;
if (f.IsStatic) {
bvThis = null;
bvThisIdExpr = null;
} else {
bvThis = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, etran.This, predef.RefType));
formals.Add(bvThis);
bvThisIdExpr = new Bpl.IdentifierExpr(f.tok, bvThis);
args.Add(bvThisIdExpr);
// add well-typedness conjunct to antecedent
Type thisType = Resolver.GetReceiverType(f.tok, f);
Bpl.Expr wh = Bpl.Expr.And(
Bpl.Expr.Neq(bvThisIdExpr, predef.Null),
etran.GoodRef(f.tok, bvThisIdExpr, thisType));
ante = Bpl.Expr.And(ante, wh);
}
if (specialization != null) {
foreach (BoundVar p in specialization.ReplacementFormals) {
bv = new Bpl.BoundVariable(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, TrType(p.Type)));
formals.Add(bv);
// add well-typedness conjunct to antecedent
Bpl.Expr wh = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, bv), p.Type, etran);
if (wh != null) { ante = Bpl.Expr.And(ante, wh); }
}
}
foreach (Formal p in f.Formals) {
int i = specialization == null ? -1 : specialization.Formals.FindIndex(val => val == p);
if (i == -1) {
bv = new Bpl.BoundVariable(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, TrType(p.Type)));
formals.Add(bv);
Bpl.Expr formal = new Bpl.IdentifierExpr(p.tok, bv);
args.Add(formal);
// add well-typedness conjunct to antecedent
Bpl.Expr wh = GetWhereClause(p.tok, formal, p.Type, etran);
if (wh != null) { ante = Bpl.Expr.And(ante, wh); }
} else {
args.Add(etran.TrExpr(specialization.ReplacementExprs[i]));
// note, well-typedness conjuncts for the replacement formals has already been done above
}
}
// mh < ModuleContextHeight || (mh == ModuleContextHeight && (fh <= FunctionContextHeight || InMethodContext))
ModuleDecl mod = f.EnclosingClass.Module;
Bpl.Expr activate = Bpl.Expr.Or(
Bpl.Expr.Lt(Bpl.Expr.Literal(mod.Height), etran.ModuleContextHeight()),
Bpl.Expr.And(
Bpl.Expr.Eq(Bpl.Expr.Literal(mod.Height), etran.ModuleContextHeight()),
Bpl.Expr.Or(
Bpl.Expr.Le(Bpl.Expr.Literal(mod.CallGraph.GetSCCRepresentativeId(f)), etran.FunctionContextHeight()),
etran.InMethodContext())));
var substMap = new Dictionary();
if (specialization != null) {
substMap = specialization.SubstMap;
}
Bpl.IdentifierExpr funcID = new Bpl.IdentifierExpr(f.tok, FunctionName(f, 1+layerOffset), TrType(f.ResultType));
Bpl.Expr funcAppl = new Bpl.NAryExpr(f.tok, new Bpl.FunctionCall(funcID), args);
Bpl.Expr pre = Bpl.Expr.True;
foreach (Expression req in f.Req) {
pre = BplAnd(pre, etran.TrExpr(Substitute(req, null, substMap)));
}
// useViaContext: (mh != ModuleContextHeight || fh != FunctionContextHeight || InMethodContext)
Bpl.Expr useViaContext =
Bpl.Expr.Or(Bpl.Expr.Or(
Bpl.Expr.Neq(Bpl.Expr.Literal(mod.Height), etran.ModuleContextHeight()),
Bpl.Expr.Neq(Bpl.Expr.Literal(mod.CallGraph.GetSCCRepresentativeId(f)), etran.FunctionContextHeight())),
etran.InMethodContext());
// useViaCanCall: f#canCall(args)
Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(f.tok, f.FullName + "#canCall", Bpl.Type.Bool);
Bpl.Expr useViaCanCall = new Bpl.NAryExpr(f.tok, new Bpl.FunctionCall(canCallFuncID), args);
// ante := useViaCanCall || (useViaContext && typeAnte && pre)
ante = Bpl.Expr.Or(useViaCanCall, BplAnd(useViaContext, BplAnd(ante, pre)));
Bpl.Trigger tr = new Bpl.Trigger(f.tok, true, new Bpl.ExprSeq(funcAppl));
Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(f.TypeArgs);
Bpl.Expr meat;
if (body == null) {
meat = Bpl.Expr.True;
} else {
Expression bodyWithSubst = Substitute(body, null, substMap);
if (layerOffset == 0) {
meat = Bpl.Expr.And(
CanCallAssumption(bodyWithSubst, etran),
Bpl.Expr.Eq(funcAppl, etran.LimitedFunctions(f).TrExpr(bodyWithSubst)));
} else {
meat = Bpl.Expr.Eq(funcAppl, etran.TrExpr(bodyWithSubst));
}
}
if (layerOffset == 0) {
foreach (Expression p in ens) {
Bpl.Expr q = etran.LimitedFunctions(f).TrExpr(Substitute(p, null, substMap));
meat = BplAnd(meat, q);
}
Bpl.Expr whr = GetWhereClause(f.tok, funcAppl, f.ResultType, etran);
if (whr != null) { meat = Bpl.Expr.And(meat, whr); }
}
Bpl.Expr ax = new Bpl.ForallExpr(f.tok, typeParams, formals, null, tr, Bpl.Expr.Imp(ante, meat));
string comment = "definition axiom for " + FunctionName(f, 1+layerOffset);
if (specialization != null) {
string sep = "{0}, specialized for '{1}'";
foreach (var formal in specialization.Formals) {
comment = string.Format(sep, comment, formal.Name);
sep = "{0}, '{1}'";
}
}
return new Bpl.Axiom(f.tok, Bpl.Expr.Imp(activate, ax), comment);
}
void AddLimitedAxioms(Function f, int fromLayer) {
Contract.Requires(f != null);
Contract.Requires(f.IsRecursive && !f.IsUnlimited);
Contract.Requires(fromLayer == 1 || fromLayer == 2);
Contract.Requires(sink != null && predef != null);
// With fromLayer==1, generate:
// axiom (forall formals :: { f(args) } f(args) == f#limited(args))
// With fromLayer==2, generate:
// axiom (forall formals :: { f#2(args) } f#2(args) == f(args))
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, predef.HeapVarName, predef.HeapType));
formals.Add(bv);
args.Add(new Bpl.IdentifierExpr(f.tok, bv));
Bpl.BoundVariable bvThis;
Bpl.Expr bvThisIdExpr;
if (f.IsStatic) {
bvThis = null;
bvThisIdExpr = null;
} else {
bvThis = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "this", predef.RefType));
formals.Add(bvThis);
bvThisIdExpr = new Bpl.IdentifierExpr(f.tok, bvThis);
args.Add(bvThisIdExpr);
}
foreach (Formal p in f.Formals) {
bv = new Bpl.BoundVariable(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, TrType(p.Type)));
formals.Add(bv);
args.Add(new Bpl.IdentifierExpr(p.tok, bv));
}
Bpl.FunctionCall origFuncID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, FunctionName(f, fromLayer), TrType(f.ResultType)));
Bpl.Expr origFuncAppl = new Bpl.NAryExpr(f.tok, origFuncID, args);
Bpl.FunctionCall limitedFuncID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, FunctionName(f, fromLayer-1), TrType(f.ResultType)));
Bpl.Expr limitedFuncAppl = new Bpl.NAryExpr(f.tok, limitedFuncID, args);
Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(f.TypeArgs);
Bpl.Trigger tr = new Bpl.Trigger(f.tok, true, new Bpl.ExprSeq(origFuncAppl));
Bpl.Expr ax = new Bpl.ForallExpr(f.tok, typeParams, formals, null, tr, Bpl.Expr.Eq(origFuncAppl, limitedFuncAppl));
sink.TopLevelDeclarations.Add(new Bpl.Axiom(f.tok, ax));
}
///
/// Returns the appropriate Boogie function for the given function. In particular:
/// Layer 2: f#2 --currently used only for induction axioms
/// Layer 1: f --this is the default name
/// Layer 0: f#limited --does not trigger the function definition axiom
///
public static string FunctionName(Function f, int layer) {
Contract.Requires(f != null);
Contract.Requires(0 <= layer && layer < 3);
Contract.Ensures(Contract.Result() != null);
string name = f.FullName;
switch (layer) {
case 2: name += "#2"; break;
case 0: name += "#limited"; break;
}
return name;
}
///
/// Generate:
/// axiom (forall h: [ref, Field x]x, o: ref ::
/// { h[o,f] }
/// $IsGoodHeap(h) && o != null && h[o,alloc] ==> h[o,f]-has-the-expected-type);
///
void AddAllocationAxiom(Field f)
{
Contract.Requires(f != null);
Contract.Requires(sink != null && predef != null);
Bpl.BoundVariable hVar = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$h", predef.HeapType));
Bpl.Expr h = new Bpl.IdentifierExpr(f.tok, hVar);
ExpressionTranslator etran = new ExpressionTranslator(this, predef, h);
Bpl.BoundVariable oVar = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$o", predef.RefType));
Bpl.Expr o = new Bpl.IdentifierExpr(f.tok, oVar);
// h[o,f]
Bpl.Expr oDotF;
if (f.IsMutable) {
oDotF = ExpressionTranslator.ReadHeap(f.tok, h, o, new Bpl.IdentifierExpr(f.tok, GetField(f)));
} else {
oDotF = new Bpl.NAryExpr(f.tok, new Bpl.FunctionCall(GetReadonlyField(f)), new Bpl.ExprSeq(o));
}
Bpl.Expr wh = GetWhereClause(f.tok, oDotF, f.Type, etran);
if (wh != null) {
// ante: $IsGoodHeap(h) && o != null && h[o,alloc]
Bpl.Expr ante = Bpl.Expr.And(Bpl.Expr.And(
FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, h),
Bpl.Expr.Neq(o, predef.Null)),
etran.IsAlloced(f.tok, o));
Bpl.Expr body = Bpl.Expr.Imp(ante, wh);
Bpl.Trigger tr = new Bpl.Trigger(f.tok, true, new Bpl.ExprSeq(oDotF));
Bpl.Expr ax = new Bpl.ForallExpr(f.tok, new Bpl.VariableSeq(hVar, oVar), tr, body);
sink.TopLevelDeclarations.Add(new Bpl.Axiom(f.tok, ax));
}
}
Bpl.Expr InSeqRange(IToken tok, Bpl.Expr index, Bpl.Expr seq, bool isSequence, Bpl.Expr lowerBound, bool includeUpperBound) {
Contract.Requires(tok != null);
Contract.Requires(index != null);
Contract.Requires(seq != null);
Contract.Ensures(Contract.Result() != null);
if (lowerBound == null) {
lowerBound = Bpl.Expr.Literal(0);
}
Bpl.Expr lower = Bpl.Expr.Le(lowerBound, index);
Bpl.Expr length = isSequence ?
FunctionCall(tok, BuiltinFunction.SeqLength, null, seq) :
ArrayLength(tok, seq, 1, 0);
Bpl.Expr upper;
if (includeUpperBound) {
upper = Bpl.Expr.Le(index, length);
} else {
upper = Bpl.Expr.Lt(index, length);
}
return Bpl.Expr.And(lower, upper);
}
Method currentMethod = null; // the method whose implementation is currently being translated
int loopHeapVarCount = 0;
int otherTmpVarCount = 0;
Dictionary _tmpIEs = new Dictionary();
Bpl.IdentifierExpr GetTmpVar_IdExpr(IToken tok, string name, Bpl.Type ty, Bpl.VariableSeq locals) // local variable that's shared between statements that need it
{
Contract.Requires(tok != null);
Contract.Requires(name != null);
Contract.Requires(ty != null);
Contract.Requires(locals != null);
Contract.Ensures(Contract.Result() != null);
Bpl.IdentifierExpr ie;
if (_tmpIEs.TryGetValue(name, out ie)) {
Contract.Assume(ie.Type.Equals(ty));
} else {
// the "tok" and "ty" of the first request for this variable is the one we use
var v = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, name, ty)); // important for the "$nw" client: no where clause (see GetNewVar_IdExpr)
locals.Add(v);
ie = new Bpl.IdentifierExpr(tok, v);
_tmpIEs.Add(name, ie);
}
return ie;
}
Bpl.IdentifierExpr GetPrevHeapVar_IdExpr(IToken tok, Bpl.VariableSeq locals) { // local variable that's shared between statements that need it
Contract.Requires(tok != null);
Contract.Requires(locals != null); Contract.Requires(predef != null);
Contract.Ensures(Contract.Result() != null);
return GetTmpVar_IdExpr(tok, "$prevHeap", predef.HeapType, locals);
}
Bpl.IdentifierExpr GetNewVar_IdExpr(IToken tok, Bpl.VariableSeq locals) // local variable that's shared between statements that need it
{
Contract.Requires(tok != null);
Contract.Requires(locals != null);
Contract.Requires(predef != null);
Contract.Ensures(Contract.Result() != null);
// important: the following declaration produces no where clause (that's why we're going through the trouble of setting of this variable in the first place)
return GetTmpVar_IdExpr(tok, "$nw", predef.RefType, locals);
}
///
/// Returns an expression whose value is the same as "expr", but that is guaranteed to preserve the its value passed
/// the evaluation of other expressions. If necessary, a new local variable called "name" with type "ty" is added to "locals" and
/// assigned in "builder" to be used to hold the value of "expr". It is assumed that all requests for a given "name"
/// have the same type "ty" and that these variables can be shared.
/// As an optimization, if "otherExprsCanAffectPreviouslyKnownExpressions" is "false", then "expr" itself is returned.
///
Bpl.Expr SaveInTemp(Bpl.Expr expr, bool otherExprsCanAffectPreviouslyKnownExpressions, string name, Bpl.Type ty, Bpl.StmtListBuilder builder, Bpl.VariableSeq locals) {
Contract.Requires(expr != null);
Contract.Requires(name != null);
Contract.Requires(ty != null);
Contract.Requires(locals != null);
Contract.Ensures(Contract.Result() != null);
if (otherExprsCanAffectPreviouslyKnownExpressions) {
var save = GetTmpVar_IdExpr(expr.tok, name, ty, locals);
builder.Add(Bpl.Cmd.SimpleAssign(expr.tok, save, expr));
return save;
} else {
return expr;
}
}
void AddMethodImpl(Method m, Bpl.Procedure proc, bool wellformednessProc)
{
Contract.Requires(m != null);
Contract.Requires(proc != null);
Contract.Requires(sink != null && predef != null);
Contract.Requires(wellformednessProc || m.Body != null);
Contract.Requires(currentMethod == null && loopHeapVarCount == 0 && _tmpIEs.Count == 0);
Contract.Ensures(currentMethod == null && loopHeapVarCount == 0 && _tmpIEs.Count == 0);
currentMethod = m;
Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(m.TypeArgs);
Bpl.VariableSeq inParams = Bpl.Formal.StripWhereClauses(proc.InParams);
Bpl.VariableSeq outParams = Bpl.Formal.StripWhereClauses(proc.OutParams);
Bpl.StmtListBuilder builder = new Bpl.StmtListBuilder();
ExpressionTranslator etran = new ExpressionTranslator(this, predef, m.tok);
Bpl.VariableSeq localVariables = new Bpl.VariableSeq();
GenerateImplPrelude(m, inParams, outParams, builder, localVariables);
Bpl.StmtList stmts;
if (!wellformednessProc) {
if (3 <= DafnyOptions.O.Induction && m.IsGhost && m.Mod.Count == 0 && m.Outs.Count == 0) {
var posts = new List();
m.Ens.ForEach(mfe => posts.Add(mfe.E));
var allIns = new List();
if (!m.IsStatic) {
allIns.Add(new ThisSurrogate(m.tok, Resolver.GetThisType(m.tok, (ClassDecl)m.EnclosingClass)));
}
allIns.AddRange(m.Ins);
var inductionVars = ApplyInduction(allIns, m.Attributes, posts, delegate(System.IO.TextWriter wr) { wr.Write(m.FullName); });
if (inductionVars.Count != 0) {
// Let the parameters be this,x,y of the method M and suppose ApplyInduction returns this,y.
// Also, let Pre be the precondition and VF be the decreases clause.
// Then, insert into the method body what amounts to:
// assume case-analysis-on-parameter[[ y' ]];
// parallel (this', y' | Pre(this', x, y') && VF(this', x, y') << VF(this, x, y)) {
// this'.M(x, y');
// }
// Generate bound variables for the parallel statement, and a substitution for the Pre and VF
// assume case-analysis-on-parameter[[ y' ]];
foreach (var inFormal in m.Ins) {
var dt = inFormal.Type.AsDatatype;
if (dt != null) {
var funcID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(inFormal.tok, "$IsA#" + dt.Name, Bpl.Type.Bool));
var f = new Bpl.IdentifierExpr(inFormal.tok, inFormal.UniqueName, TrType(inFormal.Type));
builder.Add(new Bpl.AssumeCmd(inFormal.tok, new Bpl.NAryExpr(inFormal.tok, funcID, new Bpl.ExprSeq(f))));
}
}
var parBoundVars = new List();
Expression receiverReplacement = null;
var substMap = new Dictionary();
foreach (var iv in inductionVars) {
BoundVar bv;
IdentifierExpr ie;
CloneVariableAsBoundVar(iv.tok, iv, "$ih#" + iv.Name, out bv, out ie);
parBoundVars.Add(bv);
if (iv is ThisSurrogate) {
Contract.Assert(receiverReplacement == null && substMap.Count == 0); // the receiver comes first, if at all
receiverReplacement = ie;
} else {
substMap.Add(iv, ie);
}
}
// Generate a CallStmt for the recursive call
Expression recursiveCallReceiver;
if (receiverReplacement != null) {
recursiveCallReceiver = receiverReplacement;
} else if (m.IsStatic) {
recursiveCallReceiver = new StaticReceiverExpr(m.tok, (ClassDecl)m.EnclosingClass); // this also resolves it
} else {
recursiveCallReceiver = new ImplicitThisExpr(m.tok);
recursiveCallReceiver.Type = Resolver.GetThisType(m.tok, (ClassDecl)m.EnclosingClass); // resolve here
}
var recursiveCallArgs = new List();
foreach (var inFormal in m.Ins) {
Expression inE;
if (substMap.TryGetValue(inFormal, out inE)) {
recursiveCallArgs.Add(inE);
} else {
var ie = new IdentifierExpr(inFormal.tok, inFormal.Name);
ie.Var = inFormal; // resolve here
ie.Type = inFormal.Type; // resolve here
recursiveCallArgs.Add(ie);
}
}
var recursiveCall = new CallStmt(m.tok, new List(), recursiveCallReceiver, m.Name, recursiveCallArgs);
recursiveCall.Method = m; // resolve here
Expression parRange = new LiteralExpr(m.tok, true);
parRange.Type = Type.Bool; // resolve here
if (receiverReplacement != null) {
// add "this' != null" to the range
var nil = new LiteralExpr(receiverReplacement.tok);
nil.Type = receiverReplacement.Type; // resolve here
var neqNull = new BinaryExpr(receiverReplacement.tok, BinaryExpr.Opcode.Neq, receiverReplacement, nil);
neqNull.ResolvedOp = BinaryExpr.ResolvedOpcode.NeqCommon; // resolve here
neqNull.Type = Type.Bool; // resolve here
parRange = DafnyAnd(parRange, neqNull);
}
foreach (var pre in m.Req) {
if (!pre.IsFree) {
parRange = DafnyAnd(parRange, Substitute(pre.E, receiverReplacement, substMap));
}
}
// construct an expression (generator) for: VF' << VF
ExpressionConverter decrCheck = delegate(Dictionary decrSubstMap) {
var decrToks = new List();
var decrTypes = new List();
var decrCallee = new List();
var decrCaller = new List();
bool decrInferred; // we don't actually care
foreach (var ee in MethodDecreasesWithDefault(m, out decrInferred)) {
decrToks.Add(ee.tok);
decrTypes.Add(ee.Type);
decrCaller.Add(etran.TrExpr(ee));
Expression es = Substitute(ee, receiverReplacement, substMap);
es = Substitute(es, null, decrSubstMap);
decrCallee.Add(etran.TrExpr(es));
}
return DecreasesCheck(decrToks, decrTypes, decrCallee, decrCaller, etran, null, null, false, true);
};
#if VERIFY_CORRECTNESS_OF_TRANSLATION_PARALLEL_RANGE
var definedness = new Bpl.StmtListBuilder();
var exporter = new Bpl.StmtListBuilder();
TrParallelCall(m.tok, parBoundVars, parRange, decrCheck, recursiveCall, definedness, exporter, localVariables, etran);
// All done, so put the two pieces together
builder.Add(new Bpl.IfCmd(m.tok, null, definedness.Collect(m.tok), null, exporter.Collect(m.tok)));
#else
TrParallelCall(m.tok, parBoundVars, parRange, decrCheck, recursiveCall, null, builder, localVariables, etran);
#endif
}
}
// translate the body of the method
Contract.Assert(m.Body != null); // follows from method precondition and the if guard
stmts = TrStmt2StmtList(builder, m.Body, localVariables, etran);
} else {
// check well-formedness of the preconditions, and then assume each one of them
foreach (MaybeFreeExpression p in m.Req) {
CheckWellformed(p.E, new WFOptions(), localVariables, builder, etran);
builder.Add(new Bpl.AssumeCmd(p.E.tok, etran.TrExpr(p.E)));
}
// Note: the modifies clauses are not checked for well-formedness (is that sound?), because it used to
// be that the syntax was not rich enough for programmers to specify modifies clauses and always being
// absolutely well-defined.
// check well-formedness of the decreases clauses
foreach (Expression p in m.Decreases) {
CheckWellformed(p, new WFOptions(), localVariables, builder, etran);
}
// 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.Mod, etran.Old, etran, etran.Old)) {
if (tri.IsFree) {
builder.Add(new Bpl.AssumeCmd(m.tok, tri.Expr));
}
}
// also play havoc with the out parameters
if (outParams.Length != 0) { // don't create an empty havoc statement
Bpl.IdentifierExprSeq outH = new Bpl.IdentifierExprSeq();
foreach (Bpl.Variable b in outParams) {
Contract.Assert(b != null);
outH.Add(new Bpl.IdentifierExpr(b.tok, b));
}
builder.Add(new Bpl.HavocCmd(m.tok, outH));
}
// check wellformedness of postconditions
foreach (MaybeFreeExpression p in m.Ens) {
CheckWellformed(p.E, new WFOptions(), localVariables, builder, etran);
builder.Add(new Bpl.AssumeCmd(p.E.tok, etran.TrExpr(p.E)));
}
stmts = builder.Collect(m.tok);
}
QKeyValue kv = etran.TrAttributes(m.Attributes, null);
Bpl.Implementation impl = new Bpl.Implementation(m.tok, proc.Name,
typeParams, inParams, outParams,
localVariables, stmts, kv);
sink.TopLevelDeclarations.Add(impl);
currentMethod = null;
loopHeapVarCount = 0;
otherTmpVarCount = 0;
_tmpIEs.Clear();
}
void GenerateImplPrelude(Method m, Bpl.VariableSeq inParams, Bpl.VariableSeq outParams,
Bpl.StmtListBuilder builder, Bpl.VariableSeq localVariables){
Contract.Requires(m != null);
Contract.Requires(inParams != null);
Contract.Requires(outParams != null);
Contract.Requires(builder != null);
Contract.Requires(localVariables != null);
Contract.Requires(predef != null);
// set up the information used to verify the method's modifies clause
DefineFrame(m.tok, m.Mod, builder, localVariables, null);
}
Bpl.Cmd CaptureState(IToken tok, string/*?*/ additionalInfo) {
Contract.Requires(tok != null);
Contract.Ensures(Contract.Result() != null);
string description = string.Format("{0}({1},{2}){3}{4}", tok.filename, tok.line, tok.col, additionalInfo == null ? "" : ": ", additionalInfo ?? "");
QKeyValue kv = new QKeyValue(tok, "captureState", new List