Data flow: Sync files

This commit is contained in:
Tom Hvitved
2022-05-04 14:49:26 +02:00
parent 7f7742216c
commit 9cb63c0a5e
28 changed files with 504 additions and 644 deletions

View File

@@ -4206,11 +4206,10 @@ private module Subpaths {
pragma[nomagic]
private predicate subpaths01(
PathNodeImpl arg, ParamNodeEx par, SummaryCtxSome sc, CallContext innercc, ReturnKindExt kind,
NodeEx out, FlowState sout, CallContext ccout, AccessPath apout
NodeEx out, FlowState sout, AccessPath apout
) {
exists(Configuration config |
pathThroughCallable(arg, out, pragma[only_bind_into](sout), ccout,
pragma[only_bind_into](apout)) and
pathThroughCallable(arg, out, pragma[only_bind_into](sout), _, pragma[only_bind_into](apout)) and
pathIntoCallable(arg, par, _, _, innercc, sc, _, config) and
paramFlowsThrough(kind, pragma[only_bind_into](sout), innercc, sc,
pragma[only_bind_into](apout), _, unbindConf(config)) and
@@ -4225,11 +4224,10 @@ private module Subpaths {
pragma[nomagic]
private predicate subpaths02(
PathNode arg, ParamNodeEx par, SummaryCtxSome sc, CallContext innercc, ReturnKindExt kind,
NodeEx out, FlowState sout, CallContext ccout, AccessPath apout, Configuration config
NodeEx out, FlowState sout, AccessPath apout
) {
subpaths01(arg, par, sc, innercc, kind, out, sout, ccout, apout) and
out.asNode() = kind.getAnOutNode(_) and
config = getPathNodeConf(arg)
subpaths01(arg, par, sc, innercc, kind, out, sout, apout) and
out.asNode() = kind.getAnOutNode(_)
}
pragma[nomagic]
@@ -4240,14 +4238,12 @@ private module Subpaths {
*/
pragma[nomagic]
private predicate subpaths03(
PathNodeMid arg, ParamNodeEx par, PathNodeMid ret, NodeEx out, FlowState sout,
CallContext ccout, AccessPath apout, SummaryCtx scout, Configuration config
PathNode arg, ParamNodeEx par, PathNodeMid ret, NodeEx out, FlowState sout, AccessPath apout
) {
exists(SummaryCtxSome sc, CallContext innercc, ReturnKindExt kind, RetNodeEx retnode |
subpaths02(arg, par, sc, innercc, kind, out, sout, ccout, apout, config) and
pathNode(ret, retnode, sout, innercc, sc, apout, config, _) and
kind = retnode.getKind() and
scout = arg.getSummaryCtx()
subpaths02(arg, par, sc, innercc, kind, out, sout, apout) and
pathNode(ret, retnode, sout, innercc, sc, apout, unbindConf(getPathNodeConf(arg)), _) and
kind = retnode.getKind()
)
}
@@ -4267,17 +4263,16 @@ private module Subpaths {
* `ret -> out` is summarized as the edge `arg -> out`.
*/
predicate subpaths(PathNode arg, PathNodeImpl par, PathNodeImpl ret, PathNode out) {
exists(
ParamNodeEx p, NodeEx o, FlowState sout, AccessPath apout, CallContext ccout,
SummaryCtx scout, PathNodeMid out0, Configuration config
|
pragma[only_bind_into](arg).getASuccessor() = par and
subpaths03(arg, p, localStepToHidden*(ret), o, sout, ccout, apout, scout, config) and
pathNode(out0, o, sout, ccout, scout, apout, config, _) and
exists(ParamNodeEx p, NodeEx o, FlowState sout, AccessPath apout, PathNodeMid out0 |
pragma[only_bind_into](arg).getASuccessor() = pragma[only_bind_into](par) and
pragma[only_bind_into](arg).getASuccessor() = out0 and
subpaths03(pragma[only_bind_into](arg), p, localStepToHidden*(ret), o, sout, apout) and
not ret.isHidden() and
par.getNodeEx() = p
|
out = out0 or out = out0.projectToSink()
par.getNodeEx() = p and
out0.getNodeEx() = o and
out0.getState() = sout and
out0.getAp() = apout and
(out = out0 or out = out0.projectToSink())
)
}