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.
super cool to see this catching real bugs we've had!
Last updated: Dec 23 2024 at 12:05 UTC