Skip to content

Commit 000a81f

Browse files
authored
Merge pull request github#16690 from MathiasVP/better-guards
C++: Fix missing results for `comparesEq` in `IRGuardCondition`
2 parents 06aa266 + 7819cc1 commit 000a81f

File tree

10 files changed

+135
-51
lines changed

10 files changed

+135
-51
lines changed

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

Lines changed: 70 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -375,6 +375,33 @@ cached
375375
class IRGuardCondition extends Instruction {
376376
Instruction branch;
377377

378+
/*
379+
* An `IRGuardCondition` supports reasoning about four different kinds of
380+
* relations:
381+
* 1. A unary equality relation of the form `e == k`
382+
* 2. A binary equality relation of the form `e1 == e2 + k`
383+
* 3. A unary inequality relation of the form `e < k`
384+
* 4. A binary inequality relation of the form `e1 < e2 + k`
385+
*
386+
* where `k` is a constant.
387+
*
388+
* Furthermore, the unary relations (i.e., case 1 and case 3) are also
389+
* inferred from `switch` statement guards: equality relations are inferred
390+
* from the unique `case` statement, if any, and inequality relations are
391+
* inferred from the [case range](https://gcc.gnu.org/onlinedocs/gcc/Case-Ranges.html)
392+
* gcc extension.
393+
*
394+
* The implementation of all four follows the same structure: Each relation
395+
* has a cached user-facing predicate that. For example,
396+
* `GuardCondition::comparesEq` calls `compares_eq`. This predicate has
397+
* several cases that recursively decompose the relation to bring it to a
398+
* canonical form (i.e., a relation of the form `e1 == e2 + k`). The base
399+
* case for this relation (i.e., `simple_comparison_eq`) handles
400+
* `CompareEQInstruction`s and `CompareNEInstruction`, and recursive
401+
* predicates (e.g., `complex_eq`) rewrites larger expressions such as
402+
* `e1 + k1 == e2 + k2` into canonical the form `e1 == e2 + (k2 - k1)`.
403+
*/
404+
378405
cached
379406
IRGuardCondition() { branch = getBranchForCondition(this) }
380407

@@ -776,7 +803,9 @@ private predicate unary_compares_eq(
776803
Instruction test, Operand op, int k, boolean areEqual, boolean inNonZeroCase, AbstractValue value
777804
) {
778805
/* The simple case where the test *is* the comparison so areEqual = testIsTrue xor eq. */
779-
exists(AbstractValue v | unary_simple_comparison_eq(test, op, k, inNonZeroCase, v) |
806+
exists(AbstractValue v |
807+
unary_simple_comparison_eq(test, k, inNonZeroCase, v) and op.getDef() = test
808+
|
780809
areEqual = true and value = v
781810
or
782811
areEqual = false and value = v.getDualValue()
@@ -821,45 +850,55 @@ private predicate simple_comparison_eq(
821850
value.(BooleanValue).getValue() = false
822851
}
823852

824-
/**
825-
* Holds if `test` is an instruction that is part of test that eventually is
826-
* used in a conditional branch.
827-
*/
828-
private predicate relevantUnaryComparison(Instruction test) {
829-
not test instanceof CompareInstruction and
830-
exists(IRType type, ConditionalBranchInstruction branch |
831-
type instanceof IRAddressType or type instanceof IRIntegerType
832-
|
833-
type = test.getResultIRType() and
834-
branch.getCondition() = test
835-
)
836-
or
837-
exists(LogicalNotInstruction logicalNot |
838-
relevantUnaryComparison(logicalNot) and
839-
test = logicalNot.getUnary()
840-
)
841-
}
842-
843853
/**
844854
* Rearrange various simple comparisons into `op == k` form.
845855
*/
846856
private predicate unary_simple_comparison_eq(
847-
Instruction test, Operand op, int k, boolean inNonZeroCase, AbstractValue value
857+
Instruction test, int k, boolean inNonZeroCase, AbstractValue value
848858
) {
849859
exists(SwitchInstruction switch, CaseEdge case |
850860
test = switch.getExpression() and
851-
op.getDef() = test and
852861
case = value.(MatchValue).getCase() and
853862
exists(switch.getSuccessor(case)) and
854863
case.getValue().toInt() = k and
855864
inNonZeroCase = false
856865
)
857866
or
858-
// There's no implicit CompareInstruction in files compiled as C since C
859-
// doesn't have implicit boolean conversions. So instead we check whether
860-
// there's a branch on a value of pointer or integer type.
861-
relevantUnaryComparison(test) and
862-
op.getDef() = test and
867+
// Any instruction with an integral type could potentially be part of a
868+
// check for nullness when used in a guard. So we include all integral
869+
// typed instructions here. However, since some of these instructions are
870+
// already included as guards in other cases, we exclude those here.
871+
// These are instructions that compute a binary equality or inequality
872+
// relation. For example, the following:
873+
// ```cpp
874+
// if(a == b + 42) { ... }
875+
// ```
876+
// generates the following IR:
877+
// ```
878+
// r1(glval<int>) = VariableAddress[a] :
879+
// r2(int) = Load[a] : &:r1, m1
880+
// r3(glval<int>) = VariableAddress[b] :
881+
// r4(int) = Load[b] : &:r3, m2
882+
// r5(int) = Constant[42] :
883+
// r6(int) = Add : r4, r5
884+
// r7(bool) = CompareEQ : r2, r6
885+
// v1(void) = ConditionalBranch : r7
886+
// ```
887+
// and since `r7` is an integral typed instruction this predicate could
888+
// include a case for when `r7` evaluates to true (in which case we would
889+
// infer that `r6` was non-zero, and a case for when `r7` evaluates to false
890+
// (in which case we would infer that `r6` was zero).
891+
// However, since `a == b + 42` is already supported when reasoning about
892+
// binary equalities we exclude those cases here.
893+
not test.isGLValue() and
894+
not simple_comparison_eq(test, _, _, _, _) and
895+
not simple_comparison_lt(test, _, _, _) and
896+
not test = any(SwitchInstruction switch).getExpression() and
897+
(
898+
test.getResultIRType() instanceof IRAddressType or
899+
test.getResultIRType() instanceof IRIntegerType or
900+
test.getResultIRType() instanceof IRBooleanType
901+
) and
863902
(
864903
k = 1 and
865904
value.(BooleanValue).getValue() = true and
@@ -913,7 +952,8 @@ private predicate compares_lt(
913952

914953
/** Holds if `op < k` evaluates to `isLt` given that `test` evaluates to `value`. */
915954
private predicate compares_lt(Instruction test, Operand op, int k, boolean isLt, AbstractValue value) {
916-
simple_comparison_lt(test, op, k, isLt, value)
955+
unary_simple_comparison_lt(test, k, isLt, value) and
956+
op.getDef() = test
917957
or
918958
complex_lt(test, op, k, isLt, value)
919959
or
@@ -960,12 +1000,11 @@ private predicate simple_comparison_lt(CompareInstruction cmp, Operand left, Ope
9601000
}
9611001

9621002
/** Rearrange various simple comparisons into `op < k` form. */
963-
private predicate simple_comparison_lt(
964-
Instruction test, Operand op, int k, boolean isLt, AbstractValue value
1003+
private predicate unary_simple_comparison_lt(
1004+
Instruction test, int k, boolean isLt, AbstractValue value
9651005
) {
9661006
exists(SwitchInstruction switch, CaseEdge case |
9671007
test = switch.getExpression() and
968-
op.getDef() = test and
9691008
case = value.(MatchValue).getCase() and
9701009
exists(switch.getSuccessor(case)) and
9711010
case.getMaxValue() > case.getMinValue()

cpp/ql/test/library-tests/controlflow/guards-ir/tests.expected

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -74,6 +74,8 @@ astGuardsCompare
7474
| 34 | j >= 10+0 when ... < ... is false |
7575
| 42 | 10 < j+1 when ... < ... is false |
7676
| 42 | 10 >= j+1 when ... < ... is true |
77+
| 42 | call to getABool != 0 when call to getABool is true |
78+
| 42 | call to getABool == 0 when call to getABool is false |
7779
| 42 | j < 10+0 when ... < ... is true |
7880
| 42 | j >= 10+0 when ... < ... is false |
7981
| 44 | 0 < z+0 when ... > ... is true |
@@ -537,6 +539,8 @@ astGuardsEnsure_const
537539
| test.cpp:31:7:31:13 | ... == ... | test.cpp:31:7:31:7 | x | != | -1 | 34 | 34 |
538540
| test.cpp:31:7:31:13 | ... == ... | test.cpp:31:7:31:7 | x | == | -1 | 30 | 30 |
539541
| test.cpp:31:7:31:13 | ... == ... | test.cpp:31:7:31:7 | x | == | -1 | 31 | 32 |
542+
| test.cpp:42:13:42:20 | call to getABool | test.cpp:42:13:42:20 | call to getABool | != | 0 | 43 | 45 |
543+
| test.cpp:42:13:42:20 | call to getABool | test.cpp:42:13:42:20 | call to getABool | == | 0 | 53 | 53 |
540544
irGuards
541545
| test.c:7:9:7:13 | CompareGT: ... > ... |
542546
| test.c:17:8:17:12 | CompareLT: ... < ... |
@@ -613,6 +617,8 @@ irGuardsCompare
613617
| 34 | j >= 10+0 when CompareLT: ... < ... is false |
614618
| 42 | 10 < j+1 when CompareLT: ... < ... is false |
615619
| 42 | 10 >= j+1 when CompareLT: ... < ... is true |
620+
| 42 | call to getABool != 0 when Call: call to getABool is true |
621+
| 42 | call to getABool == 0 when Call: call to getABool is false |
616622
| 42 | j < 10 when CompareLT: ... < ... is true |
617623
| 42 | j < 10+0 when CompareLT: ... < ... is true |
618624
| 42 | j >= 10 when CompareLT: ... < ... is false |
@@ -1081,3 +1087,5 @@ irGuardsEnsure_const
10811087
| test.cpp:31:7:31:13 | CompareEQ: ... == ... | test.cpp:31:7:31:7 | Load: x | != | -1 | 34 | 34 |
10821088
| test.cpp:31:7:31:13 | CompareEQ: ... == ... | test.cpp:31:7:31:7 | Load: x | == | -1 | 30 | 30 |
10831089
| test.cpp:31:7:31:13 | CompareEQ: ... == ... | test.cpp:31:7:31:7 | Load: x | == | -1 | 32 | 32 |
1090+
| test.cpp:42:13:42:20 | Call: call to getABool | test.cpp:42:13:42:20 | Call: call to getABool | != | 0 | 44 | 44 |
1091+
| test.cpp:42:13:42:20 | Call: call to getABool | test.cpp:42:13:42:20 | Call: call to getABool | == | 0 | 53 | 53 |

cpp/ql/test/library-tests/controlflow/guards/Guards.expected

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -42,3 +42,6 @@
4242
| test.cpp:99:6:99:6 | f |
4343
| test.cpp:105:6:105:14 | ... != ... |
4444
| test.cpp:111:6:111:14 | ... != ... |
45+
| test.cpp:122:9:122:9 | b |
46+
| test.cpp:125:13:125:20 | ! ... |
47+
| test.cpp:125:14:125:17 | call to safe |

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

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -44,6 +44,8 @@
4444
| 34 | j >= 10+0 when ... < ... is false |
4545
| 42 | 10 < j+1 when ... < ... is false |
4646
| 42 | 10 >= j+1 when ... < ... is true |
47+
| 42 | call to getABool != 0 when call to getABool is true |
48+
| 42 | call to getABool == 0 when call to getABool is false |
4749
| 42 | j < 10 when ... < ... is true |
4850
| 42 | j < 10+0 when ... < ... is true |
4951
| 42 | j >= 10 when ... < ... is false |
@@ -149,6 +151,13 @@
149151
| 111 | 0.0 == i+0 when ... != ... is false |
150152
| 111 | i != 0.0+0 when ... != ... is true |
151153
| 111 | i == 0.0+0 when ... != ... is false |
154+
| 122 | b != 0 when b is true |
155+
| 122 | b == 0 when b is false |
156+
| 125 | ! ... != 0 when ! ... is true |
157+
| 125 | ! ... == 0 when ! ... is false |
158+
| 125 | call to safe != 0 when ! ... is false |
159+
| 125 | call to safe != 0 when call to safe is true |
160+
| 125 | call to safe == 0 when call to safe is false |
152161
| 126 | 1 != 0 when 1 is true |
153162
| 126 | 1 != 0 when ... && ... is true |
154163
| 126 | 1 == 0 when 1 is false |

cpp/ql/test/library-tests/controlflow/guards/GuardsControl.expected

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -100,3 +100,7 @@
100100
| test.cpp:99:6:99:6 | f | true | 99 | 100 |
101101
| test.cpp:105:6:105:14 | ... != ... | true | 105 | 106 |
102102
| test.cpp:111:6:111:14 | ... != ... | true | 111 | 112 |
103+
| test.cpp:122:9:122:9 | b | true | 123 | 125 |
104+
| test.cpp:122:9:122:9 | b | true | 125 | 125 |
105+
| test.cpp:125:13:125:20 | ! ... | true | 125 | 125 |
106+
| test.cpp:125:14:125:17 | call to safe | false | 125 | 125 |

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

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -257,10 +257,16 @@ unary
257257
| test.cpp:31:7:31:13 | ... == ... | test.cpp:31:7:31:7 | x | != | -1 | 34 | 34 |
258258
| test.cpp:31:7:31:13 | ... == ... | test.cpp:31:7:31:7 | x | == | -1 | 30 | 30 |
259259
| test.cpp:31:7:31:13 | ... == ... | test.cpp:31:7:31:7 | x | == | -1 | 31 | 32 |
260+
| test.cpp:42:13:42:20 | call to getABool | test.cpp:42:13:42:20 | call to getABool | != | 0 | 43 | 45 |
261+
| test.cpp:42:13:42:20 | call to getABool | test.cpp:42:13:42:20 | call to getABool | == | 0 | 53 | 53 |
260262
| test.cpp:61:10:61:10 | i | test.cpp:61:10:61:10 | i | == | 0 | 62 | 64 |
261263
| test.cpp:61:10:61:10 | i | test.cpp:61:10:61:10 | i | == | 1 | 65 | 66 |
262264
| test.cpp:74:10:74:10 | i | test.cpp:74:10:74:10 | i | < | 11 | 75 | 77 |
263265
| test.cpp:74:10:74:10 | i | test.cpp:74:10:74:10 | i | < | 21 | 78 | 79 |
264266
| test.cpp:74:10:74:10 | i | test.cpp:74:10:74:10 | i | >= | 0 | 75 | 77 |
265267
| test.cpp:74:10:74:10 | i | test.cpp:74:10:74:10 | i | >= | 11 | 78 | 79 |
266268
| test.cpp:93:6:93:6 | c | test.cpp:93:6:93:6 | c | != | 0 | 93 | 94 |
269+
| test.cpp:122:9:122:9 | b | test.cpp:122:9:122:9 | b | != | 0 | 123 | 125 |
270+
| test.cpp:122:9:122:9 | b | test.cpp:122:9:122:9 | b | != | 0 | 125 | 125 |
271+
| test.cpp:125:13:125:20 | ! ... | test.cpp:125:13:125:20 | ! ... | != | 0 | 125 | 125 |
272+
| test.cpp:125:14:125:17 | call to safe | test.cpp:125:14:125:17 | call to safe | == | 0 | 125 | 125 |

cpp/ql/test/library-tests/controlflow/guards/test.cpp

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -112,3 +112,17 @@ void int_float_comparison(int i) {
112112
use(i);
113113
}
114114
}
115+
116+
int source();
117+
bool safe(int);
118+
119+
void test(bool b)
120+
{
121+
int x;
122+
if (b)
123+
{
124+
x = source();
125+
if (!safe(x)) return;
126+
}
127+
use(x);
128+
}

cpp/ql/test/library-tests/dataflow/dataflow-tests/BarrierGuard.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -83,7 +83,7 @@ void test_guard_and_reassign() {
8383
if(!guarded(x)) {
8484
x = 0;
8585
}
86-
sink(x); // $ SPURIOUS: ast,ir
86+
sink(x); // $ SPURIOUS: ast
8787
}
8888

8989
void test_phi_read_guard(bool b) {
@@ -98,7 +98,7 @@ void test_phi_read_guard(bool b) {
9898
return;
9999
}
100100

101-
sink(x); // $ SPURIOUS: ast,ir
101+
sink(x); // $ SPURIOUS: ast
102102
}
103103

104104
bool unsafe(int);

cpp/ql/test/library-tests/dataflow/dataflow-tests/TestBase.qll

Lines changed: 19 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -7,14 +7,17 @@ module AstTest {
77
* S in `if (guarded(x)) S`.
88
*/
99
// This is tested in `BarrierGuard.cpp`.
10-
predicate testBarrierGuard(GuardCondition g, Expr checked, boolean isTrue) {
11-
g.(FunctionCall).getTarget().getName() = "guarded" and
12-
checked = g.(FunctionCall).getArgument(0) and
13-
isTrue = true
14-
or
15-
g.(FunctionCall).getTarget().getName() = "unsafe" and
16-
checked = g.(FunctionCall).getArgument(0) and
17-
isTrue = false
10+
predicate testBarrierGuard(GuardCondition g, Expr checked, boolean branch) {
11+
exists(Call call, boolean b |
12+
checked = call.getArgument(0) and
13+
g.comparesEq(call, 0, b, any(BooleanValue bv | bv.getValue() = branch))
14+
|
15+
call.getTarget().hasName("guarded") and
16+
b = false
17+
or
18+
call.getTarget().hasName("unsafe") and
19+
b = true
20+
)
1821
}
1922

2023
/** Common data flow configuration to be used by tests. */
@@ -106,16 +109,16 @@ module IRTest {
106109
* S in `if (guarded(x)) S`.
107110
*/
108111
// This is tested in `BarrierGuard.cpp`.
109-
predicate testBarrierGuard(IRGuardCondition g, Expr checked, boolean isTrue) {
110-
exists(Call call |
111-
call = g.getUnconvertedResultExpression() and
112-
checked = call.getArgument(0)
112+
predicate testBarrierGuard(IRGuardCondition g, Expr checked, boolean branch) {
113+
exists(CallInstruction call, boolean b |
114+
checked = call.getArgument(0).getUnconvertedResultExpression() and
115+
g.comparesEq(call.getAUse(), 0, b, any(BooleanValue bv | bv.getValue() = branch))
113116
|
114-
call.getTarget().hasName("guarded") and
115-
isTrue = true
117+
call.getStaticCallTarget().hasName("guarded") and
118+
b = false
116119
or
117-
call.getTarget().hasName("unsafe") and
118-
isTrue = false
120+
call.getStaticCallTarget().hasName("unsafe") and
121+
b = true
119122
)
120123
}
121124

cpp/ql/test/library-tests/dataflow/dataflow-tests/test-source-sink.expected

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -145,8 +145,6 @@ irFlow
145145
| BarrierGuard.cpp:49:10:49:15 | call to source | BarrierGuard.cpp:55:13:55:13 | x |
146146
| BarrierGuard.cpp:60:11:60:16 | call to source | BarrierGuard.cpp:64:14:64:14 | x |
147147
| BarrierGuard.cpp:60:11:60:16 | call to source | BarrierGuard.cpp:66:14:66:14 | x |
148-
| BarrierGuard.cpp:81:11:81:16 | call to source | BarrierGuard.cpp:86:8:86:8 | x |
149-
| BarrierGuard.cpp:90:11:90:16 | call to source | BarrierGuard.cpp:101:8:101:8 | x |
150148
| acrossLinkTargets.cpp:19:27:19:32 | call to source | acrossLinkTargets.cpp:12:8:12:8 | x |
151149
| clang.cpp:12:9:12:20 | sourceArray1 | clang.cpp:18:8:18:19 | sourceArray1 |
152150
| clang.cpp:12:9:12:20 | sourceArray1 | clang.cpp:23:17:23:29 | *& ... |

0 commit comments

Comments
 (0)