Shared: add in/out barriers with flow state

Author: asgerf

shared/dataflow/codeql/dataflow/DataFlow.qll

@@ -357,9 +357,15 @@ module Configs<InputSig Lang> {
     /** Holds if data flow into `node` is prohibited. */
     default predicate isBarrierIn(Node node) { none() }
 
+    /** Holds if data flow into `node` is prohibited when the target flow state is `state`. */
+    default predicate isBarrierIn(Node node, FlowState state) { none() }
+
     /** Holds if data flow out of `node` is prohibited. */
     default predicate isBarrierOut(Node node) { none() }
 
+    /** Holds if data flow out of `node` is prohibited when the originating flow state is `state`. */
+    default predicate isBarrierOut(Node node, FlowState state) { none() }
+
     /**
      * Holds if data may flow from `node1` to `node2` in addition to the normal data-flow steps.
      */

shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll

@@ -53,9 +53,15 @@ module MakeImpl<InputSig Lang> {
     /** Holds if data flow into `node` is prohibited. */
     predicate isBarrierIn(Node node);
 
+    /** Holds if data flow into `node` is prohibited when the target flow state is `state`. */
+    predicate isBarrierIn(Node node, FlowState state);
+
     /** Holds if data flow out of `node` is prohibited. */
     predicate isBarrierOut(Node node);
 
+    /** Holds if data flow out of `node` is prohibited when the originating flow state is `state`. */
+    predicate isBarrierOut(Node node, FlowState state);
+
     /**
      * Holds if data may flow from `node1` to `node2` in addition to the normal data-flow steps.
      */
@@ -133,6 +139,10 @@ module MakeImpl<InputSig Lang> {
 
     predicate isBarrier(Node node, FlowState state) { none() }
 
+    predicate isBarrierIn(Node node, FlowState state) { none() }
+
+    predicate isBarrierOut(Node node, FlowState state) { none() }
+
     predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {
       none()
     }
@@ -220,6 +230,14 @@ module MakeImpl<InputSig Lang> {
       )
     }
 
+    private predicate inBarrier(NodeEx node, FlowState state) {
+      exists(Node n |
+        node.asNode() = n and
+        Config::isBarrierIn(n, state) and
+        Config::isSource(n, state)
+      )
+    }
+
     private predicate outBarrier(NodeEx node) {
       exists(Node n |
         node.asNode() = n and
@@ -231,6 +249,17 @@ module MakeImpl<InputSig Lang> {
       )
     }
 
+    private predicate outBarrier(NodeEx node, FlowState state) {
+      exists(Node n |
+        node.asNode() = n and
+        Config::isBarrierOut(n, state)
+      |
+        Config::isSink(n, state)
+        or
+        Config::isSink(n)
+      )
+    }
+
     pragma[nomagic]
     private predicate fullBarrier(NodeEx node) {
       exists(Node n | node.asNode() = n |
@@ -247,7 +276,16 @@ module MakeImpl<InputSig Lang> {
 
     pragma[nomagic]
     private predicate stateBarrier(NodeEx node, FlowState state) {
-      exists(Node n | node.asNode() = n | Config::isBarrier(n, state))
+      exists(Node n | node.asNode() = n |
+        Config::isBarrier(n, state)
+        or
+        Config::isBarrierIn(n, state) and
+        not Config::isSource(n, state)
+        or
+        Config::isBarrierOut(n, state) and
+        not Config::isSink(n, state) and
+        not Config::isSink(n)
+      )
     }
 
     pragma[nomagic]
@@ -265,6 +303,7 @@ module MakeImpl<InputSig Lang> {
     }
 
     /** Provides the relevant barriers for a step from `node1` to `node2`. */
+    bindingset[node1, node2]
     pragma[inline]
     private predicate stepFilter(NodeEx node1, NodeEx node2) {
       not outBarrier(node1) and
@@ -273,6 +312,17 @@ module MakeImpl<InputSig Lang> {
       not fullBarrier(node2)
     }
 
+    /** Provides the relevant barriers for a step from `node1,state1` to `node2,state2`, including stateless barriers for `node1` to `node2`. */
+    bindingset[node1, state1, node2, state2]
+    pragma[inline]
+    private predicate stateStepFilter(NodeEx node1, FlowState state1, NodeEx node2, FlowState state2) {
+      stepFilter(node1, node2) and
+      not outBarrier(node1, state1) and
+      not inBarrier(node2, state2) and
+      not stateBarrier(node1, state1) and
+      not stateBarrier(node2, state2)
+    }
+
     pragma[nomagic]
     private predicate isUnreachableInCall1(NodeEx n, LocalCallContextSpecificCall cc) {
       isUnreachableInCallCached(n.asNode(), cc.getCall())
@@ -325,9 +375,7 @@ module MakeImpl<InputSig Lang> {
         node2.asNode() = n2 and
         Config::isAdditionalFlowStep(pragma[only_bind_into](n1), s1, pragma[only_bind_into](n2), s2) and
         getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
-        stepFilter(node1, node2) and
-        not stateBarrier(node1, s1) and
-        not stateBarrier(node2, s2)
+        stateStepFilter(node1, s1, node2, s2)
       )
     }
 
@@ -364,9 +412,7 @@ module MakeImpl<InputSig Lang> {
         node2.asNode() = n2 and
         Config::isAdditionalFlowStep(pragma[only_bind_into](n1), s1, pragma[only_bind_into](n2), s2) and
         getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
-        stepFilter(node1, node2) and
-        not stateBarrier(node1, s1) and
-        not stateBarrier(node2, s2) and
+        stateStepFilter(node1, s1, node2, s2) and
         not Config::getAFeature() instanceof FeatureEqualSourceSinkCallContext
       )
     }