feat: Datatype ghost constructors #2666

RustanLeino · 2022-08-31T18:27:09Z

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 in Test/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 the ghost 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):
- If storage is really uninitialized, then a run-time garbage collector may not be able to trace pointers accurately.
- Dafny does not restrict printing of uninitialized values. If a program uses print 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 and printing 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 in DafnyAst.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 for MemberSelectExpr, DatatypeUpdateExpr, and BinaryExpr.

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 method ResolveDatatypeUpdate.

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.

… datatypes

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

fabiomadge · 2022-09-05T22:36:02Z

Source/Dafny/Compilers/Compiler-python.cs

+
+ if (usePlaceboValue) {
+ return "None";
+ }
+


This should be redundant due to L640. I wonder what's going on, in case it's necessary.

fabiomadge · 2022-09-05T22:36:44Z

Source/Dafny/Compilers/Compiler-python.cs

 foreach (var ctor in dt.Ctors) {
+ if (ctor.IsGhost) {
+ continue;
+ }


Suggested change

foreach (var ctor in dt.Ctors) {

if (ctor.IsGhost) {

continue;

}

foreach (var ctor in dt.Ctors.Where(ctor => !ctor.IsGhost)) {

I made this change throughout (i.e., not just in the Python compiler).

Source/Dafny/Compilers/Compiler-python.cs

fabiomadge · 2022-09-06T00:42:53Z

Source/Dafny/Compilers/SinglePassCompiler.cs

+ 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;
+ }


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)));

Is the second version easier to read? It repeats the expression member.EnclosingClass several times. Pattern matching like the original seems appropriate here.

I'll stay with the original.

Co-authored-by: Fabio Madge <[email protected]>

…Leino/dafny into ghost-constructors-rfc-11

# Conflicts: # Source/Dafny/AST/DafnyAst.cs

fabiomadge · 2022-09-15T23:02:20Z

Source/DafnyCore/AST/TopLevelDeclarations.cs

