islec panic: Should have been caught by typechecking

[langston-barrett]

I found a program that crashes islec. Details:

$ git rev-parse HEAD

43022c862a1d497f4b8c7c2fce47148775503add

$ cat test.isle

(type bool (primitive bool))
(type i8 (primitive i8))
(type Map extern (enum))

(decl simplify (Map) Map)

(decl pure ne (i8 i8) bool)
(extern extractor ne ne)

(decl Empty () Map)
(extern extractor Empty extr_empty)
(extern constructor Empty constr_empty)

(decl Insert (i8 i8 Map) Map)
(extern extractor Insert extr_insert)
(extern constructor Insert constr_insert)

(decl Remove (i8 Map) Map)
(extern extractor Remove extr_remove)

(rule 0
  (simplify (Insert k v (Empty)))
  (Insert k v (Empty)))

(rule 1
  (simplify (Insert k v (Remove k m)))
  (simplify (Insert k v m)))

(rule 2
  (simplify (Insert k v1 (Insert k v2 m)))
  (simplify (Insert k v1 m)))

(rule 3
  (simplify (Insert k1 v1 (Insert k2 v2 m)))
  (if (ne k1 k2))
  (Insert k1 v1 (Insert k2 v2 (simplify m))))

(rule
  (Remove k (Empty))
  (Empty))

$ cargo run -- test.isle

    Finished dev [unoptimized + debuginfo] target(s) in 0.09s
     Running `/home/langston/code/wasmtime/target/debug/islec test.isle`
