Rust: Implement ConditionalCompletionSplitting

rust/ql/consistency-queries/CfgConsistency.ql

@@ -12,8 +12,6 @@ query predicate nonPostOrderExpr(Expr e, string cls) {
   cls = e.getPrimaryQlClasses() and
   not e instanceof LetExpr and
   not e instanceof ParenExpr and
-  not e instanceof LogicalAndExpr and // todo
-  not e instanceof LogicalOrExpr and
   exists(AstNode last, Completion c |
     CfgImpl::last(e, last, c) and
     last != e and

rust/ql/lib/codeql/rust/controlflow/internal/Completion.qll

@@ -63,10 +63,8 @@ abstract class ConditionalCompletion extends NormalCompletion {
 }
 
 /** Holds if node `n` has the Boolean constant value `value`. */
-private predicate isBooleanConstant(AstNode n, Boolean value) {
-  n.(LiteralExpr).getTextValue() = value.toString()
-  or
-  isBooleanConstant(n.(ParenExpr).getExpr(), value)
+private predicate isBooleanConstant(LiteralExpr le, Boolean value) {
+  le.getTextValue() = value.toString()
 }
 
 /**
@@ -83,29 +81,22 @@ class BooleanCompletion extends ConditionalCompletion, TBooleanCompletion {
     or
     any(MatchGuard guard).getCondition() = e
     or
-    exists(BinaryExpr expr |
-      expr.getOperatorName() = ["&&", "||"] and
-      e = expr.getLhs()
-    )
+    e = any(BinaryLogicalOperation blo).getLhs()
     or
     exists(Expr parent | this.isValidForSpecific0(parent) |
       e = parent.(ParenExpr).getExpr()
       or
-      parent =
-        any(PrefixExpr expr |
-          expr.getOperatorName() = "!" and
-          e = expr.getExpr()
-        )
+      e = parent.(LogicalNotExpr).getExpr()
       or
-      parent =
-        any(BinaryExpr expr |
-          expr.getOperatorName() = ["&&", "||"] and
-          e = expr.getRhs()
-        )
+      e = parent.(BinaryLogicalOperation).getRhs()
       or
       parent = any(IfExpr ie | e = [ie.getThen(), ie.getElse()])
       or
-      parent = any(BlockExpr be | e = be.getStmtList().getTailExpr())
+      e = parent.(MatchExpr).getAnArm().getExpr()
+      or
+      e = parent.(BlockExpr).getStmtList().getTailExpr()
+      or
+      e = any(BreakExpr be | be.getTarget() = parent).getExpr()
     )
   }
 

rust/ql/lib/codeql/rust/controlflow/internal/ControlFlowGraphImpl.qll

@@ -44,9 +44,6 @@ private module CfgInput implements InputSig<Location> {
   /** Hold if `t` represents a conditional successor type. */
   predicate successorTypeIsCondition(SuccessorType t) { t instanceof Cfg::BooleanSuccessor }
 
-  /** Gets the maximum number of splits allowed for a given node. */
-  int maxSplits() { result = 0 }
-
   /** Holds if `first` is first executed when entering `scope`. */
   predicate scopeFirst(CfgScope scope, AstNode first) { scope.scopeFirst(first) }
 
@@ -86,53 +83,49 @@ class BinaryOpExprTree extends StandardPostOrderTree instanceof BinaryExpr {
   }
 }
 
-class LogicalOrBinaryOpExprTree extends PreOrderTree, LogicalOrExpr {
+class LogicalOrTree extends PostOrderTree, LogicalOrExpr {
   final override predicate propagatesAbnormal(AstNode child) { child = this.getAnOperand() }
 
+  override predicate first(AstNode node) { first(this.getLhs(), node) }
+
   override predicate succ(AstNode pred, AstNode succ, Completion c) {
-    // Edge to the first node in the lhs
-    pred = this and
-    first(this.getLhs(), succ) and
-    completionIsSimple(c)
+    // Edge from lhs to rhs
+    last(this.getLhs(), pred, c) and
+    c.(BooleanCompletion).failed() and
+    first(this.getRhs(), succ)
     or
-    // Edge from the last node in the lhs to the first node in the rhs
+    // Edge from lhs to this
     last(this.getLhs(), pred, c) and
-    first(this.getRhs(), succ) and
-    c.(BooleanCompletion).failed()
-  }
-
-  override predicate last(AstNode node, Completion c) {
-    // Lhs. as the last node
-    last(this.getLhs(), node, c) and
-    c.(BooleanCompletion).succeeded()
+    c.(BooleanCompletion).succeeded() and
+    succ = this
     or
-    // Rhs. as the last node
-    last(this.getRhs(), node, c)
+    // Edge from rhs to this
+    last(this.getRhs(), pred, c) and
+    succ = this and
+    completionIsNormal(c)
   }
 }
 
-class LogicalAndBinaryOpExprTree extends PreOrderTree, LogicalAndExpr {
+class LogicalAndTree extends PostOrderTree, LogicalAndExpr {
   final override predicate propagatesAbnormal(AstNode child) { child = this.getAnOperand() }
 
+  override predicate first(AstNode node) { first(this.getLhs(), node) }
+
   override predicate succ(AstNode pred, AstNode succ, Completion c) {
-    // Edge to the first node in the lhs
-    pred = this and
-    first(this.getLhs(), succ) and
-    completionIsSimple(c)
+    // Edge from lhs to rhs
+    last(this.getLhs(), pred, c) and
+    c.(BooleanCompletion).succeeded() and
+    first(this.getRhs(), succ)
     or
-    // Edge from the last node in the lhs to the first node in the rhs
+    // Edge from lhs to this
     last(this.getLhs(), pred, c) and
-    first(this.getRhs(), succ) and
-    c.(BooleanCompletion).succeeded()
-  }
-
-  override predicate last(AstNode node, Completion c) {
-    // Lhs. as the last node
-    last(this.getLhs(), node, c) and
-    c.(BooleanCompletion).failed()
+    c.(BooleanCompletion).failed() and
+    succ = this
     or
-    // Rhs. as the last node
-    last(this.getRhs(), node, c)
+    // Edge from rhs to this
+    last(this.getRhs(), pred, c) and
+    succ = this and
+    completionIsNormal(c)
   }
 }
 

rust/ql/lib/codeql/rust/controlflow/internal/Splitting.qll

@@ -1,17 +1,118 @@
+private import rust
+private import Completion
+private import ControlFlowGraphImpl
+private import Scope
+
 cached
 private module Cached {
-  // Not using CFG splitting, so the following are just placeholder types.
   cached
-  newtype TSplitKind = TSplitKindUnit()
+  newtype TSplitKind = TConditionalCompletionSplitKind()
 
   cached
-  newtype TSplit = TSplitUnit()
+  newtype TSplit = TConditionalCompletionSplit(ConditionalCompletion c)
 }
 
 import Cached
 
 /** A split for a control flow node. */
-class Split extends TSplit {
+abstract private class Split_ extends TSplit {
   /** Gets a textual representation of this split. */
-  string toString() { none() }
+  abstract string toString();
+}
+
+final class Split = Split_;
+
+private module ConditionalCompletionSplitting {
+  /**
+   * A split for conditional completions. For example, in
+   *
+   * ```rust
+   * if x && !y {
+   *   // ...
+   * }
+   * ```
+   *
+   * we record whether `x`, `y`, and `!y` evaluate to `true` or `false`, and restrict
+   * the edges out of `!y` and `x && !y` accordingly.
+   */
+  class ConditionalCompletionSplit extends Split_, TConditionalCompletionSplit {
+    ConditionalCompletion completion;
+
+    ConditionalCompletionSplit() { this = TConditionalCompletionSplit(completion) }
+
+    override string toString() { result = completion.toString() }
+  }
+
+  private class ConditionalCompletionSplitKind extends SplitKind, TConditionalCompletionSplitKind {
+    override int getListOrder() { result = 0 }
+
+    override predicate isEnabled(AstNode cfe) { this.appliesTo(cfe) }
+
+    override string toString() { result = "ConditionalCompletion" }
+  }
+
+  int getNextListOrder() { result = 1 }
+
+  private class ConditionalCompletionSplitImpl extends SplitImpl instanceof ConditionalCompletionSplit
+  {
+    ConditionalCompletion completion;
+
+    ConditionalCompletionSplitImpl() { this = TConditionalCompletionSplit(completion) }
+
+    override ConditionalCompletionSplitKind getKind() { any() }
+
+    override predicate hasEntry(AstNode pred, AstNode succ, Completion c) {
+      succ(pred, succ, c) and
+      last(succ, _, completion) and
+      (
+        last(succ.(LogicalNotExpr).getExpr(), pred, c) and
+        completion.(BooleanCompletion).getDual() = c
+        or
+        last(succ.(BinaryLogicalOperation).getAnOperand(), pred, c) and
+        completion = c
+        or
+        succ =
+          any(IfExpr ie |
+            last([ie.getThen(), ie.getElse()], pred, c) and
+            completion = c
+          )
+        or
+        last(succ.(MatchExpr).getAnArm().getExpr(), pred, c) and
+        completion = c
+        or
+        last(succ.(BlockExpr).getStmtList().getTailExpr(), pred, c) and
+        completion = c
+      )
+      or
+      succ(pred, succ, c) and
+      last(succ.(BreakExpr).getExpr(), pred, c) and
+      exists(AstNode target |
+        succ(succ, target, _) and
+        last(target, _, completion)
+      ) and
+      completion = c
+    }
+
+    override predicate hasEntryScope(CfgScope scope, AstNode first) { none() }
+
+    override predicate hasExit(AstNode pred, AstNode succ, Completion c) {
+      this.appliesTo(pred) and
+      succ(pred, succ, c) and
+      if c instanceof ConditionalCompletion
+      then completion = c
+      else not this.hasSuccessor(pred, succ, c)
+    }
+
+    override predicate hasExitScope(CfgScope scope, AstNode last, Completion c) {
+      this.appliesTo(last) and
+      scope.scopeLast(last, c) and
+      if c instanceof ConditionalCompletion then completion = c else any()
+    }
+
+    override predicate hasSuccessor(AstNode pred, AstNode succ, Completion c) {
+      this.appliesTo(pred) and
+      succ(pred, succ, c) and
+      not c instanceof ConditionalCompletion
+    }
+  }
 }