cprover
|
#include <language.h>
Public Member Functions | |
virtual void | get_language_options (const cmdlinet &) |
virtual bool | preprocess (std::istream &instream, const std::string &path, std::ostream &outstream) |
virtual bool | parse (std::istream &instream, const std::string &path)=0 |
virtual bool | generate_support_functions (symbol_tablet &symbol_table)=0 |
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and language-specific library functions. More... | |
virtual void | dependencies (const std::string &module, std::set< std::string > &modules) |
virtual void | modules_provided (std::set< std::string > &modules) |
virtual void | methods_provided (std::unordered_set< irep_idt > &methods) const |
virtual void | convert_lazy_method (const irep_idt &function_id, symbol_table_baset &symbol_table) |
virtual bool | final (symbol_table_baset &symbol_table) |
Final adjustments, e.g. More... | |
virtual bool | interfaces (symbol_tablet &symbol_table) |
virtual bool | typecheck (symbol_tablet &symbol_table, const std::string &module)=0 |
virtual std::string | id () const |
virtual std::string | description () const |
virtual std::set< std::string > | extensions () const |
virtual void | show_parse (std::ostream &out)=0 |
virtual bool | from_expr (const exprt &expr, std::string &code, const namespacet &ns) |
Formats the given expression in a language-specific way. More... | |
virtual bool | from_type (const typet &type, std::string &code, const namespacet &ns) |
Formats the given type in a language-specific way. More... | |
virtual bool | type_to_name (const typet &type, std::string &name, const namespacet &ns) |
Encodes the given type in a language-specific way. More... | |
virtual bool | to_expr (const std::string &code, const std::string &module, exprt &expr, const namespacet &ns)=0 |
Parses the given string into an expression. More... | |
virtual std::unique_ptr< languaget > | new_language ()=0 |
void | set_should_generate_opaque_method_stubs (bool should_generate_stubs) |
Turn on or off stub generation. More... | |
languaget () | |
virtual | ~languaget () |
Protected Member Functions | |
void | generate_opaque_method_stubs (symbol_tablet &symbol_table) |
When there are opaque methods (e.g. More... | |
virtual irep_idt | generate_opaque_stub_body (symbolt &symbol, symbol_tablet &symbol_table) |
To generate the stub function for the opaque function in question. More... | |
virtual parameter_symbolt | build_stub_parameter_symbol (const symbolt &function_symbol, size_t parameter_index, const code_typet::parametert ¶meter) |
To build the parameter symbol and choose its name. More... | |
Static Protected Member Functions | |
static irep_idt | get_stub_return_symbol_name (const irep_idt &function_id) |
To get the name of the symbol to be used for the return value of the function. More... | |
Protected Attributes | |
bool | generate_opaque_stubs =false |
bool | language_options_initialized =false |
Private Member Functions | |
bool | is_symbol_opaque_function (const symbolt &symbol) |
To identify if a given symbol is an opaque function and hence needs to be stubbed. More... | |
void | generate_opaque_parameter_symbols (symbolt &function_symbol, symbol_tablet &symbol_table) |
To create stub parameter symbols for each parameter the function has and assign their IDs into the parameters identifier. More... | |
Private Attributes | |
system_library_symbolst | system_symbols |
Additional Inherited Members |
Definition at line 39 of file language.h.
|
inline |
Definition at line 165 of file language.h.
|
inlinevirtual |
Definition at line 166 of file language.h.
|
protectedvirtual |
To build the parameter symbol and choose its name.
This should be implemented in each language.
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 |
Definition at line 129 of file language.cpp.
References messaget::eom(), messaget::error(), and id().
Referenced by generate_opaque_parameter_symbols().
|
inlinevirtual |
Reimplemented in java_bytecode_languaget.
Definition at line 85 of file language.h.
|
virtual |
Definition at line 31 of file language.cpp.
|
inlinevirtual |
Reimplemented in java_bytecode_languaget, cpp_languaget, ansi_c_languaget, and jsil_languaget.
Definition at line 107 of file language.h.
|
inlinevirtual |
Reimplemented in java_bytecode_languaget, cpp_languaget, ansi_c_languaget, and jsil_languaget.
Definition at line 108 of file language.h.
Referenced by register_language().
|
virtual |
Final adjustments, e.g.
initializing stub functions and globals that were discovered during function loading
Reimplemented in java_bytecode_languaget.
Definition at line 21 of file language.cpp.
Referenced by load_java_class().
|
virtual |
Formats the given expression in a language-specific way.
expr | the expression to format |
code | the formatted expression |
ns | a namespace |
Reimplemented in java_bytecode_languaget, cpp_languaget, jsil_languaget, and ansi_c_languaget.
Definition at line 37 of file language.cpp.
References irept::pretty().
Referenced by from_expr(), json(), language_uit::show_symbol_table_plain(), and show_symbol_table_plain().
|
virtual |
Formats the given type in a language-specific way.
type | the type to format |
code | the formatted type |
ns | a namespace |
Reimplemented in java_bytecode_languaget, cpp_languaget, jsil_languaget, and ansi_c_languaget.
Definition at line 46 of file language.cpp.
References irept::pretty().
Referenced by from_type(), json(), show_symbol_table_brief_plain(), language_uit::show_symbol_table_plain(), and show_symbol_table_plain().
|
protected |
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.
symbol_table | the symbol table for the program |
Definition at line 79 of file language.cpp.
References generate_opaque_parameter_symbols(), generate_opaque_stub_body(), generate_opaque_stubs, symbol_tablet::get_writeable(), is_symbol_opaque_function(), irept::set(), symbol_table_baset::symbols, system_symbols, and symbolt::type.
Referenced by ansi_c_languaget::generate_support_functions().
|
private |
To create stub parameter symbols for each parameter the function has and assign their IDs into the parameters identifier.
function_symbol | the symbol of an opaque function |
symbol_table | the symbol table to add the new parameter symbols into |
Definition at line 177 of file language.cpp.
References symbol_table_baset::add(), symbolt::base_name, build_stub_parameter_symbol(), symbolt::name, code_typet::parameters(), code_typet::parametert::set_base_name(), code_typet::parametert::set_identifier(), to_code_type(), and symbolt::type.
Referenced by generate_opaque_method_stubs().
|
protectedvirtual |
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.
symbol | the function symbol which is opaque |
symbol_table | the symbol table |
Definition at line 114 of file language.cpp.
Referenced by generate_opaque_method_stubs().
|
pure virtual |
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and language-specific library functions.
This runs after the typecheck
phase but before lazy function loading. Anything that must wait until lazy function loading is done can be deferred until final
, which runs after lazy function loading is complete. Functions introduced here are visible to lazy loading and can influence its decisions (e.g. picking the types of input parameters and globals), whereas anything introduced during final
cannot.
Implemented in java_bytecode_languaget, cpp_languaget, jsil_languaget, and ansi_c_languaget.
Referenced by load_java_class(), and rebuild_goto_start_function_baset< maybe_lazy_goto_modelt >::operator()().
|
inlinevirtual |
Reimplemented in java_bytecode_languaget.
Definition at line 43 of file language.h.
Referenced by cbmc_parse_optionst::doit(), jbmc_parse_optionst::doit(), lazy_goto_modelt::initialize(), initialize_goto_model(), load_java_class(), rebuild_goto_start_function_baset< maybe_lazy_goto_modelt >::operator()(), language_uit::parse(), and cbmc_parse_optionst::preprocessing().
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
function_id | the function that has a return value |
Definition at line 146 of file language.cpp.
|
inlinevirtual |
Reimplemented in java_bytecode_languaget, cpp_languaget, ansi_c_languaget, and jsil_languaget.
Definition at line 106 of file language.h.
Referenced by build_stub_parameter_symbol(), and register_language().
|
virtual |
Reimplemented in jsil_languaget.
Definition at line 26 of file language.cpp.
|
private |
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.
symbol | the symbol to be checked |
Definition at line 159 of file language.cpp.
References irept::id(), system_library_symbolst::is_symbol_internal_symbol(), symbolt::is_type, system_symbols, symbolt::type, and symbolt::value.
Referenced by generate_opaque_method_stubs().
|
inlinevirtual |
Reimplemented in java_bytecode_languaget.
Definition at line 80 of file language.h.
|
inlinevirtual |
Reimplemented in java_bytecode_languaget, cpp_languaget, ansi_c_languaget, and jsil_languaget.
Definition at line 75 of file language.h.
|
pure virtual |
Implemented in java_bytecode_languaget, cpp_languaget, ansi_c_languaget, and jsil_languaget.
|
pure virtual |
|
inlinevirtual |
Reimplemented in java_bytecode_languaget, cpp_languaget, jsil_languaget, and ansi_c_languaget.
Definition at line 47 of file language.h.
Referenced by cbmc_parse_optionst::preprocessing().
void languaget::set_should_generate_opaque_method_stubs | ( | bool | should_generate_stubs | ) |
Turn on or off stub generation.
should_generate_stubs | Should stub generation be enabled |
Definition at line 68 of file language.cpp.
References generate_opaque_stubs.
|
pure virtual |
Implemented in java_bytecode_languaget, cpp_languaget, jsil_languaget, and ansi_c_languaget.
Referenced by cbmc_parse_optionst::doit(), and jbmc_parse_optionst::doit().
|
pure virtual |
Parses the given string into an expression.
code | the string to parse |
module | prefix to be used for identifiers |
expr | the parsed expression |
ns | a namespace |
Implemented in java_bytecode_languaget, cpp_languaget, ansi_c_languaget, and jsil_languaget.
Referenced by to_expr().
|
virtual |
Encodes the given type in a language-specific way.
type | the type to encode |
name | the encoded type |
ns | a namespace |
Reimplemented in cpp_languaget, and ansi_c_languaget.
Definition at line 55 of file language.cpp.
References irept::pretty().
Referenced by type_to_name().
|
pure virtual |
Implemented in java_bytecode_languaget, cpp_languaget, jsil_languaget, and ansi_c_languaget.
Referenced by load_java_class().
|
protected |
Definition at line 181 of file language.h.
Referenced by generate_opaque_method_stubs(), and set_should_generate_opaque_method_stubs().
|
protected |
Definition at line 182 of file language.h.
Referenced by java_bytecode_languaget::final(), java_bytecode_languaget::generate_support_functions(), java_bytecode_languaget::get_language_options(), java_bytecode_languaget::parse(), and java_bytecode_languaget::typecheck().
|
private |
Definition at line 190 of file language.h.
Referenced by generate_opaque_method_stubs(), and is_symbol_opaque_function().