thread 'main' panicked at 'Should have been caught by typechecking', cranelift/isle/isle/src/sema.rs:783:26
stack backtrace:
   0:     0x5588d0fc0850 - std::backtrace_rs::backtrace::libunwind::trace::h32eb3e08e874dd27
                               at /rustc/897e37553bba8b42751c67658967889d11ecd120/library/std/src/../../backtrace/src/backtrace/libunwind.rs:93:5
   1:     0x5588d0fc0850 - std::backtrace_rs::backtrace::trace_unsynchronized::haa3f451d27bc11a5
                               at /rustc/897e37553bba8b42751c67658967889d11ecd120/library/std/src/../../backtrace/src/backtrace/mod.rs:66:5
   2:     0x5588d0fc0850 - std::sys_common::backtrace::_print_fmt::h5b94a01bb4289bb5
                               at /rustc/897e37553bba8b42751c67658967889d11ecd120/library/std/src/sys_common/backtrace.rs:66:5
   3:     0x5588d0fc0850 - <std::sys_common::backtrace::_print::DisplayBacktrace as core::fmt::Display>::fmt::hb070b7fa7e3175df
                               at /rustc/897e37553bba8b42751c67658967889d11ecd120/library/std/src/sys_common/backtrace.rs:45:22
   4:     0x5588d0fdda7e - core::fmt::write::hd5207aebbb9a86e9ISLE
                               at /rustc/897e37553bba8b42751c67658967889d11ecd120/library/core/src/fmt/mod.rs:1202:17
   5:     0x5588d0fbdcd5 - std::io::Write::write_fmt::h3bd699bbd129ab8a
                               at /rustc/897e37553bba8b42751c67658967889d11ecd120/library/std/src/io/mod.rs:1679:15
   6:     0x5588d0fc1ed3 - std::sys_common::backtrace::_print::h7a21be552fdf58da
                               at /rustc/897e37553bba8b42751c67658967889d11ecd120/library/std/src/sys_common/backtrace.rs:48:5
   7:     0x5588d0fc1ed3 - std::sys_common::backtrace::print::ha85c41fe4dd80b13
                               at /rustc/897e37553bba8b42751c67658967889d11ecd120/library/std/src/sys_common/backtrace.rs:35:9
   8:     0x5588d0fc1ed3 - std::panicking::default_hook::{{closure}}::h04cca40023d0eeca
                               at /rustc/897e37553bba8b42751c67658967889d11ecd120/library/std/src/panicking.rs:295:22
   9:     0x5588d0fc1bbf - std::panicking::default_hook::haa3ca8c310ed5402
                               at /rustc/897e37553bba8b42751c67658967889d11ecd120/library/std/src/panicking.rs:314:9
  10:     0x5588d0fc257a - std::panicking::rust_panic_with_hook::h7b190ce1a948faac
                               at /rustc/897e37553bba8b42751c67658967889d11ecd120/library/std/src/panicking.rs:698:17
  11:     0x5588d0fc2431 - std::panicking::begin_panic_handler::{{closure}}::hbafbfdc3e1b97f68
                               at /rustc/897e37553bba8b42751c67658967889d11ecd120/library/std/src/panicking.rs:586:13
  12:     0x5588d0fc0cfc - std::sys_common::backtrace::__rust_end_short_backtrace::hda93e5fef243b4c0
                               at /rustc/897e37553bba8b42751c67658967889d11ecd120/library/std/src/sys_common/backtrace.rs:138:18
  13:     0x5588d0fc2192 - rust_begin_unwind
                               at /rustc/897e37553bba8b42751c67658967889d11ecd120/library/std/src/panicking.rs:584:5
  14:     0x5588d0b0b113 - core::panicking::panic_fmt::h8d17ca1073d9a733
                               at /rustc/897e37553bba8b42751c67658967889d11ecd120/library/core/src/panicking.rs:142:14
  15:     0x5588d0d282a6 - cranelift_isle::sema::Expr::visit::h78e17866d60d927d
                               at /home/langston/code/wasmtime/cranelift/isle/isle/src/sema.rs:783:26
  16:     0x5588d0d284ec - cranelift_isle::sema::Expr::visit_in_rule::{{closure}}::hde0977027dc130f4
                               at /home/langston/code/wasmtime/cranelift/isle/isle/src/sema.rs:801:20
  17:     0x5588d0d421f7 - <cranelift_isle::trie_again::RuleSetBuilder as cranelift_isle::sema::RuleVisitor>::add_expr::hed65b425a5a91bad
                               at /home/langston/code/wasmtime/cranelift/isle/isle/src/trie_again.rs:665:9
  18:     0x5588d0d283d6 - cranelift_isle::sema::Expr::visit_in_rule::h5e39eb43e84c3c96
                               at /home/langston/code/wasmtime/cranelift/isle/isle/src/sema.rs:799:9
  19:     0x5588d0d28932 - cranelift_isle::sema::Rule::visit::h893bc3c075cbe6d9
                               at /home/langston/code/wasmtime/cranelift/isle/isle/src/sema.rs:876:27
  20:     0x5588d0dc40f7 - cranelift_isle::trie_again::RuleSetBuilder::add_rule::hce133ad78b5f9338
                               at /home/langston/code/wasmtime/cranelift/isle/isle/src/trie_again.rs:385:36
  21:     0x5588d0dc3407 - cranelift_isle::trie_again::build::h2d99db94c20d37b4
                               at /home/langston/code/wasmtime/cranelift/isle/isle/src/trie_again.rs:216:9
  22:     0x5588d0dcacae - cranelift_isle::overlap::check::h3c7602f0aefa0221
                               at /home/langston/code/wasmtime/cranelift/isle/isle/src/overlap.rs:16:31
  23:     0x5588d0d3da54 - cranelift_isle::compile::compile::h80ee996e2ab2b494
                               at /home/langston/code/wasmtime/cranelift/isle/isle/src/compile.rs:12:17
  24:     0x5588d0b133ef - cranelift_isle::compile::from_files::h531abe844c59cf17
                               at /home/langston/code/wasmtime/cranelift/isle/isle/src/compile.rs:23:5
  25:     0x5588d0b0eb35 - islec::main::h204180e4f764a747
                               at /home/langston/code/wasmtime/cranelift/isle/islec/src/main.rs:27:16
  26:     0x5588d0b10122 - core::ops::function::FnOnce::call_once::haeba8a3e3015b018
                               at /rustc/897e37553bba8b42751c67658967889d11ecd120/library/core/src/ops/function.rs:248:5
  27:     0x5588d0b0c795 - std::sys_common::backtrace::__rust_begin_short_backtrace::he495da2ee4c5c6c7
                               at /rustc/897e37553bba8b42751c67658967889d11ecd120/library/std/src/sys_common/backtrace.rs:122:18
  28:     0x5588d0b150e6 - std::rt::lang_start::{{closure}}::h62a6b89bd67457e9
                               at /rustc/897e37553bba8b42751c67658967889d11ecd120/library/std/src/rt.rs:166:18
  29:     0x5588d0fb927f - core::ops::function::impls::<impl core::ops::function::FnOnce<A> for &F>::call_once::hb69be6e0857c6cfb
                               at /rustc/897e37553bba8b42751c67658967889d11ecd120/library/core/src/ops/function.rs:283:13
  30:     0x5588d0fb927f - std::panicking::try::do_call::h39|6dfc441ee9c786
                               at /rustc/897e37553bba8b42751c67658967889d11ecd120/library/std/src/panicking.rs:492:40
  31:     0x5588d0fb927f - std::panicking::try::h6cdda972d28b3a4f
                               at /rustc/897e37553bba8b42751c67658967889d11ecd120/library/std/src/panicking.rs:456:19
  32:     0x5588d0fb927f - std::panic::catch_unwind::h376039ec264e8ef9
                               at /rustc/897e37553bba8b42751c67658967889d11ecd120/library/std/src/panic.rs:137:14
  33:     0x5588d0fb927f - std::rt::lang_start_internal::{{closure}}::hc94720ca3d4cb727
                               at /rustc/897e37553bba8b42751c67658967889d11ecd120/library/std/src/rt.rs:148:48
  34:     0x5588d0fb927f - std::panicking::try::do_call::h2422fb95933fa2d5
                               at /rustc/897e37553bba8b42751c67658967889d11ecd120/library/std/src/panicking.rs:492:40
  35:     0x5588d0fb927f - std::panicking::try::h488286b5ec8333ff
                               at /rustc/897e37553bba8b42751c67658967889d11ecd120/library/std/src/panicking.rs:456:19
  36:     0x5588d0fb927f - std::panic::catch_unwind::h81636549836d2a25
                               at /rustc/897e37553bba8b42751c67658967889d11ecd120/library/std/src/panic.rs:137:14
  37:     0x5588d0fb927f - std::rt::lang_start_internal::h6ba1bb743c1e9df9
                               at /rustc/897e37553bba8b42751c67658967889d11ecd120/library/std/src/rt.rs:148:20
  38:     0x5588d0b150ba - std::rt::lang_start::h858f0a28ab63a77d
                               at /rustc/897e37553bba8b42751c67658967889d11ecd120/library/std/src/rt.rs:165:17
  39:     0x5588d0b0fe61 - main
  40:     0x7fc5de7f3237 - __libc_start_call_main
  41:     0x7fc5de7f32f5 - __libc_start_main_impl
  42:     0x5588d0b0b3e1 - _start
                               at /build/glibc-2.34/csu/../sysdeps/x86_64/start.S:116
  43:                0x0 - <unknown>

