Stream: git-wasmtime

Topic: wasmtime / PR #13225 Fix souper harvest

Wasmtime GitHub notifications bot (Apr 29 2026 at 01:38):

bongjunj opened PR #13225 from bongjunj:souper to bytecodealliance:main:

<!--
Please make sure you include the following information:

• If this work has been discussed elsewhere, please include a link to that
  conversation. If it was discussed in an issue, just mention "issue #...".

• Explain why this change is needed. If the details are in an issue already,
  this can be brief.

Our development process is documented in the Wasmtime book:
https://docs.wasmtime.dev/contributing-development-process.html

Please ensure all communication follows the code of conduct:
https://github.com/bytecodealliance/wasmtime/blob/main/CODE_OF_CONDUCT.md
-->

Currently, clif-util souper-harvest has limitations where:

1. It does not translate bnot instruction to Souper IR, and
2. It does not correctly infer types of instructions that use an icmp instruction.

The fix for the first one is straightforward. I added a translation from bnot x (in CLIF) to xor x, -1 (in Souper IR).

The second problem arises when an instruction uses a value produced by an icmp instruction.
In Cranelift, icmp produces an i8 value; therefore, its users usually also are of i8 type too.
However, in Souper/LLVM, icmp produces an i1 value; therefore, its users, without casting, users must be of i1 type.
The current problem of the harvest is that, when determining the type of an Souper value, it directly copies the type of that of CLIF side. For example,

function %test_bor_slt_eq(i32, i32) -> i8 fast {
block0(v0: i32, v1: i32):
    v2 = icmp slt v0, v1
    v3 = icmp eq v0, v1
    v4 = bor v2, v3
    return v4
}

is translated to

...
%0:i32 = var
%1:i32 = var
%2:i1 = slt %0, %1
%3:i1 = eq %0, %1
%4:i8 = or %2, %3
infer %4

which causes type mismatch, preventing Souper from running properly. (Notice that or is i8!)

I fixed this by carrying Souper-side type information with new SouperValue struct, while such a type information is produced in souper_type_of function. Initial type informations are only produced for constants (iconst), variables, and type-casts.

However, I didn't yet implement type unification. A proper implementation would require a larger refactor to make operand types mutable and propagate inferred types back to other values. The current change is intentionally narrower to keep this simple.

Test Results

cargo run -- souper-harvest --target x86_64 cranelift/filetests/filetests/egraph/bitops.clif -o /tmp/souper/
./run-souper.sh souper-check /tmp/souper/

• Before: Produced 57 left-hand sides. 17 souper-check inference successes. 34 timed out.
  • Fails on the example case above.
• After: Processing 72 left-hand sides. 21 souper-check inference succeesses. 50 timed out.

Wasmtime GitHub notifications bot (Apr 29 2026 at 01:38):

bongjunj requested alexcrichton for a review on PR #13225.

Wasmtime GitHub notifications bot (Apr 29 2026 at 01:38):

bongjunj requested wasmtime-compiler-reviewers for a review on PR #13225.

Wasmtime GitHub notifications bot (Apr 29 2026 at 06:34):

github-actions[bot] added the label cranelift on PR #13225.

Wasmtime GitHub notifications bot (Apr 29 2026 at 12:39):

:memo: fitzgen submitted PR review:

Thanks @bongjunj! One question below.

Wasmtime GitHub notifications bot (Apr 29 2026 at 12:39):

:speech_balloon: fitzgen created PR review comment:

Would it be good enough to eagerly translate CLIF icmp instructions into two Souper instructions: a compare followed by a zero extend? Eg something like this:

;; CLIF
v3 = icmp eq v1, v2
v4 = bor v3, v3

;; Souper
%3:i1 = eq %1, %2
%4:i8 = zext %3
%5:i8 = or %4, %4

I think this would be a bit simpler and lets us avoid the SouperValue machinery, while also fixing the same set of type mismatch bugs? But I'm not 100% sure on that, so I'm interested in your feedback and whether you considered this approach.

Wasmtime GitHub notifications bot (Apr 29 2026 at 13:05):

