cprover
code_contractst Class Reference

#include <contracts.h>

+ Collaboration diagram for code_contractst:

Public Types

enum class  skipt { DontSkip , Skip }
 Tells wether to skip or not skip an action. More...
 

Public Member Functions

 code_contractst (goto_modelt &goto_model, messaget &log)
 
bool replace_calls (const std::set< std::string > &)
 Replace all calls to each function in the list with that function's contract. More...
 
bool enforce_contracts (const std::set< std::string > &functions)
 Turn requires & ensures into assumptions and assertions for each of the named functions. More...
 
void apply_loop_contracts ()
 
void check_apply_loop_contracts (const irep_idt &function_name, goto_functionst::goto_functiont &goto_function, const local_may_aliast &local_may_alias, goto_programt::targett loop_head, const loopt &loop, const irep_idt &mode)
 
symbol_tabletget_symbol_table ()
 
goto_functionstget_goto_functions ()
 

Public Attributes

namespacet ns
 

Protected Member Functions

bool enforce_contract (const irep_idt &function)
 Enforce contract of a single function. More...
 
bool check_frame_conditions_function (const irep_idt &function)
 Instrument functions to check frame conditions. More...
 
void check_frame_conditions (const irep_idt &function, goto_programt &body, goto_programt::targett instruction_it, const goto_programt::targett &instruction_end, instrument_spec_assignst &instrument_spec_assigns, skipt skip_parameter_assigns, optionalt< cfg_infot > &cfg_info_opt)
 Insert assertion statements into the goto program to ensure that assigned memory is within the assignable memory frame. More...
 
bool check_for_looped_mallocs (const goto_programt &program)
 Check if there are any malloc statements which may be repeated because of a goto statement that jumps back. More...
 
void instrument_assign_statement (goto_programt::targett &instruction_it, goto_programt &program, instrument_spec_assignst &instrument_spec_assigns, optionalt< cfg_infot > &cfg_info_opt)
 Inserts an assertion into program immediately before the assignment instruction_it, to ensure that the left-hand-side of the assignment is "included" in the (conditional address ranges in the) write set. More...
 
void instrument_call_statement (goto_programt::targett &instruction_it, const irep_idt &function, goto_programt &body, instrument_spec_assignst &instrument_spec_assigns, optionalt< cfg_infot > &cfg_info_opt)
 Inserts an assertion into program immediately before the function call at instruction_it, to ensure that all memory locations written to by the. More...
 
void apply_loop_contract (const irep_idt &function, goto_functionst::goto_functiont &goto_function)
 Apply loop contracts, whenever available, to all loops in function. More...
 
bool apply_function_contract (const irep_idt &function, const source_locationt &location, goto_programt &function_body, goto_programt::targett &target)
 Replaces function calls with assertions based on requires clauses, non-deterministic assignments for the write set, and assumptions based on ensures clauses. More...
 
void add_contract_check (const irep_idt &wrapper_function, const irep_idt &mangled_function, goto_programt &dest)
 Instruments wrapper_function adding assumptions based on requires clauses and assertions based on ensures clauses. More...
 
void add_quantified_variable (const exprt &expression, replace_symbolt &replace, const irep_idt &mode)
 This function recursively searches the expression to find nested or non-nested quantified expressions. More...
 
void replace_history_parameter (exprt &expr, std::map< exprt, exprt > &parameter2history, source_locationt location, const irep_idt &mode, goto_programt &history, const irep_idt &id)
 This function recursively identifies the "old" expressions within expr and replaces them with correspoding history variables. More...
 
std::pair< goto_programt, goto_programtcreate_ensures_instruction (codet &expression, source_locationt location, const irep_idt &mode)
 This function creates and returns an instruction that corresponds to the ensures clause. More...
 

Protected Attributes

symbol_tabletsymbol_table
 
goto_functionstgoto_functions
 
messagetlog
 
goto_convertt converter
 
std::unordered_set< irep_idtsummarized
 

