cprover
code_contractst Class Reference

#include <code_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 > &)
 Replace all calls to each function in the list with that function's contract. More...
 
bool enforce_contracts (const std::set< std::string > &)
 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...
 
const symboltnew_tmp_symbol (const typet &type, const source_locationt &source_location, const irep_idt &function_id, const irep_idt &mode)
 

Public Attributes

namespacet ns
 

Protected Member Functions

bool enforce_contract (const std::string &)
 Enforce contract of a single function. More...
 
void convert_to_goto (const codet &code, const irep_idt &mode, goto_programt &program)
 Create goto instructions based on code and add them to program. More...
 
bool add_pointer_checks (const std::string &)
 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 &)
 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, const irep_idt &function_id, 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...
 
void populate_assigns_reference (std::vector< exprt > operands, const symbolt &function_symbol, const irep_idt &function_id, goto_programt &created_declarations, std::vector< exprt > &created_references)
 Creates a local variable declaration for each expression in operands, and stores them in created_declarations. 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 (goto_functionst::goto_functiont &goto_function)
 
bool has_contract (const irep_idt)
 Does the named function have a contract? More...
 
bool apply_function_contract (const irep_idt &function_id, goto_programt &goto_program, goto_programt::targett target)
 
void add_contract_check (const irep_idt &, const irep_idt &, goto_programt &dest)
 
void add_quantified_variable (exprt expression, replace_symbolt &replace, irep_idt mode)
 This function recursively searches the expression to find nested or non-nested quantified expressions. More...
 

Protected Attributes

symbol_tabletsymbol_table
 
goto_functionstgoto_functions
 
unsigned temporary_counter
 
messagetlog
 
std::unordered_set< irep_idtsummarized
 

Detailed Description

Definition at line 33 of file code_contracts.h.

Constructor & Destructor Documentation

◆ code_contractst()

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

Definition at line 36 of file code_contracts.h.

Member Function Documentation

◆ add_contract_check()

void code_contractst::add_contract_check ( const irep_idt wrapper_fun,
const irep_idt mangled_fun,
goto_programt dest 
)
protected

Definition at line 783 of file code_contracts.cpp.

◆ add_pointer_checks()

bool code_contractst::add_pointer_checks ( const std::string &  function_name)
protected

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

Definition at line 615 of file code_contracts.cpp.

◆ add_quantified_variable()

void code_contractst::add_quantified_variable ( exprt  expression,
replace_symbolt replace,
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 177 of file code_contracts.cpp.

◆ apply_function_contract()

bool code_contractst::apply_function_contract ( const irep_idt function_id,
goto_programt goto_program,
goto_programt::targett  target 
)
protected

Definition at line 247 of file code_contracts.cpp.

◆ apply_loop_contract()

void code_contractst::apply_loop_contract ( goto_functionst::goto_functiont goto_function)
protected

Definition at line 385 of file code_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 562 of file code_contracts.cpp.

◆ convert_to_goto()

void code_contractst::convert_to_goto ( const codet code,
const irep_idt mode,
goto_programt program 
)
protected

Create goto instructions based on code and add them to program.

Definition at line 161 of file code_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 412 of file code_contracts.cpp.

◆ enforce_contract()

bool code_contractst::enforce_contract ( const std::string &  fun_to_enforce)
protected

Enforce contract of a single function.

Definition at line 721 of file code_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 976 of file code_contracts.cpp.

◆ enforce_contracts() [2/2]

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

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 989 of file code_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 170 of file code_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 425 of file code_contracts.cpp.

◆ instrument_call_statement()

void code_contractst::instrument_call_statement ( goto_programt::instructionst::iterator &  ins_it,
goto_programt program,
exprt assigns,
const irep_idt function_id,
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 449 of file code_contracts.cpp.

◆ new_tmp_symbol()

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

Definition at line 397 of file code_contracts.cpp.

◆ populate_assigns_reference()

void code_contractst::populate_assigns_reference ( std::vector< exprt operands,
const symbolt function_symbol,
const irep_idt function_id,
goto_programt created_declarations,
std::vector< exprt > &  created_references 
)
protected

Creates a local variable declaration for each expression in operands, and stores them in created_declarations.

Then creates assignment statements to capture the memory addresses of each expression in the assigns clause within the associated local variable, populating a vector created_references of these local variables.

◆ 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 965 of file code_contracts.cpp.

◆ replace_calls() [2/2]

bool code_contractst::replace_calls ( const std::set< std::string > &  funs_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 910 of file code_contracts.cpp.

Member Data Documentation

◆ goto_functions

goto_functionst& code_contractst::goto_functions
protected

Definition at line 97 of file code_contracts.h.

◆ log

messaget& code_contractst::log
protected

Definition at line 100 of file code_contracts.h.

◆ ns

namespacet code_contractst::ns

Definition at line 93 of file code_contracts.h.

◆ summarized

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

Definition at line 102 of file code_contracts.h.

◆ symbol_table

symbol_tablet& code_contractst::symbol_table
protected

Definition at line 96 of file code_contracts.h.

◆ temporary_counter

unsigned code_contractst::temporary_counter
protected

Definition at line 99 of file code_contracts.h.


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