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_modelt &	operator= (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...

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

const goto_functionst &	get_goto_functions () const override
	Accessor to retrieve the internal goto_functionst. More...

const symbol_tablet &	get_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_functiont &	get_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_modelt >	process_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_tablet &	symbol_table
	Reference to symbol_table in the internal goto_model. More...

Private Member Functions
bool	finalize ()

Private Attributes
std::unique_ptr< goto_modelt >	goto_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_handlert &	message_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

typedef lazy_goto_functions_mapt::can_generate_function_bodyt lazy_goto_modelt::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

typedef lazy_goto_functions_mapt::generate_function_bodyt lazy_goto_modelt::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<bool(goto_modelt &goto_model)> 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.

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_function	called to post-process a GOTO function after it is `goto_convert`ed 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

◆ add_language_file()

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

inline

Definition at line 185 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 237 of file lazy_goto_model.cpp.

◆ finalize()

bool lazy_goto_modelt::finalize ( )

private

Definition at line 212 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:

If we already have a GOTO function body for id, return it.
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.
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.
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 237 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 210 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 215 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.

◆ load_all_functions()

void lazy_goto_modelt::load_all_functions ( ) const

Eagerly loads all functions from the symbol table.

Definition at line 183 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

model The lazy_goto_modelt to freeze

Returns: The frozen goto_modelt or an empty optional if freezing fails

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

◆ goto_functions

const lazy_goto_functions_mapt lazy_goto_modelt::goto_functions

private

Definition at line 262 of file lazy_goto_model.h.

◆ goto_model

std::unique_ptr<goto_modelt> lazy_goto_modelt::goto_model

private

Definition at line 255 of file lazy_goto_model.h.

◆ language_files

language_filest lazy_goto_modelt::language_files

private

Definition at line 263 of file lazy_goto_model.h.

◆ message_handler

message_handlert& lazy_goto_modelt::message_handler

private

Logging helper field.

Definition at line 272 of file lazy_goto_model.h.

◆ post_process_function

const post_process_functiont lazy_goto_modelt::post_process_function

private

Definition at line 266 of file lazy_goto_model.h.

◆ post_process_functions

const post_process_functionst lazy_goto_modelt::post_process_functions

private

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

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

/home/runner/work/cbmc/cbmc/jbmc/src/java_bytecode/lazy_goto_model.h
/home/runner/work/cbmc/cbmc/jbmc/src/java_bytecode/lazy_goto_model.cpp

Public Types

Public Member Functions

Static Public Member Functions

Public Attributes

Private Member Functions

Private Attributes

Detailed Description

Member Typedef Documentation

◆ can_generate_function_bodyt

◆ generate_function_bodyt

◆ post_process_functionst

◆ post_process_functiont

Constructor & Destructor Documentation

◆ lazy_goto_modelt() [1/2]

◆ lazy_goto_modelt() [2/2]

Member Function Documentation

◆ add_language_file()

◆ can_produce_function()

◆ finalize()

◆ from_handler_object()

◆ get_goto_function()

◆ get_goto_functions()

◆ get_symbol_table()

◆ initialize()

◆ load_all_functions()

◆ operator=()

◆ process_whole_model_and_freeze()

◆ validate()

Member Data Documentation

◆ driver_program_can_generate_function_body

◆ driver_program_generate_function_body

◆ goto_functions

◆ goto_model

◆ language_files

◆ message_handler

◆ post_process_function

◆ post_process_functions

◆ symbol_table