diff --git a/cpp/ql/src/semmle/code/cpp/controlflow/IRGuards.qll b/cpp/ql/src/semmle/code/cpp/controlflow/IRGuards.qll index 55d5d4d8a84c..fddea8c6d920 100644 --- a/cpp/ql/src/semmle/code/cpp/controlflow/IRGuards.qll +++ b/cpp/ql/src/semmle/code/cpp/controlflow/IRGuards.qll @@ -171,7 +171,7 @@ private class GuardConditionFromIR extends GuardCondition { exists(Instruction li, Instruction ri | li.getUnconvertedResultExpression() = left and ri.getUnconvertedResultExpression() = right and - ir.comparesLt(li, ri, k, isLessThan, testIsTrue) + ir.comparesLt(li.getAUse(), ri.getAUse(), k, isLessThan, testIsTrue) ) } @@ -181,7 +181,7 @@ private class GuardConditionFromIR extends GuardCondition { exists(Instruction li, Instruction ri, boolean testIsTrue | li.getUnconvertedResultExpression() = left and ri.getUnconvertedResultExpression() = right and - ir.comparesLt(li, ri, k, isLessThan, testIsTrue) and + ir.comparesLt(li.getAUse(), ri.getAUse(), k, isLessThan, testIsTrue) and this.controls(block, testIsTrue) ) } @@ -191,7 +191,7 @@ private class GuardConditionFromIR extends GuardCondition { exists(Instruction li, Instruction ri | li.getUnconvertedResultExpression() = left and ri.getUnconvertedResultExpression() = right and - ir.comparesEq(li, ri, k, areEqual, testIsTrue) + ir.comparesEq(li.getAUse(), ri.getAUse(), k, areEqual, testIsTrue) ) } @@ -201,8 +201,8 @@ private class GuardConditionFromIR extends GuardCondition { exists(Instruction li, Instruction ri, boolean testIsTrue | li.getUnconvertedResultExpression() = left and ri.getUnconvertedResultExpression() = right and - ir.comparesEq(li, ri, k, areEqual, testIsTrue) - and this.controls(block, testIsTrue) + ir.comparesEq(li.getAUse(), ri.getAUse(), k, areEqual, testIsTrue) and + this.controls(block, testIsTrue) ) } @@ -269,26 +269,26 @@ class IRGuardCondition extends Instruction { } /** Holds if (determined by this guard) `left < right + k` evaluates to `isLessThan` if this expression evaluates to `testIsTrue`. */ - cached predicate comparesLt(Instruction left, Instruction right, int k, boolean isLessThan, boolean testIsTrue) { + cached predicate comparesLt(Operand left, Operand right, int k, boolean isLessThan, boolean testIsTrue) { compares_lt(this, left, right, k, isLessThan, 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(Instruction left, Instruction right, int k, IRBlock block, boolean isLessThan) { + cached predicate ensuresLt(Operand left, Operand right, int k, IRBlock block, boolean isLessThan) { exists(boolean testIsTrue | compares_lt(this, left, right, k, isLessThan, testIsTrue) and this.controls(block, testIsTrue) ) } /** Holds if (determined by this guard) `left == right + k` evaluates to `areEqual` if this expression evaluates to `testIsTrue`. */ - cached predicate comparesEq(Instruction left, Instruction right, int k, boolean areEqual, boolean testIsTrue) { + cached predicate comparesEq(Operand left, Operand right, int k, boolean areEqual, boolean testIsTrue) { compares_eq(this, left, right, k, areEqual, 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(Instruction left, Instruction right, int k, IRBlock block, boolean areEqual) { + cached predicate ensuresEq(Operand left, Operand right, int k, IRBlock block, boolean areEqual) { exists(boolean testIsTrue | compares_eq(this, left, right, k, areEqual, testIsTrue) and this.controls(block, testIsTrue) ) @@ -328,7 +328,7 @@ private predicate is_condition(Instruction guard) { * * Beware making mistaken logical implications here relating `areEqual` and `testIsTrue`. */ -private predicate compares_eq(Instruction test, Instruction left, Instruction right, int k, boolean areEqual, boolean testIsTrue) { +private predicate compares_eq(Instruction test, Operand left, Operand right, int k, boolean areEqual, boolean testIsTrue) { /* The simple case where the test *is* the comparison so areEqual = testIsTrue xor eq. */ exists(boolean eq | simple_comparison_eq(test, left, right, k, eq) | areEqual = true and testIsTrue = eq or areEqual = false and testIsTrue = eq.booleanNot() @@ -349,13 +349,13 @@ private predicate compares_eq(Instruction test, Instruction left, Instruction ri } /** Rearrange various simple comparisons into `left == right + k` form. */ -private predicate simple_comparison_eq(CompareInstruction cmp, Instruction left, Instruction right, int k, boolean areEqual) { - left = cmp.getLeftOperand() and cmp instanceof CompareEQInstruction and right = cmp.getRightOperand() and k = 0 and areEqual = true +private predicate simple_comparison_eq(CompareInstruction cmp, Operand left, Operand right, int k, boolean areEqual) { + left = cmp.getAnOperand().(LeftOperand) and cmp instanceof CompareEQInstruction and right = cmp.getAnOperand().(RightOperand) and k = 0 and areEqual = true or - left = cmp.getLeftOperand() and cmp instanceof CompareNEInstruction and right = cmp.getRightOperand() and k = 0 and areEqual = false + left = cmp.getAnOperand().(LeftOperand) and cmp instanceof CompareNEInstruction and right = cmp.getAnOperand().(RightOperand) and k = 0 and areEqual = false } -private predicate complex_eq(CompareInstruction cmp, Instruction left, Instruction right, int k, boolean areEqual, boolean testIsTrue) { +private predicate complex_eq(CompareInstruction cmp, Operand left, Operand right, int k, boolean areEqual, boolean testIsTrue) { sub_eq(cmp, left, right, k, areEqual, testIsTrue) or add_eq(cmp, left, right, k, areEqual, testIsTrue) @@ -367,7 +367,7 @@ private predicate complex_eq(CompareInstruction cmp, Instruction left, Instructi */ /** Holds if `left < right + k` evaluates to `isLt` given that test is `testIsTrue`. */ -private predicate compares_lt(Instruction test, Instruction left, Instruction right, int k, boolean isLt, boolean testIsTrue) { +private predicate compares_lt(Instruction test, Operand left, Operand right, int k, boolean isLt, boolean testIsTrue) { /* In the simple case, the test is the comparison, so isLt = testIsTrue */ simple_comparison_lt(test, left, right, k) and isLt = true and testIsTrue = true or @@ -387,22 +387,22 @@ private predicate compares_lt(Instruction test, Instruction left, Instruction ri } /** `(a < b + k) => (b > a - k) => (b >= a + (1-k))` */ -private predicate compares_ge(Instruction test, Instruction left, Instruction right, int k, boolean isGe, boolean testIsTrue) { +private predicate compares_ge(Instruction test, Operand left, Operand right, int k, boolean isGe, boolean testIsTrue) { exists(int onemk | k = 1 - onemk | compares_lt(test, right, left, onemk, isGe, testIsTrue)) } /** Rearrange various simple comparisons into `left < right + k` form. */ -private predicate simple_comparison_lt(CompareInstruction cmp, Instruction left, Instruction right, int k) { - left = cmp.getLeftOperand() and cmp instanceof CompareLTInstruction and right = cmp.getRightOperand() and k = 0 +private predicate simple_comparison_lt(CompareInstruction cmp, Operand left, Operand right, int k) { + left = cmp.getAnOperand().(LeftOperand) and cmp instanceof CompareLTInstruction and right = cmp.getAnOperand().(RightOperand) and k = 0 or - left = cmp.getLeftOperand() and cmp instanceof CompareLEInstruction and right = cmp.getRightOperand() and k = 1 + left = cmp.getAnOperand().(LeftOperand) and cmp instanceof CompareLEInstruction and right = cmp.getAnOperand().(RightOperand) and k = 1 or - right = cmp.getLeftOperand() and cmp instanceof CompareGTInstruction and left = cmp.getRightOperand() and k = 0 + right = cmp.getAnOperand().(LeftOperand) and cmp instanceof CompareGTInstruction and left = cmp.getAnOperand().(RightOperand) and k = 0 or - right = cmp.getLeftOperand() and cmp instanceof CompareGEInstruction and left = cmp.getRightOperand() and k = 1 + right = cmp.getAnOperand().(LeftOperand) and cmp instanceof CompareGEInstruction and left = cmp.getAnOperand().(RightOperand) and k = 1 } -private predicate complex_lt(CompareInstruction cmp, Instruction left, Instruction right, int k, boolean isLt, boolean testIsTrue) { +private predicate complex_lt(CompareInstruction cmp, Operand left, Operand right, int k, boolean isLt, boolean testIsTrue) { sub_lt(cmp, left, right, k, isLt, testIsTrue) or add_lt(cmp, left, right, k, isLt, testIsTrue) @@ -411,33 +411,33 @@ private predicate complex_lt(CompareInstruction cmp, Instruction left, Instructi /* left - x < right + c => left < right + (c+x) left < (right - x) + c => left < right + (c-x) */ -private predicate sub_lt(CompareInstruction cmp, Instruction left, Instruction right, int k, boolean isLt, boolean testIsTrue) { - exists(SubInstruction lhs, int c, int x | compares_lt(cmp, lhs, right, c, isLt, testIsTrue) and - left = lhs.getLeftOperand() and x = int_value(lhs.getRightOperand()) +private predicate sub_lt(CompareInstruction cmp, Operand left, Operand right, int k, boolean isLt, boolean testIsTrue) { + exists(SubInstruction lhs, int c, int x | compares_lt(cmp, lhs.getAUse(), right, c, isLt, testIsTrue) and + left = lhs.getAnOperand().(LeftOperand) and x = int_value(lhs.getRightOperand()) and k = c + x ) or - exists(SubInstruction rhs, int c, int x | compares_lt(cmp, left, rhs, c, isLt, testIsTrue) and - right = rhs.getLeftOperand() and x = int_value(rhs.getRightOperand()) + exists(SubInstruction rhs, int c, int x | compares_lt(cmp, left, rhs.getAUse(), c, isLt, testIsTrue) and + right = rhs.getAnOperand().(LeftOperand) and x = int_value(rhs.getRightOperand()) and k = c - x ) } /* left + x < right + c => left < right + (c-x) left < (right + x) + c => left < right + (c+x) */ -private predicate add_lt(CompareInstruction cmp, Instruction left, Instruction right, int k, boolean isLt, boolean testIsTrue) { - exists(AddInstruction lhs, int c, int x | compares_lt(cmp, lhs, right, c, isLt, testIsTrue) and - (left = lhs.getLeftOperand() and x = int_value(lhs.getRightOperand()) +private predicate add_lt(CompareInstruction cmp, Operand left, Operand right, int k, boolean isLt, boolean testIsTrue) { + exists(AddInstruction lhs, int c, int x | compares_lt(cmp, lhs.getAUse(), right, c, isLt, testIsTrue) and + (left = lhs.getAnOperand().(LeftOperand) and x = int_value(lhs.getRightOperand()) or - left = lhs.getRightOperand() and x = int_value(lhs.getLeftOperand()) + left = lhs.getAnOperand().(RightOperand) and x = int_value(lhs.getLeftOperand()) ) and k = c - x ) or - exists(AddInstruction rhs, int c, int x | compares_lt(cmp, left, rhs, c, isLt, testIsTrue) and - (right = rhs.getLeftOperand() and x = int_value(rhs.getRightOperand()) + exists(AddInstruction rhs, int c, int x | compares_lt(cmp, left, rhs.getAUse(), c, isLt, testIsTrue) and + (right = rhs.getAnOperand().(LeftOperand) and x = int_value(rhs.getRightOperand()) or - right = rhs.getRightOperand() and x = int_value(rhs.getLeftOperand()) + right = rhs.getAnOperand().(RightOperand) and x = int_value(rhs.getLeftOperand()) ) and k = c + x ) @@ -446,14 +446,14 @@ private predicate add_lt(CompareInstruction cmp, Instruction left, Instruction r /* left - x == right + c => left == right + (c+x) left == (right - x) + c => left == right + (c-x) */ -private predicate sub_eq(CompareInstruction cmp, Instruction left, Instruction right, int k, boolean areEqual, boolean testIsTrue) { - exists(SubInstruction lhs, int c, int x | compares_eq(cmp, lhs, right, c, areEqual, testIsTrue) and - left = lhs.getLeftOperand() and x = int_value(lhs.getRightOperand()) +private predicate sub_eq(CompareInstruction cmp, Operand left, Operand right, int k, boolean areEqual, boolean testIsTrue) { + exists(SubInstruction lhs, int c, int x | compares_eq(cmp, lhs.getAUse(), right, c, areEqual, testIsTrue) and + left = lhs.getAnOperand().(LeftOperand) and x = int_value(lhs.getRightOperand()) and k = c + x ) or - exists(SubInstruction rhs, int c, int x | compares_eq(cmp, left, rhs, c, areEqual, testIsTrue) and - right = rhs.getLeftOperand() and x = int_value(rhs.getRightOperand()) + exists(SubInstruction rhs, int c, int x | compares_eq(cmp, left, rhs.getAUse(), c, areEqual, testIsTrue) and + right = rhs.getAnOperand().(LeftOperand) and x = int_value(rhs.getRightOperand()) and k = c - x ) } @@ -461,19 +461,19 @@ private predicate sub_eq(CompareInstruction cmp, Instruction left, Instruction r /* left + x == right + c => left == right + (c-x) left == (right + x) + c => left == right + (c+x) */ -private predicate add_eq(CompareInstruction cmp, Instruction left, Instruction right, int k, boolean areEqual, boolean testIsTrue) { - exists(AddInstruction lhs, int c, int x | compares_eq(cmp, lhs, right, c, areEqual, testIsTrue) and - (left = lhs.getLeftOperand() and x = int_value(lhs.getRightOperand()) +private predicate add_eq(CompareInstruction cmp, Operand left, Operand right, int k, boolean areEqual, boolean testIsTrue) { + exists(AddInstruction lhs, int c, int x | compares_eq(cmp, lhs.getAUse(), right, c, areEqual, testIsTrue) and + (left = lhs.getAnOperand().(LeftOperand) and x = int_value(lhs.getRightOperand()) or - left = lhs.getRightOperand() and x = int_value(lhs.getLeftOperand()) + left = lhs.getAnOperand().(RightOperand) and x = int_value(lhs.getLeftOperand()) ) and k = c - x ) or - exists(AddInstruction rhs, int c, int x | compares_eq(cmp, left, rhs, c, areEqual, testIsTrue) and - (right = rhs.getLeftOperand() and x = int_value(rhs.getRightOperand()) + exists(AddInstruction rhs, int c, int x | compares_eq(cmp, left, rhs.getAUse(), c, areEqual, testIsTrue) and + (right = rhs.getAnOperand().(LeftOperand) and x = int_value(rhs.getRightOperand()) or - right = rhs.getRightOperand() and x = int_value(rhs.getLeftOperand()) + right = rhs.getAnOperand().(RightOperand) and x = int_value(rhs.getLeftOperand()) ) and k = c + x ) diff --git a/cpp/ql/src/semmle/code/cpp/ir/implementation/aliased_ssa/Instruction.qll b/cpp/ql/src/semmle/code/cpp/ir/implementation/aliased_ssa/Instruction.qll index c95cb23814e6..99255b8ffa52 100644 --- a/cpp/ql/src/semmle/code/cpp/ir/implementation/aliased_ssa/Instruction.qll +++ b/cpp/ql/src/semmle/code/cpp/ir/implementation/aliased_ssa/Instruction.qll @@ -761,6 +761,12 @@ class RemInstruction extends BinaryInstruction { } } +class NegateInstruction extends UnaryInstruction { + NegateInstruction() { + opcode instanceof Opcode::Negate + } +} + class BitAndInstruction extends BinaryInstruction { BitAndInstruction() { opcode instanceof Opcode::BitAnd diff --git a/cpp/ql/src/semmle/code/cpp/ir/implementation/raw/Instruction.qll b/cpp/ql/src/semmle/code/cpp/ir/implementation/raw/Instruction.qll index c95cb23814e6..99255b8ffa52 100644 --- a/cpp/ql/src/semmle/code/cpp/ir/implementation/raw/Instruction.qll +++ b/cpp/ql/src/semmle/code/cpp/ir/implementation/raw/Instruction.qll @@ -761,6 +761,12 @@ class RemInstruction extends BinaryInstruction { } } +class NegateInstruction extends UnaryInstruction { + NegateInstruction() { + opcode instanceof Opcode::Negate + } +} + class BitAndInstruction extends BinaryInstruction { BitAndInstruction() { opcode instanceof Opcode::BitAnd diff --git a/cpp/ql/src/semmle/code/cpp/ir/implementation/unaliased_ssa/Instruction.qll b/cpp/ql/src/semmle/code/cpp/ir/implementation/unaliased_ssa/Instruction.qll index c95cb23814e6..99255b8ffa52 100644 --- a/cpp/ql/src/semmle/code/cpp/ir/implementation/unaliased_ssa/Instruction.qll +++ b/cpp/ql/src/semmle/code/cpp/ir/implementation/unaliased_ssa/Instruction.qll @@ -761,6 +761,12 @@ class RemInstruction extends BinaryInstruction { } } +class NegateInstruction extends UnaryInstruction { + NegateInstruction() { + opcode instanceof Opcode::Negate + } +} + class BitAndInstruction extends BinaryInstruction { BitAndInstruction() { opcode instanceof Opcode::BitAnd diff --git a/cpp/ql/src/semmle/code/cpp/rangeanalysis/SignAnalysis.qll b/cpp/ql/src/semmle/code/cpp/rangeanalysis/SignAnalysis.qll new file mode 100644 index 000000000000..5e38b45602cb --- /dev/null +++ b/cpp/ql/src/semmle/code/cpp/rangeanalysis/SignAnalysis.qll @@ -0,0 +1,483 @@ +/** + * Provides sign analysis to determine whether expression are always positive + * or negative. + * + * The analysis is implemented as an abstract interpretation over the + * three-valued domain `{negative, zero, positive}`. + */ +import cpp +private import semmle.code.cpp.ir.IR +private import semmle.code.cpp.controlflow.IRGuards +private import semmle.code.cpp.ir.ValueNumbering +private import SignAnalysisCached + +private newtype TSign = TNeg() or TZero() or TPos() +private class Sign extends TSign { + string toString() { + result = "-" and this = TNeg() or + result = "0" and this = TZero() or + result = "+" and this = TPos() + } + Sign inc() { + this = TNeg() and result = TNeg() or + this = TNeg() and result = TZero() or + this = TZero() and result = TPos() or + this = TPos() and result = TPos() + } + Sign dec() { + result.inc() = this + } + Sign neg() { + this = TNeg() and result = TPos() or + this = TZero() and result = TZero() or + this = TPos() and result = TNeg() + } + Sign bitnot() { + this = TNeg() and result = TPos() or + this = TNeg() and result = TZero() or + this = TZero() and result = TNeg() or + this = TPos() and result = TNeg() + } + Sign add(Sign s) { + this = TZero() and result = s or + s = TZero() and result = this or + this = s and this = result or + this = TPos() and s = TNeg() or + this = TNeg() and s = TPos() + } + Sign mul(Sign s) { + result = TZero() and this = TZero() or + result = TZero() and s = TZero() or + result = TNeg() and this = TPos() and s = TNeg() or + result = TNeg() and this = TNeg() and s = TPos() or + result = TPos() and this = TPos() and s = TPos() or + result = TPos() and this = TNeg() and s = TNeg() + } + Sign div(Sign s) { + result = TZero() and s = TNeg() or + result = TZero() and s = TPos() or + result = TNeg() and this = TPos() and s = TNeg() or + result = TNeg() and this = TNeg() and s = TPos() or + result = TPos() and this = TPos() and s = TPos() or + result = TPos() and this = TNeg() and s = TNeg() + } + Sign rem(Sign s) { + result = TZero() and s = TNeg() or + result = TZero() and s = TPos() or + result = this and s = TNeg() or + result = this and s = TPos() + } + Sign bitand(Sign s) { + result = TZero() and this = TZero() or + result = TZero() and s = TZero() or + result = TZero() and this = TPos() or + result = TZero() and s = TPos() or + result = TNeg() and this = TNeg() and s = TNeg() or + result = TPos() and this = TNeg() and s = TPos() or + result = TPos() and this = TPos() and s = TNeg() or + result = TPos() and this = TPos() and s = TPos() + } + Sign bitor(Sign s) { + result = TZero() and this = TZero() and s = TZero() or + result = TNeg() and this = TNeg() or + result = TNeg() and s = TNeg() or + result = TPos() and this = TPos() and s = TZero() or + result = TPos() and this = TZero() and s = TPos() or + result = TPos() and this = TPos() and s = TPos() + } + Sign bitxor(Sign s) { + result = TZero() and this = s or + result = this and s = TZero() or + result = s and this = TZero() or + result = TPos() and this = TPos() and s = TPos() or + result = TNeg() and this = TNeg() and s = TPos() or + result = TNeg() and this = TPos() and s = TNeg() or + result = TPos() and this = TNeg() and s = TNeg() + } + Sign lshift(Sign s) { + result = TZero() and this = TZero() or + result = this and s = TZero() or + this != TZero() and s != TZero() + } + Sign rshift(Sign s) { + result = TZero() and this = TZero() or + result = this and s = TZero() or + result = TNeg() and this = TNeg() or + result != TNeg() and this = TPos() and s != TZero() + } + Sign urshift(Sign s) { + result = TZero() and this = TZero() or + result = this and s = TZero() or + result != TZero() and this = TNeg() and s != TZero() or + result != TNeg() and this = TPos() and s != TZero() + } +} + +private Sign certainInstructionSign(Instruction inst) { + exists(int i | inst.(IntegerConstantInstruction).getValue().toInt() = i | + i < 0 and result = TNeg() or + i = 0 and result = TZero() or + i > 0 and result = TPos() + ) + or + exists(float f | f = inst.(FloatConstantInstruction).getValue().toFloat() | + f < 0 and result = TNeg() or + f = 0 and result = TZero() or + f > 0 and result = TPos() + ) +} + +private newtype CastKind = TWiden() or TSame() or TNarrow() + +private CastKind getCastKind(ConvertInstruction ci) { + exists(int fromSize, int toSize | + toSize = ci.getResultSize() and + fromSize = ci.getOperand().getResultSize() + | + fromSize < toSize and + result = TWiden() + or + fromSize = toSize and + result = TSame() + or + fromSize > toSize and + result = TNarrow() + ) +} + +private predicate bindBool(boolean bool) { + bool = true or + bool = false +} + +private Sign castSign(Sign s, boolean fromSigned, boolean toSigned, CastKind ck) { + result = TZero() and + ( + bindBool(fromSigned) and + bindBool(toSigned) and + s = TZero() + or + bindBool(fromSigned) and + bindBool(toSigned) and + ck = TNarrow() + ) + or + result = TPos() and + ( + bindBool(fromSigned) and + bindBool(toSigned) and + s = TPos() + or + bindBool(fromSigned) and + bindBool(toSigned) and + s = TNeg() and + ck = TNarrow() + or + fromSigned = true and + toSigned = false and + s = TNeg() + ) + or + result = TNeg() and + ( + fromSigned = true and + toSigned = true and + s = TNeg() + or + fromSigned = false and + toSigned = true and + s = TPos() and + ck != TWiden() + ) +} + +/** Holds if the sign of `e` is too complicated to determine. */ +private predicate unknownSign(Instruction i) { + ( + i instanceof UnmodeledDefinitionInstruction + or + i instanceof UninitializedInstruction + or + i instanceof InitializeParameterInstruction + or + i instanceof BuiltInInstruction + or + i instanceof CallInstruction + ) +} + +/** + * Holds if `lowerbound` is a lower bound for `bounded`. This is restricted + * to only include bounds for which we might determine a sign. + */ +private predicate lowerBound(IRGuardCondition comp, Operand lowerbound, Operand bounded, boolean isStrict) { + exists(int adjustment, Operand compared | + valueNumber(bounded.getDefinitionInstruction()) = valueNumber(compared.getDefinitionInstruction()) and + ( + isStrict = true and + adjustment = 0 + or + isStrict = false and + adjustment = 1 + ) and + comp.ensuresLt(lowerbound, compared, adjustment, bounded.getInstruction().getBlock(), true) + ) +} + + +/** + * Holds if `upperbound` is an upper bound for `bounded` at `pos`. This is restricted + * to only include bounds for which we might determine a sign. + */ +private predicate upperBound(IRGuardCondition comp, Operand upperbound, Operand bounded, boolean isStrict) { + exists(int adjustment, Operand compared | + valueNumber(bounded.getDefinitionInstruction()) = valueNumber(compared.getDefinitionInstruction()) and + ( + isStrict = true and + adjustment = 0 + or + isStrict = false and + adjustment = 1 + ) and + comp.ensuresLt(compared, upperbound, adjustment, bounded.getInstruction().getBlock(), true) + ) +} + +/** + * Holds if `eqbound` is an equality/inequality for `bounded` at `pos`. This is + * restricted to only include bounds for which we might determine a sign. The + * boolean `isEq` gives the polarity: + * - `isEq = true` : `bounded = eqbound` + * - `isEq = false` : `bounded != eqbound` + */ +private predicate eqBound(IRGuardCondition guard, Operand eqbound, Operand bounded, boolean isEq) { + exists(Operand compared | + valueNumber(bounded.getDefinitionInstruction()) = valueNumber(compared.getDefinitionInstruction()) and + guard.ensuresEq(compared, eqbound, 0, bounded.getInstruction().getBlock(), isEq) + ) +} + + + +/** + * Holds if `bound` is a bound for `v` at `pos` that needs to be positive in + * order for `v` to be positive. + */ +private predicate posBound(IRGuardCondition comp, Operand bound, Operand op) { + upperBound(comp, bound, op, _) or + eqBound(comp, bound, op, true) +} + +/** + * Holds if `bound` is a bound for `v` at `pos` that needs to be negative in + * order for `v` to be negative. + */ +private predicate negBound(IRGuardCondition comp, Operand bound, Operand op) { + lowerBound(comp, bound, op, _) or + eqBound(comp, bound, op, true) +} + +/** + * Holds if `bound` is a bound for `v` at `pos` that can restrict whether `v` + * can be zero. + */ +private predicate zeroBound(IRGuardCondition comp, Operand bound, Operand op) { + lowerBound(comp, bound, op, _) or + upperBound(comp, bound, op, _) or + eqBound(comp, bound, op, _) +} + +/** Holds if `bound` allows `v` to be positive at `pos`. */ +private predicate posBoundOk(IRGuardCondition comp, Operand bound, Operand op) { + posBound(comp, bound, op) and TPos() = operandSign(bound) +} + +/** Holds if `bound` allows `v` to be negative at `pos`. */ +private predicate negBoundOk(IRGuardCondition comp, Operand bound, Operand op) { + negBound(comp, bound, op) and TNeg() = operandSign(bound) +} + +/** Holds if `bound` allows `v` to be zero at `pos`. */ +private predicate zeroBoundOk(IRGuardCondition comp, Operand bound, Operand op) { + lowerBound(comp, bound, op, _) and TNeg() = operandSign(bound) or + lowerBound(comp, bound, op, false) and TZero() = operandSign(bound) or + upperBound(comp, bound, op, _) and TPos() = operandSign(bound) or + upperBound(comp, bound, op, false) and TZero() = operandSign(bound) or + eqBound(comp, bound, op, true) and TZero() = operandSign(bound) or + eqBound(comp, bound, op, false) and TZero() != operandSign(bound) +} + +private Sign binaryOpLhsSign(Instruction i) { + result = operandSign(i.getAnOperand().(LeftOperand)) +} + +private Sign binaryOpRhsSign(Instruction i) { + result = operandSign(i.getAnOperand().(RightOperand)) +} + +pragma[noinline] +private predicate binaryOpSigns(Instruction i, Sign lhs, Sign rhs) { + lhs = binaryOpLhsSign(i) and + rhs = binaryOpRhsSign(i) +} + +private Sign unguardedOperandSign(Operand operand) { + result = instructionSign(operand.getDefinitionInstruction()) and + not hasGuard(operand, result) +} + +private Sign guardedOperandSign(Operand operand) { + result = instructionSign(operand.getDefinitionInstruction()) and + hasGuard(operand, result) +} + +private Sign guardedOperandSignOk(Operand operand) { + result = TPos() and forex(IRGuardCondition guard, Operand bound | posBound(guard, bound, operand) | posBoundOk(guard, bound, operand)) or + result = TNeg() and forex(IRGuardCondition guard, Operand bound | negBound(guard, bound, operand) | negBoundOk(guard, bound, operand)) or + result = TZero() and forex(IRGuardCondition guard, Operand bound | zeroBound(guard, bound, operand) | zeroBoundOk(guard, bound, operand)) +} + +/** + * Holds if there is a bound that might restrict whether `v` has the sign `s` + * at `pos`. + */ +private predicate hasGuard(Operand op, Sign s) { + s = TPos() and posBound(_, _, op) + or + s = TNeg() and negBound(_, _, op) + or + s = TZero() and zeroBound(_, _, op) +} + +cached module SignAnalysisCached { + /** + * Gets a sign that `operand` may have at `pos`, taking guards into account. + */ + cached + Sign operandSign(Operand operand) { + result = unguardedOperandSign(operand) + or + result = guardedOperandSign(operand) and + result = guardedOperandSignOk(operand) + } + + cached + Sign instructionSign(Instruction i) { + result = certainInstructionSign(i) + or + not exists(certainInstructionSign(i)) and + not ( + result = TNeg() and + i.getResultType().(IntegralType).isUnsigned() + ) and + ( + unknownSign(i) + or + exists(ConvertInstruction ci, Instruction prior, boolean fromSigned, boolean toSigned | + i = ci and + prior = ci.getOperand() and + ( + if ci.getResultType().(IntegralType).isSigned() + then toSigned = true + else toSigned = false + ) and + ( + if prior.getResultType().(IntegralType).isSigned() + then fromSigned = true + else fromSigned = false + ) and + result = castSign(operandSign(ci.getAnOperand()), fromSigned, toSigned, getCastKind(ci)) + ) + or + result = operandSign(i.getAnOperand().(CopySourceOperand)) + or + result = operandSign(i.(BitComplementInstruction).getAnOperand()).bitnot() + or + result = operandSign(i.(NegateInstruction).getAnOperand()).neg() + or + exists(Sign s1, Sign s2 | + binaryOpSigns(i, s1, s2) + | + i instanceof AddInstruction and result = s1.add(s2) + or + i instanceof SubInstruction and result = s1.add(s2.neg()) + or + i instanceof MulInstruction and result = s1.mul(s2) + or + i instanceof DivInstruction and result = s1.div(s2) + or + i instanceof RemInstruction and result = s1.rem(s2) + or + i instanceof BitAndInstruction and result = s1.bitand(s2) + or + i instanceof BitOrInstruction and result = s1.bitor(s2) + or + i instanceof BitXorInstruction and result = s1.bitxor(s2) + or + i instanceof ShiftLeftInstruction and result = s1.lshift(s2) + or + i instanceof ShiftRightInstruction and + i.getResultType().(IntegralType).isSigned() and + result = s1.rshift(s2) + or + i instanceof ShiftRightInstruction and + not i.getResultType().(IntegralType).isSigned() and + result = s1.urshift(s2) + ) + or + // use hasGuard here? + result = operandSign(i.(PhiInstruction).getAnOperand()) + ) + } +} + +/** Holds if `i` can be positive and cannot be negative. */ +predicate positiveInstruction(Instruction i) { + instructionSign(i) = TPos() and + not instructionSign(i) = TNeg() +} + +/** Holds if `i` at `pos` can be positive at and cannot be negative. */ +predicate positive(Operand op) { + operandSign(op) = TPos() and + not operandSign(op) = TNeg() +} + +/** Holds if `i` can be negative and cannot be positive. */ +predicate negativeInstruction(Instruction i) { + instructionSign(i) = TNeg() and + not instructionSign(i) = TPos() +} + +/** Holds if `i` at `pos` can be negative and cannot be positive. */ +predicate negative(Operand op) { + operandSign(op) = TNeg() and + not operandSign(op) = TPos() +} + +/** Holds if `i` is strictly positive. */ +predicate strictlyPositiveInstruction(Instruction i) { + instructionSign(i) = TPos() and + not instructionSign(i) = TNeg() and + not instructionSign(i) = TZero() +} + +/** Holds if `i` is strictly positive at `pos`. */ +predicate strictlyPositive(Operand op) { + operandSign(op) = TPos() and + not operandSign(op) = TNeg() and + not operandSign(op) = TZero() +} +/** Holds if `i` is strictly negative. */ +predicate strictlyNegativeInstruction(Instruction i) { + instructionSign(i) = TNeg() and + not instructionSign(i) = TPos() and + not instructionSign(i) = TZero() +} + +/** Holds if `i` is strictly negative at `pos`. */ +predicate strictlyNegative(Operand op) { + operandSign(op) = TNeg() and + not operandSign(op) = TPos() and + not operandSign(op) = TZero() +} diff --git a/cpp/ql/test/library-tests/controlflow/guards-ir/tests.ql b/cpp/ql/test/library-tests/controlflow/guards-ir/tests.ql index 2bb8b2f9fa99..173ce6c5d890 100644 --- a/cpp/ql/test/library-tests/controlflow/guards-ir/tests.ql +++ b/cpp/ql/test/library-tests/controlflow/guards-ir/tests.ql @@ -51,7 +51,7 @@ query predicate irGuards(IRGuardCondition guard) { } query predicate irGuardsCompare(int startLine, string msg) { - exists(IRGuardCondition guard, Instruction left, Instruction right, int k, string which, string op | + exists(IRGuardCondition guard, Operand left, Operand right, int k, string which, string op | exists(boolean sense | sense = true and which = "true" or sense = false and which = "false" @@ -65,7 +65,7 @@ query predicate irGuardsCompare(int startLine, string msg) { guard.comparesEq(left, right, k, false, sense) and op = " != " ) and startLine = guard.getLocation().getStartLine() - and msg = left.getUnconvertedResultExpression() + op + right.getUnconvertedResultExpression() + "+" + k + " when " + guard + " is " + which + and msg = left.getDefinitionInstruction().getUnconvertedResultExpression() + op + right.getDefinitionInstruction().getUnconvertedResultExpression() + "+" + k + " when " + guard + " is " + which ) } query predicate irGuardsControl(IRGuardCondition guard, boolean sense, int start, int end) { @@ -77,15 +77,18 @@ query predicate irGuardsControl(IRGuardCondition guard, boolean sense, int start query predicate irGuardsEnsure(IRGuardCondition guard, Instruction left, string op, Instruction right, int k, int start, int end) { - exists(IRBlock block | - guard.ensuresLt(left, right, k, block, true) and op = "<" - or - guard.ensuresLt(left, right, k, block, false) and op = ">=" - or - guard.ensuresEq(left, right, k, block, true) and op = "==" - or - guard.ensuresEq(left, right, k, block, false) and op = "!=" - | - block.getLocation().hasLocationInfo(_, start, _, end, _) + + exists(IRBlock block, Operand leftOp, Operand rightOp | + guard.ensuresLt(leftOp, rightOp, k, block, true) and op = "<" + or + guard.ensuresLt(leftOp, rightOp, k, block, false) and op = ">=" + or + guard.ensuresEq(leftOp, rightOp, k, block, true) and op = "==" + or + guard.ensuresEq(leftOp, rightOp, k, block, false) and op = "!=" + | + leftOp = left.getAUse() and + rightOp = right.getAUse() and + block.getLocation().hasLocationInfo(_, start, _, end, _) ) } diff --git a/cpp/ql/test/library-tests/rangeanalysis/signanalysis/SignAnalysis.expected b/cpp/ql/test/library-tests/rangeanalysis/signanalysis/SignAnalysis.expected new file mode 100644 index 000000000000..a1ebaf0f7bc5 --- /dev/null +++ b/cpp/ql/test/library-tests/rangeanalysis/signanalysis/SignAnalysis.expected @@ -0,0 +1,688 @@ +| binary_logical_operator.c:2:11:2:25 | Constant: ... && ... | positive strictlyPositive | +| binary_logical_operator.c:2:11:2:25 | Load: ... && ... | positive | +| binary_logical_operator.c:2:11:2:25 | Phi: ... && ... | positive | +| binary_logical_operator.c:2:11:2:25 | Store: ... && ... | positive | +| binary_logical_operator.c:2:11:2:25 | Store: ... && ... | positive strictlyPositive | +| binary_logical_operator.c:2:15:2:16 | Constant: 10 | positive strictlyPositive | +| binary_logical_operator.c:3:7:3:7 | Load: b | positive | +| bounded_bounds.c:3:12:3:12 | Load: x | negative strictlyNegative | +| bounded_bounds.c:3:12:3:12 | Store: x | negative strictlyNegative | +| bounded_bounds.c:5:7:5:7 | Load: x | positive | +| bounded_bounds.c:6:11:6:11 | Load: y | positive strictlyPositive | +| bounded_bounds.c:6:11:6:11 | Store: y | positive strictlyPositive | +| bounded_bounds.c:16:12:16:12 | Load: x | negative strictlyNegative | +| bounded_bounds.c:16:12:16:12 | Store: x | negative strictlyNegative | +| inline_assembly.c:9:23:9:23 | Uninitialized: definition of y | positive | +| inline_assembly.c:10:3:10:7 | Store: ... = ... | positive strictlyPositive | +| inline_assembly.c:10:7:10:7 | Constant: (unsigned int)... | positive strictlyPositive | +| inline_assembly.c:12:32:12:32 | Load: y | positive strictlyPositive | +| minmax.c:16:9:16:10 | Constant: 1 | positive strictlyPositive | +| minmax.c:16:9:16:10 | Store: 1 | positive strictlyPositive | +| minmax.c:16:16:16:17 | Constant: 2 | positive strictlyPositive | +| minmax.c:16:16:16:17 | Store: 2 | positive strictlyPositive | +| minmax.c:16:23:16:24 | Constant: 3 | positive strictlyPositive | +| minmax.c:16:23:16:24 | Store: 3 | positive strictlyPositive | +| minmax.c:18:37:18:37 | Load: x | positive strictlyPositive | +| minmax.c:18:40:18:40 | Load: y | positive strictlyPositive | +| minmax.c:18:43:18:43 | Load: z | positive strictlyPositive | +| test.c:7:10:7:10 | Phi: p | positive | +| test.c:8:5:8:19 | Store: ... = ... | positive strictlyPositive | +| test.c:8:13:8:17 | Load: count | positive | +| test.c:8:13:8:19 | Add: ... + ... | positive strictlyPositive | +| test.c:8:19:8:19 | Constant: 1 | positive strictlyPositive | +| test.c:10:10:10:14 | Load: count | positive | +| test.c:10:10:10:14 | Store: count | positive | +| test.c:15:10:15:10 | Phi: p | positive | +| test.c:16:5:16:26 | Store: ... = ... | positive | +| test.c:16:13:16:26 | Rem: ... % ... | positive | +| test.c:16:14:16:18 | Load: count | positive | +| test.c:16:14:16:20 | Add: ... + ... | positive strictlyPositive | +| test.c:16:20:16:20 | Constant: 1 | positive strictlyPositive | +| test.c:16:25:16:26 | Constant: 10 | positive strictlyPositive | +| test.c:18:10:18:14 | Load: count | positive | +| test.c:18:10:18:14 | Store: count | positive | +| test.c:23:10:23:10 | Phi: p | positive | +| test.c:24:5:24:11 | Add: ... ++ | positive strictlyPositive | +| test.c:24:5:24:11 | Constant: ... ++ | positive strictlyPositive | +| test.c:24:5:24:11 | Load: ... ++ | positive | +| test.c:24:5:24:11 | Store: ... ++ | positive strictlyPositive | +| test.c:25:5:25:22 | Store: ... = ... | positive | +| test.c:25:13:25:17 | Load: count | positive strictlyPositive | +| test.c:25:13:25:22 | Rem: ... % ... | positive | +| test.c:25:21:25:22 | Constant: 10 | positive strictlyPositive | +| test.c:27:10:27:14 | Load: count | positive | +| test.c:27:10:27:14 | Store: count | positive | +| test.c:33:15:33:15 | Load: i | positive | +| test.c:33:15:33:15 | Phi: i | positive | +| test.c:33:15:33:15 | Phi: i | positive | +| test.c:33:19:33:19 | Constant: 2 | positive strictlyPositive | +| test.c:33:22:33:28 | Store: ... = ... | positive strictlyPositive | +| test.c:33:26:33:26 | Load: i | positive | +| test.c:33:26:33:28 | Add: ... + ... | positive strictlyPositive | +| test.c:33:28:33:28 | Constant: 1 | positive strictlyPositive | +| test.c:34:5:34:14 | Add: ... += ... | positive | +| test.c:34:5:34:14 | Load: ... += ... | positive | +| test.c:34:5:34:14 | Store: ... += ... | positive | +| test.c:34:14:34:14 | Load: i | positive | +| test.c:36:10:36:14 | Load: total | positive | +| test.c:36:10:36:18 | Add: ... + ... | positive | +| test.c:36:10:36:18 | Store: ... + ... | positive | +| test.c:36:18:36:18 | Load: i | positive | +| test.c:42:15:42:15 | Load: i | positive | +| test.c:42:15:42:15 | Phi: i | positive | +| test.c:42:15:42:15 | Phi: i | positive | +| test.c:42:19:42:19 | Constant: 2 | positive strictlyPositive | +| test.c:42:22:42:24 | Add: ... ++ | positive strictlyPositive | +| test.c:42:22:42:24 | Constant: ... ++ | positive strictlyPositive | +| test.c:42:22:42:24 | Load: ... ++ | positive | +| test.c:42:22:42:24 | Store: ... ++ | positive strictlyPositive | +| test.c:43:5:43:14 | Add: ... += ... | positive | +| test.c:43:5:43:14 | Load: ... += ... | positive | +| test.c:43:5:43:14 | Store: ... += ... | positive | +| test.c:43:14:43:14 | Load: i | positive | +| test.c:45:10:45:14 | Load: total | positive | +| test.c:45:10:45:18 | Add: ... + ... | positive | +| test.c:45:10:45:18 | Store: ... + ... | positive | +| test.c:45:18:45:18 | Load: i | positive | +| test.c:51:15:51:15 | Load: i | positive | +| test.c:51:15:51:15 | Phi: i | positive | +| test.c:51:15:51:15 | Phi: i | positive | +| test.c:51:15:51:17 | Add: ... + ... | positive strictlyPositive | +| test.c:51:17:51:17 | Constant: 2 | positive strictlyPositive | +| test.c:51:21:51:21 | Constant: 4 | positive strictlyPositive | +| test.c:51:24:51:30 | Store: ... = ... | positive strictlyPositive | +| test.c:51:28:51:28 | Load: i | positive | +| test.c:51:28:51:30 | Add: ... + ... | positive strictlyPositive | +| test.c:51:30:51:30 | Constant: 1 | positive strictlyPositive | +| test.c:52:5:52:14 | Add: ... += ... | positive | +| test.c:52:5:52:14 | Load: ... += ... | positive | +| test.c:52:5:52:14 | Store: ... += ... | positive | +| test.c:52:14:52:14 | Load: i | positive | +| test.c:54:10:54:14 | Load: total | positive | +| test.c:54:10:54:18 | Add: ... + ... | positive | +| test.c:54:10:54:18 | Store: ... + ... | positive | +| test.c:54:18:54:18 | Load: i | positive | +| test.c:58:11:58:11 | Constant: 4 | positive strictlyPositive | +| test.c:59:13:59:13 | Constant: 5 | positive strictlyPositive | +| test.c:63:10:63:10 | Constant: 1 | positive strictlyPositive | +| test.c:63:10:63:10 | Store: 1 | positive strictlyPositive | +| test.c:67:7:67:11 | Constant: - ... | negative strictlyNegative | +| test.c:67:24:67:25 | Constant: 10 | positive strictlyPositive | +| test.c:68:15:68:15 | Constant: 2 | positive strictlyPositive | +| test.c:77:13:77:13 | Constant: 4 | positive strictlyPositive | +| test.c:81:13:81:13 | Constant: 4 | positive strictlyPositive | +| test.c:82:14:82:14 | Constant: 1 | positive strictlyPositive | +| test.c:82:14:82:14 | Store: 1 | positive strictlyPositive | +| test.c:88:5:88:10 | Phi: test10 | positive | +| test.c:89:11:89:11 | Constant: 7 | positive strictlyPositive | +| test.c:90:13:90:13 | Load: y | positive strictlyPositive | +| test.c:93:12:93:12 | Load: x | positive strictlyPositive | +| test.c:93:12:93:12 | Store: x | positive strictlyPositive | +| test.c:95:10:95:10 | Constant: 1 | positive strictlyPositive | +| test.c:95:10:95:10 | Store: 1 | positive strictlyPositive | +| test.c:98:5:98:10 | Phi: test11 | positive | +| test.c:102:6:102:8 | Constant: ... ++ | positive strictlyPositive | +| test.c:104:12:104:14 | Constant: 58 | positive strictlyPositive | +| test.c:107:8:107:10 | Constant: ... ++ | positive strictlyPositive | +| test.c:109:14:109:16 | Constant: 44 | positive strictlyPositive | +| test.c:110:14:110:14 | Constant: 1 | positive strictlyPositive | +| test.c:110:14:110:14 | Store: 1 | positive strictlyPositive | +| test.c:119:10:119:12 | Add: ... ++ | positive strictlyPositive | +| test.c:119:10:119:12 | Constant: ... ++ | positive strictlyPositive | +| test.c:119:10:119:12 | Store: ... ++ | positive strictlyPositive | +| test.c:124:11:124:15 | Load: Start | positive | +| test.c:124:11:124:15 | Phi: Start | positive | +| test.c:124:20:124:32 | Call: call to test12_helper | positive | +| test.c:124:20:124:36 | Sub: ... - ... | positive | +| test.c:124:36:124:36 | Constant: (unsigned long long)... | positive strictlyPositive | +| test.c:126:31:126:43 | Call: call to test12_helper | positive | +| test.c:126:31:126:43 | Store: call to test12_helper | positive | +| test.c:127:6:127:24 | Add: ... += ... | positive strictlyPositive | +| test.c:127:6:127:24 | Load: ... += ... | positive | +| test.c:127:6:127:24 | Store: ... += ... | positive strictlyPositive | +| test.c:127:15:127:20 | Load: Length | positive | +| test.c:127:15:127:24 | Add: ... + ... | positive strictlyPositive | +| test.c:127:24:127:24 | Constant: (unsigned long long)... | positive strictlyPositive | +| test.c:130:11:130:11 | Constant: 1 | positive strictlyPositive | +| test.c:130:11:130:11 | Store: 1 | positive strictlyPositive | +| test.c:135:22:135:22 | Convert: (unsigned char)... | positive | +| test.c:135:22:135:22 | Store: (unsigned char)... | positive | +| test.c:137:22:137:22 | Constant: (unsigned int)... | positive strictlyPositive | +| test.c:138:13:138:13 | Constant: 1 | positive strictlyPositive | +| test.c:139:19:139:28 | Convert: (unsigned int)... | positive | +| test.c:139:19:139:32 | Add: ... + ... | positive | +| test.c:139:27:139:28 | Convert: (int)... | positive | +| test.c:139:27:139:28 | Load: uc | positive | +| test.c:139:40:139:40 | Convert: (unsigned int)... | positive | +| test.c:145:12:145:32 | Convert: (int)... | positive | +| test.c:145:12:145:32 | Store: (int)... | positive | +| test.c:145:17:145:32 | Convert: (unsigned char)... | positive | +| test.c:146:12:146:33 | Convert: (int)... | positive | +| test.c:146:12:146:33 | Store: (int)... | positive | +| test.c:146:17:146:33 | Convert: (unsigned short)... | positive | +| test.c:147:17:147:31 | Convert: (unsigned int)... | positive | +| test.c:149:23:149:23 | Convert: (unsigned short)... | positive | +| test.c:149:23:149:23 | Store: (unsigned short)... | positive | +| test.c:150:15:150:16 | Load: x1 | positive | +| test.c:150:20:150:21 | Load: x2 | positive | +| test.c:150:35:150:36 | Convert: (int)... | positive | +| test.c:150:35:150:36 | Load: s0 | positive | +| test.c:154:10:154:40 | Store: ... ? ... : ... | negative strictlyNegative | +| test.c:154:10:154:40 | Store: ... ? ... : ... | positive strictlyPositive | +| test.c:154:20:154:20 | Load: x | positive strictlyPositive | +| test.c:154:25:154:30 | Convert: (int)... | positive | +| test.c:154:25:154:30 | Convert: (long long)... | positive | +| test.c:154:30:154:30 | Load: x | positive strictlyPositive | +| test.c:154:35:154:35 | Load: x | positive strictlyPositive | +| test.c:154:39:154:40 | Constant: (long long)... | negative strictlyNegative | +| test.c:161:7:161:7 | Constant: 3 | positive strictlyPositive | +| test.c:161:17:161:17 | Load: a | positive strictlyPositive | +| test.c:161:22:161:23 | Constant: 11 | positive strictlyPositive | +| test.c:162:13:162:14 | CopyValue: + ... | positive strictlyPositive | +| test.c:162:13:162:14 | Store: + ... | positive strictlyPositive | +| test.c:162:14:162:14 | Load: a | positive strictlyPositive | +| test.c:163:13:163:14 | Negate: - ... | negative strictlyNegative | +| test.c:163:13:163:14 | Store: - ... | negative strictlyNegative | +| test.c:163:14:163:14 | Load: a | positive strictlyPositive | +| test.c:164:14:164:14 | Load: b | positive strictlyPositive | +| test.c:164:16:164:16 | Load: c | negative strictlyNegative | +| test.c:166:17:166:17 | Load: a | positive | +| test.c:166:22:166:23 | Constant: 11 | positive strictlyPositive | +| test.c:167:13:167:14 | CopyValue: + ... | positive | +| test.c:167:13:167:14 | Store: + ... | positive | +| test.c:167:14:167:14 | Load: a | positive | +| test.c:168:13:168:14 | Negate: - ... | negative | +| test.c:168:13:168:14 | Store: - ... | negative | +| test.c:168:14:168:14 | Load: a | positive | +| test.c:169:14:169:14 | Load: b | positive | +| test.c:169:16:169:16 | Load: c | negative | +| test.c:171:7:171:8 | Constant: - ... | negative strictlyNegative | +| test.c:171:23:171:24 | Constant: 11 | positive strictlyPositive | +| test.c:176:7:176:8 | Constant: - ... | negative strictlyNegative | +| test.c:176:23:176:23 | Constant: 1 | positive strictlyPositive | +| test.c:181:7:181:8 | Constant: - ... | negative strictlyNegative | +| test.c:182:13:182:14 | CopyValue: + ... | negative | +| test.c:182:13:182:14 | Store: + ... | negative | +| test.c:182:14:182:14 | Load: a | negative | +| test.c:183:13:183:14 | Negate: - ... | positive | +| test.c:183:13:183:14 | Store: - ... | positive | +| test.c:183:14:183:14 | Load: a | negative | +| test.c:184:14:184:14 | Load: b | negative | +| test.c:184:16:184:16 | Load: c | positive | +| test.c:186:7:186:8 | Constant: - ... | negative strictlyNegative | +| test.c:186:23:186:24 | Constant: - ... | negative strictlyNegative | +| test.c:187:13:187:14 | CopyValue: + ... | negative strictlyNegative | +| test.c:187:13:187:14 | Store: + ... | negative strictlyNegative | +| test.c:187:14:187:14 | Load: a | negative strictlyNegative | +| test.c:188:13:188:14 | Negate: - ... | positive strictlyPositive | +| test.c:188:13:188:14 | Store: - ... | positive strictlyPositive | +| test.c:188:14:188:14 | Load: a | negative strictlyNegative | +| test.c:189:14:189:14 | Load: b | negative strictlyNegative | +| test.c:189:16:189:16 | Load: c | positive strictlyPositive | +| test.c:200:7:200:7 | Constant: 3 | positive strictlyPositive | +| test.c:200:17:200:17 | Load: a | positive strictlyPositive | +| test.c:200:22:200:23 | Constant: 11 | positive strictlyPositive | +| test.c:200:28:200:28 | Constant: 5 | positive strictlyPositive | +| test.c:200:38:200:38 | Load: b | positive strictlyPositive | +| test.c:200:43:200:44 | Constant: 23 | positive strictlyPositive | +| test.c:201:13:201:13 | Load: a | positive strictlyPositive | +| test.c:201:13:201:15 | Mul: ... * ... | positive strictlyPositive | +| test.c:201:13:201:15 | Store: ... * ... | positive strictlyPositive | +| test.c:201:15:201:15 | Load: b | positive strictlyPositive | +| test.c:202:5:202:14 | Add: ... += ... | positive strictlyPositive | +| test.c:202:5:202:14 | Store: ... += ... | positive strictlyPositive | +| test.c:202:14:202:14 | Load: r | positive strictlyPositive | +| test.c:204:7:204:7 | Constant: 3 | positive strictlyPositive | +| test.c:204:7:204:7 | Phi: 3 | positive | +| test.c:204:17:204:17 | Load: a | positive strictlyPositive | +| test.c:204:22:204:23 | Constant: 11 | positive strictlyPositive | +| test.c:204:38:204:38 | Load: b | positive | +| test.c:204:43:204:44 | Constant: 23 | positive strictlyPositive | +| test.c:205:13:205:13 | Load: a | positive strictlyPositive | +| test.c:205:13:205:15 | Mul: ... * ... | positive | +| test.c:205:13:205:15 | Store: ... * ... | positive | +| test.c:205:15:205:15 | Load: b | positive | +| test.c:206:5:206:14 | Add: ... += ... | positive | +| test.c:206:5:206:14 | Load: ... += ... | positive | +| test.c:206:5:206:14 | Store: ... += ... | positive | +| test.c:206:14:206:14 | Load: r | positive | +| test.c:208:7:208:7 | Constant: 3 | positive strictlyPositive | +| test.c:208:7:208:7 | Phi: 3 | positive | +| test.c:208:17:208:17 | Load: a | positive strictlyPositive | +| test.c:208:22:208:23 | Constant: 11 | positive strictlyPositive | +| test.c:208:28:208:30 | Constant: - ... | negative strictlyNegative | +| test.c:208:45:208:46 | Constant: 23 | positive strictlyPositive | +| test.c:209:13:209:13 | Load: a | positive strictlyPositive | +| test.c:210:5:210:14 | Load: ... += ... | positive | +| test.c:212:7:212:7 | Constant: 3 | positive strictlyPositive | +| test.c:212:17:212:17 | Load: a | positive strictlyPositive | +| test.c:212:22:212:23 | Constant: 11 | positive strictlyPositive | +| test.c:212:28:212:30 | Constant: - ... | negative strictlyNegative | +| test.c:213:13:213:13 | Load: a | positive strictlyPositive | +| test.c:213:13:213:15 | Mul: ... * ... | negative | +| test.c:213:13:213:15 | Store: ... * ... | negative | +| test.c:213:15:213:15 | Load: b | negative | +| test.c:214:14:214:14 | Load: r | negative | +| test.c:216:7:216:7 | Constant: 3 | positive strictlyPositive | +| test.c:216:17:216:17 | Load: a | positive strictlyPositive | +| test.c:216:22:216:23 | Constant: 11 | positive strictlyPositive | +| test.c:216:28:216:30 | Constant: - ... | negative strictlyNegative | +| test.c:216:45:216:46 | Constant: - ... | negative strictlyNegative | +| test.c:217:13:217:13 | Load: a | positive strictlyPositive | +| test.c:217:13:217:15 | Mul: ... * ... | negative strictlyNegative | +| test.c:217:13:217:15 | Store: ... * ... | negative strictlyNegative | +| test.c:217:15:217:15 | Load: b | negative strictlyNegative | +| test.c:218:14:218:14 | Load: r | negative strictlyNegative | +| test.c:228:17:228:17 | Load: a | positive | +| test.c:228:22:228:23 | Constant: 11 | positive strictlyPositive | +| test.c:228:28:228:28 | Constant: 5 | positive strictlyPositive | +| test.c:228:38:228:38 | Load: b | positive strictlyPositive | +| test.c:228:43:228:44 | Constant: 23 | positive strictlyPositive | +| test.c:229:13:229:13 | Load: a | positive | +| test.c:229:13:229:15 | Mul: ... * ... | positive | +| test.c:229:13:229:15 | Store: ... * ... | positive | +| test.c:229:15:229:15 | Load: b | positive strictlyPositive | +| test.c:230:5:230:14 | Add: ... += ... | positive | +| test.c:230:5:230:14 | Store: ... += ... | positive | +| test.c:230:14:230:14 | Load: r | positive | +| test.c:232:7:232:7 | Phi: 0 | positive | +| test.c:232:17:232:17 | Load: a | positive | +| test.c:232:22:232:23 | Constant: 11 | positive strictlyPositive | +| test.c:232:38:232:38 | Load: b | positive | +| test.c:232:43:232:44 | Constant: 23 | positive strictlyPositive | +| test.c:233:13:233:13 | Load: a | positive | +| test.c:233:13:233:15 | Mul: ... * ... | positive | +| test.c:233:13:233:15 | Store: ... * ... | positive | +| test.c:233:15:233:15 | Load: b | positive | +| test.c:234:5:234:14 | Add: ... += ... | positive | +| test.c:234:5:234:14 | Load: ... += ... | positive | +| test.c:234:5:234:14 | Store: ... += ... | positive | +| test.c:234:14:234:14 | Load: r | positive | +| test.c:236:7:236:7 | Phi: 0 | positive | +| test.c:236:17:236:17 | Load: a | positive | +| test.c:236:22:236:23 | Constant: 11 | positive strictlyPositive | +| test.c:236:28:236:30 | Constant: - ... | negative strictlyNegative | +| test.c:236:45:236:46 | Constant: 23 | positive strictlyPositive | +| test.c:237:13:237:13 | Load: a | positive | +| test.c:238:5:238:14 | Load: ... += ... | positive | +| test.c:240:17:240:17 | Load: a | positive | +| test.c:240:22:240:23 | Constant: 11 | positive strictlyPositive | +| test.c:240:28:240:30 | Constant: - ... | negative strictlyNegative | +| test.c:241:13:241:13 | Load: a | positive | +| test.c:241:13:241:15 | Mul: ... * ... | negative | +| test.c:241:13:241:15 | Store: ... * ... | negative | +| test.c:241:15:241:15 | Load: b | negative | +| test.c:242:14:242:14 | Load: r | negative | +| test.c:244:17:244:17 | Load: a | positive | +| test.c:244:22:244:23 | Constant: 11 | positive strictlyPositive | +| test.c:244:28:244:30 | Constant: - ... | negative strictlyNegative | +| test.c:244:45:244:46 | Constant: - ... | negative strictlyNegative | +| test.c:245:13:245:13 | Load: a | positive | +| test.c:245:13:245:15 | Mul: ... * ... | negative | +| test.c:245:13:245:15 | Store: ... * ... | negative | +| test.c:245:15:245:15 | Load: b | negative strictlyNegative | +| test.c:246:14:246:14 | Load: r | negative | +| test.c:256:7:256:9 | Constant: - ... | negative strictlyNegative | +| test.c:256:24:256:25 | Constant: 11 | positive strictlyPositive | +| test.c:256:30:256:30 | Constant: 5 | positive strictlyPositive | +| test.c:256:40:256:40 | Load: b | positive strictlyPositive | +| test.c:256:45:256:46 | Constant: 23 | positive strictlyPositive | +| test.c:257:15:257:15 | Load: b | positive strictlyPositive | +| test.c:260:7:260:9 | Constant: - ... | negative strictlyNegative | +| test.c:260:24:260:25 | Constant: 11 | positive strictlyPositive | +| test.c:260:40:260:40 | Load: b | positive | +| test.c:260:45:260:46 | Constant: 23 | positive strictlyPositive | +| test.c:261:15:261:15 | Load: b | positive | +| test.c:264:7:264:9 | Constant: - ... | negative strictlyNegative | +| test.c:264:24:264:25 | Constant: 11 | positive strictlyPositive | +| test.c:264:30:264:32 | Constant: - ... | negative strictlyNegative | +| test.c:264:47:264:48 | Constant: 23 | positive strictlyPositive | +| test.c:268:7:268:9 | Constant: - ... | negative strictlyNegative | +| test.c:268:24:268:25 | Constant: 11 | positive strictlyPositive | +| test.c:268:30:268:32 | Constant: - ... | negative strictlyNegative | +| test.c:269:15:269:15 | Load: b | negative | +| test.c:272:7:272:9 | Constant: - ... | negative strictlyNegative | +| test.c:272:24:272:25 | Constant: 11 | positive strictlyPositive | +| test.c:272:30:272:32 | Constant: - ... | negative strictlyNegative | +| test.c:272:47:272:48 | Constant: - ... | negative strictlyNegative | +| test.c:273:15:273:15 | Load: b | negative strictlyNegative | +| test.c:284:7:284:9 | Constant: - ... | negative strictlyNegative | +| test.c:284:29:284:29 | Constant: 5 | positive strictlyPositive | +| test.c:284:39:284:39 | Load: b | positive strictlyPositive | +| test.c:284:44:284:45 | Constant: 23 | positive strictlyPositive | +| test.c:285:13:285:13 | Load: a | negative | +| test.c:285:13:285:15 | Mul: ... * ... | negative | +| test.c:285:13:285:15 | Store: ... * ... | negative | +| test.c:285:15:285:15 | Load: b | positive strictlyPositive | +| test.c:286:5:286:14 | Add: ... += ... | negative | +| test.c:286:5:286:14 | Store: ... += ... | negative | +| test.c:286:14:286:14 | Load: r | negative | +| test.c:288:7:288:9 | Constant: - ... | negative strictlyNegative | +| test.c:288:7:288:9 | Phi: - ... | negative | +| test.c:288:39:288:39 | Load: b | positive | +| test.c:288:44:288:45 | Constant: 23 | positive strictlyPositive | +| test.c:289:13:289:13 | Load: a | negative | +| test.c:289:13:289:15 | Mul: ... * ... | negative | +| test.c:289:13:289:15 | Store: ... * ... | negative | +| test.c:289:15:289:15 | Load: b | positive | +| test.c:290:5:290:14 | Add: ... += ... | negative | +| test.c:290:5:290:14 | Load: ... += ... | negative | +| test.c:290:5:290:14 | Store: ... += ... | negative | +| test.c:290:14:290:14 | Load: r | negative | +| test.c:292:7:292:9 | Constant: - ... | negative strictlyNegative | +| test.c:292:7:292:9 | Phi: - ... | negative | +| test.c:292:29:292:31 | Constant: - ... | negative strictlyNegative | +| test.c:292:46:292:47 | Constant: 23 | positive strictlyPositive | +| test.c:293:13:293:13 | Load: a | negative | +| test.c:294:5:294:14 | Load: ... += ... | negative | +| test.c:296:7:296:9 | Constant: - ... | negative strictlyNegative | +| test.c:296:29:296:31 | Constant: - ... | negative strictlyNegative | +| test.c:297:13:297:13 | Load: a | negative | +| test.c:297:13:297:15 | Mul: ... * ... | positive | +| test.c:297:13:297:15 | Store: ... * ... | positive | +| test.c:297:15:297:15 | Load: b | negative | +| test.c:298:14:298:14 | Load: r | positive | +| test.c:300:7:300:9 | Constant: - ... | negative strictlyNegative | +| test.c:300:29:300:31 | Constant: - ... | negative strictlyNegative | +| test.c:300:46:300:47 | Constant: - ... | negative strictlyNegative | +| test.c:301:13:301:13 | Load: a | negative | +| test.c:301:13:301:15 | Mul: ... * ... | positive | +| test.c:301:13:301:15 | Store: ... * ... | positive | +| test.c:301:15:301:15 | Load: b | negative strictlyNegative | +| test.c:302:14:302:14 | Load: r | positive | +| test.c:312:7:312:9 | Constant: - ... | negative strictlyNegative | +| test.c:312:24:312:25 | Constant: - ... | negative strictlyNegative | +| test.c:312:30:312:30 | Constant: 5 | positive strictlyPositive | +| test.c:312:40:312:40 | Load: b | positive strictlyPositive | +| test.c:312:45:312:46 | Constant: 23 | positive strictlyPositive | +| test.c:313:13:313:13 | Load: a | negative strictlyNegative | +| test.c:313:13:313:15 | Mul: ... * ... | negative strictlyNegative | +| test.c:313:13:313:15 | Store: ... * ... | negative strictlyNegative | +| test.c:313:15:313:15 | Load: b | positive strictlyPositive | +| test.c:314:5:314:14 | Add: ... += ... | negative strictlyNegative | +| test.c:314:5:314:14 | Store: ... += ... | negative strictlyNegative | +| test.c:314:14:314:14 | Load: r | negative strictlyNegative | +| test.c:316:7:316:9 | Constant: - ... | negative strictlyNegative | +| test.c:316:7:316:9 | Phi: - ... | negative | +| test.c:316:24:316:25 | Constant: - ... | negative strictlyNegative | +| test.c:316:40:316:40 | Load: b | positive | +| test.c:316:45:316:46 | Constant: 23 | positive strictlyPositive | +| test.c:317:13:317:13 | Load: a | negative strictlyNegative | +| test.c:317:13:317:15 | Mul: ... * ... | negative | +| test.c:317:13:317:15 | Store: ... * ... | negative | +| test.c:317:15:317:15 | Load: b | positive | +| test.c:318:5:318:14 | Add: ... += ... | negative | +| test.c:318:5:318:14 | Load: ... += ... | negative | +| test.c:318:5:318:14 | Store: ... += ... | negative | +| test.c:318:14:318:14 | Load: r | negative | +| test.c:320:7:320:9 | Constant: - ... | negative strictlyNegative | +| test.c:320:7:320:9 | Phi: - ... | negative | +| test.c:320:24:320:25 | Constant: - ... | negative strictlyNegative | +| test.c:320:30:320:32 | Constant: - ... | negative strictlyNegative | +| test.c:320:47:320:48 | Constant: 23 | positive strictlyPositive | +| test.c:321:13:321:13 | Load: a | negative strictlyNegative | +| test.c:322:5:322:14 | Load: ... += ... | negative | +| test.c:324:7:324:9 | Constant: - ... | negative strictlyNegative | +| test.c:324:24:324:25 | Constant: - ... | negative strictlyNegative | +| test.c:324:30:324:32 | Constant: - ... | negative strictlyNegative | +| test.c:325:13:325:13 | Load: a | negative strictlyNegative | +| test.c:325:13:325:15 | Mul: ... * ... | positive | +| test.c:325:13:325:15 | Store: ... * ... | positive | +| test.c:325:15:325:15 | Load: b | negative | +| test.c:326:14:326:14 | Load: r | positive | +| test.c:328:7:328:9 | Constant: - ... | negative strictlyNegative | +| test.c:328:24:328:25 | Constant: - ... | negative strictlyNegative | +| test.c:328:30:328:32 | Constant: - ... | negative strictlyNegative | +| test.c:328:47:328:48 | Constant: - ... | negative strictlyNegative | +| test.c:329:13:329:13 | Load: a | negative strictlyNegative | +| test.c:329:13:329:15 | Mul: ... * ... | positive strictlyPositive | +| test.c:329:13:329:15 | Store: ... * ... | positive strictlyPositive | +| test.c:329:15:329:15 | Load: b | negative strictlyNegative | +| test.c:330:14:330:14 | Load: r | positive strictlyPositive | +| test.c:339:12:339:13 | Constant: - ... | negative strictlyNegative | +| test.c:339:12:339:13 | Store: - ... | negative strictlyNegative | +| test.c:342:10:342:10 | Load: i | positive | +| test.c:342:10:342:10 | Phi: i | positive | +| test.c:342:14:342:14 | Constant: 3 | positive strictlyPositive | +| test.c:343:5:343:7 | Add: ... ++ | positive strictlyPositive | +| test.c:343:5:343:7 | Constant: ... ++ | positive strictlyPositive | +| test.c:343:5:343:7 | Load: ... ++ | positive | +| test.c:343:5:343:7 | Store: ... ++ | positive strictlyPositive | +| test.c:345:3:345:7 | Store: ... = ... | positive | +| test.c:345:7:345:7 | Load: i | positive | +| test.c:346:7:346:7 | Load: x | positive | +| test.c:347:9:347:9 | Load: d | positive | +| test.c:348:14:348:14 | Constant: 1 | positive strictlyPositive | +| test.c:348:14:348:14 | Store: 1 | positive strictlyPositive | +| test.c:355:42:355:42 | InitializeParameter: x | positive | +| test.c:356:16:356:17 | Uninitialized: definition of y1 | positive | +| test.c:356:20:356:21 | Uninitialized: definition of y2 | positive | +| test.c:356:24:356:25 | Uninitialized: definition of y3 | positive | +| test.c:356:28:356:29 | Uninitialized: definition of y4 | positive | +| test.c:356:32:356:33 | Uninitialized: definition of y5 | positive | +| test.c:356:36:356:37 | Uninitialized: definition of y6 | positive | +| test.c:356:40:356:41 | Uninitialized: definition of y7 | positive | +| test.c:356:44:356:45 | Uninitialized: definition of y8 | positive | +| test.c:357:3:357:23 | Store: ... = ... | positive | +| test.c:357:8:357:8 | Load: x | positive | +| test.c:357:8:357:23 | Load: ... ? ... : ... | positive | +| test.c:357:8:357:23 | Phi: ... ? ... : ... | positive | +| test.c:357:8:357:23 | Store: ... ? ... : ... | positive | +| test.c:357:8:357:23 | Store: ... ? ... : ... | positive strictlyPositive | +| test.c:357:12:357:14 | Constant: (unsigned int)... | positive strictlyPositive | +| test.c:357:18:357:18 | Load: x | positive | +| test.c:357:22:357:23 | Constant: (unsigned int)... | positive strictlyPositive | +| test.c:358:3:358:24 | Store: ... = ... | positive | +| test.c:358:8:358:8 | Load: x | positive | +| test.c:358:8:358:24 | Load: ... ? ... : ... | positive | +| test.c:358:8:358:24 | Phi: ... ? ... : ... | positive | +| test.c:358:8:358:24 | Store: ... ? ... : ... | positive | +| test.c:358:8:358:24 | Store: ... ? ... : ... | positive strictlyPositive | +| test.c:358:13:358:15 | Constant: (unsigned int)... | positive strictlyPositive | +| test.c:358:19:358:20 | Constant: (unsigned int)... | positive strictlyPositive | +| test.c:358:24:358:24 | Load: x | positive | +| test.c:365:7:365:7 | Load: x | positive | +| test.c:365:11:365:13 | Constant: (unsigned int)... | positive strictlyPositive | +| test.c:366:5:366:15 | Store: ... = ... | positive | +| test.c:366:10:366:10 | Load: x | positive | +| test.c:366:10:366:15 | Load: ... ? ... : ... | positive | +| test.c:366:10:366:15 | Phi: ... ? ... : ... | positive | +| test.c:366:10:366:15 | Store: ... ? ... : ... | positive | +| test.c:366:10:366:15 | Store: ... ? ... : ... | positive strictlyPositive | +| test.c:366:15:366:15 | Constant: (unsigned int)... | positive strictlyPositive | +| test.c:367:5:367:17 | Store: ... = ... | positive | +| test.c:367:10:367:10 | Load: x | positive | +| test.c:367:10:367:17 | Load: ... ? ... : ... | positive | +| test.c:367:10:367:17 | Phi: ... ? ... : ... | positive | +| test.c:367:10:367:17 | Store: ... ? ... : ... | positive | +| test.c:367:10:367:17 | Store: ... ? ... : ... | positive strictlyPositive | +| test.c:367:15:367:17 | Constant: (unsigned int)... | positive strictlyPositive | +| test.c:368:5:368:21 | Store: ... = ... | positive strictlyPositive | +| test.c:368:10:368:21 | Load: ... ? ... : ... | positive strictlyPositive | +| test.c:368:10:368:21 | Phi: ... ? ... : ... | positive strictlyPositive | +| test.c:368:10:368:21 | Store: ... ? ... : ... | positive strictlyPositive | +| test.c:368:11:368:11 | Load: x | positive | +| test.c:368:11:368:13 | Add: ... + ... | positive strictlyPositive | +| test.c:368:13:368:13 | Constant: (unsigned int)... | positive strictlyPositive | +| test.c:368:19:368:21 | Constant: (unsigned int)... | positive strictlyPositive | +| test.c:369:5:369:36 | Store: ... = ... | positive strictlyPositive | +| test.c:369:10:369:36 | Convert: (unsigned int)... | positive strictlyPositive | +| test.c:369:10:369:36 | Load: ... ? ... : ... | positive strictlyPositive | +| test.c:369:10:369:36 | Phi: ... ? ... : ... | positive strictlyPositive | +| test.c:369:10:369:36 | Store: ... ? ... : ... | positive strictlyPositive | +| test.c:369:11:369:30 | Convert: (unsigned char)... | positive | +| test.c:369:27:369:27 | Load: x | positive | +| test.c:369:27:369:29 | Add: ... + ... | positive strictlyPositive | +| test.c:369:29:369:29 | Constant: (unsigned int)... | positive strictlyPositive | +| test.c:369:36:369:36 | Constant: 5 | positive strictlyPositive | +| test.c:370:5:370:38 | Store: ... = ... | positive strictlyPositive | +| test.c:370:10:370:38 | Convert: (unsigned int)... | positive strictlyPositive | +| test.c:370:10:370:38 | Load: ... ? ... : ... | positive strictlyPositive | +| test.c:370:10:370:38 | Phi: ... ? ... : ... | positive strictlyPositive | +| test.c:370:10:370:38 | Store: ... ? ... : ... | positive strictlyPositive | +| test.c:370:11:370:30 | Convert: (unsigned char)... | positive | +| test.c:370:27:370:27 | Load: x | positive | +| test.c:370:27:370:29 | Add: ... + ... | positive strictlyPositive | +| test.c:370:29:370:29 | Constant: (unsigned int)... | positive strictlyPositive | +| test.c:370:36:370:38 | Constant: 500 | positive strictlyPositive | +| test.c:371:5:371:39 | Store: ... = ... | positive strictlyPositive | +| test.c:371:10:371:39 | Convert: (unsigned int)... | positive strictlyPositive | +| test.c:371:10:371:39 | Load: ... ? ... : ... | positive strictlyPositive | +| test.c:371:10:371:39 | Phi: ... ? ... : ... | positive strictlyPositive | +| test.c:371:10:371:39 | Store: ... ? ... : ... | positive strictlyPositive | +| test.c:371:11:371:31 | Convert: (unsigned short)... | positive | +| test.c:371:28:371:28 | Load: x | positive | +| test.c:371:28:371:30 | Add: ... + ... | positive strictlyPositive | +| test.c:371:30:371:30 | Constant: (unsigned int)... | positive strictlyPositive | +| test.c:371:37:371:39 | Constant: 500 | positive strictlyPositive | +| test.c:373:3:373:47 | Phi: return ... | positive | +| test.c:373:3:373:47 | Phi: return ... | positive | +| test.c:373:3:373:47 | Phi: return ... | positive | +| test.c:373:3:373:47 | Phi: return ... | positive | +| test.c:373:3:373:47 | Phi: return ... | positive | +| test.c:373:3:373:47 | Phi: return ... | positive | +| test.c:373:10:373:11 | Load: y1 | positive | +| test.c:373:10:373:16 | Add: ... + ... | positive | +| test.c:373:10:373:21 | Add: ... + ... | positive | +| test.c:373:10:373:26 | Add: ... + ... | positive | +| test.c:373:10:373:31 | Add: ... + ... | positive | +| test.c:373:10:373:36 | Add: ... + ... | positive | +| test.c:373:10:373:41 | Add: ... + ... | positive | +| test.c:373:10:373:46 | Add: ... + ... | positive | +| test.c:373:10:373:46 | Store: ... + ... | positive | +| test.c:373:15:373:16 | Load: y2 | positive | +| test.c:373:20:373:21 | Load: y3 | positive | +| test.c:373:25:373:26 | Load: y4 | positive | +| test.c:373:30:373:31 | Load: y5 | positive | +| test.c:373:35:373:36 | Load: y6 | positive | +| test.c:373:40:373:41 | Load: y7 | positive | +| test.c:373:45:373:46 | Load: y8 | positive | +| test.c:377:42:377:42 | InitializeParameter: x | positive | +| test.c:378:16:378:17 | Uninitialized: definition of y1 | positive | +| test.c:378:20:378:21 | Uninitialized: definition of y2 | positive | +| test.c:378:24:378:25 | Uninitialized: definition of y3 | positive | +| test.c:378:28:378:29 | Uninitialized: definition of y4 | positive | +| test.c:378:32:378:33 | Uninitialized: definition of y5 | positive | +| test.c:379:3:379:24 | Store: ... = ... | positive strictlyPositive | +| test.c:379:8:379:8 | Load: x | positive | +| test.c:379:8:379:24 | Load: ... ? ... : ... | positive strictlyPositive | +| test.c:379:8:379:24 | Phi: ... ? ... : ... | positive strictlyPositive | +| test.c:379:8:379:24 | Store: ... ? ... : ... | positive strictlyPositive | +| test.c:379:8:379:24 | Store: ... ? ... : ... | positive strictlyPositive | +| test.c:379:12:379:14 | Constant: (unsigned int)... | positive strictlyPositive | +| test.c:379:18:379:18 | Load: x | positive strictlyPositive | +| test.c:379:22:379:24 | Constant: (unsigned int)... | positive strictlyPositive | +| test.c:380:3:380:25 | Store: ... = ... | positive strictlyPositive | +| test.c:380:8:380:8 | Load: x | positive | +| test.c:380:8:380:25 | Load: ... ? ... : ... | positive strictlyPositive | +| test.c:380:8:380:25 | Phi: ... ? ... : ... | positive strictlyPositive | +| test.c:380:8:380:25 | Store: ... ? ... : ... | positive strictlyPositive | +| test.c:380:8:380:25 | Store: ... ? ... : ... | positive strictlyPositive | +| test.c:380:13:380:15 | Constant: (unsigned int)... | positive strictlyPositive | +| test.c:380:19:380:21 | Constant: (unsigned int)... | positive strictlyPositive | +| test.c:380:25:380:25 | Load: x | positive strictlyPositive | +| test.c:381:3:381:11 | Store: ... = ... | positive strictlyPositive | +| test.c:381:8:381:11 | Constant: (unsigned int)... | positive strictlyPositive | +| test.c:382:3:382:11 | Store: ... = ... | positive strictlyPositive | +| test.c:382:8:382:11 | Constant: (unsigned int)... | positive strictlyPositive | +| test.c:383:3:383:11 | Store: ... = ... | positive strictlyPositive | +| test.c:383:8:383:11 | Constant: (unsigned int)... | positive strictlyPositive | +| test.c:384:7:384:7 | Load: x | positive | +| test.c:384:12:384:14 | Constant: (unsigned int)... | positive strictlyPositive | +| test.c:385:5:385:21 | Store: ... = ... | positive strictlyPositive | +| test.c:385:10:385:21 | Load: ... ? ... : ... | positive strictlyPositive | +| test.c:385:10:385:21 | Phi: ... ? ... : ... | positive strictlyPositive | +| test.c:385:10:385:21 | Store: ... ? ... : ... | positive strictlyPositive | +| test.c:385:11:385:11 | Load: x | positive strictlyPositive | +| test.c:385:11:385:15 | Sub: ... - ... | positive | +| test.c:385:13:385:15 | Constant: (unsigned int)... | positive strictlyPositive | +| test.c:385:21:385:21 | Constant: (unsigned int)... | positive strictlyPositive | +| test.c:386:5:386:21 | Store: ... = ... | positive strictlyPositive | +| test.c:386:10:386:21 | Load: ... ? ... : ... | positive strictlyPositive | +| test.c:386:10:386:21 | Phi: ... ? ... : ... | positive strictlyPositive | +| test.c:386:10:386:21 | Store: ... ? ... : ... | positive strictlyPositive | +| test.c:386:11:386:11 | Load: x | positive strictlyPositive | +| test.c:386:11:386:15 | Sub: ... - ... | positive | +| test.c:386:13:386:15 | Constant: (unsigned int)... | positive strictlyPositive | +| test.c:386:21:386:21 | Constant: (unsigned int)... | positive strictlyPositive | +| test.c:387:5:387:38 | Store: ... = ... | positive strictlyPositive | +| test.c:387:10:387:38 | Convert: (unsigned int)... | positive strictlyPositive | +| test.c:387:10:387:38 | Load: ... ? ... : ... | positive strictlyPositive | +| test.c:387:10:387:38 | Phi: ... ? ... : ... | positive strictlyPositive | +| test.c:387:10:387:38 | Store: ... ? ... : ... | positive strictlyPositive | +| test.c:387:11:387:32 | Convert: (unsigned char)... | positive | +| test.c:387:27:387:27 | Load: x | positive strictlyPositive | +| test.c:387:27:387:31 | Sub: ... - ... | positive | +| test.c:387:29:387:31 | Constant: (unsigned int)... | positive strictlyPositive | +| test.c:387:38:387:38 | Constant: 5 | positive strictlyPositive | +| test.c:389:3:389:32 | Phi: return ... | positive strictlyPositive | +| test.c:389:3:389:32 | Phi: return ... | positive strictlyPositive | +| test.c:389:3:389:32 | Phi: return ... | positive strictlyPositive | +| test.c:389:10:389:11 | Load: y1 | positive strictlyPositive | +| test.c:389:10:389:16 | Add: ... + ... | positive strictlyPositive | +| test.c:389:10:389:21 | Add: ... + ... | positive strictlyPositive | +| test.c:389:10:389:26 | Add: ... + ... | positive strictlyPositive | +| test.c:389:10:389:31 | Add: ... + ... | positive strictlyPositive | +| test.c:389:10:389:31 | Store: ... + ... | positive strictlyPositive | +| test.c:389:15:389:16 | Load: y2 | positive strictlyPositive | +| test.c:389:20:389:21 | Load: y3 | positive strictlyPositive | +| test.c:389:25:389:26 | Load: y4 | positive strictlyPositive | +| test.c:389:30:389:31 | Load: y5 | positive strictlyPositive | +| test.c:393:40:393:40 | InitializeParameter: x | positive | +| test.c:394:20:394:20 | Load: x | positive | +| test.c:394:20:394:36 | Load: ... ? ... : ... | positive | +| test.c:394:20:394:36 | Phi: ... ? ... : ... | positive | +| test.c:394:20:394:36 | Store: ... ? ... : ... | positive | +| test.c:394:20:394:36 | Store: ... ? ... : ... | positive | +| test.c:394:20:394:36 | Store: ... ? ... : ... | positive strictlyPositive | +| test.c:394:24:394:26 | Constant: (unsigned int)... | positive strictlyPositive | +| test.c:394:30:394:30 | Load: x | positive | +| test.c:394:34:394:36 | Constant: (unsigned int)... | positive strictlyPositive | +| test.c:395:16:395:17 | Uninitialized: definition of y1 | positive | +| test.c:396:16:396:17 | Uninitialized: definition of y2 | positive | +| test.c:397:3:397:15 | Store: ... = ... | positive strictlyPositive | +| test.c:397:9:397:11 | Add: ++ ... | positive strictlyPositive | +| test.c:397:9:397:11 | Constant: ++ ... | positive strictlyPositive | +| test.c:397:9:397:11 | Load: ++ ... | positive | +| test.c:397:9:397:11 | Store: ++ ... | positive strictlyPositive | +| test.c:397:14:397:14 | Load: y | positive strictlyPositive | +| test.c:398:3:398:23 | Store: ... = ... | positive strictlyPositive | +| test.c:398:9:398:11 | Add: ... ++ | positive strictlyPositive | +| test.c:398:9:398:11 | Constant: ... ++ | positive strictlyPositive | +| test.c:398:9:398:11 | Load: ... ++ | positive strictlyPositive | +| test.c:398:9:398:11 | Store: ... ++ | positive strictlyPositive | +| test.c:398:14:398:19 | Add: ... += ... | positive strictlyPositive | +| test.c:398:14:398:19 | Load: ... += ... | positive strictlyPositive | +| test.c:398:14:398:19 | Store: ... += ... | positive strictlyPositive | +| test.c:398:19:398:19 | Constant: (unsigned int)... | positive strictlyPositive | +| test.c:398:22:398:22 | Load: y | positive strictlyPositive | +| test.c:399:10:399:11 | Load: y1 | positive strictlyPositive | +| test.c:399:10:399:16 | Add: ... + ... | positive strictlyPositive | +| test.c:399:10:399:16 | Store: ... + ... | positive strictlyPositive | +| test.c:399:15:399:16 | Load: y2 | positive strictlyPositive | +| test.cpp:9:11:9:12 | Constant: - ... | negative strictlyNegative | +| test.cpp:9:11:9:12 | Store: - ... | negative strictlyNegative | +| test.cpp:11:13:11:13 | Constant: 3 | positive strictlyPositive | +| test.cpp:30:12:30:13 | Constant: - ... | negative strictlyNegative | +| test.cpp:31:5:31:10 | Store: ... = ... | negative strictlyNegative | +| test.cpp:31:9:31:10 | Constant: - ... | negative strictlyNegative | +| test.cpp:33:12:33:12 | Constant: 1 | positive strictlyPositive | +| test.cpp:34:5:34:9 | Store: ... = ... | positive strictlyPositive | +| test.cpp:34:9:34:9 | Constant: 1 | positive strictlyPositive | +| test.cpp:36:12:36:15 | Constant: - ... | negative strictlyNegative | +| test.cpp:37:5:37:12 | Store: ... = ... | negative strictlyNegative | +| test.cpp:37:9:37:12 | Constant: - ... | negative strictlyNegative | +| test.cpp:39:12:39:14 | Constant: 128 | positive strictlyPositive | +| test.cpp:40:5:40:11 | Store: ... = ... | positive strictlyPositive | +| test.cpp:40:9:40:11 | Constant: 128 | positive strictlyPositive | +| test.cpp:42:12:42:16 | Constant: - ... | negative strictlyNegative | +| test.cpp:43:5:43:13 | Store: ... = ... | negative strictlyNegative | +| test.cpp:43:9:43:13 | Constant: - ... | negative strictlyNegative | +| test.cpp:45:12:45:15 | Constant: 1024 | positive strictlyPositive | +| test.cpp:46:5:46:12 | Store: ... = ... | positive strictlyPositive | +| test.cpp:46:9:46:12 | Constant: 1024 | positive strictlyPositive | +| test.cpp:69:10:69:21 | Constant: ... \|\| ... | positive strictlyPositive | +| test.cpp:69:10:69:21 | Load: ... \|\| ... | positive | +| test.cpp:69:10:69:21 | Phi: ... \|\| ... | positive | +| test.cpp:69:10:69:21 | Store: ... \|\| ... | positive | +| test.cpp:69:10:69:21 | Store: ... \|\| ... | positive strictlyPositive | diff --git a/cpp/ql/test/library-tests/rangeanalysis/signanalysis/SignAnalysis.ql b/cpp/ql/test/library-tests/rangeanalysis/signanalysis/SignAnalysis.ql new file mode 100644 index 000000000000..9875a641627b --- /dev/null +++ b/cpp/ql/test/library-tests/rangeanalysis/signanalysis/SignAnalysis.ql @@ -0,0 +1,19 @@ +import semmle.code.cpp.rangeanalysis.SignAnalysis +import semmle.code.cpp.ir.IR + +string getASignString(Instruction i) { + positiveInstruction(i) and + result = "positive" + or + negativeInstruction(i) and + result = "negative" + or + strictlyPositiveInstruction(i) and + result = "strictlyPositive" + or + strictlyNegativeInstruction(i) and + result = "strictlyNegative" +} + +from Instruction i +select i, strictconcat(string s | s = getASignString(i) | s, " ") \ No newline at end of file diff --git a/cpp/ql/test/library-tests/rangeanalysis/signanalysis/binary_logical_operator.c b/cpp/ql/test/library-tests/rangeanalysis/signanalysis/binary_logical_operator.c new file mode 100644 index 000000000000..9339241bda18 --- /dev/null +++ b/cpp/ql/test/library-tests/rangeanalysis/signanalysis/binary_logical_operator.c @@ -0,0 +1,8 @@ +int test01(int x, int y) { + int b = x > 10 && y < 0; + if (b) { + return x; + } else { + return y; + } +} diff --git a/cpp/ql/test/library-tests/rangeanalysis/signanalysis/bounded_bounds.c b/cpp/ql/test/library-tests/rangeanalysis/signanalysis/bounded_bounds.c new file mode 100644 index 000000000000..7519fe001907 --- /dev/null +++ b/cpp/ql/test/library-tests/rangeanalysis/signanalysis/bounded_bounds.c @@ -0,0 +1,19 @@ +int f(int x, int y) { + if (x < 0) { + return x; + } + if (x < y) { + return y; // y is strictly positive because of the bound on x above + } + return 0; +} + +int g(int x, int y) { + if (x < y) { + return y; + } + if (x < 0) { + return x; + } + return 0; +} diff --git a/cpp/ql/test/library-tests/rangeanalysis/signanalysis/inline_assembly.c b/cpp/ql/test/library-tests/rangeanalysis/signanalysis/inline_assembly.c new file mode 100644 index 000000000000..430838d77363 --- /dev/null +++ b/cpp/ql/test/library-tests/rangeanalysis/signanalysis/inline_assembly.c @@ -0,0 +1,24 @@ +// The ASM statements are +// causing problems, because our SSA analysis does not notice that they +// might change the value of `x`. This was a latent bug that came out +// of the woodwork when we added support for statement expressions. + +int printf(const char *format, ...); + +int main() { + unsigned int x = 0, y; + y = 1; + + printf("x = %i y = %i\n", x, y); // 0, 1 + + // exchange x and y + asm volatile ( "xchg %0, %1\n" + : "+r" (x), "+a" (y) // outputs (x and y) + : + : + ); + + printf("x = %i y = %i\n", x, y); // 1, 0 (but without analysing the ASM: unknown, unknown) + + return 0; +} diff --git a/cpp/ql/test/library-tests/rangeanalysis/signanalysis/minmax.c b/cpp/ql/test/library-tests/rangeanalysis/signanalysis/minmax.c new file mode 100644 index 000000000000..460167ccb4c6 --- /dev/null +++ b/cpp/ql/test/library-tests/rangeanalysis/signanalysis/minmax.c @@ -0,0 +1,27 @@ +// semmle-extractor-options: --gnu_version 40400 +// Note: this file uses statement expressions, which are a GNU extension, +// so it has an options file to specify the compiler version. The statement +// expression extension is described here: +// https://gcc.gnu.org/onlinedocs/gcc/Statement-Exprs.html + +int printf(const char *format, ...); + +// The & operator is +// causing problems, because it disables SSA. Also, range analysis did not +// have support for the statement expression language feature that is used +// here. + +void minmax() +{ + int x = 1, y = 2, z = 3; + + printf("x = %i, y = %i, z = %i\n", x, y, z); // 1, 2, 3 + + z = ({ + int t = 0; + if (&x != &y) {t = x;} // t = 1 + t; + }); + + printf("x = %i, y = %i, z = %i\n", x, y, z); // 1, 2, 1 +} diff --git a/cpp/ql/test/library-tests/rangeanalysis/signanalysis/test.c b/cpp/ql/test/library-tests/rangeanalysis/signanalysis/test.c new file mode 100644 index 000000000000..fa294a678230 --- /dev/null +++ b/cpp/ql/test/library-tests/rangeanalysis/signanalysis/test.c @@ -0,0 +1,400 @@ +struct List { + struct List* next; +}; + +int test1(struct List* p) { + int count = 0; + for (; p; p = p->next) { + count = count+1; + } + return count; +} + +int test2(struct List* p) { + int count = 0; + for (; p; p = p->next) { + count = (count+1) % 10; + } + return count; +} + +int test3(struct List* p) { + int count = 0; + for (; p; p = p->next) { + count++; + count = count % 10; + } + return count; +} + +int test4() { + int i = 0; + int total = 0; + for (i = 0; i < 2; i = i+1) { + total += i; + } + return total + i; +} + +int test5() { + int i = 0; + int total = 0; + for (i = 0; i < 2; i++) { + total += i; + } + return total + i; +} + +int test6() { + int i = 0; + int total = 0; + for (i = 0; i+2 < 4; i = i+1) { + total += i; + } + return total + i; +} + +int test7(int i) { + if (i < 4) { + if (i < 5) { + return i; + } + } + return 1; +} + +int test8(int x, int y) { + if (-1000 < y && y < 10) { + if (x < y-2) { + return x; + } + } + return y; +} + +int test9(int x, int y) { + if (y == 0) { + if (x < 4) { + return 0; + } + } else { + if (x < 4) { + return 1; + } + } + return x; +} + +int test10(int x, int y) { + if (y > 7) { + if (x < y) { + return 0; + } + return x; + } + return 1; +} + +int test11(char *p) { + char c; + c = *p; + if (c != '\0') + *p++ = '\0'; + + if (c == ':') { + c = *p; + if (c != '\0') + *p++ = '\0'; + + if (c != ',') + return 1; + } + return 0; +} + +typedef unsigned long long size_type; + +size_type test12_helper() { + static size_type n = 0; + return n++; +} + +int test12() { + size_type Start = 0; + while (Start <= test12_helper()-1) + { + const size_type Length = test12_helper(); + Start += Length + 1; + } + + return 1; +} + +// Tests for overflow conditions. +int test13(char c, int i) { + unsigned char uc = c; + unsigned int x = 0; + unsigned int y = x-1; + int z = i+1; + return (double)(c + i + uc + x + y + z); +} + +// Regression test for ODASA-6013. +int test14(int x) { + int x0 = (int)(char)x; + int x1 = (int)(unsigned char)x; + int x2 = (int)(unsigned short)x; + int x3 = (int)(unsigned int)x; + char c0 = x; + unsigned short s0 = x; + return x0 + x1 + x2 + x3 + c0 + s0; +} + +long long test15(long long x) { + return (x > 0 && x == (int)x) ? x : -1; +} + +// Tests for unary operators. +int test_unary(int a) { + int total = 0; + + if (3 <= a && a <= 11) { + int b = +a; + int c = -a; + total += b+c; + } + if (0 <= a && a <= 11) { + int b = +a; + int c = -a; + total += b+c; + } + if (-7 <= a && a <= 11) { + int b = +a; + int c = -a; + total += b+c; + } + if (-7 <= a && a <= 1) { + int b = +a; + int c = -a; + total += b+c; + } + if (-7 <= a && a <= 0) { + int b = +a; + int c = -a; + total += b+c; + } + if (-7 <= a && a <= -2) { + int b = +a; + int c = -a; + total += b+c; + } + + return total; +} + + +// Tests for multiplication. +int test_mult01(int a, int b) { + int total = 0; + + if (3 <= a && a <= 11 && 5 <= b && b <= 23) { + int r = a*b; // 15 .. 253 + total += r; + } + if (3 <= a && a <= 11 && 0 <= b && b <= 23) { + int r = a*b; // 0 .. 253 + total += r; + } + if (3 <= a && a <= 11 && -13 <= b && b <= 23) { + int r = a*b; // -143 .. 253 + total += r; + } + if (3 <= a && a <= 11 && -13 <= b && b <= 0) { + int r = a*b; // -143 .. 0 + total += r; + } + if (3 <= a && a <= 11 && -13 <= b && b <= -7) { + int r = a*b; // -143 .. -21 + total += r; + } + + return total; +} + +// Tests for multiplication. +int test_mult02(int a, int b) { + int total = 0; + + if (0 <= a && a <= 11 && 5 <= b && b <= 23) { + int r = a*b; // 0 .. 253 + total += r; + } + if (0 <= a && a <= 11 && 0 <= b && b <= 23) { + int r = a*b; // 0 .. 253 + total += r; + } + if (0 <= a && a <= 11 && -13 <= b && b <= 23) { + int r = a*b; // -143 .. 253 + total += r; + } + if (0 <= a && a <= 11 && -13 <= b && b <= 0) { + int r = a*b; // -143 .. 0 + total += r; + } + if (0 <= a && a <= 11 && -13 <= b && b <= -7) { + int r = a*b; // -143 .. 0 + total += r; + } + + return total; +} + +// Tests for multiplication. +int test_mult03(int a, int b) { + int total = 0; + + if (-17 <= a && a <= 11 && 5 <= b && b <= 23) { + int r = a*b; // -391 .. 253 + total += r; + } + if (-17 <= a && a <= 11 && 0 <= b && b <= 23) { + int r = a*b; // -391 .. 253 + total += r; + } + if (-17 <= a && a <= 11 && -13 <= b && b <= 23) { + int r = a*b; // -391 .. 253 + total += r; + } + if (-17 <= a && a <= 11 && -13 <= b && b <= 0) { + int r = a*b; // -143 .. 221 + total += r; + } + if (-17 <= a && a <= 11 && -13 <= b && b <= -7) { + int r = a*b; // -143 .. 221 + total += r; + } + + return total; +} + +// Tests for multiplication. +int test_mult04(int a, int b) { + int total = 0; + + if (-17 <= a && a <= 0 && 5 <= b && b <= 23) { + int r = a*b; // -391 .. 0 + total += r; + } + if (-17 <= a && a <= 0 && 0 <= b && b <= 23) { + int r = a*b; // -391 .. 0 + total += r; + } + if (-17 <= a && a <= 0 && -13 <= b && b <= 23) { + int r = a*b; // -391 .. 221 + total += r; + } + if (-17 <= a && a <= 0 && -13 <= b && b <= 0) { + int r = a*b; // 0 .. 221 + total += r; + } + if (-17 <= a && a <= 0 && -13 <= b && b <= -7) { + int r = a*b; // 0 .. 221 + total += r; + } + + return total; +} + +// Tests for multiplication. +int test_mult05(int a, int b) { + int total = 0; + + if (-17 <= a && a <= -2 && 5 <= b && b <= 23) { + int r = a*b; // -391 .. -10 + total += r; + } + if (-17 <= a && a <= -2 && 0 <= b && b <= 23) { + int r = a*b; // -391 .. 0 + total += r; + } + if (-17 <= a && a <= -2 && -13 <= b && b <= 23) { + int r = a*b; // -391 .. 221 + total += r; + } + if (-17 <= a && a <= -2 && -13 <= b && b <= 0) { + int r = a*b; // 0 .. 221 + total += r; + } + if (-17 <= a && a <= -2 && -13 <= b && b <= -7) { + int r = a*b; // 14 .. 221 + total += r; + } + + return total; +} + +int test16(int x) { + int d, i = 0; + if (x < 0) { + return -1; + } + + while (i < 3) { + i++; + } + d = i; + if (x < 0) { // Comparison is always false. + if (d > -x) { // Unreachable code. + return 1; + } + } + return 0; +} + +// Test ternary expression upper bounds. +unsigned int test_ternary01(unsigned int x) { + unsigned int y1, y2, y3, y4, y5, y6, y7, y8; + y1 = x < 100 ? x : 10; // y1 < 100 + y2 = x >= 100 ? 10 : x; // y2 < 100 + y3 = 0; + y4 = 0; + y5 = 0; + y6 = 0; + y7 = 0; + y8 = 0; + if (x < 300) { + y3 = x ?: 5; // y3 < 300 + y4 = x ?: 500; // y4 <= 500 + y5 = (x+1) ?: 500; // y5 <= 300 + y6 = ((unsigned char)(x+1)) ?: 5; // y6 < 256 + y7 = ((unsigned char)(x+1)) ?: 500; // y7 <= 500 + y8 = ((unsigned short)(x+1)) ?: 500; // y8 <= 300 + } + return y1 + y2 + y3 + y4 + y5 + y6 + y7 + y8; +} + +// Test ternary expression lower bounds. +unsigned int test_ternary02(unsigned int x) { + unsigned int y1, y2, y3, y4, y5; + y1 = x > 100 ? x : 110; // y1 > 100 + y2 = x <= 100 ? 110 : x; // y2 > 100 + y3 = 1000; + y4 = 1000; + y5 = 1000; + if (x >= 300) { + y3 = (x-300) ?: 5; // y3 >= 0 + y4 = (x-200) ?: 5; // y4 >= 100 + y5 = ((unsigned char)(x-200)) ?: 5; // y6 >= 0 + } + return y1 + y2 + y3 + y4 + y5; +} + +// Test the comma expression. +unsigned int test_comma01(unsigned int x) { + unsigned int y = x < 100 ? x : 100; + unsigned int y1; + unsigned int y2; + y1 = (++y, y); + y2 = (y++, y += 3, y); + return y1 + y2; +} diff --git a/cpp/ql/test/library-tests/rangeanalysis/signanalysis/test.cpp b/cpp/ql/test/library-tests/rangeanalysis/signanalysis/test.cpp new file mode 100644 index 000000000000..9a930772b8d7 --- /dev/null +++ b/cpp/ql/test/library-tests/rangeanalysis/signanalysis/test.cpp @@ -0,0 +1,70 @@ +template +class vector { +public: + T& operator[](int); + const T& operator[](int) const; +}; + +int test1(vector vec, int b) { + int x = -1; + if (b) { + x = vec[3]; + } + return x; +} + +// Regression test for ODASA-6013. +int test2(int x) { + int x0 = static_cast(x); + return x0; +} + +// Tests for conversion to bool +bool test3(bool b, int x, int y) { + // The purpose the assignments to `x` below is to generate a lot of + // potential upper and lower bounds for `x`, so that the logic in + // boolConversionLowerBound and boolConversionUpperBound gets exercized. + if (y == 0) { + x = 0; + } + if (y == -1) { + x = -1; + } + if (y == 1) { + x = 1; + } + if (y == -128) { + x = -128; + } + if (y == 128) { + x = 128; + } + if (y == -1024) { + x = -1024; + } + if (y == 1024) { + x = 1024; + } + + int t = 0; + + if (x == 0) { + bool xb = (bool)x; // (bool)x == false + t += (int)xb; + } + + if (x > 0) { + bool xb = (bool)x; // (bool)x == true + t += (int)xb; + } + + if (x < 0) { + bool xb = (bool)x; // (bool)x == true + t += (int)xb; + } + + bool xb = (bool)x; // Value of (bool)x is unknown. + t += (int)xb; + + return b || (bool)t; +}