Skip to content
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

Test 32-bit builds in CI and fix platform-specific code and tests #7756

Merged
merged 19 commits into from
Sep 22, 2023
Merged
Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
19 commits
Select commit Hold shift + click to select a range
24d4d3a
Fix 32bit unit test build failure
tautschnig Jun 6, 2023
37ed69c
Unit tests: do not hard-code 64-bit pointer width
tautschnig Jul 7, 2023
caca58b
Interpreter: Do not hard-code platform bit width
tautschnig Aug 2, 2023
093e2f3
Make goto-inspect test patterns platform-agnostic
tautschnig Aug 2, 2023
352299a
Test patterns: fix optional casts
tautschnig Aug 2, 2023
3318f6f
goto-harness regression tests: support non-64-bit platforms
tautschnig Aug 2, 2023
ebaf09f
Arrays have a signed size
tautschnig Aug 2, 2023
a9ca74e
Fix tests and contracts wrongly assuming sizeof(long) == sizeof(long …
tautschnig Aug 2, 2023
0723271
Tests: use types that are smaller than long on all platforms
tautschnig Aug 2, 2023
ba7eb04
Tests: do not hard-code 64 bits/8 bytes as pointer width
tautschnig Aug 2, 2023
a3f1ae9
Tests: fix index typo
tautschnig Aug 2, 2023
28e4238
Properly type initial value of __CPROVER_max_malloc_size
tautschnig Aug 7, 2023
5eb8a94
Goto analyzer: do not create untyped nil expression
tautschnig Aug 7, 2023
cc27808
Make cbmc-incr-smt2 test patterns platform-agnostic
tautschnig Aug 8, 2023
9d1be21
cbmc-incr-smt2 tests: remove misguided assertion
tautschnig Aug 8, 2023
0794f5b
Incremental SMT2: support cast from pointer to integer of different w…
tautschnig Aug 8, 2023
c1f9237
Make memory-analyzer compatible with i386
tautschnig Aug 8, 2023
1cae1b3
Contracts test: ensure return value access is in bounds
tautschnig Aug 8, 2023
1a30ad4
Run 32-bit builds and tests as CI job
tautschnig Jun 6, 2023
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
17 changes: 11 additions & 6 deletions unit/goto-programs/goto_program_validate.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -10,21 +10,27 @@
/// \file
/// Unit tests for goto program validation

#include <testing-utils/use_catch.h>

#include <testing-utils/message.h>

#include <util/arith_tools.h>
#include <util/c_types.h>
#include <util/cmdline.h>
#include <util/config.h>
#include <util/pointer_expr.h>
#include <util/std_code.h>

#include <goto-programs/goto_convert_functions.h>
#include <goto-programs/goto_model.h>
#include <goto-programs/validate_goto_model.h>

#include <testing-utils/message.h>
#include <testing-utils/use_catch.h>

SCENARIO("Validation of a goto program", "[core][goto-programs][validate]")
{
// This test does require a proper architecture to be set so that C type
// widths are configured.
cmdlinet cmdline;
config.set(cmdline);

goto_modelt goto_model;

// void f(){int x = 1;}
Expand Down Expand Up @@ -54,8 +60,7 @@ SCENARIO("Validation of a goto program", "[core][goto-programs][validate]")
goto_model.symbol_table.add(z);

// pointer to fn call
symbolt fn_ptr{
"fn_ptr", pointer_typet(code_typet{{}, empty_typet()}, 64), ID_C};
symbolt fn_ptr{"fn_ptr", pointer_type(code_typet{{}, empty_typet()}), ID_C};
goto_model.symbol_table.add(fn_ptr);

symbolt entry_point{
Expand Down
10 changes: 6 additions & 4 deletions unit/interpreter/interpreter.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,8 @@ Author: Diffblue Ltd.

#include <testing-utils/use_catch.h>

#include <climits>

typedef interpretert::mp_vectort mp_vectort;

class interpreter_testt
Expand Down Expand Up @@ -46,7 +48,7 @@ SCENARIO("interpreter evaluation null pointer expressions")
THEN("null pointer without operands")
{
unsignedbv_typet java_char(16);
pointer_typet pointer_type(java_char, 64);
pointer_typet pointer_type(java_char, sizeof(void *) * CHAR_BIT);

null_pointer_exprt constant_expr{pointer_type};

Expand All @@ -56,13 +58,13 @@ SCENARIO("interpreter evaluation null pointer expressions")
}
THEN("null pointer with operands")
{
pointer_typet outer_pointer_type(empty_typet(), 64);
pointer_typet outer_pointer_type(empty_typet(), sizeof(void *) * CHAR_BIT);
constant_exprt outer_expression(
"0000000000000000000000000000000000000000000000000000000000000000",
outer_pointer_type);

outer_expression.add_to_operands(
null_pointer_exprt(pointer_typet(empty_typet(), 64)));
outer_expression.add_to_operands(null_pointer_exprt(
pointer_typet(empty_typet(), sizeof(void *) * CHAR_BIT)));

mp_vectort mp_vector = interpreter_test.evaluate(outer_expression);

Expand Down
9 changes: 6 additions & 3 deletions unit/pointer-analysis/value_set.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,8 @@ Author: Diffblue Ltd.
#include <pointer-analysis/value_set.h>
#include <testing-utils/use_catch.h>

#include <climits>

static bool object_descriptor_matches(
const exprt &descriptor_expr, const exprt &target)
{
Expand Down Expand Up @@ -49,8 +51,9 @@ SCENARIO(
{
// Create struct A { A *x; A *y }

struct_typet struct_A({{"x", pointer_typet(struct_tag_typet("A"), 64)},
{"y", pointer_typet(struct_tag_typet("A"), 64)}});
struct_typet struct_A(
{{"x", pointer_typet(struct_tag_typet("A"), sizeof(void *) * CHAR_BIT)},
{"y", pointer_typet(struct_tag_typet("A"), sizeof(void *) * CHAR_BIT)}});
struct_A.set_tag("A");

auto &A_x = struct_A.components()[0];
Expand Down Expand Up @@ -225,7 +228,7 @@ SCENARIO(
{
// Make some global integers i1, i2, i3:
signedbv_typet int32_type(32);
pointer_typet int32_ptr(int32_type, 64);
pointer_typet int32_ptr(int32_type, sizeof(void *) * CHAR_BIT);

symbolt i1{"i1", int32_type, irep_idt{}};
i1.base_name = "i1";
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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 */})},
Copy link
Collaborator

Choose a reason for hiding this comment

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

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.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

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.

Copy link
Collaborator

@thomasspriggs thomasspriggs Sep 26, 2023

Choose a reason for hiding this comment

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

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.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

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.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

So, yes, my change in this file wasn't actually necessary, but probably doesn't need to be reverted either?

Copy link
Collaborator

Choose a reason for hiding this comment

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

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.

// The reason for the more intricate elaboration of a pointer with a value
// of 12 is a limitation in the design of from_integer, which only handles
// pointers with value 0 (null pointers).
rowt{
smt_bit_vector_constant_termt{12, 64},
constant_exprt(
integer2bvrep(12, 64), pointer_typet(void_type(), 64 /* bits */))},
integer2bvrep(12, 64), pointer_typet{empty_typet{}, 64 /* bits */})},
rowt{
smt_bit_vector_constant_termt{2, 42},
constant_exprt{"2", c_enum_tag_typet{enum_type_symbol.name}}},
Expand Down Expand Up @@ -184,7 +184,7 @@ TEST_CASE(
"Unexpected conversion of exists quantifier to value expression."},
rowt{
smt_bit_vector_constant_termt{0, 16},
pointer_typet{unsigned_int_type(), 0},
pointer_typet{unsignedbv_typet{32}, 0},
"Width of smt bit vector term must match the width of pointer type"},
rowt{
smt_bit_vector_constant_termt{2, 42},
Expand Down
4 changes: 2 additions & 2 deletions unit/util/lower_byte_operators.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -279,7 +279,7 @@ SCENARIO("byte_extract_lowering", "[core][util][lowering][byte_extract]")
signedbv_typet(128),
ieee_float_spect::single_precision().to_type(),
// generates the correct value, but remains wrapped in a typecast
// pointer_typet(u64, 64),
// pointer_typet(u64, sizeof(void *) * CHAR_BIT),
vector_typet(size_type(), u8, size),
vector_typet(size_type(), u64, size),
complex_typet(s16),
Expand Down Expand Up @@ -435,7 +435,7 @@ SCENARIO("byte_update_lowering", "[core][util][lowering][byte_update]")
signedbv_typet(128),
ieee_float_spect::single_precision().to_type(),
// generates the correct value, but remains wrapped in a typecast
// pointer_typet(u64, 64),
// pointer_typet(u64, sizeof(void *) * CHAR_BIT),
vector_typet(size_type(), u8, size),
vector_typet(size_type(), u64, size),
// complex_typet(s16),
Expand Down