Skip to content

Commit d8a5669

Browse files
karkhazkarkhaz
committed
Add docs for --export-function-local-symbols
1 parent 82d0ea2 commit d8a5669

File tree

1 file changed

+153
-0
lines changed

1 file changed

+153
-0
lines changed

‎doc/architectural/static-functions.md

Lines changed: 153 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,153 @@
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 harness()
36+
{
37+
int a, b;
38+
__CPROVER_assume(a < 10);
39+
__CPROVER_assume(a >= 0);
40+
public_api_function(&a, &b);
41+
__CPROVER_assert(b != a);
42+
}
43+
\endcode
44+
45+
The following commands build and check this function:
46+
47+
\code{.sh}
48+
> goto-cc -c -o library.o library.c
49+
> goto-cc -c -o harness.o harness.c
50+
> goto-cc -o to_check.gb library.o harness.o
51+
> cbmc to_check.gb
52+
\endcode
53+
54+
\subsection stubbing-out-static Stubbing out static functions
55+
56+
For performance reasons, it might be desirable to analyze the static
57+
function separately from the API function. We can analyze the API
58+
function by "stubbing out" the static function, replacing it with a
59+
function that does nothing apart from asserting that its inputs satisfy
60+
the function's contract. Add the following to `harness.c`:
61+
62+
\code{.c}
63+
static void private_function(const int *a, int *b)
64+
{
65+
__CPROVER_assert( /* ... */ );
66+
__CPROVER_assert( /* ... */ );
67+
// ...
68+
__CPROVER_assume( /* ... */ );
69+
__CPROVER_assume( /* ... */ );
70+
}
71+
\endcode
72+
73+
And build as follows, stripping the original static function out of its
74+
object file:
75+
76+
\code{.sh}
77+
> goto-cc -c -o library.o library.c
78+
> goto-instrument --remove-function-body private_function library.o library-no-private.o
79+
>
80+
> goto-cc -c -o harness.o harness.c
81+
>
82+
> goto-cc -o to_check.gb library-no-private.o harness.o
83+
> cbmc to_check.gb
84+
\endcode
85+
86+
\subsection checking-static Separately checking static functions
87+
88+
We should now also write a harness for `private_function`. However,
89+
since that function is marked `static`, it is not possible for functions
90+
in external files to call it. We can write and link a harness by
91+
stripping the `static` attribute from `private_function` using goto-cc's
92+
`--export-function-local-symbols` flag.
93+
94+
\code{.sh}
95+
> goto-cc -c -o --export-function-local-symbols library_with_static.o library.c
96+
#
97+
# library_with_static.o now contains an implementation of private_function()
98+
# with a mangled name. We can display the mangled name with goto-instrument:
99+
#
100+
> goto-instrument --show-symbol-table library_with_static.o | grep -B1 A1 "Pretty name.: private_function"
101+
Symbol......: __CPROVER_file_local_library_c_private_function
102+
Pretty name.: private_function
103+
Module......: private_function
104+
\endcode
105+
106+
When we write a harness for the static function, we ensure that we call
107+
the mangled name:
108+
109+
\code{.c}
110+
void harness()
111+
{
112+
int a, b;
113+
__CPROVER_assume( /* ... */ );
114+
115+
// Call the static function
116+
__CPROVER_file_local_library_c_private_function(&a, &b);
117+
}
118+
\endcode
119+
120+
We can then link this harness to the object file with exported symbols
121+
and run CBMC as usual.
122+
123+
\code{.sh}
124+
> goto-cc -c -o private_harness.o private_harness.c
125+
> goto-cc -o to_test.gb private_harness.o library_with_static.o
126+
> cbmc to_test.gb
127+
\endcode
128+
129+
It is possible that CBMC will generate the same mangled name for two
130+
different static functions. This happens when the functions have the
131+
same name and are written in same-named files that live in different
132+
directories. In the following codebase, the two `qux` functions will
133+
both have their names mangled to `__CPROVER_file_local_b_c_qux`, and
134+
so any harness that requires both of those files will fail to link.
135+
136+
project
137+
|
138+
\_ foo
139+
| |
140+
| \_ a.c
141+
| \_ b.c <- contains static function "qux"
142+
|
143+
\_ bar
144+
|
145+
\_ c.c
146+
\_ b.c <- also contains static function "qux"
147+
148+
The solution is to use the `--mangle-suffix` option to goto-cc. This
149+
allows you to specify a different suffix for name-mangling. By
150+
specifying a custom, different suffix for each of the two files, the
151+
mangled names are unique and the files can be successfully linked.
152+
153+
More examples are in `regression/goto-cc-file-local`.

0 commit comments

Comments
 (0)