Skip to content

Commit

Permalink
refactor
Browse files Browse the repository at this point in the history
  • Loading branch information
@hvitved
hvitved committed Dec 10, 2024
1 parent 7bb0a4b commit c66f6ca
Show file tree
Hide file tree
Showing 2 changed files with 142 additions and 102 deletions.
4 changes: 2 additions & 2 deletions cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/ProductFlow.qll
View file
Original file line number Diff line number Diff line change
Expand Up @@ -546,7 +546,7 @@ module ProductFlow {
Flow1::PathGraph::edges(pred1, succ1, _, _) and
exists(ReturnKindExt returnKind |
succ1.getNode() = getAnOutNodeExt(call, returnKind) and
returnKind = getParamReturnPosition(_, pred1.asParameterReturnNode()).getKind()
returnKind = getParamReturnPosition(pred1.asParameterReturnNode()).getKind()
)
}

Expand Down Expand Up @@ -574,7 +574,7 @@ module ProductFlow {
Flow2::PathGraph::edges(pred2, succ2, _, _) and
exists(ReturnKindExt returnKind |
succ2.getNode() = getAnOutNodeExt(call, returnKind) and
returnKind = getParamReturnPosition(_, pred2.asParameterReturnNode()).getKind()
returnKind = getParamReturnPosition(pred2.asParameterReturnNode()).getKind()
)
}

Expand Down
240 changes: 140 additions & 100 deletions shared/dataflow/codeql/dataflow/internal/DataFlowImplCommon.qll
View file
Original file line number Diff line number Diff line change
Expand Up @@ -119,7 +119,15 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
}

// TODO: support setters
predicate storeStep(Node n1, Node n2, Content f) { storeSet(n1, f, n2, _, _) }
predicate storeStep(Node n1, Node n2, Content f) {
storeSet(n1, f, n2)
or
exists(Node pre1, Node pre2 |
pre1 = n1.(PostUpdateNode).getPreUpdateNode() and
pre2 = n2.(PostUpdateNode).getPreUpdateNode() and
argumentValueFlowsThrough(pre2, TReadStepTypesSome(_, f, _), pre1, _)
)
}

private predicate loadStep0(Node n1, Node n2, Content f) {
readSet(n1, f, n2)
Expand Down Expand Up @@ -872,7 +880,6 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
or
exists(Node n | this.isImplicitReadNode(n) | result = n.toString() + " [Ext]")
or
// exists(boolean b | result = this.asNodeReverse(b).toString() + " [Reverse, " + b + "]")
result = this.asNodeReverse(_).toString() + " [Reverse]"
}

Expand Down Expand Up @@ -968,46 +975,41 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
}
}

