Rust: SSA additions

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

@@ -49,24 +49,20 @@ module SsaInput implements SsaImplCommon::InputSig<Location> {
   /**
    * A variable amenable to SSA construction.
    *
-   * All immutable variables are amenable. Mutable variables are restricted
-   * to those that are not captured by closures, and are not borrowed
-   * (either explicitly using `& mut`, or (potentially) implicit as borrowed
-   * receivers in a method call).
+   * All immutable variables are amenable. Mutable variables are restricted to
+   * those that are not borrowed (either explicitly using `& mut`, or
+   * (potentially) implicit as borrowed receivers in a method call).
    */
   class SourceVariable extends Variable {
     SourceVariable() {
-      this.isImmutable()
-      or
-      this.isMutable() and
-      not this.isCaptured() and
-      forall(VariableAccess va | va = this.getAnAccess() |
-        va instanceof VariableReadAccess and
+      this.isMutable()
+      implies
+      not exists(VariableAccess va | va = this.getAnAccess() |
+        exists(RefExpr re | va = re.getExpr() and re.isMut())
+        or
         // receivers can be borrowed implicitly, cf.
         // https://doc.rust-lang.org/reference/expressions/method-call-expr.html
-        not va = any(MethodCallExpr mce).getReceiver()
-        or
-        variableWrite(va, this)
+        va = any(MethodCallExpr mce).getReceiver()
       )
     }
   }
@@ -102,6 +98,8 @@ module SsaInput implements SsaImplCommon::InputSig<Location> {
       v = va.getVariable() and
       certain = false
     )
+    or
+    capturedExitRead(bb, i, v) and certain = false
   }
 }
 
@@ -207,14 +205,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) {
+  result = bb.getANode().getAstNode() and
+  result.isCapture() and
+  result.getVariable() = v
+}
+
+/** Holds if `bb` contains a captured write to variable `v`. */
+pragma[noinline]
+private predicate writesCapturedVariable(BasicBlock bb, Variable v) {
+  getCapturedVariableAccess(bb, v) instanceof VariableWriteAccess
+}
+
+/** Holds if `bb` contains a captured read to variable `v`. */
 pragma[nomagic]
-private predicate hasCapturedVariableAccess(BasicBlock bb, Variable v) {
-  exists(VariableAccess read |
-    read = bb.getANode().getAstNode() and
-    read.isCapture() and
-    read.getVariable() = v
-  )
+private predicate readsCapturedVariable(BasicBlock bb, Variable v) {
+  getCapturedVariableAccess(bb, v) instanceof VariableReadAccess
+}
+
+/**
+ * Holds if a pseudo read of captured variable `v` should be inserted
+ * at index `i` in exit block `bb`.
+ */
+private predicate capturedExitRead(AnnotatedExitBasicBlock bb, int i, Variable v) {
+  bb.isNormal() and
+  writesCapturedVariable(bb.getAPredecessor*(), v) and
+  i = bb.length()
 }
 
 cached
@@ -225,7 +241,7 @@ private module Cached {
    */
   cached
   predicate capturedEntryWrite(EntryBasicBlock bb, int i, Variable v) {
-    hasCapturedVariableAccess(bb.getASuccessor*(), v) and
+    readsCapturedVariable(bb.getASuccessor*(), v) and
     i = -1
   }