//-----------------------------------------------------------------------------
//
// Copyright (C) Microsoft Corporation. All Rights Reserved.
//
//-----------------------------------------------------------------------------
using System;
using System.Collections.Generic;
using System.Linq;
using System.Numerics;
using System.Diagnostics.Contracts;
using Bpl = Microsoft.Boogie;
using BplParser = Parser;
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();
readonly Dictionary fieldConstants = new Dictionary();
Program program;
[ContractInvariantMethod]
void ObjectInvariant()
{
Contract.Invariant(cce.NonNullDictionaryAndValues(classes));
Contract.Invariant(cce.NonNullDictionaryAndValues(fields));
Contract.Invariant(cce.NonNullDictionaryAndValues(fieldFunctions));
Contract.Invariant(codeContext == null || codeContext.EnclosingModule == currentModule);
}
readonly Bpl.Program sink;
readonly PredefinedDecls predef;
public bool InsertChecksums { get; set; }
public string UniqueIdPrefix { get; set; }
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 NameFamilyType;
public readonly Bpl.Type DatatypeType;
public readonly Bpl.Type LayerType;
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(NameFamilyType != null);
Contract.Invariant(DatatypeType != null);
Contract.Invariant(LayerType != 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 List { 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 List{ 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 List { 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 List{ 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 List{ 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 nameFamilyType,
Bpl.TypeCtorDecl datatypeType, Bpl.TypeCtorDecl layerType, 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(mapTypeCtor != null);
Contract.Requires(arrayLength != null);
Contract.Requires(seqTypeCtor != null);
Contract.Requires(fieldNameType != null);
Contract.Requires(heap != null);
Contract.Requires(classNameType != null);
Contract.Requires(datatypeType != null);
Contract.Requires(layerType != null);
Contract.Requires(dtCtorId != null);
Contract.Requires(allocField != null);
Contract.Requires(classDotArray != null);
#endregion
Bpl.CtorType refT = new Bpl.CtorType(Token.NoToken, refType, new List());
this.RefType = refT;
this.BoxType = new Bpl.CtorType(Token.NoToken, boxType, new List());
this.TickType = new Bpl.CtorType(Token.NoToken, tickType, new List());
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 List());
this.NameFamilyType = new Bpl.CtorType(Token.NoToken, nameFamilyType, new List());
this.DatatypeType = new Bpl.CtorType(Token.NoToken, datatypeType, new List());
this.LayerType = new Bpl.CtorType(Token.NoToken, layerType, new List());
this.DtCtorId = new Bpl.CtorType(Token.NoToken, dtCtorId, new List());
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 nameFamilyType = null;
Bpl.TypeCtorDecl datatypeType = null;
Bpl.TypeCtorDecl layerType = 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 == "LayerType") {
layerType = dt;
} else if (dt.Name == "DtCtorId") {
dtCtorId = dt;
} else if (dt.Name == "ref") {
refType = dt;
} else if (dt.Name == "NameFamily") {
nameFamilyType = 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 (nameFamilyType == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of type NameFamily");
} else if (datatypeType == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of type DatatypeType");
} else if (layerType == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of type LayerType");
} 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, nameFamilyType, datatypeType, layerType, 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 = BplParser.Parse(preludePath, (List)null, out prelude);
if (prelude == null || errorCount > 0) {
return null;
} else {
return prelude;
}
}
public Bpl.IdentifierExpr TrVar(IToken tok, IVariable var) {
Contract.Requires(var != null);
Contract.Requires(tok != null);
Contract.Ensures(Contract.Result() != null);
return new Bpl.IdentifierExpr(tok, var.AssignUniqueName(currentDeclaration), TrType(var.Type));
}
public Bpl.Program Translate(Program p) {
Contract.Requires(p != null);
Contract.Ensures(Contract.Result() != null);
program = p;
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) {
currentDeclaration = d;
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 (ModuleDefinition m in program.Modules) {
foreach (TopLevelDecl d in m.TopLevelDecls) {
currentDeclaration = d;
if (d is ArbitraryTypeDecl) {
// nothing to do--this is treated just like a type parameter
} else if (d is DatatypeDecl) {
AddDatatype((DatatypeDecl)d);
} else if (d is ModuleDecl) {
// submodules have already been added as a top level module, ignore this.
} else if (d is ClassDecl) {
AddClassMembers((ClassDecl)d);
if (d is IteratorDecl) {
AddIteratorSpecAndBody((IteratorDecl)d);
}
} else {
Contract.Assert(false);
}
}
}
foreach(var c in fieldConstants.Values) {
sink.TopLevelDeclarations.Add(c);
}
HashSet> checkedMethods = new HashSet>();
HashSet> checkedFunctions = new HashSet>();
foreach (var t in program.TranslationTasks) {
if (t is MethodCheck) {
var m = (MethodCheck)t;
currentDeclaration = m.Refining;
var id = new Tuple(m.Refined.FullSanitizedName, m.Refining.FullSanitizedName);
if (!checkedMethods.Contains(id)) {
AddMethodRefinementCheck(m);
checkedMethods.Add(id);
}
} else if (t is FunctionCheck) {
var f = (FunctionCheck)t;
currentDeclaration = f.Refining;
var id = new Tuple(f.Refined.FullSanitizedName, f.Refining.FullSanitizedName);
if (!checkedFunctions.Contains(id)) {
AddFunctionRefinementCheck(f);
checkedFunctions.Add(id);
}
}
}
if (InsertChecksums)
{
foreach (var decl in sink.TopLevelDeclarations)
{
var impl = decl as Implementation;
if (impl != null && impl.FindStringAttribute("checksum") == null)
{
impl.AddAttribute("checksum", "dummy");
}
var func = decl as Bpl.Function;
if (func != null && func.FindStringAttribute("checksum") == null)
{
func.AddAttribute("checksum", "dummy");
}
}
}
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);
List argTypes = new List();
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);
if (InsertChecksums)
{
InsertChecksum(dt, fn);
}
sink.TopLevelDeclarations.Add(fn);
// Add: axiom (forall params :: #dt.ctor(params)-has-the-expected-type);
List 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.Count != 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.Count != 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.Count != 0) {
q = new Bpl.ExistsExpr(ctor.tok, bvs, q);
}
q = Bpl.Expr.Imp(FunctionCall(ctor.tok, ctor.QueryField.FullSanitizedName, Bpl.Type.Bool, dId), q);
q = new Bpl.ForallExpr(ctor.tok, new List { 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);
sink.TopLevelDeclarations.Add(fn);
// and here comes the associated axiom:
{
var thVar = new Bpl.BoundVariable(ctor.tok, new TypedIdent(ctor.tok, "this", predef.DatatypeType));
var th = new Bpl.IdentifierExpr(ctor.tok, thVar);
var queryPredicate = FunctionCall(ctor.tok, fn.Name, Bpl.Type.Bool, th);
var ctorId = FunctionCall(ctor.tok, BuiltinFunction.DatatypeCtorId, null, th);
var rhs = Bpl.Expr.Eq(ctorId, new Bpl.IdentifierExpr(ctor.tok, cid)); // this uses the "cid" defined for the previous axiom
var body = Bpl.Expr.Iff(queryPredicate, rhs);
var tr = new Bpl.Trigger(ctor.tok, true, new List { queryPredicate });
var ax = new Bpl.ForallExpr(ctor.tok, new List { thVar }, tr, body);
sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, ax));
}
// 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 trg = new Bpl.Trigger(ctor.tok, true, new List { lhs });
q = new Bpl.ForallExpr(ctor.tok, bvs, trg, Bpl.Expr.Imp(isGoodHeap, Bpl.Expr.Iff(lhs, pt)));
sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, q));
if (dt is IndDatatypeDecl) {
// Add Lit axiom:
// axiom (forall p0, ..., pn :: #dt.ctor(Lit(p0), ..., Lit(pn)) == Lit(#dt.ctor(p0, .., pn)));
CreateBoundVariables(ctor.Formals, out bvs, out args);
List litargs = new List();
foreach (Bpl.Expr arg in args) {
litargs.Add(Lit(arg));
}
lhs = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, litargs);
Bpl.Expr rhs = Lit(FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args), predef.DatatypeType);
q = Bpl.Expr.Eq(lhs, rhs);
if (bvs.Count() > 0) {
Bpl.Trigger tr = new Bpl.Trigger(ctor.tok, true, new List { lhs });
q = new Bpl.ForallExpr(ctor.tok, bvs, tr, q);
}
sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, q));
}
// Add injectivity axioms:
Contract.Assert(ctor.Formals.Count == ctor.Destructors.Count); // even nameless destructors are included in ctor.Destructors
i = 0;
foreach (Formal arg in ctor.Formals) {
// function ##dt.ctor#i(DatatypeType) returns (Ti);
var sf = ctor.Destructors[i];
Contract.Assert(sf != null);
fn = GetReadonlyField(sf);
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));
// axiom (forall params, SeqRank(arg) < DtRank(#dt.ctor(params)));
CreateBoundVariables(ctor.Formals, out bvs, out args);
lhs = FunctionCall(ctor.tok, BuiltinFunction.SeqRank, null, args[i]);
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 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_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.FullSanitizedName, new List { cases_dBv }, cases_resType);
if (InsertChecksums)
{
InsertChecksum(dt, cases_fn);
}
sink.TopLevelDeclarations.Add(cases_fn);
// and here comes the actual axiom:
{
var dVar = new Bpl.BoundVariable(dt.tok, new Bpl.TypedIdent(dt.tok, "d", predef.DatatypeType));
var d = new Bpl.IdentifierExpr(dt.tok, dVar);
var lhs = FunctionCall(dt.tok, cases_fn.Name, Bpl.Type.Bool, d);
Bpl.Expr cases_body = Bpl.Expr.False;
foreach (DatatypeCtor ctor in dt.Ctors) {
var disj = FunctionCall(ctor.tok, ctor.QueryField.FullSanitizedName, Bpl.Type.Bool, d);
cases_body = BplOr(cases_body, disj);
}
var body = Bpl.Expr.Iff(lhs, cases_body);
var tr = new Bpl.Trigger(dt.tok, true, new List { lhs });
var ax = new Bpl.ForallExpr(dt.tok, new List { dVar }, tr, body);
sink.TopLevelDeclarations.Add(new Bpl.Axiom(dt.tok, ax));
}
// The axiom above ($IsA#Dt(d) <==> Dt.Ctor0?(d) || Dt.Ctor1?(d)) gets triggered only with $IsA#Dt(d). The $IsA#Dt(d)
// predicate is generated only where the translation inserts it; in other words, the user cannot write any assertion
// that causes the $IsA#Dt(d) predicate to be emitted. This is what we want, because making the RHS disjunction be
// available too often makes performance go down. However, we do want to allow the disjunction to be introduced if the
// user explicitly talks about one of its disjuncts. To make this useful, we introduce the following axiom. Note that
// the DtType(d) information is available everywhere.
// axiom (forall d: DatatypeType ::
// { Dt.Ctor0?(d) }
// { Dt.Ctor1?(d) }
// DtType(d) == D ==> Dt.Ctor0?(d) || Dt.Ctor1?(d) || ...);
{
var dVar = new Bpl.BoundVariable(dt.tok, new Bpl.TypedIdent(dt.tok, "d", predef.DatatypeType));
var d = new Bpl.IdentifierExpr(dt.tok, dVar);
var lhs = Bpl.Expr.Eq(FunctionCall(dt.tok, BuiltinFunction.DtType, null, d), new Bpl.IdentifierExpr(dt.tok, GetClass(dt)));
Bpl.Expr cases_body = Bpl.Expr.False;
Bpl.Trigger tr = null;
foreach (DatatypeCtor ctor in dt.Ctors) {
var disj = FunctionCall(ctor.tok, ctor.QueryField.FullSanitizedName, Bpl.Type.Bool, d);
cases_body = BplOr(cases_body, disj);
tr = new Bpl.Trigger(ctor.tok, true, new List { disj }, tr);
}
var body = Bpl.Expr.Imp(lhs, cases_body);
var ax = new Bpl.ForallExpr(dt.tok, new List { dVar }, tr, body);
sink.TopLevelDeclarations.Add(new Bpl.Axiom(dt.tok, ax));
}
if (dt is CoDatatypeDecl) {
var codecl = (CoDatatypeDecl)dt;
// Add:
// Like for user-defined function, we add three version of the Eq (and, below, the prefix equality) function.
// Here is level 2:
// function $Eq#2#Dt(d0, d1: DatatypeType): bool;
{
var d0Var = new Bpl.Formal(dt.tok, new Bpl.TypedIdent(dt.tok, "d0", predef.DatatypeType), true);
var d1Var = new Bpl.Formal(dt.tok, new Bpl.TypedIdent(dt.tok, "d1", predef.DatatypeType), true);
var resType = new Bpl.Formal(dt.tok, new Bpl.TypedIdent(dt.tok, Bpl.TypedIdent.NoName, Bpl.Type.Bool), false);
var fn = new Bpl.Function(dt.tok, "$Eq#2#" + dt.FullSanitizedName, new List { d0Var, d1Var }, resType,
"equality for codatatype " + dt.FullName);
if (InsertChecksums)
{
InsertChecksum(dt, fn);
}
sink.TopLevelDeclarations.Add(fn);
}
// axiom (forall d0, d1: DatatypeType :: { $Eq#2#Dt(d0, d1) } $Eq#2#Dt(d0, d1) <==>
// (d0.Nil? ==> d1.Nil?) &&
// (d0.Cons? ==> d1.Cons? && d0.head == d1.head && $Eq#Dt(k-1, d0.tail, d1.tail));
{
var d0Var = new Bpl.BoundVariable(dt.tok, new Bpl.TypedIdent(dt.tok, "d0", predef.DatatypeType));
var d0 = new Bpl.IdentifierExpr(dt.tok, d0Var);
var d1Var = new Bpl.BoundVariable(dt.tok, new Bpl.TypedIdent(dt.tok, "d1", predef.DatatypeType));
var d1 = new Bpl.IdentifierExpr(dt.tok, d1Var);
var eqDt = FunctionCall(dt.tok, "$Eq#2#" + dt.FullSanitizedName, Bpl.Type.Bool, d0, d1);
var body = Bpl.Expr.Iff(eqDt, BplAnd(CoPrefixEquality(dt.tok, codecl, d0, d1, null, 1)));
var tr = new Bpl.Trigger(dt.tok, true, new List { eqDt });
var ax = new Bpl.ForallExpr(dt.tok, new List { d0Var, d1Var }, tr, body);
sink.TopLevelDeclarations.Add(new Bpl.Axiom(dt.tok, ax));
}
// Here is level 1:
// function $Eq#Dt(d0, d1: DatatypeType): bool;
{
var d0Var = new Bpl.Formal(dt.tok, new Bpl.TypedIdent(dt.tok, "d0", predef.DatatypeType), true);
var d1Var = new Bpl.Formal(dt.tok, new Bpl.TypedIdent(dt.tok, "d1", predef.DatatypeType), true);
var resType = new Bpl.Formal(dt.tok, new Bpl.TypedIdent(dt.tok, Bpl.TypedIdent.NoName, Bpl.Type.Bool), false);
var fn = new Bpl.Function(dt.tok, "$Eq#" + dt.FullSanitizedName, new List { d0Var, d1Var }, resType);
if (InsertChecksums)
{
InsertChecksum(dt, fn);
}
sink.TopLevelDeclarations.Add(fn);
}
// axiom (forall d0, d1: DatatypeType :: { $Eq#Dt(d0, d1) } $Eq#Dt(d0, d1) <==>
// (d0.Nil? ==> d1.Nil?) &&
// (d0.Cons? ==> d1.Cons? && d0.head == d1.head && $Eq#0#Dt(k-1, d0.tail, d1.tail));
{
var d0Var = new Bpl.BoundVariable(dt.tok, new Bpl.TypedIdent(dt.tok, "d0", predef.DatatypeType));
var d0 = new Bpl.IdentifierExpr(dt.tok, d0Var);
var d1Var = new Bpl.BoundVariable(dt.tok, new Bpl.TypedIdent(dt.tok, "d1", predef.DatatypeType));
var d1 = new Bpl.IdentifierExpr(dt.tok, d1Var);
var eqDt = FunctionCall(dt.tok, "$Eq#" + dt.FullSanitizedName, Bpl.Type.Bool, d0, d1);
var body = Bpl.Expr.Iff(eqDt, BplAnd(CoPrefixEquality(dt.tok, codecl, d0, d1, null, 0)));
var tr = new Bpl.Trigger(dt.tok, true, new List { eqDt });
var ax = new Bpl.ForallExpr(dt.tok, new List { d0Var, d1Var }, tr, body);
sink.TopLevelDeclarations.Add(new Bpl.Axiom(dt.tok, ax));
}
// axiom (forall d0, d1: DatatypeType :: { $Eq#2#Dt(d0, d1) } $Eq#2#Dt(d0, d1) <==>
// (d0.Nil? ==> d1.Nil?) &&
// (d0.Cons? ==> d1.Cons? && d0.head == d1.head && $Eq#Dt(k-1, d0.tail, d1.tail));
{
var d0Var = new Bpl.BoundVariable(dt.tok, new Bpl.TypedIdent(dt.tok, "d0", predef.DatatypeType));
var d0 = new Bpl.IdentifierExpr(dt.tok, d0Var);
var d1Var = new Bpl.BoundVariable(dt.tok, new Bpl.TypedIdent(dt.tok, "d1", predef.DatatypeType));
var d1 = new Bpl.IdentifierExpr(dt.tok, d1Var);
var eqDt = FunctionCall(dt.tok, "$Eq#2#" + dt.FullSanitizedName, Bpl.Type.Bool, d0, d1);
var body = Bpl.Expr.Iff(eqDt, BplAnd(CoPrefixEquality(dt.tok, codecl, d0, d1, null, 1)));
var tr = new Bpl.Trigger(dt.tok, true, new List { eqDt });
var ax = new Bpl.ForallExpr(dt.tok, new List { d0Var, d1Var }, tr, body);
sink.TopLevelDeclarations.Add(new Bpl.Axiom(dt.tok, ax));
}
// Here is level 0 (aka limited):
// function $Eq#0#Dt(d0, d1: DatatypeType): bool
{
var d0Var = new Bpl.Formal(dt.tok, new Bpl.TypedIdent(dt.tok, "d0", predef.DatatypeType), true);
var d1Var = new Bpl.Formal(dt.tok, new Bpl.TypedIdent(dt.tok, "d1", predef.DatatypeType), true);
var resType = new Bpl.Formal(dt.tok, new Bpl.TypedIdent(dt.tok, Bpl.TypedIdent.NoName, Bpl.Type.Bool), false);
var fn = new Bpl.Function(dt.tok, "$Eq#0#" + dt.FullSanitizedName, new List { d0Var, d1Var }, resType,
"equality (limited version) for codatatype " + dt.FullName);
if (InsertChecksums)
{
InsertChecksum(dt, fn);
}
sink.TopLevelDeclarations.Add(fn);
}
// axiom (forall d0: DatatypeType, d1: DatatypeType :: { $Eq#Dt(d0,d1) }
// $Eq#Dt(d0,d1) == $Eq#0#Dt(d0,d1));
{
var kVar = new Bpl.BoundVariable(dt.tok, new Bpl.TypedIdent(dt.tok, "k", Bpl.Type.Int));
var k = new Bpl.IdentifierExpr(dt.tok, kVar);
var d0Var = new Bpl.BoundVariable(dt.tok, new Bpl.TypedIdent(dt.tok, "d0", predef.DatatypeType));
var d0 = new Bpl.IdentifierExpr(dt.tok, d0Var);
var d1Var = new Bpl.BoundVariable(dt.tok, new Bpl.TypedIdent(dt.tok, "d1", predef.DatatypeType));
var d1 = new Bpl.IdentifierExpr(dt.tok, d1Var);
var eqDt = FunctionCall(dt.tok, "$Eq#" + dt.FullSanitizedName, Bpl.Type.Bool, d0, d1);
var eqDt0 = FunctionCall(dt.tok, "$Eq#0#" + dt.FullSanitizedName, Bpl.Type.Bool, d0, d1);
var tr = new Bpl.Trigger(dt.tok, true, new List { eqDt });
var ax = new Bpl.ForallExpr(dt.tok, new List { d0Var, d1Var }, tr, Bpl.Expr.Eq(eqDt, eqDt0));
sink.TopLevelDeclarations.Add(new Bpl.Axiom(dt.tok, ax));
}
// axiom (forall d0, d1: DatatypeType :: { Eq$Dt(d0, d1) } Eq$Dt(d0, d1) <==> d0 == d1);
{
var d0Var = new Bpl.BoundVariable(dt.tok, new Bpl.TypedIdent(dt.tok, "d0", predef.DatatypeType));
var d0 = new Bpl.IdentifierExpr(dt.tok, d0Var);
var d1Var = new Bpl.BoundVariable(dt.tok, new Bpl.TypedIdent(dt.tok, "d1", predef.DatatypeType));
var d1 = new Bpl.IdentifierExpr(dt.tok, d1Var);
var eqDt = FunctionCall(dt.tok, "$Eq#" + dt.FullSanitizedName, Bpl.Type.Bool, d0, d1);
var eq = Bpl.Expr.Eq(d0, d1);
var tr = new Bpl.Trigger(dt.tok, true, new List { eqDt });
var ax = new Bpl.ForallExpr(dt.tok, new List { d0Var, d1Var }, tr, Bpl.Expr.Iff(eqDt, eq));
sink.TopLevelDeclarations.Add(new Bpl.Axiom(dt.tok, ax));
}
// Now for prefix equality, which also comes in 3 levels:
// Here is level 2:
// function $PrefixEqual#2#Dt(k: int, d0: DatatypeType, d1: DatatypeType): bool
{
var kVar = new Bpl.Formal(dt.tok, new Bpl.TypedIdent(dt.tok, "k", Bpl.Type.Int), true);
var d0Var = new Bpl.Formal(dt.tok, new Bpl.TypedIdent(dt.tok, "d0", predef.DatatypeType), true);
var d1Var = new Bpl.Formal(dt.tok, new Bpl.TypedIdent(dt.tok, "d1", predef.DatatypeType), true);
var resType = new Bpl.Formal(dt.tok, new Bpl.TypedIdent(dt.tok, Bpl.TypedIdent.NoName, Bpl.Type.Bool), false);
var fn = new Bpl.Function(dt.tok, CoPrefixName(codecl, 2), new List { kVar, d0Var, d1Var }, resType,
"prefix equality for codatatype " + dt.FullName);
if (InsertChecksums)
{
InsertChecksum(dt, fn);
}
sink.TopLevelDeclarations.Add(fn);
}
// axiom (forall k: int, d0, d1: DatatypeType :: { $PrefixEqual#2#Dt(k, d0, d1) } $PrefixEqual#2#Dt(k, d0, d1) <==>
// 0 < k ==>
// (d0.Nil? ==> d1.Nil?) &&
// (d0.Cons? ==> d1.Cons? && d0.head == d1.head && $PrefixEqual#Dt(k-1, d0.tail, d1.tail))
{
var kVar = new Bpl.BoundVariable(dt.tok, new Bpl.TypedIdent(dt.tok, "k", Bpl.Type.Int));
var k = new Bpl.IdentifierExpr(dt.tok, kVar);
var d0Var = new Bpl.BoundVariable(dt.tok, new Bpl.TypedIdent(dt.tok, "d0", predef.DatatypeType));
var d0 = new Bpl.IdentifierExpr(dt.tok, d0Var);
var d1Var = new Bpl.BoundVariable(dt.tok, new Bpl.TypedIdent(dt.tok, "d1", predef.DatatypeType));
var d1 = new Bpl.IdentifierExpr(dt.tok, d1Var);
var prefixEq = FunctionCall(dt.tok, CoPrefixName(codecl, 2), Bpl.Type.Bool, k, d0, d1);
var pos = Bpl.Expr.Lt(Bpl.Expr.Literal(0), k);
var kMinusOne = Bpl.Expr.Sub(k, Bpl.Expr.Literal(1));
var body = Bpl.Expr.Iff(prefixEq, Bpl.Expr.Imp(pos, BplAnd(CoPrefixEquality(dt.tok, codecl, d0, d1, kMinusOne, 1))));
var tr = new Bpl.Trigger(dt.tok, true, new List { prefixEq });
var ax = new Bpl.ForallExpr(dt.tok, new List { kVar, d0Var, d1Var }, tr, body);
sink.TopLevelDeclarations.Add(new Bpl.Axiom(dt.tok, ax));
}
// Here is level 1:
// function $PrefixEqual#Dt(k: int, d0: DatatypeType, d1: DatatypeType): bool
{
var kVar = new Bpl.Formal(dt.tok, new Bpl.TypedIdent(dt.tok, "k", Bpl.Type.Int), true);
var d0Var = new Bpl.Formal(dt.tok, new Bpl.TypedIdent(dt.tok, "d0", predef.DatatypeType), true);
var d1Var = new Bpl.Formal(dt.tok, new Bpl.TypedIdent(dt.tok, "d1", predef.DatatypeType), true);
var resType = new Bpl.Formal(dt.tok, new Bpl.TypedIdent(dt.tok, Bpl.TypedIdent.NoName, Bpl.Type.Bool), false);
var fn = new Bpl.Function(dt.tok, CoPrefixName(codecl, 1), new List { kVar, d0Var, d1Var }, resType);
if (InsertChecksums)
{
InsertChecksum(dt, fn);
}
sink.TopLevelDeclarations.Add(fn);
}
// axiom (forall k: int, d0, d1: DatatypeType :: { $PrefixEqual#Dt(k, d0, d1) } $PrefixEqual#Dt(k, d0, d1) <==>
// 0 < k ==>
// (d0.Nil? ==> d1.Nil?) &&
// (d0.Cons? ==> d1.Cons? && d0.head == d1.head && $PrefixEqual#0#Dt(k-1, d0.tail, d1.tail))
{
var kVar = new Bpl.BoundVariable(dt.tok, new Bpl.TypedIdent(dt.tok, "k", Bpl.Type.Int));
var k = new Bpl.IdentifierExpr(dt.tok, kVar);
var d0Var = new Bpl.BoundVariable(dt.tok, new Bpl.TypedIdent(dt.tok, "d0", predef.DatatypeType));
var d0 = new Bpl.IdentifierExpr(dt.tok, d0Var);
var d1Var = new Bpl.BoundVariable(dt.tok, new Bpl.TypedIdent(dt.tok, "d1", predef.DatatypeType));
var d1 = new Bpl.IdentifierExpr(dt.tok, d1Var);
var prefixEq = FunctionCall(dt.tok, CoPrefixName(codecl, 1), Bpl.Type.Bool, k, d0, d1);
var pos = Bpl.Expr.Lt(Bpl.Expr.Literal(0), k);
var kMinusOne = Bpl.Expr.Sub(k, Bpl.Expr.Literal(1));
var body = Bpl.Expr.Iff(prefixEq, Bpl.Expr.Imp(pos, BplAnd(CoPrefixEquality(dt.tok, codecl, d0, d1, kMinusOne, 0))));
var tr = new Bpl.Trigger(dt.tok, true, new List { prefixEq });
var ax = new Bpl.ForallExpr(dt.tok, new List { kVar, d0Var, d1Var }, tr, body);
sink.TopLevelDeclarations.Add(new Bpl.Axiom(dt.tok, ax));
}
// axiom (forall k: int, d0: DatatypeType, d1: DatatypeType :: { $PrefixEqual#2#Dt(k,d0,d1) }
// $PrefixEqual#2#Dt(k,d0,d1) == $PrefixEqual#Dt(k,d0,d1));
{
var kVar = new Bpl.BoundVariable(dt.tok, new Bpl.TypedIdent(dt.tok, "k", Bpl.Type.Int));
var k = new Bpl.IdentifierExpr(dt.tok, kVar);
var d0Var = new Bpl.BoundVariable(dt.tok, new Bpl.TypedIdent(dt.tok, "d0", predef.DatatypeType));
var d0 = new Bpl.IdentifierExpr(dt.tok, d0Var);
var d1Var = new Bpl.BoundVariable(dt.tok, new Bpl.TypedIdent(dt.tok, "d1", predef.DatatypeType));
var d1 = new Bpl.IdentifierExpr(dt.tok, d1Var);
var p0 = FunctionCall(dt.tok, CoPrefixName(codecl, 1), Bpl.Type.Bool, k, d0, d1);
var p1 = FunctionCall(dt.tok, CoPrefixName(codecl, 2), Bpl.Type.Bool, k, d0, d1);
var tr = new Bpl.Trigger(dt.tok, true, new List { p1 });
var ax = new Bpl.ForallExpr(dt.tok, new List { kVar, d0Var, d1Var }, tr, Bpl.Expr.Eq(p1, p0));
sink.TopLevelDeclarations.Add(new Bpl.Axiom(dt.tok, ax));
}
// Add the 'limited' version:
// function $PrefixEqual#0#Dt(k: int, d0: DatatypeType, d1: DatatypeType): bool;
{
var kVar = new Bpl.Formal(dt.tok, new Bpl.TypedIdent(dt.tok, "k", Bpl.Type.Int), true);
var d0Var = new Bpl.Formal(dt.tok, new Bpl.TypedIdent(dt.tok, "d0", predef.DatatypeType), true);
var d1Var = new Bpl.Formal(dt.tok, new Bpl.TypedIdent(dt.tok, "d1", predef.DatatypeType), true);
var resType = new Bpl.Formal(dt.tok, new Bpl.TypedIdent(dt.tok, Bpl.TypedIdent.NoName, Bpl.Type.Bool), false);
var fn = new Bpl.Function(dt.tok, CoPrefixName(codecl, 0), new List { kVar, d0Var, d1Var }, resType);
if (InsertChecksums)
{
InsertChecksum(dt, fn);
}
sink.TopLevelDeclarations.Add(fn);
}
// axiom (forall k: int, d0: DatatypeType, d1: DatatypeType :: { $PrefixEqual#Dt(k,d0,d1) }
// $PrefixEqual#Dt(k,d0,d1) == $PrefixEqual#0#Dt(k,d0,d1));
{
var kVar = new Bpl.BoundVariable(dt.tok, new Bpl.TypedIdent(dt.tok, "k", Bpl.Type.Int));
var k = new Bpl.IdentifierExpr(dt.tok, kVar);
var d0Var = new Bpl.BoundVariable(dt.tok, new Bpl.TypedIdent(dt.tok, "d0", predef.DatatypeType));
var d0 = new Bpl.IdentifierExpr(dt.tok, d0Var);
var d1Var = new Bpl.BoundVariable(dt.tok, new Bpl.TypedIdent(dt.tok, "d1", predef.DatatypeType));
var d1 = new Bpl.IdentifierExpr(dt.tok, d1Var);
var p0 = FunctionCall(dt.tok, CoPrefixName(codecl, 0), Bpl.Type.Bool, k, d0, d1);
var p1 = FunctionCall(dt.tok, CoPrefixName(codecl, 1), Bpl.Type.Bool, k, d0, d1);
var tr = new Bpl.Trigger(dt.tok, true, new List { p1 });
var ax = new Bpl.ForallExpr(dt.tok, new List { kVar, d0Var, d1Var }, tr, Bpl.Expr.Eq(p1, p0));
sink.TopLevelDeclarations.Add(new Bpl.Axiom(dt.tok, ax));
}
// The connection between the full codatatype equality and its prefix version
// axiom (forall d0, d1: DatatypeType :: $Eq#Dt(d0, d1) <==>
// (forall k: int :: 0 <= k ==> $PrefixEqual#Dt(k, d0, d1)));
{
var kVar = new Bpl.BoundVariable(dt.tok, new Bpl.TypedIdent(dt.tok, "k", Bpl.Type.Int));
var k = new Bpl.IdentifierExpr(dt.tok, kVar);
var d0Var = new Bpl.BoundVariable(dt.tok, new Bpl.TypedIdent(dt.tok, "d0", predef.DatatypeType));
var d0 = new Bpl.IdentifierExpr(dt.tok, d0Var);
var d1Var = new Bpl.BoundVariable(dt.tok, new Bpl.TypedIdent(dt.tok, "d1", predef.DatatypeType));
var d1 = new Bpl.IdentifierExpr(dt.tok, d1Var);
var prefixEq = FunctionCall(dt.tok, CoPrefixName(codecl, 1), Bpl.Type.Bool, k, d0, d1);
var body = Bpl.Expr.Imp(Bpl.Expr.Le(Bpl.Expr.Literal(0), k), prefixEq);
var q = new Bpl.ForallExpr(dt.tok, new List { kVar }, body);
var eqDt = FunctionCall(dt.tok, "$Eq#" + dt.FullSanitizedName, Bpl.Type.Bool, d0, d1);
q = new Bpl.ForallExpr(dt.tok, new List { d0Var, d1Var }, Bpl.Expr.Iff(eqDt, q));
sink.TopLevelDeclarations.Add(new Bpl.Axiom(dt.tok, q));
}
// A consequence of the definition of prefix equalities is the following:
// axiom (forall k, m: int, d0, d1: DatatypeType :: 0 <= k <= m && $PrefixEq#Dt(m, d0, d1) ==> $PrefixEq#0#Dt(k, d0, d1));
{
var kVar = new Bpl.BoundVariable(dt.tok, new Bpl.TypedIdent(dt.tok, "k", Bpl.Type.Int));
var k = new Bpl.IdentifierExpr(dt.tok, kVar);
var mVar = new Bpl.BoundVariable(dt.tok, new Bpl.TypedIdent(dt.tok, "m", Bpl.Type.Int));
var m = new Bpl.IdentifierExpr(dt.tok, mVar);
var d0Var = new Bpl.BoundVariable(dt.tok, new Bpl.TypedIdent(dt.tok, "d0", predef.DatatypeType));
var d0 = new Bpl.IdentifierExpr(dt.tok, d0Var);
var d1Var = new Bpl.BoundVariable(dt.tok, new Bpl.TypedIdent(dt.tok, "d1", predef.DatatypeType));
var d1 = new Bpl.IdentifierExpr(dt.tok, d1Var);
var prefixEqK = FunctionCall(dt.tok, CoPrefixName(codecl, 0), Bpl.Type.Bool, k, d0, d1);
var prefixEqM = FunctionCall(dt.tok, CoPrefixName(codecl, 1), Bpl.Type.Bool, m, d0, d1);
var range = BplAnd(Bpl.Expr.Le(Bpl.Expr.Literal(0), k), Bpl.Expr.Le(k, m));
var body = Bpl.Expr.Imp(BplAnd(range, prefixEqM), prefixEqK);
var q = new Bpl.ForallExpr(dt.tok, new List { kVar, mVar, d0Var, d1Var }, body);
sink.TopLevelDeclarations.Add(new Bpl.Axiom(dt.tok, q));
}
// With the axioms above, going from d0==d1 to a prefix equality requires going via the full codatatype
// equality, which in turn requires the full codatatype equality to be present. The following axiom
// provides a shortcut:
// axiom (forall d0, d1: DatatypeType, k: int :: d0 == d1 && 0 <= k ==> $PrefixEqual#_module.Stream(k, d0, d1));
{
var kVar = new Bpl.BoundVariable(dt.tok, new Bpl.TypedIdent(dt.tok, "k", Bpl.Type.Int));
var k = new Bpl.IdentifierExpr(dt.tok, kVar);
var d0Var = new Bpl.BoundVariable(dt.tok, new Bpl.TypedIdent(dt.tok, "d0", predef.DatatypeType));
var d0 = new Bpl.IdentifierExpr(dt.tok, d0Var);
var d1Var = new Bpl.BoundVariable(dt.tok, new Bpl.TypedIdent(dt.tok, "d1", predef.DatatypeType));
var d1 = new Bpl.IdentifierExpr(dt.tok, d1Var);
var prefixEq = FunctionCall(dt.tok, CoPrefixName(codecl, 1), Bpl.Type.Bool, k, d0, d1);
var body = Bpl.Expr.Imp(BplAnd(Bpl.Expr.Eq(d0, d1), Bpl.Expr.Le(Bpl.Expr.Literal(0), k)), prefixEq);
var q = new Bpl.ForallExpr(dt.tok, new List { kVar, d0Var, d1Var }, body);
sink.TopLevelDeclarations.Add(new Bpl.Axiom(dt.tok, q));
}
}
}
///
/// Return a sequence of expressions whose conjunction denotes a memberwise equality of "dt". Recursive
/// codatatype equalities are written in one of the following ways:
/// If the codatatype equality is on a type outside the SCC of "dt", then resort to ordinary equality.
/// Else if the k==null, then:
/// Depending on "limited", use the #2, #1, or #0 (limited) form of codatatype equality.
/// Else:
/// Depending on "limited", use the #2, #1, or #0 (limited) form of prefix equality, passing "k"
/// as the first argument.
///
IEnumerable CoPrefixEquality(IToken tok, CoDatatypeDecl dt, Bpl.Expr A, Bpl.Expr B, Bpl.Expr k, int limited) {
Contract.Requires(tok != null);
Contract.Requires(dt != null);
Contract.Requires(A != null);
Contract.Requires(B != null);
Contract.Requires(0 <= limited && limited < 3);
Contract.Requires(predef != null);
var etran = new ExpressionTranslator(this, predef, dt.tok);
// For example, for possibly infinite lists:
// codatatype SList = Nil | SCons(head: T, tail: SList);
// produce:
// (A.Nil? ==> B.Nil?) &&
// (A.Cons? ==> B.Cons? && A.head == B.head && Equal(k, A.tail, B.tail))
foreach (var ctor in dt.Ctors) {
var lhs = new Bpl.NAryExpr(tok, new Bpl.FunctionCall(GetReadonlyField(ctor.QueryField)), new List { A });
Bpl.Expr rhs = new Bpl.NAryExpr(tok, new Bpl.FunctionCall(GetReadonlyField(ctor.QueryField)), new List { B });
foreach (var dtor in ctor.Destructors) { // note, ctor.Destructors has a field for every constructor parameter, whether or not the parameter was named in the source
var a = new Bpl.NAryExpr(tok, new Bpl.FunctionCall(GetReadonlyField(dtor)), new List { A });
var b = new Bpl.NAryExpr(tok, new Bpl.FunctionCall(GetReadonlyField(dtor)), new List { B });
var ty = dtor.Type;
Bpl.Expr q = null;
var codecl = ty.AsCoDatatype;
if (codecl != null && codecl.SscRepr == dt.SscRepr) {
if (k != null) {
q = FunctionCall(tok, CoPrefixName(codecl, limited), Bpl.Type.Bool, k, a, b);
} else if (limited == 2) {
q = FunctionCall(tok, "$Eq#2#" + codecl.FullSanitizedName, Bpl.Type.Bool, a, b);
} else if (limited == 0) {
q = FunctionCall(tok, "$Eq#0#" + codecl.FullSanitizedName, Bpl.Type.Bool, a, b);
} else {
q = FunctionCall(tok, "$Eq#" + codecl.FullSanitizedName, Bpl.Type.Bool, a, b);
}
}
if (q == null) {
// ordinary equality; let the usual translation machinery figure out the translation
var equal = new BinaryExpr(tok, BinaryExpr.Opcode.Eq, new BoogieWrapper(a, ty), new BoogieWrapper(b, ty));
equal.ResolvedOp = Resolver.ResolveOp(equal.Op, ty); // resolve here
equal.Type = Type.Bool; // resolve here
q = etran.TrExpr(equal);
}
rhs = BplAnd(rhs, q);
}
yield return Bpl.Expr.Binary(new NestedToken(tok, ctor.tok), BinaryOperator.Opcode.Imp, lhs, rhs);
}
}
static string CoPrefixName(CoDatatypeDecl codecl, int limited) {
Contract.Requires(codecl != null);
Contract.Requires(0 <= limited && limited < 3);
if (limited == 2) {
return "$PrefixEqual#2#" + codecl.FullSanitizedName;
} else if (limited == 0) {
return "$PrefixEqual#0#" + codecl.FullSanitizedName;
} else {
return "$PrefixEqual#" + codecl.FullSanitizedName;
}
}
void CreateBoundVariables(List/*!*/ formals, out List/*!*/ bvs, out List/*!*/ args)
{
Contract.Requires(formals != null);
Contract.Ensures(Contract.ValueAtReturn(out bvs).Count == Contract.ValueAtReturn(out args).Count);
Contract.Ensures(Contract.ValueAtReturn(out bvs) != null);
Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out args)));
bvs = new List();
args = new List();
foreach (Formal arg in formals) {
Contract.Assert(arg != null);
var nm = string.Format("a{0}#{1}", bvs.Count, 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) {
currentDeclaration = member;
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) {
var f = (Function)member;
AddClassMember_Function(f);
if (!IsOpaqueFunction(f) && !f.IsBuiltin && !(f.tok is IncludeToken)) { // Opaque function's well-formedness is checked on the full version
AddWellformednessCheck(f);
}
var cop = f as CoPredicate;
if (cop != null) {
AddClassMember_Function(cop.PrefixPredicate);
// skip the well-formedness check, because it has already been done for the copredicate
}
} else if (member is Method) {
Method m = (Method)member;
// wellformedness check for method specification
if (m.EnclosingClass is IteratorDecl && m == ((IteratorDecl)m.EnclosingClass).Member_MoveNext) {
// skip the well-formedness check, because it has already been done for the iterator
} else {
var proc = AddMethod(m, MethodTranslationKind.SpecWellformedness);
sink.TopLevelDeclarations.Add(proc);
if (!(m.tok is IncludeToken)) {
AddMethodImpl(m, proc, true);
}
}
// the method spec itself
sink.TopLevelDeclarations.Add(AddMethod(m, MethodTranslationKind.InterModuleCall));
sink.TopLevelDeclarations.Add(AddMethod(m, MethodTranslationKind.IntraModuleCall));
if (m is CoLemma) {
// Let the CoCall and Impl forms to use m.PrefixLemma signature and specification (and
// note that m.PrefixLemma.Body == m.Body.
m = ((CoLemma)m).PrefixLemma;
sink.TopLevelDeclarations.Add(AddMethod(m, MethodTranslationKind.CoCall));
}
if (m.Body != null && !(m.tok is IncludeToken)) {
// ...and its implementation
var proc = AddMethod(m, MethodTranslationKind.Implementation);
sink.TopLevelDeclarations.Add(proc);
AddMethodImpl(m, proc, false);
}
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected member
}
}
}
private bool IsOpaqueFunction(Function f) {
return Attributes.Contains(f.Attributes, "opaque") &&
!Attributes.Contains(f.Attributes, "opaque_full"); // The full version has both attributes
}
private void AddClassMember_Function(Function f) {
// declare function
AddFunction(f);
// add synonym axiom
if (f.IsRecursive) {
AddSynonymAxiom(f);
}
// add frame axiom
AddFrameAxiom(f);
// add consequence axiom
sink.TopLevelDeclarations.Add(FunctionConsequenceAxiom(f, f.Ens));
// add definition axioms, suitably specialized for "match" cases and for literals
if (f.Body != null && !IsOpaqueFunction(f)) {
AddFunctionAxiom(f, FunctionAxiomVisibility.IntraModuleOnly, f.Body.Resolved);
AddFunctionAxiom(f, FunctionAxiomVisibility.ForeignModuleOnly, f.Body.Resolved);
}
// supply the connection between co-predicates and prefix predicates
if (f is CoPredicate) {
AddPrefixPredicateAxioms(((CoPredicate)f).PrefixPredicate);
}
}
void AddIteratorSpecAndBody(IteratorDecl iter) {
Contract.Requires(iter != null);
// wellformedness check for method specification
Bpl.Procedure proc = AddIteratorProc(iter, MethodTranslationKind.SpecWellformedness);
sink.TopLevelDeclarations.Add(proc);
AddIteratorWellformed(iter, proc);
// the method itself
if (iter.Body != null) {
proc = AddIteratorProc(iter, MethodTranslationKind.Implementation);
sink.TopLevelDeclarations.Add(proc);
// ...and its implementation
AddIteratorImpl(iter, proc);
}
}
Bpl.Procedure AddIteratorProc(IteratorDecl iter, MethodTranslationKind kind) {
Contract.Requires(iter != null);
Contract.Requires(kind == MethodTranslationKind.SpecWellformedness || kind == MethodTranslationKind.Implementation);
Contract.Requires(predef != null);
Contract.Requires(currentModule == null && codeContext == null);
Contract.Ensures(currentModule == null && codeContext == null);
Contract.Ensures(Contract.Result() != null);
currentModule = iter.Module;
codeContext = iter;
ExpressionTranslator etran = new ExpressionTranslator(this, predef, iter.tok);
List inParams, outParams;
GenerateMethodParametersChoose(iter.tok, iter, kind, true, true, false, etran, out inParams, out outParams);
var req = new List();
var mod = new List();
var ens = new List();
// FREE PRECONDITIONS
if (kind == MethodTranslationKind.SpecWellformedness || kind == MethodTranslationKind.Implementation) { // the other cases have no need for a free precondition
// free requires mh == ModuleContextHeight && fh = FunctionContextHeight;
req.Add(Requires(iter.tok, true, etran.HeightContext(iter), null, null));
}
mod.Add((Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr);
mod.Add(etran.Tick());
if (kind != MethodTranslationKind.SpecWellformedness) {
// USER-DEFINED SPECIFICATIONS
var comment = "user-defined preconditions";
foreach (var p in iter.Requires) {
if (p.IsFree && !DafnyOptions.O.DisallowSoundnessCheating) {
req.Add(Requires(p.E.tok, true, etran.TrExpr(p.E), null, comment));
comment = null;
} else {
bool splitHappened; // we actually don't care
foreach (var s in TrSplitExpr(p.E, etran, kind == MethodTranslationKind.InterModuleCall ? 0 : int.MaxValue, out splitHappened)) {
if (kind == MethodTranslationKind.IntraModuleCall && RefinementToken.IsInherited(s.E.tok, currentModule)) {
// this precondition was inherited into this module, so just ignore it
} else {
req.Add(Requires(s.E.tok, s.IsOnlyFree, s.E, null, comment));
comment = null;
// the free here is not linked to the free on the original expression (this is free things generated in the splitting.)
}
}
}
}
comment = "user-defined postconditions";
foreach (var p in iter.Ensures) {
if (p.IsFree && !DafnyOptions.O.DisallowSoundnessCheating) {
ens.Add(Ensures(p.E.tok, true, etran.TrExpr(p.E), null, comment));
comment = null;
} else {
bool splitHappened; // we actually don't care
foreach (var s in TrSplitExpr(p.E, etran, kind == MethodTranslationKind.InterModuleCall ? 0 : int.MaxValue, out splitHappened)) {
if (kind == MethodTranslationKind.Implementation && RefinementToken.IsInherited(s.E.tok, currentModule)) {
// this postcondition was inherited into this module, so just ignore it
} else {
ens.Add(Ensures(s.E.tok, s.IsOnlyFree, s.E, null, comment));
comment = null;
}
}
}
}
foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(iter.tok, iter.Modifies.Expressions, false, etran.Old, etran, etran.Old)) {
ens.Add(Ensures(tri.tok, tri.IsFree, tri.Expr, tri.ErrorMessage, tri.Comment));
}
}
var typeParams = TrTypeParamDecls(iter.TypeArgs);
var name = MethodName(iter, kind);
var proc = new Bpl.Procedure(iter.tok, name, typeParams, inParams, outParams, req, mod, ens, etran.TrAttributes(iter.Attributes, null));
currentModule = null;
codeContext = null;
return proc;
}
void AddIteratorWellformed(IteratorDecl iter, Procedure proc) {
currentModule = iter.Module;
codeContext = iter;
List typeParams = TrTypeParamDecls(iter.TypeArgs);
List inParams = Bpl.Formal.StripWhereClauses(proc.InParams);
Contract.Assert(1 <= inParams.Count); // there should at least be a receiver parameter
Contract.Assert(proc.OutParams.Count == 0);
var builder = new Bpl.StmtListBuilder();
var etran = new ExpressionTranslator(this, predef, iter.tok);
var localVariables = new List();
Bpl.StmtList stmts;
// check well-formedness of the preconditions, and then assume each one of them
foreach (var p in iter.Requires) {
CheckWellformed(p.E, new WFOptions(), localVariables, builder, etran);
builder.Add(new Bpl.AssumeCmd(p.E.tok, etran.TrExpr(p.E)));
}
// check well-formedness of the modifies and reads clauses
CheckFrameWellFormed(iter.Modifies.Expressions, localVariables, builder, etran);
CheckFrameWellFormed(iter.Reads.Expressions, localVariables, builder, etran);
// check well-formedness of the decreases clauses
foreach (var p in iter.Decreases.Expressions) {
CheckWellformed(p, new WFOptions(), localVariables, builder, etran);
}
// Next, we assume about this.* whatever we said that the iterator constructor promises
foreach (var p in iter.Member_Init.Ens) {
builder.Add(new Bpl.AssumeCmd(p.E.tok, etran.TrExpr(p.E)));
}
// play havoc with the heap, except at the locations prescribed by (this._reads - this._modifies - {this})
var th = new ThisExpr(iter.tok);
th.Type = Resolver.GetThisType(iter.tok, iter); // resolve here
var rds = new FieldSelectExpr(iter.tok, th, iter.Member_Reads.Name);
rds.Field = iter.Member_Reads; // resolve here
rds.Type = iter.Member_Reads.Type; // resolve here
var mod = new FieldSelectExpr(iter.tok, th, iter.Member_Modifies.Name);
mod.Field = iter.Member_Modifies; // resolve here
mod.Type = iter.Member_Modifies.Type; // resolve here
builder.Add(new Bpl.CallCmd(iter.tok, "$IterHavoc0",
new List() { etran.TrExpr(th), etran.TrExpr(rds), etran.TrExpr(mod) },
new List()));
// assume the automatic yield-requires precondition (which is always well-formed): this.Valid()
var validCall = new FunctionCallExpr(iter.tok, "Valid", th, iter.tok, new List());
validCall.Function = iter.Member_Valid; // resolve here
validCall.Type = Type.Bool; // resolve here
validCall.TypeArgumentSubstitutions = new Dictionary(); // resolve here
builder.Add(new Bpl.AssumeCmd(iter.tok, etran.TrExpr(validCall)));
// check well-formedness of the user-defined part of the yield-requires
foreach (var p in iter.YieldRequires) {
CheckWellformed(p.E, new WFOptions(), localVariables, builder, etran);
builder.Add(new Bpl.AssumeCmd(p.E.tok, etran.TrExpr(p.E)));
}
// save the heap (representing the state where yield-requires holds): $_OldIterHeap := Heap;
var oldIterHeap = new Bpl.LocalVariable(iter.tok, new Bpl.TypedIdent(iter.tok, "$_OldIterHeap", predef.HeapType));
localVariables.Add(oldIterHeap);
builder.Add(Bpl.Cmd.SimpleAssign(iter.tok, new Bpl.IdentifierExpr(iter.tok, oldIterHeap), etran.HeapExpr));
// simulate a modifies this, this._modifies, this._new;
var nw = new FieldSelectExpr(iter.tok, th, iter.Member_New.Name);
nw.Field = iter.Member_New; // resolve here
nw.Type = iter.Member_New.Type; // resolve here
builder.Add(new Bpl.CallCmd(iter.tok, "$IterHavoc1",
new List() { etran.TrExpr(th), etran.TrExpr(mod), etran.TrExpr(nw) },
new List()));
// assume the implicit postconditions promised by MoveNext:
// assume fresh(_new - old(_new));
var yeEtran = new ExpressionTranslator(this, predef, etran.HeapExpr, new Bpl.IdentifierExpr(iter.tok, "$_OldIterHeap", predef.HeapType));
var old_nw = new OldExpr(iter.tok, nw);
old_nw.Type = nw.Type; // resolve here
var setDiff = new BinaryExpr(iter.tok, BinaryExpr.Opcode.Sub, nw, old_nw);
setDiff.ResolvedOp = BinaryExpr.ResolvedOpcode.SetDifference; setDiff.Type = nw.Type; // resolve here
Expression cond = new FreshExpr(iter.tok, setDiff);
cond.Type = Type.Bool; // resolve here
builder.Add(new Bpl.AssumeCmd(iter.tok, yeEtran.TrExpr(cond)));
// check wellformedness of postconditions
var yeBuilder = new Bpl.StmtListBuilder();
var endBuilder = new Bpl.StmtListBuilder();
// In the yield-ensures case: assume this.Valid();
yeBuilder.Add(new Bpl.AssumeCmd(iter.tok, yeEtran.TrExpr(validCall)));
Contract.Assert(iter.OutsFields.Count == iter.OutsHistoryFields.Count);
for (int i = 0; i < iter.OutsFields.Count; i++) {
var y = iter.OutsFields[i];
var ys = iter.OutsHistoryFields[i];
var thisY = new FieldSelectExpr(iter.tok, th, y.Name);
thisY.Field = y; thisY.Type = y.Type; // resolve here
var thisYs = new FieldSelectExpr(iter.tok, th, ys.Name);
thisYs.Field = ys; thisYs.Type = ys.Type; // resolve here
var oldThisYs = new OldExpr(iter.tok, thisYs);
oldThisYs.Type = thisYs.Type; // resolve here
var singleton = new SeqDisplayExpr(iter.tok, new List() { thisY });
singleton.Type = thisYs.Type; // resolve here
var concat = new BinaryExpr(iter.tok, BinaryExpr.Opcode.Add, oldThisYs, singleton);
concat.ResolvedOp = BinaryExpr.ResolvedOpcode.Concat; concat.Type = oldThisYs.Type; // resolve here
// In the yield-ensures case: assume this.ys == old(this.ys) + [this.y];
yeBuilder.Add(new Bpl.AssumeCmd(iter.tok, Bpl.Expr.Eq(yeEtran.TrExpr(thisYs), yeEtran.TrExpr(concat))));
// In the ensures case: assume this.ys == old(this.ys);
endBuilder.Add(new Bpl.AssumeCmd(iter.tok, Bpl.Expr.Eq(yeEtran.TrExpr(thisYs), yeEtran.TrExpr(oldThisYs))));
}
foreach (var p in iter.YieldEnsures) {
CheckWellformed(p.E, new WFOptions(), localVariables, yeBuilder, yeEtran);
yeBuilder.Add(new Bpl.AssumeCmd(p.E.tok, yeEtran.TrExpr(p.E)));
}
foreach (var p in iter.Ensures) {
CheckWellformed(p.E, new WFOptions(), localVariables, endBuilder, yeEtran);
endBuilder.Add(new Bpl.AssumeCmd(p.E.tok, yeEtran.TrExpr(p.E)));
}
builder.Add(new Bpl.IfCmd(iter.tok, null, yeBuilder.Collect(iter.tok), null, endBuilder.Collect(iter.tok)));
stmts = builder.Collect(iter.tok);
QKeyValue kv = etran.TrAttributes(iter.Attributes, null);
Bpl.Implementation impl = new Bpl.Implementation(iter.tok, proc.Name,
typeParams, inParams, new List(),
localVariables, stmts, kv);
sink.TopLevelDeclarations.Add(impl);
currentModule = null;
codeContext = null;
loopHeapVarCount = 0;
otherTmpVarCount = 0;
_tmpIEs.Clear();
}
void AddIteratorImpl(IteratorDecl iter, Bpl.Procedure proc) {
Contract.Requires(iter != null);
Contract.Requires(proc != null);
Contract.Requires(sink != null && predef != null);
Contract.Requires(iter.Body != null);
Contract.Requires(currentModule == null && codeContext == null && yieldCountVariable == null && loopHeapVarCount == 0 && _tmpIEs.Count == 0);
Contract.Ensures(currentModule == null && codeContext == null && yieldCountVariable == null && loopHeapVarCount == 0 && _tmpIEs.Count == 0);
currentModule = iter.Module;
codeContext = iter;
List typeParams = TrTypeParamDecls(iter.TypeArgs);
List inParams = Bpl.Formal.StripWhereClauses(proc.InParams);
Contract.Assert(1 <= inParams.Count); // there should at least be a receiver parameter
Contract.Assert(proc.OutParams.Count == 0);
Bpl.StmtListBuilder builder = new Bpl.StmtListBuilder();
ExpressionTranslator etran = new ExpressionTranslator(this, predef, iter.tok);
List localVariables = new List();
GenerateIteratorImplPrelude(iter, inParams, new List(), builder, localVariables);
// add locals for the yield-history variables and the extra variables
// Assume the precondition and postconditions of the iterator constructor method
foreach (var p in iter.Member_Init.Req) {
builder.Add(new Bpl.AssumeCmd(p.E.tok, etran.TrExpr(p.E)));
}
foreach (var p in iter.Member_Init.Ens) {
// these postconditions are two-state predicates, but that's okay, because we haven't changed anything yet
builder.Add(new Bpl.AssumeCmd(p.E.tok, etran.TrExpr(p.E)));
}
// add the _yieldCount variable, and assume its initial value to be 0
yieldCountVariable = new Bpl.LocalVariable(iter.tok,
new Bpl.TypedIdent(iter.tok, iter.YieldCountVariable.AssignUniqueName(currentDeclaration), TrType(iter.YieldCountVariable.Type)));
yieldCountVariable.TypedIdent.WhereExpr = YieldCountAssumption(iter, etran); // by doing this after setting "yieldCountVariable", the variable can be used by YieldCountAssumption
localVariables.Add(yieldCountVariable);
builder.Add(new Bpl.AssumeCmd(iter.tok, Bpl.Expr.Eq(new Bpl.IdentifierExpr(iter.tok, yieldCountVariable), Bpl.Expr.Literal(0))));
// add a variable $_OldIterHeap
var oih = new Bpl.IdentifierExpr(iter.tok, "$_OldIterHeap", predef.HeapType);
Bpl.Expr wh = BplAnd(
FunctionCall(iter.tok, BuiltinFunction.IsGoodHeap, null, oih),
FunctionCall(iter.tok, BuiltinFunction.HeapSucc, null, oih, etran.HeapExpr));
localVariables.Add(new Bpl.LocalVariable(iter.tok, new Bpl.TypedIdent(iter.tok, "$_OldIterHeap", predef.HeapType, wh)));
// do an initial YieldHavoc
YieldHavoc(iter.tok, iter, builder, etran);
// translate the body of the method
var stmts = TrStmt2StmtList(builder, iter.Body, localVariables, etran);
QKeyValue kv = etran.TrAttributes(iter.Attributes, null);
Bpl.Implementation impl = new Bpl.Implementation(iter.tok, proc.Name,
typeParams, inParams, new List(),
localVariables, stmts, kv);
sink.TopLevelDeclarations.Add(impl);
currentModule = null;
codeContext = null;
yieldCountVariable = null;
loopHeapVarCount = 0;
otherTmpVarCount = 0;
_tmpIEs.Clear();
}
Bpl.Expr YieldCountAssumption(IteratorDecl iter, ExpressionTranslator etran) {
Contract.Requires(iter != null);
Contract.Requires(etran != null);
Contract.Requires(yieldCountVariable != null);
Bpl.Expr wh = Bpl.Expr.True;
foreach (var ys in iter.OutsHistoryFields) {
// add the conjunct: _yieldCount == |this.ys|
wh = Bpl.Expr.And(wh, Bpl.Expr.Eq(new Bpl.IdentifierExpr(iter.tok, yieldCountVariable),
FunctionCall(iter.tok, BuiltinFunction.SeqLength, null,
ExpressionTranslator.ReadHeap(iter.tok, etran.HeapExpr,
new Bpl.IdentifierExpr(iter.tok, etran.This, predef.RefType),
new Bpl.IdentifierExpr(iter.tok, GetField(ys))))));
}
return wh;
}
class Specialization
{
public readonly List Formals;
public readonly List ReplacementExprs;
public readonly List ReplacementFormals;
public readonly Dictionary SubstMap;
readonly Translator translator;
[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, Translator translator) {
Contract.Requires(formal is Formal || formal is BoundVar);
Contract.Requires(mc != null);
Contract.Requires(prev == null || formal is BoundVar || !prev.Formals.Contains((Formal)formal));
Contract.Requires(translator != null);
this.translator = translator;
List rArgs = new List();
foreach (BoundVar p in mc.Arguments) {
IdentifierExpr ie = new IdentifierExpr(p.tok, p.AssignUniqueName(translator.currentDeclaration));
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*/, null);
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(translator.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, translator.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, FunctionAxiomVisibility visibility, Expression body) {
Contract.Requires(f != null);
var ax = FunctionAxiom(f, visibility, body, null);
sink.TopLevelDeclarations.Add(ax);
// TODO(namin) Is checking f.Reads.Count==0 excluding Valid() of BinaryTree in the right way?
// I don't see how this in the decreasing clause would help there.
if (!(f is CoPredicate) && f.Reads.Count == 0) {
var FVs = new HashSet();
bool usesHeap = false, usesOldHeap = false;
Type usesThis = null;
foreach (var e in f.Decreases.Expressions) {
ComputeFreeVariables(e, FVs, ref usesHeap, ref usesOldHeap, ref usesThis, false);
}
var decs = new List();
foreach (var formal in f.Formals) {
if (FVs.Contains(formal)) {
decs.Add(formal);
}
}
Contract.Assert(decs.Count <= f.Formals.Count);
if (0 < decs.Count && decs.Count < f.Formals.Count) {
ax = FunctionAxiom(f, visibility, body, decs);
sink.TopLevelDeclarations.Add(ax);
}
ax = FunctionAxiom(f, visibility, body, f.Formals);
sink.TopLevelDeclarations.Add(ax);
}
}
enum FunctionAxiomVisibility { IntraModuleOnly, ForeignModuleOnly }
Bpl.Axiom FunctionConsequenceAxiom(Function f, List ens) {
Contract.Requires(f != null);
Contract.Requires(predef != null);
Contract.Requires(f.EnclosingClass != null);
Contract.Ensures(Contract.Result() != null);
ExpressionTranslator etran = new ExpressionTranslator(this, predef, f.tok);
// This method generate the Consequence Axiom, which has information about the function's
// return type and postconditions
//
// axiom // consequence axiom
// AXIOM_ACTIVATION
// ==>
// (forall s, $Heap, formals :: // let args := $Heap,formals
// { f(s, args) }
// f#canCall(args) || USE_VIA_CONTEXT
// ==>
// ens &&
// f(s, args)-has-the-expected type);
//
// where:
//
// AXIOM_ACTIVATION
// means:
// mh < ModuleContextHeight ||
// (mh == ModuleContextHeight && fh <= FunctionContextHeight)
//
// USE_VIA_CONTEXT
// (mh != ModuleContextHeight || fh != FunctionContextHeight) &&
// GOOD_PARAMETERS
// where GOOD_PARAMETERS means:
// $IsGoodHeap($Heap) && this != null && formals-have-the-expected-types &&
// Pre($Heap,formals)
//
// 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.
//
var formals = new List();
var args = new List();
Bpl.BoundVariable layer;
if (f.IsRecursive) {
layer = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$ly", predef.LayerType));
formals.Add(layer);
// Note, "layer" is not added to "args" here; rather, that's done below, as needed
} else {
layer = null;
}
var 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: $IsGoodHeap($Heap) && this != null && formals-have-the-expected-types &&
Bpl.Expr ante = FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, etran.HeapExpr);
if (!f.IsStatic) {
var bvThis = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, etran.This, predef.RefType));
formals.Add(bvThis);
var 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);
}
var substMap = new Dictionary();
foreach (Formal p in f.Formals) {
bv = new Bpl.BoundVariable(p.tok, new Bpl.TypedIdent(p.tok, p.AssignUniqueName(currentDeclaration), TrType(p.Type)));
Bpl.Expr formal = new Bpl.IdentifierExpr(p.tok, bv);
formals.Add(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); }
}
Bpl.Expr funcAppl;
{
var funcID = new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName, TrType(f.ResultType));
var funcArgs = new List();
if (layer != null) {
var ly = new Bpl.IdentifierExpr(f.tok, layer);
funcArgs.Add(FunctionCall(f.tok, BuiltinFunction.LayerSucc, null, ly));
}
funcArgs.AddRange(args);
funcAppl = new Bpl.NAryExpr(f.tok, new Bpl.FunctionCall(funcID), funcArgs);
}
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)
var mod = f.EnclosingClass.Module;
Bpl.Expr useViaContext = 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()));
// useViaCanCall: f#canCall(args)
Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName + "#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 List { funcAppl });
var typeParams = TrTypeParamDecls(f.TypeArgs);
Bpl.Expr meat = Bpl.Expr.True;
foreach (Expression p in ens) {
Bpl.Expr q = etran.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));
var activate = AxiomActivation(f, true, true, etran);
string comment = "consequence axiom for " + f.FullSanitizedName;
return new Bpl.Axiom(f.tok, Bpl.Expr.Imp(activate, ax), comment);
}
Bpl.Expr AxiomActivation(Function f, bool interModule, bool intraModule, ExpressionTranslator etran) {
Contract.Requires(f != null);
Contract.Requires(interModule || intraModule);
Contract.Requires(etran != null);
var module = f.EnclosingClass.Module;
// mh < ModuleContextHeight
var activateForeignModule = Bpl.Expr.Lt(Bpl.Expr.Literal(module.Height), etran.ModuleContextHeight());
// mh == ModuleContextHeight && fh <= FunctionContextHeight
var activateIntraModule = Bpl.Expr.And(
Bpl.Expr.Eq(Bpl.Expr.Literal(module.Height), etran.ModuleContextHeight()),
Bpl.Expr.Le(Bpl.Expr.Literal(module.CallGraph.GetSCCRepresentativeId(f)), etran.FunctionContextHeight()));
if (interModule && !intraModule) {
return activateForeignModule;
} else if (!interModule && intraModule) {
return activateIntraModule;
} else {
return Bpl.Expr.Or(activateForeignModule, activateIntraModule);
}
}
Bpl.Axiom FunctionAxiom(Function f, FunctionAxiomVisibility visibility, Expression body, ICollection lits) {
Contract.Requires(f != null);
Contract.Requires(predef != null);
Contract.Requires(f.EnclosingClass != null);
Contract.Requires(body != null);
Contract.Ensures(Contract.Result() != null);
ExpressionTranslator etran = new ExpressionTranslator(this, predef, f.tok);
// This method generates the Definition Axiom, suitably modified according to the optional "lits".
//
// axiom // definition axiom
// AXIOM_ACTIVATION
// ==>
// (forall s, $Heap, formals :: // let args := $Heap,formals
// { f(Succ(s), args) } // (*)
// f#canCall(args) || USE_VIA_CONTEXT
// ==>
// BODY-can-make-its-calls &&
// f(Succ(s), args) == BODY); // (*)
//
// where:
//
// AXIOM_ACTIVATION
// for visibility==ForeignModuleOnly, means:
// mh < ModuleContextHeight
// for visibility==IntraModuleOnly, means:
// mh == ModuleContextHeight && fh <= FunctionContextHeight
//
// USE_VIA_CONTEXT
// for visibility==ForeignModuleOnly, means:
// GOOD_PARAMETERS
// for visibility==IntraModuleOnly, means:
// fh != FunctionContextHeight &&
// GOOD_PARAMETERS
// where GOOD_PARAMETERS means:
// $IsGoodHeap($Heap) && this != null && formals-have-the-expected-types &&
// Pre($Heap,formals)
//
// BODY
// means:
// the body of f translated with "s" as the layer argument
//
// The variables "formals" are the formals of function "f".
// The list "args" is the list of formals of function "f".
//
// The translation of "body" uses "s" as the layer argument for intra-cluster calls and the default layer argument
// (which is Succ(0)) for other calls. Usually, the layer argument in the LHS of the definition (and also in the trigger,
// see the two occurrences of (*) above) use Succ(s) as the layer argument. However, if "lits" are specified, then
// then the argument used is just "s" (in both the LHS and trigger).
//
// 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.
//
var formals = new List();
var args = new List();
Bpl.BoundVariable layer;
if (f.IsRecursive) {
layer = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$ly", predef.LayerType));
formals.Add(layer);
// Note, "layer" is not added to "args" here; rather, that's done below, as needed
} else {
layer = null;
}
var 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: $IsGoodHeap($Heap) && this != null && formals-have-the-expected-types &&
Bpl.Expr ante = FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, etran.HeapExpr);
if (!f.IsStatic) {
var bvThis = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, etran.This, predef.RefType));
formals.Add(bvThis);
var 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);
}
var substMap = new Dictionary();
foreach (Formal p in f.Formals) {
bv = new Bpl.BoundVariable(p.tok, new Bpl.TypedIdent(p.tok, p.AssignUniqueName(currentDeclaration), TrType(p.Type)));
formals.Add(bv);
Bpl.Expr formal = new Bpl.IdentifierExpr(p.tok, bv);
if (lits != null && lits.Contains(p) && !substMap.ContainsKey(p)) {
args.Add(Lit(formal));
var ie = new IdentifierExpr(p.tok, p.AssignUniqueName(f));
ie.Var = p; ie.Type = ie.Var.Type;
var l = new UnaryExpr(p.tok, UnaryExpr.Opcode.Lit, ie);
l.Type = ie.Var.Type;
substMap.Add(p, l);
} else {
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); }
}
Bpl.Expr funcAppl;
{
var funcID = new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName, TrType(f.ResultType));
var funcArgs = new List();
if (layer != null) {
var ly = new Bpl.IdentifierExpr(f.tok, layer);
if (lits == null) {
funcArgs.Add(FunctionCall(f.tok, BuiltinFunction.LayerSucc, null, ly));
} else {
funcArgs.Add(ly);
}
}
funcArgs.AddRange(args);
funcAppl = new Bpl.NAryExpr(f.tok, new Bpl.FunctionCall(funcID), funcArgs);
}
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)
ModuleDefinition mod = f.EnclosingClass.Module;
Bpl.Expr useViaContext = visibility == FunctionAxiomVisibility.ForeignModuleOnly ? (Bpl.Expr)Bpl.Expr.True :
Bpl.Expr.Neq(Bpl.Expr.Literal(mod.CallGraph.GetSCCRepresentativeId(f)), etran.FunctionContextHeight());
// useViaCanCall: f#canCall(args)
Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName + "#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 List { funcAppl });
var typeParams = TrTypeParamDecls(f.TypeArgs);
Bpl.Expr meat;
if (visibility == FunctionAxiomVisibility.ForeignModuleOnly /* TODO: add 'public' feature and add: && !IsPublic(f) */) {
meat = Bpl.Expr.True;
} else {
var bodyWithSubst = Substitute(body, null, substMap);
if (f is PrefixPredicate) {
var pp = (PrefixPredicate)f;
bodyWithSubst = PrefixSubstitution(pp, bodyWithSubst);
}
var etranBody = layer == null ? etran : etran.LimitedFunctions(f, new Bpl.IdentifierExpr(f.tok, layer));
meat = BplAnd(CanCallAssumption(bodyWithSubst, etran),
Bpl.Expr.Eq(funcAppl, etranBody.TrExpr(bodyWithSubst)));
}
QKeyValue kv = null;
if (lits != null) {
kv = new QKeyValue(f.tok, "weight", new List