From 9f79244c3f4e28dc24286ce82ee33b18175c3fc0 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 30 May 2018 15:45:23 +0100 Subject: [PATCH 1/3] C++ front-end: Remove internal symbols before linking This mirrors what the C front-end already does, but requires changes to constant propagation in the C++ front-end: we previously used macros, which serve a very different purpose otherwise. Fixes: #1490 --- regression/goto-cc-cbmc/chain.sh | 11 ++++++----- regression/goto-cc-cbmc/cpp/main.cpp | 4 ++++ regression/goto-cc-cbmc/cpp/test.desc | 8 ++++++++ src/cpp/cpp_declarator_converter.cpp | 5 ----- src/cpp/cpp_instantiate_template.cpp | 10 ++++++++++ src/cpp/cpp_language.cpp | 3 +++ src/cpp/cpp_typecheck_compound_type.cpp | 18 +++++++++++------- src/cpp/cpp_typecheck_enum_type.cpp | 2 ++ src/cpp/cpp_typecheck_resolve.cpp | 21 +++++++++++++++++++++ src/linking/remove_internal_symbols.cpp | 11 +++++++++-- 10 files changed, 74 insertions(+), 19 deletions(-) create mode 100644 regression/goto-cc-cbmc/cpp/main.cpp create mode 100644 regression/goto-cc-cbmc/cpp/test.desc diff --git a/regression/goto-cc-cbmc/chain.sh b/regression/goto-cc-cbmc/chain.sh index 9a344a3ea09..590bd4eb5da 100755 --- a/regression/goto-cc-cbmc/chain.sh +++ b/regression/goto-cc-cbmc/chain.sh @@ -6,13 +6,14 @@ is_windows=$3 options=${*:4:$#-4} name=${*:$#} -name=${name%.c} +base_name=${name%.c} +base_name=${base_name%.cpp} if [[ "${is_windows}" == "true" ]]; then - "${goto_cc}" "${name}.c" - mv "${name}.exe" "${name}.gb" + "${goto_cc}" "${name}" + mv "${base_name}.exe" "${base_name}.gb" else - "${goto_cc}" "${name}.c" -o "${name}.gb" + "${goto_cc}" "${name}" -o "${base_name}.gb" fi -"${cbmc}" "${name}.gb" ${options} +"${cbmc}" "${base_name}.gb" ${options} diff --git a/regression/goto-cc-cbmc/cpp/main.cpp b/regression/goto-cc-cbmc/cpp/main.cpp new file mode 100644 index 00000000000..f8b643afbf2 --- /dev/null +++ b/regression/goto-cc-cbmc/cpp/main.cpp @@ -0,0 +1,4 @@ +int main() +{ + return 0; +} diff --git a/regression/goto-cc-cbmc/cpp/test.desc b/regression/goto-cc-cbmc/cpp/test.desc new file mode 100644 index 00000000000..91d9cf8b52e --- /dev/null +++ b/regression/goto-cc-cbmc/cpp/test.desc @@ -0,0 +1,8 @@ +CORE +main.cpp + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/src/cpp/cpp_declarator_converter.cpp b/src/cpp/cpp_declarator_converter.cpp index 401c7e210ad..5a5f22451f8 100644 --- a/src/cpp/cpp_declarator_converter.cpp +++ b/src/cpp/cpp_declarator_converter.cpp @@ -460,11 +460,6 @@ symbolt &cpp_declarator_convertert::convert_new_symbol( symbol.is_macro=is_typedef && !is_template_parameter; symbol.pretty_name=pretty_name; - // Constant? These are propagated. - if(symbol.type.get_bool(ID_C_constant) && - symbol.value.is_not_nil()) - symbol.is_macro=true; - if(is_code && !symbol.is_type) { // it is a function diff --git a/src/cpp/cpp_instantiate_template.cpp b/src/cpp/cpp_instantiate_template.cpp index 0f283827c9c..dee01cd33f7 100644 --- a/src/cpp/cpp_instantiate_template.cpp +++ b/src/cpp/cpp_instantiate_template.cpp @@ -54,6 +54,16 @@ std::string cpp_typecheckt::template_suffix( else // expression { exprt e=expr; + + if(e.id() == ID_symbol) + { + const symbol_exprt &s = to_symbol_expr(e); + const symbolt &symbol = lookup(s.get_identifier()); + + if(cpp_is_pod(symbol.type) && symbol.type.get_bool(ID_C_constant)) + e = symbol.value; + } + make_constant(e); // this must be a constant, which includes true/false diff --git a/src/cpp/cpp_language.cpp b/src/cpp/cpp_language.cpp index e0fb25e79c5..2ab3735cbea 100644 --- a/src/cpp/cpp_language.cpp +++ b/src/cpp/cpp_language.cpp @@ -20,6 +20,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include +#include #include #include @@ -132,6 +133,8 @@ bool cpp_languaget::typecheck( cpp_parse_tree, new_symbol_table, module, get_message_handler())) return true; + remove_internal_symbols(new_symbol_table, get_message_handler(), false); + return linking(symbol_table, new_symbol_table, get_message_handler()); } diff --git a/src/cpp/cpp_typecheck_compound_type.cpp b/src/cpp/cpp_typecheck_compound_type.cpp index a3962891312..8507eca3b04 100644 --- a/src/cpp/cpp_typecheck_compound_type.cpp +++ b/src/cpp/cpp_typecheck_compound_type.cpp @@ -733,13 +733,6 @@ void cpp_typecheckt::typecheck_compound_declarator( { new_symbol->value.swap(value); c_typecheck_baset::do_initializer(*new_symbol); - - // these are macros if they are PODs and come with a (constant) value - if(new_symbol->type.get_bool(ID_C_constant)) - { - simplify(new_symbol->value, *this); - new_symbol->is_macro=true; - } } else { @@ -771,7 +764,18 @@ void cpp_typecheckt::check_fixed_size_array(typet &type) array_typet &array_type=to_array_type(type); if(array_type.size().is_not_nil()) + { + if(array_type.size().id() == ID_symbol) + { + const symbol_exprt &s = to_symbol_expr(array_type.size()); + const symbolt &symbol = lookup(s.get_identifier()); + + if(cpp_is_pod(symbol.type) && symbol.type.get_bool(ID_C_constant)) + array_type.size() = symbol.value; + } + make_constant_index(array_type.size()); + } // recursive call for multi-dimensional arrays check_fixed_size_array(array_type.subtype()); diff --git a/src/cpp/cpp_typecheck_enum_type.cpp b/src/cpp/cpp_typecheck_enum_type.cpp index 061946fb763..22331739f12 100644 --- a/src/cpp/cpp_typecheck_enum_type.cpp +++ b/src/cpp/cpp_typecheck_enum_type.cpp @@ -63,6 +63,8 @@ void cpp_typecheckt::typecheck_enum_body(symbolt &enum_symbol) symbol.type=enum_tag_type; symbol.is_type=false; symbol.is_macro=true; + symbol.is_file_local = true; + symbol.is_thread_local = true; symbolt *new_symbol; if(symbol_table.move(symbol, new_symbol)) diff --git a/src/cpp/cpp_typecheck_resolve.cpp b/src/cpp/cpp_typecheck_resolve.cpp index 6fcb2fed457..cbbeb9b89f7 100644 --- a/src/cpp/cpp_typecheck_resolve.cpp +++ b/src/cpp/cpp_typecheck_resolve.cpp @@ -22,6 +22,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include #include +#include #include #include #include @@ -1046,6 +1047,26 @@ struct_tag_typet cpp_typecheck_resolvet::disambiguate_template_classes( source_location, primary_template_symbol, full_template_args); + + for(auto &arg : full_template_args_tc.arguments()) + { + if(arg.id() == ID_type) + continue; + if(arg.id() == ID_symbol) + { + const symbol_exprt &s = to_symbol_expr(arg); + const symbolt &symbol = cpp_typecheck.lookup(s.get_identifier()); + + if( + cpp_typecheck.cpp_is_pod(symbol.type) && + symbol.type.get_bool(ID_C_constant)) + { + arg = symbol.value; + } + } + simplify(arg, cpp_typecheck); + } + // go back to where we used to be } diff --git a/src/linking/remove_internal_symbols.cpp b/src/linking/remove_internal_symbols.cpp index 26c0413d83b..977792773c4 100644 --- a/src/linking/remove_internal_symbols.cpp +++ b/src/linking/remove_internal_symbols.cpp @@ -95,6 +95,12 @@ void remove_internal_symbols( special.insert(CPROVER_PREFIX "deallocated"); special.insert(CPROVER_PREFIX "dead_object"); special.insert(CPROVER_PREFIX "rounding_mode"); + special.insert("__new"); + special.insert("__new_array"); + special.insert("__placement_new"); + special.insert("__placement_new_array"); + special.insert("__delete"); + special.insert("__delete_array"); for(symbol_tablet::symbolst::const_iterator it=symbol_table.symbols.begin(); @@ -139,8 +145,9 @@ void remove_internal_symbols( { // body? not local (i.e., "static")? if( - has_body && (!is_file_local || (config.main.has_value() && - symbol.name == config.main.value()))) + has_body && + (!is_file_local || + (config.main.has_value() && symbol.base_name == config.main.value()))) { get_symbols(ns, symbol, exported); } From 30e9554a4ac34e75fbda939fc049711a138f930c Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 23 Apr 2019 21:01:46 +0000 Subject: [PATCH 2/3] Enable internal validation for C++ regression tests We should perform as much sanity checking in regression tests as possible. This required cleaning up unused parameter identifiers and disabling sanity checking of names as is already done for Java, because we similarly have name mangling in C++. --- regression/cbmc-cpp/CMakeLists.txt | 2 +- regression/cbmc-cpp/Makefile | 4 ++-- regression/systemc/CMakeLists.txt | 2 +- regression/systemc/Makefile | 4 ++-- src/cpp/cpp_declarator_converter.cpp | 10 +++++++++- src/util/symbol.cpp | 4 +++- 6 files changed, 18 insertions(+), 8 deletions(-) diff --git a/regression/cbmc-cpp/CMakeLists.txt b/regression/cbmc-cpp/CMakeLists.txt index ea18a04ec8c..d911fb88734 100644 --- a/regression/cbmc-cpp/CMakeLists.txt +++ b/regression/cbmc-cpp/CMakeLists.txt @@ -4,6 +4,6 @@ add_test_pl_tests( ) else() add_test_pl_tests( - "$" + "$ --validate-goto-model --validate-ssa-equation" ) endif() diff --git a/regression/cbmc-cpp/Makefile b/regression/cbmc-cpp/Makefile index 6601ae0d64a..0eb592b2bf3 100644 --- a/regression/cbmc-cpp/Makefile +++ b/regression/cbmc-cpp/Makefile @@ -10,10 +10,10 @@ else endif test: - @../test.pl -e -p -c ../../../src/cbmc/cbmc $(gcc_only) + @../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" $(gcc_only) tests.log: ../test.pl - @../test.pl -e -p -c ../../../src/cbmc/cbmc $(gcc_only) + @../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" $(gcc_only) show: @for dir in *; do \ diff --git a/regression/systemc/CMakeLists.txt b/regression/systemc/CMakeLists.txt index 93d5ee716c2..8ebf053fd6d 100644 --- a/regression/systemc/CMakeLists.txt +++ b/regression/systemc/CMakeLists.txt @@ -1,3 +1,3 @@ add_test_pl_tests( - "$" + "$ --validate-goto-model --validate-ssa-equation" ) diff --git a/regression/systemc/Makefile b/regression/systemc/Makefile index 4964810a03e..2a85866896e 100644 --- a/regression/systemc/Makefile +++ b/regression/systemc/Makefile @@ -1,10 +1,10 @@ default: tests.log test: - @../test.pl -e -p -c ../../../src/cbmc/cbmc + @../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" tests.log: ../test.pl - @../test.pl -e -p -c ../../../src/cbmc/cbmc + @../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" show: @for dir in *; do \ diff --git a/src/cpp/cpp_declarator_converter.cpp b/src/cpp/cpp_declarator_converter.cpp index 5a5f22451f8..ce843c7b5ea 100644 --- a/src/cpp/cpp_declarator_converter.cpp +++ b/src/cpp/cpp_declarator_converter.cpp @@ -302,7 +302,8 @@ void cpp_declarator_convertert::combine_types( if(symbol.value.is_nil()) { symbol_parameter.set_base_name(decl_parameter.get_base_name()); - symbol_parameter.set_identifier(decl_parameter.get_identifier()); + // set an empty identifier when no body is available + symbol_parameter.set_identifier(irep_idt()); symbol_parameter.add_source_location()= decl_parameter.source_location(); } @@ -470,6 +471,13 @@ symbolt &cpp_declarator_convertert::convert_new_symbol( if(member_spec.is_inline()) to_code_type(symbol.type).set_inlined(true); + + if(symbol.value.is_nil()) + { + // we don't need the identifiers + for(auto ¶meter : to_code_type(symbol.type).parameters()) + parameter.set_identifier(irep_idt()); + } } else { diff --git a/src/util/symbol.cpp b/src/util/symbol.cpp index d44fb5f674f..457573c5d8b 100644 --- a/src/util/symbol.cpp +++ b/src/util/symbol.cpp @@ -142,7 +142,9 @@ bool symbolt::is_well_formed() const // Exception: Java symbols' base names do not have type signatures // (for example, they can have name "someclass.method:(II)V" and base name // "method") - if(!has_suffix(id2string(name), id2string(base_name)) && mode != ID_java) + if( + !has_suffix(id2string(name), id2string(base_name)) && mode != ID_java && + mode != ID_cpp) { bool criterion_must_hold = true; From 86d4c0da007d94c0d8bfc245e897826a84c63933 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 17 May 2019 12:36:11 +0000 Subject: [PATCH 3/3] Default C++ language standard on Windows is C++14 While we already configured this in goto-cc, running CBMC with --winx64 or --win32 previously failed to set this. --- src/util/config.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/util/config.cpp b/src/util/config.cpp index b590c44ad33..a943ceb74c2 100644 --- a/src/util/config.cpp +++ b/src/util/config.cpp @@ -915,6 +915,8 @@ bool configt::set(const cmdlinet &cmdline) ansi_c.preprocessor=ansi_ct::preprocessort::GCC; ansi_c.mode=ansi_ct::flavourt::VISUAL_STUDIO; #endif + + cpp.cpp_standard = cppt::cpp_standardt::CPP14; } } else if(os=="macos")