-
Notifications
You must be signed in to change notification settings - Fork 266
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
Conversation
dac8db1
to
aa4d478
Compare
It seems that in |
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 |
@RustanLeino Should the type parameters for ghost component show up in the target language of the dafny compilation? Consider the Now, consider the
|
@fpoli Very good points. It would not be correct (in general) to remove the type parameter of user-defined datatypes like 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. |
fbb6785
to
240357a
Compare
0c5d68e
to
6f3a658
Compare
@RustanLeino I addressed the review and rebased on master. |
The CI failure of the "Create release" step looks like a glitch:
I'll force-push to restart the tests. |
Based on secure-foundations@c511546, authored by Chris-Hawblitzel.
Co-authored-by: Rustan Leino <[email protected]>
Co-authored-by: Rustan Leino <[email protected]>
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); |
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 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.
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 agree, on both accounts.
@@ -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) { |
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 ttd.Dims == 2
still be in 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.
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.
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'm actually not sure how to observe a difference in the verification time of Dafny. It's a suggestion that I got from Rustan.
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 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;
}
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'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) { |
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 ttd.Dims == 2
still be in 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.
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.
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 ttd.Dims == 2 && ttd.NonGhostDims == 2
is correct. See this message in the other conversation.
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 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.
@RustanLeino I fixed the equality support check and added the following test
|
This PR adds support for tuples with ghost components. In addition to secure-foundations@c511546, authored by @Chris-Hawblitzel, the major changes are:
ghost
keyword is not allowed in the patterns of match statements.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)
.ghost
keyword is pretty-printed.