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

@@ -362,14 +362,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));
@@ -446,7 +442,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);
@@ -489,7 +485,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
@@ -1025,7 +1021,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;
@@ -1075,13 +1071,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)));
  }
  }