Skip to content

Commit e67b6d6

Browse files
MathiasVPMathiasVP
committed
C++: Add another inference step.
1 parent a271354 commit e67b6d6

File tree

5 files changed

+50
-17
lines changed

5 files changed

+50
-17
lines changed

‎cpp/ql/lib/semmle/code/cpp/controlflow/IRGuards.qll‎

Lines changed: 28 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -966,6 +966,18 @@ private module Cached {
966966
)
967967
or
968968
compares_eq(test.(BuiltinExpectCallValueNumber).getCondition(), left, right, k, areEqual, value)
969+
or
970+
exists(Operand l, BooleanValue bv |
971+
// 1. test = value -> int(l) = 0 is !bv
972+
unary_compares_eq(test, l, 0, bv.getValue().booleanNot(), value) and
973+
// 2. l = bv -> left + right is areEqual
974+
compares_eq(valueNumberOfOperand(l), left, right, k, areEqual, bv)
975+
// We want this to hold:
976+
// `test = value -> left + right is areEqual`
977+
// Applying 2 we need to show:
978+
// `test = value -> l = bv`
979+
// And `l = bv` holds by `int(l) = 0 is !bv`
980+
)
969981
}
970982

971983
private predicate isConvertedBool(Instruction instr) {
@@ -1006,19 +1018,10 @@ private module Cached {
10061018
k = k1 + k2
10071019
)
10081020
or
1009-
exists(CompareValueNumber cmp, Operand left, Operand right, AbstractValue v |
1010-
test = cmp and
1011-
pragma[only_bind_into](cmp)
1012-
.hasOperands(pragma[only_bind_into](left), pragma[only_bind_into](right)) and
1013-
isConvertedBool(left.getDef()) and
1014-
int_value(right.getDef()) = 0 and
1015-
unary_compares_eq(valueNumberOfOperand(left), op, k, areEqual, v)
1016-
|
1017-
cmp instanceof CompareNEValueNumber and
1018-
v = value
1019-
or
1020-
cmp instanceof CompareEQValueNumber and
1021-
v.getDualValue() = value
1021+
// See argument for why this is correct in compares_eq
1022+
exists(Operand l, BooleanValue bv |
1023+
unary_compares_eq(test, l, 0, bv.getValue().booleanNot(), value) and
1024+
unary_compares_eq(valueNumberOfOperand(l), op, k, areEqual, bv)
10221025
)
10231026
or
10241027
unary_compares_eq(test.(BuiltinExpectCallValueNumber).getCondition(), op, k, areEqual, value)
@@ -1215,6 +1218,12 @@ private module Cached {
12151218
exists(AbstractValue dual | value = dual.getDualValue() |
12161219
compares_lt(test.(LogicalNotValueNumber).getUnary(), left, right, k, isLt, dual)
12171220
)
1221+
or
1222+
// See argument for why this is correct in compares_eq
1223+
exists(Operand l, BooleanValue bv |
1224+
unary_compares_eq(test, l, 0, bv.getValue().booleanNot(), value) and
1225+
compares_lt(valueNumberOfOperand(l), left, right, k, isLt, bv)
1226+
)
12181227
}
12191228

12201229
/** Holds if `op < k` evaluates to `isLt` given that `test` evaluates to `value`. */
@@ -1234,6 +1243,12 @@ private module Cached {
12341243
int_value(const) = k1 and
12351244
k = k1 + k2
12361245
)
1246+
or
1247+
// See argument for why this is correct in compares_eq
1248+
exists(Operand l, BooleanValue bv |
1249+
unary_compares_eq(test, l, 0, bv.getValue().booleanNot(), value) and
1250+
compares_lt(valueNumberOfOperand(l), op, k, isLt, bv)
1251+
)
12371252
}
12381253

12391254
/** `(a < b + k) => (b > a - k) => (b >= a + (1-k))` */

‎cpp/ql/test/library-tests/controlflow/guards/GuardsCompare.expected‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -278,18 +278,34 @@
278278
| test.c:176:8:176:15 | ! ... | ! ... == 1 when ! ... is true |
279279
| test.c:176:8:176:15 | ! ... | ... < ... != 0 when ! ... is false |
280280
| test.c:176:8:176:15 | ! ... | ... < ... == 0 when ! ... is true |
281+
| test.c:176:8:176:15 | ! ... | a < b+0 when ! ... is false |
282+
| test.c:176:8:176:15 | ! ... | a >= b+0 when ! ... is true |
283+
| test.c:176:8:176:15 | ! ... | b < a+1 when ! ... is true |
284+
| test.c:176:8:176:15 | ! ... | b >= a+1 when ! ... is false |
281285
| test.c:176:10:176:14 | ... < ... | ! ... != 0 when ... < ... is false |
282286
| test.c:176:10:176:14 | ... < ... | ! ... != 1 when ... < ... is true |
283287
| test.c:176:10:176:14 | ... < ... | ! ... == 0 when ... < ... is true |
284288
| test.c:176:10:176:14 | ... < ... | ! ... == 1 when ... < ... is false |
285289
| test.c:176:10:176:14 | ... < ... | ... < ... != 0 when ... < ... is true |
286290
| test.c:176:10:176:14 | ... < ... | ... < ... == 0 when ... < ... is false |
291+
| test.c:176:10:176:14 | ... < ... | a < b+0 when ... < ... is true |
292+
| test.c:176:10:176:14 | ... < ... | a >= b+0 when ... < ... is false |
293+
| test.c:176:10:176:14 | ... < ... | b < a+1 when ... < ... is false |
294+
| test.c:176:10:176:14 | ... < ... | b >= a+1 when ... < ... is true |
295+
| test.c:182:8:182:34 | ! ... | 1.0 >= foo+1 when ! ... is false |
296+
| test.c:182:8:182:34 | ! ... | 9.999999999999999547e-07 < foo+1 when ! ... is false |
287297
| test.c:182:8:182:34 | ! ... | ! ... != 0 when ! ... is true |
288298
| test.c:182:8:182:34 | ! ... | ! ... != 1 when ! ... is false |
289299
| test.c:182:8:182:34 | ! ... | ! ... == 0 when ! ... is false |
290300
| test.c:182:8:182:34 | ! ... | ! ... == 1 when ! ... is true |
291301
| test.c:182:8:182:34 | ! ... | ... && ... != 0 when ! ... is false |
292302
| test.c:182:8:182:34 | ! ... | ... && ... == 0 when ! ... is true |
303+
| test.c:182:8:182:34 | ! ... | ... < ... != 0 when ! ... is false |
304+
| test.c:182:8:182:34 | ! ... | ... < ... == 1 when ! ... is false |
305+
| test.c:182:8:182:34 | ! ... | ... >= ... != 0 when ! ... is false |
306+
| test.c:182:8:182:34 | ! ... | ... >= ... == 1 when ! ... is false |
307+
| test.c:182:8:182:34 | ! ... | foo < 1.0+0 when ! ... is false |
308+
| test.c:182:8:182:34 | ! ... | foo >= 9.999999999999999547e-07+0 when ! ... is false |
293309
| test.c:182:10:182:20 | ... >= ... | 9.999999999999999547e-07 < foo+1 when ... >= ... is true |
294310
| test.c:182:10:182:20 | ... >= ... | 9.999999999999999547e-07 >= foo+1 when ... >= ... is false |
295311
| test.c:182:10:182:20 | ... >= ... | ... >= ... != 0 when ... >= ... is true |

‎cpp/ql/test/library-tests/controlflow/guards/GuardsEnsure.expected‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -165,6 +165,10 @@ binary
165165
| test.c:109:9:109:23 | ... \|\| ... | test.c:109:23:109:23 | 0 | < | test.c:109:19:109:19 | y | 1 | test.c:113:9:113:16 | return ... |
166166
| test.c:109:19:109:23 | ... < ... | test.c:109:19:109:19 | y | >= | test.c:109:23:109:23 | 0 | 0 | test.c:113:9:113:16 | return ... |
167167
| test.c:109:19:109:23 | ... < ... | test.c:109:23:109:23 | 0 | < | test.c:109:19:109:19 | y | 1 | test.c:113:9:113:16 | return ... |
168+
| test.c:176:8:176:15 | ! ... | test.c:176:10:176:10 | a | >= | test.c:176:14:176:14 | b | 0 | test.c:176:18:178:5 | { ... } |
169+
| test.c:176:8:176:15 | ! ... | test.c:176:14:176:14 | b | < | test.c:176:10:176:10 | a | 1 | test.c:176:18:178:5 | { ... } |
170+
| test.c:176:10:176:14 | ... < ... | test.c:176:10:176:10 | a | >= | test.c:176:14:176:14 | b | 0 | test.c:176:18:178:5 | { ... } |
171+
| test.c:176:10:176:14 | ... < ... | test.c:176:14:176:14 | b | < | test.c:176:10:176:10 | a | 1 | test.c:176:18:178:5 | { ... } |
168172
| test.c:182:10:182:20 | ... >= ... | test.c:182:10:182:12 | foo | >= | test.c:182:17:182:20 | 9.999999999999999547e-07 | 0 | test.c:181:25:182:20 | { ... } |
169173
| test.c:182:10:182:20 | ... >= ... | test.c:182:10:182:12 | foo | >= | test.c:182:17:182:20 | 9.999999999999999547e-07 | 0 | test.c:182:25:182:33 | foo |
170174
| test.c:182:10:182:20 | ... >= ... | test.c:182:17:182:20 | 9.999999999999999547e-07 | < | test.c:182:10:182:12 | foo | 1 | test.c:181:25:182:20 | { ... } |

‎cpp/ql/test/query-tests/Critical/MissingCheckScanf/MissingCheckScanf.expected‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -190,5 +190,3 @@ subpaths
190190
| test.cpp:484:9:484:9 | i | test.cpp:480:25:480:26 | scanf output argument | test.cpp:484:9:484:9 | i | This variable is read, but may not have been written. It should be guarded by a check that the $@ returns at least 1. | test.cpp:480:13:480:17 | call to scanf | call to scanf |
191191
| test.cpp:495:8:495:8 | i | test.cpp:491:25:491:26 | scanf output argument | test.cpp:495:8:495:8 | i | This variable is read, but may not have been written. It should be guarded by a check that the $@ returns at least 1. | test.cpp:491:13:491:17 | call to scanf | call to scanf |
192192
| test.cpp:545:8:545:8 | f | test.cpp:541:43:541:44 | sscanf output argument | test.cpp:545:8:545:8 | f | This variable is read, but may not have been written. It should be guarded by a check that the $@ returns at least 3. | test.cpp:541:10:541:15 | call to sscanf | call to sscanf |
193-
| test.cpp:569:9:569:9 | i | test.cpp:567:35:567:36 | scanf output argument | test.cpp:569:9:569:9 | i | This variable is read, but may not have been written. It should be guarded by a check that the $@ returns at least 1. | test.cpp:567:23:567:27 | call to scanf | call to scanf |
194-
| test.cpp:577:9:577:9 | i | test.cpp:575:30:575:31 | scanf output argument | test.cpp:577:9:577:9 | i | This variable is read, but may not have been written. It should be guarded by a check that the $@ returns at least 1. | test.cpp:575:18:575:22 | call to scanf | call to scanf |

‎cpp/ql/test/query-tests/Critical/MissingCheckScanf/test.cpp‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -566,14 +566,14 @@ void test_scanf_compared_in_conjunct_right(bool b) {
566566
int i;
567567
bool success = b && scanf("%d", &i) == 1;
568568
if(success) {
569-
use(i); // GOOD [FALSE POSITIVE]
569+
use(i); // GOOD
570570
}
571571
}
572572

573573
void test_scanf_compared_in_conjunct_left(bool b) {
574574
int i;
575575
bool success = scanf("%d", &i) == 1 && b;
576576
if(success) {
577-
use(i); // GOOD [FALSE POSITIVE]
577+
use(i); // GOOD
578578
}
579579
}

0 commit comments

Comments
 (0)