cprover
languaget Class Referenceabstract

#include <language.h>

+ Inheritance diagram for languaget:
+ Collaboration diagram for languaget:

Public Member Functions

virtual void set_language_options (const optionst &)
 Set language-specific options. More...
 
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< languagetnew_language ()=0
 
void set_should_generate_opaque_method_stubs (bool should_generate_stubs)
 Turn on or off stub generation. More...
 
 languaget ()
 
virtual ~languaget ()
 
- Public Member Functions inherited from messaget
virtual void set_message_handler (message_handlert &_message_handler)
 
message_handlertget_message_handler ()
 
 messaget ()
 
 messaget (const messaget &other)
 
messagetoperator= (const messaget &other)
 
 messaget (message_handlert &_message_handler)
 
virtual ~messaget ()
 
mstreamtget_mstream (unsigned message_level) const
 
mstreamterror () const
 
mstreamtwarning () const
 
mstreamtresult () const
 
mstreamtstatus () const
 
mstreamtstatistics () const
 
mstreamtprogress () const
 
mstreamtdebug () const
 
void conditional_output (mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
 Generate output to message_stream using output_generator if the configured verbosity is at least as high as that of message_stream. More...
 

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 &parameter)
 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
 
- Protected Attributes inherited from messaget
message_handlertmessage_handler
 
mstreamt mstream
 

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

- Public Types inherited from messaget
enum  message_levelt {
  M_ERROR =1, M_WARNING =2, M_RESULT =4, M_STATUS =6,
  M_STATISTICS =8, M_PROGRESS =9, M_DEBUG =10
}
 
