From 17e0dec08a4a5bbf5d2225dbf1b03e7bf2313a08 Mon Sep 17 00:00:00 2001 From: Simon Friis Vindum Date: Fri, 24 Oct 2025 16:01:38 +0200 Subject: [PATCH 1/5] C++: Add toString for RelationStrictness This helps for debugging. --- .../cpp/rangeanalysis/RangeAnalysisUtils.qll | 17 +++++++++++++++-- 1 file changed, 15 insertions(+), 2 deletions(-) diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/RangeAnalysisUtils.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/RangeAnalysisUtils.qll index 07c6ee1cd2b3..58c824453317 100644 --- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/RangeAnalysisUtils.qll +++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/RangeAnalysisUtils.qll @@ -1,10 +1,10 @@ import cpp /** - * Describes whether a relation is 'strict' (that is, a `<` or `>` + * The strictness of a relation. Either 'strict' (that is, a `<` or `>` * relation) or 'non-strict' (a `<=` or `>=` relation). */ -newtype RelationStrictness = +newtype TRelationStrictness = /** * Represents that a relation is 'strict' (that is, a `<` or `>` relation). */ @@ -14,6 +14,19 @@ newtype RelationStrictness = */ Nonstrict() +/** + * The strictness of a relation. Either 'strict' (that is, a `<` or `>` + * relation) or 'non-strict' (a `<=` or `>=` relation). + */ +class RelationStrictness extends TRelationStrictness { + /** Gets the string representation of this relation strictness. */ + string toString() { + this = Strict() and result = "strict" + or + this = Nonstrict() and result = "non-strict" + } +} + /** * Describes whether a relation is 'greater' (that is, a `>` or `>=` * relation) or 'lesser' (a `<` or `<=` relation). From 3af9885489d0fefdcae83ffff5c58876fde6aa40 Mon Sep 17 00:00:00 2001 From: Simon Friis Vindum Date: Fri, 24 Oct 2025 16:04:34 +0200 Subject: [PATCH 2/5] C++: Fix typos in tests --- .../library-tests/rangeanalysis/SimpleRangeAnalysis/test.c | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/test.c b/cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/test.c index 61996ffa840b..c161dcdbb058 100644 --- a/cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/test.c +++ b/cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/test.c @@ -914,7 +914,7 @@ void guard_with_exit(int x, int y) { // This test ensures that we correctly identify // that the upper bound for y is max_int when calling `out(y)`. - // The RangeSsa will place guardPhy on `out(y)`, and consequently there is no + // The RangeSsa will place guardPhi on `out(y)`, and consequently there is no // frontier phi node at out(y). } @@ -922,7 +922,7 @@ void test(int x) { if (x >= 10) { return; } - // The basic below has two predecessors. + // The basic block below has two predecessors. label: out(x); goto label; From 383e6a44aa20746baf23f2bc72c37f16932840e4 Mon Sep 17 00:00:00 2001 From: Simon Friis Vindum Date: Fri, 24 Oct 2025 16:08:35 +0200 Subject: [PATCH 3/5] C++: Use `or` instead of `if` The proposition in the true branch implied the condition, so `or` is more appropriate. Also eliminated an existentially quantified variable. --- .../cpp/rangeanalysis/SimpleRangeAnalysis.qll | 37 +++++++++---------- 1 file changed, 18 insertions(+), 19 deletions(-) diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/SimpleRangeAnalysis.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/SimpleRangeAnalysis.qll index a2e41fcf6931..802d816945ba 100644 --- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/SimpleRangeAnalysis.qll +++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/SimpleRangeAnalysis.qll @@ -111,25 +111,24 @@ float widenUpperBound(Type type, float ub) { * compilation units, which doesn't necessarily have a getValue() result from the extractor. */ private string getValue(Expr e) { - if exists(e.getValue()) - then result = e.getValue() - else - /* - * It should be safe to propagate the initialization value to a variable if: - * The type of v is const, and - * The type of v is not volatile, and - * Either: - * v is a local/global variable, or - * v is a static member variable - */ - - exists(VariableAccess access, StaticStorageDurationVariable v | - not v.getUnderlyingType().isVolatile() and - v.getUnderlyingType().isConst() and - e = access and - v = access.getTarget() and - result = getValue(v.getAnAssignedValue()) - ) + result = e.getValue() + or + not exists(e.getValue()) and + /* + * It should be safe to propagate the initialization value to a variable if: + * The type of v is const, and + * The type of v is not volatile, and + * Either: + * v is a local/global variable, or + * v is a static member variable + */ + + exists(StaticStorageDurationVariable v | + not v.getUnderlyingType().isVolatile() and + v.getUnderlyingType().isConst() and + v = e.(VariableAccess).getTarget() and + result = getValue(v.getAnAssignedValue()) + ) } /** From 5709964fbf356ee642a755bec5f95799d7055a5c Mon Sep 17 00:00:00 2001 From: Simon Friis Vindum Date: Fri, 24 Oct 2025 16:12:05 +0200 Subject: [PATCH 4/5] C++: Simplify boundFromGuard The last disjunct in `boundFromGuard` is moved into `linearBoundFromGuard`. This avoids repeating the calculation for `boundValue`. `getBounds` and `getExprTypeBounds` are turned into predicates with result. Their middle argument was the "output" which was confusing. --- .../cpp/rangeanalysis/SimpleRangeAnalysis.qll | 89 +++++++++---------- 1 file changed, 40 insertions(+), 49 deletions(-) diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/SimpleRangeAnalysis.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/SimpleRangeAnalysis.qll index 802d816945ba..942b81551397 100644 --- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/SimpleRangeAnalysis.qll +++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/SimpleRangeAnalysis.qll @@ -1770,22 +1770,10 @@ private predicate boundFromGuard( ) { exists(float p, float q, float r, boolean isLB | linearBoundFromGuard(guard, v, p, q, r, isLB, strictness, branch) and - boundValue = (r - q) / p - | + boundValue = (r - q) / p and // If the multiplier is negative then the direction of the comparison // needs to be flipped. - p > 0 and isLowerBound = isLB - or - p < 0 and isLowerBound = isLB.booleanNot() - ) - or - // When `!e` is true, we know that `0 <= e <= 0` - exists(float p, float q, Expr e | - linearAccess(e, v, p, q) and - eqZeroWithNegate(guard, e, true, branch) and - boundValue = (0.0 - q) / p and - isLowerBound = [false, true] and - strictness = Nonstrict() + if p < 0 then isLowerBound = isLB.booleanNot() else isLowerBound = isLB ) } @@ -1795,54 +1783,57 @@ private predicate boundFromGuard( * lower or upper bound for `v`. */ private predicate linearBoundFromGuard( - ComparisonOperation guard, VariableAccess v, float p, float q, float boundValue, + Expr guard, VariableAccess v, float p, float q, float r, boolean isLowerBound, // Is this a lower or an upper bound? RelationStrictness strictness, boolean branch // Which control-flow branch is this bound valid on? ) { - // For the comparison x < RHS, we create two bounds: - // - // 1. x < upperbound(RHS) - // 2. x >= typeLowerBound(RHS.getUnspecifiedType()) - // - exists(Expr lhs, Expr rhs, RelationDirection dir, RelationStrictness st | - linearAccess(lhs, v, p, q) and - relOpWithSwapAndNegate(guard, lhs, rhs, dir, st, branch) - | - isLowerBound = directionIsGreater(dir) and - strictness = st and - getBounds(rhs, boundValue, isLowerBound) + exists(Expr lhs | linearAccess(lhs, v, p, q) | + // For the comparison x < RHS, we create the following bounds: + // 1. x < upperbound(RHS) + // 2. x >= typeLowerBound(RHS.getUnspecifiedType()) + exists(Expr rhs, RelationDirection dir, RelationStrictness st | + relOpWithSwapAndNegate(guard, lhs, rhs, dir, st, branch) + | + isLowerBound = directionIsGreater(dir) and + strictness = st and + r = getBounds(rhs, isLowerBound) + or + isLowerBound = directionIsLesser(dir) and + strictness = Nonstrict() and + r = getExprTypeBounds(rhs, isLowerBound) + ) or - isLowerBound = directionIsLesser(dir) and - strictness = Nonstrict() and - exprTypeBounds(rhs, boundValue, isLowerBound) - ) - or - // For x == RHS, we create the following bounds: - // - // 1. x <= upperbound(RHS) - // 2. x >= lowerbound(RHS) - // - exists(Expr lhs, Expr rhs | - linearAccess(lhs, v, p, q) and - eqOpWithSwapAndNegate(guard, lhs, rhs, true, branch) and - getBounds(rhs, boundValue, isLowerBound) and + // For x == RHS, we create the following bounds: + // 1. x <= upperbound(RHS) + // 2. x >= lowerbound(RHS) + exists(Expr rhs | + eqOpWithSwapAndNegate(guard, lhs, rhs, true, branch) and + r = getBounds(rhs, isLowerBound) and + strictness = Nonstrict() + ) + or + // When `x` is equal to 0 we create the following bounds: + // 1. x <= 0 + // 2. x >= 0 + eqZeroWithNegate(guard, lhs, true, branch) and + r = 0.0 and + isLowerBound = [false, true] and strictness = Nonstrict() ) - // x != RHS and !x are handled elsewhere } -/** Utility for `linearBoundFromGuard`. */ -private predicate getBounds(Expr expr, float boundValue, boolean isLowerBound) { - isLowerBound = true and boundValue = getFullyConvertedLowerBounds(expr) +/** Get the fully converted lower or upper bounds of `expr` based on `isLowerBound`. */ +private float getBounds(Expr expr, boolean isLowerBound) { + isLowerBound = true and result = getFullyConvertedLowerBounds(expr) or - isLowerBound = false and boundValue = getFullyConvertedUpperBounds(expr) + isLowerBound = false and result = getFullyConvertedUpperBounds(expr) } /** Utility for `linearBoundFromGuard`. */ -private predicate exprTypeBounds(Expr expr, float boundValue, boolean isLowerBound) { - isLowerBound = true and boundValue = exprMinVal(expr.getFullyConverted()) +private float getExprTypeBounds(Expr expr, boolean isLowerBound) { + isLowerBound = true and result = exprMinVal(expr.getFullyConverted()) or - isLowerBound = false and boundValue = exprMaxVal(expr.getFullyConverted()) + isLowerBound = false and result = exprMaxVal(expr.getFullyConverted()) } /** From d1ea1af9452f29ec32ad2d48d0206de683ad7559 Mon Sep 17 00:00:00 2001 From: Simon Friis Vindum Date: Fri, 24 Oct 2025 16:16:57 +0200 Subject: [PATCH 5/5] C++: Make small trivial tweaks --- .../code/cpp/rangeanalysis/RangeAnalysisUtils.qll | 8 ++++---- .../code/cpp/rangeanalysis/SimpleRangeAnalysis.qll | 14 +++++--------- 2 files changed, 9 insertions(+), 13 deletions(-) diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/RangeAnalysisUtils.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/RangeAnalysisUtils.qll index 58c824453317..2423a3a71a0a 100644 --- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/RangeAnalysisUtils.qll +++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/RangeAnalysisUtils.qll @@ -118,10 +118,10 @@ predicate relOpWithSwap( * * This allows for the relation to be either as written, or with its * arguments reversed; for example, if `rel` is `x < 5` then - * `relOpWithSwapAndNegate(rel, x, 5, Lesser(), Strict(), true)`, - * `relOpWithSwapAndNegate(rel, 5, x, Greater(), Strict(), true)`, - * `relOpWithSwapAndNegate(rel, x, 5, Greater(), Nonstrict(), false)` and - * `relOpWithSwapAndNegate(rel, 5, x, Lesser(), Nonstrict(), false)` hold. + * - `relOpWithSwapAndNegate(rel, x, 5, Lesser(), Strict(), true)`, + * - `relOpWithSwapAndNegate(rel, 5, x, Greater(), Strict(), true)`, + * - `relOpWithSwapAndNegate(rel, x, 5, Greater(), Nonstrict(), false)` and + * - `relOpWithSwapAndNegate(rel, 5, x, Lesser(), Nonstrict(), false)` hold. */ predicate relOpWithSwapAndNegate( RelationalOperation rel, Expr a, Expr b, RelationDirection dir, RelationStrictness strict, diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/SimpleRangeAnalysis.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/SimpleRangeAnalysis.qll index 942b81551397..fcb99487d2a3 100644 --- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/SimpleRangeAnalysis.qll +++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/SimpleRangeAnalysis.qll @@ -1213,7 +1213,7 @@ private float getLowerBoundsImpl(Expr expr) { // equal to `min(-y + 1,y - 1)`. exists(float childLB | childLB = getFullyConvertedLowerBounds(remExpr.getAnOperand()) and - not childLB >= 0 + childLB < 0 | result = getFullyConvertedLowerBounds(remExpr.getRightOperand()) - 1 or @@ -1425,8 +1425,7 @@ private float getUpperBoundsImpl(Expr expr) { // adding `-rhsLB` to the set of upper bounds. exists(float rhsLB | rhsLB = getFullyConvertedLowerBounds(remExpr.getRightOperand()) and - not rhsLB >= 0 - | + rhsLB < 0 and result = -rhsLB + 1 ) ) @@ -1571,8 +1570,7 @@ private float getPhiLowerBounds(StackVariable v, RangeSsaDefinition phi) { exists(VariableAccess access, Expr guard, boolean branch, float defLB, float guardLB | phi.isGuardPhi(v, access, guard, branch) and lowerBoundFromGuard(guard, access, guardLB, branch) and - defLB = getFullyConvertedLowerBounds(access) - | + defLB = getFullyConvertedLowerBounds(access) and // Compute the maximum of `guardLB` and `defLB`. if guardLB > defLB then result = guardLB else result = defLB ) @@ -1596,8 +1594,7 @@ private float getPhiUpperBounds(StackVariable v, RangeSsaDefinition phi) { exists(VariableAccess access, Expr guard, boolean branch, float defUB, float guardUB | phi.isGuardPhi(v, access, guard, branch) and upperBoundFromGuard(guard, access, guardUB, branch) and - defUB = getFullyConvertedUpperBounds(access) - | + defUB = getFullyConvertedUpperBounds(access) and // Compute the minimum of `guardUB` and `defUB`. if guardUB < defUB then result = guardUB else result = defUB ) @@ -1761,8 +1758,7 @@ private predicate upperBoundFromGuard(Expr guard, VariableAccess v, float ub, bo } /** - * This predicate simplifies the results returned by - * `linearBoundFromGuard`. + * This predicate simplifies the results returned by `linearBoundFromGuard`. */ private predicate boundFromGuard( Expr guard, VariableAccess v, float boundValue, boolean isLowerBound,