diff --git a/cpp/ql/lib/change-notes/2024-12-04-guard-conditions.md b/cpp/ql/lib/change-notes/2024-12-04-guard-conditions.md new file mode 100644 index 000000000000..f60a6a2970a6 --- /dev/null +++ b/cpp/ql/lib/change-notes/2024-12-04-guard-conditions.md @@ -0,0 +1,4 @@ +--- +category: minorAnalysis +--- +* The `Guards` library (`semmle.code.cpp.controlflow.Guards`) has been improved to recognize more guard conditions. \ No newline at end of file diff --git a/cpp/ql/lib/semmle/code/cpp/controlflow/IRGuards.qll b/cpp/ql/lib/semmle/code/cpp/controlflow/IRGuards.qll index 9b4d28430ff3..bb2b71e65495 100644 --- a/cpp/ql/lib/semmle/code/cpp/controlflow/IRGuards.qll +++ b/cpp/ql/lib/semmle/code/cpp/controlflow/IRGuards.qll @@ -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 @@ -59,26 +60,17 @@ class MatchValue extends AbstractValue, TMatchValue { } /** - * A Boolean condition in the AST that guards one or more basic blocks. + * A Boolean condition in the AST that guards one or more basic blocks. This includes + * operands of logical operators but not switch statements. */ -cached -class GuardCondition extends Expr { - cached - GuardCondition() { - exists(IRGuardCondition ir | this = ir.getUnconvertedResultExpression()) - or - // no binary operators in the IR - this.(BinaryLogicalOperation).getAnOperand() instanceof GuardCondition - } - +abstract private class GuardConditionImpl extends Expr { /** * Holds if this condition controls `controlled`, meaning that `controlled` is only * entered if the value of this condition is `v`. * * For details on what "controls" mean, see the QLDoc for `controls`. */ - cached - predicate valueControls(BasicBlock controlled, AbstractValue v) { none() } + abstract predicate valueControls(BasicBlock controlled, AbstractValue v); /** * Holds if this condition controls `controlled`, meaning that `controlled` is only @@ -106,67 +98,64 @@ class GuardCondition extends Expr { * being short-circuited) then it will only control blocks dominated by the * true (for `&&`) or false (for `||`) branch. */ - cached final predicate controls(BasicBlock controlled, boolean testIsTrue) { this.valueControls(controlled, any(BooleanValue bv | bv.getValue() = testIsTrue)) } /** Holds if (determined by this guard) `left < right + k` evaluates to `isLessThan` if this expression evaluates to `testIsTrue`. */ - cached - predicate comparesLt(Expr left, Expr right, int k, boolean isLessThan, boolean testIsTrue) { - none() - } + pragma[inline] + abstract predicate comparesLt(Expr left, Expr right, int k, boolean isLessThan, boolean testIsTrue); /** * Holds if (determined by this guard) `left < right + k` must be `isLessThan` in `block`. * If `isLessThan = false` then this implies `left >= right + k`. */ - cached - predicate ensuresLt(Expr left, Expr right, int k, BasicBlock block, boolean isLessThan) { none() } + pragma[inline] + abstract predicate ensuresLt(Expr left, Expr right, int k, BasicBlock block, boolean isLessThan); /** * 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() } + pragma[inline] + abstract predicate comparesLt(Expr e, int k, boolean isLessThan, AbstractValue value); /** * Holds if (determined by this guard) `e < k` must be `isLessThan` in `block`. * If `isLessThan = false` then this implies `e >= k`. */ - cached - predicate ensuresLt(Expr e, int k, BasicBlock block, boolean isLessThan) { none() } + pragma[inline] + abstract predicate ensuresLt(Expr e, int k, BasicBlock block, boolean isLessThan); /** 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) { - none() - } + pragma[inline] + abstract predicate comparesEq(Expr left, Expr right, int k, boolean areEqual, boolean testIsTrue); /** * Holds if (determined by this guard) `left == right + k` must be `areEqual` in `block`. * If `areEqual = false` then this implies `left != right + k`. */ - cached - predicate ensuresEq(Expr left, Expr right, int k, BasicBlock block, boolean areEqual) { none() } + pragma[inline] + abstract predicate ensuresEq(Expr left, Expr right, int k, BasicBlock block, boolean areEqual); /** Holds if (determined by this guard) `e == k` evaluates to `areEqual` if this expression evaluates to `value`. */ - cached - predicate comparesEq(Expr e, int k, boolean areEqual, AbstractValue value) { none() } + pragma[inline] + abstract predicate comparesEq(Expr e, int k, boolean areEqual, AbstractValue value); /** * Holds if (determined by this guard) `e == k` must be `areEqual` in `block`. * If `areEqual = false` then this implies `e != k`. */ - cached - predicate ensuresEq(Expr e, int k, BasicBlock block, boolean areEqual) { none() } + pragma[inline] + abstract predicate ensuresEq(Expr e, int k, BasicBlock block, boolean areEqual); } +final class GuardCondition = GuardConditionImpl; + /** * A binary logical operator in the AST that guards one or more basic blocks. */ -private class GuardConditionFromBinaryLogicalOperator extends GuardCondition { +private class GuardConditionFromBinaryLogicalOperator extends GuardConditionImpl { GuardConditionFromBinaryLogicalOperator() { this.(BinaryLogicalOperation).getAnOperand() instanceof GuardCondition } @@ -198,12 +187,14 @@ private class GuardConditionFromBinaryLogicalOperator extends GuardCondition { ) } + pragma[inline] 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) ) } + pragma[inline] 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) @@ -218,6 +209,7 @@ private class GuardConditionFromBinaryLogicalOperator extends GuardCondition { ) } + pragma[inline] override predicate ensuresEq(Expr left, Expr right, int k, BasicBlock block, boolean areEqual) { exists(boolean testIsTrue | this.comparesEq(left, right, k, areEqual, testIsTrue) and this.controls(block, testIsTrue) @@ -233,6 +225,7 @@ private class GuardConditionFromBinaryLogicalOperator extends GuardCondition { ) } + pragma[inline] override predicate ensuresEq(Expr e, int k, BasicBlock block, boolean areEqual) { exists(AbstractValue value | this.comparesEq(e, k, areEqual, value) and this.valueControls(block, value) @@ -244,7 +237,7 @@ private class GuardConditionFromBinaryLogicalOperator extends GuardCondition { * A Boolean condition in the AST that guards one or more basic blocks and has a corresponding IR * instruction. */ -private class GuardConditionFromIR extends GuardCondition { +private class GuardConditionFromIR extends GuardConditionImpl { IRGuardCondition ir; GuardConditionFromIR() { this = ir.getUnconvertedResultExpression() } @@ -255,6 +248,7 @@ private class GuardConditionFromIR extends GuardCondition { this.controlsBlock(controlled, v) } + pragma[inline] override predicate comparesLt(Expr left, Expr right, int k, boolean isLessThan, boolean testIsTrue) { exists(Instruction li, Instruction ri | li.getUnconvertedResultExpression() = left and @@ -263,6 +257,7 @@ private class GuardConditionFromIR extends GuardCondition { ) } + pragma[inline] override predicate comparesLt(Expr e, int k, boolean isLessThan, AbstractValue value) { exists(Instruction i | i.getUnconvertedResultExpression() = e and @@ -270,6 +265,7 @@ private class GuardConditionFromIR extends GuardCondition { ) } + pragma[inline] override predicate ensuresLt(Expr left, Expr right, int k, BasicBlock block, boolean isLessThan) { exists(Instruction li, Instruction ri, boolean testIsTrue | li.getUnconvertedResultExpression() = left and @@ -279,6 +275,7 @@ private class GuardConditionFromIR extends GuardCondition { ) } + pragma[inline] override predicate ensuresLt(Expr e, int k, BasicBlock block, boolean isLessThan) { exists(Instruction i, AbstractValue value | i.getUnconvertedResultExpression() = e and @@ -287,6 +284,7 @@ private class GuardConditionFromIR extends GuardCondition { ) } + pragma[inline] override predicate comparesEq(Expr left, Expr right, int k, boolean areEqual, boolean testIsTrue) { exists(Instruction li, Instruction ri | li.getUnconvertedResultExpression() = left and @@ -295,6 +293,7 @@ private class GuardConditionFromIR extends GuardCondition { ) } + pragma[inline] override predicate ensuresEq(Expr left, Expr right, int k, BasicBlock block, boolean areEqual) { exists(Instruction li, Instruction ri, boolean testIsTrue | li.getUnconvertedResultExpression() = left and @@ -304,6 +303,7 @@ private class GuardConditionFromIR extends GuardCondition { ) } + pragma[inline] override predicate comparesEq(Expr e, int k, boolean areEqual, AbstractValue value) { exists(Instruction i | i.getUnconvertedResultExpression() = e and @@ -311,6 +311,7 @@ private class GuardConditionFromIR extends GuardCondition { ) } + pragma[inline] override predicate ensuresEq(Expr e, int k, BasicBlock block, boolean areEqual) { exists(Instruction i, AbstractValue value | i.getUnconvertedResultExpression() = e and @@ -370,7 +371,6 @@ private predicate nonExcludedIRAndBasicBlock(IRBlock irb, BasicBlock controlled) * Note that `&&` and `||` don't have an explicit representation in the IR, * and therefore will not appear as IRGuardConditions. */ -cached class IRGuardCondition extends Instruction { Instruction branch; @@ -391,7 +391,7 @@ class IRGuardCondition extends Instruction { * gcc extension. * * The implementation of all four follows the same structure: Each relation - * has a cached user-facing predicate that. For example, + * has a user-facing predicate that. For example, * `GuardCondition::comparesEq` calls `compares_eq`. This predicate has * several cases that recursively decompose the relation to bring it to a * canonical form (i.e., a relation of the form `e1 == e2 + k`). The base @@ -401,7 +401,6 @@ class IRGuardCondition extends Instruction { * `e1 + k1 == e2 + k2` into canonical the form `e1 == e2 + (k2 - k1)`. */ - cached IRGuardCondition() { branch = getBranchForCondition(this) } /** @@ -410,7 +409,6 @@ class IRGuardCondition extends Instruction { * * For details on what "controls" mean, see the QLDoc for `controls`. */ - cached predicate valueControls(IRBlock controlled, AbstractValue v) { // This condition must determine the flow of control; that is, this // node must be a top-level condition. @@ -448,7 +446,6 @@ class IRGuardCondition extends Instruction { * being short-circuited) then it will only control blocks dominated by the * true (for `&&`) or false (for `||`) branch. */ - cached predicate controls(IRBlock controlled, boolean testIsTrue) { this.valueControls(controlled, any(BooleanValue bv | bv.getValue() = testIsTrue)) } @@ -457,7 +454,6 @@ class IRGuardCondition extends Instruction { * Holds if the control-flow edge `(pred, succ)` may be taken only if * the value of this condition is `v`. */ - cached predicate valueControlsEdge(IRBlock pred, IRBlock succ, AbstractValue v) { pred.getASuccessor() = succ and this.valueControls(pred, v) @@ -476,7 +472,6 @@ class IRGuardCondition extends Instruction { * Holds if the control-flow edge `(pred, succ)` may be taken only if * the value of this condition is `testIsTrue`. */ - cached final predicate controlsEdge(IRBlock pred, IRBlock succ, boolean testIsTrue) { this.valueControlsEdge(pred, succ, any(BooleanValue bv | bv.getValue() = testIsTrue)) } @@ -514,10 +509,10 @@ class IRGuardCondition extends Instruction { } /** Holds if (determined by this guard) `left < right + k` evaluates to `isLessThan` if this expression evaluates to `testIsTrue`. */ - cached + pragma[inline] predicate comparesLt(Operand left, Operand right, int k, boolean isLessThan, boolean testIsTrue) { exists(BooleanValue value | - compares_lt(this, left, right, k, isLessThan, value) and + compares_lt(valueNumber(this), left, right, k, isLessThan, value) and value.getValue() = testIsTrue ) } @@ -526,19 +521,20 @@ class IRGuardCondition extends Instruction { * Holds if (determined by this guard) `op < k` evaluates to `isLessThan` if * this expression evaluates to `value`. */ - cached + pragma[inline] predicate comparesLt(Operand op, int k, boolean isLessThan, AbstractValue value) { - compares_lt(this, op, k, isLessThan, value) + compares_lt(valueNumber(this), op, 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`. */ - cached + pragma[inline] predicate ensuresLt(Operand left, Operand right, int k, IRBlock block, boolean isLessThan) { exists(AbstractValue value | - compares_lt(this, left, right, k, isLessThan, value) and this.valueControls(block, value) + compares_lt(valueNumber(this), left, right, k, isLessThan, value) and + this.valueControls(block, value) ) } @@ -546,10 +542,11 @@ class IRGuardCondition extends Instruction { * Holds if (determined by this guard) `op < k` must be `isLessThan` in `block`. * If `isLessThan = false` then this implies `op >= k`. */ - cached + pragma[inline] 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) + compares_lt(valueNumber(this), op, k, isLessThan, value) and + this.valueControls(block, value) ) } @@ -557,12 +554,12 @@ class IRGuardCondition extends Instruction { * Holds if (determined by this guard) `left < right + k` must be `isLessThan` on the edge from * `pred` to `succ`. If `isLessThan = false` then this implies `left >= right + k`. */ - cached + pragma[inline] predicate ensuresLtEdge( Operand left, Operand right, int k, IRBlock pred, IRBlock succ, boolean isLessThan ) { exists(AbstractValue value | - compares_lt(this, left, right, k, isLessThan, value) and + compares_lt(valueNumber(this), left, right, k, isLessThan, value) and this.valueControlsEdge(pred, succ, value) ) } @@ -571,37 +568,38 @@ class IRGuardCondition extends Instruction { * 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 + pragma[inline] predicate ensuresLtEdge(Operand left, int k, IRBlock pred, IRBlock succ, boolean isLessThan) { exists(AbstractValue value | - compares_lt(this, left, k, isLessThan, value) and + compares_lt(valueNumber(this), left, k, isLessThan, value) and this.valueControlsEdge(pred, succ, value) ) } /** Holds if (determined by this guard) `left == right + k` evaluates to `areEqual` if this expression evaluates to `testIsTrue`. */ - cached + pragma[inline] predicate comparesEq(Operand left, Operand right, int k, boolean areEqual, boolean testIsTrue) { exists(BooleanValue value | - compares_eq(this, left, right, k, areEqual, value) and + compares_eq(valueNumber(this), left, right, k, areEqual, value) and value.getValue() = testIsTrue ) } /** Holds if (determined by this guard) `op == k` evaluates to `areEqual` if this expression evaluates to `value`. */ - cached + pragma[inline] predicate comparesEq(Operand op, int k, boolean areEqual, AbstractValue value) { - unary_compares_eq(this, op, k, areEqual, false, value) + unary_compares_eq(valueNumber(this), op, k, areEqual, false, value) } /** * Holds if (determined by this guard) `left == right + k` must be `areEqual` in `block`. * If `areEqual = false` then this implies `left != right + k`. */ - cached + pragma[inline] predicate ensuresEq(Operand left, Operand right, int k, IRBlock block, boolean areEqual) { exists(AbstractValue value | - compares_eq(this, left, right, k, areEqual, value) and this.valueControls(block, value) + compares_eq(valueNumber(this), left, right, k, areEqual, value) and + this.valueControls(block, value) ) } @@ -609,10 +607,11 @@ class IRGuardCondition extends Instruction { * Holds if (determined by this guard) `op == k` must be `areEqual` in `block`. * If `areEqual = false` then this implies `op != k`. */ - cached + pragma[inline] predicate ensuresEq(Operand op, int k, IRBlock block, boolean areEqual) { exists(AbstractValue value | - unary_compares_eq(this, op, k, areEqual, false, value) and this.valueControls(block, value) + unary_compares_eq(valueNumber(this), op, k, areEqual, false, value) and + this.valueControls(block, value) ) } @@ -620,12 +619,12 @@ class IRGuardCondition extends Instruction { * Holds if (determined by this guard) `left == right + k` must be `areEqual` on the edge from * `pred` to `succ`. If `areEqual = false` then this implies `left != right + k`. */ - cached + pragma[inline] predicate ensuresEqEdge( Operand left, Operand right, int k, IRBlock pred, IRBlock succ, boolean areEqual ) { exists(AbstractValue value | - compares_eq(this, left, right, k, areEqual, value) and + compares_eq(valueNumber(this), left, right, k, areEqual, value) and this.valueControlsEdge(pred, succ, value) ) } @@ -634,10 +633,10 @@ class IRGuardCondition extends Instruction { * Holds if (determined by this guard) `op == k` must be `areEqual` on the edge from * `pred` to `succ`. If `areEqual = false` then this implies `op != k`. */ - cached + pragma[inline] predicate ensuresEqEdge(Operand op, int k, IRBlock pred, IRBlock succ, boolean areEqual) { exists(AbstractValue value | - unary_compares_eq(this, op, k, areEqual, false, value) and + unary_compares_eq(valueNumber(this), op, k, areEqual, false, value) and this.valueControlsEdge(pred, succ, value) ) } @@ -727,630 +726,730 @@ class IRGuardCondition extends Instruction { private Instruction getBranchForCondition(Instruction guard) { result.(ConditionalBranchInstruction).getCondition() = guard or - exists(LogicalNotInstruction cond | - result = getBranchForCondition(cond) and cond.getUnary() = guard - ) - or result.(SwitchInstruction).getExpression() = guard -} - -/** - * Holds if `left == right + k` is `areEqual` given that test is `testIsTrue`. - * - * 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 -) { - /* 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) | - areEqual = true and value = v - or - areEqual = false and value = v.getDualValue() - ) - or - // I think this is handled by forwarding in controlsBlock. - //or - //logical_comparison_eq(test, left, right, k, areEqual, testIsTrue) - /* a == b + k => b == a - k */ - exists(int mk | k = -mk | compares_eq(test, right, left, mk, areEqual, value)) - or - 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) - ) or - compares_eq(test.(BuiltinExpectCallInstruction).getCondition(), left, right, k, areEqual, 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, 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, k, inNonZeroCase, v) and op.getDef() = test - | - areEqual = true and value = v - or - areEqual = false and value = v.getDualValue() - ) - or - unary_complex_eq(test, op, k, areEqual, inNonZeroCase, value) - or - /* (x is true => (op == k)) => (!x is false => (op == k)) */ - 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 - k = k1 + k2 + exists(LogicalNotInstruction cond | + result = getBranchForCondition(cond) and cond.getUnary() = guard ) - or - unary_compares_eq(test.(BuiltinExpectCallInstruction).getCondition(), op, k, areEqual, - inNonZeroCase, value) } -/** Rearrange various simple comparisons into `left == right + k` form. */ -private predicate simple_comparison_eq( - CompareInstruction cmp, Operand left, Operand right, int k, AbstractValue value -) { - left = cmp.getLeftOperand() and - cmp instanceof CompareEQInstruction and - right = cmp.getRightOperand() and - k = 0 and - value.(BooleanValue).getValue() = true - or - left = cmp.getLeftOperand() and - cmp instanceof CompareNEInstruction and - right = cmp.getRightOperand() and - k = 0 and - value.(BooleanValue).getValue() = false -} +cached +private module Cached { + /** + * 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 a `CompareInstruction` belonging to this value number. */ + CompareInstruction getCompareInstruction() { result = cmp } + + /** + * Gets the left and right operands of a `CompareInstruction` that + * belong to this value number. + */ + predicate hasOperands(Operand left, Operand right) { + left = cmp.getLeftOperand() and + right = cmp.getRightOperand() + } + } -/** - * Rearrange various simple comparisons into `op == k` form. - */ -private predicate unary_simple_comparison_eq( - Instruction test, int k, boolean inNonZeroCase, AbstractValue value -) { - exists(SwitchInstruction switch, CaseEdge case | - test = switch.getExpression() and - case = value.(MatchValue).getCase() and - exists(switch.getSuccessor(case)) and - case.getValue().toInt() = k and - inNonZeroCase = false - ) - or - // Any instruction with an integral type could potentially be part of a - // check for nullness when used in a guard. So we include all integral - // typed instructions here. However, since some of these instructions are - // already included as guards in other cases, we exclude those here. - // These are instructions that compute a binary equality or inequality - // relation. For example, the following: - // ```cpp - // if(a == b + 42) { ... } - // ``` - // generates the following IR: - // ``` - // r1(glval) = VariableAddress[a] : - // r2(int) = Load[a] : &:r1, m1 - // r3(glval) = VariableAddress[b] : - // r4(int) = Load[b] : &:r3, m2 - // r5(int) = Constant[42] : - // r6(int) = Add : r4, r5 - // r7(bool) = CompareEQ : r2, r6 - // v1(void) = ConditionalBranch : r7 - // ``` - // and since `r7` is an integral typed instruction this predicate could - // include a case for when `r7` evaluates to true (in which case we would - // infer that `r6` was non-zero, and a case for when `r7` evaluates to false - // (in which case we would infer that `r6` was zero). - // However, since `a == b + 42` is already supported when reasoning about - // binary equalities we exclude those cases here. - not test.isGLValue() and - not simple_comparison_eq(test, _, _, _, _) and - not simple_comparison_lt(test, _, _, _) and - not test = any(SwitchInstruction switch).getExpression() and - ( - test.getResultIRType() instanceof IRAddressType or - test.getResultIRType() instanceof IRIntegerType or - test.getResultIRType() instanceof IRBooleanType - ) and - ( - k = 1 and - value.(BooleanValue).getValue() = true and - inNonZeroCase = true - or - k = 0 and - value.(BooleanValue).getValue() = false and - inNonZeroCase = false - ) -} + private class CompareEQValueNumber extends CompareValueNumber { + override CompareEQInstruction cmp; + } -/** A call to the builtin operation `__builtin_expect`. */ -private class BuiltinExpectCallInstruction extends CallInstruction { - BuiltinExpectCallInstruction() { this.getStaticCallTarget().hasName("__builtin_expect") } + private class CompareNEValueNumber extends CompareValueNumber { + override CompareNEInstruction cmp; + } - /** Gets the condition of this call. */ - Instruction getCondition() { - // The first parameter of `__builtin_expect` has type `long`. So we skip - // the conversion when inferring guards. - result = this.getArgument(0).(ConvertInstruction).getUnary() + private class CompareLTValueNumber extends CompareValueNumber { + override CompareLTInstruction cmp; } -} -/** - * Holds if `left == right + k` is `areEqual` if `cmp` evaluates to `value`, - * and `cmp` is an instruction that compares the value of - * `__builtin_expect(left == right + k, _)` to `0`. - */ -private predicate builtin_expect_eq( - CompareInstruction cmp, Operand left, Operand right, int k, boolean areEqual, AbstractValue value -) { - exists(BuiltinExpectCallInstruction call, Instruction const, AbstractValue innerValue | - int_value(const) = 0 and - cmp.hasOperands(call.getAUse(), const.getAUse()) and - compares_eq(call.getCondition(), left, right, k, areEqual, innerValue) - | - cmp instanceof CompareNEInstruction and - value = innerValue - or - cmp instanceof CompareEQInstruction and - value.getDualValue() = innerValue - ) -} + private class CompareGTValueNumber extends CompareValueNumber { + override CompareGTInstruction cmp; + } -private predicate complex_eq( - CompareInstruction cmp, Operand left, Operand right, int k, boolean areEqual, AbstractValue value -) { - sub_eq(cmp, left, right, k, areEqual, value) - or - add_eq(cmp, left, right, k, areEqual, value) - or - builtin_expect_eq(cmp, left, right, k, areEqual, value) -} + private class CompareLEValueNumber extends CompareValueNumber { + override CompareLEInstruction cmp; + } -/** - * Holds if `op == k` is `areEqual` if `cmp` evaluates to `value`, and `cmp` is - * an instruction that compares the value of `__builtin_expect(op == k, _)` to `0`. - */ -private predicate unary_builtin_expect_eq( - CompareInstruction cmp, Operand op, int k, boolean areEqual, boolean inNonZeroCase, - AbstractValue value -) { - exists(BuiltinExpectCallInstruction 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) - | - cmp instanceof CompareNEInstruction and - value = innerValue - or - cmp instanceof CompareEQInstruction and - value.getDualValue() = innerValue - ) -} + private class CompareGEValueNumber extends CompareValueNumber { + override CompareGEInstruction cmp; + } -private predicate unary_complex_eq( - Instruction test, Operand op, int k, boolean areEqual, boolean inNonZeroCase, AbstractValue value -) { - unary_sub_eq(test, op, k, areEqual, inNonZeroCase, value) - or - unary_add_eq(test, op, k, areEqual, inNonZeroCase, value) - or - unary_builtin_expect_eq(test, op, k, areEqual, inNonZeroCase, value) -} + /** + * A value number such that at least one of the instructions provides + * the integer value controlling a `SwitchInstruction`. + */ + private class SwitchConditionValueNumber extends ValueNumber { + SwitchInstruction switch; -/* - * Simplification of inequality expressions - * Simplify conditions in the source to the canonical form l < r + k. - */ + pragma[nomagic] + SwitchConditionValueNumber() { this.getAnInstruction() = switch.getExpression() } -/** 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 -) { - /* In the simple case, the test is the comparison, so isLt = testIsTrue */ - simple_comparison_lt(test, left, right, k) and - value.(BooleanValue).getValue() = isLt - or - 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, 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) - ) -} + /** Gets an expression that belongs to this value number. */ + Operand getExpressionOperand() { result = switch.getExpressionOperand() } -/** 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) { - unary_simple_comparison_lt(test, k, isLt, value) and - op.getDef() = test - 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 - ) -} + Instruction getSuccessor(CaseEdge kind) { result = switch.getSuccessor(kind) } + } -/** `(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 -) { - exists(int onemk | k = 1 - onemk | compares_lt(test, right, left, onemk, isGe, value)) -} + private class BuiltinExpectCallValueNumber extends ValueNumber { + BuiltinExpectCallInstruction instr; -/** Rearrange various simple comparisons into `left < right + k` form. */ -private predicate simple_comparison_lt(CompareInstruction cmp, Operand left, Operand right, int k) { - left = cmp.getLeftOperand() and - cmp instanceof CompareLTInstruction and - right = cmp.getRightOperand() and - k = 0 - or - left = cmp.getLeftOperand() and - cmp instanceof CompareLEInstruction and - right = cmp.getRightOperand() and - k = 1 - or - right = cmp.getLeftOperand() and - cmp instanceof CompareGTInstruction and - left = cmp.getRightOperand() and - k = 0 - or - right = cmp.getLeftOperand() and - cmp instanceof CompareGEInstruction and - left = cmp.getRightOperand() and - k = 1 -} + BuiltinExpectCallValueNumber() { this.getAnInstruction() = instr } -/** Rearrange various simple comparisons into `op < k` form. */ -private predicate unary_simple_comparison_lt( - Instruction test, int k, boolean isLt, AbstractValue value -) { - exists(SwitchInstruction switch, CaseEdge case | - test = switch.getExpression() 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 - ) -} + ValueNumber getCondition() { result.getAnInstruction() = instr.getCondition() } -private predicate complex_lt( - CompareInstruction 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) -} + Operand getAUse() { result = instr.getAUse() } + } -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) -} + private class LogicalNotValueNumber extends ValueNumber { + LogicalNotInstruction instr; -// 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 -) { - exists(SubInstruction lhs, int c, int x | - 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, 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, 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, value) and - right = rhs.getLeftOperand() and - x = int_value(rhs.getRight()) and - k = c - x - ) -} + LogicalNotValueNumber() { this.getAnInstruction() = instr } -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 - ) -} + ValueNumber getUnary() { result.getAnInstruction() = instr.getUnary() } + } -// 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 -) { - exists(AddInstruction lhs, int c, int x | - compares_lt(cmp, lhs.getAUse(), right, 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(AddInstruction rhs, int c, int x | - compares_lt(cmp, left, rhs.getAUse(), c, isLt, value) and - ( - right = rhs.getLeftOperand() and x = int_value(rhs.getRight()) + /** + * Holds if `left == right + k` is `areEqual` given that test is `testIsTrue`. + * + * Beware making mistaken logical implications here relating `areEqual` and `value`. + */ + cached + predicate compares_eq( + 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) | + areEqual = true and value = v or - right = rhs.getRightOperand() and x = int_value(rhs.getLeft()) - ) and - k = c + x - ) - or - exists(PointerAddInstruction lhs, int c, int x | - compares_lt(cmp, lhs.getAUse(), right, c, isLt, value) and - ( - left = lhs.getLeftOperand() and x = int_value(lhs.getRight()) + areEqual = false and value = v.getDualValue() + ) + or + // I think this is handled by forwarding in controlsBlock. + //or + //logical_comparison_eq(test, left, right, k, areEqual, testIsTrue) + /* a == b + k => b == a - k */ + exists(int mk | k = -mk | compares_eq(test, right, left, mk, areEqual, value)) + or + 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.(LogicalNotValueNumber).getUnary(), left, right, k, areEqual, dual) + ) + or + compares_eq(test.(BuiltinExpectCallValueNumber).getCondition(), left, right, k, areEqual, 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. + */ + cached + predicate unary_compares_eq( + ValueNumber 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, inNonZeroCase, v) | + areEqual = true and value = v or - left = lhs.getRightOperand() and x = int_value(lhs.getLeft()) - ) and - k = c - x - ) - or - exists(PointerAddInstruction rhs, int c, int x | - compares_lt(cmp, left, rhs.getAUse(), c, isLt, value) and - ( - right = rhs.getLeftOperand() and x = int_value(rhs.getRight()) + areEqual = false and value = v.getDualValue() + ) + or + unary_complex_eq(test, op, k, areEqual, inNonZeroCase, value) + or + /* (x is true => (op == k)) => (!x is false => (op == k)) */ + exists(AbstractValue dual, boolean inNonZeroCase0 | + value = dual.getDualValue() and + unary_compares_eq(test.(LogicalNotValueNumber).getUnary(), op, k, inNonZeroCase0, areEqual, + dual) + | + k = 0 and inNonZeroCase = inNonZeroCase0 or - right = rhs.getRightOperand() and x = int_value(rhs.getLeft()) - ) and - k = c + x - ) -} + 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, 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) + } -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()) + /** Rearrange various simple comparisons into `left == right + k` form. */ + private predicate simple_comparison_eq( + CompareValueNumber cmp, Operand left, Operand right, int k, AbstractValue value + ) { + cmp instanceof CompareEQValueNumber and + cmp.hasOperands(left, right) and + k = 0 and + value.(BooleanValue).getValue() = true + or + cmp instanceof CompareNEValueNumber and + cmp.hasOperands(left, right) and + k = 0 and + value.(BooleanValue).getValue() = false + } + + /** + * Holds if `op` is an operand that is eventually used in a unary comparison + * with a constant. + */ + private predicate isRelevantUnaryComparisonOperand(Operand op) { + // Base case: `op` is an operand of a `CompareEQInstruction` or `CompareNEInstruction`, + // and the other operand is a constant. + exists(CompareInstruction eq, Instruction instr | + eq.hasOperands(op, instr.getAUse()) and + exists(int_value(instr)) + | + eq instanceof CompareEQInstruction 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 + eq instanceof CompareNEInstruction + ) + or + // C doesn't have int-to-bool conversions, so `if(x)` will just generate: + // r2_1(glval) = VariableAddress[x] + // r2_2(int) = Load[x] : &:r2_1, m1_6 + // v2_3(void) = ConditionalBranch : r2_2 + exists(ConditionalBranchInstruction branch | branch.getConditionOperand() = op) + or + // If `!x` is a relevant unary comparison then so is `x`. + exists(LogicalNotInstruction logicalNot | + isRelevantUnaryComparisonOperand(unique( | | logicalNot.getAUse())) and + logicalNot.getUnaryOperand() = op + ) + or + // If `y` is a relevant unary comparison and `y = x` then so is `x`. + not op.isDefinitionInexact() and + exists(CopyInstruction copy | + isRelevantUnaryComparisonOperand(unique( | | copy.getAUse())) and + op = copy.getSourceValueOperand() + ) + or + // If phi(x1, x2) is a relevant unary comparison then so are `x1` and `x2`. + not op.isDefinitionInexact() and + exists(PhiInstruction phi | + isRelevantUnaryComparisonOperand(unique( | | phi.getAUse())) and + op = phi.getAnInputOperand() + ) + or + // If `__builtin_expect(x)` is a relevant unary comparison then so is `x`. + exists(BuiltinExpectCallInstruction call | + isRelevantUnaryComparisonOperand(unique( | | call.getAUse())) and + op = call.getConditionOperand() + ) + } + + /** Rearrange various simple comparisons into `op == k` form. */ + private predicate unary_simple_comparison_eq( + ValueNumber test, Operand op, int k, boolean inNonZeroCase, 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 + ) + or + isRelevantUnaryComparisonOperand(op) and + op.getDef() = test.getAnInstruction() and ( - left = lhs.getLeftOperand() and x = int_value(lhs.getRight()) + k = 1 and + value.(BooleanValue).getValue() = true and + inNonZeroCase = true or - left = lhs.getRightOperand() and x = int_value(lhs.getLeft()) - ) and - k = c - x - ) -} + k = 0 and + value.(BooleanValue).getValue() = false and + inNonZeroCase = false + ) + } -// 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 -) { - exists(SubInstruction lhs, int c, int x | - compares_eq(cmp, lhs.getAUse(), right, c, areEqual, value) and - left = lhs.getLeftOperand() and - x = int_value(lhs.getRight()) and - k = c + x - ) - or - exists(SubInstruction rhs, int c, int x | - compares_eq(cmp, left, rhs.getAUse(), c, areEqual, value) and - right = rhs.getLeftOperand() and - x = int_value(rhs.getRight()) and - k = c - x - ) - or - exists(PointerSubInstruction lhs, int c, int x | - compares_eq(cmp, lhs.getAUse(), right, c, areEqual, value) and - left = lhs.getLeftOperand() and - x = int_value(lhs.getRight()) and - k = c + x - ) - or - exists(PointerSubInstruction rhs, int c, int x | - compares_eq(cmp, left, rhs.getAUse(), c, areEqual, value) and - right = rhs.getLeftOperand() and - x = int_value(rhs.getRight()) and - k = c - x - ) -} + /** A call to the builtin operation `__builtin_expect`. */ + private class BuiltinExpectCallInstruction extends CallInstruction { + BuiltinExpectCallInstruction() { this.getStaticCallTarget().hasName("__builtin_expect") } -// op - x == c => op == (c+x) -private predicate unary_sub_eq( - 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, 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, inNonZeroCase, value) and - op = sub.getLeftOperand() and - x = int_value(sub.getRight()) and - k = c + x - ) -} + /** Gets the condition of this call. */ + Instruction getCondition() { result = this.getConditionOperand().getDef() } -// 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 -) { - exists(AddInstruction lhs, int c, int x | - compares_eq(cmp, lhs.getAUse(), right, c, areEqual, 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(AddInstruction rhs, int c, int x | - compares_eq(cmp, left, rhs.getAUse(), c, areEqual, value) and - ( - right = rhs.getLeftOperand() and x = int_value(rhs.getRight()) - or - right = rhs.getRightOperand() and x = int_value(rhs.getLeft()) - ) and - k = c + x - ) - or - exists(PointerAddInstruction lhs, int c, int x | - compares_eq(cmp, lhs.getAUse(), right, c, areEqual, 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 rhs, int c, int x | - compares_eq(cmp, left, rhs.getAUse(), c, areEqual, value) and - ( - right = rhs.getLeftOperand() and x = int_value(rhs.getRight()) + Operand getConditionOperand() { + // The first parameter of `__builtin_expect` has type `long`. So we skip + // the conversion when inferring guards. + result = this.getArgument(0).(ConvertInstruction).getUnaryOperand() + } + } + + /** + * Holds if `left == right + k` is `areEqual` if `cmp` evaluates to `value`, + * and `cmp` is an instruction that compares the value of + * `__builtin_expect(left == right + k, _)` to `0`. + */ + private predicate builtin_expect_eq( + CompareValueNumber cmp, Operand left, Operand right, 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 + compares_eq(call.getCondition(), left, right, k, areEqual, innerValue) + | + cmp instanceof CompareNEValueNumber and + value = innerValue or - right = rhs.getRightOperand() and x = int_value(rhs.getLeft()) - ) and - k = c + x - ) -} + cmp instanceof CompareEQValueNumber and + value.getDualValue() = innerValue + ) + } -// left + x == right + c => left == right + (c-x) -private predicate unary_add_eq( - 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, inNonZeroCase, value) and - ( - left = lhs.getLeftOperand() and x = int_value(lhs.getRight()) + private predicate complex_eq( + ValueNumber cmp, Operand left, Operand right, int k, boolean areEqual, AbstractValue value + ) { + sub_eq(cmp, left, right, k, areEqual, value) + or + add_eq(cmp, left, right, k, areEqual, value) + or + builtin_expect_eq(cmp, left, right, k, areEqual, value) + } + + /** + * Holds if `op == k` is `areEqual` if `cmp` evaluates to `value`, and `cmp` is + * 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 + ) { + 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) + | + cmp instanceof CompareNEValueNumber and + value = innerValue or - left = lhs.getRightOperand() and x = int_value(lhs.getLeft()) - ) and - 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 - ( - left = lhs.getLeftOperand() and x = int_value(lhs.getRight()) + cmp instanceof CompareEQValueNumber and + value.getDualValue() = innerValue + ) + } + + private predicate unary_complex_eq( + ValueNumber test, Operand op, int k, boolean areEqual, boolean inNonZeroCase, + AbstractValue value + ) { + unary_sub_eq(test, op, k, areEqual, inNonZeroCase, value) + or + unary_add_eq(test, op, k, areEqual, inNonZeroCase, value) + or + unary_builtin_expect_eq(test, op, k, areEqual, inNonZeroCase, value) + } + + /* + * Simplification of inequality expressions + * Simplify conditions in the source to the canonical form l < r + k. + */ + + /** Holds if `left < right + k` evaluates to `isLt` given that test is `value`. */ + cached + predicate compares_lt( + 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 + value.(BooleanValue).getValue() = isLt + or + 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, value)) + or + /* (x is true => (left < right + k)) => (!x is false => (left < right + k)) */ + exists(AbstractValue dual | value = dual.getDualValue() | + compares_lt(test.(LogicalNotValueNumber).getUnary(), left, right, k, isLt, dual) + ) + } + + /** Holds if `op < k` evaluates to `isLt` given that `test` evaluates to `value`. */ + cached + predicate compares_lt(ValueNumber test, Operand op, int k, boolean isLt, AbstractValue value) { + unary_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.(LogicalNotValueNumber).getUnary(), op, k, isLt, dual) + ) + or + exists(int k1, int k2, Instruction 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( + 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(CompareValueNumber cmp, Operand left, Operand right, int k) { + cmp.hasOperands(left, right) and + cmp instanceof CompareLTValueNumber and + k = 0 + or + cmp.hasOperands(left, right) and + cmp instanceof CompareLEValueNumber and + k = 1 + or + cmp.hasOperands(right, left) and + cmp instanceof CompareGTValueNumber and + k = 0 + or + cmp.hasOperands(right, left) and + cmp instanceof CompareGEValueNumber and + k = 1 + } + + /** Rearrange various simple comparisons into `op < k` form. */ + private predicate unary_simple_comparison_lt( + SwitchConditionValueNumber test, Operand op, int k, boolean isLt, AbstractValue value + ) { + exists(CaseEdge case | + test.getExpressionOperand() = op and + case = value.(MatchValue).getCase() and + exists(test.getSuccessor(case)) and + case.getMaxValue() > case.getMinValue() + | + // op <= k => op < k - 1 + isLt = true and + case.getMaxValue().toInt() = k - 1 or - left = lhs.getRightOperand() and x = int_value(lhs.getLeft()) - ) and - k = c - x - ) -} + isLt = false and + case.getMinValue().toInt() = k + ) + } -private class IntegerOrPointerConstantInstruction extends ConstantInstruction { - IntegerOrPointerConstantInstruction() { - this instanceof IntegerConstantInstruction or - this instanceof PointerConstantInstruction + private predicate complex_lt( + 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( + ValueNumber 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( + 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 + 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, 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, 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, value) and + right = rhs.getLeftOperand() and + x = int_value(rhs.getRight()) and + k = c - x + ) + } + + 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 + 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( + 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 + ( + 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(AddInstruction rhs, int c, int x | + compares_lt(cmp, left, rhs.getAUse(), c, isLt, value) and + ( + right = rhs.getLeftOperand() and x = int_value(rhs.getRight()) + or + right = rhs.getRightOperand() and x = int_value(rhs.getLeft()) + ) and + k = c + x + ) + or + exists(PointerAddInstruction lhs, int c, int x | + compares_lt(cmp, lhs.getAUse(), right, 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 rhs, int c, int x | + compares_lt(cmp, left, rhs.getAUse(), c, isLt, value) and + ( + right = rhs.getLeftOperand() and x = int_value(rhs.getRight()) + or + right = rhs.getRightOperand() and x = int_value(rhs.getLeft()) + ) and + k = c + x + ) + } + + 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 + ( + 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( + 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 + left = lhs.getLeftOperand() and + x = int_value(lhs.getRight()) and + k = c + x + ) + or + exists(SubInstruction rhs, int c, int x | + compares_eq(cmp, left, rhs.getAUse(), c, areEqual, value) and + right = rhs.getLeftOperand() and + x = int_value(rhs.getRight()) and + k = c - x + ) + or + exists(PointerSubInstruction lhs, int c, int x | + compares_eq(cmp, lhs.getAUse(), right, c, areEqual, value) and + left = lhs.getLeftOperand() and + x = int_value(lhs.getRight()) and + k = c + x + ) + or + exists(PointerSubInstruction rhs, int c, int x | + compares_eq(cmp, left, rhs.getAUse(), c, areEqual, value) and + right = rhs.getLeftOperand() and + x = int_value(rhs.getRight()) and + k = c - x + ) + } + + // op - x == c => op == (c+x) + private predicate unary_sub_eq( + ValueNumber 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, 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, inNonZeroCase, value) and + op = sub.getLeftOperand() and + x = int_value(sub.getRight()) and + k = c + x + ) } -} -/** The int value of integer constant expression. */ -private int int_value(Instruction i) { - result = i.(IntegerOrPointerConstantInstruction).getValue().toInt() + // left + x == right + c => left == right + (c-x) + // left == (right + x) + c => left == right + (c+x) + private predicate add_eq( + 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 + ( + 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(AddInstruction rhs, int c, int x | + compares_eq(cmp, left, rhs.getAUse(), c, areEqual, value) and + ( + right = rhs.getLeftOperand() and x = int_value(rhs.getRight()) + or + right = rhs.getRightOperand() and x = int_value(rhs.getLeft()) + ) and + k = c + x + ) + or + exists(PointerAddInstruction lhs, int c, int x | + compares_eq(cmp, lhs.getAUse(), right, c, areEqual, 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 rhs, int c, int x | + compares_eq(cmp, left, rhs.getAUse(), c, areEqual, value) and + ( + right = rhs.getLeftOperand() and x = int_value(rhs.getRight()) + or + right = rhs.getRightOperand() and x = int_value(rhs.getLeft()) + ) and + k = c + x + ) + } + + // 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 + ) { + inNonZeroCase = false and + exists(AddInstruction lhs, int c, int x | + unary_compares_eq(test, lhs.getAUse(), c, areEqual, inNonZeroCase, 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 + inNonZeroCase = false and + exists(PointerAddInstruction lhs, int c, int x | + unary_compares_eq(test, lhs.getAUse(), c, areEqual, inNonZeroCase, 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 + ) + } + + private class IntegerOrPointerConstantInstruction extends ConstantInstruction { + IntegerOrPointerConstantInstruction() { + this instanceof IntegerConstantInstruction or + this instanceof PointerConstantInstruction + } + } + + /** The int value of integer constant expression. */ + private int int_value(IntegerOrPointerConstantInstruction i) { result = i.getValue().toInt() } } + +private import Cached diff --git a/cpp/ql/test/experimental/library-tests/rangeanalysis/rangeanalysis/RangeAnalysis.expected b/cpp/ql/test/experimental/library-tests/rangeanalysis/rangeanalysis/RangeAnalysis.expected index 106313c87079..15125038d19c 100644 --- a/cpp/ql/test/experimental/library-tests/rangeanalysis/rangeanalysis/RangeAnalysis.expected +++ b/cpp/ql/test/experimental/library-tests/rangeanalysis/rangeanalysis/RangeAnalysis.expected @@ -17,6 +17,7 @@ | test.cpp:49:12:49:12 | Load: x | test.cpp:46:22:46:22 | ValueNumberBound | -1 | true | CompareLT: ... < ... | test.cpp:48:9:48:13 | test.cpp:48:9:48:13 | | test.cpp:49:12:49:12 | Load: x | test.cpp:46:29:46:29 | ValueNumberBound | -2 | true | CompareLT: ... < ... | test.cpp:48:9:48:13 | test.cpp:48:9:48:13 | | test.cpp:54:12:54:12 | Load: x | test.cpp:46:22:46:22 | ValueNumberBound | -1 | true | CompareLT: ... < ... | test.cpp:52:7:52:11 | test.cpp:52:7:52:11 | +| test.cpp:54:12:54:12 | Load: x | test.cpp:46:29:46:29 | ValueNumberBound | -2 | true | CompareLT: ... < ... | test.cpp:52:7:52:11 | test.cpp:52:7:52:11 | | test.cpp:62:10:62:13 | Load: iter | test.cpp:60:17:60:17 | ValueNumberBound | 0 | false | NoReason | file://:0:0:0:0 | file://:0:0:0:0 | | test.cpp:62:10:62:13 | Load: iter | test.cpp:60:17:60:17 | ValueNumberBound | 3 | true | CompareLT: ... < ... | test.cpp:61:32:61:51 | test.cpp:61:32:61:51 | | test.cpp:62:10:62:13 | Load: iter | test.cpp:61:39:61:51 | ValueNumberBound | -1 | true | CompareLT: ... < ... | test.cpp:61:32:61:51 | test.cpp:61:32:61:51 | diff --git a/cpp/ql/test/experimental/library-tests/rangeanalysis/rangeanalysis/test.cpp b/cpp/ql/test/experimental/library-tests/rangeanalysis/rangeanalysis/test.cpp index 87653c2fa43d..6b241fc42f77 100644 --- a/cpp/ql/test/experimental/library-tests/rangeanalysis/rangeanalysis/test.cpp +++ b/cpp/ql/test/experimental/library-tests/rangeanalysis/rangeanalysis/test.cpp @@ -51,7 +51,7 @@ int test5(int x, int y, int z) { } if (x < y) { if (y < z) { - sink(x); // x < z is not inferred here + sink(x); // x < z is inferred here } } } 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 d097fa7dfa67..24ce995f8133 100644 --- a/cpp/ql/test/library-tests/controlflow/guards-ir/tests.expected +++ b/cpp/ql/test/library-tests/controlflow/guards-ir/tests.expected @@ -42,6 +42,8 @@ astGuards astGuardsCompare | 7 | 0 < x+0 when ... > ... is true | | 7 | 0 >= x+0 when ... > ... is false | +| 7 | ... > ... != 0 when ... > ... is true | +| 7 | ... > ... == 0 when ... > ... is false | | 7 | x < 0+1 when ... > ... is false | | 7 | x >= 0+1 when ... > ... is true | | 17 | 0 < x+1 when ... < ... is false | @@ -50,6 +52,12 @@ astGuardsCompare | 17 | 1 < y+0 when ... && ... is true | | 17 | 1 < y+0 when ... > ... is true | | 17 | 1 >= y+0 when ... > ... is false | +| 17 | ... < ... != 0 when ... && ... is true | +| 17 | ... < ... != 0 when ... < ... is true | +| 17 | ... < ... == 0 when ... < ... is false | +| 17 | ... > ... != 0 when ... && ... is true | +| 17 | ... > ... != 0 when ... > ... is true | +| 17 | ... > ... == 0 when ... > ... is false | | 17 | x < 0+0 when ... && ... is true | | 17 | x < 0+0 when ... < ... is true | | 17 | x >= 0+0 when ... < ... is false | @@ -60,30 +68,42 @@ astGuardsCompare | 18 | call to get == 0 when call to get is false | | 26 | 0 < x+0 when ... > ... is true | | 26 | 0 >= x+0 when ... > ... is false | +| 26 | ... > ... != 0 when ... > ... is true | +| 26 | ... > ... == 0 when ... > ... is false | | 26 | x < 0+1 when ... > ... is false | | 26 | x >= 0+1 when ... > ... is true | | 31 | - ... != x+0 when ... == ... is false | | 31 | - ... == x+0 when ... == ... is true | +| 31 | ... == ... != 0 when ... == ... is true | +| 31 | ... == ... == 0 when ... == ... is false | | 31 | x != -1 when ... == ... is false | | 31 | x != - ...+0 when ... == ... is false | | 31 | x == -1 when ... == ... is true | | 31 | x == - ...+0 when ... == ... is true | | 34 | 10 < j+1 when ... < ... is false | | 34 | 10 >= j+1 when ... < ... is true | +| 34 | ... < ... != 0 when ... < ... is true | +| 34 | ... < ... == 0 when ... < ... is false | | 34 | j < 10+0 when ... < ... is true | | 34 | j >= 10+0 when ... < ... is false | | 42 | 10 < j+1 when ... < ... is false | | 42 | 10 >= j+1 when ... < ... is true | +| 42 | ... < ... != 0 when ... < ... is true | +| 42 | ... < ... == 0 when ... < ... is false | | 42 | call to getABool != 0 when call to getABool is true | | 42 | call to getABool == 0 when call to getABool is false | | 42 | j < 10+0 when ... < ... is true | | 42 | j >= 10+0 when ... < ... is false | | 44 | 0 < z+0 when ... > ... is true | | 44 | 0 >= z+0 when ... > ... is false | +| 44 | ... > ... != 0 when ... > ... is true | +| 44 | ... > ... == 0 when ... > ... is false | | 44 | z < 0+1 when ... > ... is false | | 44 | z >= 0+1 when ... > ... is true | | 45 | 0 < y+0 when ... > ... is true | | 45 | 0 >= y+0 when ... > ... is false | +| 45 | ... > ... != 0 when ... > ... is true | +| 45 | ... > ... == 0 when ... > ... is false | | 45 | y < 0+1 when ... > ... is false | | 45 | y >= 0+1 when ... > ... is true | | 58 | 0 != x+0 when ... == ... is false | @@ -92,6 +112,12 @@ astGuardsCompare | 58 | 0 < y+1 when ... \|\| ... is false | | 58 | 0 == x+0 when ... == ... is true | | 58 | 0 >= y+1 when ... < ... is true | +| 58 | ... < ... != 0 when ... < ... is true | +| 58 | ... < ... == 0 when ... < ... is false | +| 58 | ... < ... == 0 when ... \|\| ... is false | +| 58 | ... == ... != 0 when ... == ... is true | +| 58 | ... == ... == 0 when ... == ... is false | +| 58 | ... == ... == 0 when ... \|\| ... is false | | 58 | x != 0 when ... == ... is false | | 58 | x != 0 when ... \|\| ... is false | | 58 | x != 0+0 when ... == ... is false | @@ -103,6 +129,8 @@ astGuardsCompare | 58 | y >= 0+0 when ... \|\| ... is false | | 75 | 0 != x+0 when ... == ... is false | | 75 | 0 == x+0 when ... == ... is true | +| 75 | ... == ... != 0 when ... == ... is true | +| 75 | ... == ... == 0 when ... == ... is false | | 75 | x != 0 when ... == ... is false | | 75 | x != 0+0 when ... == ... is false | | 75 | x == 0 when ... == ... is true | @@ -113,6 +141,12 @@ astGuardsCompare | 85 | 0 == x+0 when ... && ... is true | | 85 | 0 == x+0 when ... == ... is true | | 85 | 0 == y+0 when ... != ... is false | +| 85 | ... != ... != 0 when ... != ... is true | +| 85 | ... != ... != 0 when ... && ... is true | +| 85 | ... != ... == 0 when ... != ... is false | +| 85 | ... == ... != 0 when ... && ... is true | +| 85 | ... == ... != 0 when ... == ... is true | +| 85 | ... == ... == 0 when ... == ... is false | | 85 | x != 0 when ... == ... is false | | 85 | x != 0+0 when ... == ... is false | | 85 | x == 0 when ... && ... is true | @@ -127,12 +161,16 @@ astGuardsCompare | 85 | y == 0+0 when ... != ... is false | | 94 | 0 != x+0 when ... != ... is true | | 94 | 0 == x+0 when ... != ... is false | +| 94 | ... != ... != 0 when ... != ... is true | +| 94 | ... != ... == 0 when ... != ... is false | | 94 | x != 0 when ... != ... is true | | 94 | x != 0+0 when ... != ... is true | | 94 | x == 0 when ... != ... is false | | 94 | x == 0+0 when ... != ... is false | | 102 | 10 < j+1 when ... < ... is false | | 102 | 10 >= j+1 when ... < ... is true | +| 102 | ... < ... != 0 when ... < ... is true | +| 102 | ... < ... == 0 when ... < ... is false | | 102 | j < 10+0 when ... < ... is true | | 102 | j >= 10+0 when ... < ... is false | | 109 | 0 != x+0 when ... == ... is false | @@ -141,6 +179,12 @@ astGuardsCompare | 109 | 0 < y+1 when ... \|\| ... is false | | 109 | 0 == x+0 when ... == ... is true | | 109 | 0 >= y+1 when ... < ... is true | +| 109 | ... < ... != 0 when ... < ... is true | +| 109 | ... < ... == 0 when ... < ... is false | +| 109 | ... < ... == 0 when ... \|\| ... is false | +| 109 | ... == ... != 0 when ... == ... is true | +| 109 | ... == ... == 0 when ... == ... is false | +| 109 | ... == ... == 0 when ... \|\| ... is false | | 109 | x != 0 when ... == ... is false | | 109 | x != 0 when ... \|\| ... is false | | 109 | x != 0+0 when ... == ... is false | @@ -173,6 +217,8 @@ astGuardsCompare | 152 | y == 0 when y is false | | 156 | ... + ... != x+0 when ... == ... is false | | 156 | ... + ... == x+0 when ... == ... is true | +| 156 | ... == ... != 0 when ... == ... is true | +| 156 | ... == ... == 0 when ... == ... is false | | 156 | x != ... + ...+0 when ... == ... is false | | 156 | x != y+42 when ... == ... is false | | 156 | x == ... + ...+0 when ... == ... is true | @@ -181,6 +227,8 @@ astGuardsCompare | 156 | y == x+-42 when ... == ... is true | | 159 | ... - ... != x+0 when ... == ... is false | | 159 | ... - ... == x+0 when ... == ... is true | +| 159 | ... == ... != 0 when ... == ... is true | +| 159 | ... == ... == 0 when ... == ... is false | | 159 | x != ... - ...+0 when ... == ... is false | | 159 | x != y+-42 when ... == ... is false | | 159 | x == ... - ...+0 when ... == ... is true | @@ -189,6 +237,8 @@ astGuardsCompare | 159 | y == x+42 when ... == ... is true | | 162 | ... + ... < x+1 when ... < ... is false | | 162 | ... + ... >= x+1 when ... < ... is true | +| 162 | ... < ... != 0 when ... < ... is true | +| 162 | ... < ... == 0 when ... < ... is false | | 162 | x < ... + ...+0 when ... < ... is true | | 162 | x < y+42 when ... < ... is true | | 162 | x >= ... + ...+0 when ... < ... is false | @@ -197,6 +247,8 @@ astGuardsCompare | 162 | y >= x+-41 when ... < ... is true | | 165 | ... - ... < x+1 when ... < ... is false | | 165 | ... - ... >= x+1 when ... < ... is true | +| 165 | ... < ... != 0 when ... < ... is true | +| 165 | ... < ... == 0 when ... < ... is false | | 165 | x < ... - ...+0 when ... < ... is true | | 165 | x < y+-42 when ... < ... is true | | 165 | x >= ... - ...+0 when ... < ... is false | @@ -205,6 +257,8 @@ astGuardsCompare | 165 | y >= x+43 when ... < ... is true | | 175 | 0 != call to foo+0 when ... == ... is false | | 175 | 0 == call to foo+0 when ... == ... is true | +| 175 | ... == ... != 0 when ... == ... is true | +| 175 | ... == ... == 0 when ... == ... is false | | 175 | call to foo != 0 when ... == ... is false | | 175 | call to foo != 0+0 when ... == ... is false | | 175 | call to foo == 0 when ... == ... is true | @@ -414,10 +468,20 @@ astGuardsEnsure | test.c:75:9:75:14 | ... == ... | test.c:75:9:75:9 | x | == | test.c:75:14:75:14 | 0 | 0 | 75 | 77 | | test.c:75:9:75:14 | ... == ... | test.c:75:14:75:14 | 0 | != | test.c:75:9:75:9 | x | 0 | 78 | 79 | | test.c:75:9:75:14 | ... == ... | test.c:75:14:75:14 | 0 | == | test.c:75:9:75:9 | x | 0 | 75 | 77 | +| test.c:75:9:75:14 | ... == ... | test.c:85:8:85:8 | x | != | test.c:85:13:85:13 | 0 | 0 | 78 | 79 | +| test.c:75:9:75:14 | ... == ... | test.c:85:8:85:8 | x | == | test.c:85:13:85:13 | 0 | 0 | 75 | 77 | +| test.c:75:9:75:14 | ... == ... | test.c:85:13:85:13 | 0 | != | test.c:85:8:85:8 | x | 0 | 78 | 79 | +| test.c:75:9:75:14 | ... == ... | test.c:85:13:85:13 | 0 | == | test.c:85:8:85:8 | x | 0 | 75 | 77 | +| test.c:85:8:85:13 | ... == ... | test.c:75:9:75:9 | x | == | test.c:75:14:75:14 | 0 | 0 | 85 | 85 | +| test.c:85:8:85:13 | ... == ... | test.c:75:9:75:9 | x | == | test.c:75:14:75:14 | 0 | 0 | 86 | 86 | +| test.c:85:8:85:13 | ... == ... | test.c:75:14:75:14 | 0 | == | test.c:75:9:75:9 | x | 0 | 85 | 85 | +| test.c:85:8:85:13 | ... == ... | test.c:75:14:75:14 | 0 | == | test.c:75:9:75:9 | x | 0 | 86 | 86 | | test.c:85:8:85:13 | ... == ... | test.c:85:8:85:8 | x | == | test.c:85:13:85:13 | 0 | 0 | 85 | 85 | | test.c:85:8:85:13 | ... == ... | test.c:85:8:85:8 | x | == | test.c:85:13:85:13 | 0 | 0 | 86 | 86 | | test.c:85:8:85:13 | ... == ... | test.c:85:13:85:13 | 0 | == | test.c:85:8:85:8 | x | 0 | 85 | 85 | | test.c:85:8:85:13 | ... == ... | test.c:85:13:85:13 | 0 | == | test.c:85:8:85:8 | x | 0 | 86 | 86 | +| test.c:85:8:85:23 | ... && ... | test.c:75:9:75:9 | x | == | test.c:75:14:75:14 | 0 | 0 | 86 | 86 | +| test.c:85:8:85:23 | ... && ... | test.c:75:14:75:14 | 0 | == | test.c:75:9:75:9 | x | 0 | 86 | 86 | | test.c:85:8:85:23 | ... && ... | test.c:85:8:85:8 | x | == | test.c:85:13:85:13 | 0 | 0 | 86 | 86 | | test.c:85:8:85:23 | ... && ... | test.c:85:13:85:13 | 0 | == | test.c:85:8:85:8 | x | 0 | 86 | 86 | | test.c:85:8:85:23 | ... && ... | test.c:85:18:85:18 | y | != | test.c:85:23:85:23 | 0 | 0 | 86 | 86 | @@ -491,16 +555,81 @@ astGuardsEnsure | test.cpp:31:7:31:13 | ... == ... | test.cpp:31:12:31:13 | - ... | == | test.cpp:31:7:31:7 | x | 0 | 30 | 30 | | test.cpp:31:7:31:13 | ... == ... | test.cpp:31:12:31:13 | - ... | == | test.cpp:31:7:31:7 | x | 0 | 31 | 32 | astGuardsEnsure_const +| test.c:7:9:7:13 | ... > ... | test.c:7:9:7:13 | ... > ... | != | 0 | 7 | 9 | +| test.c:7:9:7:13 | ... > ... | test.c:7:9:7:13 | ... > ... | == | 0 | 10 | 11 | +| test.c:17:8:17:12 | ... < ... | test.c:17:8:17:12 | ... < ... | != | 0 | 17 | 17 | +| test.c:17:8:17:12 | ... < ... | test.c:17:8:17:12 | ... < ... | != | 0 | 18 | 18 | +| test.c:17:8:17:21 | ... && ... | test.c:17:8:17:12 | ... < ... | != | 0 | 18 | 18 | +| test.c:17:8:17:21 | ... && ... | test.c:17:17:17:21 | ... > ... | != | 0 | 18 | 18 | +| test.c:17:17:17:21 | ... > ... | test.c:17:17:17:21 | ... > ... | != | 0 | 18 | 18 | +| test.c:26:11:26:15 | ... > ... | test.c:26:11:26:15 | ... > ... | != | 0 | 26 | 28 | +| test.c:26:11:26:15 | ... > ... | test.c:26:11:26:15 | ... > ... | == | 0 | 2 | 2 | +| test.c:26:11:26:15 | ... > ... | test.c:26:11:26:15 | ... > ... | == | 0 | 31 | 34 | +| test.c:26:11:26:15 | ... > ... | test.c:26:11:26:15 | ... > ... | == | 0 | 34 | 34 | +| test.c:26:11:26:15 | ... > ... | test.c:26:11:26:15 | ... > ... | == | 0 | 39 | 42 | +| test.c:26:11:26:15 | ... > ... | test.c:26:11:26:15 | ... > ... | == | 0 | 42 | 42 | +| test.c:26:11:26:15 | ... > ... | test.c:26:11:26:15 | ... > ... | == | 0 | 42 | 44 | +| test.c:26:11:26:15 | ... > ... | test.c:26:11:26:15 | ... > ... | == | 0 | 45 | 45 | +| test.c:26:11:26:15 | ... > ... | test.c:26:11:26:15 | ... > ... | == | 0 | 45 | 47 | +| test.c:26:11:26:15 | ... > ... | test.c:26:11:26:15 | ... > ... | == | 0 | 51 | 53 | +| test.c:26:11:26:15 | ... > ... | test.c:26:11:26:15 | ... > ... | == | 0 | 56 | 58 | +| test.c:26:11:26:15 | ... > ... | test.c:26:11:26:15 | ... > ... | == | 0 | 58 | 58 | +| test.c:26:11:26:15 | ... > ... | test.c:26:11:26:15 | ... > ... | == | 0 | 58 | 66 | +| test.c:26:11:26:15 | ... > ... | test.c:26:11:26:15 | ... > ... | == | 0 | 62 | 62 | +| test.c:34:16:34:21 | ... < ... | test.c:34:16:34:21 | ... < ... | != | 0 | 34 | 34 | +| test.c:34:16:34:21 | ... < ... | test.c:34:16:34:21 | ... < ... | == | 0 | 2 | 2 | +| test.c:34:16:34:21 | ... < ... | test.c:34:16:34:21 | ... < ... | == | 0 | 39 | 42 | +| test.c:34:16:34:21 | ... < ... | test.c:34:16:34:21 | ... < ... | == | 0 | 42 | 42 | +| test.c:34:16:34:21 | ... < ... | test.c:34:16:34:21 | ... < ... | == | 0 | 42 | 44 | +| test.c:34:16:34:21 | ... < ... | test.c:34:16:34:21 | ... < ... | == | 0 | 45 | 45 | +| test.c:34:16:34:21 | ... < ... | test.c:34:16:34:21 | ... < ... | == | 0 | 45 | 47 | +| test.c:34:16:34:21 | ... < ... | test.c:34:16:34:21 | ... < ... | == | 0 | 51 | 53 | +| test.c:34:16:34:21 | ... < ... | test.c:34:16:34:21 | ... < ... | == | 0 | 56 | 58 | +| test.c:34:16:34:21 | ... < ... | test.c:34:16:34:21 | ... < ... | == | 0 | 58 | 58 | +| test.c:34:16:34:21 | ... < ... | test.c:34:16:34:21 | ... < ... | == | 0 | 58 | 66 | +| test.c:34:16:34:21 | ... < ... | test.c:34:16:34:21 | ... < ... | == | 0 | 62 | 62 | +| test.c:42:16:42:21 | ... < ... | test.c:42:16:42:21 | ... < ... | != | 0 | 42 | 42 | +| test.c:42:16:42:21 | ... < ... | test.c:42:16:42:21 | ... < ... | != | 0 | 42 | 44 | +| test.c:42:16:42:21 | ... < ... | test.c:42:16:42:21 | ... < ... | != | 0 | 45 | 45 | +| test.c:42:16:42:21 | ... < ... | test.c:42:16:42:21 | ... < ... | != | 0 | 45 | 47 | +| test.c:42:16:42:21 | ... < ... | test.c:42:16:42:21 | ... < ... | != | 0 | 51 | 53 | +| test.c:44:12:44:16 | ... > ... | test.c:44:12:44:16 | ... > ... | != | 0 | 45 | 45 | +| test.c:44:12:44:16 | ... > ... | test.c:44:12:44:16 | ... > ... | != | 0 | 45 | 47 | +| test.c:44:12:44:16 | ... > ... | test.c:44:12:44:16 | ... > ... | == | 0 | 42 | 42 | +| test.c:44:12:44:16 | ... > ... | test.c:44:12:44:16 | ... > ... | == | 0 | 51 | 53 | +| test.c:45:16:45:20 | ... > ... | test.c:45:16:45:20 | ... > ... | != | 0 | 45 | 47 | | test.c:58:9:58:14 | ... == ... | test.c:58:9:58:9 | x | != | 0 | 58 | 58 | | test.c:58:9:58:14 | ... == ... | test.c:58:9:58:9 | x | != | 0 | 62 | 62 | +| test.c:58:9:58:14 | ... == ... | test.c:58:9:58:14 | ... == ... | == | 0 | 58 | 58 | +| test.c:58:9:58:14 | ... == ... | test.c:58:9:58:14 | ... == ... | == | 0 | 62 | 62 | | test.c:58:9:58:23 | ... \|\| ... | test.c:58:9:58:9 | x | != | 0 | 62 | 62 | +| test.c:58:9:58:23 | ... \|\| ... | test.c:58:9:58:14 | ... == ... | == | 0 | 62 | 62 | +| test.c:58:9:58:23 | ... \|\| ... | test.c:58:19:58:23 | ... < ... | == | 0 | 62 | 62 | +| test.c:58:19:58:23 | ... < ... | test.c:58:19:58:23 | ... < ... | == | 0 | 62 | 62 | | test.c:75:9:75:14 | ... == ... | test.c:75:9:75:9 | x | != | 0 | 78 | 79 | | test.c:75:9:75:14 | ... == ... | test.c:75:9:75:9 | x | == | 0 | 75 | 77 | +| test.c:75:9:75:14 | ... == ... | test.c:75:9:75:14 | ... == ... | != | 0 | 75 | 77 | +| test.c:75:9:75:14 | ... == ... | test.c:75:9:75:14 | ... == ... | == | 0 | 78 | 79 | +| test.c:75:9:75:14 | ... == ... | test.c:85:8:85:8 | x | != | 0 | 78 | 79 | +| test.c:75:9:75:14 | ... == ... | test.c:85:8:85:8 | x | == | 0 | 75 | 77 | +| test.c:75:9:75:14 | ... == ... | test.c:85:8:85:13 | ... == ... | != | 0 | 75 | 77 | +| test.c:75:9:75:14 | ... == ... | test.c:85:8:85:13 | ... == ... | == | 0 | 78 | 79 | +| test.c:85:8:85:13 | ... == ... | test.c:75:9:75:9 | x | == | 0 | 85 | 85 | +| test.c:85:8:85:13 | ... == ... | test.c:75:9:75:9 | x | == | 0 | 86 | 86 | +| test.c:85:8:85:13 | ... == ... | test.c:75:9:75:14 | ... == ... | != | 0 | 85 | 85 | +| test.c:85:8:85:13 | ... == ... | test.c:75:9:75:14 | ... == ... | != | 0 | 86 | 86 | | test.c:85:8:85:13 | ... == ... | test.c:85:8:85:8 | x | == | 0 | 85 | 85 | | test.c:85:8:85:13 | ... == ... | test.c:85:8:85:8 | x | == | 0 | 86 | 86 | +| test.c:85:8:85:13 | ... == ... | test.c:85:8:85:13 | ... == ... | != | 0 | 85 | 85 | +| test.c:85:8:85:13 | ... == ... | test.c:85:8:85:13 | ... == ... | != | 0 | 86 | 86 | +| test.c:85:8:85:23 | ... && ... | test.c:75:9:75:9 | x | == | 0 | 86 | 86 | +| test.c:85:8:85:23 | ... && ... | test.c:75:9:75:14 | ... == ... | != | 0 | 86 | 86 | | test.c:85:8:85:23 | ... && ... | test.c:85:8:85:8 | x | == | 0 | 86 | 86 | +| test.c:85:8:85:23 | ... && ... | test.c:85:8:85:13 | ... == ... | != | 0 | 86 | 86 | | test.c:85:8:85:23 | ... && ... | test.c:85:18:85:18 | y | != | 0 | 86 | 86 | +| test.c:85:8:85:23 | ... && ... | test.c:85:18:85:23 | ... != ... | != | 0 | 86 | 86 | | test.c:85:18:85:23 | ... != ... | test.c:85:18:85:18 | y | != | 0 | 86 | 86 | +| test.c:85:18:85:23 | ... != ... | test.c:85:18:85:23 | ... != ... | != | 0 | 86 | 86 | | test.c:94:11:94:16 | ... != ... | test.c:94:11:94:11 | x | != | 0 | 94 | 96 | | test.c:94:11:94:16 | ... != ... | test.c:94:11:94:11 | x | == | 0 | 70 | 70 | | test.c:94:11:94:16 | ... != ... | test.c:94:11:94:11 | x | == | 0 | 99 | 102 | @@ -509,16 +638,41 @@ astGuardsEnsure_const | test.c:94:11:94:16 | ... != ... | test.c:94:11:94:11 | x | == | 0 | 109 | 109 | | test.c:94:11:94:16 | ... != ... | test.c:94:11:94:11 | x | == | 0 | 109 | 117 | | test.c:94:11:94:16 | ... != ... | test.c:94:11:94:11 | x | == | 0 | 113 | 113 | +| test.c:94:11:94:16 | ... != ... | test.c:94:11:94:16 | ... != ... | != | 0 | 94 | 96 | +| test.c:94:11:94:16 | ... != ... | test.c:94:11:94:16 | ... != ... | == | 0 | 70 | 70 | +| test.c:94:11:94:16 | ... != ... | test.c:94:11:94:16 | ... != ... | == | 0 | 99 | 102 | +| test.c:94:11:94:16 | ... != ... | test.c:94:11:94:16 | ... != ... | == | 0 | 102 | 102 | +| test.c:94:11:94:16 | ... != ... | test.c:94:11:94:16 | ... != ... | == | 0 | 107 | 109 | +| test.c:94:11:94:16 | ... != ... | test.c:94:11:94:16 | ... != ... | == | 0 | 109 | 109 | +| test.c:94:11:94:16 | ... != ... | test.c:94:11:94:16 | ... != ... | == | 0 | 109 | 117 | +| test.c:94:11:94:16 | ... != ... | test.c:94:11:94:16 | ... != ... | == | 0 | 113 | 113 | +| test.c:102:16:102:21 | ... < ... | test.c:102:16:102:21 | ... < ... | != | 0 | 102 | 102 | +| test.c:102:16:102:21 | ... < ... | test.c:102:16:102:21 | ... < ... | == | 0 | 70 | 70 | +| test.c:102:16:102:21 | ... < ... | test.c:102:16:102:21 | ... < ... | == | 0 | 107 | 109 | +| test.c:102:16:102:21 | ... < ... | test.c:102:16:102:21 | ... < ... | == | 0 | 109 | 109 | +| test.c:102:16:102:21 | ... < ... | test.c:102:16:102:21 | ... < ... | == | 0 | 109 | 117 | +| test.c:102:16:102:21 | ... < ... | test.c:102:16:102:21 | ... < ... | == | 0 | 113 | 113 | | test.c:109:9:109:14 | ... == ... | test.c:109:9:109:9 | x | != | 0 | 109 | 109 | | test.c:109:9:109:14 | ... == ... | test.c:109:9:109:9 | x | != | 0 | 113 | 113 | +| test.c:109:9:109:14 | ... == ... | test.c:109:9:109:14 | ... == ... | == | 0 | 109 | 109 | +| test.c:109:9:109:14 | ... == ... | test.c:109:9:109:14 | ... == ... | == | 0 | 113 | 113 | | test.c:109:9:109:23 | ... \|\| ... | test.c:109:9:109:9 | x | != | 0 | 113 | 113 | +| test.c:109:9:109:23 | ... \|\| ... | test.c:109:9:109:14 | ... == ... | == | 0 | 113 | 113 | +| test.c:109:9:109:23 | ... \|\| ... | test.c:109:19:109:23 | ... < ... | == | 0 | 113 | 113 | +| test.c:109:19:109:23 | ... < ... | test.c:109:19:109:23 | ... < ... | == | 0 | 113 | 113 | | test.c:126:7:126:7 | 1 | test.c:126:7:126:7 | 1 | != | 0 | 126 | 126 | | test.c:126:7:126:7 | 1 | test.c:126:7:126:7 | 1 | != | 0 | 126 | 128 | | test.c:126:7:126:7 | 1 | test.c:126:7:126:7 | 1 | != | 0 | 131 | 131 | | test.c:126:7:126:7 | 1 | test.c:126:7:126:7 | 1 | != | 0 | 131 | 132 | | test.c:126:7:126:7 | 1 | test.c:126:7:126:7 | 1 | != | 0 | 134 | 123 | +| test.c:126:7:126:7 | 1 | test.c:127:9:127:9 | 1 | != | 0 | 126 | 126 | +| test.c:126:7:126:7 | 1 | test.c:127:9:127:9 | 1 | != | 0 | 126 | 128 | +| test.c:126:7:126:7 | 1 | test.c:127:9:127:9 | 1 | != | 0 | 131 | 131 | +| test.c:126:7:126:7 | 1 | test.c:127:9:127:9 | 1 | != | 0 | 131 | 132 | +| test.c:126:7:126:7 | 1 | test.c:127:9:127:9 | 1 | != | 0 | 134 | 123 | | test.c:126:7:126:28 | ... && ... | test.c:126:7:126:7 | 1 | != | 0 | 126 | 128 | | test.c:126:7:126:28 | ... && ... | test.c:126:12:126:26 | call to test3_condition | != | 0 | 126 | 128 | +| test.c:126:7:126:28 | ... && ... | test.c:127:9:127:9 | 1 | != | 0 | 126 | 128 | | test.c:126:12:126:26 | call to test3_condition | test.c:126:12:126:26 | call to test3_condition | != | 0 | 126 | 128 | | 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 | @@ -529,8 +683,14 @@ astGuardsEnsure_const | test.c:152:10:152:15 | ... && ... | test.c:152:10:152:10 | x | != | 0 | 151 | 152 | | test.c:152:10:152:15 | ... && ... | test.c:152:15:152:15 | y | != | 0 | 151 | 152 | | test.c:152:15:152:15 | y | test.c:152:15:152:15 | y | != | 0 | 151 | 152 | +| test.c:156:9:156:19 | ... == ... | test.c:156:9:156:19 | ... == ... | != | 0 | 156 | 157 | +| test.c:159:9:159:19 | ... == ... | test.c:159:9:159:19 | ... == ... | != | 0 | 159 | 160 | +| test.c:162:9:162:18 | ... < ... | test.c:162:9:162:18 | ... < ... | != | 0 | 162 | 163 | +| test.c:165:9:165:18 | ... < ... | test.c:165:9:165:18 | ... < ... | != | 0 | 165 | 166 | | test.c:175:13:175:32 | ... == ... | test.c:175:13:175:15 | call to foo | != | 0 | 175 | 175 | | test.c:175:13:175:32 | ... == ... | test.c:175:13:175:15 | call to foo | == | 0 | 175 | 175 | +| test.c:175:13:175:32 | ... == ... | test.c:175:13:175:32 | ... == ... | != | 0 | 175 | 175 | +| test.c:175:13:175:32 | ... == ... | test.c:175:13:175:32 | ... == ... | == | 0 | 175 | 175 | | test.c:181:9:181:9 | x | test.c:181:9:181:9 | x | != | 0 | 181 | 182 | | test.c:181:9:181:9 | x | test.c:181:9:181:9 | x | != | 0 | 186 | 180 | | test.c:181:9:181:9 | x | test.c:181:9:181:9 | x | == | 0 | 183 | 184 | @@ -539,6 +699,10 @@ astGuardsEnsure_const | test.cpp:31:7:31:13 | ... == ... | test.cpp:31:7:31:7 | x | != | -1 | 34 | 34 | | 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 | 31 | 32 | +| test.cpp:31:7:31:13 | ... == ... | test.cpp:31:7:31:13 | ... == ... | != | 0 | 30 | 30 | +| test.cpp:31:7:31:13 | ... == ... | test.cpp:31:7:31:13 | ... == ... | != | 0 | 31 | 32 | +| test.cpp:31:7:31:13 | ... == ... | test.cpp:31:7:31:13 | ... == ... | == | 0 | 30 | 30 | +| test.cpp:31:7:31:13 | ... == ... | test.cpp:31:7:31:13 | ... == ... | == | 0 | 34 | 34 | | test.cpp:42:13:42:20 | call to getABool | test.cpp:42:13:42:20 | call to getABool | != | 0 | 43 | 45 | | test.cpp:42:13:42:20 | call to getABool | test.cpp:42:13:42:20 | call to getABool | == | 0 | 53 | 53 | irGuards @@ -579,6 +743,8 @@ irGuards irGuardsCompare | 7 | 0 < x+0 when CompareGT: ... > ... is true | | 7 | 0 >= x+0 when CompareGT: ... > ... is false | +| 7 | ... > ... != 0 when CompareGT: ... > ... is true | +| 7 | ... > ... == 0 when CompareGT: ... > ... is false | | 7 | x < 0+1 when CompareGT: ... > ... is false | | 7 | x < 1 when CompareGT: ... > ... is false | | 7 | x >= 0+1 when CompareGT: ... > ... is true | @@ -587,6 +753,10 @@ irGuardsCompare | 17 | 0 >= x+1 when CompareLT: ... < ... is true | | 17 | 1 < y+0 when CompareGT: ... > ... is true | | 17 | 1 >= y+0 when CompareGT: ... > ... is false | +| 17 | ... < ... != 0 when CompareLT: ... < ... is true | +| 17 | ... < ... == 0 when CompareLT: ... < ... is false | +| 17 | ... > ... != 0 when CompareGT: ... > ... is true | +| 17 | ... > ... == 0 when CompareGT: ... > ... is false | | 17 | x < 0 when CompareLT: ... < ... is true | | 17 | x < 0+0 when CompareLT: ... < ... is true | | 17 | x >= 0 when CompareLT: ... < ... is false | @@ -599,24 +769,32 @@ irGuardsCompare | 18 | call to get == 0 when CompareNE: (bool)... is false | | 26 | 0 < x+0 when CompareGT: ... > ... is true | | 26 | 0 >= x+0 when CompareGT: ... > ... is false | +| 26 | ... > ... != 0 when CompareGT: ... > ... is true | +| 26 | ... > ... == 0 when CompareGT: ... > ... is false | | 26 | x < 0+1 when CompareGT: ... > ... is false | | 26 | x < 1 when CompareGT: ... > ... is false | | 26 | x >= 0+1 when CompareGT: ... > ... is true | | 26 | x >= 1 when CompareGT: ... > ... is true | | 31 | - ... != x+0 when CompareEQ: ... == ... is false | | 31 | - ... == x+0 when CompareEQ: ... == ... is true | +| 31 | ... == ... != 0 when CompareEQ: ... == ... is true | +| 31 | ... == ... == 0 when CompareEQ: ... == ... is false | | 31 | x != -1 when CompareEQ: ... == ... is false | | 31 | x != - ...+0 when CompareEQ: ... == ... is false | | 31 | x == -1 when CompareEQ: ... == ... is true | | 31 | x == - ...+0 when CompareEQ: ... == ... is true | | 34 | 10 < j+1 when CompareLT: ... < ... is false | | 34 | 10 >= j+1 when CompareLT: ... < ... is true | +| 34 | ... < ... != 0 when CompareLT: ... < ... is true | +| 34 | ... < ... == 0 when CompareLT: ... < ... is false | | 34 | j < 10 when CompareLT: ... < ... is true | | 34 | j < 10+0 when CompareLT: ... < ... is true | | 34 | j >= 10 when CompareLT: ... < ... is false | | 34 | j >= 10+0 when CompareLT: ... < ... is false | | 42 | 10 < j+1 when CompareLT: ... < ... is false | | 42 | 10 >= j+1 when CompareLT: ... < ... is true | +| 42 | ... < ... != 0 when CompareLT: ... < ... is true | +| 42 | ... < ... == 0 when CompareLT: ... < ... is false | | 42 | call to getABool != 0 when Call: call to getABool is true | | 42 | call to getABool == 0 when Call: call to getABool is false | | 42 | j < 10 when CompareLT: ... < ... is true | @@ -625,12 +803,16 @@ irGuardsCompare | 42 | j >= 10+0 when CompareLT: ... < ... is false | | 44 | 0 < z+0 when CompareGT: ... > ... is true | | 44 | 0 >= z+0 when CompareGT: ... > ... is false | +| 44 | ... > ... != 0 when CompareGT: ... > ... is true | +| 44 | ... > ... == 0 when CompareGT: ... > ... is false | | 44 | z < 0+1 when CompareGT: ... > ... is false | | 44 | z < 1 when CompareGT: ... > ... is false | | 44 | z >= 0+1 when CompareGT: ... > ... is true | | 44 | z >= 1 when CompareGT: ... > ... is true | | 45 | 0 < y+0 when CompareGT: ... > ... is true | | 45 | 0 >= y+0 when CompareGT: ... > ... is false | +| 45 | ... > ... != 0 when CompareGT: ... > ... is true | +| 45 | ... > ... == 0 when CompareGT: ... > ... is false | | 45 | y < 0+1 when CompareGT: ... > ... is false | | 45 | y < 1 when CompareGT: ... > ... is false | | 45 | y >= 0+1 when CompareGT: ... > ... is true | @@ -639,6 +821,10 @@ irGuardsCompare | 58 | 0 < y+1 when CompareLT: ... < ... is false | | 58 | 0 == x+0 when CompareEQ: ... == ... is true | | 58 | 0 >= y+1 when CompareLT: ... < ... is true | +| 58 | ... < ... != 0 when CompareLT: ... < ... is true | +| 58 | ... < ... == 0 when CompareLT: ... < ... is false | +| 58 | ... == ... != 0 when CompareEQ: ... == ... is true | +| 58 | ... == ... == 0 when CompareEQ: ... == ... is false | | 58 | x != 0 when CompareEQ: ... == ... is false | | 58 | x != 0+0 when CompareEQ: ... == ... is false | | 58 | x == 0 when CompareEQ: ... == ... is true | @@ -649,6 +835,8 @@ irGuardsCompare | 58 | y >= 0+0 when CompareLT: ... < ... is false | | 75 | 0 != x+0 when CompareEQ: ... == ... is false | | 75 | 0 == x+0 when CompareEQ: ... == ... is true | +| 75 | ... == ... != 0 when CompareEQ: ... == ... is true | +| 75 | ... == ... == 0 when CompareEQ: ... == ... is false | | 75 | x != 0 when CompareEQ: ... == ... is false | | 75 | x != 0+0 when CompareEQ: ... == ... is false | | 75 | x == 0 when CompareEQ: ... == ... is true | @@ -657,6 +845,10 @@ irGuardsCompare | 85 | 0 != y+0 when CompareNE: ... != ... is true | | 85 | 0 == x+0 when CompareEQ: ... == ... is true | | 85 | 0 == y+0 when CompareNE: ... != ... is false | +| 85 | ... != ... != 0 when CompareNE: ... != ... is true | +| 85 | ... != ... == 0 when CompareNE: ... != ... is false | +| 85 | ... == ... != 0 when CompareEQ: ... == ... is true | +| 85 | ... == ... == 0 when CompareEQ: ... == ... is false | | 85 | x != 0 when CompareEQ: ... == ... is false | | 85 | x != 0+0 when CompareEQ: ... == ... is false | | 85 | x == 0 when CompareEQ: ... == ... is true | @@ -667,12 +859,16 @@ irGuardsCompare | 85 | y == 0+0 when CompareNE: ... != ... is false | | 94 | 0 != x+0 when CompareNE: ... != ... is true | | 94 | 0 == x+0 when CompareNE: ... != ... is false | +| 94 | ... != ... != 0 when CompareNE: ... != ... is true | +| 94 | ... != ... == 0 when CompareNE: ... != ... is false | | 94 | x != 0 when CompareNE: ... != ... is true | | 94 | x != 0+0 when CompareNE: ... != ... is true | | 94 | x == 0 when CompareNE: ... != ... is false | | 94 | x == 0+0 when CompareNE: ... != ... is false | | 102 | 10 < j+1 when CompareLT: ... < ... is false | | 102 | 10 >= j+1 when CompareLT: ... < ... is true | +| 102 | ... < ... != 0 when CompareLT: ... < ... is true | +| 102 | ... < ... == 0 when CompareLT: ... < ... is false | | 102 | j < 10 when CompareLT: ... < ... is true | | 102 | j < 10+0 when CompareLT: ... < ... is true | | 102 | j >= 10 when CompareLT: ... < ... is false | @@ -681,6 +877,10 @@ irGuardsCompare | 109 | 0 < y+1 when CompareLT: ... < ... is false | | 109 | 0 == x+0 when CompareEQ: ... == ... is true | | 109 | 0 >= y+1 when CompareLT: ... < ... is true | +| 109 | ... < ... != 0 when CompareLT: ... < ... is true | +| 109 | ... < ... == 0 when CompareLT: ... < ... is false | +| 109 | ... == ... != 0 when CompareEQ: ... == ... is true | +| 109 | ... == ... == 0 when CompareEQ: ... == ... is false | | 109 | x != 0 when CompareEQ: ... == ... is false | | 109 | x != 0+0 when CompareEQ: ... == ... is false | | 109 | x == 0 when CompareEQ: ... == ... is true | @@ -708,6 +908,8 @@ irGuardsCompare | 152 | y == 0 when Load: y is false | | 156 | ... + ... != x+0 when CompareEQ: ... == ... is false | | 156 | ... + ... == x+0 when CompareEQ: ... == ... is true | +| 156 | ... == ... != 0 when CompareEQ: ... == ... is true | +| 156 | ... == ... == 0 when CompareEQ: ... == ... is false | | 156 | x != ... + ...+0 when CompareEQ: ... == ... is false | | 156 | x != y+42 when CompareEQ: ... == ... is false | | 156 | x == ... + ...+0 when CompareEQ: ... == ... is true | @@ -716,6 +918,8 @@ irGuardsCompare | 156 | y == x+-42 when CompareEQ: ... == ... is true | | 159 | ... - ... != x+0 when CompareEQ: ... == ... is false | | 159 | ... - ... == x+0 when CompareEQ: ... == ... is true | +| 159 | ... == ... != 0 when CompareEQ: ... == ... is true | +| 159 | ... == ... == 0 when CompareEQ: ... == ... is false | | 159 | x != ... - ...+0 when CompareEQ: ... == ... is false | | 159 | x != y+-42 when CompareEQ: ... == ... is false | | 159 | x == ... - ...+0 when CompareEQ: ... == ... is true | @@ -724,6 +928,8 @@ irGuardsCompare | 159 | y == x+42 when CompareEQ: ... == ... is true | | 162 | ... + ... < x+1 when CompareLT: ... < ... is false | | 162 | ... + ... >= x+1 when CompareLT: ... < ... is true | +| 162 | ... < ... != 0 when CompareLT: ... < ... is true | +| 162 | ... < ... == 0 when CompareLT: ... < ... is false | | 162 | x < ... + ...+0 when CompareLT: ... < ... is true | | 162 | x < y+42 when CompareLT: ... < ... is true | | 162 | x >= ... + ...+0 when CompareLT: ... < ... is false | @@ -732,6 +938,8 @@ irGuardsCompare | 162 | y >= x+-41 when CompareLT: ... < ... is true | | 165 | ... - ... < x+1 when CompareLT: ... < ... is false | | 165 | ... - ... >= x+1 when CompareLT: ... < ... is true | +| 165 | ... < ... != 0 when CompareLT: ... < ... is true | +| 165 | ... < ... == 0 when CompareLT: ... < ... is false | | 165 | x < ... - ...+0 when CompareLT: ... < ... is true | | 165 | x < y+-42 when CompareLT: ... < ... is true | | 165 | x >= ... - ...+0 when CompareLT: ... < ... is false | @@ -740,6 +948,8 @@ irGuardsCompare | 165 | y >= x+43 when CompareLT: ... < ... is true | | 175 | 0 != call to foo+0 when CompareEQ: ... == ... is false | | 175 | 0 == call to foo+0 when CompareEQ: ... == ... is true | +| 175 | ... == ... != 0 when CompareEQ: ... == ... is true | +| 175 | ... == ... == 0 when CompareEQ: ... == ... is false | | 175 | call to foo != 0 when CompareEQ: ... == ... is false | | 175 | call to foo != 0+0 when CompareEQ: ... == ... is false | | 175 | call to foo == 0 when CompareEQ: ... == ... is true | @@ -930,6 +1140,14 @@ irGuardsEnsure | test.c:75:9:75:14 | CompareEQ: ... == ... | test.c:75:9:75:9 | Load: x | == | test.c:75:14:75:14 | Constant: 0 | 0 | 76 | 76 | | test.c:75:9:75:14 | CompareEQ: ... == ... | test.c:75:14:75:14 | Constant: 0 | != | test.c:75:9:75:9 | Load: x | 0 | 79 | 79 | | test.c:75:9:75:14 | CompareEQ: ... == ... | test.c:75:14:75:14 | Constant: 0 | == | test.c:75:9:75:9 | Load: x | 0 | 76 | 76 | +| test.c:75:9:75:14 | CompareEQ: ... == ... | test.c:85:8:85:8 | Load: x | != | test.c:85:13:85:13 | Constant: 0 | 0 | 79 | 79 | +| test.c:75:9:75:14 | CompareEQ: ... == ... | test.c:85:8:85:8 | Load: x | == | test.c:85:13:85:13 | Constant: 0 | 0 | 76 | 76 | +| test.c:75:9:75:14 | CompareEQ: ... == ... | test.c:85:13:85:13 | Constant: 0 | != | test.c:85:8:85:8 | Load: x | 0 | 79 | 79 | +| test.c:75:9:75:14 | CompareEQ: ... == ... | test.c:85:13:85:13 | Constant: 0 | == | test.c:85:8:85:8 | Load: x | 0 | 76 | 76 | +| test.c:85:8:85:13 | CompareEQ: ... == ... | test.c:75:9:75:9 | Load: x | == | test.c:75:14:75:14 | Constant: 0 | 0 | 85 | 85 | +| test.c:85:8:85:13 | CompareEQ: ... == ... | test.c:75:9:75:9 | Load: x | == | test.c:75:14:75:14 | Constant: 0 | 0 | 86 | 86 | +| test.c:85:8:85:13 | CompareEQ: ... == ... | test.c:75:14:75:14 | Constant: 0 | == | test.c:75:9:75:9 | Load: x | 0 | 85 | 85 | +| test.c:85:8:85:13 | CompareEQ: ... == ... | test.c:75:14:75:14 | Constant: 0 | == | test.c:75:9:75:9 | Load: x | 0 | 86 | 86 | | test.c:85:8:85:13 | CompareEQ: ... == ... | test.c:85:8:85:8 | Load: x | == | test.c:85:13:85:13 | Constant: 0 | 0 | 85 | 85 | | test.c:85:8:85:13 | CompareEQ: ... == ... | test.c:85:8:85:8 | Load: x | == | test.c:85:13:85:13 | Constant: 0 | 0 | 86 | 86 | | test.c:85:8:85:13 | CompareEQ: ... == ... | test.c:85:13:85:13 | Constant: 0 | == | test.c:85:8:85:8 | Load: x | 0 | 85 | 85 | @@ -1003,9 +1221,14 @@ irGuardsEnsure irGuardsEnsure_const | test.c:7:9:7:13 | CompareGT: ... > ... | test.c:7:9:7:9 | Load: x | < | 1 | 11 | 11 | | test.c:7:9:7:13 | CompareGT: ... > ... | test.c:7:9:7:9 | Load: x | >= | 1 | 8 | 8 | +| test.c:7:9:7:13 | CompareGT: ... > ... | test.c:7:9:7:13 | CompareGT: ... > ... | != | 0 | 8 | 8 | +| test.c:7:9:7:13 | CompareGT: ... > ... | test.c:7:9:7:13 | CompareGT: ... > ... | == | 0 | 11 | 11 | | test.c:17:8:17:12 | CompareLT: ... < ... | test.c:17:8:17:8 | Load: x | < | 0 | 17 | 17 | | test.c:17:8:17:12 | CompareLT: ... < ... | test.c:17:8:17:8 | Load: x | < | 0 | 18 | 18 | +| test.c:17:8:17:12 | CompareLT: ... < ... | test.c:17:8:17:12 | CompareLT: ... < ... | != | 0 | 17 | 17 | +| test.c:17:8:17:12 | CompareLT: ... < ... | test.c:17:8:17:12 | CompareLT: ... < ... | != | 0 | 18 | 18 | | test.c:17:17:17:21 | CompareGT: ... > ... | test.c:17:17:17:17 | Load: y | >= | 2 | 18 | 18 | +| test.c:17:17:17:21 | CompareGT: ... > ... | test.c:17:17:17:21 | CompareGT: ... > ... | != | 0 | 18 | 18 | | test.c:26:11:26:15 | CompareGT: ... > ... | test.c:26:11:26:11 | Load: x | < | 1 | 2 | 2 | | test.c:26:11:26:15 | CompareGT: ... > ... | test.c:26:11:26:11 | Load: x | < | 1 | 31 | 31 | | test.c:26:11:26:15 | CompareGT: ... > ... | test.c:26:11:26:11 | Load: x | < | 1 | 34 | 34 | @@ -1021,6 +1244,21 @@ irGuardsEnsure_const | test.c:26:11:26:15 | CompareGT: ... > ... | test.c:26:11:26:11 | Load: x | < | 1 | 59 | 59 | | test.c:26:11:26:15 | CompareGT: ... > ... | test.c:26:11:26:11 | Load: x | < | 1 | 62 | 62 | | test.c:26:11:26:15 | CompareGT: ... > ... | test.c:26:11:26:11 | Load: x | >= | 1 | 27 | 27 | +| test.c:26:11:26:15 | CompareGT: ... > ... | test.c:26:11:26:15 | CompareGT: ... > ... | != | 0 | 27 | 27 | +| test.c:26:11:26:15 | CompareGT: ... > ... | test.c:26:11:26:15 | CompareGT: ... > ... | == | 0 | 2 | 2 | +| test.c:26:11:26:15 | CompareGT: ... > ... | test.c:26:11:26:15 | CompareGT: ... > ... | == | 0 | 31 | 31 | +| test.c:26:11:26:15 | CompareGT: ... > ... | test.c:26:11:26:15 | CompareGT: ... > ... | == | 0 | 34 | 34 | +| test.c:26:11:26:15 | CompareGT: ... > ... | test.c:26:11:26:15 | CompareGT: ... > ... | == | 0 | 35 | 35 | +| test.c:26:11:26:15 | CompareGT: ... > ... | test.c:26:11:26:15 | CompareGT: ... > ... | == | 0 | 39 | 39 | +| test.c:26:11:26:15 | CompareGT: ... > ... | test.c:26:11:26:15 | CompareGT: ... > ... | == | 0 | 42 | 42 | +| test.c:26:11:26:15 | CompareGT: ... > ... | test.c:26:11:26:15 | CompareGT: ... > ... | == | 0 | 43 | 43 | +| test.c:26:11:26:15 | CompareGT: ... > ... | test.c:26:11:26:15 | CompareGT: ... > ... | == | 0 | 45 | 45 | +| test.c:26:11:26:15 | CompareGT: ... > ... | test.c:26:11:26:15 | CompareGT: ... > ... | == | 0 | 46 | 46 | +| test.c:26:11:26:15 | CompareGT: ... > ... | test.c:26:11:26:15 | CompareGT: ... > ... | == | 0 | 52 | 52 | +| test.c:26:11:26:15 | CompareGT: ... > ... | test.c:26:11:26:15 | CompareGT: ... > ... | == | 0 | 56 | 56 | +| test.c:26:11:26:15 | CompareGT: ... > ... | test.c:26:11:26:15 | CompareGT: ... > ... | == | 0 | 58 | 58 | +| test.c:26:11:26:15 | CompareGT: ... > ... | test.c:26:11:26:15 | CompareGT: ... > ... | == | 0 | 59 | 59 | +| test.c:26:11:26:15 | CompareGT: ... > ... | test.c:26:11:26:15 | CompareGT: ... > ... | == | 0 | 62 | 62 | | test.c:34:16:34:21 | CompareLT: ... < ... | test.c:34:16:34:16 | Load: j | < | 10 | 35 | 35 | | test.c:34:16:34:21 | CompareLT: ... < ... | test.c:34:16:34:16 | Load: j | >= | 10 | 2 | 2 | | test.c:34:16:34:21 | CompareLT: ... < ... | test.c:34:16:34:16 | Load: j | >= | 10 | 39 | 39 | @@ -1033,22 +1271,58 @@ irGuardsEnsure_const | test.c:34:16:34:21 | CompareLT: ... < ... | test.c:34:16:34:16 | Load: j | >= | 10 | 58 | 58 | | test.c:34:16:34:21 | CompareLT: ... < ... | test.c:34:16:34:16 | Load: j | >= | 10 | 59 | 59 | | test.c:34:16:34:21 | CompareLT: ... < ... | test.c:34:16:34:16 | Load: j | >= | 10 | 62 | 62 | +| test.c:34:16:34:21 | CompareLT: ... < ... | test.c:34:16:34:21 | CompareLT: ... < ... | != | 0 | 35 | 35 | +| test.c:34:16:34:21 | CompareLT: ... < ... | test.c:34:16:34:21 | CompareLT: ... < ... | == | 0 | 2 | 2 | +| test.c:34:16:34:21 | CompareLT: ... < ... | test.c:34:16:34:21 | CompareLT: ... < ... | == | 0 | 39 | 39 | +| test.c:34:16:34:21 | CompareLT: ... < ... | test.c:34:16:34:21 | CompareLT: ... < ... | == | 0 | 42 | 42 | +| test.c:34:16:34:21 | CompareLT: ... < ... | test.c:34:16:34:21 | CompareLT: ... < ... | == | 0 | 43 | 43 | +| test.c:34:16:34:21 | CompareLT: ... < ... | test.c:34:16:34:21 | CompareLT: ... < ... | == | 0 | 45 | 45 | +| test.c:34:16:34:21 | CompareLT: ... < ... | test.c:34:16:34:21 | CompareLT: ... < ... | == | 0 | 46 | 46 | +| test.c:34:16:34:21 | CompareLT: ... < ... | test.c:34:16:34:21 | CompareLT: ... < ... | == | 0 | 52 | 52 | +| test.c:34:16:34:21 | CompareLT: ... < ... | test.c:34:16:34:21 | CompareLT: ... < ... | == | 0 | 56 | 56 | +| test.c:34:16:34:21 | CompareLT: ... < ... | test.c:34:16:34:21 | CompareLT: ... < ... | == | 0 | 58 | 58 | +| test.c:34:16:34:21 | CompareLT: ... < ... | test.c:34:16:34:21 | CompareLT: ... < ... | == | 0 | 59 | 59 | +| test.c:34:16:34:21 | CompareLT: ... < ... | test.c:34:16:34:21 | CompareLT: ... < ... | == | 0 | 62 | 62 | | test.c:42:16:42:21 | CompareLT: ... < ... | test.c:42:16:42:16 | Load: j | < | 10 | 43 | 43 | | test.c:42:16:42:21 | CompareLT: ... < ... | test.c:42:16:42:16 | Load: j | < | 10 | 45 | 45 | | test.c:42:16:42:21 | CompareLT: ... < ... | test.c:42:16:42:16 | Load: j | < | 10 | 46 | 46 | | test.c:42:16:42:21 | CompareLT: ... < ... | test.c:42:16:42:16 | Load: j | < | 10 | 52 | 52 | +| test.c:42:16:42:21 | CompareLT: ... < ... | test.c:42:16:42:21 | CompareLT: ... < ... | != | 0 | 43 | 43 | +| test.c:42:16:42:21 | CompareLT: ... < ... | test.c:42:16:42:21 | CompareLT: ... < ... | != | 0 | 45 | 45 | +| test.c:42:16:42:21 | CompareLT: ... < ... | test.c:42:16:42:21 | CompareLT: ... < ... | != | 0 | 46 | 46 | +| test.c:42:16:42:21 | CompareLT: ... < ... | test.c:42:16:42:21 | CompareLT: ... < ... | != | 0 | 52 | 52 | | test.c:44:12:44:16 | CompareGT: ... > ... | test.c:44:12:44:12 | Load: z | < | 1 | 52 | 52 | | test.c:44:12:44:16 | CompareGT: ... > ... | test.c:44:12:44:12 | Load: z | >= | 1 | 45 | 45 | | test.c:44:12:44:16 | CompareGT: ... > ... | test.c:44:12:44:12 | Load: z | >= | 1 | 46 | 46 | +| test.c:44:12:44:16 | CompareGT: ... > ... | test.c:44:12:44:16 | CompareGT: ... > ... | != | 0 | 45 | 45 | +| test.c:44:12:44:16 | CompareGT: ... > ... | test.c:44:12:44:16 | CompareGT: ... > ... | != | 0 | 46 | 46 | +| test.c:44:12:44:16 | CompareGT: ... > ... | test.c:44:12:44:16 | CompareGT: ... > ... | == | 0 | 52 | 52 | | test.c:45:16:45:20 | CompareGT: ... > ... | test.c:45:16:45:16 | Load: y | >= | 1 | 46 | 46 | +| test.c:45:16:45:20 | CompareGT: ... > ... | test.c:45:16:45:20 | CompareGT: ... > ... | != | 0 | 46 | 46 | | test.c:58:9:58:14 | CompareEQ: ... == ... | test.c:58:9:58:9 | Load: x | != | 0 | 58 | 58 | | test.c:58:9:58:14 | CompareEQ: ... == ... | test.c:58:9:58:9 | Load: x | != | 0 | 62 | 62 | +| test.c:58:9:58:14 | CompareEQ: ... == ... | test.c:58:9:58:14 | CompareEQ: ... == ... | == | 0 | 58 | 58 | +| test.c:58:9:58:14 | CompareEQ: ... == ... | test.c:58:9:58:14 | CompareEQ: ... == ... | == | 0 | 62 | 62 | | test.c:58:19:58:23 | CompareLT: ... < ... | test.c:58:19:58:19 | Load: y | >= | 0 | 62 | 62 | +| test.c:58:19:58:23 | CompareLT: ... < ... | test.c:58:19:58:23 | CompareLT: ... < ... | == | 0 | 62 | 62 | | test.c:75:9:75:14 | CompareEQ: ... == ... | test.c:75:9:75:9 | Load: x | != | 0 | 79 | 79 | | test.c:75:9:75:14 | CompareEQ: ... == ... | test.c:75:9:75:9 | Load: x | == | 0 | 76 | 76 | +| test.c:75:9:75:14 | CompareEQ: ... == ... | test.c:75:9:75:14 | CompareEQ: ... == ... | != | 0 | 76 | 76 | +| test.c:75:9:75:14 | CompareEQ: ... == ... | test.c:75:9:75:14 | CompareEQ: ... == ... | == | 0 | 79 | 79 | +| test.c:75:9:75:14 | CompareEQ: ... == ... | test.c:85:8:85:8 | Load: x | != | 0 | 79 | 79 | +| test.c:75:9:75:14 | CompareEQ: ... == ... | test.c:85:8:85:8 | Load: x | == | 0 | 76 | 76 | +| test.c:75:9:75:14 | CompareEQ: ... == ... | test.c:85:8:85:13 | CompareEQ: ... == ... | != | 0 | 76 | 76 | +| test.c:75:9:75:14 | CompareEQ: ... == ... | test.c:85:8:85:13 | CompareEQ: ... == ... | == | 0 | 79 | 79 | +| test.c:85:8:85:13 | CompareEQ: ... == ... | test.c:75:9:75:9 | Load: x | == | 0 | 85 | 85 | +| test.c:85:8:85:13 | CompareEQ: ... == ... | test.c:75:9:75:9 | Load: x | == | 0 | 86 | 86 | +| test.c:85:8:85:13 | CompareEQ: ... == ... | test.c:75:9:75:14 | CompareEQ: ... == ... | != | 0 | 85 | 85 | +| test.c:85:8:85:13 | CompareEQ: ... == ... | test.c:75:9:75:14 | CompareEQ: ... == ... | != | 0 | 86 | 86 | | test.c:85:8:85:13 | CompareEQ: ... == ... | test.c:85:8:85:8 | Load: x | == | 0 | 85 | 85 | | test.c:85:8:85:13 | CompareEQ: ... == ... | test.c:85:8:85:8 | Load: x | == | 0 | 86 | 86 | +| test.c:85:8:85:13 | CompareEQ: ... == ... | test.c:85:8:85:13 | CompareEQ: ... == ... | != | 0 | 85 | 85 | +| test.c:85:8:85:13 | CompareEQ: ... == ... | test.c:85:8:85:13 | CompareEQ: ... == ... | != | 0 | 86 | 86 | | test.c:85:18:85:23 | CompareNE: ... != ... | test.c:85:18:85:18 | Load: y | != | 0 | 86 | 86 | +| test.c:85:18:85:23 | CompareNE: ... != ... | test.c:85:18:85:23 | CompareNE: ... != ... | != | 0 | 86 | 86 | | test.c:94:11:94:16 | CompareNE: ... != ... | test.c:94:11:94:11 | Load: x | != | 0 | 95 | 95 | | test.c:94:11:94:16 | CompareNE: ... != ... | test.c:94:11:94:11 | Load: x | == | 0 | 70 | 70 | | test.c:94:11:94:16 | CompareNE: ... != ... | test.c:94:11:94:11 | Load: x | == | 0 | 99 | 99 | @@ -1058,34 +1332,78 @@ irGuardsEnsure_const | test.c:94:11:94:16 | CompareNE: ... != ... | test.c:94:11:94:11 | Load: x | == | 0 | 109 | 109 | | test.c:94:11:94:16 | CompareNE: ... != ... | test.c:94:11:94:11 | Load: x | == | 0 | 110 | 110 | | test.c:94:11:94:16 | CompareNE: ... != ... | test.c:94:11:94:11 | Load: x | == | 0 | 113 | 113 | +| test.c:94:11:94:16 | CompareNE: ... != ... | test.c:94:11:94:16 | CompareNE: ... != ... | != | 0 | 95 | 95 | +| test.c:94:11:94:16 | CompareNE: ... != ... | test.c:94:11:94:16 | CompareNE: ... != ... | == | 0 | 70 | 70 | +| test.c:94:11:94:16 | CompareNE: ... != ... | test.c:94:11:94:16 | CompareNE: ... != ... | == | 0 | 99 | 99 | +| test.c:94:11:94:16 | CompareNE: ... != ... | test.c:94:11:94:16 | CompareNE: ... != ... | == | 0 | 102 | 102 | +| test.c:94:11:94:16 | CompareNE: ... != ... | test.c:94:11:94:16 | CompareNE: ... != ... | == | 0 | 103 | 103 | +| test.c:94:11:94:16 | CompareNE: ... != ... | test.c:94:11:94:16 | CompareNE: ... != ... | == | 0 | 107 | 107 | +| test.c:94:11:94:16 | CompareNE: ... != ... | test.c:94:11:94:16 | CompareNE: ... != ... | == | 0 | 109 | 109 | +| test.c:94:11:94:16 | CompareNE: ... != ... | test.c:94:11:94:16 | CompareNE: ... != ... | == | 0 | 110 | 110 | +| test.c:94:11:94:16 | CompareNE: ... != ... | test.c:94:11:94:16 | CompareNE: ... != ... | == | 0 | 113 | 113 | | test.c:102:16:102:21 | CompareLT: ... < ... | test.c:102:16:102:16 | Load: j | < | 10 | 103 | 103 | | test.c:102:16:102:21 | CompareLT: ... < ... | test.c:102:16:102:16 | Load: j | >= | 10 | 70 | 70 | | test.c:102:16:102:21 | CompareLT: ... < ... | test.c:102:16:102:16 | Load: j | >= | 10 | 107 | 107 | | test.c:102:16:102:21 | CompareLT: ... < ... | test.c:102:16:102:16 | Load: j | >= | 10 | 109 | 109 | | test.c:102:16:102:21 | CompareLT: ... < ... | test.c:102:16:102:16 | Load: j | >= | 10 | 110 | 110 | | test.c:102:16:102:21 | CompareLT: ... < ... | test.c:102:16:102:16 | Load: j | >= | 10 | 113 | 113 | +| test.c:102:16:102:21 | CompareLT: ... < ... | test.c:102:16:102:21 | CompareLT: ... < ... | != | 0 | 103 | 103 | +| test.c:102:16:102:21 | CompareLT: ... < ... | test.c:102:16:102:21 | CompareLT: ... < ... | == | 0 | 70 | 70 | +| test.c:102:16:102:21 | CompareLT: ... < ... | test.c:102:16:102:21 | CompareLT: ... < ... | == | 0 | 107 | 107 | +| test.c:102:16:102:21 | CompareLT: ... < ... | test.c:102:16:102:21 | CompareLT: ... < ... | == | 0 | 109 | 109 | +| test.c:102:16:102:21 | CompareLT: ... < ... | test.c:102:16:102:21 | CompareLT: ... < ... | == | 0 | 110 | 110 | +| test.c:102:16:102:21 | CompareLT: ... < ... | test.c:102:16:102:21 | CompareLT: ... < ... | == | 0 | 113 | 113 | | test.c:109:9:109:14 | CompareEQ: ... == ... | test.c:109:9:109:9 | Load: x | != | 0 | 109 | 109 | | test.c:109:9:109:14 | CompareEQ: ... == ... | test.c:109:9:109:9 | Load: x | != | 0 | 113 | 113 | +| test.c:109:9:109:14 | CompareEQ: ... == ... | test.c:109:9:109:14 | CompareEQ: ... == ... | == | 0 | 109 | 109 | +| test.c:109:9:109:14 | CompareEQ: ... == ... | test.c:109:9:109:14 | CompareEQ: ... == ... | == | 0 | 113 | 113 | | test.c:109:19:109:23 | CompareLT: ... < ... | test.c:109:19:109:19 | Load: y | >= | 0 | 113 | 113 | +| test.c:109:19:109:23 | CompareLT: ... < ... | test.c:109:19:109:23 | CompareLT: ... < ... | == | 0 | 113 | 113 | | test.c:126:7:126:7 | Constant: 1 | test.c:126:7:126:7 | Constant: 1 | != | 0 | 126 | 126 | | test.c:126:7:126:7 | Constant: 1 | test.c:126:7:126:7 | Constant: 1 | != | 0 | 127 | 127 | | test.c:126:7:126:7 | Constant: 1 | test.c:126:7:126:7 | Constant: 1 | != | 0 | 131 | 131 | | test.c:126:7:126:7 | Constant: 1 | test.c:126:7:126:7 | Constant: 1 | != | 0 | 132 | 132 | | test.c:126:7:126:7 | Constant: 1 | test.c:126:7:126:7 | Constant: 1 | != | 0 | 134 | 134 | +| test.c:126:7:126:7 | Constant: 1 | test.c:127:5:127:9 | Store: ... = ... | != | 0 | 126 | 126 | +| test.c:126:7:126:7 | Constant: 1 | test.c:127:5:127:9 | Store: ... = ... | != | 0 | 127 | 127 | +| test.c:126:7:126:7 | Constant: 1 | test.c:127:5:127:9 | Store: ... = ... | != | 0 | 131 | 131 | +| test.c:126:7:126:7 | Constant: 1 | test.c:127:5:127:9 | Store: ... = ... | != | 0 | 132 | 132 | +| test.c:126:7:126:7 | Constant: 1 | test.c:127:5:127:9 | Store: ... = ... | != | 0 | 134 | 134 | +| test.c:126:7:126:7 | Constant: 1 | test.c:127:9:127:9 | Constant: 1 | != | 0 | 126 | 126 | +| test.c:126:7:126:7 | Constant: 1 | test.c:127:9:127:9 | Constant: 1 | != | 0 | 127 | 127 | +| test.c:126:7:126:7 | Constant: 1 | test.c:127:9:127:9 | Constant: 1 | != | 0 | 131 | 131 | +| test.c:126:7:126:7 | Constant: 1 | test.c:127:9:127:9 | Constant: 1 | != | 0 | 132 | 132 | +| test.c:126:7:126:7 | Constant: 1 | test.c:127:9:127:9 | Constant: 1 | != | 0 | 134 | 134 | | test.c:126:12:126:26 | Call: call to test3_condition | test.c:126:12:126:26 | Call: call to test3_condition | != | 0 | 127 | 127 | | test.c:131:7:131:7 | Load: b | test.c:131:7:131:7 | Load: b | != | 0 | 132 | 132 | +| test.c:131:7:131:7 | Load: b | test.c:131:7:131:7 | Phi: 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:145:16:145:16 | InitializeParameter: x | == | 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:151:16:151:16 | InitializeParameter: x | != | 0 | 152 | 152 | | 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:151:23:151:23 | InitializeParameter: y | != | 0 | 152 | 152 | | test.c:152:15:152:15 | Load: y | test.c:152:15:152:15 | Load: y | != | 0 | 152 | 152 | +| test.c:156:9:156:19 | CompareEQ: ... == ... | test.c:156:9:156:19 | CompareEQ: ... == ... | != | 0 | 156 | 157 | +| test.c:159:9:159:19 | CompareEQ: ... == ... | test.c:159:9:159:19 | CompareEQ: ... == ... | != | 0 | 159 | 160 | +| test.c:162:9:162:18 | CompareLT: ... < ... | test.c:162:9:162:18 | CompareLT: ... < ... | != | 0 | 162 | 163 | +| test.c:165:9:165:18 | CompareLT: ... < ... | test.c:165:9:165:18 | CompareLT: ... < ... | != | 0 | 165 | 166 | | test.c:175:13:175:32 | CompareEQ: ... == ... | test.c:175:13:175:15 | Call: call to foo | != | 0 | 175 | 175 | | test.c:175:13:175:32 | CompareEQ: ... == ... | test.c:175:13:175:15 | Call: call to foo | == | 0 | 175 | 175 | +| test.c:175:13:175:32 | CompareEQ: ... == ... | test.c:175:13:175:32 | CompareEQ: ... == ... | != | 0 | 175 | 175 | +| test.c:175:13:175:32 | CompareEQ: ... == ... | test.c:175:13:175:32 | CompareEQ: ... == ... | == | 0 | 175 | 175 | +| test.c:181:9:181:9 | Load: x | test.c:180:20:180:20 | InitializeParameter: x | != | 0 | 182 | 182 | +| test.c:181:9:181:9 | Load: x | test.c:180:20:180:20 | InitializeParameter: x | == | 0 | 184 | 184 | | test.c:181:9:181:9 | Load: x | test.c:181:9:181:9 | Load: x | != | 0 | 182 | 182 | | test.c:181:9:181:9 | Load: x | test.c:181:9:181:9 | Load: x | == | 0 | 184 | 184 | | test.cpp:18:8:18:12 | CompareNE: (bool)... | test.cpp:18:8:18:10 | Call: call to get | != | 0 | 19 | 19 | +| test.cpp:18:8:18:12 | CompareNE: (bool)... | test.cpp:18:8:18:12 | CompareNE: (bool)... | != | 0 | 19 | 19 | | test.cpp:31:7:31:13 | CompareEQ: ... == ... | test.cpp:31:7:31:7 | Load: x | != | -1 | 34 | 34 | | test.cpp:31:7:31:13 | CompareEQ: ... == ... | test.cpp:31:7:31:7 | Load: x | == | -1 | 30 | 30 | | test.cpp:31:7:31:13 | CompareEQ: ... == ... | test.cpp:31:7:31:7 | Load: x | == | -1 | 32 | 32 | +| test.cpp:31:7:31:13 | CompareEQ: ... == ... | test.cpp:31:7:31:13 | CompareEQ: ... == ... | != | 0 | 30 | 30 | +| test.cpp:31:7:31:13 | CompareEQ: ... == ... | test.cpp:31:7:31:13 | CompareEQ: ... == ... | != | 0 | 32 | 32 | +| test.cpp:31:7:31:13 | CompareEQ: ... == ... | test.cpp:31:7:31:13 | CompareEQ: ... == ... | == | 0 | 34 | 34 | | test.cpp:42:13:42:20 | Call: call to getABool | test.cpp:42:13:42:20 | Call: call to getABool | != | 0 | 44 | 44 | | test.cpp:42:13:42:20 | Call: call to getABool | test.cpp:42:13:42:20 | Call: call to getABool | == | 0 | 53 | 53 | diff --git a/cpp/ql/test/library-tests/controlflow/guards/GuardsCompare.expected b/cpp/ql/test/library-tests/controlflow/guards/GuardsCompare.expected index 8480a1f86138..4f44591e0b81 100644 --- a/cpp/ql/test/library-tests/controlflow/guards/GuardsCompare.expected +++ b/cpp/ql/test/library-tests/controlflow/guards/GuardsCompare.expected @@ -1,5 +1,7 @@ | 7 | 0 < x+0 when ... > ... is true | | 7 | 0 >= x+0 when ... > ... is false | +| 7 | ... > ... != 0 when ... > ... is true | +| 7 | ... > ... == 0 when ... > ... is false | | 7 | x < 0+1 when ... > ... is false | | 7 | x < 1 when ... > ... is false | | 7 | x >= 0+1 when ... > ... is true | @@ -10,6 +12,12 @@ | 17 | 1 < y+0 when ... && ... is true | | 17 | 1 < y+0 when ... > ... is true | | 17 | 1 >= y+0 when ... > ... is false | +| 17 | ... < ... != 0 when ... && ... is true | +| 17 | ... < ... != 0 when ... < ... is true | +| 17 | ... < ... == 0 when ... < ... is false | +| 17 | ... > ... != 0 when ... && ... is true | +| 17 | ... > ... != 0 when ... > ... is true | +| 17 | ... > ... == 0 when ... > ... is false | | 17 | x < 0 when ... && ... is true | | 17 | x < 0 when ... < ... is true | | 17 | x < 0+0 when ... && ... is true | @@ -26,24 +34,32 @@ | 18 | call to get == 0 when call to get is false | | 26 | 0 < x+0 when ... > ... is true | | 26 | 0 >= x+0 when ... > ... is false | +| 26 | ... > ... != 0 when ... > ... is true | +| 26 | ... > ... == 0 when ... > ... is false | | 26 | x < 0+1 when ... > ... is false | | 26 | x < 1 when ... > ... is false | | 26 | x >= 0+1 when ... > ... is true | | 26 | x >= 1 when ... > ... is true | | 31 | - ... != x+0 when ... == ... is false | | 31 | - ... == x+0 when ... == ... is true | +| 31 | ... == ... != 0 when ... == ... is true | +| 31 | ... == ... == 0 when ... == ... is false | | 31 | x != -1 when ... == ... is false | | 31 | x != - ...+0 when ... == ... is false | | 31 | x == -1 when ... == ... is true | | 31 | x == - ...+0 when ... == ... is true | | 34 | 10 < j+1 when ... < ... is false | | 34 | 10 >= j+1 when ... < ... is true | +| 34 | ... < ... != 0 when ... < ... is true | +| 34 | ... < ... == 0 when ... < ... is false | | 34 | j < 10 when ... < ... is true | | 34 | j < 10+0 when ... < ... is true | | 34 | j >= 10 when ... < ... is false | | 34 | j >= 10+0 when ... < ... is false | | 42 | 10 < j+1 when ... < ... is false | | 42 | 10 >= j+1 when ... < ... is true | +| 42 | ... < ... != 0 when ... < ... is true | +| 42 | ... < ... == 0 when ... < ... is false | | 42 | call to getABool != 0 when call to getABool is true | | 42 | call to getABool == 0 when call to getABool is false | | 42 | j < 10 when ... < ... is true | @@ -52,12 +68,16 @@ | 42 | j >= 10+0 when ... < ... is false | | 44 | 0 < z+0 when ... > ... is true | | 44 | 0 >= z+0 when ... > ... is false | +| 44 | ... > ... != 0 when ... > ... is true | +| 44 | ... > ... == 0 when ... > ... is false | | 44 | z < 0+1 when ... > ... is false | | 44 | z < 1 when ... > ... is false | | 44 | z >= 0+1 when ... > ... is true | | 44 | z >= 1 when ... > ... is true | | 45 | 0 < y+0 when ... > ... is true | | 45 | 0 >= y+0 when ... > ... is false | +| 45 | ... > ... != 0 when ... > ... is true | +| 45 | ... > ... == 0 when ... > ... is false | | 45 | y < 0+1 when ... > ... is false | | 45 | y < 1 when ... > ... is false | | 45 | y >= 0+1 when ... > ... is true | @@ -68,6 +88,12 @@ | 58 | 0 < y+1 when ... \|\| ... is false | | 58 | 0 == x+0 when ... == ... is true | | 58 | 0 >= y+1 when ... < ... is true | +| 58 | ... < ... != 0 when ... < ... is true | +| 58 | ... < ... == 0 when ... < ... is false | +| 58 | ... < ... == 0 when ... \|\| ... is false | +| 58 | ... == ... != 0 when ... == ... is true | +| 58 | ... == ... == 0 when ... == ... is false | +| 58 | ... == ... == 0 when ... \|\| ... is false | | 58 | x != 0 when ... == ... is false | | 58 | x != 0 when ... \|\| ... is false | | 58 | x != 0+0 when ... == ... is false | @@ -89,6 +115,8 @@ | 74 | i >= 11 when i is Case[11..20] | | 75 | 0 != x+0 when ... == ... is false | | 75 | 0 == x+0 when ... == ... is true | +| 75 | ... == ... != 0 when ... == ... is true | +| 75 | ... == ... == 0 when ... == ... is false | | 75 | x != 0 when ... == ... is false | | 75 | x != 0+0 when ... == ... is false | | 75 | x == 0 when ... == ... is true | @@ -99,6 +127,12 @@ | 85 | 0 == x+0 when ... && ... is true | | 85 | 0 == x+0 when ... == ... is true | | 85 | 0 == y+0 when ... != ... is false | +| 85 | ... != ... != 0 when ... != ... is true | +| 85 | ... != ... != 0 when ... && ... is true | +| 85 | ... != ... == 0 when ... != ... is false | +| 85 | ... == ... != 0 when ... && ... is true | +| 85 | ... == ... != 0 when ... == ... is true | +| 85 | ... == ... == 0 when ... == ... is false | | 85 | x != 0 when ... == ... is false | | 85 | x != 0+0 when ... == ... is false | | 85 | x == 0 when ... && ... is true | @@ -115,18 +149,26 @@ | 93 | c == 0 when c is false | | 94 | 0 != x+0 when ... != ... is true | | 94 | 0 == x+0 when ... != ... is false | +| 94 | ... != ... != 0 when ... != ... is true | +| 94 | ... != ... == 0 when ... != ... is false | | 94 | x != 0 when ... != ... is true | | 94 | x != 0+0 when ... != ... is true | | 94 | x == 0 when ... != ... is false | | 94 | x == 0+0 when ... != ... is false | +| 99 | f != 0 when f is true | +| 99 | f == 0 when f is false | | 102 | 10 < j+1 when ... < ... is false | | 102 | 10 >= j+1 when ... < ... is true | +| 102 | ... < ... != 0 when ... < ... is true | +| 102 | ... < ... == 0 when ... < ... is false | | 102 | j < 10 when ... < ... is true | | 102 | j < 10+0 when ... < ... is true | | 102 | j >= 10 when ... < ... is false | | 102 | j >= 10+0 when ... < ... is false | | 105 | 0.0 != f+0 when ... != ... is true | | 105 | 0.0 == f+0 when ... != ... is false | +| 105 | ... != ... != 0 when ... != ... is true | +| 105 | ... != ... == 0 when ... != ... is false | | 105 | f != 0.0+0 when ... != ... is true | | 105 | f == 0.0+0 when ... != ... is false | | 109 | 0 != x+0 when ... == ... is false | @@ -135,6 +177,12 @@ | 109 | 0 < y+1 when ... \|\| ... is false | | 109 | 0 == x+0 when ... == ... is true | | 109 | 0 >= y+1 when ... < ... is true | +| 109 | ... < ... != 0 when ... < ... is true | +| 109 | ... < ... == 0 when ... < ... is false | +| 109 | ... < ... == 0 when ... \|\| ... is false | +| 109 | ... == ... != 0 when ... == ... is true | +| 109 | ... == ... == 0 when ... == ... is false | +| 109 | ... == ... == 0 when ... \|\| ... is false | | 109 | x != 0 when ... == ... is false | | 109 | x != 0 when ... \|\| ... is false | | 109 | x != 0+0 when ... == ... is false | @@ -149,6 +197,8 @@ | 109 | y >= 0+0 when ... \|\| ... is false | | 111 | 0.0 != i+0 when ... != ... is true | | 111 | 0.0 == i+0 when ... != ... is false | +| 111 | ... != ... != 0 when ... != ... is true | +| 111 | ... != ... == 0 when ... != ... is false | | 111 | i != 0.0+0 when ... != ... is true | | 111 | i == 0.0+0 when ... != ... is false | | 122 | b != 0 when b is true | @@ -166,6 +216,8 @@ | 126 | call to test3_condition == 0 when call to test3_condition is false | | 131 | ... + ... != a+0 when call to __builtin_expect is false | | 131 | ... + ... == a+0 when call to __builtin_expect is true | +| 131 | ... == ... != 0 when call to __builtin_expect is true | +| 131 | ... == ... == 0 when call to __builtin_expect is false | | 131 | a != ... + ...+0 when call to __builtin_expect is false | | 131 | a != b+42 when call to __builtin_expect is false | | 131 | a == ... + ...+0 when call to __builtin_expect is true | @@ -176,6 +228,8 @@ | 131 | b == a+-42 when call to __builtin_expect is true | | 131 | call to __builtin_expect != 0 when call to __builtin_expect is true | | 131 | call to __builtin_expect == 0 when call to __builtin_expect is false | +| 135 | ... != ... != 0 when call to __builtin_expect is true | +| 135 | ... != ... == 0 when call to __builtin_expect is false | | 135 | ... + ... != a+0 when call to __builtin_expect is true | | 135 | ... + ... == a+0 when call to __builtin_expect is false | | 135 | a != ... + ...+0 when call to __builtin_expect is true | @@ -190,6 +244,8 @@ | 137 | 0 == 0 when 0 is false | | 141 | 42 != a+0 when call to __builtin_expect is false | | 141 | 42 == a+0 when call to __builtin_expect is true | +| 141 | ... == ... != 0 when call to __builtin_expect is true | +| 141 | ... == ... == 0 when call to __builtin_expect is false | | 141 | a != 42 when call to __builtin_expect is false | | 141 | a != 42+0 when call to __builtin_expect is false | | 141 | a == 42 when call to __builtin_expect is true | @@ -198,6 +254,8 @@ | 141 | call to __builtin_expect == 0 when call to __builtin_expect is false | | 145 | 42 != a+0 when call to __builtin_expect is true | | 145 | 42 == a+0 when call to __builtin_expect is false | +| 145 | ... != ... != 0 when call to __builtin_expect is true | +| 145 | ... != ... == 0 when call to __builtin_expect is false | | 145 | a != 42 when call to __builtin_expect is true | | 145 | a != 42+0 when call to __builtin_expect is true | | 145 | a == 42 when call to __builtin_expect 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 c520b48f94e4..c41cdfd6063d 100644 --- a/cpp/ql/test/library-tests/controlflow/guards/GuardsEnsure.expected +++ b/cpp/ql/test/library-tests/controlflow/guards/GuardsEnsure.expected @@ -99,10 +99,20 @@ binary | test.c:75:9:75:14 | ... == ... | test.c:75:9:75:9 | x | == | test.c:75:14:75:14 | 0 | 0 | 75 | 77 | | test.c:75:9:75:14 | ... == ... | test.c:75:14:75:14 | 0 | != | test.c:75:9:75:9 | x | 0 | 78 | 79 | | test.c:75:9:75:14 | ... == ... | test.c:75:14:75:14 | 0 | == | test.c:75:9:75:9 | x | 0 | 75 | 77 | +| test.c:75:9:75:14 | ... == ... | test.c:85:8:85:8 | x | != | test.c:85:13:85:13 | 0 | 0 | 78 | 79 | +| test.c:75:9:75:14 | ... == ... | test.c:85:8:85:8 | x | == | test.c:85:13:85:13 | 0 | 0 | 75 | 77 | +| test.c:75:9:75:14 | ... == ... | test.c:85:13:85:13 | 0 | != | test.c:85:8:85:8 | x | 0 | 78 | 79 | +| test.c:75:9:75:14 | ... == ... | test.c:85:13:85:13 | 0 | == | test.c:85:8:85:8 | x | 0 | 75 | 77 | +| test.c:85:8:85:13 | ... == ... | test.c:75:9:75:9 | x | == | test.c:75:14:75:14 | 0 | 0 | 85 | 85 | +| test.c:85:8:85:13 | ... == ... | test.c:75:9:75:9 | x | == | test.c:75:14:75:14 | 0 | 0 | 86 | 86 | +| test.c:85:8:85:13 | ... == ... | test.c:75:14:75:14 | 0 | == | test.c:75:9:75:9 | x | 0 | 85 | 85 | +| test.c:85:8:85:13 | ... == ... | test.c:75:14:75:14 | 0 | == | test.c:75:9:75:9 | x | 0 | 86 | 86 | | test.c:85:8:85:13 | ... == ... | test.c:85:8:85:8 | x | == | test.c:85:13:85:13 | 0 | 0 | 85 | 85 | | test.c:85:8:85:13 | ... == ... | test.c:85:8:85:8 | x | == | test.c:85:13:85:13 | 0 | 0 | 86 | 86 | | test.c:85:8:85:13 | ... == ... | test.c:85:13:85:13 | 0 | == | test.c:85:8:85:8 | x | 0 | 85 | 85 | | test.c:85:8:85:13 | ... == ... | test.c:85:13:85:13 | 0 | == | test.c:85:8:85:8 | x | 0 | 86 | 86 | +| test.c:85:8:85:23 | ... && ... | test.c:75:9:75:9 | x | == | test.c:75:14:75:14 | 0 | 0 | 86 | 86 | +| test.c:85:8:85:23 | ... && ... | test.c:75:14:75:14 | 0 | == | test.c:75:9:75:9 | x | 0 | 86 | 86 | | test.c:85:8:85:23 | ... && ... | test.c:85:8:85:8 | x | == | test.c:85:13:85:13 | 0 | 0 | 86 | 86 | | test.c:85:8:85:23 | ... && ... | test.c:85:13:85:13 | 0 | == | test.c:85:8:85:8 | x | 0 | 86 | 86 | | test.c:85:8:85:23 | ... && ... | test.c:85:18:85:18 | y | != | test.c:85:23:85:23 | 0 | 0 | 86 | 86 | @@ -174,11 +184,18 @@ binary unary | test.c:7:9:7:13 | ... > ... | test.c:7:9:7:9 | x | < | 1 | 10 | 11 | | test.c:7:9:7:13 | ... > ... | test.c:7:9:7:9 | x | >= | 1 | 7 | 9 | +| test.c:7:9:7:13 | ... > ... | test.c:7:9:7:13 | ... > ... | != | 0 | 7 | 9 | +| test.c:7:9:7:13 | ... > ... | test.c:7:9:7:13 | ... > ... | == | 0 | 10 | 11 | | test.c:17:8:17:12 | ... < ... | test.c:17:8:17:8 | x | < | 0 | 17 | 17 | | test.c:17:8:17:12 | ... < ... | test.c:17:8:17:8 | x | < | 0 | 18 | 18 | +| test.c:17:8:17:12 | ... < ... | test.c:17:8:17:12 | ... < ... | != | 0 | 17 | 17 | +| test.c:17:8:17:12 | ... < ... | test.c:17:8:17:12 | ... < ... | != | 0 | 18 | 18 | | test.c:17:8:17:21 | ... && ... | test.c:17:8:17:8 | x | < | 0 | 18 | 18 | +| test.c:17:8:17:21 | ... && ... | test.c:17:8:17:12 | ... < ... | != | 0 | 18 | 18 | | test.c:17:8:17:21 | ... && ... | test.c:17:17:17:17 | y | >= | 2 | 18 | 18 | +| test.c:17:8:17:21 | ... && ... | test.c:17:17:17:21 | ... > ... | != | 0 | 18 | 18 | | test.c:17:17:17:21 | ... > ... | test.c:17:17:17:17 | y | >= | 2 | 18 | 18 | +| test.c:17:17:17:21 | ... > ... | test.c:17:17:17:21 | ... > ... | != | 0 | 18 | 18 | | test.c:26:11:26:15 | ... > ... | test.c:26:11:26:11 | x | < | 1 | 2 | 2 | | test.c:26:11:26:15 | ... > ... | test.c:26:11:26:11 | x | < | 1 | 31 | 34 | | test.c:26:11:26:15 | ... > ... | test.c:26:11:26:11 | x | < | 1 | 34 | 34 | @@ -193,6 +210,20 @@ unary | test.c:26:11:26:15 | ... > ... | test.c:26:11:26:11 | x | < | 1 | 58 | 66 | | test.c:26:11:26:15 | ... > ... | test.c:26:11:26:11 | x | < | 1 | 62 | 62 | | test.c:26:11:26:15 | ... > ... | test.c:26:11:26:11 | x | >= | 1 | 26 | 28 | +| test.c:26:11:26:15 | ... > ... | test.c:26:11:26:15 | ... > ... | != | 0 | 26 | 28 | +| test.c:26:11:26:15 | ... > ... | test.c:26:11:26:15 | ... > ... | == | 0 | 2 | 2 | +| test.c:26:11:26:15 | ... > ... | test.c:26:11:26:15 | ... > ... | == | 0 | 31 | 34 | +| test.c:26:11:26:15 | ... > ... | test.c:26:11:26:15 | ... > ... | == | 0 | 34 | 34 | +| test.c:26:11:26:15 | ... > ... | test.c:26:11:26:15 | ... > ... | == | 0 | 39 | 42 | +| test.c:26:11:26:15 | ... > ... | test.c:26:11:26:15 | ... > ... | == | 0 | 42 | 42 | +| test.c:26:11:26:15 | ... > ... | test.c:26:11:26:15 | ... > ... | == | 0 | 42 | 44 | +| test.c:26:11:26:15 | ... > ... | test.c:26:11:26:15 | ... > ... | == | 0 | 45 | 45 | +| test.c:26:11:26:15 | ... > ... | test.c:26:11:26:15 | ... > ... | == | 0 | 45 | 47 | +| test.c:26:11:26:15 | ... > ... | test.c:26:11:26:15 | ... > ... | == | 0 | 51 | 53 | +| test.c:26:11:26:15 | ... > ... | test.c:26:11:26:15 | ... > ... | == | 0 | 56 | 58 | +| test.c:26:11:26:15 | ... > ... | test.c:26:11:26:15 | ... > ... | == | 0 | 58 | 58 | +| test.c:26:11:26:15 | ... > ... | test.c:26:11:26:15 | ... > ... | == | 0 | 58 | 66 | +| test.c:26:11:26:15 | ... > ... | test.c:26:11:26:15 | ... > ... | == | 0 | 62 | 62 | | test.c:34:16:34:21 | ... < ... | test.c:34:16:34:16 | j | < | 10 | 34 | 34 | | test.c:34:16:34:21 | ... < ... | test.c:34:16:34:16 | j | >= | 10 | 2 | 2 | | test.c:34:16:34:21 | ... < ... | test.c:34:16:34:16 | j | >= | 10 | 39 | 42 | @@ -205,28 +236,72 @@ unary | test.c:34:16:34:21 | ... < ... | test.c:34:16:34:16 | j | >= | 10 | 58 | 58 | | test.c:34:16:34:21 | ... < ... | test.c:34:16:34:16 | j | >= | 10 | 58 | 66 | | test.c:34:16:34:21 | ... < ... | test.c:34:16:34:16 | j | >= | 10 | 62 | 62 | +| test.c:34:16:34:21 | ... < ... | test.c:34:16:34:21 | ... < ... | != | 0 | 34 | 34 | +| test.c:34:16:34:21 | ... < ... | test.c:34:16:34:21 | ... < ... | == | 0 | 2 | 2 | +| test.c:34:16:34:21 | ... < ... | test.c:34:16:34:21 | ... < ... | == | 0 | 39 | 42 | +| test.c:34:16:34:21 | ... < ... | test.c:34:16:34:21 | ... < ... | == | 0 | 42 | 42 | +| test.c:34:16:34:21 | ... < ... | test.c:34:16:34:21 | ... < ... | == | 0 | 42 | 44 | +| test.c:34:16:34:21 | ... < ... | test.c:34:16:34:21 | ... < ... | == | 0 | 45 | 45 | +| test.c:34:16:34:21 | ... < ... | test.c:34:16:34:21 | ... < ... | == | 0 | 45 | 47 | +| test.c:34:16:34:21 | ... < ... | test.c:34:16:34:21 | ... < ... | == | 0 | 51 | 53 | +| test.c:34:16:34:21 | ... < ... | test.c:34:16:34:21 | ... < ... | == | 0 | 56 | 58 | +| test.c:34:16:34:21 | ... < ... | test.c:34:16:34:21 | ... < ... | == | 0 | 58 | 58 | +| test.c:34:16:34:21 | ... < ... | test.c:34:16:34:21 | ... < ... | == | 0 | 58 | 66 | +| test.c:34:16:34:21 | ... < ... | test.c:34:16:34:21 | ... < ... | == | 0 | 62 | 62 | | test.c:42:16:42:21 | ... < ... | test.c:42:16:42:16 | j | < | 10 | 42 | 42 | | test.c:42:16:42:21 | ... < ... | test.c:42:16:42:16 | j | < | 10 | 42 | 44 | | test.c:42:16:42:21 | ... < ... | test.c:42:16:42:16 | j | < | 10 | 45 | 45 | | test.c:42:16:42:21 | ... < ... | test.c:42:16:42:16 | j | < | 10 | 45 | 47 | | test.c:42:16:42:21 | ... < ... | test.c:42:16:42:16 | j | < | 10 | 51 | 53 | +| test.c:42:16:42:21 | ... < ... | test.c:42:16:42:21 | ... < ... | != | 0 | 42 | 42 | +| test.c:42:16:42:21 | ... < ... | test.c:42:16:42:21 | ... < ... | != | 0 | 42 | 44 | +| test.c:42:16:42:21 | ... < ... | test.c:42:16:42:21 | ... < ... | != | 0 | 45 | 45 | +| test.c:42:16:42:21 | ... < ... | test.c:42:16:42:21 | ... < ... | != | 0 | 45 | 47 | +| test.c:42:16:42:21 | ... < ... | test.c:42:16:42:21 | ... < ... | != | 0 | 51 | 53 | | test.c:44:12:44:16 | ... > ... | test.c:44:12:44:12 | z | < | 1 | 42 | 42 | | test.c:44:12:44:16 | ... > ... | test.c:44:12:44:12 | z | < | 1 | 51 | 53 | | test.c:44:12:44:16 | ... > ... | test.c:44:12:44:12 | z | >= | 1 | 45 | 45 | | test.c:44:12:44:16 | ... > ... | test.c:44:12:44:12 | z | >= | 1 | 45 | 47 | +| test.c:44:12:44:16 | ... > ... | test.c:44:12:44:16 | ... > ... | != | 0 | 45 | 45 | +| test.c:44:12:44:16 | ... > ... | test.c:44:12:44:16 | ... > ... | != | 0 | 45 | 47 | +| test.c:44:12:44:16 | ... > ... | test.c:44:12:44:16 | ... > ... | == | 0 | 42 | 42 | +| test.c:44:12:44:16 | ... > ... | test.c:44:12:44:16 | ... > ... | == | 0 | 51 | 53 | | test.c:45:16:45:20 | ... > ... | test.c:45:16:45:16 | y | >= | 1 | 45 | 47 | +| test.c:45:16:45:20 | ... > ... | test.c:45:16:45:20 | ... > ... | != | 0 | 45 | 47 | | test.c:58:9:58:14 | ... == ... | test.c:58:9:58:9 | x | != | 0 | 58 | 58 | | test.c:58:9:58:14 | ... == ... | test.c:58:9:58:9 | x | != | 0 | 62 | 62 | +| test.c:58:9:58:14 | ... == ... | test.c:58:9:58:14 | ... == ... | == | 0 | 58 | 58 | +| test.c:58:9:58:14 | ... == ... | test.c:58:9:58:14 | ... == ... | == | 0 | 62 | 62 | | test.c:58:9:58:23 | ... \|\| ... | test.c:58:9:58:9 | x | != | 0 | 62 | 62 | +| test.c:58:9:58:23 | ... \|\| ... | test.c:58:9:58:14 | ... == ... | == | 0 | 62 | 62 | | test.c:58:9:58:23 | ... \|\| ... | test.c:58:19:58:19 | y | >= | 0 | 62 | 62 | +| test.c:58:9:58:23 | ... \|\| ... | test.c:58:19:58:23 | ... < ... | == | 0 | 62 | 62 | | test.c:58:19:58:23 | ... < ... | test.c:58:19:58:19 | y | >= | 0 | 62 | 62 | +| test.c:58:19:58:23 | ... < ... | test.c:58:19:58:23 | ... < ... | == | 0 | 62 | 62 | | test.c:75:9:75:14 | ... == ... | test.c:75:9:75:9 | x | != | 0 | 78 | 79 | | test.c:75:9:75:14 | ... == ... | test.c:75:9:75:9 | x | == | 0 | 75 | 77 | +| test.c:75:9:75:14 | ... == ... | test.c:75:9:75:14 | ... == ... | != | 0 | 75 | 77 | +| test.c:75:9:75:14 | ... == ... | test.c:75:9:75:14 | ... == ... | == | 0 | 78 | 79 | +| test.c:75:9:75:14 | ... == ... | test.c:85:8:85:8 | x | != | 0 | 78 | 79 | +| test.c:75:9:75:14 | ... == ... | test.c:85:8:85:8 | x | == | 0 | 75 | 77 | +| test.c:75:9:75:14 | ... == ... | test.c:85:8:85:13 | ... == ... | != | 0 | 75 | 77 | +| test.c:75:9:75:14 | ... == ... | test.c:85:8:85:13 | ... == ... | == | 0 | 78 | 79 | +| test.c:85:8:85:13 | ... == ... | test.c:75:9:75:9 | x | == | 0 | 85 | 85 | +| test.c:85:8:85:13 | ... == ... | test.c:75:9:75:9 | x | == | 0 | 86 | 86 | +| test.c:85:8:85:13 | ... == ... | test.c:75:9:75:14 | ... == ... | != | 0 | 85 | 85 | +| test.c:85:8:85:13 | ... == ... | test.c:75:9:75:14 | ... == ... | != | 0 | 86 | 86 | | test.c:85:8:85:13 | ... == ... | test.c:85:8:85:8 | x | == | 0 | 85 | 85 | | test.c:85:8:85:13 | ... == ... | test.c:85:8:85:8 | x | == | 0 | 86 | 86 | +| test.c:85:8:85:13 | ... == ... | test.c:85:8:85:13 | ... == ... | != | 0 | 85 | 85 | +| test.c:85:8:85:13 | ... == ... | test.c:85:8:85:13 | ... == ... | != | 0 | 86 | 86 | +| test.c:85:8:85:23 | ... && ... | test.c:75:9:75:9 | x | == | 0 | 86 | 86 | +| test.c:85:8:85:23 | ... && ... | test.c:75:9:75:14 | ... == ... | != | 0 | 86 | 86 | | test.c:85:8:85:23 | ... && ... | test.c:85:8:85:8 | x | == | 0 | 86 | 86 | +| test.c:85:8:85:23 | ... && ... | test.c:85:8:85:13 | ... == ... | != | 0 | 86 | 86 | | test.c:85:8:85:23 | ... && ... | test.c:85:18:85:18 | y | != | 0 | 86 | 86 | +| test.c:85:8:85:23 | ... && ... | test.c:85:18:85:23 | ... != ... | != | 0 | 86 | 86 | | test.c:85:18:85:23 | ... != ... | test.c:85:18:85:18 | y | != | 0 | 86 | 86 | +| test.c:85:18:85:23 | ... != ... | test.c:85:18:85:23 | ... != ... | != | 0 | 86 | 86 | | test.c:94:11:94:16 | ... != ... | test.c:94:11:94:11 | x | != | 0 | 94 | 96 | | test.c:94:11:94:16 | ... != ... | test.c:94:11:94:11 | x | == | 0 | 70 | 70 | | test.c:94:11:94:16 | ... != ... | test.c:94:11:94:11 | x | == | 0 | 99 | 102 | @@ -235,24 +310,49 @@ unary | test.c:94:11:94:16 | ... != ... | test.c:94:11:94:11 | x | == | 0 | 109 | 109 | | test.c:94:11:94:16 | ... != ... | test.c:94:11:94:11 | x | == | 0 | 109 | 117 | | test.c:94:11:94:16 | ... != ... | test.c:94:11:94:11 | x | == | 0 | 113 | 113 | +| test.c:94:11:94:16 | ... != ... | test.c:94:11:94:16 | ... != ... | != | 0 | 94 | 96 | +| test.c:94:11:94:16 | ... != ... | test.c:94:11:94:16 | ... != ... | == | 0 | 70 | 70 | +| test.c:94:11:94:16 | ... != ... | test.c:94:11:94:16 | ... != ... | == | 0 | 99 | 102 | +| test.c:94:11:94:16 | ... != ... | test.c:94:11:94:16 | ... != ... | == | 0 | 102 | 102 | +| test.c:94:11:94:16 | ... != ... | test.c:94:11:94:16 | ... != ... | == | 0 | 107 | 109 | +| test.c:94:11:94:16 | ... != ... | test.c:94:11:94:16 | ... != ... | == | 0 | 109 | 109 | +| test.c:94:11:94:16 | ... != ... | test.c:94:11:94:16 | ... != ... | == | 0 | 109 | 117 | +| test.c:94:11:94:16 | ... != ... | test.c:94:11:94:16 | ... != ... | == | 0 | 113 | 113 | | test.c:102:16:102:21 | ... < ... | test.c:102:16:102:16 | j | < | 10 | 102 | 102 | | test.c:102:16:102:21 | ... < ... | test.c:102:16:102:16 | j | >= | 10 | 70 | 70 | | test.c:102:16:102:21 | ... < ... | test.c:102:16:102:16 | j | >= | 10 | 107 | 109 | | test.c:102:16:102:21 | ... < ... | test.c:102:16:102:16 | j | >= | 10 | 109 | 109 | | test.c:102:16:102:21 | ... < ... | test.c:102:16:102:16 | j | >= | 10 | 109 | 117 | | test.c:102:16:102:21 | ... < ... | test.c:102:16:102:16 | j | >= | 10 | 113 | 113 | +| test.c:102:16:102:21 | ... < ... | test.c:102:16:102:21 | ... < ... | != | 0 | 102 | 102 | +| test.c:102:16:102:21 | ... < ... | test.c:102:16:102:21 | ... < ... | == | 0 | 70 | 70 | +| test.c:102:16:102:21 | ... < ... | test.c:102:16:102:21 | ... < ... | == | 0 | 107 | 109 | +| test.c:102:16:102:21 | ... < ... | test.c:102:16:102:21 | ... < ... | == | 0 | 109 | 109 | +| test.c:102:16:102:21 | ... < ... | test.c:102:16:102:21 | ... < ... | == | 0 | 109 | 117 | +| test.c:102:16:102:21 | ... < ... | test.c:102:16:102:21 | ... < ... | == | 0 | 113 | 113 | | test.c:109:9:109:14 | ... == ... | test.c:109:9:109:9 | x | != | 0 | 109 | 109 | | test.c:109:9:109:14 | ... == ... | test.c:109:9:109:9 | x | != | 0 | 113 | 113 | +| test.c:109:9:109:14 | ... == ... | test.c:109:9:109:14 | ... == ... | == | 0 | 109 | 109 | +| test.c:109:9:109:14 | ... == ... | test.c:109:9:109:14 | ... == ... | == | 0 | 113 | 113 | | test.c:109:9:109:23 | ... \|\| ... | test.c:109:9:109:9 | x | != | 0 | 113 | 113 | +| test.c:109:9:109:23 | ... \|\| ... | test.c:109:9:109:14 | ... == ... | == | 0 | 113 | 113 | | test.c:109:9:109:23 | ... \|\| ... | test.c:109:19:109:19 | y | >= | 0 | 113 | 113 | +| test.c:109:9:109:23 | ... \|\| ... | test.c:109:19:109:23 | ... < ... | == | 0 | 113 | 113 | | test.c:109:19:109:23 | ... < ... | test.c:109:19:109:19 | y | >= | 0 | 113 | 113 | +| test.c:109:19:109:23 | ... < ... | test.c:109:19:109:23 | ... < ... | == | 0 | 113 | 113 | | test.c:126:7:126:7 | 1 | test.c:126:7:126:7 | 1 | != | 0 | 126 | 126 | | test.c:126:7:126:7 | 1 | test.c:126:7:126:7 | 1 | != | 0 | 126 | 128 | | test.c:126:7:126:7 | 1 | test.c:126:7:126:7 | 1 | != | 0 | 131 | 131 | | test.c:126:7:126:7 | 1 | test.c:126:7:126:7 | 1 | != | 0 | 131 | 132 | | test.c:126:7:126:7 | 1 | test.c:126:7:126:7 | 1 | != | 0 | 134 | 123 | +| test.c:126:7:126:7 | 1 | test.c:127:9:127:9 | 1 | != | 0 | 126 | 126 | +| test.c:126:7:126:7 | 1 | test.c:127:9:127:9 | 1 | != | 0 | 126 | 128 | +| test.c:126:7:126:7 | 1 | test.c:127:9:127:9 | 1 | != | 0 | 131 | 131 | +| test.c:126:7:126:7 | 1 | test.c:127:9:127:9 | 1 | != | 0 | 131 | 132 | +| test.c:126:7:126:7 | 1 | test.c:127:9:127:9 | 1 | != | 0 | 134 | 123 | | test.c:126:7:126:28 | ... && ... | test.c:126:7:126:7 | 1 | != | 0 | 126 | 128 | | test.c:126:7:126:28 | ... && ... | test.c:126:12:126:26 | call to test3_condition | != | 0 | 126 | 128 | +| test.c:126:7:126:28 | ... && ... | test.c:127:9:127:9 | 1 | != | 0 | 126 | 128 | | test.c:126:12:126:26 | call to test3_condition | test.c:126:12:126:26 | call to test3_condition | != | 0 | 126 | 128 | | 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 | @@ -269,6 +369,10 @@ unary | test.cpp:31:7:31:13 | ... == ... | test.cpp:31:7:31:7 | x | != | -1 | 34 | 34 | | 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 | 31 | 32 | +| test.cpp:31:7:31:13 | ... == ... | test.cpp:31:7:31:13 | ... == ... | != | 0 | 30 | 30 | +| test.cpp:31:7:31:13 | ... == ... | test.cpp:31:7:31:13 | ... == ... | != | 0 | 31 | 32 | +| test.cpp:31:7:31:13 | ... == ... | test.cpp:31:7:31:13 | ... == ... | == | 0 | 30 | 30 | +| test.cpp:31:7:31:13 | ... == ... | test.cpp:31:7:31:13 | ... == ... | == | 0 | 34 | 34 | | test.cpp:42:13:42:20 | call to getABool | test.cpp:42:13:42:20 | call to getABool | != | 0 | 43 | 45 | | test.cpp:42:13:42:20 | call to getABool | test.cpp:42:13:42:20 | call to getABool | == | 0 | 53 | 53 | | test.cpp:61:10:61:10 | i | test.cpp:61:10:61:10 | i | == | 0 | 62 | 64 | @@ -278,13 +382,20 @@ unary | test.cpp:74:10:74:10 | i | test.cpp:74:10:74:10 | i | >= | 0 | 75 | 77 | | test.cpp:74:10:74:10 | i | test.cpp:74:10:74:10 | i | >= | 11 | 78 | 79 | | test.cpp:93:6:93:6 | c | test.cpp:93:6:93:6 | c | != | 0 | 93 | 94 | +| test.cpp:99:6:99:6 | f | test.cpp:99:6:99:6 | f | != | 0 | 99 | 100 | +| test.cpp:105:6:105:14 | ... != ... | test.cpp:105:6:105:14 | ... != ... | != | 0 | 105 | 106 | +| test.cpp:111:6:111:14 | ... != ... | test.cpp:111:6:111:14 | ... != ... | != | 0 | 111 | 112 | | test.cpp:122:9:122:9 | b | test.cpp:122:9:122:9 | b | != | 0 | 123 | 125 | | test.cpp:122:9:122:9 | b | test.cpp:122:9:122:9 | b | != | 0 | 125 | 125 | | test.cpp:125:13:125:20 | ! ... | test.cpp:125:13:125:20 | ! ... | != | 0 | 125 | 125 | | test.cpp:125:14:125:17 | call to safe | test.cpp:125:14:125:17 | call to safe | == | 0 | 125 | 125 | | test.cpp:131:6:131:21 | call to __builtin_expect | test.cpp:131:6:131:21 | call to __builtin_expect | != | 0 | 131 | 132 | +| test.cpp:131:6:131:21 | call to __builtin_expect | test.cpp:131:23:131:33 | ... == ... | != | 0 | 131 | 132 | | test.cpp:135:6:135:21 | call to __builtin_expect | test.cpp:135:6:135:21 | call to __builtin_expect | != | 0 | 135 | 136 | +| test.cpp:135:6:135:21 | call to __builtin_expect | test.cpp:135:23:135:33 | ... != ... | != | 0 | 135 | 136 | | test.cpp:141:6:141:21 | call to __builtin_expect | test.cpp:141:6:141:21 | call to __builtin_expect | != | 0 | 141 | 142 | | test.cpp:141:6:141:21 | call to __builtin_expect | test.cpp:141:23:141:23 | a | == | 42 | 141 | 142 | +| test.cpp:141:6:141:21 | call to __builtin_expect | test.cpp:141:23:141:29 | ... == ... | != | 0 | 141 | 142 | | test.cpp:145:6:145:21 | call to __builtin_expect | test.cpp:145:6:145:21 | call to __builtin_expect | != | 0 | 145 | 146 | | test.cpp:145:6:145:21 | call to __builtin_expect | test.cpp:145:23:145:23 | a | != | 42 | 145 | 146 | +| test.cpp:145:6:145:21 | call to __builtin_expect | test.cpp:145:23:145:29 | ... != ... | != | 0 | 145 | 146 | diff --git a/cpp/ql/test/query-tests/Critical/MissingCheckScanf/MissingCheckScanf.expected b/cpp/ql/test/query-tests/Critical/MissingCheckScanf/MissingCheckScanf.expected index dac8afd3fd31..1edf3b1ae99f 100644 --- a/cpp/ql/test/query-tests/Critical/MissingCheckScanf/MissingCheckScanf.expected +++ b/cpp/ql/test/query-tests/Critical/MissingCheckScanf/MissingCheckScanf.expected @@ -52,6 +52,9 @@ edges | test.cpp:541:39:541:40 | sscanf output argument | test.cpp:549:8:549:8 | e | provenance | | | test.cpp:541:43:541:44 | sscanf output argument | test.cpp:545:8:545:8 | f | provenance | | | test.cpp:541:43:541:44 | sscanf output argument | test.cpp:550:8:550:8 | f | provenance | | +| test.cpp:559:30:559:31 | scanf output argument | test.cpp:561:9:561:9 | i | provenance | | +| test.cpp:567:35:567:36 | scanf output argument | test.cpp:569:9:569:9 | i | provenance | | +| test.cpp:575:30:575:31 | scanf output argument | test.cpp:577:9:577: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 | @@ -154,6 +157,12 @@ nodes | test.cpp:548:8:548:8 | d | semmle.label | d | | test.cpp:549:8:549:8 | e | semmle.label | e | | test.cpp:550:8:550:8 | f | semmle.label | f | +| test.cpp:559:30:559:31 | scanf output argument | semmle.label | scanf output argument | +| test.cpp:561:9:561:9 | i | semmle.label | i | +| test.cpp:567:35:567:36 | scanf output argument | semmle.label | scanf output argument | +| test.cpp:569:9:569:9 | i | semmle.label | i | +| test.cpp:575:30:575:31 | scanf output argument | semmle.label | scanf output argument | +| test.cpp:577:9:577: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 | @@ -177,3 +186,5 @@ subpaths | test.cpp:484:9:484:9 | i | test.cpp:480:25:480:26 | scanf output argument | test.cpp:484:9:484: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:480:13:480:17 | call to scanf | call to scanf | | test.cpp:495:8:495:8 | i | test.cpp:491:25:491:26 | scanf output argument | test.cpp:495:8:495:8 | 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:491:13:491:17 | call to scanf | call to scanf | | test.cpp:545:8:545:8 | f | test.cpp:541:43:541:44 | sscanf output argument | test.cpp:545:8:545:8 | f | This variable is read, but may not have been written. It should be guarded by a check that the $@ returns at least 3. | test.cpp:541:10:541:15 | call to sscanf | call to sscanf | +| test.cpp:569:9:569:9 | i | test.cpp:567:35:567:36 | scanf output argument | test.cpp:569:9:569: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:567:23:567:27 | call to scanf | call to scanf | +| test.cpp:577:9:577:9 | i | test.cpp:575:30:575:31 | scanf output argument | test.cpp:577:9:577: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:575:18:575:22 | call to scanf | call to scanf | diff --git a/cpp/ql/test/query-tests/Critical/MissingCheckScanf/test.cpp b/cpp/ql/test/query-tests/Critical/MissingCheckScanf/test.cpp index efc37060a554..9cfad40a1480 100644 --- a/cpp/ql/test/query-tests/Critical/MissingCheckScanf/test.cpp +++ b/cpp/ql/test/query-tests/Critical/MissingCheckScanf/test.cpp @@ -553,3 +553,27 @@ void switch_cases(const char *data) { break; } } + +void test_scanf_compared_right_away() { + int i; + bool success = scanf("%d", &i) == 1; + if(success) { + use(i); // GOOD + } +} + +void test_scanf_compared_in_conjunct_right(bool b) { + int i; + bool success = b && scanf("%d", &i) == 1; + if(success) { + use(i); // GOOD [FALSE POSITIVE] + } +} + +void test_scanf_compared_in_conjunct_left(bool b) { + int i; + bool success = scanf("%d", &i) == 1 && b; + if(success) { + use(i); // GOOD [FALSE POSITIVE] + } +}