Test 32-bit builds in CI and fix platform-specific code and tests #7756
Conversation
Codecov ReportPatch coverage:
Additional details and impacted files@@ Coverage Diff @@
## develop #7756 +/- ##
===========================================
- Coverage 78.86% 78.40% -0.47%
===========================================
Files 1699 1699
Lines 195229 195239 +10
===========================================
- Hits 153977 153075 -902
- Misses 41252 42164 +912
☔ View full report in Codecov by Sentry. |
Well, the tests are failing… |
tautschnig
force-pushed
the
bugfixes/32-bit
branch
from
3d71815
to
141a923
Compare
tautschnig
requested review from
a team,
peterschrammel,
thomasspriggs,
NlightNFotis,
kroening,
martin-cs and
remi-delmas-3000
as code owners
|
My apologies for producing such a large size of this bug-fixing PR: please do review commit-by-commit as each of them should be self-contained. |
tautschnig
assigned kroening, remi-delmas-3000, martin-cs and thomasspriggs and unassigned tautschnig
tautschnig
force-pushed
the
bugfixes/32-bit
branch
from
141a923
to
9aae4e7
Compare
|
This does remind me that we need to think about the type of the array size. |
Yes, we might be able to modify/partly revert the commit "Arrays have a signed size" once/if we change that. (I tried to make sure that all changes related to array-size-signedness are contained in that one commit.) |
tautschnig
force-pushed
the
bugfixes/32-bit
branch
from
9aae4e7
to
f548c16
Compare
GCC defines i386 as a macro (with value 1) on 32-bit x86.
We also support 32-bit architectures.
Not all systems have 64-bit addresses. Also fix an off-by-power-of-2 error in the comment.
Not all platforms have 32-bit int, and the size of long int may be the same as int.
Not all platforms require casts from int to long int as those may have the same bit width.
The pointer width encoded in pre-built snapshots is 64 bits. Replace that width at test runtime with the host system bit width.
Fix tests and argc/argv constraints to account for the fact that our arrays (at present) use signed sizes. We previously didn't always consider the case that where sizeof(int) == sizeof(long), which demonstrated overflows.
…long) This isn't true for all platforms.
Some tests assumed that sizeof(int) < sizeof(long), which need not be the case.
This wouldn't be true for all platforms.
The comparison previously succeeded by chance on 64-bit platforms, but didn't pass on ones that have a smaller pointer width.
Use a suffix to ensure the constant isn't treated as an int, but instead matches the left-hand side's type.
We need to create a typed variant of top rather than relying on eval to produce a typed expression. Tests involving pointer difference spuriously passed for 64-bit platforms include a type cast in those expressions. The abstract evaluation of said type cast resulted in typed expressions despite the untyped nil input.
Not all platforms have 32-bit int, and the size of long int may be the same as int.
There is no reason an integer couldn't have the same value as a pointer (when converted to an integer type). This assertion might accidentally hold on platforms where sizeof(int) != sizeof(int *) given our current pointer model, but this is an implementation detail that we must not rely on. The assertion certainly doesn't hold when sizeof(int) == sizeof(int *).
…idth Do a zero extension, just like the propositional back-end does.
We previously hard-coded x86_64 calling conventions for malloc.
We ended up with an assumption that performed an out-of-bounds access as there was no link between `size` and the return value in the contract.
This is to detect hardwired 64-bit configuration or tests when those should be platform-independent instead.
tautschnig
force-pushed
the
bugfixes/32-bit
branch
from
f548c16
to
1a30ad4
Compare
| @@ -103,14 +103,14 @@ TEST_CASE("Value expr construction from smt.", "[core][smt2_incremental]") | |||
| rowt{smt_bit_vector_constant_termt{1, 8}, from_integer(1, c_bool_typet(8))}, | |||
| rowt{ | |||
| smt_bit_vector_constant_termt{0, 64}, | |||
| from_integer(0, pointer_typet(void_type(), 64 /* bits */))}, | |||
| from_integer(0, pointer_typet{empty_typet{}, 64 /* bits */})}, | |||
There was a problem hiding this comment.
My apologies for nitpicking something which is already merged, but how does swapping from void_type() to empty_typet{} fix a 32-bit build problem? The void_type() function just returns an instance of empty_typet{}, and neither of these depend on a bit width, as far as I can see.
There was a problem hiding this comment.
Oh, yes, that indeed wasn't a complete fix: it was my attempt to get rid of util/c_types.h, for many of the types in there are by definition platform-dependent. But turns out that fully removing that include is impossible, because there also is use of c_bool_typet and c_enum_typet.
There was a problem hiding this comment.
Ah, so I could effectively think of this as a front-end de-coupling effort. There are many C front end specific types in the unit tests for the new SMT decision procedure because the decision procedure needs to implement support for them specifically. This is the case because these data structures find thier way all the way through cbmc to the decision procedure rather than being lowered to some kind of goto construct at the end of the processing of the front end. Another one for the list is union_typet which is defined in util/c_types.h, but which is sent to the decision procedure.
Whilst the decision procedure needs front-end specific functionality I would prefer to keep matching front-end specific types in the unit tests. That way we can remove the front end specifics from the decision procedure and the unit tests if and when we ever sufficiently decouple to stop them getting to the decision procedure.
There was a problem hiding this comment.
I entirely agree with your assessment. One day we should come clean on this and decide whether the types you mentioned are to be considered fundamental types, and therefore, should be moved out of c_types.h, or be lowered and not be ones to handle in back-ends.
There was a problem hiding this comment.
So, yes, my change in this file wasn't actually necessary, but probably doesn't need to be reverted either?
There was a problem hiding this comment.
I think it was somewhat easier to read as a void pointer, rather than an empty pointer. However I also don't think it is worth taking the time to revert. I questioned it as it didn't appear to match the commit message concerning 32 bit support, so I didn't initially understand why the change had been made. Thank you for taking the time to respond.
Please review commit-by-commit.