Stream: cranelift

Topic: ISLE verification found previously reported bug

Monica Pardeshi (Jan 11 2023 at 20:37):

We've updated the verification engine to verify several more instructions now, including clz and cls. Interestingly enough, we were able to catch a cls bug that was reported previously(!) We've reproduced the bug here.

Here are the relevant parts of a counterexample from the solver.
Suppose we start with x = 0xc0:

(
    "x__clif0__2", <-- x on the lhs (clif) side is 0xc0
    [],
    "(_ BitVec 8)",
    "#xc0",
),

This is also the arg to cls:

(
    "cls__5__a__17", <-- arg to cls is 0xc0
    [],
    "(_ BitVec 8)",
    "#xc0",
),

The solver concludes that cls(0xc0: bv8) should be 1:

(
    "cls8ret_18", <-- cls returns 1 because 0xc0 has two leading 1s
    [],
    "(_ BitVec 8)",
    "#x01",
),

On the rhs we have that the input to aarch64 cls is 0xc0 extended to 32 bits, plus an extra 32 unconstrained bits (these get ignored):

(
    "a64_cls__11__a__45", <-- input to rhs (a64) cls is 0xc0 extended to 64 bits
    [],
    "(_ BitVec 64)",
    "#x40000000000000c0",
),

Since the buggy rule zero extends instead of sign extending, the solver concludes that a64cls(0x000000c0: bv32) = 23:

(
    "a64cls32ret_46",
    [],
    "(_ BitVec 64)",
    "#x0000000000000017",
),

If the input had been sign extended, the result would have been 25. In this counterexample, when the solver subtracts the result is -1:

(
    "sub_imm__14__ret__64", <-- results in -1
    [],
    "(_ BitVec 64)",
    "#xffffffffffffffff",
),

But the result from the lhs is 1, so verification fails.

fitzgen (he/him) (Jan 11 2023 at 21:04):

super cool to see this catching real bugs we've had!

Last updated: Oct 23 2024 at 20:03 UTC