Stream: cranelift

Topic: Semantics of `if` clause of ISLE

view this post on Zulip Bongjun Jang (May 19 2025 at 04:01):

Hi, I'm trying to write some mid-end optimization rules in ISLE.
Further, I want to verify the rules with crocus.
But I think I observed a weird behavior of the verifier.
The if clause does not work as expected.

In detail, the rule below is one of the rules I'm writing.
It is a simple rewrite of (X | Y) & Z => Z if (X | Y) & Z = Z.

(rule
  (simplify (band ty (bor ty (iconst ty (u64_from_imm64 x)) (iconst ty (u64_from_imm64 y))) (iconst ty (u64_from_imm64 z))))
  (if (u64_eq z (u64_and z (u64_or x y))))
  (iconst ty (imm64 z)))

Interestingly, the crocus says it is a wrong rewrite with a following counter example.

(simplify
  (band [ty|64]
    (bor [ty|64]
      (iconst [ty|64] (u64_from_imm64 [x|#x0000000000000000]))
      (iconst [ty|64] (u64_from_imm64 [y|#x0000000000000000])))
    (iconst [ty|64] (u64_from_imm64 [z|#x0000000000000001]))))
  (if-let ((_) (u64_eq [z|#x0000000000000001]
    (u64_and [z|#x0000000000000001] (u64_or [x|#x0000000000000000] [y|#x0000000000000000]))))
)
=>
(iconst [ty|64] (imm64 [z|#x0000000000000001]))

#x0000000000000000=>
#x0000000000000001

The (u64_and z (u64_or x y)) in the if clause is evaluated to 0 while z is 1.
Therefore, the whole expression in the if clause is falsy.
That means it should've prevented the rewrite from happening, but it seems like the rewrite is applied anyway.

This is the input I used to run crocus:
spec.isle

And it is the command I used:
crocus -i <the-input.isle> -t simplify --noprelude --codegen <codegen-dir>

view this post on Zulip Chris Fallin (May 19 2025 at 16:01):

cc @Alexa VanHattum and @Michael McLoughlin -- I'm not sure if if clauses are accounted for in the SMT generation for the version that is upstream (in the main repo)? I.e. we may be trying to verify the "widened" rule that omits the conditions and always applies?

view this post on Zulip Chris Fallin (May 19 2025 at 16:01):

(I forget exactly what's been upstreamed but that's my first hunch at least)

view this post on Zulip Bongjun Jang (May 20 2025 at 06:05):

So it could be the SMT encoded from ISLE rule, not the ISLE rule itself?
I remember the crocus paper reported similar problem, so they updated the if semantics on the ISLE side.

view this post on Zulip Chris Fallin (May 20 2025 at 16:06):

Oh! Actually I think we're hitting that same footgun here! It's technically ISLE "operating as designed" but the semantics of (if ...) (as sugar for (if-let _ ...)) look for a match while we've designed our equality helpers to always match but return a true or false value. So I suspect you need (if-let true (u64_eq ...)) instead. Sorry for not picking that up

view this post on Zulip Bongjun Jang (May 21 2025 at 03:10):

Oh yeah. Now it works. Thanks for letting me know.

Last updated: Dec 06 2025 at 07:03 UTC