Prerequisite PR diffblue#5176 -- do not review

petr-bauch · petr-bauch · commit 831fa1a3be3d · 2019-11-13T09:01:47.000Z
diff --git a/regression/goto-harness/function_pointer_argument/test.c b/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);
+}
diff --git a/regression/goto-harness/function_pointer_argument/test.desc b/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
diff --git a/regression/goto-harness/function_pointer_nullable/test.c b/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;
+}
diff --git a/regression/goto-harness/function_pointer_nullable/test.desc b/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
diff --git a/regression/goto-harness/mixed-constructors/test.c b/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);
+}
diff --git a/regression/goto-harness/mixed-constructors/test.desc b/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
diff --git a/regression/goto-harness/parameter_and_global_variable_distinction/test.c b/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));
+}
diff --git a/regression/goto-harness/parameter_and_global_variable_distinction/test.desc b/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
diff --git a/regression/goto-harness/pointer-function-parameters-equal-simple/main.c b/regression/goto-harness/pointer-function-parameters-equal-simple/main.c
@@ -0,0 +1,16 @@
+#include <assert.h>
+#include <stdlib.h>
+
+typedef struct st
+{
+  struct st *next;
+  int data;
+} st_t;
+
+void func(st_t *p, st_t *q)
+{
+  assert(p != NULL);
+  assert(p->next != NULL);
+
+  assert(p == q);
+}
diff --git a/regression/goto-harness/pointer-function-parameters-equal-simple/test.desc b/regression/goto-harness/pointer-function-parameters-equal-simple/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--function func --min-null-tree-depth 10 --max-nondet-tree-depth 3 --harness-type call-function --treat-pointers-equal p,q
+^EXIT=0$
+^SIGNAL=0$
+VERIFICATION SUCCESSFUL
+--
+^warning: ignoring
diff --git a/src/goto-harness/common_harness_generator_options.h b/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
diff --git a/src/goto-harness/function_call_harness_generator.cpp b/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>
@@ -48,6 +49,9 @@ struct function_call_harness_generatort::implt
   std::set<irep_idt> function_parameters_to_treat_as_arrays;
   std::set<irep_idt> function_arguments_to_treat_as_arrays;
 
+  std::set<irep_idt> function_parameters_to_treat_equal;
+  std::set<irep_idt> function_arguments_to_treat_equal;
+
   std::set<irep_idt> function_parameters_to_treat_as_cstrings;
   std::set<irep_idt> function_arguments_to_treat_as_cstrings;
 
@@ -69,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 correspond 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(
@@ -112,6 +126,16 @@ void function_call_harness_generatort::handle_option(
     p_impl->function_parameters_to_treat_as_arrays.insert(
       values.begin(), values.end());
   }
+  else if(option == FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_OPT)
+  {
+    for(auto const &value : values)
+    {
+      for(auto const &param_id : split_string(value, ','))
+      {
+        p_impl->function_parameters_to_treat_equal.insert(param_id);
+      }
+    }
+  }
   else if(option == FUNCTION_HARNESS_GENERATOR_ASSOCIATED_ARRAY_SIZE_OPT)
   {
     for(auto const &array_size_pair : values)
@@ -183,13 +207,17 @@ void function_call_harness_generatort::implt::generate(
   recursive_initialization_config.mode = function_to_call.mode;
   recursive_initialization_config.pointers_to_treat_as_arrays =
     function_arguments_to_treat_as_arrays;
+  recursive_initialization_config.pointers_to_treat_equal =
+    function_arguments_to_treat_equal;
   recursive_initialization_config.array_name_to_associated_array_size_variable =
     function_argument_to_associated_array_size;
   for(const auto &pair : function_argument_to_associated_array_size)
   {
     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>(
@@ -238,14 +266,14 @@ void function_call_harness_generatort::implt::generate_initialisation_code_for(
 {
   recursive_initialization->initialize(
     lhs, from_integer(0, signed_int_type()), block);
-  if(lhs.type().id() == ID_pointer)
+  if(recursive_initialization->needs_freeing(lhs))
     global_pointers.insert(to_symbol_expr(lhs));
 }
 
 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};
@@ -258,6 +286,92 @@ void function_call_harness_generatort::validate_options(
       "--" COMMON_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT
       " --" COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT};
   }
+
+  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 &pointer_id : p_impl->function_parameters_to_treat_equal)
+  {
+    std::string decorated_pointer_id =
+      id2string(p_impl->function) + "::" + id2string(pointer_id);
+    bool is_a_param = false;
+    typet common_type = empty_typet{};
+    for(auto const &formal_param : ftype.parameters())
+    {
+      if(formal_param.get_identifier() == decorated_pointer_id)
+      {
+        is_a_param = true;
+        if(formal_param.type().id() != ID_pointer)
+        {
+          throw invalid_command_line_argument_exceptiont{
+            id2string(pointer_id) + " is not a pointer parameter",
+            "--" FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_OPT};
+        }
+        if(common_type.id() != ID_empty)
+        {
+          if(common_type != formal_param.type())
+          {
+            throw invalid_command_line_argument_exceptiont{
+              "pointer arguments of conflicting type",
+              "--" FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_OPT};
+          }
+        }
+        else
+          common_type = formal_param.type();
+      }
+    }
+    if(!is_a_param)
+    {
+      throw invalid_command_line_argument_exceptiont{
+        id2string(pointer_id) + " is not a parameter",
+        "--" FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_OPT};
+    }
+  }
+
+  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 &
@@ -348,6 +462,11 @@ function_call_harness_generatort::implt::declare_arguments(
       function_arguments_to_treat_as_cstrings.insert(argument_name);
     }
 
+    if(function_parameters_to_treat_equal.count(parameter_name) != 0)
+    {
+      function_arguments_to_treat_equal.insert(argument_name);
+    }
+
     auto it = function_parameter_to_associated_array_size.find(parameter_name);
     if(it != function_parameter_to_associated_array_size.end())
     {
@@ -377,7 +496,7 @@ void function_call_harness_generatort::implt::call_function(
   for(auto const &argument : arguments)
   {
     generate_initialisation_code_for(function_body, argument);
-    if(argument.type().id() == ID_pointer)
+    if(recursive_initialization->needs_freeing(argument))
       global_pointers.insert(to_symbol_expr(argument));
   }
   code_function_callt function_call{function_to_call.symbol_expr(),
@@ -386,3 +505,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;
+}
diff --git a/src/goto-harness/function_harness_generator_options.h b/src/goto-harness/function_harness_generator_options.h
diff --git a/src/goto-harness/recursive_initialization.cpp b/src/goto-harness/recursive_initialization.cpp
diff --git a/src/goto-harness/recursive_initialization.h b/src/goto-harness/recursive_initialization.h
