Skip to content

constraint elimination should understand the (x<0)||(y<0) => (x|y)<0 canonicalization #118114

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

Open
regehr opened this issue Nov 29, 2024 · 3 comments

Comments

@regehr
Copy link
Contributor

regehr commented Nov 29, 2024

here's a function:

extern void side_effect(void);

void f(int v1, int v2) {
  if (v1 < 0) return;
  if (v2 < 0) return;
  if (v2 > -5) return;
  side_effect();
}

at present, we're not optimizing this away. the IR is:

define void @f(i32 noundef %v1, i32 noundef %v2) {
entry:
  %0 = or i32 %v2, %v1
  %or.cond = icmp slt i32 %0, 0
  %cmp4 = icmp sgt i32 %v2, -5
  %or.cond7 = or i1 %cmp4, %or.cond
  br i1 %or.cond7, label %return, label %if.end6

if.end6:                                          ; preds = %entry
  tail call void @side_effect() #2
  br label %return

return:                                           ; preds = %entry, %if.end6
  ret void
}

constraint elimination is correctly learning that !(%0 < 0) but I guess we need a little recognizer for the (x<0)||(y<0) => (x|y)<0 canonicalization

Processing condition to simplify:   %or.cond = icmp slt i32 %0, 0
Checking   %or.cond = icmp slt i32 %0, 0
   failed to decompose condition
Adding 'icmp sle i32 %v2, -5'
  constraint: %v2 <= -5

Checking   %or.cond = icmp slt i32 %0, 0
   failed to decompose condition
Processing condition to simplify:   %cmp4 = icmp sgt i32 %v2, -5
Checking   %cmp4 = icmp sgt i32 %v2, -5
---
%v2 <= -5
sat
---
-1 * %v2 <= 4
sat
Adding 'icmp sge i32 %0, 0'
  constraint: -1 * %0 <= 0

Checking   %cmp4 = icmp sgt i32 %v2, -5
---
-1 * %0 <= 0
%v2 <= -5
sat
---
-1 * %0 <= 0
-1 * %v2 <= 4
sat
Processing fact to add to the system: icmp sle i32 %v2, -5
Adding 'icmp sle i32 %v2, -5'
  constraint: %v2 <= -5

Top of stack : 3 4
CB: 3 4
Processing fact to add to the system: icmp sge i32 %0, 0
Adding 'icmp sge i32 %0, 0'
  constraint: -1 * %0 <= 0

Adding 'icmp uge i32 %0, 0'
  constraint: -1 * %0 <= 0

cc @fhahn @dtcxzyw

@regehr regehr changed the title constraint elimination not adding a signed constraint constraint elimination should understand the (x<0)&&(y<0) => (x|y)<0 canonicalization Nov 29, 2024
@regehr regehr changed the title constraint elimination should understand the (x<0)&&(y<0) => (x|y)<0 canonicalization constraint elimination should understand the (x<0)||(y<0) => (x|y)<0 canonicalization Nov 29, 2024
@regehr
Copy link
Contributor Author

regehr commented Nov 29, 2024

we also have this canonicalization for the and condition:
https://alive2.llvm.org/ce/z/hJBDHx

@dtcxzyw
Copy link
Member

dtcxzyw commented Nov 30, 2024

@nikic Can we extend #97289 to handle bitwise and/or?

@fhahn
Copy link
Contributor

fhahn commented Dec 2, 2024

Should be possible to handle this during de-composition. cc @zjaffal

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.

4 participants