Add docs for --export-file-local-symbols

doc/architectural/static-functions.md

@@ -0,0 +1,161 @@
+\ingroup module_hidden
+\page modular-verification-static Modular Verification of Static Functions
+
+\section verification-of-static Modular Verification of Static Functions
+
+\author Kareem Khazem
+
+This page describes how to use CBMC on static functions.
+
+\tableofcontents
+
+CBMC can check libraries and other codebases that expose several
+entry points. To do this, users typically write a *harness* that
+captures the entry points' API contract, and that calls into the API
+with unconstrained values. The example below shows such a library and
+harness:
+
+\code{.c}
+void public_api_function(const int *a, int *b)
+{
+  // ...
+  private_function(a, b);
+  // ...
+}
+
+static void private_function(const int *a, int *b)
+{
+  // ...
+}
+\endcode
+
+The harness sets up some assumptions and then calls into the API:
+
+\code{.c}
+void public_api_function(int *a, int *b);
+
+void harness()
+{
+  int a, b;
+  __CPROVER_assume(a < 10);
+  __CPROVER_assume(a >= 0);
+  public_api_function(&a, &b);
+  __CPROVER_assert(b != a);
+}
+\endcode
+
+The following commands build and check this function:
+
+\code{.sh}
+> goto-cc -c -o library.o library.c
+> goto-cc -c -o harness.o harness.c
+> goto-cc -o to_check.gb library.o harness.o
+> cbmc --function harness to_check.gb
+\endcode
+
+\subsection stubbing-out-static Stubbing out static functions
+
+For performance reasons, it might be desirable to analyze the API
+function independently of the static function. We can analyze the API
+function by "stubbing out" the static function, replacing it with a
+function that does nothing apart from asserting that its inputs satisfy
+the function's contract. ("Stubbing out" a function is sometimes known
+as "modelling" or "abstracting it out".) Add the following to
+`harness.c`:
+
+\code{.c}
+static void private_function(const int *a, int *b)
+{
+  __CPROVER_assert( private_function_precondition );
+  __CPROVER_assume( private_function_postcondition );
+}
+\endcode
+
+And build as follows, stripping the original static function out of its
+object file:
+
+\code{.sh}
+> goto-cc -c -o library.o library.c
+> goto-instrument --remove-function-body private_function library.o library-no-private.o
+>
+> goto-cc -c -o harness.o harness.c
+>
+> # The stub in the harness overrides the implementation of
+> # private_function whose body has been removed
+> goto-cc -o to_check.gb library-no-private.o harness.o
+> cbmc --function harness to_check.gb
+\endcode
+
+\subsection checking-static Separately checking static functions
+
+We should now also write a harness for `private_function`. However,
+since that function is marked `static`, it is not possible for functions
+in external files to call it. We can write and link a harness by
+stripping the `static` attribute from `private_function` using goto-cc's
+`--export-file-local-symbols` flag.
+
+\code{.sh}
+> goto-cc -c -o --export-file-local-symbols library_with_static.o library.c
+\endcode
+
+`library_with_static.o` now contains an implementation of `private_function()`
+with a mangled name. We can display the mangled name with goto-instrument:
+
+\code{.sh}
+> goto-instrument --show-symbol-table library_with_static.o | grep -B1 -A1 "Pretty name.: private_function"
+Symbol......: __CPROVER_file_local_library_c_private_function
+Pretty name.: private_function
+Module......: private_function
+\endcode
+
+When we write a harness for the static function, we ensure that we call
+the mangled name:
+
+\code{.c}
+void harness()
+{
+  int a, b;
+
+  __CPROVER_assume( private_function_precondition );
+
+  // Call the static function
+  __CPROVER_file_local_library_c_private_function(&a, &b);
+
+  __CPROVER_assert( private_function_postcondition );
+}
+\endcode
+
+We can then link this harness to the object file with exported symbols
+and run CBMC as usual.
+
+\code{.sh}
+> goto-cc -c -o private_harness.o private_harness.c
+> goto-cc -o to_test.gb private_harness.o library_with_static.o
+> cbmc --function harness to_test.gb
+\endcode
+
+It is possible that CBMC will generate the same mangled name for two
+different static functions. This happens when the functions have the
+same name and are written in same-named files that live in different
+directories. In the following codebase, the two `qux` functions will
+both have their names mangled to `__CPROVER_file_local_b_c_qux`, and
+so any harness that requires both of those files will fail to link.
+
+    project
+    |
+    \_ foo
+    |  |
+    |  \_ a.c
+    |  \_ b.c <- contains static function "qux"
+    |
+    \_ bar
+       |
+       \_ c.c
+       \_ b.c <- also contains static function "qux"
+
+The solution is to use the `--mangle-suffix` option to goto-cc. This
+allows you to specify a different suffix for name-mangling. By
+specifying a custom, different suffix for each of the two files, the
+mangled names are unique and the files can be successfully linked.
+
+More examples are in `regression/goto-cc-file-local`.

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

