From 3e555a0ec048e297c2e1e7603516793854a39fcb Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 26 May 2023 00:49:27 +0200 Subject: [PATCH] Do not let `Parser.Parse` edit the default module (#4059) - `Parser.Parse` no longer takes the default module as an argument which it then appends to, but instead returns a new type `FileModuleDefinition`, which acts as a container for file contents. - `SourceProcessor.ProcessDirectives` now makes sure not to remove or add newlines at the end of the file. - Parsing code is shared between CLI and IDE - Module cloning code has been moved out of `Cloner` and into the module classes. By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt). --- Source/DafnyCore.Test/DooFileTest.cs | 10 +- Source/DafnyCore/AST/BuiltIns.cs | 19 +- Source/DafnyCore/AST/Cloner.cs | 185 +----- Source/DafnyCore/AST/DafnyAst.cs | 15 +- Source/DafnyCore/AST/FileModuleDefinition.cs | 20 + Source/DafnyCore/AST/Grammar/ParseUtils.cs | 270 ++++++++ Source/DafnyCore/AST/Grammar/Printer.cs | 25 +- .../AST/Grammar/SourcePreprocessor.cs | 60 +- .../AST/Modules/AbstractSignatureCloner.cs | 19 + Source/DafnyCore/AST/Modules/ScopeCloner.cs | 151 +++++ .../AST/{ => Modules}/TopLevelDeclarations.cs | 201 +++--- Source/DafnyCore/AST/ShouldCompileOrVerify.cs | 2 +- Source/DafnyCore/AST/Tokens.cs | 2 +- Source/DafnyCore/Coco/Parser.frame | 9 +- Source/DafnyCore/Coco/Scanner.frame | 3 + .../Compilers/Cplusplus/Compiler-cpp.cs | 2 +- Source/DafnyCore/Dafny.atg | 144 +---- Source/DafnyCore/DafnyFile.cs | 25 +- Source/DafnyCore/DafnyMain.cs | 155 +---- Source/DafnyCore/Generic/IPointer.cs | 28 + Source/DafnyCore/Generic/Reporting.cs | 3 +- Source/DafnyCore/Generic/Util.cs | 4 +- Source/DafnyCore/Options/ProjectFile.cs | 8 +- Source/DafnyCore/Resolver/Resolver.cs | 34 +- .../Rewriters/RefinementTransformer.cs | 51 +- Source/DafnyCore/Verifier/Translator.cs | 2 +- .../DafnyDriver/Commands/CommandRegistry.cs | 6 +- Source/DafnyDriver/DafnyDriver.cs | 37 +- .../Lookup/DefinitionTest.cs | 3 +- .../Unit/DafnyLangSymbolResolverTest.cs | 2 +- .../Unit/GhostStateDiagnosticCollectorTest.cs | 2 +- .../Unit/ParserExceptionTest.cs | 8 +- .../Unit/TextDocumentLoaderTest.cs | 4 +- .../_plugins/PluginsTest.cs | 4 +- .../Language/DafnyLangParser.cs | 101 +-- .../Language/IDafnyParser.cs | 3 +- .../Symbols/SignatureAndCompletionTable.cs | 2 +- .../Workspace/DocumentManager.cs | 3 +- .../Workspace/DocumentTextBuffer.cs | 2 + .../Workspace/SymbolTable.cs | 6 +- .../Workspace/TextDocumentLoader.cs | 2 +- .../DafnyPipeline.Test/FormatterBaseTest.cs | 19 +- Source/DafnyPipeline.Test/TranslatorTest.cs | 7 +- Source/DafnyPipeline.Test/Trivia.cs | 19 +- .../DafnyRuntimeGo/DafnyRuntimeFromDafny.go | 590 +++++++++--------- Source/DafnyServer/DafnyHelper.cs | 15 +- .../SignatureAndCompletionTable.cs | 2 +- Source/DafnyTestGeneration/DafnyInfo.cs | 5 +- Source/DafnyTestGeneration/Utils.cs | 16 +- Source/IntegrationTests/LitTests.cs | 7 +- Test/allocated1/dafny0/Definedness.dfy | 2 +- Test/allocated1/dafny0/DirtyLoops.dfy | 2 +- Test/allocated1/dafny0/LetExpr.dfy | 2 +- Test/allocated1/dafny0/Parallel.dfy | 2 +- Test/allocated1/dafny0/Reads.dfy | 2 +- Test/allocated1/dafny0/SmallTests.dfy | 2 +- .../dafny0/Twostate-Verification.dfy | 2 +- .../git-issue-3451/git-issue-3451a.dfy.expect | 2 +- Test/git-issues/git-issue-3757a.dfy.expect | 2 +- .../assumptions.dfy.expect | 2 +- 60 files changed, 1189 insertions(+), 1143 deletions(-) create mode 100644 Source/DafnyCore/AST/FileModuleDefinition.cs create mode 100644 Source/DafnyCore/AST/Grammar/ParseUtils.cs create mode 100644 Source/DafnyCore/AST/Modules/AbstractSignatureCloner.cs create mode 100644 Source/DafnyCore/AST/Modules/ScopeCloner.cs rename Source/DafnyCore/AST/{ => Modules}/TopLevelDeclarations.cs (94%) create mode 100644 Source/DafnyCore/Generic/IPointer.cs diff --git a/Source/DafnyCore.Test/DooFileTest.cs b/Source/DafnyCore.Test/DooFileTest.cs index 2fb4a01cae0..3c9eee0a2e0 100644 --- a/Source/DafnyCore.Test/DooFileTest.cs +++ b/Source/DafnyCore.Test/DooFileTest.cs @@ -31,13 +31,11 @@ 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 { rootUri }); - var module = new LiteralModuleDecl(outerModule, null); + var outerModule = new DefaultModuleDefinition(new List { rootUri }, false); 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(), Sets.Empty()); + 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 index 9c889d67b17..63a2f8620d4 100644 --- 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(), false, false, null, null, null, true); + public readonly ModuleDefinition SystemModule = new(RangeToken.NoToken, new Name("_System"), new List(), + false, false, null, null, null, true, false); internal readonly Dictionary arrayTypeDecls = new Dictionary(); public readonly Dictionary ArrowTypeDecls = new Dictionary(); public readonly Dictionary PartialArrowTypeDecls = new Dictionary(); // same keys as arrowTypeDecl @@ -34,7 +35,7 @@ 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(), 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)); @@ -42,10 +43,10 @@ public BuiltIns(DafnyOptions options) { NatDecl = new SubsetTypeDecl(RangeToken.NoToken, new Name("nat"), new TypeParameter.TypeParameterCharacteristics(TypeParameter.EqualitySupportValue.InferredRequired, Type.AutoInitInfo.CompilableValue, false), new List(), 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(), new List(), 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); @@ -87,7 +88,7 @@ public UserDefinedType ArrayType(IToken tok, int dims, List optTypeArgs, b arrayClass.Members.Add(len); } arrayTypeDecls.Add(dims, arrayClass); - SystemModule.TopLevelDecls.Add(arrayClass); + SystemModule.SourceDecls.Add(arrayClass); 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); @@ -145,7 +146,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 +159,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 +173,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); } /// @@ -263,7 +264,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 index 88bd4efcfc5..f5f0dd90aef 100644 --- 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, 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 /// 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 reverseMap = new Dictionary(); - - 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(); - var declmap = new Dictionary>(); - var vismap = new Dictionary(); - - 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()); - 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(). - 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(); - 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()); - } 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; - } - - } - /// /// 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; - } - } - /// /// 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 compilationModuleClones; public CompilationCloner(Dictionary compilationModuleClones) - : base() { + : base(false) { this.compilationModuleClones = compilationModuleClones; } diff --git a/Source/DafnyCore/AST/DafnyAst.cs b/Source/DafnyCore/AST/DafnyAst.cs index 9f5a2c755a9..06c9b8adc04 100644 --- a/Source/DafnyCore/AST/DafnyAst.cs +++ b/Source/DafnyCore/AST/DafnyAst.cs @@ -73,7 +73,7 @@ public Program(string name, [Captured] LiteralModuleDecl module, [Captured] Buil Contract.Requires(reporter != null); FullName = name; DefaultModule = module; - DefaultModuleDef = (DefaultModuleDefinition)((LiteralModuleDecl)module).ModuleDef; + DefaultModuleDef = (DefaultModuleDefinition)module.ModuleDef; BuiltIns = builtIns; this.Reporter = reporter; AlreadyVerifiedRoots = alreadyVerifiedRoots; @@ -110,13 +110,14 @@ public string Name { /// Get the first token that is in the same file as the DefaultModule.RootToken.FileName /// (skips included tokens) public IToken GetFirstTopLevelToken() { - if (DefaultModule.RootToken.Next == null) { + var rootToken = DefaultModule.RangeToken.StartToken; + if (rootToken.Next == null) { return null; } - var firstToken = DefaultModule.RootToken.Next; + var firstToken = rootToken; // We skip all included files - while (firstToken is { Next: { } } && firstToken.Next.Filepath != DefaultModule.RootToken.Filepath) { + while (firstToken is { Next: { } } && firstToken.Next.Filepath != rootToken.Filepath) { firstToken = firstToken.Next; } @@ -138,15 +139,15 @@ public override IEnumerable Assumptions(Declaration decl) { public class Include : TokenNode, IComparable { public Uri IncluderFilename { get; } - public string IncludedFilename { get; } + public Uri IncludedFilename { get; } public string CanonicalPath { get; } public bool ErrorReported; - public Include(IToken tok, Uri includer, string theFilename) { + public Include(IToken tok, Uri includer, Uri theFilename) { this.tok = tok; this.IncluderFilename = includer; this.IncludedFilename = theFilename; - this.CanonicalPath = DafnyFile.Canonicalize(theFilename).LocalPath; + this.CanonicalPath = DafnyFile.Canonicalize(theFilename.LocalPath).LocalPath; this.ErrorReported = false; } diff --git a/Source/DafnyCore/AST/FileModuleDefinition.cs b/Source/DafnyCore/AST/FileModuleDefinition.cs new file mode 100644 index 00000000000..d5aa4572b1f --- /dev/null +++ b/Source/DafnyCore/AST/FileModuleDefinition.cs @@ -0,0 +1,20 @@ +using System.Collections.Generic; + +namespace Microsoft.Dafny; + +/// +/// This is a temporary container of everything declared at the top level of a file, including include directives. +/// After parsing, the contents of this 'module' are moved into the default module. +/// In the future, files may declare implicit modules and then this class will play a non-temporary role: +/// https://github.com/dafny-lang/dafny/issues/3027 +/// +public class FileModuleDefinition : ModuleDefinition { + public List Includes { get; } = new(); + + public FileModuleDefinition() : + base(RangeToken.NoToken, new Name("_module"), new List(), + false, false, null, null, null, true, false) { + { + } + } +} \ No newline at end of file diff --git a/Source/DafnyCore/AST/Grammar/ParseUtils.cs b/Source/DafnyCore/AST/Grammar/ParseUtils.cs new file mode 100644 index 00000000000..d4e24669ba7 --- /dev/null +++ b/Source/DafnyCore/AST/Grammar/ParseUtils.cs @@ -0,0 +1,270 @@ +using System; +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using System.IO; +using System.Linq; +using System.Text; +using System.Threading; + +namespace Microsoft.Dafny; + +public record DfyParseResult(int ErrorCount, FileModuleDefinition Module); + +public class ParseUtils { + + /// + /// Parses top-level things (modules, classes, datatypes, class members) from "filename" + /// and appends them in appropriate form to "module". + /// Returns the number of parsing errors encountered. + /// Note: first initialize the Scanner. + /// + public static DfyParseResult Parse(TextReader reader, Uri /*!*/ uri, BuiltIns builtIns, ErrorReporter /*!*/ errorReporter) /* throws System.IO.IOException */ { + Contract.Requires(uri != null); + var text = SourcePreprocessor.ProcessDirectives(reader, new List()); + try { + return Parse(text, uri, builtIns, errorReporter); + } catch (Exception e) { + var internalErrorDummyToken = new Token { + Uri = uri, + line = 1, + col = 1, + pos = 0, + val = string.Empty + }; + errorReporter.Error(MessageSource.Parser, internalErrorDummyToken, + "[internal error] Parser exception: " + e.Message); + throw; + } + } + + /// + /// Parses top-level things (modules, classes, datatypes, class members) + /// and appends them in appropriate form to "module". + /// Returns the number of parsing errors encountered. + /// Note: first initialize the Scanner. + /// + public static DfyParseResult Parse(string /*!*/ s, Uri /*!*/ uri, BuiltIns builtIns, ErrorReporter reporter) { + Contract.Requires(s != null); + Contract.Requires(uri != null); + Errors errors = new Errors(reporter); + return Parse(s, uri, builtIns, errors); + } + + /// + /// Parses top-level things (modules, classes, datatypes, class members) + /// and appends them in appropriate form to "module". + /// Returns the number of parsing errors encountered. + /// Note: first initialize the Scanner with the given Errors sink. + /// + public static DfyParseResult Parse(string /*!*/ s, Uri /*!*/ uri, + BuiltIns builtIns, Errors /*!*/ errors) { + Parser parser = SetupParser(s, uri, builtIns, errors); + parser.Parse(); + + if (parser.theModule.DefaultClass.Members.Count == 0 && parser.theModule.Includes.Count == 0 && !parser.theModule.SourceDecls.Any() + && (parser.theModule.PrefixNamedModules == null || parser.theModule.PrefixNamedModules.Count == 0)) { + errors.Warning(new Token(1, 1) { Uri = uri }, "File contains no code"); + } + + return new DfyParseResult(parser.errors.ErrorCount, parser.theModule); + } + + private static Parser SetupParser(string /*!*/ s, Uri /*!*/ uri, + BuiltIns builtIns, Errors /*!*/ errors) { + Contract.Requires(s != null); + Contract.Requires(uri != null); + Contract.Requires(errors != null); + System.Runtime.CompilerServices.RuntimeHelpers.RunClassConstructor(typeof(ParseErrors).TypeHandle); + System.Runtime.CompilerServices.RuntimeHelpers.RunClassConstructor(typeof(ResolutionErrors).TypeHandle); + byte[] /*!*/ buffer = cce.NonNull(Encoding.Default.GetBytes(s)); + var ms = new MemoryStream(buffer, false); + var firstToken = new Token { + Uri = uri + }; + + Scanner scanner = new Scanner(ms, errors, uri, firstToken: firstToken); + return new Parser(scanner, errors, builtIns); + } + + public static Program Parse(string source, Uri uri, ErrorReporter reporter) { + var files = new[] { new DafnyFile(reporter.Options, uri, new StringReader(source)) }; + return ParseFiles(uri.ToString(), files, reporter, CancellationToken.None); + } + + public static Program ParseFiles(string programName, IReadOnlyList files, ErrorReporter errorReporter, + CancellationToken cancellationToken) { + var options = errorReporter.Options; + var builtIns = new BuiltIns(options); + var defaultModule = errorReporter.OuterModule; + foreach (var dafnyFile in files) { + + if (options.Trace) { + options.OutputWriter.WriteLine("Parsing " + dafnyFile.FilePath); + } + + if (options.XmlSink is { IsOpen: true } && dafnyFile.Uri.IsFile) { + options.XmlSink.WriteFileFragment(dafnyFile.Uri.LocalPath); + } + + try { + var include = dafnyFile.IsPrecompiled ? new Include(new Token { + Uri = dafnyFile.Uri, + col = 1, + line = 0 + }, new Uri("cli://"), dafnyFile.Uri) : null; + if (include != null) { + // TODO this can be removed once the include error message in ErrorReporter.Error is removed. + defaultModule.Includes.Add(include); + } + + var parseResult = Parse( + dafnyFile.Content, + dafnyFile.Uri, + builtIns, + errorReporter + ); + + AddFileModuleToProgram(parseResult.Module, defaultModule); + if (defaultModule.RangeToken.StartToken.Uri == null) { + defaultModule.RangeToken = parseResult.Module.RangeToken; + } + + } catch (Exception e) { + var internalErrorDummyToken = new Token { + Uri = dafnyFile.Uri, + line = 1, + col = 1, + pos = 0, + val = string.Empty + }; + errorReporter.Error(MessageSource.Parser, internalErrorDummyToken, "[internal error] Parser exception: " + e.Message); + } + } + + if (!(options.DisallowIncludes || options.PrintIncludesMode == DafnyOptions.IncludesModes.Immediate)) { + var includedModules = TryParseIncludes(files, defaultModule.Includes.ToList(), + builtIns, errorReporter, cancellationToken); + + foreach (var module in includedModules) { + AddFileModuleToProgram(module, defaultModule); + } + } + + if (options.PrintIncludesMode == DafnyOptions.IncludesModes.Immediate) { + var dependencyMap = new DependencyMap(); + dependencyMap.AddIncludes(defaultModule.Includes); + dependencyMap.PrintMap(options); + } + + var verifiedRoots = files.Where(df => df.IsPreverified).Select(df => df.Uri).ToHashSet(); + var compiledRoots = files.Where(df => df.IsPrecompiled).Select(df => df.Uri).ToHashSet(); + var program = new Program( + programName, + new LiteralModuleDecl(errorReporter.OuterModule, null), + builtIns, + errorReporter, verifiedRoots, compiledRoots + ); + + if (errorReporter.ErrorCount == 0) { + DafnyMain.MaybePrintProgram(program, options.DafnyPrintFile, false); + } + return program; + } + + public static void AddFileModuleToProgram(FileModuleDefinition fileModule, DefaultModuleDefinition defaultModule) { + foreach (var declToMove in fileModule.TopLevelDecls. + Where(d => d != null) // Can occur when there are parse errors. Error correction is at fault but we workaround it here + ) { + declToMove.EnclosingModuleDefinition = defaultModule; + if (declToMove is LiteralModuleDecl literalModuleDecl) { + literalModuleDecl.ModuleDef.EnclosingModule = defaultModule; + } + + if (declToMove is ClassLikeDecl classDecl) { + classDecl.NonNullTypeDecl.EnclosingModuleDefinition = defaultModule; + } + if (declToMove is DefaultClassDecl defaultClassDecl) { + foreach (var member in defaultClassDecl.Members) { + defaultModule.DefaultClass.Members.Add(member); + member.EnclosingClass = defaultModule.DefaultClass; + } + } else { + defaultModule.SourceDecls.Add(declToMove); + } + } + + foreach (var include in fileModule.Includes) { + defaultModule.Includes.Add(include); + } + + foreach (var prefixNamedModule in fileModule.PrefixNamedModules) { + defaultModule.PrefixNamedModules.Add(prefixNamedModule); + } + + defaultModule.DefaultClass.SetMembersBeforeResolution(); + } + + public static IList TryParseIncludes( + IReadOnlyList files, + IEnumerable roots, + BuiltIns builtIns, + ErrorReporter errorReporter, + CancellationToken cancellationToken + ) { + var stack = new Stack(); + var result = new List(); + var resolvedFiles = new HashSet(); + foreach (var rootFile in files) { + resolvedFiles.Add(rootFile.Uri); + } + + foreach (var root in roots) { + var dafnyFile = IncludeToDafnyFile(builtIns, errorReporter, root); + if (dafnyFile != null) { + stack.Push(dafnyFile); + } + } + + while (stack.Any()) { + var top = stack.Pop(); + if (!resolvedFiles.Add(top.Uri)) { + continue; + } + + cancellationToken.ThrowIfCancellationRequested(); + try { + var parseIncludeResult = Parse( + top.Content, + top.Uri, + builtIns, + errorReporter + ); + result.Add(parseIncludeResult.Module); + + foreach (var include in parseIncludeResult.Module.Includes) { + var dafnyFile = IncludeToDafnyFile(builtIns, errorReporter, include); + if (dafnyFile != null) { + stack.Push(dafnyFile); + } + } + } catch (Exception) { + // ignored + } + } + + return result; + } + + private static DafnyFile IncludeToDafnyFile(BuiltIns builtIns, ErrorReporter errorReporter, Include include) { + try { + return new DafnyFile(builtIns.Options, include.IncludedFilename); + } catch (IllegalDafnyFile) { + errorReporter.Error(MessageSource.Parser, include.tok, $"Include of file '{include.IncludedFilename}' failed."); + return null; + } catch (IOException) { + errorReporter.Error(MessageSource.Parser, include.tok, + $"Unable to open the include {include.IncludedFilename}."); + return null; + } + } +} \ No newline at end of file diff --git a/Source/DafnyCore/AST/Grammar/Printer.cs b/Source/DafnyCore/AST/Grammar/Printer.cs index 4d004b80c3d..8cf2ec19b15 100644 --- a/Source/DafnyCore/AST/Grammar/Printer.cs +++ b/Source/DafnyCore/AST/Grammar/Printer.cs @@ -246,10 +246,10 @@ public void PrintCallGraph(ModuleDefinition module, int indent) { } return string.CompareOrdinal(m.NameRelativeToModule, n.NameRelativeToModule); }); - foreach (var clbl in SCCs) { + foreach (var callable in SCCs) { Indent(indent); - wr.WriteLine(" * SCC at height {0}:", module.CallGraph.GetSCCRepresentativePredecessorCount(clbl)); - var r = module.CallGraph.GetSCC(clbl); + wr.WriteLine(" * SCC at height {0}:", module.CallGraph.GetSCCRepresentativePredecessorCount(callable)); + var r = module.CallGraph.GetSCC(callable); foreach (var m in r) { Indent(indent); var maybeByMethod = m is Method method && method.IsByMethod ? " (by method)" : ""; @@ -260,7 +260,7 @@ public void PrintCallGraph(ModuleDefinition module, int indent) { } } - public void PrintTopLevelDecls(Program program, List decls, int indent, List/*?*/ prefixIds, string fileBeingPrinted) { + public void PrintTopLevelDecls(Program program, IEnumerable decls, int indent, List/*?*/ prefixIds, string fileBeingPrinted) { Contract.Requires(decls != null); int i = 0; foreach (TopLevelDecl d in decls) { @@ -577,9 +577,9 @@ public void PrintModuleDefinition(Program program, ModuleDefinition module, Visi } wr.Write("{0} ", module.Name); if (module.RefinementQId != null) { - wr.Write("refines {0} ", module.RefinementQId.ToString()); + wr.Write("refines {0} ", module.RefinementQId); } - if (module.TopLevelDecls.Count == 0) { + if (!module.TopLevelDecls.Any()) { wr.WriteLine("{ }"); } else { wr.WriteLine("{"); @@ -595,19 +595,12 @@ void PrintTopLevelDeclsOrExportedView(Program program, ModuleDefinition module, var decls = module.TopLevelDecls; // only filter based on view name after resolver. if (afterResolver && options.DafnyPrintExportedViews.Count != 0) { - decls = new List(); - foreach (var nameOfView in options.DafnyPrintExportedViews) { - foreach (var decl in module.TopLevelDecls) { - if (decl.FullName.Equals(nameOfView)) { - decls.Add(decl); - } - } - } + var views = options.DafnyPrintExportedViews.ToHashSet(); + decls = decls.Where(d => views.Contains(d.FullName)); } PrintTopLevelDecls(program, decls, indent + IndentAmount, null, fileBeingPrinted); foreach (var tup in module.PrefixNamedModules) { - decls = new List() { tup.Item2 }; - PrintTopLevelDecls(program, decls, indent + IndentAmount, tup.Item1, fileBeingPrinted); + PrintTopLevelDecls(program, new TopLevelDecl[] { tup.Item2 }, indent + IndentAmount, tup.Item1, fileBeingPrinted); } } diff --git a/Source/DafnyCore/AST/Grammar/SourcePreprocessor.cs b/Source/DafnyCore/AST/Grammar/SourcePreprocessor.cs index 31db67415f1..00c0eb8ee4d 100644 --- a/Source/DafnyCore/AST/Grammar/SourcePreprocessor.cs +++ b/Source/DafnyCore/AST/Grammar/SourcePreprocessor.cs @@ -62,19 +62,12 @@ public static string ProcessDirectives(TextReader reader, List /*!*/ def Contract.Ensures(Contract.Result() != null); string newline = null; StringBuilder sb = new StringBuilder(); - List /*!*/ - ifDirectiveStates = new List(); // readState.Count is the current nesting level of #if's - int ignoreCutoff = - -1; // -1 means we're not ignoring; for 0<=n, n means we're ignoring because of something at nesting level n + List /*!*/ ifDirectiveStates = new List(); // readState.Count is the current nesting level of #if's + int ignoreCutoff = -1; // -1 means we're not ignoring; for 0<=n, n means we're ignoring because of something at nesting level n while (true) //invariant -1 <= ignoreCutoff && ignoreCutoff < readState.Count; { - string line; - if (newline == null) { - line = ReadLineAndDetermineNewline(reader, out newline); - } else { - line = reader.ReadLine(); - } + (string line, newline) = ReadLineAndDetermineNewline(reader); if (line == null) { if (ifDirectiveStates.Count != 0) { sb.AppendLine("#MalformedInput: missing #endif"); @@ -83,12 +76,14 @@ public static string ProcessDirectives(TextReader reader, List /*!*/ def break; } - string t = line.Trim(); - if (t.StartsWith("#if")) { + var addedNewline = string.IsNullOrEmpty(newline) ? Environment.NewLine : newline; + string trimmedLine = line.Trim(); + + if (trimmedLine.StartsWith("#if")) { IfDirectiveState rs = new IfDirectiveState(false, false); if (ignoreCutoff != -1) { // we're already in a state of ignoring, so continue to ignore - } else if (IfdefConditionSaysToInclude(t.Substring(3).TrimStart(), defines)) { + } else if (IfdefConditionSaysToInclude(trimmedLine.Substring(3).TrimStart(), defines)) { // include this branch } else { ignoreCutoff = ifDirectiveStates.Count; // start ignoring @@ -96,11 +91,10 @@ public static string ProcessDirectives(TextReader reader, List /*!*/ def } ifDirectiveStates.Add(rs); - sb.Append(newline); // ignore the #if line - } else if (t.StartsWith("#elsif")) { + } else if (trimmedLine.StartsWith("#elsif")) { IfDirectiveState rs; - if (ifDirectiveStates.Count == 0 || (rs = ifDirectiveStates[ifDirectiveStates.Count - 1]).hasSeenElse) { - sb.Append("#MalformedInput: misplaced #elsif" + newline); // malformed input + if (ifDirectiveStates.Count == 0 || (rs = ifDirectiveStates[^1]).hasSeenElse) { + sb.Append("#MalformedInput: misplaced #elsif" + addedNewline); // malformed input break; } @@ -109,18 +103,17 @@ public static string ProcessDirectives(TextReader reader, List /*!*/ def //Contract.Assert(!rs.mayStillIncludeAnotherAlternative); ignoreCutoff = ifDirectiveStates.Count - 1; // start ignoring } else if (rs.mayStillIncludeAnotherAlternative && - IfdefConditionSaysToInclude(t.Substring(6).TrimStart(), defines)) { + IfdefConditionSaysToInclude(trimmedLine.Substring(6).TrimStart(), defines)) { // include this branch, but no subsequent branch at this level ignoreCutoff = -1; rs.mayStillIncludeAnotherAlternative = false; - ifDirectiveStates[ifDirectiveStates.Count - 1] = rs; + ifDirectiveStates[^1] = rs; } - sb.Append(newline); // ignore the #elsif line - } else if (t == "#else") { + } else if (trimmedLine == "#else") { IfDirectiveState rs; if (ifDirectiveStates.Count == 0 || (rs = ifDirectiveStates[ifDirectiveStates.Count - 1]).hasSeenElse) { - sb.Append("#MalformedInput: misplaced #else" + newline); // malformed input + sb.Append("#MalformedInput: misplaced #else" + addedNewline); // malformed input break; } @@ -135,11 +128,10 @@ public static string ProcessDirectives(TextReader reader, List /*!*/ def rs.mayStillIncludeAnotherAlternative = false; } - ifDirectiveStates[ifDirectiveStates.Count - 1] = rs; - sb.Append(newline); // ignore the #else line - } else if (t == "#endif") { + ifDirectiveStates[^1] = rs; + } else if (trimmedLine == "#endif") { if (ifDirectiveStates.Count == 0) { - sb.Append("#MalformedInput: misplaced #endif" + newline); // malformed input + sb.Append("#MalformedInput: misplaced #endif" + addedNewline); // malformed input break; } @@ -149,22 +141,19 @@ public static string ProcessDirectives(TextReader reader, List /*!*/ def ignoreCutoff = -1; } - sb.Append(newline); // ignore the #endif line } else if (ignoreCutoff == -1) { sb.Append(line); - sb.Append(newline); - } else { - sb.Append(newline); // ignore the line } + sb.Append(newline); } return sb.ToString(); } - public static string ReadLineAndDetermineNewline(TextReader reader, out string newline) { + + public static (string content, string newline) ReadLineAndDetermineNewline(TextReader reader) { StringBuilder sb = new StringBuilder(); - newline = null; while (true) { int ch = reader.Read(); if (ch == -1) { @@ -172,6 +161,7 @@ public static string ReadLineAndDetermineNewline(TextReader reader, out string n } if (ch == '\r' || ch == '\n') { + string newline; if (ch == '\r') { if (reader.Peek() == '\n') { newline = "\r\n"; @@ -183,15 +173,15 @@ public static string ReadLineAndDetermineNewline(TextReader reader, out string n newline = "\n"; } - return sb.ToString(); + return (sb.ToString(), newline); } sb.Append((char)ch); } if (sb.Length > 0) { - return sb.ToString(); + return (sb.ToString(), ""); } - return null; + return (null, ""); } /// diff --git a/Source/DafnyCore/AST/Modules/AbstractSignatureCloner.cs b/Source/DafnyCore/AST/Modules/AbstractSignatureCloner.cs new file mode 100644 index 00000000000..e59b028b471 --- /dev/null +++ b/Source/DafnyCore/AST/Modules/AbstractSignatureCloner.cs @@ -0,0 +1,19 @@ +namespace Microsoft.Dafny; + +class AbstractSignatureCloner : ScopeCloner { + + public AbstractSignatureCloner(VisibilityScope scope) + : base(scope) { + } + + public override ModuleDefinition CloneModuleDefinition(ModuleDefinition m, Name name) { + var basem = base.CloneModuleDefinition(m, name); + basem.SourceDecls.RemoveAll(t => t is ModuleExportDecl); + basem.ResolvedPrefixNamedModules.RemoveAll(t => t is ModuleExportDecl); + return basem; + } + + public override BlockStmt CloneMethodBody(Method m) { + return null; + } +} \ No newline at end of file diff --git a/Source/DafnyCore/AST/Modules/ScopeCloner.cs b/Source/DafnyCore/AST/Modules/ScopeCloner.cs new file mode 100644 index 00000000000..c83221777bc --- /dev/null +++ b/Source/DafnyCore/AST/Modules/ScopeCloner.cs @@ -0,0 +1,151 @@ +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using System.Linq; +using Microsoft.Boogie; + +namespace Microsoft.Dafny; + +class ScopeCloner : DeepModuleSignatureCloner { + private VisibilityScope scope = null; + + private Dictionary reverseMap = new(); + + 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(); + var declmap = new Dictionary>(); + var vismap = new Dictionary(); + + 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()); + 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]; + } + } + + bool RemovePredicate(TopLevelDecl topLevelDecl) { + if (topLevelDecl is AliasModuleDecl aliasModuleDecl) { + var def = aliasModuleDecl.Signature.ModuleDef; + return def != null && vismap[def].IsEmpty(); + } + + return IsInvisibleClone(topLevelDecl); + } + + basem.SourceDecls.RemoveAll(RemovePredicate); + basem.ResolvedPrefixNamedModules.RemoveAll(RemovePredicate); + + basem.TopLevelDecls.OfType(). + 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(); + 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) { + if (f is ConstantField { Rhs: not null } cf && !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()); + } 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; + } + +} \ No newline at end of file diff --git a/Source/DafnyCore/AST/TopLevelDeclarations.cs b/Source/DafnyCore/AST/Modules/TopLevelDeclarations.cs similarity index 94% rename from Source/DafnyCore/AST/TopLevelDeclarations.cs rename to Source/DafnyCore/AST/Modules/TopLevelDeclarations.cs index 07471c7cf5f..6815cc4e7f4 100644 --- a/Source/DafnyCore/AST/TopLevelDeclarations.cs +++ b/Source/DafnyCore/AST/Modules/TopLevelDeclarations.cs @@ -4,6 +4,9 @@ using System.Diagnostics.Contracts; using System.Numerics; using System.Linq; +using System.Reflection; +using System.Xml; +using Microsoft.CodeAnalysis.CSharp.Syntax; using Microsoft.Dafny.Auditor; namespace Microsoft.Dafny; @@ -387,7 +390,6 @@ public virtual ModuleSignature AccessibleSignature() { return Signature; } public int Height; - public Token RootToken = new Token(); public readonly bool Opened; @@ -847,19 +849,40 @@ public string FullName { Attributes IAttributeBearingDeclaration.Attributes => Attributes; public ModuleQualifiedId RefinementQId; // full qualified ID of the refinement parent, null if no refinement base public bool SuccessfullyResolved; // set to true upon successful resolution; modules that import an unsuccessfully resolved module are not themselves resolved - - // TODO move to Program once this list is no longer mutated by parsing. - public List Includes; - - [FilledInDuringResolution] public readonly List TopLevelDecls = new List(); // filled in by the parser; readonly after that, except for the addition of prefix-named modules, which happens in the resolver - [FilledInDuringResolution] public readonly List, LiteralModuleDecl>> PrefixNamedModules = new List, LiteralModuleDecl>>(); // filled in by the parser; emptied by the resolver - [FilledInDuringResolution] public readonly Graph CallGraph = new Graph(); - [FilledInDuringResolution] public int Height; // height in the topological sorting of modules; public readonly bool IsAbstract; public readonly bool IsFacade; // True iff this module represents a module facade (that is, an abstract interface) private readonly bool IsBuiltinName; // true if this is something like _System that shouldn't have it's name mangled. - - public int? ResolvedHash { get; set; } + private readonly bool defaultClassFirst; + + public DefaultClassDecl DefaultClass { get; set; } + + public readonly List SourceDecls = new(); + [FilledInDuringResolution] + public readonly List ResolvedPrefixNamedModules = new(); + [FilledInDuringResolution] + public readonly List, LiteralModuleDecl>> PrefixNamedModules = new(); // filled in by the parser; emptied by the resolver + public virtual IEnumerable TopLevelDecls => + defaultClassFirst ? DefaultClasses. + Concat(SourceDecls). + Concat(ResolvedPrefixNamedModules) + : SourceDecls. + Concat(DefaultClasses). + Concat(ResolvedPrefixNamedModules); + + public IEnumerable> TopLevelDeclPointers => + (DefaultClass == null + ? Enumerable.Empty>() + : new[] { new Pointer(() => DefaultClass, v => DefaultClass = (DefaultClassDecl)v) }). + Concat(SourceDecls.ToPointers()).Concat(ResolvedPrefixNamedModules.ToPointers()); + + protected IEnumerable DefaultClasses { + get { return DefaultClass == null ? Enumerable.Empty() : new TopLevelDecl[] { DefaultClass }; } + } + + [FilledInDuringResolution] + public readonly Graph CallGraph = new(); + [FilledInDuringResolution] + public int Height; // height in the topological sorting of modules; [ContractInvariantMethod] void ObjectInvariant() { @@ -867,8 +890,41 @@ void ObjectInvariant() { Contract.Invariant(CallGraph != null); } + public ModuleDefinition(Cloner cloner, ModuleDefinition original, Name name) : base(cloner, original) { + NameNode = name; + IsBuiltinName = true; + PrefixIds = original.PrefixIds.Select(cloner.Tok).ToList(); + IsFacade = original.IsFacade; + Attributes = original.Attributes; + IsAbstract = original.IsAbstract; + RefinementQId = original.RefinementQId; + EnclosingModule = original.EnclosingModule; + defaultClassFirst = original.defaultClassFirst; + foreach (var d in original.SourceDecls) { + SourceDecls.Add(cloner.CloneDeclaration(d, this)); + } + + DefaultClass = (DefaultClassDecl)cloner.CloneDeclaration(original.DefaultClass, this); + foreach (var tup in original.PrefixNamedModules) { + var newTup = new Tuple, LiteralModuleDecl>(tup.Item1, (LiteralModuleDecl)cloner.CloneDeclaration(tup.Item2, this)); + PrefixNamedModules.Add(newTup); + } + + // For cloning modules into their compiled variants, we don't want to copy resolved fields, but we do need to copy this. + // We're hoping to remove the copying of modules into compiled variants altogether, + // and then this can be moved to inside the `if (cloner.CloneResolvedFields)` block + foreach (var tup in original.ResolvedPrefixNamedModules) { + ResolvedPrefixNamedModules.Add(cloner.CloneDeclaration(tup, this)); + } + + if (cloner.CloneResolvedFields) { + Height = original.Height; + } + } + public ModuleDefinition(RangeToken tok, Name name, List prefixIds, bool isAbstract, bool isFacade, - ModuleQualifiedId refinementQId, ModuleDefinition parent, Attributes attributes, bool isBuiltinName) : base(tok) { + ModuleQualifiedId refinementQId, ModuleDefinition parent, Attributes attributes, + bool isBuiltinName, bool defaultClassFirst = false) : base(tok) { Contract.Requires(tok != null); Contract.Requires(name != null); this.NameNode = name; @@ -878,19 +934,19 @@ public ModuleDefinition(RangeToken tok, Name name, List prefixIds, bool this.RefinementQId = refinementQId; this.IsAbstract = isAbstract; this.IsFacade = isFacade; - this.Includes = new List(); this.IsBuiltinName = isBuiltinName; + this.defaultClassFirst = defaultClassFirst; + + if (Name != "_System") { + DefaultClass = new DefaultClassDecl(this, new List()); + } } - VisibilityScope visibilityScope; + private VisibilityScope visibilityScope; public VisibilityScope VisibilityScope => visibilityScope ??= new VisibilityScope(this.SanitizedName); - public virtual bool IsDefaultModule { - get { - return false; - } - } + public virtual bool IsDefaultModule => false; private string sanitizedName = null; @@ -980,13 +1036,11 @@ public static IEnumerable AllFunctions(List declarations } } - public static IEnumerable AllFields(List declarations) { + public static IEnumerable AllFields(IEnumerable declarations) { foreach (var d in declarations) { - var cl = d as TopLevelDeclWithMembers; - if (cl != null) { + if (d is TopLevelDeclWithMembers cl) { foreach (var member in cl.Members) { - var fn = member as Field; - if (fn != null) { + if (member is Field fn) { yield return fn; } } @@ -994,18 +1048,6 @@ public static IEnumerable AllFields(List declarations) { } } - /// - /// Return every ClassDecl (including ArrayClassDecl and IteratorDecl), TraitDecl, and DefaultClassDecl - /// among the given "declarations". - /// - public static IEnumerable AllClasses(List declarations) { - foreach (var d in declarations) { - if (d is ClassLikeDecl or DefaultClassDecl) { - yield return (TopLevelDeclWithMembers)d; - } - } - } - public static IEnumerable AllTypesWithMembers(List declarations) { foreach (var d in declarations) { if (d is TopLevelDeclWithMembers cl) { @@ -1022,7 +1064,7 @@ public static IEnumerable AllTypesWithMembers(List - public static IEnumerable AllCallables(List declarations) { + public static IEnumerable AllCallables(IEnumerable declarations) { foreach (var d in declarations) { if (d is TopLevelDeclWithMembers cl) { foreach (var member in cl.Members.Where(member => member is ICallable and not ConstantField)) { @@ -1039,7 +1081,7 @@ public static IEnumerable AllCallables(List declaration /// Yields all functions and methods that are members of some type in the given list of /// declarations, including prefix lemmas and prefix predicates. /// - public static IEnumerable AllCallablesIncludingPrefixDeclarations(List declarations) { + public static IEnumerable AllCallablesIncludingPrefixDeclarations(IEnumerable declarations) { foreach (var decl in AllCallables(declarations)) { yield return decl; if (decl is ExtremeLemma extremeLemma) { @@ -1054,7 +1096,7 @@ public static IEnumerable AllCallablesIncludingPrefixDeclarations(Lis /// Yields all functions and methods that are members of some non-iterator type in the given /// list of declarations, as well as any IteratorDecl's in that list. /// - public static IEnumerable AllItersAndCallables(List declarations) { + public static IEnumerable AllItersAndCallables(IEnumerable declarations) { foreach (var d in declarations) { if (d is IteratorDecl) { yield return (IteratorDecl)d; @@ -1069,19 +1111,11 @@ public static IEnumerable AllItersAndCallables(List dec } } - public static IEnumerable AllIteratorDecls(List declarations) { - foreach (var d in declarations) { - if (d is IteratorDecl iter) { - yield return iter; - } - } - } - /// /// Emits the declarations in "declarations", but for each such declaration that is a class with /// a corresponding non-null type, also emits that non-null type *after* the class declaration. /// - public static IEnumerable AllDeclarationsAndNonNullTypeDecls(List declarations) { + public static IEnumerable AllDeclarationsAndNonNullTypeDecls(IEnumerable declarations) { foreach (var d in declarations) { yield return d; if (d is ClassLikeDecl { NonNullTypeDecl: { } } cl) { @@ -1106,32 +1140,6 @@ public bool IsEssentiallyEmptyModuleBody() { return TopLevelDecls.All(decl => decl.IsEssentiallyEmpty()); } - public IToken GetFirstTopLevelToken() { - if (StartToken.line > 0) { - return StartToken; - } - if (this is DefaultModuleDefinition { Includes: { Count: > 0 } includes } && - includes[0].OwnedTokens.Any()) { - return includes[0].OwnedTokens.First(); - } - IEnumerable topTokens = TopLevelDecls.SelectMany(decl => { - if (decl.StartToken.line > 0) { - return new List() { decl.StartToken }; - } else if (decl is TopLevelDeclWithMembers declWithMembers) { - return declWithMembers.Members.Where( - member => member.tok.line > 0) - .Select(member => member.StartToken); - } else if (decl is LiteralModuleDecl literalModuleDecl) { - return literalModuleDecl.ModuleDef.PrefixNamedModules.Select(module => - module.Item2.ModuleDef.GetFirstTopLevelToken()).Where((IToken t) => t is { line: > 0 }); - } else { - return new List() { }; - } - }); - - return topTokens.MinBy(token => token.pos); - } - public IToken NameToken => tok; public override IEnumerable Children => (Attributes != null ? new List { Attributes } : @@ -1140,18 +1148,20 @@ public IToken GetFirstTopLevelToken() { private IEnumerable preResolveTopLevelDecls; private IEnumerable preResolvePrefixNamedModules; - public override IEnumerable PreResolveChildren => - Includes.Concat(Attributes != null ? - new List { Attributes } : - Enumerable.Empty()).Concat(preResolveTopLevelDecls ?? TopLevelDecls).Concat( - (preResolvePrefixNamedModules ?? PrefixNamedModules.Select(tuple => tuple.Item2))); + + public override IEnumerable PreResolveChildren { + get { + var attributes = Attributes != null ? new List { Attributes } : Enumerable.Empty(); + return attributes.Concat(preResolveTopLevelDecls ?? TopLevelDecls).Concat( + (preResolvePrefixNamedModules ?? PrefixNamedModules.Select(tuple => tuple.Item2))); + } + } public void PreResolveSnapshotForFormatter() { preResolveTopLevelDecls = TopLevelDecls.ToImmutableList(); preResolvePrefixNamedModules = PrefixNamedModules.Select(tuple => tuple.Item2).ToImmutableList(); } - public override IEnumerable Assumptions(Declaration decl) { return TopLevelDecls.SelectMany(m => m.Assumptions(decl)); } @@ -1159,18 +1169,26 @@ public override IEnumerable Assumptions(Declaration decl) { public class DefaultModuleDefinition : ModuleDefinition { + public List Includes { get; } = new(); public IList RootSourceUris { get; } - public DefaultModuleDefinition(IList rootSourceUris) - : base(RangeToken.NoToken, new Name("_module"), new List(), false, false, null, null, null, true) { + + public DefaultModuleDefinition(IList rootSourceUris, bool defaultClassFirst) + : base(RangeToken.NoToken, new Name("_module"), new List(), false, false, + null, null, null, true, defaultClassFirst) { RootSourceUris = rootSourceUris; } + public DefaultModuleDefinition(Cloner cloner, DefaultModuleDefinition original) : base(cloner, original, original.NameNode) { + RootSourceUris = original.RootSourceUris; + } + public override bool IsDefaultModule => true; + public override IEnumerable PreResolveChildren => Includes.Concat(base.PreResolveChildren); } public abstract class TopLevelDecl : Declaration, TypeParameter.ParentType { public abstract string WhatKind { get; } - public readonly ModuleDefinition EnclosingModuleDefinition; + public ModuleDefinition EnclosingModuleDefinition; public readonly List TypeArgs; [ContractInvariantMethod] void ObjectInvariant() { @@ -1277,10 +1295,11 @@ public virtual bool IsEssentiallyEmpty() { public abstract class TopLevelDeclWithMembers : TopLevelDecl { public readonly List Members; - public readonly ImmutableList MembersBeforeResolution; + // TODO remove this and instead clone the AST after parsing. + public ImmutableList MembersBeforeResolution; // The following fields keep track of parent traits - public readonly List InheritedMembers = new List(); // these are instance members declared in parent traits + public readonly List InheritedMembers = new(); // these are instance members declared in parent traits public readonly List ParentTraits; // these are the types that are parsed after the keyword 'extends'; note, for a successfully resolved program, these are UserDefinedType's where .ResolvedClass is NonNullTypeDecl public readonly Dictionary ParentFormalTypeParametersToActuals = new Dictionary(); // maps parent traits' type parameters to actuals @@ -1346,15 +1365,21 @@ public void Extend(TraitDecl parent, InheritanceInformationClass parentInfo, Dic } } - protected TopLevelDeclWithMembers(RangeToken rangeToken, Name name, ModuleDefinition module, List typeArgs, List members, Attributes attributes, bool isRefining, List/*?*/ traits = null) + protected TopLevelDeclWithMembers(RangeToken rangeToken, Name name, ModuleDefinition module, + List typeArgs, List members, Attributes attributes, + bool isRefining, List/*?*/ traits = null) : base(rangeToken, name, module, typeArgs, attributes, isRefining) { Contract.Requires(rangeToken != null); Contract.Requires(name != null); Contract.Requires(cce.NonNullElements(typeArgs)); Contract.Requires(cce.NonNullElements(members)); Members = members; - MembersBeforeResolution = members.ToImmutableList(); ParentTraits = traits ?? new List(); + SetMembersBeforeResolution(); + } + + public void SetMembersBeforeResolution() { + MembersBeforeResolution = Members.ToImmutableList(); } public static List CommonTraits(TopLevelDeclWithMembers a, TopLevelDeclWithMembers b) { @@ -2082,7 +2107,7 @@ public NoContext(ModuleDefinition module) { public bool AllowsAllocation => true; } -public class AbstractTypeDecl : TopLevelDeclWithMembers, TypeParameter.ParentType, RevealableTypeDecl, ICanFormat, IHasDocstring { +public class AbstractTypeDecl : TopLevelDeclWithMembers, RevealableTypeDecl, ICanFormat, IHasDocstring { public override string WhatKind { get { return "abstract type"; } } public override bool CanBeRevealed() { return true; } public readonly TypeParameter.TypeParameterCharacteristics Characteristics; diff --git a/Source/DafnyCore/AST/ShouldCompileOrVerify.cs b/Source/DafnyCore/AST/ShouldCompileOrVerify.cs index eae9cbf80a4..b77edbad58a 100644 --- a/Source/DafnyCore/AST/ShouldCompileOrVerify.cs +++ b/Source/DafnyCore/AST/ShouldCompileOrVerify.cs @@ -79,7 +79,7 @@ private static ISet GetReachableUris(Program program, ISet stopUris) { var visited = new HashSet(); var edges = program.Includes.GroupBy(i => i.IncluderFilename) - .ToDictionary(g => g.Key, g => g.Select(i => new Uri(i.IncludedFilename)).ToList()); + .ToDictionary(g => g.Key, g => g.Select(x => x.IncludedFilename).ToList()); while (toVisit.Any()) { var uri = toVisit.Pop(); if (stopUris.Contains(uri)) { diff --git a/Source/DafnyCore/AST/Tokens.cs b/Source/DafnyCore/AST/Tokens.cs index 0c8cf0f57be..54f9e522a14 100644 --- a/Source/DafnyCore/AST/Tokens.cs +++ b/Source/DafnyCore/AST/Tokens.cs @@ -56,7 +56,7 @@ string Boogie.IToken.filename { public class Token : IToken { public Token peekedTokens; // Used only internally by Coco when the scanner "peeks" tokens. Normallly null at the end of parsing - public static readonly IToken NoToken = new Token(); + public static readonly Token NoToken = new Token(); static Token() { NoToken.Next = NoToken; diff --git a/Source/DafnyCore/Coco/Parser.frame b/Source/DafnyCore/Coco/Parser.frame index e52f57599d6..b21adbad0f1 100644 --- a/Source/DafnyCore/Coco/Parser.frame +++ b/Source/DafnyCore/Coco/Parser.frame @@ -55,10 +55,8 @@ public class Parser { public Parser(Scanner scanner, Errors errors) { this.scanner = scanner; this.errors = errors; - Token tok = new Token(); - tok.val = ""; - this.la = tok; - this.t = new Token(); // just to satisfy its non-null constraint + this.la = scanner.FirstToken; + this.t = scanner.FirstToken; // just to satisfy its non-null constraint } void SynErr (int n) { @@ -145,8 +143,7 @@ public class Parser { -->productions public void Parse() { - la = new Token(); - la.val = ""; + la = scanner.FirstToken; Get(); -->parseRoot } diff --git a/Source/DafnyCore/Coco/Scanner.frame b/Source/DafnyCore/Coco/Scanner.frame index 77b7cdaa30c..a98d10d01a7 100644 --- a/Source/DafnyCore/Coco/Scanner.frame +++ b/Source/DafnyCore/Coco/Scanner.frame @@ -306,6 +306,7 @@ public class Scanner { bool triviaTrailing = false; // The first trivia is always leading int triviaNewlines = 0; // How many newlines in the trivia so far bool lastWasCr = false; // if the last newline character was \r + public Token FirstToken { get; } private Errors/*!*/ errorHandler; @@ -324,6 +325,7 @@ public class Scanner { if(firstToken.Uri == null) { firstToken.Uri = uri; } + this.FirstToken = firstToken; pt = tokens = firstToken ?? new Token(); // first token is a dummy t = firstToken ?? new Token(); // dummy because t is a non-null field try { @@ -344,6 +346,7 @@ public class Scanner { if(firstToken.Uri == null) { firstToken.Uri = uri; } + this.FirstToken = firstToken; pt = tokens = firstToken ?? new Token(); // first token is a dummy t = firstToken ?? new Token(); // dummy because t is a non-null field this._buffer = new Buffer(s, true); diff --git a/Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs b/Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs index 90adcca7943..afd410280a2 100644 --- a/Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs +++ b/Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs @@ -159,7 +159,7 @@ protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string a } protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, bool isExtern, string/*?*/ libraryName, ConcreteSyntaxTree wr) { - var s = string.Format("namespace {0} ", IdProtect(moduleName)); + var s = $"namespace {IdProtect(moduleName)} "; string footer = "// end of " + s + " declarations"; this.modDeclWr = this.modDeclsWr.NewBlock(s, footer); string footer1 = "// end of " + s + " datatype declarations"; diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg index 012cf3b5181..0ed24d28a72 100644 --- a/Source/DafnyCore/Dafny.atg +++ b/Source/DafnyCore/Dafny.atg @@ -26,7 +26,7 @@ readonly AssignmentRhs/*!*/ dummyRhs; readonly FrameExpression/*!*/ dummyFrameExpr; readonly Statement/*!*/ dummyStmt; readonly Statement/*!*/ dummyIfStmt; -readonly ModuleDecl theModule; +public readonly FileModuleDefinition theModule; readonly BuiltIns theBuiltIns; DafnyOptions theOptions; int anonymousIds = 0; @@ -140,66 +140,6 @@ bool IsAssumeTypeKeyword(IToken la) { return la.kind == _assume || la.kind == _assert || la.kind == _expect; } -/// -/// Parses top-level things (modules, classes, datatypes, class members) from "filename" -/// and appends them in appropriate form to "module". -/// Returns the number of parsing errors encountered. -/// Note: first initialize the Scanner. -/// -public static int Parse(TextReader reader, Uri/*!*/ uri, ModuleDecl module, BuiltIns builtIns, Errors/*!*/ errors) /* throws System.IO.IOException */ { - Contract.Requires(uri != null); - Contract.Requires(module != null); - var text = Microsoft.Dafny.SourcePreprocessor.ProcessDirectives(reader, new List()); - return Parse(text, uri, module, builtIns, errors); -} - -/// -/// Parses top-level things (modules, classes, datatypes, class members) -/// and appends them in appropriate form to "module". -/// Returns the number of parsing errors encountered. -/// Note: first initialize the Scanner. -/// -public static int Parse(string/*!*/ s, Uri/*!*/ uri, ModuleDecl module, BuiltIns builtIns, ErrorReporter reporter) { - Contract.Requires(s != null); - Contract.Requires(uri != null); - Contract.Requires(module != null); - Errors errors = new Errors(reporter); - return Parse(s, uri, module, builtIns, errors); -} - -public static Parser SetupParser(string/*!*/ s, Uri/*!*/ uri, ModuleDecl module, - BuiltIns builtIns, Errors/*!*/ errors) { - Contract.Requires(s != null); - Contract.Requires(uri != null); - Contract.Requires(module != null); - Contract.Requires(errors != null); - System.Runtime.CompilerServices.RuntimeHelpers.RunClassConstructor(typeof(ParseErrors).TypeHandle); - System.Runtime.CompilerServices.RuntimeHelpers.RunClassConstructor(typeof(ResolutionErrors).TypeHandle); - byte[]/*!*/ buffer = cce.NonNull( UTF8Encoding.Default.GetBytes(s)); - MemoryStream ms = new MemoryStream(buffer,false); - Token firstToken; - if((module.RootToken.Filepath ?? "") == "") { // This is the first module - module.RootToken.Uri = uri; - firstToken = module.RootToken; - } else { - firstToken = new Token(); // It's an included file - } - Scanner scanner = new Scanner(ms, errors, uri, firstToken: firstToken); - return new Parser(scanner, errors, module, builtIns); -} - -// Unused code -public static Expression ParseExpression(string/*!*/ s, Uri/*!*/ uri, ModuleDecl module, - BuiltIns builtIns, Errors/*!*/ errors) { - Parser parser = SetupParser(s, uri, module, builtIns, errors); - parser.la = new Token(); - parser.la.val = ""; - parser.Get(); - Expression e; - parser.Expression(out e, true, true, true); - return e; -} - public void ApplyOptionsFromAttributes(Attributes attrs) { var overrides = attrs.AsEnumerable().Where(a => a.Name == "options") .Reverse().Select(a => @@ -238,20 +178,7 @@ public void ApplyOptionsFromAttributes(Attributes attrs) { } } -/// -/// Parses top-level things (modules, classes, datatypes, class members) -/// and appends them in appropriate form to "module". -/// Returns the number of parsing errors encountered. -/// Note: first initialize the Scanner with the given Errors sink. -/// -public static int Parse(string/*!*/ s, Uri/*!*/ uri, ModuleDecl module, - BuiltIns builtIns, Errors/*!*/ errors) { - Parser parser = SetupParser(s, uri, module, builtIns, errors); - parser.Parse(); - return parser.errors.ErrorCount; -} - -public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, ModuleDecl module, BuiltIns builtIns) +public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, BuiltIns builtIns) : this(scanner, errors) // the real work { // initialize readonly fields @@ -261,7 +188,8 @@ public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, ModuleDecl module, Built dummyStmt = new ReturnStmt(Token.NoToken.ToRange(), null); var dummyBlockStmt = new BlockStmt(Token.NoToken.ToRange(), new List()); dummyIfStmt = new IfStmt(Token.NoToken.ToRange(), false, null, dummyBlockStmt, null); - theModule = module; + + theModule = new FileModuleDefinition(); theBuiltIns = builtIns; theOptions = new DafnyOptions(builtIns.Options); } @@ -1002,14 +930,10 @@ IGNORE cr + lf + tab /*------------------------------------------------------------------------*/ PRODUCTIONS Dafny -= (. List membersDefaultClass = new List(); - // to support multiple files, create a default module only if theModule is null - DefaultModuleDefinition defaultModule = (DefaultModuleDefinition)((LiteralModuleDecl)theModule).ModuleDef; - // theModule should be a DefaultModuleDefinition (actually, the singular DefaultModuleDefinition) - Contract.Assert(defaultModule != null); - IToken startToken = t; - .) - { "include" (. startToken = t; .) += (. IToken includeStartToken; + IToken fileStartToken = t; + .) + { "include" (. includeStartToken = t; .) stringToken (. { Uri parsedFile = scanner.Uri; bool isVerbatimString; @@ -1020,32 +944,16 @@ Dafny string basePath = Path.GetDirectoryName(parsedFile.LocalPath); includedFile = Path.Combine(basePath, includedFile); } - var oneInclude = new Include(t, parsedFile, includedFile); - oneInclude.RangeToken = new RangeToken(startToken, t); - defaultModule.Includes.Add(oneInclude); + var oneInclude = new Include(t, parsedFile, new Uri(Path.GetFullPath(includedFile))); + oneInclude.RangeToken = new RangeToken(includeStartToken, t); + theModule.Includes.Add(oneInclude); } .) } - { TopDecl } + { TopDecl } (. - defaultModule.RangeToken = new RangeToken(startToken, t); - // find the default class in the default module, then append membersDefaultClass to its member list - if (membersDefaultClass.Count == 0 && defaultModule.Includes.Count == 0 && defaultModule.TopLevelDecls.Count == 0 - && (defaultModule.PrefixNamedModules == null || defaultModule.PrefixNamedModules.Count == 0)) { - errors.Warning(new Token(1, 1) { Uri = la.Uri }, "File contains no code"); - } - DefaultClassDecl defaultClass = null; - foreach (TopLevelDecl topleveldecl in defaultModule.TopLevelDecls) { - defaultClass = topleveldecl as DefaultClassDecl; - if (defaultClass != null) { - defaultClass.Members.AddRange(membersDefaultClass); - break; - } - } - if (defaultClass == null) { // create the default class here, because it wasn't found - defaultClass = new DefaultClassDecl(defaultModule, membersDefaultClass); - defaultModule.TopLevelDecls.Add(defaultClass); - } .) + theModule.RangeToken = new RangeToken(fileStartToken.Next, t); + .) SYNC EOF . @@ -1060,7 +968,7 @@ DeclModifier . /*------------------------------------------------------------------------*/ -TopDecl<. ModuleDefinition module, List membersDefaultClass, bool isTopLevel, bool isAbstract .> +TopDecl<. ModuleDefinition module, bool isTopLevel, bool isAbstract .> = (. DeclModifierData dmod = new DeclModifierData(); ModuleDecl submodule; DatatypeDecl/*!*/ dt; TopLevelDecl td; IteratorDecl iter; TraitDecl/*!*/ trait; @@ -1072,16 +980,16 @@ TopDecl<. ModuleDefinition module, List membersDefaultClass, bo var tup = new Tuple, LiteralModuleDecl>(litmod.ModuleDef.PrefixIds, litmod); module.PrefixNamedModules.Add(tup); } else { - module.TopLevelDecls.Add(submodule); + module.SourceDecls.Add(submodule); } .) - | ClassDecl (. module.TopLevelDecls.Add(td); .) - | DatatypeDecl (. module.TopLevelDecls.Add(dt); .) - | NewtypeDecl (. module.TopLevelDecls.Add(td); .) - | SynonymTypeDecl (. module.TopLevelDecls.Add(td); .) - | IteratorDecl (. module.TopLevelDecls.Add(iter); .) - | TraitDecl (. module.TopLevelDecls.Add(trait); .) - | ClassMemberDecl + | ClassDecl (. module.SourceDecls.Add(td); .) + | DatatypeDecl (. module.SourceDecls.Add(dt); .) + | NewtypeDecl (. module.SourceDecls.Add(td); .) + | SynonymTypeDecl (. module.SourceDecls.Add(td); .) + | IteratorDecl (. module.SourceDecls.Add(iter); .) + | TraitDecl (. module.SourceDecls.Add(trait); .) + | ClassMemberDecl (. module.DefaultClass.SetMembersBeforeResolution(); .) ) . @@ -1106,7 +1014,6 @@ ModuleDefinition(); - List namedModuleDefaultClassMembers = new List();; List idRefined = null; ModuleDefinition module; submodule = null; // appease compiler @@ -1129,11 +1036,10 @@ ModuleDefinition} + { TopDecl} "}" (. module.RangeToken = new RangeToken(dmod.FirstToken, t); - module.TopLevelDecls.Add(new DefaultClassDecl(module, namedModuleDefaultClassMembers)); module.TokenWithTrailingDocString = tokenWithTrailingDocString; submodule = new LiteralModuleDecl(module, parent); submodule.RangeToken = module.RangeToken; @@ -1654,7 +1560,7 @@ SynonymTypeDecl ] (. if (td == null) { - if (module is DefaultModuleDefinition) { + if (module is DefaultModuleDefinition or FileModuleDefinition) { // abstract type declarations at the very outermost program scope get an automatic (!new) characteristics.ContainsNoReferenceTypes = true; } diff --git a/Source/DafnyCore/DafnyFile.cs b/Source/DafnyCore/DafnyFile.cs index 1b194fe12f3..d6d4fa80510 100644 --- a/Source/DafnyCore/DafnyFile.cs +++ b/Source/DafnyCore/DafnyFile.cs @@ -1,6 +1,7 @@ using System; using System.Collections.Generic; using System.IO; +using System.Linq; using System.Reflection.Metadata; using System.Reflection.PortableExecutable; using DafnyCore; @@ -8,21 +9,27 @@ namespace Microsoft.Dafny; public class DafnyFile { - public bool UseStdin { get; private set; } public string FilePath => Uri.LocalPath; public string CanonicalPath { get; private set; } public string BaseName { get; private set; } public bool IsPreverified { get; set; } public bool IsPrecompiled { get; set; } - public TextReader Content { get; } + public TextReader Content { get; set; } public Uri Uri { get; } - public DafnyFile(DafnyOptions options, string filePath, TextReader contentOverride = null) { - UseStdin = contentOverride != null; - Uri = contentOverride != null ? new Uri("stdin:///") : new Uri(filePath); - BaseName = contentOverride != null ? "" : Path.GetFileName(filePath); - var extension = contentOverride != null ? ".dfy" : Path.GetExtension(filePath); - if (extension != null) { extension = extension.ToLower(); } + public DafnyFile(DafnyOptions options, Uri uri, TextReader contentOverride = null) { + Uri = uri; + var filePath = uri.LocalPath; + + var extension = ".dfy"; + if (uri.IsFile) { + extension = Path.GetExtension(uri.LocalPath).ToLower(); + BaseName = Path.GetFileName(uri.LocalPath); + } + if (uri.Scheme == "stdin") { + contentOverride = options.Input; + BaseName = ""; + } // Normalizing symbolic links appears to be not // supported in .Net APIs, because it is very difficult in general @@ -113,7 +120,7 @@ public static Uri Canonicalize(string filePath) { } return new Uri(filePath.Substring("file:".Length)); } - public static List FileNames(IList dafnyFiles) { + public static List FileNames(IReadOnlyList dafnyFiles) { var sourceFiles = new List(); foreach (DafnyFile f in dafnyFiles) { sourceFiles.Add(f.FilePath); diff --git a/Source/DafnyCore/DafnyMain.cs b/Source/DafnyCore/DafnyMain.cs index c7a7d51a761..84a34a8b270 100644 --- a/Source/DafnyCore/DafnyMain.cs +++ b/Source/DafnyCore/DafnyMain.cs @@ -40,11 +40,11 @@ public static void MaybePrintProgram(Program program, string filename, bool afte /// /// Returns null on success, or an error string otherwise. /// - public static string ParseCheck(TextReader stdIn, IList /*!*/ files, string /*!*/ programName, + public static string ParseCheck(TextReader stdIn, IReadOnlyList /*!*/ files, string /*!*/ programName, DafnyOptions options, out Program program) //modifies Bpl.options.XmlSink.*; { - string err = Parse(stdIn, files, programName, options, out program); + string err = Parse(files, programName, options, out program); if (err != null) { return err; } @@ -52,69 +52,27 @@ public static string ParseCheck(TextReader stdIn, IList /*!*/ f return Resolve(program); } - public static string Parse(TextReader stdIn, IList files, string programName, DafnyOptions options, + public static string Parse(IReadOnlyList files, string programName, DafnyOptions options, out Program program) { Contract.Requires(programName != null); Contract.Requires(files != null); program = null; + var defaultClassFirst = options.VerifyAllModules; var defaultModuleDefinition = - new DefaultModuleDefinition(files.Where(f => !f.IsPreverified).Select(f => f.Uri).ToList()); + new DefaultModuleDefinition(files.Where(f => !f.IsPreverified).Select(f => f.Uri).ToList(), defaultClassFirst); ErrorReporter reporter = options.DiagnosticsFormat switch { DafnyOptions.DiagnosticsFormats.PlainText => new ConsoleErrorReporter(options, defaultModuleDefinition), DafnyOptions.DiagnosticsFormats.JSON => new JsonConsoleErrorReporter(options, defaultModuleDefinition), _ => throw new ArgumentOutOfRangeException() }; - LiteralModuleDecl module = new LiteralModuleDecl(defaultModuleDefinition, null); - BuiltIns builtIns = new BuiltIns(options); - - foreach (DafnyFile dafnyFile in files) { - Contract.Assert(dafnyFile != null); - if (options.XmlSink is { IsOpen: true } && !dafnyFile.UseStdin) { - options.XmlSink.WriteFileFragment(dafnyFile.FilePath); - } - - if (options.Trace) { - options.OutputWriter.WriteLine("Parsing " + dafnyFile.FilePath); - } - - // We model a precompiled file, a library, as an include - var include = dafnyFile.IsPrecompiled ? new Include(new Token { - Uri = dafnyFile.Uri, - col = 1, - line = 0 - }, new Uri("cli://"), dafnyFile.FilePath) : null; - if (include != null) { - // TODO this can be removed once the include error message in ErrorReporter.Error is removed. - module.ModuleDef.Includes.Add(include); - } - var err = ParseFile(dafnyFile, null, module, builtIns, new Errors(reporter)); - if (err != null) { - return err; - } + program = ParseUtils.ParseFiles(programName, files, reporter, CancellationToken.None); + var errorCount = program.Reporter.ErrorCount; + if (errorCount != 0) { + return $"{errorCount} parse errors detected in {program.Name}"; } - - if (!(options.DisallowIncludes || options.PrintIncludesMode == DafnyOptions.IncludesModes.Immediate)) { - string errString = ParseIncludes(module, builtIns, files.Select(f => f.FilePath).ToHashSet(), new Errors(reporter)); - if (errString != null) { - return errString; - } - } - - if (options.PrintIncludesMode == DafnyOptions.IncludesModes.Immediate) { - DependencyMap dmap = new DependencyMap(); - dmap.AddIncludes(module.ModuleDef.Includes); - dmap.PrintMap(options); - } - - var verifiedRoots = files.Where(df => df.IsPreverified).Select(df => df.Uri).ToHashSet(); - var compiledRoots = files.Where(df => df.IsPrecompiled).Select(df => df.Uri).ToHashSet(); - program = new Program(programName, module, builtIns, reporter, verifiedRoots, compiledRoots); - - MaybePrintProgram(program, options.DafnyPrintFile, false); - - return null; // success + return null; } private static readonly TaskScheduler largeThreadScheduler = @@ -140,83 +98,22 @@ public static string Resolve(Program program) { return null; // success } - // Lower-case file names before comparing them, since Windows uses case-insensitive file names - private class IncludeComparer : IComparer { - public int Compare(Include x, Include y) { - return x.CompareTo(y); - } - } - - public static string ParseIncludes(ModuleDecl module, BuiltIns builtIns, ISet excludeFiles, Errors errs) { - var includesFound = new SortedSet(new IncludeComparer()); - var allIncludes = ((LiteralModuleDecl)module).ModuleDef.Includes; - - var notCompiledResult = TraverseIncludesFrom(0); - if (notCompiledResult != null) { - return notCompiledResult; - } - - if (builtIns.Options.PrintIncludesMode != DafnyOptions.IncludesModes.None) { - var dependencyMap = new DependencyMap(); - dependencyMap.AddIncludes(allIncludes); - dependencyMap.PrintMap(builtIns.Options); - } - - return null; // Success - - string TraverseIncludesFrom(int startingIndex) { - var includeIndex = startingIndex; - var stack = new Stack(); - - while (true) { - var addedItems = allIncludes.Skip(includeIndex); - foreach (var addedItem in addedItems.Reverse()) { - stack.Push(addedItem); - } - - includeIndex = allIncludes.Count; - - if (stack.Count == 0) { - break; - } - - var include = stack.Pop(); - if (!includesFound.Add(include) || excludeFiles.Contains(include.CanonicalPath)) { - continue; - } - - DafnyFile file; - try { - file = new DafnyFile(builtIns.Options, include.IncludedFilename); - } catch (IllegalDafnyFile) { - return ($"Include of file \"{include.IncludedFilename}\" failed."); - } - - string result = ParseFile(file, include, module, builtIns, errs); - if (result != null) { - return result; - } - } - - return null; - } - } - - private static string ParseFile(DafnyFile dafnyFile, Include include, ModuleDecl module, BuiltIns builtIns, Errors errs) { - var fn = builtIns.Options.UseBaseNameForFileName ? Path.GetFileName(dafnyFile.FilePath) : dafnyFile.FilePath; - try { - int errorCount = Parser.Parse(dafnyFile.Content, dafnyFile.Uri, module, builtIns, errs); - if (errorCount != 0) { - return $"{errorCount} parse errors detected in {fn}"; - } - } catch (IOException e) { - IToken tok = include == null ? Token.NoToken : include.tok; - errs.SemErr(tok, "Unable to open included file"); - return $"Error opening file \"{fn}\": {e.Message}"; - } - - return null; // Success - } + // private static string ParseFile(DafnyFile dafnyFile, Include include, BuiltIns builtIns, ErrorReporter errorReporter) { + // var fn = builtIns.Options.UseBaseNameForFileName ? Path.GetFileName(dafnyFile.FilePath) : dafnyFile.FilePath; + // try { + // var parseResult = ParseUtils.Parse(dafnyFile.Content, dafnyFile.Uri, builtIns, errorReporter); + // var errorCount = parseResult.ErrorCount; + // if (errorCount != 0) { + // return $"{errorCount} parse errors detected in {fn}"; + // } + // } catch (IOException e) { + // IToken tok = include == null ? Token.NoToken : include.tok; + // errorReporter.Error(MessageSource.Parser, tok, "Unable to open included file"); + // return $"Error opening file \"{fn}\": {e.Message}"; + // } + // + // return null; // Success + // } public static async Task<(PipelineOutcome Outcome, PipelineStatistics Statistics)> BoogieOnce( DafnyOptions options, diff --git a/Source/DafnyCore/Generic/IPointer.cs b/Source/DafnyCore/Generic/IPointer.cs new file mode 100644 index 00000000000..8f4b7f3d729 --- /dev/null +++ b/Source/DafnyCore/Generic/IPointer.cs @@ -0,0 +1,28 @@ +using System; +using System.Collections.Generic; +using System.Linq; +using System.Reflection; + +namespace Microsoft.Dafny; + +public interface IPointer { + T Get(); + void Set(T value); +} + +record Pointer(Func Get, Action Set) : IPointer { + T IPointer.Get() { + return Get(); + } + + void IPointer.Set(T value) { + Set(value); + } +} + +public static class PointerExtensions { + public static IEnumerable> ToPointers(this IList values) { + return Enumerable.Range(0, values.Count) + .Select(index => new Pointer(() => values[index], value => values[index] = value)); + } +} \ No newline at end of file diff --git a/Source/DafnyCore/Generic/Reporting.cs b/Source/DafnyCore/Generic/Reporting.cs index fefd9ffb538..9ec27181a17 100644 --- a/Source/DafnyCore/Generic/Reporting.cs +++ b/Source/DafnyCore/Generic/Reporting.cs @@ -46,8 +46,9 @@ public void Error(MessageSource source, IToken tok, string msg) { public virtual void Error(MessageSource source, string errorId, IToken tok, string msg) { Contract.Requires(tok != null); Contract.Requires(msg != null); + // TODO move this out of ErrorReporter together with OuterModule. Let Program have a list of FileModuleDefinitions as constructor input and create its default module there. if (tok.FromIncludeDirective(OuterModule) && OuterModule != null) { - var include = OuterModule.Includes.First(i => new Uri(i.IncludedFilename).LocalPath == tok.ActualFilename); + var include = OuterModule.Includes.First(i => i.IncludedFilename == tok.Uri); if (!include.ErrorReported) { Message(source, ErrorLevel.Error, null, include.tok, "the included file " + Path.GetFileName(tok.ActualFilename) + " contains error(s)"); include.ErrorReported = true; diff --git a/Source/DafnyCore/Generic/Util.cs b/Source/DafnyCore/Generic/Util.cs index ae1117bf1eb..1f087f4c4c4 100644 --- a/Source/DafnyCore/Generic/Util.cs +++ b/Source/DafnyCore/Generic/Util.cs @@ -13,8 +13,8 @@ using JetBrains.Annotations; using Microsoft.Boogie; -namespace Microsoft.Dafny { +namespace Microsoft.Dafny { public static class Sets { public static ISet Empty() { return new HashSet(); @@ -715,7 +715,7 @@ public bool Traverse(ModuleDefinition moduleDefinition) { return Traverse(moduleDefinition.TopLevelDecls); } - public bool Traverse(List topLevelDecls) { + public bool Traverse(IEnumerable topLevelDecls) { if (topLevelDecls == null) { return false; } diff --git a/Source/DafnyCore/Options/ProjectFile.cs b/Source/DafnyCore/Options/ProjectFile.cs index 2ecc79bcfe4..fa1be2c0565 100644 --- a/Source/DafnyCore/Options/ProjectFile.cs +++ b/Source/DafnyCore/Options/ProjectFile.cs @@ -25,9 +25,9 @@ public class ProjectFile { public string[] Excludes { get; set; } public Dictionary Options { get; set; } - public static ProjectFile Open(Uri uri, TextWriter errorWriter) { + public static ProjectFile Open(Uri uri, TextWriter outputWriter, TextWriter errorWriter) { if (Path.GetFileName(uri.LocalPath) != FileName) { - Console.WriteLine($"Warning: only Dafny project files named {FileName} are recognised by the Dafny IDE."); + outputWriter.WriteLine($"Warning: only Dafny project files named {FileName} are recognised by the Dafny IDE."); } try { var file = File.Open(uri.LocalPath, FileMode.Open); @@ -67,14 +67,14 @@ public void AddFilesToOptions(DafnyOptions options) { } } - public void Validate(IEnumerable - private void AddDefaultBaseTypeToUnresolvedNewtypes(List topLevelDecls) { + private void AddDefaultBaseTypeToUnresolvedNewtypes(IEnumerable topLevelDecls) { foreach (var d in topLevelDecls) { if (d is NewtypeDecl { IsRefining: true, BaseType: null } decl) { Reporter.Info(MessageSource.RefinementTransformer, decl.tok, $"defaulting to 'int' for unspecified base type of '{decl.Name}'"); @@ -296,8 +295,10 @@ private void MergeModuleExports(ModuleExportDecl nw, ModuleExportDecl d) { nw.Extends.AddRange(d.Extends); } - private void MergeTopLevelDecls(ModuleDefinition m, TopLevelDecl nw, TopLevelDecl d, int index) { + private void MergeTopLevelDecls(ModuleDefinition m, IPointer nwPointer, TopLevelDecl d) { + var nw = nwPointer.Get(); var commonMsg = "a {0} declaration ({1}) in a refinement module can only refine a {0} declaration or replace an abstract type declaration"; + // Prefix decls. if (d is ModuleDecl) { if (!(nw is ModuleDecl)) { @@ -373,7 +374,7 @@ private void MergeTopLevelDecls(ModuleDefinition m, TopLevelDecl nw, TopLevelDec } } if (nw is TopLevelDeclWithMembers) { - m.TopLevelDecls[index] = MergeClass((TopLevelDeclWithMembers)nw, od); + nwPointer.Set(MergeClass((TopLevelDeclWithMembers)nw, od)); } else if (od.Members.Count != 0) { Reporter.Error(MessageSource.RefinementTransformer, nw, "a {0} ({1}) cannot declare members, so it cannot refine an abstract type with members", @@ -389,7 +390,7 @@ private void MergeTopLevelDecls(ModuleDefinition m, TopLevelDecl nw, TopLevelDec var (dd, nwd) = ((DatatypeDecl)d, (DatatypeDecl)nw); Contract.Assert(!nwd.Ctors.Any()); nwd.Ctors.AddRange(dd.Ctors.Select(refinementCloner.CloneCtor)); - m.TopLevelDecls[index] = MergeClass((DatatypeDecl)nw, (DatatypeDecl)d); + nwPointer.Set(MergeClass((DatatypeDecl)nw, (DatatypeDecl)d)); } else if (nw is DatatypeDecl) { Reporter.Error(MessageSource.RefinementTransformer, nw, commonMsg, nw.WhatKind, nw.Name); } else if (d is NewtypeDecl && nw is NewtypeDecl) { @@ -401,31 +402,31 @@ private void MergeTopLevelDecls(ModuleDefinition m, TopLevelDecl nw, TopLevelDec nwn.Constraint = dn.Constraint == null ? null : refinementCloner.CloneExpr(dn.Constraint); nwn.WitnessKind = dn.WitnessKind; nwn.Witness = dn.Witness == null ? null : refinementCloner.CloneExpr(dn.Witness); - m.TopLevelDecls[index] = MergeClass((NewtypeDecl)nw, (NewtypeDecl)d); + nwPointer.Set(MergeClass((NewtypeDecl)nw, (NewtypeDecl)d)); } else if (nw is NewtypeDecl) { // `.Basetype` will be set in AddDefaultBaseTypeToUnresolvedNewtypes Reporter.Error(MessageSource.RefinementTransformer, nw, commonMsg, nw.WhatKind, nw.Name); } else if (nw is IteratorDecl) { if (d is IteratorDecl) { - m.TopLevelDecls[index] = MergeIterator((IteratorDecl)nw, (IteratorDecl)d); + nwPointer.Set(MergeIterator((IteratorDecl)nw, (IteratorDecl)d)); } else { Reporter.Error(MessageSource.RefinementTransformer, nw, "an iterator declaration ({0}) in a refining module cannot replace a different kind of declaration in the refinement base", nw.Name); } } else if (nw is TraitDecl) { if (d is TraitDecl) { - m.TopLevelDecls[index] = MergeClass((TraitDecl)nw, (TraitDecl)d); + nwPointer.Set(MergeClass((TraitDecl)nw, (TraitDecl)d)); } else { Reporter.Error(MessageSource.RefinementTransformer, nw, commonMsg, nw.WhatKind, nw.Name); } } else if (nw is ClassDecl) { if (d is ClassDecl) { - m.TopLevelDecls[index] = MergeClass((ClassDecl)nw, (ClassDecl)d); + nwPointer.Set(MergeClass((ClassDecl)nw, (ClassDecl)d)); } else { Reporter.Error(MessageSource.RefinementTransformer, nw, commonMsg, nw.WhatKind, nw.Name); } } else if (nw is DefaultClassDecl) { if (d is DefaultClassDecl) { - m.TopLevelDecls[index] = MergeClass((DefaultClassDecl)nw, (DefaultClassDecl)d); + m.DefaultClass = (DefaultClassDecl)MergeClass((DefaultClassDecl)nw, (DefaultClassDecl)d); } else { Reporter.Error(MessageSource.RefinementTransformer, nw, commonMsg, nw.WhatKind, nw.Name); } diff --git a/Source/DafnyCore/Verifier/Translator.cs b/Source/DafnyCore/Verifier/Translator.cs index f773eae7f12..13b50ddbc71 100644 --- a/Source/DafnyCore/Verifier/Translator.cs +++ b/Source/DafnyCore/Verifier/Translator.cs @@ -793,7 +793,7 @@ private Bpl.Program DoTranslation(Program p, ModuleDefinition forModule) { mods.Insert(0, forModule); foreach (ModuleDefinition m in mods) { - foreach (TopLevelDecl d in m.TopLevelDecls.FindAll(VisibleInScope)) { + foreach (TopLevelDecl d in m.TopLevelDecls.Where(VisibleInScope)) { currentDeclaration = d; if (d is AbstractTypeDecl) { var dd = (AbstractTypeDecl)d; diff --git a/Source/DafnyDriver/Commands/CommandRegistry.cs b/Source/DafnyDriver/Commands/CommandRegistry.cs index fe8b37c5198..b02041897c3 100644 --- a/Source/DafnyDriver/Commands/CommandRegistry.cs +++ b/Source/DafnyDriver/Commands/CommandRegistry.cs @@ -7,6 +7,7 @@ using System.CommandLine.Invocation; using System.CommandLine.IO; using System.CommandLine.Parsing; +using System.Diagnostics; using System.IO; using System.Linq; using System.Reflection; @@ -58,6 +59,7 @@ static CommandRegistry() { GetValueForOptionMethod = method; } } + Debug.Assert(GetValueForOptionMethod != null); } public static Argument FileArgument { get; } @@ -257,11 +259,11 @@ private static bool ProcessFile(DafnyOptions dafnyOptions, FileInfo singleFile) dafnyOptions.ErrorWriter.WriteLine($"Error: file {filePathForErrors} not found"); return false; } - var projectFile = ProjectFile.Open(new Uri(singleFile.FullName), dafnyOptions.ErrorWriter); + var projectFile = ProjectFile.Open(new Uri(singleFile.FullName), dafnyOptions.OutputWriter, dafnyOptions.ErrorWriter); if (projectFile == null) { return false; } - projectFile.Validate(AllOptions); + projectFile.Validate(dafnyOptions.OutputWriter, AllOptions); dafnyOptions.ProjectFile = projectFile; projectFile.AddFilesToOptions(dafnyOptions); } else { diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index 2c0d9f096ef..568dcde26a7 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -18,16 +18,12 @@ using System; using System.Collections.Generic; using System.Collections.ObjectModel; -using System.CommandLine; -using System.CommandLine.IO; using System.Diagnostics.Contracts; using System.IO; using System.Linq; using Microsoft.Boogie; using Bpl = Microsoft.Boogie; using System.Diagnostics; -using System.Threading; -using DafnyCore; using Microsoft.Dafny.Plugins; namespace Microsoft.Dafny { @@ -242,8 +238,9 @@ public static CommandLineArgumentsResult ProcessCommandLineArguments(TextWriter } if (options.UseStdin) { - options.CliRootSourceUris.Add(new Uri("stdin:///")); - dafnyFiles.Add(new DafnyFile(options, "", inputReader)); + var uri = new Uri("stdin:///"); + options.CliRootSourceUris.Add(uri); + dafnyFiles.Add(new DafnyFile(options, uri)); } else if (options.CliRootSourceUris.Count == 0 && !options.Format) { options.Printer.ErrorWriteLine(options.ErrorWriter, "*** Error: No input files were specified in command-line " + string.Join("|", args) + "."); return CommandLineArgumentsResult.PREPROCESSING_ERROR; @@ -272,12 +269,12 @@ public static CommandLineArgumentsResult ProcessCommandLineArguments(TextWriter if (extension != null) { extension = extension.ToLower(); } bool isDafnyFile = false; - var relative = System.IO.Path.GetFileName(file); + var relative = Path.GetFileName(file); bool useRelative = options.UseBaseNameForFileName || relative.StartsWith("-"); var nameToShow = useRelative ? relative : Path.GetRelativePath(Directory.GetCurrentDirectory(), file); try { - var df = new DafnyFile(options, Path.GetFullPath(file)); + var df = new DafnyFile(options, new Uri(Path.GetFullPath(file))); if (options.LibraryFiles.Contains(file)) { df.IsPreverified = true; df.IsPrecompiled = true; @@ -359,7 +356,7 @@ public static CommandLineArgumentsResult ProcessCommandLineArguments(TextWriter return CommandLineArgumentsResult.OK; } - private async Task ProcessFilesAsync(IList/*!*/ dafnyFiles, + private async Task ProcessFilesAsync(IReadOnlyList/*!*/ dafnyFiles, ReadOnlyCollection otherFileNames, DafnyOptions options, bool lookForSnapshots = true, string programId = null) { Contract.Requires(cce.NonNullElements(dafnyFiles)); @@ -402,8 +399,9 @@ private async Task ProcessFilesAsync(IList/*!*/ dafny foreach (var s in snapshotsByVersion) { var snapshots = new List(); foreach (var f in s) { - snapshots.Add(new DafnyFile(options, f)); - options.CliRootSourceUris.Add(new Uri(Path.GetFullPath(f))); + var uri = new Uri(Path.GetFullPath(f)); + snapshots.Add(new DafnyFile(options, uri)); + options.CliRootSourceUris.Add(uri); } var ev = await ProcessFilesAsync(snapshots, new List().AsReadOnly(), options, false, programId); if (exitValue != ev && ev != ExitValue.SUCCESS) { @@ -458,12 +456,12 @@ private async Task ProcessFilesAsync(IList/*!*/ dafny return exitValue; } - private static ExitValue DoFormatting(IList dafnyFiles, DafnyOptions options, string programName, TextWriter errorWriter) { + private static ExitValue DoFormatting(IReadOnlyList dafnyFiles, DafnyOptions options, string programName, TextWriter errorWriter) { var exitValue = ExitValue.SUCCESS; Contract.Assert(dafnyFiles.Count > 0 || options.FoldersToFormat.Count > 0); dafnyFiles = dafnyFiles.Concat(options.FoldersToFormat.SelectMany(folderPath => { return Directory.GetFiles(folderPath, "*.dfy", SearchOption.AllDirectories) - .Select(name => new DafnyFile(options, name)).ToList(); + .Select(name => new DafnyFile(options, new Uri(name))).ToList(); })).ToList(); var failedToParseFiles = new List(); @@ -474,24 +472,23 @@ private static ExitValue DoFormatting(IList dafnyFiles, DafnyOptions var neededFormatting = 0; foreach (var file in dafnyFiles) { var dafnyFile = file; - if (dafnyFile.UseStdin && !doCheck && !doPrint) { + if (!dafnyFile.Uri.IsFile && !doCheck && !doPrint) { errorWriter.WriteLine("Please use the --check and/or --print option as stdin cannot be formatted in place."); exitValue = ExitValue.PREPROCESSING_ERROR; continue; } string tempFileName = null; - if (dafnyFile.UseStdin) { + if (!dafnyFile.Uri.IsFile) { tempFileName = Path.GetTempFileName() + ".dfy"; WriteFile(tempFileName, Console.In.ReadToEnd()); - dafnyFile = new DafnyFile(options, tempFileName); + dafnyFile = new DafnyFile(options, new Uri(tempFileName)); } + var originalText = dafnyFile.Content.ReadToEnd(); + dafnyFile.Content = new StringReader(originalText); // Might not be totally optimized but let's do that for now - var err = DafnyMain.Parse(options.Input, new List { dafnyFile }, programName, options, out var dafnyProgram); - var originalText = dafnyFile.UseStdin ? Console.In.ReadToEnd() : - File.Exists(dafnyFile.FilePath) ? - File.ReadAllText(dafnyFile.FilePath) : null; + var err = DafnyMain.Parse(new List { dafnyFile }, programName, options, out var dafnyProgram); if (err != null) { exitValue = ExitValue.DAFNY_ERROR; errorWriter.WriteLine(err); diff --git a/Source/DafnyLanguageServer.Test/Lookup/DefinitionTest.cs b/Source/DafnyLanguageServer.Test/Lookup/DefinitionTest.cs index 659711bbfac..88e8e6f4527 100644 --- a/Source/DafnyLanguageServer.Test/Lookup/DefinitionTest.cs +++ b/Source/DafnyLanguageServer.Test/Lookup/DefinitionTest.cs @@ -295,7 +295,8 @@ method DoIt() { }".TrimStart(); var documentItem = CreateTestDocument(source); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); - Assert.False((await RequestDefinition(documentItem, (2, 14)).AsTask()).Any()); + var locations = await RequestDefinition(documentItem, (2, 14)).AsTask(); + Assert.False(locations.Any()); } [Fact] diff --git a/Source/DafnyLanguageServer.Test/Unit/DafnyLangSymbolResolverTest.cs b/Source/DafnyLanguageServer.Test/Unit/DafnyLangSymbolResolverTest.cs index b7b87d2c10a..dcd3fcd2ad6 100644 --- a/Source/DafnyLanguageServer.Test/Unit/DafnyLangSymbolResolverTest.cs +++ b/Source/DafnyLanguageServer.Test/Unit/DafnyLangSymbolResolverTest.cs @@ -27,7 +27,7 @@ public CollectingErrorReporter(DafnyOptions options, DefaultModuleDefinition out class DummyModuleDecl : LiteralModuleDecl { public DummyModuleDecl() : base( - new DefaultModuleDefinition(new List()), null) { + new DefaultModuleDefinition(new List(), false), null) { } public override object Dereference() { return this; diff --git a/Source/DafnyLanguageServer.Test/Unit/GhostStateDiagnosticCollectorTest.cs b/Source/DafnyLanguageServer.Test/Unit/GhostStateDiagnosticCollectorTest.cs index ce4f4d6c0ef..d36131fe201 100644 --- a/Source/DafnyLanguageServer.Test/Unit/GhostStateDiagnosticCollectorTest.cs +++ b/Source/DafnyLanguageServer.Test/Unit/GhostStateDiagnosticCollectorTest.cs @@ -49,7 +49,7 @@ public CollectingErrorReporter(DafnyOptions options, DefaultModuleDefinition out class DummyModuleDecl : LiteralModuleDecl { public DummyModuleDecl(IList rootUris) : base( - new DefaultModuleDefinition(rootUris), null) { + new DefaultModuleDefinition(rootUris, false), null) { } public override object Dereference() { return this; diff --git a/Source/DafnyLanguageServer.Test/Unit/ParserExceptionTest.cs b/Source/DafnyLanguageServer.Test/Unit/ParserExceptionTest.cs index 99b23a347af..b60aa674664 100644 --- a/Source/DafnyLanguageServer.Test/Unit/ParserExceptionTest.cs +++ b/Source/DafnyLanguageServer.Test/Unit/ParserExceptionTest.cs @@ -2,6 +2,7 @@ using System.Collections.Generic; using Microsoft.Dafny.LanguageServer.Language; using System.IO; +using Microsoft.Dafny.LanguageServer.Workspace; using Microsoft.Extensions.Logging; using OmniSharp.Extensions.LanguageServer.Protocol; using OmniSharp.Extensions.LanguageServer.Protocol.Models; @@ -28,10 +29,9 @@ public void DocumentWithParserExceptionDisplaysIt() { var options = new DafnyOptions(DafnyOptions.DefaultImmutableOptions); var documentItem = CreateTestDocument(source, TestFilePath); var uri = new Uri("file:///" + TestFilePath); - var outerModule = new DefaultModuleDefinition(new List { uri }); + var outerModule = new DefaultModuleDefinition(new List { uri }, false); var errorReporter = new ParserExceptionSimulatingErrorReporter(options, outerModule); - parser.Parse(documentItem, errorReporter, default); - Assert.Equal($"encountered an exception while parsing {uri}", lastDebugLogger.LastDebugMessage); + parser.Parse(new DocumentTextBuffer(documentItem), errorReporter, default); Assert.Equal($"/{TestFilePath}(1,0): Error: [internal error] Parser exception: Simulated parser internal error", errorReporter.LastMessage); } @@ -56,7 +56,7 @@ public override bool Message(MessageSource source, ErrorLevel level, string erro } public override int Count(ErrorLevel level) { - throw new NotImplementedException(); + return numberOfErrors; } public override int CountExceptVerifierAndCompiler(ErrorLevel level) { diff --git a/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs b/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs index 67d4097e263..0bcd53bdfae 100644 --- a/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs +++ b/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs @@ -58,7 +58,7 @@ private static DocumentTextBuffer CreateTestDocument() { [Fact] public async Task LoadReturnsCanceledTaskIfOperationIsCanceled() { var source = new CancellationTokenSource(); - parser.Setup(p => p.Parse(It.IsAny(), + parser.Setup(p => p.Parse(It.IsAny(), It.IsAny(), It.IsAny())).Callback(() => source.Cancel()) .Throws(); @@ -75,7 +75,7 @@ public async Task LoadReturnsCanceledTaskIfOperationIsCanceled() { [Fact] public async Task LoadReturnsFaultedTaskIfAnyExceptionOccured() { - parser.Setup(p => p.Parse(It.IsAny(), It.IsAny(), It.IsAny())) + parser.Setup(p => p.Parse(It.IsAny(), It.IsAny(), It.IsAny())) .Throws(); var task = textDocumentLoader.LoadAsync(DafnyOptions.Default, CreateTestDocument(), default); try { diff --git a/Source/DafnyLanguageServer.Test/_plugins/PluginsTest.cs b/Source/DafnyLanguageServer.Test/_plugins/PluginsTest.cs index 06744a75af1..6e651b8380a 100644 --- a/Source/DafnyLanguageServer.Test/_plugins/PluginsTest.cs +++ b/Source/DafnyLanguageServer.Test/_plugins/PluginsTest.cs @@ -21,8 +21,8 @@ public ErrorRewriter(ErrorReporter reporter, TestConfiguration configuration) : this.configuration = configuration; } - public override void PostResolve(ModuleDefinition moduleDefinition) { - Reporter.Error(MessageSource.Resolver, moduleDefinition.GetFirstTopLevelToken(), "Impossible to continue " + configuration.Argument); + public override void PostResolve(Program program) { + Reporter.Error(MessageSource.Resolver, program.GetFirstTopLevelToken(), "Impossible to continue " + configuration.Argument); } } diff --git a/Source/DafnyLanguageServer/Language/DafnyLangParser.cs b/Source/DafnyLanguageServer/Language/DafnyLangParser.cs index e34315f203a..f94fadad33c 100644 --- a/Source/DafnyLanguageServer/Language/DafnyLangParser.cs +++ b/Source/DafnyLanguageServer/Language/DafnyLangParser.cs @@ -4,8 +4,10 @@ using System; using System.Collections.Generic; using System.IO; +using System.Linq; using System.Threading; using Microsoft.Boogie; +using Microsoft.Dafny.LanguageServer.Workspace; using OmniSharp.Extensions.LanguageServer.Protocol; namespace Microsoft.Dafny.LanguageServer.Language { @@ -46,38 +48,16 @@ public Dafny.Program CreateUnparsed(TextDocumentItem document, ErrorReporter err } } - public Dafny.Program Parse(TextDocumentItem document, ErrorReporter errorReporter, CancellationToken cancellationToken) { + public Dafny.Program Parse(DocumentTextBuffer document, ErrorReporter errorReporter, CancellationToken cancellationToken) { mutex.Wait(cancellationToken); - var program = NewDafnyProgram(document, errorReporter); - try { - var parseErrors = Parser.Parse( - document.Text, - // We use the full path as filename so we can better re-construct the DocumentUri for the definition lookup. - document.Uri.ToUri(), - program.DefaultModule, - program.BuiltIns, - errorReporter - ); - if (parseErrors != 0) { - logger.LogDebug("encountered {ErrorCount} errors while parsing {DocumentUri}", parseErrors, document.Uri); - } - - if (!TryParseIncludesOfModule(document.Uri, program.DefaultModule, program.BuiltIns, errorReporter, cancellationToken)) { - logger.LogDebug("encountered error while parsing the includes of {DocumentUri}", document.Uri); - } - return program; - } catch (Exception e) { - logger.LogDebug(e, "encountered an exception while parsing {DocumentUri}", document.Uri); - var internalErrorDummyToken = new Token { - Uri = document.Uri.ToUri(), - line = 1, - col = 1, - pos = 0, - val = string.Empty - }; - errorReporter.Error(MessageSource.Parser, internalErrorDummyToken, "[internal error] Parser exception: " + e.Message); - return program; + try { + return ParseUtils.ParseFiles(document.Uri.ToString(), + new DafnyFile[] + { + new(errorReporter.Options, document.Uri.ToUri(), document.Content) + }, + errorReporter, cancellationToken); } finally { mutex.Release(); @@ -99,66 +79,5 @@ private Dafny.Program NewDafnyProgram(TextDocumentItem document, ErrorReporter e public void Dispose() { mutex.Dispose(); } - - // TODO The following methods are based on the ones from DafnyPipeline/DafnyMain.cs. - // It could be convenient to adapt them in the main-repo so location info could be extracted. - private bool TryParseIncludesOfModule( - DocumentUri root, - ModuleDecl module, - BuiltIns builtIns, - ErrorReporter errorReporter, - CancellationToken cancellationToken - ) { - var errors = new Errors(errorReporter); - // Issue #40: - // A HashSet must not be used here since equals treats A included by B not equal to A included by C. - // In contrast, the compareTo-Method treats them as the same. - var resolvedIncludes = new SortedSet(); - resolvedIncludes.Add(new Include(Token.NoToken, root.ToUri(), root.ToString())); - - bool newIncludeParsed = true; - while (newIncludeParsed) { - cancellationToken.ThrowIfCancellationRequested(); - newIncludeParsed = false; - // Parser.Parse appears to modify the include list; thus, we create a copy to avoid concurrent modifications. - var moduleIncludes = new List(((LiteralModuleDecl)module).ModuleDef.Includes); - foreach (var include in moduleIncludes) { - bool isNewInclude = resolvedIncludes.Add(include); - if (isNewInclude) { - newIncludeParsed = true; - if (!TryParseInclude(include, module, builtIns, errorReporter, errors)) { - return false; - } - } - } - } - - return true; - } - - private bool TryParseInclude(Include include, ModuleDecl module, BuiltIns builtIns, ErrorReporter errorReporter, Errors errors) { - try { - var dafnyFile = new DafnyFile(builtIns.Options, include.IncludedFilename); - int errorCount = Parser.Parse( - dafnyFile.Content, - dafnyFile.Uri, - module, - builtIns, - errors - ); - if (errorCount != 0) { - return false; - } - } catch (IllegalDafnyFile e) { - errorReporter.Error(MessageSource.Parser, include.tok, $"Include of file '{include.IncludedFilename}' failed."); - logger.LogDebug(e, "encountered include of illegal dafny file {Filename}", include.IncludedFilename); - return false; - } catch (IOException e) { - errorReporter.Error(MessageSource.Parser, include.tok, $"Unable to open the include {include.IncludedFilename}."); - logger.LogDebug(e, "could not open file {Filename}", include.IncludedFilename); - return false; - } - return true; - } } } diff --git a/Source/DafnyLanguageServer/Language/IDafnyParser.cs b/Source/DafnyLanguageServer/Language/IDafnyParser.cs index a5be6125b0e..f1d3fc393d3 100644 --- a/Source/DafnyLanguageServer/Language/IDafnyParser.cs +++ b/Source/DafnyLanguageServer/Language/IDafnyParser.cs @@ -1,5 +1,6 @@ using OmniSharp.Extensions.LanguageServer.Protocol.Models; using System.Threading; +using Microsoft.Dafny.LanguageServer.Workspace; namespace Microsoft.Dafny.LanguageServer.Language { /// @@ -29,6 +30,6 @@ public interface IDafnyParser { /// The parsed document represented as a dafny program. /// Thrown when the cancellation was requested before completion. /// Thrown if the cancellation token was disposed before the completion. - Dafny.Program Parse(TextDocumentItem textDocument, ErrorReporter errorReporter, CancellationToken cancellationToken); + Dafny.Program Parse(DocumentTextBuffer textDocument, ErrorReporter errorReporter, CancellationToken cancellationToken); } } diff --git a/Source/DafnyLanguageServer/Language/Symbols/SignatureAndCompletionTable.cs b/Source/DafnyLanguageServer/Language/Symbols/SignatureAndCompletionTable.cs index 759d7341b82..886ea00a133 100644 --- a/Source/DafnyLanguageServer/Language/Symbols/SignatureAndCompletionTable.cs +++ b/Source/DafnyLanguageServer/Language/Symbols/SignatureAndCompletionTable.cs @@ -43,7 +43,7 @@ public class SignatureAndCompletionTable { private readonly DafnyLangTypeResolver typeResolver; public static SignatureAndCompletionTable Empty(DafnyOptions options, DocumentTextBuffer textDocument) { - var outerModule = new DefaultModuleDefinition(new List() { textDocument.Uri.ToUri() }); + var outerModule = new DefaultModuleDefinition(new List() { textDocument.Uri.ToUri() }, false); var errorReporter = new DiagnosticErrorReporter(options, outerModule, textDocument.Text, textDocument.Uri); return new SignatureAndCompletionTable( NullLogger.Instance, diff --git a/Source/DafnyLanguageServer/Workspace/DocumentManager.cs b/Source/DafnyLanguageServer/Workspace/DocumentManager.cs index e4b1b956cc0..d972e1f0f61 100644 --- a/Source/DafnyLanguageServer/Workspace/DocumentManager.cs +++ b/Source/DafnyLanguageServer/Workspace/DocumentManager.cs @@ -140,8 +140,7 @@ private static DafnyOptions DetermineDocumentOptions(DafnyOptions serverOptions, while (!string.IsNullOrEmpty(folder)) { var children = Directory.GetFiles(folder, "dfyconfig.toml"); if (children.Length > 0) { - var errorWriter = TextWriter.Null; - projectFile = ProjectFile.Open(new Uri(children[0]), errorWriter); + projectFile = ProjectFile.Open(new Uri(children[0]), serverOptions.OutputWriter, serverOptions.ErrorWriter); if (projectFile != null) { break; } diff --git a/Source/DafnyLanguageServer/Workspace/DocumentTextBuffer.cs b/Source/DafnyLanguageServer/Workspace/DocumentTextBuffer.cs index b3b5b705821..c28f12da43b 100644 --- a/Source/DafnyLanguageServer/Workspace/DocumentTextBuffer.cs +++ b/Source/DafnyLanguageServer/Workspace/DocumentTextBuffer.cs @@ -1,3 +1,4 @@ +using System.IO; using System.Net.Mime; using OmniSharp.Extensions.LanguageServer.Protocol; using OmniSharp.Extensions.LanguageServer.Protocol.Models; @@ -37,4 +38,5 @@ public string Extract(Range range) { public int? Version => TextDocumentItem.Version; public int NumberOfLines => Buffer.Lines.Count; + public TextReader Content => new StringReader(Text); } \ No newline at end of file diff --git a/Source/DafnyLanguageServer/Workspace/SymbolTable.cs b/Source/DafnyLanguageServer/Workspace/SymbolTable.cs index fe7cbc4b337..548a7b36332 100644 --- a/Source/DafnyLanguageServer/Workspace/SymbolTable.cs +++ b/Source/DafnyLanguageServer/Workspace/SymbolTable.cs @@ -21,13 +21,15 @@ private SymbolTable() { public SymbolTable(Document document, IReadOnlyList<(IDeclarationOrUsage usage, IDeclarationOrUsage declaration)> usages) { var safeUsages = usages.Where(k => k.declaration.NameToken.Uri != null).ToList(); - Declarations = safeUsages.DistinctBy(k => k.usage).ToDictionary(k => k.usage, k => k.declaration); + Declarations = safeUsages.DistinctBy(k => k.usage). + ToDictionary(k => k.usage, k => k.declaration); Usages = safeUsages.GroupBy(u => u.declaration).ToDictionary( g => g.Key, g => (ISet)g.Select(k => k.usage).ToHashSet()); NodePositions = new IntervalTree(); var symbols = safeUsages.Select(u => u.declaration).Concat(usages.Select(u => u.usage)). - Where(u => u.NameToken.Uri == document.Uri.ToUri() && !AutoGeneratedToken.Is(u.NameToken)).Distinct(); + Where(u => u.NameToken.Uri == document.Uri.ToUri() + && !AutoGeneratedToken.Is(u.NameToken)).Distinct(); foreach (var symbol in symbols) { var range = symbol.NameToken.GetLspRange(); NodePositions.Add(range.Start, range.End, symbol); diff --git a/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs b/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs index e0d26389fc2..3846d072aa1 100644 --- a/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs +++ b/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs @@ -82,7 +82,7 @@ public async Task LoadAsync(DafnyOptions options, Document private DocumentAfterParsing LoadInternal(DafnyOptions options, DocumentTextBuffer textDocument, CancellationToken cancellationToken) { - var outerModule = new DefaultModuleDefinition(new List() { textDocument.Uri.ToUri() }); + var outerModule = new DefaultModuleDefinition(new List() { textDocument.Uri.ToUri() }, false); var errorReporter = new DiagnosticErrorReporter(options, outerModule, textDocument.Text, textDocument.Uri); statusPublisher.SendStatusNotification(textDocument, CompilationStatus.Parsing); var program = parser.Parse(textDocument, errorReporter, cancellationToken); diff --git a/Source/DafnyPipeline.Test/FormatterBaseTest.cs b/Source/DafnyPipeline.Test/FormatterBaseTest.cs index 0af51e22af4..5cb07ebb7eb 100644 --- a/Source/DafnyPipeline.Test/FormatterBaseTest.cs +++ b/Source/DafnyPipeline.Test/FormatterBaseTest.cs @@ -42,6 +42,7 @@ enum Newlines { protected void FormatterWorksFor(string testCase, string? expectedProgramString = null, bool expectNoToken = false, bool reduceBlockiness = true) { var options = DafnyOptions.Create(output); + options.DisallowIncludes = true; var newlineTypes = Enum.GetValues(typeof(Newlines)); foreach (Newlines newLinesType in newlineTypes) { currentNewlines = newLinesType; @@ -54,13 +55,11 @@ protected void FormatterWorksFor(string testCase, string? expectedProgramString : removeTrailingNewlineRegex.Replace(programString, ""); var uri = new Uri("virtual:virtual"); - var outerModule = new DefaultModuleDefinition(new List() { uri }); + var outerModule = new DefaultModuleDefinition(new List() { uri }, false); BatchErrorReporter reporter = new BatchErrorReporter(options, outerModule); - var module = new LiteralModuleDecl(outerModule, null); Microsoft.Dafny.Type.ResetScopes(); - BuiltIns builtIns = new BuiltIns(options); - Parser.Parse(programNotIndented, uri, module, builtIns, reporter); - var dafnyProgram = new Program("programName", module, builtIns, reporter, Sets.Empty(), Sets.Empty()); + + var dafnyProgram = ParseUtils.Parse(programNotIndented, uri, reporter); if (reporter.ErrorCount > 0) { var error = reporter.AllMessages[ErrorLevel.Error][0]; @@ -95,14 +94,12 @@ protected void FormatterWorksFor(string testCase, string? expectedProgramString var initErrorCount = reporter.ErrorCount; // Verify that the formatting is stable. - module = new LiteralModuleDecl(new DefaultModuleDefinition(new List() { uri }), null); Microsoft.Dafny.Type.ResetScopes(); - builtIns = new BuiltIns(options); - Parser.Parse(reprinted, uri, module, builtIns, reporter); - dafnyProgram = new Program("programName", module, builtIns, reporter, Sets.Empty(), Sets.Empty()); + var newOuterModule = new DefaultModuleDefinition(new List() { uri }, false); + var newReporter = new BatchErrorReporter(options, newOuterModule); + dafnyProgram = ParseUtils.Parse(reprinted, uri, newReporter); ; - var newReporter = (BatchErrorReporter)dafnyProgram.Reporter; - Assert.Equal(initErrorCount, newReporter.ErrorCount); + Assert.Equal(initErrorCount, reporter.ErrorCount + newReporter.ErrorCount); firstToken = dafnyProgram.GetFirstTopLevelToken(); var reprinted2 = firstToken != null && firstToken.line > 0 ? Formatting.__default.ReindentProgramFromFirstToken(firstToken, diff --git a/Source/DafnyPipeline.Test/TranslatorTest.cs b/Source/DafnyPipeline.Test/TranslatorTest.cs index 6249374202b..19376b424e5 100644 --- a/Source/DafnyPipeline.Test/TranslatorTest.cs +++ b/Source/DafnyPipeline.Test/TranslatorTest.cs @@ -75,12 +75,9 @@ private void ShouldHaveImplicitCode(string program, string expected, DafnyOption Microsoft.Dafny.Type.ResetScopes(); options = options ?? new DafnyOptions(TextReader.Null, TextWriter.Null, TextWriter.Null); var uri = new Uri("virtual:///virtual"); - var defaultModuleDefinition = new DefaultModuleDefinition(new List() { uri }); - var module = new LiteralModuleDecl(defaultModuleDefinition, null); + var defaultModuleDefinition = new DefaultModuleDefinition(new List() { uri }, false); BatchErrorReporter reporter = new BatchErrorReporter(options, defaultModuleDefinition); - var builtIns = new BuiltIns(options); - var dafnyProgram = new Program("programName", module, builtIns, reporter, Sets.Empty(), Sets.Empty()); - Parser.Parse(program, uri, module, builtIns, reporter); + var dafnyProgram = ParseUtils.Parse(program, uri, reporter); if (reporter.ErrorCount > 0) { var error = reporter.AllMessages[ErrorLevel.Error][0]; Assert.False(true, $"{error.Message}: line {error.Token.line} col {error.Token.col}"); diff --git a/Source/DafnyPipeline.Test/Trivia.cs b/Source/DafnyPipeline.Test/Trivia.cs index 4decd97dd60..d85f8ac1db9 100644 --- a/Source/DafnyPipeline.Test/Trivia.cs +++ b/Source/DafnyPipeline.Test/Trivia.cs @@ -1,6 +1,7 @@ using System; using System.Collections.Generic; using System.IO; +using System.Linq; using System.Text.RegularExpressions; using DafnyTestGeneration; using Bpl = Microsoft.Boogie; @@ -80,13 +81,14 @@ ensures true var dafnyProgram = Utils.Parse(options, programString, false); var reporter = dafnyProgram.Reporter; Assert.Equal(0, reporter.ErrorCount); - Assert.Equal(6, dafnyProgram.DefaultModuleDef.TopLevelDecls.Count); - var moduleTest = dafnyProgram.DefaultModuleDef.TopLevelDecls[0] as LiteralModuleDecl; - var trait1 = dafnyProgram.DefaultModuleDef.TopLevelDecls[1]; - var trait2 = dafnyProgram.DefaultModuleDef.TopLevelDecls[2]; - var subsetType = dafnyProgram.DefaultModuleDef.TopLevelDecls[3]; - var class1 = dafnyProgram.DefaultModuleDef.TopLevelDecls[4] as ClassDecl; - var defaultClass = dafnyProgram.DefaultModuleDef.TopLevelDecls[5] as DefaultClassDecl; + var topLevelDecls = dafnyProgram.DefaultModuleDef.TopLevelDecls.ToList(); + Assert.Equal(6, topLevelDecls.Count()); + var moduleTest = topLevelDecls[0] as LiteralModuleDecl; + var trait1 = topLevelDecls[1]; + var trait2 = topLevelDecls[2]; + var subsetType = topLevelDecls[3]; + var class1 = topLevelDecls[4] as ClassDecl; + var defaultClass = topLevelDecls[5] as DefaultClassDecl; Assert.NotNull(moduleTest); Assert.NotNull(class1); Assert.NotNull(defaultClass); @@ -130,10 +132,8 @@ void Traverse(Node node) { Traverse(program); - var count = 0; void AreAllTokensOwned(Node node) { if (node.StartToken is { filename: { } }) { - count++; var t = node.StartToken; while (t != null && t != node.EndToken) { Assert.Contains(t, allTokens); @@ -147,7 +147,6 @@ void AreAllTokensOwned(Node node) { } AreAllTokensOwned(program); - Assert.Equal(9, count); // Sanity check } private string AdjustNewlines(string programString) { diff --git a/Source/DafnyRuntime/DafnyRuntimeGo/DafnyRuntimeFromDafny.go b/Source/DafnyRuntime/DafnyRuntimeGo/DafnyRuntimeFromDafny.go index ca1b7f77c50..793b842259b 100644 --- a/Source/DafnyRuntime/DafnyRuntimeGo/DafnyRuntimeFromDafny.go +++ b/Source/DafnyRuntime/DafnyRuntimeGo/DafnyRuntimeFromDafny.go @@ -299,176 +299,6 @@ func (CompanionStruct_Sequence_) CastTo_(x interface{}) Sequence { } // End of trait Sequence -// Definition of class Default__ -type Default__ struct { - dummy byte -} - -func New_Default___() *Default__ { - _this := Default__{} - - return &_this -} - -type CompanionStruct_Default___ struct { -} -var Companion_Default___ = CompanionStruct_Default___ { -} - -func (_this *Default__) Equals(other *Default__) bool { - return _this == other -} - -func (_this *Default__) EqualsGeneric(x interface{}) bool { - other, ok := x.(*Default__) - return ok && _this.Equals(other) -} - -func (*Default__) String() string { - return "dafny.Default__" -} -func (_this *Default__) ParentTraits_() []*TraitID { - return [](*TraitID){}; -} -var _ TraitOffspring = &Default__{} -func (_static *CompanionStruct_Default___) SizeAdditionInRange(a uint32, b uint32) bool { - var _hresult bool = false - _ = _hresult - _hresult = (a) <= ((Companion_Default___.SIZE__T__MAX()) - (func () uint32 { return (b) })()) - return _hresult - return _hresult -} -func (_static *CompanionStruct_Default___) AppendRecursive(builder *Vector, e Sequence) { - if (func (_is_2 Sequence) bool { - return InstanceOf(_is_2, (*ConcatSequence)(nil)) - }(e)) { - var _18_concat *ConcatSequence - _ = _18_concat - _18_concat = e.(*ConcatSequence) - Companion_Default___.AppendRecursive(builder, (_18_concat).Left()) - Companion_Default___.AppendRecursive(builder, (_18_concat).Right()) - } else if (func (_is_3 Sequence) bool { - return InstanceOf(_is_3, (*LazySequence)(nil)) - }(e)) { - var _19_lazy *LazySequence - _ = _19_lazy - _19_lazy = e.(*LazySequence) - var _20_boxed Sequence - _ = _20_boxed - var _out18 interface{} - _ = _out18 - _out18 = ((_19_lazy).Box()).Get() - _20_boxed = Companion_Sequence_.CastTo_(_out18) - Companion_Default___.AppendRecursive(builder, _20_boxed) - } else { - var _21_a ImmutableArray - _ = _21_a - var _out19 ImmutableArray - _ = _out19 - _out19 = (e).ToArray() - _21_a = _out19 - (builder).Append(_21_a) - } -} -func (_static *CompanionStruct_Default___) AppendOptimized(builder *Vector, e Sequence, stack *Vector) { - goto TAIL_CALL_START - TAIL_CALL_START: - if (func (_is_4 Sequence) bool { - return InstanceOf(_is_4, (*ConcatSequence)(nil)) - }(e)) { - var _22_concat *ConcatSequence - _ = _22_concat - _22_concat = e.(*ConcatSequence) - if (!(Companion_Default___.SizeAdditionInRange(stack.Size, Companion_Default___.ONE__SIZE()))) { - panic("dafnyRuntime.dfy[DafnyGo](747,6): " + (SeqOfString("expectation violation")).String()) - } - (stack).AddLast((_22_concat).Right()) - var _in0 *Vector = builder - _ = _in0 - var _in1 Sequence = (_22_concat).Left() - _ = _in1 - var _in2 *Vector = stack - _ = _in2 - builder = _in0 - e = _in1 - stack = _in2 - goto TAIL_CALL_START - } else if (func (_is_5 Sequence) bool { - return InstanceOf(_is_5, (*LazySequence)(nil)) - }(e)) { - var _23_lazy *LazySequence - _ = _23_lazy - _23_lazy = e.(*LazySequence) - var _24_boxed Sequence - _ = _24_boxed - var _out20 interface{} - _ = _out20 - _out20 = ((_23_lazy).Box()).Get() - _24_boxed = Companion_Sequence_.CastTo_(_out20) - var _in3 *Vector = builder - _ = _in3 - var _in4 Sequence = _24_boxed - _ = _in4 - var _in5 *Vector = stack - _ = _in5 - builder = _in3 - e = _in4 - stack = _in5 - goto TAIL_CALL_START - } else if (func (_is_6 Sequence) bool { - return InstanceOf(_is_6, (*ArraySequence)(nil)) - }(e)) { - var _25_a *ArraySequence - _ = _25_a - _25_a = e.(*ArraySequence) - (builder).Append((_25_a).Values()) - if ((uint32(0)) < (stack.Size)) { - var _26_next Sequence - _ = _26_next - var _out21 interface{} - _ = _out21 - _out21 = (stack).RemoveLast() - _26_next = Companion_Sequence_.CastTo_(_out21) - var _in6 *Vector = builder - _ = _in6 - var _in7 Sequence = _26_next - _ = _in7 - var _in8 *Vector = stack - _ = _in8 - builder = _in6 - e = _in7 - stack = _in8 - goto TAIL_CALL_START - } - } else { - if (!(false)) { - panic("dafnyRuntime.dfy[DafnyGo](765,6): " + (SeqOfString("Unsupported Sequence implementation")).String()) - } - } -} -func (_static *CompanionStruct_Default___) SIZE__T__LIMIT() Int { - return IntOfInt64(2147483648) -} -func (_static *CompanionStruct_Default___) MIN__SIZE__T__LIMIT() Int { - return IntOfInt64(128) -} -func (_static *CompanionStruct_Default___) TEN__SIZE() uint32 { - return uint32(10) -} -func (_static *CompanionStruct_Default___) ONE__SIZE() uint32 { - return uint32(1) -} -func (_static *CompanionStruct_Default___) SIZE__T__MAX() uint32 { - return ((Companion_Default___.SIZE__T__LIMIT()).Minus(One)).Uint32() -} -func (_static *CompanionStruct_Default___) TWO__SIZE() uint32 { - return uint32(2) -} -func (_static *CompanionStruct_Default___) ZERO__SIZE() uint32 { - return uint32(0) -} -// End of class Default__ - // Definition of trait Validatable type Validatable interface { String() string @@ -735,13 +565,13 @@ var _ Validatable = &Vector{} var _ TraitOffspring = &Vector{} func (_this *Vector) Ctor__(length uint32) { { - var _27_storage NativeArray - _ = _27_storage - var _out22 NativeArray - _ = _out22 - _out22 = Companion_NativeArray_.Make(length) - _27_storage = _out22 - (_this).Storage = _27_storage + var _18_storage NativeArray + _ = _18_storage + var _out18 NativeArray + _ = _out18 + _out18 = Companion_NativeArray_.Make(length) + _18_storage = _out18 + (_this).Storage = _18_storage (_this).Size = uint32(0) } } @@ -776,26 +606,26 @@ func (_this *Vector) EnsureCapacity(newMinCapacity uint32) { if (((_this.Storage).Length()) >= (newMinCapacity)) { return } - var _28_newCapacity uint32 - _ = _28_newCapacity - _28_newCapacity = newMinCapacity + var _19_newCapacity uint32 + _ = _19_newCapacity + _19_newCapacity = newMinCapacity if (((_this.Storage).Length()) <= ((Companion_Default___.SIZE__T__MAX()) / (Companion_Default___.TWO__SIZE()))) { - _28_newCapacity = (_this).Max(_28_newCapacity, ((_this.Storage).Length()) * (Companion_Default___.TWO__SIZE())) + _19_newCapacity = (_this).Max(_19_newCapacity, ((_this.Storage).Length()) * (Companion_Default___.TWO__SIZE())) } - var _29_newStorage NativeArray - _ = _29_newStorage - var _out23 NativeArray - _ = _out23 - _out23 = Companion_NativeArray_.Make(_28_newCapacity) - _29_newStorage = _out23 - var _30_values ImmutableArray - _ = _30_values - var _out24 ImmutableArray - _ = _out24 - _out24 = (_this.Storage).Freeze(_this.Size) - _30_values = _out24 - (_29_newStorage).UpdateSubarray(uint32(0), _30_values) - (_this).Storage = _29_newStorage + var _20_newStorage NativeArray + _ = _20_newStorage + var _out19 NativeArray + _ = _out19 + _out19 = Companion_NativeArray_.Make(_19_newCapacity) + _20_newStorage = _out19 + var _21_values ImmutableArray + _ = _21_values + var _out20 ImmutableArray + _ = _out20 + _out20 = (_this.Storage).Freeze(_this.Size) + _21_values = _out20 + (_20_newStorage).UpdateSubarray(uint32(0), _21_values) + (_this).Storage = _20_newStorage } } func (_this *Vector) RemoveLast() interface{} { @@ -809,10 +639,10 @@ func (_this *Vector) RemoveLast() interface{} { } func (_this *Vector) Append(other ImmutableArray) { { - var _31_newSize uint32 - _ = _31_newSize - _31_newSize = (_this.Size) + ((other).Length()) - (_this).EnsureCapacity(_31_newSize) + var _22_newSize uint32 + _ = _22_newSize + _22_newSize = (_this.Size) + ((other).Length()) + (_this).EnsureCapacity(_22_newSize) (_this.Storage).UpdateSubarray(_this.Size, other) (_this).Size = (_this.Size) + ((other).Length()) } @@ -821,10 +651,10 @@ func (_this *Vector) Freeze() ImmutableArray { { var ret ImmutableArray = (ImmutableArray)(nil) _ = ret - var _out25 ImmutableArray - _ = _out25 - _out25 = (_this.Storage).Freeze(_this.Size) - ret = _out25 + var _out21 ImmutableArray + _ = _out21 + _out21 = (_this.Storage).Freeze(_this.Size) + ret = _out21 return ret } } @@ -890,10 +720,10 @@ func (_this *ArraySequence) ParentTraits_() []*TraitID { var _ Sequence = &ArraySequence{} var _ TraitOffspring = &ArraySequence{} func (_this *ArraySequence) SetString() Sequence { - var _out26 Sequence - _ = _out26 - _out26 = Companion_Sequence_.SetString(_this) - return _out26 + var _out22 Sequence + _ = _out22 + _out22 = Companion_Sequence_.SetString(_this) + return _out22 } func (_this *ArraySequence) IsString() bool { return _this._isString @@ -902,28 +732,28 @@ func (_this *ArraySequence) IsString_set_(value bool) { _this._isString = value } func (_this *ArraySequence) Select(index uint32) interface{} { - var _out27 interface{} - _ = _out27 - _out27 = Companion_Sequence_.Select(_this, index) - return _out27 + var _out23 interface{} + _ = _out23 + _out23 = Companion_Sequence_.Select(_this, index) + return _out23 } func (_this *ArraySequence) Drop(lo uint32) Sequence { - var _out28 Sequence - _ = _out28 - _out28 = Companion_Sequence_.Drop(_this, lo) - return _out28 + var _out24 Sequence + _ = _out24 + _out24 = Companion_Sequence_.Drop(_this, lo) + return _out24 } func (_this *ArraySequence) Take(hi uint32) Sequence { - var _out29 Sequence - _ = _out29 - _out29 = Companion_Sequence_.Take(_this, hi) - return _out29 + var _out25 Sequence + _ = _out25 + _out25 = Companion_Sequence_.Take(_this, hi) + return _out25 } func (_this *ArraySequence) Subsequence(lo uint32, hi uint32) Sequence { - var _out30 Sequence - _ = _out30 - _out30 = Companion_Sequence_.Subsequence(_this, lo, hi) - return _out30 + var _out26 Sequence + _ = _out26 + _out26 = Companion_Sequence_.Subsequence(_this, lo, hi) + return _out26 } func (_this *ArraySequence) Elements() Sequence { return Companion_Sequence_.Elements(_this) @@ -1000,10 +830,10 @@ func (_this *ConcatSequence) ParentTraits_() []*TraitID { var _ Sequence = &ConcatSequence{} var _ TraitOffspring = &ConcatSequence{} func (_this *ConcatSequence) SetString() Sequence { - var _out31 Sequence - _ = _out31 - _out31 = Companion_Sequence_.SetString(_this) - return _out31 + var _out27 Sequence + _ = _out27 + _out27 = Companion_Sequence_.SetString(_this) + return _out27 } func (_this *ConcatSequence) IsString() bool { return _this._isString @@ -1012,28 +842,28 @@ func (_this *ConcatSequence) IsString_set_(value bool) { _this._isString = value } func (_this *ConcatSequence) Select(index uint32) interface{} { - var _out32 interface{} - _ = _out32 - _out32 = Companion_Sequence_.Select(_this, index) - return _out32 + var _out28 interface{} + _ = _out28 + _out28 = Companion_Sequence_.Select(_this, index) + return _out28 } func (_this *ConcatSequence) Drop(lo uint32) Sequence { - var _out33 Sequence - _ = _out33 - _out33 = Companion_Sequence_.Drop(_this, lo) - return _out33 + var _out29 Sequence + _ = _out29 + _out29 = Companion_Sequence_.Drop(_this, lo) + return _out29 } func (_this *ConcatSequence) Take(hi uint32) Sequence { - var _out34 Sequence - _ = _out34 - _out34 = Companion_Sequence_.Take(_this, hi) - return _out34 + var _out30 Sequence + _ = _out30 + _out30 = Companion_Sequence_.Take(_this, hi) + return _out30 } func (_this *ConcatSequence) Subsequence(lo uint32, hi uint32) Sequence { - var _out35 Sequence - _ = _out35 - _out35 = Companion_Sequence_.Subsequence(_this, lo, hi) - return _out35 + var _out31 Sequence + _ = _out31 + _out31 = Companion_Sequence_.Subsequence(_this, lo, hi) + return _out31 } func (_this *ConcatSequence) Elements() Sequence { return Companion_Sequence_.Elements(_this) @@ -1055,23 +885,23 @@ func (_this *ConcatSequence) ToArray() ImmutableArray { { var ret ImmutableArray = (ImmutableArray)(nil) _ = ret - var _32_builder *Vector - _ = _32_builder + var _23_builder *Vector + _ = _23_builder var _nw5 *Vector = New_Vector_() _ = _nw5 _nw5.Ctor__((_this).Length()) - _32_builder = _nw5 - var _33_stack *Vector - _ = _33_stack + _23_builder = _nw5 + var _24_stack *Vector + _ = _24_stack var _nw6 *Vector = New_Vector_() _ = _nw6 _nw6.Ctor__(Companion_Default___.TEN__SIZE()) - _33_stack = _nw6 - Companion_Default___.AppendOptimized(_32_builder, _this, _33_stack) - var _out36 ImmutableArray - _ = _out36 - _out36 = (_32_builder).Freeze() - ret = _out36 + _24_stack = _nw6 + Companion_Default___.AppendOptimized(_23_builder, _this, _24_stack) + var _out32 ImmutableArray + _ = _out32 + _out32 = (_23_builder).Freeze() + ret = _out32 return ret } } @@ -1135,10 +965,10 @@ func (_this *LazySequence) ParentTraits_() []*TraitID { var _ Sequence = &LazySequence{} var _ TraitOffspring = &LazySequence{} func (_this *LazySequence) SetString() Sequence { - var _out37 Sequence - _ = _out37 - _out37 = Companion_Sequence_.SetString(_this) - return _out37 + var _out33 Sequence + _ = _out33 + _out33 = Companion_Sequence_.SetString(_this) + return _out33 } func (_this *LazySequence) IsString() bool { return _this._isString @@ -1147,41 +977,41 @@ func (_this *LazySequence) IsString_set_(value bool) { _this._isString = value } func (_this *LazySequence) Select(index uint32) interface{} { - var _out38 interface{} - _ = _out38 - _out38 = Companion_Sequence_.Select(_this, index) - return _out38 + var _out34 interface{} + _ = _out34 + _out34 = Companion_Sequence_.Select(_this, index) + return _out34 } func (_this *LazySequence) Drop(lo uint32) Sequence { - var _out39 Sequence - _ = _out39 - _out39 = Companion_Sequence_.Drop(_this, lo) - return _out39 + var _out35 Sequence + _ = _out35 + _out35 = Companion_Sequence_.Drop(_this, lo) + return _out35 } func (_this *LazySequence) Take(hi uint32) Sequence { - var _out40 Sequence - _ = _out40 - _out40 = Companion_Sequence_.Take(_this, hi) - return _out40 + var _out36 Sequence + _ = _out36 + _out36 = Companion_Sequence_.Take(_this, hi) + return _out36 } func (_this *LazySequence) Subsequence(lo uint32, hi uint32) Sequence { - var _out41 Sequence - _ = _out41 - _out41 = Companion_Sequence_.Subsequence(_this, lo, hi) - return _out41 + var _out37 Sequence + _ = _out37 + _out37 = Companion_Sequence_.Subsequence(_this, lo, hi) + return _out37 } func (_this *LazySequence) Elements() Sequence { return Companion_Sequence_.Elements(_this) } func (_this *LazySequence) Ctor__(wrapped Sequence) { { - var _34_box AtomicBox - _ = _34_box - var _out42 AtomicBox - _ = _out42 - _out42 = Companion_AtomicBox_.Make(wrapped) - _34_box = _out42 - (_this)._box = _34_box + var _25_box AtomicBox + _ = _25_box + var _out38 AtomicBox + _ = _out38 + _out38 = Companion_AtomicBox_.Make(wrapped) + _25_box = _out38 + (_this)._box = _25_box (_this)._length = (wrapped).Cardinality() (_this)._isString = wrapped.IsString() } @@ -1195,23 +1025,23 @@ func (_this *LazySequence) ToArray() ImmutableArray { { var ret ImmutableArray = (ImmutableArray)(nil) _ = ret - var _35_expr Sequence - _ = _35_expr - var _out43 interface{} - _ = _out43 - _out43 = ((_this).Box()).Get() - _35_expr = Companion_Sequence_.CastTo_(_out43) - var _out44 ImmutableArray - _ = _out44 - _out44 = (_35_expr).ToArray() - ret = _out44 - var _36_arraySeq *ArraySequence - _ = _36_arraySeq + var _26_expr Sequence + _ = _26_expr + var _out39 interface{} + _ = _out39 + _out39 = ((_this).Box()).Get() + _26_expr = Companion_Sequence_.CastTo_(_out39) + var _out40 ImmutableArray + _ = _out40 + _out40 = (_26_expr).ToArray() + ret = _out40 + var _27_arraySeq *ArraySequence + _ = _27_arraySeq var _nw7 *ArraySequence = New_ArraySequence_() _ = _nw7 _nw7.Ctor__(ret, false) - _36_arraySeq = _nw7 - ((_this).Box()).Put(_36_arraySeq) + _27_arraySeq = _nw7 + ((_this).Box()).Put(_27_arraySeq) return ret } } @@ -1243,3 +1073,173 @@ func (CompanionStruct_Helpers_) CastTo_(x interface{}) Helpers { return t } // End of trait Helpers + +// Definition of class Default__ +type Default__ struct { + dummy byte +} + +func New_Default___() *Default__ { + _this := Default__{} + + return &_this +} + +type CompanionStruct_Default___ struct { +} +var Companion_Default___ = CompanionStruct_Default___ { +} + +func (_this *Default__) Equals(other *Default__) bool { + return _this == other +} + +func (_this *Default__) EqualsGeneric(x interface{}) bool { + other, ok := x.(*Default__) + return ok && _this.Equals(other) +} + +func (*Default__) String() string { + return "dafny.Default__" +} +func (_this *Default__) ParentTraits_() []*TraitID { + return [](*TraitID){}; +} +var _ TraitOffspring = &Default__{} +func (_static *CompanionStruct_Default___) SizeAdditionInRange(a uint32, b uint32) bool { + var _hresult bool = false + _ = _hresult + _hresult = (a) <= ((Companion_Default___.SIZE__T__MAX()) - (func () uint32 { return (b) })()) + return _hresult + return _hresult +} +func (_static *CompanionStruct_Default___) AppendRecursive(builder *Vector, e Sequence) { + if (func (_is_2 Sequence) bool { + return InstanceOf(_is_2, (*ConcatSequence)(nil)) + }(e)) { + var _28_concat *ConcatSequence + _ = _28_concat + _28_concat = e.(*ConcatSequence) + Companion_Default___.AppendRecursive(builder, (_28_concat).Left()) + Companion_Default___.AppendRecursive(builder, (_28_concat).Right()) + } else if (func (_is_3 Sequence) bool { + return InstanceOf(_is_3, (*LazySequence)(nil)) + }(e)) { + var _29_lazy *LazySequence + _ = _29_lazy + _29_lazy = e.(*LazySequence) + var _30_boxed Sequence + _ = _30_boxed + var _out41 interface{} + _ = _out41 + _out41 = ((_29_lazy).Box()).Get() + _30_boxed = Companion_Sequence_.CastTo_(_out41) + Companion_Default___.AppendRecursive(builder, _30_boxed) + } else { + var _31_a ImmutableArray + _ = _31_a + var _out42 ImmutableArray + _ = _out42 + _out42 = (e).ToArray() + _31_a = _out42 + (builder).Append(_31_a) + } +} +func (_static *CompanionStruct_Default___) AppendOptimized(builder *Vector, e Sequence, stack *Vector) { + goto TAIL_CALL_START + TAIL_CALL_START: + if (func (_is_4 Sequence) bool { + return InstanceOf(_is_4, (*ConcatSequence)(nil)) + }(e)) { + var _32_concat *ConcatSequence + _ = _32_concat + _32_concat = e.(*ConcatSequence) + if (!(Companion_Default___.SizeAdditionInRange(stack.Size, Companion_Default___.ONE__SIZE()))) { + panic("dafnyRuntime.dfy[DafnyGo](747,6): " + (SeqOfString("expectation violation")).String()) + } + (stack).AddLast((_32_concat).Right()) + var _in0 *Vector = builder + _ = _in0 + var _in1 Sequence = (_32_concat).Left() + _ = _in1 + var _in2 *Vector = stack + _ = _in2 + builder = _in0 + e = _in1 + stack = _in2 + goto TAIL_CALL_START + } else if (func (_is_5 Sequence) bool { + return InstanceOf(_is_5, (*LazySequence)(nil)) + }(e)) { + var _33_lazy *LazySequence + _ = _33_lazy + _33_lazy = e.(*LazySequence) + var _34_boxed Sequence + _ = _34_boxed + var _out43 interface{} + _ = _out43 + _out43 = ((_33_lazy).Box()).Get() + _34_boxed = Companion_Sequence_.CastTo_(_out43) + var _in3 *Vector = builder + _ = _in3 + var _in4 Sequence = _34_boxed + _ = _in4 + var _in5 *Vector = stack + _ = _in5 + builder = _in3 + e = _in4 + stack = _in5 + goto TAIL_CALL_START + } else if (func (_is_6 Sequence) bool { + return InstanceOf(_is_6, (*ArraySequence)(nil)) + }(e)) { + var _35_a *ArraySequence + _ = _35_a + _35_a = e.(*ArraySequence) + (builder).Append((_35_a).Values()) + if ((uint32(0)) < (stack.Size)) { + var _36_next Sequence + _ = _36_next + var _out44 interface{} + _ = _out44 + _out44 = (stack).RemoveLast() + _36_next = Companion_Sequence_.CastTo_(_out44) + var _in6 *Vector = builder + _ = _in6 + var _in7 Sequence = _36_next + _ = _in7 + var _in8 *Vector = stack + _ = _in8 + builder = _in6 + e = _in7 + stack = _in8 + goto TAIL_CALL_START + } + } else { + if (!(false)) { + panic("dafnyRuntime.dfy[DafnyGo](765,6): " + (SeqOfString("Unsupported Sequence implementation")).String()) + } + } +} +func (_static *CompanionStruct_Default___) SIZE__T__LIMIT() Int { + return IntOfInt64(2147483648) +} +func (_static *CompanionStruct_Default___) MIN__SIZE__T__LIMIT() Int { + return IntOfInt64(128) +} +func (_static *CompanionStruct_Default___) TEN__SIZE() uint32 { + return uint32(10) +} +func (_static *CompanionStruct_Default___) ONE__SIZE() uint32 { + return uint32(1) +} +func (_static *CompanionStruct_Default___) SIZE__T__MAX() uint32 { + return ((Companion_Default___.SIZE__T__LIMIT()).Minus(One)).Uint32() +} +func (_static *CompanionStruct_Default___) TWO__SIZE() uint32 { + return uint32(2) +} +func (_static *CompanionStruct_Default___) ZERO__SIZE() uint32 { + return uint32(0) +} +// End of class Default__ diff --git a/Source/DafnyServer/DafnyHelper.cs b/Source/DafnyServer/DafnyHelper.cs index d4e6c4313ae..8ca6c8375b9 100644 --- a/Source/DafnyServer/DafnyHelper.cs +++ b/Source/DafnyServer/DafnyHelper.cs @@ -7,6 +7,7 @@ using System.Linq; using System.Runtime.Serialization.Json; using System.Text; +using System.Threading; using Microsoft.Boogie; using DafnyServer; using Bpl = Microsoft.Boogie; @@ -40,14 +41,14 @@ public bool Verify() { private bool Parse() { var uri = new Uri("transcript:///" + fname); - var defaultModuleDefinition = new DefaultModuleDefinition(new List() { uri }); - var module = new LiteralModuleDecl(defaultModuleDefinition, null); + var defaultModuleDefinition = new DefaultModuleDefinition(new List() { uri }, false); reporter = new ConsoleErrorReporter(options, defaultModuleDefinition); - BuiltIns builtIns = new BuiltIns(options); - var success = (Parser.Parse(source, uri, module, builtIns, new Errors(reporter)) == 0 && - DafnyMain.ParseIncludes(module, builtIns, new HashSet(), new Errors(reporter)) == null); + var program = ParseUtils.ParseFiles(fname, new DafnyFile[] { new(reporter.Options, uri, new StringReader(source)) }, + reporter, CancellationToken.None); + + var success = reporter.ErrorCount == 0; if (success) { - dafnyProgram = new Program(fname, module, builtIns, reporter, Sets.Empty(), Sets.Empty()); + dafnyProgram = program; } return success; } @@ -60,7 +61,7 @@ private bool Resolve() { private bool Translate() { boogiePrograms = Translator.Translate(dafnyProgram, reporter, - new Translator.TranslatorFlags(options) { InsertChecksums = true, UniqueIdPrefix = fname }); // FIXME how are translation errors reported? + new Translator.TranslatorFlags(options) { InsertChecksums = true, UniqueIdPrefix = fname }).ToList(); // FIXME how are translation errors reported? return true; } diff --git a/Source/DafnyServer/SignatureAndCompletionTable.cs b/Source/DafnyServer/SignatureAndCompletionTable.cs index b4d163853fe..47fe9137250 100644 --- a/Source/DafnyServer/SignatureAndCompletionTable.cs +++ b/Source/DafnyServer/SignatureAndCompletionTable.cs @@ -107,7 +107,7 @@ private void AddFields(ModuleDefinition module, List informat } private void AddClasses(ModuleDefinition module, List information) { - foreach (var cs in ModuleDefinition.AllClasses(module.TopLevelDecls). + foreach (var cs in module.TopLevelDecls.Where(t => t is ClassLikeDecl or DefaultClassDecl). Where(cl => !cl.Tok.FromIncludeDirective(_dafnyProgram))) { if (cs.EnclosingModuleDefinition != null && cs.tok != null) { var classSymbol = new SymbolInformation { diff --git a/Source/DafnyTestGeneration/DafnyInfo.cs b/Source/DafnyTestGeneration/DafnyInfo.cs index 895f2460c09..d401e807be0 100644 --- a/Source/DafnyTestGeneration/DafnyInfo.cs +++ b/Source/DafnyTestGeneration/DafnyInfo.cs @@ -484,7 +484,10 @@ private void Visit(LiteralModuleDecl d) { } else if (d.FullDafnyName != "") { info.ToImportAs[d.FullDafnyName] = d.Name; } - d.ModuleDef.TopLevelDecls.ForEach(Visit); + + foreach (var topLevelDecl in d.ModuleDef.TopLevelDecls) { + Visit(topLevelDecl); + } } private void Visit(IndDatatypeDecl d) { diff --git a/Source/DafnyTestGeneration/Utils.cs b/Source/DafnyTestGeneration/Utils.cs index 479a862c0a0..7ec8ddc2e9a 100644 --- a/Source/DafnyTestGeneration/Utils.cs +++ b/Source/DafnyTestGeneration/Utils.cs @@ -3,6 +3,7 @@ using System.Collections.Generic; using System.IO; using System.Linq; +using System.Threading; using DafnyServer.CounterexampleGeneration; using Microsoft.Boogie; using Microsoft.Dafny; @@ -77,14 +78,11 @@ public static Type CopyWithReplacements(Type type, List from, List /// public static Program/*?*/ Parse(DafnyOptions options, string source, bool resolve = true, Uri uri = null) { uri ??= new Uri(Path.GetTempPath()); - var defaultModuleDefinition = new DefaultModuleDefinition(new List() { uri }); - var module = new LiteralModuleDecl(defaultModuleDefinition, null); - var builtIns = new BuiltIns(options); + var defaultModuleDefinition = new DefaultModuleDefinition(new List() { uri }, false); var reporter = new BatchErrorReporter(options, defaultModuleDefinition); - var success = Parser.Parse(source, uri, module, builtIns, - new Errors(reporter)) == 0 && DafnyMain.ParseIncludes(module, builtIns, - new HashSet(), new Errors(reporter)) == null; - var program = new Program(uri.LocalPath, module, builtIns, reporter, Sets.Empty(), Sets.Empty()); + + var program = ParseUtils.ParseFiles(uri.LocalPath, new DafnyFile[] { new(reporter.Options, uri, new StringReader(source)) }, + reporter, CancellationToken.None); if (!resolve) { return program; @@ -141,7 +139,9 @@ internal void PreResolve(Program program) { private static void AddByMethod(TopLevelDecl d) { if (d is LiteralModuleDecl moduleDecl) { - moduleDecl.ModuleDef.TopLevelDecls.ForEach(AddByMethod); + foreach (var topLevelDecl in moduleDecl.ModuleDef.TopLevelDecls) { + AddByMethod(topLevelDecl); + } } else if (d is TopLevelDeclWithMembers withMembers) { withMembers.Members.OfType().Iter(AddByMethod); } diff --git a/Source/IntegrationTests/LitTests.cs b/Source/IntegrationTests/LitTests.cs index 6390b9fb5c2..ace67f5c8d0 100644 --- a/Source/IntegrationTests/LitTests.cs +++ b/Source/IntegrationTests/LitTests.cs @@ -90,11 +90,8 @@ IEnumerable AddExtraArgs(IEnumerable args, IEnumerable l "%testDafnyForEachCompiler", (args, config) => MainMethodLitCommand.Parse(TestDafnyAssembly, new []{ "for-each-compiler" }.Concat(args), config, InvokeMainMethodsDirectly) }, { - "%server", (args, config) => // TODO - { - var shellArguments = new[] { DafnyServerAssembly.Location }.Concat(args); - return new ShellLitCommand("dotnet", shellArguments, config.PassthroughEnvironmentVariables); - } + "%server", (args, config) => + MainMethodLitCommand.Parse(DafnyServerAssembly, args, config, InvokeMainMethodsDirectly) }, { "%boogie", (args, config) => // TODO new DotnetToolCommand("boogie", diff --git a/Test/allocated1/dafny0/Definedness.dfy b/Test/allocated1/dafny0/Definedness.dfy index 99c994c14b2..a8450756d4e 100644 --- a/Test/allocated1/dafny0/Definedness.dfy +++ b/Test/allocated1/dafny0/Definedness.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 4 %dafny /verifyAllModules /allocated:1 /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %exits-with 4 %dafny /allocated:1 /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" // RUN: %diff "%s.expect" "%t" // ----------------- wellformed specifications ---------------------- diff --git a/Test/allocated1/dafny0/DirtyLoops.dfy b/Test/allocated1/dafny0/DirtyLoops.dfy index f8a1063e2c0..44987813a8c 100644 --- a/Test/allocated1/dafny0/DirtyLoops.dfy +++ b/Test/allocated1/dafny0/DirtyLoops.dfy @@ -1,4 +1,4 @@ // RUN: %exits-with 4 %dafny /verifyAllModules /allocated:1 /compile:0 /dprint:"%t.dprint.dfy" "%s" > "%t" -// RUN: %exits-with 0 %dafny /verifyAllModules /allocated:1 /noVerify "%t.dprint.dfy" >> "%t" +// RUN: %exits-with 0 %dafny /allocated:1 /noVerify "%t.dprint.dfy" >> "%t" // RUN: %diff "%s.expect" "%t" include "../../dafny0/DirtyLoops.dfy" diff --git a/Test/allocated1/dafny0/LetExpr.dfy b/Test/allocated1/dafny0/LetExpr.dfy index a478d95f15c..bd7f568f749 100644 --- a/Test/allocated1/dafny0/LetExpr.dfy +++ b/Test/allocated1/dafny0/LetExpr.dfy @@ -1,4 +1,4 @@ // RUN: %exits-with 4 %dafny /verifyAllModules /allocated:1 /compile:0 /print:"%t.print" /dprint:"%t.dprint.dfy" "%s" > "%t" -// RUN: %dafny /verifyAllModules /allocated:1 /noVerify /compile:0 "%t.dprint.dfy" >> "%t" +// RUN: %dafny /allocated:1 /noVerify /compile:0 "%t.dprint.dfy" >> "%t" // RUN: %diff "%s.expect" "%t" include "../../dafny0/LetExpr.dfy" diff --git a/Test/allocated1/dafny0/Parallel.dfy b/Test/allocated1/dafny0/Parallel.dfy index 6457b7aab34..5f48294b555 100644 --- a/Test/allocated1/dafny0/Parallel.dfy +++ b/Test/allocated1/dafny0/Parallel.dfy @@ -1,5 +1,5 @@ // UNSUPPORTED: windows -// RUN: %exits-with 4 %dafny /verifyAllModules /allocated:1 /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" +// RUN: %exits-with 4 %dafny /allocated:1 /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" class C { var data: int diff --git a/Test/allocated1/dafny0/Reads.dfy b/Test/allocated1/dafny0/Reads.dfy index f08fe274068..550c7e54411 100644 --- a/Test/allocated1/dafny0/Reads.dfy +++ b/Test/allocated1/dafny0/Reads.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 4 %dafny /verifyAllModules /allocated:1 /compile:0 "%s" > "%t" +// RUN: %exits-with 4 %dafny /allocated:1 /compile:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" // Checking that the reads clause also is checked over requires diff --git a/Test/allocated1/dafny0/SmallTests.dfy b/Test/allocated1/dafny0/SmallTests.dfy index 7c49d74205e..0169ef40a47 100644 --- a/Test/allocated1/dafny0/SmallTests.dfy +++ b/Test/allocated1/dafny0/SmallTests.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 4 %dafny /verifyAllModules /allocated:1 /compile:0 /print:"%t.print" /dprint:"%t.dprint.dfy" "%s" > "%t" +// RUN: %exits-with 4 %dafny /allocated:1 /compile:0 /print:"%t.print" /dprint:"%t.dprint.dfy" "%s" > "%t" // RUN: %dafny /verifyAllModules /allocated:1 /noVerify /compile:0 "%t.dprint.dfy" >> "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Test/allocated1/dafny0/Twostate-Verification.dfy b/Test/allocated1/dafny0/Twostate-Verification.dfy index 2b1344e3391..8234188cc59 100644 --- a/Test/allocated1/dafny0/Twostate-Verification.dfy +++ b/Test/allocated1/dafny0/Twostate-Verification.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 4 %dafny /verifyAllModules /allocated:1 /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %exits-with 4 %dafny /allocated:1 /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" // RUN: %diff "%s.expect" "%t" method Main() { diff --git a/Test/git-issues/git-issue-3451/git-issue-3451a.dfy.expect b/Test/git-issues/git-issue-3451/git-issue-3451a.dfy.expect index 813b6fa066a..847b628e43e 100644 --- a/Test/git-issues/git-issue-3451/git-issue-3451a.dfy.expect +++ b/Test/git-issues/git-issue-3451/git-issue-3451a.dfy.expect @@ -1,3 +1,3 @@ -git-issue-3451a.dfy(1,0): Warning: File contains no code git-issue-3451a.dfy(5,0): Error: this symbol not expected in Dafny +git-issue-3451a.dfy(1,0): Warning: File contains no code 1 parse errors detected in git-issue-3451a.dfy diff --git a/Test/git-issues/git-issue-3757a.dfy.expect b/Test/git-issues/git-issue-3757a.dfy.expect index 074e8ca0638..b2ffcad38e9 100644 --- a/Test/git-issues/git-issue-3757a.dfy.expect +++ b/Test/git-issues/git-issue-3757a.dfy.expect @@ -1,4 +1,4 @@ git-issue-3757a.dfy(4,6): Error: expected an identifier after 'const' and any attributes -git-issue-3757a.dfy(1,0): Warning: File contains no code git-issue-3757a.dfy(4,6): Error: this symbol not expected in Dafny +git-issue-3757a.dfy(1,0): Warning: File contains no code 2 parse errors detected in git-issue-3757a.dfy diff --git a/Test/separate-verification/assumptions.dfy.expect b/Test/separate-verification/assumptions.dfy.expect index 467bc9cc08a..85c5c7955bc 100644 --- a/Test/separate-verification/assumptions.dfy.expect +++ b/Test/separate-verification/assumptions.dfy.expect @@ -9,6 +9,7 @@ TestAuditor.dfy(126,2): Warning: /!\ No terms found to trigger on. Dafny program verifier did not attempt verification assumptions.dfy(6,8): Error: the included file TestAuditor.dfy contains error(s) +TestAuditor.dfy(89,27): Error: Trait method calls may not terminate (uses [{:termination false}]). TestAuditor.dfy(22,6): Error: Ghost declaration has no body and has an ensures clause. TestAuditor.dfy(27,15): Error: Ghost declaration has no body and has an ensures clause. TestAuditor.dfy(45,17): Error: Declaration with [{:extern}] has a ensures clause. @@ -29,5 +30,4 @@ TestAuditor.dfy(130,2): Error: Definition contains loop with no body. TestAuditor.dfy(137,2): Error: Assertion has explicit temporary [{:only}] attribute. TestAuditor.dfy(11,8): Error: the included file IgnoredAssumptions.dfy contains error(s) IgnoredAssumptions.dfy(2,15): Error: Ghost declaration has no body and has an ensures clause. -TestAuditor.dfy(89,27): Error: Trait method calls may not terminate (uses [{:termination false}]). Wrote textual form of partial target program to assumptions-lib/assumptions.doo