Skip to content

Data flow: Take conjunctive With(out)Contents into account in prohibitsUseUseFlow #10691

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 5 commits into from
Oct 6, 2022
Merged

Data flow: Take conjunctive With(out)Contents into account in prohibitsUseUseFlow #10691

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
9d23742
Ruby: Add test that illustrates issue with conjunctive `WithoutContent`s
hvitved Oct 5, 2022
e51c20b
Data flow: Take conjunctive `With(out)Contents` into account in `proh…
hvitved Oct 5, 2022
3f0f16a
Ruby: Update flow summary for `Hash#except`
hvitved Oct 5, 2022
6f518c1
Data flow: Sync files
hvitved Oct 5, 2022
0beea9f
Fix typos
hvitved Oct 5, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
29 changes: 23 additions & 6 deletions csharp/ql/lib/semmle/code/csharp/dataflow/internal/FlowSummaryImpl.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -750,6 +750,27 @@ module Private {
)
}

/**
* Holds if `p` can reach `n` in a summarized callable, using only value-preserving
* local steps. `clearsOrExpects` records whether any node on the path from `p` to
* `n` either clears or expects contents.
*/
private predicate paramReachesLocal(ParamNode p, Node n, boolean clearsOrExpects) {
viableParam(_, _, _, p) and
n = p and
clearsOrExpects = false
or
exists(Node mid, boolean clearsOrExpectsMid |
paramReachesLocal(p, mid, clearsOrExpectsMid) and
summaryLocalStep(mid, n, true) and
if
summaryClearsContent(n, _) or
summaryExpectsContent(n, _)
then clearsOrExpects = true
else clearsOrExpects = clearsOrExpectsMid
)
}

/**
* Holds if use-use flow starting from `arg` should be prohibited.
*
Expand All @@ -759,15 +780,11 @@ module Private {
*/
pragma[nomagic]
predicate prohibitsUseUseFlow(ArgNode arg, SummarizedCallable sc) {
exists(ParamNode p, Node mid, ParameterPosition ppos, Node ret |
exists(ParamNode p, ParameterPosition ppos, Node ret |
paramReachesLocal(p, ret, true) and
p = summaryArgParam0(_, arg, sc) and
p.isParameterOf(_, pragma[only_bind_into](ppos)) and
summaryLocalStep(p, mid, true) and
summaryLocalStep(mid, ret, true) and
isParameterPostUpdate(ret, _, pragma[only_bind_into](ppos))
|
summaryClearsContent(mid, _) or
summaryExpectsContent(mid, _)
)
}

Expand Down
29 changes: 23 additions & 6 deletions java/ql/lib/semmle/code/java/dataflow/internal/FlowSummaryImpl.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -750,6 +750,27 @@ module Private {
)
}

/**
* Holds if `p` can reach `n` in a summarized callable, using only value-preserving
* local steps. `clearsOrExpects` records whether any node on the path from `p` to
* `n` either clears or expects contents.
*/
private predicate paramReachesLocal(ParamNode p, Node n, boolean clearsOrExpects) {
viableParam(_, _, _, p) and
n = p and
clearsOrExpects = false
or
exists(Node mid, boolean clearsOrExpectsMid |
paramReachesLocal(p, mid, clearsOrExpectsMid) and
summaryLocalStep(mid, n, true) and
if
summaryClearsContent(n, _) or
summaryExpectsContent(n, _)
then clearsOrExpects = true
else clearsOrExpects = clearsOrExpectsMid
)
}

/**
* Holds if use-use flow starting from `arg` should be prohibited.
*
Expand All @@ -759,15 +780,11 @@ module Private {
*/
pragma[nomagic]
predicate prohibitsUseUseFlow(ArgNode arg, SummarizedCallable sc) {
exists(ParamNode p, Node mid, ParameterPosition ppos, Node ret |
exists(ParamNode p, ParameterPosition ppos, Node ret |
paramReachesLocal(p, ret, true) and
p = summaryArgParam0(_, arg, sc) and
p.isParameterOf(_, pragma[only_bind_into](ppos)) and
summaryLocalStep(p, mid, true) and
summaryLocalStep(mid, ret, true) and
isParameterPostUpdate(ret, _, pragma[only_bind_into](ppos))
|
summaryClearsContent(mid, _) or
summaryExpectsContent(mid, _)
)
}

Expand Down
29 changes: 23 additions & 6 deletions python/ql/lib/semmle/python/dataflow/new/internal/FlowSummaryImpl.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -750,6 +750,27 @@ module Private {
)
}

/**
* Holds if `p` can reach `n` in a summarized callable, using only value-preserving
* local steps. `clearsOrExpects` records whether any node on the path from `p` to
* `n` either clears or expects contents.
*/
private predicate paramReachesLocal(ParamNode p, Node n, boolean clearsOrExpects) {
viableParam(_, _, _, p) and
n = p and
clearsOrExpects = false
or
exists(Node mid, boolean clearsOrExpectsMid |
paramReachesLocal(p, mid, clearsOrExpectsMid) and
summaryLocalStep(mid, n, true) and
if
summaryClearsContent(n, _) or
summaryExpectsContent(n, _)
then clearsOrExpects = true
else clearsOrExpects = clearsOrExpectsMid
)
}

/**
* Holds if use-use flow starting from `arg` should be prohibited.
*
Expand All @@ -759,15 +780,11 @@ module Private {
*/
pragma[nomagic]
predicate prohibitsUseUseFlow(ArgNode arg, SummarizedCallable sc) {
exists(ParamNode p, Node mid, ParameterPosition ppos, Node ret |
exists(ParamNode p, ParameterPosition ppos, Node ret |
paramReachesLocal(p, ret, true) and
p = summaryArgParam0(_, arg, sc) and
p.isParameterOf(_, pragma[only_bind_into](ppos)) and
summaryLocalStep(p, mid, true) and
summaryLocalStep(mid, ret, true) and
isParameterPostUpdate(ret, _, pragma[only_bind_into](ppos))
|
summaryClearsContent(mid, _) or
summaryExpectsContent(mid, _)
)
}

Expand Down
29 changes: 23 additions & 6 deletions ruby/ql/lib/codeql/ruby/dataflow/internal/FlowSummaryImpl.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -750,6 +750,27 @@ module Private {
)
}

/**
* Holds if `p` can reach `n` in a summarized callable, using only value-preserving
* local steps. `clearsOrExpects` records whether any node on the path from `p` to
* `n` either clears or expects contents.
*/
private predicate paramReachesLocal(ParamNode p, Node n, boolean clearsOrExpects) {
viableParam(_, _, _, p) and
n = p and
clearsOrExpects = false
or
exists(Node mid, boolean clearsOrExpectsMid |
paramReachesLocal(p, mid, clearsOrExpectsMid) and
summaryLocalStep(mid, n, true) and
if
summaryClearsContent(n, _) or
summaryExpectsContent(n, _)
then clearsOrExpects = true
else clearsOrExpects = clearsOrExpectsMid
)
}

