Test 32-bit builds in CI and fix platform-specific code and tests #7756
Commits on Aug 23, 2023
-
Fix 32bit unit test build failure
GCC defines i386 as a macro (with value 1) on 32-bit x86.
-
Unit tests: do not hard-code 64-bit pointer width
We also support 32-bit architectures.
-
Interpreter: Do not hard-code platform bit width
Not all systems have 64-bit addresses. Also fix an off-by-power-of-2 error in the comment.
-
Make goto-inspect test patterns platform-agnostic
Not all platforms have 32-bit int, and the size of long int may be the same as int.
-
Test patterns: fix optional casts
Not all platforms require casts from int to long int as those may have the same bit width.
-
goto-harness regression tests: support non-64-bit platforms
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.
-
Fix tests and contracts wrongly assuming sizeof(long) == sizeof(long …
…long) This isn't true for all platforms.
-
Tests: use types that are smaller than long on all platforms
Some tests assumed that sizeof(int) < sizeof(long), which need not be the case.
-
Tests: do not hard-code 64 bits/8 bytes as pointer width
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.
-
Properly type initial value of __CPROVER_max_malloc_size
Use a suffix to ensure the constant isn't treated as an int, but instead matches the left-hand side's type.
-
Goto analyzer: do not create untyped nil expression
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.
-
Make cbmc-incr-smt2 test patterns platform-agnostic
Not all platforms have 32-bit int, and the size of long int may be the same as int.
-
cbmc-incr-smt2 tests: remove misguided assertion
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 *).
-
Incremental SMT2: support cast from pointer to integer of different w…
…idth Do a zero extension, just like the propositional back-end does.
-
Make memory-analyzer compatible with i386
We previously hard-coded x86_64 calling conventions for malloc.
-
Contracts test: ensure return value access is in bounds
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.
-
Run 32-bit builds and tests as CI job
This is to detect hardwired 64-bit configuration or tests when those should be platform-independent instead.
