Rust: Make logical operator pre order nodes and eliminate impossible paths in CFG

Author: paldepind

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

@@ -67,7 +67,10 @@ class BooleanCompletion extends ConditionalCompletion, TBooleanCompletion {
   override predicate isValidForSpecific(AstNode e) {
     e = any(IfExpr c).getCondition()
     or
-    exists(BinaryOpExpr expr | expr.getOp() = ["&&", "||"] and expr.getLhs() = e)
+    exists(BinaryOpExpr expr |
+      expr.getOp() = ["&&", "||"] and
+      e = [expr.getLhs(), expr.getRhs()]
+    )
   }
 
   /** Gets the dual Boolean completion. */

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

@@ -69,45 +69,63 @@ class BinaryOpExprTree extends StandardPostOrderTree instanceof BinaryOpExpr {
   }
 }
 
-class LogicalOrBinaryOpExprTree extends PostOrderTree instanceof BinaryOpExpr {
+class LogicalOrBinaryOpExprTree extends PreOrderTree instanceof BinaryOpExpr {
   LogicalOrBinaryOpExprTree() { super.getOp() = "||" }
 
   final override predicate propagatesAbnormal(AstNode child) {
     child = [super.getRhs(), super.getLhs()]
   }
 
-  override predicate first(AstNode node) { first(super.getLhs(), node) }
-
+  // override predicate first(AstNode node) { first(super.getLhs(), node) }
   override predicate succ(AstNode pred, AstNode succ, Completion c) {
+    // Edge to the first node in the lhs
+    pred = this and
+    first(super.getLhs(), succ) and
+    completionIsSimple(c)
+    or
+    // Edge from the last node in the lhs to the first node in the rhs
     last(super.getLhs(), pred, c) and
-    (
-      succ = this and c.(BooleanCompletion).getValue() = true
-      or
-      first(super.getRhs(), succ) and c.(BooleanCompletion).getValue() = false
-    )
+    first(super.getRhs(), succ) and
+    c.(BooleanCompletion).getValue() = false
+  }
+
+  override predicate last(AstNode node, Completion c) {
+    // Lhs. as the last node
+    last(super.getLhs(), node, c) and
+    c.(BooleanCompletion).getValue() = true
     or
-    last(super.getRhs(), pred, c) and succ = this
+    // Rhs. as the last node
+    last(super.getRhs(), node, c) // and
   }
 }
 
-class LogicalAndBinaryOpExprTree extends PostOrderTree instanceof BinaryOpExpr {
+class LogicalAndBinaryOpExprTree extends PreOrderTree instanceof BinaryOpExpr {
   LogicalAndBinaryOpExprTree() { super.getOp() = "&&" }
 
   final override predicate propagatesAbnormal(AstNode child) {
     child = [super.getRhs(), super.getLhs()]
   }
 
-  override predicate first(AstNode node) { first(super.getLhs(), node) }
-
+  // override predicate first(AstNode node) { first(super.getLhs(), node) }
   override predicate succ(AstNode pred, AstNode succ, Completion c) {
+    // Edge to the first node in the lhs
+    pred = this and
+    first(super.getLhs(), succ) and
+    completionIsSimple(c)
+    or
+    // Edge from the last node in the lhs to the first node in the rhs
     last(super.getLhs(), pred, c) and
-    (
-      succ = this and c.(BooleanCompletion).getValue() = false
-      or
-      first(super.getRhs(), succ) and c.(BooleanCompletion).getValue() = true
-    )
+    first(super.getRhs(), succ) and
+    c.(BooleanCompletion).getValue() = true
+  }
+
+  override predicate last(AstNode node, Completion c) {
+    // Lhs. as the last node
+    last(super.getLhs(), node, c) and
+    c.(BooleanCompletion).getValue() = false
     or
-    last(super.getRhs(), pred, c) and succ = this
+    // Rhs. as the last node
+    last(super.getRhs(), node, c)
   }
 }