Skip to content

Commit

Permalink
refactor2
Browse files Browse the repository at this point in the history
  • Loading branch information
@hvitved
hvitved committed Jun 19, 2024
1 parent 29ac38c commit 5ce9a85
Show file tree
Hide file tree
Showing 3 changed files with 80 additions and 73 deletions.
99 changes: 60 additions & 39 deletions shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1021,6 +1021,10 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
callEdgeReturn(call, c, _, _, _, _, _)
}

predicate storeMayReachRead(NodeEx storeSource, Content c, NodeEx readTarget) { none() }

predicate providesStoreReadMatching() { none() }

additional predicate stats(
boolean fwd, int nodes, int fields, int conscand, int states, int tuples, int calledges
) {
Expand Down Expand Up @@ -1320,6 +1324,10 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
predicate relevantCallEdgeIn(DataFlowCall call, DataFlowCallable c);

predicate relevantCallEdgeOut(DataFlowCall call, DataFlowCallable c);

predicate storeMayReachRead(NodeEx storeSource, Content c, NodeEx readTarget);

default predicate providesStoreReadMatching() { any() }
}

private module MkStage<StageSig PrevStage> {
Expand Down Expand Up @@ -1425,8 +1433,6 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
predicate typecheckStore(Typ typ, DataFlowType contentType);

default predicate enableTypeFlow() { any() }

default predicate enableStoreReadMatching() { any() }
}

