Do not hardcode char/bytes having 8 bits #917

tautschnig · 2017-05-13T18:41:30Z

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.

tautschnig · 2017-05-23T11:59:44Z

~~Marking do-not-merge as it includes a commit that overlaps with #955.~~

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.

peterschrammel

tautschnig created on 13 May 2017

Last one on the stack?

thomasspriggs · 2022-10-17T15:02:04Z

src/goto-instrument/synthesizer/expr_enumerator.cpp

@@ -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;


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?

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.

If you are convinced that we are depending on the right thing in this case, then I am happy to merge this as is.

This specific case it is to enumerate various bit sequences, and this enumeration is done by the compiled CBMC binary.

tautschnig · 2022-10-18T07:34:22Z

tautschnig created on 13 May 2017

Last one on the stack?

🤣 You wish!

thomasspriggs

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.

feliperodri · 2022-10-18T14:14:47Z

src/util/pointer_offset_size.cpp

@@ -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;


I'm assuming we guarantee that char_width is always different than zero in all these cases, right?

Yes, though we might one day want to have some architecture sanity check.

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.

remi-delmas-3000 · 2022-10-18T14:19:50Z

src/goto-instrument/contracts/memory_predicates.cpp

@@ -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()));


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 ?

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?

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.

tautschnig force-pushed the byte-config branch from dd4210c to bc36ba0 Compare May 23, 2017 11:58

tautschnig self-assigned this May 23, 2017

tautschnig added the do not merge label May 23, 2017

tautschnig force-pushed the byte-config branch 3 times, most recently from d6010a2 to 4047f38 Compare May 23, 2017 17:43

tautschnig removed the do not merge label May 23, 2017

tautschnig force-pushed the byte-config branch from 4047f38 to a2edaec Compare May 24, 2017 08:04

tautschnig assigned kroening and unassigned tautschnig May 25, 2017

tautschnig force-pushed the byte-config branch from a2edaec to e62a5f5 Compare May 29, 2017 15:45

tautschnig force-pushed the byte-config branch from e62a5f5 to 5111350 Compare June 8, 2017 06:30

tautschnig added the cleanup label Jun 9, 2017

tautschnig force-pushed the byte-config branch 2 times, most recently from c5fb9c2 to ebc4c75 Compare June 28, 2017 14:16

tautschnig force-pushed the byte-config branch 2 times, most recently from ff0e2f6 to 437462a Compare July 15, 2017 18:22

tautschnig force-pushed the byte-config branch from 437462a to 90365a2 Compare August 7, 2017 12:21

tautschnig changed the base branch from master to develop August 22, 2017 12:25

tautschnig assigned tautschnig and unassigned kroening Sep 2, 2017

tautschnig changed the title ~~Do not assume that chars/bytes have 8 bits (and some cleanup)~~ [depends: #1331,#1332,#1333] Do not assume that chars/bytes have 8 bits (and some cleanup) Sep 2, 2017

tautschnig changed the title ~~[depends: #1331,#1332,#1333] Do not assume that chars/bytes have 8 bits (and some cleanup)~~ [depends: #1333] Do not assume that chars/bytes have 8 bits (and some cleanup) Sep 4, 2017

tautschnig mentioned this pull request Nov 17, 2017

Simplify equalities of constants #1598

Merged

tautschnig force-pushed the byte-config branch from 90365a2 to 3f38349 Compare January 5, 2018 19:22

tautschnig requested review from cesaro, chrisr-diffblue, kroening and martin-cs as code owners January 5, 2018 19:22

tautschnig force-pushed the byte-config branch 3 times, most recently from 2b06c7b to 5062aa8 Compare April 7, 2021 16:24

tautschnig force-pushed the byte-config branch from 5062aa8 to 4c871ca Compare April 14, 2021 19:09

tautschnig mentioned this pull request Apr 27, 2021

make_byte_{extract,update} to build byte_{extract,update} expressions #6056

Merged

4 tasks

tautschnig added the dependent - do not merge label May 1, 2021

peterschrammel mentioned this pull request Sep 13, 2021

Fix applicability condition of simplify_byte_update #6311

Merged

7 tasks

Do not hardcode char/bytes having 8 bits

9ab636f

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.

tautschnig force-pushed the byte-config branch from 4c871ca to 9ab636f Compare October 17, 2022 12:03

tautschnig changed the title ~~Do not hardcode char/bytes having 8 bits [depends-on: #6009]~~ Do not hardcode char/bytes having 8 bits Oct 17, 2022

tautschnig removed the dependent - do not merge label Oct 17, 2022

tautschnig marked this pull request as ready for review October 17, 2022 12:03

tautschnig requested review from feliperodri, remi-delmas-3000 and chris-ryder as code owners October 17, 2022 12:03

tautschnig assigned kroening, remi-delmas-3000, peterschrammel and feliperodri and unassigned tautschnig Oct 17, 2022

peterschrammel approved these changes Oct 17, 2022

View reviewed changes

thomasspriggs reviewed Oct 17, 2022

View reviewed changes

tautschnig unassigned kroening and peterschrammel Oct 18, 2022

thomasspriggs approved these changes Oct 18, 2022

View reviewed changes

feliperodri approved these changes Oct 18, 2022

View reviewed changes

tautschnig merged commit baef5a3 into diffblue:develop Oct 18, 2022

tautschnig deleted the byte-config branch October 18, 2022 14:17

remi-delmas-3000 reviewed Oct 18, 2022

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Do not hardcode char/bytes having 8 bits #917

Do not hardcode char/bytes having 8 bits #917

tautschnig commented May 13, 2017 •

edited

Loading

tautschnig commented May 23, 2017 •

edited

Loading

peterschrammel left a comment

thomasspriggs Oct 17, 2022

tautschnig Oct 18, 2022

thomasspriggs Oct 18, 2022

tautschnig Oct 18, 2022

tautschnig commented Oct 18, 2022

thomasspriggs left a comment

feliperodri Oct 18, 2022

tautschnig Oct 18, 2022

thomasspriggs Oct 18, 2022

remi-delmas-3000 Oct 18, 2022 •

edited

Loading

tautschnig Oct 18, 2022

thomasspriggs Oct 18, 2022

Do not hardcode char/bytes having 8 bits #917

Do not hardcode char/bytes having 8 bits #917

Conversation

tautschnig commented May 13, 2017 • edited Loading

tautschnig commented May 23, 2017 • edited Loading

peterschrammel left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tautschnig commented Oct 18, 2022

thomasspriggs left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

remi-delmas-3000 Oct 18, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tautschnig commented May 13, 2017 •

edited

Loading

tautschnig commented May 23, 2017 •

edited

Loading

remi-delmas-3000 Oct 18, 2022 •

edited

Loading