From 74978c0c393ee784aa29d76a37a694c1228bc62e Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 13 May 2017 19:35:39 +0100 Subject: [PATCH] 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. --- .../src/janalyzer/janalyzer_parse_options.cpp | 6 ++-- jbmc/src/jbmc/jbmc_parse_options.cpp | 8 ++++-- jbmc/src/jdiff/jdiff_parse_options.cpp | 6 ++-- .../literals/convert_character_literal.cpp | 6 ++-- src/cbmc/cbmc_parse_options.cpp | 8 ++++-- .../goto_analyzer_parse_options.cpp | 8 ++++-- src/goto-cc/ms_cl_cmdline.cpp | 7 +++-- src/goto-diff/goto_diff_parse_options.cpp | 6 ++-- src/memory-analyzer/analyze_symbol.cpp | 7 +++-- src/util/config.cpp | 28 ++++++++++--------- src/util/irep_hash.h | 24 ++++++++-------- src/util/irep_serialization.cpp | 5 ++-- src/util/mp_arith.cpp | 11 ++++---- 13 files changed, 74 insertions(+), 56 deletions(-) diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp index b8b1df6b78f..006922c7426 100644 --- 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 #include // exit() #include #include @@ -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 index 8a95b6b4057..747a633b6f4 100644 --- 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 +#include #include // exit() +#include #include #include @@ -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 index e84e0d96599..1a35ff0cfac 100644 --- 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 #include // exit() #include #include @@ -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 index a33d69c7acb..7d4fa9d7f79 100644 --- 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 + #include #include #include @@ -51,7 +53,7 @@ exprt convert_character_literal( for(unsigned i=0; i +#include #include // exit() +#include #include #include @@ -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 index d17aec57623..848d0c33acd 100644 --- 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 #include // exit() -#include #include +#include #include #include @@ -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 index 3367adddb7f..ca0a153cc09 100644 --- 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 +#include #include -#include +#include #include +#include #include @@ -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 index 1a14aea32b8..6dda6edf82d 100644 --- 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 #include // exit() #include #include @@ -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 index 65072ac034d..cdee3ab789b 100644 --- a/src/memory-analyzer/analyze_symbol.cpp +++ b/src/memory-analyzer/analyze_symbol.cpp @@ -7,8 +7,6 @@ Author: Malte Mues \*******************************************************************/ -#include - #include "analyze_symbol.h" #include @@ -20,6 +18,9 @@ Author: Malte Mues #include #include +#include +#include + gdb_value_extractort::gdb_value_extractort( const symbol_tablet &symbol_table, const std::vector &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 &symbols) diff --git a/src/util/config.cpp b/src/util/config.cpp index f6a65dd95a7..017c04c4a21 100644 --- a/src/util/config.cpp +++ b/src/util/config.cpp @@ -8,6 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "config.h" +#include #include #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(255) == 255), + ansi_c.char_is_unsigned == + (static_cast((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 index ce4ef52da76..0d5962a221d 100644 --- 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 #include // 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(h1, h2) -#define hash_finalize(h1, len) \ - basic_hash_finalize(h1, len) +# define hash_combine(h1, h2) \ + basic_hash_combine(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(h1, h2) -#define hash_finalize(h1, len) \ - murmurhash2a_hash_finalize(h1, len) +# define hash_combine(h1, h2) \ + murmurhash2a_hash_combine(h1, h2) +# define hash_finalize(h1, len) \ + murmurhash2a_hash_finalize(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(h1, h2) -#define hash_finalize(h1, len) \ - murmurhash3_hash_finalize(h1, len) +# define hash_combine(h1, h2) \ + murmurhash3_hash_combine(h1, h2) +# define hash_finalize(h1, len) \ + murmurhash3_hash_finalize(h1, len) #endif diff --git a/src/util/irep_serialization.cpp b/src/util/irep_serialization.cpp index f0851dc048a..c33851fb6b7 100644 --- a/src/util/irep_serialization.cpp +++ b/src/util/irep_serialization.cpp @@ -13,8 +13,9 @@ Date: May 2007 #include "irep_serialization.h" -#include +#include #include +#include #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(in.get()); diff --git a/src/util/mp_arith.cpp b/src/util/mp_arith.cpp index b9a7ad4f55a..60065dcaac8 100644 --- a/src/util/mp_arith.cpp +++ b/src/util/mp_arith.cpp @@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include @@ -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()<