diff --git a/regression/.gitignore b/regression/.gitignore new file mode 100644 index 00000000000..750ecf9f446 --- /dev/null +++ b/regression/.gitignore @@ -0,0 +1 @@ +tests.log diff --git a/src/ansi-c/ansi_c_language.cpp b/src/ansi-c/ansi_c_language.cpp index dc69515ede2..159b0d6df40 100644 --- a/src/ansi-c/ansi_c_language.cpp +++ b/src/ansi-c/ansi_c_language.cpp @@ -196,6 +196,8 @@ Function: ansi_c_languaget::final bool ansi_c_languaget::final(symbol_tablet &symbol_table) { + generate_opaque_method_stubs(symbol_table); + if(ansi_c_entry_point(symbol_table, "main", get_message_handler())) return true; diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index a6975bdab19..5de8c7688b0 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -518,28 +518,40 @@ std::string expr2ct::convert_rec( } else if(src.id()==ID_symbol) { - const typet &followed=ns.follow(src); + symbol_typet symbolic_type=to_symbol_type(src); + const irep_idt &typedef_identifer=symbolic_type.get(ID_typedef); - if(followed.id()==ID_struct) + // Providing we have a valid identifer, we can just use that rather than + // trying to find the concrete type + if(typedef_identifer!="") { - std::string dest=q+"struct"; - const irep_idt &tag=to_struct_type(followed).get_tag(); - if(tag!="") - dest+=" "+id2string(tag); - dest+=d; - return dest; + return q+id2string(typedef_identifer)+d; } - else if(followed.id()==ID_union) + else { - std::string dest=q+"union"; - const irep_idt &tag=to_union_type(followed).get_tag(); - if(tag!="") - dest+=" "+id2string(tag); - dest+=d; - return dest; + const typet &followed=ns.follow(src); + + if(followed.id()==ID_struct) + { + std::string dest=q+"struct"; + const irep_idt &tag=to_struct_type(followed).get_tag(); + if(tag!="") + dest+=" "+id2string(tag); + dest+=d; + return dest; + } + else if(followed.id()==ID_union) + { + std::string dest=q+"union"; + const irep_idt &tag=to_union_type(followed).get_tag(); + if(tag!="") + dest+=" "+id2string(tag); + dest+=d; + return dest; + } + else + return convert_rec(followed, new_qualifiers, declarator); } - else - return convert_rec(followed, new_qualifiers, declarator); } else if(src.id()==ID_struct_tag) { diff --git a/src/langapi/language_ui.cpp b/src/langapi/language_ui.cpp index 95b5d104a4f..4b0f3fa0d75 100644 --- a/src/langapi/language_ui.cpp +++ b/src/langapi/language_ui.cpp @@ -183,6 +183,10 @@ bool language_uit::final() { language_files.set_message_handler(*message_handler); + // Enable/disable stub generation for opaque methods + bool stubs_enabled=_cmdline.isset("generate-opaque-stubs"); + language_files.set_should_generate_opaque_method_stubs(stubs_enabled); + if(language_files.final(symbol_table)) { if(get_ui()==ui_message_handlert::PLAIN) diff --git a/src/util/language.cpp b/src/util/language.cpp index 4b4a1ba4ae4..ddb41979040 100644 --- a/src/util/language.cpp +++ b/src/util/language.cpp @@ -8,6 +8,11 @@ Author: Daniel Kroening, kroening@kroening.com #include "language.h" #include "expr.h" +#include +#include +#include +#include +#include /*******************************************************************\ @@ -125,3 +130,209 @@ bool languaget::type_to_name( name=type.pretty(); return false; } + +/*******************************************************************\ + +Function: languaget::set_should_generate_opaque_method_stubs + + Inputs: + should_generate_stubs - Should stub generation be enabled + + Outputs: + + Purpose: Turn on or off stub generation. + +\*******************************************************************/ +void languaget::set_should_generate_opaque_method_stubs( + bool should_generate_stubs) +{ + generate_opaque_stubs=should_generate_stubs; +} + +/*******************************************************************\ + +Function: languaget::generate_opaque_method_stubs + + Inputs: + symbol_table - the symbol table for the program + + Outputs: + + Purpose: When there are opaque methods (e.g. ones where we don't + have a body), we create a stub function in the goto + program and mark it as opaque so the interpreter fills in + appropriate values for it. This will only happen if + generate_opaque_stubs is enabled. + +\*******************************************************************/ + +void languaget::generate_opaque_method_stubs(symbol_tablet &symbol_table) +{ + if(generate_opaque_stubs) + { + system_symbols=system_library_symbolst(); + + for(auto &symbol_entry : symbol_table.symbols) + { + if(is_symbol_opaque_function(symbol_entry.second)) + { + symbolt &symbol=symbol_entry.second; + + generate_opaque_parameter_symbols(symbol, symbol_table); + + irep_idt return_symbol_id=generate_opaque_stub_body( + symbol, + symbol_table); + + if(return_symbol_id!=ID_nil) + { + symbol.type.set("opaque_method_capture_symbol", return_symbol_id); + } + } + } + } +} + +/*******************************************************************\ + +Function: languaget::generate_opaque_stub_body + + Inputs: + symbol - the function symbol which is opaque + symbol_table - the symbol table + + Outputs: The identifier of the return variable. ID_nil if the function + doesn't return anything. + + Purpose: To generate the stub function for the opaque function in + question. The identifier is used in the flag to the interpreter + that the function is opaque. This function should be implemented + in the languages. + +\*******************************************************************/ + +irep_idt languaget::generate_opaque_stub_body( + symbolt &symbol, + symbol_tablet &symbol_table) +{ + return ID_nil; +} + +/*******************************************************************\ + +Function: languaget::build_stub_parameter_symbol + + Inputs: + function_symbol - the symbol of an opaque function + parameter_index - the index of the parameter within the + the parameter list + parameter_type - the type of the parameter + + Outputs: A named symbol to be added to the symbol table representing + one of the parameters in this opaque function. + + Purpose: To build the parameter symbol and choose its name. This should + be implemented in each language. + +\*******************************************************************/ + +parameter_symbolt languaget::build_stub_parameter_symbol( + const symbolt &function_symbol, + size_t parameter_index, + const code_typet::parametert ¶meter) +{ + error() << "language " << id() + << " doesn't implement build_stub_parameter_symbol. " + << "This means cannot use opaque functions." << eom; + + return parameter_symbolt(); +} + +/*******************************************************************\ + +Function: languaget::get_stub_return_symbol_name + + Inputs: + function_id - the function that has a return value + + Outputs: the identifier to use for the symbol that will store the + return value of this function. + + Purpose: To get the name of the symbol to be used for the return value + of the function. Generates a name like to_return_function_name + +\*******************************************************************/ + +irep_idt languaget::get_stub_return_symbol_name(const irep_idt &function_id) +{ + std::ostringstream return_symbol_name_builder; + return_symbol_name_builder << "to_return_" << function_id; + return return_symbol_name_builder.str(); +} + + +/*******************************************************************\ + +Function: languaget::is_symbol_opaque_function + + Inputs: + symbol - the symbol to be checked + + Outputs: True if the symbol is an opaque (e.g. non-bodied) function + + Purpose: To identify if a given symbol is an opaque function and + hence needs to be stubbed. We explicitly exclude CPROVER + functions, if they have no body it is because we haven't + generated it yet. + +\*******************************************************************/ + +bool languaget::is_symbol_opaque_function(const symbolt &symbol) +{ + std::set headers; + // Don't create stubs for symbols like: + // __CPROVER_blah (which aren't real external functions) + // and strstr (which we will model for ourselves later) + bool is_internal=system_symbols.is_symbol_internal_symbol(symbol, headers); + + return !symbol.is_type && + symbol.value.id()==ID_nil && + symbol.type.id()==ID_code && + !is_internal; +} + +/*******************************************************************\ + +Function: languaget::generate_opaque_parameter_symbols + + Inputs: + function_symbol - the symbol of an opaque function + symbol_table - the symbol table to add the new parameter + symbols into + + Outputs: + + Purpose: To create stub parameter symbols for each parameter the + function has and assign their IDs into the parameters + identifier. + +\*******************************************************************/ + +void languaget::generate_opaque_parameter_symbols( + symbolt &function_symbol, + symbol_tablet &symbol_table) +{ + code_typet &function_type = to_code_type(function_symbol.type); + code_typet::parameterst ¶meters=function_type.parameters(); + for(std::size_t i=0; i #include #include +#include +#include +#include #include "message.h" @@ -110,9 +113,34 @@ class languaget:public messaget virtual languaget *new_language()=0; + void set_should_generate_opaque_method_stubs(bool should_generate_stubs); + // constructor / destructor languaget() { } virtual ~languaget() { } + +protected: + void generate_opaque_method_stubs(symbol_tablet &symbol_table); + virtual irep_idt generate_opaque_stub_body( + symbolt &symbol, + symbol_tablet &symbol_table); + + virtual parameter_symbolt build_stub_parameter_symbol( + const symbolt &function_symbol, + size_t parameter_index, + const code_typet::parametert ¶meter); + + static irep_idt get_stub_return_symbol_name(const irep_idt &function_id); + + bool generate_opaque_stubs; + +private: + bool is_symbol_opaque_function(const symbolt &symbol); + void generate_opaque_parameter_symbols( + symbolt &function_symbol, + symbol_tablet &symbol_table); + + system_library_symbolst system_symbols; }; #endif // CPROVER_UTIL_LANGUAGE_H diff --git a/src/util/language_file.cpp b/src/util/language_file.cpp index 46f51564b54..b0fbb47c2f9 100644 --- a/src/util/language_file.cpp +++ b/src/util/language_file.cpp @@ -93,6 +93,28 @@ void language_filest::show_parse(std::ostream &out) /*******************************************************************\ +Function: language_filest::set_should_generate_opqaue_method_stubs + + Inputs: + should_generate_stubs - Should stub generation be enabled + + Outputs: + + Purpose: Turn on or off stub generation for all the languages + +\*******************************************************************/ + +void language_filest::set_should_generate_opaque_method_stubs( + bool stubs_enabled) +{ + for(file_mapt::value_type &language_file_entry : file_map) + { + languaget *language=language_file_entry.second.language; + language->set_should_generate_opaque_method_stubs(stubs_enabled); + } +} + +/*******************************************************************\ Function: language_filest::parse Inputs: diff --git a/src/util/language_file.h b/src/util/language_file.h index d3184d48697..9fffc7f14f1 100644 --- a/src/util/language_file.h +++ b/src/util/language_file.h @@ -75,6 +75,8 @@ class language_filest:public messaget file_map.clear(); } + void set_should_generate_opaque_method_stubs(bool stubs_enabled); + bool parse(); void show_parse(std::ostream &out);