Merge pull request #4565 from karkhaz/kk-mangle-basename

Mangle static functions using basename, not path

Author: karkhaz

regression/goto-cc-file-local/chain.sh

@@ -23,45 +23,78 @@ goto_instrument=$2
 cbmc=$3
 is_windows=$4
 
-for src in *.c; do
+if [[ "${is_windows}" != "true" && "${is_windows}" != "false" ]]; then
+  (>&2 echo "\$is_windows should be true or false (got '" "${is_windows}" "')")
+  exit 1
+fi
+
+if is_in use_find "$ALL_ARGS"; then
+  SRC=$(find . -name "*.c")
+else
+  SRC=*.c
+fi
+
+echo "Source files are ${SRC}"
+
+wall=""
+if is_in wall "$ALL_ARGS"; then
+  if [[ "${is_windows}" == "true" ]]; then
+    wall="/Wall"
+  else
+    wall="-Wall"
+  fi
+fi
+
+cnt=0
+for src in ${SRC}; do
+  cnt=$((cnt + 1))
+  out_suffix=""
+  if is_in out-file-counter "$ALL_ARGS"; then
+    out_suffix="_$cnt"
+    if is_in suffix "$ALL_ARGS"; then
+      suffix="--mangle-suffix custom_$cnt"
+    fi
+  fi
+
   base=${src%.c}
-  OUT_FILE="${base}.gb"
+  OUT_FILE=$(basename "${base}${out_suffix}")".gb"
 
   if [[ "${is_windows}" == "true" ]]; then
     "${goto_cc}"                        \
-        /export-function-local-symbols  \
-        /verbosity 10                   \
+        --export-function-local-symbols \
+        --verbosity 10                  \
+        ${wall}                         \
         ${suffix}                       \
-        /c"${base}.c"                   \
+        /c "${base}.c"                  \
         /Fo"${OUT_FILE}"
 
-  elif [[ "${is_windows}" == "false" ]]; then
+  else
     "${goto_cc}"                        \
         --export-function-local-symbols \
         --verbosity 10                  \
+        ${wall}                         \
         ${suffix}                       \
         -c "${base}.c"                  \
         -o "${OUT_FILE}"
-  else
-    (>&2 echo "\$is_windows should be true or false (got '" "${is_windows}" "')")
-    exit 1
   fi
 done
 
 if is_in final-link "$ALL_ARGS"; then
   OUT_FILE=final-link.gb
   if [[ "${is_windows}" == "true" ]]; then
     "${goto_cc}"                        \
