Configure bits_per_byte in byte_extract/byte_update expression

Semantically evaluating a byte_extract/byte_update expression requires
knowledge of the number of bits that a byte is composed of. This,
however, is a configuration parameter known to the front-end that
created the expression in the first place. The back-end should not need
to consult configuration information to evaluate the expression.

Author: tautschnig

jbmc/unit/java_bytecode/java_trace_validation/java_trace_validation.cpp

@@ -17,6 +17,8 @@ Author: Diffblue Ltd.
 #include <util/byte_operators.h>
 #include <util/pointer_expr.h>
 
+#include <climits>
+
 TEST_CASE("java trace validation", "[core][java_trace_validation]")
 {
   const exprt plain_expr = exprt();
@@ -33,9 +35,9 @@ TEST_CASE("java trace validation", "[core][java_trace_validation]")
     index_exprt(valid_symbol_expr, valid_constant);
   const index_exprt index_plain = index_exprt(exprt(), exprt());
   const byte_extract_exprt byte_little_endian = byte_extract_exprt(
-    ID_byte_extract_little_endian, exprt(), exprt(), typet());
-  const byte_extract_exprt byte_big_endian =
-    byte_extract_exprt(ID_byte_extract_big_endian, exprt(), exprt(), typet());
+    ID_byte_extract_little_endian, exprt(), exprt(), CHAR_BIT, typet());
+  const byte_extract_exprt byte_big_endian = byte_extract_exprt(
+    ID_byte_extract_big_endian, exprt(), exprt(), CHAR_BIT, typet());
   const address_of_exprt valid_address = address_of_exprt(valid_symbol_expr);
   const address_of_exprt invalid_address = address_of_exprt(exprt());
   const struct_exprt struct_plain =

src/analyses/goto_rw.cpp

@@ -154,7 +154,7 @@ void rw_range_sett::get_objects_byte_extract(
     get_objects_rec(mode, be.op(), -1, size);
   else
   {
-    *index *= 8;
+    *index *= be.get_bits_per_byte();
     if(*index >= *pointer_offset_bits(be.op().type(), ns))
       return;
 

src/goto-symex/symex_assign.cpp

@@ -378,7 +378,8 @@ void symex_assignt::assign_byte_extract(
   else
     UNREACHABLE;
 
-  const byte_update_exprt new_rhs{byte_update_id, lhs.op(), lhs.offset(), rhs};
+  const byte_update_exprt new_rhs{
+    byte_update_id, lhs.op(), lhs.offset(), rhs, lhs.get_bits_per_byte()};
   const expr_skeletont new_skeleton =
     full_lhs.compose(expr_skeletont::remove_op0(lhs));
   assign_rec(lhs.op(), new_skeleton, new_rhs, guard);

src/solvers/flattening/boolbv_byte_extract.cpp

@@ -48,11 +48,12 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
   #if 0
   if(expr.id()==ID_byte_extract_big_endian &&
      expr.type().id()==ID_c_bit_field &&
-     (width%8)!=0)
+     (width%expr.get_bits_per_byte())!=0)
   {
     byte_extract_exprt tmp=expr;
     // round up
-    to_c_bit_field_type(tmp.type()).set_width(width+8-width%8);
+    to_c_bit_field_type(tmp.type()).set_width(
+      width+expr.get_bits_per_byte()-width%expr.get_bits_per_byte());
     convert_byte_extract(tmp, bv);
     bv.resize(width); // chop down
     return;
@@ -86,6 +87,7 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
       expr.id(),
       o.root_object(),
       plus_exprt(o.offset(), expr.offset()),
+      expr.get_bits_per_byte(),
       expr.type());
 
     return convert_bv(be);
@@ -107,11 +109,9 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
   bv.resize(width);
 
   // see if the byte number is constant
-  unsigned byte_width=8;
-
   if(index.has_value())
   {
-    const mp_integer offset = *index * byte_width;
+    const mp_integer offset = *index * expr.get_bits_per_byte();
 
     for(std::size_t i=0; i<width; i++)
       // out of bounds?
@@ -122,7 +122,7 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
   }
   else
   {
-    std::size_t bytes=op_bv.size()/byte_width;
+    std::size_t bytes = op_bv.size() / expr.get_bits_per_byte();
 
     if(prop.has_set_to())
     {
@@ -139,7 +139,7 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
 
       for(std::size_t i=0; i<bytes; i++)
       {
-        std::size_t offset=i*byte_width;
+        std::size_t offset = i * expr.get_bits_per_byte();
 
         for(std::size_t j=0; j<width; j++)
           if(offset+j<op_bv.size())
@@ -162,7 +162,7 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
         literalt e =
           convert(equal_exprt(expr.offset(), from_integer(i, constant_type)));
 
-        std::size_t offset=i*byte_width;
+        std::size_t offset = i * expr.get_bits_per_byte();
 
         for(std::size_t j=0; j<width; j++)
         {

src/solvers/flattening/boolbv_byte_update.cpp

@@ -38,7 +38,7 @@ bvt boolbvt::convert_byte_update(const byte_update_exprt &expr)
 
   const bvt &value_bv=convert_bv(value);
   std::size_t update_width=value_bv.size();
-  std::size_t byte_width=8;
+  std::size_t byte_width = expr.get_bits_per_byte();
 
   if(update_width>bv.size())
     update_width=bv.size();
@@ -49,7 +49,7 @@ bvt boolbvt::convert_byte_update(const byte_update_exprt &expr)
   if(index.has_value())
   {
     // yes!
-    const mp_integer offset = *index * 8;
+    const mp_integer offset = *index * byte_width;
 
     if(offset+update_width>mp_integer(bv.size()) || offset<0)
     {