@@ -63,7 +63,7 @@ for src in ${SRC}; do
 
   if [[ "${is_windows}" == "true" ]]; then
     "${goto_cc}"                        \
-        --export-function-local-symbols \
+        --export-file-local-symbols \
         --verbosity 10                  \
         ${wall}                         \
         ${suffix}                       \
@@ -72,7 +72,7 @@ for src in ${SRC}; do
 
   else
     "${goto_cc}"                        \
-        --export-function-local-symbols \
+        --export-file-local-symbols \
         --verbosity 10                  \
         ${wall}                         \
         ${suffix}                       \
@@ -86,7 +86,7 @@ if is_in final-link "$ALL_ARGS"; then
   rm -f ${OUT_FILE}
   if [[ "${is_windows}" == "true" ]]; then
     "${goto_cc}"                        \
-        --export-function-local-symbols \
+        --export-file-local-symbols \
         --verbosity 10                  \
         ${wall}                         \
         ${suffix}                       \
@@ -95,7 +95,7 @@ if is_in final-link "$ALL_ARGS"; then
 
   else
     "${goto_cc}"                        \
-        --export-function-local-symbols \
+        --export-file-local-symbols \
         --verbosity 10                  \
         ${wall}                         \
         ${suffix}                       \

src/goto-cc/compile.cpp

@@ -626,14 +626,22 @@ compilet::compilet(cmdlinet &_cmdline, message_handlert &mh, bool Werror)
     ns(goto_model.symbol_table),
     cmdline(_cmdline),
     warning_is_fatal(Werror),
-    keep_file_local(cmdline.isset("export-function-local-symbols")),
+    keep_file_local(
+      // function-local is the old name and is still in use, but is misleading
+      cmdline.isset("export-function-local-symbols") ||
+      cmdline.isset("export-file-local-symbols")),
     file_local_mangle_suffix(
       cmdline.isset("mangle-suffix") ? cmdline.get_value("mangle-suffix") : "")
 {
   mode=COMPILE_LINK_EXECUTABLE;
   echo_file_name=false;
   wrote_object=false;
   working_directory=get_current_working_directory();
+
+  if(cmdline.isset("export-function-local-symbols"))
+    warning() << "The `--export-function-local-symbols` flag is deprecated. "
+                 "Please use `--export-file-local-symbols` instead."
+              << eom;
 }
 
 /// cleans up temporary files

src/goto-cc/gcc_cmdline.cpp

@@ -52,7 +52,7 @@ const char *goto_cc_options_without_argument[]=
   "--partial-inlining",
   "--validate-goto-model",
   "-?",
-  "--export-function-local-symbols",
+  "--export-file-local-symbols",
   nullptr
 };
 

src/goto-cc/ms_cl_cmdline.cpp

@@ -46,7 +46,7 @@ const char *non_ms_cl_options[]=
   "--verbosity",
   "--function",
   "--validate-goto-model",
-  "--export-function-local-symbols",
+  "--export-file-local-symbols",
   "--mangle-suffix",
   nullptr
 };