C++: Make small trivial tweaks

This commit is contained in:
Simon Friis Vindum
2025-10-24 16:16:57 +02:00
parent 5709964fbf
commit d1ea1af945
2 changed files with 9 additions and 13 deletions

View File

@@ -118,10 +118,10 @@ predicate relOpWithSwap(
* *
* This allows for the relation to be either as written, or with its * This allows for the relation to be either as written, or with its
* arguments reversed; for example, if `rel` is `x < 5` then * arguments reversed; for example, if `rel` is `x < 5` then
* `relOpWithSwapAndNegate(rel, x, 5, Lesser(), Strict(), true)`, * - `relOpWithSwapAndNegate(rel, x, 5, Lesser(), Strict(), true)`,
* `relOpWithSwapAndNegate(rel, 5, x, Greater(), Strict(), true)`, * - `relOpWithSwapAndNegate(rel, 5, x, Greater(), Strict(), true)`,
* `relOpWithSwapAndNegate(rel, x, 5, Greater(), Nonstrict(), false)` and * - `relOpWithSwapAndNegate(rel, x, 5, Greater(), Nonstrict(), false)` and
* `relOpWithSwapAndNegate(rel, 5, x, Lesser(), Nonstrict(), false)` hold. * - `relOpWithSwapAndNegate(rel, 5, x, Lesser(), Nonstrict(), false)` hold.
*/ */
predicate relOpWithSwapAndNegate( predicate relOpWithSwapAndNegate(
RelationalOperation rel, Expr a, Expr b, RelationDirection dir, RelationStrictness strict, RelationalOperation rel, Expr a, Expr b, RelationDirection dir, RelationStrictness strict,

View File

@@ -1213,7 +1213,7 @@ private float getLowerBoundsImpl(Expr expr) {
// equal to `min(-y + 1,y - 1)`. // equal to `min(-y + 1,y - 1)`.
exists(float childLB | exists(float childLB |
childLB = getFullyConvertedLowerBounds(remExpr.getAnOperand()) and childLB = getFullyConvertedLowerBounds(remExpr.getAnOperand()) and
not childLB >= 0 childLB < 0
| |
result = getFullyConvertedLowerBounds(remExpr.getRightOperand()) - 1 result = getFullyConvertedLowerBounds(remExpr.getRightOperand()) - 1
or or
@@ -1425,8 +1425,7 @@ private float getUpperBoundsImpl(Expr expr) {
// adding `-rhsLB` to the set of upper bounds. // adding `-rhsLB` to the set of upper bounds.
exists(float rhsLB | exists(float rhsLB |
rhsLB = getFullyConvertedLowerBounds(remExpr.getRightOperand()) and rhsLB = getFullyConvertedLowerBounds(remExpr.getRightOperand()) and
not rhsLB >= 0 rhsLB < 0 and
|
result = -rhsLB + 1 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 | exists(VariableAccess access, Expr guard, boolean branch, float defLB, float guardLB |
phi.isGuardPhi(v, access, guard, branch) and phi.isGuardPhi(v, access, guard, branch) and
lowerBoundFromGuard(guard, access, guardLB, branch) and lowerBoundFromGuard(guard, access, guardLB, branch) and
defLB = getFullyConvertedLowerBounds(access) defLB = getFullyConvertedLowerBounds(access) and
|
// Compute the maximum of `guardLB` and `defLB`. // Compute the maximum of `guardLB` and `defLB`.
if guardLB > defLB then result = guardLB else result = 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 | exists(VariableAccess access, Expr guard, boolean branch, float defUB, float guardUB |
phi.isGuardPhi(v, access, guard, branch) and phi.isGuardPhi(v, access, guard, branch) and
upperBoundFromGuard(guard, access, guardUB, branch) and upperBoundFromGuard(guard, access, guardUB, branch) and
defUB = getFullyConvertedUpperBounds(access) defUB = getFullyConvertedUpperBounds(access) and
|
// Compute the minimum of `guardUB` and `defUB`. // Compute the minimum of `guardUB` and `defUB`.
if guardUB < defUB then result = guardUB else result = 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 * This predicate simplifies the results returned by `linearBoundFromGuard`.
* `linearBoundFromGuard`.
*/ */
private predicate boundFromGuard( private predicate boundFromGuard(
Expr guard, VariableAccess v, float boundValue, boolean isLowerBound, Expr guard, VariableAccess v, float boundValue, boolean isLowerBound,