Do not hardcode char/bytes having 8 bits

The C standard does not guarantee that char is exactly 8 bits, and there are
DSPs (such Texas Instruments C55x) that do not have 8-bit-bytes. Use the
configuration value instead.

Author: tautschnig

src/analyses/goto_rw.cpp

@@ -11,6 +11,7 @@ Date: April 2010
 #include <limits>
 #include <algorithm>
 
+#include <util/config.h>
 #include <util/std_code.h>
 #include <util/std_expr.h>
 #include <util/pointer_offset_size.h>
@@ -235,7 +236,7 @@ void rw_range_sett::get_objects_byte_extract(
     get_objects_rec(mode, be.op(), -1, size);
   else
   {
-    index*=8;
+    index*=config.ansi_c.char_width;
     if(index>=pointer_offset_bits(be.op().type(), ns))
       return;
 

src/analyses/invariant_set.cpp

@@ -556,6 +556,7 @@ void invariant_sett::add_type_bounds(const exprt &expr, const typet &type)
   {
     unsigned op_width=to_unsignedbv_type(type).get_width();
 
+    // TODO - 8 appears to be a magic number here
     if(op_width<=8)
     {
       unsigned a;

src/ansi-c/ansi_c_entry_point.cpp

@@ -299,6 +299,8 @@ bool ansi_c_entry_point(
       }
 
       {
+        // TODO I have no idea what MAX refers to, or how the
+        // int_width-4 relates to it
         // assume argc is at most MAX/8-1
         mp_integer upper_bound=
           power(2, config.ansi_c.int_width-4);

src/ansi-c/padding.cpp

@@ -29,6 +29,8 @@ Function: alignment
 
 mp_integer alignment(const typet &type, const namespacet &ns)
 {
+  const unsigned bits=config.ansi_c.char_width;
+
   // we need to consider a number of different cases:
   // - alignment specified in the source, which will be recorded in
   // ID_C_alignment
@@ -85,7 +87,7 @@ mp_integer alignment(const typet &type, const namespacet &ns)
           type.id()==ID_c_bool)
   {
     std::size_t width=to_bitvector_type(type).get_width();
-    result=width%8?width/8+1:width/8;
+    result=width%bits?width/bits+1:width/bits;
   }
   else if(type.id()==ID_c_enum)
     result=alignment(type.subtype(), ns);
@@ -94,7 +96,7 @@ mp_integer alignment(const typet &type, const namespacet &ns)
   else if(type.id()==ID_pointer)
   {
     std::size_t width=config.ansi_c.pointer_width;
-    result=width%8?width/8+1:width/8;
+    result=width%bits?width/bits+1:width/bits;
   }
   else if(type.id()==ID_symbol)
     result=alignment(ns.follow(type), ns);
@@ -152,9 +154,10 @@ void add_padding(struct_typet &type, const namespacet &ns)
       else if(bit_field_bits!=0)
       {
         // not on a byte-boundary?
-        if((bit_field_bits%8)!=0)
+        if((bit_field_bits%config.ansi_c.char_width)!=0)
         {
-          std::size_t pad=8-bit_field_bits%8;
+          std::size_t pad=
+            config.ansi_c.char_width-bit_field_bits%config.ansi_c.char_width;
           c_bit_field_typet padding_type(unsignedbv_typet(pad), pad);
 
           struct_typet::componentt component;
@@ -174,9 +177,10 @@ void add_padding(struct_typet &type, const namespacet &ns)
     }
 
     // Add padding at the end?
-    if((bit_field_bits%8)!=0)
+    if((bit_field_bits%config.ansi_c.char_width)!=0)
     {
-      std::size_t pad=8-bit_field_bits%8;
+      std::size_t pad=
+        config.ansi_c.char_width-bit_field_bits%config.ansi_c.char_width;
       c_bit_field_typet padding_type(unsignedbv_typet(pad), pad);
 
       struct_typet::componentt component;
@@ -225,8 +229,12 @@ void add_padding(struct_typet &type, const namespacet &ns)
           max_alignment=a;
 
         std::size_t w=to_c_bit_field_type(it_type).get_width();
-        std::size_t bytes;
-        for(bytes=0; w>bit_field_bits; ++bytes, bit_field_bits+=8) {}
+        std::size_t bytes=0;
+        while(w>bit_field_bits)
+        {
+          ++bytes;
+          bit_field_bits+=config.ansi_c.char_width;
+        }
         bit_field_bits-=w;
         offset+=bytes;
         continue;
@@ -252,7 +260,7 @@ void add_padding(struct_typet &type, const namespacet &ns)
         mp_integer pad=a-displacement;
 
         unsignedbv_typet padding_type;
-        padding_type.set_width(integer2unsigned(pad*8));
+        padding_type.set_width(integer2unsigned(pad*config.ansi_c.char_width));
 
         struct_typet::componentt component;
         component.type()=padding_type;
@@ -274,8 +282,8 @@ void add_padding(struct_typet &type, const namespacet &ns)
 
   if(bit_field_bits!=0)
   {
-    // these are now assumed to be multiples of 8
-    offset+=bit_field_bits/8;
+    // these are now assumed to be multiples of bytes
+    offset+=bit_field_bits/config.ansi_c.char_width;
   }
 
   // any explicit alignment for the struct?
@@ -309,7 +317,7 @@ void add_padding(struct_typet &type, const namespacet &ns)
       mp_integer pad=max_alignment-displacement;
 
       unsignedbv_typet padding_type;
-      padding_type.set_width(integer2unsigned(pad*8));
+      padding_type.set_width(integer2unsigned(pad*config.ansi_c.char_width));
 
       // we insert after any final 'flexible member'
       struct_typet::componentt component;
@@ -336,16 +344,16 @@ Function: add_padding
 
 void add_padding(union_typet &type, const namespacet &ns)
 {
-  mp_integer max_alignment=alignment(type, ns)*8;
+  mp_integer max_alignment=alignment(type, ns)*config.ansi_c.char_width;
   mp_integer size_bits=pointer_offset_bits(type, ns);
 
   union_typet::componentst &components=type.components();
 
   // Is the union packed?
   if(type.get_bool(ID_C_packed))
   {
-    // The size needs to be a multiple of 8 only.
-    max_alignment=8;
+    // The size needs to be a multiple of bytes only.
+    max_alignment=config.ansi_c.char_width;
   }
 
   // The size must be a multiple of the alignment, or

src/goto-instrument/stack_depth.cpp

@@ -14,6 +14,8 @@ Date: November 2011
 #include <util/arith_tools.h>
 #include <util/cprover_prefix.h>
 
+#include <ansi-c/c_types.h>
+
 #include <goto-programs/goto_functions.h>
 
 #include "stack_depth.h"
@@ -33,7 +35,7 @@ Function: add_stack_depth_symbol
 symbol_exprt add_stack_depth_symbol(symbol_tablet &symbol_table)
 {
   const irep_idt identifier="$stack_depth";
-  signedbv_typet type(sizeof(int)*8);
+  typet type=size_type();
 
   symbolt new_symbol;
   new_symbol.name=identifier;

src/goto-programs/vcd_goto_trace.cpp

@@ -82,7 +82,7 @@ std::string as_vcd_binary(
      type.id()==ID_bv)
     width=string2integer(type.get_string(ID_width));
   else
-    width=pointer_offset_size(type, ns)*8;
+    width=pointer_offset_bits(type, ns);
 
   if(width>=0)
     return std::string(integer2size_t(width), 'x');

src/solvers/flattening/boolbv.cpp

@@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <map>
 #include <set>
 
+#include <util/config.h>
 #include <util/symbol.h>
 #include <util/mp_arith.h>
 #include <util/arith_tools.h>
@@ -235,7 +236,10 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
 
     if(expr.type().id()==ID_unsignedbv ||
        expr.type().id()==ID_signedbv)
-      return bv_utils.build_constant(op_width/8, result_width);
+      return
+        bv_utils.build_constant(
+          op_width/config.ansi_c.char_width,
+          result_width);
   }
   else if(expr.id()==ID_case)
     return convert_case(expr);

src/solvers/flattening/boolbv_byte_extract.cpp

@@ -9,6 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <cassert>
 
 #include <util/arith_tools.h>
+#include <util/config.h>
 #include <util/std_expr.h>
 #include <util/byte_operators.h>
 #include <util/endianness_map.h>
@@ -76,11 +77,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%config.ansi_c.char_width)!=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+config.ansi_c.char_width-width%config.ansi_c.char_width);
     convert_byte_extract(tmp, bv);
     bv.resize(width); // chop down
     return;
@@ -116,7 +118,7 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
   bv.resize(width);
 
   // see if the byte number is constant
-  unsigned byte_width=8;
+  unsigned byte_width=config.ansi_c.char_width;
 
   mp_integer index;
   if(!to_integer(offset, index))

src/solvers/flattening/boolbv_byte_update.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/arith_tools.h>
 #include <util/byte_operators.h>
+#include <util/config.h>
 #include <util/endianness_map.h>
 
 #include "boolbv.h"
@@ -49,7 +50,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=config.ansi_c.char_width;
 
   if(update_width>bv.size())
     update_width=bv.size();
@@ -60,7 +61,7 @@ bvt boolbvt::convert_byte_update(const byte_update_exprt &expr)
   if(!to_integer(offset_expr, index))
   {
     // yes!
-    mp_integer offset=index*8;
+    mp_integer offset=index*byte_width;
 
     if(offset+update_width>mp_integer(bv.size()) || offset<0)
     {

src/solvers/flattening/flatten_byte_operators.cpp

@@ -6,6 +6,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
+#include <util/config.h>
 #include <util/expr.h>
 #include <util/std_types.h>
 #include <util/std_expr.h>
@@ -66,7 +67,7 @@ exprt flatten_byte_extract(
     const typet &offset_type=ns.follow(offset.type());
 
     // byte-array?
-    if(element_width==8)
+    if(element_width==config.ansi_c.char_width)
     {
       // get 'width'-many bytes, and concatenate
       std::size_t width_bytes=integer2unsigned(num_elements);
@@ -84,7 +85,8 @@ exprt flatten_byte_extract(
         op.push_back(index_expr);
       }
 
-      // TODO this doesn't seem correct if size_bits%8!=0 as more
+      // TODO this doesn't seem correct if
+      // size_bits%config.ansi_c.char_width!=0 as more
       // bits than the original expression will be returned.
       if(width_bytes==1)
         return op.front();
@@ -107,9 +109,11 @@ exprt flatten_byte_extract(
       concatenation_exprt concat(
         unsignedbv_typet(integer2unsigned(element_width*num_elements)));
 
-      assert(element_width%8==0);
+      assert(element_width%config.ansi_c.char_width==0);
       exprt first_index=
-        div_exprt(offset, from_integer(element_width/8, offset_type));
+        div_exprt(
+          offset,
+          from_integer(element_width/config.ansi_c.char_width, offset_type));
 
       // byte extract will do the appropriate mapping, thus MSB comes
       // last here (as opposed to the above, where no further byte
@@ -125,8 +129,9 @@ exprt flatten_byte_extract(
       }
 
       // the new offset is offset%width
-      mod_exprt new_offset(offset,
-                           from_integer(element_width/8, offset_type));
+      mod_exprt new_offset(
+        offset,
+        from_integer(element_width/config.ansi_c.char_width, offset_type));
 
       // build new byte-extract expression
       byte_extract_exprt tmp(src);
@@ -154,11 +159,14 @@ exprt flatten_byte_extract(
       adjusted_offset=offset;
     else
     {
-      exprt width_constant=from_integer(op0_bits/8-1, offset_type);
+      exprt width_constant=
+        from_integer(op0_bits/config.ansi_c.char_width-1, offset_type);
       adjusted_offset=minus_exprt(width_constant, offset);
     }
 
-    mult_exprt times_eight(adjusted_offset, from_integer(8, offset_type));
+    mult_exprt times_eight(
+      adjusted_offset,
+      from_integer(config.ansi_c.char_width, offset_type));
 
     // cast to generic bit-vector
     std::size_t op0_width=integer2unsigned(op0_bits);
@@ -378,31 +386,37 @@ exprt flatten_byte_update(
           t.id()==ID_pointer)
   {
     // do a shift, mask and OR
-    std::size_t width=integer2size_t(pointer_offset_size(t, ns)*8);
+    std::size_t width=integer2size_t(pointer_offset_bits(t, ns));
 
     assert(width!=0);
 
-    if(element_size*8>width)
+    if(element_size*config.ansi_c.char_width>width)
       throw "flatten_byte_update to update element that is too large";
 
     // build mask
     exprt mask=
-      from_integer(power(2, element_size*8)-1, unsignedbv_typet(width));
+      from_integer(
+        power(2, element_size*config.ansi_c.char_width)-1,
+        unsignedbv_typet(width));
 
     // zero-extend the value, but only if needed
     exprt value_extended;
 
-    if(width>integer2unsigned(element_size)*8)
+    if(width>integer2unsigned(element_size)*config.ansi_c.char_width)
       value_extended=
         concatenation_exprt(
           from_integer(
-            0, unsignedbv_typet(width-integer2unsigned(element_size)*8)),
+            0,
+            unsignedbv_typet(
+              width-integer2unsigned(element_size)*config.ansi_c.char_width)),
           src.op2(), t);
     else
       value_extended=src.op2();
 
     const typet &offset_type=ns.follow(src.op1().type());
-    mult_exprt offset_times_eight(src.op1(), from_integer(8, offset_type));
+    mult_exprt offset_times_eight(
+      src.op1(),
+      from_integer(config.ansi_c.char_width, offset_type));
 
     binary_predicate_exprt offset_ge_zero(
       offset_times_eight,