Merge branch 'main' into js/shared-dataflow-merge-main

This commit is contained in:
Asger F
2024-11-20 14:05:03 +01:00
2341 changed files with 169482 additions and 106842 deletions

View File

@@ -1,3 +1,7 @@
## 1.1.5
No user-facing changes.
## 1.1.4
No user-facing changes.

View File

@@ -0,0 +1,3 @@
## 1.1.5
No user-facing changes.

View File

@@ -1,2 +1,2 @@
---
lastReleaseVersion: 1.1.4
lastReleaseVersion: 1.1.5

View File

@@ -676,6 +676,12 @@ module DataFlowMake<LocationSig Location, InputSig<Location> Lang> {
predicate isAdditionalFlowStep(Node node1, Node node2, string model) {
Config::isAdditionalFlowStep(node1, node2) and model = "Config"
}
predicate isAdditionalFlowStep(
Node node1, FlowState state1, Node node2, FlowState state2, string model
) {
Config::isAdditionalFlowStep(node1, state1, node2, state2) and model = "Config"
}
}
import Impl<C>

View File

@@ -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);
}
/**
@@ -63,7 +69,7 @@ module TaintFlowMake<
Config::isSink(node) or
Config::isSink(node, _) or
Config::isAdditionalFlowStep(node, _, _) or
Config::isAdditionalFlowStep(node, _, _, _)
Config::isAdditionalFlowStep(node, _, _, _, _)
) and
defaultImplicitTaintRead(node, c)
}
@@ -108,6 +114,13 @@ module TaintFlowMake<
) {
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 {
@@ -123,4 +136,132 @@ 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()
}
}
/**
* Constructs a global taint tracking computation that also allows a given
* maximum number of speculative taint steps.
*/
module SpeculativeGlobal<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>
}
/**
* Constructs a global taint tracking computation using flow state that also
* allows a given maximum number of speculative taint steps.
*/
module SpeculativeGlobalWithState<
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>
}
}

View File

