Skip to content
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

Support tuples with ghost components #1269

Merged
merged 11 commits into from
Aug 3, 2021
Merged

Conversation

fpoli
Copy link
Contributor

@fpoli fpoli commented Jul 1, 2021

This PR adds support for tuples with ghost components. In addition to secure-foundations@c511546, authored by @Chris-Hawblitzel, the major changes are:

  • The ghost keyword is not allowed in the patterns of match statements.
  • The parser handles ambiguous cases like u := F( a < (b, ghost b), c > (d) );
  • ghost can be added to tuples with named arguments. For example (1 := 123, ghost 0 := 234), which is equivalent to (ghost 234, 123).
  • The ghost keyword is pretty-printed.
  • Various fixes to the compilers, such that ghost components of tuples don't show up in the target language. In particular, unlike with user-defined datatypes, ghost components of tuples don't cause the generation of type parameter in C#.

@fpoli fpoli force-pushed the ghost-args branch 4 times, most recently from dac8db1 to aa4d478 Compare July 2, 2021 10:45
Source/Dafny/Dafny.atg Outdated Show resolved Hide resolved
Source/Dafny/Dafny.atg Outdated Show resolved Hide resolved
Source/Dafny/Dafny.atg Outdated Show resolved Hide resolved
Source/Dafny/Dafny.atg Outdated Show resolved Hide resolved
Source/Dafny/Dafny.atg Outdated Show resolved Hide resolved
Source/Dafny/DafnyAst.cs Outdated Show resolved Hide resolved
Source/Dafny/DafnyAst.cs Outdated Show resolved Hide resolved
Source/Dafny/DafnyAst.cs Outdated Show resolved Hide resolved
Test/ghost/PhantomData.dfy Outdated Show resolved Hide resolved
Test/ghost/PhantomData.dfy Outdated Show resolved Hide resolved
@fpoli
Copy link
Contributor Author

fpoli commented Jul 8, 2021

It seems that in Compiler-java.cs the generic code that compiles a DatatypeValue (supertype of tuples) needs to be special cased to skip type arguments for ghost components. That is, dafny already compiles datatypes with N non-ghost arguments and M ghost to classes with N+M type parameters, but in the case of tuples we want to compile to classes with just the N non-ghost type parameters.

@fpoli
Copy link
Contributor Author

fpoli commented Jul 8, 2021

Where is the code that emits the types (and type parameters) of method arguments in the Java compiler?

// Dafny
method Test0(t0: (ghost int)) { ... }

Compilation:

// Java
public class __default {
  public __default() {
  }
  public static void Test0(dafny.Tuple0<java.math.BigInteger> t0)
  //                                   ^^^^^^^^^^^^^^^^^^^^^^---- This is what I'm trying to fix. Where is it generated?
  {
    ...
  }
}

Edit: I found it, it's the method TypeName_UDT implemented in Compiler.cs.

@fpoli
Copy link
Contributor Author

fpoli commented Jul 9, 2021

@RustanLeino Should the type parameters for ghost component show up in the target language of the dafny compilation?

Consider the datatype PhantomData<T> = PhantomData(ghost value: T) datatype. In Java and C# it's currently compiled to a class with a <T> type parameter for the ghost argument, even if the argument is unused in the program.

Now, consider the (ghost T) tuple type, which should be compiled to an empty tuple. We have some options:

  1. If we consider the tuple to be a special case of a datatype (in fact, TupleTypeDecl extends DatatypeDecl) then (ghost T) should be compiled to a class Tuple1G<T> where the type T is unused. To do this, the generation of tuple class declarations in the Java compiler should be changed to generate ghost type parameters.
  2. If we want to avoid generating unnecessary code, (ghost T) should be compiled to a class Tuple0 with no type parameters. To do this, the generic generation of datatype class declarations in the C# compiler should be fixed to special-case the tuple types.
  3. In addition to option 2, we can also change the compilation of datatypes like datatype PhantomData<T> = PhantomData(ghost value: T) to generate classes without type parameters for the ghost components. This would produce the best target code in my opinion, but it requires more implementation effort.

@RustanLeino
Copy link
Collaborator

@fpoli Very good points.

It would not be correct (in general) to remove the type parameter of user-defined datatypes like PhantomData above. The reason is that such a type could have a member that makes use of the type parameter. So, we should not do option 3.

I think we should aim for option 2. That is, I think it is worthwhile to special-case tuple types to remove the type arguments that are not needed. Since tuples are built in, they are known not to have any compiled members that need the type parameters corresponding to the ghost arguments.

@fpoli fpoli force-pushed the ghost-args branch 3 times, most recently from fbb6785 to 240357a Compare July 13, 2021 08:37
@fpoli
Copy link
Contributor Author

fpoli commented Jul 13, 2021

