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 1b2c84bd523..4f22c72316d 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 { @@ -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( @@ -693,9 +691,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{}; @@ -737,34 +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())}; - body.add(code_assignt{ - index_expr, side_effect_expr_nondett{char_type(), source_locationt{}}}); - 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) @@ -830,9 +803,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 +1003,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) 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