hohn/codeql
1
0
Fork 0
mirror of https://github.com/github/codeql.git synced 2025-12-21 11:16:30 +01:00
Code Issues Packages Projects Releases Wiki Activity

C++: Only give the best delta in range analysis

Browse Source 
This mirrors Java's 6b85fe087a.
This commit is contained in:
Jonas Jensen
2019-10-29 11:49:49 +01:00
parent 2cddb82f10
commit 311963906b
2 changed files with 43 additions and 7 deletions
Download Patch File Download Diff File Expand all files Collapse all files

49
cpp/ql/src/semmle/code/cpp/rangeanalysis/RangeAnalysis.qll
View File

@@ -80,7 +80,7 @@ private module RangeAnalysisCache {
cached
module RangeAnalysisPublic {
/**
* Holds if `b + delta` is a valid bound for `i`.
* Holds if `b + delta` is a valid bound for `i` and this is the best such delta.
* - `upper = true` : `i <= b + delta`
* - `upper = false` : `i >= b + delta`
*
@@ -90,11 +90,12 @@ private module RangeAnalysisCache {
*/
cached
predicate boundedInstruction(Instruction i, Bound b, int delta, boolean upper, Reason reason) {
boundedInstruction(i, b, delta, upper, _, _, reason)
boundedInstruction(i, b, delta, upper, _, _, reason) and
bestInstructionBound(i, b, delta, upper)
}
/**
* Holds if `b + delta` is a valid bound for `op`.
* Holds if `b + delta` is a valid bound for `op` and this is the best such delta.
* - `upper = true` : `op <= b + delta`
* - `upper = false` : `op >= b + delta`
*
@@ -104,9 +105,8 @@ private module RangeAnalysisCache {
*/
cached
predicate boundedOperand(Operand op, Bound b, int delta, boolean upper, Reason reason) {
boundedNonPhiOperand(op, b, delta, upper, _, _, reason)
or
boundedPhiOperand(op, b, delta, upper, _, _, reason)
boundedOperandCand(op, b, delta, upper, reason) and
bestOperandBound(op, b, delta, upper)
}
}
@@ -124,6 +124,43 @@ private module RangeAnalysisCache {
private import RangeAnalysisCache
import RangeAnalysisPublic
/**
* Holds if `b + delta` is a valid bound for `e` and this is the best such delta.
* - `upper = true` : `e <= b + delta`
* - `upper = false` : `e >= b + delta`
*/
private predicate bestInstructionBound(Instruction i, Bound b, int delta, boolean upper) {
delta = min(int d | boundedInstruction(i, b, d, upper, _, _, _)) and upper = true
or
delta = max(int d | boundedInstruction(i, b, d, upper, _, _, _)) and upper = false
}
/**
* Holds if `b + delta` is a valid bound for `op`.
* - `upper = true` : `op <= b + delta`
* - `upper = false` : `op >= b + delta`
*
* The reason for the bound is given by `reason` and may be either a condition
* or `NoReason` if the bound was proven directly without the use of a bounding
* condition.
*/
private predicate boundedOperandCand(Operand op, Bound b, int delta, boolean upper, Reason reason) {
boundedNonPhiOperand(op, b, delta, upper, _, _, reason)
or
boundedPhiOperand(op, b, delta, upper, _, _, reason)
}
/**
* Holds if `b + delta` is a valid bound for `op` and this is the best such delta.
* - `upper = true` : `op <= b + delta`
* - `upper = false` : `op >= b + delta`
*/
private predicate bestOperandBound(Operand op, Bound b, int delta, boolean upper) {
delta = min(int d | boundedOperandCand(op, b, d, upper, _)) and upper = true
or
delta = max(int d | boundedOperandCand(op, b, d, upper, _)) and upper = false
}
/**
* Gets a condition that tests whether `vn` equals `bound + delta`.
*

1
cpp/ql/test/library-tests/rangeanalysis/rangeanalysis/RangeAnalysis.expected
View File

@@ -51,7 +51,6 @@
| test.cpp:163:12:163:12 | Load: x | test.cpp:153:23:153:23 | InitializeParameter: y | -1 | false | CompareNE: ... != ... | test.cpp:160:9:160:16 | test.cpp:160:9:160:16 |
| test.cpp:163:12:163:12 | Load: x | test.cpp:153:23:153:23 | InitializeParameter: y | -1 | true | CompareLT: ... < ... | test.cpp:154:6:154:10 | test.cpp:154:6:154:10 |
| test.cpp:163:12:163:12 | Load: x | test.cpp:153:23:153:23 | InitializeParameter: y | -1 | true | CompareNE: ... != ... | test.cpp:160:9:160:16 | test.cpp:160:9:160:16 |
| test.cpp:167:12:167:12 | Load: x | test.cpp:153:23:153:23 | InitializeParameter: y | 0 | false | CompareLT: ... < ... | test.cpp:154:6:154:10 | test.cpp:154:6:154:10 |
| test.cpp:167:12:167:12 | Load: x | test.cpp:153:23:153:23 | InitializeParameter: y | 1 | false | CompareEQ: ... == ... | test.cpp:166:9:166:16 | test.cpp:166:9:166:16 |
| test.cpp:167:12:167:12 | Load: x | test.cpp:153:23:153:23 | InitializeParameter: y | 1 | true | CompareEQ: ... == ... | test.cpp:166:9:166:16 | test.cpp:166:9:166:16 |
| test.cpp:169:12:169:12 | Load: x | test.cpp:153:23:153:23 | InitializeParameter: y | 0 | false | CompareLT: ... < ... | test.cpp:154:6:154:10 | test.cpp:154:6:154:10 |