Merge pull request #5412 from NlightNFotis/fix_static_symbols_referencing

Fix static symbols referencing in harness file

Author: NlightNFotis

regression/goto-harness-multi-file-project/static_symbols_referencing/first_one.c

@@ -0,0 +1,25 @@
+#include "first_one.h"
+#include <assert.h>
+
+static int static_function(int a)
+{
+  assert(a == 0);
+  return a;
+}
+
+int non_static_function(int a)
+{
+  return static_function(a);
+}
+
+static int with_matching_signature(int a)
+{
+  assert(0 && "this is not reachable as far as goto-harness is concerned");
+  return 0;
+}
+
+void non_static_with_non_matching_signature(void)
+{
+  // this is just here so `static_with_matching_signature` has a non-file-local use
+  assert(static_with_matching_signature(10) == 10);
+}

regression/goto-harness-multi-file-project/static_symbols_referencing/first_one.h

@@ -0,0 +1 @@
+int non_static_function(int a);

regression/goto-harness-multi-file-project/static_symbols_referencing/second_one.c

@@ -0,0 +1,8 @@
+#include "first_one.h"
+
+int another(int (*fun_ptr)(int), int c)
+{
+  int a = (*fun_ptr)(c);
+
+  return a;
+}

regression/goto-harness-multi-file-project/static_symbols_referencing/test.desc

@@ -0,0 +1,15 @@
+CORE
+dummy.c
+--function another --harness-type call-function
+^EXIT=10$
+^SIGNAL=0$
+\[static_function\.assertion\.1\] line \d assertion a == 0: FAILURE
+\[non_static_with_non_matching_signature\.assertion\.1] line \d+ assertion static_with_matching_signature\(10\) == 10: SUCCESS
+
+^VERIFICATION FAILED$
+--
+^CONVERSION ERROR$
+--
+For this particular error, we care mostly that goto-harness
+doesn't reference static symbols in other files, which would
+cause analysis through CBMC to fail with a conversion error.

src/goto-harness/recursive_initialization.cpp

@@ -8,6 +8,7 @@ Author: Diffblue Ltd.
 
 #include "recursive_initialization.h"
 
+#include <goto-programs/name_mangler.h>
 #include <util/allocate_objects.h>
 #include <util/arith_tools.h>
 #include <util/c_types.h>
@@ -1008,6 +1009,27 @@ code_blockt recursive_initializationt::build_function_pointer_constructor(
   for(const auto &target : targets)
   {
     auto const assign = code_assignt{dereference_exprt{result}, target};
+    auto const sym_to_lookup =
+      target.id() == ID_address_of
+        ?
+        // This is either address of or pointer; in pointer case, we don't
+        // need to do anything. In the address of case, the operand is
+        // a symbol representing a target function.
+        to_symbol_expr(to_address_of_expr(target).object()).get_identifier()
+        : "";
+    // skip referencing globals because the corresponding symbols in the symbol
+    // table are no longer marked as file local.
+    if(has_prefix(id2string(sym_to_lookup), FILE_LOCAL_PREFIX))
+    {
+      continue;
+    }
+    else if(
+      goto_model.get_symbol_table().lookup(sym_to_lookup) &&
+      goto_model.get_symbol_table().lookup(sym_to_lookup)->is_file_local)
+    {
+      continue;
+    }
+
     if(function_pointer_index != targets.size() - 1)
     {
       auto const condition = equal_exprt{

src/goto-programs/name_mangler.cpp

@@ -19,7 +19,7 @@ operator()(const symbolt &src, const std::string &extra_info)
   std::string basename = get_base_name(src.location.get_file().c_str(), false);
 
   std::stringstream ss;
-  ss << CPROVER_PREFIX << "file_local_";
+  ss << FILE_LOCAL_PREFIX;
   ss << std::regex_replace(
           std::regex_replace(basename, forbidden, "_"), multi_under, "_")
      << "_";
@@ -42,7 +42,7 @@ operator()(const symbolt &src, const std::string &extra_info)
   uint32_t eight_nibble_hash = (uint32_t)hash;
 
   std::stringstream ss;
-  ss << CPROVER_PREFIX << "file_local_" << std::setfill('0') << std::setw(8)
-     << std::hex << eight_nibble_hash << "_" << extra_info << "_" << src.name;
+  ss << FILE_LOCAL_PREFIX << std::setfill('0') << std::setw(8) << std::hex
+     << eight_nibble_hash << "_" << extra_info << "_" << src.name;
   return irep_idt(ss.str());
 }

src/goto-programs/name_mangler.h

@@ -13,6 +13,8 @@
 #include <regex>
 #include <vector>
 
+#define FILE_LOCAL_PREFIX CPROVER_PREFIX "file_local_"
+
 /// \brief Mangles the names in an entire program and its symbol table
 ///
 /// The type parameter to this class should be a functor that has a no-arg