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...

Eagerly loads all functions from the symbol table. More...

void unload (const irep_idt &name) const

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) 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...

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.

## ◆ 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

 typedef std::function lazy_goto_modelt::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.

## ◆ 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_function called 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_functions called 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_body boolean 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_body called 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_handler used for logging.

## ◆ lazy_goto_modelt() [2/2]

 lazy_goto_modelt::lazy_goto_modelt ( lazy_goto_modelt && other )

## Member Function Documentation

 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
 id function 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
 handler An object that defines the handlers options The options passed to process_goto_functions message_handler The message_handler to use for logging
Template Parameters
 THandler a 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
 files source files and GOTO binaries to load options options to pass on to the language front-ends

Definition at line 110 of file lazy_goto_model.cpp.

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 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
 model The 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.

 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 ) 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.

## ◆ driver_program_can_generate_function_body

 const can_generate_function_bodyt lazy_goto_modelt::driver_program_can_generate_function_body
private

Definition at line 269 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 270 of file lazy_goto_model.h.

## ◆ goto_functions

 const lazy_goto_functions_mapt lazy_goto_modelt::goto_functions
private

Definition at line 263 of file lazy_goto_model.h.

## ◆ goto_model

 std::unique_ptr lazy_goto_modelt::goto_model
private

Definition at line 256 of file lazy_goto_model.h.

## ◆ language_files

 language_filest lazy_goto_modelt::language_files
private

Definition at line 264 of file lazy_goto_model.h.

## ◆ message_handler

 message_handlert& lazy_goto_modelt::message_handler
private

Logging helper field.

Definition at line 273 of file lazy_goto_model.h.

## ◆ post_process_function

 const post_process_functiont lazy_goto_modelt::post_process_function
private

Definition at line 267 of file lazy_goto_model.h.

## ◆ post_process_functions

 const post_process_functionst lazy_goto_modelt::post_process_functions
private

Definition at line 268 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 260 of file lazy_goto_model.h.

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