Skip to content

Commit 4438e77

Browse files
karkhazkarkhaz
committed
Add --export-function-local-symbols to goto-cc
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.
1 parent 12bb475 commit 4438e77

File tree

32 files changed

+497
-6
lines changed

32 files changed

+497
-6
lines changed

‎regression/CMakeLists.txt

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -50,3 +50,4 @@ add_subdirectory(goto-cc-goto-analyzer)
5050
add_subdirectory(systemc)
5151
add_subdirectory(contracts)
5252
add_subdirectory(goto-harness)
53+
add_subdirectory(goto-cc-file-local)

‎regression/goto-cc-file-local/CMakeLists.txt

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
if(WIN32)
2+
set(is_windows true)
3+
else()
4+
set(is_windows false)
5+
endif()
6+
7+
add_test_pl_tests(
8+
"${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-instrument> $<TARGET_FILE:cbmc> ${is_windows}"
9+
)

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

Lines changed: 77 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,77 @@
1+
#!/usr/bin/env bash
2+
#
3+
# Invoke one or more CPROVER tools depending on arguments
4+
#
5+
# Author: Kareem Khazem <[email protected]>
6+
7+
is_in()
8+
{
9+
[[ "$2" =~ $1 ]] && return 0 || return 1
10+
}
11+
12+
ALL_ARGS="$@"
13+
OUT_FILE=""
14+
15+
if is_in suffix "$ALL_ARGS"; then
16+
suffix="--mangle-suffix custom_suffix"
17+
else
18+
suffix=""
19+
fi
20+
21+
goto_cc=$1
22+
goto_instrument=$2
23+
cbmc=$3
24+
is_windows=$4
25+
26+
for src in *.c; do
27+
base=${src%.c}
28+
OUT_FILE="${base}.gb"
29+
30+
if [[ "${is_windows}" == "true" ]]; then
31+
"${goto_cc}" \
32+
/export-function-local-symbols \
33+
/verbosity 10 \
34+
${suffix} \
35+
/c"${base}.c" \
36+
/Fo"${OUT_FILE}"
37+
38+
elif [[ "${is_windows}" == "false" ]]; then
39+
"${goto_cc}" \
40+
--export-function-local-symbols \
41+
--verbosity 10 \
42+
${suffix} \
43+
-c "${base}.c" \
44+
-o "${OUT_FILE}"
45+
else
46+
(>&2 echo "\$is_windows should be true or false (got '" "${is_windows}" "')")
47+
exit 1
48+
fi
49+
done
50+
51+
if is_in final-link "$ALL_ARGS"; then
52+
OUT_FILE=final-link.gb
53+
if [[ "${is_windows}" == "true" ]]; then
54+
"${goto_cc}" \
55+
/export-function-local-symbols \
56+
/verbosity 10 \
57+
${suffix} \
58+
./*.gb \
59+
/Fe "${OUT_FILE}"
60+
61+
elif [[ "${is_windows}" == "false" ]]; then
62+
"${goto_cc}" \
63+
--export-function-local-symbols \
64+
--verbosity 10 \
65+
${suffix} \
66+
./*.gb \
67+
-o "${OUT_FILE}"
68+
fi
69+
fi
70+
71+
if is_in show-symbol-table "$ALL_ARGS"; then
72+
"${goto_instrument}" --show-symbol-table "${OUT_FILE}"
73+
fi
74+
75+
if is_in assertion-check "$ALL_ARGS"; then
76+
"${cbmc}" "${OUT_FILE}"
77+
fi

‎regression/goto-cc-file-local/result-multi-file-bad/foo.c

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
static int foo()
2+
{
3+
assert(0);
4+
return 1;
5+
}

‎regression/goto-cc-file-local/result-multi-file-bad/main.c

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
int __CPROVER_file_local_foo_c_foo();
2+
3+
int main()
4+
{
5+
int x = __CPROVER_file_local_foo_c_foo();
6+
}

‎regression/goto-cc-file-local/result-multi-file-bad/test.desc

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
main.c
3+
final-link assertion-check
4+
5+
^EXIT=10$
6+
^SIGNAL=0$
7+
^VERIFICATION FAILED$
8+
--
9+
^warning: ignoring
10+
^\*\*\*\* WARNING: no body for function
11+
--
12+
Check that CBMC symbolically executes a static function in a different
13+
file

‎regression/goto-cc-file-local/result-multi-file-good/foo.c

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
static int foo()
2+
{
3+
return 1;
4+
}

‎regression/goto-cc-file-local/result-multi-file-good/main.c

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
int __CPROVER_file_local_foo_c_foo();
2+
3+
int main()
4+
{
5+
int x = __CPROVER_file_local_foo_c_foo();
6+
}

‎regression/goto-cc-file-local/result-multi-file-good/test.desc

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
main.c
3+
final-link assertion-check
4+
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
^VERIFICATION SUCCESSFUL$
8+
--
9+
^warning: ignoring
10+
^\*\*\*\* WARNING: no body for function
11+
--
12+
Check that CBMC symbolically executes a static function in a different
13+
file

‎regression/goto-cc-file-local/result-multi-file-transitive/foo.c

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
static int bar()
2+
{
3+
assert(0);
4+
return 1;
5+
}
6+
7+
static int foo()
8+
{
9+
return bar();
10+
}

‎regression/goto-cc-file-local/result-multi-file-transitive/main.c

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
int __CPROVER_file_local_foo_c_foo();
2+
3+
int main()
4+
{
5+
int x = __CPROVER_file_local_foo_c_foo();
6+
}

‎regression/goto-cc-file-local/result-multi-file-transitive/test.desc

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
CORE
2+
main.c
3+
final-link assertion-check
4+
5+
^EXIT=10$
6+
^SIGNAL=0$
7+
^VERIFICATION FAILED$
8+
--
9+
^warning: ignoring
10+
^\*\*\*\* WARNING: no body for function
11+
--
12+
Check that CBMC symbolically executes static functions in a different
13+
file. Ensure that static functions are transitively called. Function
14+
calls don't need to be manually mangled in the same file.

‎regression/goto-cc-file-local/result-suffix/foo.c

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
static int foo()
2+
{
3+
assert(0);
4+
return 1;
5+
}

‎regression/goto-cc-file-local/result-suffix/main.c

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
int __CPROVER_file_local_foo_c_custom_suffix_foo();
2+
3+
int main()
4+
{
5+
int x = __CPROVER_file_local_foo_c_custom_suffix_foo();
6+
}

‎regression/goto-cc-file-local/result-suffix/test.desc

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
main.c
3+
final-link assertion-check suffix
4+
5+
^EXIT=10$
6+
^SIGNAL=0$
7+
^VERIFICATION FAILED$
8+
--
9+
^warning: ignoring
10+
^\*\*\*\* WARNING: no body for function
11+
--
12+
Check that CBMC symbolically executes a static function in a different
13+
file. Use a suffix.

‎regression/goto-cc-file-local/symbol-compiled/main.c

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
static int foo()
2+
{
3+
return 3;
4+
}
5+
6+
int main()
7+
{
8+
int x = foo();
9+
}

‎regression/goto-cc-file-local/symbol-compiled/test.desc

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
CORE
2+
main.c
3+
show-symbol-table
4+
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
^Symbol......: __CPROVER_file_local_main_c_foo$
8+
--
9+
^warning: ignoring
10+
^\*\*\*\* WARNING: no body for function
11+
--
12+
This is similar to check-symbol-fully-linked, except that we're not
13+
linking the binary (we're using -c and not subsequently not using it).
14+
Check that we still keep the file-local implementations.

‎regression/goto-cc-file-local/symbol-fully-linked/main.c

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
static int foo()
2+
{
3+
return 3;
4+
}
5+
6+
int main()
7+
{
8+
int x = foo();
9+
}

‎regression/goto-cc-file-local/symbol-fully-linked/test.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
main.c
3+
final-link show-symbol-table
4+
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
^Symbol......: __CPROVER_file_local_main_c_foo$
8+
--
9+
^warning: ignoring
10+
^\*\*\*\* WARNING: no body for function

‎regression/goto-cc-file-local/symbol-multi-file/foo.c

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
static int foo()
2+
{
3+
return 3;
4+
}

‎regression/goto-cc-file-local/symbol-multi-file/main.c

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
int foo();
2+
3+
int main()
4+
{
5+
int x = foo();
6+
}

‎regression/goto-cc-file-local/symbol-multi-file/test.desc

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
main.c
3+
final-link show-symbol-table
4+
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
^Symbol......: __CPROVER_file_local_foo_c_foo$
8+
--
9+
^warning: ignoring
10+
^\*\*\*\* WARNING: no body for function
11+
--
12+
Check that a static function in a different file appears in the symbol
13+
table of the fully-linked binary

‎src/ansi-c/ansi_c_language.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -119,7 +119,8 @@ bool ansi_c_languaget::typecheck(
119119
return true;
120120
}
121121

122-
remove_internal_symbols(new_symbol_table, this->get_message_handler());
122+
remove_internal_symbols(
123+
new_symbol_table, this->get_message_handler(), keep_file_local);
123124

124125
if(linking(symbol_table, new_symbol_table, get_message_handler()))
125126
return true;

‎src/goto-cc/compile.cpp

Lines changed: 13 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -34,6 +34,7 @@ Date: June 2006
3434

3535
#include <goto-programs/goto_convert.h>
3636
#include <goto-programs/goto_convert_functions.h>
37+
#include <goto-programs/name_mangler.h>
3738
#include <goto-programs/read_goto_binary.h>
3839
#include <goto-programs/validate_goto_model.h>
3940
#include <goto-programs/write_goto_binary.h>
@@ -401,6 +402,13 @@ bool compilet::compile()
401402
else
402403
cfn = output_file_object;
403404

405+
if(keep_file_local)
406+
{
407+
function_name_manglert<file_name_manglert> mangler(
408+
get_message_handler(), goto_model, file_local_mangle_suffix);
409+
mangler.mangle();
410+
}
411+
404412
if(write_bin_object_file(cfn, goto_model))
405413
return true;
406414

@@ -593,7 +601,7 @@ bool compilet::parse_source(const std::string &file_name)
593601
return true;
594602

595603
// we just typecheck one file here
596-
if(language_files.typecheck(goto_model.symbol_table))
604+
if(language_files.typecheck(goto_model.symbol_table, keep_file_local))
597605
{
598606
error() << "CONVERSION ERROR" << eom;
599607
return true;
@@ -614,7 +622,10 @@ compilet::compilet(cmdlinet &_cmdline, message_handlert &mh, bool Werror)
614622
: messaget(mh),
615623
ns(goto_model.symbol_table),
616624
cmdline(_cmdline),
617-
warning_is_fatal(Werror)
625+
warning_is_fatal(Werror),
626+
keep_file_local(cmdline.isset("export-function-local-symbols")),
627+
file_local_mangle_suffix(
628+
cmdline.isset("mangle-suffix") ? cmdline.get_value("mangle-suffix") : "")
618629
{
619630
mode=COMPILE_LINK_EXECUTABLE;
620631
echo_file_name=false;

‎src/goto-cc/compile.h

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -96,6 +96,12 @@ class compilet : public messaget
9696
cmdlinet &cmdline;
9797
bool warning_is_fatal;
9898

99+
/// \brief Whether to keep implementations of file-local symbols
100+
const bool keep_file_local;
101+
102+
/// \brief String to include in all mangled names
103+
const std::string file_local_mangle_suffix;
104+
99105
std::size_t function_body_count(const goto_functionst &) const;
100106

101107
void add_compiler_specific_defines() const;

‎src/goto-cc/gcc_cmdline.cpp

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,7 @@ const char *goto_cc_options_with_separated_argument[]=
2727
"--native-compiler",
2828
"--native-linker",
2929
"--print-rejected-preprocessed-source",
30+
"--mangle-suffix",
3031
nullptr
3132
};
3233

@@ -51,6 +52,7 @@ const char *goto_cc_options_without_argument[]=
5152
"--partial-inlining",
5253
"--validate-goto-model",
5354
"-?",
55+
"--export-function-local-symbols",
5456
nullptr
5557
};
5658

‎src/goto-cc/ms_cl_cmdline.cpp

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -46,6 +46,8 @@ const char *non_ms_cl_options[]=
4646
"--verbosity",
4747
"--function",
4848
"--validate-goto-model",
49+
"--export-function-local-symbols",
50+
"--mangle-suffix",
4951
nullptr
5052
};
5153
// clang-format on

‎src/goto-programs/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -32,6 +32,7 @@ SRC = adjust_float_expressions.cpp \
3232
link_to_library.cpp \
3333
loop_ids.cpp \
3434
mm_io.cpp \
35+
name_mangler.cpp \
3536
osx_fat_reader.cpp \
3637
parameter_assignments.cpp \
3738
pointer_arithmetic.cpp \

0 commit comments

Comments
 (0)