Do not use side_effect_expr_nondett in recursive_initialization

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

Author: hannes-steffenhagen-diffblue

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
         {
@@ -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)