//-----------------------------------------------------------------------------
//
// 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));
Contract.Invariant(currentMethod == null || currentMethod.EnclosingClass.Module == currentModule);
}
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;
private readonly Bpl.TypeCtorDecl mapTypeCtor;
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 MapType(IToken tok, Bpl.Type tya, Bpl.Type tyb) {
Contract.Requires(tok != null);
Contract.Requires(tya != null && tyb != null);
Contract.Ensures(Contract.Result() != null);
return new Bpl.CtorType(Token.NoToken, mapTypeCtor, new Bpl.TypeSeq(tya, tyb));
}
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.TypeCtorDecl mapTypeCtor, 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.mapTypeCtor = mapTypeCtor;
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.TypeCtorDecl mapTypeCtor = 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 (dt.Name == "Map") {
mapTypeCtor = 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._System.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 == "_System.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 (mapTypeCtor == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of type Map");
} else if (arrayLength == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of function _System.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._System.array");
} else {
return new PredefinedDecls(refType, boxType, tickType,
setTypeCtor, multiSetTypeCtor, mapTypeCtor, 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, (List)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 ArbitraryTypeDecl) {
// nothing to do--this is treated just like a type parameter
} else 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 ArbitraryTypeDecl) {
// nothing to do--this is treated just like a type parameter
} else 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 (dt is IndDatatypeDecl) {
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.FullName, 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);
AddFunctionAxiom(f, null, f.Ens, null, layerOffset);
} else {
AddFunctionAxiom(f, body, f.Ens, null, layerOffset);
}
if (!f.IsRecursive || f.IsUnlimited) { break; }
}
AddFrameAxiom(f);
AddWellformednessCheck(f);
} else if (member is Method) {
Method m = (Method)member;
bool isRefinementMethod = RefinementToken.IsInherited(m.tok, m.EnclosingClass.Module);
// wellformedness check for method specification
Bpl.Procedure proc = AddMethod(m, 0, isRefinementMethod);
sink.TopLevelDeclarations.Add(proc);
AddMethodImpl(m, proc, true);
// the method itself
proc = AddMethod(m, 1, isRefinementMethod);
sink.TopLevelDeclarations.Add(proc);
if (isRefinementMethod) {
proc = AddMethod(m, 2, isRefinementMethod);
sink.TopLevelDeclarations.Add(proc);
proc = AddMethod(m, 3, isRefinementMethod);
sink.TopLevelDeclarations.Add(proc);
}
if (m.Body != null) {
// ...and its implementation
AddMethodImpl(m, proc, false);
}
} 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 {
AddFunctionAxiom(f, body, new List(), s, layerOffset);
}
}
}
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);
}
}
void AddFunctionAxiom(Function/*!*/ f, Expression body, List/*!*/ ens, Specialization specialization, int layerOffset) {
if (f is Predicate) {
var ax = FunctionAxiom(f, FunctionAxiomVisibility.IntraModuleOnly, body, ens, specialization, layerOffset);
sink.TopLevelDeclarations.Add(ax);
ax = FunctionAxiom(f, FunctionAxiomVisibility.ForeignModuleOnly, body, ens, specialization, layerOffset);
sink.TopLevelDeclarations.Add(ax);
} else {
var ax = FunctionAxiom(f, FunctionAxiomVisibility.All, body, ens, specialization, layerOffset);
sink.TopLevelDeclarations.Add(ax);
}
}
enum FunctionAxiomVisibility { All, IntraModuleOnly, ForeignModuleOnly }
Bpl.Axiom/*!*/ FunctionAxiom(Function/*!*/ f, FunctionAxiomVisibility visibility, 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 || // (a)
// (mh == ModuleContextHeight && (fh <= FunctionContextHeight || InMethodContext)) // (b)
// ==>
// (forall $Heap, formals ::
// { f(args) }
// f#canCall(args) ||
// ( (mh != ModuleContextHeight || fh != FunctionContextHeight || InMethodContext) && // (c)
// $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 && // (d)
// 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.
//
// Visibility: The above description is for visibility==All. If visibility==IntraModuleOnly, then
// disjunct (a) is dropped (which also has a simplifying effect on (c)). Finally, if visibility==ForeignModuleOnly,
// then disjunct (b) is dropped (which also has a simplify effect on(c)); furthermore, if f is a Predicate,
// then the equality in (d) is replaced by an implication.
//
// 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;
var activateForeign = Bpl.Expr.Lt(Bpl.Expr.Literal(mod.Height), etran.ModuleContextHeight());
var activateIntra =
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()));
Bpl.Expr activate =
visibility == FunctionAxiomVisibility.All ? Bpl.Expr.Or(activateForeign, activateIntra) :
visibility == FunctionAxiomVisibility.IntraModuleOnly ? activateIntra : activateForeign;
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 = visibility == FunctionAxiomVisibility.ForeignModuleOnly ? Bpl.Expr.True :
Bpl.Expr.Or(Bpl.Expr.Or(
visibility == FunctionAxiomVisibility.IntraModuleOnly ?
(Bpl.Expr)Bpl.Expr.False :
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),
visibility == FunctionAxiomVisibility.ForeignModuleOnly && f is Predicate ?
Bpl.Expr.Imp(funcAppl, etran.LimitedFunctions(f).TrExpr(bodyWithSubst)) :
Bpl.Expr.Eq(funcAppl, etran.LimitedFunctions(f).TrExpr(bodyWithSubst)));
} else {
meat = visibility == FunctionAxiomVisibility.ForeignModuleOnly && f is Predicate ?
Bpl.Expr.Imp(funcAppl, etran.TrExpr(bodyWithSubst)) :
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 (visibility == FunctionAxiomVisibility.IntraModuleOnly) {
comment += " (intra-module)";
} else if (visibility == FunctionAxiomVisibility.ForeignModuleOnly) {
comment += " (foreign modules)";
}
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);
}
ModuleDecl currentModule = null; // the name of the module whose members are currently being translated
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(currentModule == null && currentMethod == null && loopHeapVarCount == 0 && _tmpIEs.Count == 0);
Contract.Ensures(currentModule == null && currentMethod == null && loopHeapVarCount == 0 && _tmpIEs.Count == 0);
currentModule = m.EnclosingClass.Module;
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.Expressions.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.FullName, 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, ExpressionTranslator exprTran) {
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(exprTran.TrExpr(ee));
Expression es = Substitute(ee, receiverReplacement, substMap);
es = Substitute(es, null, decrSubstMap);
decrCallee.Add(exprTran.TrExpr(es));
}
return DecreasesCheck(decrToks, decrTypes, decrCallee, decrCaller, exprTran, 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.Expressions)
{
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.Expressions, 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);
currentModule = null;
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.Expressions, 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