Skip to content

Commit

Permalink
C++: Remove the 'inNonZeroCase' column.
Browse files Browse the repository at this point in the history
  • Loading branch information
@MathiasVP
MathiasVP committed Nov 20, 2024
1 parent dc46d45 commit 9787712
Show file tree
Hide file tree
Showing 4 changed files with 519 additions and 72 deletions.
97 changes: 25 additions & 72 deletions cpp/ql/lib/semmle/code/cpp/controlflow/IRGuards.qll
View file
Original file line number Diff line number Diff line change
Expand Up @@ -681,7 +681,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(valueNumber(this), op, k, areEqual, false, value)
unary_compares_eq(valueNumber(this), op, k, areEqual, value)
}

/**
Expand All @@ -703,7 +703,7 @@ class IRGuardCondition extends Instruction {
cached
predicate ensuresEq(Operand op, int k, IRBlock block, boolean areEqual) {
exists(AbstractValue value |
unary_compares_eq(valueNumber(this), op, k, areEqual, false, value) and
unary_compares_eq(valueNumber(this), op, k, areEqual, value) and
this.valueControls(block, value)
)
}
Expand All @@ -729,7 +729,7 @@ class IRGuardCondition extends Instruction {
cached
predicate ensuresEqEdge(Operand op, int k, IRBlock pred, IRBlock succ, boolean areEqual) {
exists(AbstractValue value |
unary_compares_eq(valueNumber(this), op, k, areEqual, false, value) and
unary_compares_eq(valueNumber(this), op, k, areEqual, value) and
this.valueControlsEdge(pred, succ, value)
)
}
Expand Down Expand Up @@ -866,72 +866,34 @@ private predicate compares_eq(

/**
* 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<int>::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(
ValueNumber test, Operand op, int k, boolean areEqual, boolean inNonZeroCase, 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 | unary_simple_comparison_eq(test, op, k, inNonZeroCase, 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
unary_complex_eq(test, op, k, areEqual, inNonZeroCase, value)
unary_complex_eq(test, op, k, areEqual, value)
or
/* (x is true => (op == k)) => (!x is false => (op == k)) */
exists(AbstractValue dual, boolean inNonZeroCase0 |
exists(AbstractValue dual |
value = dual.getDualValue() and
unary_compares_eq(test.(LogicalNotValueNumber).getUnary(), op, k, inNonZeroCase0, areEqual, dual)
|
k = 0 and inNonZeroCase = inNonZeroCase0
or
k != 0 and inNonZeroCase = true
unary_compares_eq(test.(LogicalNotValueNumber).getUnary(), op, k, areEqual, dual)
)
or
// ((test is `areEqual` => op == const + k2) and const == `k1`) =>
// test is `areEqual` => op == k1 + k2
inNonZeroCase = false and
exists(int k1, int k2, Instruction const |
compares_eq(test, op, const.getAUse(), k2, areEqual, value) and
int_value(const) = k1 and
k = k1 + k2
)
or
unary_compares_eq(test.(BuiltinExpectCallValueNumber).getCondition(), op, k, areEqual,
inNonZeroCase, value)
unary_compares_eq(test.(BuiltinExpectCallValueNumber).getCondition(), op, k, areEqual, value)
}