@@ -73,7 +73,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
* Holds if data may flow from `node1` to `node2` in addition to the normal data-flow steps.
* This step is only applicable in `state1` and updates the flow state to `state2`.
*/
predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2);
predicate isAdditionalFlowStep(
Node node1, FlowState state1, Node node2, FlowState state2, string model
);
/**
* Holds if an arbitrary number of implicit read steps of content `c` may be
@@ -153,7 +155,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
predicate isBarrierOut(Node node, FlowState state) { none() }
predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {
predicate isAdditionalFlowStep(
Node node1, FlowState state1, Node node2, FlowState state2, string model
) {
none()
}
}
@@ -364,12 +368,13 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
}
private predicate additionalLocalStateStep(
NodeEx node1, FlowState s1, NodeEx node2, FlowState s2
NodeEx node1, FlowState s1, NodeEx node2, FlowState s2, string model
) {
exists(Node n1, Node n2 |
node1.asNodeOrImplicitRead() = n1 and
node2.asNode() = n2 and
Config::isAdditionalFlowStep(pragma[only_bind_into](n1), s1, pragma[only_bind_into](n2), s2) and
Config::isAdditionalFlowStep(pragma[only_bind_into](n1), s1, pragma[only_bind_into](n2), s2,
model) and
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
stateStepFilter(node1, s1, node2, s2)
)
@@ -402,11 +407,14 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
)
}
private predicate additionalJumpStateStep(NodeEx node1, FlowState s1, NodeEx node2, FlowState s2) {
private predicate additionalJumpStateStep(
NodeEx node1, FlowState s1, NodeEx node2, FlowState s2, string model
) {
exists(Node n1, Node n2 |
node1.asNodeOrImplicitRead() = n1 and
node2.asNode() = n2 and
Config::isAdditionalFlowStep(pragma[only_bind_into](n1), s1, pragma[only_bind_into](n2), s2) and
Config::isAdditionalFlowStep(pragma[only_bind_into](n1), s1, pragma[only_bind_into](n2), s2,
model) and
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
stateStepFilter(node1, s1, node2, s2) and
not Config::getAFeature() instanceof FeatureEqualSourceSinkCallContext
@@ -537,13 +545,13 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
exists(NodeEx mid | fwdFlow(mid, cc) |
localFlowStepEx(mid, node, _) or
additionalLocalFlowStep(mid, node, _) or
additionalLocalStateStep(mid, _, node, _)
additionalLocalStateStep(mid, _, node, _, _)
)
or
exists(NodeEx mid | fwdFlow(mid, _) and cc = false |
jumpStepEx(mid, node) or
additionalJumpStep(mid, node, _) or
additionalJumpStateStep(mid, _, node, _)
additionalJumpStateStep(mid, _, node, _, _)
)
or
// store
@@ -684,8 +692,8 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
private predicate stateStepFwd(FlowState state1, FlowState state2) {
exists(NodeEx node1 |
additionalLocalStateStep(node1, state1, _, state2) or
additionalJumpStateStep(node1, state1, _, state2)
additionalLocalStateStep(node1, state1, _, state2, _) or
additionalJumpStateStep(node1, state1, _, state2, _)
|
fwdFlow(node1)
)
@@ -730,13 +738,13 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
exists(NodeEx mid | revFlow(mid, toReturn) |
localFlowStepEx(node, mid, _) or
additionalLocalFlowStep(node, mid, _) or
additionalLocalStateStep(node, _, mid, _)
additionalLocalStateStep(node, _, mid, _, _)
)
or
exists(NodeEx mid | revFlow(mid, _) and toReturn = false |
jumpStepEx(node, mid) or
additionalJumpStep(node, mid, _) or
additionalJumpStateStep(node, _, mid, _)
additionalJumpStateStep(node, _, mid, _, _)
)
or
// store
@@ -854,8 +862,8 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
private predicate stateStepRev(FlowState state1, FlowState state2) {
exists(NodeEx node1, NodeEx node2 |
additionalLocalStateStep(node1, state1, node2, state2) or
additionalJumpStateStep(node1, state1, node2, state2)
additionalLocalStateStep(node1, state1, node2, state2, _) or
additionalJumpStateStep(node1, state1, node2, state2, _)
|
revFlow(node1, _) and
revFlow(node2, _) and
@@ -1075,8 +1083,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
) {
Stage1::revFlow(node1) and
Stage1::revFlow(node2) and
additionalLocalStateStep(node1, state1, node2, state2) and
label = "Config" and
additionalLocalStateStep(node1, state1, node2, state2, label) and
t = node2.getDataFlowType() and
lcc.relevantFor(node1.getEnclosingCallable()) and
not isUnreachableInCall1(node1, lcc) and
@@ -1628,7 +1635,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
or
exists(NodeEx mid, FlowState state0 |
fwdFlow(mid, state0, _, _, _, ap, apa) and
additionalJumpStateStep(mid, state0, node, state) and
additionalJumpStateStep(mid, state0, node, state, _) and
t = getNodeTyp(node) and
ap instanceof ApNil
)
@@ -2293,7 +2300,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
)
or
exists(NodeEx mid, FlowState state0 |
additionalJumpStateStep(node, state, mid, state0) and
additionalJumpStateStep(node, state, mid, state0, _) and
revFlow(pragma[only_bind_into](mid), pragma[only_bind_into](state0), _, _, ap) and
ap instanceof ApNil
)
@@ -2596,31 +2603,27 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
callEdgeReturn(call, c, _, _, _, _, _)
}
/** Provides the input to `LocalFlowBigStep`. */
signature module LocalFlowBigStepInputSig {
bindingset[node1, state1]
bindingset[node2, state2]
predicate localStep(
NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue,
DataFlowType t, LocalCallContext lcc, string label
);
}
/** Holds if `node1` can step to `node2` in one or more local steps. */
bindingset[node1, state1]
bindingset[node2, state2]
signature predicate localStepSig(
NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue,
DataFlowType t, LocalCallContext lcc, string label
);
/**
* Provides a big-step relation for local flow steps.
*
* The big-step releation is based on the `localStep` relation from the
* input module, restricted to nodes that are forwards and backwards
* reachable in this stage.
* The big-step releation is based on the `localStepInput` relation,
* restricted to nodes that are forwards and backwards reachable in
* this stage.
*/
additional module LocalFlowBigStep<LocalFlowBigStepInputSig Input> {
final private class NodeExFinal = NodeEx;
additional module LocalFlowBigStep<localStepSig/8 localStepInput> {
/**
* A node where some checking is required, and hence the big-step relation
* is not allowed to step over.
*/
private class FlowCheckNode extends NodeExFinal {
private class FlowCheckNode extends NodeEx {
FlowCheckNode() {
revFlow(this, _, _) and
(
@@ -2640,7 +2643,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
exists(ApNil nil |
revFlow(node1, state1, pragma[only_bind_into](nil)) and
revFlow(node2, state2, pragma[only_bind_into](nil)) and
Input::localStep(node1, state1, node2, state2, false, t, lcc, label) and
localStepInput(node1, state1, node2, state2, false, t, lcc, label) and
state1 != state2
)
}
@@ -2658,7 +2661,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
or
additionalJumpStep(_, node, _)
or
additionalJumpStateStep(_, _, node, state)
additionalJumpStateStep(_, _, node, state, _)
or
node instanceof ParamNodeEx
or
@@ -2706,9 +2709,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
exists(NodeEx next, FlowState s |
revFlow(next, s, pragma[only_bind_into](ap)) and ap instanceof ApNil
|
additionalJumpStateStep(node, state, next, s)
additionalJumpStateStep(node, state, next, s, _)
or
additionalLocalStateStep(node, state, next, s) and
additionalLocalStateStep(node, state, next, s, _) and
s != state
)
or
@@ -2734,7 +2737,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
not inBarrier(node2, state) and
not outBarrier(node1, state) and
exists(NodeEx mid, boolean preservesValue2, DataFlowType t2, string label2, Ap ap |
Input::localStep(mid, state, node2, state, preservesValue2, t2, cc, label2) and
localStepInput(mid, state, node2, state, preservesValue2, t2, cc, label2) and
revFlow(node2, pragma[only_bind_into](state), pragma[only_bind_into](ap)) and
not outBarrier(mid, state) and
(preservesValue = true or ap instanceof ApNil)
@@ -2769,6 +2772,33 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
exists(Ap ap |
localFlowStepPlus(node1, state1, node2, preservesValue, t, callContext, label) and
localFlowExit(node2, state1, ap) and
state1 = state2 and
node1 != node2
|
preservesValue = true or ap instanceof ApNil
)
or
additionalLocalStateStep(node1, state1, node2, state2, t, callContext, label) and
preservesValue = false
}
/**
* Holds if `node1` can step to `node2` in one or more local steps and this
* path can occur as a maximal subsequence of local steps in a dataflow path.
*
* This predicate should be used when `localStepInput` is already a big-step
* relation, which will do the same as `localFlowBigStep`, but avoids potential
* worst-case quadratic complexity.
*/
pragma[nomagic]
predicate localFlowBigStepTc(
NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue,
DataFlowType t, LocalCallContext callContext, string label
) {
exists(Ap ap |
localFlowEntry(node1, pragma[only_bind_into](state1), pragma[only_bind_into](ap)) and
localStepInput(node1, state1, node2, state2, preservesValue, t, callContext, label) and
localFlowExit(node2, pragma[only_bind_into](state2), pragma[only_bind_into](ap)) and
state1 = state2
|
preservesValue = true or ap instanceof ApNil
@@ -3253,10 +3283,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
t = getNodeTyp(node) and
ap instanceof ApNil
or
additionalJumpStateStep(mid, state0, node, state) and
additionalJumpStateStep(mid, state0, node, state, label) and
t = getNodeTyp(node) and
ap instanceof ApNil and
label = "Config"
ap instanceof ApNil
)
or
// flow into a callable
@@ -3790,27 +3819,25 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
import CallContextSensitivity<CallContextSensitivityInput>
import NoLocalCallContext
private module BigStepInput implements PrevStage::LocalFlowBigStepInputSig {
bindingset[node1, state1]
bindingset[node2, state2]
predicate localStep(
NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue,
DataFlowType t, LocalCallContext lcc, string label
) {
localStepNodeCand1(node1, node2, preservesValue, t, lcc, label) and
state1 = state2
or
localStateStepNodeCand1(node1, state1, node2, state2, t, lcc, label) and
preservesValue = false
}
bindingset[node1, state1]
bindingset[node2, state2]
private predicate localStepInput(
NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue,
DataFlowType t, LocalCallContext lcc, string label
) {
localStepNodeCand1(node1, node2, preservesValue, t, lcc, label) and
state1 = state2
or
localStateStepNodeCand1(node1, state1, node2, state2, t, lcc, label) and
preservesValue = false
}
additional predicate localFlowBigStep(
NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue,
DataFlowType t, LocalCallContext lcc, string label
) {
PrevStage::LocalFlowBigStep<BigStepInput>::localFlowBigStep(node1, state1, node2, state2,
preservesValue, t, lcc, label)
PrevStage::LocalFlowBigStep<localStepInput/8>::localFlowBigStep(node1, state1, node2,
state2, preservesValue, t, lcc, label)
}
bindingset[node1, state1]
@@ -4205,14 +4232,8 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
import CallContextSensitivity<CallContextSensitivityInput>
import LocalCallContext
predicate localStep(
NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue,
Typ t, LocalCc lcc, string label
) {
Stage3Param::localFlowBigStep(node1, state1, node2, state2, preservesValue, t, lcc, label) and
PrevStage::revFlow(node1, pragma[only_bind_into](state1), _) and
PrevStage::revFlow(node2, pragma[only_bind_into](state2), _)
}
predicate localStep =
PrevStage::LocalFlowBigStep<Stage3Param::localFlowBigStep/8>::localFlowBigStepTc/8;
bindingset[node, state, t0, ap]
predicate filter(NodeEx node, FlowState state, Typ t0, Ap ap, Typ t) {
@@ -4410,18 +4431,8 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
import CallContextSensitivity<CallContextSensitivityInput>
import LocalCallContext
private module BigStepInput implements PrevStage::LocalFlowBigStepInputSig {
predicate localStep(
NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue,
DataFlowType t, LocalCallContext lcc, string label
) {
Stage3Param::localFlowBigStep(node1, state1, node2, state2, preservesValue, t, lcc, label) and
PrevStage::revFlow(node1, pragma[only_bind_into](state1), _) and
PrevStage::revFlow(node2, pragma[only_bind_into](state2), _)
}
}
predicate localStep = PrevStage::LocalFlowBigStep<BigStepInput>::localFlowBigStep/8;
predicate localStep =
PrevStage::LocalFlowBigStep<Stage5Param::localStep/8>::localFlowBigStepTc/8;
bindingset[node, state, t0, ap]
predicate filter(NodeEx node, FlowState state, Typ t0, Ap ap, Typ t) {
@@ -4817,7 +4828,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
or
additionalJumpStep(node1, node2, _)
or
additionalJumpStateStep(node1, _, node2, _)
additionalJumpStateStep(node1, _, node2, _, _)
or
// flow into callable
viableParamArgEx(_, node2, node1)
@@ -4931,10 +4942,10 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
private predicate relevantState(FlowState state) {
sourceNode(_, state) or
sinkNodeWithState(_, state) or
additionalLocalStateStep(_, state, _, _) or
additionalLocalStateStep(_, _, _, state) or
additionalJumpStateStep(_, state, _, _) or
additionalJumpStateStep(_, _, _, state)
additionalLocalStateStep(_, state, _, _, _) or
additionalLocalStateStep(_, _, _, state, _) or
additionalJumpStateStep(_, state, _, _, _) or
additionalJumpStateStep(_, _, _, state, _)
}
private predicate revSinkNode(NodeEx node, FlowState state) {
@@ -5270,7 +5281,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
t = node.getDataFlowType() and
ap = TPartialNil()
or
additionalLocalStateStep(mid.getNodeEx(), mid.getState(), node, state) and
additionalLocalStateStep(mid.getNodeEx(), mid.getState(), node, state, _) and
cc = mid.getCallContext() and
sc1 = mid.getSummaryCtx1() and
sc2 = mid.getSummaryCtx2() and
@@ -5305,7 +5316,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
ap = TPartialNil() and
isStoreStep = false
or
additionalJumpStateStep(mid.getNodeEx(), mid.getState(), node, state) and
additionalJumpStateStep(mid.getNodeEx(), mid.getState(), node, state, _) and
cc = callContextNone() and
sc1 = TSummaryCtx1None() and
sc2 = TSummaryCtx2None() and
@@ -5577,7 +5588,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
ap = TPartialNil() and
isStoreStep = false
or
additionalLocalStateStep(node, state, mid.getNodeEx(), mid.getState()) and
additionalLocalStateStep(node, state, mid.getNodeEx(), mid.getState(), _) and
sc1 = mid.getSummaryCtx1() and
sc2 = mid.getSummaryCtx2() and
sc3 = mid.getSummaryCtx3() and
@@ -5602,7 +5613,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
ap = TPartialNil() and
isStoreStep = false
or
additionalJumpStateStep(node, state, mid.getNodeEx(), mid.getState()) and
additionalJumpStateStep(node, state, mid.getNodeEx(), mid.getState(), _) and
sc1 = TRevSummaryCtx1None() and
sc2 = TRevSummaryCtx2None() and
sc3 = TRevSummaryCtx3None() and

View File

@@ -323,4 +323,121 @@ module MakeConsistency<
lambdaCall(call, _, receiver) and
not nodeGetEnclosingCallable(receiver) = call.getEnclosingCallable()
}
query predicate speculativeStepAlreadyHasModel(Node n1, Node n2, string model) {
speculativeTaintStep(n1, n2) and
not defaultAdditionalTaintStep(n1, n2, _) and
(
simpleLocalFlowStep(n1, n2, _) and model = "SimpleLocalFlowStep"
or
exists(DataFlowCall call |
exists(viableCallable(call)) and
isArgumentNode(n1, call, _) and
model = "dispatch"
)
)
}
/**
* Gets counts of inconsistencies of each type.
*/
int getInconsistencyCounts(string type) {
// total results from all the AST consistency query predicates.
type = "Node should have one enclosing callable" and
result = count(Node n | uniqueEnclosingCallable(n, _))
or
type = "Call should have one enclosing callable" and
result = count(DataFlowCall c | uniqueCallEnclosingCallable(c, _))
or
type = "Node should have one type" and
result = count(Node n | uniqueType(n, _))
or
type = "Node should have one location" and
result = count(Node n | uniqueNodeLocation(n, _))
or
type = "Nodes without location" and
result = count( | missingLocation(_) | 1)
or
type = "Node should have one toString" and
result = count(Node n | uniqueNodeToString(n, _))
or
type = "Callable mismatch for parameter" and
result = count(ParameterNode p | parameterCallable(p, _))
or
type = "Local flow step does not preserve enclosing callable" and
result = count(Node n1, Node n2 | localFlowIsLocal(n1, n2, _))
or
type = "Read step does not preserve enclosing callable" and
result = count(Node n1, Node n2 | readStepIsLocal(n1, n2, _))
or
type = "Store step does not preserve enclosing callable" and
result = count(Node n1, Node n2 | storeStepIsLocal(n1, n2, _))
or
type = "Type compatibility predicate is not reflexive" and
result = count(DataFlowType t | compatibleTypesReflexive(t, _))
or
type = "Call context for isUnreachableInCall is inconsistent with call graph" and
result = count(Node n, DataFlowCall call | unreachableNodeCCtx(n, call, _))
or
type = "Node and call does not share enclosing callable" and
result = count(DataFlowCall call, Node n | localCallNodes(call, n, _))
or
type = "PostUpdateNode should not equal its pre-update node" and
result = count(PostUpdateNode n | postIsNotPre(n, _))
or
type = "PostUpdateNode should have one pre-update node" and
result = count(PostUpdateNode n | postHasUniquePre(n, _))
or
type = "Node has multiple PostUpdateNodes" and
result = count(Node n | uniquePostUpdate(n, _))
or
type = "PostUpdateNode does not share callable with its pre-update node" and
result = count(PostUpdateNode n | postIsInSameCallable(n, _))
or
type = "Origin of readStep is missing a PostUpdateNode" and
result = count(Node n | reverseRead(n, _))
or
type = "ArgumentNode is missing PostUpdateNode" and
result = count(ArgumentNode n | argHasPostUpdate(n, _))
or
type = "PostUpdateNode should not be the target of local flow" and
result = count(PostUpdateNode n | postWithInFlow(n, _))
or
type = "Call context too large" and
result =
count(DataFlowCall call, DataFlowCall ctx, DataFlowCallable callable |
viableImplInCallContextTooLarge(call, ctx, callable)
)
or
type = "Parameters with overlapping positions" and
result =
count(DataFlowCallable c, ParameterPosition pos, Node p |
uniqueParameterNodeAtPosition(c, pos, p, _)
)
or
type = "Parameter node with multiple positions" and
result =
count(DataFlowCallable c, ParameterPosition pos, Node p |
uniqueParameterNodePosition(c, pos, p, _)
)
or
type = "Non-unique content approximation" and
result = count(Content c | uniqueContentApprox(c, _))
or
type = "Node steps to itself" and
result = count(Node n | identityLocalStep(n, _))
or
type = "Missing call for argument node" and
result = count(ArgumentNode n | missingArgumentCall(n, _))
or
type = "Multiple calls for argument node" and
result = count(ArgumentNode arg, DataFlowCall call | multipleArgumentCall(arg, call, _))
or
type = "Lambda call enclosing callable mismatch" and
result =
count(DataFlowCall call, Node receiver | lambdaCallEnclosingCallableMismatch(call, receiver))
or
type = "Speculative step already hasM Model" and
result = count(Node n1, Node n2 | speculativeStepAlreadyHasModel(n1, n2, _))
}
}

View File

@@ -17,7 +17,7 @@ signature class PathNodeSig {
private signature predicate provenanceSig(string model);
private module TranslateModels<
interpretModelForTestSig/2 interpretModelForTest, provenanceSig/1 provenance>
interpretModelForTestSig/2 interpretModelForTest0, provenanceSig/1 provenance>
{
private predicate madIds(string madId) {
exists(string model |
@@ -26,15 +26,42 @@ private module TranslateModels<
)
}
private predicate rankedMadIds(string madId, int r) {
madId = rank[r](string madId0 | madIds(madId0) | madId0 order by madId0.toInt())
// Be robust against MaD IDs with multiple textual representations; simply
// concatenate them all
private predicate interpretModelForTest(QlBuiltins::ExtensionId madId, string model) {
model = strictconcat(string mod | interpretModelForTest0(madId, mod) | mod, ", ")
}
private QlBuiltins::ExtensionId getModelId(string model) {
madIds(result.toString()) and
interpretModelForTest(result, model)
}
// collapse models with the same textual representation, in order to not rely
// on the order of `ExtensionId`s
private module ExtensionIdSets =
QlBuiltins::InternSets<string, QlBuiltins::ExtensionId, getModelId/1>;
private predicate rankedMadIds(ExtensionIdSets::Set extIdSet, int r) {
extIdSet =
rank[r](ExtensionIdSets::Set extIdSet0, string model |
extIdSet0 = ExtensionIdSets::getSet(model)
|
extIdSet0 order by model
)
}
private predicate translateModel(string id, int r) {
exists(QlBuiltins::ExtensionId madId, ExtensionIdSets::Set extIdSet |
id = madId.toString() and
extIdSet.contains(madId) and
rankedMadIds(extIdSet, r)
)
}
/** Lists the renumbered and pretty-printed models used in the edges relation. */
predicate models(int r, string model) {
exists(QlBuiltins::ExtensionId madId |
rankedMadIds(madId.toString(), r) and interpretModelForTest(madId, model)
)
exists(string madId | translateModel(madId, r) and getModelId(model).toString() = madId)
}
private predicate translateModelsPart(string model1, string model2, int i) {
@@ -46,7 +73,7 @@ private module TranslateModels<
translateModelsPart(model1, part, i - 1) and
madId = s.regexpCapture("([0-9]*)(.*)", 1) and
rest = s.regexpCapture("([0-9]*)(.*)", 2) and
rankedMadIds(madId, r) and
translateModel(madId, r) and
model2 = part + "MaD:" + r + rest
)
)
@@ -102,18 +129,7 @@ module TestPostProcessing {
private module Models = TranslateModels<interpretModelForTest/2, provenance/1>;
private newtype TModelRow = TMkModelRow(int r, string model) { Models::models(r, model) }
private predicate rankedModels(int i, int r, string model) {
TMkModelRow(r, model) =
rank[i](TModelRow row, int r0, string model0 |
row = TMkModelRow(r0, model0)
|
row order by r0, model0
)
}
predicate results(string relation, int row, int column, string data) {
query predicate results(string relation, int row, int column, string data) {
queryResults(relation, row, column, data) and
(relation != "edges" or column != provenanceColumn())
or
@@ -124,11 +140,11 @@ module TestPostProcessing {
Models::translateModels(model, data)
)
or
exists(int r, string model |
exists(string model |
relation = "models" and
rankedModels(row, r, model)
Models::models(row, model)
|
column = 0 and data = r.toString()
column = 0 and data = row.toString()
or
column = 1 and data = model
)

View File

@@ -1,5 +1,5 @@
name: codeql/dataflow
version: 1.1.5-dev
version: 1.1.6-dev
groups: shared
library: true
dependencies: