Skip to content

Commit d4f1a96

Browse files
committed
Dataflow: Force high precision of certain Contents.
1 parent 45cf634 commit d4f1a96

File tree

3 files changed

+24
-7
lines changed

3 files changed

+24
-7
lines changed

java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl.qll

Lines changed: 11 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -2139,7 +2139,8 @@ private predicate expensiveLen2unfolding(TypedContent tc, Configuration config)
21392139
) and
21402140
accessPathApproxCostLimits(apLimit, tupleLimit) and
21412141
apLimit < tails and
2142-
tupleLimit < (tails - 1) * nodes
2142+
tupleLimit < (tails - 1) * nodes and
2143+
not tc.forceHighPrecision()
21432144
)
21442145
}
21452146

@@ -2973,12 +2974,15 @@ private AccessPathApprox getATail(AccessPathApprox apa, Configuration config) {
29732974
* expected to be expensive. Holds with `unfold = true` otherwise.
29742975
*/
29752976
private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration config) {
2976-
exists(int aps, int nodes, int apLimit, int tupleLimit |
2977-
aps = countPotentialAps(apa, config) and
2978-
nodes = countNodesUsingAccessPath(apa, config) and
2979-
accessPathCostLimits(apLimit, tupleLimit) and
2980-
if apLimit < aps and tupleLimit < (aps - 1) * nodes then unfold = false else unfold = true
2981-
)
2977+
if apa.getHead().forceHighPrecision()
2978+
then unfold = true
2979+
else
2980+
exists(int aps, int nodes, int apLimit, int tupleLimit |
2981+
aps = countPotentialAps(apa, config) and
2982+
nodes = countNodesUsingAccessPath(apa, config) and
2983+
accessPathCostLimits(apLimit, tupleLimit) and
2984+
if apLimit < aps and tupleLimit < (aps - 1) * nodes then unfold = false else unfold = true
2985+
)
29822986
}
29832987

29842988
/**

java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImplCommon.qll

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1236,6 +1236,13 @@ class TypedContent extends MkTypedContent {
12361236

12371237
/** Gets a textual representation of this content. */
12381238
string toString() { result = c.toString() }
1239+
1240+
/**
1241+
* Holds if accesspaths with this `TypedContent` at their head always should
1242+
* be tracked at high precision. This disables adaptive accesspath precision
1243+
* for such accesspaths.
1244+
*/
1245+
predicate forceHighPrecision() { forceHighPrecision(c) }
12391246
}
12401247

12411248
/**

java/ql/lib/semmle/code/java/dataflow/internal/DataFlowPrivate.qll

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -308,6 +308,12 @@ predicate isUnreachableInCall(Node n, DataFlowCall call) {
308308

309309
int accessPathLimit() { result = 5 }
310310

311+
/**
312+
* Holds if accesspaths with `c` at their head always should be tracked at high
313+
* precision. This disables adaptive accesspath precision for such accesspaths.
314+
*/
315+
predicate forceHighPrecision(Content c) { c instanceof ArrayContent or c instanceof CollectionContent }
316+
311317
/**
312318
* Holds if `n` does not require a `PostUpdateNode` as it either cannot be
313319
* modified or its modification cannot be observed, for example if it is a

0 commit comments

Comments
 (0)