Rust: Fix variable capture inconsistencies

Author: hvitved

rust/ql/lib/codeql/rust/dataflow/internal/DataFlowImpl.qll

@@ -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 }

rust/ql/lib/codeql/rust/dataflow/internal/SsaImpl.qll

@@ -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,18 +118,18 @@ 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]
 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)
     )
   }

rust/ql/test/library-tests/variables/Ssa.expected

@@ -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 |