Data flow: Adjust callMayFlowThroughFwd pragmas

This commit is contained in:
Tom Hvitved
2021-09-01 12:02:37 +02:00
parent c3ecae503b
commit 296d10fe2a
25 changed files with 375 additions and 225 deletions

View File

@@ -1170,10 +1170,12 @@ private module Stage2 {
pragma[nomagic]
private predicate callMayFlowThroughFwd(DataFlowCall call, Configuration config) {
exists(Ap argAp0, NodeEx out, Cc cc, ApOption argAp, Ap ap |
fwdFlow(pragma[only_bind_out](out), pragma[only_bind_out](cc), pragma[only_bind_out](argAp),
pragma[only_bind_out](ap), pragma[only_bind_out](config)) and
fwdFlow(out, pragma[only_bind_into](cc), pragma[only_bind_into](argAp), ap,
pragma[only_bind_into](config)) and
fwdFlowOutFromArg(call, out, argAp0, ap, config) and
fwdFlowIsEntered(call, cc, argAp, argAp0, config)
fwdFlowIsEntered(pragma[only_bind_into](call), pragma[only_bind_into](cc),
pragma[only_bind_into](argAp), pragma[only_bind_into](argAp0),
pragma[only_bind_into](config))
)
}
@@ -1857,10 +1859,12 @@ private module Stage3 {
pragma[nomagic]
private predicate callMayFlowThroughFwd(DataFlowCall call, Configuration config) {
exists(Ap argAp0, NodeEx out, Cc cc, ApOption argAp, Ap ap |
fwdFlow(pragma[only_bind_out](out), pragma[only_bind_out](cc), pragma[only_bind_out](argAp),
pragma[only_bind_out](ap), pragma[only_bind_out](config)) and
fwdFlow(out, pragma[only_bind_into](cc), pragma[only_bind_into](argAp), ap,
pragma[only_bind_into](config)) and
fwdFlowOutFromArg(call, out, argAp0, ap, config) and
fwdFlowIsEntered(call, cc, argAp, argAp0, config)
fwdFlowIsEntered(pragma[only_bind_into](call), pragma[only_bind_into](cc),
pragma[only_bind_into](argAp), pragma[only_bind_into](argAp0),
pragma[only_bind_into](config))
)
}
@@ -2614,10 +2618,12 @@ private module Stage4 {
pragma[nomagic]
private predicate callMayFlowThroughFwd(DataFlowCall call, Configuration config) {
exists(Ap argAp0, NodeEx out, Cc cc, ApOption argAp, Ap ap |
fwdFlow(pragma[only_bind_out](out), pragma[only_bind_out](cc), pragma[only_bind_out](argAp),
pragma[only_bind_out](ap), pragma[only_bind_out](config)) and
fwdFlow(out, pragma[only_bind_into](cc), pragma[only_bind_into](argAp), ap,
pragma[only_bind_into](config)) and
fwdFlowOutFromArg(call, out, argAp0, ap, config) and
fwdFlowIsEntered(call, cc, argAp, argAp0, config)
fwdFlowIsEntered(pragma[only_bind_into](call), pragma[only_bind_into](cc),
pragma[only_bind_into](argAp), pragma[only_bind_into](argAp0),
pragma[only_bind_into](config))
)
}

View File

@@ -1170,10 +1170,12 @@ private module Stage2 {
pragma[nomagic]
private predicate callMayFlowThroughFwd(DataFlowCall call, Configuration config) {
exists(Ap argAp0, NodeEx out, Cc cc, ApOption argAp, Ap ap |
fwdFlow(pragma[only_bind_out](out), pragma[only_bind_out](cc), pragma[only_bind_out](argAp),
pragma[only_bind_out](ap), pragma[only_bind_out](config)) and
fwdFlow(out, pragma[only_bind_into](cc), pragma[only_bind_into](argAp), ap,
pragma[only_bind_into](config)) and
fwdFlowOutFromArg(call, out, argAp0, ap, config) and
fwdFlowIsEntered(call, cc, argAp, argAp0, config)
fwdFlowIsEntered(pragma[only_bind_into](call), pragma[only_bind_into](cc),
pragma[only_bind_into](argAp), pragma[only_bind_into](argAp0),
pragma[only_bind_into](config))
)
}
@@ -1857,10 +1859,12 @@ private module Stage3 {
pragma[nomagic]
private predicate callMayFlowThroughFwd(DataFlowCall call, Configuration config) {
exists(Ap argAp0, NodeEx out, Cc cc, ApOption argAp, Ap ap |
fwdFlow(pragma[only_bind_out](out), pragma[only_bind_out](cc), pragma[only_bind_out](argAp),
pragma[only_bind_out](ap), pragma[only_bind_out](config)) and
fwdFlow(out, pragma[only_bind_into](cc), pragma[only_bind_into](argAp), ap,
pragma[only_bind_into](config)) and
fwdFlowOutFromArg(call, out, argAp0, ap, config) and
fwdFlowIsEntered(call, cc, argAp, argAp0, config)
fwdFlowIsEntered(pragma[only_bind_into](call), pragma[only_bind_into](cc),
pragma[only_bind_into](argAp), pragma[only_bind_into](argAp0),
pragma[only_bind_into](config))
)
}
@@ -2614,10 +2618,12 @@ private module Stage4 {
pragma[nomagic]
private predicate callMayFlowThroughFwd(DataFlowCall call, Configuration config) {
exists(Ap argAp0, NodeEx out, Cc cc, ApOption argAp, Ap ap |
fwdFlow(pragma[only_bind_out](out), pragma[only_bind_out](cc), pragma[only_bind_out](argAp),
pragma[only_bind_out](ap), pragma[only_bind_out](config)) and
fwdFlow(out, pragma[only_bind_into](cc), pragma[only_bind_into](argAp), ap,
pragma[only_bind_into](config)) and
fwdFlowOutFromArg(call, out, argAp0, ap, config) and
fwdFlowIsEntered(call, cc, argAp, argAp0, config)
fwdFlowIsEntered(pragma[only_bind_into](call), pragma[only_bind_into](cc),
pragma[only_bind_into](argAp), pragma[only_bind_into](argAp0),
pragma[only_bind_into](config))
)
}

View File

@@ -1170,10 +1170,12 @@ private module Stage2 {
pragma[nomagic]
private predicate callMayFlowThroughFwd(DataFlowCall call, Configuration config) {
exists(Ap argAp0, NodeEx out, Cc cc, ApOption argAp, Ap ap |
fwdFlow(pragma[only_bind_out](out), pragma[only_bind_out](cc), pragma[only_bind_out](argAp),
pragma[only_bind_out](ap), pragma[only_bind_out](config)) and
fwdFlow(out, pragma[only_bind_into](cc), pragma[only_bind_into](argAp), ap,
pragma[only_bind_into](config)) and
fwdFlowOutFromArg(call, out, argAp0, ap, config) and
fwdFlowIsEntered(call, cc, argAp, argAp0, config)
fwdFlowIsEntered(pragma[only_bind_into](call), pragma[only_bind_into](cc),
pragma[only_bind_into](argAp), pragma[only_bind_into](argAp0),
pragma[only_bind_into](config))
)
}
@@ -1857,10 +1859,12 @@ private module Stage3 {
pragma[nomagic]
private predicate callMayFlowThroughFwd(DataFlowCall call, Configuration config) {
exists(Ap argAp0, NodeEx out, Cc cc, ApOption argAp, Ap ap |
fwdFlow(pragma[only_bind_out](out), pragma[only_bind_out](cc), pragma[only_bind_out](argAp),
pragma[only_bind_out](ap), pragma[only_bind_out](config)) and
fwdFlow(out, pragma[only_bind_into](cc), pragma[only_bind_into](argAp), ap,
pragma[only_bind_into](config)) and
fwdFlowOutFromArg(call, out, argAp0, ap, config) and
fwdFlowIsEntered(call, cc, argAp, argAp0, config)
fwdFlowIsEntered(pragma[only_bind_into](call), pragma[only_bind_into](cc),
pragma[only_bind_into](argAp), pragma[only_bind_into](argAp0),
pragma[only_bind_into](config))
)
}
@@ -2614,10 +2618,12 @@ private module Stage4 {
pragma[nomagic]
private predicate callMayFlowThroughFwd(DataFlowCall call, Configuration config) {
exists(Ap argAp0, NodeEx out, Cc cc, ApOption argAp, Ap ap |
fwdFlow(pragma[only_bind_out](out), pragma[only_bind_out](cc), pragma[only_bind_out](argAp),
pragma[only_bind_out](ap), pragma[only_bind_out](config)) and
fwdFlow(out, pragma[only_bind_into](cc), pragma[only_bind_into](argAp), ap,
pragma[only_bind_into](config)) and
fwdFlowOutFromArg(call, out, argAp0, ap, config) and
fwdFlowIsEntered(call, cc, argAp, argAp0, config)
fwdFlowIsEntered(pragma[only_bind_into](call), pragma[only_bind_into](cc),
pragma[only_bind_into](argAp), pragma[only_bind_into](argAp0),
pragma[only_bind_into](config))
)
}

View File

@@ -1170,10 +1170,12 @@ private module Stage2 {
pragma[nomagic]
private predicate callMayFlowThroughFwd(DataFlowCall call, Configuration config) {
exists(Ap argAp0, NodeEx out, Cc cc, ApOption argAp, Ap ap |
fwdFlow(pragma[only_bind_out](out), pragma[only_bind_out](cc), pragma[only_bind_out](argAp),
pragma[only_bind_out](ap), pragma[only_bind_out](config)) and
fwdFlow(out, pragma[only_bind_into](cc), pragma[only_bind_into](argAp), ap,
pragma[only_bind_into](config)) and
fwdFlowOutFromArg(call, out, argAp0, ap, config) and
fwdFlowIsEntered(call, cc, argAp, argAp0, config)
fwdFlowIsEntered(pragma[only_bind_into](call), pragma[only_bind_into](cc),
pragma[only_bind_into](argAp), pragma[only_bind_into](argAp0),
pragma[only_bind_into](config))
)
}
@@ -1857,10 +1859,12 @@ private module Stage3 {
pragma[nomagic]
private predicate callMayFlowThroughFwd(DataFlowCall call, Configuration config) {
exists(Ap argAp0, NodeEx out, Cc cc, ApOption argAp, Ap ap |
fwdFlow(pragma[only_bind_out](out), pragma[only_bind_out](cc), pragma[only_bind_out](argAp),
pragma[only_bind_out](ap), pragma[only_bind_out](config)) and
fwdFlow(out, pragma[only_bind_into](cc), pragma[only_bind_into](argAp), ap,
pragma[only_bind_into](config)) and
fwdFlowOutFromArg(call, out, argAp0, ap, config) and
fwdFlowIsEntered(call, cc, argAp, argAp0, config)
fwdFlowIsEntered(pragma[only_bind_into](call), pragma[only_bind_into](cc),
pragma[only_bind_into](argAp), pragma[only_bind_into](argAp0),
pragma[only_bind_into](config))
)
}
@@ -2614,10 +2618,12 @@ private module Stage4 {
pragma[nomagic]
private predicate callMayFlowThroughFwd(DataFlowCall call, Configuration config) {
exists(Ap argAp0, NodeEx out, Cc cc, ApOption argAp, Ap ap |
fwdFlow(pragma[only_bind_out](out), pragma[only_bind_out](cc), pragma[only_bind_out](argAp),
pragma[only_bind_out](ap), pragma[only_bind_out](config)) and
fwdFlow(out, pragma[only_bind_into](cc), pragma[only_bind_into](argAp), ap,
pragma[only_bind_into](config)) and
fwdFlowOutFromArg(call, out, argAp0, ap, config) and
fwdFlowIsEntered(call, cc, argAp, argAp0, config)
fwdFlowIsEntered(pragma[only_bind_into](call), pragma[only_bind_into](cc),
pragma[only_bind_into](argAp), pragma[only_bind_into](argAp0),
pragma[only_bind_into](config))
)
}

View File

@@ -1170,10 +1170,12 @@ private module Stage2 {
pragma[nomagic]
private predicate callMayFlowThroughFwd(DataFlowCall call, Configuration config) {
exists(Ap argAp0, NodeEx out, Cc cc, ApOption argAp, Ap ap |
fwdFlow(pragma[only_bind_out](out), pragma[only_bind_out](cc), pragma[only_bind_out](argAp),
pragma[only_bind_out](ap), pragma[only_bind_out](config)) and
fwdFlow(out, pragma[only_bind_into](cc), pragma[only_bind_into](argAp), ap,
pragma[only_bind_into](config)) and
fwdFlowOutFromArg(call, out, argAp0, ap, config) and
fwdFlowIsEntered(call, cc, argAp, argAp0, config)
fwdFlowIsEntered(pragma[only_bind_into](call), pragma[only_bind_into](cc),
pragma[only_bind_into](argAp), pragma[only_bind_into](argAp0),
pragma[only_bind_into](config))
)
}
@@ -1857,10 +1859,12 @@ private module Stage3 {
pragma[nomagic]
private predicate callMayFlowThroughFwd(DataFlowCall call, Configuration config) {
exists(Ap argAp0, NodeEx out, Cc cc, ApOption argAp, Ap ap |
fwdFlow(pragma[only_bind_out](out), pragma[only_bind_out](cc), pragma[only_bind_out](argAp),
pragma[only_bind_out](ap), pragma[only_bind_out](config)) and
fwdFlow(out, pragma[only_bind_into](cc), pragma[only_bind_into](argAp), ap,
pragma[only_bind_into](config)) and
fwdFlowOutFromArg(call, out, argAp0, ap, config) and
fwdFlowIsEntered(call, cc, argAp, argAp0, config)
fwdFlowIsEntered(pragma[only_bind_into](call), pragma[only_bind_into](cc),
pragma[only_bind_into](argAp), pragma[only_bind_into](argAp0),
pragma[only_bind_into](config))
)
}
@@ -2614,10 +2618,12 @@ private module Stage4 {
pragma[nomagic]
private predicate callMayFlowThroughFwd(DataFlowCall call, Configuration config) {
exists(Ap argAp0, NodeEx out, Cc cc, ApOption argAp, Ap ap |
fwdFlow(pragma[only_bind_out](out), pragma[only_bind_out](cc), pragma[only_bind_out](argAp),
pragma[only_bind_out](ap), pragma[only_bind_out](config)) and
fwdFlow(out, pragma[only_bind_into](cc), pragma[only_bind_into](argAp), ap,
pragma[only_bind_into](config)) and
fwdFlowOutFromArg(call, out, argAp0, ap, config) and
fwdFlowIsEntered(call, cc, argAp, argAp0, config)
fwdFlowIsEntered(pragma[only_bind_into](call), pragma[only_bind_into](cc),
pragma[only_bind_into](argAp), pragma[only_bind_into](argAp0),
pragma[only_bind_into](config))
)
}

View File

@@ -1170,10 +1170,12 @@ private module Stage2 {
pragma[nomagic]
private predicate callMayFlowThroughFwd(DataFlowCall call, Configuration config) {
exists(Ap argAp0, NodeEx out, Cc cc, ApOption argAp, Ap ap |
fwdFlow(pragma[only_bind_out](out), pragma[only_bind_out](cc), pragma[only_bind_out](argAp),
pragma[only_bind_out](ap), pragma[only_bind_out](config)) and
fwdFlow(out, pragma[only_bind_into](cc), pragma[only_bind_into](argAp), ap,
pragma[only_bind_into](config)) and
fwdFlowOutFromArg(call, out, argAp0, ap, config) and
fwdFlowIsEntered(call, cc, argAp, argAp0, config)
fwdFlowIsEntered(pragma[only_bind_into](call), pragma[only_bind_into](cc),
pragma[only_bind_into](argAp), pragma[only_bind_into](argAp0),
pragma[only_bind_into](config))
)
}
@@ -1857,10 +1859,12 @@ private module Stage3 {
pragma[nomagic]
private predicate callMayFlowThroughFwd(DataFlowCall call, Configuration config) {
exists(Ap argAp0, NodeEx out, Cc cc, ApOption argAp, Ap ap |
fwdFlow(pragma[only_bind_out](out), pragma[only_bind_out](cc), pragma[only_bind_out](argAp),
pragma[only_bind_out](ap), pragma[only_bind_out](config)) and
fwdFlow(out, pragma[only_bind_into](cc), pragma[only_bind_into](argAp), ap,
pragma[only_bind_into](config)) and
fwdFlowOutFromArg(call, out, argAp0, ap, config) and
fwdFlowIsEntered(call, cc, argAp, argAp0, config)
fwdFlowIsEntered(pragma[only_bind_into](call), pragma[only_bind_into](cc),
pragma[only_bind_into](argAp), pragma[only_bind_into](argAp0),
pragma[only_bind_into](config))
)
}
@@ -2614,10 +2618,12 @@ private module Stage4 {
pragma[nomagic]
private predicate callMayFlowThroughFwd(DataFlowCall call, Configuration config) {
exists(Ap argAp0, NodeEx out, Cc cc, ApOption argAp, Ap ap |
fwdFlow(pragma[only_bind_out](out), pragma[only_bind_out](cc), pragma[only_bind_out](argAp),
pragma[only_bind_out](ap), pragma[only_bind_out](config)) and
fwdFlow(out, pragma[only_bind_into](cc), pragma[only_bind_into](argAp), ap,
pragma[only_bind_into](config)) and
fwdFlowOutFromArg(call, out, argAp0, ap, config) and
fwdFlowIsEntered(call, cc, argAp, argAp0, config)
fwdFlowIsEntered(pragma[only_bind_into](call), pragma[only_bind_into](cc),
pragma[only_bind_into](argAp), pragma[only_bind_into](argAp0),
pragma[only_bind_into](config))
)
}

View File

@@ -1170,10 +1170,12 @@ private module Stage2 {
pragma[nomagic]
private predicate callMayFlowThroughFwd(DataFlowCall call, Configuration config) {
exists(Ap argAp0, NodeEx out, Cc cc, ApOption argAp, Ap ap |
fwdFlow(pragma[only_bind_out](out), pragma[only_bind_out](cc), pragma[only_bind_out](argAp),
pragma[only_bind_out](ap), pragma[only_bind_out](config)) and
fwdFlow(out, pragma[only_bind_into](cc), pragma[only_bind_into](argAp), ap,
pragma[only_bind_into](config)) and
fwdFlowOutFromArg(call, out, argAp0, ap, config) and
fwdFlowIsEntered(call, cc, argAp, argAp0, config)
fwdFlowIsEntered(pragma[only_bind_into](call), pragma[only_bind_into](cc),
pragma[only_bind_into](argAp), pragma[only_bind_into](argAp0),
pragma[only_bind_into](config))
)
}
@@ -1857,10 +1859,12 @@ private module Stage3 {
pragma[nomagic]
private predicate callMayFlowThroughFwd(DataFlowCall call, Configuration config) {
exists(Ap argAp0, NodeEx out, Cc cc, ApOption argAp, Ap ap |
fwdFlow(pragma[only_bind_out](out), pragma[only_bind_out](cc), pragma[only_bind_out](argAp),
pragma[only_bind_out](ap), pragma[only_bind_out](config)) and
fwdFlow(out, pragma[only_bind_into](cc), pragma[only_bind_into](argAp), ap,
pragma[only_bind_into](config)) and
fwdFlowOutFromArg(call, out, argAp0, ap, config) and
fwdFlowIsEntered(call, cc, argAp, argAp0, config)
fwdFlowIsEntered(pragma[only_bind_into](call), pragma[only_bind_into](cc),
pragma[only_bind_into](argAp), pragma[only_bind_into](argAp0),
pragma[only_bind_into](config))
)
}
@@ -2614,10 +2618,12 @@ private module Stage4 {
pragma[nomagic]
private predicate callMayFlowThroughFwd(DataFlowCall call, Configuration config) {
exists(Ap argAp0, NodeEx out, Cc cc, ApOption argAp, Ap ap |
fwdFlow(pragma[only_bind_out](out), pragma[only_bind_out](cc), pragma[only_bind_out](argAp),
pragma[only_bind_out](ap), pragma[only_bind_out](config)) and
fwdFlow(out, pragma[only_bind_into](cc), pragma[only_bind_into](argAp), ap,
pragma[only_bind_into](config)) and
fwdFlowOutFromArg(call, out, argAp0, ap, config) and
fwdFlowIsEntered(call, cc, argAp, argAp0, config)
fwdFlowIsEntered(pragma[only_bind_into](call), pragma[only_bind_into](cc),
pragma[only_bind_into](argAp), pragma[only_bind_into](argAp0),
pragma[only_bind_into](config))
)
}