final class ArgNodeEx extends NodeEx {
abstract class ArgNodeEx extends NodeEx {
abstract predicate argumentOf(DataFlowCallEx call, ArgumentPositionEx pos);

DataFlowCallEx getCall() { this.argumentOf(result, _) }
}

final class NormalArgNodeEx extends ArgNodeEx {
private DataFlowCallEx call_;
private ArgumentPositionEx pos_;

ArgNodeEx() {
NormalArgNodeEx() {
this.asNode().(ArgNode).argumentOf(call_.asDataFlowCall(true), pos_.asArgumentPosition())
or
exists(boolean allowFwdFlowOut |
pragma[only_bind_into](this.asNodeReverse(allowFwdFlowOut)) =
getAnOutNode(call_.asDataFlowCall(allowFwdFlowOut),
pos_.asReturnKind().(ValueReturnKind).getKind())
)
}

predicate argumentOf(DataFlowCallEx call, ArgumentPositionEx pos) {
override predicate argumentOf(DataFlowCallEx call, ArgumentPositionEx pos) {
call = call_ and
pos = pos_
}
}

DataFlowCallEx getCall() { this.argumentOf(result, _) }
abstract class ParamNodeEx extends NodeEx {
abstract predicate isParameterOf(DataFlowCallable c, ParameterPositionEx pos);

ParameterPositionEx getPosition() { this.isParameterOf(_, result) }
}

final class ParamNodeEx extends NodeEx {
final class NormalParamNodeEx extends ParamNodeEx {
private DataFlowCallable c_;
private ParameterPositionEx pos_;

ParamNodeEx() {
this.asNode().(ParamNode).isParameterOf(c_, pos_.asParameterPosition())
or
// todo: returnkindext?
exists(ReturnPosition pos |
pos = getValueReturnPosition(this.asNodeReverse(true)) and
c_ = pos.getCallable() and
pos_.asReturnKind() = pos.getKind()
)
}
NormalParamNodeEx() { this.asNode().(ParamNode).isParameterOf(c_, pos_.asParameterPosition()) }

predicate isParameterOf(DataFlowCallable c, ParameterPositionEx pos) { c = c_ and pos = pos_ }

ParameterPositionEx getPosition() { this.isParameterOf(_, result) }
override predicate isParameterOf(DataFlowCallable c, ParameterPositionEx pos) {
c = c_ and pos = pos_
}
}

/**
Expand All @@ -1017,11 +1019,7 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
final class RetNodeEx extends NodeEx {
private ReturnPosition pos;

RetNodeEx() {
pos = getReturnPositionEx(this) //and
// this.toString() = "this [Reverse]" and
// this.getLocation().getStartLine() = 71
}
RetNodeEx() { pos = getReturnPositionEx(this) }

ReturnPosition getReturnPosition() { result = pos }

Expand All @@ -1044,6 +1042,104 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
not exists(getSecondLevelScope(n))
}

private module ReverseFlow {
/**
* Holds if the local step from `arg` to `out` actually models a flow-through
* step.
*/
pragma[nomagic]
private predicate isFlowThroughLocalStep(ArgNode arg, OutNode out, string model) {
exists(DataFlowCall c |
out = getAnOutNode(c, _) and
arg.argumentOf(c, _) and
simpleLocalFlowStep(arg, out, model)
)
}

predicate localFlowStep(NodeEx node1, NodeEx node2, string model) {
// as soon as we take a reverse local step, forward out flow must be prohibited
// in order to prevent time travelling
exists(Node n1, Node n2 |
node1.asNodeReverse(_) = n1 and
node2.asNodeReverse(false) = n2 and
simpleLocalFlowStep(pragma[only_bind_into](n2), pragma[only_bind_into](n1), model) and
validParameterAliasStep(n2, n1) and
not isFlowThroughLocalStep(n2, n1, model)
)
or
exists(Node n1, Node n2, boolean allowFwdFlowOut |
node1.asNodeReverse(pragma[only_bind_into](allowFwdFlowOut)) = n1 and
isFlowThroughLocalStep(n2, n1, model) and
validParameterAliasStep(n2, n1)
|
node2.asNodeReverse(pragma[only_bind_into](allowFwdFlowOut)) = n2
or
allowFwdFlowOut = true and
node2.asNode().(PostUpdateNode).getPreUpdateNode() = n2
)
or
node1.asNode().(PostUpdateNode).getPreUpdateNode() = node2.asNodeReverse(true) and
model = ""
}

predicate storeStep(NodeEx node1, Content c, NodeEx node2) {
exists(ContentSet cs | c = cs.getAStoreContent() |
exists(Node n1, Node n2, boolean allowFwdFlowOut |
n1 = pragma[only_bind_into](node1.asNodeReverse(allowFwdFlowOut)) and
n2 = pragma[only_bind_into](node2.asNodeReverse(allowFwdFlowOut)) and
Lang::readStep(n2, cs, n1) and
// avoid overlap with `storeSet`
not exists(PostUpdateNode pn1, PostUpdateNode pn2 |
n1 = pn1.getPreUpdateNode() and
n2 = pn2.getPreUpdateNode()
)
)
)
}

predicate readStep(NodeEx node1, ContentSet c, NodeEx node2) {
exists(boolean allowFwdFlowOut |
Lang::storeStep(pragma[only_bind_into](node2.asNodeReverse(allowFwdFlowOut)), c,
pragma[only_bind_into](node1.asNodeReverse(allowFwdFlowOut)))
)
}

final class ReverseArgNodeEx extends ArgNodeEx {
private DataFlowCallEx call_;
private ArgumentPositionEx pos_;

ReverseArgNodeEx() {
exists(boolean allowFwdFlowOut |
pragma[only_bind_into](this.asNodeReverse(allowFwdFlowOut)) =
getAnOutNode(call_.asDataFlowCall(allowFwdFlowOut),
pos_.asReturnKind().(ValueReturnKind).getKind())
)
}

override predicate argumentOf(DataFlowCallEx call, ArgumentPositionEx pos) {
call = call_ and
pos = pos_
}
}

final class ReverseParamNodeEx extends ParamNodeEx {
private DataFlowCallable c_;
private ParameterPositionEx pos_;

ReverseParamNodeEx() {
exists(ReturnPosition pos |
pos = getValueReturnPosition(this.asNodeReverse(true)) and
c_ = pos.getCallable() and
pos_.asReturnKind() = pos.getKind()
)
}

override predicate isParameterOf(DataFlowCallable c, ParameterPositionEx pos) {
c = c_ and pos = pos_
}
}
}

cached
private module Cached {
/**
Expand Down Expand Up @@ -1776,29 +1872,17 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
predicate readEx(NodeEx node1, ContentSet c, NodeEx node2) {
readSet(pragma[only_bind_into](node1.asNode()), c, pragma[only_bind_into](node2.asNode()))
or
exists(boolean allowFwdFlowOut |
storeSet(pragma[only_bind_into](node2.asNodeReverse(allowFwdFlowOut)), c,
pragma[only_bind_into](node1.asNodeReverse(allowFwdFlowOut)), _, _)
)
ReverseFlow::readStep(node1, c, node2)
}

cached
predicate storeSet(
Node node1, ContentSet c, Node node2, DataFlowType contentType, DataFlowType containerType
) {
storeStep(node1, c, node2) and
contentType = getNodeDataFlowType(node1) and
containerType = getNodeDataFlowType(node2)
predicate storeSet(Node node1, ContentSet c, Node node2) {
storeStep(node1, c, node2)
or
exists(Node n1, Node n2 |
n1 = node1.(PostUpdateNode).getPreUpdateNode() and
n2 = node2.(PostUpdateNode).getPreUpdateNode()
|
// argumentValueFlowsThrough(n2, TReadStepTypesSome(containerType, c, contentType), n1, _) // TODO
// or
readSet(n2, c, n1) and
contentType = getNodeDataFlowType(n1) and
containerType = getNodeDataFlowType(n2)
n2 = node2.(PostUpdateNode).getPreUpdateNode() and
readSet(n2, c, n1)
)
}

Expand All @@ -1813,23 +1897,14 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
predicate storeEx(
NodeEx node1, Content c, NodeEx node2, DataFlowType contentType, DataFlowType containerType
) {
exists(ContentSet cs | c = cs.getAStoreContent() |
storeSet(pragma[only_bind_into](node1.asNode()), cs, pragma[only_bind_into](node2.asNode()),
contentType, containerType)
exists(ContentSet cs |
c = cs.getAStoreContent() and
contentType = node1.getDataFlowType() and
containerType = node2.getDataFlowType()
|
storeSet(pragma[only_bind_into](node1.asNode()), cs, pragma[only_bind_into](node2.asNode()))
or
exists(Node n1, Node n2, boolean allowFwdFlowOut |
n1 = pragma[only_bind_into](node1.asNodeReverse(allowFwdFlowOut)) and
n2 = pragma[only_bind_into](node2.asNodeReverse(allowFwdFlowOut)) and
readSet(n2, cs, n1) and
contentType = getNodeDataFlowType(n1) and
containerType = getNodeDataFlowType(n2) and
not exists(
PostUpdateNode pn1, PostUpdateNode pn2 // why?
|
n1 = pn1.getPreUpdateNode() and
n2 = pn2.getPreUpdateNode()
)
)
ReverseFlow::storeStep(node1, c, node2)
)
}

Expand Down Expand Up @@ -1992,19 +2067,6 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
TNodeImplicitRead(Node n) or // will be restricted to nodes with actual implicit reads in `DataFlowImpl.qll`
TNodeReverse(Node n, Boolean allowFwdFlowOut)

/**
* Holds if the local step from `arg` to `out` actually models a flow-through
* step.
*/
pragma[nomagic]
private predicate isFlowThroughLocalStep(ArgNode arg, OutNode out, string model) {
exists(DataFlowCall c |
out = getAnOutNode(c, _) and
arg.argumentOf(c, _) and
simpleLocalFlowStep(arg, out, model)
)
}

/**
* Holds if data can flow in one local step from `node1` to `node2`.
*/
Expand All @@ -2016,29 +2078,7 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
simpleLocalFlowStep(pragma[only_bind_into](n1), pragma[only_bind_into](n2), model)
)
or
// as soon as we take a reverse local step, forward out flow must be prohibited
// in order to prevent time travelling
exists(Node n1, Node n2 |
node1.asNodeReverse(_) = n1 and
node2.asNodeReverse(false) = n2 and
simpleLocalFlowStep(pragma[only_bind_into](n2), pragma[only_bind_into](n1), model) and
validParameterAliasStep(n2, n1) and
not isFlowThroughLocalStep(n2, n1, model)
)
or
exists(Node n1, Node n2, boolean allowFwdFlowOut |
node1.asNodeReverse(pragma[only_bind_into](allowFwdFlowOut)) = n1 and
isFlowThroughLocalStep(n2, n1, model) and
validParameterAliasStep(n2, n1)
|
node2.asNodeReverse(pragma[only_bind_into](allowFwdFlowOut)) = n2
or
allowFwdFlowOut = true and
node2.asNode().(PostUpdateNode).getPreUpdateNode() = n2
)
or
node1.asNode().(PostUpdateNode).getPreUpdateNode() = node2.asNodeReverse(true) and
model = ""
ReverseFlow::localFlowStep(node1, node2, model)
}

cached
Expand Down

0 comments on commit c66f6ca

Please sign in to comment.