Skip to content

Commit 8c30146

Browse files
karkhazkarkhaz
committed
Add docs for --export-function-local-symbols
1 parent dbac963 commit 8c30146

File tree

1 file changed

+159
-0
lines changed

1 file changed

+159
-0
lines changed

‎doc/architectural/static-functions.md

Lines changed: 159 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,159 @@
1+
\ingroup module_hidden
2+
\page modular-verification-static Modular Verification of Static Functions
3+
4+
\section verification-of-static Modular Verification of Static Functions
5+
6+
\author Kareem Khazem
7+
8+
This page describes how to use CBMC on static functions.
9+
10+
\tableofcontents
11+
12+
CBMC can check libraries and other codebases that expose several
13+
entry points. To do this, users typically write a *harness* that
14+
captures the entry points' API contract, and that calls into the API
15+
with unconstrained values. The example below shows such a library and
16+
harness:
17+
18+
\code{.c}
19+
void public_api_function(const int *a, int *b)
20+
{
21+
// ...
22+
private_function(a, b);
23+
// ...
24+
}
25+
26+
static void private_function(const int *a, int *b)
27+
{
28+
// ...
29+
}
30+
\endcode
31+
32+
The harness sets up some assumptions and then calls into the API:
33+
34+
\code{.c}
35+
void public_api_function(int *a, int *b);
36+
37+
void harness()
38+
{
39+
int a, b;
40+
__CPROVER_assume(a < 10);
41+
__CPROVER_assume(a >= 0);
42+
public_api_function(&a, &b);
43+
__CPROVER_assert(b != a);
44+
}
45+
\endcode
46+
47+
The following commands build and check this function:
48+
49+
\code{.sh}
50+
> goto-cc -c -o library.o library.c
51+
> goto-cc -c -o harness.o harness.c
52+
> goto-cc -o to_check.gb library.o harness.o
53+
> cbmc --function harness to_check.gb
54+
\endcode
55+
56+
\subsection stubbing-out-static Stubbing out static functions
57+
58+
For performance reasons, it might be desirable to analyze the API
59+
function independently of the static function. We can analyze the API
60+
function by "stubbing out" the static function, replacing it with a
61+
function that does nothing apart from asserting that its inputs satisfy
62+
the function's contract. Add the following to `harness.c`:
63+
64+
\code{.c}
65+
static void private_function(const int *a, int *b)
66+
{
67+
__CPROVER_assert( private_function_precondition );
68+
__CPROVER_assume( private_function_postcondition );
69+
}
70+
\endcode
71+
72+
And build as follows, stripping the original static function out of its
73+
object file:
74+
75+
\code{.sh}
76+
> goto-cc -c -o library.o library.c
77+
> goto-instrument --remove-function-body private_function library.o library-no-private.o
78+
>
79+
> goto-cc -c -o harness.o harness.c
80+
>
81+
> # The stub in the harness overrides the implementation of
82+
> # private_function whose body has been removed
83+
> goto-cc -o to_check.gb library-no-private.o harness.o
84+
> cbmc --function harness to_check.gb
85+
\endcode
86+
87+
\subsection checking-static Separately checking static functions
88+
89+
We should now also write a harness for `private_function`. However,
90+
since that function is marked `static`, it is not possible for functions
91+
in external files to call it. We can write and link a harness by
92+
stripping the `static` attribute from `private_function` using goto-cc's
93+
`--export-file-local-symbols` flag.
94+
95+
\code{.sh}
96+
> goto-cc -c -o --export-file-local-symbols library_with_static.o library.c
97+
\endcode
98+
99+
`library_with_static.o` now contains an implementation of `private_function()`
100+
with a mangled name. We can display the mangled name with goto-instrument:
101+
102+
\code{.sh}
103+
> goto-instrument --show-symbol-table library_with_static.o | grep -B1 -A1 "Pretty name.: private_function"
104+
Symbol......: __CPROVER_file_local_library_c_private_function
105+
Pretty name.: private_function
106+
Module......: private_function
107+
\endcode
108+
109+
When we write a harness for the static function, we ensure that we call
110+
the mangled name:
111+
112+
\code{.c}
113+
void harness()
114+
{
115+
int a, b;
116+
117+
__CPROVER_assume( private_function_precondition );
118+
119+
// Call the static function
120+
__CPROVER_file_local_library_c_private_function(&a, &b);
121+
122+
__CPROVER_assert( private_function_postcondition );
123+
}
124+
\endcode
125+
126+
We can then link this harness to the object file with exported symbols
127+
and run CBMC as usual.
128+
129+
\code{.sh}
130+
> goto-cc -c -o private_harness.o private_harness.c
131+
> goto-cc -o to_test.gb private_harness.o library_with_static.o
132+
> cbmc --function harness to_test.gb
133+
\endcode
134+
135+
It is possible that CBMC will generate the same mangled name for two
136+
different static functions. This happens when the functions have the
137+
same name and are written in same-named files that live in different
138+
directories. In the following codebase, the two `qux` functions will
139+
both have their names mangled to `__CPROVER_file_local_b_c_qux`, and
140+
so any harness that requires both of those files will fail to link.
141+
142+
project
143+
|
144+
\_ foo
145+
| |
146+
| \_ a.c
147+
| \_ b.c <- contains static function "qux"
148+
|
149+
\_ bar
150+
|
151+
\_ c.c
152+
\_ b.c <- also contains static function "qux"
153+
154+
The solution is to use the `--mangle-suffix` option to goto-cc. This
155+
allows you to specify a different suffix for name-mangling. By
156+
specifying a custom, different suffix for each of the two files, the
157+
mangled names are unique and the files can be successfully linked.
158+
159+
More examples are in `regression/goto-cc-file-local`.

0 commit comments

Comments
 (0)