Move code out of BoogieGenerator.cs

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<Bpl.Expr>() != null);
+
+      return ApplyUnbox(tok, ReadHeap(tok, heapExpr, e, Predef.Alloc(tok)), Bpl.Type.Bool);
+    }
+
+    /// <summary>
+    /// Returns read(heap: Heap, r: ref, f: Field) : Box.
+    /// </summary>
+    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<Bpl.NAryExpr>() != null);
+
+      var res = new Bpl.NAryExpr(tok,
+        new Bpl.FunctionCall(new Bpl.IdentifierExpr(tok, "read", Predef.BoxType)),
+        new List<Bpl.Expr> { 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<Bpl.NAryExpr>() != null);
+      return new Bpl.NAryExpr(tok, new Bpl.MapSelect(tok, 1), new List<Bpl.Expr> { heap, r });
+    }
+
+    /// <summary>
+    /// Returns update(h: Heap, r: ref, f: Field, v: Box) : Heap.
+    /// </summary>
+    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<Boogie.NAryExpr>() != null);
+
+
+      return new Boogie.NAryExpr(tok,
+        new Boogie.FunctionCall(new Boogie.IdentifierExpr(tok, "update", heap.Type)),
+        new List<Boogie.Expr> { heap, r, f, ApplyBox(tok, v) });
+    }
+
+  /// <summary>
+  /// For every revealed type (class or trait) C<T> that extends a trait J<G(T)>, 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.
+  /// </summary>
+  private void AddTraitParentAxioms() {
+    foreach (ModuleDefinition m in program.RawModules()) {
+      foreach (var c in m.TopLevelDecls.OfType<TopLevelDeclWithMembers>().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<Type>() { 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<Bpl.Variable>();
+          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<Bpl.Variable>();
+          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));
+        }
+      }
+    }
+  }
+}

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 {
+
+
+    /// <summary>
+    /// 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.
+    /// </summary>
+    IEnumerable<Bpl.Expr> CoPrefixEquality(IToken tok, CoDatatypeDecl dt, List<Type> largs, List<Type> 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<T> = Nil | SCons(head: T, tail: SList<T>);
+      // 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<TypeParameter, Type> lsu = Util.Dict(GetTypeParams(dt), largs);
+      Dictionary<TypeParameter, Type> 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<Bpl.Expr> { A });
+        Bpl.Expr bq = new Bpl.NAryExpr(tok, new Bpl.FunctionCall(GetReadonlyField(ctor.QueryField)), new List<Bpl.Expr> { 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<Bpl.Expr> { A });
+          var b = new Bpl.NAryExpr(tok, new Bpl.FunctionCall(GetReadonlyField(dtor)), new List<Bpl.Expr> { 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<Bpl.Expr> largs, List<Bpl.Expr> 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<Bpl.Expr> args = Concat(largs, rargs);
+      if (k != null) {
+        args.Add(k);
+      }
+      args.AddRange(new List<Bpl.Expr> { 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<Type> largs, List<Type> 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;
+    }
+}

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));
   }
+
+
+  /// <summary>
+  /// 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
+  /// </summary>
+  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);
+          }
+        }
+      }
+    }
+  }
 }

Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs

@@ -1940,5 +1940,12 @@ public void TypeBoundAxiomExpressions(IToken tok, List<Bpl.Variable> bvarsTypePa
         isAllocBoxExpr = new Bpl.ForallExpr(tok, vars, BplTrigger(isAllocBox), body);
       }
     }
+
+    void AddEnsures(List<Bpl.Ensures> list, Bpl.Ensures ens) {
+      list.Add(ens);
+      if (!ens.Free) {
+        this.assertionCount++;
+      }
+    }
   }
 }