Merge pull request #5962 from tautschnig/char_bit

tautschnig · web-flow · commit bcb3821f1574 · 2021-05-06T22:30:45.000+02:00
Do not assume that build architecture has byte/char==8 bits
diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp
@@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #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();
 
diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp
@@ -11,8 +11,9 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "jbmc_parse_options.h"
 
-#include <fstream>
+#include <climits>
 #include <cstdlib> // exit()
+#include <fstream>
 #include <iostream>
 #include <memory>
 
@@ -484,8 +485,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
diff --git a/jbmc/src/jdiff/jdiff_parse_options.cpp b/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)
diff --git a/src/ansi-c/literals/convert_character_literal.cpp b/src/ansi-c/literals/convert_character_literal.cpp
@@ -11,6 +11,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #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;
       }
 
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
@@ -11,8 +11,9 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "cbmc_parse_options.h"
 
-#include <fstream>
+#include <climits>
 #include <cstdlib> // exit()
+#include <fstream>
 #include <iostream>
 #include <memory>
 
@@ -519,8 +520,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;
 
   //
diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp
@@ -11,9 +11,10 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #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();
 
diff --git a/src/goto-cc/ms_cl_cmdline.cpp b/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;
diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/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)
   {
diff --git a/src/memory-analyzer/analyze_symbol.cpp b/src/memory-analyzer/analyze_symbol.cpp
@@ -7,8 +7,6 @@ Author: Malte Mues <mail.mues@gmail.com>
 
 \*******************************************************************/
 
-#include <cstdlib>
-
 #include "analyze_symbol.h"
 
 #include <util/c_types.h>
@@ -20,6 +18,9 @@ Author: Malte Mues <mail.mues@gmail.com>
 #include <util/string_constant.h>
 #include <util/string_utils.h>
 
+#include <climits>
+#include <cstdlib>
+
 gdb_value_extractort::gdb_value_extractort(
   const symbol_tablet &symbol_table,
   const std::vector<std::string> &args)
@@ -102,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)
diff --git a/src/util/config.cpp b/src/util/config.cpp
@@ -8,6 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #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
diff --git a/src/util/irep_hash.h b/src/util/irep_hash.h
@@ -35,6 +35,7 @@ Author: Michael Tautschnig, mt@eecs.qmul.ac.uk
 // 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
 
diff --git a/src/util/irep_serialization.cpp b/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());
diff --git a/src/util/mp_arith.cpp b/src/util/mp_arith.cpp
@@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <algorithm>
 #include <cctype>
+#include <climits>
 #include <cstdlib>
 #include <limits>
 #include <ostream>
@@ -122,7 +123,7 @@ const mp_integer binary2integer(const std::string &n, bool is_signed)
   if(n.empty())
     return 0;
 
-  if(n.size()<=(sizeof(unsigned long)*8))
+  if(n.size() <= (sizeof(unsigned long) * CHAR_BIT))
   {
     // this is a tuned implementation for short integers
 
@@ -264,10 +265,8 @@ mp_integer arith_left_shift(
   ullong_t shift=b.to_ulong();
 
   llong_t result=a.to_long()<<shift;
-  llong_t mask=
-    true_size<(sizeof(llong_t)*8) ?
-    (1LL << true_size) - 1 :
-    -1;
+  llong_t mask =
+    true_size < (sizeof(llong_t) * CHAR_BIT) ? (1LL << true_size) - 1 : -1;
   return result&mask;
 }
 
@@ -303,7 +302,7 @@ mp_integer logic_left_shift(
 
   ullong_t shift=b.to_ulong();
   llong_t result=a.to_long()<<shift;
-  if(true_size<(sizeof(llong_t)*8))
+  if(true_size < (sizeof(llong_t) * CHAR_BIT))
   {
     const llong_t sign = (1LL << (true_size - 1)) & result;
     const llong_t mask = (1LL << true_size) - 1;

Original file line number	Diff line number	Diff line change
`@@ -11,6 +11,8 @@ Author: Daniel Kroening, kroening@kroening.com`
`11`	`11`
`12`	`12`	`#include "convert_character_literal.h"`
`13`	`13`
	`14`	`+#include <climits>`
	`15`	`+`
`14`	`16`	`#include <util/arith_tools.h>`
`15`	`17`	`#include <util/c_types.h>`
`16`	`18`	`#include <util/std_expr.h>`
`@@ -51,7 +53,7 @@ exprt convert_character_literal(`
`51`	`53`	`for(unsigned i=0; i<value.size(); i++)`
`52`	`54`	`{`
`53`	`55`	`mp_integer z=(unsigned char)(value[i]);`
`54`		`- z=z<<((value.size()-i-1)*8);`
	`56`	`+ z = z << ((value.size() - i - 1) * CHAR_BIT);`
`55`	`57`	`x+=z;`
`56`	`58`	`}`
`57`	`59`
`@@ -84,7 +86,7 @@ exprt convert_character_literal(`
`84`	`86`	`for(unsigned i=0; i<value.size(); i++)`
`85`	`87`	`{`
`86`	`88`	`mp_integer z=(unsigned char)(value[i]);`
`87`		`- z=z<<((value.size()-i-1)*8);`
	`89`	`+ z = z << ((value.size() - i - 1) * CHAR_BIT);`
`88`	`90`	`x+=z;`
`89`	`91`	`}`
`90`	`92`