Merge pull request #3457 from danpoe/feature/nondet-return-values

Generate function bodies with nondet return values

Author: danpoe

regression/goto-instrument/generate-function-body-nondet-return-const/main.c

@@ -0,0 +1,9 @@
+#include <assert.h>
+
+const int func();
+
+void main()
+{
+  assert(func() == 0);
+  assert(func() != 0);
+}

regression/goto-instrument/generate-function-body-nondet-return-const/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--generate-function-body func --generate-function-body-options nondet-return
+^SIGNAL=0$
+\[main.assertion.1\] line \d+ assertion func\(\) == 0: FAILURE
+\[main.assertion.2\] line \d+ assertion func\(\) != 0: FAILURE
+--
+^warning: ignoring

regression/goto-instrument/generate-function-body-nondet-return-double-pointer/main.c

@@ -0,0 +1,15 @@
+#include <assert.h>
+#include <stdlib.h>
+
+int **func();
+
+void main()
+{
+  int **p = func();
+
+  assert(p != NULL);
+  assert(*p != NULL);
+
+  assert(**p == 0);
+  assert(**p != 0);
+}

regression/goto-instrument/generate-function-body-nondet-return-double-pointer/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--generate-function-body func --generate-function-body-options nondet-return --min-null-tree-depth 10 --max-nondet-tree-depth 5
+^SIGNAL=0$
+\[main.assertion.1\] line \d+ assertion p != .*(0|(NULL))\)?: SUCCESS
+\[main.assertion.2\] line \d+ assertion \*p != .*(0|(NULL))\)?: SUCCESS
+\[main.assertion.3\] line \d+ assertion \*\*p == 0: FAILURE
+\[main.assertion.4\] line \d+ assertion \*\*p != 0: FAILURE
+--
+^warning: ignoring

regression/goto-instrument/generate-function-body-nondet-return-simple/main.c

@@ -0,0 +1,9 @@
+#include <assert.h>
+
+int func();
+
+void main()
+{
+  assert(func() == 0);
+  assert(func() != 0);
+}

regression/goto-instrument/generate-function-body-nondet-return-simple/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--generate-function-body func --generate-function-body-options nondet-return
+^SIGNAL=0$
+\[main.assertion.1\] line \d+ assertion func\(\) == 0: FAILURE
+\[main.assertion.2\] line \d+ assertion func\(\) != 0: FAILURE
+--
+^warning: ignoring

regression/goto-instrument/generate-function-body-nondet-return-struct-simple-recursion/main.c

@@ -0,0 +1,27 @@
+#include <assert.h>
+#include <stdlib.h>
+
+typedef struct st
+{
+  struct st *next;
+  int data;
+} st_t;
+
+st_t dummy;
+
+st_t *func();
+
+void main()
+{
+  st_t *st = func();
+
+  assert(st != NULL);
+
+  assert(st->next != NULL);
+  assert(st->next->next != NULL);
+  assert(st->next->next->next == NULL);
+
+  assert(st != &dummy);
+  assert(st->next != &dummy);
+  assert(st->next->next != &dummy);
+}

regression/goto-instrument/generate-function-body-nondet-return-struct-simple-recursion/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--generate-function-body func --generate-function-body-options nondet-return --min-null-tree-depth 10 --max-nondet-tree-depth 3
+^EXIT=0$
+^SIGNAL=0$
+VERIFICATION SUCCESSFUL
+--
+^warning: ignoring

src/goto-instrument/generate_function_bodies.cpp

@@ -16,6 +16,7 @@ Author: Diffblue Ltd.
 
 #include <util/arith_tools.h>
 #include <util/format_expr.h>
+#include <util/fresh_symbol.h>
 #include <util/make_unique.h>
 #include <util/string_utils.h>
 
@@ -271,11 +272,46 @@ class havoc_generate_function_bodiest : public generate_function_bodiest
 
     if(function.type.return_type() != void_typet())
     {
+      typet type(function.type.return_type());
+      type.remove(ID_C_constant);
+
+      symbolt &aux_symbol = get_fresh_aux_symbol(
+        type,
+        id2string(function_name),
+        "return_value",
+        function_symbol.location,
+        ID_C,
+        symbol_table);
+
+      aux_symbol.is_static_lifetime = false;
+
+      auto decl_instruction = add_instruction();
+      decl_instruction->make_decl();
+      decl_instruction->code = code_declt(aux_symbol.symbol_expr());
+
+      goto_programt dest;
+
+      havoc_expr_rec(
+        aux_symbol.symbol_expr(),
+        0,
+        function_symbol.location,
+        symbol_table,
+        dest);
+
+      function.body.destructive_append(dest);
+
+      exprt return_expr = typecast_exprt::conditional_cast(
+        aux_symbol.symbol_expr(), function.type.return_type());
+
       auto return_instruction = add_instruction();
       return_instruction->make_return();
-      return_instruction->code = code_returnt(side_effect_expr_nondett(
-        function.type.return_type(), function_symbol.location));
+      return_instruction->code = code_returnt(return_expr);
+
+      auto dead_instruction = add_instruction();
+      dead_instruction->make_dead();
+      dead_instruction->code = code_deadt(aux_symbol.symbol_expr());
     }
+
     auto end_function_instruction = add_instruction();
     end_function_instruction->make_end_function();