Merge branch 'master' into fix-4074-only-on-single-declaration

dafny-lang · May 27, 2023 · 5839315 · 5839315
2 parents e78e3ec + 80b81c0
commit 5839315
Show file tree

Hide file tree

Showing 330 changed files with 2,567 additions and 7,614 deletions.
diff --git a/.github/workflows/doc-tests.yml b/.github/workflows/doc-tests.yml
@@ -45,6 +45,11 @@ jobs:
         chmod +x dafny/Binaries/z3/bin/z3-*
     - name: Build Dafny
       run: dotnet build dafny/Source/Dafny.sln
+    - name: Check generated error catalog
+      run: |
+        which java
+        chmod +x dafny/docs/HowToFAQ/make-error-catalog
+        ./dafny/docs/HowToFAQ/make-error-catalog
     - name: Check OnlineTutorial examples
       run: |
         cd dafny/docs

diff --git a/.github/workflows/integration-tests-reusable.yml b/.github/workflows/integration-tests-reusable.yml
@@ -136,7 +136,7 @@ jobs:
       if: runner.os != 'Windows'
       run: |
         cd dafny/docs/HowToFAQ
-        ../check-examples -c Errors-Parser.md
+        ../check-examples -c Errors-Parser.md Errors-Compiler.md Errors-CommandLine.md
     - name: Run integration tests (non-Windows)
       if: runner.os != 'Windows'
       env:

diff --git a/Source/DafnyCore.Test/DooFileTest.cs b/Source/DafnyCore.Test/DooFileTest.cs
@@ -31,13 +31,10 @@ public void UnknownManifestEntries() {
   private static Program ParseProgram(string dafnyProgramText, DafnyOptions options) {
     const string fullFilePath = "untitled:foo";
     var rootUri = new Uri(fullFilePath);
-    var outerModule = new DefaultModuleDefinition(new List<Uri> { rootUri });
-    var module = new LiteralModuleDecl(outerModule, null);
     Microsoft.Dafny.Type.ResetScopes();
-    var builtIns = new BuiltIns(options);
-    var errorReporter = new ConsoleErrorReporter(options, outerModule);
-    var parseResult = Parser.Parse(dafnyProgramText, rootUri, module, builtIns, errorReporter);
-    Assert.Equal(0, parseResult);
-    return new Program(fullFilePath, module, builtIns, errorReporter, Sets.Empty<System.Uri>(), Sets.Empty<System.Uri>());
+    var errorReporter = new ConsoleErrorReporter(options);
+    var program = ParseUtils.Parse(dafnyProgramText, rootUri, errorReporter);
+    Assert.Equal(0, errorReporter.ErrorCount);
+    return program;
   }
 }
