Rust: Handle calls that might read/write variables through closures

This implementation is copied and adapted from the Ruby SSA
implementation.

Author: paldepind

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

@@ -74,6 +74,8 @@ module SsaInput implements SsaImplCommon::InputSig<Location> {
       capturedEntryWrite(bb, i, v)
     ) and
     certain = true
+    or
+    capturedCallWrite(_, bb, i, v) and certain = false
   }
 
   predicate variableRead(BasicBlock bb, int i, SourceVariable v, boolean certain) {
@@ -99,6 +101,8 @@ module SsaInput implements SsaImplCommon::InputSig<Location> {
       certain = false
     )
     or
+    capturedCallRead(_, bb, i, v) and certain = false
+    or
     capturedExitRead(bb, i, v) and certain = false
   }
 }
@@ -145,6 +149,35 @@ private predicate variableReadActual(BasicBlock bb, int i, Variable v) {
   )
 }
 
+/**
+ * Holds if captured variable `v` is written directly inside `scope`,
+ * or inside a (transitively) nested scope of `scope`.
+ */
+pragma[noinline]
+private predicate hasCapturedWrite(Variable v, Cfg::CfgScope scope) {
+  any(VariableWriteAccess write | write.getVariable() = v and scope = write.getEnclosingCallable*())
+      .isCapture()
+}
+
+/**
+ * Holds if `v` is read inside basic block `bb` at index `i`, which is in the
+ * immediate outer scope of `scope`.
+ */
+pragma[noinline]
+private predicate variableReadActualInOuterScope(
+  BasicBlock bb, int i, Variable v, Cfg::CfgScope scope
+) {
+  variableReadActual(bb, i, v) and bb.getScope() = scope.getEnclosingCallable()
+}
+
+pragma[noinline]
+private predicate hasVariableReadWithCapturedWrite(
+  BasicBlock bb, int i, Variable v, Cfg::CfgScope scope
+) {
+  hasCapturedWrite(v, scope) and
+  variableReadActualInOuterScope(bb, i, v, scope)
+}
+
 private predicate adjacentDefReachesRead(
   Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2
 ) {
@@ -223,6 +256,40 @@ private predicate readsCapturedVariable(BasicBlock bb, Variable v) {
   getCapturedVariableAccess(bb, v) instanceof VariableReadAccess
 }
 
+/**
+ * Holds if captured variable `v` is read directly inside `scope`,
+ * or inside a (transitively) nested scope of `scope`.
+ */
+pragma[noinline]
+private predicate hasCapturedRead(Variable v, Cfg::CfgScope scope) {
+  any(VariableReadAccess read | read.getVariable() = v and scope = read.getEnclosingCallable*())
+      .isCapture()
+}
+
+/**
+ * Holds if `v` is written inside basic block `bb` at index `i`, which is in
+ * the immediate outer scope of `scope`.
+ */
+pragma[noinline]
+private predicate variableWriteInOuterScope(BasicBlock bb, int i, Variable v, Cfg::CfgScope scope) {
+  SsaInput::variableWrite(bb, i, v, _) and scope.getEnclosingCallable() = bb.getScope()
+}
+
+/**
+ * Holds if the call `call` at index `i` in basic block `bb` may reach
+ * a callable that reads captured variable `v`.
+ */
+private predicate capturedCallRead(CallExprBase call, BasicBlock bb, int i, Variable v) {
+  exists(Cfg::CfgScope scope |
+    hasCapturedRead(v, scope) and
+    (
+      variableWriteInOuterScope(bb, any(int j | j < i), v, scope) or
+      variableWriteInOuterScope(bb.getAPredecessor+(), _, v, scope)
+    ) and
+    call = bb.getNode(i).getAstNode()
+  )
+}
+
 /**
  * Holds if a pseudo read of captured variable `v` should be inserted
  * at index `i` in exit block `bb`.
@@ -245,6 +312,20 @@ 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`.

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

@@ -120,6 +120,7 @@ definition
 | variables.rs:418:9:418:13 | y | variables.rs:418:13:418:13 | y |
 | variables.rs:420:9:420:20 | closure2 | variables.rs:420:13:420:20 | closure2 |
 | variables.rs:421:9:421:9 | y | variables.rs:418:13:418:13 | y |
+| variables.rs:423:5:423:14 | CallExpr | variables.rs:418:13:418:13 | y |
 | variables.rs:428:9:428:20 | closure3 | variables.rs:428:13:428:20 | closure3 |
 | variables.rs:435:8:435:8 | b | variables.rs:435:8:435:8 | b |
 | variables.rs:436:9:436:13 | x | variables.rs:436:13:436:13 | x |
@@ -233,8 +234,8 @@ read
 | variables.rs:410:9:410:13 | x | variables.rs:410:13:410:13 | x | variables.rs:416:15:416:15 | x |
 | 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 |
 | variables.rs:420:9:420:20 | closure2 | variables.rs:420:13:420:20 | closure2 | variables.rs:423:5:423:12 | closure2 |
+| variables.rs:423:5:423:14 | CallExpr | variables.rs:418:13:418:13 | y | variables.rs:424:15:424:15 | y |
 | variables.rs:428:9:428:20 | closure3 | variables.rs:428:13:428:20 | closure3 | variables.rs:431:5:431:12 | closure3 |
 | variables.rs:435:8:435:8 | b | variables.rs:435:8:435:8 | b | variables.rs:439:8:439:8 | b |
 | variables.rs:436:9:436:13 | x | variables.rs:436:13:436:13 | x | variables.rs:437:15:437:15 | x |
@@ -335,8 +336,8 @@ firstRead
 | variables.rs:410:9:410:13 | x | variables.rs:410:13:410:13 | x | variables.rs:416:15:416:15 | x |
 | 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 |
 | variables.rs:420:9:420:20 | closure2 | variables.rs:420:13:420:20 | closure2 | variables.rs:423:5:423:12 | closure2 |
+| variables.rs:423:5:423:14 | CallExpr | variables.rs:418:13:418:13 | y | variables.rs:424:15:424:15 | y |
 | variables.rs:428:9:428:20 | closure3 | variables.rs:428:13:428:20 | closure3 | variables.rs:431:5:431:12 | closure3 |
 | variables.rs:435:8:435:8 | b | variables.rs:435:8:435:8 | b | variables.rs:439:8:439:8 | b |
 | variables.rs:436:9:436:13 | x | variables.rs:436:13:436:13 | x | variables.rs:437:15:437:15 | x |
@@ -433,8 +434,8 @@ lastRead
 | variables.rs:410:9:410:13 | x | variables.rs:410:13:410:13 | x | variables.rs:416:15:416:15 | x |
 | 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 |
 | variables.rs:420:9:420:20 | closure2 | variables.rs:420:13:420:20 | closure2 | variables.rs:423:5:423:12 | closure2 |
+| variables.rs:423:5:423:14 | CallExpr | variables.rs:418:13:418:13 | y | variables.rs:424:15:424:15 | y |
 | variables.rs:428:9:428:20 | closure3 | variables.rs:428:13:428:20 | closure3 | variables.rs:431:5:431:12 | closure3 |
 | variables.rs:435:8:435:8 | b | variables.rs:435:8:435:8 | b | variables.rs:439:8:439:8 | b |
 | variables.rs:436:9:436:13 | x | variables.rs:436:13:436:13 | x | variables.rs:438:15:438:15 | x |