Support for the extract bits operator over a non-constant range is not implemented in the incremental smt2 decision procedure

[thomasspriggs]

Support for the extract bits operator over a non-constant range is not implemented in the incremental smt2 decision procedure. This is extractbits_exprt when it arrives at the decision procedure. Support is implemented where the operands for the upper and lower bands are constant. Support where they are non-constant is less straight forward to implement because the SMT bitvector theory only supports extraction using constant ranges.

There is a workaround for this SMT limitation which could be implemented. The extractbits_exprt expression given has a bit vector type where the width of the bit vector is constant. Therefore we can use logical_shift_right / bvlshr to shift the bits of interest such that the first bit of interest is the least significant bit and then apply the extract operator from the lowest bit to the expected width of the result.

The regression tests which are affected by this issue include -

• cbmc/array_constraints1/test.desc
• cbmc/aws-byte-buf-regression/test.desc
• cbmc/byte_update16/big-endian.desc
• cbmc/byte_update16/little-endian.desc
• cbmc/Pointer28/test.desc
• cbmc/simplify-array-size/test.desc