CBMC
dfcc_lift_memory_predicatest Class Reference

#include <dfcc_lift_memory_predicates.h>

+ Collaboration diagram for dfcc_lift_memory_predicatest:

Public Member Functions

 dfcc_lift_memory_predicatest (goto_modelt &goto_model, dfcc_libraryt &library, dfcc_instrumentt &instrument, message_handlert &message_handler)
 
std::set< irep_idtlift_predicates (std::set< irep_idt > &discovered_function_pointer_contracts)
 Collects and lifts all user-defined memory predicates. More...
 
void fix_calls (goto_programt &program)
 Fixes calls to user-defined memory predicates in the given program, by adding an address-of to arguments passed in lifted position. More...
 
void fix_calls (goto_programt &program, goto_programt::targett first_instruction, const goto_programt::targett &last_instruction)
 Fixes calls to user-defined memory predicates in the given program, by adding an address-of to arguments passed in lifted position, between first_instruction (included) and last_instruction (excluded). More...
 

Protected Member Functions

bool calls_memory_predicates (const goto_programt &goto_program, const std::set< irep_idt > &predicates)
 Returns true iff goto_program calls core memory predicates. More...
 
void lift_predicate (const irep_idt &function_id, std::set< irep_idt > &discovered_function_pointer_contracts)
 
void lift_parameters_and_update_body (const irep_idt &function_id, std::set< irep_idt > &discovered_function_pointer_contracts)
 
void add_pointer_type (const irep_idt &function_id, const std::size_t parameter_rank, replace_symbolt &replace_lifted_param)
 adds a pointer_type to the parameter of a function More...
 
void collect_parameters_to_lift (const irep_idt &function_id)
 Computes the subset of function parameters of function_id that are passed directly to core predicates and must be lifted. More...
 
bool is_lifted_function (const irep_idt &function_id)
 True if a function at least had one of its parameters lifted. More...
 

Protected Attributes

goto_modeltgoto_model
 
dfcc_librarytlibrary
 
dfcc_instrumenttinstrument
 
messaget log
 
std::map< irep_idt, std::set< std::size_t > > lifted_parameters
 

Detailed Description

Definition at line 36 of file dfcc_lift_memory_predicates.h.

Constructor & Destructor Documentation

◆ dfcc_lift_memory_predicatest()

dfcc_lift_memory_predicatest::dfcc_lift_memory_predicatest ( goto_modelt goto_model,
dfcc_libraryt library,
dfcc_instrumentt instrument,
message_handlert message_handler 
)
Parameters
goto_modelThe goto model to process
libraryThe contracts instrumentation library
instrumentThe DFCC instrumenter object
message_handlerUsed for messages

Definition at line 25 of file dfcc_lift_memory_predicates.cpp.

Member Function Documentation

◆ add_pointer_type()

void dfcc_lift_memory_predicatest::add_pointer_type ( const irep_idt function_id,
const std::size_t  parameter_rank,
replace_symbolt replace_lifted_param 
)
protected

adds a pointer_type to the parameter of a function

Parameters
function_idThe function to update
parameter_rankThe parameter to update
replace_lifted_paramSymbol replacer (receives p ~> *p mappings) The parameter symbol gets updated in the symbol table and the function signature gets updated with the new type.

Definition at line 276 of file dfcc_lift_memory_predicates.cpp.

◆ calls_memory_predicates()

bool dfcc_lift_memory_predicatest::calls_memory_predicates ( const goto_programt goto_program,
const std::set< irep_idt > &  predicates 
)
protected

Returns true iff goto_program calls core memory predicates.

or one of the functions found in predicates .

Definition at line 52 of file dfcc_lift_memory_predicates.cpp.

◆ collect_parameters_to_lift()

void dfcc_lift_memory_predicatest::collect_parameters_to_lift ( const irep_idt function_id)
protected

Computes the subset of function parameters of function_id that are passed directly to core predicates and must be lifted.

Definition at line 212 of file dfcc_lift_memory_predicates.cpp.

◆ fix_calls() [1/2]

void dfcc_lift_memory_predicatest::fix_calls ( goto_programt program)

Fixes calls to user-defined memory predicates in the given program, by adding an address-of to arguments passed in lifted position.

Definition at line 394 of file dfcc_lift_memory_predicates.cpp.

◆ fix_calls() [2/2]

void dfcc_lift_memory_predicatest::fix_calls ( goto_programt program,
goto_programt::targett  first_instruction,
const goto_programt::targett last_instruction 
)

Fixes calls to user-defined memory predicates in the given program, by adding an address-of to arguments passed in lifted position, between first_instruction (included) and last_instruction (excluded).

Definition at line 399 of file dfcc_lift_memory_predicates.cpp.

◆ is_lifted_function()

bool dfcc_lift_memory_predicatest::is_lifted_function ( const irep_idt function_id)
protected

True if a function at least had one of its parameters lifted.

True if a function had at least one of its parameters lifted.

Definition at line 38 of file dfcc_lift_memory_predicates.cpp.

◆ lift_parameters_and_update_body()

void dfcc_lift_memory_predicatest::lift_parameters_and_update_body ( const irep_idt function_id,
std::set< irep_idt > &  discovered_function_pointer_contracts 
)
protected

Definition at line 317 of file dfcc_lift_memory_predicates.cpp.

◆ lift_predicate()

void dfcc_lift_memory_predicatest::lift_predicate ( const irep_idt function_id,
std::set< irep_idt > &  discovered_function_pointer_contracts 
)
protected

Definition at line 362 of file dfcc_lift_memory_predicates.cpp.

◆ lift_predicates()

std::set< irep_idt > dfcc_lift_memory_predicatest::lift_predicates ( std::set< irep_idt > &  discovered_function_pointer_contracts)

Collects and lifts all user-defined memory predicates.

Parameters
[out]discovered_function_pointer_contractsSet of function pointer contracts discovered during instrumentation
Returns
The set of predicates that were lifted

Definition at line 76 of file dfcc_lift_memory_predicates.cpp.

Member Data Documentation

◆ goto_model

goto_modelt& dfcc_lift_memory_predicatest::goto_model
protected

Definition at line 69 of file dfcc_lift_memory_predicates.h.

◆ instrument

dfcc_instrumentt& dfcc_lift_memory_predicatest::instrument
protected

Definition at line 71 of file dfcc_lift_memory_predicates.h.

◆ library

dfcc_libraryt& dfcc_lift_memory_predicatest::library
protected

Definition at line 70 of file dfcc_lift_memory_predicates.h.

◆ lifted_parameters

std::map<irep_idt, std::set<std::size_t> > dfcc_lift_memory_predicatest::lifted_parameters
protected

Definition at line 74 of file dfcc_lift_memory_predicates.h.

◆ log

messaget dfcc_lift_memory_predicatest::log
protected

Definition at line 72 of file dfcc_lift_memory_predicates.h.


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