module Stage<StageParam Param> implements StageSig {
Expand Down Expand Up @@ -1457,43 +1463,49 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {

private class NodeExAlias = NodeEx;

final private class ApFinal = Ap;

private module StoreReadMatchingInput implements StoreReadMatchingInputSig {
class NodeEx = NodeExAlias;

final private class ApApproxFinal = PrevStage::Ap;

class Ap extends ApApproxFinal {
Content getHead() { result = PrevStage::getAHeadContent(this) }
class Ap extends ApFinal {
Content getHead() { result = getAHeadContent(this) }
}

predicate revFlow(NodeEx node, Ap ap) {
enableStoreReadMatching() and PrevStage::revFlowAp(node, ap)
}
predicate nodeApRange(NodeEx node, Ap ap) { revFlowAp(node, ap) }

predicate localValueStep(NodeEx node1, NodeEx node2) { localValueStep(node1, node2, _) }
predicate localValueStep(NodeEx node1, NodeEx node2) {
exists(FlowState state, Ap ap, ApOption returnAp |
revFlow(node1, pragma[only_bind_into](state), _, pragma[only_bind_into](returnAp),
pragma[only_bind_into](ap)) and
revFlow(node2, pragma[only_bind_into](state), _, pragma[only_bind_into](returnAp),
pragma[only_bind_into](ap)) and
localValueStep(node1, node2, _)
)
}

predicate jumpValueStep(NodeEx node1, NodeEx node2) { jumpStepEx(node1, node2) }

predicate callEdgeArgParam(NodeEx arg, NodeEx param, Ap ap) {
PrevStage::callEdgeArgParam(_, _, arg, param, true, ap)
predicate callEdgeArgParam(NodeEx arg, NodeEx param) {
callEdgeArgParam(_, _, arg, param, true, _)
}

predicate callEdgeReturn(NodeEx ret, NodeEx out, Ap ap) {
PrevStage::callEdgeReturn(_, _, ret, _, out, true, ap)
predicate callEdgeReturn(NodeEx ret, NodeEx out) {
callEdgeReturn(_, _, ret, _, out, true, _)
}

predicate readContentStep(NodeEx node1, Content c, NodeEx node2) {
PrevStage::readStepCand(node1, c, node2)
readStepCand0(node1, c, node2)
}

predicate storeContentStep(NodeEx node1, Content c, NodeEx node2) {
PrevStage::storeStepCand(node1, _, c, node2, _, _)
storeStepCand0(node1, _, c, node2, _, _)
}

int accessPathConfigLimit() { result = Config::accessPathLimit() }
}

private import StoreReadMatching<StoreReadMatchingInput>
import StoreReadMatching<StoreReadMatchingInput>

/**
* Holds if `node` is reachable with access path `ap` from a source.
Expand Down Expand Up @@ -1529,7 +1541,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
private predicate storeMayReachReadInlineLate(
NodeEx storeSource, Content c, NodeEx readTarget
) {
storeMayReachRead(storeSource, c, readTarget)
PrevStage::storeMayReachRead(storeSource, c, readTarget)
}

bindingset[node1, state1]
Expand Down Expand Up @@ -1656,8 +1668,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
fwdFlow(node1, state, cc, summaryCtx, argT, argAp, t1, ap1, apa1) and
PrevStage::storeStepCand(node1, apa1, c, node2, contentType, containerType) and
t2 = getTyp(containerType) and
typecheckStore(t1, contentType) and
if enableStoreReadMatching() then storeMayReachRead(node1, c, _) else any()
typecheckStore(t1, contentType)
)
}

Expand All @@ -1666,13 +1677,14 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
* store of `c` on a container of type `t2` resulting in access path
* `cons`. `storeSource` is a relevant store source.
*
* This predicate is only evaluated when `enableStoreReadMatching()` holds.
* This predicate is only evaluated when `PrevStage::providesStoreReadMatching()`
* holds.
*/
pragma[nomagic]
private predicate fwdFlowConsCandStoreReadMatchingEnabled(
NodeEx storeSource, Typ t2, Ap cons, Content c, Typ t1, Ap tail
) {
enableStoreReadMatching() and
PrevStage::providesStoreReadMatching() and
fwdFlowStore(storeSource, t1, tail, c, t2, _, _, _, _, _, _) and
cons = apCons(c, t1, tail)
or
Expand All @@ -1687,14 +1699,14 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
* store of `c` on a container of type `t2` resulting in access path
* `cons`.
*
* This predicate is only evaluated when `enableStoreReadMatching()`
* This predicate is only evaluated when `PrevStage::providesStoreReadMatching()`
* doesn't hold.
*/
pragma[nomagic]
private predicate fwdFlowConsCandStoreReadMatchingDisabled(
Typ t2, Ap cons, Content c, Typ t1, Ap tail
) {
not enableStoreReadMatching() and
not PrevStage::providesStoreReadMatching() and
fwdFlowStore(_, t1, tail, c, t2, _, _, _, _, _, _) and
cons = apCons(c, t1, tail)
or
Expand All @@ -1707,8 +1719,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
pragma[nomagic]
private predicate readStepCand(NodeEx node1, ApHeadContent apc, Content c, NodeEx node2) {
PrevStage::readStepCand(node1, c, node2) and
apc = projectToHeadContent(c) and
if enableStoreReadMatching() then storeMayReachRead(_, c, node2) else any()
apc = projectToHeadContent(c)
}

bindingset[node1, apc]
Expand Down Expand Up @@ -2360,7 +2371,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
*/
pragma[nomagic]
private predicate revFlowConsCandStoreReadMatchingDisabled(Ap cons, Content c, Ap tail) {
not enableStoreReadMatching() and
not PrevStage::providesStoreReadMatching() and
revFlowConsCand(_, cons, c, tail)
}

Expand Down Expand Up @@ -2481,7 +2492,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
}

pragma[nomagic]
predicate storeStepCand(
private predicate storeStepCand0(
NodeEx node1, Ap ap1, Content c, NodeEx node2, DataFlowType contentType,
DataFlowType containerType
) {
Expand All @@ -2493,7 +2504,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
}

pragma[nomagic]
predicate readStepCand(NodeEx node1, Content c, NodeEx node2) {
private predicate readStepCand0(NodeEx node1, Content c, NodeEx node2) {
exists(Ap ap1, Ap ap2 |
revFlow(node2, _, _, _, pragma[only_bind_into](ap2)) and
readStepFwd(node1, ap1, c, node2, ap2) and
Expand All @@ -2514,12 +2525,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
private predicate fwdConsCand(Content c, Typ t, Ap ap) { storeStepFwd(_, t, ap, c, _, _) }

private predicate revConsCand(NodeEx readTarget, Content c, Typ t, Ap ap) {
exists(NodeEx storeSource, Ap ap2 |
revFlowStore(ap2, c, ap, t, storeSource, _, _, _, _) and
revFlowConsCand(readTarget, ap2, c, ap) and
if enableStoreReadMatching()
then storeMayReachRead(storeSource, c, readTarget)
else any()
exists(Ap ap2 |
revFlowStore(ap2, c, ap, t, _, _, _, _, _) and
revFlowConsCand(readTarget, ap2, c, ap)
)
}

Expand Down Expand Up @@ -2622,6 +2630,21 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
callEdgeReturn(call, c, _, _, _, _, _)
}

pragma[nomagic]
predicate storeStepCand(
NodeEx node1, Ap ap1, Content c, NodeEx node2, DataFlowType contentType,
DataFlowType containerType
) {
storeStepCand0(node1, ap1, c, node2, contentType, containerType) and
storeMayReachRead(node1, c, _)
}

pragma[nomagic]
predicate readStepCand(NodeEx node1, Content c, NodeEx node2) {
readStepCand0(node1, c, node2) and
storeMayReachRead(_, c, node2)
}

additional predicate stats(
boolean fwd, int nodes, int fields, int conscand, int states, int tuples, int calledges,
int tfnodes, int tftuples
Expand Down Expand Up @@ -2797,8 +2820,6 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
predicate typecheckStore(Typ typ, DataFlowType contentType) { any() }

predicate enableTypeFlow() { none() }

predicate enableStoreReadMatching() { none() }
}

private module Stage2 = MkStage<Stage1>::Stage<Stage2Param>;
Expand Down Expand Up @@ -3445,7 +3466,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
pragma[nomagic]
predicate localValueStep(NodeEx node1, NodeEx node2, LocalCc lcc) {
exists(FlowState state |
localFlowBigStep(node1, _, node2, _, true, _, _, _) and
localFlowBigStep(node1, _, node2, _, true, _, lcc, _) and
PrevStage::revFlow(node1, pragma[only_bind_into](state), _) and
PrevStage::revFlow(node2, pragma[only_bind_into](state), _) and
exists(lcc)

Check warning

Code scanning / CodeQL

Superfluous 'exists' conjunct. Warning

This conjunct is superfluous as the existence is implied by
this conjunct
Loading
.
Expand All @@ -3456,7 +3477,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
predicate localTaintStep(
NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, Typ t, LocalCc lcc
) {
localFlowBigStep(node1, state1, node2, state2, false, t, _, _) and
localFlowBigStep(node1, state1, node2, state2, false, t, lcc, _) and
PrevStage::revFlow(node1, pragma[only_bind_into](state1), _) and
PrevStage::revFlow(node2, pragma[only_bind_into](state2), _) and
exists(lcc)

Check warning

Code scanning / CodeQL

Superfluous 'exists' conjunct. Warning

This conjunct is superfluous as the existence is implied by
this conjunct
Loading
.
Expand Down
40 changes: 20 additions & 20 deletions shared/dataflow/codeql/dataflow/internal/DataFlowImplCommon.qll
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2363,15 +2363,15 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
Content getHead();
}

predicate revFlow(NodeEx node, Ap ap);
predicate nodeApRange(NodeEx node, Ap ap);

predicate localValueStep(NodeEx node1, NodeEx node2);

predicate jumpValueStep(NodeEx node1, NodeEx node2);

predicate callEdgeArgParam(NodeEx arg, NodeEx param, Ap ap);
predicate callEdgeArgParam(NodeEx arg, NodeEx param);

predicate callEdgeReturn(NodeEx ret, NodeEx out, Ap ap);
predicate callEdgeReturn(NodeEx ret, NodeEx out);

predicate readContentStep(NodeEx node1, Content c, NodeEx node2);

Expand Down Expand Up @@ -2410,16 +2410,16 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
pragma[nomagic]
private predicate valueStep(NodeEx node1, NodeEx node2) {
exists(ApCons ap |
revFlow(node1, pragma[only_bind_into](ap)) and
revFlow(node2, pragma[only_bind_into](ap))
nodeApRange(node1, pragma[only_bind_into](ap)) and
nodeApRange(node2, pragma[only_bind_into](ap))
|
localValueStep(node1, node2)
or
jumpValueStep(node1, node2)
or
callEdgeArgParam(node1, node2, ap)
callEdgeArgParam(node1, node2)
or
callEdgeReturn(node1, node2, ap)
callEdgeReturn(node1, node2)
)
}

Expand Down Expand Up @@ -2448,7 +2448,7 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
private newtype TNodeOrContent =
TNodeOrContentNode(NodeEx n, ApCons ap, UsesPrevDeltaInfo usesPrevDelta) {
enabled() and
revFlow(n, ap)
nodeApRange(n, ap)
} or
TNodeOrContentContentStart(Content c) { enabled() and storeContentStep(_, c, _) } or
TNodeOrContentContentEnd(Content c) { enabled() and readContentStep(_, c, _) }
Expand All @@ -2471,6 +2471,10 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
}
}

bindingset[ap, result]
pragma[inline_late]
private Content getHeadInlineLate(Ap ap) { result = ap.getHead() }

pragma[nomagic]
private predicate step(NodeOrContent node1, NodeOrContent node2) {
exists(
Expand Down Expand Up @@ -2530,22 +2534,24 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
)
}

pragma[nomagic]
private predicate isStoreTarget0(NodeOrContent node, Content c) {
exists(Ap ap, UsesPrevDeltaInfo usesPrevDelta |
contentIsReadAndStored(c) and
storeContentStep(_, c, node.asNodeEx(ap, usesPrevDelta)) and
c = ap.getHead() and
c = getHeadInlineLate(ap) and
usesPrevDelta.toBoolean() = false
)
}

private predicate isStoreTarget(NodeOrContent node) { isStoreTarget0(node, _) }

pragma[nomagic]
private predicate isReadSource0(NodeOrContent node, Content c) {
exists(Ap ap, UsesPrevDeltaInfo usesPrevDelta |
contentIsReadAndStored(c) and
readContentStep(node.asNodeEx(ap, usesPrevDelta), c, _) and
c = ap.getHead() and
c = getHeadInlineLate(ap) and
usesPrevDelta.toBoolean() = true
)
}
Expand Down Expand Up @@ -2584,15 +2590,9 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
)
}

private predicate isStoreTargetPruned(NodeOrContent node) {
isStoreTarget(node) and
storeMayReachARead(node, _)
}
private predicate isStoreTargetPruned(NodeOrContent node) { storeMayReachARead(node, _) }

private predicate isReadSourcePruned(NodeOrContent node) {
isReadSource(node) and
aStoreMayReachRead(node, _)
}
private predicate isReadSourcePruned(NodeOrContent node) { aStoreMayReachRead(node, _) }

private predicate storeMayReachReadTc(NodeOrContent node1, NodeOrContent node2) =
doublyBoundedFastTC(step/2, isStoreTargetPruned/1, isReadSourcePruned/1)(node1, node2)
Expand All @@ -2602,7 +2602,7 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
exists(Ap ap, UsesPrevDeltaInfo usesPrevDelta |
storeMayReachARead(node2, c) and
storeContentStep(node1, c, node2.asNodeEx(ap, usesPrevDelta)) and
c = ap.getHead() and
c = getHeadInlineLate(ap) and
usesPrevDelta.toBoolean() = false
)
}
Expand All @@ -2612,7 +2612,7 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
exists(Ap ap, UsesPrevDeltaInfo usesPrevDelta |
aStoreMayReachRead(node1, c) and
readContentStep(node1.asNodeEx(ap, usesPrevDelta), c, node2) and
c = ap.getHead() and
c = getHeadInlineLate(ap) and
usesPrevDelta.toBoolean() = true
)
}
Expand Down
Loading

0 comments on commit 5ce9a85

Please sign in to comment.