Repository navigation
Cranelift: rule verifier unsoundness bug #14957
Description
Hi, I think I found the verifier's unsoundness bug regarding bitwidth (type) analysis.
.isle Test Case
Add this to one of the opt files. For example, cranelift/codegen/src/opts/arithmetic.isle
(rule rhs_type_repro (simplify (ireduce ty (iadd cty (sextend cty x) (sextend cty y)))) (iadd ty x y))
Prepare this test case to trigger the rule.
// repro.clif
function %rhs_type_repro(i16, i64) -> i32 {
block0(v0: i16, v1: i64):
v2 = sextend.i128 v0
v3 = sextend.i128 v1
v4 = iadd v2, v3
v5 = ireduce.i32 v4
return v5
}
Steps to Reproduce
- Run the rule verifier with the rule above.
cargo run -p cranelift-isle-veri --bin veri -- --name opt --rule rhs_type_repro --solver z3
This will accept the rule.
However, when the the CLIF file is compiled with optimization:
// cargo run -p cranelift-tools --bin clif-util compile --target x86_64 --set opt_level=speed ./repro.clif
Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.21s
Running `target/debug/clif-util compile --target x86_64 --set opt_level=speed ./repro.clif`
Error: function %rhs_type_repro(i16, i64) -> i32 fast {
block0(v0: i16, v1: i64):
v6 = iadd v0, v1
; ^~~~~~~~~~~~~~~~
; error: inst5 (v6 = iadd.i32 v0, v1): arg 0 (v0) has type i16, expected i32
; error: inst5 (v6 = iadd.i32 v0, v1): arg 1 (v1) has type i64, expected i32
return v6
}
; 2 verifier errors detected (see above). Compilation aborted.
Expected Results
The verifier should reject the rule. This is because of the counterexample as shown in the CLIF test case: (x: i16, y: i64, ty: i32, cty: i128).
While the LHS is valid, the RHS is ill-typed since he x and y have different bitwidths.
Actual Results
The verifier accepts the rule with
============================= Verification summary ============================
...
Applicable: 6
Verification passed: 6
Verification failed: 0
Verification unknown: 0
===============================================================================
Versions and Environment
Cranelift version or commit: 65e9dcc
Operating system: Ubuntu 24.04
Architecture: x86
Extra Info
The verifier collects the type information across both LHS and RHS for type analysis.
However, the type analysis should be directional. That is, it should, using the type info in LHS, determine if the RHS is valid or not.
Thanks for reading!
Activity
avanhatt commentedon Oct 23, 2026
Thank you very much for the report! Looking into it.