Skip to content

C++: Support < reasoning for switch statements in Guards library #15980

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 6 commits into from
Mar 20, 2024
+308 −41
Merged

C++: Support < reasoning for switch statements in Guards library #15980

Show file tree
Hide file tree
Changes from 5 commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
8b85735
C++: Generalize predicates from booleans to abstract values.
MathiasVP Mar 19, 2024
a78080c
C++: Implement less-than logic for guard conditions when comparing to…
MathiasVP Mar 19, 2024
1411ee5
C++: Extend tests to also test the new predicates and accept test cha…
MathiasVP Mar 19, 2024
88bfb81
C++: Add change note.
MathiasVP Mar 19, 2024
97aa301
C++: Accept more test changes.
MathiasVP Mar 19, 2024
3a7b80d
C++: Respond to review comments.
MathiasVP Mar 20, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 5 additions & 0 deletions cpp/ql/lib/change-notes/2024-03-19-predicates-for-switches-as-guards-2.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
---
category: feature
---
* Added a predicate `GuardCondition.comparesLt/4` to query whether an expression is compared to a constant.
* Added a predicate `GuardCondition.ensuresLt/4` to query whether a basic block is guarded by an expression being less than a constant.
230 changes: 199 additions & 31 deletions cpp/ql/lib/semmle/code/cpp/controlflow/IRGuards.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -125,6 +125,20 @@ class GuardCondition extends Expr {
cached
predicate ensuresLt(Expr left, Expr right, int k, BasicBlock block, boolean isLessThan) { none() }

/**
* Holds if (determined by this guard) `e < k` evaluates to `isLessThan` if
* this expression evaluates to `value`.
*/
cached
predicate comparesLt(Expr e, int k, boolean isLessThan, AbstractValue value) { none() }

/**
* Holds if (determined by this guard) `e < k` must be `isLessThan` in `block`.
* If `isLessThan = false` then this implies `left >= k`.
*/
cached
predicate ensuresLt(Expr e, int k, BasicBlock block, boolean isLessThan) { none() }

/** Holds if (determined by this guard) `left == right + k` evaluates to `areEqual` if this expression evaluates to `testIsTrue`. */
cached
predicate comparesEq(Expr left, Expr right, int k, boolean areEqual, boolean testIsTrue) {
Expand Down Expand Up @@ -176,12 +190,27 @@ private class GuardConditionFromBinaryLogicalOperator extends GuardCondition {
)
}

override predicate comparesLt(Expr e, int k, boolean isLessThan, AbstractValue value) {
exists(BooleanValue partValue, GuardCondition part |
this.(BinaryLogicalOperation)
.impliesValue(part, partValue.getValue(), value.(BooleanValue).getValue())
|
part.comparesLt(e, k, isLessThan, partValue)
)
}

override predicate ensuresLt(Expr left, Expr right, int k, BasicBlock block, boolean isLessThan) {
exists(boolean testIsTrue |
this.comparesLt(left, right, k, isLessThan, testIsTrue) and this.controls(block, testIsTrue)
)
}

override predicate ensuresLt(Expr e, int k, BasicBlock block, boolean isLessThan) {
exists(AbstractValue value |
this.comparesLt(e, k, isLessThan, value) and this.valueControls(block, value)
)
}

override predicate comparesEq(Expr left, Expr right, int k, boolean areEqual, boolean testIsTrue) {
exists(boolean partIsTrue, GuardCondition part |
this.(BinaryLogicalOperation).impliesValue(part, partIsTrue, testIsTrue)
Expand Down Expand Up @@ -236,6 +265,17 @@ private class GuardConditionFromIR extends GuardCondition {
)
}

/**
* Holds if (determined by this guard) `e < k` evaluates to `isLessThan` if
* this expression evaluates to `value`.
*/
override predicate comparesLt(Expr e, int k, boolean isLessThan, AbstractValue value) {
exists(Instruction i |
i.getUnconvertedResultExpression() = e and
ir.comparesLt(i.getAUse(), k, isLessThan, value)
)
}

/**
* Holds if (determined by this guard) `left < right + k` must be `isLessThan` in `block`.
* If `isLessThan = false` then this implies `left >= right + k`.
Expand All @@ -249,6 +289,18 @@ private class GuardConditionFromIR extends GuardCondition {
)
}

/**
* Holds if (determined by this guard) `e < k` must be `isLessThan` in `block`.
* If `isLessThan = false` then this implies `e >= k`.
*/
override predicate ensuresLt(Expr e, int k, BasicBlock block, boolean isLessThan) {
exists(Instruction i, AbstractValue value |
i.getUnconvertedResultExpression() = e and
ir.comparesLt(i.getAUse(), k, isLessThan, value) and
this.valueControls(block, value)
)
}

/** Holds if (determined by this guard) `left == right + k` evaluates to `areEqual` if this expression evaluates to `testIsTrue`. */
override predicate comparesEq(Expr left, Expr right, int k, boolean areEqual, boolean testIsTrue) {
exists(Instruction li, Instruction ri |
Expand Down Expand Up @@ -456,7 +508,19 @@ class IRGuardCondition extends Instruction {
/** Holds if (determined by this guard) `left < right + k` evaluates to `isLessThan` if this expression evaluates to `testIsTrue`. */
cached
predicate comparesLt(Operand left, Operand right, int k, boolean isLessThan, boolean testIsTrue) {
compares_lt(this, left, right, k, isLessThan, testIsTrue)
exists(BooleanValue value |
compares_lt(this, left, right, k, isLessThan, value) and
value.getValue() = testIsTrue
)
}

/**
* Holds if (determined by this guard) `op < k` evaluates to `isLessThan` if
* this expression evaluates to `value`.
*/
cached
predicate comparesLt(Operand op, int k, boolean isLessThan, AbstractValue value) {
compares_lt(this, op, k, isLessThan, value)
}

/**
Expand All @@ -465,8 +529,19 @@ class IRGuardCondition extends Instruction {
*/
cached
predicate ensuresLt(Operand left, Operand right, int k, IRBlock block, boolean isLessThan) {
exists(boolean testIsTrue |
compares_lt(this, left, right, k, isLessThan, testIsTrue) and this.controls(block, testIsTrue)
exists(AbstractValue value |
compares_lt(this, left, right, k, isLessThan, value) and this.valueControls(block, value)
)
}

/**
* Holds if (determined by this guard) `op < k` must be `isLessThan` in `block`.
* If `isLessThan = false` then this implies `op >= k`.
*/
cached
predicate ensuresLt(Operand op, int k, IRBlock block, boolean isLessThan) {
exists(AbstractValue value |
compares_lt(this, op, k, isLessThan, value) and this.valueControls(block, value)
)
}

Expand All @@ -478,9 +553,21 @@ class IRGuardCondition extends Instruction {
predicate ensuresLtEdge(
Operand left, Operand right, int k, IRBlock pred, IRBlock succ, boolean isLessThan
) {
exists(boolean testIsTrue |
compares_lt(this, left, right, k, isLessThan, testIsTrue) and
this.controlsEdge(pred, succ, testIsTrue)
exists(AbstractValue value |
compares_lt(this, left, right, k, isLessThan, value) and
this.valueControlsEdge(pred, succ, value)
)
}

/**
* Holds if (determined by this guard) `op < k` must be `isLessThan` on the edge from
* `pred` to `succ`. If `isLessThan = false` then this implies `op >= k`.
*/
cached
predicate ensuresLtEdge(Operand left, int k, IRBlock pred, IRBlock succ, boolean isLessThan) {
exists(AbstractValue value |
compares_lt(this, left, k, isLessThan, value) and
this.valueControlsEdge(pred, succ, value)
)
}

Expand Down Expand Up @@ -746,31 +833,46 @@ 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, boolean testIsTrue
Instruction 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 isLt = true and testIsTrue = true
simple_comparison_lt(test, left, right, k) and
value.(BooleanValue).getValue() = isLt
or
simple_comparison_lt(test, left, right, k) and isLt = false and testIsTrue = false
or
complex_lt(test, left, right, k, isLt, testIsTrue)
complex_lt(test, left, right, k, isLt, value)
or
/* (not (left < right + k)) => (left >= right + k) */
exists(boolean isGe | isLt = isGe.booleanNot() |
compares_ge(test, left, right, k, isGe, testIsTrue)
)
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(boolean isFalse | testIsTrue = isFalse.booleanNot() |
compares_lt(test.(LogicalNotInstruction).getUnary(), left, right, k, isLt, isFalse)
exists(AbstractValue dual | value = dual.getDualValue() |
compares_lt(test.(LogicalNotInstruction).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) {
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)
)
or
exists(int k1, int k2, ConstantInstruction const |
compares_lt(test, op, const.getAUse(), k2, isLt, value) and
int_value(const) = k1 and
k = k1 + k2
)
}

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

/** Rearrange various simple comparisons into `left < right + k` form. */
Expand All @@ -796,55 +898,99 @@ private predicate simple_comparison_lt(CompareInstruction cmp, Operand left, Ope
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
) {
exists(SwitchInstruction switch, CaseEdge case |
test = switch.getExpression() and
op.getDef() = test and
case = value.(MatchValue).getCase() and
exists(switch.getSuccessor(case)) and
case.getMaxValue() > case.getMinValue()
|
// op <= k => op < k - 1
isLt = true and
case.getMaxValue().toInt() = k - 1
or
isLt = false and
case.getMinValue().toInt() = k
)
}

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

private predicate complex_lt(
Instruction test, Operand left, int k, boolean isLt, AbstractValue value
) {
sub_lt(test, left, k, isLt, value)
or
add_lt(test, left, k, isLt, value)
}

// 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, boolean testIsTrue
CompareInstruction 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, testIsTrue) and
compares_lt(cmp, lhs.getAUse(), right, c, isLt, value) and
left = lhs.getLeftOperand() and
x = int_value(lhs.getRight()) and
k = c + x
)
or
exists(SubInstruction rhs, int c, int x |
compares_lt(cmp, left, rhs.getAUse(), c, isLt, testIsTrue) and
compares_lt(cmp, left, rhs.getAUse(), c, isLt, value) and
right = rhs.getLeftOperand() and
x = int_value(rhs.getRight()) and
k = c - x
)
or
exists(PointerSubInstruction lhs, int c, int x |
compares_lt(cmp, lhs.getAUse(), right, c, isLt, testIsTrue) and
compares_lt(cmp, lhs.getAUse(), right, c, isLt, value) and
left = lhs.getLeftOperand() and
x = int_value(lhs.getRight()) and
k = c + x
)
or
exists(PointerSubInstruction rhs, int c, int x |
compares_lt(cmp, left, rhs.getAUse(), c, isLt, testIsTrue) and
compares_lt(cmp, left, rhs.getAUse(), c, isLt, value) and
right = rhs.getLeftOperand() and
x = int_value(rhs.getRight()) and
k = c - x
)
}

private predicate sub_lt(Instruction 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
x = int_value(lhs.getRight()) and
k = c + x
)
or
exists(PointerSubInstruction lhs, int c, int x |
compares_lt(test, lhs.getAUse(), c, isLt, value) and
left = lhs.getLeftOperand() and
x = int_value(lhs.getRight()) and
k = c + x
)
}

// 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, boolean testIsTrue
CompareInstruction 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, testIsTrue) and
compares_lt(cmp, lhs.getAUse(), right, c, isLt, value) and
(
left = lhs.getLeftOperand() and x = int_value(lhs.getRight())
or
Expand All @@ -854,7 +1000,7 @@ private predicate add_lt(
)
or
exists(AddInstruction rhs, int c, int x |
compares_lt(cmp, left, rhs.getAUse(), c, isLt, testIsTrue) and
compares_lt(cmp, left, rhs.getAUse(), c, isLt, value) and
(
right = rhs.getLeftOperand() and x = int_value(rhs.getRight())
or
Expand All @@ -864,7 +1010,7 @@ private predicate add_lt(
)
or
exists(PointerAddInstruction lhs, int c, int x |
compares_lt(cmp, lhs.getAUse(), right, c, isLt, testIsTrue) and
compares_lt(cmp, lhs.getAUse(), right, c, isLt, value) and
(
left = lhs.getLeftOperand() and x = int_value(lhs.getRight())
or
Expand All @@ -874,7 +1020,7 @@ private predicate add_lt(
)
or
exists(PointerAddInstruction rhs, int c, int x |
compares_lt(cmp, left, rhs.getAUse(), c, isLt, testIsTrue) and
compares_lt(cmp, left, rhs.getAUse(), c, isLt, value) and
(
right = rhs.getLeftOperand() and x = int_value(rhs.getRight())
or
Expand All @@ -884,6 +1030,28 @@ private predicate add_lt(
)
}

private predicate add_lt(Instruction 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
(
left = lhs.getLeftOperand() and x = int_value(lhs.getRight())
or
left = lhs.getRightOperand() and x = int_value(lhs.getLeft())
) and
k = c - x
)
or
exists(PointerAddInstruction lhs, int c, int x |
compares_lt(test, lhs.getAUse(), c, isLt, value) and
(
left = lhs.getLeftOperand() and x = int_value(lhs.getRight())
or
left = lhs.getRightOperand() and x = int_value(lhs.getLeft())
) and
k = c - x
)
}

// left - x == right + c => left == right + (c+x)
// left == (right - x) + c => left == right + (c-x)
private predicate sub_eq(
Expand Down
Loading