Rust: Address PR comments

This commit is contained in:
Simon Friis Vindum
2024-10-28 15:15:38 +01:00
parent cab916453d
commit 8f8564ddfd

View File

@@ -155,7 +155,7 @@ private predicate variableReadActual(BasicBlock bb, int i, Variable v) {
*/
pragma[noinline]
private predicate hasCapturedWrite(Variable v, Cfg::CfgScope scope) {
any(VariableWriteAccess write | write.getVariable() = v and scope = write.getEnclosingCallable*())
any(VariableWriteAccess write | write.getVariable() = v and scope = write.getEnclosingCallable+())
.isCapture()
}
@@ -262,7 +262,7 @@ private predicate readsCapturedVariable(BasicBlock bb, Variable v) {
*/
pragma[noinline]
private predicate hasCapturedRead(Variable v, Cfg::CfgScope scope) {
any(VariableReadAccess read | read.getVariable() = v and scope = read.getEnclosingCallable*())
any(VariableReadAccess read | read.getVariable() = v and scope = read.getEnclosingCallable+())
.isCapture()
}
@@ -290,6 +290,19 @@ private predicate capturedCallRead(CallExprBase call, BasicBlock bb, int i, Vari
)
}
/**
* Holds if the call `call` at index `i` in basic block `bb` may reach a callable
* that writes captured variable `v`.
*/
predicate capturedCallWrite(CallExprBase call, BasicBlock bb, int i, Variable v) {
call = bb.getNode(i).getAstNode() and
exists(Cfg::CfgScope scope |
hasVariableReadWithCapturedWrite(bb, any(int j | j > i), v, scope)
or
hasVariableReadWithCapturedWrite(bb.getASuccessor+(), _, v, scope)
)
}
/**
* Holds if a pseudo read of captured variable `v` should be inserted
* at index `i` in exit block `bb`.
@@ -312,20 +325,6 @@ private module Cached {
i = -1
}
/**
* Holds if the call `call` at index `i` in basic block `bb` may reach a callable
* that writes captured variable `v`.
*/
cached
predicate capturedCallWrite(CallExprBase call, BasicBlock bb, int i, Variable v) {
call = bb.getNode(i).getAstNode() and
exists(Cfg::CfgScope scope |
hasVariableReadWithCapturedWrite(bb, any(int j | j > i), v, scope)
or
hasVariableReadWithCapturedWrite(bb.getASuccessor+(), _, v, scope)
)
}
/**
* Holds if `v` is written at index `i` in basic block `bb`, and the corresponding
* AST write access is `write`.