diff --git a/regression/CMakeLists.txt b/regression/CMakeLists.txt index 1d6765b5444..06a388929ff 100644 --- a/regression/CMakeLists.txt +++ b/regression/CMakeLists.txt @@ -50,3 +50,4 @@ add_subdirectory(goto-cc-goto-analyzer) add_subdirectory(systemc) add_subdirectory(contracts) add_subdirectory(goto-harness) +add_subdirectory(goto-cc-file-local) diff --git a/regression/goto-cc-file-local/CMakeLists.txt b/regression/goto-cc-file-local/CMakeLists.txt new file mode 100644 index 00000000000..f7f08694f6a --- /dev/null +++ b/regression/goto-cc-file-local/CMakeLists.txt @@ -0,0 +1,9 @@ +if(WIN32) + set(is_windows true) +else() + set(is_windows false) +endif() + +add_test_pl_tests( + "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $ $ $ ${is_windows}" +) diff --git a/regression/goto-cc-file-local/chain.sh b/regression/goto-cc-file-local/chain.sh new file mode 100755 index 00000000000..bff91960681 --- /dev/null +++ b/regression/goto-cc-file-local/chain.sh @@ -0,0 +1,77 @@ +#!/usr/bin/env bash +# +# Invoke one or more CPROVER tools depending on arguments +# +# Author: Kareem Khazem + +is_in() +{ + [[ "$2" =~ $1 ]] && return 0 || return 1 +} + +ALL_ARGS="$@" +OUT_FILE="" + +if is_in suffix "$ALL_ARGS"; then + suffix="--mangle-suffix custom_suffix" +else + suffix="" +fi + +goto_cc=$1 +goto_instrument=$2 +cbmc=$3 +is_windows=$4 + +for src in *.c; do + base=${src%.c} + OUT_FILE="${base}.gb" + + if [[ "${is_windows}" == "true" ]]; then + "${goto_cc}" \ + /export-function-local-symbols \ + /verbosity 10 \ + ${suffix} \ + /c"${base}.c" \ + /Fo"${OUT_FILE}" + + elif [[ "${is_windows}" == "false" ]]; then + "${goto_cc}" \ + --export-function-local-symbols \ + --verbosity 10 \ + ${suffix} \ + -c "${base}.c" \ + -o "${OUT_FILE}" + else + (>&2 echo "\$is_windows should be true or false (got '" "${is_windows}" "')") + exit 1 + fi +done + +if is_in final-link "$ALL_ARGS"; then + OUT_FILE=final-link.gb + if [[ "${is_windows}" == "true" ]]; then + "${goto_cc}" \ + /export-function-local-symbols \ + /verbosity 10 \ + ${suffix} \ + ./*.gb \ + /Fe "${OUT_FILE}" + + elif [[ "${is_windows}" == "false" ]]; then + "${goto_cc}" \ + --export-function-local-symbols \ + --verbosity 10 \ + ${suffix} \ + ./*.gb \ + -o "${OUT_FILE}" + fi +fi + +if is_in show-symbol-table "$ALL_ARGS"; then + "${goto_instrument}" --show-symbol-table "${OUT_FILE}" +fi + +if is_in assertion-check "$ALL_ARGS"; then + "${cbmc}" "${OUT_FILE}" +fi diff --git a/regression/goto-cc-file-local/result-multi-file-bad/foo.c b/regression/goto-cc-file-local/result-multi-file-bad/foo.c new file mode 100644 index 00000000000..50a663850d7 --- /dev/null +++ b/regression/goto-cc-file-local/result-multi-file-bad/foo.c @@ -0,0 +1,5 @@ +static int foo() +{ + assert(0); + return 1; +} diff --git a/regression/goto-cc-file-local/result-multi-file-bad/main.c b/regression/goto-cc-file-local/result-multi-file-bad/main.c new file mode 100644 index 00000000000..ae38bfe5666 --- /dev/null +++ b/regression/goto-cc-file-local/result-multi-file-bad/main.c @@ -0,0 +1,6 @@ +int __CPROVER_file_local_foo_c_foo(); + +int main() +{ + int x = __CPROVER_file_local_foo_c_foo(); +} diff --git a/regression/goto-cc-file-local/result-multi-file-bad/test.desc b/regression/goto-cc-file-local/result-multi-file-bad/test.desc new file mode 100644 index 00000000000..14b79feac7b --- /dev/null +++ b/regression/goto-cc-file-local/result-multi-file-bad/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +final-link assertion-check + +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring +^\*\*\*\* WARNING: no body for function +-- +Check that CBMC symbolically executes a static function in a different +file diff --git a/regression/goto-cc-file-local/result-multi-file-good/foo.c b/regression/goto-cc-file-local/result-multi-file-good/foo.c new file mode 100644 index 00000000000..65b091b64ad --- /dev/null +++ b/regression/goto-cc-file-local/result-multi-file-good/foo.c @@ -0,0 +1,4 @@ +static int foo() +{ + return 1; +} diff --git a/regression/goto-cc-file-local/result-multi-file-good/main.c b/regression/goto-cc-file-local/result-multi-file-good/main.c new file mode 100644 index 00000000000..ae38bfe5666 --- /dev/null +++ b/regression/goto-cc-file-local/result-multi-file-good/main.c @@ -0,0 +1,6 @@ +int __CPROVER_file_local_foo_c_foo(); + +int main() +{ + int x = __CPROVER_file_local_foo_c_foo(); +} diff --git a/regression/goto-cc-file-local/result-multi-file-good/test.desc b/regression/goto-cc-file-local/result-multi-file-good/test.desc new file mode 100644 index 00000000000..3e0ffa77857 --- /dev/null +++ b/regression/goto-cc-file-local/result-multi-file-good/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +final-link assertion-check + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +^\*\*\*\* WARNING: no body for function +-- +Check that CBMC symbolically executes a static function in a different +file diff --git a/regression/goto-cc-file-local/result-multi-file-transitive/foo.c b/regression/goto-cc-file-local/result-multi-file-transitive/foo.c new file mode 100644 index 00000000000..d5a1ba2c56b --- /dev/null +++ b/regression/goto-cc-file-local/result-multi-file-transitive/foo.c @@ -0,0 +1,10 @@ +static int bar() +{ + assert(0); + return 1; +} + +static int foo() +{ + return bar(); +} diff --git a/regression/goto-cc-file-local/result-multi-file-transitive/main.c b/regression/goto-cc-file-local/result-multi-file-transitive/main.c new file mode 100644 index 00000000000..ae38bfe5666 --- /dev/null +++ b/regression/goto-cc-file-local/result-multi-file-transitive/main.c @@ -0,0 +1,6 @@ +int __CPROVER_file_local_foo_c_foo(); + +int main() +{ + int x = __CPROVER_file_local_foo_c_foo(); +} diff --git a/regression/goto-cc-file-local/result-multi-file-transitive/test.desc b/regression/goto-cc-file-local/result-multi-file-transitive/test.desc new file mode 100644 index 00000000000..c96932db305 --- /dev/null +++ b/regression/goto-cc-file-local/result-multi-file-transitive/test.desc @@ -0,0 +1,14 @@ +CORE +main.c +final-link assertion-check + +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring +^\*\*\*\* WARNING: no body for function +-- +Check that CBMC symbolically executes static functions in a different +file. Ensure that static functions are transitively called. Function +calls don't need to be manually mangled in the same file. diff --git a/regression/goto-cc-file-local/result-suffix/foo.c b/regression/goto-cc-file-local/result-suffix/foo.c new file mode 100644 index 00000000000..50a663850d7 --- /dev/null +++ b/regression/goto-cc-file-local/result-suffix/foo.c @@ -0,0 +1,5 @@ +static int foo() +{ + assert(0); + return 1; +} diff --git a/regression/goto-cc-file-local/result-suffix/main.c b/regression/goto-cc-file-local/result-suffix/main.c new file mode 100644 index 00000000000..7c0c2a5409e --- /dev/null +++ b/regression/goto-cc-file-local/result-suffix/main.c @@ -0,0 +1,6 @@ +int __CPROVER_file_local_foo_c_custom_suffix_foo(); + +int main() +{ + int x = __CPROVER_file_local_foo_c_custom_suffix_foo(); +} diff --git a/regression/goto-cc-file-local/result-suffix/test.desc b/regression/goto-cc-file-local/result-suffix/test.desc new file mode 100644 index 00000000000..1fb9836701b --- /dev/null +++ b/regression/goto-cc-file-local/result-suffix/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +final-link assertion-check suffix + +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring +^\*\*\*\* WARNING: no body for function +-- +Check that CBMC symbolically executes a static function in a different +file. Use a suffix. diff --git a/regression/goto-cc-file-local/symbol-compiled/main.c b/regression/goto-cc-file-local/symbol-compiled/main.c new file mode 100644 index 00000000000..a0441110489 --- /dev/null +++ b/regression/goto-cc-file-local/symbol-compiled/main.c @@ -0,0 +1,9 @@ +static int foo() +{ + return 3; +} + +int main() +{ + int x = foo(); +} diff --git a/regression/goto-cc-file-local/symbol-compiled/test.desc b/regression/goto-cc-file-local/symbol-compiled/test.desc new file mode 100644 index 00000000000..fe8df7de0b5 --- /dev/null +++ b/regression/goto-cc-file-local/symbol-compiled/test.desc @@ -0,0 +1,14 @@ +CORE +main.c +show-symbol-table + +^EXIT=0$ +^SIGNAL=0$ +^Symbol......: __CPROVER_file_local_main_c_foo$ +-- +^warning: ignoring +^\*\*\*\* WARNING: no body for function +-- +This is similar to check-symbol-fully-linked, except that we're not +linking the binary (we're using -c and not subsequently not using it). +Check that we still keep the file-local implementations. diff --git a/regression/goto-cc-file-local/symbol-fully-linked/main.c b/regression/goto-cc-file-local/symbol-fully-linked/main.c new file mode 100644 index 00000000000..a0441110489 --- /dev/null +++ b/regression/goto-cc-file-local/symbol-fully-linked/main.c @@ -0,0 +1,9 @@ +static int foo() +{ + return 3; +} + +int main() +{ + int x = foo(); +} diff --git a/regression/goto-cc-file-local/symbol-fully-linked/test.desc b/regression/goto-cc-file-local/symbol-fully-linked/test.desc new file mode 100644 index 00000000000..e840162d25a --- /dev/null +++ b/regression/goto-cc-file-local/symbol-fully-linked/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +final-link show-symbol-table + +^EXIT=0$ +^SIGNAL=0$ +^Symbol......: __CPROVER_file_local_main_c_foo$ +-- +^warning: ignoring +^\*\*\*\* WARNING: no body for function diff --git a/regression/goto-cc-file-local/symbol-multi-file/foo.c b/regression/goto-cc-file-local/symbol-multi-file/foo.c new file mode 100644 index 00000000000..a2a056a5506 --- /dev/null +++ b/regression/goto-cc-file-local/symbol-multi-file/foo.c @@ -0,0 +1,4 @@ +static int foo() +{ + return 3; +} diff --git a/regression/goto-cc-file-local/symbol-multi-file/main.c b/regression/goto-cc-file-local/symbol-multi-file/main.c new file mode 100644 index 00000000000..9c270e6dc75 --- /dev/null +++ b/regression/goto-cc-file-local/symbol-multi-file/main.c @@ -0,0 +1,6 @@ +int foo(); + +int main() +{ + int x = foo(); +} diff --git a/regression/goto-cc-file-local/symbol-multi-file/test.desc b/regression/goto-cc-file-local/symbol-multi-file/test.desc new file mode 100644 index 00000000000..c6433cc9d1a --- /dev/null +++ b/regression/goto-cc-file-local/symbol-multi-file/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +final-link show-symbol-table + +^EXIT=0$ +^SIGNAL=0$ +^Symbol......: __CPROVER_file_local_foo_c_foo$ +-- +^warning: ignoring +^\*\*\*\* WARNING: no body for function +-- +Check that a static function in a different file appears in the symbol +table of the fully-linked binary diff --git a/src/ansi-c/ansi_c_language.cpp b/src/ansi-c/ansi_c_language.cpp index 92acb8a5e2f..acebc866760 100644 --- a/src/ansi-c/ansi_c_language.cpp +++ b/src/ansi-c/ansi_c_language.cpp @@ -105,7 +105,8 @@ bool ansi_c_languaget::parse( bool ansi_c_languaget::typecheck( symbol_tablet &symbol_table, - const std::string &module) + const std::string &module, + const bool keep_file_local) { symbol_tablet new_symbol_table; @@ -118,7 +119,8 @@ bool ansi_c_languaget::typecheck( return true; } - remove_internal_symbols(new_symbol_table); + remove_internal_symbols( + new_symbol_table, this->get_message_handler(), keep_file_local); if(linking(symbol_table, new_symbol_table, get_message_handler())) return true; diff --git a/src/ansi-c/ansi_c_language.h b/src/ansi-c/ansi_c_language.h index d554dbb9d0c..2fa003c521a 100644 --- a/src/ansi-c/ansi_c_language.h +++ b/src/ansi-c/ansi_c_language.h @@ -53,7 +53,19 @@ class ansi_c_languaget:public languaget bool typecheck( symbol_tablet &symbol_table, - const std::string &module) override; + const std::string &module, + const bool keep_file_local) override; + + bool can_keep_file_local() override + { + return true; + } + + bool + typecheck(symbol_tablet &symbol_table, const std::string &module) override + { + return typecheck(symbol_table, module, true); + } void show_parse(std::ostream &out) override; diff --git a/src/cpp/cpp_language.h b/src/cpp/cpp_language.h index 00c06d73c1f..f72784f7420 100644 --- a/src/cpp/cpp_language.h +++ b/src/cpp/cpp_language.h @@ -42,9 +42,8 @@ class cpp_languaget:public languaget bool generate_support_functions( symbol_tablet &symbol_table) override; - bool typecheck( - symbol_tablet &symbol_table, - const std::string &module) override; + bool + typecheck(symbol_tablet &symbol_table, const std::string &module) override; bool merge_symbol_table( symbol_tablet &dest, diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp index 0d21575bc63..cc4c6b91f2b 100644 --- a/src/goto-cc/compile.cpp +++ b/src/goto-cc/compile.cpp @@ -34,6 +34,7 @@ Date: June 2006 #include #include +#include #include #include #include @@ -401,6 +402,13 @@ bool compilet::compile() else cfn = output_file_object; + if(keep_file_local) + { + function_name_manglert mangler( + get_message_handler(), goto_model, file_local_mangle_suffix); + mangler.mangle(); + } + if(write_bin_object_file(cfn, goto_model)) return true; @@ -593,7 +601,7 @@ bool compilet::parse_source(const std::string &file_name) return true; // we just typecheck one file here - if(language_files.typecheck(goto_model.symbol_table)) + if(language_files.typecheck(goto_model.symbol_table, keep_file_local)) { error() << "CONVERSION ERROR" << eom; return true; @@ -614,7 +622,10 @@ compilet::compilet(cmdlinet &_cmdline, message_handlert &mh, bool Werror) : messaget(mh), ns(goto_model.symbol_table), cmdline(_cmdline), - warning_is_fatal(Werror) + warning_is_fatal(Werror), + keep_file_local(cmdline.isset("export-function-local-symbols")), + file_local_mangle_suffix( + cmdline.isset("mangle-suffix") ? cmdline.get_value("mangle-suffix") : "") { mode=COMPILE_LINK_EXECUTABLE; echo_file_name=false; diff --git a/src/goto-cc/compile.h b/src/goto-cc/compile.h index 3d80d0d8e7b..6f1f7117a5e 100644 --- a/src/goto-cc/compile.h +++ b/src/goto-cc/compile.h @@ -96,6 +96,12 @@ class compilet : public messaget cmdlinet &cmdline; bool warning_is_fatal; + /// \brief Whether to keep implementations of file-local symbols + const bool keep_file_local; + + /// \brief String to include in all mangled names + const std::string file_local_mangle_suffix; + std::size_t function_body_count(const goto_functionst &) const; void add_compiler_specific_defines() const; diff --git a/src/goto-cc/gcc_cmdline.cpp b/src/goto-cc/gcc_cmdline.cpp index a80ffa91da7..87747e7da34 100644 --- a/src/goto-cc/gcc_cmdline.cpp +++ b/src/goto-cc/gcc_cmdline.cpp @@ -27,6 +27,7 @@ const char *goto_cc_options_with_separated_argument[]= "--native-compiler", "--native-linker", "--print-rejected-preprocessed-source", + "--mangle-suffix", nullptr }; @@ -51,6 +52,7 @@ const char *goto_cc_options_without_argument[]= "--partial-inlining", "--validate-goto-model", "-?", + "--export-function-local-symbols", nullptr }; diff --git a/src/goto-cc/ms_cl_cmdline.cpp b/src/goto-cc/ms_cl_cmdline.cpp index 9736ce801a2..0da4061da2f 100644 --- a/src/goto-cc/ms_cl_cmdline.cpp +++ b/src/goto-cc/ms_cl_cmdline.cpp @@ -46,6 +46,8 @@ const char *non_ms_cl_options[]= "--verbosity", "--function", "--validate-goto-model", + "--export-function-local-symbols", + "--mangle-suffix", nullptr }; // clang-format on diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile index c66e8a4c837..870590d8ffc 100644 --- a/src/goto-programs/Makefile +++ b/src/goto-programs/Makefile @@ -32,6 +32,7 @@ SRC = adjust_float_expressions.cpp \ link_to_library.cpp \ loop_ids.cpp \ mm_io.cpp \ + name_mangler.cpp \ osx_fat_reader.cpp \ parameter_assignments.cpp \ pointer_arithmetic.cpp \ diff --git a/src/goto-programs/name_mangler.cpp b/src/goto-programs/name_mangler.cpp new file mode 100644 index 00000000000..17e2a18c610 --- /dev/null +++ b/src/goto-programs/name_mangler.cpp @@ -0,0 +1,46 @@ +/*******************************************************************\ + +Module: Name mangling + +Author: Kareem Khazem , 2019 + +\*******************************************************************/ + +#include "name_mangler.h" + +#include +#include + +irep_idt file_name_manglert:: +operator()(const symbolt &src, const std::string &extra_info) +{ + std::stringstream ss; + ss << CPROVER_PREFIX << "file_local_"; + ss << std::regex_replace( + std::regex_replace(src.location.get_file().c_str(), forbidden, "_"), + multi_under, + "_") + << "_"; + + if(extra_info != "") + ss << extra_info << "_"; + ss << src.name; + return irep_idt(ss.str()); +} + +irep_idt djb_manglert:: +operator()(const symbolt &src, const std::string &extra_info) +{ + char const *str = src.location.get_working_directory().c_str(); + unsigned long hash = 5381; + int c; + while((c = *str++)) + hash = ((hash << 5) + hash) + c; + + uint32_t eight_nibble_hash = (uint32_t)hash; + + std::stringstream ss; + ss << CPROVER_PREFIX << "file_local_" << std::setfill('0') << std::setw(8) + << std::hex << eight_nibble_hash << "_" << extra_info << "_" << src.name; + return irep_idt(ss.str()); +} diff --git a/src/goto-programs/name_mangler.h b/src/goto-programs/name_mangler.h new file mode 100644 index 00000000000..a4a5beaa35e --- /dev/null +++ b/src/goto-programs/name_mangler.h @@ -0,0 +1,155 @@ +/// \file name_mangler.h +/// \brief Mangle names of file-local functions to make them unique +/// \author Kareem Khazem + +#ifndef CPROVER_GOTO_PROGRAMS_NAME_MANGLER_H +#define CPROVER_GOTO_PROGRAMS_NAME_MANGLER_H + +#include +#include + +#include "goto_model.h" + +#include +#include + +/// \brief Mangles the names in an entire program and its symbol table +/// +/// The type parameter to this class should be a functor that has a no-arg +/// constructor and an `operator()` override with the following signature: +/// +/// irep_idt operator()(const symbolt &, const std::string &); +/// +/// The return type doesn't actually have to be an irep_idt, just something +/// that can be assigned to one. The function is expected to return the +/// mangled name of its \ref symbolt argument, incorporating the second +/// argument into the mangled name if possible. +template +class function_name_manglert +{ +public: + /// \param mh: handler to construct a log from + /// \param gm: mangle all names in gm's symbol table and goto program + /// \param extra_info: a string to be included in each mangled name + function_name_manglert( + message_handlert &mh, + goto_modelt &gm, + const std::string &extra_info) + : log(mh), model(gm), mangle_fun(), extra_info(extra_info) + { + } + + /// \brief Mangle all file-local function symbols in the program + /// + /// The way in which the symbols will be mangled is decided by which mangler + /// type this object is instantiated with, e.g. DJB_manglert mangles the path + /// name by hashing it. + void mangle() + { + rename_symbolt rename; + std::map renamed_funs; + std::vector new_syms; + std::vector old_syms; + + for(auto sym_it = model.symbol_table.symbols.begin(); + sym_it != model.symbol_table.symbols.end(); + ++sym_it) + { + const symbolt &sym = sym_it->second; + + if(sym.type.id() != ID_code) // is not a function + continue; + if(sym.value.is_nil()) // has no body + continue; + if(!sym.is_file_local) + continue; + + const irep_idt mangled = mangle_fun(sym, extra_info); + symbolt new_sym; + new_sym = sym; + new_sym.name = mangled; + new_sym.is_file_local = false; + + new_syms.push_back(new_sym); + old_syms.push_back(sym_it); + + rename.insert(sym.symbol_expr(), new_sym.symbol_expr()); + renamed_funs.insert(std::make_pair(sym.name, mangled)); + + log.debug() << "Mangling: " << sym.name << " -> " << mangled << log.eom; + } + + for(const auto &sym : new_syms) + model.symbol_table.insert(sym); + for(const auto &sym : old_syms) + model.symbol_table.erase(sym); + + for(auto &fun : model.goto_functions.function_map) + { + if(!fun.second.body_available()) + continue; + for(auto &ins : fun.second.body.instructions) + { + rename(ins.code); + rename(ins.guard); + } + } + + // Add goto-programs with new function names + for(const auto &pair : renamed_funs) + { + auto found = model.goto_functions.function_map.find(pair.first); + INVARIANT( + found != model.goto_functions.function_map.end(), + "There should exist an entry in the function_map for the original name " + "of the function that we renamed '" + + std::string(pair.first.c_str()) + "'"); + + auto inserted = model.goto_functions.function_map.emplace( + pair.second, std::move(found->second)); + INVARIANT( + inserted.second, + "The mangled name '" + std::string(pair.second.c_str()) + + "' should not already exist in the codebase"); + + model.goto_functions.function_map.erase(found); + } + } + +protected: + mutable messaget log; + goto_modelt &model; + MangleFun mangle_fun; + const std::string &extra_info; +}; + +/// \brief Mangle identifiers by including their filename +class file_name_manglert +{ +public: + file_name_manglert() + : forbidden("[^\\w]", std::regex::ECMAScript), + multi_under("_+", std::regex::ECMAScript) + { + } + irep_idt operator()(const symbolt &, const std::string &); + +protected: + const std::regex forbidden; + const std::regex multi_under; +}; + +/// \brief Mangle identifiers by hashing their working directory with djb2 hash +/// +/// Hashes emitted by objects of this class include the leading 8 digits of the +/// djb2 hash of the file path. +class djb_manglert +{ +public: + djb_manglert() + { + } + irep_idt operator()(const symbolt &, const std::string &); +}; + +#endif // CPROVER_GOTO_PROGRAMS_NAME_MANGLER_H diff --git a/src/langapi/language.h b/src/langapi/language.h index 046101f7f11..693a9100a09 100644 --- a/src/langapi/language.h +++ b/src/langapi/language.h @@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include @@ -123,6 +124,32 @@ class languaget:public messaget symbol_tablet &symbol_table, const std::string &module)=0; + /// \brief Is it possible to call three-argument typecheck() on this object? + virtual bool can_keep_file_local() + { + return false; + } + + /// \brief typecheck without removing specified entries from the symbol table + /// + /// Some concrete subclasses of \ref languaget discard unused symbols from a + /// goto binary as part of typechecking it. This function allows the caller + /// to specify a list of symbols that should be kept, even if that language's + /// typecheck() implementation would normally discard those symbols. + /// + /// This function should only be called on objects for which a call to + /// can_keep_symbols() returns `true`. + virtual bool typecheck( + symbol_tablet &symbol_table, + const std::string &module, + const bool keep_file_local) + { + INVARIANT( + false, + "three-argument typecheck should only be called for files written" + " in a language that allows file-local symbols, like C"); + } + // language id / description virtual std::string id() const = 0; diff --git a/src/langapi/language_file.cpp b/src/langapi/language_file.cpp index 431de2aa22a..27da3bef681 100644 --- a/src/langapi/language_file.cpp +++ b/src/langapi/language_file.cpp @@ -82,7 +82,9 @@ bool language_filest::parse() return false; } -bool language_filest::typecheck(symbol_tablet &symbol_table) +bool language_filest::typecheck( + symbol_tablet &symbol_table, + const bool keep_file_local) { // typecheck interfaces @@ -129,8 +131,16 @@ bool language_filest::typecheck(symbol_tablet &symbol_table) { if(file.second.modules.empty()) { - if(file.second.language->typecheck(symbol_table, "")) - return true; + if(file.second.language->can_keep_file_local()) + { + if(file.second.language->typecheck(symbol_table, "", keep_file_local)) + return true; + } + else + { + if(file.second.language->typecheck(symbol_table, "")) + return true; + } // register lazy methods. // TODO: learn about modules and generalise this // to module-providing languages if required. @@ -145,7 +155,7 @@ bool language_filest::typecheck(symbol_tablet &symbol_table) for(auto &module : module_map) { - if(typecheck_module(symbol_table, module.second)) + if(typecheck_module(symbol_table, module.second, keep_file_local)) return true; } @@ -195,7 +205,8 @@ bool language_filest::interfaces( bool language_filest::typecheck_module( symbol_tablet &symbol_table, - const std::string &module) + const std::string &module, + const bool keep_file_local) { // check module map @@ -207,12 +218,13 @@ bool language_filest::typecheck_module( return true; } - return typecheck_module(symbol_table, it->second); + return typecheck_module(symbol_table, it->second, keep_file_local); } bool language_filest::typecheck_module( symbol_tablet &symbol_table, - language_modulet &module) + language_modulet &module, + const bool keep_file_local) { // already typechecked? @@ -240,23 +252,29 @@ bool language_filest::typecheck_module( it!=dependency_set.end(); it++) { - if(typecheck_module(symbol_table, *it)) - { - module.in_progress=false; + module.in_progress = !typecheck_module(symbol_table, *it, keep_file_local); + if(module.in_progress == false) return true; - } } // type check it status() << "Type-checking " << module.name << eom; - if(module.file->language->typecheck(symbol_table, module.name)) + if(module.file->language->can_keep_file_local()) { - module.in_progress=false; - return true; + module.in_progress = !module.file->language->typecheck( + symbol_table, module.name, keep_file_local); + } + else + { + module.in_progress = + !module.file->language->typecheck(symbol_table, module.name); } + if(!module.in_progress) + return true; + module.type_checked=true; module.in_progress=false; diff --git a/src/langapi/language_file.h b/src/langapi/language_file.h index 10d73fa29f6..9b1591bd44d 100644 --- a/src/langapi/language_file.h +++ b/src/langapi/language_file.h @@ -107,7 +107,8 @@ class language_filest:public messaget bool generate_support_functions(symbol_tablet &symbol_table); - bool typecheck(symbol_tablet &symbol_table); + bool + typecheck(symbol_tablet &symbol_table, const bool keep_file_local = false); bool final(symbol_table_baset &symbol_table); @@ -141,11 +142,13 @@ class language_filest:public messaget protected: bool typecheck_module( symbol_tablet &symbol_table, - language_modulet &module); + language_modulet &module, + const bool keep_file_local); bool typecheck_module( symbol_tablet &symbol_table, - const std::string &module); + const std::string &module, + const bool keep_file_local); }; #endif // CPROVER_UTIL_LANGUAGE_FILE_H diff --git a/src/linking/remove_internal_symbols.cpp b/src/linking/remove_internal_symbols.cpp index e9fc3742652..16c1e34e3d0 100644 --- a/src/linking/remove_internal_symbols.cpp +++ b/src/linking/remove_internal_symbols.cpp @@ -71,11 +71,17 @@ static void get_symbols( /// http://gcc.gnu.org/ml/gcc/2006-11/msg00006.html /// on "extern inline" /// \param symbol_table: symbol table to clean up +/// \param mh: log handler +/// \param keep_file_local: keep file-local functions with bodies even if we +/// would otherwise remove them void remove_internal_symbols( - symbol_tablet &symbol_table) + symbol_tablet &symbol_table, + message_handlert &mh, + const bool keep_file_local) { namespacet ns(symbol_table); find_symbols_sett exported; + messaget log(mh); // we retain certain special ones find_symbols_sett special; @@ -134,7 +140,13 @@ void remove_internal_symbols( // body? not local (i.e., "static")? if(has_body && (!is_file_local || (config.main==symbol.name.c_str()))) + { get_symbols(ns, symbol, exported); + } + else if(has_body && is_file_local && keep_file_local) + { + get_symbols(ns, symbol, exported); + } } else { diff --git a/src/linking/remove_internal_symbols.h b/src/linking/remove_internal_symbols.h index f9d8a465162..dc77b0d60f3 100644 --- a/src/linking/remove_internal_symbols.h +++ b/src/linking/remove_internal_symbols.h @@ -12,7 +12,13 @@ Author: Daniel Kroening #ifndef CPROVER_LINKING_REMOVE_INTERNAL_SYMBOLS_H #define CPROVER_LINKING_REMOVE_INTERNAL_SYMBOLS_H +#include + +#include + void remove_internal_symbols( - class symbol_tablet &symbol_table); + class symbol_tablet &symbol_table, + message_handlert &, + const bool); #endif // CPROVER_LINKING_REMOVE_INTERNAL_SYMBOLS_H