Detailed Description

Definition at line 53 of file contracts.h.

Member Enumeration Documentation

◆ skipt

enum class code_contractst::skipt
strong

Tells wether to skip or not skip an action.

Enumerator
DontSkip 
Skip 

Definition at line 115 of file contracts.h.

Constructor & Destructor Documentation

◆ code_contractst()

code_contractst::code_contractst ( goto_modelt goto_model,
messaget log 
)
inline

Definition at line 56 of file contracts.h.

Member Function Documentation

◆ add_contract_check()

void code_contractst::add_contract_check ( const irep_idt wrapper_function,
const irep_idt mangled_function,
goto_programt dest 
)
protected

Instruments wrapper_function adding assumptions based on requires clauses and assertions based on ensures clauses.

Definition at line 1414 of file contracts.cpp.

◆ add_quantified_variable()

void code_contractst::add_quantified_variable ( const exprt expression,
replace_symbolt replace,
const irep_idt mode 
)
protected

This function recursively searches the expression to find nested or non-nested quantified expressions.

When a quantified expression is found, the quantified variable is added to the symbol table and to the expression map.

Definition at line 499 of file contracts.cpp.

◆ apply_function_contract()

bool code_contractst::apply_function_contract ( const irep_idt function,
const source_locationt location,
goto_programt function_body,
goto_programt::targett target 
)
protected

Replaces function calls with assertions based on requires clauses, non-deterministic assignments for the write set, and assumptions based on ensures clauses.

Definition at line 661 of file contracts.cpp.

◆ apply_loop_contract()

void code_contractst::apply_loop_contract ( const irep_idt function,
goto_functionst::goto_functiont goto_function 
)
protected

Apply loop contracts, whenever available, to all loops in function.

Loop invariants, loop variants, and loop assigns clauses.

Definition at line 870 of file contracts.cpp.

◆ apply_loop_contracts()

void code_contractst::apply_loop_contracts ( )

Definition at line 1610 of file contracts.cpp.

◆ check_apply_loop_contracts()

void code_contractst::check_apply_loop_contracts ( const irep_idt function_name,
goto_functionst::goto_functiont goto_function,
const local_may_aliast local_may_alias,
goto_programt::targett  loop_head,
const loopt loop,
const irep_idt mode 
)

Definition at line 138 of file contracts.cpp.

◆ check_for_looped_mallocs()

bool code_contractst::check_for_looped_mallocs ( const goto_programt program)
protected

Check if there are any malloc statements which may be repeated because of a goto statement that jumps back.

Definition at line 1025 of file contracts.cpp.

◆ check_frame_conditions()

void code_contractst::check_frame_conditions ( const irep_idt function,
goto_programt body,
goto_programt::targett  instruction_it,
const goto_programt::targett instruction_end,
instrument_spec_assignst instrument_spec_assigns,
skipt  skip_parameter_assigns,
optionalt< cfg_infot > &  cfg_info_opt 
)
protected

Insert assertion statements into the goto program to ensure that assigned memory is within the assignable memory frame.

Parameters
functionName of the function getting instrumented.
bodyBody of the function getting instrumented.
instruction_itIterator to the instruction from which to start instrumentation (inclusive).
instruction_endIterator to the instruction at which to stop instrumentation (exclusive).
instrument_spec_assignsAssigns clause instrumenter of the function
skip_parameter_assignsIf true, will cause assignments to symbol marked as is_parameter to not be instrumented.
cfg_info_optControl flow graph information can will be used for write set optimisation if available.

Definition at line 1253 of file contracts.cpp.

◆ check_frame_conditions_function()

bool code_contractst::check_frame_conditions_function ( const irep_idt function)
protected

Instrument functions to check frame conditions.

Definition at line 1088 of file contracts.cpp.

◆ create_ensures_instruction()

std::pair< goto_programt, goto_programt > code_contractst::create_ensures_instruction ( codet expression,
source_locationt  location,
const irep_idt mode 
)
protected

