diff --git a/cpp/ql/src/semmle/code/cpp/rangeanalysis/RangeAnalysis.qll b/cpp/ql/src/semmle/code/cpp/rangeanalysis/RangeAnalysis.qll index 50fe6ab9a55..b663f336d0a 100644 --- a/cpp/ql/src/semmle/code/cpp/rangeanalysis/RangeAnalysis.qll +++ b/cpp/ql/src/semmle/code/cpp/rangeanalysis/RangeAnalysis.qll @@ -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`. * diff --git a/cpp/ql/test/library-tests/rangeanalysis/rangeanalysis/RangeAnalysis.expected b/cpp/ql/test/library-tests/rangeanalysis/rangeanalysis/RangeAnalysis.expected index cb3366e91b5..a7d7a6684e3 100644 --- a/cpp/ql/test/library-tests/rangeanalysis/rangeanalysis/RangeAnalysis.expected +++ b/cpp/ql/test/library-tests/rangeanalysis/rangeanalysis/RangeAnalysis.expected @@ -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 |