Skip to content
Closed
169 changes: 126 additions & 43 deletions cpp/ql/lib/semmle/code/cpp/controlflow/IRGuards.qll
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@

import cpp
import semmle.code.cpp.ir.IR
private import semmle.code.cpp.ir.ValueNumbering
private import semmle.code.cpp.ir.implementation.raw.internal.TranslatedExpr
private import semmle.code.cpp.ir.implementation.raw.internal.InstructionTag

Expand Down Expand Up @@ -58,6 +59,78 @@ class MatchValue extends AbstractValue, TMatchValue {
override string toString() { result = this.getCase().toString() }
}

/**
* A value number such that at least one of the instructions is
* a `CompareInstruction`.
*/
private class CompareValueNumber extends ValueNumber {
CompareInstruction cmp;

CompareValueNumber() { cmp = this.getAnInstruction() }

/** Gets an `CompareInstruction` belonging to this value number. */
CompareInstruction getCompareInstruction() { result = cmp }

/**
* Gets a left operand of a `CompareInstruction` that belongs to this
* value number
*/
Operand getLeftOperand() { result = cmp.getLeftOperand() }

/**
* Gets a right operand of a `CompareInstruction` that belongs to this
* value number
*/
Operand getRightOperand() { result = cmp.getRightOperand() }
}

private class CompareEQValueNumber extends CompareValueNumber {
override CompareEQInstruction cmp;
}

private class CompareNEValueNumber extends CompareValueNumber {
override CompareNEInstruction cmp;
}

private class CompareLTValueNumber extends CompareValueNumber {
override CompareLTInstruction cmp;
}

private class CompareGTValueNumber extends CompareValueNumber {
override CompareGTInstruction cmp;
}

private class CompareLEValueNumber extends CompareValueNumber {
override CompareLEInstruction cmp;
}

private class CompareGEValueNumber extends CompareValueNumber {
override CompareGEInstruction cmp;
}

/**
* A value number such that at least one of the instructions is an
* insruction that is used in a `SwitchInstruction`'s expression.
*/
private class ScrutineeValueNumber extends ValueNumber {
SwitchInstruction switch;
Instruction scrutinee;

ScrutineeValueNumber() {
switch.getExpression() = scrutinee and
this.getAnInstruction() = scrutinee
}

/**
* Gets a `SwitchInstruction` that branches based on the value
* of this value number's value.
*/
SwitchInstruction getSwitchInstruction() { result = switch }

/** Gets an expression that belongs to this value number. */
SwitchInstruction getExpressionInstruction() { result = scrutinee }
}

