Do not assume that build architecture has byte/char==8 bits

The C/C++ standard does not guarantee this, and limits.h/climits has the
CHAR_BIT define set properly.

All changes in this commit only refer to the platform the tool is being
built for. The analysis target requires a separate set of changes where
the byte width must be taken from the configuration or annotations
within expressions.

Author: tautschnig

jbmc/src/janalyzer/janalyzer_parse_options.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "janalyzer_parse_options.h"
 
+#include <climits>
 #include <cstdlib> // exit()
 #include <fstream>
 #include <iostream>
@@ -357,8 +358,9 @@ int janalyzer_parse_optionst::doit()
   // Print a banner
   //
   log.status() << "JANALYZER version " << CBMC_VERSION << " "
-               << sizeof(void *) * 8 << "-bit " << config.this_architecture()
-               << " " << config.this_operating_system() << messaget::eom;
+               << sizeof(void *) * CHAR_BIT << "-bit "
+               << config.this_architecture() << " "
+               << config.this_operating_system() << messaget::eom;
 
   register_languages();
 

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -11,8 +11,9 @@ Author: Daniel Kroening, [email protected]
 
 #include "jbmc_parse_options.h"
 
-#include <fstream>
+#include <climits>
 #include <cstdlib> // exit()
+#include <fstream>
 #include <iostream>
 #include <memory>
 
@@ -481,8 +482,9 @@ int jbmc_parse_optionst::doit()
   //
   // Print a banner
   //
-  log.status() << "JBMC version " << CBMC_VERSION << " " << sizeof(void *) * 8
-               << "-bit " << config.this_architecture() << " "
+  log.status() << "JBMC version " << CBMC_VERSION << " "
+               << sizeof(void *) * CHAR_BIT << "-bit "
+               << config.this_architecture() << " "
                << config.this_operating_system() << messaget::eom;
 
   // output the options

jbmc/src/jdiff/jdiff_parse_options.cpp

@@ -11,6 +11,7 @@ Author: Peter Schrammel
 
 #include "jdiff_parse_options.h"
 
+#include <climits>
 #include <cstdlib> // exit()
 #include <fstream>
 #include <iostream>
@@ -194,8 +195,9 @@ int jdiff_parse_optionst::doit()
   //
   // Print a banner
   //
-  log.status() << "JDIFF version " << CBMC_VERSION << " " << sizeof(void *) * 8
-               << "-bit " << config.this_architecture() << " "
+  log.status() << "JDIFF version " << CBMC_VERSION << " "
+               << sizeof(void *) * CHAR_BIT << "-bit "
+               << config.this_architecture() << " "
                << config.this_operating_system() << messaget::eom;
 
   if(cmdline.args.size() != 2)

src/ansi-c/library/gcc.c

@@ -35,6 +35,11 @@ inline void __sync_synchronize(void)
 
 /* FUNCTION: __builtin_ffs */
 
+#ifndef __CPROVER_LIMITS_H_INCLUDED
+#  include <limits.h>
+#  define __CPROVER_LIMITS_H_INCLUDED
+#endif
+
 int __builtin_clz(unsigned int x);
 
 inline int __builtin_ffs(int x)
@@ -47,11 +52,16 @@ inline int __builtin_ffs(int x)
   unsigned int u = (unsigned int)x;
 #pragma CPROVER check pop
 
-  return sizeof(int) * 8 - __builtin_clz(u & ~(u - 1));
+  return sizeof(int) * CHAR_BIT - __builtin_clz(u & ~(u - 1));
 }
 
 /* FUNCTION: __builtin_ffsl */
 
+#ifndef __CPROVER_LIMITS_H_INCLUDED
+#  include <limits.h>
+#  define __CPROVER_LIMITS_H_INCLUDED
+#endif
+
 int __builtin_clzl(unsigned long x);
 
 inline int __builtin_ffsl(long x)
@@ -64,11 +74,16 @@ inline int __builtin_ffsl(long x)
   unsigned long u = (unsigned long)x;
 #pragma CPROVER check pop
 
