Fix souper harvest

[bongjunj]

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.

[fitzgen]

Thanks @bongjunj! One question below.

[fitzgen]

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.

[bongjunj]

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!

[bongjunj]

@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

[fitzgen]

Awesome, thanks!