feat!: Remove /ironFlag flag (#1083)

RustanLeino · davidcok · web-flow · commit c2c5c2cd5b52 · 2021-01-29T21:04:20.000-05:00
* feat!: Remove /ironFlag flag

Also, don’t warn about body-less functions/methods in the parser — this is done by the compiler.

* Remove /ironDafny flag from tests

* Move a test to wish folder

Co-authored-by: David Cok &lt;david.r.cok@gmail.com&gt;
diff --git a/Source/Dafny/Compiler-Csharp.cs b/Source/Dafny/Compiler-Csharp.cs
@@ -1036,12 +1036,6 @@ protected override string TypeName(Type type, TextWriter wr, Bpl.IToken tok, Mem
         bool isHandle = true;
         if (cl != null && Attributes.ContainsBool(cl.Attributes, "handle", ref isHandle) && isHandle) {
           return "ulong";
-        } else if (DafnyOptions.O.IronDafny &&
-            !(xType is ArrowType) &&
-            cl != null &&
-            cl.EnclosingModuleDefinition != null &&
-            !cl.EnclosingModuleDefinition.IsDefaultModule) {
-          s = cl.FullCompileName;
         }
         return TypeName_UDT(s, udt, wr, udt.tok);
       } else if (xType is SetType) {
@@ -1175,14 +1169,6 @@ protected override string TypeInitializationValue(Type type, TextWriter wr, Bpl.
         }
       } else if (cl is DatatypeDecl dt) {
         var s = FullTypeName(udt);
-        var rc = cl;
-        if (DafnyOptions.O.IronDafny &&
-            !(xType is ArrowType) &&
-            rc != null &&
-            rc.EnclosingModuleDefinition != null &&
-            !rc.EnclosingModuleDefinition.IsDefaultModule) {
-          s = "@" + rc.FullCompileName;
-        }
         if (udt.TypeArgs.Count != 0) {
           s += "<" + TypeNames(udt.TypeArgs, wr, udt.tok) + ">";
         }
diff --git a/Source/Dafny/Compiler-cpp.cs b/Source/Dafny/Compiler-cpp.cs
@@ -897,12 +897,6 @@ protected string TypeName(Type type, TextWriter wr, Bpl.IToken tok, MemberDecl/*
         bool isHandle = true;
         if (cl != null && Attributes.ContainsBool(cl.Attributes, "handle", ref isHandle) && isHandle) {
           return "ulong";
-        } else if (DafnyOptions.O.IronDafny &&
-            !(xType is ArrowType) &&
-            cl != null &&
-            cl.EnclosingModuleDefinition != null &&
-            !cl.EnclosingModuleDefinition.IsDefaultModule) {
-          s = cl.FullCompileName;
         }
         if (class_name || xType.IsTypeParameter || xType.IsDatatype) {  // Don't add pointer decorations to class names or type parameters
           return IdProtect(s) + ActualTypeArgs(xType.TypeArgs);
diff --git a/Source/Dafny/Compiler-go.cs b/Source/Dafny/Compiler-go.cs
@@ -1358,12 +1358,6 @@ protected override string TypeName(Type type, TextWriter wr, Bpl.IToken tok, Mem
         bool isHandle = true;
         if (cl != null && Attributes.ContainsBool(cl.Attributes, "handle", ref isHandle) && isHandle) {
           return "ulong";
-        } else if (DafnyOptions.O.IronDafny &&
-            !(xType is ArrowType) &&
-            cl != null &&
-            cl.EnclosingModuleDefinition != null &&
-            !cl.EnclosingModuleDefinition.IsDefaultModule) {
-          s = cl.FullCompileName;
         } else if (xType is ArrowType at) {
           return string.Format("func ({0}) {1}", Util.Comma(at.Args, arg => TypeName(arg, wr, tok)), TypeName(at.Result, wr, tok));
         } else if (cl is TupleTypeDecl) {
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
@@ -901,8 +901,7 @@ TopDecl<. ModuleDefinition module, List<MemberDecl/*!*/> membersDefaultClass, bo
   | SynonymTypeDecl<dmod, module, out td>      (. module.TopLevelDecls.Add(td); .)
   | IteratorDecl<dmod, module, out iter>       (. module.TopLevelDecls.Add(iter); .)
   | TraitDecl<dmod, module, out trait>         (. module.TopLevelDecls.Add(trait); .)
-  | ClassMemberDecl<dmod, membersDefaultClass, false, true, !DafnyOptions.O.AllowGlobals,
-                    !isTopLevel && DafnyOptions.O.IronDafny && isAbstract>
+  | ClassMemberDecl<dmod, membersDefaultClass, false, true, !DafnyOptions.O.AllowGlobals>
   )
   .
 
@@ -1104,7 +1103,7 @@ ClassDecl<DeclModifierData dmodClass, ModuleDefinition/*!*/ module, out TopLevel
   "{"                                            (. bodyStart = t;  .)
     { (. dmod = new DeclModifierData(); .)
       { DeclModifier<ref dmod> }
-      ClassMemberDecl<dmod, members, true, false, false, false>
+      ClassMemberDecl<dmod, members, true, false, false>
     }
   "}"
   (. c = new ClassDecl(id, id.val, module, typeArgs, members, attrs, isRefining, parentTraits);
@@ -1141,7 +1140,7 @@ TraitDecl<DeclModifierData dmodIn, ModuleDefinition/*!*/ module, out TraitDecl/*
   "{"                                            (. bodyStart = t; .)
     { (. dmod  = new DeclModifierData(); .)
       { DeclModifier<ref dmod> }
-      ClassMemberDecl<dmod, members, true, false, false, false>
+      ClassMemberDecl<dmod, members, true, false, false>
     }
   "}"
   (. trait = new TraitDecl(id, id.val, module, typeArgs, members, attrs, isRefining, parentTraits);
@@ -1151,7 +1150,7 @@ TraitDecl<DeclModifierData dmodIn, ModuleDefinition/*!*/ module, out TraitDecl/*
   .
 
 /*------------------------------------------------------------------------*/
-ClassMemberDecl<. DeclModifierData dmod, List<MemberDecl> mm, bool allowConstructors, bool isValueType, bool moduleLevelDecl, bool isWithinAbstractModule.>
+ClassMemberDecl<. DeclModifierData dmod, List<MemberDecl> mm, bool allowConstructors, bool isValueType, bool moduleLevelDecl.>
 = (. Contract.Requires(cce.NonNullElements(mm));
      Method/*!*/ m;
      Function/*!*/ f;
@@ -1169,13 +1168,13 @@ ClassMemberDecl<. DeclModifierData dmod, List<MemberDecl> mm, bool allowConstruc
          dmod.IsStatic = false;
        }
     .)
-    FunctionDecl<dmod, isWithinAbstractModule, out f>                   (. mm.Add(f); .)
+    FunctionDecl<dmod, out f>                   (. mm.Add(f); .)
   | (. if (moduleLevelDecl && dmod.StaticToken != null) {
          errors.Warning(dmod.StaticToken, "module-level methods are always non-instance, so the 'static' keyword is not allowed here");
          dmod.IsStatic = false;
        }
     .)
-    MethodDecl<dmod, allowConstructors, isWithinAbstractModule, out m>  (. mm.Add(m); .)
+    MethodDecl<dmod, allowConstructors, out m>  (. mm.Add(m); .)
   )
   .
 
@@ -1240,7 +1239,7 @@ TypeMembers<. ModuleDefinition/*!*/ module, List<MemberDecl> members .>
   "{"
   { (. dmod = new DeclModifierData(); .)
     { DeclModifier<ref dmod> }
-    ClassMemberDecl<dmod, members, false, true, false, module.IsAbstract>
+    ClassMemberDecl<dmod, members, false, true, false>
   }
   "}"
   .
@@ -1613,7 +1612,7 @@ TPCharOption<ref TypeParameter.TypeParameterCharacteristics characteristics>
   .
 
 /*------------------------------------------------------------------------*/
-MethodDecl<DeclModifierData dmod, bool allowConstructor, bool isWithinAbstractModule, out Method/*!*/ m>
+MethodDecl<DeclModifierData dmod, bool allowConstructor, out Method/*!*/ m>
 = (. Contract.Ensures(Contract.ValueAtReturn(out m) !=null);
      IToken/*!*/ id = Token.NoToken;
      bool hasName = false;  IToken keywordToken;
@@ -1697,12 +1696,7 @@ MethodDecl<DeclModifierData dmod, bool allowConstructor, bool isWithinAbstractMo
     (. body = dividedBody; .)
   | BlockStmt<out body, out bodyStart, out bodyEnd>
   ]
-  (.
-     if (!isWithinAbstractModule && DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 && !Attributes.Contains(attrs, "axiom") && !Attributes.Contains(attrs, "imported") && !Attributes.Contains(attrs, "decl") && theVerifyThisFile) {
-        SemErr(t, "a method with an ensures clause must have a body, unless given the :axiom attribute");
-     }
-
-     IToken tok = id;
+  (. IToken tok = id;
      if (isConstructor) {
        m = new Constructor(tok, hasName ? id.val : "_ctor", typeArgs, ins,
                            req, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), (DividedBlockStmt)body, attrs, signatureEllipsis);
@@ -2043,7 +2037,7 @@ GenericInstantiation<.List<Type> gt.>
   .
 
 /*------------------------------------------------------------------------*/
-FunctionDecl<DeclModifierData dmod, bool isWithinAbstractModule, out Function/*!*/ f>
+FunctionDecl<DeclModifierData dmod, out Function/*!*/ f>
 = (. Contract.Ensures(Contract.ValueAtReturn(out f)!=null);
      Attributes attrs = null;
      IToken/*!*/ id = Token.NoToken;  // to please compiler
@@ -2175,11 +2169,7 @@ FunctionDecl<DeclModifierData dmod, bool isWithinAbstractModule, out Function/*!
   FunctionSpec<reqs, reads, ens, decreases>
   [ FunctionBody<out body, out bodyStart, out bodyEnd>
   ]
-  (. if (!isWithinAbstractModule && DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 &&
-         !Attributes.Contains(attrs, "axiom") && !Attributes.Contains(attrs, "imported")) {
-        SemErr(t, "a function with an ensures clause must have a body, unless given the :axiom attribute");
-     }
-     IToken tok = id;
+  (. IToken tok = id;
      if (isTwoState && isPredicate) {
         f = new TwoStatePredicate(tok, id.val, dmod.IsStatic, typeArgs, formals,
                                   reqs, reads, ens, new Specification<Expression>(decreases, null), body, attrs, signatureEllipsis);
diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs
@@ -22,11 +22,7 @@ public DafnyOptions(ErrorReporter errorReporter = null)
 
     public override string VersionNumber {
       get {
-        return System.Diagnostics.FileVersionInfo.GetVersionInfo(System.Reflection.Assembly.GetExecutingAssembly().Location).FileVersion
-#if ENABLE_IRONDAFNY
-          + "[IronDafny]"
-#endif
-          ;
+        return System.Diagnostics.FileVersionInfo.GetVersionInfo(System.Reflection.Assembly.GetExecutingAssembly().Location).FileVersion;
       }
     }
     public override string Version {
@@ -102,13 +98,6 @@ public enum IncludesModes { None, Immediate, Transitive }
     public bool UseRuntimeLib = false;
     public bool DisableScopes = false;
     public int Allocated = 3;
-    public bool IronDafny =
-#if ENABLE_IRONDAFNY
-      true
-#else
-      false
-#endif
-    ;
 
     protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.CommandLineParseState ps) {
       var args = ps.args;  // convenient synonym
@@ -354,16 +343,6 @@ protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.Com
             return true;
         }
 
-        case "noIronDafny": {
-            IronDafny = false;
-            return true;
-        }
-
-        case "ironDafny": {
-            IronDafny = true;
-            return true;
-        }
-
         case "optimizeResolution": {
             int d = 2;
             if (ps.GetNumericArgument(ref d, 3)) {
@@ -844,10 +823,6 @@ even bound variables in quantifiers.  This option is
     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.
-/noIronDafny  Disable Ironclad/Ironfleet features, if enabled by default.
 /printTooltips
     Dump additional positional information (displayed as mouse-over tooltips by
     the VS plugin) to stdout as 'Info' messages.
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
@@ -1766,17 +1766,12 @@ static void ResolveOpenedImportsWorker(ModuleSignature sig, ModuleDefinition mod
 
       importedSigs.Add(s);
 
-      if (useImports || DafnyOptions.O.IronDafny) {
+      if (useImports) {
         // classes:
         foreach (var kv in s.TopLevels) {
           if (!kv.Value.CanBeExported())
             continue;
 
-          if (kv.Value is ModuleDecl && ((ModuleDecl)kv.Value).Opened && DafnyOptions.O.IronDafny) {
-            ResolveOpenedImportsWorker(sig, moduleDef, (ModuleDecl)kv.Value, importedSigs, useCompileSignatures);
-          }
-
-          // IronDafny: we need to pull the members of the opened module's _default class in so that they can be merged.
           if (useImports || string.Equals(kv.Key, "_default", StringComparison.InvariantCulture)) {
             TopLevelDecl d;
             if (sig.TopLevels.TryGetValue(kv.Key, out d)) {
@@ -1823,7 +1818,7 @@ static void ResolveOpenedImportsWorker(ModuleSignature sig, ModuleDefinition mod
           }
         }
 
-        if (useImports || DafnyOptions.O.IronDafny) {
+        if (useImports) {
           // static members:
           foreach (var kv in s.StaticMembers) {
             if (!kv.Value.CanBeExported())
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
@@ -15341,11 +15341,7 @@ public Bpl.Expr TrExpr(Expression expr) {
             }
 
             var ty = translator.TrType(e.Type);
-            var name = e.Function.FullSanitizedName;
-            if (DafnyOptions.O.IronDafny) {
-              name = e.Function.FullSanitizedRefinementName;
-            }
-            var id = new Bpl.IdentifierExpr(e.tok, name, ty);
+            var id = new Bpl.IdentifierExpr(e.tok, e.Function.FullSanitizedName, ty);
 
             bool argsAreLit;
             var args = FunctionInvocationArguments(e, layerArgument, false, out argsAreLit);
@@ -17305,11 +17301,6 @@ Bpl.Trigger TrTrigger(ExpressionTranslator etran, Attributes attribs, IToken tok
 
       bool useFuelAsQuantifier = argsEtran.Statistics_CustomLayerFunctionCount > 0;
       bool useHeapAsQuantifier = argsEtran.Statistics_HeapAsQuantifierCount > 0;
-      Expr qly = null;
-      if (useFuelAsQuantifier && DafnyOptions.O.IronDafny) {
-        qly = BplBoundVar(CurrentIdGenerator.FreshId("tr$ly#"), predef.LayerType, bvars);
-        argsEtran = argsEtran.WithLayer(qly);
-      }
       if (useHeapAsQuantifier) {
         var heapExpr = BplBoundVar(CurrentIdGenerator.FreshId("tr$heap#"), predef.HeapType, bvars);
         argsEtran = new ExpressionTranslator(argsEtran, heapExpr);
@@ -17328,11 +17319,6 @@ Bpl.Trigger TrTrigger(ExpressionTranslator etran, Attributes attribs, IToken tok
         if (useHeapAsQuantifier) {
           tt.Add(FunctionCall(tok, BuiltinFunction.IsGoodHeap, null, argsEtran.HeapExpr));
         }
-        if (useFuelAsQuantifier && !fueledTrigger[trigger.Args] && DafnyOptions.O.IronDafny) {
-          // We quantified over fuel, but this particular trigger doesn't use it,
-          // so we need to add a dummy trigger.  Hopefully it will always be in scope when needed.
-          tt.Add(FunctionCall(tok, BuiltinFunction.AsFuelBottom, null, qly));
-        }
         tr = new Bpl.Trigger(tok, true, tt, tr);
       }
       return tr;
diff --git a/Test/allocated1/dafny0/FuelTriggers.dfy b/Test/allocated1/dafny0/FuelTriggers.dfy
diff --git a/Test/allocated1/dafny0/FuelTriggers.dfy.expect b/Test/allocated1/dafny0/FuelTriggers.dfy.expect
diff --git a/Test/dafny0/FuelTriggers.dfy.expect b/Test/dafny0/FuelTriggers.dfy.expect
diff --git a/Test/dafny4/Bug134.dfy b/Test/dafny4/Bug134.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /ironDafny "%s" > "%t"
+// RUN: %dafny /compile:0 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 module NativeTypes {
diff --git a/Test/dafny4/Bug70.dfy b/Test/dafny4/Bug70.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0  /ironDafny "%s" > "%t"
+// RUN: %dafny /compile:0 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 module M1
@@ -11,8 +11,9 @@ module M3 { import opened M1 }
 
 module M4
 {
-  import opened M2
-  import opened M3
+  import opened M1  // this is required to access D() unqualified below
+  import opened M2  // this causes no name conflict
+  import opened M3  // this causes no name conflict
   method Main()
   {
     var x := D();
diff --git a/Test/irondafny0/opened_workaround.dfy b/Test/irondafny0/opened_workaround.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /ironDafny /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 module A {
diff --git a/Test/wishlist/FuelTriggers.dfy b/Test/wishlist/FuelTriggers.dfy
@@ -1,16 +1,17 @@
-// RUN: %dafny /ironDafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
+// XFAIL: *
 
-// In one version of opaque + fuel, the following failed to verify
+// With the default version of opaque + fuel, the following fails to verify
 // because the quantifier in the requires used a trigger that included
 // StartFuel_P, while the assert used StartFuelAssert_P.  Since P is
 // opaque, we can't tell that those fuels are the same, and hence the
-// trigger never fires
+// trigger never fires. A wish would be to fix this.
 
 predicate {:opaque} P(x:int)
 
 method test(y:int)
-    requires forall x :: P(x);
+  requires forall x :: P(x)
 {
-    assert P(y);
+  assert P(y);
 }
diff --git a/Test/wishlist/FuelTriggers.dfy.expect b/Test/wishlist/FuelTriggers.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 2 verified, 0 errors
