Set up for a future mode /allocated:4 that also adds allocated antecedents for bound variables that are not already bounded by their types or range expressions.

Author: RustanLeino

Source/Dafny/DafnyAst.cs

@@ -276,10 +276,12 @@ private Expression ArrowSubtypeConstraint(IToken tok, BoundVar id, Function memb
       // forall x0,x1,x2 :: f.requires(x0,x1,x2)
       var bvs = new List<BoundVar>();
       var args = new List<Expression>();
+      var bounds = new List<ComprehensionExpr.BoundedPool>();
       for (int i = 0; i < tps.Count - 1; i++) {
         var bv = new BoundVar(tok, "x" + i, new UserDefinedType(tps[i]));
         bvs.Add(bv);
         args.Add(new IdentifierExpr(tok, bv));
+        bounds.Add(new ComprehensionExpr.SpecialAllocIndependenceAllocatedBoundedPool());
       }
       var fn = new MemberSelectExpr(tok, f, member.Name) {
         Member = member,
@@ -294,8 +296,7 @@ private Expression ArrowSubtypeConstraint(IToken tok, BoundVar id, Function memb
         body = Expression.CreateEq(body, emptySet, member.ResultType);
       }
       if (tps.Count > 1) {
-        body = new ForallExpr(tok, bvs, null, body, null);
-        body.Type = Type.Bool;  // resolve here
+        body = new ForallExpr(tok, bvs, null, body, null) { Type = Type.Bool, Bounds = bounds };
       }
       return body;
     }
@@ -9693,6 +9694,7 @@ public enum PoolVirtues { None = 0, Finite = 1, Enumerable = 2, IndependentOfAll
       /// 
       /// 0: AllocFreeBoundedPool
       /// 0: ExplicitAllocatedBoundedPool
+      /// 0: SpecialAllocIndependenceAllocatedBoundedPool
       /// 
       /// 1: WiggleWaggleBound
       /// 
@@ -9744,6 +9746,12 @@ public static List<VT> MissingBounds<VT>(List<VT> vars, List<BoundedPool> bounds
         }
         return missing;
       }
+      public static List<bool> HasBounds(List<BoundedPool> bounds, PoolVirtues requiredVirtues = PoolVirtues.None) {
+        Contract.Requires(bounds != null);
+        Contract.Ensures(Contract.Result<List<bool>>() != null);
+        Contract.Ensures(Contract.Result<List<bool>>().Count == bounds.Count);
+        return bounds.ConvertAll(bound => bound != null && (bound.Virtues & requiredVirtues) == requiredVirtues);
+      }
       static List<BoundedPool> CombineIntegerBounds(List<BoundedPool> bounds) {
         var lowerBounds = new List<IntBoundedPool>();
         var upperBounds = new List<IntBoundedPool>();
@@ -9816,6 +9824,13 @@ public ExplicitAllocatedBoundedPool() {
       public override PoolVirtues Virtues => PoolVirtues.Finite | PoolVirtues.IndependentOfAlloc_or_ExplicitAlloc;
       public override int Preference() => 0;
     }
+    public class SpecialAllocIndependenceAllocatedBoundedPool : BoundedPool
+    {
+      public SpecialAllocIndependenceAllocatedBoundedPool() {
+      }
+      public override PoolVirtues Virtues => PoolVirtues.IndependentOfAlloc_or_ExplicitAlloc;
+      public override int Preference() => 0;
+    }
     public class IntBoundedPool : BoundedPool
     {
       public readonly Expression LowerBound;

Source/Dafny/DafnyOptions.cs

@@ -302,7 +302,7 @@ protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.Com
         }
 
         case "allocated": {
-            ps.GetNumericArgument(ref Allocated, 4);
+            ps.GetNumericArgument(ref Allocated, 5);
             return true;
         }
 
@@ -559,6 +559,8 @@ than including DafnyRuntime.cs verbatim.
                     even bound variables in quantifiers.  This option is
                     the easiest to use for heapful code.
                 3 - (default) Frugal use of heap parameters.
+                4 - mode 3 but with alloc antecedents when ranges don't imply
+                    allocatedness.
   /ironDafny    Enable experimental features needed to support Ironclad/Ironfleet. Use of
                 these features may cause your code to become incompatible with future
                 releases of Dafny.

Source/Dafny/Rewriter.cs

@@ -111,6 +111,7 @@ protected override bool VisitOneStmt(Statement stmt, ref bool st) {
             List<Expression> exprList = new List<Expression>();
             ForallExpr expr = new ForallExpr(s.Tok, s.BoundVars, s.Range, term, s.Attributes);
             expr.Type = Type.Bool; // resolve here
+            expr.Bounds = s.Bounds;
             exprList.Add(expr);
             s.ForallExpressions = exprList;
           } else if (s.Kind == ForallStmt.BodyKind.Assign) {
@@ -191,6 +192,7 @@ protected override bool VisitOneStmt(Statement stmt, ref bool st) {
                 if (!usedInversion) {
                   var expr = new ForallExpr(s.Tok, s.BoundVars, s.Range, new BinaryExpr(s.Tok, BinaryExpr.ResolvedOpcode.EqCommon, lhs, rhs), s.Attributes);
                   expr.Type = Type.Bool; // resolve here
+                  expr.Bounds = s.Bounds;
                   exprList.Add(expr);
                 }
                 s.ForallExpressions = exprList;
@@ -212,6 +214,7 @@ protected override bool VisitOneStmt(Statement stmt, ref bool st) {
             List<Expression> exprList = new List<Expression>();
             ForallExpr expr = new ForallExpr(s.Tok, s.BoundVars, s.Range, term, s.Attributes);
             expr.Type = Type.Bool; // resolve here
+            expr.Bounds = s.Bounds;
             exprList.Add(expr);
             s.ForallExpressions = exprList;
           } else {