/**
* Holds if use-use flow starting from `arg` should be prohibited.
*
Expand All @@ -759,15 +780,11 @@ module Private {
*/
pragma[nomagic]
predicate prohibitsUseUseFlow(ArgNode arg, SummarizedCallable sc) {
exists(ParamNode p, Node mid, ParameterPosition ppos, Node ret |
exists(ParamNode p, ParameterPosition ppos, Node ret |
paramReachesLocal(p, ret, true) and
p = summaryArgParam0(_, arg, sc) and
p.isParameterOf(_, pragma[only_bind_into](ppos)) and
summaryLocalStep(p, mid, true) and
summaryLocalStep(mid, ret, true) and
isParameterPostUpdate(ret, _, pragma[only_bind_into](ppos))
|
summaryClearsContent(mid, _) or
summaryExpectsContent(mid, _)
)
}

Expand Down
2 changes: 1 addition & 1 deletion ruby/ql/lib/codeql/ruby/frameworks/core/Hash.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -267,7 +267,7 @@ module Hash {
s = getExceptComponent(mc, i)
|
".WithoutElement[" + s + "!]" order by i
) and
) + ".WithElement[any]" and
output = "ReturnValue" and
preservesValue = true
}
Expand Down
6 changes: 0 additions & 6 deletions ruby/ql/test/library-tests/dataflow/array-flow/array-flow.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -564,8 +564,6 @@ edges
| array_flow.rb:334:10:334:10 | a [element] : | array_flow.rb:334:10:334:13 | ...[...] |
| array_flow.rb:338:16:338:25 | call to source : | array_flow.rb:339:9:339:9 | a [element 2] : |
| array_flow.rb:338:16:338:25 | call to source : | array_flow.rb:339:9:339:9 | a [element 2] : |
| array_flow.rb:338:16:338:25 | call to source : | array_flow.rb:345:10:345:10 | a [element 2] : |
| array_flow.rb:338:16:338:25 | call to source : | array_flow.rb:345:10:345:10 | a [element 2] : |
| array_flow.rb:339:9:339:9 | [post] a [element] : | array_flow.rb:343:10:343:10 | a [element] : |
| array_flow.rb:339:9:339:9 | [post] a [element] : | array_flow.rb:343:10:343:10 | a [element] : |
| array_flow.rb:339:9:339:9 | [post] a [element] : | array_flow.rb:344:10:344:10 | a [element] : |
Expand All @@ -588,8 +586,6 @@ edges
| array_flow.rb:343:10:343:10 | a [element] : | array_flow.rb:343:10:343:13 | ...[...] |
| array_flow.rb:344:10:344:10 | a [element] : | array_flow.rb:344:10:344:13 | ...[...] |
| array_flow.rb:344:10:344:10 | a [element] : | array_flow.rb:344:10:344:13 | ...[...] |
| array_flow.rb:345:10:345:10 | a [element 2] : | array_flow.rb:345:10:345:13 | ...[...] |
| array_flow.rb:345:10:345:10 | a [element 2] : | array_flow.rb:345:10:345:13 | ...[...] |
| array_flow.rb:345:10:345:10 | a [element] : | array_flow.rb:345:10:345:13 | ...[...] |
| array_flow.rb:345:10:345:10 | a [element] : | array_flow.rb:345:10:345:13 | ...[...] |
| array_flow.rb:349:16:349:25 | call to source : | array_flow.rb:350:9:350:9 | a [element 2] : |
Expand Down Expand Up @@ -4098,8 +4094,6 @@ nodes
| array_flow.rb:344:10:344:10 | a [element] : | semmle.label | a [element] : |
| array_flow.rb:344:10:344:13 | ...[...] | semmle.label | ...[...] |
| array_flow.rb:344:10:344:13 | ...[...] | semmle.label | ...[...] |
| array_flow.rb:345:10:345:10 | a [element 2] : | semmle.label | a [element 2] : |
| array_flow.rb:345:10:345:10 | a [element 2] : | semmle.label | a [element 2] : |
| array_flow.rb:345:10:345:10 | a [element] : | semmle.label | a [element] : |
| array_flow.rb:345:10:345:10 | a [element] : | semmle.label | a [element] : |
| array_flow.rb:345:10:345:13 | ...[...] | semmle.label | ...[...] |
Expand Down
2 changes: 0 additions & 2 deletions ruby/ql/test/library-tests/dataflow/hash-flow/hash-flow.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -102,7 +102,6 @@ edges
| hash_flow.rb:185:9:185:12 | hash [element :a] : | hash_flow.rb:185:9:185:23 | call to delete : |
| hash_flow.rb:185:9:185:23 | call to delete : | hash_flow.rb:186:10:186:10 | a |
| hash_flow.rb:194:15:194:25 | call to taint : | hash_flow.rb:197:9:197:12 | hash [element :a] : |
| hash_flow.rb:194:15:194:25 | call to taint : | hash_flow.rb:202:10:202:13 | hash [element :a] : |
| hash_flow.rb:197:9:197:12 | [post] hash [element :a] : | hash_flow.rb:202:10:202:13 | hash [element :a] : |
| hash_flow.rb:197:9:197:12 | hash [element :a] : | hash_flow.rb:197:9:197:12 | [post] hash [element :a] : |
| hash_flow.rb:197:9:197:12 | hash [element :a] : | hash_flow.rb:197:9:200:7 | call to delete_if [element :a] : |
Expand Down Expand Up @@ -307,7 +306,6 @@ edges
| hash_flow.rb:477:29:477:33 | value : | hash_flow.rb:479:14:479:18 | value |
| hash_flow.rb:482:10:482:10 | b [element :a] : | hash_flow.rb:482:10:482:14 | ...[...] |
| hash_flow.rb:489:15:489:25 | call to taint : | hash_flow.rb:492:9:492:12 | hash [element :a] : |
| hash_flow.rb:489:15:489:25 | call to taint : | hash_flow.rb:498:10:498:13 | hash [element :a] : |
| hash_flow.rb:492:9:492:12 | [post] hash [element :a] : | hash_flow.rb:498:10:498:13 | hash [element :a] : |
| hash_flow.rb:492:9:492:12 | hash [element :a] : | hash_flow.rb:492:9:492:12 | [post] hash [element :a] : |
| hash_flow.rb:492:9:492:12 | hash [element :a] : | hash_flow.rb:492:9:496:7 | call to reject! [element :a] : |
Expand Down
Loading