cprover
lazy_goto_modelt Class Reference

Model that holds partially loaded map of functions. More...

#include <lazy_goto_model.h>

Inheritance diagram for lazy_goto_modelt:
[legend]
Collaboration diagram for lazy_goto_modelt:
[legend]

Public Types

typedef std::function< void(goto_model_functiont &function, const abstract_goto_modelt &)> post_process_functiont
 
typedef std::function< bool(goto_modelt &goto_model)> post_process_functionst
 
typedef lazy_goto_functions_mapt::can_generate_function_bodyt can_generate_function_bodyt
 
typedef lazy_goto_functions_mapt::generate_function_bodyt generate_function_bodyt
 

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)
 
 lazy_goto_modelt (lazy_goto_modelt &&other)
 
lazy_goto_modeltoperator= (lazy_goto_modelt &&other)
 
void initialize (const cmdlinet &cmdline)
 
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 by name, or throw if no such function exists. 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

Model that holds partially loaded map of functions.

Definition at line 20 of file lazy_goto_model.h.

Member Typedef Documentation

◆ can_generate_function_bodyt

◆ generate_function_bodyt

◆ post_process_functionst

Definition at line 26 of file lazy_goto_model.h.

◆ post_process_functiont

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

Referenced by from_handler_object().

◆ 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 92 of file lazy_goto_model.h.

References language_filest::add_file(), and language_files.

Referenced by initialize().

◆ 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 268 of file lazy_goto_model.cpp.

References lazy_goto_functions_mapt::can_produce_function(), and goto_functions.

◆ finalize()

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

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 56 of file lazy_goto_model.h.

References goto_model, lazy_goto_modelt(), message_handler, and symbol_table.

Referenced by jbmc_parse_optionst::doit(), and jbmc_parse_optionst::get_goto_program().

◆ get_goto_function()

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

Get a GOTO function by name, or throw if no such function exists.

May have side-effects on the GOTO function map provided by get_goto_functions, or the symbol table returned by get_symbol_table, so iterators pointing into either may be invalidated.

Parameters
idfunction to get
Returns
function body

Implements abstract_goto_modelt.

Definition at line 129 of file lazy_goto_model.h.

References lazy_goto_functions_mapt::at(), and goto_functions.

◆ 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 117 of file lazy_goto_model.h.

References goto_model.

◆ 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 122 of file lazy_goto_model.h.

References symbol_table.

◆ initialize()

◆ load_all_functions()

void lazy_goto_modelt::load_all_functions ( ) const

Eagerly loads all functions from the symbol table.

Definition at line 215 of file lazy_goto_model.cpp.

References lazy_goto_functions_mapt::ensure_function_loaded(), goto_functions, goto_model, size_type(), symbol_table, and symbol_table_baset::symbols.

Referenced by jbmc_parse_optionst::get_goto_program().

◆ operator=()

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

Definition at line 41 of file lazy_goto_model.h.

References goto_model, and language_files.

◆ 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 103 of file lazy_goto_model.h.

Referenced by jbmc_parse_optionst::get_goto_program(), and load_java_class().

◆ unload()

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

Definition at line 90 of file lazy_goto_model.h.

References goto_functions, and lazy_goto_functions_mapt::unload().

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 149 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 150 of file lazy_goto_model.h.

◆ goto_functions

const lazy_goto_functions_mapt lazy_goto_modelt::goto_functions
private

◆ goto_model

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

◆ language_files

language_filest lazy_goto_modelt::language_files
private

Definition at line 144 of file lazy_goto_model.h.

Referenced by add_language_file(), finalize(), initialize(), and operator=().

◆ message_handler

message_handlert& lazy_goto_modelt::message_handler
private

Logging helper field.

Definition at line 153 of file lazy_goto_model.h.

Referenced by finalize(), from_handler_object(), and initialize().

◆ post_process_function

const post_process_functiont lazy_goto_modelt::post_process_function
private

Definition at line 147 of file lazy_goto_model.h.

◆ post_process_functions

const post_process_functionst lazy_goto_modelt::post_process_functions
private

Definition at line 148 of file lazy_goto_model.h.

Referenced by finalize().

◆ symbol_table

symbol_tablet& lazy_goto_modelt::symbol_table

Reference to symbol_table in the internal goto_model.

Definition at line 140 of file lazy_goto_model.h.

Referenced by jbmc_parse_optionst::doit(), finalize(), from_handler_object(), jbmc_parse_optionst::get_goto_program(), get_symbol_table(), initialize(), and load_all_functions().


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