Add --export-function-local-symbols to goto-cc

karkhaz · karkhaz · commit 00b179738c19 · 2019-04-01T18:49:00.000-07:00
This switch makes goto-cc do three things:

- retain the implementations of all static functions.
- mangle the names of all static functions.
- unset the file_local flag on all static function symbols.

This feature is intended to help users writing CBMC checks for
file-local functions (i.e., those declared as `static` in the C
language). The intended workflow is: compile the code under test with
the -fkeep-static-functions flag. Then link the code under test with
the 'harness' file, again using the flag. This allows the harness to
call into static functions in the codebase under test.
diff --git a/regression/CMakeLists.txt b/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)
diff --git a/regression/goto-cc-file-local/CMakeLists.txt b/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}"
+)
diff --git a/regression/goto-cc-file-local/chain.sh b/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 <karkhaz@karkhaz.com>
+
+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
diff --git a/regression/goto-cc-file-local/result-multi-file-bad/foo.c b/regression/goto-cc-file-local/result-multi-file-bad/foo.c
@@ -0,0 +1,5 @@
+static int foo()
+{
+  assert(0);
+  return 1;
+}
diff --git a/regression/goto-cc-file-local/result-multi-file-bad/main.c b/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();
+}
diff --git a/regression/goto-cc-file-local/result-multi-file-bad/test.desc b/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
diff --git a/regression/goto-cc-file-local/result-multi-file-good/foo.c b/regression/goto-cc-file-local/result-multi-file-good/foo.c
@@ -0,0 +1,4 @@
+static int foo()
+{
+  return 1;
+}
diff --git a/regression/goto-cc-file-local/result-multi-file-good/main.c b/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();
+}
diff --git a/regression/goto-cc-file-local/result-multi-file-good/test.desc b/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
diff --git a/regression/goto-cc-file-local/result-multi-file-transitive/foo.c b/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();
+}
diff --git a/regression/goto-cc-file-local/result-multi-file-transitive/main.c b/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();
+}
diff --git a/regression/goto-cc-file-local/result-multi-file-transitive/test.desc b/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.
diff --git a/regression/goto-cc-file-local/result-suffix/foo.c b/regression/goto-cc-file-local/result-suffix/foo.c
@@ -0,0 +1,5 @@
+static int foo()
+{
+  assert(0);
+  return 1;
+}
diff --git a/regression/goto-cc-file-local/result-suffix/main.c b/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();
+}
diff --git a/regression/goto-cc-file-local/result-suffix/test.desc b/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.
diff --git a/regression/goto-cc-file-local/symbol-compiled/main.c b/regression/goto-cc-file-local/symbol-compiled/main.c
@@ -0,0 +1,9 @@
+static int foo()
+{
+  return 3;
+}
+
+int main()
+{
+  int x = foo();
+}
diff --git a/regression/goto-cc-file-local/symbol-compiled/test.desc b/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.
diff --git a/regression/goto-cc-file-local/symbol-fully-linked/main.c b/regression/goto-cc-file-local/symbol-fully-linked/main.c
@@ -0,0 +1,9 @@
+static int foo()
+{
+  return 3;
+}
+
+int main()
+{
+  int x = foo();
+}
diff --git a/regression/goto-cc-file-local/symbol-fully-linked/test.desc b/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
diff --git a/regression/goto-cc-file-local/symbol-multi-file/foo.c b/regression/goto-cc-file-local/symbol-multi-file/foo.c
@@ -0,0 +1,4 @@
+static int foo()
+{
+  return 3;
+}
diff --git a/regression/goto-cc-file-local/symbol-multi-file/main.c b/regression/goto-cc-file-local/symbol-multi-file/main.c
@@ -0,0 +1,6 @@
+int foo();
+
+int main()
+{
+  int x = foo();
+}
diff --git a/regression/goto-cc-file-local/symbol-multi-file/test.desc b/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
diff --git a/src/ansi-c/ansi_c_language.cpp b/src/ansi-c/ansi_c_language.cpp
@@ -119,7 +119,8 @@ bool ansi_c_languaget::typecheck(
     return true;
   }
 
-  remove_internal_symbols(new_symbol_table, this->get_message_handler());
+  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;
diff --git a/src/goto-cc/compile.cpp b/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)
+      {
+        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,12 @@ 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;
diff --git a/src/goto-cc/compile.h b/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;
diff --git a/src/goto-cc/gcc_cmdline.cpp b/src/goto-cc/gcc_cmdline.cpp
@@ -26,6 +26,7 @@ const char *goto_cc_options_with_separated_argument[]=
   "--function",
   "--native-compiler",
   "--native-linker",
+  "--mangle-suffix",
   "--print-rejected-preprocessed-source",
   nullptr
 };
@@ -51,6 +52,7 @@ const char *goto_cc_options_without_argument[]=
   "--partial-inlining",
   "--validate-goto-model",
   "-?",
+  "--export-function-local-symbols",
   nullptr
 };
 
diff --git a/src/goto-cc/ms_cl_cmdline.cpp b/src/goto-cc/ms_cl_cmdline.cpp
@@ -46,6 +46,8 @@ const char *non_ms_cl_options[]=
   "--verbosity",
   "--function",
   "--validate-goto-model",
+  "--export-function-local-symbols",
+  "--mangle-suffix",
   nullptr
 };
 // clang-format on
diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile
@@ -32,6 +32,7 @@ SRC = adjust_float_expressions.cpp \
       link_to_library.cpp \
       loop_ids.cpp \
       mm_io.cpp \
+      name_mangler.cpp \
       osx_fat_reader.cpp \
       parameter_assignments.cpp \
       pointer_arithmetic.cpp \
diff --git a/src/goto-programs/name_mangler.cpp b/src/goto-programs/name_mangler.cpp
diff --git a/src/goto-programs/name_mangler.h b/src/goto-programs/name_mangler.h
diff --git a/src/linking/remove_internal_symbols.cpp b/src/linking/remove_internal_symbols.cpp
diff --git a/src/linking/remove_internal_symbols.h b/src/linking/remove_internal_symbols.h

-Original file line number
+Diff line change
@@ @@ -0,0 +1,4 @@ @@
 +static int foo()
 +{
 +  return 1;
 +}