- Static Public Member Functions inherited from messaget
static unsigned eval_verbosity (const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
 Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest. More...
 
static commandt command (unsigned c)
 Create an ECMA-48 SGR (Select Graphic Rendition) command. More...
 
- Static Public Attributes inherited from messaget
static eomt eom
 
static const commandt reset
 return to default formatting, as defined by the terminal More...
 
static const commandt red
 render text with red foreground color More...
 
static const commandt green
 render text with green foreground color More...
 
static const commandt yellow
 render text with yellow foreground color More...
 
static const commandt blue
 render text with blue foreground color More...
 
static const commandt magenta
 render text with magenta foreground color More...
 
static const commandt cyan
 render text with cyan foreground color More...
 
static const commandt bright_red
 render text with bright red foreground color More...
 
static const commandt bright_green
 render text with bright green foreground color More...
 
static const commandt bright_yellow
 render text with bright yellow foreground color More...
 
static const commandt bright_blue
 render text with bright blue foreground color More...
 
static const commandt bright_magenta
 render text with bright magenta foreground color More...
 
static const commandt bright_cyan
 render text with bright cyan foreground color More...
 
static const commandt bold
 render text with bold font More...
 
static const commandt faint
 render text with faint font More...
 
static const commandt italic
 render italic text More...
 
static const commandt underline
 render underlined text More...
 

Detailed Description

Definition at line 39 of file language.h.

Constructor & Destructor Documentation

◆ languaget()

languaget::languaget ( )
inline

Definition at line 182 of file language.h.

◆ ~languaget()

virtual languaget::~languaget ( )
inlinevirtual

Definition at line 183 of file language.h.

Member Function Documentation

◆ build_stub_parameter_symbol()

parameter_symbolt languaget::build_stub_parameter_symbol ( const symbolt function_symbol,
size_t  parameter_index,
const code_typet::parametert parameter 
)
protectedvirtual

To build the parameter symbol and choose its name.

This should be implemented in each language.

Parameters
function_symbolthe symbol of an opaque function
parameter_indexthe index of the parameter within the the parameter list
parameter_typethe type of the parameter
Returns
A named symbol to be added to the symbol table representing one of the parameters in this opaque function.

Definition at line 132 of file language.cpp.

◆ convert_lazy_method()

virtual void languaget::convert_lazy_method ( const irep_idt function_id,
symbol_table_baset symbol_table 
)
inlinevirtual

Reimplemented in java_bytecode_languaget.

Definition at line 98 of file language.h.

◆ dependencies()

void languaget::dependencies ( const std::string &  module,
std::set< std::string > &  modules 
)
virtual

Definition at line 31 of file language.cpp.

◆ description()

virtual std::string languaget::description ( ) const
inlinevirtual

Reimplemented in java_bytecode_languaget, cpp_languaget, ansi_c_languaget, and jsil_languaget.

Definition at line 124 of file language.h.

◆ extensions()

virtual std::set<std::string> languaget::extensions ( ) const
inlinevirtual

Reimplemented in java_bytecode_languaget, cpp_languaget, ansi_c_languaget, and jsil_languaget.

Definition at line 125 of file language.h.

◆ final()

bool languaget::final ( symbol_table_baset symbol_table)
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.

◆ from_expr()

bool languaget::from_expr ( const exprt expr,
std::string &  code,
const namespacet ns 
)
virtual

Formats the given expression in a language-specific way.

Parameters
exprthe expression to format
codethe formatted expression
nsa namespace
Returns
false if conversion succeeds

Reimplemented in java_bytecode_languaget, cpp_languaget, jsil_languaget, and ansi_c_languaget.

Definition at line 37 of file language.cpp.

◆ from_type()

bool languaget::from_type ( const typet type,
std::string &  code,
const namespacet ns 
)
virtual

Formats the given type in a language-specific way.

Parameters
typethe type to format
codethe formatted type
nsa namespace
Returns
false if conversion succeeds

Reimplemented in java_bytecode_languaget, cpp_languaget, jsil_languaget, and ansi_c_languaget.

Definition at line 46 of file language.cpp.

◆ generate_opaque_method_stubs()

void languaget::generate_opaque_method_stubs ( symbol_tablet symbol_table)
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.

Parameters
symbol_tablethe symbol table for the program

Definition at line 79 of file language.cpp.

◆ generate_opaque_parameter_symbols()

void languaget::generate_opaque_parameter_symbols ( symbolt function_symbol,
symbol_tablet symbol_table 
)
private

To create stub parameter symbols for each parameter the function has and assign their IDs into the parameters identifier.

Parameters
function_symbolthe symbol of an opaque function
symbol_tablethe symbol table to add the new parameter symbols into

Definition at line 184 of file language.cpp.

◆ generate_opaque_stub_body()

irep_idt languaget::generate_opaque_stub_body ( symbolt symbol,
symbol_tablet symbol_table 
)
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.

Parameters
symbolthe function symbol which is opaque
symbol_tablethe symbol table
Returns
The identifier of the return variable. ID_nil if the function doesn't return anything.

Definition at line 114 of file language.cpp.

◆ generate_support_functions()

virtual bool languaget::generate_support_functions ( symbol_tablet symbol_table)
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.

◆ get_stub_return_symbol_name()

irep_idt languaget::get_stub_return_symbol_name ( const irep_idt function_id)
staticprotected

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

Parameters
function_idthe function that has a return value
Returns
the identifier to use for the symbol that will store the return value of this function.

Definition at line 153 of file language.cpp.

◆ id()

virtual std::string languaget::id ( ) const
inlinevirtual

Reimplemented in java_bytecode_languaget, cpp_languaget, ansi_c_languaget, and jsil_languaget.

Definition at line 123 of file language.h.

◆ interfaces()

bool languaget::interfaces ( symbol_tablet symbol_table)
virtual

Reimplemented in jsil_languaget.

Definition at line 26 of file language.cpp.

◆ is_symbol_opaque_function()

bool languaget::is_symbol_opaque_function ( const symbolt symbol)
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.

Parameters
symbolthe symbol to be checked
Returns
True if the symbol is an opaque (e.g. non-bodied) function

Definition at line 166 of file language.cpp.

◆ methods_provided()

virtual void languaget::methods_provided ( std::unordered_set< irep_idt > &  methods) const
inlinevirtual

Reimplemented in java_bytecode_languaget.

Definition at line 91 of file language.h.

◆ modules_provided()

virtual void languaget::modules_provided ( std::set< std::string > &  modules)
inlinevirtual

Reimplemented in java_bytecode_languaget, cpp_languaget, ansi_c_languaget, and jsil_languaget.

Definition at line 84 of file language.h.

◆ new_language()

virtual std::unique_ptr<languaget> languaget::new_language ( )
pure virtual

◆ parse()

virtual bool languaget::parse ( std::istream &  instream,
const std::string &  path 
)
pure virtual

◆ preprocess()

virtual bool languaget::preprocess ( std::istream &  instream,
const std::string &  path,
std::ostream &  outstream 
)
inlinevirtual

Reimplemented in java_bytecode_languaget, cpp_languaget, jsil_languaget, and ansi_c_languaget.

Definition at line 49 of file language.h.

◆ set_language_options()

virtual void languaget::set_language_options ( const optionst )
inlinevirtual

Set language-specific options.

Reimplemented in java_bytecode_languaget.

Definition at line 43 of file language.h.

◆ set_should_generate_opaque_method_stubs()

void languaget::set_should_generate_opaque_method_stubs ( bool  should_generate_stubs)

Turn on or off stub generation.

Parameters
should_generate_stubsShould stub generation be enabled

Definition at line 68 of file language.cpp.

◆ show_parse()

virtual void languaget::show_parse ( std::ostream &  out)
pure virtual

◆ to_expr()

virtual bool languaget::to_expr ( const std::string &  code,
const std::string &  module,
exprt expr,
const namespacet ns 
)
pure virtual

Parses the given string into an expression.

Parameters
codethe string to parse
moduleprefix to be used for identifiers
exprthe parsed expression
nsa namespace
Returns
false if the conversion succeeds

Implemented in java_bytecode_languaget, cpp_languaget, ansi_c_languaget, and jsil_languaget.

◆ type_to_name()

bool languaget::type_to_name ( const typet type,
std::string &  name,
const namespacet ns 
)
virtual

Encodes the given type in a language-specific way.

Parameters
typethe type to encode
namethe encoded type
nsa namespace
Returns
false if the conversion succeeds

Reimplemented in cpp_languaget, and ansi_c_languaget.

Definition at line 55 of file language.cpp.

◆ typecheck()

virtual bool languaget::typecheck ( symbol_tablet symbol_table,
const std::string &  module 
)
pure virtual

Member Data Documentation

◆ generate_opaque_stubs

bool languaget::generate_opaque_stubs =false
protected

Definition at line 198 of file language.h.

◆ language_options_initialized

bool languaget::language_options_initialized =false
protected

Definition at line 199 of file language.h.

◆ system_symbols

system_library_symbolst languaget::system_symbols
private

Definition at line 207 of file language.h.


The documentation for this class was generated from the following files: