Data flow: Prune parameter-self flow in stage 1

This commit is contained in:
Tom Hvitved
2024-12-19 20:19:35 +01:00
parent b0062fc727
commit 06ba814929
2 changed files with 61 additions and 28 deletions

View File

@@ -557,17 +557,18 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
)
or
// flow into a callable
fwdFlowIn(_, _, _, node) and
fwdFlowInParam(_, node, _) and
cc = true
or
// flow out of a callable
fwdFlowOut(_, node, false) and
fwdFlowOut(_, _, node, false) and
cc = false
or
// flow through a callable
exists(DataFlowCall call |
fwdFlowOutFromArg(call, node) and
fwdFlowIsEntered(call, cc)
exists(DataFlowCall call, ReturnKindExtOption kind, ReturnKindExtOption disallowReturnKind |
fwdFlowOutFromArg(call, kind, node) and
fwdFlowIsEntered(call, disallowReturnKind, cc) and
kind != disallowReturnKind
)
}
@@ -593,11 +594,30 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
)
}
pragma[nomagic]
private predicate fwdFlowInParam(DataFlowCall call, ParamNodeEx p, Cc cc) {
fwdFlowIn(call, _, cc, p)
}
pragma[nomagic]
private ReturnKindExtOption getDisallowedReturnKind(ParamNodeEx p) {
if allowParameterReturnInSelfEx(p)
then result.isNone()
else p.isParameterOf(_, result.asSome().(ParamUpdateReturnKind).getPosition())
}
/**
* Holds if an argument to `call` is reached in the flow covered by `fwdFlow`.
*/
pragma[nomagic]
private predicate fwdFlowIsEntered(DataFlowCall call, Cc cc) { fwdFlowIn(call, _, cc, _) }
private predicate fwdFlowIsEntered(
DataFlowCall call, ReturnKindExtOption disallowReturnKind, Cc cc
) {
exists(ParamNodeEx p |
fwdFlowInParam(call, p, cc) and
disallowReturnKind = getDisallowedReturnKind(p)
)
}
pragma[nomagic]
private predicate fwdFlowInReducedViableImplInSomeCallContext(
@@ -618,7 +638,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
pragma[nomagic]
private DataFlowCallable viableImplInSomeFwdFlowCallContextExt(DataFlowCall call) {
exists(DataFlowCall ctx |
fwdFlowIsEntered(ctx, _) and
fwdFlowIsEntered(ctx, _, _) and
result = viableImplInCallContextExt(call, ctx)
)
}
@@ -666,17 +686,18 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
// inline to reduce the number of iterations
pragma[inline]
private predicate fwdFlowOut(DataFlowCall call, NodeEx out, Cc cc) {
private predicate fwdFlowOut(DataFlowCall call, ReturnKindExt kind, NodeEx out, Cc cc) {
exists(ReturnPosition pos |
fwdFlowReturnPosition(pos, cc) and
viableReturnPosOutEx(call, pos, out) and
not fullBarrier(out)
not fullBarrier(out) and
kind = pos.getKind()
)
}
pragma[nomagic]
private predicate fwdFlowOutFromArg(DataFlowCall call, NodeEx out) {
fwdFlowOut(call, out, true)
private predicate fwdFlowOutFromArg(DataFlowCall call, ReturnKindExtOption kind, NodeEx out) {
fwdFlowOut(call, kind.asSome(), out, true)
}
private predicate stateStepFwd(FlowState state1, FlowState state2) {
@@ -750,7 +771,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
)
or
// flow into a callable
revFlowIn(_, node, false) and
revFlowIn(_, _, node, false) and
toReturn = false
or
// flow out of a callable
@@ -761,9 +782,10 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
)
or
// flow through a callable
exists(DataFlowCall call |
revFlowInToReturn(call, node) and
revFlowIsReturned(call, toReturn)
exists(DataFlowCall call, ReturnKindExtOption kind, ReturnKindExtOption disallowReturnKind |
revFlowIsReturned(call, kind, toReturn) and
revFlowInToReturn(call, disallowReturnKind, node) and
kind != disallowReturnKind
)
}
@@ -824,16 +846,19 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
// inline to reduce the number of iterations
pragma[inline]
private predicate revFlowIn(DataFlowCall call, ArgNodeEx arg, boolean toReturn) {
exists(ParamNodeEx p |
revFlow(p, toReturn) and
viableParamArgNodeCandFwd1(call, p, arg)
)
private predicate revFlowIn(DataFlowCall call, ParamNodeEx p, ArgNodeEx arg, boolean toReturn) {
revFlow(p, toReturn) and
viableParamArgNodeCandFwd1(call, p, arg)
}
pragma[nomagic]
private predicate revFlowInToReturn(DataFlowCall call, ArgNodeEx arg) {
revFlowIn(call, arg, true)
private predicate revFlowInToReturn(
DataFlowCall call, ReturnKindExtOption disallowReturnKind, ArgNodeEx arg
) {
exists(ParamNodeEx p |
revFlowIn(call, p, arg, true) and
disallowReturnKind = getDisallowedReturnKind(p)
)
}
/**
@@ -842,10 +867,12 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
* reaching an argument of `call`.
*/
pragma[nomagic]
private predicate revFlowIsReturned(DataFlowCall call, boolean toReturn) {
private predicate revFlowIsReturned(
DataFlowCall call, ReturnKindExtOption kind, boolean toReturn
) {
exists(NodeEx out |
revFlow(out, toReturn) and
fwdFlowOutFromArg(call, out)
fwdFlowOutFromArg(call, kind, out)
)
}
@@ -947,10 +974,14 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
pragma[nomagic]
predicate callMayFlowThroughRev(DataFlowCall call) {
exists(ArgNodeEx arg, boolean toReturn |
revFlow(arg, toReturn) and
revFlowInToReturn(call, arg) and
revFlowIsReturned(call, toReturn)
exists(
ArgNodeEx arg, ReturnKindExtOption kind, ReturnKindExtOption disallowReturnKind,
boolean toReturn
|
revFlow(arg, pragma[only_bind_into](toReturn)) and
revFlowIsReturned(call, kind, pragma[only_bind_into](toReturn)) and
revFlowInToReturn(call, disallowReturnKind, arg) and
kind != disallowReturnKind
)
}

View File

@@ -2417,6 +2417,8 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
override string toString() { result = "param update " + pos }
}
class ReturnKindExtOption = Option<ReturnKindExt>::Option;
/** A callable tagged with a relevant return kind. */
class ReturnPosition extends TReturnPosition0 {
private DataFlowCallable c;