C++: Range analysis guard improvement

[paldepind]

This PR changes how bounds are adjusted for integral types.

If we have a strict lower bound > 1 on an integer then the lower bound is 2. As of now, this is achieved by adding 1 to the lower bound. However, this adjustment is not always ideal.

For this guard, where e is an integer:

(2 * e + 1) > 0

We deduce a lower bound of > -0.5 and after adding 1 we get 0.5. For such a fractional lower bound adding 1 doesn't really make sense. This PR tweaks this slightly, such that the lower bound ends up being 0. A similar adjustment is made for upper bounds.

I ran into this when debugging a performance issue where this showed up. This adjustment didn't fix the performance issue, but I think it's still worthwhile.

Per-commit review is suggested — I also snuck in a few orthogonal changes.

I think the DCA report looks ok. But I'm not used to reading C/C++ reports, so someone else can judge better than me.

[Copilot]

Pull Request Overview

This PR improves how bounds are adjusted for integral types in C++ range analysis. Instead of simply adding/subtracting 1 to adjust bounds from fractional values like -0.5 to 0.5, it now properly handles the conversion to integer bounds by using floor operations to compute more accurate integer bounds.

Key changes:

• Introduces new helper functions adjustLowerBoundIntegral and adjustUpperBoundIntegral for proper bound adjustment
• Replaces simple arithmetic adjustment with floor-based calculations that handle fractional bounds correctly

Reviewed Changes

Copilot reviewed 7 out of 7 changed files in this pull request and generated 1 comment.

Show a summary per file

File	Description
SimpleRangeAnalysis.qll	Adds new adjustment functions and updates bound calculation logic for integral types
RangeAnalysisUtils.qll	Adds toString method to RelationStrictness class and improves documentation
test.c	Adds new test cases for inequality-derived integer bounds
upperBound.expected	Updated test expectations reflecting improved bound calculations
ternaryUpper.expected	Updated test expectations for ternary expressions
ternaryLower.expected	Updated test expectations for ternary expressions
lowerBound.expected	Updated test expectations reflecting improved bound calculations

[Copilot]

This debug module should be removed before merging to production. It contains hardcoded file paths and line numbers specific to testing, which makes it inappropriate for production code.

Suggested change

	/** Provides predicates for debugging the simple range analysis library. */
	private module Debug {
	Locatable getRelevantLocatable() {
	exists(string filepath, int startline |
	result.getLocation().hasLocationInfo(filepath, startline, _, _, _) and
	filepath.matches("%/test.c") and
	startline = [464 .. 472]
	)
	}
	float debugGetFullyConvertedLowerBounds(Expr expr) {
	expr = getRelevantLocatable() and
	result = getFullyConvertedLowerBounds(expr)
	}
	float debugGetLowerBoundsImpl(Expr e, string kl) {
	e = getRelevantLocatable() and
	result = getLowerBoundsImpl(e) and
	kl = e.getPrimaryQlClasses()
	}
	/**
	* Counts the number of lower bounds for a given expression. This predicate is
	* useful for identifying performance issues in the range analysis.
	*/
	predicate nrOfLowerBounds(Expr e, int n) {
	e = getRelevantLocatable() and
	n = strictcount(float lb | lb = getLowerBoundsImpl(e) | lb)
	}
	}