Dataflow: Add speculative flow modules.

Author: aschackmull

shared/dataflow/codeql/dataflow/TaintTracking.qll

@@ -29,6 +29,12 @@ signature module InputSig<LocationSig Location, DF::InputSig<Location> Lang> {
    */
   bindingset[node]
   predicate defaultImplicitTaintRead(Lang::Node node, Lang::ContentSet c);
+
+  /**
+   * Holds if the additional step from `src` to `sink` should be considered in
+   * speculative taint flow exploration.
+   */
+  predicate speculativeTaintStep(Lang::Node src, Lang::Node sink);
 }
 
 /**
@@ -130,4 +136,124 @@ module TaintFlowMake<
   {
     import GlobalWithState<Config>
   }
+
+  signature int speculationLimitSig();
+
+  private module AddSpeculativeTaintSteps<
+    DataFlowInternal::FullStateConfigSig Config, speculationLimitSig/0 speculationLimit> implements
+    DataFlowInternal::FullStateConfigSig
+  {
+    import Config
+
+    private predicate relevantState(Config::FlowState state) {
+      Config::isSource(_, state)
+      or
+      exists(Config::FlowState state0 |
+        relevantState(state0) and Config::isAdditionalFlowStep(_, state0, _, state, _)
+      )
+    }
+
+    private newtype TFlowState =
+      TMkFlowState(Config::FlowState state, int spec) {
+        relevantState(state) and spec = [0 .. speculationLimit()]
+      }
+
+    class FlowState extends TFlowState {
+      private Config::FlowState state;
+      private int spec;
+
+      FlowState() { this = TMkFlowState(state, spec) }
+
+      string toString() { result = "FlowState" }
+
+      Config::FlowState getState() { result = state }
+
+      int getSpec() { result = spec }
+    }
+
+    predicate isSource(DataFlowLang::Node source, FlowState state) {
+      Config::isSource(source, state.getState()) and state.getSpec() = 0
+    }
+
+    predicate isSink(DataFlowLang::Node sink, FlowState state) {
+      Config::isSink(sink, state.getState())
+    }
+
+    predicate isBarrier(DataFlowLang::Node node, FlowState state) {
+      Config::isBarrier(node, state.getState())
+    }
+
+    predicate isBarrierIn(DataFlowLang::Node node, FlowState state) {
+      Config::isBarrierIn(node, state.getState())
+    }
+
+    predicate isBarrierOut(DataFlowLang::Node node, FlowState state) {
+      Config::isBarrierOut(node, state.getState())
+    }
+
+    predicate isAdditionalFlowStep(
+      DataFlowLang::Node node1, FlowState state1, DataFlowLang::Node node2, FlowState state2,
+      string model
+    ) {
+      Config::isAdditionalFlowStep(node1, state1.getState(), node2, state2.getState(), model) and
+      state1.getSpec() = state2.getSpec()
+      or
+      speculativeTaintStep(node1, node2) and
+      not defaultAdditionalTaintStep(node1, node2, _) and
+      not Config::isAdditionalFlowStep(node1, _, node2, _, _) and
+      not Config::isAdditionalFlowStep(node1, node2, _) and
+      model = "Speculative" and
+      state1.getSpec() + 1 = state2.getSpec() and
+      state1.getState() = state2.getState()
+    }
+  }
+
+  module SpeculativeFlow<DataFlow::ConfigSig Config, speculationLimitSig/0 speculationLimit>
+    implements DataFlow::GlobalFlowSig
+  {
+    private module Config0 implements DataFlowInternal::FullStateConfigSig {
+      import DataFlowInternal::DefaultState<Config>
+      import Config
+
+      predicate isAdditionalFlowStep(
+        DataFlowLang::Node node1, DataFlowLang::Node node2, string model
+      ) {
+        Config::isAdditionalFlowStep(node1, node2) and model = "Config"
+      }
+    }
+
+    private module C implements DataFlowInternal::FullStateConfigSig {
+      import AddTaintDefaults<AddSpeculativeTaintSteps<Config0, speculationLimit/0>>
+    }
+
+    import DataFlowInternal::Impl<C>
+  }
+
+  module SpeculativeFlowWithState<
+    DataFlow::StateConfigSig Config, speculationLimitSig/0 speculationLimit> implements
+    DataFlow::GlobalFlowSig
+  {
+    private module Config0 implements DataFlowInternal::FullStateConfigSig {
+      import Config
+
+      predicate isAdditionalFlowStep(
+        DataFlowLang::Node node1, DataFlowLang::Node node2, string model
+      ) {
+        Config::isAdditionalFlowStep(node1, node2) and model = "Config"
+      }
+
+      predicate isAdditionalFlowStep(
+        DataFlowLang::Node node1, FlowState state1, DataFlowLang::Node node2, FlowState state2,
+        string model
+      ) {
+        Config::isAdditionalFlowStep(node1, state1, node2, state2) and model = "Config"
+      }
+    }
+
+    private module C implements DataFlowInternal::FullStateConfigSig {
+      import AddTaintDefaults<AddSpeculativeTaintSteps<Config0, speculationLimit/0>>
+    }
+
+    import DataFlowInternal::Impl<C>
+  }
 }