SMT2 backend truncates shift distance when it is wider than the shifted operand

[kroening]

Summary

The SMT2 backend (smt2_convt::convert_expr, shift handling in
src/solvers/smt2/smt2_conv.cpp) mis-encodes a bit-vector shift (ID_lshr,
ID_ashr, ID_shl) when the shift distance operand is wider than the
value being shifted. In that case it emits an (_ extract (width_op0-1) 0)
that truncates the distance down to the width of the shifted operand. This
discards the high bits of the distance and produces an incorrect result; a
distance that should shift the operand fully out instead becomes a smaller (or
zero) distance.

The SAT/boolbv backend handles the same expression correctly, so the two
backends disagree.

Location

src/solvers/smt2/smt2_conv.cpp, in the ID_ashr || ID_lshr || ID_shl branch
of convert_expr:

std::size_t width_op0 = boolbv_width(shift_expr.op().type());
std::size_t width_op1 = boolbv_width(distance_type);

if(width_op0==width_op1)
  convert_expr(shift_expr.distance());
else if(width_op0>width_op1)
{
  out << "((_ zero_extend " << width_op0-width_op1 << ") ";
  convert_expr(shift_expr.distance());
  out << ")"; // zero_extend
}
else // width_op0<width_op1
{
  out << "((_ extract " << width_op0-1 << " 0) ";   // <-- BUG: truncates distance
  convert_expr(shift_expr.distance());
  out << ")"; // extract
}

When width_op1 > width_op0, truncating the distance via extract is
unsound: high bits of the distance that are set would mean the shift distance
is >= the operand width, which must shift the operand entirely out (result 0
for bvlshr/bvshl, all sign bits for bvashr). Truncation drops exactly
those bits.

Reproducer

An 8-bit value shifted by a 16-bit distance of 256:

• 0xff >> 256 must be 0 (distance 256 >= operand width 8).
• The SMT backend emits (bvlshr a ((_ extract 7 0) b)). With b = 0x0100,
  (extract 7 0) yields 0x00, so it computes 0xff >> 0 = 0xff.

A reduced SMT2 snippet showing the generated (wrong) encoding:

; a = 0xff (8-bit), b = 256 (16-bit), c should be 0
(define-fun c () (_ BitVec 8)
  (bvlshr #xff ((_ extract 7 0) #x0100)))  ; evaluates to #xff, should be #x00

The SAT (boolbv) backend computes the correct 0.

Suggested fix

When width_op1 > width_op0, do not truncate. Instead perform the shift in a
width wide enough to hold the distance (e.g. zero-extend the shifted operand to
width_op1, shift, then extract the low width_op0 bits), or guard the result
so that a distance >= width_op0 yields the fully-shifted-out value. The
boolbv implementation (bv_utils.shift) can serve as the reference
semantics.

Context

Found via EBMC (diffblue/hw-cbmc): a SystemVerilog compound assignment
a >>= b with reg [7:0] a; reg [15:0] b = 256; is PROVED by the SAT backend
but REFUTED by z3/cvc5 because of this truncation. The affected hw-cbmc
regression test is marked broken-smt-backend pending this fix.