From 398b90a15df7514eaec928c3f6abb6bbbe691b44 Mon Sep 17 00:00:00 2001 From: Mathias Vorreiter Pedersen Date: Mon, 20 May 2024 17:15:20 +0100 Subject: [PATCH 1/3] C++: Rename a few predicates. --- .../semmle/code/cpp/controlflow/IRGuards.qll | 42 +++++++++++-------- 1 file changed, 24 insertions(+), 18 deletions(-) diff --git a/cpp/ql/lib/semmle/code/cpp/controlflow/IRGuards.qll b/cpp/ql/lib/semmle/code/cpp/controlflow/IRGuards.qll index 83f8dc8b3bc7..4cb91228d43f 100644 --- a/cpp/ql/lib/semmle/code/cpp/controlflow/IRGuards.qll +++ b/cpp/ql/lib/semmle/code/cpp/controlflow/IRGuards.qll @@ -565,7 +565,7 @@ class IRGuardCondition extends Instruction { /** Holds if (determined by this guard) `op == k` evaluates to `areEqual` if this expression evaluates to `value`. */ cached predicate comparesEq(Operand op, int k, boolean areEqual, AbstractValue value) { - compares_eq(this, op, k, areEqual, value) + unary_compares_eq(this, op, k, areEqual, value) } /** @@ -586,7 +586,7 @@ class IRGuardCondition extends Instruction { cached predicate ensuresEq(Operand op, int k, IRBlock block, boolean areEqual) { exists(AbstractValue value | - compares_eq(this, op, k, areEqual, value) and this.valueControls(block, value) + unary_compares_eq(this, op, k, areEqual, value) and this.valueControls(block, value) ) } @@ -611,7 +611,7 @@ class IRGuardCondition extends Instruction { cached predicate ensuresEqEdge(Operand op, int k, IRBlock pred, IRBlock succ, boolean areEqual) { exists(AbstractValue value | - compares_eq(this, op, k, areEqual, value) and + unary_compares_eq(this, op, k, areEqual, value) and this.valueControlsEdge(pred, succ, value) ) } @@ -738,21 +738,21 @@ private predicate compares_eq( } /** Holds if `op == k` is `areEqual` given that `test` is equal to `value`. */ -private predicate compares_eq( +private predicate unary_compares_eq( Instruction test, Operand op, int k, boolean areEqual, AbstractValue value ) { /* The simple case where the test *is* the comparison so areEqual = testIsTrue xor eq. */ - exists(AbstractValue v | simple_comparison_eq(test, op, k, v) | + exists(AbstractValue v | unary_simple_comparison_eq(test, op, k, v) | areEqual = true and value = v or areEqual = false and value = v.getDualValue() ) or - complex_eq(test, op, k, areEqual, value) + unary_complex_eq(test, op, k, areEqual, value) or /* (x is true => (op == k)) => (!x is false => (op == k)) */ exists(AbstractValue dual | value = dual.getDualValue() | - compares_eq(test.(LogicalNotInstruction).getUnary(), op, k, areEqual, dual) + unary_compares_eq(test.(LogicalNotInstruction).getUnary(), op, k, areEqual, dual) ) or // ((test is `areEqual` => op == const + k2) and const == `k1`) => @@ -782,7 +782,9 @@ private predicate simple_comparison_eq( } /** Rearrange various simple comparisons into `op == k` form. */ -private predicate simple_comparison_eq(Instruction test, Operand op, int k, AbstractValue value) { +private predicate unary_simple_comparison_eq( + Instruction test, Operand op, int k, AbstractValue value +) { exists(SwitchInstruction switch, CaseEdge case | test = switch.getExpression() and op.getDef() = test and @@ -821,12 +823,12 @@ private predicate complex_eq( add_eq(cmp, left, right, k, areEqual, value) } -private predicate complex_eq( +private predicate unary_complex_eq( Instruction test, Operand op, int k, boolean areEqual, AbstractValue value ) { - sub_eq(test, op, k, areEqual, value) + unary_sub_eq(test, op, k, areEqual, value) or - add_eq(test, op, k, areEqual, value) + unary_add_eq(test, op, k, areEqual, value) } /* @@ -1090,16 +1092,18 @@ private predicate sub_eq( } // op - x == c => op == (c+x) -private predicate sub_eq(Instruction test, Operand op, int k, boolean areEqual, AbstractValue value) { +private predicate unary_sub_eq( + Instruction test, Operand op, int k, boolean areEqual, AbstractValue value +) { exists(SubInstruction sub, int c, int x | - compares_eq(test, sub.getAUse(), c, areEqual, value) and + unary_compares_eq(test, sub.getAUse(), c, areEqual, value) and op = sub.getLeftOperand() and x = int_value(sub.getRight()) and k = c + x ) or exists(PointerSubInstruction sub, int c, int x | - compares_eq(test, sub.getAUse(), c, areEqual, value) and + unary_compares_eq(test, sub.getAUse(), c, areEqual, value) and op = sub.getLeftOperand() and x = int_value(sub.getRight()) and k = c + x @@ -1153,11 +1157,12 @@ private predicate add_eq( } // left + x == right + c => left == right + (c-x) -private predicate add_eq( - Instruction test, Operand left, int k, boolean areEqual, AbstractValue value +private predicate unary_add_eq( + Instruction test, Operand left, int k, boolean areEqual, + AbstractValue value ) { exists(AddInstruction lhs, int c, int x | - compares_eq(test, lhs.getAUse(), c, areEqual, value) and + unary_compares_eq(test, lhs.getAUse(), c, areEqual, value) and ( left = lhs.getLeftOperand() and x = int_value(lhs.getRight()) or @@ -1167,7 +1172,8 @@ private predicate add_eq( ) or exists(PointerAddInstruction lhs, int c, int x | - compares_eq(test, lhs.getAUse(), c, areEqual, value) and + + unary_compares_eq(test, lhs.getAUse(), c, areEqual, value) and ( left = lhs.getLeftOperand() and x = int_value(lhs.getRight()) or From 0a550bb919737e0cfed87b01fbc0466c64a2a79b Mon Sep 17 00:00:00 2001 From: Mathias Vorreiter Pedersen Date: Mon, 20 May 2024 17:25:57 +0100 Subject: [PATCH 2/3] C++: Support 'if(!p)' for C programs in IRGuards. --- .../semmle/code/cpp/controlflow/IRGuards.qll | 133 +++++++++++++----- 1 file changed, 96 insertions(+), 37 deletions(-) diff --git a/cpp/ql/lib/semmle/code/cpp/controlflow/IRGuards.qll b/cpp/ql/lib/semmle/code/cpp/controlflow/IRGuards.qll index 4cb91228d43f..f06db98e91b7 100644 --- a/cpp/ql/lib/semmle/code/cpp/controlflow/IRGuards.qll +++ b/cpp/ql/lib/semmle/code/cpp/controlflow/IRGuards.qll @@ -565,7 +565,7 @@ class IRGuardCondition extends Instruction { /** Holds if (determined by this guard) `op == k` evaluates to `areEqual` if this expression evaluates to `value`. */ cached predicate comparesEq(Operand op, int k, boolean areEqual, AbstractValue value) { - unary_compares_eq(this, op, k, areEqual, value) + unary_compares_eq(this, op, k, areEqual, false, value) } /** @@ -586,7 +586,7 @@ class IRGuardCondition extends Instruction { cached predicate ensuresEq(Operand op, int k, IRBlock block, boolean areEqual) { exists(AbstractValue value | - unary_compares_eq(this, op, k, areEqual, value) and this.valueControls(block, value) + unary_compares_eq(this, op, k, areEqual, false, value) and this.valueControls(block, value) ) } @@ -611,7 +611,7 @@ class IRGuardCondition extends Instruction { cached predicate ensuresEqEdge(Operand op, int k, IRBlock pred, IRBlock succ, boolean areEqual) { exists(AbstractValue value | - unary_compares_eq(this, op, k, areEqual, value) and + unary_compares_eq(this, op, k, areEqual, false, value) and this.valueControlsEdge(pred, succ, value) ) } @@ -737,26 +737,66 @@ private predicate compares_eq( ) } -/** Holds if `op == k` is `areEqual` given that `test` is equal to `value`. */ +/** + * Holds if `op == k` is `areEqual` given that `test` is equal to `value`. + * + * Many internal predicates in this file have a `inNonZeroCase` column. + * Ideally, the `k` column would be a type such as `Option::Option`, to + * represent whether we have a concrete value `k` such that `op == k`, or whether + * we only know that `op != 0`. + * However, cannot instantiate `Option` with an infinite type. Thus the boolean + * `inNonZeroCase` is used to distinquish the `Some` (where we have a concrete + * value `k`) and `None` cases (where we only know that `op != 0`). + * + * Thus, if `inNonZeroCase = true` then `op != 0` and the value of `k` is + * meaningless. + * + * To see why `inNonZeroCase` is needed consider the following C program: + * ```c + * char* p = ...; + * if(p) { + * use(p); + * } + * ``` + * in C++ there would be an int-to-bool conversion on `p`. However, since C + * does not have booleans there is no conversion. We want to be able to + * conclude that `p` is non-zero in the true branch, so we need to give `k` + * some value. However, simply setting `k = 1` would make the rest of the + * analysis think that `k == 1` holds inside the branch. So we distinquish + * between the above case and + * ```c + * if(p == 1) { + * use(p) + * } + * ``` + * by setting `inNonZeroCase` to `true` in the former case, but not in the + * latter. + */ private predicate unary_compares_eq( - Instruction test, Operand op, int k, boolean areEqual, AbstractValue value + Instruction test, Operand op, int k, boolean areEqual, boolean inNonZeroCase, AbstractValue value ) { /* The simple case where the test *is* the comparison so areEqual = testIsTrue xor eq. */ - exists(AbstractValue v | unary_simple_comparison_eq(test, op, k, v) | + exists(AbstractValue v | unary_simple_comparison_eq(test, op, k, inNonZeroCase, v) | areEqual = true and value = v or areEqual = false and value = v.getDualValue() ) or - unary_complex_eq(test, op, k, areEqual, value) + unary_complex_eq(test, op, k, areEqual, inNonZeroCase, value) or /* (x is true => (op == k)) => (!x is false => (op == k)) */ - exists(AbstractValue dual | value = dual.getDualValue() | - unary_compares_eq(test.(LogicalNotInstruction).getUnary(), op, k, areEqual, dual) + exists(AbstractValue dual, boolean inNonZeroCase0 | + value = dual.getDualValue() and + unary_compares_eq(test.(LogicalNotInstruction).getUnary(), op, k, inNonZeroCase0, areEqual, dual) + | + k = 0 and inNonZeroCase = inNonZeroCase0 + or + k != 0 and inNonZeroCase = true ) or // ((test is `areEqual` => op == const + k2) and const == `k1`) => // test is `areEqual` => op == k1 + k2 + inNonZeroCase = false and exists(int k1, int k2, ConstantInstruction const | compares_eq(test, op, const.getAUse(), k2, areEqual, value) and int_value(const) = k1 and @@ -781,37 +821,53 @@ private predicate simple_comparison_eq( value.(BooleanValue).getValue() = false } -/** Rearrange various simple comparisons into `op == k` form. */ +/** + * Holds if `test` is an instruction that is part of test that eventually is + * used in a conditional branch. + */ +private predicate relevantUnaryComparison(Instruction test) { + not test instanceof CompareInstruction and + exists(IRType type, ConditionalBranchInstruction branch | + type instanceof IRAddressType or type instanceof IRIntegerType + | + type = test.getResultIRType() and + branch.getCondition() = test + ) + or + exists(LogicalNotInstruction logicalNot | + relevantUnaryComparison(logicalNot) and + test = logicalNot.getUnary() + ) +} + +/** + * Rearrange various simple comparisons into `op == k` form. + */ private predicate unary_simple_comparison_eq( - Instruction test, Operand op, int k, AbstractValue value + Instruction test, Operand op, int k, boolean inNonZeroCase, AbstractValue value ) { exists(SwitchInstruction switch, CaseEdge case | test = switch.getExpression() and op.getDef() = test and case = value.(MatchValue).getCase() and exists(switch.getSuccessor(case)) and - case.getValue().toInt() = k + case.getValue().toInt() = k and + inNonZeroCase = false ) or // There's no implicit CompareInstruction in files compiled as C since C // doesn't have implicit boolean conversions. So instead we check whether // there's a branch on a value of pointer or integer type. - exists(ConditionalBranchInstruction branch, IRType type | - not test instanceof CompareInstruction and - type = test.getResultIRType() and - (type instanceof IRAddressType or type instanceof IRIntegerType) and - test = branch.getCondition() and - op.getDef() = test - | - // We'd like to also include a case such as: - // ``` - // k = 1 and - // value.(BooleanValue).getValue() = true - // ``` - // but all we know is that the value is non-zero in the true branch. - // So we can only conclude something in the false branch. + relevantUnaryComparison(test) and + op.getDef() = test and + ( + k = 1 and + value.(BooleanValue).getValue() = true and + inNonZeroCase = true + or k = 0 and - value.(BooleanValue).getValue() = false + value.(BooleanValue).getValue() = false and + inNonZeroCase = false ) } @@ -824,11 +880,11 @@ private predicate complex_eq( } private predicate unary_complex_eq( - Instruction test, Operand op, int k, boolean areEqual, AbstractValue value + Instruction test, Operand op, int k, boolean areEqual, boolean inNonZeroCase, AbstractValue value ) { - unary_sub_eq(test, op, k, areEqual, value) + unary_sub_eq(test, op, k, areEqual, inNonZeroCase, value) or - unary_add_eq(test, op, k, areEqual, value) + unary_add_eq(test, op, k, areEqual, inNonZeroCase, value) } /* @@ -1093,17 +1149,19 @@ private predicate sub_eq( // op - x == c => op == (c+x) private predicate unary_sub_eq( - Instruction test, Operand op, int k, boolean areEqual, AbstractValue value + Instruction test, Operand op, int k, boolean areEqual, boolean inNonZeroCase, AbstractValue value ) { + inNonZeroCase = false and exists(SubInstruction sub, int c, int x | - unary_compares_eq(test, sub.getAUse(), c, areEqual, value) and + unary_compares_eq(test, sub.getAUse(), c, areEqual, inNonZeroCase, value) and op = sub.getLeftOperand() and x = int_value(sub.getRight()) and k = c + x ) or + inNonZeroCase = false and exists(PointerSubInstruction sub, int c, int x | - unary_compares_eq(test, sub.getAUse(), c, areEqual, value) and + unary_compares_eq(test, sub.getAUse(), c, areEqual, inNonZeroCase, value) and op = sub.getLeftOperand() and x = int_value(sub.getRight()) and k = c + x @@ -1158,11 +1216,12 @@ private predicate add_eq( // left + x == right + c => left == right + (c-x) private predicate unary_add_eq( - Instruction test, Operand left, int k, boolean areEqual, + Instruction test, Operand left, int k, boolean areEqual, boolean inNonZeroCase, AbstractValue value ) { + inNonZeroCase = false and exists(AddInstruction lhs, int c, int x | - unary_compares_eq(test, lhs.getAUse(), c, areEqual, value) and + unary_compares_eq(test, lhs.getAUse(), c, areEqual, inNonZeroCase, value) and ( left = lhs.getLeftOperand() and x = int_value(lhs.getRight()) or @@ -1171,9 +1230,9 @@ private predicate unary_add_eq( k = c - x ) or + inNonZeroCase = false and exists(PointerAddInstruction lhs, int c, int x | - - unary_compares_eq(test, lhs.getAUse(), c, areEqual, value) and + unary_compares_eq(test, lhs.getAUse(), c, areEqual, inNonZeroCase, value) and ( left = lhs.getLeftOperand() and x = int_value(lhs.getRight()) or From 5893e3856743d0d43902086cf9c78cc73922e09e Mon Sep 17 00:00:00 2001 From: Mathias Vorreiter Pedersen Date: Mon, 20 May 2024 17:33:33 +0100 Subject: [PATCH 3/3] C++: Accept test changes. --- .../library-tests/controlflow/guards-ir/tests.expected | 8 ++++++++ .../controlflow/guards/GuardsCompare.expected | 9 +++++++++ .../controlflow/guards/GuardsEnsure.expected | 3 +++ 3 files changed, 20 insertions(+) diff --git a/cpp/ql/test/library-tests/controlflow/guards-ir/tests.expected b/cpp/ql/test/library-tests/controlflow/guards-ir/tests.expected index d50ca1609163..6cf7d2b6a958 100644 --- a/cpp/ql/test/library-tests/controlflow/guards-ir/tests.expected +++ b/cpp/ql/test/library-tests/controlflow/guards-ir/tests.expected @@ -160,6 +160,9 @@ astGuardsCompare | 137 | 0 == 0 when 0 is false | | 146 | ! ... != 0 when ! ... is true | | 146 | ! ... == 0 when ! ... is false | +| 146 | x != 0 when ! ... is false | +| 146 | x != 0 when x is true | +| 146 | x == 0 when x is false | | 152 | x != 0 when ... && ... is true | | 152 | x != 0 when x is true | | 152 | x == 0 when x is false | @@ -518,6 +521,7 @@ astGuardsEnsure_const | test.c:131:7:131:7 | b | test.c:131:7:131:7 | b | != | 0 | 131 | 132 | | test.c:137:7:137:7 | 0 | test.c:137:7:137:7 | 0 | == | 0 | 142 | 136 | | test.c:146:7:146:8 | ! ... | test.c:146:7:146:8 | ! ... | != | 0 | 146 | 147 | +| test.c:146:8:146:8 | x | test.c:146:8:146:8 | x | == | 0 | 146 | 147 | | test.c:152:10:152:10 | x | test.c:152:10:152:10 | x | != | 0 | 151 | 152 | | test.c:152:10:152:10 | x | test.c:152:10:152:10 | x | != | 0 | 152 | 152 | | test.c:152:10:152:15 | ... && ... | test.c:152:10:152:10 | x | != | 0 | 151 | 152 | @@ -689,6 +693,9 @@ irGuardsCompare | 137 | 0 == 0 when Constant: 0 is false | | 146 | ! ... != 0 when LogicalNot: ! ... is true | | 146 | ! ... == 0 when LogicalNot: ! ... is false | +| 146 | x != 0 when Load: x is true | +| 146 | x != 0 when LogicalNot: ! ... is false | +| 146 | x == 0 when Load: x is false | | 152 | x != 0 when Load: x is true | | 152 | x == 0 when Load: x is false | | 152 | y != 0 when Load: y is true | @@ -1063,6 +1070,7 @@ irGuardsEnsure_const | test.c:131:7:131:7 | Load: b | test.c:131:7:131:7 | Load: b | != | 0 | 132 | 132 | | test.c:137:7:137:7 | Constant: 0 | test.c:137:7:137:7 | Constant: 0 | == | 0 | 142 | 142 | | test.c:146:7:146:8 | LogicalNot: ! ... | test.c:146:7:146:8 | LogicalNot: ! ... | != | 0 | 147 | 147 | +| test.c:146:8:146:8 | Load: x | test.c:146:8:146:8 | Load: x | == | 0 | 147 | 147 | | test.c:152:10:152:10 | Load: x | test.c:152:10:152:10 | Load: x | != | 0 | 152 | 152 | | test.c:152:15:152:15 | Load: y | test.c:152:15:152:15 | Load: y | != | 0 | 152 | 152 | | test.c:175:13:175:32 | CompareEQ: ... == ... | test.c:175:13:175:15 | Call: call to foo | != | 0 | 175 | 175 | diff --git a/cpp/ql/test/library-tests/controlflow/guards/GuardsCompare.expected b/cpp/ql/test/library-tests/controlflow/guards/GuardsCompare.expected index a2f418b3d7bb..3d32ada5f301 100644 --- a/cpp/ql/test/library-tests/controlflow/guards/GuardsCompare.expected +++ b/cpp/ql/test/library-tests/controlflow/guards/GuardsCompare.expected @@ -161,11 +161,20 @@ | 137 | 0 == 0 when 0 is false | | 146 | ! ... != 0 when ! ... is true | | 146 | ! ... == 0 when ! ... is false | +| 146 | x != 0 when ! ... is false | +| 146 | x != 0 when x is true | +| 146 | x == 0 when x is false | | 152 | p != 0 when p is true | | 152 | p == 0 when p is false | | 158 | ! ... != 0 when ! ... is true | | 158 | ! ... == 0 when ! ... is false | +| 158 | p != 0 when ! ... is false | +| 158 | p != 0 when p is true | +| 158 | p == 0 when p is false | | 164 | s != 0 when s is true | | 164 | s == 0 when s is false | | 170 | ! ... != 0 when ! ... is true | | 170 | ! ... == 0 when ! ... is false | +| 170 | s != 0 when ! ... is false | +| 170 | s != 0 when s is true | +| 170 | s == 0 when s is false | diff --git a/cpp/ql/test/library-tests/controlflow/guards/GuardsEnsure.expected b/cpp/ql/test/library-tests/controlflow/guards/GuardsEnsure.expected index 45d63f6dd536..84c416445aef 100644 --- a/cpp/ql/test/library-tests/controlflow/guards/GuardsEnsure.expected +++ b/cpp/ql/test/library-tests/controlflow/guards/GuardsEnsure.expected @@ -245,10 +245,13 @@ unary | test.c:131:7:131:7 | b | test.c:131:7:131:7 | b | != | 0 | 131 | 132 | | test.c:137:7:137:7 | 0 | test.c:137:7:137:7 | 0 | == | 0 | 142 | 136 | | test.c:146:7:146:8 | ! ... | test.c:146:7:146:8 | ! ... | != | 0 | 146 | 147 | +| test.c:146:8:146:8 | x | test.c:146:8:146:8 | x | == | 0 | 146 | 147 | | test.c:152:8:152:8 | p | test.c:152:8:152:8 | p | != | 0 | 152 | 154 | | test.c:158:8:158:9 | ! ... | test.c:158:8:158:9 | ! ... | != | 0 | 158 | 160 | +| test.c:158:9:158:9 | p | test.c:158:9:158:9 | p | == | 0 | 158 | 160 | | test.c:164:8:164:8 | s | test.c:164:8:164:8 | s | != | 0 | 164 | 166 | | test.c:170:8:170:9 | ! ... | test.c:170:8:170:9 | ! ... | != | 0 | 170 | 172 | +| test.c:170:9:170:9 | s | test.c:170:9:170:9 | s | == | 0 | 170 | 172 | | test.cpp:18:8:18:10 | call to get | test.cpp:18:8:18:10 | call to get | != | 0 | 19 | 19 | | test.cpp:31:7:31:13 | ... == ... | test.cpp:31:7:31:7 | x | != | -1 | 30 | 30 | | test.cpp:31:7:31:13 | ... == ... | test.cpp:31:7:31:7 | x | != | -1 | 34 | 34 |