Configure bits_per_byte in byte_extract/byte_update expression

jbmc/unit/java_bytecode/java_trace_validation/java_trace_validation.cpp

@@ -6,17 +6,18 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
+#include <util/byte_operators.h>
+#include <util/pointer_expr.h>
+#include <util/symbol_table.h>
+
 #include <goto-programs/goto_trace.h>
 
 #include <java_bytecode/java_trace_validation.h>
 #include <java_bytecode/java_types.h>
-
 #include <testing-utils/message.h>
 #include <testing-utils/use_catch.h>
 
-#include <util/byte_operators.h>
-#include <util/pointer_expr.h>
-#include <util/symbol_table.h>
+#include <climits>
 
 TEST_CASE("java trace validation", "[core][java_trace_validation]")
 {
@@ -36,9 +37,9 @@ TEST_CASE("java trace validation", "[core][java_trace_validation]")
   const index_exprt index_plain =
     index_exprt(exprt(ID_nil, array_typet(typet(), nil_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

@@ -161,7 +161,7 @@ void rw_range_sett::get_objects_byte_extract(
   }
   else
   {
-    *index *= 8;
+    *index *= be.get_bits_per_byte();
     if(*index >= *object_size_bits_opt)
       return;
 

src/goto-symex/symex_assign.cpp

@@ -383,7 +383,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;
@@ -83,6 +84,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);
@@ -104,11 +106,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?
@@ -119,7 +119,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())
     {
@@ -136,7 +136,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())
@@ -159,7 +159,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)
     {