Merge pull request #4409 from karkhaz/kk-strip-statics

Allow `static` attribute to be stripped from symbols

Author: tautschnig

regression/CMakeLists.txt

@@ -50,3 +50,4 @@ add_subdirectory(goto-cc-goto-analyzer)
 add_subdirectory(systemc)
 add_subdirectory(contracts)
 add_subdirectory(goto-harness)
+add_subdirectory(goto-cc-file-local)

regression/goto-cc-file-local/CMakeLists.txt

@@ -0,0 +1,9 @@
+if(WIN32)
+    set(is_windows true)
+else()
+    set(is_windows false)
+endif()
+
+add_test_pl_tests(
+    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-instrument> $<TARGET_FILE:cbmc> ${is_windows}"
+)

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

@@ -0,0 +1,77 @@
+#!/usr/bin/env bash
+#
+# Invoke one or more CPROVER tools depending on arguments
+#
+# Author: Kareem Khazem <[email protected]>
+
+is_in()
+{
+  [[ "$2" =~ $1 ]] && return 0 || return 1
+}
+
+ALL_ARGS="$@"
+OUT_FILE=""
+
+if is_in suffix "$ALL_ARGS"; then
+  suffix="--mangle-suffix custom_suffix"
+else
+  suffix=""
+fi
+
+goto_cc=$1
+goto_instrument=$2
+cbmc=$3
+is_windows=$4
+
+for src in *.c; do
+  base=${src%.c}
+  OUT_FILE="${base}.gb"
+
+  if [[ "${is_windows}" == "true" ]]; then
+    "${goto_cc}"                        \
+        /export-function-local-symbols  \
+        /verbosity 10                   \
+        ${suffix}                       \
+        /c"${base}.c"                   \
+        /Fo"${OUT_FILE}"
+
+  elif [[ "${is_windows}" == "false" ]]; then
+    "${goto_cc}"                        \
+        --export-function-local-symbols \
+        --verbosity 10                  \
+        ${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                   \
+        ${suffix}                       \
+        ./*.gb                          \
+        /Fe "${OUT_FILE}"
+
+  elif [[ "${is_windows}" == "false" ]]; then
+    "${goto_cc}"                        \
+        --export-function-local-symbols \
+        --verbosity 10                  \
+        ${suffix}                       \
+        ./*.gb                          \
+        -o "${OUT_FILE}"
+  fi
+fi
+
+if is_in show-symbol-table "$ALL_ARGS"; then
+  "${goto_instrument}" --show-symbol-table "${OUT_FILE}"
+fi
+
+if is_in assertion-check "$ALL_ARGS"; then
+  "${cbmc}" "${OUT_FILE}"
+fi

regression/goto-cc-file-local/result-multi-file-bad/foo.c

@@ -0,0 +1,5 @@
+static int foo()
+{
+  assert(0);
+  return 1;
+}

regression/goto-cc-file-local/result-multi-file-bad/main.c

@@ -0,0 +1,6 @@
+int __CPROVER_file_local_foo_c_foo();
+
+int main()
+{
+  int x = __CPROVER_file_local_foo_c_foo();
+}

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

@@ -0,0 +1,13 @@
+CORE
+main.c
+final-link assertion-check
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+^\*\*\*\* WARNING: no body for function
+--
+Check that CBMC symbolically executes a static function in a different
+file

regression/goto-cc-file-local/result-multi-file-good/foo.c

@@ -0,0 +1,4 @@
+static int foo()
+{
+  return 1;
+}

regression/goto-cc-file-local/result-multi-file-good/main.c

@@ -0,0 +1,6 @@
+int __CPROVER_file_local_foo_c_foo();
+
+int main()
+{
+  int x = __CPROVER_file_local_foo_c_foo();
+}

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

@@ -0,0 +1,13 @@
+CORE
+main.c
+final-link assertion-check
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+^\*\*\*\* WARNING: no body for function
+--
+Check that CBMC symbolically executes a static function in a different
+file

regression/goto-cc-file-local/result-multi-file-transitive/foo.c

@@ -0,0 +1,10 @@
+static int bar()
+{
+  assert(0);
+  return 1;
+}
+
+static int foo()
+{
+  return bar();
+}

regression/goto-cc-file-local/result-multi-file-transitive/main.c

@@ -0,0 +1,6 @@
+int __CPROVER_file_local_foo_c_foo();
+
+int main()
+{
+  int x = __CPROVER_file_local_foo_c_foo();
+}

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

@@ -0,0 +1,14 @@
+CORE
+main.c
+final-link assertion-check
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+^\*\*\*\* WARNING: no body for function
+--
+Check that CBMC symbolically executes static functions in a different
+file. Ensure that static functions are transitively called. Function
+calls don't need to be manually mangled in the same file.

regression/goto-cc-file-local/result-suffix/foo.c

@@ -0,0 +1,5 @@
+static int foo()
+{
+  assert(0);
+  return 1;
+}

regression/goto-cc-file-local/result-suffix/main.c

@@ -0,0 +1,6 @@
+int __CPROVER_file_local_foo_c_custom_suffix_foo();
+
+int main()
+{
+  int x = __CPROVER_file_local_foo_c_custom_suffix_foo();
+}

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

@@ -0,0 +1,13 @@
+CORE
+main.c
+final-link assertion-check suffix
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+^\*\*\*\* WARNING: no body for function
+--
+Check that CBMC symbolically executes a static function in a different
+file. Use a suffix.

regression/goto-cc-file-local/symbol-compiled/main.c

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

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

@@ -0,0 +1,14 @@
+CORE
+main.c
+show-symbol-table
+
+^EXIT=0$
+^SIGNAL=0$
+^Symbol......: __CPROVER_file_local_main_c_foo$
+--
+^warning: ignoring
+^\*\*\*\* WARNING: no body for function
+--
+This is similar to check-symbol-fully-linked, except that we're not
+linking the binary (we're using -c and not subsequently not using it).
+Check that we still keep the file-local implementations.

regression/goto-cc-file-local/symbol-fully-linked/main.c

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

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

@@ -0,0 +1,10 @@
+CORE
+main.c
+final-link show-symbol-table
+
+^EXIT=0$
+^SIGNAL=0$
+^Symbol......: __CPROVER_file_local_main_c_foo$
+--
+^warning: ignoring
+^\*\*\*\* WARNING: no body for function

regression/goto-cc-file-local/symbol-multi-file/foo.c

@@ -0,0 +1,4 @@
+static int foo()
+{
+  return 3;
+}

regression/goto-cc-file-local/symbol-multi-file/main.c

@@ -0,0 +1,6 @@
+int foo();
+
+int main()
+{
+  int x = foo();
+}

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

@@ -0,0 +1,13 @@
+CORE
+main.c
+final-link show-symbol-table
+
+^EXIT=0$
+^SIGNAL=0$
+^Symbol......: __CPROVER_file_local_foo_c_foo$
+--
+^warning: ignoring
+^\*\*\*\* WARNING: no body for function
+--
+Check that a static function in a different file appears in the symbol
+table of the fully-linked binary

src/ansi-c/ansi_c_language.cpp

@@ -105,7 +105,8 @@ bool ansi_c_languaget::parse(
 
 bool ansi_c_languaget::typecheck(
   symbol_tablet &symbol_table,
-  const std::string &module)
+  const std::string &module,
+  const bool keep_file_local)
 {
   symbol_tablet new_symbol_table;
 
@@ -118,7 +119,8 @@ bool ansi_c_languaget::typecheck(
     return true;
   }
 
-  remove_internal_symbols(new_symbol_table);
+  remove_internal_symbols(
+    new_symbol_table, this->get_message_handler(), keep_file_local);
 
   if(linking(symbol_table, new_symbol_table, get_message_handler()))
     return true;

src/ansi-c/ansi_c_language.h

@@ -53,7 +53,19 @@ class ansi_c_languaget:public languaget
 
   bool typecheck(
     symbol_tablet &symbol_table,
-    const std::string &module) override;
+    const std::string &module,
+    const bool keep_file_local) override;
+
+  bool can_keep_file_local() override
+  {
+    return true;
+  }
+
+  bool
+  typecheck(symbol_tablet &symbol_table, const std::string &module) override
+  {
+    return typecheck(symbol_table, module, true);
+  }
 
   void show_parse(std::ostream &out) override;
 

src/cpp/cpp_language.h

@@ -42,9 +42,8 @@ class cpp_languaget:public languaget
   bool generate_support_functions(
     symbol_tablet &symbol_table) override;
 
-  bool typecheck(
-    symbol_tablet &symbol_table,
-    const std::string &module) override;
+  bool
+  typecheck(symbol_tablet &symbol_table, const std::string &module) override;
 
   bool merge_symbol_table(
     symbol_tablet &dest,

src/goto-cc/compile.cpp

@@ -34,6 +34,7 @@ Date: June 2006
 
 #include <goto-programs/goto_convert.h>
 #include <goto-programs/goto_convert_functions.h>
+#include <goto-programs/name_mangler.h>
 #include <goto-programs/read_goto_binary.h>
 #include <goto-programs/validate_goto_model.h>
 #include <goto-programs/write_goto_binary.h>
@@ -401,6 +402,13 @@ bool compilet::compile()
       else
         cfn = output_file_object;
 
+      if(keep_file_local)
+      {
+        function_name_manglert<file_name_manglert> mangler(
+          get_message_handler(), goto_model, file_local_mangle_suffix);
+        mangler.mangle();
+      }
+
       if(write_bin_object_file(cfn, goto_model))
         return true;
 
@@ -593,7 +601,7 @@ bool compilet::parse_source(const std::string &file_name)
     return true;
 
   // we just typecheck one file here
-  if(language_files.typecheck(goto_model.symbol_table))
+  if(language_files.typecheck(goto_model.symbol_table, keep_file_local))
   {
     error() << "CONVERSION ERROR" << eom;
     return true;
@@ -614,7 +622,10 @@ compilet::compilet(cmdlinet &_cmdline, message_handlert &mh, bool Werror)
   : messaget(mh),
     ns(goto_model.symbol_table),
     cmdline(_cmdline),
-    warning_is_fatal(Werror)
+    warning_is_fatal(Werror),
+    keep_file_local(cmdline.isset("export-function-local-symbols")),
+    file_local_mangle_suffix(
+      cmdline.isset("mangle-suffix") ? cmdline.get_value("mangle-suffix") : "")
 {
   mode=COMPILE_LINK_EXECUTABLE;
   echo_file_name=false;

src/goto-cc/compile.h

@@ -96,6 +96,12 @@ class compilet : public messaget
   cmdlinet &cmdline;
   bool warning_is_fatal;
 
+  /// \brief Whether to keep implementations of file-local symbols
+  const bool keep_file_local;
+
+  /// \brief String to include in all mangled names
+  const std::string file_local_mangle_suffix;
+
   std::size_t function_body_count(const goto_functionst &) const;
 
   void add_compiler_specific_defines() const;