cprover
lazy_goto_modelt Class Reference

A GOTO model that produces function bodies on demand. More...

#include <lazy_goto_model.h>

+ Inheritance diagram for lazy_goto_modelt:
+ Collaboration diagram for lazy_goto_modelt:

Public Types

typedef std::function< void(goto_model_functiont &function, const abstract_goto_modelt &model)> post_process_functiont
 Callback function that post-processes a GOTO function. More...
 
typedef std::function< bool(goto_modelt &goto_model)> post_process_functionst
 Callback function that post-processes a whole GOTO model. More...
 
typedef lazy_goto_functions_mapt::can_generate_function_bodyt can_generate_function_bodyt
 Callback function that determines whether the creator of a lazy_goto_modelt can itself supply a function body for a given name, whether as a fallback or an override. More...
 
typedef lazy_goto_functions_mapt::generate_function_bodyt generate_function_bodyt
 Callback function that may provide a body for a GOTO function, either as a fallback (when we don't have source code for a function, often called a stub function) or as an override (when we do have source code, but want to e.g. More...
 

Public Member Functions

 lazy_goto_modelt (post_process_functiont post_process_function, post_process_functionst post_process_functions, can_generate_function_bodyt driver_program_can_generate_function_body, generate_function_bodyt driver_program_generate_function_body, message_handlert &message_handler)
 Construct a lazy GOTO model, supplying callbacks that customise its behaviour. More...
 
 lazy_goto_modelt (lazy_goto_modelt &&other)
 
lazy_goto_modeltoperator= (lazy_goto_modelt &&other)
 
void initialize (const std::vector< std::string > &files, const optionst &options)
 Performs initial symbol table and language_filest initialization from a given commandline and parsed options. More...
 
void load_all_functions () const
 Eagerly loads all functions from the symbol table. More...
 
void unload (const irep_idt &name) const
 
language_filetadd_language_file (const std::string &filename)
 
const goto_functionstget_goto_functions () const override
 Accessor to retrieve the internal goto_functionst. More...
 
const symbol_tabletget_symbol_table () const override
 Accessor to get the symbol table. More...
 
bool can_produce_function (const irep_idt &id) const override
 Determines if this model can produce a body for the given function. More...
 
const goto_functionst::goto_functiontget_goto_function (const irep_idt &id) override
 Get a GOTO function body. More...
 
void validate (const validation_modet vm=validation_modet::INVARIANT, const goto_model_validation_optionst &goto_model_validation_options=goto_model_validation_optionst{}) const override
 Check that the goto model is well-formed. More...
 
- Public Member Functions inherited from abstract_goto_modelt
virtual ~abstract_goto_modelt ()
 

Static Public Member Functions

template<typename THandler >
static lazy_goto_modelt from_handler_object (THandler &handler, const optionst &options, message_handlert &message_handler)
 Create a lazy_goto_modelt from a object that defines function/module pass handlers. More...
 
static std::unique_ptr< goto_modeltprocess_whole_model_and_freeze (lazy_goto_modelt &&model)
 The model returned here has access to the functions we've already loaded but is frozen in the sense that, with regard to the facility to load new functions, it has let it go. More...
 

Public Attributes

symbol_tabletsymbol_table
 Reference to symbol_table in the internal goto_model. More...
 

Private Member Functions

bool finalize ()
 

Private Attributes

std::unique_ptr< goto_modeltgoto_model
 
const lazy_goto_functions_mapt goto_functions
 
language_filest language_files
 
const post_process_functiont post_process_function
 
const post_process_functionst post_process_functions
 
const can_generate_function_bodyt driver_program_can_generate_function_body
 
const generate_function_bodyt driver_program_generate_function_body
 
message_handlertmessage_handler
 Logging helper field. More...
 

Detailed Description

A GOTO model that produces function bodies on demand.

It owns a language_filest, which is used to populate symbol-table method bodies. They are then passed through goto_convert and any driver-program-supplied post-convert transformations to produce the final GOTO representation of the desired function.

This can be converted to a conventional goto_modelt if desired by calling process_whole_model_and_freeze.

The typical use case looks like:

lazy_goto_modelt model(...callback parameters...);
model.initialize(cmdline.args, options);
model.get_goto_function("needed_function1")
model.get_goto_function("needed_function2");
...
model.get_goto_function("needed_functionN");
// optional:
std::unique_ptr<goto_modelt> concrete_model =
  model.process_whole_model_and_freeze();

See the constructor lazy_goto_modelt::lazy_goto_modelt for more detail on the callbacks needed.

Definition at line 41 of file lazy_goto_model.h.

Member Typedef Documentation

◆ can_generate_function_bodyt

Callback function that determines whether the creator of a lazy_goto_modelt can itself supply a function body for a given name, whether as a fallback or an override.

Only used from can_produce_goto_function, but should only return true for a function that generate_function_body can actually provide a body for, otherwise the lazy_goto_modelt user is likely to end up confused.

Definition at line 69 of file lazy_goto_model.h.

◆ generate_function_bodyt

Callback function that may provide a body for a GOTO function, either as a fallback (when we don't have source code for a function, often called a stub function) or as an override (when we do have source code, but want to e.g.

replace a difficult-to-analyse function body with a simpler model, or outright omission). Gets parameters: function_name: a symbol-table symbol name we're asked to populate symbol_table: symbol table we should add new symbols to, such as function local variables. function: goto_functiont that we may populate. That could be done directly, or by populating the corresponding symbol in the symbol table and calling goto_convert. body_available: true if we have source code for the function body, and so the function will be given a body if this callback declines to provide one. If you only want to provide fallback (stub) bodies, check this is false before proceeding. If it is true and a body is supplied, we are overriding the source code definition. Returns: true if we provided a function body; false otherwise. When true is returned our definition is definitive; when false is returned a body will be generated from source code where available.

Definition at line 92 of file lazy_goto_model.h.

◆ post_process_functionst

Callback function that post-processes a whole GOTO model.

The functions in the model have been produced by goto_convert and then passed through the corresponding post_process_functiont. Returns true on error, in which case lazy_goto_modelt::process_whole_model_and_freeze will return null.

Definition at line 60 of file lazy_goto_model.h.

◆ post_process_functiont

typedef std::function< void(goto_model_functiont &function, const abstract_goto_modelt &model)> lazy_goto_modelt::post_process_functiont

Callback function that post-processes a GOTO function.

The goto_model_functiont passed in has just been produced by goto_convert, and so may contain function pointers, RETURN statements and other GOTO constructs that are conventionally post-processed away. The model parameter can be used to inspect other functions, but the implementation should be aware that there may be GOTO functions that are still to be converted, so it is not in its final state at this point.

Definition at line 53 of file lazy_goto_model.h.

Constructor & Destructor Documentation

◆ lazy_goto_modelt() [1/2]

lazy_goto_modelt::lazy_goto_modelt ( post_process_functiont  post_process_function,
post_process_functionst  post_process_functions,
can_generate_function_bodyt  driver_program_can_generate_function_body,
generate_function_bodyt  driver_program_generate_function_body,
message_handlert message_handler 
)
explicit

Construct a lazy GOTO model, supplying callbacks that customise its behaviour.

Consider using from_handler_object if the callbacks supplied would be members of the same class (i.e. my_drivert::process_goto_function, my_drivert::generate_function_body etc). See the documentation of the parameter types for more precise information on what a given callback should do.

Parameters
post_process_functioncalled to post-process a GOTO function after it is goto_converted but before get_goto_function returns. This usually runs transformations such as remove_returns and remove_virtual_functions. It can be a no-op, in which case GOTO programs will be returned exactly as produced by goto_convert.
post_process_functionscalled to post-process the whole model before process_whole_model_and_freeze returns. This usually runs transformations that can only be applied once all functions to be converted are known, such as dead global variable elimination.
driver_program_can_generate_function_bodyboolean predicate to indicate whether driver_program_generate_function_body can produce a body for a given function name. If this returns true for a particular function, so will can_produce_function.
driver_program_generate_function_bodycalled to give the driver program the opportunity to provide a body for a function. It is passed a boolean indicating whether a body is available conventionally (i.e. generated from source code), so this hook can be used to provide fallbacks for missing functions or to override available functions as you like.
message_handlerused for logging.

◆ lazy_goto_modelt() [2/2]

lazy_goto_modelt::lazy_goto_modelt ( lazy_goto_modelt &&  other)

Member Function Documentation

◆ add_language_file()

language_filet& lazy_goto_modelt::add_language_file ( const std::string &  filename)
inline

Definition at line 189 of file lazy_goto_model.h.

◆ can_produce_function()

bool lazy_goto_modelt::can_produce_function ( const irep_idt id) const
overridevirtual

Determines if this model can produce a body for the given function.

Parameters
idfunction ID to query
Returns
true if we can produce a function body, or false if we would leave it a bodyless stub.

Implements abstract_goto_modelt.

Definition at line 281 of file lazy_goto_model.cpp.

◆ finalize()

bool lazy_goto_modelt::finalize ( )
private

Definition at line 256 of file lazy_goto_model.cpp.

◆ from_handler_object()

template<typename THandler >
static lazy_goto_modelt lazy_goto_modelt::from_handler_object ( THandler &  handler,
const optionst options,
message_handlert message_handler 
)
inlinestatic

Create a lazy_goto_modelt from a object that defines function/module pass handlers.

Its members functions will be used to construct the lazy model: post_process_function gets handler.process_goto_function post_process_functions gets handler.process_goto_functions driver_program_can_generate_function_body gets handler.can_generate_function_body driver_program_generate_function_body gets handler.generate_function_body

Parameters
handlerAn object that defines the handlers
optionsThe options passed to process_goto_functions
message_handlerThe message_handler to use for logging
Template Parameters
THandlera type that defines methods process_goto_function and process_goto_functions

Definition at line 152 of file lazy_goto_model.h.

◆ get_goto_function()

const goto_functionst::goto_functiont& lazy_goto_modelt::get_goto_function ( const irep_idt id)
inlineoverridevirtual

Get a GOTO function body.

id must be a valid symbol-table symbol. Its body is produced by:

  1. If we already have a GOTO function body for id, return it.
  2. If the user's driver_program_generate_function_body function provides a body, pass it through the user's post_process_function callback, store and return it.
  3. If we already have a codet for the function stored in the symbol table, goto_convert it, pass it through the user's post_process_function callback, store it and return it.
  4. Otherwise, if some languaget claims to be able to produce it (this is determined by languaget::methods_provided), call its languaget::convert_lazy_method function. If that results in a codet representation of the function stored in the symbol table, convert it to GOTO and return it as in step (3).

Implements abstract_goto_modelt.

Definition at line 240 of file lazy_goto_model.h.

◆ get_goto_functions()

const goto_functionst& lazy_goto_modelt::get_goto_functions ( ) const
inlineoverridevirtual

Accessor to retrieve the internal goto_functionst.

Use with care; concurrent use of get_goto_function will have side-effects on this map which may surprise users, including invalidating any iterators they have stored.

Implements abstract_goto_modelt.

Definition at line 214 of file lazy_goto_model.h.

◆ get_symbol_table()

const symbol_tablet& lazy_goto_modelt::get_symbol_table ( ) const
inlineoverridevirtual

Accessor to get the symbol table.

Concurrent use of get_goto_function may invalidate iterators or otherwise surprise users by modifying the map underneath them, so this should only be used to lend a reference to code that cannot also call get_goto_function.

Implements abstract_goto_modelt.

Definition at line 219 of file lazy_goto_model.h.

◆ initialize()

void lazy_goto_modelt::initialize ( const std::vector< std::string > &  files,
const optionst options 
)

Performs initial symbol table and language_filest initialization from a given commandline and parsed options.

This is much the same as the initial parsing phase of initialize_goto_model, except that all function bodies may be left blank until get_goto_function is called for the first time. This must be called before get_goto_function is called.

Whether they are in fact left blank depends on the language front-end responsible for a particular function: it may be fully eager, in which case only the goto_convert phase is performed lazily, or fully lazy, in which case no function has a body until get_goto_function is called, or anything in between. At the time of writing only Java-specific frontend programs use lazy_goto_modelt, so only java_bytecode_languaget is relevant, and that front-end supplies practically all methods lazily, apart from __CPROVER__start and __CPROVER_initialize. In general check whether a language implements languaget::convert_lazy_method; any method not handled there must be populated eagerly. See lazy_goto_modelt::get_goto_function for more detail.

Parameters
filessource files and GOTO binaries to load
optionsoptions to pass on to the language front-ends

Definition at line 110 of file lazy_goto_model.cpp.

◆ load_all_functions()

void lazy_goto_modelt::load_all_functions ( ) const

Eagerly loads all functions from the symbol table.

Definition at line 228 of file lazy_goto_model.cpp.

◆ operator=()

lazy_goto_modelt& lazy_goto_modelt::operator= ( lazy_goto_modelt &&  other)
inline

Definition at line 130 of file lazy_goto_model.h.

◆ process_whole_model_and_freeze()

static std::unique_ptr<goto_modelt> lazy_goto_modelt::process_whole_model_and_freeze ( lazy_goto_modelt &&  model)
inlinestatic

The model returned here has access to the functions we've already loaded but is frozen in the sense that, with regard to the facility to load new functions, it has let it go.

Before freezing the functions all module-level passes are run

Parameters
modelThe lazy_goto_modelt to freeze
Returns
The frozen goto_modelt or an empty optional if freezing fails

Definition at line 200 of file lazy_goto_model.h.

◆ unload()

void lazy_goto_modelt::unload ( const irep_idt name) const
inline

Definition at line 187 of file lazy_goto_model.h.

◆ validate()

void lazy_goto_modelt::validate ( const validation_modet  vm = validation_modet::INVARIANT,
const goto_model_validation_optionst goto_model_validation_options = goto_model_validation_optionst{} 
) const
inlineoverridevirtual

Check that the goto model is well-formed.

The validation mode indicates whether well-formedness check failures are reported via DATA_INVARIANT violations or exceptions.

Implements abstract_goto_modelt.

Definition at line 250 of file lazy_goto_model.h.

Member Data Documentation

◆ driver_program_can_generate_function_body

const can_generate_function_bodyt lazy_goto_modelt::driver_program_can_generate_function_body
private

Definition at line 272 of file lazy_goto_model.h.

◆ driver_program_generate_function_body

const generate_function_bodyt lazy_goto_modelt::driver_program_generate_function_body
private

Definition at line 273 of file lazy_goto_model.h.

◆ goto_functions

const lazy_goto_functions_mapt lazy_goto_modelt::goto_functions
private

Definition at line 266 of file lazy_goto_model.h.

◆ goto_model

std::unique_ptr<goto_modelt> lazy_goto_modelt::goto_model
private

Definition at line 259 of file lazy_goto_model.h.

◆ language_files

language_filest lazy_goto_modelt::language_files
private

Definition at line 267 of file lazy_goto_model.h.

◆ message_handler

message_handlert& lazy_goto_modelt::message_handler
private

Logging helper field.

Definition at line 276 of file lazy_goto_model.h.

◆ post_process_function

const post_process_functiont lazy_goto_modelt::post_process_function
private

Definition at line 270 of file lazy_goto_model.h.

◆ post_process_functions

const post_process_functionst lazy_goto_modelt::post_process_functions
private

Definition at line 271 of file lazy_goto_model.h.

◆ symbol_table

symbol_tablet& lazy_goto_modelt::symbol_table

Reference to symbol_table in the internal goto_model.

Definition at line 263 of file lazy_goto_model.h.


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