diff --git a/Source/DafnyCore/AST/BuiltIns.cs b/Source/DafnyCore/AST/BuiltIns.cs
@@ -8,7 +8,8 @@ namespace Microsoft.Dafny;
 
 public class BuiltIns {
   public DafnyOptions Options { get; }
-  public readonly ModuleDefinition SystemModule = new ModuleDefinition(RangeToken.NoToken, new Name("_System"), new List<IToken>(), false, false, null, null, null, true);
+  public readonly ModuleDefinition SystemModule = new(RangeToken.NoToken, new Name("_System"), new List<IToken>(),
+    false, false, null, null, null, true, false);
   internal readonly Dictionary<int, ClassDecl> arrayTypeDecls = new Dictionary<int, ClassDecl>();
   public readonly Dictionary<int, ArrowTypeDecl> ArrowTypeDecls = new Dictionary<int, ArrowTypeDecl>();
   public readonly Dictionary<int, SubsetTypeDecl> PartialArrowTypeDecls = new Dictionary<int, SubsetTypeDecl>();  // same keys as arrowTypeDecl
@@ -34,18 +35,18 @@ public BuiltIns(DafnyOptions options) {
     var str = new TypeSynonymDecl(RangeToken.NoToken, new Name("string"),
       new TypeParameter.TypeParameterCharacteristics(TypeParameter.EqualitySupportValue.InferredRequired, Type.AutoInitInfo.CompilableValue, false),
       new List<TypeParameter>(), SystemModule, new SeqType(new CharType()), null);
-    SystemModule.TopLevelDecls.Add(str);
+    SystemModule.SourceDecls.Add(str);
     // create subset type 'nat'
     var bvNat = new BoundVar(Token.NoToken, "x", Type.Int);
     var natConstraint = Expression.CreateAtMost(Expression.CreateIntLiteral(Token.NoToken, 0), Expression.CreateIdentExpr(bvNat));
     var ax = AxiomAttribute();
     NatDecl = new SubsetTypeDecl(RangeToken.NoToken, new Name("nat"),
       new TypeParameter.TypeParameterCharacteristics(TypeParameter.EqualitySupportValue.InferredRequired, Type.AutoInitInfo.CompilableValue, false),
       new List<TypeParameter>(), SystemModule, bvNat, natConstraint, SubsetTypeDecl.WKind.CompiledZero, null, ax);
-    SystemModule.TopLevelDecls.Add(NatDecl);
+    SystemModule.SourceDecls.Add(NatDecl);
     // create trait 'object'
     ObjectDecl = new TraitDecl(RangeToken.NoToken, new Name("object"), SystemModule, new List<TypeParameter>(), new List<MemberDecl>(), DontCompile(), false, null);
-    SystemModule.TopLevelDecls.Add(ObjectDecl);
+    SystemModule.SourceDecls.Add(ObjectDecl);
     // add one-dimensional arrays, since they may arise during type checking
     // Arrays of other dimensions may be added during parsing as the parser detects the need for these
     UserDefinedType tmp = ArrayType(1, Type.Int, true);
@@ -66,32 +67,42 @@ public static Attributes AxiomAttribute() {
   public UserDefinedType ArrayType(int dims, Type arg, bool allowCreationOfNewClass) {
     Contract.Requires(1 <= dims);
     Contract.Requires(arg != null);
-    return ArrayType(Token.NoToken, dims, new List<Type>() { arg }, allowCreationOfNewClass);
+    var (result, mod) = ArrayType(Token.NoToken, dims, new List<Type> { arg }, allowCreationOfNewClass);
+    mod(this);
+    return result;
   }
-  public UserDefinedType ArrayType(IToken tok, int dims, List<Type> optTypeArgs, bool allowCreationOfNewClass, bool useClassNameType = false) {
+
+  public static (UserDefinedType type, Action<BuiltIns> ModifyBuiltins) ArrayType(IToken tok, int dims, List<Type> optTypeArgs, bool allowCreationOfNewClass, bool useClassNameType = false) {
     Contract.Requires(tok != null);
     Contract.Requires(1 <= dims);
     Contract.Requires(optTypeArgs == null || optTypeArgs.Count > 0);  // ideally, it is 1, but more will generate an error later, and null means it will be filled in automatically
     Contract.Ensures(Contract.Result<UserDefinedType>() != null);
 
     var arrayName = ArrayClassName(dims);
     if (useClassNameType) {
-      arrayName = arrayName + "?";
+      arrayName += "?";
     }
-    if (allowCreationOfNewClass && !arrayTypeDecls.ContainsKey(dims)) {
-      ArrayClassDecl arrayClass = new ArrayClassDecl(dims, SystemModule, DontCompile());
+
+    void ModifyBuiltins(BuiltIns builtIns) {
+      if (!allowCreationOfNewClass || builtIns.arrayTypeDecls.ContainsKey(dims)) {
+        return;
+      }
+
+      ArrayClassDecl arrayClass = new ArrayClassDecl(dims, builtIns.SystemModule, builtIns.DontCompile());
       for (int d = 0; d < dims; d++) {
         string name = dims == 1 ? "Length" : "Length" + d;
         Field len = new SpecialField(RangeToken.NoToken, name, SpecialField.ID.ArrayLength, dims == 1 ? null : (object)d, false, false, false, Type.Int, null);
-        len.EnclosingClass = arrayClass;  // resolve here
+        len.EnclosingClass = arrayClass; // resolve here
         arrayClass.Members.Add(len);
       }
-      arrayTypeDecls.Add(dims, arrayClass);
-      SystemModule.TopLevelDecls.Add(arrayClass);
-      CreateArrowTypeDecl(dims);  // also create an arrow type with this arity, since it may be used in an initializing expression for the array
+
+      builtIns.arrayTypeDecls.Add(dims, arrayClass);
+      builtIns.SystemModule.SourceDecls.Add(arrayClass);
+      builtIns.CreateArrowTypeDecl(dims); // also create an arrow type with this arity, since it may be used in an initializing expression for the array
     }
-    UserDefinedType udt = new UserDefinedType(tok, arrayName, optTypeArgs);
-    return udt;
+
+    var udt = new UserDefinedType(tok, arrayName, optTypeArgs);
+    return (udt, ModifyBuiltins);
   }
 
   public static string ArrayClassName(int dims) {
@@ -145,7 +156,7 @@ Function createMember(string name, Type resultType, Function readsFunction = nul
 
     var arrowDecl = new ArrowTypeDecl(tps, req, reads, SystemModule, DontCompile());
     ArrowTypeDecls.Add(arity, arrowDecl);
-    SystemModule.TopLevelDecls.Add(arrowDecl);
+    SystemModule.SourceDecls.Add(arrowDecl);
 
     // declaration of read-effect-free arrow-type, aka heap-independent arrow-type, aka partial-function arrow-type
     tps = Util.Map(Enumerable.Range(0, arity + 1),
@@ -158,7 +169,7 @@ Function createMember(string name, Type resultType, Function readsFunction = nul
       new TypeParameter.TypeParameterCharacteristics(false), tps, SystemModule,
       id, ArrowSubtypeConstraint(tok, tok.ToRange(), id, reads, tps, false), SubsetTypeDecl.WKind.Special, null, DontCompile());
     PartialArrowTypeDecls.Add(arity, partialArrow);
-    SystemModule.TopLevelDecls.Add(partialArrow);
+    SystemModule.SourceDecls.Add(partialArrow);
 
     // declaration of total arrow-type
 
@@ -172,7 +183,7 @@ Function createMember(string name, Type resultType, Function readsFunction = nul
       new TypeParameter.TypeParameterCharacteristics(false), tps, SystemModule,
       id, ArrowSubtypeConstraint(tok, tok.ToRange(), id, req, tps, true), SubsetTypeDecl.WKind.Special, null, DontCompile());
     TotalArrowTypeDecls.Add(arity, totalArrow);
-    SystemModule.TopLevelDecls.Add(totalArrow);
+    SystemModule.SourceDecls.Add(totalArrow);
   }
 
   /// <summary>
@@ -263,7 +274,7 @@ public TupleTypeDecl TupleType(IToken tok, int dims, bool allowCreationOfNewType
       }
 
       tupleTypeDecls.Add(argumentGhostness, tt);
-      SystemModule.TopLevelDecls.Add(tt);
+      SystemModule.SourceDecls.Add(tt);
     }
     return tt;
   }

diff --git a/Source/DafnyCore/AST/Cloner.cs b/Source/DafnyCore/AST/Cloner.cs
@@ -5,9 +5,7 @@
 using System.Collections.Generic;
 using System.Numerics;
 using System.Diagnostics.Contracts;
-using System.Linq;
 using System.Xml;
-using Microsoft.Boogie;
 
 namespace Microsoft.Dafny {
 
@@ -30,23 +28,11 @@ public Cloner(bool cloneResolvedFields = false) {
     }
 
     public virtual ModuleDefinition CloneModuleDefinition(ModuleDefinition m, Name name) {
-      ModuleDefinition nw;
       if (m is DefaultModuleDefinition defaultModuleDefinition) {
-        nw = new DefaultModuleDefinition(defaultModuleDefinition.RootSourceUris);
-      } else {
-        nw = new ModuleDefinition(Range(m.RangeToken), name, m.PrefixIds, m.IsAbstract, m.IsFacade,
-          m.RefinementQId, m.EnclosingModule, CloneAttributes(m.Attributes),
-          true);
-      }
-      foreach (var d in m.TopLevelDecls) {
-        nw.TopLevelDecls.Add(CloneDeclaration(d, nw));
-      }
-      foreach (var tup in m.PrefixNamedModules) {
-        var newTup = new Tuple<List<IToken>, LiteralModuleDecl>(tup.Item1, (LiteralModuleDecl)CloneDeclaration(tup.Item2, nw));
-        nw.PrefixNamedModules.Add(newTup);
+        return new DefaultModuleDefinition(this, defaultModuleDefinition);
       }
-      nw.Height = m.Height;
-      return nw;
+
+      return new ModuleDefinition(this, m, name);
     }
 
     public virtual TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition m) {
@@ -695,6 +681,9 @@ public override Expression CloneExpr(Expression expr) {
   /// This cloner copies the origin module signatures to their cloned declarations
   /// </summary>
   class DeepModuleSignatureCloner : Cloner {
+    public DeepModuleSignatureCloner(bool cloneResolvedFields = false) : base(cloneResolvedFields) {
+    }
+
     public override TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition m) {
       var dd = base.CloneDeclaration(d, m);
       if (d is ModuleDecl) {
@@ -719,149 +708,6 @@ public override TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition m
   }
 
 
-  class ScopeCloner : DeepModuleSignatureCloner {
-    private VisibilityScope scope = null;
-
-    private Dictionary<Declaration, Declaration> reverseMap = new Dictionary<Declaration, Declaration>();
-
-    private bool isInvisibleClone(Declaration d) {
-      Contract.Assert(reverseMap.ContainsKey(d));
-      return !reverseMap[d].IsVisibleInScope(scope);
-    }
-
-    public ScopeCloner(VisibilityScope scope) {
-      this.scope = scope;
-    }
-
-    private bool RevealedInScope(Declaration d) {
-      return d.IsRevealedInScope(scope);
-    }
-
-    private bool VisibleInScope(Declaration d) {
-      return d.IsVisibleInScope(scope);
-    }
-
-    public override ModuleDefinition CloneModuleDefinition(ModuleDefinition m, Name name) {
-      var basem = base.CloneModuleDefinition(m, name);
-
-      //Merge signatures for imports which point to the same module
-      //This makes the consistency check understand that the same element
-      //may be referred to via different qualifications.
-      var sigmap = new Dictionary<ModuleDefinition, ModuleSignature>();
-      var declmap = new Dictionary<ModuleDefinition, List<AliasModuleDecl>>();
-      var vismap = new Dictionary<ModuleDefinition, VisibilityScope>();
-
-      foreach (var top in basem.TopLevelDecls) {
-        var import = reverseMap[top] as AliasModuleDecl;
-        if (import == null) {
-          continue;
-        }
-
-        var def = import.Signature.ModuleDef;
-        if (def == null) {
-          continue;
-        }
-
-        if (!declmap.ContainsKey(def)) {
-          declmap.Add(def, new List<AliasModuleDecl>());
-          sigmap.Add(def, new ModuleSignature());
-          vismap.Add(def, new VisibilityScope());
-        }
-
-        sigmap[def] = Resolver.MergeSignature(sigmap[def], import.Signature);
-        sigmap[def].ModuleDef = def;
-        declmap[def].Add((AliasModuleDecl)top);
-        if (VisibleInScope(import)) {
-          vismap[def].Augment(import.Signature.VisibilityScope);
-        }
-
-      }
-
-      foreach (var decls in declmap) {
-        sigmap[decls.Key].VisibilityScope = vismap[decls.Key];
-        foreach (var decl in decls.Value) {
-          decl.Signature = sigmap[decls.Key];
-        }
-      }
-
-      basem.TopLevelDecls.RemoveAll(t => {
-        if (t is AliasModuleDecl aliasModuleDecl) {
-          var def = aliasModuleDecl.Signature.ModuleDef;
-          return def != null && vismap[def].IsEmpty();
-        }
-
-        return isInvisibleClone(t);
-      });
-
-      basem.TopLevelDecls.OfType<TopLevelDeclWithMembers>().
-        Iter(t => t.Members.RemoveAll(isInvisibleClone));
-
-      return basem;
-    }
-
-    public override TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition m) {
-      var based = base.CloneDeclaration(d, m);
-      if (d is (RevealableTypeDecl or TopLevelDeclWithMembers) and not DefaultClassDecl && !RevealedInScope(d)) {
-        var tps = d.TypeArgs.ConvertAll(CloneTypeParam);
-        var characteristics = TypeParameter.GetExplicitCharacteristics(d);
-        var members = based is TopLevelDeclWithMembers tm ? tm.Members : new List<MemberDecl>();
-        var otd = new AbstractTypeDecl(Range(d.RangeToken), d.NameNode.Clone(this), m, characteristics, tps, members, CloneAttributes(d.Attributes), d.IsRefining);
-        based = otd;
-        if (d is ClassLikeDecl { IsReferenceTypeDecl: true } cl) {
-          reverseMap.Add(based, cl.NonNullTypeDecl);
-          return based;
-        }
-      }
-
-      reverseMap.Add(based, d);
-      return based;
-
-    }
-
-    public override Field CloneField(Field f) {
-      var cf = f as ConstantField;
-      if (cf != null && cf.Rhs != null && !RevealedInScope(f)) {
-        // We erase the RHS value. While we do that, we must also make sure the declaration does have a type, so instead of
-        // cloning cf.Type, we assume "f" has been resolved and clone cf.Type.NormalizeExpandKeepConstraints().
-        return new ConstantField(Range(cf.RangeToken), cf.NameNode.Clone(this), null, cf.HasStaticKeyword, cf.IsGhost, cf.IsOpaque, CloneType(cf.Type.NormalizeExpandKeepConstraints()), CloneAttributes(cf.Attributes));
-      }
-      return base.CloneField(f);
-    }
-
-    public override Function CloneFunction(Function f, string newName = null) {
-      var basef = base.CloneFunction(f, newName);
-      if (basef.ByMethodBody != null) {
-        Contract.Assert(!basef.IsGhost); // a function-by-method has .IsGhost == false
-        Contract.Assert(basef.Body != null); // a function-by-method has a nonempty .Body
-        if (RevealedInScope(f)) {
-          // For an "export reveals", use an empty (but not absent) by-method part.
-          basef.ByMethodBody = new BlockStmt(basef.ByMethodBody.RangeToken, new List<Statement>());
-        } else {
-          // For an "export provides", remove the by-method part altogether.
-          basef.ByMethodTok = null;
-          basef.ByMethodBody = null;
-        }
-      }
-      if (!RevealedInScope(f)) {
-        basef.Body = null;
-      }
-      return basef;
-    }
-
-    public override Method CloneMethod(Method m) {
-      var basem = base.CloneMethod(m);
-      basem.Body = null; //exports never reveal method bodies
-      return basem;
-    }
-
-    public override MemberDecl CloneMember(MemberDecl member, bool isReference) {
-      var basem = base.CloneMember(member, isReference);
-      reverseMap.Add(basem, member);
-      return basem;
-    }
-
-  }
-
   /// <summary>
   /// This cloner is used during the creation of a module signature for a method facade.
   /// It does not clone method bodies, and it copies module signatures.
@@ -876,23 +722,6 @@ public override BlockStmt CloneBlockStmt(BlockStmt stmt) {
     }
   }
 
-  class AbstractSignatureCloner : ScopeCloner {
-
-    public AbstractSignatureCloner(VisibilityScope scope)
-      : base(scope) {
-    }
-
-    public override ModuleDefinition CloneModuleDefinition(ModuleDefinition m, Name name) {
-      var basem = base.CloneModuleDefinition(m, name);
-      basem.TopLevelDecls.RemoveAll(t => t is ModuleExportDecl);
-      return basem;
-    }
-
-    public override BlockStmt CloneMethodBody(Method m) {
-      return null;
-    }
-  }
-
   /// <summary>
   /// This cloner is used to clone a module into a _Compile module.  This is different from
   /// the standard cloner in the following ways:
@@ -906,7 +735,7 @@ public override BlockStmt CloneMethodBody(Method m) {
   class CompilationCloner : DeepModuleSignatureCloner {
     Dictionary<ModuleDefinition, ModuleDefinition> compilationModuleClones;
     public CompilationCloner(Dictionary<ModuleDefinition, ModuleDefinition> compilationModuleClones)
-      : base() {
+      : base(false) {
       this.compilationModuleClones = compilationModuleClones;
     }