Merge pull request #19916 from hvitved/rust/fix-capture-inconsistencies

Rust: Fix variable capture inconsistencies
This commit is contained in:
Tom Hvitved
2025-06-30 14:18:00 +02:00
committed by GitHub
5 changed files with 28 additions and 41 deletions

View File

@@ -910,7 +910,11 @@ module VariableCapture {
CapturedVariable v;
VariableRead() {
exists(VariableReadAccess read | this.getExpr() = read and v = read.getVariable())
exists(VariableAccess read | this.getExpr() = read and v = read.getVariable() |
read instanceof VariableReadAccess
or
read = any(RefExpr re).getExpr()
)
}
CapturedVariable getVariable() { result = v }

View File

@@ -38,6 +38,22 @@ predicate variableWrite(AstNode write, Variable v) {
)
}
private predicate variableReadCertain(BasicBlock bb, int i, VariableAccess va, Variable v) {
bb.getNode(i).getAstNode() = va and
va = v.getAnAccess() and
(
va instanceof VariableReadAccess
or
// For immutable variables, we model a read when they are borrowed
// (although the actual read happens later, if at all).
va = any(RefExpr re).getExpr()
or
// Although compound assignments, like `x += y`, may in fact not read `x`,
// it makes sense to treat them as such
va = any(CompoundAssignmentExpr cae).getLhs()
)
}
module SsaInput implements SsaImplCommon::InputSig<Location> {
class BasicBlock = BasicBlocks::BasicBlock;
@@ -66,20 +82,7 @@ module SsaInput implements SsaImplCommon::InputSig<Location> {
}
predicate variableRead(BasicBlock bb, int i, SourceVariable v, boolean certain) {
exists(VariableAccess va |
bb.getNode(i).getAstNode() = va and
va = v.getAnAccess()
|
va instanceof VariableReadAccess
or
// For immutable variables, we model a read when they are borrowed
// (although the actual read happens later, if at all).
va = any(RefExpr re).getExpr()
or
// Although compound assignments, like `x += y`, may in fact not read `x`,
// it makes sense to treat them as such
va = any(CompoundAssignmentExpr cae).getLhs()
) and
variableReadCertain(bb, i, _, v) and
certain = true
or
capturedCallRead(_, bb, i, v) and certain = false
@@ -100,16 +103,6 @@ class PhiDefinition = Impl::PhiNode;
module Consistency = Impl::Consistency;
/** Holds if `v` is read at index `i` in basic block `bb`. */
private predicate variableReadActual(BasicBlock bb, int i, Variable v) {
exists(VariableAccess read |
read instanceof VariableReadAccess or read = any(RefExpr re).getExpr()
|
read.getVariable() = v and
read = bb.getNode(i).getAstNode()
)
}
/**
* Holds if captured variable `v` is written directly inside `scope`,
* or inside a (transitively) nested scope of `scope`.
@@ -125,10 +118,10 @@ private predicate hasCapturedWrite(Variable v, Cfg::CfgScope scope) {
* immediate outer CFG scope of `scope`.
*/
pragma[noinline]
private predicate variableReadActualInOuterScope(
private predicate variableReadCertainInOuterScope(
BasicBlock bb, int i, Variable v, Cfg::CfgScope scope
) {
variableReadActual(bb, i, v) and bb.getScope() = scope.getEnclosingCfgScope()
variableReadCertain(bb, i, _, v) and bb.getScope() = scope.getEnclosingCfgScope()
}
pragma[noinline]
@@ -136,7 +129,7 @@ private predicate hasVariableReadWithCapturedWrite(
BasicBlock bb, int i, Variable v, Cfg::CfgScope scope
) {
hasCapturedWrite(v, scope) and
variableReadActualInOuterScope(bb, i, v, scope)
variableReadCertainInOuterScope(bb, i, v, scope)
}
private VariableAccess getACapturedVariableAccess(BasicBlock bb, Variable v) {
@@ -154,7 +147,7 @@ private predicate writesCapturedVariable(BasicBlock bb, Variable v) {
/** Holds if `bb` contains a captured read to variable `v`. */
pragma[nomagic]
private predicate readsCapturedVariable(BasicBlock bb, Variable v) {
getACapturedVariableAccess(bb, v) instanceof VariableReadAccess
variableReadCertain(_, _, getACapturedVariableAccess(bb, v), _)
}
/**
@@ -254,7 +247,7 @@ private module Cached {
CfgNode getARead(Definition def) {
exists(Variable v, BasicBlock bb, int i |
Impl::ssaDefReachesRead(v, def, bb, i) and
variableReadActual(bb, i, v) and
variableReadCertain(bb, i, v.getAnAccess(), v) and
result = bb.getNode(i)
)
}

View File

@@ -255,6 +255,7 @@ read
| main.rs:355:14:355:14 | x | main.rs:355:14:355:14 | x | main.rs:356:13:356:13 | x |
| main.rs:362:9:362:9 | v | main.rs:362:9:362:9 | v | main.rs:365:12:365:12 | v |
| main.rs:364:9:364:12 | text | main.rs:364:9:364:12 | text | main.rs:366:19:366:22 | text |
| main.rs:371:13:371:13 | a | main.rs:371:13:371:13 | a | main.rs:372:5:372:5 | a |
| main.rs:372:5:372:5 | a | main.rs:371:13:371:13 | a | main.rs:373:15:373:15 | a |
| main.rs:372:5:372:5 | a | main.rs:371:13:371:13 | a | main.rs:374:11:374:11 | a |
| main.rs:374:6:374:11 | &mut a | main.rs:371:13:371:13 | a | main.rs:375:15:375:15 | a |

View File

@@ -1,6 +0,0 @@
readWithoutDef
| lifetime.rs:511:6:511:14 | my_local2 | lifetime.rs:514:9:527:2 | enter \|...\| ... | 2 |
| lifetime.rs:564:6:564:14 | my_local2 | lifetime.rs:567:9:580:2 | enter { ... } | 2 |
readWithoutPriorRef
| lifetime.rs:511:6:511:14 | my_local2 | lifetime.rs:514:9:527:2 | enter \|...\| ... | 2 |
| lifetime.rs:564:6:564:14 | my_local2 | lifetime.rs:567:9:580:2 | enter { ... } | 2 |

View File

@@ -1,5 +0,0 @@
variableIsCaptured
| lifetime.rs:511:6:511:14 | my_local2 | CapturedVariable is not captured |
| lifetime.rs:564:6:564:14 | my_local2 | CapturedVariable is not captured |
consistencyOverview
| CapturedVariable is not captured | 2 |