Merge pull request #5409 from hannes-steffenhagen-diffblue/fix/do_not…

…_use_side_effect_expr_nondett_in_goto_harness

Do not use side_effect_expr_nondett in recursive_initialization

regression/goto-harness/do-not-use-nondet-for-primitives/test.c

@@ -0,0 +1,6 @@
+#include <assert.h>
+
+void test_function(int test)
+{
+  assert(test != 42);
+}

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.

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);
+}

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).

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);
+}

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.

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<std::size_t>(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)

src/goto-harness/recursive_initialization.h

@@ -262,11 +262,6 @@ class recursive_initializationt
     const exprt &size,
     const optionalt<irep_idt> &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