/**
* A Boolean condition in the AST that guards one or more basic blocks. This includes
* operands of logical operators but not switch statements.
Expand Down Expand Up @@ -714,7 +787,7 @@ private Instruction getBranchForCondition(Instruction guard) {
* Beware making mistaken logical implications here relating `areEqual` and `testIsTrue`.
*/
private predicate compares_eq(
Instruction test, Operand left, Operand right, int k, boolean areEqual, AbstractValue value
ValueNumber test, Operand left, Operand right, 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, left, right, k, v) |
Expand All @@ -732,14 +805,16 @@ private predicate compares_eq(
complex_eq(test, left, right, k, areEqual, value)
or
/* (x is true => (left == right + k)) => (!x is false => (left == right + k)) */
exists(AbstractValue dual | value = dual.getDualValue() |
compares_eq(test.(LogicalNotInstruction).getUnary(), left, right, k, areEqual, dual)
exists(AbstractValue dual, LogicalNotInstruction logicalNot |
value = dual.getDualValue() and
logicalNot = test.getAnInstruction() and
compares_eq(valueNumber(logicalNot.getUnary()), left, right, k, areEqual, dual)
)
}

/** Holds if `op == k` is `areEqual` given that `test` is equal to `value`. */
private predicate compares_eq(
Instruction test, Operand op, int k, boolean areEqual, AbstractValue value
ValueNumber 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) |
Expand All @@ -751,8 +826,10 @@ private predicate compares_eq(
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)
exists(AbstractValue dual, LogicalNotInstruction logicalNot |
value = dual.getDualValue() and
logicalNot = test.getAnInstruction() and
compares_eq(valueNumber(logicalNot.getUnary()), op, k, areEqual, dual)
)
or
// ((test is `areEqual` => op == const + k2) and const == `k1`) =>
Expand All @@ -766,42 +843,44 @@ private predicate compares_eq(

/** Rearrange various simple comparisons into `left == right + k` form. */
private predicate simple_comparison_eq(
CompareInstruction cmp, Operand left, Operand right, int k, AbstractValue value
CompareValueNumber cmp, Operand left, Operand right, int k, AbstractValue value
) {
left = cmp.getLeftOperand() and
cmp instanceof CompareEQInstruction and
cmp instanceof CompareEQValueNumber and
right = cmp.getRightOperand() and
k = 0 and
value.(BooleanValue).getValue() = true
or
left = cmp.getLeftOperand() and
cmp instanceof CompareNEInstruction and
cmp instanceof CompareNEValueNumber and
right = cmp.getRightOperand() and
k = 0 and
value.(BooleanValue).getValue() = false
}

/** Rearrange various simple comparisons into `op == k` form. */
private predicate simple_comparison_eq(Instruction test, Operand op, int k, AbstractValue value) {
exists(SwitchInstruction switch, CaseEdge case |
test = switch.getExpression() and
op.getDef() = test and
private predicate simple_comparison_eq(
ScrutineeValueNumber test, Operand op, int k, AbstractValue value
) {
exists(CaseEdge case, Instruction expression |
expression = test.getExpressionInstruction() and
op.getDef() = expression and
case = value.(MatchValue).getCase() and
exists(switch.getSuccessor(case)) and
exists(test.getSwitchInstruction().getSuccessor(case)) and
case.getValue().toInt() = k
)
}

private predicate complex_eq(
CompareInstruction cmp, Operand left, Operand right, int k, boolean areEqual, AbstractValue value
ValueNumber cmp, Operand left, Operand right, int k, boolean areEqual, AbstractValue value
Copy link
Contributor

@jketema jketema Mar 21, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is there a reason for not using the newly introduced CompareValueNumber here? And also in some other places in the commit that introduces this.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It actually does matter because of the LogicalNotInstruction case:

exists(AbstractValue dual, LogicalNotInstruction logicalNot |
  value = dual.getDualValue() and
  logicalNot = test.getAnInstruction() and
  compares_eq(valueNumber(logicalNot.getUnary()), left, right, k, areEqual, dual)
)

here we don't require the value number to be a CompareValueNumber, but instead we require it to be something of the form !x, where the x is then used recursively.

I'll see if I can come up with a testcase where this is important 🤔

) {
sub_eq(cmp, left, right, k, areEqual, value)
or
add_eq(cmp, left, right, k, areEqual, value)
}

private predicate complex_eq(
Instruction test, Operand op, int k, boolean areEqual, AbstractValue value
ValueNumber test, Operand op, int k, boolean areEqual, AbstractValue value
) {
sub_eq(test, op, k, areEqual, value)
or
Expand All @@ -815,7 +894,7 @@ private predicate complex_eq(

/** Holds if `left < right + k` evaluates to `isLt` given that test is `testIsTrue`. */
private predicate compares_lt(
Instruction test, Operand left, Operand right, int k, boolean isLt, AbstractValue value
ValueNumber test, Operand left, Operand right, int k, boolean isLt, AbstractValue value
) {
/* In the simple case, the test is the comparison, so isLt = testIsTrue */
simple_comparison_lt(test, left, right, k) and
Expand All @@ -827,20 +906,24 @@ private predicate compares_lt(
exists(boolean isGe | isLt = isGe.booleanNot() | compares_ge(test, left, right, k, isGe, value))
or
/* (x is true => (left < right + k)) => (!x is false => (left < right + k)) */
exists(AbstractValue dual | value = dual.getDualValue() |
compares_lt(test.(LogicalNotInstruction).getUnary(), left, right, k, isLt, dual)
exists(AbstractValue dual, LogicalNotInstruction logicalNot |
value = dual.getDualValue() and
logicalNot = test.getAnInstruction() and
compares_lt(valueNumber(logicalNot.getUnary()), left, right, k, isLt, dual)
)
}

/** Holds if `op < k` evaluates to `isLt` given that `test` evaluates to `value`. */
private predicate compares_lt(Instruction test, Operand op, int k, boolean isLt, AbstractValue value) {
private predicate compares_lt(ValueNumber test, Operand op, int k, boolean isLt, AbstractValue value) {
simple_comparison_lt(test, op, k, isLt, value)
or
complex_lt(test, op, k, isLt, value)
or
/* (x is true => (op < k)) => (!x is false => (op < k)) */
exists(AbstractValue dual | value = dual.getDualValue() |
compares_lt(test.(LogicalNotInstruction).getUnary(), op, k, isLt, dual)
exists(AbstractValue dual, LogicalNotInstruction logicalNot |
value = dual.getDualValue() and
logicalNot = test.getAnInstruction() and
compares_lt(valueNumber(logicalNot.getUnary()), op, k, isLt, dual)
)
or
exists(int k1, int k2, ConstantInstruction const |
Expand All @@ -852,43 +935,43 @@ private predicate compares_lt(Instruction test, Operand op, int k, boolean isLt,

/** `(a < b + k) => (b > a - k) => (b >= a + (1-k))` */
private predicate compares_ge(
Instruction test, Operand left, Operand right, int k, boolean isGe, AbstractValue value
ValueNumber test, Operand left, Operand right, int k, boolean isGe, AbstractValue value
) {
exists(int onemk | k = 1 - onemk | compares_lt(test, right, left, onemk, isGe, value))
}

/** Rearrange various simple comparisons into `left < right + k` form. */
private predicate simple_comparison_lt(CompareInstruction cmp, Operand left, Operand right, int k) {
private predicate simple_comparison_lt(CompareValueNumber cmp, Operand left, Operand right, int k) {
left = cmp.getLeftOperand() and
cmp instanceof CompareLTInstruction and
cmp instanceof CompareLTValueNumber and
right = cmp.getRightOperand() and
k = 0
or
left = cmp.getLeftOperand() and
cmp instanceof CompareLEInstruction and
cmp instanceof CompareLEValueNumber and
right = cmp.getRightOperand() and
k = 1
or
right = cmp.getLeftOperand() and
cmp instanceof CompareGTInstruction and
cmp instanceof CompareGTValueNumber and
left = cmp.getRightOperand() and
k = 0
or
right = cmp.getLeftOperand() and
cmp instanceof CompareGEInstruction and
cmp instanceof CompareGEValueNumber and
left = cmp.getRightOperand() and
k = 1
}

/** Rearrange various simple comparisons into `op < k` form. */
private predicate simple_comparison_lt(
Instruction test, Operand op, int k, boolean isLt, AbstractValue value
ScrutineeValueNumber test, Operand op, int k, boolean isLt, AbstractValue value
) {
exists(SwitchInstruction switch, CaseEdge case |
test = switch.getExpression() and
op.getDef() = test and
exists(CaseEdge case, Instruction expression |
expression = test.getExpressionInstruction() and
op.getDef() = expression and
case = value.(MatchValue).getCase() and
exists(switch.getSuccessor(case)) and
exists(test.getSwitchInstruction().getSuccessor(case)) and
case.getMaxValue() > case.getMinValue()
|
// op <= k => op < k - 1
Expand All @@ -901,15 +984,15 @@ private predicate simple_comparison_lt(
}

private predicate complex_lt(
CompareInstruction cmp, Operand left, Operand right, int k, boolean isLt, AbstractValue value
ValueNumber cmp, Operand left, Operand right, int k, boolean isLt, AbstractValue value
) {
sub_lt(cmp, left, right, k, isLt, value)
or
add_lt(cmp, left, right, k, isLt, value)
}

private predicate complex_lt(
Instruction test, Operand left, int k, boolean isLt, AbstractValue value
ValueNumber test, Operand left, int k, boolean isLt, AbstractValue value
) {
sub_lt(test, left, k, isLt, value)
or
Expand All @@ -919,7 +1002,7 @@ private predicate complex_lt(
// left - x < right + c => left < right + (c+x)
// left < (right - x) + c => left < right + (c-x)
private predicate sub_lt(
CompareInstruction cmp, Operand left, Operand right, int k, boolean isLt, AbstractValue value
ValueNumber cmp, Operand left, Operand right, int k, boolean isLt, AbstractValue value
) {
exists(SubInstruction lhs, int c, int x |
compares_lt(cmp, lhs.getAUse(), right, c, isLt, value) and
Expand Down Expand Up @@ -950,7 +1033,7 @@ private predicate sub_lt(
)
}

private predicate sub_lt(Instruction test, Operand left, int k, boolean isLt, AbstractValue value) {
private predicate sub_lt(ValueNumber test, Operand left, int k, boolean isLt, AbstractValue value) {
exists(SubInstruction lhs, int c, int x |
compares_lt(test, lhs.getAUse(), c, isLt, value) and
left = lhs.getLeftOperand() and
Expand All @@ -969,7 +1052,7 @@ private predicate sub_lt(Instruction test, Operand left, int k, boolean isLt, Ab
// left + x < right + c => left < right + (c-x)
// left < (right + x) + c => left < right + (c+x)
private predicate add_lt(
CompareInstruction cmp, Operand left, Operand right, int k, boolean isLt, AbstractValue value
ValueNumber cmp, Operand left, Operand right, int k, boolean isLt, AbstractValue value
) {
exists(AddInstruction lhs, int c, int x |
compares_lt(cmp, lhs.getAUse(), right, c, isLt, value) and
Expand Down Expand Up @@ -1012,7 +1095,7 @@ private predicate add_lt(
)
}

private predicate add_lt(Instruction test, Operand left, int k, boolean isLt, AbstractValue value) {
private predicate add_lt(ValueNumber test, Operand left, int k, boolean isLt, AbstractValue value) {
exists(AddInstruction lhs, int c, int x |
compares_lt(test, lhs.getAUse(), c, isLt, value) and
(
Expand All @@ -1037,7 +1120,7 @@ private predicate add_lt(Instruction test, Operand left, int k, boolean isLt, Ab
// left - x == right + c => left == right + (c+x)
// left == (right - x) + c => left == right + (c-x)
private predicate sub_eq(
CompareInstruction cmp, Operand left, Operand right, int k, boolean areEqual, AbstractValue value
ValueNumber cmp, Operand left, Operand right, int k, boolean areEqual, AbstractValue value
) {
exists(SubInstruction lhs, int c, int x |
compares_eq(cmp, lhs.getAUse(), right, c, areEqual, value) and
Expand Down Expand Up @@ -1069,7 +1152,7 @@ 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 sub_eq(ValueNumber 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
op = sub.getLeftOperand() and
Expand All @@ -1088,7 +1171,7 @@ private predicate sub_eq(Instruction test, Operand op, int k, boolean areEqual,
// left + x == right + c => left == right + (c-x)
// left == (right + x) + c => left == right + (c+x)
private predicate add_eq(
CompareInstruction cmp, Operand left, Operand right, int k, boolean areEqual, AbstractValue value
ValueNumber cmp, Operand left, Operand right, int k, boolean areEqual, AbstractValue value
) {
exists(AddInstruction lhs, int c, int x |
compares_eq(cmp, lhs.getAUse(), right, c, areEqual, value) and
Expand Down Expand Up @@ -1133,7 +1216,7 @@ 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
ValueNumber 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
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,9 @@ edges
| test.cpp:420:19:420:20 | scanf output argument | test.cpp:423:7:423:7 | i | provenance | |
| test.cpp:455:41:455:46 | sscanf output argument | test.cpp:460:6:460:10 | value | provenance | |
| test.cpp:467:20:467:25 | scanf output argument | test.cpp:474:6:474:10 | value | provenance | |
| test.cpp:479:30:479:31 | scanf output argument | test.cpp:481:9:481:9 | i | provenance | |
| test.cpp:487:35:487:36 | scanf output argument | test.cpp:489:9:489:9 | i | provenance | |
| test.cpp:495:30:495:31 | scanf output argument | test.cpp:497:9:497:9 | i | provenance | |
nodes
| test.cpp:34:15:34:16 | scanf output argument | semmle.label | scanf output argument |
| test.cpp:35:7:35:7 | i | semmle.label | i |
Expand Down Expand Up @@ -114,6 +117,12 @@ nodes
| test.cpp:460:6:460:10 | value | semmle.label | value |
| test.cpp:467:20:467:25 | scanf output argument | semmle.label | scanf output argument |
| test.cpp:474:6:474:10 | value | semmle.label | value |
| test.cpp:479:30:479:31 | scanf output argument | semmle.label | scanf output argument |
| test.cpp:481:9:481:9 | i | semmle.label | i |
| test.cpp:487:35:487:36 | scanf output argument | semmle.label | scanf output argument |
| test.cpp:489:9:489:9 | i | semmle.label | i |
| test.cpp:495:30:495:31 | scanf output argument | semmle.label | scanf output argument |
| test.cpp:497:9:497:9 | i | semmle.label | i |
subpaths
#select
| test.cpp:35:7:35:7 | i | test.cpp:34:15:34:16 | scanf output argument | test.cpp:35:7:35:7 | 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:34:3:34:7 | call to scanf | call to scanf |
Expand All @@ -134,3 +143,6 @@ subpaths
| test.cpp:423:7:423:7 | i | test.cpp:420:19:420:20 | scanf output argument | test.cpp:423:7:423:7 | 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:420:7:420:11 | call to scanf | call to scanf |
| test.cpp:460:6:460:10 | value | test.cpp:455:41:455:46 | sscanf output argument | test.cpp:460:6:460:10 | value | 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:455:12:455:17 | call to sscanf | call to sscanf |
| test.cpp:474:6:474:10 | value | test.cpp:467:20:467:25 | scanf output argument | test.cpp:474:6:474:10 | value | 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:467:8:467:12 | call to scanf | call to scanf |
| test.cpp:481:9:481:9 | i | test.cpp:479:30:479:31 | scanf output argument | test.cpp:481:9:481: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:479:18:479:22 | call to scanf | call to scanf |
| test.cpp:489:9:489:9 | i | test.cpp:487:35:487:36 | scanf output argument | test.cpp:489:9:489: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:487:23:487:27 | call to scanf | call to scanf |
| test.cpp:497:9:497:9 | i | test.cpp:495:30:495:31 | scanf output argument | test.cpp:497:9:497: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:495:18:495:22 | call to scanf | call to scanf |
Loading