Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Simplify add-with-overflow pattern (uaddo) #65863

Closed
chfast opened this issue Sep 9, 2023 · 0 comments · Fixed by #65910
Closed

Simplify add-with-overflow pattern (uaddo) #65863

chfast opened this issue Sep 9, 2023 · 0 comments · Fixed by #65910

Comments

@chfast
Copy link
Member

chfast commented Sep 9, 2023

For unsigned integers to check if an addition overflowed (get carry bit) it is enough to compare the sum with one of its arguments carry = sum < a. However, it is not obvious that it is enough to only check one of the arguments and we may encounter a pattern where both arguments are checked.

define i1 @src(i64 %a, i64 %b){
  %s = add i64 %a, %b
  %cond_a = icmp ult i64 %s, %a
  %cond_b = icmp ult i64 %s, %b
  %cond = or i1 %cond_a, %cond_b
  ret i1 %cond
}

define i1 @tgt(i64 %a, i64 %b){
  %s = add i64 %a, %b
  %cond_a = icmp ult i64 %s, %a
  ret i1 %cond_a
}

Playground: https://godbolt.org/z/TW8enc6zo
Proof: https://alive2.llvm.org/ce/z/iPAE7t

@dtcxzyw dtcxzyw self-assigned this Sep 10, 2023
@RKSimon RKSimon removed the new issue label Sep 10, 2023
dtcxzyw added a commit that referenced this issue Sep 28, 2023
This patch simplifies the overflow check of unsigned addition.

`a + b <u a` implies `a + b <u b`
`a + b >=u a` implies `a + b >=u b`

Alive2: https://alive2.llvm.org/ce/z/H8oK8n
Fixes #65863.
legrosbuffle pushed a commit to legrosbuffle/llvm-project that referenced this issue Sep 29, 2023
This patch simplifies the overflow check of unsigned addition.

`a + b <u a` implies `a + b <u b`
`a + b >=u a` implies `a + b >=u b`

Alive2: https://alive2.llvm.org/ce/z/H8oK8n
Fixes llvm#65863.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging a pull request may close this issue.

3 participants