Stream: git-wasmtime

Topic: wasmtime / issue #14957 Cranelift: rule verifier unsoundn...

view this post on Zulip Wasmtime GitHub notifications bot (Oct 23 2026 at 07:04):

bongjunj opened issue #14957:

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

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: 65e9dcc3e3

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.

view this post on Zulip Wasmtime GitHub notifications bot (Oct 23 2026 at 07:04):

bongjunj added the bug label to Issue #14957.

view this post on Zulip Wasmtime GitHub notifications bot (Oct 23 2026 at 07:04):

bongjunj added the cranelift label to Issue #14957.

view this post on Zulip Wasmtime GitHub notifications bot (Oct 23 2026 at 07:48):

bongjunj edited issue #14957:

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

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: 65e9dcc3e3

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!

view this post on Zulip Wasmtime GitHub notifications bot (Oct 23 2026 at 20:42):

avanhatt commented on issue #14957:

Thank you very much for the report! Looking into it.

Last updated: Oct 31 2026 at 23:03 UTC