I just noticed that there is a C++ compiler. Should I test this PR on that as well, or is C++ "less supported" by dafny (see #1293 and #1294)? In the latter case this PR is ready to be reviewed and later merged.

@fpoli fpoli marked this pull request as ready for review July 13, 2021 08:44
Source/Dafny/Dafny.atg Outdated Show resolved Hide resolved
Source/Dafny/Dafny.atg Outdated Show resolved Hide resolved
Source/Dafny/DafnyAst.cs Outdated Show resolved Hide resolved
@fpoli fpoli force-pushed the ghost-args branch 2 times, most recently from 0c5d68e to 6f3a658 Compare July 19, 2021 09:11
@fpoli
Copy link
Contributor Author

fpoli commented Jul 19, 2021

@RustanLeino I addressed the review and rebased on master.

@fpoli
Copy link
Contributor Author

fpoli commented Jul 19, 2021

The CI failure of the "Create release" step looks like a glitch:

   Segmentation fault (core dumped)
/home/runner/work/dafny/dafny/dafny/Source/Dafny/DafnyPipeline.csproj(4,5): error MSB3073: The command "dotnet tool restore" exited with code 139.
  Successfully created package '/home/runner/work/dafny/dafny/dafny/Binaries/DafnyRuntime.1.1.0.nupkg'.
failed! (Is Dafny or the Dafny server running?)

I'll force-push to restart the tests.

Based on secure-foundations@c511546, authored by Chris-Hawblitzel.
Source/Dafny/Compiler.cs Outdated Show resolved Hide resolved
Source/Dafny/Compiler.cs Outdated Show resolved Hide resolved
Source/Dafny/Dafny.atg Outdated Show resolved Hide resolved
Source/Dafny/Dafny.atg Outdated Show resolved Hide resolved
Source/Dafny/Dafny.atg Show resolved Hide resolved
Source/Dafny/DafnyAst.cs Outdated Show resolved Hide resolved
Source/Dafny/DafnyAst.cs Outdated Show resolved Hide resolved
Source/Dafny/Resolver.cs Outdated Show resolved Hide resolved
Test/ghost/AmbiguousGhost.dfy Outdated Show resolved Hide resolved
Test/ghost/AllowedGhost.dfy Outdated Show resolved Hide resolved
fpoli and others added 3 commits July 30, 2021 09:19
@fpoli
Copy link
Contributor Author

fpoli commented Jul 30, 2021

Let me know if I should squash all the commits of this PR together.

@keyboardDrummer
Copy link
Member

Let me know if I should squash all the commits of this PR together.

No need, Dafny's repository only allows merging PRs by squashing them.

@@ -347,7 +347,8 @@ public CsharpCompiler(ErrorReporter reporter)
// }}
// ...
// }
var DtT_TypeArgs = TypeParameters(dt.TypeArgs);
var nonGhostTypeArgs = SelectNonGhost(dt, dt.TypeArgs);
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I feel we need a compilation step that removes anything ghost, to prevent having to filter out ghostness in each of the compilers, but I guess that's out of scope for this PR.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I agree, on both accounts.

Source/Dafny/DafnyAst.cs Show resolved Hide resolved
Source/Dafny/Util.cs Outdated Show resolved Hide resolved
@@ -1384,7 +1384,7 @@ internal class PredefinedDecls {
}
Bpl.Variable resType = new Bpl.Formal(ctor.tok, new Bpl.TypedIdent(ctor.tok, Bpl.TypedIdent.NoName, predef.DatatypeType), false);
Bpl.Function fn;
if (dt is TupleTypeDecl ttd && ttd.Dims == 2) {
if (dt is TupleTypeDecl ttd && ttd.Dims == 2 && ttd.NonGhostDims == 2) {
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should ttd.Dims == 2 still be in here?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Tuples like (int, int, ghost int) and (int, int) should be translated to different types because we want Boogie to know that instances of the former cannot alias instances of the latter.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm actually not sure how to observe a difference in the verification time of Dafny. It's a suggestion that I got from Rustan.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The following assertion should be provable by the verifier, which requires that the verifier treat (int, int, ghost int) as a different type than (int, int).

method M(a: array<(int, int, ghost int)>, b: array<(int, int)>)
{
  assert a as object != b;
}

Copy link
Contributor Author

@fpoli fpoli Aug 2, 2021

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm going to add that example, thanks.

Regarding the if condition on tdd, we want to only match tuples of size 2 that have no ghost components, because in that case we should use the Tuple2 definition provided by DafnyPrelude.bpl. Other conditions (ttd.NonGhostDims == 2 only, ttd.Dims == 2 only, ttd.Dims == 2 && ttd.NonGhostDims == 0) lead to Boogie errors like "Error: use of undeclared function: Tclass._System.Tuple3OOG" because they make Dafny skip the translation of tuples that are not defined in DafnyPrelude.bpl.

@@ -9416,7 +9416,7 @@ AND Apply(f,h0,bxs) == Apply(f,h0,bxs)
// Create the type constructor
if (td is ClassDecl cl && cl.IsObjectTrait) {
// the type constructor for "object" is in DafnyPrelude.bpl
} else if (td is TupleTypeDecl ttd && ttd.Dims == 2) {
} else if (td is TupleTypeDecl ttd && ttd.Dims == 2 && ttd.NonGhostDims == 2) {
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should ttd.Dims == 2 still be in here?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actually, shouldn't it be ttd.Dims == 2 && ttd.NonGhostDims == 0?
Also, the same test appears in one more place in Translator.cs, around line 1387.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think ttd.Dims == 2 && ttd.NonGhostDims == 2 is correct. See this message in the other conversation.

Copy link
Member

@keyboardDrummer keyboardDrummer left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do we need to update the reference manual as well? Here's a section on tuples: https://dafny-lang.github.io/dafny/DafnyRef/DafnyRef#sec-tuple-types. I think we can add an example indicating that the ghost modifier is valid in front of types in tuples.

@fpoli
Copy link
Contributor Author

fpoli commented Aug 2, 2021

@RustanLeino I fixed the equality support check and added the following test

method M<T(==)>(a: T)

method P() {
  var x: (int, int, ghost int);
  M(x); // Disallowed. It's not possible to compile an equality function that also checks ghost components.
}

@RustanLeino RustanLeino merged commit d3efcc2 into dafny-lang:master Aug 3, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants