-
Notifications
You must be signed in to change notification settings - Fork 261
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
feat: Datatype ghost constructors #2666
feat: Datatype ghost constructors #2666
Conversation
By trimming down the test file to features that the Python compiler currently support, I was able to make some changes to support ghost constructors. However, full support requires other features of the language that haven’t been addressed in the Python compiler yet.
# Conflicts: # Source/Dafny/Compilers/Compiler-python.cs
|
||
if (usePlaceboValue) { | ||
return "None"; | ||
} | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This should be redundant due to L640. I wonder what's going on, in case it's necessary.
foreach (var ctor in dt.Ctors) { | ||
if (ctor.IsGhost) { | ||
continue; | ||
} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
foreach (var ctor in dt.Ctors) { | |
if (ctor.IsGhost) { | |
continue; | |
} | |
foreach (var ctor in dt.Ctors.Where(ctor => !ctor.IsGhost)) { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I made this change throughout (i.e., not just in the Python compiler).
if (member.IsStatic) { | ||
return false; | ||
} else if (member.EnclosingClass is NewtypeDecl) { | ||
return true; | ||
} else if (member.EnclosingClass is TraitDecl) { | ||
return member is ConstantField { Rhs: { } } or Function { Body: { } } or Method { Body: { } }; | ||
} else if (member.EnclosingClass is DatatypeDecl datatypeDecl) { | ||
// An undefined value "o" cannot use this o.F(...) form in most languages. | ||
return datatypeDecl.Ctors.Any(ctor => ctor.IsGhost); | ||
} else { | ||
return false; | ||
} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Consider
if (member.IsStatic) {
return false;
}
return member.EnclosingClass switch {
NewtypeDecl => true,
TraitDecl => member is ConstantField { Rhs: { } } or Function { Body: { } } or Method { Body: { } },
DatatypeDecl datatypeDecl => datatypeDecl.Ctors.Any(ctor => ctor.IsGhost),
_ => false
};
or
return !member.IsStatic
&& (member.EnclosingClass is NewtypeDecl
|| (member.EnclosingClass is TraitDecl
&& member is ConstantField { Rhs: { } } or Function { Body: { } } or Method { Body: { } })
|| (member.EnclosingClass is DatatypeDecl datatypeDecl && datatypeDecl.Ctors.Any(ctor => ctor.IsGhost)));
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Is the second version easier to read? It repeats the expression member.EnclosingClass
several times. Pattern matching like the original seems appropriate here.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'll stay with the original.
Co-authored-by: Fabio Madge <fabio@madge.me>
…Leino/dafny into ghost-constructors-rfc-11
# Conflicts: # Source/Dafny/AST/DafnyAst.cs
@@ -1382,7 +1385,7 @@ public class CoDatatypeDecl : DatatypeDecl { | |||
} | |||
|
|||
public override DatatypeCtor GetGroundingCtor() { | |||
return Ctors[0]; | |||
return Ctors.FirstOrDefault(ctor => ctor.IsGhost, Ctors[0]); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
return Ctors.FirstOrDefault(ctor => ctor.IsGhost, Ctors[0]); | |
return Ctors.FirstOrDefault(ctor => !ctor.IsGhost, Ctors[0]); |
Then again, that's probably what we want for efficiency, right?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The "grounding constructor" is what the compiler will use as a default value. In an inductive datatype, there are various limitations, since the grounding constructor must be a constructor whose arguments can be constructed. But for a codatatype, any any constructor will do, since any recursive calls will be hidden inside a thunk anyway. So, the code here used to pick Ctors[0]
, rather arbitrarily.
If there is a ghost constructors, that's a great choice, because then the compiler can (essentially) leave the value uninitialized. So, that's why the code picks the first ghost constructor, if there is one, and otherwise picks the first non-ghost constructor.
Source/DafnyCore/AST/Types.cs
Outdated
public override bool PartiallySupportsEquality { | ||
get { | ||
var totalEqualitySupport = SupportsEquality; | ||
if (!totalEqualitySupport && ResolvedClass is IndDatatypeDecl dt && dt.IsRevealedInScope(Type.GetScope())) { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Should we add CoDatatypeDecl as well?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
No, because codatatypes never support equality at runtime.
Source/DafnyCore/AST/Types.cs
Outdated
foreach (var ctor in dt.Ctors) { | ||
if (!ctor.IsGhost) { | ||
hasNonGhostConstructor = true; | ||
if (!ctor.Formals.All(formal => !formal.IsGhost && formal.Type.SupportsEquality)) { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Don't we want an implication here?
if (!ctor.Formals.All(formal => !formal.IsGhost && formal.Type.SupportsEquality)) { | |
if (!ctor.Formals.All(formal => formal.IsGhost || formal.Type.SupportsEquality)) { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
No, because if an argument is ghost, it is not available at run time, so then it can't be compared. (Note that all occurrences of "equality support" and "partial equality support" refers to compiled support of equality, that is, run time support.)
I expanded the comment in the code that try to better clarify these things.
Source/DafnyCore/AST/Types.cs
Outdated
foreach (var ctor in dt.Ctors) { | ||
if (!ctor.IsGhost) { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
foreach (var ctor in dt.Ctors) { | |
if (!ctor.IsGhost) { | |
foreach (var ctor in dt.Ctors.Where(ctor => !ctor.IsGhost)) |
} | ||
} | ||
Contract.Assert(dt.HasGhostVariant); // sanity check (if the types of all formals support equality, then either .SupportsEquality or there is a ghost constructor) | ||
return hasNonGhostConstructor; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think this is equivalent:
return dt.Ctors.All(ctor => ctor.IsGhost || ctor.Formals.All(formal => formal.IsGhost || formal.Type.SupportsEquality));
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
No, this would give true
if all constructors are ghost.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
True, that is different, but doesn't a Datatype like that support partial equality at runtime?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
No, if all the constructors are ghost, then the values at run time may be uninitialized, so then it's not possible to compare them accurately.
@@ -1138,7 +1139,7 @@ protected class ClassWriter : IClassWriter { | |||
protected override void EmitThis(ConcreteSyntaxTree wr) { | |||
var custom = | |||
(enclosingMethod != null && enclosingMethod.IsTailRecursive) || | |||
(enclosingFunction != null && enclosingFunction.IsTailRecursive) || | |||
(enclosingFunction != null && (enclosingFunction.IsTailRecursive || NeedsCustomReceiver(enclosingFunction))) || |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Should we do the same for methods?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes! Good call! (I also fixed it in the C# compiler.)
@@ -2805,7 +2826,8 @@ protected class NullClassWriter : IClassWriter { | |||
|
|||
type = type.NormalizeExpandKeepConstraints(); | |||
Contract.Assert(type is NonProxyType); // this should never happen, since all types should have been successfully resolved | |||
return TypeInitializationValue(type, wr, tok, false, constructTypeParameterDefaultsFromTypeDescriptors); | |||
var usePlaceboValue = type.AsDatatype?.GetGroundingCtor().IsGhost == true; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Do we know that type.HasCompilableValue
?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The precondition of this DefaultValue
method previously stated Contract.Requires(type.HasCompilableValue);
, so I was going to answer "yes". But then I experimentally found that this condition does not hold at all call sites. After a further investigation, my conclusion is that the precondition was incorrectly stated. It is fine and expected that this method can be called with a type that has no compilable value. This happens when type
(or any component of type
) is a type parameter that is not auto-init. In those cases, DefaultValue
emits code that produces a default value either from a parameter in the target-code context (for example, this may be a parameter G _default_G
that gives a G
value to be used as default) or from a type descriptor in the target-code context (for example, the target-code context may contain a parameter Dafny.TypeDescriptor<G> _td_G
and the default value will then be produced from _td_G.Default()
).
My conclusion is that the precondition of DefaultValue
was stated incorrectly. So, I removed it.
} else if (e.Member != null && e.Member.IsGhost) { | ||
return true; | ||
} else if (e.Member is DatatypeDestructor dtor) { | ||
return dtor.EnclosingCtors.All(ctor => ctor.IsGhost); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Would it be wrong to strengthen this to any?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes, the semantics (which hadn't been clear before this PR, but which I have added some comments about) is that UsesSpecFeatures
returns true
if the only possible use of the expression is in ghost contexts. That's true if the member is found only in ghost constructors. However, if the member is found in some non-ghost constructor, then the verifier will check that the datatype value is of the appropriate constructor at run time.
case BinaryExpr.ResolvedOpcode.NeqCommon: | ||
CheckWellformed(e.E1, options, locals, builder, etran); | ||
if (e.InCompiledContext) { | ||
if (Resolver.CanCompareWith(e.E0) || Resolver.CanCompareWith(e.E1)) { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
if (Resolver.CanCompareWith(e.E0) || Resolver.CanCompareWith(e.E1)) { | |
if (Resolver.CanCompareWith(e.E0) && Resolver.CanCompareWith(e.E1)) { |
Not sure, but seems sensical without much context.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
As far as ghost constructors are concerned, your hunch is correct. For such types, I believe CanCompareWith
always returns the same thing for e.E0
and e.E1
, so an &&
would seem sensical and, in fact, it would be fine to check just one of these. However, the use of CanCompareWith
is to allow comparisons like x == None
, where None
is a constructor and the type of x
is a type that, in general, does not support equality. Such comparisons can be allowed, provided there are no issues of uninitialized values. For the comparison x == None
, CanCompareWith(e.E0)
returns false
whereas CanCompareWith(e.E1)
returns true
.
So, we do need both comparisons, and they should be connected with a ||
. I added a test case to make sure this works as intended.
if (e.InCompiledContext) { | ||
if (Resolver.CanCompareWith(e.E0) || Resolver.CanCompareWith(e.E1)) { | ||
// everything's fine | ||
} else if (!e.E0.Type.SupportsEquality) { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Can we skip E1
here?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
You mean on L908, right? (For L906, see my comment above.) The test on L908 is unnecessary, because CanCompareWith
on L906 always returns true
if .SupportsEquality
holds. (This applies to both e.E0
and e.E1
.) So, I removed the test (and added an Assert
as a sanity check.)
Co-authored-by: Fabio Madge <fabio@madge.me>
…ot querying calls)
This PR introduces ghost constructors for datatypes, as per RFC dafny-lang/rfcs#11.
For motivation of this feature, see the RFC or the example
Stack
class inTest/comp/Uninitialized.dfy
.Feature description
Any (and all) constructor of a datatype can be declared as ghost. This is done by preceding the constructor name by the keyword
ghost
. (Note, if the constructor has attributes, those are placed before the name of the constructor, which is consistent with the attribute placement in other declarations. For a ghost constructor, this means the attribute is placed between theghost
keyword and the identifier that names the constructor.)Compiled code may not explicitly name a ghost constructor. Moreover, compiled code is not allowed to depend on the need to check if a datatype value is of a ghost variant. Consequently, the verifier (and in some cases, the resolver) will enforce that any discriminator (e.g.,
Cons?
) or destructor (e.g.,tail
) is used only when the datatype value is known not to be of a ghost variant. In other words, a precondition for these operations (in compiled contexts) is that the datatype value is not of a ghost variant.Even though a program cannot (in compiled contexts) explicitly create ghost variants, Dafny might assign ghost variants as part of auto-initialization. These "assignments" are performed by... doing nothing! (Or nearly nothing.) In other words, since the verifier makes sure that ghost variants are never looked at, the compiler feels free to leave such variables as uninitialized.
Uninitialized variables usually means asking for trouble. Ghost constructors provides uninitialized storage and verifies that that program never looks at uninitialized variables. Still, there are two areas where uninitialized storage may affect execution (these two points were not mentioned in the RFC):
print
ing of uninitialized values. If a program usesprint
with an uninitialized values, there is in general no way to tell what will happen.The compilers that Dafny supports are managed languages (with the exception of C++, but C++ does not use a garbage collector; furthermore, the C++ compiler currently supports only a subset of Dafny, and that subset does not include ghost constructors). Since the target languages are managed and type safe, there is no way for the Dafny compilers to really leave storage uninitialized. Instead, values will typically have a
null
-equivalent value. This means that garbage collection will work andprint
ing will not crash the program.As for printing,
print
should be considered a debugging facility or a facility to make it easy to write student programs.The RFC mentions a compiler optimization where a datatype with exactly one non-ghost constructor with exactly one non-ghost parameter can compiled as just that one parameter. This PR does not implement that optimization. A separate PR could implement this optimization along with the similar optimization for tuples with ghost components. Ghost constructors would benefit from the optimization, but do not depend on it.
Comments for reviewers
The
PartiallySupportsEquality
getter inDafnyAst.cs
paves the way to let other, future types supports==
under a precondition.The verifier treats some expressions in different ways, depending on if the expression is used in a ghost context or a compiled context. This context information is available in the resolver, but not in the traversals in the verifier. Instead, some bread crumbs are places in the AST by the resolver, and the verifier looks at these bread crumbs. This PR introduces an
.InCompiledContext
field forMemberSelectExpr
,DatatypeUpdateExpr
, andBinaryExpr
.The
DatatypeUpdateExpr
is desugared during resolution. Unfortunately, at that time, it is not known if the expression will be used in a ghost context or a compiled context. So, this PR generates two candidate desugarings during resolution. Later during the pipeline, if it's determined that the expression is used in compiled contexts (CheckIsCompilable
), then the ghost-desugaring (which is the default) is switched to the compiled-desugaring. See comment in code for methodResolveDatatypeUpdate
.The PR includes ghost-constructor support for C#, Java, JavaScript, and Go. In addition, some changes were made in the Python compiler in support of ghost constructors. Full support in Python would require some other features that are not yet supported in that compiled. Also, no support of ghost constructor was added for the C++ compiler (because there are too many features that it doesn't support, so the test files don't even start to go through).
Closes dafny-lang/rfcs#11
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.