//-----------------------------------------------------------------------------
//
// 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 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;
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 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(DtCtorId != null);
Contract.Invariant(Null != null);
Contract.Invariant(allocField != null);
Contract.Invariant(ClassDotArray != null);
}
public Bpl.Type SetType(IToken tok, Bpl.Type ty) {
Contract.Requires(tok != null);
Contract.Requires(ty != null);
Contract.Ensures(Contract.Result() != null);
return new Bpl.TypeSynonymAnnotation(Token.NoToken, setTypeCtor, new Bpl.TypeSeq(ty));
}
public Bpl.Type MultiSetType(IToken tok, Bpl.Type ty) {
Contract.Requires(tok != null);
Contract.Requires(ty != null);
Contract.Ensures(Contract.Result() != null);
return new Bpl.TypeSynonymAnnotation(Token.NoToken, multiSetTypeCtor, new Bpl.TypeSeq(ty));
}
public Bpl.Type MapType(IToken tok, Bpl.Type tya, Bpl.Type tyb) {
Contract.Requires(tok != null);
Contract.Requires(tya != null && tyb != null);
Contract.Ensures(Contract.Result() != null);
return new Bpl.CtorType(Token.NoToken, mapTypeCtor, new Bpl.TypeSeq(tya, tyb));
}
public Bpl.Type SeqType(IToken tok, Bpl.Type ty) {
Contract.Requires(tok != null);
Contract.Requires(ty != null);
Contract.Ensures(Contract.Result() != null);
return new Bpl.CtorType(Token.NoToken, seqTypeCtor, new Bpl.TypeSeq(ty));
}
public Bpl.Type FieldName(IToken tok, Bpl.Type ty) {
Contract.Requires(tok != null);
Contract.Requires(ty != null);
Contract.Ensures(Contract.Result() != null);
return new Bpl.CtorType(tok, fieldName, new Bpl.TypeSeq(ty));
}
public Bpl.IdentifierExpr Alloc(IToken tok) {
Contract.Requires(tok != null);
Contract.Ensures(Contract.Result() != null);
return new Bpl.IdentifierExpr(tok, allocField);
}
public PredefinedDecls(Bpl.TypeCtorDecl refType, Bpl.TypeCtorDecl boxType, Bpl.TypeCtorDecl tickType,
Bpl.TypeSynonymDecl setTypeCtor, Bpl.TypeSynonymDecl multiSetTypeCtor, Bpl.TypeCtorDecl mapTypeCtor, Bpl.Function arrayLength, Bpl.TypeCtorDecl seqTypeCtor, Bpl.TypeCtorDecl fieldNameType,
Bpl.GlobalVariable heap, Bpl.TypeCtorDecl classNameType, Bpl.TypeCtorDecl nameFamilyType,
Bpl.TypeCtorDecl datatypeType, Bpl.TypeCtorDecl dtCtorId,
Bpl.Constant allocField, Bpl.Constant classDotArray) {
#region Non-null preconditions on parameters
Contract.Requires(refType != null);
Contract.Requires(boxType != null);
Contract.Requires(tickType != null);
Contract.Requires(setTypeCtor != null);
Contract.Requires(multiSetTypeCtor != null);
Contract.Requires(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(dtCtorId != null);
Contract.Requires(allocField != null);
Contract.Requires(classDotArray != null);
#endregion
Bpl.CtorType refT = new Bpl.CtorType(Token.NoToken, refType, new Bpl.TypeSeq());
this.RefType = refT;
this.BoxType = new Bpl.CtorType(Token.NoToken, boxType, new Bpl.TypeSeq());
this.TickType = new Bpl.CtorType(Token.NoToken, tickType, new Bpl.TypeSeq());
this.setTypeCtor = setTypeCtor;
this.multiSetTypeCtor = multiSetTypeCtor;
this.mapTypeCtor = mapTypeCtor;
this.ArrayLength = arrayLength;
this.seqTypeCtor = seqTypeCtor;
this.fieldName = fieldNameType;
this.HeapType = heap.TypedIdent.Type;
this.HeapVarName = heap.Name;
this.ClassNameType = new Bpl.CtorType(Token.NoToken, classNameType, new Bpl.TypeSeq());
this.NameFamilyType = new Bpl.CtorType(Token.NoToken, nameFamilyType, new Bpl.TypeSeq());
this.DatatypeType = new Bpl.CtorType(Token.NoToken, datatypeType, new Bpl.TypeSeq());
this.DtCtorId = new Bpl.CtorType(Token.NoToken, dtCtorId, new Bpl.TypeSeq());
this.allocField = allocField;
this.Null = new Bpl.IdentifierExpr(Token.NoToken, "null", refT);
this.ClassDotArray = classDotArray;
}
}
static PredefinedDecls FindPredefinedDecls(Bpl.Program prog) {
Contract.Requires(prog != null);
if (prog.Resolve() != 0) {
Console.WriteLine("Error: resolution errors encountered in Dafny prelude");
return null;
}
Bpl.TypeCtorDecl refType = null;
Bpl.TypeSynonymDecl setTypeCtor = null;
Bpl.TypeSynonymDecl multiSetTypeCtor = null;
Bpl.Function arrayLength = null;
Bpl.TypeCtorDecl seqTypeCtor = null;
Bpl.TypeCtorDecl fieldNameType = null;
Bpl.TypeCtorDecl classNameType = null;
Bpl.TypeCtorDecl nameFamilyType = null;
Bpl.TypeCtorDecl datatypeType = null;
Bpl.TypeCtorDecl dtCtorId = null;
Bpl.TypeCtorDecl boxType = null;
Bpl.TypeCtorDecl tickType = null;
Bpl.TypeCtorDecl mapTypeCtor = null;
Bpl.GlobalVariable heap = null;
Bpl.Constant allocField = null;
Bpl.Constant classDotArray = null;
foreach (var d in prog.TopLevelDeclarations) {
if (d is Bpl.TypeCtorDecl) {
Bpl.TypeCtorDecl dt = (Bpl.TypeCtorDecl)d;
if (dt.Name == "Seq") {
seqTypeCtor = dt;
} else if (dt.Name == "Field") {
fieldNameType = dt;
} else if (dt.Name == "ClassName") {
classNameType = dt;
} else if (dt.Name == "DatatypeType") {
datatypeType = dt;
} else if (dt.Name == "DtCtorId") {
dtCtorId = dt;
} else if (dt.Name == "ref") {
refType = dt;
} else if (dt.Name == "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 (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, dtCtorId,
allocField, classDotArray);
}
return null;
}
static Bpl.Program ReadPrelude() {
string preludePath = DafnyOptions.O.DafnyPrelude;
if (preludePath == null)
{
//using (System.IO.Stream stream = cce.NonNull( System.Reflection.Assembly.GetExecutingAssembly().GetManifestResourceStream("DafnyPrelude.bpl")) // Use this once Spec#/VSIP supports designating a non-.resx project item as an embedded resource
string codebase = cce.NonNull(System.IO.Path.GetDirectoryName(cce.NonNull(System.Reflection.Assembly.GetExecutingAssembly().Location)));
preludePath = System.IO.Path.Combine(codebase, "DafnyPrelude.bpl");
}
Bpl.Program prelude;
int errorCount = Bpl.Parser.Parse(preludePath, (List)null, out prelude);
if (prelude == null || errorCount > 0) {
return null;
} else {
return prelude;
}
}
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) {
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) {
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;
var id = new Tuple(m.Refined.FullCompileName, m.Refining.FullCompileName);
if (!checkedMethods.Contains(id)) {
AddMethodRefinementCheck(m);
checkedMethods.Add(id);
}
} else if (t is FunctionCheck) {
var f = (FunctionCheck)t;
var id = new Tuple(f.Refined.FullCompileName, f.Refining.FullCompileName);
if (!checkedFunctions.Contains(id)) {
AddFunctionRefinementCheck(f);
checkedFunctions.Add(id);
}
}
}
return sink;
}
void AddDatatype(DatatypeDecl dt) {
Contract.Requires(dt != null);
Contract.Requires(sink != null && predef != null);
sink.TopLevelDeclarations.Add(GetClass(dt));
foreach (DatatypeCtor ctor in dt.Ctors) {
// Add: function #dt.ctor(paramTypes) returns (DatatypeType);
Bpl.VariableSeq argTypes = new Bpl.VariableSeq();
foreach (Formal arg in ctor.Formals) {
Bpl.Variable a = new Bpl.Formal(arg.tok, new Bpl.TypedIdent(arg.tok, Bpl.TypedIdent.NoName, TrType(arg.Type)), true);
argTypes.Add(a);
}
Bpl.Variable resType = new Bpl.Formal(ctor.tok, new Bpl.TypedIdent(ctor.tok, Bpl.TypedIdent.NoName, predef.DatatypeType), false);
Bpl.Function fn = new Bpl.Function(ctor.tok, ctor.FullName, argTypes, resType);
sink.TopLevelDeclarations.Add(fn);
// Add: axiom (forall params :: #dt.ctor(params)-has-the-expected-type);
Bpl.VariableSeq bvs;
List args;
CreateBoundVariables(ctor.Formals, out bvs, out args);
Bpl.Expr ct = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);
List tpArgs = new List(); // we use an empty list of type arguments, because we don't want Good_Datatype to produce any DtTypeParams predicates anyway
Bpl.Expr wh = new ExpressionTranslator(this, predef, ctor.tok).Good_Datatype(ctor.tok, ct, dt, tpArgs);
if (bvs.Length != 0) {
wh = new Bpl.ForallExpr(ctor.tok, bvs, wh);
}
sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, wh));
// Add: const unique ##dt.ctor: DtCtorId;
Bpl.Constant cid = new Bpl.Constant(ctor.tok, new Bpl.TypedIdent(ctor.tok, "#" + ctor.FullName, predef.DtCtorId), true);
sink.TopLevelDeclarations.Add(cid);
// Add: axiom (forall params :: DatatypeCtorId(#dt.ctor(params)) == ##dt.ctor);
CreateBoundVariables(ctor.Formals, out bvs, out args);
Bpl.Expr lhs = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);
lhs = FunctionCall(ctor.tok, BuiltinFunction.DatatypeCtorId, null, lhs);
Bpl.Expr q = Bpl.Expr.Eq(lhs, new Bpl.IdentifierExpr(ctor.tok, cid));
if (bvs.Length != 0) {
q = new Bpl.ForallExpr(ctor.tok, bvs, q);
}
sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, q));
// Add: axiom (forall d: DatatypeType :: dt.ctor?(d) ==> (exists params :: d == #dt.ctor(params));
CreateBoundVariables(ctor.Formals, out bvs, out args);
lhs = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);
var dBv = new Bpl.BoundVariable(ctor.tok, new Bpl.TypedIdent(ctor.tok, "d", predef.DatatypeType));
var dId = new Bpl.IdentifierExpr(ctor.tok, dBv.Name, predef.DatatypeType);
q = Bpl.Expr.Eq(dId, lhs);
if (bvs.Length != 0) {
q = new Bpl.ExistsExpr(ctor.tok, bvs, q);
}
q = Bpl.Expr.Imp(FunctionCall(ctor.tok, ctor.QueryField.FullCompileName, Bpl.Type.Bool, dId), q);
q = new Bpl.ForallExpr(ctor.tok, new VariableSeq(dBv), q);
sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, q));
// Add: function dt.ctor?(this: DatatypeType): bool { DatatypeCtorId(this) == ##dt.ctor }
fn = GetReadonlyField(ctor.QueryField);
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 ExprSeq(queryPredicate));
var ax = new Bpl.ForallExpr(ctor.tok, new VariableSeq(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 ExprSeq(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));
// 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));
} 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.FullCompileName, new Bpl.VariableSeq(cases_dBv), cases_resType);
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.FullCompileName, 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 ExprSeq(lhs));
var ax = new Bpl.ForallExpr(dt.tok, new VariableSeq(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.FullCompileName, new Bpl.VariableSeq(d0Var, d1Var), resType,
"equality for codatatype " + dt.FullName);
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.FullCompileName, 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 ExprSeq(eqDt));
var ax = new Bpl.ForallExpr(dt.tok, new VariableSeq(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.FullCompileName, new Bpl.VariableSeq(d0Var, d1Var), resType);
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.FullCompileName, 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 ExprSeq(eqDt));
var ax = new Bpl.ForallExpr(dt.tok, new VariableSeq(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.FullCompileName, 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 ExprSeq(eqDt));
var ax = new Bpl.ForallExpr(dt.tok, new VariableSeq(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.FullCompileName, new Bpl.VariableSeq(d0Var, d1Var), resType,
"equality (limited version) for codatatype " + dt.FullName);
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.FullCompileName, Bpl.Type.Bool, d0, d1);
var eqDt0 = FunctionCall(dt.tok, "$Eq#0#" + dt.FullCompileName, Bpl.Type.Bool, d0, d1);
var tr = new Bpl.Trigger(dt.tok, true, new ExprSeq(eqDt));
var ax = new Bpl.ForallExpr(dt.tok, new VariableSeq(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.FullCompileName, Bpl.Type.Bool, d0, d1);
var eq = Bpl.Expr.Eq(d0, d1);
var tr = new Bpl.Trigger(dt.tok, true, new ExprSeq(eqDt));
var ax = new Bpl.ForallExpr(dt.tok, new VariableSeq(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 Bpl.VariableSeq(kVar, d0Var, d1Var), resType,
"prefix equality for codatatype " + dt.FullName);
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 ExprSeq(prefixEq));
var ax = new Bpl.ForallExpr(dt.tok, new VariableSeq(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 Bpl.VariableSeq(kVar, d0Var, d1Var), resType);
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 ExprSeq(prefixEq));
var ax = new Bpl.ForallExpr(dt.tok, new VariableSeq(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 ExprSeq(p1));
var ax = new Bpl.ForallExpr(dt.tok, new VariableSeq(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 Bpl.VariableSeq(kVar, d0Var, d1Var), resType);
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 ExprSeq(p1));
var ax = new Bpl.ForallExpr(dt.tok, new VariableSeq(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 VariableSeq(kVar), body);
var eqDt = FunctionCall(dt.tok, "$Eq#" + dt.FullCompileName, Bpl.Type.Bool, d0, d1);
q = new Bpl.ForallExpr(dt.tok, new VariableSeq(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 VariableSeq(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 VariableSeq(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 Bpl.ExprSeq(A));
Bpl.Expr rhs = new Bpl.NAryExpr(tok, new Bpl.FunctionCall(GetReadonlyField(ctor.QueryField)), new Bpl.ExprSeq(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 Bpl.ExprSeq(A));
var b = new Bpl.NAryExpr(tok, new Bpl.FunctionCall(GetReadonlyField(dtor)), new Bpl.ExprSeq(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.FullCompileName, Bpl.Type.Bool, a, b);
} else if (limited == 0) {
q = FunctionCall(tok, "$Eq#0#" + codecl.FullCompileName, Bpl.Type.Bool, a, b);
} else {
q = FunctionCall(tok, "$Eq#" + codecl.FullCompileName, 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.FullCompileName;
} else if (limited == 0) {
return "$PrefixEqual#0#" + codecl.FullCompileName;
} else {
return "$PrefixEqual#" + codecl.FullCompileName;
}
}
void CreateBoundVariables(List/*!*/ formals, out Bpl.VariableSeq/*!*/ bvs, out List/*!*/ args)
{
Contract.Requires(formals != null);
Contract.Ensures(Contract.ValueAtReturn(out bvs).Length == Contract.ValueAtReturn(out args).Count);
Contract.Ensures(Contract.ValueAtReturn(out bvs) != null);
Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out args)));
bvs = new Bpl.VariableSeq();
args = new List();
foreach (Formal arg in formals) {
Contract.Assert(arg != null);
var nm = string.Format("a{0}#{1}", bvs.Length, otherTmpVarCount);
otherTmpVarCount++;
Bpl.Variable bv = new Bpl.BoundVariable(arg.tok, new Bpl.TypedIdent(arg.tok, nm, TrType(arg.Type)));
bvs.Add(bv);
args.Add(new Bpl.IdentifierExpr(arg.tok, bv));
}
}
void AddClassMembers(ClassDecl c)
{
Contract.Requires(sink != null && predef != null);
Contract.Requires(c != null);
if (c.Name == "array") {
classes.Add(c, predef.ClassDotArray);
} else {
sink.TopLevelDeclarations.Add(GetClass(c));
}
foreach (MemberDecl member in c.Members) {
if (member is Field) {
Field f = (Field)member;
if (f.IsMutable) {
Bpl.Constant fc = GetField(f);
sink.TopLevelDeclarations.Add(fc);
} else {
Bpl.Function ff = GetReadonlyField(f);
if (ff != predef.ArrayLength)
sink.TopLevelDeclarations.Add(ff);
}
AddAllocationAxiom(f);
} else if (member is Function) {
var f = (Function)member;
AddClassMember_Function(f);
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);
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 CoMethod) {
// Let the CoCall and Impl forms to use m.PrefixMethod signature and specification (and
// note that m.PrefixMethod.Body == m.Body.
m = ((CoMethod)m).PrefixMethod;
sink.TopLevelDeclarations.Add(AddMethod(m, MethodTranslationKind.CoCall));
}
if (m.Body != null) {
// ...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 void AddClassMember_Function(Function f) {
AddFunction(f);
if (f.IsRecursive) {
AddLimitedAxioms(f, 2);
AddLimitedAxioms(f, 1);
}
for (int layerOffset = 0; layerOffset < 2; layerOffset++) {
var body = f.Body == null ? null : f.Body.Resolved;
if (body is MatchExpr) {
AddFunctionAxiomCase(f, (MatchExpr)body, null, layerOffset);
AddFunctionAxiom(f, null, f.Ens, null, layerOffset);
} else {
AddFunctionAxiom(f, body, f.Ens, null, layerOffset);
}
if (!f.IsRecursive) { break; }
}
AddFrameAxiom(f);
}
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);
Bpl.VariableSeq inParams, outParams;
GenerateMethodParametersChoose(iter.tok, iter, kind, true, true, false, etran, out inParams, out outParams);
var req = new Bpl.RequiresSeq();
var mod = new Bpl.IdentifierExprSeq();
var ens = new Bpl.EnsuresSeq();
// FREE PRECONDITIONS
if (kind == MethodTranslationKind.SpecWellformedness || kind == MethodTranslationKind.Implementation) { // the other cases have no need for a free precondition
// free requires mh == ModuleContextHeight && InMethodContext;
Bpl.Expr context = Bpl.Expr.And(
Bpl.Expr.Eq(Bpl.Expr.Literal(iter.Module.Height), etran.ModuleContextHeight()),
etran.InMethodContext());
req.Add(Requires(iter.tok, true, context, 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));
} else {
bool splitHappened; // we actually don't care
foreach (var s in TrSplitExpr(p.E, etran, 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, null));
// the free here is not linked to the free on the original expression (this is free things generated in the splitting.)
}
}
}
comment = null;
}
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));
} else {
bool splitHappened; // we actually don't care
foreach (var s in TrSplitExpr(p.E, etran, 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, null));
}
}
}
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);
currentModule = null;
codeContext = null;
return proc;
}
void AddIteratorWellformed(IteratorDecl iter, Procedure proc) {
currentModule = iter.Module;
codeContext = iter;
Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(iter.TypeArgs);
Bpl.VariableSeq inParams = Bpl.Formal.StripWhereClauses(proc.InParams);
Contract.Assert(1 <= inParams.Length); // there should at least be a receiver parameter
Contract.Assert(proc.OutParams.Length == 0);
var builder = new Bpl.StmtListBuilder();
var etran = new ExpressionTranslator(this, predef, iter.tok);
var localVariables = new Bpl.VariableSeq();
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
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 VariableSeq(),
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;
Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(iter.TypeArgs);
Bpl.VariableSeq inParams = Bpl.Formal.StripWhereClauses(proc.InParams);
Contract.Assert(1 <= inParams.Length); // there should at least be a receiver parameter
Contract.Assert(proc.OutParams.Length == 0);
Bpl.StmtListBuilder builder = new Bpl.StmtListBuilder();
ExpressionTranslator etran = new ExpressionTranslator(this, predef, iter.tok);
Bpl.VariableSeq localVariables = new Bpl.VariableSeq();
GenerateIteratorImplPrelude(iter, inParams, new VariableSeq(), 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, "_yieldCount", Bpl.Type.Int));
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 VariableSeq(),
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;
}
void AddFunctionAxiomCase(Function f, MatchExpr me, Specialization prev, int layerOffset) {
Contract.Requires(f != null);
Contract.Requires(me != null);
Contract.Requires(layerOffset == 0 || layerOffset == 1);
IVariable formal = ((IdentifierExpr)me.Source.Resolved).Var; // correctness of casts follows from what resolution checks
foreach (MatchCaseExpr mc in me.Cases) {
Contract.Assert(mc.Ctor != null); // the field is filled in by resolution
Specialization s = new Specialization(formal, mc, prev);
var body = mc.Body.Resolved;
if (body is MatchExpr) {
AddFunctionAxiomCase(f, (MatchExpr)body, s, layerOffset);
} else {
AddFunctionAxiom(f, body, new List(), s, layerOffset);
}
}
}
class Specialization
{
public readonly List Formals;
public readonly List ReplacementExprs;
public readonly List ReplacementFormals;
public readonly Dictionary SubstMap;
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(cce.NonNullElements(Formals));
Contract.Invariant(cce.NonNullElements(ReplacementExprs));
Contract.Invariant(Formals.Count == ReplacementExprs.Count);
Contract.Invariant(cce.NonNullElements(ReplacementFormals));
Contract.Invariant(SubstMap != null);
}
public Specialization(IVariable formal, MatchCase mc, Specialization prev) {
Contract.Requires(formal is Formal || formal is BoundVar);
Contract.Requires(mc != null);
Contract.Requires(prev == null || formal is BoundVar || !prev.Formals.Contains((Formal)formal));
List rArgs = new List();
foreach (BoundVar p in mc.Arguments) {
IdentifierExpr ie = new IdentifierExpr(p.tok, p.UniqueName);
ie.Var = p; ie.Type = ie.Var.Type; // resolve it here
rArgs.Add(ie);
}
// create and resolve datatype value
var r = new DatatypeValue(mc.tok, mc.Ctor.EnclosingDatatype.Name, mc.Ctor.Name, rArgs);
r.Ctor = mc.Ctor;
r.Type = new UserDefinedType(mc.tok, mc.Ctor.EnclosingDatatype.Name, new List()/*this is not right, but it seems like it won't matter here*/, 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(Substitute(e, null, substMap));
}
foreach (var rf in prev.ReplacementFormals) {
if (rf != formal) {
ReplacementFormals.Add(rf);
}
}
foreach (var entry in prev.SubstMap) {
SubstMap.Add(entry.Key, Substitute(entry.Value, null, substMap));
}
}
if (formal is Formal) {
Formals.Add((Formal)formal);
ReplacementExprs.Add(r);
}
ReplacementFormals.AddRange(mc.Arguments);
SubstMap.Add(formal, r);
}
}
void AddFunctionAxiom(Function/*!*/ f, Expression body, List/*!*/ ens, Specialization specialization, int layerOffset) {
if (f is Predicate || f is CoPredicate) {
var ax = FunctionAxiom(f, FunctionAxiomVisibility.IntraModuleOnly, body, ens, specialization, layerOffset);
sink.TopLevelDeclarations.Add(ax);
ax = FunctionAxiom(f, FunctionAxiomVisibility.ForeignModuleOnly, body, ens, specialization, layerOffset);
sink.TopLevelDeclarations.Add(ax);
if (f is CoPredicate) {
AddPrefixPredicateAxioms(((CoPredicate)f).PrefixPredicate);
}
} else {
var ax = FunctionAxiom(f, FunctionAxiomVisibility.All, body, ens, specialization, layerOffset);
sink.TopLevelDeclarations.Add(ax);
}
}
enum FunctionAxiomVisibility { All, IntraModuleOnly, ForeignModuleOnly }
Bpl.Axiom/*!*/ FunctionAxiom(Function/*!*/ f, FunctionAxiomVisibility visibility, Expression body, List/*!*/ ens, Specialization specialization, int layerOffset) {
Contract.Requires(f != null);
Contract.Requires(ens != null);
Contract.Requires(layerOffset == 0 || (layerOffset == 1 && f.IsRecursive));
Contract.Requires(predef != null);
Contract.Requires(f.EnclosingClass != null);
ExpressionTranslator etran = new ExpressionTranslator(this, predef, f.tok);
// axiom
// mh < ModuleContextHeight || // (a)
// (mh == ModuleContextHeight && (fh <= FunctionContextHeight || InMethodContext)) // (b)
// ==>
// (forall $Heap, formals ::
// { f(args) }
// f#canCall(args) ||
// ( (mh != ModuleContextHeight || fh != FunctionContextHeight || InMethodContext) && // (c)
// $IsHeap($Heap) && this != null && formals-have-the-expected-types &&
// Pre($Heap,args))
// ==>
// body-can-make-its-calls && // generated only for layerOffset==0
// f(args) == body && // (d)
// ens && // generated only for layerOffset==0
// f(args)-has-the-expected-type); // generated only for layerOffset==0
//
// The variables "formals" are the formals of function "f"; except, if a specialization is provided, then
// "specialization.Formals" (which are expected to be among the formals of "f") are excluded and replaced by
// "specialization.ReplacementFormals".
// The list "args" is the list of formals of function "f"; except, if a specialization is provided, then
// each of the "specialization.Formals" is replaced by the corresponding expression in "specialization.ReplacementExprs".
// If a specialization is provided, occurrences of "specialization.Formals" in "body", "f.Req", and "f.Ens"
// are also replaced by those corresponding expressions.
//
// The translation of "body" uses the #limited form whenever the callee is in the same SCC of the call graph.
//
// if layerOffset==1, then the names f#2 and f are used instead of f and f#limited.
//
// Visibility: The above description is for visibility==All. If visibility==IntraModuleOnly, then
// disjunct (a) is dropped (which also has a simplifying effect on (c)). Finally, if visibility==ForeignModuleOnly,
// then disjunct (b) is dropped (which also has a simplify effect on(c)); furthermore, if f is a Predicate,
// then the equality in (d) is replaced by an implication.
//
// Note, an antecedent $Heap[this,alloc] is intentionally left out: including it would only weaken
// the axiom. Moreover, leaving it out does not introduce any soundness problem, because the Dafny
// allocation statement changes only an allocation bit and then re-assumes $IsGoodHeap; so if it is
// sound after that, then it would also have been sound just before the allocation.
//
Bpl.VariableSeq formals = new Bpl.VariableSeq();
Bpl.ExprSeq args = new Bpl.ExprSeq();
Bpl.BoundVariable bv = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, predef.HeapVarName, predef.HeapType));
formals.Add(bv);
args.Add(new Bpl.IdentifierExpr(f.tok, bv));
// ante: $IsHeap($Heap) && this != null && formals-have-the-expected-types &&
Bpl.Expr ante = FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, etran.HeapExpr);
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);
}
if (specialization != null) {
foreach (BoundVar p in specialization.ReplacementFormals) {
bv = new Bpl.BoundVariable(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, TrType(p.Type)));
formals.Add(bv);
// add well-typedness conjunct to antecedent
Bpl.Expr wh = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, bv), p.Type, etran);
if (wh != null) { ante = Bpl.Expr.And(ante, wh); }
}
}
List specializationFormals;
if (specialization == null) {
specializationFormals = null;
} else if (f is PrefixPredicate) {
var pp = (PrefixPredicate)f;
// the specialization formals are given in terms of the co-predicate formals, but we're sitting
// here with the prefix predicate, so lets map them over
var paramMap = new Dictionary();
for (int i = 0; i < pp.Co.Formals.Count; i++) {
paramMap.Add(pp.Co.Formals[i], pp.Formals[i + 1]);
}
specializationFormals = new List();
foreach (var p in specialization.Formals) {
specializationFormals.Add(paramMap[p]);
}
Contract.Assert(specializationFormals.Count == specialization.Formals.Count);
} else {
specializationFormals = specialization.Formals;
}
foreach (Formal p in f.Formals) {
int i = specializationFormals == null ? -1 : specializationFormals.FindIndex(val => val == p);
if (i == -1) {
bv = new Bpl.BoundVariable(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, TrType(p.Type)));
formals.Add(bv);
Bpl.Expr formal = new Bpl.IdentifierExpr(p.tok, bv);
args.Add(formal);
// add well-typedness conjunct to antecedent
Bpl.Expr wh = GetWhereClause(p.tok, formal, p.Type, etran);
if (wh != null) { ante = Bpl.Expr.And(ante, wh); }
} else {
args.Add(etran.TrExpr(specialization.ReplacementExprs[i]));
// note, well-typedness conjuncts for the replacement formals has already been done above
}
}
// mh < ModuleContextHeight || (mh == ModuleContextHeight && (fh <= FunctionContextHeight || InMethodContext))
ModuleDefinition mod = f.EnclosingClass.Module;
var activateForeign = Bpl.Expr.Lt(Bpl.Expr.Literal(mod.Height), etran.ModuleContextHeight());
var activateIntra =
Bpl.Expr.And(
Bpl.Expr.Eq(Bpl.Expr.Literal(mod.Height), etran.ModuleContextHeight()),
Bpl.Expr.Or(
Bpl.Expr.Le(Bpl.Expr.Literal(mod.CallGraph.GetSCCRepresentativeId(f)), etran.FunctionContextHeight()),
etran.InMethodContext()));
Bpl.Expr activate =
visibility == FunctionAxiomVisibility.All ? Bpl.Expr.Or(activateForeign, activateIntra) :
visibility == FunctionAxiomVisibility.IntraModuleOnly ? activateIntra : activateForeign;
var substMap = new Dictionary();
if (specialization != null) {
substMap = specialization.SubstMap;
}
Bpl.IdentifierExpr funcID = new Bpl.IdentifierExpr(f.tok, FunctionName(f, 1+layerOffset), TrType(f.ResultType));
Bpl.Expr funcAppl = new Bpl.NAryExpr(f.tok, new Bpl.FunctionCall(funcID), args);
Bpl.Expr pre = Bpl.Expr.True;
foreach (Expression req in f.Req) {
pre = BplAnd(pre, etran.TrExpr(Substitute(req, null, substMap)));
}
// useViaContext: (mh != ModuleContextHeight || fh != FunctionContextHeight || InMethodContext)
Bpl.Expr useViaContext = visibility == FunctionAxiomVisibility.ForeignModuleOnly ? Bpl.Expr.True :
Bpl.Expr.Or(Bpl.Expr.Or(
visibility == FunctionAxiomVisibility.IntraModuleOnly ?
(Bpl.Expr)Bpl.Expr.False :
Bpl.Expr.Neq(Bpl.Expr.Literal(mod.Height), etran.ModuleContextHeight()),
Bpl.Expr.Neq(Bpl.Expr.Literal(mod.CallGraph.GetSCCRepresentativeId(f)), etran.FunctionContextHeight())),
etran.InMethodContext());
// useViaCanCall: f#canCall(args)
Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(f.tok, f.FullCompileName + "#canCall", Bpl.Type.Bool);
Bpl.Expr useViaCanCall = new Bpl.NAryExpr(f.tok, new Bpl.FunctionCall(canCallFuncID), args);
// ante := useViaCanCall || (useViaContext && typeAnte && pre)
ante = Bpl.Expr.Or(useViaCanCall, BplAnd(useViaContext, BplAnd(ante, pre)));
Bpl.Trigger tr = new Bpl.Trigger(f.tok, true, new Bpl.ExprSeq(funcAppl));
Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(f.TypeArgs);
Bpl.Expr meat;
if (body == null) {
meat = Bpl.Expr.True;
} else {
var bodyWithSubst = Substitute(body, null, substMap);
if (f is PrefixPredicate) {
var pp = (PrefixPredicate)f;
bodyWithSubst = PrefixSubstitution(pp, bodyWithSubst);
}
if (layerOffset == 0) {
meat = Bpl.Expr.And(
CanCallAssumption(bodyWithSubst, etran),
visibility == FunctionAxiomVisibility.ForeignModuleOnly && (f is Predicate || f is CoPredicate) ?
Bpl.Expr.Imp(funcAppl, etran.LimitedFunctions(f).TrExpr(bodyWithSubst)) :
Bpl.Expr.Eq(funcAppl, etran.LimitedFunctions(f).TrExpr(bodyWithSubst)));
} else {
meat = visibility == FunctionAxiomVisibility.ForeignModuleOnly && (f is Predicate || f is CoPredicate) ?
Bpl.Expr.Imp(funcAppl, etran.TrExpr(bodyWithSubst)) :
Bpl.Expr.Eq(funcAppl, etran.TrExpr(bodyWithSubst));
}
}
if (layerOffset == 0) {
foreach (Expression p in ens) {
Bpl.Expr q = etran.LimitedFunctions(f).TrExpr(Substitute(p, null, substMap));
meat = BplAnd(meat, q);
}
Bpl.Expr whr = GetWhereClause(f.tok, funcAppl, f.ResultType, etran);
if (whr != null) { meat = Bpl.Expr.And(meat, whr); }
}
Bpl.Expr ax = new Bpl.ForallExpr(f.tok, typeParams, formals, null, tr, Bpl.Expr.Imp(ante, meat));
string comment = "definition axiom for " + FunctionName(f, 1+layerOffset);
if (visibility == FunctionAxiomVisibility.IntraModuleOnly) {
comment += " (intra-module)";
} else if (visibility == FunctionAxiomVisibility.ForeignModuleOnly) {
comment += " (foreign modules)";
}
if (specialization != null) {
string sep = "{0}, specialized for '{1}'";
foreach (var formal in specialization.Formals) {
comment = string.Format(sep, comment, formal.Name);
sep = "{0}, '{1}'";
}
}
return new Bpl.Axiom(f.tok, Bpl.Expr.Imp(activate, ax), comment);
}
///
/// For a copredicate P, "pp" is the prefix predicate for P (such that P = pp.Co) and
/// "body" is the body of P. Return what would be the body of the prefix predicate pp.
/// In particular, return
/// 0 LESS _k IMPLIES body'
/// where body' is body with the formals of P replaced by the corresponding
/// formals of pp and with corecursive calls P(s) replaced by recursive calls to
/// pp(_k - 1, s).
///
Expression PrefixSubstitution(PrefixPredicate pp, Expression body) {
Contract.Requires(pp != null);
var paramMap = new Dictionary();
for (int i = 0; i < pp.Co.Formals.Count; i++) {
var replacement = pp.Formals[i + 1]; // the +1 is to skip pp's _k parameter
var param = new IdentifierExpr(replacement.tok, replacement.Name);
param.Var = replacement; // resolve here
param.Type = replacement.Type; // resolve here
paramMap.Add(pp.Co.Formals[i], param);
}
var k = new IdentifierExpr(pp.tok, pp.K.Name);
k.Var = pp.K; // resolve here
k.Type = pp.K.Type; // resolve here
var kMinusOne = CreateIntSub(pp.tok, k, Resolver.CreateResolvedLiteral(pp.tok, 1));
var s = new PrefixCallSubstituter(null, paramMap, pp.Co, kMinusOne);
body = s.Substitute(body);
// add antecedent "0 < _k ==>"
var kIsPositive = new BinaryExpr(pp.tok, BinaryExpr.Opcode.Lt, Resolver.CreateResolvedLiteral(pp.tok, 0), k);
kIsPositive.ResolvedOp = BinaryExpr.ResolvedOpcode.Lt; // resolve here
kIsPositive.Type = Type.Int; // resolve here
return DafnyImp(kIsPositive, body);
}
void AddLimitedAxioms(Function f, int fromLayer) {
Contract.Requires(f != null);
Contract.Requires(f.IsRecursive);
Contract.Requires(fromLayer == 1 || fromLayer == 2);
Contract.Requires(sink != null && predef != null);
// With fromLayer==1, generate:
// axiom (forall formals :: { f(args) } f(args) == f#limited(args))
// With fromLayer==2, generate:
// axiom (forall formals :: { f#2(args) } f#2(args) == f(args))
Bpl.VariableSeq formals = new Bpl.VariableSeq();
Bpl.ExprSeq args = new Bpl.ExprSeq();
Bpl.BoundVariable bv = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, predef.HeapVarName, predef.HeapType));
formals.Add(bv);
args.Add(new Bpl.IdentifierExpr(f.tok, bv));
Bpl.BoundVariable bvThis;
Bpl.Expr bvThisIdExpr;
if (f.IsStatic) {
bvThis = null;
bvThisIdExpr = null;
} else {
bvThis = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "this", predef.RefType));
formals.Add(bvThis);
bvThisIdExpr = new Bpl.IdentifierExpr(f.tok, bvThis);
args.Add(bvThisIdExpr);
}
foreach (Formal p in f.Formals) {
bv = new Bpl.BoundVariable(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, TrType(p.Type)));
formals.Add(bv);
args.Add(new Bpl.IdentifierExpr(p.tok, bv));
}
Bpl.FunctionCall origFuncID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, FunctionName(f, fromLayer), TrType(f.ResultType)));
Bpl.Expr origFuncAppl = new Bpl.NAryExpr(f.tok, origFuncID, args);
Bpl.FunctionCall limitedFuncID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, FunctionName(f, fromLayer-1), TrType(f.ResultType)));
Bpl.Expr limitedFuncAppl = new Bpl.NAryExpr(f.tok, limitedFuncID, args);
Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(f.TypeArgs);
Bpl.Trigger tr = new Bpl.Trigger(f.tok, true, new Bpl.ExprSeq(origFuncAppl));
Bpl.Expr ax = new Bpl.ForallExpr(f.tok, typeParams, formals, null, tr, Bpl.Expr.Eq(origFuncAppl, limitedFuncAppl));
sink.TopLevelDeclarations.Add(new Bpl.Axiom(f.tok, ax));
}
///
/// Add the axioms:
/// forall s :: P(s) ==> forall k: nat :: P#[k](s)
/// forall s :: (forall k: nat :: P#[k](s)) ==> P(s)
/// forall s,k :: k == 0 ==> P#[k](s)
/// where "s" is "heap, formals". In more details:
/// forall s :: { P(s) } s-has-appropriate-values && P(s) ==> forall k { P#[k](s) } :: 0 ATMOST k ==> P#[k](s)
/// forall s :: { P(s) } s-has-appropriate-values && (forall k :: 0 ATMOST k ==> P#[k](s)) ==> P(s)
/// forall s,k :: s-has-appropriate-values && k == 0 ==> P#0#[k](s)
///
void AddPrefixPredicateAxioms(PrefixPredicate pp) {
Contract.Requires(pp != null);
Contract.Requires(predef != null);
var co = pp.Co;
var tok = pp.tok;
var etran = new ExpressionTranslator(this, predef, tok);
var bvs = new Bpl.VariableSeq();
var coArgs = new Bpl.ExprSeq();
var prefixArgs = new Bpl.ExprSeq();
var bv = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, predef.HeapVarName, predef.HeapType));
bvs.Add(bv);
coArgs.Add(new Bpl.IdentifierExpr(tok, bv));
prefixArgs.Add(new Bpl.IdentifierExpr(tok, bv));
// ante: $IsHeap($Heap) && this != null && formals-have-the-expected-types &&
Bpl.Expr ante = FunctionCall(tok, BuiltinFunction.IsGoodHeap, null, etran.HeapExpr);
if (!pp.IsStatic) {
var bvThis = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, etran.This, predef.RefType));
bvs.Add(bvThis);
var bvThisIdExpr = new Bpl.IdentifierExpr(tok, bvThis);
coArgs.Add(bvThisIdExpr);
prefixArgs.Add(bvThisIdExpr);
// add well-typedness conjunct to antecedent
Type thisType = Resolver.GetReceiverType(tok, pp);
Bpl.Expr wh = Bpl.Expr.And(
Bpl.Expr.Neq(bvThisIdExpr, predef.Null),
etran.GoodRef(tok, bvThisIdExpr, thisType));
ante = Bpl.Expr.And(ante, wh);
}
// add the formal _k
var k = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, pp.Formals[0].UniqueName, TrType(pp.Formals[0].Type)));
var kId = new Bpl.IdentifierExpr(tok, k);
prefixArgs.Add(kId);
var kWhere = GetWhereClause(tok, kId, pp.Formals[0].Type, etran);
foreach (var p in co.Formals) {
bv = new Bpl.BoundVariable(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, TrType(p.Type)));
bvs.Add(bv);
var formal = new Bpl.IdentifierExpr(p.tok, bv);
coArgs.Add(formal);
prefixArgs.Add(formal);
// add well-typedness conjunct to antecedent
var wh = GetWhereClause(p.tok, formal, p.Type, etran);
if (wh != null) { ante = Bpl.Expr.And(ante, wh); }
}
var funcID = new Bpl.IdentifierExpr(tok, FunctionName(co, 1), TrType(co.ResultType));
var coAppl = new Bpl.NAryExpr(tok, new Bpl.FunctionCall(funcID), coArgs);
funcID = new Bpl.IdentifierExpr(tok, FunctionName(pp, 1), TrType(pp.ResultType));
var prefixAppl = new Bpl.NAryExpr(tok, new Bpl.FunctionCall(funcID), prefixArgs);
// forall s :: { P(s) } s-has-appropriate-values && P(s) ==> forall k { P#[k](s) } :: 0 ATMOST k ==> P#[k](s)
var tr = new Bpl.Trigger(tok, true, new ExprSeq(prefixAppl));
var allK = new Bpl.ForallExpr(tok, new VariableSeq(k), tr, BplImp(kWhere, prefixAppl));
tr = new Bpl.Trigger(tok, true, new ExprSeq(coAppl));
var allS = new Bpl.ForallExpr(tok, bvs, tr, BplImp(BplAnd(ante, coAppl), allK));
sink.TopLevelDeclarations.Add(new Bpl.Axiom(tok, allS));
// forall s :: { P(s) } s-has-appropriate-values && (forall k :: 0 ATMOST k ==> P#[k](s)) ==> P(s)
allS = new Bpl.ForallExpr(tok, bvs, tr, BplImp(BplAnd(ante, allK), coAppl));
sink.TopLevelDeclarations.Add(new Bpl.Axiom(tok, allS));
// forall s,k :: s-has-appropriate-values && k == 0 ==> P#0#[k](s)
var moreBvs = new VariableSeq();
moreBvs.AddRange(bvs);
moreBvs.Add(k);
var z = Bpl.Expr.Eq(kId, Bpl.Expr.Literal(0));
funcID = new Bpl.IdentifierExpr(tok, FunctionName(pp, pp.IsRecursive ? 0 : 1), TrType(pp.ResultType));
var prefixLimited = new Bpl.NAryExpr(tok, new Bpl.FunctionCall(funcID), prefixArgs);
var trueAtZero = new Bpl.ForallExpr(tok, moreBvs, BplImp(BplAnd(ante, z), prefixLimited));
sink.TopLevelDeclarations.Add(new Bpl.Axiom(tok, trueAtZero));
}
///
/// Returns the appropriate Boogie function for the given function. In particular:
/// Layer 2: f#2 --currently used only for induction axioms
/// Layer 1: f --this is the default name
/// Layer 0: f#limited --does not trigger the function definition axiom
///
public static string FunctionName(Function f, int layer) {
Contract.Requires(f != null);
Contract.Requires(0 <= layer && layer < 3);
Contract.Ensures(Contract.Result() != null);
string name = f.FullCompileName;
switch (layer) {
case 2: name += "#2"; break;
case 0: name += "#limited"; break;
}
return name;
}
///
/// Generate:
/// axiom (forall h: [ref, Field x]x, o: ref ::
/// { h[o,f] }
/// $IsGoodHeap(h) && o != null && h[o,alloc] ==> h[o,f]-has-the-expected-type);
///
void AddAllocationAxiom(Field f)
{
Contract.Requires(f != null);
Contract.Requires(sink != null && predef != null);
Bpl.BoundVariable hVar = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$h", predef.HeapType));
Bpl.Expr h = new Bpl.IdentifierExpr(f.tok, hVar);
ExpressionTranslator etran = new ExpressionTranslator(this, predef, h);
Bpl.BoundVariable oVar = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$o", predef.RefType));
Bpl.Expr o = new Bpl.IdentifierExpr(f.tok, oVar);
// h[o,f]
Bpl.Expr oDotF;
if (f.IsMutable) {
oDotF = ExpressionTranslator.ReadHeap(f.tok, h, o, new Bpl.IdentifierExpr(f.tok, GetField(f)));
} else {
oDotF = new Bpl.NAryExpr(f.tok, new Bpl.FunctionCall(GetReadonlyField(f)), new Bpl.ExprSeq(o));
}
Bpl.Expr wh = GetWhereClause(f.tok, oDotF, f.Type, etran);
if (wh != null) {
// ante: $IsGoodHeap(h) && o != null && h[o,alloc]
Bpl.Expr ante = Bpl.Expr.And(Bpl.Expr.And(
FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, h),
Bpl.Expr.Neq(o, predef.Null)),
etran.IsAlloced(f.tok, o));
Bpl.Expr body = Bpl.Expr.Imp(ante, wh);
Bpl.Trigger tr = f.IsMutable ? new Bpl.Trigger(f.tok, true, new Bpl.ExprSeq(oDotF)) : null; // the trigger must include both "o" and "h"
Bpl.Expr ax = new Bpl.ForallExpr(f.tok, new Bpl.VariableSeq(hVar, oVar), tr, body);
sink.TopLevelDeclarations.Add(new Bpl.Axiom(f.tok, ax));
}
}
Bpl.Expr InSeqRange(IToken tok, Bpl.Expr index, Bpl.Expr seq, bool isSequence, Bpl.Expr lowerBound, bool includeUpperBound) {
Contract.Requires(tok != null);
Contract.Requires(index != null);
Contract.Requires(seq != null);
Contract.Ensures(Contract.Result() != null);
if (lowerBound == null) {
lowerBound = Bpl.Expr.Literal(0);
}
Bpl.Expr lower = Bpl.Expr.Le(lowerBound, index);
Bpl.Expr length = isSequence ?
FunctionCall(tok, BuiltinFunction.SeqLength, null, seq) :
ArrayLength(tok, seq, 1, 0);
Bpl.Expr upper;
if (includeUpperBound) {
upper = Bpl.Expr.Le(index, length);
} else {
upper = Bpl.Expr.Lt(index, length);
}
return Bpl.Expr.And(lower, upper);
}
ModuleDefinition currentModule = null; // the name of the module whose members are currently being translated
ICodeContext codeContext = null; // the method/iterator whose implementation is currently being translated
LocalVariable yieldCountVariable = null; // non-null when an iterator body is being translated
bool assertAsAssume = false; // generate assume statements instead of assert statements
int loopHeapVarCount = 0;
int otherTmpVarCount = 0;
Dictionary _tmpIEs = new Dictionary();
Bpl.IdentifierExpr GetTmpVar_IdExpr(IToken tok, string name, Bpl.Type ty, Bpl.VariableSeq locals) // local variable that's shared between statements that need it
{
Contract.Requires(tok != null);
Contract.Requires(name != null);
Contract.Requires(ty != null);
Contract.Requires(locals != null);
Contract.Ensures(Contract.Result() != null);
Bpl.IdentifierExpr ie;
if (_tmpIEs.TryGetValue(name, out ie)) {
Contract.Assume(ie.Type.Equals(ty));
} else {
// the "tok" and "ty" of the first request for this variable is the one we use
var v = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, name, ty)); // important for the "$nw" client: no where clause (see GetNewVar_IdExpr)
locals.Add(v);
ie = new Bpl.IdentifierExpr(tok, v);
_tmpIEs.Add(name, ie);
}
return ie;
}
Bpl.IdentifierExpr GetPrevHeapVar_IdExpr(IToken tok, Bpl.VariableSeq locals) { // local variable that's shared between statements that need it
Contract.Requires(tok != null);
Contract.Requires(locals != null); Contract.Requires(predef != null);
Contract.Ensures(Contract.Result() != null);
return GetTmpVar_IdExpr(tok, "$prevHeap", predef.HeapType, locals);
}
Bpl.IdentifierExpr GetNewVar_IdExpr(IToken tok, Bpl.VariableSeq locals) // local variable that's shared between statements that need it
{
Contract.Requires(tok != null);
Contract.Requires(locals != null);
Contract.Requires(predef != null);
Contract.Ensures(Contract.Result() != null);
// important: the following declaration produces no where clause (that's why we're going through the trouble of setting of this variable in the first place)
return GetTmpVar_IdExpr(tok, "$nw", predef.RefType, locals);
}
///
/// Returns an expression whose value is the same as "expr", but that is guaranteed to preserve the its value passed
/// the evaluation of other expressions. If necessary, a new local variable called "name" with type "ty" is added to "locals" and
/// assigned in "builder" to be used to hold the value of "expr". It is assumed that all requests for a given "name"
/// have the same type "ty" and that these variables can be shared.
/// As an optimization, if "otherExprsCanAffectPreviouslyKnownExpressions" is "false", then "expr" itself is returned.
///
Bpl.Expr SaveInTemp(Bpl.Expr expr, bool otherExprsCanAffectPreviouslyKnownExpressions, string name, Bpl.Type ty, Bpl.StmtListBuilder builder, Bpl.VariableSeq locals) {
Contract.Requires(expr != null);
Contract.Requires(name != null);
Contract.Requires(ty != null);
Contract.Requires(locals != null);
Contract.Ensures(Contract.Result() != null);
if (otherExprsCanAffectPreviouslyKnownExpressions) {
var save = GetTmpVar_IdExpr(expr.tok, name, ty, locals);
builder.Add(Bpl.Cmd.SimpleAssign(expr.tok, save, expr));
return save;
} else {
return expr;
}
}
void AddMethodImpl(Method m, Bpl.Procedure proc, bool wellformednessProc)
{
Contract.Requires(m != null);
Contract.Requires(proc != null);
Contract.Requires(sink != null && predef != null);
Contract.Requires(wellformednessProc || m.Body != null);
Contract.Requires(currentModule == null && codeContext == null && loopHeapVarCount == 0 && _tmpIEs.Count == 0);
Contract.Ensures(currentModule == null && codeContext == null && loopHeapVarCount == 0 && _tmpIEs.Count == 0);
currentModule = m.EnclosingClass.Module;
codeContext = m;
Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(m.TypeArgs);
Bpl.VariableSeq inParams = Bpl.Formal.StripWhereClauses(proc.InParams);
Bpl.VariableSeq outParams = Bpl.Formal.StripWhereClauses(proc.OutParams);
Bpl.StmtListBuilder builder = new Bpl.StmtListBuilder();
ExpressionTranslator etran = new ExpressionTranslator(this, predef, m.tok);
Bpl.VariableSeq localVariables = new Bpl.VariableSeq();
GenerateImplPrelude(m, inParams, outParams, builder, localVariables);
Bpl.StmtList stmts;
if (!wellformednessProc) {
if (3 <= DafnyOptions.O.Induction && m.IsGhost && m.Mod.Expressions.Count == 0 && m.Outs.Count == 0 && !(m is CoMethod)) {
var posts = new List();
m.Ens.ForEach(mfe => posts.Add(mfe.E));
var allIns = new List();
if (!m.IsStatic) {
allIns.Add(new ThisSurrogate(m.tok, Resolver.GetThisType(m.tok, (ClassDecl)m.EnclosingClass)));
}
allIns.AddRange(m.Ins);
var inductionVars = ApplyInduction(allIns, m.Attributes, posts, delegate(System.IO.TextWriter wr) { wr.Write(m.FullName); });
if (inductionVars.Count != 0) {
// Let the parameters be this,x,y of the method M and suppose ApplyInduction returns this,y.
// Also, let Pre be the precondition and VF be the decreases clause.
// Then, insert into the method body what amounts to:
// assume case-analysis-on-parameter[[ y' ]];
// forall (this', y' | Pre(this', x, y') && VF(this', x, y') << VF(this, x, y)) {
// this'.M(x, y');
// }
// Generate bound variables for the forall statement, and a substitution for the Pre and VF
// assume case-analysis-on-parameter[[ y' ]];
foreach (var inFormal in m.Ins) {
var dt = inFormal.Type.AsDatatype;
if (dt != null) {
var funcID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(inFormal.tok, "$IsA#" + dt.FullCompileName, Bpl.Type.Bool));
var f = new Bpl.IdentifierExpr(inFormal.tok, inFormal.UniqueName, TrType(inFormal.Type));
builder.Add(new Bpl.AssumeCmd(inFormal.tok, new Bpl.NAryExpr(inFormal.tok, funcID, new Bpl.ExprSeq(f))));
}
}
var parBoundVars = new List();
Expression receiverReplacement = null;
var substMap = new Dictionary();
foreach (var iv in inductionVars) {
BoundVar bv;
IdentifierExpr ie;
CloneVariableAsBoundVar(iv.tok, iv, "$ih#" + iv.Name, out bv, out ie);
parBoundVars.Add(bv);
if (iv is ThisSurrogate) {
Contract.Assert(receiverReplacement == null && substMap.Count == 0); // the receiver comes first, if at all
receiverReplacement = ie;
} else {
substMap.Add(iv, ie);
}
}
// Generate a CallStmt for the recursive call
Expression recursiveCallReceiver;
if (receiverReplacement != null) {
recursiveCallReceiver = receiverReplacement;
} else if (m.IsStatic) {
recursiveCallReceiver = new StaticReceiverExpr(m.tok, (ClassDecl)m.EnclosingClass); // this also resolves it
} else {
recursiveCallReceiver = new ImplicitThisExpr(m.tok);
recursiveCallReceiver.Type = Resolver.GetThisType(m.tok, (ClassDecl)m.EnclosingClass); // resolve here
}
var recursiveCallArgs = new List();
foreach (var inFormal in m.Ins) {
Expression inE;
if (substMap.TryGetValue(inFormal, out inE)) {
recursiveCallArgs.Add(inE);
} else {
var ie = new IdentifierExpr(inFormal.tok, inFormal.Name);
ie.Var = inFormal; // resolve here
ie.Type = inFormal.Type; // resolve here
recursiveCallArgs.Add(ie);
}
}
var recursiveCall = new CallStmt(m.tok, new List(), recursiveCallReceiver, m.Name, recursiveCallArgs);
recursiveCall.Method = m; // resolve here
Expression parRange = new LiteralExpr(m.tok, true);
parRange.Type = Type.Bool; // resolve here
if (receiverReplacement != null) {
// add "this' != null" to the range
var nil = new LiteralExpr(receiverReplacement.tok);
nil.Type = receiverReplacement.Type; // resolve here
var neqNull = new BinaryExpr(receiverReplacement.tok, BinaryExpr.Opcode.Neq, receiverReplacement, nil);
neqNull.ResolvedOp = BinaryExpr.ResolvedOpcode.NeqCommon; // resolve here
neqNull.Type = Type.Bool; // resolve here
parRange = DafnyAnd(parRange, neqNull);
}
foreach (var pre in m.Req) {
if (!pre.IsFree) {
parRange = DafnyAnd(parRange, Substitute(pre.E, receiverReplacement, substMap));
}
}
// construct an expression (generator) for: VF' << VF
ExpressionConverter decrCheck = delegate(Dictionary decrSubstMap, ExpressionTranslator exprTran) {
var decrToks = new List();
var decrTypes = new List();
var decrCallee = new List();
var decrCaller = new List();
bool decrInferred; // we don't actually care
foreach (var ee in MethodDecreasesWithDefault(m, out decrInferred)) {
decrToks.Add(ee.tok);
decrTypes.Add(ee.Type);
decrCaller.Add(exprTran.TrExpr(ee));
Expression es = Substitute(ee, receiverReplacement, substMap);
es = Substitute(es, null, decrSubstMap);
decrCallee.Add(exprTran.TrExpr(es));
}
return DecreasesCheck(decrToks, decrTypes, decrCallee, decrCaller, null, null, false, true);
};
#if VERIFY_CORRECTNESS_OF_TRANSLATION_FORALL_STATEMENT_RANGE
var definedness = new Bpl.StmtListBuilder();
var exporter = new Bpl.StmtListBuilder();
TrForallStmtCall(m.tok, parBoundVars, parRange, decrCheck, recursiveCall, definedness, exporter, localVariables, etran);
// All done, so put the two pieces together
builder.Add(new Bpl.IfCmd(m.tok, null, definedness.Collect(m.tok), null, exporter.Collect(m.tok)));
#else
TrForallStmtCall(m.tok, parBoundVars, parRange, decrCheck, recursiveCall, null, builder, localVariables, etran);
#endif
}
}
// translate the body of the method
Contract.Assert(m.Body != null); // follows from method precondition and the if guard
// $_reverifyPost := false;
builder.Add(Bpl.Cmd.SimpleAssign(m.tok, new Bpl.IdentifierExpr(m.tok, "$_reverifyPost", Bpl.Type.Bool), Bpl.Expr.False));
stmts = TrStmt2StmtList(builder, m.Body, localVariables, etran);
} else {
// check well-formedness of the preconditions, and then assume each one of them
foreach (MaybeFreeExpression p in m.Req) {
CheckWellformed(p.E, new WFOptions(), localVariables, builder, etran);
builder.Add(new Bpl.AssumeCmd(p.E.tok, etran.TrExpr(p.E)));
}
// check well-formedness of the modifies clause
CheckFrameWellFormed(m.Mod.Expressions, localVariables, builder, etran);
// check well-formedness of the decreases clauses
foreach (Expression p in m.Decreases.Expressions)
{
CheckWellformed(p, new WFOptions(), localVariables, builder, etran);
}
// play havoc with the heap according to the modifies clause
builder.Add(new Bpl.HavocCmd(m.tok, new Bpl.IdentifierExprSeq((Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr)));
// assume the usual two-state boilerplate information
foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(m.tok, m.Mod.Expressions, m.IsGhost, etran.Old, etran, etran.Old))
{
if (tri.IsFree) {
builder.Add(new Bpl.AssumeCmd(m.tok, tri.Expr));
}
}
// also play havoc with the out parameters
if (outParams.Length != 0) { // don't create an empty havoc statement
Bpl.IdentifierExprSeq outH = new Bpl.IdentifierExprSeq();
foreach (Bpl.Variable b in outParams) {
Contract.Assert(b != null);
outH.Add(new Bpl.IdentifierExpr(b.tok, b));
}
builder.Add(new Bpl.HavocCmd(m.tok, outH));
}
// check wellformedness of postconditions
foreach (MaybeFreeExpression p in m.Ens) {
CheckWellformed(p.E, new WFOptions(), localVariables, builder, etran);
builder.Add(new Bpl.AssumeCmd(p.E.tok, etran.TrExpr(p.E)));
}
stmts = builder.Collect(m.tok);
}
QKeyValue kv = etran.TrAttributes(m.Attributes, null);
Bpl.Implementation impl = new Bpl.Implementation(m.tok, proc.Name,
typeParams, inParams, outParams,
localVariables, stmts, kv);
sink.TopLevelDeclarations.Add(impl);
currentModule = null;
codeContext = null;
loopHeapVarCount = 0;
otherTmpVarCount = 0;
_tmpIEs.Clear();
}
void CheckFrameWellFormed(List fes, VariableSeq locals, StmtListBuilder builder, ExpressionTranslator etran) {
Contract.Requires(fes != null);
Contract.Requires(locals != null);
Contract.Requires(builder != null);
Contract.Requires(etran != null);
foreach (var fe in fes) {
CheckWellformed(fe.E, new WFOptions(), locals, builder, etran);
if (fe.Field != null && fe.E.Type.IsRefType) {
builder.Add(Assert(fe.tok, Bpl.Expr.Neq(etran.TrExpr(fe.E), predef.Null), "frame expression may dereference null"));
}
}
}
void GenerateImplPrelude(Method m, Bpl.VariableSeq inParams, Bpl.VariableSeq outParams,
Bpl.StmtListBuilder builder, Bpl.VariableSeq localVariables){
Contract.Requires(m != null);
Contract.Requires(inParams != null);
Contract.Requires(outParams != null);
Contract.Requires(builder != null);
Contract.Requires(localVariables != null);
Contract.Requires(predef != null);
// set up the information used to verify the method's modifies clause
DefineFrame(m.tok, m.Mod.Expressions, builder, localVariables, null);
}
void GenerateIteratorImplPrelude(IteratorDecl iter, Bpl.VariableSeq inParams, Bpl.VariableSeq outParams,
Bpl.StmtListBuilder builder, Bpl.VariableSeq localVariables) {
Contract.Requires(iter != null);
Contract.Requires(inParams != null);
Contract.Requires(outParams != null);
Contract.Requires(builder != null);
Contract.Requires(localVariables != null);
Contract.Requires(predef != null);
// set up the information used to verify the method's modifies clause
var iteratorFrame = new List();
var th = new ThisExpr(iter.tok);
th.Type = Resolver.GetThisType(iter.tok, iter); // resolve here
iteratorFrame.Add(new FrameExpression(iter.tok, th, null));
iteratorFrame.AddRange(iter.Modifies.Expressions);
DefineFrame(iter.tok, iteratorFrame, builder, localVariables, null);
}
Bpl.Cmd CaptureState(IToken tok, string/*?*/ additionalInfo) {
Contract.Requires(tok != null);
Contract.Ensures(Contract.Result() != null);
string description = string.Format("{0}({1},{2}){3}{4}", tok.filename, tok.line, tok.col, additionalInfo == null ? "" : ": ", additionalInfo ?? "");
QKeyValue kv = new QKeyValue(tok, "captureState", new List