Stream: git-wasmtime

Topic: wasmtime / issue #10277 [Crocus] crocus example does not ...

view this post on Zulip Wasmtime GitHub notifications bot (Feb 23 2025 at 09:34):

bongjunj opened issue #10277:

Hi, I'm running the examples of crocus (cranelift/isle/veri/veri_engine).
The doc says I can test crocus using the following command:

cargo build --package=veri_engine # build crocus

path/to/pcrocus -i cranelift/isle/veri/veri_engine/examples/mid-end/broken_bor_band_consts.isle -t simplify --codegen cranelift/codegen/ --x64

(I added --x64 part since the error message tells me to do so)

But it fails with the following error messages

Writing generated file: /home/llfuzz/transopt-experiment/wasmtime/output/clif_opt.isle
Writing generated file: /home/llfuzz/transopt-experiment/wasmtime/output/clif_lower.isle
Missing term type instantiation for simplify

But the input ISLE file does have instantiation for simplify.

// wasmtime/cranelift/isle/veri/veri_engine/examples/mid-end/broken_bor_band_consts.isle
// ...

(spec (simplify x) (provide (= x result)))
(instantiate simplify
    ((args (bv 8)) (ret (bv 8)) (canon (bv 8)))
    ((args (bv 16)) (ret (bv 16)) (canon (bv 16)))
    ((args (bv 32)) (ret (bv 32)) (canon (bv 32)))
    ((args (bv 64)) (ret (bv 64)) (canon (bv 64)))
)
(decl simplify (Value) Value)

// ...

I think the parsing part is not working for crocus.

view this post on Zulip Wasmtime GitHub notifications bot (Feb 24 2025 at 05:58):

cfallin commented on issue #10277:

cc @avanhatt or @mmcloughlin , any thoughts?

view this post on Zulip Wasmtime GitHub notifications bot (Feb 25 2025 at 23:17):

avanhatt commented on issue #10277:

Thanks for the report!

Looks like there are 2 issues:

  1. The documentation should specify that for "broken" examples, you should pass --noprelude instead of e.g. --x64. This is because the broken examples include the necessary definitions without pulling in the x64/aarch64 preludes. In this case, the broken example is also from the midend, so no specific target architecture is relevant. I'll update the documentation to include this.
  2. It looks like maybe #9593 made a breaking change to the test file in changing ISLE's boolean representation, which we didn't catch because Crocus currently isn't running in CI on main in this repo. You can fix it by deleting the line (extern const true bool) from the file.

After deleting that line, you should be able to run the following successfully to get the counterexample:

<crocus> -i cranelift/isle/veri/veri_engine/examples/mid-end/broken_bor_band_consts.isle -t simplify --noprelude --codegen cranelift/codegen/

I'll also put up a PR to fix this, but probably won't have time to get to that until later this week. Thanks!

Last updated: Feb 28 2025 at 01:30 UTC