Do not hardcode char/bytes having 8 bits #917
Conversation
|
|
d6010a2 to
4047f38
Compare
c5fb9c2 to
ebc4c75
Compare
ff0e2f6 to
437462a
Compare
90365a2 to
3f38349
Compare
2b06c7b to
5062aa8
Compare
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.
4c871ca to
9ab636f
Compare
| @@ -185,7 +187,7 @@ get_partitions_long(const std::size_t n, const std::size_t k) | |||
| /// Compute all positions of ones in the bit vector `v` (1-indexed). | |||
| std::vector<std::size_t> get_ones_pos(std::size_t v) | |||
| { | |||
| const std::size_t length = sizeof(std::size_t) * 8; | |||
| const std::size_t length = sizeof(std::size_t) * CHAR_BIT; | |||
There was a problem hiding this comment.
The PR description states that you are using the width from the configuration. But this line is using the width for the machine for which cbmc is being compiled. Shouldn't config.ansi_c.char_width be used instead? The distinction could be important if cbmc is to be used for program written for a machine such as a DSP like you suggested in the PR desription. Wouldn't these architectures be more likely to be targeted using a cross compiler rather than porting cbmc to the target hardware itself?
There was a problem hiding this comment.
You are right in that care is required where CHAR_BIT is the right choice and where config.ansi_c.char_width is to be used instead. I hope to have made the right choice in all places, but of course may have made mistakes. For this particular case: as far as I understand the code, this is about the width of bytes that CBMC is being compiled for, and not whatever the verification target might be. So I claim that CHAR_BIT is correct. Now you are also right in that, in all likelihood, one would use a cross compiler for such a DSP, and it may well be that no platform that CBMC ever runs on has CHAR_BIT != 8 - but I'd also like to avoid magic numbers, making it very difficult to tell whether the use of "8" is one that should be config.ansi_c.char_width instead, or is actually fine for it's the compile-time byte width on all relevant platforms.
There was a problem hiding this comment.
If you are convinced that we are depending on the right thing in this case, then I am happy to merge this as is.
There was a problem hiding this comment.
This specific case it is to enumerate various bit sequences, and this enumeration is done by the compiled CBMC binary.
🤣 You wish! |
There was a problem hiding this comment.
FYI - CHAR_BIT is the C standard library version of this constant. The C++ equivalent is std::numeric_limits<char>::digits. In this case digits refers to binary digits on the underlying hardware and std::numeric_limits<char>::radix is 2.
🤔 I am happy for debugging and addition of tests for a platform where char is not 8 bits to be left for a follow-up PR if and when this becomes a priority.
| @@ -38,14 +39,14 @@ optionalt<mp_integer> member_offset( | |||
| { | |||
| const std::size_t w = to_c_bit_field_type(comp.type()).get_width(); | |||
| bit_field_bits += w; | |||
| result += bit_field_bits / 8; | |||
| bit_field_bits %= 8; | |||
| result += bit_field_bits / config.ansi_c.char_width; | |||
There was a problem hiding this comment.
I'm assuming we guarantee that char_width is always different than zero in all these cases, right?
There was a problem hiding this comment.
Yes, though we might one day want to have some architecture sanity check.
There was a problem hiding this comment.
It can be loaded from file through configt::set_from_symbol_table and symtab2gb. Therefore it could theoretically be set to 0 in the file and I am not sure we have appropriate validation that the value from file is not 0.
| @@ -137,7 +137,7 @@ void is_fresh_baset::update_ensures(goto_programt &ensures) | |||
|
|
|||
| array_typet is_fresh_baset::get_memmap_type() | |||
| { | |||
| return array_typet(c_bool_typet(8), infinity_exprt(size_type())); | |||
There was a problem hiding this comment.
Do we really need to propagate this to instrumentation code ? This code does not represent anything running on an actual processor. Should c_bool_typet(8) be deprecated completely ?
There was a problem hiding this comment.
I'm ok with an arbitrary type, but we must not have "8" as a magic number. I assumed this was "8" in the first place so as to have byte granularity? Was I wrong?
There was a problem hiding this comment.
My usual assumption is that architecture should be well defined at the point of running the front end. This is because the C front end runs an external C pre-processor which can have architecture specific macro expansions. As goto-instrument runs after the front end, it is operating on an architecture specific program form. Note for example that the c_bool_type() construction function in src/util/c_types.cpp references the same config field.
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.