Skip to content

Cranelift: Rewrite or(and(x, y), not(y)) => or(x, not(y)) #5676

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.

Sign up for GitHub

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

Merged
fitzgen merged 1 commit into from
Jan 31, 2023
Merged

Cranelift: Rewrite or(and(x, y), not(y)) => or(x, not(y)) #5676

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
5 changes: 5 additions & 0 deletions cranelift/codegen/src/isle_prelude.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -109,6 +109,11 @@ macro_rules! isle_common_prelude_methods {
!x
}

#[inline]
fn u64_eq(&mut self, x: u64, y: u64) -> u64 {
u64::from(x == y)
}

#[inline]
fn u64_is_zero(&mut self, value: u64) -> bool {
0 == value
Expand Down
27 changes: 27 additions & 0 deletions cranelift/codegen/src/opts/algebraic.isle
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -138,6 +138,33 @@
(rule (simplify (bnot ty (band t x y)))
(bor ty (bnot ty x) (bnot ty y)))

;; `or(and(x, y), not(y)) == or(x, not(y))`
(rule (simplify (bor ty
(band ty x y)
z @ (bnot ty y)))
Comment thread
fitzgen marked this conversation as resolved.
(bor ty x z))
;; Duplicate the rule but swap the `bor` operands because `bor` is
;; commutative. We could, of course, add a `simplify` rule to do the commutative
;; swap for all `bor`s but this will bloat the e-graph with many e-nodes. It is
;; cheaper to have additional rules, rather than additional e-nodes, because we
;; amortize their cost via ISLE's smart codegen.
(rule (simplify (bor ty
z @ (bnot ty y)
(band ty x y)))
(bor ty x z))

;; `or(and(x, y), not(y)) == or(x, not(y))` specialized for constants, since
;; otherwise we may not know that `z == not(y)` since we don't generally expand
;; constants in the e-graph.
;;
;; (No need to duplicate for commutative `bor` for this constant version because
;; we move constants to the right.)
(rule (simplify (bor ty
(band ty x (iconst ty (u64_from_imm64 y)))
z @ (iconst ty (u64_from_imm64 zk))))
(if (u64_eq zk (u64_not y)))
(bor ty x z))
Copy link
Copy Markdown
Member

@avanhatt avanhatt Feb 1, 2023

Choose a reason for hiding this comment

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

Our verifier prototype finds the following counterexample for this rule (lightly edited for readability):

simplify (lhs):
#x0000000000000000
#b0

bor (rhs):
#x0000000000000001
#b1

x:
#x0000000000000001
#b1

y:
#x0000000000000002
#b10

z:
#x0000000000000000
#b0

zk:
#x0000000000000000
#b0

Copy link
Copy Markdown
Member Author

@fitzgen fitzgen Feb 1, 2023

Choose a reason for hiding this comment

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

I believe that this is because the if precondition is buggy. It is just checking whether the constructor succeeds or not, it is not checking if it returned true. Basically ignoring that predicate. (Funnily enough, because u64_eq is pure, the constructor will always succeed! This seems like something the ISLE compiler can check for and reject.) This is a pretty big foot gun with if, IMHO.

Anyways, the predicate needs to be rewritten as (if-let $true ...).

Copy link
Copy Markdown
Contributor

@jameysharp jameysharp Feb 1, 2023

Choose a reason for hiding this comment

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

That's so cool! I don't understand it but it's awesome. 😆

Here's what's confusing me: The rule should only fire if zk is equal to !y. But in this counterexample, y is 2, so u64_not y is 0xfffffffffffffffd, but zk is 0. Is the verifier missing the if condition? Or is u64_not modeled incorrectly, maybe? (It's supposed to be bitwise-not, but this counterexample would make sense if that were modeled as boolean-not, turning non-zero values into 0.)

Also, what type is this counterexample for? I'd be especially interested if you can find counterexamples for I64 specifically, because I think the rule as-written is wrong for any other width. That said, I'd expect other widths to just fail to match the rule most of the time, rather than ever rewriting incorrectly, so if you find a narrower counterexample it's probably a real issue.

Copy link
Copy Markdown
Contributor

@jameysharp jameysharp Feb 1, 2023

Choose a reason for hiding this comment

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

Ohhh, Nick's got it right. Although it's because u64_eq is not partial, not because it's pure. (Those flags are independent now.)

We also need to mask both constants down to the appropriate width if we want to make the rule fire on <64-bit types.

Copy link
Copy Markdown
Member

@avanhatt avanhatt Feb 1, 2023 •
edited
Loading

Choose a reason for hiding this comment

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

To restate what @fitzgen realized:

(if (u64_eq zk (u64_not y))) desugars to (if-let _ (u64_eq zk (u64_not y))), which ISLE is perfectly happy to match on. That is, the semantics for if is whether some match is possible, not whether the match is possible and its boolean value is truthy. The verifier models these weird semantics implicitly, since it treats if-let statements as constraints setting the LHS and RHS of the if-let clause to be equal---in this case, happily setting the wildcard to false and considering the rule to have matched.

Right now, this counterexample is for BVs of width 64, and the verifier is complaining that the rule is infeasible (that is, doesn't match) for other widths (which, based on your comment, seems correct?).


;; x*2 == 2*x == x+x.
(rule (simplify (imul ty x (iconst _ (simm32 2))))
(iadd ty x x))
Expand Down
3 changes: 3 additions & 0 deletions cranelift/codegen/src/prelude.isle
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -141,6 +141,9 @@
(decl pure u64_not (u64) u64)
(extern constructor u64_not u64_not)

(decl pure u64_eq (u64 u64) u64)
(extern constructor u64_eq u64_eq)

(decl pure u64_sextend_u32 (u64) u64)
(extern constructor u64_sextend_u32 u64_sextend_u32)

Expand Down
44 changes: 43 additions & 1 deletion cranelift/filetests/filetests/egraph/algebraic.clif
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,7 @@ block0(v0: i32):
return v3
; check: v4 = iconst.i32 0xffff_ffe0
; check: v5 = band v0, v4
; return v5
; check: return v5
}

function %unsigned_shift_right_shift_left_i64(i64) -> i64 {
Expand Down Expand Up @@ -86,3 +86,45 @@ block0(v0: i64):
; check: v5 = band v0, v4
; return v5
}

function %or_and_y_with_not_y(i8, i8) -> i8 {
block0(v0: i8, v1: i8):
v2 = band v0, v1
v3 = bnot v1
v4 = bor v2, v3
return v4
; check: v5 = bor v0, v3
; check: return v5
}

function %or_and_constant_with_not_constant(i8) -> i8 {
Comment thread
fitzgen marked this conversation as resolved.
block0(v0: i8):
v1 = iconst.i8 -4
v2 = band v0, v1
v3 = iconst.i8 3
v4 = bor v2, v3
return v4
; check: v5 = bor v0, v3
; check: return v5
}

function %or_and_y_with_not_y(i8, i8) -> i8 {
block0(v0: i8, v1: i8):
v2 = band v0, v1
v3 = bnot v1
v4 = bor v3, v2
return v4
; check: v5 = bor v0, v3
; check: return v5
}

function %or_and_constant_with_not_constant(i8) -> i8 {
block0(v0: i8):
v1 = iconst.i8 -4
v2 = band v0, v1
v3 = iconst.i8 3
v4 = bor v3, v2
return v4
; check: v6 = bor v0, v3
; check: return v6
}
34 changes: 34 additions & 0 deletions cranelift/filetests/filetests/runtests/or-and-y-with-not-y.clif
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,34 @@
;; Test the rewrite: `or(and(x, y), not(y)) => or(x, not(y))`

test interpret
test run
target aarch64
target x86_64
target riscv64
target s390x

function %or_and_y_with_not_y(i8, i8) -> i8 {
block0(v0: i8, v1: i8):
v2 = band v0, v1
v3 = bnot v1
v4 = bor v2, v3
return v4
}
; run: %or_and_y_with_not_y(0xff, 0x0a) == 0xff
; run: %or_and_y_with_not_y(0xff, 0xb0) == 0xff
; run: %or_and_y_with_not_y(0xaa, 0x0a) == 0xff
; run: %or_and_y_with_not_y(0xaa, 0xb0) == 0xef
; run: %or_and_y_with_not_y(0x00, 0x0a) == 0xf5
; run: %or_and_y_with_not_y(0x00, 0xb0) == 0x4f

function %or_and_constant_with_not_constant(i8) -> i8 {
block0(v0: i8):
v1 = iconst.i8 -4
v2 = band v0, v1
v3 = iconst.i8 3
v4 = bor v2, v3
return v4
}
; run: %or_and_constant_with_not_constant(0xff) == 0xff
; run: %or_and_constant_with_not_constant(0xaa) == 0xab
; run: %or_and_constant_with_not_constant(0x00) == 0x03