[langston-barrett]

Not sure if this is related or separate, but this slight variation gives an assertion failure:

(type bool (primitive u8))
(type i8 (primitive i8))
(type Map extern (enum))

(decl simplify (Map) Map)

(decl pure ne (i8 i8) bool)
(extern constructor ne ne)

(decl Empty () Map)
(extern extractor Empty extr_empty)
(extern constructor Empty constr_empty)

(decl Insert (i8 i8 Map) Map)
(extern extractor Insert extr_insert)
(extern constructor Insert constr_insert)

(decl Remove (i8 Map) Map)
(extern extractor Remove extr_remove)

(rule 0
  (simplify (Insert k v (Empty)))
  (Insert k v (Empty)))

(rule 1
  (simplify (Insert k v (Remove k m)))
  (simplify (Insert k v m)))

(rule 2
  (simplify (Insert k v1 (Insert k v2 m)))
  (simplify (Insert k v1 m)))

(rule 3
  (simplify (Insert k1 v1 (Insert k2 v2 m)))
  (if (ne k1 k2))
  (Insert k1 v1 (Insert k2 v2 (simplify m))))

(rule
  (Remove k (Empty))
  (Empty))

thread 'main' panicked at 'assertion failed: `(left == right)`
  left: `1`,
 right: `0`', cranelift/isle/isle/src/codegen.rs:433:17

[cfallin]

cc @jameysharp for the codegen assert, and we can take a look at the typechecking hole as well (probably on Monday), but one quick note as I see something:

(decl pure ne (i8 i8) bool) (if (ne k1 k2))

We actually ran into this footgun elsewhere recently, and it is subtle: the (if (ne ...)) form is testing whether the ne constructor matches, not whether it returns true. We'll probably rename if (to if-matches or similar?) to make this clearer -- see this thread on #5676.

So you'll probably want something like (if-let $true (ne k1 k2)). We could potentially add some sugar for that form too if it becomes annoying enough.

[jameysharp]

Chris' suggestion to change the (if (ne ...)) to (if-let $true ...) fixes the codegen assertion failure. The proximate cause of the assertion failure was that of the two rules matching (Insert ... (Insert ...)), the higher-priority one matched first in all the cases where the lower-priority one could possibly match. If the assert were removed, ISLE would have emitted Rust with a return statement for the higher-priority rule, immediately followed by an unreachable if statement to check the equality constraint on the lower-priority rule. Then the Rust compiler would have refused to compile the generated code.

Ideally, overlap/subset checking would have noticed that the rule with priority 2 could never match because the rule with priority 3 would always match first. However, there's an equality constraint in the former rule, and currently that check gives up and decides everything's fine if a rule has any equality constraints, because they're harder to reason about.

I thought this assert was impossible if overlap checking passed, so I didn't think hard about good error messages. But I didn't think about the impact of this hole in overlap checking's completeness.

By the way, a better way to write this pair of rules is to swap their priority and remove the (if ...) entirely. Because the rule which requires equality will match first, we'll only check the other rule when the map keys are not equal.

(rule 3
  (simplify (Insert k v1 (Insert k v2 m)))
  (simplify (Insert k v1 m)))

(rule 2
  (simplify (Insert k1 v1 (Insert k2 v2 m)))
  (Insert k1 v1 (Insert k2 v2 (simplify m))))

[jameysharp]

And I'm not sure why the error that "should have been caught by typechecking", er, wasn't. But I can tell you the problem is that in the first version, the ne term was declared without a constructor, but used in expression context (in an if). You fixed that in the second version by changing it from an extractor to a constructor.

[langston-barrett]

The proximate cause of the assertion failure was that of the two rules matching (Insert ... (Insert ...)), the higher-priority one matched first in all the cases where the lower-priority one could possibly match.

I see, thanks! Changing the rules to not cover one another did indeed fix this.

Thanks to both of you for the ISLE programming tips! I'm excited to use this tool - it's very neat!

[jameysharp]

Glad we could help! I'd love to hear what you're using ISLE for.

Let's leave this issue open even though your immediate issues are resolved, because we really should make sure typechecking actually catches this case instead of hitting a later panic.