Skip to content
Merged
Show file tree
Hide file tree
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
)
)
Expand Down Expand Up @@ -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
)
Expand All @@ -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
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

For what reason do you prefer and over | here?

Copy link
Copy Markdown
Contributor Author

@paldepind paldepind Oct 27, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

In my experience | is usually used for some reason. Either because there is an or afterwards or because the thing before and after are somehow different. Here there doesn't seem to be any reason, so going with the default and seems clearer :)

// Compute the minimum of `guardUB` and `defUB`.
if guardUB < defUB then result = guardUB else result = defUB
)
Expand Down Expand Up @@ -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,
Expand Down
Loading