Skip to content

Commit

Permalink
refactor2
Browse files Browse the repository at this point in the history
  • Loading branch information
@hvitved
hvitved committed Aug 5, 2024
1 parent 9f9aaa6 commit 9c4a378
Show file tree
Hide file tree
Showing 3 changed files with 77 additions and 82 deletions.
105 changes: 57 additions & 48 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 @@ -1482,43 +1488,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 @@ -1562,7 +1574,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 @@ -1689,8 +1701,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 @@ -1699,13 +1710,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 @@ -1720,14 +1732,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 @@ -1740,8 +1752,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 @@ -2392,7 +2403,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 @@ -2513,7 +2524,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 @@ -2525,7 +2536,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 @@ -2546,12 +2557,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 @@ -2856,8 +2864,14 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
// read
exists(NodeEx mid, Typ t0, Ap ap0, Content c |
pn1 = TStagePathNodeMid(mid, state, cc, summaryCtx, argT, argAp, t0, ap0) and
fwdFlowRead(t0, ap0, c, mid, node, state, cc, summaryCtx, argT, argAp) and
fwdFlowConsCand(t0, ap0, c, t, ap)
fwdFlowRead(t0, ap0, c, mid, node, state, cc, summaryCtx, argT, argAp)
|
exists(NodeEx storeSource |
fwdFlowConsCandStoreReadMatchingEnabled(storeSource, t0, ap0, c, t, ap) and
storeMayReachReadInlineLate(storeSource, c, node)
)
or
fwdFlowConsCandStoreReadMatchingDisabled(t0, ap0, c, t, ap)
)
or
// flow into a callable
Expand Down Expand Up @@ -2933,8 +2947,6 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
* be able to handle access paths of maximum length 5.
*/
private module StoreReadReachability {
final private class ApFinal = Ap;

private class ApCons extends ApFinal {
ApCons() { not this instanceof ApNil }
}
Expand Down Expand Up @@ -3380,8 +3392,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 @@ -3631,7 +3641,8 @@ 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, _, _, _) and
exists(t) and
exists(lcc)
}

Expand Down Expand Up @@ -4031,21 +4042,19 @@ 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)
PrevStage::revFlow(node2, pragma[only_bind_into](state), _)
)
}

pragma[nomagic]
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)
PrevStage::revFlow(node2, pragma[only_bind_into](state2), _)
}

bindingset[node, state, t0, ap]
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 9c4a378

Please sign in to comment.