@@ -1382,7 +1385,7 @@ public class CoDatatypeDecl : DatatypeDecl {
 }

 public override DatatypeCtor GetGroundingCtor() {
- return Ctors[0];
+ return Ctors.FirstOrDefault(ctor => ctor.IsGhost, Ctors[0]);


Suggested change

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?

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.

fabiomadge · 2022-09-15T23:08:58Z

Source/DafnyCore/AST/Types.cs

+ public override bool PartiallySupportsEquality {
+ get {
+ var totalEqualitySupport = SupportsEquality;
+ if (!totalEqualitySupport && ResolvedClass is IndDatatypeDecl dt && dt.IsRevealedInScope(Type.GetScope())) {


Should we add CoDatatypeDecl as well?

No, because codatatypes never support equality at runtime.

fabiomadge · 2022-09-15T23:14:44Z

Source/DafnyCore/AST/Types.cs

+ foreach (var ctor in dt.Ctors) {
+ if (!ctor.IsGhost) {
+ hasNonGhostConstructor = true;
+ if (!ctor.Formals.All(formal => !formal.IsGhost && formal.Type.SupportsEquality)) {


Don't we want an implication here?

Suggested change

if (!ctor.Formals.All(formal => !formal.IsGhost && formal.Type.SupportsEquality)) {

if (!ctor.Formals.All(formal => formal.IsGhost || formal.Type.SupportsEquality)) {

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.

fabiomadge · 2022-09-15T23:15:33Z

Source/DafnyCore/AST/Types.cs

+ foreach (var ctor in dt.Ctors) {
+ if (!ctor.IsGhost) {


Suggested change

foreach (var ctor in dt.Ctors) {

if (!ctor.IsGhost) {

foreach (var ctor in dt.Ctors.Where(ctor => !ctor.IsGhost))

fabiomadge · 2022-09-15T23:26:44Z

Source/DafnyCore/AST/Types.cs

+ }
+ }
+ 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;


I think this is equivalent:

return dt.Ctors.All(ctor => ctor.IsGhost || ctor.Formals.All(formal => formal.IsGhost || formal.Type.SupportsEquality));

No, this would give true if all constructors are ghost.

True, that is different, but doesn't a Datatype like that support partial equality at runtime?

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.

fabiomadge · 2022-09-15T23:52:36Z

Source/DafnyCore/Compilers/Compiler-java.cs

@@ -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))) ||


Should we do the same for methods?

Yes! Good call! (I also fixed it in the C# compiler.)

fabiomadge · 2022-09-15T23:59:28Z

Source/DafnyCore/Compilers/SinglePassCompiler.cs

@@ -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;


Do we know that type.HasCompilableValue?

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.

fabiomadge · 2022-09-16T15:06:13Z

Source/DafnyCore/Util.cs

+ } else if (e.Member != null && e.Member.IsGhost) {
+ return true;
+ } else if (e.Member is DatatypeDestructor dtor) {
+ return dtor.EnclosingCtors.All(ctor => ctor.IsGhost);


Would it be wrong to strengthen this to any?

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.

fabiomadge · 2022-09-16T15:28:49Z

Source/DafnyCore/Verifier/Translator.ExpressionWellformed.cs

+ case BinaryExpr.ResolvedOpcode.NeqCommon:
+ CheckWellformed(e.E1, options, locals, builder, etran);
+ if (e.InCompiledContext) {
+ if (Resolver.CanCompareWith(e.E0) || Resolver.CanCompareWith(e.E1)) {


Suggested change

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.

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.

fabiomadge · 2022-09-16T15:50:28Z

Source/DafnyCore/Verifier/Translator.ExpressionWellformed.cs

+ if (e.InCompiledContext) {
+ if (Resolver.CanCompareWith(e.E0) || Resolver.CanCompareWith(e.E1)) {
+ // everything's fine
+ } else if (!e.E0.Type.SupportsEquality) {


Can we skip E1 here?

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 <[email protected]>

…ot querying calls)

RustanLeino added 28 commits August 31, 2022 11:10

Add syntax for ghost constructors

6bcd5d5

Improve error messages

6e9681c

Use subclass to distinguish discriminators from other SpecialFields

3aa3b15

Mark ghost-variant datatypes as not supporting equality

f4b39bd

Add resolution tests

796cc09

Add resolution checks for match

affcac1

Check ghost constructors are used only in ghost contexts

3091bf1

Improve resolution

b1cab13

fix: Check expressions to be compilable

7c20ade

Check precondition of discriminators and destructors in ghost-variant…

3c4219f

… datatypes

Add more bookkeeping info for DatatypeUpdateExpr

9fcfa34

Add verification tests for datatype update

4e784b1

Add additional test

429ec6c

Reformat test

cb850d7

fix: datatype update resolution re ghosts

5746e9d

Improve resolution checks for select/update

61c9a2f

Update tests

09dbf9b

Add compilation tests

aaf6d93

fix: Java compilation of array allocation must erase type args

8e968f8

Add motivating test program for ghost constructors

276200e

Support partial equality (for ghost-variant datatypes)

dee6160

Don’t generate code for ghost constructors

14d65b9

Desugar DatatypeUpdateExpr twice (ghost and compiled)

2826da5

Compile

0c6bfff

Add release notes

d0c0177

Update release notes with PR number

843d27e

Refactor to share more code

2b299cc

RustanLeino marked this pull request as ready for review August 31, 2022 20:55

Merge branch 'master' into ghost-constructors-rfc-11

e715df5

# Conflicts: # Source/Dafny/Compilers/Compiler-python.cs

Merge branch 'master' into ghost-constructors-rfc-11

6b1c000

fabiomadge reviewed Sep 5, 2022

View reviewed changes

Python: it just works

d0c9cfc

fabiomadge reviewed Sep 6, 2022

View reviewed changes

RustanLeino and others added 6 commits September 12, 2022 16:16

Update Source/Dafny/Compilers/Compiler-python.cs

9457cf7

Co-authored-by: Fabio Madge <[email protected]>

Improve code as suggested by review comments

913e9cd

Merge branch 'ghost-constructors-rfc-11' of https://github.com/Rustan…

50979c5

…Leino/dafny into ghost-constructors-rfc-11

Merge branch 'master' into ghost-constructors-rfc-11

2420aa4

# Conflicts: # Source/Dafny/AST/DafnyAst.cs

Fix merge

2385b03

Merge branch 'master' into ghost-constructors-rfc-11

a6bc864

fabiomadge reviewed Sep 16, 2022

View reviewed changes

RustanLeino and others added 10 commits September 19, 2022 11:42

Update Source/DafnyCore/Compilers/Compiler-Csharp.cs

7bcc607

Co-authored-by: Fabio Madge <[email protected]>

Improve comment

e1e2f5c

Use better C#

b839f62

fix: Check for custom-receiver methods when emitting “this”

5315dcd

fix: Remove incorrect precondition

c9d2255

Improve code based on review comments

9ad188d

Add sanity-check asserts

0eb89dc

Merge branch 'master' into ghost-constructors-rfc-11

8112da5

Don’t emit unused Go variable for String() and Equals()

72b919c

Update .InCompiledContext only for serious CheckIsCompilable calls (n…

e067070

…ot querying calls)

fabiomadge approved these changes Sep 20, 2022

View reviewed changes

RustanLeino merged commit a969ac0 into dafny-lang:master Sep 20, 2022

RustanLeino deleted the ghost-constructors-rfc-11 branch September 20, 2022 15:59

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: Datatype ghost constructors #2666

feat: Datatype ghost constructors #2666

RustanLeino commented Aug 31, 2022 •

edited

Loading

fabiomadge Sep 5, 2022 •

edited

Loading

fabiomadge Sep 5, 2022

RustanLeino Sep 12, 2022

fabiomadge Sep 6, 2022

keyboardDrummer Sep 6, 2022 •

edited

Loading

RustanLeino Sep 12, 2022

fabiomadge Sep 15, 2022

RustanLeino Sep 19, 2022

fabiomadge Sep 15, 2022

RustanLeino Sep 19, 2022

fabiomadge Sep 15, 2022

RustanLeino Sep 19, 2022

fabiomadge Sep 15, 2022

fabiomadge Sep 15, 2022

RustanLeino Sep 19, 2022

fabiomadge Sep 19, 2022

RustanLeino Sep 19, 2022

fabiomadge Sep 15, 2022

RustanLeino Sep 19, 2022

fabiomadge Sep 15, 2022

RustanLeino Sep 19, 2022

fabiomadge Sep 16, 2022

RustanLeino Sep 19, 2022

fabiomadge Sep 16, 2022

RustanLeino Sep 19, 2022

fabiomadge Sep 16, 2022

RustanLeino Sep 19, 2022

	return Ctors.FirstOrDefault(ctor => ctor.IsGhost, Ctors[0]);
	return Ctors.FirstOrDefault(ctor => !ctor.IsGhost, Ctors[0]);

	if (!ctor.Formals.All(formal => !formal.IsGhost && formal.Type.SupportsEquality)) {
	if (!ctor.Formals.All(formal => formal.IsGhost \|\| formal.Type.SupportsEquality)) {

	foreach (var ctor in dt.Ctors) {
	if (!ctor.IsGhost) {
	foreach (var ctor in dt.Ctors.Where(ctor => !ctor.IsGhost))

	if (Resolver.CanCompareWith(e.E0) \|\| Resolver.CanCompareWith(e.E1)) {
	if (Resolver.CanCompareWith(e.E0) && Resolver.CanCompareWith(e.E1)) {

feat: Datatype ghost constructors #2666

feat: Datatype ghost constructors #2666

Conversation

RustanLeino commented Aug 31, 2022 • edited Loading

Feature description

Comments for reviewers

fabiomadge Sep 5, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer Sep 6, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

RustanLeino commented Aug 31, 2022 •

edited

Loading

fabiomadge Sep 5, 2022 •

edited

Loading

keyboardDrummer Sep 6, 2022 •

edited

Loading