Merge pull request #4227 from jbj/SimpleRangeAnalysis-NotExpr

C++: Support `(bool)x` and `!x` in SimpleRangeAnalysis
This commit is contained in:
Mathias Vorreiter Pedersen
2020-09-11 08:59:03 +02:00
committed by GitHub
9 changed files with 235 additions and 35 deletions

View File

@@ -171,6 +171,65 @@ predicate eqOpWithSwapAndNegate(EqualityOperation cmp, Expr a, Expr b, boolean i
eqOpWithSwap(cmp, a, b, branch.booleanNot()) and isEQ = false
}
/**
* Holds if `cmp` is an unconverted conversion of `a` to a Boolean that
* evalutes to `isEQ` iff `a` is 0.
*
* Note that `a` can be `cmp` itself or a conversion thereof.
*/
private predicate eqZero(Expr cmp, Expr a, boolean isEQ) {
// The `!a` expression tests `a` equal to zero when `a` is a number converted
// to a Boolean.
isEQ = true and
exists(Expr notOperand | notOperand = cmp.(NotExpr).getOperand().getFullyConverted() |
// In C++ code there will be a BoolConversion in `!myInt`
a = notOperand.(BoolConversion).getExpr()
or
// In C code there is no conversion since there was no bool type before C99
a = notOperand and
not a instanceof BoolConversion // avoid overlap with the case above
)
or
// The `(bool)a` expression tests `a` NOT equal to zero when `a` is a number
// converted to a Boolean. To avoid overlap with the case above, this case
// excludes conversions that are right below a `!`.
isEQ = false and
linearAccess(cmp, _, _, _) and
// This test for `isCondition` implies that `cmp` is unconverted and that the
// parent of `cfg` is not a `NotExpr` -- the CFG doesn't do branching from
// inside `NotExpr`.
cmp.isCondition() and
// The GNU two-operand conditional expression is not supported for the
// purpose of guards, but the value of the conditional expression itself is
// modeled in the range analysis.
not exists(ConditionalExpr cond | cmp = cond.getCondition() and cond.isTwoOperand()) and
(
// In C++ code there will be a BoolConversion in `if (myInt)`
a = cmp.getFullyConverted().(BoolConversion).getExpr()
or
// In C code there is no conversion since there was no bool type before C99
a = cmp.getFullyConverted() and
not a instanceof BoolConversion // avoid overlap with the case above
)
}
/**
* Holds if `branch` of `cmp` is taken when `a` compares `isEQ` to zero.
*
* Note that `a` can be `cmp` itself or a conversion thereof.
*/
predicate eqZeroWithNegate(Expr cmp, Expr a, boolean isEQ, boolean branch) {
// The comparison for _equality_ to zero is on the `true` branch when `cmp`
// compares equal to zero and on the `false` branch when `cmp` compares not
// equal to zero.
eqZero(cmp, a, branch) and isEQ = true
or
// The comparison for _inequality_ to zero is on the `false` branch when
// `cmp` compares equal to zero and on the `true` branch when `cmp` compares
// not equal to zero.
eqZero(cmp, a, branch.booleanNot()) and isEQ = false
}
/**
* Holds if `expr` is equivalent to `p*v + q`, where `p` is a non-zero
* number. This takes into account the associativity, commutativity and

View File

@@ -40,21 +40,20 @@ library class RangeSSA extends SSAHelper {
}
}
private predicate guard_defn(
VariableAccess v, ComparisonOperation guard, BasicBlock b, boolean branch
) {
private predicate guard_defn(VariableAccess v, Expr guard, BasicBlock b, boolean branch) {
guardCondition(guard, v, branch) and
guardSuccessor(guard, branch, b)
}
private predicate guardCondition(ComparisonOperation guard, VariableAccess v, boolean branch) {
private predicate guardCondition(Expr guard, VariableAccess v, boolean branch) {
exists(Expr lhs | linearAccess(lhs, v, _, _) |
relOpWithSwapAndNegate(guard, lhs, _, _, _, branch) or
eqOpWithSwapAndNegate(guard, lhs, _, _, branch)
eqOpWithSwapAndNegate(guard, lhs, _, _, branch) or
eqZeroWithNegate(guard, lhs, _, branch)
)
}
private predicate guardSuccessor(ComparisonOperation guard, boolean branch, BasicBlock succ) {
private predicate guardSuccessor(Expr guard, boolean branch, BasicBlock succ) {
branch = true and succ = guard.getATrueSuccessor()
or
branch = false and succ = guard.getAFalseSuccessor()
@@ -98,7 +97,7 @@ class RangeSsaDefinition extends ControlFlowNodeBase {
* If this definition is a phi node corresponding to a guard,
* then return the variable and the guard.
*/
predicate isGuardPhi(VariableAccess v, ComparisonOperation guard, boolean branch) {
predicate isGuardPhi(VariableAccess v, Expr guard, boolean branch) {
guard_defn(v, guard, this, branch)
}

View File

@@ -427,11 +427,11 @@ private predicate exprDependsOnDef(Expr e, RangeSsaDefinition srcDef, StackVaria
private predicate phiDependsOnDef(
RangeSsaDefinition phi, StackVariable v, RangeSsaDefinition srcDef, StackVariable srcVar
) {
exists(VariableAccess access, ComparisonOperation guard |
exists(VariableAccess access, Expr guard |
access = v.getAnAccess() and
phi.isGuardPhi(access, guard, _)
|
exprDependsOnDef(guard.getAnOperand(), srcDef, srcVar) or
exprDependsOnDef(guard.(ComparisonOperation).getAnOperand(), srcDef, srcVar) or
exprDependsOnDef(access, srcDef, srcVar)
)
or
@@ -1132,9 +1132,7 @@ private float boolConversionUpperBound(Expr expr) {
* use the guard to deduce that the lower bound is 2 inside the block.
*/
private float getPhiLowerBounds(StackVariable v, RangeSsaDefinition phi) {
exists(
VariableAccess access, ComparisonOperation guard, boolean branch, float defLB, float guardLB
|
exists(VariableAccess access, Expr guard, boolean branch, float defLB, float guardLB |
access = v.getAnAccess() and
phi.isGuardPhi(access, guard, branch) and
lowerBoundFromGuard(guard, access, guardLB, branch) and
@@ -1146,13 +1144,13 @@ private float getPhiLowerBounds(StackVariable v, RangeSsaDefinition phi) {
or
exists(VariableAccess access, float neConstant, float lower |
isNEPhi(v, phi, access, neConstant) and
lower = getFullyConvertedLowerBounds(access) and
lower = getTruncatedLowerBounds(access) and
if lower = neConstant then result = lower + 1 else result = lower
)
or
exists(VariableAccess access |
isUnsupportedGuardPhi(v, phi, access) and
result = getFullyConvertedLowerBounds(access)
result = getTruncatedLowerBounds(access)
)
or
result = getDefLowerBounds(phi.getAPhiInput(v), v)
@@ -1160,9 +1158,7 @@ private float getPhiLowerBounds(StackVariable v, RangeSsaDefinition phi) {
/** See comment for `getPhiLowerBounds`, above. */
private float getPhiUpperBounds(StackVariable v, RangeSsaDefinition phi) {
exists(
VariableAccess access, ComparisonOperation guard, boolean branch, float defUB, float guardUB
|
exists(VariableAccess access, Expr guard, boolean branch, float defUB, float guardUB |
access = v.getAnAccess() and
phi.isGuardPhi(access, guard, branch) and
upperBoundFromGuard(guard, access, guardUB, branch) and
@@ -1174,13 +1170,13 @@ private float getPhiUpperBounds(StackVariable v, RangeSsaDefinition phi) {
or
exists(VariableAccess access, float neConstant, float upper |
isNEPhi(v, phi, access, neConstant) and
upper = getFullyConvertedUpperBounds(access) and
upper = getTruncatedUpperBounds(access) and
if upper = neConstant then result = upper - 1 else result = upper
)
or
exists(VariableAccess access |
isUnsupportedGuardPhi(v, phi, access) and
result = getFullyConvertedUpperBounds(access)
result = getTruncatedUpperBounds(access)
)
or
result = getDefUpperBounds(phi.getAPhiInput(v), v)
@@ -1334,7 +1330,7 @@ private predicate unanalyzableDefBounds(RangeSsaDefinition def, StackVariable v,
* inferences about `v`.
*/
bindingset[guard, v, branch]
predicate nonNanGuardedVariable(ComparisonOperation guard, VariableAccess v, boolean branch) {
predicate nonNanGuardedVariable(Expr guard, VariableAccess v, boolean branch) {
getVariableRangeType(v.getTarget()) instanceof IntegralType
or
getVariableRangeType(v.getTarget()) instanceof FloatingPointType and
@@ -1353,9 +1349,7 @@ predicate nonNanGuardedVariable(ComparisonOperation guard, VariableAccess v, boo
* predicate uses the bounds information for `r` to compute a lower bound
* for `v`.
*/
private predicate lowerBoundFromGuard(
ComparisonOperation guard, VariableAccess v, float lb, boolean branch
) {
private predicate lowerBoundFromGuard(Expr guard, VariableAccess v, float lb, boolean branch) {
exists(float childLB, RelationStrictness strictness |
boundFromGuard(guard, v, childLB, true, strictness, branch)
|
@@ -1375,9 +1369,7 @@ private predicate lowerBoundFromGuard(
* predicate uses the bounds information for `r` to compute a upper bound
* for `v`.
*/
private predicate upperBoundFromGuard(
ComparisonOperation guard, VariableAccess v, float ub, boolean branch
) {
private predicate upperBoundFromGuard(Expr guard, VariableAccess v, float ub, boolean branch) {
exists(float childUB, RelationStrictness strictness |
boundFromGuard(guard, v, childUB, false, strictness, branch)
|
@@ -1397,7 +1389,7 @@ private predicate upperBoundFromGuard(
* `linearBoundFromGuard`.
*/
private predicate boundFromGuard(
ComparisonOperation guard, VariableAccess v, float boundValue, boolean isLowerBound,
Expr guard, VariableAccess v, float boundValue, boolean isLowerBound,
RelationStrictness strictness, boolean branch
) {
exists(float p, float q, float r, boolean isLB |
@@ -1410,6 +1402,15 @@ private predicate boundFromGuard(
or
p < 0 and isLowerBound = isLB.booleanNot()
)
or
// When `!e` is true, we know that `0 <= e <= 0`
exists(float p, float q, Expr e |
linearAccess(e, v, p, q) and
eqZeroWithNegate(guard, e, true, branch) and
boundValue = (0.0 - q) / p and
isLowerBound = [false, true] and
strictness = Nonstrict()
)
}
/**
@@ -1487,6 +1488,15 @@ private predicate isNEPhi(
linearAccess(linearExpr, access, p, q) and
neConstant = (r - q) / p
)
or
exists(Expr op, boolean branch, Expr linearExpr, float p, float q |
access.getTarget() = v and
phi.isGuardPhi(access, op, branch) and
eqZeroWithNegate(op, linearExpr, false, branch) and
v.getUnspecifiedType() instanceof IntegralOrEnumType and // Float `!` is too imprecise
linearAccess(linearExpr, access, p, q) and
neConstant = (0.0 - q) / p
)
}
/**
@@ -1496,10 +1506,13 @@ private predicate isNEPhi(
* compile-time constant.
*/
private predicate isUnsupportedGuardPhi(Variable v, RangeSsaDefinition phi, VariableAccess access) {
exists(ComparisonOperation cmp, boolean branch |
exists(Expr cmp, boolean branch |
eqOpWithSwapAndNegate(cmp, _, _, false, branch)
or
eqZeroWithNegate(cmp, _, false, branch)
|
access.getTarget() = v and
phi.isGuardPhi(access, cmp, branch) and
eqOpWithSwapAndNegate(cmp, _, _, false, branch) and
not isNEPhi(v, phi, access, _)
)
}

View File

@@ -540,7 +540,7 @@
| test.c:548:9:548:9 | n | 0 |
| test.c:551:8:551:8 | n | 0 |
| test.c:552:9:552:9 | n | 0 |
| test.c:554:9:554:9 | n | 0 |
| test.c:554:9:554:9 | n | 1 |
| test.c:557:10:557:10 | n | 0 |
| test.c:558:5:558:5 | n | 1 |
| test.c:561:7:561:7 | n | 0 |
@@ -549,7 +549,7 @@
| test.c:569:9:569:9 | n | 0 |
| test.c:571:9:571:9 | n | 1 |
| test.c:574:7:574:7 | n | 0 |
| test.c:575:9:575:9 | n | 0 |
| test.c:575:9:575:9 | n | 1 |
| test.c:577:9:577:9 | n | 0 |
| test.c:580:10:580:10 | n | 0 |
| test.c:581:5:581:5 | n | 1 |
@@ -563,6 +563,25 @@
| test.c:601:7:601:7 | n | -32768 |
| test.c:601:22:601:22 | n | -32767 |
| test.c:602:9:602:9 | n | -32766 |
| test.c:605:7:605:7 | n | -32768 |
| test.c:606:5:606:5 | n | 0 |
| test.c:606:10:606:10 | n | 1 |
| test.c:606:14:606:14 | n | 0 |
| test.c:607:6:607:6 | n | 0 |
| test.c:607:10:607:10 | n | 0 |
| test.c:607:14:607:14 | n | 1 |
| test.c:618:7:618:8 | ss | -32768 |
| test.c:619:9:619:10 | ss | 0 |
| test.c:622:7:622:8 | ss | -32768 |
| test.c:623:9:623:10 | ss | -32768 |
| test.c:626:14:626:15 | us | 0 |
| test.c:627:9:627:10 | us | 0 |
| test.c:630:14:630:15 | us | 0 |
| test.c:631:9:631:10 | us | 0 |
| test.c:634:7:634:8 | ss | -32768 |
| test.c:635:9:635:10 | ss | -32768 |
| test.c:638:7:638:8 | ss | -32768 |
| test.c:639:9:639:10 | ss | -1 |
| test.cpp:10:7:10:7 | b | -2147483648 |
| test.cpp:11:5:11:5 | x | -2147483648 |
| test.cpp:13:10:13:10 | x | -2147483648 |
@@ -616,3 +635,16 @@
| test.cpp:97:10:97:10 | i | -2147483648 |
| test.cpp:97:22:97:22 | i | -2147483648 |
| test.cpp:98:5:98:5 | i | -2147483648 |
| test.cpp:105:7:105:7 | n | -32768 |
| test.cpp:108:7:108:7 | n | 0 |
| test.cpp:109:5:109:5 | n | 1 |
| test.cpp:111:5:111:5 | n | 0 |
| test.cpp:114:8:114:8 | n | 0 |
| test.cpp:115:5:115:5 | n | 0 |
| test.cpp:117:5:117:5 | n | 1 |
| test.cpp:120:3:120:3 | n | 0 |
| test.cpp:120:8:120:8 | n | 1 |
| test.cpp:120:12:120:12 | n | 0 |
| test.cpp:121:4:121:4 | n | 0 |
| test.cpp:121:8:121:8 | n | 0 |
| test.cpp:121:12:121:12 | n | 1 |

View File

@@ -13,3 +13,7 @@
| test.c:386:10:386:21 | ... ? ... : ... | 100.0 | 100.0 | 5.0 |
| test.c:387:10:387:38 | ... ? ... : ... | 0.0 | 100.0 | 5.0 |
| test.c:394:20:394:36 | ... ? ... : ... | 0.0 | 0.0 | 100.0 |
| test.c:606:5:606:14 | ... ? ... : ... | 0.0 | 1.0 | 0.0 |
| test.c:607:5:607:14 | ... ? ... : ... | 0.0 | 0.0 | 1.0 |
| test.cpp:120:3:120:12 | ... ? ... : ... | 0.0 | 1.0 | 0.0 |
| test.cpp:121:3:121:12 | ... ? ... : ... | 0.0 | 0.0 | 1.0 |

View File

@@ -13,3 +13,7 @@
| test.c:386:10:386:21 | ... ? ... : ... | 4.294967295E9 | 4.294967295E9 | 5.0 |
| test.c:387:10:387:38 | ... ? ... : ... | 255.0 | 4.294967295E9 | 5.0 |
| test.c:394:20:394:36 | ... ? ... : ... | 100.0 | 99.0 | 100.0 |
| test.c:606:5:606:14 | ... ? ... : ... | 32767.0 | 32767.0 | 0.0 |
| test.c:607:5:607:14 | ... ? ... : ... | 32767.0 | 0.0 | 32767.0 |
| test.cpp:120:3:120:12 | ... ? ... : ... | 32767.0 | 32767.0 | 0.0 |
| test.cpp:121:3:121:12 | ... ? ... : ... | 32767.0 | 0.0 | 32767.0 |

View File

@@ -551,7 +551,7 @@ int notequal_type_endpoint(unsigned n) {
if (!n) {
out(n); // 0 .. 0
} else {
out(n); // 1 .. [BUG: lower bound is deduced to be 0]
out(n); // 1 ..
}
while (n != 0) {
@@ -572,7 +572,7 @@ void notequal_refinement(short n) {
}
if (n) {
out(n); // 1 .. [BUG: lower bound is deduced to be 0]
out(n); // 1 ..
} else {
out(n); // 0 .. 0
}
@@ -601,4 +601,41 @@ void notequal_variations(short n, float f) {
if (n != -32768 && n != -32767) {
out(n); // -32766 ..
}
if (n >= 0) {
n ? n : n; // ? 1.. : 0..0
!n ? n : n; // ? 0..0 : 1..
}
}
void two_bounds_from_one_test(short ss, unsigned short us) {
// These tests demonstrate how the range analysis is often able to deduce
// both an upper bound and a lower bound even when there is only one
// inequality in the source. For example `signedInt < 4U` establishes that
// `signedInt >= 0` since if `signedInt` were negative then it would be
// greater than 4 in the unsigned comparison.
if (ss < sizeof(int)) { // Lower bound added in `linearBoundFromGuard`
out(ss); // 0 .. 3
}
if (ss < 0x8001) { // Lower bound removed in `getDefLowerBounds`
out(ss); // -32768 .. 32767
}
if ((short)us >= 0) {
out(us); // 0 .. 32767
}
if ((short)us >= -1) {
out(us); // 0 .. 65535
}
if (ss >= sizeof(int)) { // test is true for negative numbers
out(ss); // -32768 .. 32767
}
if (ss + 1 < sizeof(int)) {
out(ss); // -1 .. 2
}
}

View File

@@ -100,3 +100,23 @@ int ref_to_number(int &i, const int &ci, int &aliased) {
return 0;
}
void notequal_refinement(short n) {
if (n < 0)
return;
if (n) {
n; // 1 ..
} else {
n; // 0 .. 0
}
if (!n) {
n; // 0 .. 0
} else {
n; // 1 ..
}
n ? n : n; // ? 1.. : 0..0
!n ? n : n; // ? 0..0 : 1..
}

View File

@@ -539,7 +539,7 @@
| test.c:546:9:546:9 | n | 4294967295 |
| test.c:548:9:548:9 | n | 0 |
| test.c:551:8:551:8 | n | 4294967295 |
| test.c:552:9:552:9 | n | 4294967295 |
| test.c:552:9:552:9 | n | 0 |
| test.c:554:9:554:9 | n | 4294967295 |
| test.c:557:10:557:10 | n | 4294967295 |
| test.c:558:5:558:5 | n | 4294967295 |
@@ -550,7 +550,7 @@
| test.c:571:9:571:9 | n | 32767 |
| test.c:574:7:574:7 | n | 32767 |
| test.c:575:9:575:9 | n | 32767 |
| test.c:577:9:577:9 | n | 32767 |
| test.c:577:9:577:9 | n | 0 |
| test.c:580:10:580:10 | n | 32767 |
| test.c:581:5:581:5 | n | 32767 |
| test.c:584:7:584:7 | n | 0 |
@@ -563,6 +563,25 @@
| test.c:601:7:601:7 | n | 32767 |
| test.c:601:22:601:22 | n | 32767 |
| test.c:602:9:602:9 | n | 32767 |
| test.c:605:7:605:7 | n | 32767 |
| test.c:606:5:606:5 | n | 32767 |
| test.c:606:10:606:10 | n | 32767 |
| test.c:606:14:606:14 | n | 0 |
| test.c:607:6:607:6 | n | 32767 |
| test.c:607:10:607:10 | n | 0 |
| test.c:607:14:607:14 | n | 32767 |
| test.c:618:7:618:8 | ss | 32767 |
| test.c:619:9:619:10 | ss | 3 |
| test.c:622:7:622:8 | ss | 32767 |
| test.c:623:9:623:10 | ss | 32767 |
| test.c:626:14:626:15 | us | 65535 |
| test.c:627:9:627:10 | us | 32767 |
| test.c:630:14:630:15 | us | 65535 |
| test.c:631:9:631:10 | us | 65535 |
| test.c:634:7:634:8 | ss | 32767 |
| test.c:635:9:635:10 | ss | 32767 |
| test.c:638:7:638:8 | ss | 32767 |
| test.c:639:9:639:10 | ss | 2 |
| test.cpp:10:7:10:7 | b | 2147483647 |
| test.cpp:11:5:11:5 | x | 2147483647 |
| test.cpp:13:10:13:10 | x | 2147483647 |
@@ -616,3 +635,16 @@
| test.cpp:97:10:97:10 | i | 65535 |
| test.cpp:97:22:97:22 | i | 32767 |
| test.cpp:98:5:98:5 | i | 32767 |
| test.cpp:105:7:105:7 | n | 32767 |
| test.cpp:108:7:108:7 | n | 32767 |
| test.cpp:109:5:109:5 | n | 32767 |
| test.cpp:111:5:111:5 | n | 0 |
| test.cpp:114:8:114:8 | n | 32767 |
| test.cpp:115:5:115:5 | n | 0 |
| test.cpp:117:5:117:5 | n | 32767 |
| test.cpp:120:3:120:3 | n | 32767 |
| test.cpp:120:8:120:8 | n | 32767 |
| test.cpp:120:12:120:12 | n | 0 |
| test.cpp:121:4:121:4 | n | 32767 |
| test.cpp:121:8:121:8 | n | 0 |
| test.cpp:121:12:121:12 | n | 32767 |