-        /export-function-local-symbols  \
-        /verbosity 10                   \
+        --export-function-local-symbols \
+        --verbosity 10                  \
+        ${wall}                         \
         ${suffix}                       \
         ./*.gb                          \
-        /Fe "${OUT_FILE}"
+        /Fe"${OUT_FILE}"
 
-  elif [[ "${is_windows}" == "false" ]]; then
+  else
     "${goto_cc}"                        \
         --export-function-local-symbols \
         --verbosity 10                  \
+        ${wall}                         \
         ${suffix}                       \
         ./*.gb                          \
         -o "${OUT_FILE}"

regression/goto-cc-file-local/name-clash-with-suffix/bar/main.c

@@ -0,0 +1,9 @@
+static int static_fun()
+{
+  return 3;
+}
+
+int bar()
+{
+  return static_fun();
+}

regression/goto-cc-file-local/name-clash-with-suffix/foo/main.c

@@ -0,0 +1,13 @@
+#include <assert.h>
+
+int bar();
+
+static int static_fun()
+{
+  return bar();
+}
+
+int main()
+{
+  assert(static_fun() == 3);
+}

regression/goto-cc-file-local/name-clash-with-suffix/test.desc

@@ -0,0 +1,18 @@
+CORE
+foo/bar/baz/main.c
+use_find out-file-counter final-link wall suffix assertion-check
+^EXIT=0$
+^SIGNAL=0$
+--
+^.*warning: function `__CPROVER_file_local_main_c_static_fun' in module `main' is shadowed by a definition in module `main'
+^warning: ignoring
+^\*\*\*\* WARNING: no body for function
+--
+This test contains two identically-named static functions in two
+identically-named files in different directories. By default, the
+name-mangling scheme would have the static functions identical names when
+they got exported. This test ensures the functions each get a unique
+suffix.
+
+CBMC should work on the finally-linked binary because the functions have
+been correctly mangled.

regression/goto-cc-file-local/name-clash/bar/main.c

@@ -0,0 +1,9 @@
+static int static_fun()
+{
+  return 3;
+}
+
+int bar()
+{
+  return static_fun();
+}

regression/goto-cc-file-local/name-clash/foo/main.c

@@ -0,0 +1,13 @@
+#include <assert.h>
+
+int bar();
+
+static int static_fun()
+{
+  return bar();
+}
+
+int main()
+{
+  assert(static_fun() == 3);
+}

regression/goto-cc-file-local/name-clash/test.desc

@@ -0,0 +1,20 @@
+CORE
+foo/bar/baz/main.c
+use_find out-file-counter final-link wall
+^EXIT=0$
+^SIGNAL=0$
+^.*warning: function `__CPROVER_file_local_main_c_static_fun' in module `main' is shadowed by a definition in module `main'
+--
+^warning: ignoring
+^\*\*\*\* WARNING: no body for function
+--
+This test contains two identically-named static functions in two
+identically-named files in different directories. The name-mangling
+scheme will give the static functions identical names when they get
+exported. This test ensures that the compiler emits a warning about
+this.
+
+CBMC spins forever when run on the final object file, since the `foo'
+implementation of `static_fun` is the one that is kept. There is thus an
+infinite loop where foo/static_fun() calls bar(), and bar() calls
+foo/static_fun() instead of bar/static_fun().

regression/goto-cc-file-local/nested/foo/bar/baz/main.c

@@ -0,0 +1,9 @@
+static int foo()
+{
+  return 3;
+}
+
+int main()
+{
+  int x = foo();
+}

regression/goto-cc-file-local/nested/test.desc

@@ -0,0 +1,15 @@
+CORE
+foo/bar/baz/main.c
+show-symbol-table use_find
+
+^EXIT=0$
+^SIGNAL=0$
+^Symbol......: __CPROVER_file_local_main_c_foo$
+--
+^warning: ignoring
+^\*\*\*\* WARNING: no body for function
+^Symbol......: __CPROVER_file_local_foo_bar_baz_main_c_foo$
+--
+This test checks that a file that we compile several directories up from
+its actual location will get mangled based on its basename, not its
+entire path.

regression/goto-cc-file-local/result-multi-file-bad/test.desc

@@ -1,7 +1,6 @@
 CORE
 main.c
 final-link assertion-check
-
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/goto-cc-file-local/result-multi-file-good/test.desc

@@ -1,7 +1,6 @@
 CORE
 main.c
 final-link assertion-check
-
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/goto-cc-file-local/result-multi-file-transitive/test.desc

@@ -1,7 +1,6 @@
 CORE
 main.c
 final-link assertion-check
-
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/goto-cc-file-local/result-suffix/test.desc

@@ -1,7 +1,6 @@
 CORE
 main.c
 final-link assertion-check suffix
-
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/goto-cc-file-local/symbol-compiled/test.desc

@@ -1,7 +1,6 @@
 CORE
 main.c
 show-symbol-table
-
 ^EXIT=0$
 ^SIGNAL=0$
 ^Symbol......: __CPROVER_file_local_main_c_foo$

regression/goto-cc-file-local/symbol-fully-linked/test.desc

@@ -1,7 +1,6 @@
 CORE
 main.c
 final-link show-symbol-table
-
 ^EXIT=0$
 ^SIGNAL=0$
 ^Symbol......: __CPROVER_file_local_main_c_foo$

regression/goto-cc-file-local/symbol-multi-file/test.desc

@@ -1,7 +1,6 @@
 CORE
 main.c
 final-link show-symbol-table
-
 ^EXIT=0$
 ^SIGNAL=0$
 ^Symbol......: __CPROVER_file_local_foo_c_foo$

src/goto-cc/ms_cl_cmdline.cpp

@@ -61,7 +61,9 @@ bool ms_cl_cmdlinet::parse(const std::vector<std::string> &arguments)
     {
       process_non_cl_option(arguments[i]);
 
-      if(arguments[i] == "--verbosity" || arguments[i] == "--function")
+      if(
+        arguments[i] == "--verbosity" || arguments[i] == "--function" ||
+        arguments[i] == "--mangle-suffix")
       {
         if(i < arguments.size() - 1)
         {

src/goto-programs/name_mangler.cpp

@@ -8,18 +8,20 @@ Author: Kareem Khazem <[email protected]>, 2019
 
 #include "name_mangler.h"
 
+#include <util/get_base_name.h>
+
 #include <iomanip>
 #include <sstream>
 
 irep_idt file_name_manglert::
 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 << std::regex_replace(
-          std::regex_replace(src.location.get_file().c_str(), forbidden, "_"),
-          multi_under,
-          "_")
+          std::regex_replace(basename, forbidden, "_"), multi_under, "_")
      << "_";
 
   if(extra_info != "")