Merge pull request #5176 from NlightNFotis/feature/function-pointer-nondet-harness

Function pointer non-det initialisation in goto-harness [depends-on: #5171]

Author: NlightNFotis

regression/goto-harness/function_pointer_argument/test.c

@@ -0,0 +1,20 @@
+#include <assert.h>
+
+typedef int (*fptr)(int a, int b);
+
+int max_normal(int first, int second)
+{
+  return first >= second ? first : second;
+}
+
+int max_crazy(int first, int second)
+{
+  return first >= second ? second : first;
+}
+
+void use_fptr(fptr max, int first, int second)
+{
+  int m = max(first, second);
+  assert(m == first || m == second);
+  assert(m >= first && m >= second);
+}

regression/goto-harness/function_pointer_argument/test.desc

@@ -0,0 +1,9 @@
+CORE
+test.c
+--harness-type call-function --harness-function-name harness --function use_fptr
+^EXIT=10$
+^SIGNAL=0$
+\[use_fptr.assertion.1\] line \d+ assertion m == first \|\| m == second: SUCCESS
+\[use_fptr.assertion.2\] line \d+ assertion m >= first && m >= second: FAILURE
+--
+^warning: ignoring

regression/goto-harness/function_pointer_nullable/test.c

@@ -0,0 +1,18 @@
+#include <assert.h>
+#include <stdlib.h>
+
+typedef int (*fptr_t)(void);
+
+void entry_point(fptr_t f, fptr_t f_but_may_be_null)
+{
+  assert(f != (void *)0);                 // expected to succeed
+  assert(f == (void *)0);                 // expected to fail
+  assert(f_but_may_be_null != (void *)0); // expected to fail
+  assert(f_but_may_be_null == (void *)0); // expected to fail
+  assert(f_but_may_be_null == (void *)0 || f() == f_but_may_be_null());
+}
+
+int f(void)
+{
+  return 42;
+}

regression/goto-harness/function_pointer_nullable/test.desc

@@ -0,0 +1,12 @@
+CORE
+test.c
+--harness-type call-function --function entry_point --function-pointer-can-be-null entry_point::f_but_may_be_null
+^EXIT=10$
+^SIGNAL=0$
+\[entry_point.assertion.1\] line \d+ assertion f != \(void \*\)0: SUCCESS
+\[entry_point.assertion.2\] line \d+ assertion f == \(void \*\)0: FAILURE
+\[entry_point.assertion.3\] line \d+ assertion f_but_may_be_null != \(void \*\)0: FAILURE
+\[entry_point.assertion.4\] line \d+ assertion f_but_may_be_null == \(void \*\)0: FAILURE
+\[entry_point.assertion.5\] line \d+ assertion f_but_may_be_null == \(void \*\)0 || f\(\) == f_but_may_be_null\(\): SUCCESS
+--
+^warning: ignoring

regression/goto-harness/mixed-constructors/test.c

@@ -0,0 +1,5 @@
+void entry_point(int *array_with_size, int size, int *array_without_size)
+{
+  assert(array_with_size != (void *)0);
+  assert(array_with_size != (void *)0);
+}

regression/goto-harness/mixed-constructors/test.desc

@@ -0,0 +1,8 @@
+CORE
+test.c
+--function entry_point --harness-type call-function --associated-array-size array_with_size:size
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+call to '\w+': not enough arguments, inserting non-deterministic value

regression/goto-harness/parameter_and_global_variable_distinction/test.c

@@ -0,0 +1,18 @@
+#include <assert.h>
+
+typedef int (*fptr_t)(void);
+
+fptr_t f;
+
+int call_f()
+{
+  assert(f != ((void *)0));
+  return f();
+}
+
+void function(fptr_t f)
+{
+  if(f != ((void *)0))
+    assert(f() == call_f());
+  assert(f != ((void *)0));
+}

regression/goto-harness/parameter_and_global_variable_distinction/test.desc

@@ -0,0 +1,10 @@
+CORE
+test.c
+--harness-type call-function --function function --function-pointer-can-be-null function::f
+^EXIT=10$
+^SIGNAL=0$
+\[function.assertion.1\] line \d+ assertion f\(\) == call_f\(\): SUCCESS
+\[function.assertion.2\] line \d+ assertion f != \(\(void \*\)0\): FAILURE
+\[call_f.assertion.1\] line \d+ assertion f != \(\(void \*\)0\): SUCCESS
+--
+^warning: ignoring

src/goto-harness/common_harness_generator_options.h

@@ -14,13 +14,16 @@ Author: Diffblue Ltd.
   "max-nondet-tree-depth"
 #define COMMON_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT "min-array-size"
 #define COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT "max-array-size"
+#define COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT              \
+  "function-pointer-can-be-null"
 
 // clang-format off
 #define COMMON_HARNESS_GENERATOR_OPTIONS                                       \
   "(" COMMON_HARNESS_GENERATOR_MIN_NULL_TREE_DEPTH_OPT "):"                    \
   "(" COMMON_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT "):"                  \
   "(" COMMON_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT "):"                         \
   "(" COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT "):"                         \
+  "(" COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT "):"           \
 // COMMON_HARNESS_GENERATOR_OPTIONS
 
 // clang-format on
@@ -39,6 +42,9 @@ Author: Diffblue Ltd.
   "--" COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT                             \
   " N            maximum size of dynamically created arrays\n"                 \
   "                              (default: 2)\n"                               \
+  "--" COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT               \
+  " <function-name>,  name of the function(s) pointer parameters\n"            \
+  "              that can be NULL pointing."
   // COMMON_HARNESS_GENERATOR_HELP
 
 // clang-format on

src/goto-harness/function_call_harness_generator.cpp

@@ -12,6 +12,7 @@ Author: Diffblue Ltd.
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/exception_utils.h>
+#include <util/prefix.h>
 #include <util/std_code.h>
 #include <util/std_expr.h>
 #include <util/string2int.h>
@@ -72,14 +73,24 @@ struct function_call_harness_generatort::implt
   void ensure_harness_does_not_already_exist();
   /// Update the goto-model with the new harness function.
   void add_harness_function_to_goto_model(code_blockt function_body);
-  /// declare local variables for each of the parameters of the entry function
+  /// Declare local variables for each of the parameters of the entry function
   /// and return them
   code_function_callt::argumentst declare_arguments(code_blockt &function_body);
-  /// write initialisation code for each of the arguments into function_body,
+  /// Write initialisation code for each of the arguments into function_body,
   /// then insert a call to the entry function with the arguments
   void call_function(
     const code_function_callt::argumentst &arguments,
     code_blockt &function_body);
+  /// For function parameters that are pointers to functions we want to
+  /// be able to specify whether or not they can be NULL. To disambiguate
+  /// this specification from that for a global variable of the same name,
+  /// we prepend the name of the function to the parameter name. However,
+  /// what is actually being initialised in the implementation is not the
+  /// parameter itself, but a corresponding function argument (local variable
+  /// of the harness function). We need a mapping from function parameter
+  /// name to function argument names, and this is what this function does.
+  std::unordered_set<irep_idt>
+  map_function_parameters_to_function_argument_names();
 };
 
 function_call_harness_generatort::function_call_harness_generatort(
@@ -173,6 +184,30 @@ void function_call_harness_generatort::handle_option(
   {
     p_impl->recursive_initialization_config.arguments_may_be_equal = true;
   }
+  else if(option == COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT)
+  {
+    std::transform(
+      values.begin(),
+      values.end(),
+      std::inserter(
+        p_impl->recursive_initialization_config
+          .potential_null_function_pointers,
+        p_impl->recursive_initialization_config.potential_null_function_pointers
+          .end()),
+      [](const std::string &opt) -> irep_idt { return irep_idt{opt}; });
+  }
+  else if(option == COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT)
+  {
+    std::transform(
+      values.begin(),
+      values.end(),
+      std::inserter(
+        p_impl->recursive_initialization_config
+          .potential_null_function_pointers,
+        p_impl->recursive_initialization_config.potential_null_function_pointers
+          .end()),
+      [](const std::string &opt) -> irep_idt { return irep_idt{opt}; });
+  }
   else
   {
     throw invalid_command_line_argument_exceptiont{
@@ -214,6 +249,8 @@ void function_call_harness_generatort::implt::generate(
     recursive_initialization_config.variables_that_hold_array_sizes.insert(
       pair.second);
   }
+  recursive_initialization_config.potential_null_function_pointers =
+    map_function_parameters_to_function_argument_names();
   recursive_initialization_config.pointers_to_treat_as_cstrings =
     function_arguments_to_treat_as_cstrings;
   recursive_initialization = util_make_unique<recursive_initializationt>(
@@ -269,7 +306,7 @@ void function_call_harness_generatort::implt::generate_initialisation_code_for(
 void function_call_harness_generatort::validate_options(
   const goto_modelt &goto_model)
 {
-  if(p_impl->function == ID_empty)
+  if(p_impl->function == ID_empty_string)
     throw invalid_command_line_argument_exceptiont{
       "required parameter entry function not set",
       "--" FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT};
@@ -283,8 +320,17 @@ void function_call_harness_generatort::validate_options(
       " --" COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT};
   }
 
-  auto function_to_call = goto_model.symbol_table.lookup_ref(p_impl->function);
-  auto ftype = to_code_type(function_to_call.type);
+  const auto function_to_call_pointer =
+    goto_model.symbol_table.lookup(p_impl->function);
+  if(function_to_call_pointer == nullptr)
+  {
+    throw invalid_command_line_argument_exceptiont{
+      "entry function `" + id2string(p_impl->function) +
+        "' does not exist in the symbol table",
+      "--" FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT};
+  }
+  const auto &function_to_call = *function_to_call_pointer;
+  const auto &ftype = to_code_type(function_to_call.type);
   for(auto const &equal_cluster : p_impl->function_parameters_to_treat_equal)
   {
     for(auto const &pointer_id : equal_cluster)
@@ -325,6 +371,43 @@ void function_call_harness_generatort::validate_options(
       }
     }
   }
+
+  const namespacet ns{goto_model.symbol_table};
+
+  // Make sure all function pointers that the user asks are nullable are
+  // present in the symbol table.
+  for(const auto &nullable :
+      p_impl->recursive_initialization_config.potential_null_function_pointers)
+  {
+    const auto &function_pointer_symbol_pointer =
+      goto_model.symbol_table.lookup(nullable);
+
+    if(function_pointer_symbol_pointer == nullptr)
+    {
+      throw invalid_command_line_argument_exceptiont{
+        "nullable function pointer `" + id2string(nullable) +
+          "' not found in symbol table",
+        "--" COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT};
+    }
+
+    const auto &function_pointer_type =
+      ns.follow(function_pointer_symbol_pointer->type);
+
+    if(!can_cast_type<pointer_typet>(function_pointer_type))
+    {
+      throw invalid_command_line_argument_exceptiont{
+        "`" + id2string(nullable) + "' is not a pointer",
+        "--" COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT};
+    }
+
+    if(!can_cast_type<code_typet>(
+         to_pointer_type(function_pointer_type).subtype()))
+    {
+      throw invalid_command_line_argument_exceptiont{
+        "`" + id2string(nullable) + "' is not pointing to a function",
+        "--" COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT};
+    }
+  }
 }
 
 const symbolt &
@@ -469,3 +552,25 @@ void function_call_harness_generatort::implt::call_function(
 
   function_body.add(std::move(function_call));
 }
+
+std::unordered_set<irep_idt> function_call_harness_generatort::implt::
+  map_function_parameters_to_function_argument_names()
+{
+  std::unordered_set<irep_idt> nullables;
+  for(const auto &nullable :
+      recursive_initialization_config.potential_null_function_pointers)
+  {
+    const auto &nullable_name = id2string(nullable);
+    const auto &function_prefix = id2string(function) + "::";
+    if(has_prefix(nullable_name, function_prefix))
+    {
+      nullables.insert(
+        "__goto_harness::" + nullable_name.substr(function_prefix.size()));
+    }
+    else
+    {
+      nullables.insert(nullable_name);
+    }
+  }
+  return nullables;
+}