From 31615c6a8d48c00515ac130a188d295526dbf8c1 Mon Sep 17 00:00:00 2001 From: Hannes Steffenhagen Date: Thu, 2 Jul 2020 15:48:04 +0100 Subject: [PATCH 1/2] Do not use side_effect_expr_nondett in recursive_initialization MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit If we use side_effect_expr_nondett then dump_c will generation function calls to functions with names like `nondet_int` without declaration. This is a problem because it’ll lead the C frontend to complain about undeclared identifiers and such. To fix this, we changed goto-harness to just not use side_effect_expr_nondett at all (better long term fix would be to make sure `dump_c` outputs declarations too). --- .../do-not-use-nondet-for-primitives/test.c | 6 ++++ .../test.desc | 17 +++++++++++ .../do-not-use-nondet-for-recursion/test.c | 11 +++++++ .../do-not-use-nondet-for-recursion/test.desc | 14 +++++++++ .../test.c | 8 +++++ .../test.desc | 18 +++++++++++ src/goto-harness/recursive_initialization.cpp | 30 ++++++++++--------- 7 files changed, 90 insertions(+), 14 deletions(-) create mode 100644 regression/goto-harness/do-not-use-nondet-for-primitives/test.c create mode 100644 regression/goto-harness/do-not-use-nondet-for-primitives/test.desc create mode 100644 regression/goto-harness/do-not-use-nondet-for-recursion/test.c create mode 100644 regression/goto-harness/do-not-use-nondet-for-recursion/test.desc create mode 100644 regression/goto-harness/do-not-use-nondet-for-selecting-pointers-to-treat-as-equal/test.c create mode 100644 regression/goto-harness/do-not-use-nondet-for-selecting-pointers-to-treat-as-equal/test.desc diff --git a/regression/goto-harness/do-not-use-nondet-for-primitives/test.c b/regression/goto-harness/do-not-use-nondet-for-primitives/test.c new file mode 100644 index 00000000000..9affdade89a --- /dev/null +++ b/regression/goto-harness/do-not-use-nondet-for-primitives/test.c @@ -0,0 +1,6 @@ +#include + +void test_function(int test) +{ + assert(test != 42); +} diff --git a/regression/goto-harness/do-not-use-nondet-for-primitives/test.desc b/regression/goto-harness/do-not-use-nondet-for-primitives/test.desc new file mode 100644 index 00000000000..4e89f3f2ca8 --- /dev/null +++ b/regression/goto-harness/do-not-use-nondet-for-primitives/test.desc @@ -0,0 +1,17 @@ +CORE +test.c +--function test_function --harness-type call-function +\[test_function\.assertion\.1\] line \d+ assertion test != 42 +^EXIT=10$ +^SIGNAL=0$ +-- +nondet_signed_int +-- +If we use side_effect_expr_nondett then dump_c will generation function calls +to functions with names like nondet_signed_int without declaration. +This can cause problems around usability. + +To fix this, we changed goto-harness to just not use side_effect_expr_nondett +at all. + +This test tests for the absence the use for these things. diff --git a/regression/goto-harness/do-not-use-nondet-for-recursion/test.c b/regression/goto-harness/do-not-use-nondet-for-recursion/test.c new file mode 100644 index 00000000000..47649c76cad --- /dev/null +++ b/regression/goto-harness/do-not-use-nondet-for-recursion/test.c @@ -0,0 +1,11 @@ +struct linked_list +{ + struct linked_list *next; +}; + +void test(struct linked_list *list) +{ + assert(list); + assert(list->next); + assert(!list->next); +} diff --git a/regression/goto-harness/do-not-use-nondet-for-recursion/test.desc b/regression/goto-harness/do-not-use-nondet-for-recursion/test.desc new file mode 100644 index 00000000000..43efcf9fcec --- /dev/null +++ b/regression/goto-harness/do-not-use-nondet-for-recursion/test.desc @@ -0,0 +1,14 @@ +CORE +test.c +--function test --harness-type call-function +\[test.assertion.1\] line \d+ assertion list: SUCCESS +\[test.assertion.2\] line \d+ assertion list->next: FAILURE +\[test.assertion.3\] line \d+ assertion !\(list->next != \(\(struct linked_list \*\).*\)\): FAILURE +should_recurse_nondet +^EXIT=10$ +^SIGNAL=0$ +-- +__CPROVER_nondet_bool +-- +This is to check that we use the new mechanism to decide whether we should recurse +non-deterministically (i.e. without using side_effect_expr_nondett). diff --git a/regression/goto-harness/do-not-use-nondet-for-selecting-pointers-to-treat-as-equal/test.c b/regression/goto-harness/do-not-use-nondet-for-selecting-pointers-to-treat-as-equal/test.c new file mode 100644 index 00000000000..3477023e956 --- /dev/null +++ b/regression/goto-harness/do-not-use-nondet-for-selecting-pointers-to-treat-as-equal/test.c @@ -0,0 +1,8 @@ +void test(int *x, int *y) +{ + assert(x); + assert(y); + assert(x == y); + assert(x != y); + assert(*x == *y); +} diff --git a/regression/goto-harness/do-not-use-nondet-for-selecting-pointers-to-treat-as-equal/test.desc b/regression/goto-harness/do-not-use-nondet-for-selecting-pointers-to-treat-as-equal/test.desc new file mode 100644 index 00000000000..b335d59d79f --- /dev/null +++ b/regression/goto-harness/do-not-use-nondet-for-selecting-pointers-to-treat-as-equal/test.desc @@ -0,0 +1,18 @@ +CORE +test.c +--function test --harness-type call-function --treat-pointers-equal x,y --treat-pointers-equal-maybe +should_make_equal +\[test.assertion.1\] line 3 assertion x: SUCCESS +\[test.assertion.2\] line 4 assertion y: SUCCESS +\[test.assertion.3\] line 5 assertion x == y: FAILURE +\[test.assertion.4\] line 6 assertion x != y: FAILURE +\[test.assertion.5\] line 7 assertion \*x == \*y: FAILURE +^EXIT=10$ +^SIGNAL=0$ +-- +__CPROVER_nondet_bool +-- +We are no longer using side_effect_expr_nondett for nondet primitives, +specifically this is testing that we are using a variable called some variation +of “should_make_equal” (plus some optional postfix) as the condition variable +that assigns the same destination to pointers. diff --git a/src/goto-harness/recursive_initialization.cpp b/src/goto-harness/recursive_initialization.cpp index 58ccb864d67..bca89aec733 100644 --- a/src/goto-harness/recursive_initialization.cpp +++ b/src/goto-harness/recursive_initialization.cpp @@ -169,11 +169,11 @@ void recursive_initializationt::initialize( goto_model.symbol_table.lookup_ref(fun_name); const auto proper_init_case = code_function_callt{ fun_symbol.symbol_expr(), {depth, address_of_exprt{lhs}}}; - + const auto should_make_equal = + get_fresh_local_typed_symexpr("should_make_equal", bool_typet{}); + body.add(code_declt{should_make_equal}); body.add(code_ifthenelset{ - side_effect_expr_nondett{bool_typet{}, source_locationt{}}, - set_equal_case, - proper_init_case}); + should_make_equal, set_equal_case, proper_init_case}); } else { @@ -693,9 +693,12 @@ code_blockt recursive_initializationt::build_pointer_constructor( code_blockt null_and_return{{assign_null, code_returnt{}}}; body.add(code_ifthenelset{conjunction(should_not_recurse), null_and_return}); + const auto should_recurse_nondet = + get_fresh_local_typed_symexpr("should_recurse_nondet", bool_typet{}); + body.add(code_declt{should_recurse_nondet}); exprt::operandst should_recurse_ops{ binary_predicate_exprt{depth, ID_lt, get_symbol_expr(min_depth_var_name)}, - side_effect_expr_nondett{bool_typet{}, source_locationt{}}}; + should_recurse_nondet}; code_blockt then_case{}; code_assignt seen_assign_prev{}; @@ -753,8 +756,10 @@ code_blockt recursive_initializationt::build_array_string_constructor( { index_exprt index_expr{dereference_exprt{result}, from_integer(index, size_type())}; - body.add(code_assignt{ - index_expr, side_effect_expr_nondett{char_type(), source_locationt{}}}); + auto const nondet_char = + get_fresh_local_typed_symexpr("nondet_char", char_type()); + body.add(code_declt{nondet_char}); + body.add(code_assignt{index_expr, nondet_char}); body.add(code_assumet{ notequal_exprt{index_expr, from_integer(0, array_type.subtype())}}); } @@ -830,9 +835,10 @@ code_blockt recursive_initializationt::build_nondet_constructor( { PRECONDITION(result.type().id() == ID_pointer); code_blockt body{}; - body.add(code_assignt{ - dereference_exprt{result}, - side_effect_expr_nondett{result.type().subtype(), source_locationt{}}}); + auto const nondet_symbol = + get_fresh_local_typed_symexpr("nondet", result.type().subtype()); + body.add(code_declt{nondet_symbol}); + body.add(code_assignt{dereference_exprt{result}, nondet_symbol}); return body; } @@ -1029,10 +1035,6 @@ code_blockt recursive_initializationt::build_function_pointer_constructor( const auto function_pointer_selector = get_fresh_local_symexpr("function_pointer_selector"); body.add(code_declt{function_pointer_selector}); - body.add( - code_assignt{function_pointer_selector, - side_effect_expr_nondett{function_pointer_selector.type(), - source_locationt{}}}); auto function_pointer_index = std::size_t{0}; for(const auto &target : targets) From 430ab005aa90ce7fd17291909a621a56cd4184e5 Mon Sep 17 00:00:00 2001 From: Hannes Steffenhagen Date: Tue, 7 Jul 2020 19:23:29 +0100 Subject: [PATCH 2/2] Remove dead method from recursive initialization MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The ::build_array_string_constructor method was originally intended to be used for building C string constructors. Unfortunately as written the condition for calling it was actually impossible to satisfy. This wasn’t noticed so far because similar code is now generated in ::build_dynamic_array_constructor instead. Dead code is a maintenance burden so it’s removed here. --- src/goto-harness/recursive_initialization.cpp | 34 +------------------ src/goto-harness/recursive_initialization.h | 5 --- 2 files changed, 1 insertion(+), 38 deletions(-) diff --git a/src/goto-harness/recursive_initialization.cpp b/src/goto-harness/recursive_initialization.cpp index bca89aec733..d9ae3643ebd 100644 --- a/src/goto-harness/recursive_initialization.cpp +++ b/src/goto-harness/recursive_initialization.cpp @@ -265,9 +265,7 @@ code_blockt recursive_initializationt::build_constructor_body( } if(lhs_name.has_value()) { - if(should_be_treated_as_cstring(*lhs_name) && type == char_type()) - return build_array_string_constructor(result_symbol); - else if(should_be_treated_as_array(*lhs_name)) + if(should_be_treated_as_array(*lhs_name)) { CHECK_RETURN(size_symbol.has_value()); return build_dynamic_array_constructor( @@ -740,36 +738,6 @@ code_blockt recursive_initializationt::build_pointer_constructor( return body; } -code_blockt recursive_initializationt::build_array_string_constructor( - const symbol_exprt &result) const -{ - PRECONDITION(result.type().id() == ID_pointer); - const typet &type = result.type().subtype(); - PRECONDITION(type.id() == ID_array); - PRECONDITION(type.subtype() == char_type()); - const array_typet &array_type = to_array_type(type); - const auto array_size = - numeric_cast_v(to_constant_expr(array_type.size())); - code_blockt body{}; - - for(std::size_t index = 0; index < array_size - 1; index++) - { - index_exprt index_expr{dereference_exprt{result}, - from_integer(index, size_type())}; - auto const nondet_char = - get_fresh_local_typed_symexpr("nondet_char", char_type()); - body.add(code_declt{nondet_char}); - body.add(code_assignt{index_expr, nondet_char}); - body.add(code_assumet{ - notequal_exprt{index_expr, from_integer(0, array_type.subtype())}}); - } - body.add(code_assignt{index_exprt{dereference_exprt{result}, - from_integer(array_size - 1, size_type())}, - from_integer(0, array_type.subtype())}); - - return body; -} - code_blockt recursive_initializationt::build_array_constructor( const exprt &depth, const symbol_exprt &result) diff --git a/src/goto-harness/recursive_initialization.h b/src/goto-harness/recursive_initialization.h index e562388c3ea..5a2b60878d4 100644 --- a/src/goto-harness/recursive_initialization.h +++ b/src/goto-harness/recursive_initialization.h @@ -262,11 +262,6 @@ class recursive_initializationt const exprt &size, const optionalt &lhs_name); - /// Constructor for strings: as array but the last element is zero. - /// \param result: symbol of the result parameter - /// \return the body of the constructor - code_blockt build_array_string_constructor(const symbol_exprt &result) const; - /// Select the specified struct-member to be non-deterministically /// initialized. /// \param lhs: symbol expression of the top structure