Merge pull request #917 from tautschnig/byte-config

Do not hardcode char/bytes having 8 bits

Author: tautschnig

src/cprover/cprover_parse_options.cpp

@@ -308,11 +308,9 @@ void cprover_parse_optionst::help()
 {
   std::cout << '\n';
 
-  std::cout
-    << u8"* * CPROVER " << CBMC_VERSION << " (" << (sizeof(void *) * 8)
-    << "-bit)"
-    << " * *\n"
-    << "* *                       Copyright 2022                       * *\n";
+  std::cout << '\n'
+            << banner_string("CPROVER", CBMC_VERSION) << '\n'
+            << align_center_with_border("Copyright 2022") << '\n';
 
   // clang-format off
   std::cout << help_formatter(

src/goto-instrument/contracts/memory_predicates.cpp

@@ -137,7 +137,7 @@ void is_fresh_baset::update_ensures(goto_programt &ensures)
 
 array_typet is_fresh_baset::get_memmap_type()
 {
-  return array_typet(c_bool_typet(8), infinity_exprt(size_type()));
+  return array_typet(unsigned_char_type(), infinity_exprt(size_type()));
 }
 
 void is_fresh_baset::add_memory_map_decl(goto_programt &program)
@@ -149,7 +149,8 @@ void is_fresh_baset::add_memory_map_decl(goto_programt &program)
     goto_programt::make_decl(memmap_symbol.symbol_expr(), source_location));
   program.add(goto_programt::make_assignment(
     memmap_symbol.symbol_expr(),
-    array_of_exprt(from_integer(0, c_bool_typet(8)), get_memmap_type()),
+    array_of_exprt(
+      from_integer(0, get_memmap_type().element_type()), get_memmap_type()),
     source_location));
 }
 

src/goto-instrument/stack_depth.cpp

@@ -15,6 +15,7 @@ Date: November 2011
 
 #include <util/arith_tools.h>
 #include <util/bitvector_types.h>
+#include <util/c_types.h>
 
 #include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/goto_model.h>
