Dataflow: Postpone typeflow calledge pruning until stage 3.

This commit is contained in:
Anders Schack-Mulligen 2023-09-08 13:40:31 +02:00
Родитель f5a4b792bd
Коммит 47f68504a8
2 изменённых файлов: 45 добавлений и 24 удалений

Просмотреть файл

@ -1185,6 +1185,8 @@ module MakeImpl<InputSig Lang> {
bindingset[typ, contentType]
predicate typecheckStore(Typ typ, DataFlowType contentType);
default predicate enableTypeFlow() { any() }
}
module Stage<StageParam Param> implements StageSig {
@ -1541,6 +1543,8 @@ module MakeImpl<InputSig Lang> {
}
private module FwdTypeFlowInput implements TypeFlowInput {
predicate enableTypeFlow = Param::enableTypeFlow/0;
predicate relevantCallEdgeIn(DataFlowCall call, DataFlowCallable c) {
flowIntoCallApa(call, c, _, _, _, _)
}
@ -1845,6 +1849,8 @@ module MakeImpl<InputSig Lang> {
}
private module RevTypeFlowInput implements TypeFlowInput {
predicate enableTypeFlow = Param::enableTypeFlow/0;
predicate relevantCallEdgeIn(DataFlowCall call, DataFlowCallable c) {
flowOutOfCallAp(call, c, _, _, _, _)
}
@ -2306,6 +2312,8 @@ module MakeImpl<InputSig Lang> {
bindingset[typ, contentType]
predicate typecheckStore(Typ typ, DataFlowType contentType) { any() }
predicate enableTypeFlow() { none() }
}
private module Stage2 implements StageSig {

Просмотреть файл

@ -971,6 +971,8 @@ module MakeImplCommon<InputSig Lang> {
}
signature module TypeFlowInput {
predicate enableTypeFlow();
/** Holds if the edge is possibly needed in the direction `call` to `c`. */
predicate relevantCallEdgeIn(DataFlowCall call, DataFlowCallable c);
@ -1036,24 +1038,27 @@ module MakeImplCommon<InputSig Lang> {
*/
pragma[nomagic]
private predicate trackedArgTypeCand(ArgNode arg) {
exists(ParamNode p, DataFlowType at, DataFlowType pt |
at = getNodeType(arg) and
pt = getNodeType(p) and
relevantCallEdge(_, _, arg, p) and
typeStrongerThan0(pt, at)
)
or
exists(ParamNode p, DataFlowType at, DataFlowType pt |
at = getNodeType(arg) and
pt = getNodeType(p) and
paramMustFlow(p, arg) and
relevantCallEdge(_, _, arg, _) and
typeStrongerThan0(at, pt)
)
or
exists(ParamNode p |
trackedParamTypeCand(p) and
relevantCallEdge(_, _, arg, p)
Input::enableTypeFlow() and
(
exists(ParamNode p, DataFlowType at, DataFlowType pt |
at = getNodeType(arg) and
pt = getNodeType(p) and
relevantCallEdge(_, _, arg, p) and
typeStrongerThan0(pt, at)
)
or
exists(ParamNode p, DataFlowType at, DataFlowType pt |
at = getNodeType(arg) and
pt = getNodeType(p) and
paramMustFlow(p, arg) and
relevantCallEdge(_, _, arg, _) and
typeStrongerThan0(at, pt)
)
or
exists(ParamNode p |
trackedParamTypeCand(p) and
relevantCallEdge(_, _, arg, p)
)
)
}
@ -1276,10 +1281,14 @@ module MakeImplCommon<InputSig Lang> {
predicate typeFlowValidEdgeIn(DataFlowCall call, DataFlowCallable c, boolean cc) {
Input::relevantCallEdgeIn(call, c) and
cc = [true, false] and
forall(ArgNode arg, ParamNode p |
callEdge(call, c, arg, p) and trackedArgType(arg) and paramMustFlow(_, arg)
|
validArgParamIn(arg, p, cc)
(
not Input::enableTypeFlow()
or
forall(ArgNode arg, ParamNode p |
callEdge(call, c, arg, p) and trackedArgType(arg) and paramMustFlow(_, arg)
|
validArgParamIn(arg, p, cc)
)
)
}
@ -1313,8 +1322,12 @@ module MakeImplCommon<InputSig Lang> {
*/
predicate typeFlowValidEdgeOut(DataFlowCall call, DataFlowCallable c) {
Input::relevantCallEdgeOut(call, c) and
forall(ArgNode arg, ParamNode p | callEdge(call, c, arg, p) and trackedParamType(p) |
validArgParamOut(arg, p)
(
not Input::enableTypeFlow()
or
forall(ArgNode arg, ParamNode p | callEdge(call, c, arg, p) and trackedParamType(p) |
validArgParamOut(arg, p)
)
)
}
}