-  return sizeof(long) * 8 - __builtin_clzl(u & ~(u - 1));
+  return sizeof(long) * CHAR_BIT - __builtin_clzl(u & ~(u - 1));
 }
 
 /* FUNCTION: __builtin_ffsll */
 
+#ifndef __CPROVER_LIMITS_H_INCLUDED
+#  include <limits.h>
+#  define __CPROVER_LIMITS_H_INCLUDED
+#endif
+
 int __builtin_clzll(unsigned long long x);
 
 inline int __builtin_ffsll(long long x)
@@ -81,7 +96,7 @@ inline int __builtin_ffsll(long long x)
   unsigned long long u = (unsigned long long)x;
 #pragma CPROVER check pop
 
-  return sizeof(long long) * 8 - __builtin_clzll(u & ~(u - 1));
+  return sizeof(long long) * CHAR_BIT - __builtin_clzll(u & ~(u - 1));
 }
 
 /* FUNCTION: __atomic_test_and_set */

src/ansi-c/literals/convert_character_literal.cpp

@@ -11,6 +11,8 @@ Author: Daniel Kroening, [email protected]
 
 #include "convert_character_literal.h"
 
+#include <climits>
+
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/std_expr.h>
@@ -51,7 +53,7 @@ exprt convert_character_literal(
       for(unsigned i=0; i<value.size(); i++)
       {
         mp_integer z=(unsigned char)(value[i]);
-        z=z<<((value.size()-i-1)*8);
+        z = z << ((value.size() - i - 1) * CHAR_BIT);
         x+=z;
       }
 
@@ -84,7 +86,7 @@ exprt convert_character_literal(
       for(unsigned i=0; i<value.size(); i++)
       {
         mp_integer z=(unsigned char)(value[i]);
-        z=z<<((value.size()-i-1)*8);
+        z = z << ((value.size() - i - 1) * CHAR_BIT);
         x+=z;
       }
 

src/cbmc/cbmc_parse_options.cpp

@@ -11,8 +11,9 @@ Author: Daniel Kroening, [email protected]
 
 #include "cbmc_parse_options.h"
 
-#include <fstream>
+#include <climits>
 #include <cstdlib> // exit()
+#include <fstream>
 #include <iostream>
 #include <memory>
 
@@ -516,8 +517,9 @@ int cbmc_parse_optionst::doit()
   //
   // Print a banner
   //
-  log.status() << "CBMC version " << CBMC_VERSION << " " << sizeof(void *) * 8
-               << "-bit " << config.this_architecture() << " "
+  log.status() << "CBMC version " << CBMC_VERSION << " "
+               << sizeof(void *) * CHAR_BIT << "-bit "
+               << config.this_architecture() << " "
                << config.this_operating_system() << messaget::eom;
 
   //

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -11,9 +11,10 @@ Author: Daniel Kroening, [email protected]
 
 #include "goto_analyzer_parse_options.h"
 
+#include <climits>
 #include <cstdlib> // exit()
-#include <iostream>
 #include <fstream>
+#include <iostream>
 #include <memory>
 
 #include <ansi-c/ansi_c_language.h>
@@ -402,8 +403,9 @@ int goto_analyzer_parse_optionst::doit()
   // Print a banner
   //
   log.status() << "GOTO-ANALYSER version " << CBMC_VERSION << " "
-               << sizeof(void *) * 8 << "-bit " << config.this_architecture()
-               << " " << config.this_operating_system() << messaget::eom;
+               << sizeof(void *) * CHAR_BIT << "-bit "
+               << config.this_architecture() << " "
+               << config.this_operating_system() << messaget::eom;
 
   register_languages();
 

src/goto-cc/ms_cl_cmdline.cpp

@@ -11,10 +11,11 @@ Author: Daniel Kroening
 
 #include "ms_cl_cmdline.h"
 
-#include <cstring>
+#include <climits>
 #include <cstdlib>
-#include <iostream>
+#include <cstring>
 #include <fstream>
+#include <iostream>
 
 #include <util/unicode.h>
 
@@ -165,7 +166,7 @@ static std::istream &my_wgetline(std::istream &in, std::wstring &dest)
       break; // line end
     }
     else
-      dest+=wchar_t(ch1+(ch2<<8));
+      dest += wchar_t(ch1 + (ch2 << CHAR_BIT));
   }
 
   return in;

