From 8c30146301b80e92d6f7e074b7bcab99494f956f Mon Sep 17 00:00:00 2001 From: Kareem Khazem Date: Mon, 16 Sep 2019 12:14:10 -0400 Subject: [PATCH 1/2] Add docs for --export-function-local-symbols --- doc/architectural/static-functions.md | 159 ++++++++++++++++++++++++++ 1 file changed, 159 insertions(+) create mode 100644 doc/architectural/static-functions.md diff --git a/doc/architectural/static-functions.md b/doc/architectural/static-functions.md new file mode 100644 index 00000000000..eb5043c9190 --- /dev/null +++ b/doc/architectural/static-functions.md @@ -0,0 +1,159 @@ +\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. 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`. From a3a7edbbd9cba6b6810fb601c41c45c08828417e Mon Sep 17 00:00:00 2001 From: Kareem Khazem Date: Tue, 11 Feb 2020 10:18:49 -0500 Subject: [PATCH 2/2] Add docs for --export-file-local-symbols --- doc/architectural/static-functions.md | 4 +++- regression/goto-cc-file-local/chain.sh | 8 ++++---- src/goto-cc/compile.cpp | 10 +++++++++- src/goto-cc/gcc_cmdline.cpp | 2 +- src/goto-cc/ms_cl_cmdline.cpp | 2 +- 5 files changed, 18 insertions(+), 8 deletions(-) diff --git a/doc/architectural/static-functions.md b/doc/architectural/static-functions.md index eb5043c9190..8c38b797675 100644 --- a/doc/architectural/static-functions.md +++ b/doc/architectural/static-functions.md @@ -59,7 +59,9 @@ 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. Add the following to `harness.c`: +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) diff --git a/regression/goto-cc-file-local/chain.sh b/regression/goto-cc-file-local/chain.sh index 557e1856734..7ac73356815 100755 --- a/regression/goto-cc-file-local/chain.sh +++ b/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} \ diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp index adae4517091..3c3389024d7 100644 --- a/src/goto-cc/compile.cpp +++ b/src/goto-cc/compile.cpp @@ -626,7 +626,10 @@ 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") : "") { @@ -634,6 +637,11 @@ compilet::compilet(cmdlinet &_cmdline, message_handlert &mh, bool Werror) 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 diff --git a/src/goto-cc/gcc_cmdline.cpp b/src/goto-cc/gcc_cmdline.cpp index 87747e7da34..07bce3808f9 100644 --- a/src/goto-cc/gcc_cmdline.cpp +++ b/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 }; diff --git a/src/goto-cc/ms_cl_cmdline.cpp b/src/goto-cc/ms_cl_cmdline.cpp index 07beba4d466..7b2dcc21036 100644 --- a/src/goto-cc/ms_cl_cmdline.cpp +++ b/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 };