Skip to content

C++: Sign analysis library #251

New issue

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

Sign up for GitHub

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

Already on GitHub? Sign in to your account

Merged
jbj merged 14 commits into from
Nov 12, 2018
Merged

C++: Sign analysis library #251

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
14 commits
Select commit Hold shift + click to select a range
a3c6b8e
C++: port sign analysis library from Java
Sep 17, 2018
08e9eea
Add NegateInstruction
Sep 19, 2018
d1ae939
C++: use guards and operands in sign analysis
Sep 19, 2018
554fea4
C++: Sign analysis for casts and unsigned integers
Sep 19, 2018
bf946c3
C++: remove comments about Java implies predicates
Sep 20, 2018
d9e6a6e
Move cached predicates to cached module
Oct 3, 2018
6d06db7
C++: fix comments
Oct 3, 2018
2d04d9e
C++: sync NegateInstruction between IR passes
Oct 3, 2018
9d2d381
C++: test fixes for sign analysis
Oct 15, 2018
1d7e802
C++: move sign analysis to new Operand type
Nov 8, 2018
0d9e209
C++: test for bounded bounds in sign analysis
Nov 8, 2018
72bb7c9
C++: remove double backtick in qldoc
Nov 8, 2018
4fdc992
C++: IRGuards uses Operand; fix CP in SignAnalysis
Nov 8, 2018
d9495da
C++: fix test
Nov 9, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
92 changes: 46 additions & 46 deletions cpp/ql/src/semmle/code/cpp/controlflow/IRGuards.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
)
}

Expand All @@ -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)
)
}
Expand All @@ -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)
)
}

Expand All @@ -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)
)
}

Expand Down Expand Up @@ -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)
)
Expand Down Expand Up @@ -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()
Expand All @@ -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)
Expand All @@ -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
Expand All @@ -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)
Expand All @@ -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
)
Expand All @@ -446,34 +446,34 @@ 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
)
}


/* 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
)
Expand Down
6 changes: 6 additions & 0 deletions cpp/ql/src/semmle/code/cpp/ir/implementation/aliased_ssa/Instruction.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -761,6 +761,12 @@ class RemInstruction extends BinaryInstruction {
}
}

class NegateInstruction extends UnaryInstruction {
NegateInstruction() {
opcode instanceof Opcode::Negate
}
}

Copy link
Contributor

@jbj jbj Oct 3, 2018

Choose a reason for hiding this comment

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

You have to change all three copies of Instruction.qll. Check with buildutils-internal/scripts/pr-checks/sync-identical-files.py if it worked.

class BitAndInstruction extends BinaryInstruction {
BitAndInstruction() {
opcode instanceof Opcode::BitAnd
Expand Down
6 changes: 6 additions & 0 deletions cpp/ql/src/semmle/code/cpp/ir/implementation/raw/Instruction.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
6 changes: 6 additions & 0 deletions cpp/ql/src/semmle/code/cpp/ir/implementation/unaliased_ssa/Instruction.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Loading