//-----------------------------------------------------------------------------
//
// 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() {
InsertChecksums = 0 < CommandLineOptions.Clo.VerifySnapshots;
Bpl.Program boogieProgram = ReadPrelude();
if (boogieProgram != null) {
sink = boogieProgram;
predef = FindPredefinedDecls(boogieProgram);
}
}
// translation state
readonly Dictionary/*!*/ classes = new Dictionary();
readonly Dictionary/*!*/ classConstants = new Dictionary();
readonly Dictionary functionConstants = new Dictionary();
readonly Dictionary functionHandles = new Dictionary();
readonly Dictionary/*!*/ fields = new Dictionary();
readonly Dictionary/*!*/ fieldFunctions = new Dictionary();
readonly Dictionary fieldConstants = new Dictionary();
readonly ISet abstractTypes = new HashSet();
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 HandleType;
public readonly Bpl.Type LayerType;
public readonly Bpl.Type DtCtorId;
public readonly Bpl.Type Ty;
public readonly Bpl.Type TyTag;
public readonly Bpl.Expr Null;
private readonly Bpl.Constant allocField;
[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(HeapVarName != null);
Contract.Invariant(ClassNameType != null);
Contract.Invariant(NameFamilyType != null);
Contract.Invariant(DatatypeType != null);
Contract.Invariant(HandleType != null);
Contract.Invariant(LayerType != null);
Contract.Invariant(DtCtorId != null);
Contract.Invariant(Ty != null);
Contract.Invariant(TyTag != null);
Contract.Invariant(Null != null);
Contract.Invariant(allocField != 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.TypeCtorDecl tyType, Bpl.TypeCtorDecl tyTagType,
Bpl.GlobalVariable heap, Bpl.TypeCtorDecl classNameType, Bpl.TypeCtorDecl nameFamilyType,
Bpl.TypeCtorDecl datatypeType, Bpl.TypeCtorDecl handleType, Bpl.TypeCtorDecl layerType, Bpl.TypeCtorDecl dtCtorId,
Bpl.Constant allocField) {
#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(tyType != null);
Contract.Requires(tyTagType != 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.Ty = new Bpl.CtorType(Token.NoToken, tyType, new List());
this.TyTag = new Bpl.CtorType(Token.NoToken, tyTagType, new List());
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.HandleType = new Bpl.CtorType(Token.NoToken, handleType, 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);
}
}
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 tyType = null;
Bpl.TypeCtorDecl tyTagType = null;
Bpl.TypeCtorDecl nameFamilyType = null;
Bpl.TypeCtorDecl datatypeType = null;
Bpl.TypeCtorDecl handleType = 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;
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 == "Ty") {
tyType = dt;
} else if (dt.Name == "TyTag") {
tyTagType = dt;
} else if (dt.Name == "DatatypeType") {
datatypeType = dt;
} else if (dt.Name == "HandleType") {
handleType = 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 == "Box") {
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 (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 (tyType == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of type Ty");
} else if (tyTagType == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of type TyTag");
} 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 (handleType == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of type HandleType");
} 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 Box");
} 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 {
return new PredefinedDecls(refType, boxType, tickType,
setTypeCtor, multiSetTypeCtor, mapTypeCtor, arrayLength, seqTypeCtor, fieldNameType, tyType, tyTagType, heap, classNameType, nameFamilyType, datatypeType, handleType, layerType, dtCtorId,
allocField);
}
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 (var ad in ArrowType.ArrowTypeDecls) {
currentDeclaration = ad;
GetClassTyCon(ad);
AddArrowTypeAxioms(ad);
}
foreach (TopLevelDecl d in program.BuiltIns.SystemModule.TopLevelDecls) {
currentDeclaration = d;
if (d is OpaqueTypeDecl) {
AddTypeDecl((OpaqueTypeDecl)d);
} 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 OpaqueTypeDecl) {
AddTypeDecl((OpaqueTypeDecl)d);
} else if (d is TypeSynonymDecl) {
// do nothing, just bypass type synonyms in the translation
} 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", "stable");
}
var func = decl as Bpl.Function;
if (func != null && func.FindStringAttribute("checksum") == null)
{
func.AddAttribute("checksum", "stable");
}
}
}
return sink;
}
void AddTypeDecl(OpaqueTypeDecl td) {
Contract.Requires(td != null);
string nm = nameTypeParam(td.TheType);
if (abstractTypes.Contains(nm)) {
// nothing to do; has already been added
return;
}
if (td.TypeArgs.Count == 0) {
sink.TopLevelDeclarations.Add(
new Bpl.Constant(td.tok,
new TypedIdent(td.tok, nm, predef.Ty), false /* not unique */));
} else {
// Note, the function produced is NOT necessarily injective, because the type may be replaced
// in a refinement module in such a way that the type arguments do not matter.
var args = new List(td.TypeArgs.ConvertAll(a => (Bpl.Variable)BplFormalVar(null, predef.Ty, true)));
var func = new Bpl.Function(td.tok, nm, args, BplFormalVar(null, predef.Ty, false));
sink.TopLevelDeclarations.Add(func);
}
abstractTypes.Add(nm);
}
void AddDatatype(DatatypeDecl dt) {
Contract.Requires(dt != null);
Contract.Requires(sink != null && predef != null);
Bpl.Constant dt_const = GetClass(dt);
sink.TopLevelDeclarations.Add(dt_const);
foreach (DatatypeCtor ctor in dt.Ctors) {
int i;
// Add: function #dt.ctor(tyVars, 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, "Constructor function declaration");
if (InsertChecksums) {
InsertChecksum(dt, fn);
}
sink.TopLevelDeclarations.Add(fn);
List bvs;
List args;
{
// Add: const unique ##dt.ctor: DtCtorId;
Bpl.Constant cid = new Bpl.Constant(ctor.tok, new Bpl.TypedIdent(ctor.tok, "#" + ctor.FullName, predef.DtCtorId), true);
Bpl.Expr c = new Bpl.IdentifierExpr(ctor.tok, cid);
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, c);
sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, BplForall(bvs, q), "Constructor identifier"));
}
{
// 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:
Bpl.Expr th; var thVar = BplBoundVar("d", predef.DatatypeType, out th);
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, c);
var body = Bpl.Expr.Iff(queryPredicate, rhs);
var tr = BplTrigger(queryPredicate);
var ax = BplForall(thVar, tr, body);
sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, ax, "Questionmark and identifier"));
}
}
{
// Add: axiom (forall d: DatatypeType :: dt.ctor?(d) ==> (exists params :: d == #dt.ctor(params));
CreateBoundVariables(ctor.Formals, out bvs, out args);
Bpl.Expr lhs = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);
Bpl.Expr dId; var dBv = BplBoundVar("d", predef.DatatypeType, out dId);
Bpl.Expr q = Bpl.Expr.Eq(dId, lhs);
if (bvs.Count != 0) {
q = new Bpl.ExistsExpr(ctor.tok, bvs, q);
}
Bpl.Expr dtq = FunctionCall(ctor.tok, ctor.QueryField.FullSanitizedName, Bpl.Type.Bool, dId);
q = BplForall(dBv, null, BplImp(dtq, q));
sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, q, "Constructor questionmark has arguments"));
}
MapM(Bools, is_alloc => {
/*
(forall x0 : C0, ..., xn : Cn, G : Ty •
{ $Is(C(x0,...,xn), T(G)) }
$Is(C(x0,...,xn), T(G)) <==>
$Is[Box](x0, C0(G)) && ... && $Is[Box](xn, Cn(G)));
(forall x0 : C0, ..., xn : Cn, G : Ty •
{ $IsAlloc(C(G, x0,...,xn), T(G)) }
$IsAlloc(C(G, x0,...,xn), T(G)) ==>
$IsAlloc[Box](x0, C0(G)) && ... && $IsAlloc[Box](xn, Cn(G)));
*/
List tyexprs;
var tyvars = MkTyParamBinders(dt.TypeArgs, out tyexprs);
CreateBoundVariables(ctor.Formals, out bvs, out args);
Bpl.Expr h;
var hVar = BplBoundVar("$h", predef.HeapType, out h);
Bpl.Expr conj = Bpl.Expr.True;
i = 0;
foreach (Formal arg in ctor.Formals) {
if (is_alloc) {
conj = BplAnd(conj, MkIsAlloc(args[i], arg.Type, h));
} else {
conj = BplAnd(conj, MkIs(args[i], arg.Type));
}
i++;
}
var c_params = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);
var c_ty = ClassTyCon((TopLevelDecl)dt, tyexprs);
bvs.InsertRange(0, tyvars);
if (!is_alloc) {
var c_is = MkIs(c_params, c_ty);
sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok,
BplForall(bvs, BplTrigger(c_is), BplIff(c_is, conj)),
"Constructor $Is"));
} else if (is_alloc) {
var isGoodHeap = FunctionCall(ctor.tok, BuiltinFunction.IsGoodHeap, null, h);
var c_alloc = MkIsAlloc(c_params, c_ty, h);
bvs.Add(hVar);
sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok,
BplForall(bvs, BplTrigger(c_alloc),
BplImp(isGoodHeap, BplIff(c_alloc, conj))),
"Constructor $IsAlloc"));
}
});
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);
var litargs = new List();
foreach (Bpl.Expr arg in args) {
litargs.Add(Lit(arg));
}
Bpl.Expr lhs = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, litargs);
Bpl.Expr rhs = Lit(FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args), predef.DatatypeType);
Bpl.Expr q = BplForall(bvs, BplTrigger(lhs), Bpl.Expr.Eq(lhs, rhs));
sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, q, "Constructor literal"));
}
// Injectivity axioms for normal arguments
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);
var inner = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);
var outer = FunctionCall(ctor.tok, fn.Name, TrType(arg.Type), inner);
var q = BplForall(bvs, BplTrigger(inner), Bpl.Expr.Eq(outer, args[i]));
sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, q, "Constructor injectivity"));
if (dt is IndDatatypeDecl) {
var argType = arg.Type.NormalizeExpand();
if (argType.IsDatatype || argType.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);
Bpl.Expr lhs = FunctionCall(ctor.tok, arg.Type.IsDatatype ? BuiltinFunction.DtRank : BuiltinFunction.BoxRank, null, args[i]);
/* CHECK
Bpl.Expr lhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null,
argType.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, "Inductive rank"));
} else if (argType 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])));
Bpl.Expr 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, "Inductive seq rank"));
} else if (argType 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));
Bpl.Expr 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, "Inductive set rank"));
} else if (argType 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));
Bpl.Expr 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, "Inductive multiset rank"));
}
}
i++;
}
}
{
// Add:
// function $IsA#Dt(G: Ty,d: DatatypeType): bool {
// Dt.Ctor0?(G, d) || Dt.Ctor1?(G, d) || ...
// }
var cases_dBv = new Bpl.Formal(dt.tok, new Bpl.TypedIdent(dt.tok, Bpl.TypedIdent.NoName, 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,
"One-depth case-split function");
if (InsertChecksums) {
InsertChecksum(dt, cases_fn);
}
sink.TopLevelDeclarations.Add(cases_fn);
// and here comes the actual axiom:
{
Bpl.Expr d;
var dVar = BplBoundVar("d", predef.DatatypeType, out d);
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 ax = BplForall(new List { dVar }, BplTrigger(lhs), BplImp(lhs, cases_body));
sink.TopLevelDeclarations.Add(new Bpl.Axiom(dt.tok, ax, "One-depth case-split axiom"));
}
}
// 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 G: Ty, d: DatatypeType ::
// { Dt.Ctor0?(G,d) }
// { Dt.Ctor1?(G,d) }
// $Is(d, T(G)) ==> Dt.Ctor0?(G,d) || Dt.Ctor1?(G,d) || ...);
{
List tyexprs;
var tyvars = MkTyParamBinders(dt.TypeArgs, out tyexprs);
Bpl.Expr d;
var dVar = BplBoundVar("d", predef.DatatypeType, out d);
var d_is = MkIs(d, ClassTyCon(dt, tyexprs));
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, d_is }, tr);
}
var body = Bpl.Expr.Imp(d_is, cases_body);
var ax = BplForall(Snoc(tyvars, dVar), tr, body);
sink.TopLevelDeclarations.Add(new Bpl.Axiom(dt.tok, ax, "Questionmark data type disjunctivity"));
}
if (dt is CoDatatypeDecl) {
var codecl = (CoDatatypeDecl)dt;
Func MinusOne = k => {
if (k == null) {
return null;
} else {
return Bpl.Expr.Sub(k, Bpl.Expr.Literal(1));
};
};
Action, List>, List, List, List, Bpl.Variable, Bpl.Expr, Bpl.Expr, Bpl.Expr, Bpl.Expr, Bpl.Expr>> CoAxHelper = (add_k, K) => {
Func> renew = s =>
Map(codecl.TypeArgs, tp =>
new TypeParameter(tp.tok, tp.Name + "#" + s, tp.PositionalIndex, tp.Parent));
List typaramsL = renew("l"), typaramsR = renew("r");
List lexprs; var lvars = MkTyParamBinders(typaramsL, out lexprs);
List rexprs; var rvars = MkTyParamBinders(typaramsR, out rexprs);
Func, List> Types = l => Map(l, tp => (Type)new UserDefinedType(tp));
var tyargs = Tuple.Create(Types(typaramsL), Types(typaramsR));
var vars = Concat(lvars, rvars);
Bpl.Expr k, kGtZero;
Bpl.Variable kVar;
if (add_k) {
kVar = BplBoundVar("k", Bpl.Type.Int, out k); vars.Add(kVar);
kGtZero = Bpl.Expr.Lt(Bpl.Expr.Literal(0), k);
} else {
kVar = null; k = null; kGtZero = Bpl.Expr.True;
}
var ly = BplBoundVar("ly", predef.LayerType, vars);
var d0 = BplBoundVar("d0", predef.DatatypeType, vars);
var d1 = BplBoundVar("d1", predef.DatatypeType, vars);
K(tyargs, vars, lexprs, rexprs, kVar, k, kGtZero, ly, d0, d1);
};
Action AddAxioms = add_k => {
{
// Add two copies of the type parameter lists!
var args = MkTyParamFormals(Concat(GetTypeParams(dt), GetTypeParams(dt)), false);
if (add_k) {
args.Add(BplFormalVar(null, Bpl.Type.Int, true));
}
args.Add(BplFormalVar(null, predef.LayerType, true));
args.Add(BplFormalVar(null, predef.DatatypeType, true));
args.Add(BplFormalVar(null, predef.DatatypeType, true));
var r = BplFormalVar(null, Bpl.Type.Bool, false);
var fn_nm = add_k ? CoPrefixName(codecl) : CoEqualName(codecl);
var fn = new Bpl.Function(dt.tok, fn_nm, args, r);
if (InsertChecksums) {
InsertChecksum(dt, fn);
}
sink.TopLevelDeclarations.Add(fn);
}
// axiom (forall G0,...,Gn : Ty, k: int, ly : Layer, d0, d1: DatatypeType ::
// { Eq(G0, .., Gn, S(ly), k, d0, d1) }
// Is(d0, T(G0, .., Gn)) && Is(d1, T(G0, ... Gn)) ==>
// (Eq(G0, .., Gn, S(ly), k, d0, d1)
// <==>
// 0 < k ==>
// (d0.Nil? && d1.Nil?) ||
// (d0.Cons? && d1.Cons? && d0.head == d1.head && Eq(G0, .., Gn, ly, k-1, d0.tail, d1.tail)))
CoAxHelper(add_k, (tyargs, vars, lexprs, rexprs, kVar, k, kGtZero, ly, d0, d1) => {
var eqDt = CoEqualCall(codecl, lexprs, rexprs, k, LayerSucc(ly), d0, d1);
var iss = BplAnd(MkIs(d0, ClassTyCon(dt, lexprs)), MkIs(d1, ClassTyCon(dt, rexprs)));
var body = BplImp(
iss,
BplIff(eqDt,
BplImp(kGtZero, BplOr(CoPrefixEquality(dt.tok, codecl, tyargs.Item1, tyargs.Item2, MinusOne(k), ly, d0, d1)))));
var ax = BplForall(vars, BplTrigger(eqDt), body);
sink.TopLevelDeclarations.Add(new Bpl.Axiom(dt.tok, ax, "Layered co-equality axiom"));
});
// axiom (forall G0,...,Gn : Ty, k: int, ly : Layer, d0, d1: DatatypeType ::
// { Eq(G0, .., Gn, S(ly), k, d0, d1) }
// 0 < k ==>
// (Eq(G0, .., Gn, S(ly), k, d0, d1) <==>
// Eq(G0, .., Gn, ly, k, d0, d))
CoAxHelper(add_k, (tyargs, vars, lexprs, rexprs, kVar, k, kGtZero, ly, d0, d1) => {
var eqDtSL = CoEqualCall(codecl, lexprs, rexprs, k, LayerSucc(ly), d0, d1);
var eqDtL = CoEqualCall(codecl, lexprs, rexprs, k, ly, d0, d1);
var body = BplImp(kGtZero, BplIff(eqDtSL, eqDtL));
var ax = BplForall(vars, BplTrigger(eqDtSL), body);
sink.TopLevelDeclarations.Add(new Bpl.Axiom(dt.tok, ax, "Unbump layer co-equality axiom"));
});
};
AddAxioms(false); // Add the above axioms for $Equal
// axiom (forall d0, d1: DatatypeType, k: int :: { $Equal(d0, d1) } :: Equal(d0, d1) <==> d0 == d1);
CoAxHelper(false, (tyargs, vars, lexprs, rexprs, kVar, k, kGtZero, ly, d0, d1) => {
var Eq = CoEqualCall(codecl, lexprs, rexprs, k, LayerSucc(ly), d0, d1);
var equal = Bpl.Expr.Eq(d0, d1);
sink.TopLevelDeclarations.Add(new Axiom(dt.tok,
BplForall(vars, BplTrigger(Eq), BplIff(Eq, equal)),
"Equality for codatatypes"));
});
AddAxioms(true); // Add the above axioms for $PrefixEqual
// 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)));
CoAxHelper(true, (tyargs, vars, lexprs, rexprs, kVar, k, kGtZero, ly, d0, d1) => {
var Eq = CoEqualCall(codecl, lexprs, rexprs, null, LayerSucc(ly), d0, d1);
var PEq = CoEqualCall(codecl, lexprs, rexprs, k, LayerSucc(ly), d0, d1);
vars.Remove(kVar);
sink.TopLevelDeclarations.Add(new Axiom(dt.tok,
BplForall(vars, BplTrigger(Eq), BplIff(Eq, BplForall(kVar, BplTrigger(PEq), BplImp(kGtZero, PEq)))),
"Coequality and prefix equality connection"));
});
// 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));
CoAxHelper(true, (tyargs, vars, lexprs, rexprs, kVar, k, kGtZero, ly, d0, d1) => {
var m = BplBoundVar("m", Bpl.Type.Int, vars);
var PEqK = CoEqualCall(codecl, lexprs, rexprs, k, LayerSucc(ly), d0, d1);
var PEqM = CoEqualCall(codecl, lexprs, rexprs, m, LayerSucc(ly), d0, d1);
var kLtM = Bpl.Expr.Lt(k, m);
sink.TopLevelDeclarations.Add(new Axiom(dt.tok,
BplForall(vars,
new Bpl.Trigger(dt.tok, true, new List { PEqK, PEqM }),
BplImp(BplAnd(BplAnd(kGtZero, kLtM), PEqM), PEqK)),
"Prefix equality consequence"));
});
// 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));
CoAxHelper(true, (tyargs, vars, lexprs, rexprs, kVar, k, kGtZero, ly, d0, d1) => {
var equal = Bpl.Expr.Eq(d0, d1);
var PEq = CoEqualCall(codecl, lexprs, rexprs, k, LayerSucc(ly), d0, d1);
sink.TopLevelDeclarations.Add(new Axiom(dt.tok,
BplForall(vars, null, BplImp(BplAnd(equal, kGtZero), PEq)),
"Prefix equality shortcut"));
});
}
}
///
/// 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, List largs, List rargs, Bpl.Expr k, Bpl.Expr l, Bpl.Expr A, Bpl.Expr B, bool conjuncts = false) {
Contract.Requires(tok != null);
Contract.Requires(dt != null);
Contract.Requires(A != null);
Contract.Requires(B != null);
Contract.Requires(l != null);
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 with conjucts=false (default):
// (A.Nil? && B.Nil?) ||
// (A.Cons? && B.Cons? && A.head == B.head && Equal(k, A.tail, B.tail))
//
// with conjuncts=true:
// (A.Nil? ==> B.Nil?) &&
// (A.Cons? ==> (B.Cons? && A.head == B.head && Equal(k, A.tail, B.tail)))
Dictionary lsu = Util.Dict(GetTypeParams(dt), largs);
Dictionary rsu = Util.Dict(GetTypeParams(dt), rargs);
foreach (var ctor in dt.Ctors) {
Bpl.Expr aq = new Bpl.NAryExpr(tok, new Bpl.FunctionCall(GetReadonlyField(ctor.QueryField)), new List { A });
Bpl.Expr bq = new Bpl.NAryExpr(tok, new Bpl.FunctionCall(GetReadonlyField(ctor.QueryField)), new List { B });
Bpl.Expr chunk = Bpl.Expr.True;
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;
var codecl = ty.AsCoDatatype;
if (codecl != null && codecl.SscRepr == dt.SscRepr) {
var lexprs = Map(ty.TypeArgs, tt => Resolver.SubstType(tt, lsu));
var rexprs = Map(ty.TypeArgs, tt => Resolver.SubstType(tt, rsu));
q = CoEqualCall(codecl, lexprs, rexprs, k, l, a, b);
} else {
// 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);
}
chunk = BplAnd(chunk, q);
}
if (conjuncts) {
yield return Bpl.Expr.Binary(new NestedToken(tok, ctor.tok), BinaryOperator.Opcode.Imp, aq, BplAnd(bq, chunk));
} else {
yield return BplAnd(BplAnd(aq, bq), BplImp(BplAnd(aq, bq), chunk));
}
}
}
Bpl.Expr LayerSucc(Bpl.Expr e, int amt = 1) {
if (amt == 0) {
return e;
} else if (amt > 0) {
return FunctionCall(e.tok, BuiltinFunction.LayerSucc, null, LayerSucc(e, amt-1));
} else {
Contract.Assert(false);
return null;
}
}
// Makes a call to equality, if k is null, or otherwise prefix equality. For codatatypes.
Bpl.Expr CoEqualCall(CoDatatypeDecl codecl, List largs, List rargs, Bpl.Expr k, Bpl.Expr l, Bpl.Expr A, Bpl.Expr B, IToken tok = null) {
Contract.Requires(codecl != null);
Contract.Requires(largs != null);
Contract.Requires(rargs != null);
Contract.Requires(l != null);
Contract.Requires(A != null);
Contract.Requires(B != null);
if (tok == null) {
tok = A.tok;
}
List args = Concat(largs, rargs);
if (k != null) {
args.Add(k);
}
args.AddRange(new List { l, A, B });
var fn = k == null ? CoEqualName(codecl) : CoPrefixName(codecl);
return FunctionCall(tok, fn, Bpl.Type.Bool, args);
}
// Same as above, but with Dafny-typed type-argument lists
Bpl.Expr CoEqualCall(CoDatatypeDecl codecl, List largs, List rargs, Bpl.Expr k, Bpl.Expr l, Bpl.Expr A, Bpl.Expr B, IToken tok = null) {
Contract.Requires(codecl != null);
Contract.Requires(largs != null);
Contract.Requires(rargs != null);
Contract.Requires(l != null);
Contract.Requires(A != null);
Contract.Requires(B != null);
return CoEqualCall(codecl, Map(largs, TypeToTy), Map(rargs, TypeToTy), k, l, A, B, tok);
}
static string CoEqualName(CoDatatypeDecl codecl) {
Contract.Requires(codecl != null);
return "$Eq#" + codecl.FullSanitizedName;
}
static string CoPrefixName(CoDatatypeDecl codecl) {
Contract.Requires(codecl != null);
return "$PrefixEq#" + 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));
}
}
// This one says that this is /directly/ allocated, not that its "children" are,
// i.e. h[x, alloc]
public Bpl.Expr IsAlloced(IToken tok, Bpl.Expr heapExpr, Bpl.Expr e) {
Contract.Requires(tok != null);
Contract.Requires(e != null);
Contract.Ensures(Contract.Result() != null);
return ReadHeap(tok, heapExpr, e, predef.Alloc(tok));
}
public static Bpl.NAryExpr ReadHeap(IToken tok, Expr heap, Expr r, Expr f) {
Contract.Requires(tok != null);
Contract.Requires(heap != null);
Contract.Requires(r != null);
Contract.Requires(f != null);
Contract.Ensures(Contract.Result() != null);
List args = new List();
args.Add(heap);
args.Add(r);
args.Add(f);
Bpl.Type t = (f.Type != null) ? f.Type : f.ShallowType;
return new Bpl.NAryExpr(tok,
new Bpl.FunctionCall(new Bpl.IdentifierExpr(tok, "read", t.AsCtor.Arguments[0])),
args);
}
public Bpl.Expr DType(Bpl.Expr e, Bpl.Expr type) {
return Bpl.Expr.Eq(FunctionCall(e.tok, BuiltinFunction.DynamicType, null, e), type);
}
public Bpl.Expr GetArrayIndexFieldName(IToken tok, List indices) {
Bpl.Expr fieldName = null;
foreach (Bpl.Expr index in indices) {
if (fieldName == null) {
// the index in dimension 0: IndexField(index0)
fieldName = FunctionCall(tok, BuiltinFunction.IndexField, null, index);
} else {
// the index in dimension n: MultiIndexField(...field name for first n indices..., index_n)
fieldName = FunctionCall(tok, BuiltinFunction.MultiIndexField, null, fieldName, index);
}
}
return fieldName;
}
void AddClassMembers(ClassDecl c)
{
Contract.Requires(sink != null && predef != null);
Contract.Requires(c != null);
sink.TopLevelDeclarations.Add(GetClass(c));
if (c is ArrayClassDecl) {
// classes.Add(c, predef.ClassDotArray);
AddAllocationAxiom(null, c, true);
}
/* // Add $Is and $IsAlloc for this class :
axiom (forall p: ref, G: Ty ::
{ $Is(p, TClassA(G), h) }
$Is(p, TClassA(G), h) <=> (p == null || dtype(p) == TClassA(G));
axiom (forall p: ref, h: Heap, G: Ty ::
{ $IsAlloc(p, TClassA(G), h) }
$IsAlloc(p, TClassA(G), h) => (p == null || h[p, alloc]);
*/
MapM(Bools, is_alloc => {
List tyexprs;
var vars = MkTyParamBinders(GetTypeParams(c), out tyexprs);
var o = BplBoundVar("$o", predef.RefType, vars);
Bpl.Expr body, is_o;
Bpl.Expr o_null = Bpl.Expr.Eq(o, predef.Null);
Bpl.Expr o_ty = ClassTyCon(c, tyexprs);
string name;
if (is_alloc) {
name = c + ": Class $IsAlloc";
var h = BplBoundVar("$h", predef.HeapType, vars);
// $IsAlloc(o, ..)
is_o = MkIsAlloc(o, o_ty, h);
body = BplIff(is_o, BplOr(o_null, IsAlloced(c.tok, h, o)));
} else {
name = c + ": Class $Is";
// $Is(o, ..)
is_o = MkIs(o, o_ty);
Bpl.Expr rhs;
if (c == program.BuiltIns.ObjectDecl) {
rhs = Bpl.Expr.True;
} else {
//generating $o == null || implements$J(dtype(x))
if (c is TraitDecl)
{
var t = (TraitDecl)c;
var dtypeFunc = FunctionCall(o.tok, BuiltinFunction.DynamicType, null, o);
Bpl.Expr implementsFunc = FunctionCall(t.tok, "implements$" + t.Name, Bpl.Type.Bool, new List { dtypeFunc });
rhs = BplOr(o_null, implementsFunc);
}
else
{
rhs = BplOr(o_null, DType(o, o_ty));
}
}
body = BplIff(is_o, rhs);
}
sink.TopLevelDeclarations.Add(new Bpl.Axiom(c.tok, BplForall(vars, BplTrigger(is_o), body), name));
});
//this adds: function implements$J(ClassName): bool;
if (c is TraitDecl)
{
var arg_ref = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, Bpl.TypedIdent.NoName, predef.Ty), true);
var res = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, Bpl.TypedIdent.NoName, Bpl.Type.Bool), false);
var implement_intr = new Bpl.Function(c.tok, "implements$" + c.Name, new List { arg_ref }, res);
sink.TopLevelDeclarations.Add(implement_intr);
}
//this adds: axiom implements$J(class.C);
else if (c is ClassDecl)
{
if (c.Trait != null)
{
//var dtypeFunc = FunctionCall(c.tok, BuiltinFunction.DynamicType, null, o);
//Bpl.Expr implementsFunc = FunctionCall(t.tok, "implements$" + t.Name, Bpl.Type.Bool, new List { dtypeFunc });
var args = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, Bpl.TypedIdent.NoName, predef.ClassNameType), true);
var ret_value = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, Bpl.TypedIdent.NoName, Bpl.Type.Bool), false);
var funCall = new Bpl.FunctionCall(new Bpl.Function(c.tok, "implements$" + c.TraitId.val, new List { args }, ret_value));
var expr = new Bpl.NAryExpr(c.tok, funCall, new List { new Bpl.IdentifierExpr(c.tok, string.Format("class.{0}", c.FullSanitizedName), predef.ClassNameType) });
var implements_axiom = new Bpl.Axiom(c.tok, expr);
sink.TopLevelDeclarations.Add(implements_axiom);
}
}
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, c);
} 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);
if (f.OverriddenFunction != null) //it means that f is overriding its associated parent function
{
AddFunctionOverrideCheckImpl(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);
}
if (m.OverriddenMethod != null) //method has overrided a parent method
{
var procOverrideChk = AddMethod(m, MethodTranslationKind.OverrideCheck);
sink.TopLevelDeclarations.Add(procOverrideChk);
AddMethodOverrideCheckImpl(m, procOverrideChk);
}
}
// 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);
}
// for body-less functions, at least generate its #requires function
if (f.Body == null) {
var b = FunctionAxiom(f, FunctionAxiomVisibility.ForeignModuleOnly, null, null);
Contract.Assert(b == null);
}
// 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, true, 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, true, 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(new WFOptions(), iter.Modifies.Expressions, localVariables, builder, etran);
CheckFrameWellFormed(new WFOptions(), 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 MemberSelectExpr(iter.tok, th, iter.Member_Reads.Name);
rds.Member = iter.Member_Reads; // resolve here
rds.Type = iter.Member_Reads.Type; // resolve here
var mod = new MemberSelectExpr(iter.tok, th, iter.Member_Modifies.Name);
mod.Member = 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();
foreach (var p in iter.TypeArgs) {
validCall.TypeArgumentSubstitutions[p] = new UserDefinedType(p);
} // resolved 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 MemberSelectExpr(iter.tok, th, iter.Member_New.Name);
nw.Member = 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 UnaryOpExpr(iter.tok, UnaryOpExpr.Opcode.Fresh, 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 MemberSelectExpr(iter.tok, th, y.Name);
thisY.Member = y; thisY.Type = y.Type; // resolve here
var thisYs = new MemberSelectExpr(iter.tok, th, ys.Name);
thisYs.Member = 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,
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);
Contract.Requires(body != 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.
// danr: Let's create the literal function axioms if there is an arrow type in the signature
if (!(f is CoPredicate) && (f.Reads.Count == 0 || f.Formals.Exists(a => a.Type is ArrowType))) {
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.
//
List tyargs;
var formals = MkTyParamBinders(GetTypeParams(f), out tyargs);
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();
funcArgs.AddRange(tyargs);
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), Concat(tyargs, 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);
// only if body is null, we will return null:
Contract.Ensures((Contract.Result() == null) == (body == 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)
//
// NOTE: this is lifted out to a #requires function for intra module calls,
// and used in the function pseudo-handles for top level functions.
// For body-less functions, this is emitted when body is null.
//
// 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.
//
// quantify over the type arguments, and add them first to the arguments
List args = new List();
List tyargs;
var formals = MkTyParamBinders(GetTypeParams(f), out tyargs);
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 UnaryOpExpr(p.tok, UnaryOpExpr.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 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());
// ante := (useViaContext && typeAnte && pre)
ante = BplAnd(useViaContext, BplAnd(ante, pre));
// Add the precondition function and its axiom (which is equivalent to the ante)
if (body == null || (visibility == FunctionAxiomVisibility.IntraModuleOnly && lits == null)) {
var precondF = new Bpl.Function(f.tok,
RequiresName(f), new List(),
formals.ConvertAll(v => (Bpl.Variable)BplFormalVar(null, v.TypedIdent.Type, true)),
BplFormalVar(null, Bpl.Type.Bool, false));
sink.TopLevelDeclarations.Add(precondF);
var appl = FunctionCall(f.tok, RequiresName(f), Bpl.Type.Bool,
formals.ConvertAll(x => (Bpl.Expr)(new Bpl.IdentifierExpr(f.tok, x))));
sink.TopLevelDeclarations.Add(new Axiom(f.tok, BplForall(formals, BplTrigger(appl), Bpl.Expr.Eq(appl, ante))));
// you could use it to check that it always works, but it makes VSI-Benchmarks/b3.dfy time out:
// ante = appl;
if (body == null) {
return null;
}
}
// 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), Concat(tyargs,args));
// ante := useViaCanCall || (useViaContext && typeAnte && pre)
ante = Bpl.Expr.Or(useViaCanCall, ante);
Bpl.Expr funcAppl;
{
var funcID = new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName, TrType(f.ResultType));
var funcArgs = new List();
funcArgs.AddRange(tyargs);
if (layer != null) {
var ly = new Bpl.IdentifierExpr(f.tok, layer);
if (lits == null) {
funcArgs.Add(LayerSucc(ly));
} else {
funcArgs.Add(ly);
}
}
funcArgs.AddRange(args);
funcAppl = new Bpl.NAryExpr(f.tok, new Bpl.FunctionCall(funcID), funcArgs);
}
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, etranBody),
Bpl.Expr.Eq(funcAppl, etranBody.TrExpr(bodyWithSubst)));
}
QKeyValue kv = null;
if (lits != null) {
kv = new QKeyValue(f.tok, "weight", new List