alexcrichton unassigned alexcrichton from PR #13225 Fix souper harvest.

Wasmtime GitHub notifications bot (Apr 29 2026 at 13:05):

alexcrichton requested fitzgen for a review on PR #13225.

Wasmtime GitHub notifications bot (Apr 30 2026 at 02:08):

:memo: bongjunj submitted PR review.

Wasmtime GitHub notifications bot (Apr 30 2026 at 02:08):

:speech_balloon: bongjunj created PR review comment:

Oh, haven't considered this approach, and I agree this would make this PR much simpler...
In addition, having the bitwidth semantics aligned (or i8 vs or i1) is a huge plus!

Imagine that or is being used by other instructions, then the i1 type of the or would affect the user instructions. And this effect would be descended further on and on. Restoring the type of the comparison immediately with zext will rule out this scenario.

I will come back once I complete implementing your approach. Thanks for the insight!

Wasmtime GitHub notifications bot (May 01 2026 at 05:30):

bongjunj updated PR #13225.

Wasmtime GitHub notifications bot (May 01 2026 at 06:04):

bongjunj commented on PR #13225:

Change the implementation.

• Now it zero-extends the icmp result immediately, instead of keeping i1 results down the instruction sequence.
• Fixed a bug where ule was mistranslated to sle.

One thing to keep in mind:
souper now inserts freeze instruction at the end. However, the insertion is proven not necessary: https://alive2.llvm.org/ce/z/2B5qiB

souper-check --infer-rhs -souper-enumerative-synthesis-max-instructions=3
%0:i32 = var
%1:i32 = var
%2:i1 = ult %0, %1
%4:i1 = eq %0, %1
%5:i1 = or %2, %4
infer %5
; RHS inferred successfully
%5:i1 = ule %0, %1
result %5

souper-check --infer-rhs -souper-enumerative-synthesis-max-instructions=3
%0:i32 = var
%1:i32 = var
%2:i1 = ult %0, %1
%3:i8 = zext %2
%4:i1 = eq %0, %1
%5:i8 = zext %4
%6:i8 = or %3, %5
infer %6
; RHS inferred successfully
%7:i1 = ule %0, %1
%8:i8 = zext %7
%9:i8 = freeze %8
result %9

Wasmtime GitHub notifications bot (May 01 2026 at 06:04):

bongjunj edited a comment on PR #13225:

@fitzgen Change the implementation.

• Now it zero-extends the icmp result immediately, instead of keeping i1 results down the instruction sequence.
• Fixed a bug where ule was mistranslated to sle.

One thing to keep in mind:
souper now inserts freeze instruction at the end. However, the insertion is proven not necessary: https://alive2.llvm.org/ce/z/2B5qiB

souper-check --infer-rhs -souper-enumerative-synthesis-max-instructions=3
%0:i32 = var
%1:i32 = var
%2:i1 = ult %0, %1
%4:i1 = eq %0, %1
%5:i1 = or %2, %4
infer %5
; RHS inferred successfully
%5:i1 = ule %0, %1
result %5

souper-check --infer-rhs -souper-enumerative-synthesis-max-instructions=3
%0:i32 = var
%1:i32 = var
%2:i1 = ult %0, %1
%3:i8 = zext %2
%4:i1 = eq %0, %1
%5:i8 = zext %4
%6:i8 = or %3, %5
infer %6
; RHS inferred successfully
%7:i1 = ule %0, %1
%8:i8 = zext %7
%9:i8 = freeze %8
result %9

Wasmtime GitHub notifications bot (May 01 2026 at 18:27):

:thumbs_up: fitzgen submitted PR review:

Awesome, thanks!

Wasmtime GitHub notifications bot (May 01 2026 at 18:27):

fitzgen added PR #13225 Fix souper harvest to the merge queue.

Wasmtime GitHub notifications bot (May 01 2026 at 18:53):

:check: fitzgen merged PR #13225.

Wasmtime GitHub notifications bot (May 01 2026 at 18:53):

fitzgen removed PR #13225 Fix souper harvest from the merge queue.

Last updated: May 03 2026 at 22:13 UTC