src/goto-diff/goto_diff_parse_options.cpp

@@ -11,6 +11,7 @@ Author: Peter Schrammel
 
 #include "goto_diff_parse_options.h"
 
+#include <climits>
 #include <cstdlib> // exit()
 #include <fstream>
 #include <iostream>
@@ -162,8 +163,9 @@ int goto_diff_parse_optionst::doit()
   // Print a banner
   //
   log.status() << "GOTO-DIFF version " << CBMC_VERSION << " "
-               << sizeof(void *) * 8 << "-bit " << config.this_architecture()
-               << " " << config.this_operating_system() << messaget::eom;
+               << sizeof(void *) * CHAR_BIT << "-bit "
+               << config.this_architecture() << " "
+               << config.this_operating_system() << messaget::eom;
 
   if(cmdline.args.size()!=2)
   {

src/memory-analyzer/analyze_symbol.cpp

@@ -103,7 +103,7 @@ mp_integer gdb_value_extractort::get_type_size(const typet &type) const
 {
   const auto maybe_size = pointer_offset_bits(type, ns);
   CHECK_RETURN(maybe_size.has_value());
-  return *maybe_size / 8;
+  return *maybe_size / CHAR_BIT;
 }
 
 void gdb_value_extractort::analyze_symbols(const std::vector<irep_idt> &symbols)

src/util/config.cpp

@@ -8,6 +8,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "config.h"
 
+#include <climits>
 #include <cstdlib>
 
 #include "arith_tools.h"
@@ -1010,42 +1011,43 @@ bool configt::set(const cmdlinet &cmdline)
   if(arch==this_arch && os==this_os)
   {
     INVARIANT(
-      ansi_c.int_width == sizeof(int) * 8,
+      ansi_c.int_width == sizeof(int) * CHAR_BIT,
       "int width shall be equal to the system int width");
     INVARIANT(
-      ansi_c.long_int_width == sizeof(long) * 8,
+      ansi_c.long_int_width == sizeof(long) * CHAR_BIT,
       "long int width shall be equal to the system long int width");
     INVARIANT(
-      ansi_c.bool_width == sizeof(bool) * 8,
+      ansi_c.bool_width == sizeof(bool) * CHAR_BIT,
       "bool width shall be equal to the system bool width");
     INVARIANT(
-      ansi_c.char_width == sizeof(char) * 8,
+      ansi_c.char_width == sizeof(char) * CHAR_BIT,
       "char width shall be equal to the system char width");
     INVARIANT(
-      ansi_c.short_int_width == sizeof(short) * 8,
+      ansi_c.short_int_width == sizeof(short) * CHAR_BIT,
       "short int width shall be equal to the system short int width");
     INVARIANT(
-      ansi_c.long_long_int_width == sizeof(long long) * 8,
+      ansi_c.long_long_int_width == sizeof(long long) * CHAR_BIT,
       "long long int width shall be equal to the system long long int width");
     INVARIANT(
-      ansi_c.pointer_width == sizeof(void *) * 8,
+      ansi_c.pointer_width == sizeof(void *) * CHAR_BIT,
       "pointer width shall be equal to the system pointer width");
     INVARIANT(
-      ansi_c.single_width == sizeof(float) * 8,
+      ansi_c.single_width == sizeof(float) * CHAR_BIT,
       "float width shall be equal to the system float width");
     INVARIANT(
-      ansi_c.double_width == sizeof(double) * 8,
+      ansi_c.double_width == sizeof(double) * CHAR_BIT,
       "double width shall be equal to the system double width");
     INVARIANT(
-      ansi_c.char_is_unsigned == (static_cast<char>(255) == 255),
+      ansi_c.char_is_unsigned ==
+        (static_cast<char>((1 << CHAR_BIT) - 1) == (1 << CHAR_BIT) - 1),
       "char_is_unsigned flag shall indicate system char unsignedness");
 
-    #ifndef _WIN32
+#ifndef _WIN32
     // On Windows, long double width varies by compiler
     INVARIANT(
-      ansi_c.long_double_width == sizeof(long double) * 8,
+      ansi_c.long_double_width == sizeof(long double) * CHAR_BIT,
       "long double width shall be equal to the system long double width");
-    #endif
+#endif
   }
 
   // the following allows overriding the defaults

src/util/irep_hash.h

@@ -35,6 +35,7 @@ Author: Michael Tautschnig, [email protected]
 // MURMURHASH2A compares most favourably on String6 with 3076 fewer
 // calls (2.9%)
 
+#include <climits>
 #include <cstddef> // std::size_t
 
 #ifdef _MSC_VER
@@ -117,10 +118,9 @@ inline std::size_t basic_hash_finalize(
 
 // Boost uses the symbol hash_combine, if you're getting problems here then
 //  you've probably included a Boost header after this one
-#define hash_combine(h1, h2) \
-  basic_hash_combine<sizeof(std::size_t)*8>(h1, h2)
-#define hash_finalize(h1, len) \
-  basic_hash_finalize(h1, len)
+#  define hash_combine(h1, h2)                                                 \
+    basic_hash_combine<sizeof(std::size_t) * CHAR_BIT>(h1, h2)
+#  define hash_finalize(h1, len) basic_hash_finalize(h1, len)
 
 #endif
 
@@ -224,10 +224,10 @@ inline std::size_t murmurhash2a_hash_finalize<64>(
   return h1;
 }
 
-#define hash_combine(h1, h2) \
-  murmurhash2a_hash_combine<sizeof(std::size_t)*8>(h1, h2)
-#define hash_finalize(h1, len) \
-  murmurhash2a_hash_finalize<sizeof(std::size_t)*8>(h1, len)
+#  define hash_combine(h1, h2)                                                 \
+    murmurhash2a_hash_combine<sizeof(std::size_t) * CHAR_BIT>(h1, h2)
+#  define hash_finalize(h1, len)                                               \
+    murmurhash2a_hash_finalize<sizeof(std::size_t) * CHAR_BIT>(h1, len)
 
 #endif
 
@@ -340,10 +340,10 @@ inline std::size_t murmurhash3_hash_finalize<64>(
   return fmix64(h1);
 }
 
-#define hash_combine(h1, h2) \
-  murmurhash3_hash_combine<sizeof(std::size_t)*8>(h1, h2)
-#define hash_finalize(h1, len) \
-  murmurhash3_hash_finalize<sizeof(std::size_t)*8>(h1, len)
+#  define hash_combine(h1, h2)                                                 \
+    murmurhash3_hash_combine<sizeof(std::size_t) * CHAR_BIT>(h1, h2)
+#  define hash_finalize(h1, len)                                               \
+    murmurhash3_hash_finalize<sizeof(std::size_t) * CHAR_BIT>(h1, len)
 
 #endif
 

src/util/irep_serialization.cpp

@@ -13,8 +13,9 @@ Date: May 2007
 
 #include "irep_serialization.h"
 
-#include <sstream>
+#include <climits>
 #include <iostream>
+#include <sstream>
 
 #include "exception_utils.h"
 #include "string_hash.h"
@@ -161,7 +162,7 @@ std::size_t irep_serializationt::read_gb_word(std::istream &in)
 
   while(in.good())
   {
-    if(shift_distance >= sizeof(res) * 8)
+    if(shift_distance >= sizeof(res) * CHAR_BIT)
       throw deserialization_exceptiont("input number too large");
 
     unsigned char ch=static_cast<unsigned char>(in.get());