-
Notifications
You must be signed in to change notification settings - Fork 1.6k
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
Rust: SSA additions #17786
Rust: SSA additions #17786
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.
Great to have the SSA analysis apply to more cases!
We need a bit more work, though, to make the analysis sound for captured mutable variables.
| variables.rs:412:9:412:16 | closure1 | variables.rs:412:9:412:16 | closure1 | variables.rs:415:5:415:12 | closure1 | | ||
| variables.rs:412:20:414:5 | <captured entry> x | variables.rs:410:13:410:13 | x | variables.rs:413:19:413:19 | x | | ||
| variables.rs:418:9:418:13 | y | variables.rs:418:13:418:13 | y | variables.rs:424:15:424:15 | y | |
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 line illustrates the problem with allowing for captured mutable variables: The test snippet is
let mut y = 2; // y [line 418]
// Captures mutable value by mutable reference
let mut closure2 = || {
y = 3; // $ write_access=y
};
closure2(); // $ read_access=closure2
print_i64(y); // $ read_access=y [line 424]
It is not true that the value written at line 418 is the one read at line 424, because the value is updated in the call to closure2
.
One way that we can fix it is to say that mutable captured variables may be read/written via any call, by adding uncertain pseudo reads and writes at all call nodes. In Ruby this is done in the predicates
capturedCallRead
and capturedCallWrite
, respectively.
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.
That makes sense and I did not think of that. I'll look at the Ruby approach and try an adapt it.
@@ -207,14 +207,32 @@ private predicate lastRefSkipUncertainReadsExt(DefinitionExt def, BasicBlock bb, | |||
) | |||
} | |||
|
|||
/** Holds if `bb` contains a captured access to variable `v`. */ | |||
private VariableAccess getCapturedVariableAccess(BasicBlock bb, Variable v) { |
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.
Nit: getACapturedVariableAccess
.
this.isMutable() | ||
implies | ||
not exists(VariableAccess va | va = this.getAnAccess() | | ||
exists(RefExpr re | va = re.getExpr() and re.isMut()) |
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.
Nit: I prefer va = any(RefExpr re | re.isMut()).getExpr()
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.
Thanks. That is definitely nicer.
This implementation is copied and adapted from the Ruby SSA implementation.
I've updated the PR to address comment and to handle captured variables in the same way as in Ruby. This fixes the error that was previously pointed out. I think the way Ruby detects when a call can write/read might have a small soundness problem. Consider this example: fn mutable_capture_and_write_in_a_sibling_closure() {
let mut y = 2; // y
let mut closure1 = || { y = 3; };
let mut closure2 = || {
y = 2; // (1): SSA definition for `y`
closure1(); // no SSA definition for `y` here
print_i64(y); // (2): reads from (1) which is not correct
};
closure2();
print_i64(y);
} Here the read at The above example doesn't actually compile due to Rust's borrow checker (which I didn't realize at first). When one closure ( To fix the above and improve precision, we could say that a call might write to a variable
This should fix the above problem and also make the check more control flow sensitive in examples such as the following: fn mutable_capture_further_down_in_the_cfg() {
let mut y = 2;
print_i64(y); // (1): This call can not write to `y` as the capturing closure is not yet in scope
let mut closure = || { y = 3; // $ write_access=y };
closure();
print_i64(y);
} In this example the current analysis will conclude that the call at |
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.
A few minor comments, otherwise LGTM. We should also do a DCA run before merging.
*/ | ||
pragma[noinline] | ||
private predicate hasCapturedWrite(Variable v, Cfg::CfgScope scope) { | ||
any(VariableWriteAccess write | write.getVariable() = v and scope = write.getEnclosingCallable*()) |
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 be getEnclosingCallable+
.
*/ | ||
pragma[noinline] | ||
private predicate hasCapturedRead(Variable v, Cfg::CfgScope scope) { | ||
any(VariableReadAccess read | read.getVariable() = v and scope = read.getEnclosingCallable*()) |
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.
Same
* that writes captured variable `v`. | ||
*/ | ||
cached | ||
predicate capturedCallWrite(CallExprBase call, BasicBlock bb, int i, Variable v) { |
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.
There should be no need to cache this.
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 I just remove the cached
annotation or should I also move it out of the Cached
module?
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 Ruby equivalent is also cached. Is there something different about that one that causes it to need caching?
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.
It needs to be moved out, otherwise the compiler will complain (all public declarations in a cached
module must be marked as cached
).
The reason why it is cached in Ruby is that it is referenced in a user-visible class.
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 see, thanks. I've addressed the comments :)
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.
LGTM. Let's wait for DCA (I have started a run) before merging.
DCA looks fine to me. |
It's not very important right now, but I wonder what you think about #17786 (comment) @hvitved? |
I think you are right that it may be unsound, but it is probably not something that is likely to happen often in practice. |
This PR makes two small improvements to the SSA:
Mutable variables that are captured are now supported. Immutable variables where already supported. I don't think allowing mutable variables as well pose much of a problem, as they don't introduce the same issues that mutable borrows do.
The only change I made to support this was to insert pseudo reads upon exit from a closure where captured variables are written to, which I observed was done in the Ruby SSA implementation. There might be other necessary changes that I've missed, so please double check 🙏
Mutable variables are now only excluded from SSA when they are mutably borrowed (
&mut
) whereas before merely immutably borrowing them (&
) excluded them. I don't think immutable borrows pose any problems for the SSA construction.