Skip to content

Commit

Permalink
Do not let Parser.Parse edit the default module (#4059)
Browse files Browse the repository at this point in the history 
- `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.

<small>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).</small>
  • Loading branch information
@keyboardDrummer
keyboardDrummer authored May 25, 2023
1 parent abf4e4d commit 3e555a0
Show file tree
Hide file tree
Showing 60 changed files with 1,189 additions and 1,143 deletions.
10 changes: 4 additions & 6 deletions Source/DafnyCore.Test/DooFileTest.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<Uri> { rootUri });
var module = new LiteralModuleDecl(outerModule, null);
var outerModule = new DefaultModuleDefinition(new List<Uri> { 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<System.Uri>(), Sets.Empty<System.Uri>());
var program = ParseUtils.Parse(dafnyProgramText, rootUri, errorReporter);
Assert.Equal(0, errorReporter.ErrorCount);
return program;
}
}
19 changes: 10 additions & 9 deletions Source/DafnyCore/AST/BuiltIns.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,8 @@ namespace Microsoft.Dafny;

public class BuiltIns {
public DafnyOptions Options { get; }
public readonly ModuleDefinition SystemModule = new ModuleDefinition(RangeToken.NoToken, new Name("_System"), new List<IToken>(), false, false, null, null, null, true);
public readonly ModuleDefinition SystemModule = new(RangeToken.NoToken, new Name("_System"), new List<IToken>(),
false, false, null, null, null, true, false);
internal readonly Dictionary<int, ClassDecl> arrayTypeDecls = new Dictionary<int, ClassDecl>();
public readonly Dictionary<int, ArrowTypeDecl> ArrowTypeDecls = new Dictionary<int, ArrowTypeDecl>();
public readonly Dictionary<int, SubsetTypeDecl> PartialArrowTypeDecls = new Dictionary<int, SubsetTypeDecl>(); // same keys as arrowTypeDecl
Expand All @@ -34,18 +35,18 @@ public BuiltIns(DafnyOptions options) {
var str = new TypeSynonymDecl(RangeToken.NoToken, new Name("string"),
new TypeParameter.TypeParameterCharacteristics(TypeParameter.EqualitySupportValue.InferredRequired, Type.AutoInitInfo.CompilableValue, false),
new List<TypeParameter>(), SystemModule, new SeqType(new CharType()), null);
SystemModule.TopLevelDecls.Add(str);
SystemModule.SourceDecls.Add(str);
// create subset type 'nat'
var bvNat = new BoundVar(Token.NoToken, "x", Type.Int);
var natConstraint = Expression.CreateAtMost(Expression.CreateIntLiteral(Token.NoToken, 0), Expression.CreateIdentExpr(bvNat));
var ax = AxiomAttribute();
NatDecl = new SubsetTypeDecl(RangeToken.NoToken, new Name("nat"),
new TypeParameter.TypeParameterCharacteristics(TypeParameter.EqualitySupportValue.InferredRequired, Type.AutoInitInfo.CompilableValue, false),
new List<TypeParameter>(), SystemModule, bvNat, natConstraint, SubsetTypeDecl.WKind.CompiledZero, null, ax);
SystemModule.TopLevelDecls.Add(NatDecl);
SystemModule.SourceDecls.Add(NatDecl);
// create trait 'object'
ObjectDecl = new TraitDecl(RangeToken.NoToken, new Name("object"), SystemModule, new List<TypeParameter>(), new List<MemberDecl>(), DontCompile(), false, null);
SystemModule.TopLevelDecls.Add(ObjectDecl);
SystemModule.SourceDecls.Add(ObjectDecl);
// add one-dimensional arrays, since they may arise during type checking
// Arrays of other dimensions may be added during parsing as the parser detects the need for these
UserDefinedType tmp = ArrayType(1, Type.Int, true);
Expand Down Expand Up @@ -87,7 +88,7 @@ public UserDefinedType ArrayType(IToken tok, int dims, List<Type> 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);
Expand Down Expand Up @@ -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),
Expand All @@ -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

Expand All @@ -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);
}

/// <summary>
Expand Down Expand Up @@ -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;
}
Expand Down
185 changes: 7 additions & 178 deletions Source/DafnyCore/AST/Cloner.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 {

Expand All @@ -30,23 +28,11 @@ public Cloner(bool cloneResolvedFields = false) {
}

public virtual ModuleDefinition CloneModuleDefinition(ModuleDefinition m, Name name) {
ModuleDefinition nw;
if (m is DefaultModuleDefinition defaultModuleDefinition) {
nw = new DefaultModuleDefinition(defaultModuleDefinition.RootSourceUris);
} else {
nw = new ModuleDefinition(Range(m.RangeToken), name, m.PrefixIds, m.IsAbstract, m.IsFacade,
m.RefinementQId, m.EnclosingModule, CloneAttributes(m.Attributes),
true);
}
foreach (var d in m.TopLevelDecls) {
nw.TopLevelDecls.Add(CloneDeclaration(d, nw));
}
foreach (var tup in m.PrefixNamedModules) {
var newTup = new Tuple<List<IToken>, LiteralModuleDecl>(tup.Item1, (LiteralModuleDecl)CloneDeclaration(tup.Item2, nw));
nw.PrefixNamedModules.Add(newTup);
return new DefaultModuleDefinition(this, defaultModuleDefinition);
}
nw.Height = m.Height;
return nw;

return new ModuleDefinition(this, m, name);
}

public virtual TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition m) {
Expand Down Expand Up @@ -695,6 +681,9 @@ public override Expression CloneExpr(Expression expr) {
/// This cloner copies the origin module signatures to their cloned declarations
/// </summary>
class DeepModuleSignatureCloner : Cloner {
public DeepModuleSignatureCloner(bool cloneResolvedFields = false) : base(cloneResolvedFields) {
}

public override TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition m) {
var dd = base.CloneDeclaration(d, m);
if (d is ModuleDecl) {
Expand All @@ -719,149 +708,6 @@ public override TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition m
}


class ScopeCloner : DeepModuleSignatureCloner {
private VisibilityScope scope = null;

private Dictionary<Declaration, Declaration> reverseMap = new Dictionary<Declaration, Declaration>();

private bool isInvisibleClone(Declaration d) {
Contract.Assert(reverseMap.ContainsKey(d));
return !reverseMap[d].IsVisibleInScope(scope);
}

public ScopeCloner(VisibilityScope scope) {
this.scope = scope;
}

private bool RevealedInScope(Declaration d) {
return d.IsRevealedInScope(scope);
}

private bool VisibleInScope(Declaration d) {
return d.IsVisibleInScope(scope);
}

public override ModuleDefinition CloneModuleDefinition(ModuleDefinition m, Name name) {
var basem = base.CloneModuleDefinition(m, name);

//Merge signatures for imports which point to the same module
//This makes the consistency check understand that the same element
//may be referred to via different qualifications.
var sigmap = new Dictionary<ModuleDefinition, ModuleSignature>();
var declmap = new Dictionary<ModuleDefinition, List<AliasModuleDecl>>();
var vismap = new Dictionary<ModuleDefinition, VisibilityScope>();

foreach (var top in basem.TopLevelDecls) {
var import = reverseMap[top] as AliasModuleDecl;
if (import == null) {
continue;
}

var def = import.Signature.ModuleDef;
if (def == null) {
continue;
}

if (!declmap.ContainsKey(def)) {
declmap.Add(def, new List<AliasModuleDecl>());
sigmap.Add(def, new ModuleSignature());
vismap.Add(def, new VisibilityScope());
}

sigmap[def] = Resolver.MergeSignature(sigmap[def], import.Signature);
sigmap[def].ModuleDef = def;
declmap[def].Add((AliasModuleDecl)top);
if (VisibleInScope(import)) {
vismap[def].Augment(import.Signature.VisibilityScope);
}

}

foreach (var decls in declmap) {
sigmap[decls.Key].VisibilityScope = vismap[decls.Key];
foreach (var decl in decls.Value) {
decl.Signature = sigmap[decls.Key];
}
}

basem.TopLevelDecls.RemoveAll(t => {
if (t is AliasModuleDecl aliasModuleDecl) {
var def = aliasModuleDecl.Signature.ModuleDef;
return def != null && vismap[def].IsEmpty();
}
return isInvisibleClone(t);
});

basem.TopLevelDecls.OfType<TopLevelDeclWithMembers>().
Iter(t => t.Members.RemoveAll(isInvisibleClone));

return basem;
}

public override TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition m) {
var based = base.CloneDeclaration(d, m);
if (d is (RevealableTypeDecl or TopLevelDeclWithMembers) and not DefaultClassDecl && !RevealedInScope(d)) {
var tps = d.TypeArgs.ConvertAll(CloneTypeParam);
var characteristics = TypeParameter.GetExplicitCharacteristics(d);
var members = based is TopLevelDeclWithMembers tm ? tm.Members : new List<MemberDecl>();
var otd = new AbstractTypeDecl(Range(d.RangeToken), d.NameNode.Clone(this), m, characteristics, tps, members, CloneAttributes(d.Attributes), d.IsRefining);
based = otd;
if (d is ClassLikeDecl { IsReferenceTypeDecl: true } cl) {
reverseMap.Add(based, cl.NonNullTypeDecl);
return based;
}
}

reverseMap.Add(based, d);
return based;

}

public override Field CloneField(Field f) {
var cf = f as ConstantField;
if (cf != null && cf.Rhs != null && !RevealedInScope(f)) {
// We erase the RHS value. While we do that, we must also make sure the declaration does have a type, so instead of
// cloning cf.Type, we assume "f" has been resolved and clone cf.Type.NormalizeExpandKeepConstraints().
return new ConstantField(Range(cf.RangeToken), cf.NameNode.Clone(this), null, cf.HasStaticKeyword, cf.IsGhost, cf.IsOpaque, CloneType(cf.Type.NormalizeExpandKeepConstraints()), CloneAttributes(cf.Attributes));
}
return base.CloneField(f);
}

public override Function CloneFunction(Function f, string newName = null) {
var basef = base.CloneFunction(f, newName);
if (basef.ByMethodBody != null) {
Contract.Assert(!basef.IsGhost); // a function-by-method has .IsGhost == false
Contract.Assert(basef.Body != null); // a function-by-method has a nonempty .Body
if (RevealedInScope(f)) {
// For an "export reveals", use an empty (but not absent) by-method part.
basef.ByMethodBody = new BlockStmt(basef.ByMethodBody.RangeToken, new List<Statement>());
} else {
// For an "export provides", remove the by-method part altogether.
basef.ByMethodTok = null;
basef.ByMethodBody = null;
}
}
if (!RevealedInScope(f)) {
basef.Body = null;
}
return basef;
}

public override Method CloneMethod(Method m) {
var basem = base.CloneMethod(m);
basem.Body = null; //exports never reveal method bodies
return basem;
}

public override MemberDecl CloneMember(MemberDecl member, bool isReference) {
var basem = base.CloneMember(member, isReference);
reverseMap.Add(basem, member);
return basem;
}

}

/// <summary>
/// This cloner is used during the creation of a module signature for a method facade.
/// It does not clone method bodies, and it copies module signatures.
Expand All @@ -876,23 +722,6 @@ public override BlockStmt CloneBlockStmt(BlockStmt stmt) {
}
}

class AbstractSignatureCloner : ScopeCloner {

public AbstractSignatureCloner(VisibilityScope scope)
: base(scope) {
}

public override ModuleDefinition CloneModuleDefinition(ModuleDefinition m, Name name) {
var basem = base.CloneModuleDefinition(m, name);
basem.TopLevelDecls.RemoveAll(t => t is ModuleExportDecl);
return basem;
}

public override BlockStmt CloneMethodBody(Method m) {
return null;
}
}

/// <summary>
/// This cloner is used to clone a module into a _Compile module. This is different from
/// the standard cloner in the following ways:
Expand All @@ -906,7 +735,7 @@ public override BlockStmt CloneMethodBody(Method m) {
class CompilationCloner : DeepModuleSignatureCloner {
Dictionary<ModuleDefinition, ModuleDefinition> compilationModuleClones;
public CompilationCloner(Dictionary<ModuleDefinition, ModuleDefinition> compilationModuleClones)
: base() {
: base(false) {
this.compilationModuleClones = compilationModuleClones;
}

Expand Down
15 changes: 8 additions & 7 deletions Source/DafnyCore/AST/DafnyAst.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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;
}

Expand All @@ -138,15 +139,15 @@ public override IEnumerable<Assumption> 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;
}

Expand Down
20 changes: 20 additions & 0 deletions Source/DafnyCore/AST/FileModuleDefinition.cs
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
using System.Collections.Generic;

namespace Microsoft.Dafny;

/// <summary>
/// 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
/// </summary>
public class FileModuleDefinition : ModuleDefinition {
public List<Include> Includes { get; } = new();

public FileModuleDefinition() :
base(RangeToken.NoToken, new Name("_module"), new List<IToken>(),
false, false, null, null, null, true, false) {
{
}
}
}
Loading

0 comments on commit 3e555a0

Please sign in to comment.