Shared ConditionalSplitting implementation

Author: hvitved

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

@@ -7,7 +7,6 @@ private import codeql.rust.controlflow.ControlFlowGraph as Cfg
 private module CfgInput implements InputSig<Location> {
   private import rust as Rust
   private import Completion as C
-  private import Splitting as S
 
   class AstNode = Rust::AstNode;
 
@@ -24,10 +23,6 @@ private module CfgInput implements InputSig<Location> {
 
   CfgScope getCfgScope(AstNode n) { result = Scope::scopeOfAst(n) }
 
-  class SplitKindBase = S::TSplitKind;
-
-  class Split = S::Split;
-
   class SuccessorType = Cfg::SuccessorType;
 
   /** Gets a successor type that matches completion `c`. */
@@ -51,7 +46,22 @@ private module CfgInput implements InputSig<Location> {
   predicate scopeLast(CfgScope scope, AstNode last, Completion c) { scope.scopeLast(last, c) }
 }
 
-private module CfgImpl = Make<Location, CfgInput>;
+private module CfgSplittingInput implements SplittingInputSig<Location, CfgInput> {
+  private import Splitting as S
+
+  class SplitKindBase = S::TSplitKind;
+
+  class Split = S::Split;
+}
+
+private module ConditionalCompletionSplittingInput implements
+  ConditionalCompletionSplittingInputSig<Location, CfgInput, CfgSplittingInput>
+{
+  import Splitting::ConditionalCompletionSplitting::ConditionalCompletionSplittingInput
+}
+
+private module CfgImpl =
+  MakeWithSplitting<Location, CfgInput, CfgSplittingInput, ConditionalCompletionSplittingInput>;
 
 import CfgImpl
 

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

@@ -21,7 +21,7 @@ abstract private class Split_ extends TSplit {
 
 final class Split = Split_;
 
-private module ConditionalCompletionSplitting {
+module ConditionalCompletionSplitting {
   /**
    * A split for conditional completions. For example, in
    *
@@ -39,77 +39,77 @@ private module ConditionalCompletionSplitting {
 
     ConditionalCompletionSplit() { this = TConditionalCompletionSplit(completion) }
 
+    ConditionalCompletion getCompletion() { result = completion }
+
     override string toString() { result = completion.toString() }
   }
 
-  private class ConditionalCompletionSplitKind extends SplitKind, TConditionalCompletionSplitKind {
+  private class ConditionalCompletionSplitKind_ extends SplitKind, TConditionalCompletionSplitKind {
     override int getListOrder() { result = 0 }
 
     override predicate isEnabled(AstNode cfe) { this.appliesTo(cfe) }
 
     override string toString() { result = "ConditionalCompletion" }
   }
 
-  private class ConditionalCompletionSplitImpl extends SplitImpl instanceof ConditionalCompletionSplit
-  {
-    ConditionalCompletion completion;
+  module ConditionalCompletionSplittingInput {
+    private import Completion as Comp
 
-    ConditionalCompletionSplitImpl() { this = TConditionalCompletionSplit(completion) }
+    class ConditionalCompletion = Comp::ConditionalCompletion;
 
-    override ConditionalCompletionSplitKind getKind() { any() }
+    class ConditionalCompletionSplitKind extends ConditionalCompletionSplitKind_, TSplitKind { }
 
-    override predicate hasEntry(AstNode pred, AstNode succ, Completion c) {
-      succ(pred, succ, c) and
-      last(succ, _, completion) and
+    class ConditionalCompletionSplit = ConditionalCompletionSplitting::ConditionalCompletionSplit;
+
+    bindingset[parent, parentCompletion]
+    predicate condPropagateExpr(
+      AstNode parent, ConditionalCompletion parentCompletion, AstNode child,
+      ConditionalCompletion childCompletion
+    ) {
+      child = parent.(LogicalNotExpr).getExpr() and
+      childCompletion.getDual() = parentCompletion
+      or
+      childCompletion = parentCompletion and
       (
-        last(succ.(LogicalNotExpr).getExpr(), pred, c) and
-        completion.(BooleanCompletion).getDual() = c
-        or
-        last(succ.(BinaryLogicalOperation).getAnOperand(), pred, c) and
-        completion = c
+        child = parent.(BinaryLogicalOperation).getAnOperand()
         or
-        succ =
-          any(IfExpr ie |
-            last([ie.getThen(), ie.getElse()], pred, c) and
-            completion = c
-          )
+        parent = any(IfExpr ie | child = [ie.getThen(), ie.getElse()])
         or
-        last(succ.(MatchExpr).getAnArm().getExpr(), pred, c) and
-        completion = c
+        child = parent.(MatchExpr).getAnArm().getExpr()
         or
-        last(succ.(BlockExpr).getStmtList().getTailExpr(), pred, c) and
-        completion = c
+        child = parent.(BlockExpr).getStmtList().getTailExpr()
       )
-      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)
+  private class ConditionalCompletionSplitImpl extends SplitImplementations::ConditionalCompletionSplitting::ConditionalCompletionSplitImpl
+  {
+    /**
+     * Gets a `break` expression whose target can have a Boolean completion that
+     * matches this split.
+     */
+    private BreakExpr getABreakExpr(Expr target) {
+      target = result.getTarget() and
+      last(target, _, this.getCompletion())
     }
 
-    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 hasEntry(AstNode pred, AstNode succ, Completion c) {
+      super.hasEntry(pred, succ, c)
+      or
+      succ(pred, succ, c) and
+      last(succ.(BreakExpr).getExpr(), pred, c) and
+      succ = this.getABreakExpr(_) and
+      c = this.getCompletion()
     }
 
     override predicate hasSuccessor(AstNode pred, AstNode succ, Completion c) {
+      super.hasSuccessor(pred, succ, c)
+      or
       this.appliesTo(pred) and
       succ(pred, succ, c) and
-      not c instanceof ConditionalCompletion
+      pred = this.getABreakExpr(succ)
     }
   }
+
+  int getNextListOrder() { result = 1 }
 }