Removing allocated option and locking in allocated=4

Source/DafnyCore/AST/FreeVariablesUtil.cs

@@ -81,7 +81,7 @@ public static void ComputeFreeVariables(DafnyOptions options, Expression expr,
         usesHeap = true;
       } else if (expr is FunctionCallExpr) {
         var e = (FunctionCallExpr)expr;
-        if (options.AlwaysUseHeap || e.Function == null || e.Function.ReadsHeap) {
+        if (e.Function == null || e.Function.ReadsHeap) {
           usesHeap = true;
         }
         if (e.AtLabel != null) {

Source/DafnyCore/DafnyOptions.cs

@@ -43,11 +43,7 @@ public class DafnyOptions : Bpl.CommandLineOptions {
 
     public ProjectFile ProjectFile { get; set; }
     public Command CurrentCommand { get; set; }
-    public bool NonGhostsUseHeap => Allocated == 1 || Allocated == 2;
-    public bool AlwaysUseHeap => Allocated == 2;
-    public bool CommonHeapUse => Allocated >= 2;
-    public bool FrugalHeapUse => Allocated >= 3;
-    public bool FrugalHeapUseX => Allocated == 4;
+
 
     static DafnyOptions() {
       RegisterLegacyUi(CommonOptionBag.Target, ParseString, "Compilation options", "compileTarget", @"
@@ -348,7 +344,6 @@ public enum IncludesModes {
     public bool IncludeRuntime = true;
     public bool UseJavadocLikeDocstringRewriter = false;
     public bool DisableScopes = false;
-    public int Allocated = 4;
     public bool UseStdin = false;
     public bool WarningsAsErrors = false;
     [CanBeNull] private TestGenerationOptions testGenOptions = null;
@@ -699,14 +694,6 @@ protected bool ParseDafnySpecificOption(string name, Bpl.CommandLineParseState p
             return true;
           }
 
-        case "allocated": {
-            ps.GetIntArgument(ref Allocated, 5);
-            if (Allocated != 4) {
-              Printer.AdvisoryWriteLine(OutputWriter, "The /allocated:<n> option is deprecated");
-            }
-            return true;
-          }
-
         case "optimizeResolution": {
             int d = 2;
             if (ps.GetIntArgument(ref d, 3)) {
@@ -1397,31 +1384,6 @@ quantifiers and lemmas.
     1 - A compiled method, constructor, or iterator is allowed to have
        print effects only if it is marked with {{:print}}.
 
-/allocated:<n>
-    This option is deprecated. Going forward, only what is /allocated:4
-    will be supported.
-    Specify defaults for where Dafny should assert and assume
-    allocated(x) for various parameters x, local variables x, bound
-    variables x, etc. Lower <n> may require more manual allocated(x)
-    annotations and thus may be more difficult to use. Warning: this
-    option should be chosen consistently across an entire project; it
-    would be unsound to use different defaults for different files or
-    modules within a project. And even so, modes /allocated:0 and
-    /allocated:1 let functions depend on the allocation state, which is
-    not sound in general.
-
-    0 - Nowhere (never assume/assert allocated(x) by default).
-    1 - Assume allocated(x) only for non-ghost variables and fields
-        (these assumptions are free, since non-ghost variables always
-        contain allocated values at run-time). This option may speed up
-        verification relative to /allocated:2.
-    2 - Assert/assume allocated(x) on all variables, even bound
-        variables in quantifiers. This option is the easiest to use for
-        heapful code.
-    3 - Frugal use of heap parameter (not sound).
-    4 - (default) Mode 3 but with alloc antecedents when ranges don't imply
-        allocatedness.
-
 /definiteAssignment:<n>
     0 - Ignores definite-assignment rules. This mode is for testing
         only--it is not sound.

Source/DafnyCore/Resolver/BoundsDiscovery.cs

@@ -194,7 +194,7 @@ protected override bool VisitOneExpression(Expression expr, BoundsDiscoveryConte
           }
           if (whereToLookForBounds != null) {
             e.Bounds = DiscoverBestBounds_MultipleVars_AllowReordering(e.BoundVars, whereToLookForBounds, polarity);
-            if (2 <= reporter.Options.Allocated && !context.AllowedToDependOnAllocationState) {
+            if (!context.AllowedToDependOnAllocationState) {
               foreach (var bv in ComprehensionExpr.BoundedPool.MissingBounds(e.BoundVars, e.Bounds,
                          ComprehensionExpr.BoundedPool.PoolVirtues.IndependentOfAlloc)) {
                 var how = Attributes.Contains(e.Attributes, "_reads") ? "(implicitly by using a function in a reads clause) " : "";

Source/DafnyCore/Resolver/NameResolutionAndTypeInference.cs

@@ -670,7 +670,7 @@ public void ResolveExpressionX(Expression expr, ResolutionContext resolutionCont
           case UnaryOpExpr.Opcode.Allocated:
             // the argument is allowed to have any type at all
             expr.Type = Type.Bool;
-            if (2 <= Options.Allocated &&
+            if (
               ((resolutionContext.CodeContext is Function && !resolutionContext.InOld) || resolutionContext.CodeContext is ConstantField || CodeContextWrapper.Unwrap(resolutionContext.CodeContext) is RedirectingTypeDecl)) {
               var declKind = CodeContextWrapper.Unwrap(resolutionContext.CodeContext) is RedirectingTypeDecl redir ? redir.WhatKind : ((MemberDecl)resolutionContext.CodeContext).WhatKind;
               reporter.Error(MessageSource.Resolver, expr, "a {0} definition is not allowed to depend on the set of allocated references", declKind);

Source/DafnyCore/Verifier/Translator.ClassMembers.cs

@@ -360,14 +360,10 @@ private void AddInstanceFieldAllocationAxioms(Bpl.Declaration fieldDeclaration,
       Bpl.Expr is_hf, isalloc_hf = null;
       if (is_array) {
         is_hf = MkIs(oDotF, tyexprs[0], true);
-        if (options.CommonHeapUse || options.NonGhostsUseHeap) {
-          isalloc_hf = MkIsAlloc(oDotF, tyexprs[0], h, true);
-        }
+        isalloc_hf = MkIsAlloc(oDotF, tyexprs[0], h, true);
       } else {
         is_hf = MkIs(oDotF, f.Type); // $Is(h[o, f], ..)
-        if (options.CommonHeapUse || (options.NonGhostsUseHeap && !f.IsGhost)) {
-          isalloc_hf = MkIsAlloc(oDotF, f.Type, h); // $IsAlloc(h[o, f], ..)
-        }
+        isalloc_hf = MkIsAlloc(oDotF, f.Type, h); // $IsAlloc(h[o, f], ..)
       }
 
       Bpl.Expr ax = BplForall(bvsTypeAxiom, tr, BplImp(ante, is_hf));
@@ -444,7 +440,7 @@ private void AddStaticConstFieldAllocationAxiom(Boogie.Declaration fieldDeclarat
       var isAxiom = new Boogie.Axiom(c.tok, BplImp(heightAntecedent, ax), $"{c}.{f}: Type axiom");
       AddOtherDefinition(fieldDeclaration, isAxiom);
 
-      if (options.CommonHeapUse || (options.NonGhostsUseHeap && !f.IsGhost)) {
+      {
         var hVar = BplBoundVar("$h", predef.HeapType, out var h);
         bvsAllocationAxiom.Add(hVar);
         var isGoodHeap = FunctionCall(c.tok, BuiltinFunction.IsGoodHeap, null, h);
@@ -487,7 +483,7 @@ private void AddClassMember_Function(Function f) {
         AddFuelZeroSynonymAxiom(f);
       }
       // add frame axiom
-      if (options.AlwaysUseHeap || f.ReadsHeap) {
+      if (f.ReadsHeap) {
         AddFrameAxiom(f);
       }
       // add consequence axiom
@@ -1023,7 +1019,7 @@ private Boogie.Axiom FunctionOverrideAxiom(Function f, Function overridingFuncti
       Contract.Requires(overridingFunction.EnclosingClass is TopLevelDeclWithMembers);
       Contract.Ensures(Contract.Result<Boogie.Axiom>() != null);
 
-      bool readsHeap = options.AlwaysUseHeap || f.ReadsHeap || overridingFunction.ReadsHeap;
+      bool readsHeap = f.ReadsHeap || overridingFunction.ReadsHeap;
 
       ExpressionTranslator etran;
       Boogie.BoundVariable bvPrevHeap = null;
@@ -1073,13 +1069,13 @@ private Boogie.Axiom FunctionOverrideAxiom(Function f, Function overridingFuncti
         argsJF.Add(etran.Old.HeapExpr);
         moreArgsCF.Add(etran.Old.HeapExpr);
       }
-      if (options.AlwaysUseHeap || f.ReadsHeap || overridingFunction.ReadsHeap) {
+      if (f.ReadsHeap || overridingFunction.ReadsHeap) {
         var heap = new Boogie.BoundVariable(f.tok, new Boogie.TypedIdent(f.tok, predef.HeapVarName, predef.HeapType));
         forallFormals.Add(heap);
-        if (options.AlwaysUseHeap || f.ReadsHeap) {
+        if (f.ReadsHeap) {
           argsJF.Add(new Boogie.IdentifierExpr(f.tok, heap));
         }
-        if (options.AlwaysUseHeap || overridingFunction.ReadsHeap) {
+        if (overridingFunction.ReadsHeap) {
           moreArgsCF.Add(new Boogie.IdentifierExpr(overridingFunction.tok, heap));
         }
       }

Source/DafnyCore/Verifier/Translator.DataTypes.cs

@@ -650,12 +650,10 @@ private void AddIsAllocConstructorAxiom(DatatypeDecl dt, DatatypeCtor ctor, Bpl.
       Bpl.Expr conj = Bpl.Expr.True;
       for (var i = 0; i < ctor.Formals.Count; i++) {
         var arg = ctor.Formals[i];
-        if (options.CommonHeapUse || (options.NonGhostsUseHeap && !arg.IsGhost)) {
-          conj = BplAnd(conj, MkIsAlloc(args[i], arg.Type, h));
-        }
+        conj = BplAnd(conj, MkIsAlloc(args[i], arg.Type, h));
       }
 
-      if (options.CommonHeapUse || options.NonGhostsUseHeap) {
+      {
         var isGoodHeap = FunctionCall(ctor.tok, BuiltinFunction.IsGoodHeap, null, h);
         var c_alloc = MkIsAlloc(c_params, c_ty, h);
         bvs.Add(hVar);
@@ -687,7 +685,7 @@ private void AddCommonIsAllocConstructorAxiom(DatatypeDecl dt) {
 
       var body = BplImp(BplAnd(isGoodHeap, isPredicate), isAlloc);
 
-      if (options.CommonHeapUse || options.NonGhostsUseHeap) {
+      {
         var tr = BplTrigger(isAlloc);
         var ax = new Bpl.Axiom(dt.tok, BplForall(Snoc(boundVariables, hVar), tr, body), "Datatype $IsAlloc");
         sink.AddTopLevelDeclaration(ax);
@@ -722,9 +720,6 @@ private void MkIsPredicateForDatatype(DatatypeDecl datatypeDecl, out List<Bpl.Va
                    $IsAlloc[Box](Dtor(d), D(G), H))
          */
     private void AddDestructorAxiom(DatatypeDecl dt, DatatypeCtor ctor, Bpl.Function ctorFunction, List<Variable> tyvars, Expr c_ty) {
-      if (!options.CommonHeapUse || options.AlwaysUseHeap) {
-        return;
-      }
 
       var hVar = BplBoundVar("$h", predef.HeapType, out var h);
       for (int i = 0; i < ctor.Formals.Count; i++) {
@@ -799,4 +794,4 @@ private Axiom CreateConstructorIdentifierAxiom(DatatypeCtor ctor, Expr c) {
       return axiom;
     }
   }
-}
+}

Source/DafnyCore/Verifier/Translator.ExpressionTranslator.cs

@@ -1262,10 +1262,7 @@ public Boogie.Expr TrExpr(Expression expr) {
 
                 Boogie.Expr antecedent = Boogie.Expr.True;
 
-                List<bool> freeOfAlloc = null;
-                if (options.FrugalHeapUseX) {
-                  freeOfAlloc = ComprehensionExpr.BoundedPool.HasBounds(e.Bounds, ComprehensionExpr.BoundedPool.PoolVirtues.IndependentOfAlloc_or_ExplicitAlloc);
-                }
+                List<bool> freeOfAlloc = ComprehensionExpr.BoundedPool.HasBounds(e.Bounds, ComprehensionExpr.BoundedPool.PoolVirtues.IndependentOfAlloc_or_ExplicitAlloc);
                 antecedent = BplAnd(antecedent, bodyEtran.TrBoundVariables(e.BoundVars, bvars, false, freeOfAlloc)); // initHeapForAllStmt
 
                 Boogie.QKeyValue kv = TrAttributes(e.Attributes, "trigger");
@@ -1286,10 +1283,8 @@ public Boogie.Expr TrExpr(Expression expr) {
             }
           case SetComprehension comprehension: {
               var e = comprehension;
-              List<bool> freeOfAlloc = null;
-              if (options.FrugalHeapUseX) {
-                freeOfAlloc = ComprehensionExpr.BoundedPool.HasBounds(e.Bounds, ComprehensionExpr.BoundedPool.PoolVirtues.IndependentOfAlloc_or_ExplicitAlloc);
-              }
+              List<bool> freeOfAlloc = ComprehensionExpr.BoundedPool.HasBounds(e.Bounds, ComprehensionExpr.BoundedPool.PoolVirtues.IndependentOfAlloc_or_ExplicitAlloc);
+
               // Translate "set xs | R :: T" into:
               //     lambda y: BoxType :: (exists xs :: CorrectType(xs) && R && y==Box(T))
               // or if "T" is "xs", then:
@@ -1338,10 +1333,7 @@ public Boogie.Expr TrExpr(Expression expr) {
               //          lambda w: BoxType :: G(unbox(w)),
               //          type)".
               List<Variable> bvars = new List<Variable>();
-              List<bool> freeOfAlloc = null;
-              if (options.FrugalHeapUseX) {
-                freeOfAlloc = ComprehensionExpr.BoundedPool.HasBounds(e.Bounds, ComprehensionExpr.BoundedPool.PoolVirtues.IndependentOfAlloc_or_ExplicitAlloc);
-              }
+              List<bool> freeOfAlloc = ComprehensionExpr.BoundedPool.HasBounds(e.Bounds, ComprehensionExpr.BoundedPool.PoolVirtues.IndependentOfAlloc_or_ExplicitAlloc);
 
               Boogie.QKeyValue kv = TrAttributes(e.Attributes, "trigger");
 
@@ -1668,7 +1660,7 @@ public Boogie.Expr TrBoundVariablesRename(List<BoundVar> boundVars, List<Variabl
         if (e.Function is TwoStateFunction) {
           args.Add(OldAt(e.AtLabel).HeapExpr);
         }
-        if (!omitHeapArgument && (options.AlwaysUseHeap || e.Function.ReadsHeap)) {
+        if (!omitHeapArgument && e.Function.ReadsHeap) {
           Contract.Assert(HeapExpr != null);
           args.Add(HeapExpr);
           // If the function doesn't use the heap, but global settings say to use it,
@@ -1820,10 +1812,7 @@ public Boogie.Expr TrInSet_Aux(IToken tok, Boogie.Expr elmt, Boogie.Expr elmtBox
             return BplAnd(typeAntecedent, TrExpr(range));
           } else {
             // exists xs :: CorrectType(xs) && R && elmt==T
-            List<bool> freeOfAlloc = null;
-            if (options.FrugalHeapUseX) {
-              freeOfAlloc = ComprehensionExpr.BoundedPool.HasBounds(compr.Bounds, ComprehensionExpr.BoundedPool.PoolVirtues.IndependentOfAlloc_or_ExplicitAlloc);
-            }
+            List<bool> freeOfAlloc = ComprehensionExpr.BoundedPool.HasBounds(compr.Bounds, ComprehensionExpr.BoundedPool.PoolVirtues.IndependentOfAlloc_or_ExplicitAlloc);
             var bvars = new List<Variable>();
             Boogie.Expr typeAntecedent = TrBoundVariables(compr.BoundVars, bvars, false, freeOfAlloc) ?? Boogie.Expr.True;
             var eq = Boogie.Expr.Eq(elmtBox, BoxIfNecessary(GetToken(compr), TrExpr(compr.Term), compr.Term.Type));

Source/DafnyCore/Verifier/Translator.ExpressionWellformed.cs

@@ -369,7 +369,7 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re
             Bpl.Expr seq = etran.TrExpr(e.Seq);
             if (eSeqType.IsArrayType) {
               builder.Add(Assert(GetToken(e.Seq), Bpl.Expr.Neq(seq, predef.Null), new PODesc.NonNull("array")));
-              if (!options.CommonHeapUse || etran.UsesOldHeap) {
+              if (etran.UsesOldHeap) {
                 builder.Add(Assert(GetToken(e.Seq), MkIsAlloc(seq, eSeqType, etran.HeapExpr), new PODesc.IsAllocated("array", null)));
               }
             }
@@ -437,7 +437,7 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re
             CheckWellformed(e.Array, wfOptions, locals, builder, etran);
             Bpl.Expr array = etran.TrExpr(e.Array);
             builder.Add(Assert(GetToken(e.Array), Bpl.Expr.Neq(array, predef.Null), new PODesc.NonNull("array")));
-            if (!options.CommonHeapUse || etran.UsesOldHeap) {
+            if (etran.UsesOldHeap) {
               builder.Add(Assert(GetToken(e.Array), MkIsAlloc(array, e.Array.Type, etran.HeapExpr), new PODesc.IsAllocated("array", null)));
             }
             for (int idxId = 0; idxId < e.Indices.Count; idxId++) {
@@ -615,7 +615,7 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re
               } else if (e.Receiver.Type.IsArrowType) {
                 CheckFunctionSelectWF("function specification", builder, etran, e.Receiver, "");
               }
-              if (!e.Function.IsStatic && options.CommonHeapUse && !etran.UsesOldHeap) {
+              if (!e.Function.IsStatic && !etran.UsesOldHeap) {
                 // the argument can't be assumed to be allocated for the old heap
                 Type et = UserDefinedType.FromTopLevelDecl(e.tok, e.Function.EnclosingClass).Subst(e.GetTypeArgumentSubstitutions());
                 builder.Add(new Bpl.CommentCmd("assume allocatedness for receiver argument to function"));
@@ -645,7 +645,7 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re
                 CheckSubrange(ee.tok, etran.TrExpr(ee), ee.Type, et, builder);
                 Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(p.tok, lhs, CondApplyBox(p.tok, etran.TrExpr(ee), cce.NonNull(ee.Type), et));
                 builder.Add(cmd);
-                if (options.CommonHeapUse && !etran.UsesOldHeap) {
+                if (!etran.UsesOldHeap) {
                   // the argument can't be assumed to be allocated for the old heap
                   builder.Add(new Bpl.CommentCmd("assume allocatedness for argument to function"));
                   builder.Add(TrAssumeCmd(e.Args[i].tok, MkIsAlloc(lhs, et, etran.HeapExpr)));
@@ -1196,9 +1196,6 @@ void CheckOperand(Expression operand) {
         builder.Add(TrAssumeCmd(expr.tok, Bpl.Expr.Eq(result, bResult)));
         builder.Add(TrAssumeCmd(expr.tok, CanCallAssumption(expr, etran)));
         builder.Add(new CommentCmd("CheckWellformedWithResult: any expression"));
-        if (options.AlwaysUseHeap) {
-          builder.Add(TrAssumeCmd(expr.tok, MkIsAlloc(result, resultType, etran.HeapExpr)));
-        }
         builder.Add(TrAssumeCmd(expr.tok, MkIs(result, resultType)));
       }
     }
@@ -1410,9 +1407,6 @@ void CheckWellformedLetExprWithResult(LetExpr e, WFOptions wfOptions, Bpl.Expr r
           builder.Add(TrAssumeCmd(letBody.tok, Bpl.Expr.Eq(result, bResult)));
           builder.Add(TrAssumeCmd(letBody.tok, CanCallAssumption(letBody, etran)));
           builder.Add(new CommentCmd("CheckWellformedWithResult: Let expression"));
-          if (options.AlwaysUseHeap) {
-            builder.Add(TrAssumeCmd(letBody.tok, MkIsAlloc(result, resultType, etran.HeapExpr)));
-          }
           builder.Add(TrAssumeCmd(letBody.tok, MkIs(result, resultType)));
         }
       }