Dataflow: Add support for not skipping configuration-specific nodes in big-step.

Author: aschackmull

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

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())
       }
     }
 

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() }