@@ -26,7 +27,7 @@ static symbol_exprt add_stack_depth_symbol(
   message_handlert &message_handler)
 {
   const irep_idt identifier="$stack_depth";
-  unsignedbv_typet type(sizeof(std::size_t)*8);
+  typet type = size_type();
 
   symbolt new_symbol;
   new_symbol.name=identifier;

src/goto-instrument/synthesizer/expr_enumerator.cpp

@@ -8,6 +8,8 @@ Author: Qinheping Hu
 #include <util/format_expr.h>
 #include <util/simplify_expr.h>
 
+#include <climits>
+
 expr_sett leaf_enumeratort::enumerate(const std::size_t size) const
 {
   // Size of leaf expressions must be 1.
@@ -185,7 +187,7 @@ get_partitions_long(const std::size_t n, const std::size_t k)
 /// Compute all positions of ones in the bit vector `v` (1-indexed).
 std::vector<std::size_t> get_ones_pos(std::size_t v)
 {
-  const std::size_t length = sizeof(std::size_t) * 8;
+  const std::size_t length = sizeof(std::size_t) * CHAR_BIT;
   std::vector<std::size_t> result;
 
   // Start from the lowest bit at position `length`
@@ -236,7 +238,7 @@ std::list<partitiont> non_leaf_enumeratort::get_partitions(
     return {};
 
   // Number of bits at all.
-  const std::size_t length = sizeof(std::size_t) * 8;
+  const std::size_t length = sizeof(std::size_t) * CHAR_BIT;
 
   // This bithack-based implementation works only for `n` no larger than
   // `length`. Use the vector-based implementation `n` is too large.

src/goto-programs/goto_trace.cpp

@@ -13,11 +13,10 @@ Author: Daniel Kroening
 
 #include "goto_trace.h"
 
-#include <ostream>
-
 #include <util/arith_tools.h>
 #include <util/byte_operators.h>
 #include <util/c_types.h>
+#include <util/config.h>
 #include <util/format_expr.h>
 #include <util/merge_irep.h>
 #include <util/range.h>
@@ -28,6 +27,8 @@ Author: Daniel Kroening
 
 #include "printf_formatter.h"
 
+#include <ostream>
+
 static optionalt<symbol_exprt> get_object_rec(const exprt &src)
 {
   if(src.id()==ID_symbol)
@@ -195,7 +196,7 @@ static std::string numeric_representation(
   for(const auto c : result)
   {
     oss << c;
-    if(++i % 8 == 0 && result.size() != i)
+    if(++i % config.ansi_c.char_width == 0 && result.size() != i)
       oss << ' ';
   }
   if(options.base_prefix)

src/util/pointer_offset_size.cpp

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 #include "arith_tools.h"
 #include "byte_operators.h"
 #include "c_types.h"
+#include "config.h"
 #include "invariant.h"
 #include "namespace.h"
 #include "pointer_expr.h"
@@ -38,14 +39,14 @@ optionalt<mp_integer> member_offset(
     {
       const std::size_t w = to_c_bit_field_type(comp.type()).get_width();
       bit_field_bits += w;
-      result += bit_field_bits / 8;
-      bit_field_bits %= 8;
+      result += bit_field_bits / config.ansi_c.char_width;
+      bit_field_bits %= config.ansi_c.char_width;
     }
     else if(comp.type().id() == ID_bool)
     {
       ++bit_field_bits;
-      result += bit_field_bits / 8;
-      bit_field_bits %= 8;
+      result += bit_field_bits / config.ansi_c.char_width;
+      bit_field_bits %= config.ansi_c.char_width;
     }
     else
     {
@@ -92,7 +93,7 @@ pointer_offset_size(const typet &type, const namespacet &ns)
   auto bits = pointer_offset_bits(type, ns);
 
   if(bits.has_value())
-    return (*bits + 7) / 8;
+    return (*bits + config.ansi_c.char_width - 1) / config.ansi_c.char_width;
   else
     return {};
 }
@@ -249,16 +250,16 @@ optionalt<exprt> member_offset_expr(
     {
       std::size_t w = to_c_bit_field_type(c.type()).get_width();
       bit_field_bits += w;
-      const std::size_t bytes = bit_field_bits / 8;
-      bit_field_bits %= 8;
+      const std::size_t bytes = bit_field_bits / config.ansi_c.char_width;
+      bit_field_bits %= config.ansi_c.char_width;
       if(bytes > 0)
         result = plus_exprt(result, from_integer(bytes, result.type()));
     }
     else if(c.type().id() == ID_bool)
     {
       ++bit_field_bits;
-      const std::size_t bytes = bit_field_bits / 8;
-      bit_field_bits %= 8;
+      const std::size_t bytes = bit_field_bits / config.ansi_c.char_width;
+      bit_field_bits %= config.ansi_c.char_width;
       if(bytes > 0)
         result = plus_exprt(result, from_integer(bytes, result.type()));
     }
@@ -289,7 +290,9 @@ optionalt<exprt> size_of_expr(const typet &type, const namespacet &ns)
       auto bits = pointer_offset_bits(array_type, ns);
 
       if(bits.has_value())
-        return from_integer((*bits + 7) / 8, size_type());
+        return from_integer(
+          (*bits + config.ansi_c.char_width - 1) / config.ansi_c.char_width,
+          size_type());
     }
 
     auto sub = size_of_expr(array_type.element_type(), ns);
@@ -316,7 +319,9 @@ optionalt<exprt> size_of_expr(const typet &type, const namespacet &ns)
       auto bits = pointer_offset_bits(vector_type, ns);
 
       if(bits.has_value())
-        return from_integer((*bits + 7) / 8, size_type());
+        return from_integer(
+          (*bits + config.ansi_c.char_width - 1) / config.ansi_c.char_width,
+          size_type());
     }
 
     auto sub = size_of_expr(vector_type.element_type(), ns);
@@ -355,16 +360,16 @@ optionalt<exprt> size_of_expr(const typet &type, const namespacet &ns)
       {
         std::size_t w = to_c_bit_field_type(c.type()).get_width();
         bit_field_bits += w;
-        const std::size_t bytes = bit_field_bits / 8;
-        bit_field_bits %= 8;
+        const std::size_t bytes = bit_field_bits / config.ansi_c.char_width;
+        bit_field_bits %= config.ansi_c.char_width;
         if(bytes > 0)
           result = plus_exprt(result, from_integer(bytes, result.type()));
       }
       else if(c.type().id() == ID_bool)
       {
         ++bit_field_bits;
-        const std::size_t bytes = bit_field_bits / 8;
-        bit_field_bits %= 8;
+        const std::size_t bytes = bit_field_bits / config.ansi_c.char_width;
+        bit_field_bits %= config.ansi_c.char_width;
         if(bytes > 0)
           result = plus_exprt(result, from_integer(bytes, result.type()));
       }
@@ -415,7 +420,8 @@ optionalt<exprt> size_of_expr(const typet &type, const namespacet &ns)
       }
       else
       {
-        mp_integer sub_bytes = (*sub_bits + 7) / 8;
+        mp_integer sub_bytes =
+          (*sub_bits + config.ansi_c.char_width - 1) / config.ansi_c.char_width;
 
         if(max_bytes>=0)
         {
@@ -449,19 +455,14 @@ optionalt<exprt> size_of_expr(const typet &type, const namespacet &ns)
           type.id()==ID_c_bit_field)
   {
     std::size_t width=to_bitvector_type(type).get_width();
-    std::size_t bytes=width/8;
-    if(bytes*8!=width)
+    std::size_t bytes = width / config.ansi_c.char_width;
+    if(bytes * config.ansi_c.char_width != width)
       bytes++;
     return from_integer(bytes, size_type());
   }
   else if(type.id()==ID_c_enum)
   {
-    std::size_t width =
-      to_bitvector_type(to_c_enum_type(type).underlying_type()).get_width();
-    std::size_t bytes=width/8;
-    if(bytes*8!=width)
-      bytes++;
-    return from_integer(bytes, size_type());
+    return size_of_expr(to_c_enum_type(type).underlying_type(), ns);
   }
   else if(type.id()==ID_c_enum_tag)
   {
@@ -475,11 +476,11 @@ optionalt<exprt> size_of_expr(const typet &type, const namespacet &ns)
   {
     // the following is an MS extension
     if(type.get_bool(ID_C_ptr32))
-      return from_integer(4, size_type());
+      return from_integer(32 / config.ansi_c.char_width, size_type());
 
     std::size_t width=to_bitvector_type(type).get_width();
-    std::size_t bytes=width/8;
-    if(bytes*8!=width)
+    std::size_t bytes = width / config.ansi_c.char_width;
+    if(bytes * config.ansi_c.char_width != width)
       bytes++;
     return from_integer(bytes, size_type());
   }
@@ -497,7 +498,7 @@ optionalt<exprt> size_of_expr(const typet &type, const namespacet &ns)
   }
   else if(type.id()==ID_string)
   {
-    return from_integer(32/8, size_type());
+    return from_integer(32 / config.ansi_c.char_width, size_type());
   }
   else
     return {};
@@ -607,12 +608,17 @@ optionalt<exprt> get_subexpression_at_offset(
       // if this member completely contains the target, and this member is
       // byte-aligned, recurse into it
       if(
-        offset_bytes * 8 >= m_offset_bits && m_offset_bits % 8 == 0 &&
-        offset_bytes * 8 + *target_size_bits <= m_offset_bits + *m_size_bits)
+        offset_bytes * config.ansi_c.char_width >= m_offset_bits &&
+        m_offset_bits % config.ansi_c.char_width == 0 &&
+        offset_bytes * config.ansi_c.char_width + *target_size_bits <=
+          m_offset_bits + *m_size_bits)
       {
         const member_exprt member(expr, component.get_name(), component.type());
         return get_subexpression_at_offset(
-          member, offset_bytes - m_offset_bits / 8, target_type_raw, ns);
+          member,
+          offset_bytes - m_offset_bits / config.ansi_c.char_width,
+          target_type_raw,
+          ns);
       }
 
       m_offset_bits += *m_size_bits;
@@ -628,11 +634,14 @@ optionalt<exprt> get_subexpression_at_offset(
     // no arrays of non-byte-aligned, zero-, or unknown-sized objects
     if(
       elem_size_bits.has_value() && *elem_size_bits > 0 &&
-      *elem_size_bits % 8 == 0 && *target_size_bits <= *elem_size_bits)
+      *elem_size_bits % config.ansi_c.char_width == 0 &&
+      *target_size_bits <= *elem_size_bits)
     {
-      const mp_integer elem_size_bytes = *elem_size_bits / 8;
+      const mp_integer elem_size_bytes =
+        *elem_size_bits / config.ansi_c.char_width;
       const auto offset_inside_elem = offset_bytes % elem_size_bytes;
-      const auto target_size_bytes = *target_size_bits / 8;
+      const auto target_size_bytes =
+        *target_size_bits / config.ansi_c.char_width;
       // only recurse if the cell completely contains the target
       if(offset_inside_elem + target_size_bytes <= elem_size_bytes)
       {
@@ -660,7 +669,9 @@ optionalt<exprt> get_subexpression_at_offset(
         continue;
 
       // if this member completely contains the target, recurse into it
-      if(offset_bytes * 8 + *target_size_bits <= *m_size_bits)
+      if(
+        offset_bytes * config.ansi_c.char_width + *target_size_bits <=
+        *m_size_bits)
       {
         const member_exprt member(expr, component.get_name(), component.type());
         return get_subexpression_at_offset(

src/util/simplify_expr.cpp

@@ -821,6 +821,8 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
   }
 
   // circular casts through types shorter than `int`
+  // we use fixed bit widths as this is specifically for the Java bytecode
+  // front-end
   if(op_type == signedbv_typet(32) && expr.op().id() == ID_typecast)
   {
     if(expr_type==c_bool_typet(8) ||
@@ -1817,7 +1819,7 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr)
         // the next member would be misaligned, abort
         if(
           !component_bits.has_value() || *component_bits == 0 ||
-          *component_bits % 8 != 0)
+          *component_bits % expr.get_bits_per_byte() != 0)
         {
           failed = true;
           break;
@@ -1868,10 +1870,12 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr)
       pointer_offset_bits(array_type.element_type(), ns);
     if(element_bit_width.has_value() && *element_bit_width > 0)
     {
-      if(*offset > 0 && *offset * 8 % *element_bit_width == 0)
+      if(
+        *offset > 0 &&
+        *offset * expr.get_bits_per_byte() % *element_bit_width == 0)
       {
-        const auto elements_to_erase =
-          numeric_cast_v<std::size_t>((*offset * 8) / *element_bit_width);
+        const auto elements_to_erase = numeric_cast_v<std::size_t>(
+          (*offset * expr.get_bits_per_byte()) / *element_bit_width);
         array_exprt slice = to_array_expr(expr.op());
         slice.operands().erase(
           slice.operands().begin(),
@@ -1953,7 +1957,7 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
   if(
     root_size.has_value() && *root_size >= 0 && val_size.has_value() &&
     *val_size >= 0 && offset_int.has_value() && *offset_int >= 0 &&
-    *offset_int * 8 + *val_size <= *root_size)
+    *offset_int * expr.get_bits_per_byte() + *val_size <= *root_size)
   {
     auto root_bits =
       expr2bits(root, expr.id() == ID_byte_update_little_endian, ns);

src/util/simplify_expr_struct.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 #include "arith_tools.h"
 #include "byte_operators.h"
 #include "c_types.h"
+#include "config.h"
 #include "invariant.h"
 #include "namespace.h"
 #include "pointer_offset_size.h"
@@ -185,7 +186,7 @@ simplify_exprt::simplify_member(const member_exprt &expr)
 
     if(target_size.has_value())
     {
-      mp_integer target_bits = target_size.value() * 8;
+      mp_integer target_bits = target_size.value() * config.ansi_c.char_width;
       const auto bits = expr2bits(op, true, ns);
 
       if(bits.has_value() &&