/** Rearrange various simple comparisons into `left == right + k` form. */
Expand Down Expand Up @@ -1000,27 +962,24 @@ private predicate isRelevantUnaryComparisonOperand(Operand op) {

/** Rearrange various simple comparisons into `op == k` form. */
private predicate unary_simple_comparison_eq(
ValueNumber test, Operand op, int k, boolean inNonZeroCase, AbstractValue value
ValueNumber test, Operand op, int k, AbstractValue value
) {
exists(CaseEdge case, SwitchConditionValueNumber condition |
condition = test and
op = condition.getExpressionOperand() and
case = value.(MatchValue).getCase() and
exists(condition.getSuccessor(case)) and
case.getValue().toInt() = k and
inNonZeroCase = false
case.getValue().toInt() = k
)
or
isRelevantUnaryComparisonOperand(op) and
op.getDef() = test.getAnInstruction() and
(
k = 1 and
value.(BooleanValue).getValue() = true and
inNonZeroCase = true
value.(BooleanValue).getValue() = true
or
k = 0 and
value.(BooleanValue).getValue() = false and
inNonZeroCase = false
value.(BooleanValue).getValue() = false
)
}

Expand Down Expand Up @@ -1074,13 +1033,12 @@ private predicate complex_eq(
* an instruction that compares the value of `__builtin_expect(op == k, _)` to `0`.
*/
private predicate unary_builtin_expect_eq(
CompareValueNumber cmp, Operand op, int k, boolean areEqual, boolean inNonZeroCase,
AbstractValue value
CompareValueNumber cmp, Operand op, int k, boolean areEqual, AbstractValue value
) {
exists(BuiltinExpectCallValueNumber call, Instruction const, AbstractValue innerValue |
int_value(const) = 0 and
cmp.hasOperands(call.getAUse(), const.getAUse()) and
unary_compares_eq(call.getCondition(), op, k, areEqual, inNonZeroCase, innerValue)
unary_compares_eq(call.getCondition(), op, k, areEqual, innerValue)
|
cmp instanceof CompareNEValueNumber and
value = innerValue
Expand All @@ -1091,13 +1049,13 @@ private predicate unary_builtin_expect_eq(
}

private predicate unary_complex_eq(
ValueNumber test, Operand op, int k, boolean areEqual, boolean inNonZeroCase, AbstractValue value
ValueNumber test, Operand op, int k, boolean areEqual, AbstractValue value
) {
unary_sub_eq(test, op, k, areEqual, inNonZeroCase, value)
unary_sub_eq(test, op, k, areEqual, value)
or
unary_add_eq(test, op, k, areEqual, inNonZeroCase, value)
unary_add_eq(test, op, k, areEqual, value)
or
unary_builtin_expect_eq(test, op, k, areEqual, inNonZeroCase, value)
unary_builtin_expect_eq(test, op, k, areEqual, value)
}

/*
Expand Down Expand Up @@ -1357,19 +1315,17 @@ private predicate sub_eq(

// op - x == c => op == (c+x)
private predicate unary_sub_eq(
ValueNumber test, Operand op, int k, boolean areEqual, boolean inNonZeroCase, AbstractValue value
ValueNumber test, Operand op, int k, boolean areEqual, AbstractValue value
) {
inNonZeroCase = false and
exists(SubInstruction sub, int c, int x |
unary_compares_eq(test, sub.getAUse(), c, areEqual, inNonZeroCase, 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
inNonZeroCase = false and
exists(PointerSubInstruction sub, int c, int x |
unary_compares_eq(test, sub.getAUse(), c, areEqual, inNonZeroCase, 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
Expand Down Expand Up @@ -1424,12 +1380,10 @@ private predicate add_eq(

// left + x == right + c => left == right + (c-x)
private predicate unary_add_eq(
ValueNumber test, Operand left, int k, boolean areEqual, boolean inNonZeroCase,
AbstractValue value
ValueNumber test, Operand left, int k, boolean areEqual, AbstractValue value
) {
inNonZeroCase = false and
exists(AddInstruction lhs, int c, int x |
unary_compares_eq(test, lhs.getAUse(), c, areEqual, inNonZeroCase, value) and
unary_compares_eq(test, lhs.getAUse(), c, areEqual, value) and
(
left = lhs.getLeftOperand() and x = int_value(lhs.getRight())
or
Expand All @@ -1438,9 +1392,8 @@ 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, inNonZeroCase, value) and
unary_compares_eq(test, lhs.getAUse(), c, areEqual, value) and
(
left = lhs.getLeftOperand() and x = int_value(lhs.getRight())
or
Expand Down
Loading

0 comments on commit 9787712

Please sign in to comment.