Dataflow: Force high precision of certain Contents.

This commit is contained in:
Anders Schack-Mulligen
2021-10-01 13:03:50 +02:00
parent 45cf6344cd
commit d4f1a9602f
3 changed files with 24 additions and 7 deletions

View File

@@ -2139,7 +2139,8 @@ private predicate expensiveLen2unfolding(TypedContent tc, Configuration config)
) and
accessPathApproxCostLimits(apLimit, tupleLimit) and
apLimit < tails and
tupleLimit < (tails - 1) * nodes
tupleLimit < (tails - 1) * nodes and
not tc.forceHighPrecision()
)
}
@@ -2973,12 +2974,15 @@ private AccessPathApprox getATail(AccessPathApprox apa, Configuration config) {
* expected to be expensive. Holds with `unfold = true` otherwise.
*/
private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration config) {
exists(int aps, int nodes, int apLimit, int tupleLimit |
aps = countPotentialAps(apa, config) and
nodes = countNodesUsingAccessPath(apa, config) and
accessPathCostLimits(apLimit, tupleLimit) and
if apLimit < aps and tupleLimit < (aps - 1) * nodes then unfold = false else unfold = true
)
if apa.getHead().forceHighPrecision()
then unfold = true
else
exists(int aps, int nodes, int apLimit, int tupleLimit |
aps = countPotentialAps(apa, config) and
nodes = countNodesUsingAccessPath(apa, config) and
accessPathCostLimits(apLimit, tupleLimit) and
if apLimit < aps and tupleLimit < (aps - 1) * nodes then unfold = false else unfold = true
)
}
/**

View File

@@ -1236,6 +1236,13 @@ class TypedContent extends MkTypedContent {
/** Gets a textual representation of this content. */
string toString() { result = c.toString() }
/**
* Holds if accesspaths with this `TypedContent` at their head always should
* be tracked at high precision. This disables adaptive accesspath precision
* for such accesspaths.
*/
predicate forceHighPrecision() { forceHighPrecision(c) }
}
/**

View File

@@ -308,6 +308,12 @@ predicate isUnreachableInCall(Node n, DataFlowCall call) {
int accessPathLimit() { result = 5 }
/**
* Holds if accesspaths with `c` at their head always should be tracked at high
* precision. This disables adaptive accesspath precision for such accesspaths.
*/
predicate forceHighPrecision(Content c) { c instanceof ArrayContent or c instanceof CollectionContent }
/**
* Holds if `n` does not require a `PostUpdateNode` as it either cannot be
* modified or its modification cannot be observed, for example if it is a