cprover
code_contractst Class Reference

#include <contracts.h>

+ Collaboration diagram for code_contractst:

Public Member Functions

 code_contractst (goto_modelt &goto_model, messaget &log)
 
bool replace_calls (const std::set< std::string > &functions)
 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...
 
bool enforce_contracts ()
 Call enforce_contracts() on all functions that have a contract. More...
 
bool replace_calls ()
 Call replace_calls() on all calls to any function that has a contract. More...
 
void apply_loop_contracts ()
 
const symboltnew_tmp_symbol (const typet &type, const source_locationt &source_location, const irep_idt &mode)
 
void check_apply_loop_contracts (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 (goto_programt &program, const symbolt &target)
 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::instructionst::iterator &instruction_it, goto_programt &program, exprt &assigns, std::set< irep_idt > &freely_assignable_symbols, assigns_clauset &assigns_clause)
 Inserts an assertion statement into program before the assignment instruction_it, to ensure that the left-hand-side of the assignment aliases some expression in original_references, unless it is contained in freely_assignable_exprs. More...
 
void instrument_call_statement (goto_programt::instructionst::iterator &ins_it, goto_programt &program, exprt &assigns, std::set< irep_idt > &freely_assignable_symbols, assigns_clauset &assigns_clause)
 Inserts an assertion statement into program before the function call at ins_it, to ensure that any memory which may be written by the call is aliased by some expression in assigns_references,unless it is contained in freely_assignable_exprs. More...
 
exprt create_alias_expression (const exprt &lhs, std::vector< exprt > &aliasable_references)
 Creates a boolean expression which is true when there exists an expression in aliasable_references with the same pointer object and pointer offset as the address of lhs. 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 has_contract (const irep_idt)
 Does the named function have a contract? More...
 
bool apply_function_contract (goto_programt &goto_program, 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 61 of file contracts.h.

Constructor & Destructor Documentation

◆ code_contractst()

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

Definition at line 64 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 1047 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 327 of file contracts.cpp.

◆ apply_function_contract()

bool code_contractst::apply_function_contract ( goto_programt goto_program,
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 475 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 625 of file contracts.cpp.

◆ apply_loop_contracts()

void code_contractst::apply_loop_contracts ( )

Definition at line 1244 of file contracts.cpp.

◆ check_apply_loop_contracts()

void code_contractst::check_apply_loop_contracts ( 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 95 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 823 of file contracts.cpp.

◆ check_frame_conditions()

void code_contractst::check_frame_conditions ( goto_programt program,
const symbolt target 
)
protected

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

Definition at line 914 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 886 of file contracts.cpp.

◆ create_alias_expression()

exprt code_contractst::create_alias_expression ( const exprt lhs,
std::vector< exprt > &  aliasable_references 
)
protected

Creates a boolean expression which is true when there exists an expression in aliasable_references with the same pointer object and pointer offset as the address of lhs.

Definition at line 669 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 453 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 984 of file contracts.cpp.

◆ enforce_contracts() [1/2]

bool code_contractst::enforce_contracts ( )

Call enforce_contracts() on all functions that have a contract.

Returns
true on failure, false otherwise

Definition at line 1261 of file contracts.cpp.

◆ enforce_contracts() [2/2]

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 1272 of file contracts.cpp.

◆ get_goto_functions()

goto_functionst & code_contractst::get_goto_functions ( )

Definition at line 664 of file contracts.cpp.

◆ get_symbol_table()

symbol_tablet & code_contractst::get_symbol_table ( )

Definition at line 659 of file contracts.cpp.

◆ has_contract()

bool code_contractst::has_contract ( const irep_idt  fun_name)
protected

Does the named function have a contract?

Definition at line 320 of file contracts.cpp.

◆ instrument_assign_statement()

void code_contractst::instrument_assign_statement ( goto_programt::instructionst::iterator &  instruction_it,
goto_programt program,
exprt assigns,
std::set< irep_idt > &  freely_assignable_symbols,
assigns_clauset assigns_clause 
)
protected

Inserts an assertion statement into program before the assignment instruction_it, to ensure that the left-hand-side of the assignment aliases some expression in original_references, unless it is contained in freely_assignable_exprs.

Definition at line 682 of file contracts.cpp.

◆ instrument_call_statement()

void code_contractst::instrument_call_statement ( goto_programt::instructionst::iterator &  ins_it,
goto_programt program,
exprt assigns,
std::set< irep_idt > &  freely_assignable_symbols,
assigns_clauset assigns_clause 
)
protected

Inserts an assertion statement into program before the function call at ins_it, to ensure that any memory which may be written by the call is aliased by some expression in assigns_references,unless it is contained in freely_assignable_exprs.

Definition at line 711 of file contracts.cpp.

◆ new_tmp_symbol()

const symbolt & code_contractst::new_tmp_symbol ( const typet type,
const source_locationt source_location,
const irep_idt mode 
)

Definition at line 645 of file contracts.cpp.

◆ replace_calls() [1/2]

bool code_contractst::replace_calls ( )

Call replace_calls() on all calls to any function that has a contract.

Returns
true on failure, false otherwise

Definition at line 1250 of file contracts.cpp.

◆ replace_calls() [2/2]

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

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 1195 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 395 of file contracts.cpp.

Member Data Documentation

◆ converter

goto_convertt code_contractst::converter
protected

Definition at line 141 of file contracts.h.

◆ goto_functions

goto_functionst& code_contractst::goto_functions
protected

Definition at line 138 of file contracts.h.

◆ log

messaget& code_contractst::log
protected

Definition at line 140 of file contracts.h.

◆ ns

namespacet code_contractst::ns

Definition at line 134 of file contracts.h.

◆ summarized

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

Definition at line 143 of file contracts.h.

◆ symbol_table

symbol_tablet& code_contractst::symbol_table
protected

Definition at line 137 of file contracts.h.


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