Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
May 6, 2021
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 4 additions & 2 deletions jbmc/src/janalyzer/janalyzer_parse_options.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]

#include "janalyzer_parse_options.h"

#include <climits>
#include <cstdlib> // exit()
#include <fstream>
#include <iostream>
Expand Down Expand Up @@ -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 "
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Out-of-scope for this PR, but give how this exact log.status pattern is duplicated several times, it does rather feel like a utility function could be useful :-)

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thank you for highlighting this. Now PR'ed in #6089.

<< config.this_architecture() << " "
<< config.this_operating_system() << messaget::eom;

register_languages();

Expand Down
8 changes: 5 additions & 3 deletions jbmc/src/jbmc/jbmc_parse_options.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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>

Expand Down Expand Up @@ -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
Expand Down
6 changes: 4 additions & 2 deletions jbmc/src/jdiff/jdiff_parse_options.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ Author: Peter Schrammel

#include "jdiff_parse_options.h"

#include <climits>
#include <cstdlib> // exit()
#include <fstream>
#include <iostream>
Expand Down Expand Up @@ -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)
Expand Down
6 changes: 4 additions & 2 deletions src/ansi-c/literals/convert_character_literal.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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>
Expand Down Expand Up @@ -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;
}

Expand Down Expand Up @@ -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;
}

Expand Down
8 changes: 5 additions & 3 deletions src/cbmc/cbmc_parse_options.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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>

Expand Down Expand Up @@ -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;

//
Expand Down
8 changes: 5 additions & 3 deletions src/goto-analyzer/goto_analyzer_parse_options.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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>
Expand Down Expand Up @@ -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();

Expand Down
7 changes: 4 additions & 3 deletions src/goto-cc/ms_cl_cmdline.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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>

Expand Down Expand Up @@ -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;
Expand Down
6 changes: 4 additions & 2 deletions src/goto-diff/goto_diff_parse_options.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ Author: Peter Schrammel

#include "goto_diff_parse_options.h"

#include <climits>
#include <cstdlib> // exit()
#include <fstream>
#include <iostream>
Expand Down Expand Up @@ -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)
{
Expand Down
7 changes: 4 additions & 3 deletions src/memory-analyzer/analyze_symbol.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,6 @@ Author: Malte Mues <[email protected]>

\*******************************************************************/

#include <cstdlib>

#include "analyze_symbol.h"

#include <util/c_types.h>
Expand All @@ -20,6 +18,9 @@ Author: Malte Mues <[email protected]>
#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)
Expand Down Expand Up @@ -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)
Expand Down
28 changes: 15 additions & 13 deletions src/util/config.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ Author: Daniel Kroening, [email protected]

#include "config.h"

#include <climits>
#include <cstdlib>

#include "arith_tools.h"
Expand Down Expand Up @@ -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
Expand Down
24 changes: 12 additions & 12 deletions src/util/irep_hash.h
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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

Expand Down Expand Up @@ -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

Expand Down Expand Up @@ -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

Expand Down
5 changes: 3 additions & 2 deletions src/util/irep_serialization.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down Expand Up @@ -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());
Expand Down
11 changes: 5 additions & 6 deletions src/util/mp_arith.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@ Author: Daniel Kroening, [email protected]

#include <algorithm>
#include <cctype>
#include <climits>
#include <cstdlib>
#include <limits>
#include <ostream>
Expand Down Expand Up @@ -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

Expand Down Expand Up @@ -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;
}

Expand Down Expand Up @@ -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;
Expand Down