This function creates and returns an instruction that corresponds to the ensures clause.

It also returns a list of instructions related to initializing history variables, if required.

Definition at line 639 of file contracts.cpp.

◆ enforce_contract()

bool code_contractst::enforce_contract ( const irep_idt function)
protected

Enforce contract of a single function.

Definition at line 1351 of file contracts.cpp.

◆ enforce_contracts()

bool code_contractst::enforce_contracts ( const std::set< std::string > &  functions)

Turn requires & ensures into assumptions and assertions for each of the named functions.

Use this function to prove the correctness of a function F independently of its calling context. If you have proved that F is correct, then you can soundly replace all calls to F with F's contract using the code_contractst::replace_calls() function; this means that symbolic execution does not need to explore F every time it is called, increasing scalability.

Implementation: mangle the name of each function F into a new name, __CPROVER_contracts_original_F (CF for short). Then mint a new function called F that assumes CF's requires clause, calls CF, and then asserts CF's ensures clause.

Returns
true on failure, false otherwise

Definition at line 1616 of file contracts.cpp.

◆ get_goto_functions()

goto_functionst & code_contractst::get_goto_functions ( )

Definition at line 958 of file contracts.cpp.

◆ get_symbol_table()

symbol_tablet & code_contractst::get_symbol_table ( )

Definition at line 953 of file contracts.cpp.

◆ instrument_assign_statement()

void code_contractst::instrument_assign_statement ( goto_programt::targett instruction_it,
goto_programt program,
instrument_spec_assignst instrument_spec_assigns,
optionalt< cfg_infot > &  cfg_info_opt 
)
protected

Inserts an assertion into program immediately before the assignment instruction_it, to ensure that the left-hand-side of the assignment is "included" in the (conditional address ranges in the) write set.

Definition at line 963 of file contracts.cpp.

◆ instrument_call_statement()

void code_contractst::instrument_call_statement ( goto_programt::targett instruction_it,
const irep_idt function,
goto_programt body,
instrument_spec_assignst instrument_spec_assigns,
optionalt< cfg_infot > &  cfg_info_opt 
)
protected

Inserts an assertion into program immediately before the function call at instruction_it, to ensure that all memory locations written to by the.

Definition at line 977 of file contracts.cpp.

◆ replace_calls()

bool code_contractst::replace_calls ( const std::set< std::string > &  to_replace)

Replace all calls to each function in the list with that function's contract.

Use this function when proving code that calls into an expensive function, F. You can write a contract for F using __CPROVER_requires and __CPROVER_ensures, and then use this function to replace all calls to F with an assertion that the requires clause holds followed by an assumption that the ensures clause holds. In order to ensure that F actually abides by its ensures and requires clauses, you should separately call code_constractst::enforce_contracts() on F and verify it using cbmc --function F.

Returns
true on failure, false otherwise

Definition at line 1567 of file contracts.cpp.

◆ replace_history_parameter()

void code_contractst::replace_history_parameter ( exprt expr,
std::map< exprt, exprt > &  parameter2history,
source_locationt  location,
const irep_idt mode,
goto_programt history,
const irep_idt id 
)
protected

This function recursively identifies the "old" expressions within expr and replaces them with correspoding history variables.

Definition at line 565 of file contracts.cpp.

Member Data Documentation

◆ converter

goto_convertt code_contractst::converter
protected

Definition at line 126 of file contracts.h.

◆ goto_functions

goto_functionst& code_contractst::goto_functions
protected

Definition at line 123 of file contracts.h.

◆ log

messaget& code_contractst::log
protected

Definition at line 125 of file contracts.h.

◆ ns

namespacet code_contractst::ns

Definition at line 112 of file contracts.h.

◆ summarized

std::unordered_set<irep_idt> code_contractst::summarized
protected

Definition at line 128 of file contracts.h.

◆ symbol_table

symbol_tablet& code_contractst::symbol_table
protected

Definition at line 122 of file contracts.h.


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