Merge pull request #6790 from aschackmull/dataflow/force-precision

Dataflow: Force high precision of certain Contents.
This commit is contained in:
Anders Schack-Mulligen 2021-10-08 11:44:26 +02:00 коммит произвёл GitHub
Родитель 951df380a9 1bec58dee5
Коммит 446c738f20
Не найден ключ, соответствующий данной подписи
Идентификатор ключа GPG: 4AEE18F83AFDEB23
35 изменённых файлов: 342 добавлений и 175 удалений

Просмотреть файл

@ -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
)
}
/**

Просмотреть файл

@ -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
)
}
/**

Просмотреть файл

@ -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
)
}
/**

Просмотреть файл

@ -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
)
}
/**

Просмотреть файл

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

Просмотреть файл

@ -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
)
}
/**

Просмотреть файл

@ -240,6 +240,12 @@ predicate isUnreachableInCall(Node n, DataFlowCall call) { none() } // stub impl
int accessPathLimit() { result = 5 }
/**
* Holds if access paths with `c` at their head always should be tracked at high
* precision. This disables adaptive access path precision for such access paths.
*/
predicate forceHighPrecision(Content c) { none() }
/** The unit type. */
private newtype TUnit = TMkUnit()

Просмотреть файл

@ -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
)
}
/**

Просмотреть файл

@ -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
)
}
/**

Просмотреть файл

@ -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
)
}
/**

Просмотреть файл

@ -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
)
}
/**

Просмотреть файл

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

Просмотреть файл

@ -466,6 +466,12 @@ predicate isUnreachableInCall(Node n, DataFlowCall call) { none() } // stub impl
int accessPathLimit() { result = 5 }
/**
* Holds if access paths with `c` at their head always should be tracked at high
* precision. This disables adaptive access path precision for such access paths.
*/
predicate forceHighPrecision(Content c) { none() }
/** The unit type. */
private newtype TUnit = TMkUnit()

Просмотреть файл

@ -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
)
}
/**

Просмотреть файл

@ -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
)
}
/**

Просмотреть файл

@ -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
)
}
/**

Просмотреть файл

@ -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
)
}
/**

Просмотреть файл

@ -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
)
}
/**

Просмотреть файл

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

Просмотреть файл

@ -1918,6 +1918,12 @@ private predicate viableConstantBooleanParamArg(
int accessPathLimit() { result = 5 }
/**
* Holds if access paths with `c` at their head always should be tracked at high
* precision. This disables adaptive access path precision for such access paths.
*/
predicate forceHighPrecision(Content c) { c instanceof ElementContent }
/** The unit type. */
private newtype TUnit = TMkUnit()

Просмотреть файл

@ -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
)
}
/**

Просмотреть файл

@ -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
)
}
/**

Просмотреть файл

@ -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
)
}
/**

Просмотреть файл

@ -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
)
}
/**

Просмотреть файл

@ -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
)
}
/**

Просмотреть файл

@ -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
)
}
/**

Просмотреть файл

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

Просмотреть файл

@ -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
)
}
/**

Просмотреть файл

@ -308,6 +308,14 @@ predicate isUnreachableInCall(Node n, DataFlowCall call) {
int accessPathLimit() { result = 5 }
/**
* Holds if access paths with `c` at their head always should be tracked at high
* precision. This disables adaptive access path precision for such access paths.
*/
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

Просмотреть файл

@ -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
)
}
/**

Просмотреть файл

@ -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
)
}
/**

Просмотреть файл

@ -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
)
}
/**

Просмотреть файл

@ -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
)
}
/**

Просмотреть файл

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

Просмотреть файл

@ -1620,6 +1620,12 @@ predicate isImmutableOrUnobservable(Node n) { none() }
int accessPathLimit() { result = 5 }
/**
* Holds if access paths with `c` at their head always should be tracked at high
* precision. This disables adaptive access path precision for such access paths.
*/
predicate forceHighPrecision(Content c) { none() }
/** Holds if `n` should be hidden from path explanations. */
predicate nodeIsHidden(Node n) { none() }