From fd83b6afdb6b34eeda8260846daec18b9ccdd070 Mon Sep 17 00:00:00 2001
From: Anders Schack-Mulligen <aschackmull@github.com>
Date: Tue, 11 Jul 2023 13:41:24 +0200
Subject: [PATCH] Dataflow: Add support for not skipping configuration-specific
 nodes in big-step.

---
 .../code/java/dataflow/internal/DataFlow.qll  | 19 +++++++++++++++++++
 .../java/dataflow/internal/DataFlowImpl.qll   |  9 ++++++++-
 .../java/dataflow/internal/DataFlowImpl1.qll  |  2 ++
 3 files changed, 29 insertions(+), 1 deletion(-)

diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/DataFlow.qll b/java/ql/lib/semmle/code/java/dataflow/internal/DataFlow.qll
index 47329d133a4..03975c6a54a 100644
--- a/java/ql/lib/semmle/code/java/dataflow/internal/DataFlow.qll
+++ b/java/ql/lib/semmle/code/java/dataflow/internal/DataFlow.qll
@@ -46,6 +46,14 @@ signature module ConfigSig {
    */
   default predicate allowImplicitRead(Node node, ContentSet c) { none() }
 
+  /**
+   * Holds if `node` should never be skipped over in the `PathGraph` and in path
+   * explanations.
+   */
+  default predicate neverSkip(Node node) {
+    isAdditionalFlowStep(node, _) or isAdditionalFlowStep(_, node)
+  }
+
   /**
    * Gets the virtual dispatch branching limit when calculating field flow.
    * This can be overridden to a smaller value to improve performance (a
@@ -141,6 +149,17 @@ signature module StateConfigSig {
    */
   default predicate allowImplicitRead(Node node, ContentSet c) { none() }
 
+  /**
+   * Holds if `node` should never be skipped over in the `PathGraph` and in path
+   * explanations.
+   */
+  default predicate neverSkip(Node node) {
+    isAdditionalFlowStep(node, _) or
+    isAdditionalFlowStep(_, node) or
+    isAdditionalFlowStep(node, _, _, _) or
+    isAdditionalFlowStep(_, _, node, _)
+  }
+
   /**
    * Gets the virtual dispatch branching limit when calculating field flow.
    * This can be overridden to a smaller value to improve performance (a
diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl.qll b/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl.qll
index fe8633e9218..29561b0f0a6 100644
--- a/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl.qll
+++ b/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl.qll
@@ -66,6 +66,12 @@ signature module FullStateConfigSig {
    */
   predicate allowImplicitRead(Node node, ContentSet c);
 
+  /**
+   * Holds if `node` should never be skipped over in the `PathGraph` and in path
+   * explanations.
+   */
+  predicate neverSkip(Node node);
+
   /**
    * Gets the virtual dispatch branching limit when calculating field flow.
    * This can be overridden to a smaller value to improve performance (a
@@ -2024,7 +2030,8 @@ module Impl<FullStateConfigSig Config> {
         castNode(this.asNode()) or
         clearsContentCached(this.asNode(), _) or
         expectsContentCached(this.asNode(), _) or
-        neverSkipInPathGraph(this.asNode())
+        neverSkipInPathGraph(this.asNode()) or
+        Config::neverSkip(this.asNode())
       }
     }
 
diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl1.qll b/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl1.qll
index be70086a93a..b0de9745816 100644
--- a/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl1.qll
+++ b/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl1.qll
@@ -313,6 +313,8 @@ private module Config implements FullStateConfigSig {
     any(Configuration config).allowImplicitRead(node, c)
   }
 
+  predicate neverSkip(Node node) { none() }
+
   int fieldFlowBranchLimit() { result = min(any(Configuration config).fieldFlowBranchLimit()) }
 
   FlowFeature getAFeature() { result = any(Configuration config).getAFeature() }