From e39faec0ed77aa057b53ad77a972059cac2db128 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 6 Nov 2024 13:10:29 +0100 Subject: [PATCH] Move code out of BoogieGenerator.cs --- .../Verifier/BoogieGenerator.Classes.cs | 160 +++++ .../Verifier/BoogieGenerator.Datatypes.cs | 139 +++++ .../Verifier/BoogieGenerator.Functions.cs | 65 ++ .../Verifier/BoogieGenerator.Methods.cs | 7 + .../Verifier/BoogieGenerator.Prelude.cs | 244 ++++++++ .../Verifier/BoogieGenerator.Types.cs | 61 +- Source/DafnyCore/Verifier/BoogieGenerator.cs | 587 +----------------- Source/DafnyCore/Verifier/Specialization.cs | 69 ++ 8 files changed, 714 insertions(+), 618 deletions(-) create mode 100644 Source/DafnyCore/Verifier/BoogieGenerator.Classes.cs create mode 100644 Source/DafnyCore/Verifier/BoogieGenerator.Datatypes.cs create mode 100644 Source/DafnyCore/Verifier/BoogieGenerator.Prelude.cs create mode 100644 Source/DafnyCore/Verifier/Specialization.cs diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Classes.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Classes.cs new file mode 100644 index 00000000000..4f528eb684e --- /dev/null +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Classes.cs @@ -0,0 +1,160 @@ +//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// Copyright by the contributors to the Dafny Project +// SPDX-License-Identifier: MIT +// +//----------------------------------------------------------------------------- +using System; +using System.Collections.Generic; +using System.Collections.Immutable; +using System.Linq; +using System.Numerics; +using System.Diagnostics.Contracts; +using Bpl = Microsoft.Boogie; +using BplParser = Microsoft.Boogie.Parser; +using System.Text; +using System.Threading; +using DafnyCore; +using Microsoft.Boogie; +using static Microsoft.Dafny.Util; +using DafnyCore.Verifier; +using JetBrains.Annotations; +using Microsoft.Dafny.Triggers; +using PODesc = Microsoft.Dafny.ProofObligationDescription; +using static Microsoft.Dafny.GenericErrors; + +namespace Microsoft.Dafny; + +public partial class BoogieGenerator { + + + // This one says that this is /directly/ allocated, not that its "children" are, + // i.e. h[x, alloc] + public Bpl.Expr IsAlloced(IToken tok, Bpl.Expr heapExpr, Bpl.Expr e) { + Contract.Requires(tok != null); + Contract.Requires(heapExpr != null); + Contract.Requires(e != null); + Contract.Ensures(Contract.Result() != null); + + return ApplyUnbox(tok, ReadHeap(tok, heapExpr, e, Predef.Alloc(tok)), Bpl.Type.Bool); + } + + /// + /// Returns read(heap: Heap, r: ref, f: Field) : Box. + /// + public Bpl.Expr ReadHeap(IToken tok, Expr heap, Expr r, Expr f) { + Contract.Requires(tok != null); + Contract.Requires(heap != null); + Contract.Requires(r != null); + Contract.Requires(f != null); + Contract.Ensures(Contract.Result() != null); + + var res = new Bpl.NAryExpr(tok, + new Bpl.FunctionCall(new Bpl.IdentifierExpr(tok, "read", Predef.BoxType)), + new List { heap, r, f }); + res.Type = Predef.BoxType; + return res; + } + + public Bpl.NAryExpr ReadHeap(IToken tok, Expr heap, Expr r) { + Contract.Requires(tok != null); + Contract.Requires(heap != null); + Contract.Requires(r != null); + Contract.Ensures(Contract.Result() != null); + return new Bpl.NAryExpr(tok, new Bpl.MapSelect(tok, 1), new List { heap, r }); + } + + /// + /// Returns update(h: Heap, r: ref, f: Field, v: Box) : Heap. + /// + public Boogie.NAryExpr UpdateHeap(IToken tok, Expr heap, Expr r, Expr f, Expr v) { + Contract.Requires(tok != null); + Contract.Requires(heap != null); + Contract.Requires(r != null); + Contract.Requires(f != null); + Contract.Requires(v != null); + Contract.Ensures(Contract.Result() != null); + + + return new Boogie.NAryExpr(tok, + new Boogie.FunctionCall(new Boogie.IdentifierExpr(tok, "update", heap.Type)), + new List { heap, r, f, ApplyBox(tok, v) }); + } + + /// + /// For every revealed type (class or trait) C that extends a trait J, add: + /// axiom (forall T: Ty, $o: ref :: + /// { $Is($o, C(T)) } + /// $o != null && $Is($o, C(T)) ==> $Is($o, J(G(T))); + /// axiom (forall T: Ty, $Heap: Heap, $o: ref :: + /// { $IsAlloc($o, C(T), $Heap) } + /// $o != null && $IsAlloc($o, C(T), $Heap) ==> $IsAlloc($o, J(G(T)), $Heap); + /// Note: + /// It is sometimes useful also to be able to determine the _absence_ of trait-parent relationships. + /// For example, suppose one can tell from the looking at the "extends" clauses in a program + /// that a class C does not (directly or transitively) extend a trait T. Then, given variables c and t + /// of static types C and T, respectively, the verifier should be able to infer c != t. This is not + /// possible with the axioms below. It will require an axiomatization of _all_ possible parent traits, not just + /// saying that some are possible. When this becomes needed, the axiomatization will need to be + /// embellished. + /// + private void AddTraitParentAxioms() { + foreach (ModuleDefinition m in program.RawModules()) { + foreach (var c in m.TopLevelDecls.OfType().Where(RevealedInScope)) { + foreach (var parentTypeInExtendsClause in c.ParentTraits) { + var childType = UserDefinedType.FromTopLevelDecl(c.tok, c); + var parentType = (UserDefinedType)parentTypeInExtendsClause; + if (parentType.IsRefType) { + // use the nullable versions of the types + Contract.Assert(childType.IsRefType); + parentType = UserDefinedType.CreateNullableType(parentType); + } else { + childType = UserDefinedType.CreateNonNullTypeIfReferenceType(childType); + } + + var bvarsTypeParameters = MkTyParamBinders(GetTypeParams(c), out _); + + // axioms with "$IsBox(...) ==> ..." and "$IsAllocBox(...) ==> ..." + TypeBoundAxiomExpressions(c.tok, bvarsTypeParameters, childType, new List() { parentType }, + out var isBoxExpr, out var isAllocBoxExpr); + + var heapVar = BplBoundVar("$heap", Predef.HeapType, out var heap); + var oVar = BplBoundVar("$o", TrType(childType), out var o); + + var oj = BoxifyForTraitParent(c.tok, o, ((UserDefinedType)parentType.NormalizeExpand()).ResolvedClass, childType); + + // axiom (forall T: Ty, $o: ref :: + // { $Is($o, C(T)) } + // $Is($o, C(T)) ==> $Is($o, J(G(T))); + var isC = MkIs(o, childType); + var isJ = MkIs(oj, parentType); + var bvs = new List(); + bvs.AddRange(bvarsTypeParameters); + bvs.Add(oVar); + var tr = BplTrigger(isC); + var body = BplImp(isC, isJ); + + sink.AddTopLevelDeclaration(new Bpl.Axiom(c.tok, new Bpl.ForallExpr(c.tok, bvs, tr, body), + $"type axiom for trait parent: {childType.Name} extends {parentType}")); + sink.AddTopLevelDeclaration(new Bpl.Axiom(c.tok, isBoxExpr)); + + // axiom (forall T: Ty, $Heap: Heap, $o: ref :: + // { $IsAlloc($o, C(T), $Heap) } + // $IsAlloc($o, C(T), $Heap) ==> $IsAlloc($o, J(G(T)), $Heap); + var isAllocC = MkIsAlloc(o, childType, heap); + var isAllocJ = MkIsAlloc(oj, parentType, heap); + bvs = new List(); + bvs.AddRange(bvarsTypeParameters); + bvs.Add(oVar); + bvs.Add(heapVar); + tr = BplTrigger(isAllocC); + body = BplImp(isAllocC, isAllocJ); + sink.AddTopLevelDeclaration(new Bpl.Axiom(c.tok, new Bpl.ForallExpr(c.tok, bvs, tr, body), + $"allocation axiom for trait parent: {childType.Name} extends {parentType}")); + sink.AddTopLevelDeclaration(new Bpl.Axiom(c.tok, isAllocBoxExpr)); + } + } + } + } +} \ No newline at end of file diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Datatypes.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Datatypes.cs new file mode 100644 index 00000000000..fb7c17e6eec --- /dev/null +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Datatypes.cs @@ -0,0 +1,139 @@ +//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// Copyright by the contributors to the Dafny Project +// SPDX-License-Identifier: MIT +// +//----------------------------------------------------------------------------- +using System; +using System.Collections.Generic; +using System.Collections.Immutable; +using System.Linq; +using System.Numerics; +using System.Diagnostics.Contracts; +using Bpl = Microsoft.Boogie; +using BplParser = Microsoft.Boogie.Parser; +using System.Text; +using System.Threading; +using DafnyCore; +using Microsoft.Boogie; +using static Microsoft.Dafny.Util; +using DafnyCore.Verifier; +using JetBrains.Annotations; +using Microsoft.Dafny.Triggers; +using PODesc = Microsoft.Dafny.ProofObligationDescription; +using static Microsoft.Dafny.GenericErrors; + +namespace Microsoft.Dafny; + +public partial class BoogieGenerator { + + + /// + /// Return a sequence of expressions whose conjunction denotes a memberwise equality of "dt". Recursive + /// codatatype equalities are written in one of the following ways: + /// If the codatatype equality is on a type outside the SCC of "dt", then resort to ordinary equality. + /// Else if the k==null, then: + /// Depending on "limited", use the #2, #1, or #0 (limited) form of codatatype equality. + /// Else: + /// Depending on "limited", use the #2, #1, or #0 (limited) form of prefix equality, passing "k" + /// as the first argument. + /// + IEnumerable CoPrefixEquality(IToken tok, CoDatatypeDecl dt, List largs, List rargs, Bpl.Expr k, Bpl.Expr l, Bpl.Expr A, Bpl.Expr B, bool conjuncts = false) { + Contract.Requires(tok != null); + Contract.Requires(dt != null); + Contract.Requires(A != null); + Contract.Requires(B != null); + Contract.Requires(l != null); + Contract.Requires(Predef != null); + var etran = new ExpressionTranslator(this, Predef, dt.tok, dt); + // For example, for possibly infinite lists: + // codatatype SList = Nil | SCons(head: T, tail: SList); + // produce with conjucts=false (default): + // (A.Nil? && B.Nil?) || + // (A.Cons? && B.Cons? && A.head == B.head && Equal(k, A.tail, B.tail)) + // + // with conjuncts=true: + // (A.Nil? ==> B.Nil?) && + // (A.Cons? ==> (B.Cons? && A.head == B.head && Equal(k, A.tail, B.tail))) + + Dictionary lsu = Util.Dict(GetTypeParams(dt), largs); + Dictionary rsu = Util.Dict(GetTypeParams(dt), rargs); + + foreach (var ctor in dt.Ctors) { + Bpl.Expr aq = new Bpl.NAryExpr(tok, new Bpl.FunctionCall(GetReadonlyField(ctor.QueryField)), new List { A }); + Bpl.Expr bq = new Bpl.NAryExpr(tok, new Bpl.FunctionCall(GetReadonlyField(ctor.QueryField)), new List { B }); + Bpl.Expr chunk = Bpl.Expr.True; + foreach (var dtor in ctor.Destructors) { // note, ctor.Destructors has a field for every constructor parameter, whether or not the parameter was named in the source + var a = new Bpl.NAryExpr(tok, new Bpl.FunctionCall(GetReadonlyField(dtor)), new List { A }); + var b = new Bpl.NAryExpr(tok, new Bpl.FunctionCall(GetReadonlyField(dtor)), new List { B }); + var ty = dtor.Type; + Bpl.Expr q; + var codecl = ty.AsCoDatatype; + if (codecl != null && codecl.SscRepr == dt.SscRepr) { + var lexprs = Map(ty.TypeArgs, tt => tt.Subst(lsu)); + var rexprs = Map(ty.TypeArgs, tt => tt.Subst(rsu)); + q = CoEqualCall(codecl, lexprs, rexprs, k, l, a, b); + } else { + // ordinary equality; let the usual translation machinery figure out the translation + var tyA = ty.Subst(lsu); + var tyB = ty.Subst(rsu); + var aa = CondApplyUnbox(tok, a, ty, tyA); + var bb = CondApplyUnbox(tok, b, ty, tyB); + var equal = new BinaryExpr(tok, BinaryExpr.Opcode.Eq, new BoogieWrapper(aa, tyA), new BoogieWrapper(bb, tyB)); + equal.ResolvedOp = ModuleResolver.ResolveOp(equal.Op, tyA, tyB); // resolve here + equal.Type = Type.Bool; // resolve here + q = etran.TrExpr(equal); + } + chunk = BplAnd(chunk, q); + } + if (conjuncts) { + yield return Bpl.Expr.Binary(new NestedToken(tok, ctor.tok), BinaryOperator.Opcode.Imp, aq, BplAnd(bq, chunk)); + } else { + yield return BplAnd(BplAnd(aq, bq), BplImp(BplAnd(aq, bq), chunk)); + } + } + } + + + // Makes a call to equality, if k is null, or otherwise prefix equality. For codatatypes. + Bpl.Expr CoEqualCall(CoDatatypeDecl codecl, List largs, List rargs, Bpl.Expr k, Bpl.Expr l, Bpl.Expr A, Bpl.Expr B, Bpl.IToken tok = null) { + Contract.Requires(codecl != null); + Contract.Requires(largs != null); + Contract.Requires(rargs != null); + Contract.Requires(l != null); + Contract.Requires(A != null); + Contract.Requires(B != null); + if (tok == null) { + tok = A.tok; + } + List args = Concat(largs, rargs); + if (k != null) { + args.Add(k); + } + args.AddRange(new List { l, A, B }); + var fn = k == null ? CoEqualName(codecl) : CoPrefixName(codecl); + return FunctionCall(tok, fn, Bpl.Type.Bool, args); + } + + // Same as above, but with Dafny-typed type-argument lists + Bpl.Expr CoEqualCall(CoDatatypeDecl codecl, List largs, List rargs, Bpl.Expr k, Bpl.Expr l, Bpl.Expr A, Bpl.Expr B, IToken tok = null) { + Contract.Requires(codecl != null); + Contract.Requires(largs != null); + Contract.Requires(rargs != null); + Contract.Requires(l != null); + Contract.Requires(A != null); + Contract.Requires(B != null); + return CoEqualCall(codecl, Map(largs, TypeToTy), Map(rargs, TypeToTy), k, l, A, B, tok); + } + + static string CoEqualName(CoDatatypeDecl codecl) { + Contract.Requires(codecl != null); + return "$Eq#" + codecl.FullSanitizedName; + } + + static string CoPrefixName(CoDatatypeDecl codecl) { + Contract.Requires(codecl != null); + return "$PrefixEq#" + codecl.FullSanitizedName; + } +} \ No newline at end of file diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs index 5d1b4865e5d..5e757a03230 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs @@ -980,4 +980,69 @@ void AddFrameAxiom(Function f) { BplImp(q0, eq))); sink.AddTopLevelDeclaration(new Bpl.Axiom(f.tok, ax, comment)); } + + + /// + /// Returns true if the body of function "f" is available in module "context". + /// This happens when the following conditions all hold: + /// - "f" has a body + /// - "f" is not opaque + /// + bool FunctionBodyIsAvailable(Function f, ModuleDefinition context, VisibilityScope scope) { + Contract.Requires(f != null); + Contract.Requires(context != null); + return f.Body != null && !IsOpaque(f, options) && f.IsRevealedInScope(scope); + } + public static bool IsOpaque(MemberDecl f, DafnyOptions options) { + Contract.Requires(f != null); + if (f is Function f1) { + return Attributes.Contains(f.Attributes, "opaque") || f.IsOpaque || f1.IsMadeImplicitlyOpaque(options); + } else { + return Attributes.Contains(f.Attributes, "opaque") || f.IsOpaque; + } + } + static bool IsOpaqueRevealLemma(Method m) { + Contract.Requires(m != null); + return Attributes.Contains(m.Attributes, "opaque_reveal"); + } + + + private void ComputeFunctionFuel() { + foreach (ModuleDefinition m in program.RawModules()) { + foreach (TopLevelDecl d in m.TopLevelDecls) { + if (d is not TopLevelDeclWithMembers) { + continue; + } + + var c = (TopLevelDeclWithMembers)d; + foreach (MemberDecl member in c.Members) { + if (member is not Function || !RevealedInScope(member)) { + continue; + } + + Function f = (Function)member; + // declare the fuel constant + if (f.IsFueled) { + // const BaseFuel_FunctionA : LayerType + Bpl.Constant baseFuel = new Bpl.Constant(f.tok, new Bpl.TypedIdent(f.tok, "BaseFuel_" + f.FullName, Predef.LayerType), false); + sink.AddTopLevelDeclaration(baseFuel); + Bpl.Expr baseFuel_expr = new Bpl.IdentifierExpr(f.tok, baseFuel); + // const StartFuel_FunctionA : LayerType + Bpl.Constant startFuel = new Bpl.Constant(f.tok, new Bpl.TypedIdent(f.tok, "StartFuel_" + f.FullName, Predef.LayerType), false); + sink.AddTopLevelDeclaration(startFuel); + Bpl.Expr startFuel_expr = new Bpl.IdentifierExpr(f.tok, startFuel); + // const StartFuelAssert_FunctionA : LayerType + Bpl.Constant startFuelAssert = new Bpl.Constant(f.tok, new Bpl.TypedIdent(f.tok, "StartFuelAssert_" + f.FullName, Predef.LayerType), false); + sink.AddTopLevelDeclaration(startFuelAssert); + Bpl.Expr startFuelAssert_expr = new Bpl.IdentifierExpr(f.tok, startFuelAssert); + this.functionFuel.Add(new FuelConstant(f, baseFuel_expr, startFuel_expr, startFuelAssert_expr)); + } + + if (f.IsOpaque || f.IsMadeImplicitlyOpaque(options)) { + CreateRevealableConstant(f); + } + } + } + } + } } diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs index 88edc5bab9a..4fac38db673 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs @@ -1940,5 +1940,12 @@ public void TypeBoundAxiomExpressions(IToken tok, List bvarsTypePa isAllocBoxExpr = new Bpl.ForallExpr(tok, vars, BplTrigger(isAllocBox), body); } } + + void AddEnsures(List list, Bpl.Ensures ens) { + list.Add(ens); + if (!ens.Free) { + this.assertionCount++; + } + } } } diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Prelude.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Prelude.cs new file mode 100644 index 00000000000..482c76f1f46 --- /dev/null +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Prelude.cs @@ -0,0 +1,244 @@ +//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// Copyright by the contributors to the Dafny Project +// SPDX-License-Identifier: MIT +// +//----------------------------------------------------------------------------- + +using System.Collections.Generic; +using System.Numerics; +using System.Diagnostics.Contracts; +using Bpl = Microsoft.Boogie; +using Microsoft.Boogie; + +namespace Microsoft.Dafny; + +public partial class BoogieGenerator { + private void AddPreludeBoogieDefinitions() { + + foreach (var w in program.SystemModuleManager.Bitwidths) { + // type axioms + AddBitvectorTypeAxioms(w); + // bitwise operations + AddBitvectorFunction(w, "and_bv", "bvand"); + AddBitvectorFunction(w, "or_bv", "bvor"); + AddBitvectorFunction(w, "xor_bv", "bvxor"); // Z3 supports this, but it seems not to be in the SMT-LIB 2 standard + AddBitvectorFunction(w, "not_bv", "bvnot", false); + // arithmetic operations + AddBitvectorFunction(w, "add_bv", "bvadd"); + AddBitvectorFunction(w, "sub_bv", "bvsub"); // Z3 supports this, but it seems not to be in the SMT-LIB 2 standard + AddBitvectorFunction(w, "mul_bv", "bvmul"); + AddBitvectorFunction(w, "div_bv", "bvudiv"); + AddBitvectorFunction(w, "mod_bv", "bvurem"); + // comparisons + AddBitvectorFunction(w, "lt_bv", "bvult", true, Bpl.Type.Bool, false); + AddBitvectorFunction(w, "le_bv", "bvule", true, Bpl.Type.Bool, true); // Z3 supports this, but it seems not to be in the SMT-LIB 2 standard + AddBitvectorFunction(w, "ge_bv", "bvuge", true, Bpl.Type.Bool, true); // Z3 supports this, but it seems not to be in the SMT-LIB 2 standard + AddBitvectorFunction(w, "gt_bv", "bvugt", true, Bpl.Type.Bool, false); // Z3 supports this, but it seems not to be in the SMT-LIB 2 standard + // shifts + AddBitvectorShiftFunction(w, "LeftShift_bv", "bvshl"); + AddBitvectorShiftFunction(w, "RightShift_bv", "bvlshr"); + // rotates + AddBitvectorShiftFunction(w, "LeftRotate_bv", "ext_rotate_left"); + AddBitvectorShiftFunction(w, "RightRotate_bv", "ext_rotate_right"); + // conversion functions + AddBitvectorNatConversionFunction(w); + } + + foreach (TopLevelDecl d in program.SystemModuleManager.SystemModule.TopLevelDecls) { + CurrentDeclaration = d; + if (d is AbstractTypeDecl abstractType) { + GetOrCreateTypeConstructor(abstractType); + AddClassMembers(abstractType, true, true); + } else if (d is NewtypeDecl) { + var dd = (NewtypeDecl)d; + AddTypeDecl(dd); + AddClassMembers(dd, true, true); + } else if (d is SubsetTypeDecl) { + AddTypeDecl((SubsetTypeDecl)d); + } else if (d is TypeSynonymDecl) { + // do nothing, just bypass type synonyms in the translation + } else if (d is DatatypeDecl) { + var dd = (DatatypeDecl)d; + AddDatatype(dd); + AddClassMembers(dd, true, true); + } else if (d is ArrowTypeDecl) { + var ad = (ArrowTypeDecl)d; + GetClassTyCon(ad); + AddArrowTypeAxioms(ad); + } else if (d is ClassLikeDecl) { + var cl = (ClassLikeDecl)d; + AddClassMembers(cl, true, true); + if (cl.NonNullTypeDecl != null) { + AddTypeDecl(cl.NonNullTypeDecl); + } + } else { + Contract.Assert(d is ValuetypeDecl); + } + } + } + + + private void AddBitvectorTypeAxioms(int w) { + Contract.Requires(0 <= w); + + if (w == 0) { + // the axioms for bv0 are already in DafnyPrelude.bpl + return; + } + + // box/unbox axiom + var tok = Token.NoToken; + var printableName = "bv" + w; + var dafnyType = new BitvectorType(options, w); + var boogieType = BplBvType(w); + var typeTerm = TypeToTy(dafnyType); + AddBoxUnboxAxiom(tok, printableName, typeTerm, boogieType, new List()); + + // axiom (forall v: bv3 :: { $Is(v, TBitvector(3)) } $Is(v, TBitvector(3))); + var vVar = BplBoundVar("v", boogieType, out var v); + var bvs = new List() { vVar }; + var isBv = MkIs(v, typeTerm); + var tr = BplTrigger(isBv); + sink.AddTopLevelDeclaration(new Bpl.Axiom(tok, new Bpl.ForallExpr(tok, bvs, tr, isBv))); + + // axiom (forall v: bv3, heap: Heap :: { $IsAlloc(v, TBitvector(3), h) } $IsAlloc(v, TBitvector(3), heap)); + vVar = BplBoundVar("v", boogieType, out v); + var heapVar = BplBoundVar("heap", Predef.HeapType, out var heap); + bvs = new List() { vVar, heapVar }; + var isAllocBv = MkIsAlloc(v, typeTerm, heap); + tr = BplTrigger(isAllocBv); + sink.AddTopLevelDeclaration(new Bpl.Axiom(tok, new Bpl.ForallExpr(tok, bvs, tr, isAllocBv))); + } + + /// + /// Declare and add to the sink a Boogie function named "namePrefix + w". + /// If "binary", then the function takes two arguments; otherwise, it takes one. Arguments have the type + /// corresponding to the Dafny type for w-width bitvectors. + /// The function's result type is the same as the argument type, unless "resultType" is non-null, in which + /// case the function's result type is "resultType". + /// For w > 0: + /// Attach an attribute {:bvbuiltin smtFunctionName}. + /// For w == 0: + /// Attach an attribute {:inline} and add a .Body to the function. + /// If "resultType" is null, then use 0 as the body; otherwise, use "bodyForBv0" as the body (which + /// assumes "resultType" is actually Bpl.Type.Bool). + /// + private void AddBitvectorFunction(int w, string namePrefix, string smtFunctionName, bool binary = true, Bpl.Type resultType = null, bool bodyForBv0 = false) { + Contract.Requires(0 <= w); + Contract.Requires(namePrefix != null); + Contract.Requires(smtFunctionName != null); + var tok = Token.NoToken; + var t = BplBvType(w); + List args; + if (binary) { + var a0 = BplFormalVar(null, t, true); + var a1 = BplFormalVar(null, t, true); + args = new List() { a0, a1 }; + } else { + var a0 = BplFormalVar(null, t, true); + args = new List() { a0 }; + } + var r = BplFormalVar(null, resultType ?? t, false); + Bpl.QKeyValue attr; + if (w == 0) { + attr = InlineAttribute(tok); + } else { + attr = new Bpl.QKeyValue(tok, "bvbuiltin", new List() { smtFunctionName }, null); + } + var func = new Bpl.Function(tok, namePrefix + w, new List(), args, r, null, attr); + if (w == 0) { + if (resultType != null) { + func.Body = Bpl.Expr.Literal(bodyForBv0); + } else { + func.Body = BplBvLiteralExpr(tok, BaseTypes.BigNum.ZERO, w); + } + } + sink.AddTopLevelDeclaration(func); + } + + private void AddBitvectorShiftFunction(int w, string namePrefix, string smtFunctionName) { + Contract.Requires(0 <= w); + Contract.Requires(namePrefix != null); + Contract.Requires(smtFunctionName != null); + var tok = Token.NoToken; + var t = BplBvType(w); + List args; + var a0 = BplFormalVar(null, t, true); + var a1 = BplFormalVar(null, t, true); + args = new List() { a0, a1 }; + var r = BplFormalVar(null, t, false); + Bpl.QKeyValue attr; + if (w == 0) { + attr = InlineAttribute(tok); + } else { + attr = new Bpl.QKeyValue(tok, "bvbuiltin", new List() { smtFunctionName }, null); + } + var func = new Bpl.Function(tok, namePrefix + w, new List(), args, r, null, attr); + if (w == 0) { + func.Body = BplBvLiteralExpr(tok, BaseTypes.BigNum.ZERO, w); + } + sink.AddTopLevelDeclaration(func); + } + + private void AddBitvectorNatConversionFunction(int w) { + Contract.Requires(0 <= w); + var tok = Token.NoToken; + var bv = BplBvType(w); + Bpl.QKeyValue attr; + Bpl.Function func; + + // function {:bvbuiltin "(_ int2bv 67)"} nat_to_bv67(int) : bv67; + // OR: + // function {:inline} nat_to_bv0(int) : Bv0 { ZERO } + if (w == 0) { + attr = InlineAttribute(tok); + } else { + var smt_int2bv = string.Format("(_ int2bv {0})", w); + attr = new Bpl.QKeyValue(tok, "bvbuiltin", new List() { smt_int2bv }, null); // SMT-LIB 2 calls this function nat2bv, but Z3 apparently calls it int2bv + } + func = new Bpl.Function(tok, "nat_to_bv" + w, new List(), + new List() { BplFormalVar(null, Bpl.Type.Int, true) }, BplFormalVar(null, bv, false), + null, attr); + if (w == 0) { + func.Body = BplBvLiteralExpr(tok, BaseTypes.BigNum.ZERO, w); + } + sink.AddTopLevelDeclaration(func); + + if (w == 0) { + // function {:inline} nat_from_bv0_smt(Bv0) : int { 0 } + attr = InlineAttribute(tok); + func = new Bpl.Function(tok, "nat_from_bv" + w, new List(), + new List() { BplFormalVar(null, bv, true) }, BplFormalVar(null, Bpl.Type.Int, false), + null, attr); + func.Body = Bpl.Expr.Literal(0); + sink.AddTopLevelDeclaration(func); + } else { + // function {:bvbuiltin "bv2int"} smt_nat_from_bv67(bv67) : int; + attr = new Bpl.QKeyValue(tok, "bvbuiltin", new List() { "bv2int" }, null); // SMT-LIB 2 calls this function bv2nat, but Z3 apparently calls it bv2int + var smtFunc = new Bpl.Function(tok, "smt_nat_from_bv" + w, new List(), + new List() { BplFormalVar(null, bv, true) }, BplFormalVar(null, Bpl.Type.Int, false), + null, attr); + sink.AddTopLevelDeclaration(smtFunc); + // function nat_from_bv67(bv67) : int; + func = new Bpl.Function(tok, "nat_from_bv" + w, new List(), + new List() { BplFormalVar(null, bv, true) }, BplFormalVar(null, Bpl.Type.Int, false), + null, null); + sink.AddTopLevelDeclaration(func); + // axiom (forall b: bv67 :: { nat_from_bv67(b) } + // 0 <= nat_from_bv67(b) && nat_from_bv67(b) < 0x8_0000_0000_0000_0000 && + // nat_from_bv67(b) == smt_nat_from_bv67(b)); + var bVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "b", BplBvType(w))); + var b = new Bpl.IdentifierExpr(tok, bVar); + var bv2nat = FunctionCall(tok, "nat_from_bv" + w, Bpl.Type.Int, b); + var smt_bv2nat = FunctionCall(tok, "smt_nat_from_bv" + w, Bpl.Type.Int, b); + var body = BplAnd(BplAnd( + Bpl.Expr.Le(Bpl.Expr.Literal(0), bv2nat), + Bpl.Expr.Lt(bv2nat, Bpl.Expr.Literal(BaseTypes.BigNum.FromBigInt(BigInteger.One << w)))), + Bpl.Expr.Eq(bv2nat, smt_bv2nat)); + var ax = new Bpl.ForallExpr(tok, new List() { bVar }, BplTrigger(bv2nat), body); + sink.AddTopLevelDeclaration(new Bpl.Axiom(tok, ax)); + } + } +} \ No newline at end of file diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs index 9f13ac9c91e..1a0a9899a14 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs @@ -562,38 +562,6 @@ private Axiom CreateTagAndCallingForTypeConstructor(TopLevelDecl td) { return tagAxiom; } - private void AddBitvectorTypeAxioms(int w) { - Contract.Requires(0 <= w); - - if (w == 0) { - // the axioms for bv0 are already in DafnyPrelude.bpl - return; - } - - // box/unbox axiom - var tok = Token.NoToken; - var printableName = "bv" + w; - var dafnyType = new BitvectorType(options, w); - var boogieType = BplBvType(w); - var typeTerm = TypeToTy(dafnyType); - AddBoxUnboxAxiom(tok, printableName, typeTerm, boogieType, new List()); - - // axiom (forall v: bv3 :: { $Is(v, TBitvector(3)) } $Is(v, TBitvector(3))); - var vVar = BplBoundVar("v", boogieType, out var v); - var bvs = new List() { vVar }; - var isBv = MkIs(v, typeTerm); - var tr = BplTrigger(isBv); - sink.AddTopLevelDeclaration(new Bpl.Axiom(tok, new Bpl.ForallExpr(tok, bvs, tr, isBv))); - - // axiom (forall v: bv3, heap: Heap :: { $IsAlloc(v, TBitvector(3), h) } $IsAlloc(v, TBitvector(3), heap)); - vVar = BplBoundVar("v", boogieType, out v); - var heapVar = BplBoundVar("heap", Predef.HeapType, out var heap); - bvs = new List() { vVar, heapVar }; - var isAllocBv = MkIsAlloc(v, typeTerm, heap); - tr = BplTrigger(isAllocBv); - sink.AddTopLevelDeclaration(new Bpl.Axiom(tok, new Bpl.ForallExpr(tok, bvs, tr, isAllocBv))); - } - /// /// Generate: /// axiom (forall args: Ty, bx: Box :: @@ -1601,4 +1569,33 @@ private BoogieStmtListBuilder CheckConstraintWellformedness(RedirectingTypeDecl PathAsideBlock(decl.Tok, constraintCheckBuilder, builder); return builderInitializationArea; } + + + /// + /// Construct an expression denoting the equality of e0 and e1, taking advantage of + /// any available extensional equality based on the given Dafny type. + /// + public Expr TypeSpecificEqual(IToken tok, Dafny.Type type, Expr e0, Expr e1) { + Contract.Requires(tok != null); + Contract.Requires(type != null); + Contract.Requires(e0 != null); + Contract.Requires(e1 != null); + + type = type.NormalizeToAncestorType(); + if (type.AsSetType != null) { + var finite = type.AsSetType.Finite; + return FunctionCall(tok, finite ? BuiltinFunction.SetEqual : BuiltinFunction.ISetEqual, null, e0, e1); + } else if (type.AsMapType != null) { + var finite = type.AsMapType.Finite; + return FunctionCall(tok, finite ? BuiltinFunction.MapEqual : BuiltinFunction.IMapEqual, null, e0, e1); + } else if (type.AsMultiSetType != null) { + return FunctionCall(tok, BuiltinFunction.MultiSetEqual, null, e0, e1); + } else if (type.AsSeqType != null) { + return FunctionCall(tok, BuiltinFunction.SeqEqual, null, e0, e1); + } else if (type.IsIndDatatype) { + return FunctionCall(tok, type.AsIndDatatype.FullSanitizedName + "#Equal", Bpl.Type.Bool, e0, e1); + } else { + return Bpl.Expr.Eq(e0, e1); + } + } } diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.cs index 134442cd3d5..b61758d5c1d 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.cs @@ -713,66 +713,7 @@ public Bpl.Program DoTranslation(Program p, ModuleDefinition forModule) { EstablishModuleScope(p.SystemModuleManager.SystemModule, forModule); Type.PushScope(this.currentScope); - foreach (var w in program.SystemModuleManager.Bitwidths) { - // type axioms - AddBitvectorTypeAxioms(w); - // bitwise operations - AddBitvectorFunction(w, "and_bv", "bvand"); - AddBitvectorFunction(w, "or_bv", "bvor"); - AddBitvectorFunction(w, "xor_bv", "bvxor"); // Z3 supports this, but it seems not to be in the SMT-LIB 2 standard - AddBitvectorFunction(w, "not_bv", "bvnot", false); - // arithmetic operations - AddBitvectorFunction(w, "add_bv", "bvadd"); - AddBitvectorFunction(w, "sub_bv", "bvsub"); // Z3 supports this, but it seems not to be in the SMT-LIB 2 standard - AddBitvectorFunction(w, "mul_bv", "bvmul"); - AddBitvectorFunction(w, "div_bv", "bvudiv"); - AddBitvectorFunction(w, "mod_bv", "bvurem"); - // comparisons - AddBitvectorFunction(w, "lt_bv", "bvult", true, Bpl.Type.Bool, false); - AddBitvectorFunction(w, "le_bv", "bvule", true, Bpl.Type.Bool, true); // Z3 supports this, but it seems not to be in the SMT-LIB 2 standard - AddBitvectorFunction(w, "ge_bv", "bvuge", true, Bpl.Type.Bool, true); // Z3 supports this, but it seems not to be in the SMT-LIB 2 standard - AddBitvectorFunction(w, "gt_bv", "bvugt", true, Bpl.Type.Bool, false); // Z3 supports this, but it seems not to be in the SMT-LIB 2 standard - // shifts - AddBitvectorShiftFunction(w, "LeftShift_bv", "bvshl"); - AddBitvectorShiftFunction(w, "RightShift_bv", "bvlshr"); - // rotates - AddBitvectorShiftFunction(w, "LeftRotate_bv", "ext_rotate_left"); - AddBitvectorShiftFunction(w, "RightRotate_bv", "ext_rotate_right"); - // conversion functions - AddBitvectorNatConversionFunction(w); - } - - foreach (TopLevelDecl d in program.SystemModuleManager.SystemModule.TopLevelDecls) { - CurrentDeclaration = d; - if (d is AbstractTypeDecl abstractType) { - GetOrCreateTypeConstructor(abstractType); - AddClassMembers(abstractType, true, true); - } else if (d is NewtypeDecl) { - var dd = (NewtypeDecl)d; - AddTypeDecl(dd); - AddClassMembers(dd, true, true); - } else if (d is SubsetTypeDecl) { - AddTypeDecl((SubsetTypeDecl)d); - } else if (d is TypeSynonymDecl) { - // do nothing, just bypass type synonyms in the translation - } else if (d is DatatypeDecl) { - var dd = (DatatypeDecl)d; - AddDatatype(dd); - AddClassMembers(dd, true, true); - } else if (d is ArrowTypeDecl) { - var ad = (ArrowTypeDecl)d; - GetClassTyCon(ad); - AddArrowTypeAxioms(ad); - } else if (d is ClassLikeDecl) { - var cl = (ClassLikeDecl)d; - AddClassMembers(cl, true, true); - if (cl.NonNullTypeDecl != null) { - AddTypeDecl(cl.NonNullTypeDecl); - } - } else { - Contract.Assert(d is ValuetypeDecl); - } - } + AddPreludeBoogieDefinitions(); ComputeFunctionFuel(); // compute which function needs fuel constants. @@ -876,171 +817,6 @@ public static IEnumerable VerifiableModules(Program p) { } } - /// - /// Declare and add to the sink a Boogie function named "namePrefix + w". - /// If "binary", then the function takes two arguments; otherwise, it takes one. Arguments have the type - /// corresponding to the Dafny type for w-width bitvectors. - /// The function's result type is the same as the argument type, unless "resultType" is non-null, in which - /// case the function's result type is "resultType". - /// For w > 0: - /// Attach an attribute {:bvbuiltin smtFunctionName}. - /// For w == 0: - /// Attach an attribute {:inline} and add a .Body to the function. - /// If "resultType" is null, then use 0 as the body; otherwise, use "bodyForBv0" as the body (which - /// assumes "resultType" is actually Bpl.Type.Bool). - /// - private void AddBitvectorFunction(int w, string namePrefix, string smtFunctionName, bool binary = true, Bpl.Type resultType = null, bool bodyForBv0 = false) { - Contract.Requires(0 <= w); - Contract.Requires(namePrefix != null); - Contract.Requires(smtFunctionName != null); - var tok = Token.NoToken; - var t = BplBvType(w); - List args; - if (binary) { - var a0 = BplFormalVar(null, t, true); - var a1 = BplFormalVar(null, t, true); - args = new List() { a0, a1 }; - } else { - var a0 = BplFormalVar(null, t, true); - args = new List() { a0 }; - } - var r = BplFormalVar(null, resultType ?? t, false); - Bpl.QKeyValue attr; - if (w == 0) { - attr = InlineAttribute(tok); - } else { - attr = new Bpl.QKeyValue(tok, "bvbuiltin", new List() { smtFunctionName }, null); - } - var func = new Bpl.Function(tok, namePrefix + w, new List(), args, r, null, attr); - if (w == 0) { - if (resultType != null) { - func.Body = Bpl.Expr.Literal(bodyForBv0); - } else { - func.Body = BplBvLiteralExpr(tok, BaseTypes.BigNum.ZERO, w); - } - } - sink.AddTopLevelDeclaration(func); - } - - private void AddBitvectorShiftFunction(int w, string namePrefix, string smtFunctionName) { - Contract.Requires(0 <= w); - Contract.Requires(namePrefix != null); - Contract.Requires(smtFunctionName != null); - var tok = Token.NoToken; - var t = BplBvType(w); - List args; - var a0 = BplFormalVar(null, t, true); - var a1 = BplFormalVar(null, t, true); - args = new List() { a0, a1 }; - var r = BplFormalVar(null, t, false); - Bpl.QKeyValue attr; - if (w == 0) { - attr = InlineAttribute(tok); - } else { - attr = new Bpl.QKeyValue(tok, "bvbuiltin", new List() { smtFunctionName }, null); - } - var func = new Bpl.Function(tok, namePrefix + w, new List(), args, r, null, attr); - if (w == 0) { - func.Body = BplBvLiteralExpr(tok, BaseTypes.BigNum.ZERO, w); - } - sink.AddTopLevelDeclaration(func); - } - - private void AddBitvectorNatConversionFunction(int w) { - Contract.Requires(0 <= w); - var tok = Token.NoToken; - var bv = BplBvType(w); - Bpl.QKeyValue attr; - Bpl.Function func; - - // function {:bvbuiltin "(_ int2bv 67)"} nat_to_bv67(int) : bv67; - // OR: - // function {:inline} nat_to_bv0(int) : Bv0 { ZERO } - if (w == 0) { - attr = InlineAttribute(tok); - } else { - var smt_int2bv = string.Format("(_ int2bv {0})", w); - attr = new Bpl.QKeyValue(tok, "bvbuiltin", new List() { smt_int2bv }, null); // SMT-LIB 2 calls this function nat2bv, but Z3 apparently calls it int2bv - } - func = new Bpl.Function(tok, "nat_to_bv" + w, new List(), - new List() { BplFormalVar(null, Bpl.Type.Int, true) }, BplFormalVar(null, bv, false), - null, attr); - if (w == 0) { - func.Body = BplBvLiteralExpr(tok, BaseTypes.BigNum.ZERO, w); - } - sink.AddTopLevelDeclaration(func); - - if (w == 0) { - // function {:inline} nat_from_bv0_smt(Bv0) : int { 0 } - attr = InlineAttribute(tok); - func = new Bpl.Function(tok, "nat_from_bv" + w, new List(), - new List() { BplFormalVar(null, bv, true) }, BplFormalVar(null, Bpl.Type.Int, false), - null, attr); - func.Body = Bpl.Expr.Literal(0); - sink.AddTopLevelDeclaration(func); - } else { - // function {:bvbuiltin "bv2int"} smt_nat_from_bv67(bv67) : int; - attr = new Bpl.QKeyValue(tok, "bvbuiltin", new List() { "bv2int" }, null); // SMT-LIB 2 calls this function bv2nat, but Z3 apparently calls it bv2int - var smtFunc = new Bpl.Function(tok, "smt_nat_from_bv" + w, new List(), - new List() { BplFormalVar(null, bv, true) }, BplFormalVar(null, Bpl.Type.Int, false), - null, attr); - sink.AddTopLevelDeclaration(smtFunc); - // function nat_from_bv67(bv67) : int; - func = new Bpl.Function(tok, "nat_from_bv" + w, new List(), - new List() { BplFormalVar(null, bv, true) }, BplFormalVar(null, Bpl.Type.Int, false), - null, null); - sink.AddTopLevelDeclaration(func); - // axiom (forall b: bv67 :: { nat_from_bv67(b) } - // 0 <= nat_from_bv67(b) && nat_from_bv67(b) < 0x8_0000_0000_0000_0000 && - // nat_from_bv67(b) == smt_nat_from_bv67(b)); - var bVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "b", BplBvType(w))); - var b = new Bpl.IdentifierExpr(tok, bVar); - var bv2nat = FunctionCall(tok, "nat_from_bv" + w, Bpl.Type.Int, b); - var smt_bv2nat = FunctionCall(tok, "smt_nat_from_bv" + w, Bpl.Type.Int, b); - var body = BplAnd(BplAnd( - Bpl.Expr.Le(Bpl.Expr.Literal(0), bv2nat), - Bpl.Expr.Lt(bv2nat, Bpl.Expr.Literal(BaseTypes.BigNum.FromBigInt(BigInteger.One << w)))), - Bpl.Expr.Eq(bv2nat, smt_bv2nat)); - var ax = new Bpl.ForallExpr(tok, new List() { bVar }, BplTrigger(bv2nat), body); - sink.AddTopLevelDeclaration(new Bpl.Axiom(tok, ax)); - } - } - - private void ComputeFunctionFuel() { - foreach (ModuleDefinition m in program.RawModules()) { - foreach (TopLevelDecl d in m.TopLevelDecls) { - if (d is TopLevelDeclWithMembers) { - var c = (TopLevelDeclWithMembers)d; - foreach (MemberDecl member in c.Members) { - if (member is Function && RevealedInScope(member)) { - Function f = (Function)member; - // declare the fuel constant - if (f.IsFueled) { - // const BaseFuel_FunctionA : LayerType - Bpl.Constant baseFuel = new Bpl.Constant(f.tok, new Bpl.TypedIdent(f.tok, "BaseFuel_" + f.FullName, Predef.LayerType), false); - sink.AddTopLevelDeclaration(baseFuel); - Bpl.Expr baseFuel_expr = new Bpl.IdentifierExpr(f.tok, baseFuel); - // const StartFuel_FunctionA : LayerType - Bpl.Constant startFuel = new Bpl.Constant(f.tok, new Bpl.TypedIdent(f.tok, "StartFuel_" + f.FullName, Predef.LayerType), false); - sink.AddTopLevelDeclaration(startFuel); - Bpl.Expr startFuel_expr = new Bpl.IdentifierExpr(f.tok, startFuel); - // const StartFuelAssert_FunctionA : LayerType - Bpl.Constant startFuelAssert = new Bpl.Constant(f.tok, new Bpl.TypedIdent(f.tok, "StartFuelAssert_" + f.FullName, Predef.LayerType), false); - sink.AddTopLevelDeclaration(startFuelAssert); - Bpl.Expr startFuelAssert_expr = new Bpl.IdentifierExpr(f.tok, startFuelAssert); - this.functionFuel.Add(new FuelConstant(f, baseFuel_expr, startFuel_expr, startFuelAssert_expr)); - } - - if (f.IsOpaque || f.IsMadeImplicitlyOpaque(options)) { - CreateRevealableConstant(f); - } - } - } - } - } - } - } - private void CreateRevealableConstant(Function f) { if (!this.functionReveals.ContainsKey(f)) { // const reveal_FunctionA : bool @@ -1060,176 +836,6 @@ private void CreateRevealableConstant(Function f) { } } - /// - /// For every revealed type (class or trait) C that extends a trait J, add: - /// axiom (forall T: Ty, $o: ref :: - /// { $Is($o, C(T)) } - /// $o != null && $Is($o, C(T)) ==> $Is($o, J(G(T))); - /// axiom (forall T: Ty, $Heap: Heap, $o: ref :: - /// { $IsAlloc($o, C(T), $Heap) } - /// $o != null && $IsAlloc($o, C(T), $Heap) ==> $IsAlloc($o, J(G(T)), $Heap); - /// Note: - /// It is sometimes useful also to be able to determine the _absence_ of trait-parent relationships. - /// For example, suppose one can tell from the looking at the "extends" clauses in a program - /// that a class C does not (directly or transitively) extend a trait T. Then, given variables c and t - /// of static types C and T, respectively, the verifier should be able to infer c != t. This is not - /// possible with the axioms below. It will require an axiomatization of _all_ possible parent traits, not just - /// saying that some are possible. When this becomes needed, the axiomatization will need to be - /// embellished. - /// - private void AddTraitParentAxioms() { - foreach (ModuleDefinition m in program.RawModules()) { - foreach (var c in m.TopLevelDecls.OfType().Where(RevealedInScope)) { - foreach (var parentTypeInExtendsClause in c.ParentTraits) { - var childType = UserDefinedType.FromTopLevelDecl(c.tok, c); - var parentType = (UserDefinedType)parentTypeInExtendsClause; - if (parentType.IsRefType) { - // use the nullable versions of the types - Contract.Assert(childType.IsRefType); - parentType = UserDefinedType.CreateNullableType(parentType); - } else { - childType = UserDefinedType.CreateNonNullTypeIfReferenceType(childType); - } - - var bvarsTypeParameters = MkTyParamBinders(GetTypeParams(c), out _); - - // axioms with "$IsBox(...) ==> ..." and "$IsAllocBox(...) ==> ..." - TypeBoundAxiomExpressions(c.tok, bvarsTypeParameters, childType, new List() { parentType }, - out var isBoxExpr, out var isAllocBoxExpr); - - var heapVar = BplBoundVar("$heap", Predef.HeapType, out var heap); - var oVar = BplBoundVar("$o", TrType(childType), out var o); - - var oj = BoxifyForTraitParent(c.tok, o, ((UserDefinedType)parentType.NormalizeExpand()).ResolvedClass, childType); - - // axiom (forall T: Ty, $o: ref :: - // { $Is($o, C(T)) } - // $Is($o, C(T)) ==> $Is($o, J(G(T))); - var isC = MkIs(o, childType); - var isJ = MkIs(oj, parentType); - var bvs = new List(); - bvs.AddRange(bvarsTypeParameters); - bvs.Add(oVar); - var tr = BplTrigger(isC); - var body = BplImp(isC, isJ); - - sink.AddTopLevelDeclaration(new Bpl.Axiom(c.tok, new Bpl.ForallExpr(c.tok, bvs, tr, body), - $"type axiom for trait parent: {childType.Name} extends {parentType}")); - sink.AddTopLevelDeclaration(new Bpl.Axiom(c.tok, isBoxExpr)); - - // axiom (forall T: Ty, $Heap: Heap, $o: ref :: - // { $IsAlloc($o, C(T), $Heap) } - // $IsAlloc($o, C(T), $Heap) ==> $IsAlloc($o, J(G(T)), $Heap); - var isAllocC = MkIsAlloc(o, childType, heap); - var isAllocJ = MkIsAlloc(oj, parentType, heap); - bvs = new List(); - bvs.AddRange(bvarsTypeParameters); - bvs.Add(oVar); - bvs.Add(heapVar); - tr = BplTrigger(isAllocC); - body = BplImp(isAllocC, isAllocJ); - sink.AddTopLevelDeclaration(new Bpl.Axiom(c.tok, new Bpl.ForallExpr(c.tok, bvs, tr, body), - $"allocation axiom for trait parent: {childType.Name} extends {parentType}")); - sink.AddTopLevelDeclaration(new Bpl.Axiom(c.tok, isAllocBoxExpr)); - } - } - } - } - - /// - /// Construct an expression denoting the equality of e0 and e1, taking advantage of - /// any available extensional equality based on the given Dafny type. - /// - public Expr TypeSpecificEqual(IToken tok, Dafny.Type type, Expr e0, Expr e1) { - Contract.Requires(tok != null); - Contract.Requires(type != null); - Contract.Requires(e0 != null); - Contract.Requires(e1 != null); - - type = type.NormalizeToAncestorType(); - if (type.AsSetType != null) { - var finite = type.AsSetType.Finite; - return FunctionCall(tok, finite ? BuiltinFunction.SetEqual : BuiltinFunction.ISetEqual, null, e0, e1); - } else if (type.AsMapType != null) { - var finite = type.AsMapType.Finite; - return FunctionCall(tok, finite ? BuiltinFunction.MapEqual : BuiltinFunction.IMapEqual, null, e0, e1); - } else if (type.AsMultiSetType != null) { - return FunctionCall(tok, BuiltinFunction.MultiSetEqual, null, e0, e1); - } else if (type.AsSeqType != null) { - return FunctionCall(tok, BuiltinFunction.SeqEqual, null, e0, e1); - } else if (type.IsIndDatatype) { - return FunctionCall(tok, type.AsIndDatatype.FullSanitizedName + "#Equal", Bpl.Type.Bool, e0, e1); - } else { - return Bpl.Expr.Eq(e0, e1); - } - } - - /// - /// Return a sequence of expressions whose conjunction denotes a memberwise equality of "dt". Recursive - /// codatatype equalities are written in one of the following ways: - /// If the codatatype equality is on a type outside the SCC of "dt", then resort to ordinary equality. - /// Else if the k==null, then: - /// Depending on "limited", use the #2, #1, or #0 (limited) form of codatatype equality. - /// Else: - /// Depending on "limited", use the #2, #1, or #0 (limited) form of prefix equality, passing "k" - /// as the first argument. - /// - IEnumerable CoPrefixEquality(IToken tok, CoDatatypeDecl dt, List largs, List rargs, Bpl.Expr k, Bpl.Expr l, Bpl.Expr A, Bpl.Expr B, bool conjuncts = false) { - Contract.Requires(tok != null); - Contract.Requires(dt != null); - Contract.Requires(A != null); - Contract.Requires(B != null); - Contract.Requires(l != null); - Contract.Requires(Predef != null); - var etran = new ExpressionTranslator(this, Predef, dt.tok, dt); - // For example, for possibly infinite lists: - // codatatype SList = Nil | SCons(head: T, tail: SList); - // produce with conjucts=false (default): - // (A.Nil? && B.Nil?) || - // (A.Cons? && B.Cons? && A.head == B.head && Equal(k, A.tail, B.tail)) - // - // with conjuncts=true: - // (A.Nil? ==> B.Nil?) && - // (A.Cons? ==> (B.Cons? && A.head == B.head && Equal(k, A.tail, B.tail))) - - Dictionary lsu = Util.Dict(GetTypeParams(dt), largs); - Dictionary rsu = Util.Dict(GetTypeParams(dt), rargs); - - foreach (var ctor in dt.Ctors) { - Bpl.Expr aq = new Bpl.NAryExpr(tok, new Bpl.FunctionCall(GetReadonlyField(ctor.QueryField)), new List { A }); - Bpl.Expr bq = new Bpl.NAryExpr(tok, new Bpl.FunctionCall(GetReadonlyField(ctor.QueryField)), new List { B }); - Bpl.Expr chunk = Bpl.Expr.True; - foreach (var dtor in ctor.Destructors) { // note, ctor.Destructors has a field for every constructor parameter, whether or not the parameter was named in the source - var a = new Bpl.NAryExpr(tok, new Bpl.FunctionCall(GetReadonlyField(dtor)), new List { A }); - var b = new Bpl.NAryExpr(tok, new Bpl.FunctionCall(GetReadonlyField(dtor)), new List { B }); - var ty = dtor.Type; - Bpl.Expr q; - var codecl = ty.AsCoDatatype; - if (codecl != null && codecl.SscRepr == dt.SscRepr) { - var lexprs = Map(ty.TypeArgs, tt => tt.Subst(lsu)); - var rexprs = Map(ty.TypeArgs, tt => tt.Subst(rsu)); - q = CoEqualCall(codecl, lexprs, rexprs, k, l, a, b); - } else { - // ordinary equality; let the usual translation machinery figure out the translation - var tyA = ty.Subst(lsu); - var tyB = ty.Subst(rsu); - var aa = CondApplyUnbox(tok, a, ty, tyA); - var bb = CondApplyUnbox(tok, b, ty, tyB); - var equal = new BinaryExpr(tok, BinaryExpr.Opcode.Eq, new BoogieWrapper(aa, tyA), new BoogieWrapper(bb, tyB)); - equal.ResolvedOp = ModuleResolver.ResolveOp(equal.Op, tyA, tyB); // resolve here - equal.Type = Type.Bool; // resolve here - q = etran.TrExpr(equal); - } - chunk = BplAnd(chunk, q); - } - if (conjuncts) { - yield return Bpl.Expr.Binary(new NestedToken(tok, ctor.tok), BinaryOperator.Opcode.Imp, aq, BplAnd(bq, chunk)); - } else { - yield return BplAnd(BplAnd(aq, bq), BplImp(BplAnd(aq, bq), chunk)); - } - } - } - public Bpl.Expr LayerSucc(Bpl.Expr e, int amt = 1) { if (amt == 0) { return e; @@ -1241,47 +847,6 @@ public Bpl.Expr LayerSucc(Bpl.Expr e, int amt = 1) { } } - // Makes a call to equality, if k is null, or otherwise prefix equality. For codatatypes. - Bpl.Expr CoEqualCall(CoDatatypeDecl codecl, List largs, List rargs, Bpl.Expr k, Bpl.Expr l, Bpl.Expr A, Bpl.Expr B, Bpl.IToken tok = null) { - Contract.Requires(codecl != null); - Contract.Requires(largs != null); - Contract.Requires(rargs != null); - Contract.Requires(l != null); - Contract.Requires(A != null); - Contract.Requires(B != null); - if (tok == null) { - tok = A.tok; - } - List args = Concat(largs, rargs); - if (k != null) { - args.Add(k); - } - args.AddRange(new List { l, A, B }); - var fn = k == null ? CoEqualName(codecl) : CoPrefixName(codecl); - return FunctionCall(tok, fn, Bpl.Type.Bool, args); - } - - // Same as above, but with Dafny-typed type-argument lists - Bpl.Expr CoEqualCall(CoDatatypeDecl codecl, List largs, List rargs, Bpl.Expr k, Bpl.Expr l, Bpl.Expr A, Bpl.Expr B, IToken tok = null) { - Contract.Requires(codecl != null); - Contract.Requires(largs != null); - Contract.Requires(rargs != null); - Contract.Requires(l != null); - Contract.Requires(A != null); - Contract.Requires(B != null); - return CoEqualCall(codecl, Map(largs, TypeToTy), Map(rargs, TypeToTy), k, l, A, B, tok); - } - - static string CoEqualName(CoDatatypeDecl codecl) { - Contract.Requires(codecl != null); - return "$Eq#" + codecl.FullSanitizedName; - } - - static string CoPrefixName(CoDatatypeDecl codecl) { - Contract.Requires(codecl != null); - return "$PrefixEq#" + codecl.FullSanitizedName; - } - void CreateBoundVariables(List formals, out List bvs, out List args) where VT : IVariable { Contract.Requires(formals != null); Contract.Ensures(Contract.ValueAtReturn(out bvs).Count == Contract.ValueAtReturn(out args).Count); @@ -1300,59 +865,6 @@ void CreateBoundVariables(List formals, out List bvs, out List } } - // This one says that this is /directly/ allocated, not that its "children" are, - // i.e. h[x, alloc] - public Bpl.Expr IsAlloced(IToken tok, Bpl.Expr heapExpr, Bpl.Expr e) { - Contract.Requires(tok != null); - Contract.Requires(heapExpr != null); - Contract.Requires(e != null); - Contract.Ensures(Contract.Result() != null); - - return ApplyUnbox(tok, ReadHeap(tok, heapExpr, e, Predef.Alloc(tok)), Bpl.Type.Bool); - } - - /// - /// Returns read(heap: Heap, r: ref, f: Field) : Box. - /// - public Bpl.Expr ReadHeap(IToken tok, Expr heap, Expr r, Expr f) { - Contract.Requires(tok != null); - Contract.Requires(heap != null); - Contract.Requires(r != null); - Contract.Requires(f != null); - Contract.Ensures(Contract.Result() != null); - - var res = new Bpl.NAryExpr(tok, - new Bpl.FunctionCall(new Bpl.IdentifierExpr(tok, "read", Predef.BoxType)), - new List { heap, r, f }); - res.Type = Predef.BoxType; - return res; - } - - public Bpl.NAryExpr ReadHeap(IToken tok, Expr heap, Expr r) { - Contract.Requires(tok != null); - Contract.Requires(heap != null); - Contract.Requires(r != null); - Contract.Ensures(Contract.Result() != null); - return new Bpl.NAryExpr(tok, new Bpl.MapSelect(tok, 1), new List { heap, r }); - } - - /// - /// Returns update(h: Heap, r: ref, f: Field, v: Box) : Heap. - /// - public Boogie.NAryExpr UpdateHeap(IToken tok, Expr heap, Expr r, Expr f, Expr v) { - Contract.Requires(tok != null); - Contract.Requires(heap != null); - Contract.Requires(r != null); - Contract.Requires(f != null); - Contract.Requires(v != null); - Contract.Ensures(Contract.Result() != null); - - - return new Boogie.NAryExpr(tok, - new Boogie.FunctionCall(new Boogie.IdentifierExpr(tok, "update", heap.Type)), - new List { heap, r, f, ApplyBox(tok, v) }); - } - public Bpl.Expr DType(Bpl.Expr e, Bpl.Expr type) { return Bpl.Expr.Eq(FunctionCall(e.tok, BuiltinFunction.DynamicType, null, e), type); } @@ -1371,38 +883,6 @@ public Bpl.Expr GetArrayIndexFieldName(IToken tok, List indices) { return fieldName; } - /// - /// Returns true if the body of function "f" is available in module "context". - /// This happens when the following conditions all hold: - /// - "f" has a body - /// - "f" is not opaque - /// - bool FunctionBodyIsAvailable(Function f, ModuleDefinition context, VisibilityScope scope) { - Contract.Requires(f != null); - Contract.Requires(context != null); - return f.Body != null && !IsOpaque(f, options) && f.IsRevealedInScope(scope); - } - public static bool IsOpaque(MemberDecl f, DafnyOptions options) { - Contract.Requires(f != null); - if (f is Function f1) { - return Attributes.Contains(f.Attributes, "opaque") || f.IsOpaque || f1.IsMadeImplicitlyOpaque(options); - } else { - return Attributes.Contains(f.Attributes, "opaque") || f.IsOpaque; - } - } - static bool IsOpaqueRevealLemma(Method m) { - Contract.Requires(m != null); - return Attributes.Contains(m.Attributes, "opaque_reveal"); - } - - - void AddEnsures(List list, Bpl.Ensures ens) { - list.Add(ens); - if (!ens.Free) { - this.assertionCount++; - } - } - private Implementation AddImplementationWithAttributes(IToken tok, Procedure proc, List inParams, List outParams, Variables localVariables, StmtList stmts, QKeyValue kv) { Bpl.Implementation impl = new Bpl.Implementation(tok, proc.Name, @@ -1443,71 +923,6 @@ public static Bpl.QKeyValue InlineAttribute(Bpl.IToken tok, Bpl.QKeyValue/*?*/ n return new QKeyValue(tok, "inline", new List(), next); } - class Specialization { - public readonly List Formals; - public readonly List ReplacementExprs; - public readonly List ReplacementFormals; - public readonly Dictionary SubstMap; - readonly BoogieGenerator boogieGenerator; - [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, BoogieGenerator boogieGenerator) { - Contract.Requires(formal is Formal || formal is BoundVar); - Contract.Requires(mc != null); - Contract.Requires(prev == null || formal is BoundVar || !prev.Formals.Contains((Formal)formal)); - Contract.Requires(boogieGenerator != null); - - this.boogieGenerator = boogieGenerator; - - List rArgs = new List(); - foreach (BoundVar p in mc.Arguments) { - IdentifierExpr ie = new IdentifierExpr(p.tok, p.AssignUniqueName(boogieGenerator.CurrentDeclaration.IdGenerator)); - ie.Var = p; ie.Type = ie.Var.Type; // resolve it here - rArgs.Add(ie); - } - // create and resolve datatype value - var r = new DatatypeValue(mc.tok, mc.Ctor.EnclosingDatatype.Name, mc.Ctor.Name, rArgs); - r.Ctor = mc.Ctor; - r.Type = new UserDefinedType(mc.tok, mc.Ctor.EnclosingDatatype.Name, new List()/*this is not right, but it seems like it won't matter here*/); - - Dictionary substMap = new Dictionary(); - substMap.Add(formal, r); - - // Fill in the fields - Formals = new List(); - ReplacementExprs = new List(); - ReplacementFormals = new List(); - SubstMap = new Dictionary(); - if (prev != null) { - Formals.AddRange(prev.Formals); - foreach (var e in prev.ReplacementExprs) { - ReplacementExprs.Add(BoogieGenerator.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, BoogieGenerator.Substitute(entry.Value, null, substMap)); - } - } - if (formal is Formal) { - Formals.Add((Formal)formal); - ReplacementExprs.Add(r); - } - ReplacementFormals.AddRange(mc.Arguments); - SubstMap.Add(formal, r); - } - } - (int olderParameterCount, Bpl.Expr olderCondition) OlderCondition(Function f, Bpl.Expr funcAppl, List inParams) { Contract.Requires(f != null); Contract.Requires(funcAppl != null); diff --git a/Source/DafnyCore/Verifier/Specialization.cs b/Source/DafnyCore/Verifier/Specialization.cs new file mode 100644 index 00000000000..da04a8b09f5 --- /dev/null +++ b/Source/DafnyCore/Verifier/Specialization.cs @@ -0,0 +1,69 @@ +using System.Collections.Generic; +using System.Diagnostics.Contracts; + +namespace Microsoft.Dafny; + +class Specialization { + public readonly List Formals; + public readonly List ReplacementExprs; + public readonly List ReplacementFormals; + public readonly Dictionary SubstMap; + readonly BoogieGenerator boogieGenerator; + [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, BoogieGenerator boogieGenerator) { + Contract.Requires(formal is Formal || formal is BoundVar); + Contract.Requires(mc != null); + Contract.Requires(prev == null || formal is BoundVar || !prev.Formals.Contains((Formal)formal)); + Contract.Requires(boogieGenerator != null); + + this.boogieGenerator = boogieGenerator; + + List rArgs = new List(); + foreach (BoundVar p in mc.Arguments) { + IdentifierExpr ie = new IdentifierExpr(p.tok, p.AssignUniqueName(boogieGenerator.CurrentDeclaration.IdGenerator)); + ie.Var = p; ie.Type = ie.Var.Type; // resolve it here + rArgs.Add(ie); + } + // create and resolve datatype value + var r = new DatatypeValue(mc.tok, mc.Ctor.EnclosingDatatype.Name, mc.Ctor.Name, rArgs); + r.Ctor = mc.Ctor; + r.Type = new UserDefinedType(mc.tok, mc.Ctor.EnclosingDatatype.Name, new List()/*this is not right, but it seems like it won't matter here*/); + + Dictionary substMap = new Dictionary(); + substMap.Add(formal, r); + + // Fill in the fields + Formals = new List(); + ReplacementExprs = new List(); + ReplacementFormals = new List(); + SubstMap = new Dictionary(); + if (prev != null) { + Formals.AddRange(prev.Formals); + foreach (var e in prev.ReplacementExprs) { + ReplacementExprs.Add(BoogieGenerator.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, BoogieGenerator.Substitute(entry.Value, null, substMap)); + } + } + if (formal is Formal) { + Formals.Add((Formal)formal); + ReplacementExprs.Add(r); + } + ReplacementFormals.AddRange(mc.Arguments); + SubstMap.Add(formal, r); + } +} \ No newline at end of file