Merge pull request #5290 from thk123/goto-harness-void-star-pointers

Add support for void* pointers in goto-harness

Author: Thomas Kiley

regression/goto-harness/do_not_nondet_globals_by_default/main.c

@@ -1,3 +1,5 @@
+#include <assert.h>
+
 int a_global;
 
 void entry_function(void)

regression/goto-harness/havoc-global-int-01/main.c

@@ -1,3 +1,5 @@
+#include <assert.h>
+
 int x = 1;
 
 int main()

regression/goto-harness/void-star-pointer/main.c

@@ -0,0 +1,21 @@
+#include <assert.h>
+#include <stdbool.h>
+
+void test_function(void *input)
+{
+  assert(input == 0);
+}
+
+void test_void_array(void *input_array[10])
+{
+  __CPROVER_assume(input_array != 0);
+  assert(input_array[0] == 0);
+  assert(false);
+}
+
+void test_ptr_array(void **input_array)
+{
+  __CPROVER_assume(input_array != 0);
+  assert(input_array[0] == 0);
+  assert(false);
+}

regression/goto-harness/void-star-pointer/test-array-as-array.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--harness-type call-function --function test_ptr_array --treat-pointer-as-array input_array
+\[test_ptr_array\.assertion\.1\] line \d+ assertion input_array\[0\] == 0: SUCCESS
+\[test_ptr_array\.assertion\.2\] line \d+ assertion .*: FAILURE
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Ensure the harness is able to initalize an array of void* pointers where
+the array is non-null, but the elements are null, if the void** is treated as an
+array.

regression/goto-harness/void-star-pointer/test-array.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--harness-type call-function --function test_void_array
+\[test_void_array\.assertion\.1\] line \d+ assertion input_array\[0\] == 0: SUCCESS
+\[test_void_array\.assertion\.2\] line \d+ assertion .*: FAILURE
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Ensure the harness is able to initalize an array of void* pointers where
+the array is non-null, but the elements are null.

regression/goto-harness/void-star-pointer/test-as-array.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--harness-type call-function --function test_function --treat-pointer-as-array input
+\[test_function\.assertion\.1\] line \d+ assertion input == 0: SUCCESS
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+Ensure the harness is able to initalize a void* ptr to a null value, even when
+the parameter is specified to be treated as an array.

regression/goto-harness/void-star-pointer/test-as-c-string.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--harness-type call-function --function test_function --treat-pointer-as-cstring input
+\[test_function\.assertion\.1\] line \d+ assertion input == 0: SUCCESS
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+Ensure the harness is able to initalize a void* ptr to a null value, even when
+the parameter is specified to be treated as a string.

regression/goto-harness/void-star-pointer/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--harness-type call-function --function test_function
+\[test_function\.assertion\.1\] line \d+ assertion input == 0: SUCCESS
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+Ensure the harness is able to initalize a void* ptr to a null value.

src/goto-harness/recursive_initialization.cpp

@@ -230,6 +230,15 @@ void recursive_initializationt::initialize(
                                {depth, address_of_exprt{lhs}}});
 }
 
+code_blockt build_null_pointer(const symbol_exprt &result_symbol)
+{
+  const typet &type_to_construct = result_symbol.type().subtype();
+  const null_pointer_exprt nullptr_expr{to_pointer_type(type_to_construct)};
+  const code_assignt assign_null{dereference_exprt{result_symbol},
+                                 nullptr_expr};
+  return code_blockt{{assign_null, code_returnt{}}};
+}
+
 code_blockt recursive_initializationt::build_constructor_body(
   const exprt &depth_symbol,
   const symbol_exprt &result_symbol,
@@ -249,6 +258,11 @@ code_blockt recursive_initializationt::build_constructor_body(
     {
       return build_function_pointer_constructor(result_symbol, is_nullable);
     }
+    if(type.subtype().id() == ID_empty)
+    {
+      // always initalize void* pointers as NULL
+      return build_null_pointer(result_symbol);
+    }
     if(lhs_name.has_value())
     {
       if(should_be_treated_as_cstring(*lhs_name) && type == char_type())
@@ -620,15 +634,16 @@ code_blockt recursive_initializationt::build_pointer_constructor(
   PRECONDITION(result.type().id() == ID_pointer);
   const typet &type = result.type().subtype();
   PRECONDITION(type.id() == ID_pointer);
+  PRECONDITION(type.subtype().id() != ID_empty);
 
   code_blockt body{};
-
   // build:
   // void type_constructor_ptr_T(int depth, T** result)
   // {
   //   if(has_seen && depth >= max_depth)
   //     *result=NULL;
-  //   else if(depth < min_null_tree_depth || nondet()) {
+  //     return
+  //   if(nondet()) {
   //     size_t has_seen_prev;
   //     has_seen_prev = T_has_seen;
   //     T_has_seen = 1;
@@ -655,10 +670,8 @@ code_blockt recursive_initializationt::build_pointer_constructor(
   }
 
   null_pointer_exprt nullptr_expr{pointer_type(type.subtype())};
-  code_blockt null_and_return{};
-  code_assignt assign_null{dereference_exprt{result}, nullptr_expr};
-  null_and_return.add(assign_null);
-  null_and_return.add(code_returnt{});
+  const code_assignt assign_null{dereference_exprt{result}, nullptr_expr};
+  code_blockt null_and_return{{assign_null, code_returnt{}}};
   body.add(code_ifthenelset{conjunction(should_not_recurse), null_and_return});
 
   exprt::operandst should_recurse_ops{
@@ -787,6 +800,7 @@ code_blockt recursive_initializationt::build_dynamic_array_constructor(
   const typet &pointer_type = result.type().subtype();
   PRECONDITION(pointer_type.id() == ID_pointer);
   const typet &element_type = pointer_type.subtype();
+  PRECONDITION(element_type.id() != ID_empty);
 
   // builds:
   // void type_constructor_ptr_T(int depth, T** result, int* size)