cprover
Loading...
Searching...
No Matches
dfcc_instrument.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Dynamic frame condition checking for function contracts
4
5Author: Remi Delmas, delmasrd@amazon.com
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_INSTRUMENT_H
13#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_INSTRUMENT_H
14
15#include <util/arith_tools.h>
16#include <util/c_types.h>
17#include <util/message.h>
18#include <util/namespace.h>
19#include <util/std_expr.h>
20#include <util/std_types.h>
21
23
24#include "dfcc_contract_mode.h"
27
28#include <map>
29#include <set>
30
31class goto_modelt;
33class symbolt;
35class dfcc_libraryt;
38class dfcc_cfg_infot;
39
43{
44public:
51
53 bool is_internal_symbol(const irep_idt &id) const;
54
57 bool do_not_instrument(const irep_idt &id) const;
58
82 const irep_idt &function_id,
83 const dfcc_loop_contract_modet loop_contract_mode,
84 std::set<irep_idt> &function_pointer_contracts);
85
103 const irep_idt &function_id,
104 const dfcc_loop_contract_modet loop_contract_mode,
105 std::set<irep_idt> &function_pointer_contracts);
106
130 const dfcc_loop_contract_modet loop_contract_mode,
131 std::set<irep_idt> &function_pointer_contracts);
132
151 const irep_idt &function_id,
152 goto_programt &goto_program,
153 const exprt &write_set,
154 std::set<irep_idt> &function_pointer_contracts);
155
158 void get_instrumented_functions(std::set<irep_idt> &dest) const;
159
162 std::size_t get_max_assigns_clause_size() const;
163
164protected:
173
176 static std::set<irep_idt> function_cache;
177
181 std::set<irep_idt> internal_symbols;
182
187 std::set<symbol_exprt> get_local_statics(const irep_idt &function_id);
188
203 const irep_idt &function_id,
204 const exprt &write_set,
205 const symbol_exprt &symbol_expr,
207 goto_programt &goto_program);
208
223 const irep_idt &function_id,
224 const exprt &write_set,
225 const symbol_exprt &symbol_expr,
227 goto_programt &goto_program);
228
233 const irep_idt &function_id,
234 goto_functiont &goto_function,
235 const exprt &write_set,
236 const std::set<symbol_exprt> &local_statics,
237 const dfcc_loop_contract_modet loop_contract_mode,
238 std::set<irep_idt> &function_pointer_contracts);
239
253 const irep_idt &function_id,
254 goto_programt &goto_program,
256 const goto_programt::targett &last_instruction, // excluding the last
257 dfcc_cfg_infot &cfg_info,
258 std::set<irep_idt> &function_pointer_contracts);
259
262 void instrument_decl(
263 const irep_idt &function_id,
265 goto_programt &goto_program,
266 dfcc_cfg_infot &cfg_info);
267
270 void instrument_dead(
271 const irep_idt &function_id,
273 goto_programt &goto_program,
274 dfcc_cfg_infot &cfg_info);
275
278 void instrument_lhs(
279 const irep_idt &function_id,
281 const exprt &lhs,
282 goto_programt &goto_program,
283 dfcc_cfg_infot &cfg_info);
284
289 optionalt<exprt> is_dead_object_update(const exprt &lhs, const exprt &rhs);
290
299 const irep_idt &function_id,
301 goto_programt &goto_program,
302 dfcc_cfg_infot &cfg_info);
303
308 const exprt &write_set,
310 goto_programt &goto_program);
311
321 const exprt &write_set,
323 goto_programt &goto_program);
324
329 const irep_idt &function_id,
330 const exprt &write_set,
332 goto_programt &goto_program);
333
339 const irep_idt &function_id,
341 goto_programt &goto_program,
342 dfcc_cfg_infot &cfg_info);
343
348 void instrument_other(
349 const irep_idt &function_id,
351 goto_programt &goto_program,
352 dfcc_cfg_infot &cfg_info);
353
360 const irep_idt &function_id,
361 goto_functiont &goto_function,
362 dfcc_cfg_infot &cfg_info,
363 const dfcc_loop_contract_modet loop_contract_mode,
364 const std::set<symbol_exprt> &local_statics,
365 std::set<irep_idt> &function_pointer_contracts);
366};
367
368#endif
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
A class for an expression that represents a conditional target or a list of targets sharing a common ...
Definition c_expr.h:232
Computes natural loops, enforces normal form conditions, computes the nesting graph,...
Translates assigns and frees clauses of a function contract or loop contract into GOTO programs that ...
This class applies the loop contract transformation to a loop in a goto function.
This class instruments GOTO functions or instruction sequences for frame condition checking and loop ...
dfcc_contract_clauses_codegent & contract_clauses_codegen
dfcc_libraryt & library
void instrument_goto_program(const irep_idt &function_id, goto_programt &goto_program, const exprt &write_set, std::set< irep_idt > &function_pointer_contracts)
Instruments a GOTO program against a given write set variable.
void instrument_call_instruction(const exprt &write_set, goto_programt::targett &target, goto_programt &goto_program)
Adds the write_set as extra argument to a function of function pointer call instruction.
void apply_loop_contracts(const irep_idt &function_id, goto_functiont &goto_function, dfcc_cfg_infot &cfg_info, const dfcc_loop_contract_modet loop_contract_mode, const std::set< symbol_exprt > &local_statics, std::set< irep_idt > &function_pointer_contracts)
Applies loop contracts transformations to the given GOTO function, using the given cfg_info instance ...
void instrument_lhs(const irep_idt &function_id, goto_programt::targett &target, const exprt &lhs, goto_programt &goto_program, dfcc_cfg_infot &cfg_info)
Instruments the LHS of an assignment instruction instruction by adding an inclusion check of lhs in w...
void instrument_other(const irep_idt &function_id, goto_programt::targett &target, goto_programt &goto_program, dfcc_cfg_infot &cfg_info)
Instruments a OTHER statement; instruction.
void instrument_assign(const irep_idt &function_id, goto_programt::targett &target, goto_programt &goto_program, dfcc_cfg_infot &cfg_info)
Instrument the lhs of an ASSIGN lhs := rhs instruction by adding an inclusion check of lhs in write_s...
void instrument_deallocate_call(const irep_idt &function_id, const exprt &write_set, goto_programt::targett &target, goto_programt &goto_program)
Inserts deallocation checks and a write set update before a call to the __CPROVER_deallocate function...
std::set< irep_idt > internal_symbols
Set of internal symbols which implementation is generated and inlined into the model at conversion or...
dfcc_instrument_loopt instrument_loop
void get_instrumented_functions(std::set< irep_idt > &dest) const
Adds the names of instrumented functions to dest.
message_handlert & message_handler
void instrument_goto_function(const irep_idt &function_id, goto_functiont &goto_function, const exprt &write_set, const std::set< symbol_exprt > &local_statics, const dfcc_loop_contract_modet loop_contract_mode, std::set< irep_idt > &function_pointer_contracts)
Instruments the body of a GOTO function against a given write set.
static std::set< irep_idt > function_cache
Keeps track of instrumented functions, so that no function gets instrumented more than once.
void instrument_function_call(const irep_idt &function_id, goto_programt::targett &target, goto_programt &goto_program, dfcc_cfg_infot &cfg_info)
Instruments a CALL lhs := function(params) instruction by adding an inclusion check of lhs in write_s...
void instrument_instructions(const irep_idt &function_id, goto_programt &goto_program, goto_programt::targett first_instruction, const goto_programt::targett &last_instruction, dfcc_cfg_infot &cfg_info, std::set< irep_idt > &function_pointer_contracts)
Instruments the instructions found between first_instruction and last_instruction in the instructions...
void instrument_wrapped_function(const irep_idt &wrapped_function_id, const irep_idt &initial_function_id, const dfcc_loop_contract_modet loop_contract_mode, std::set< irep_idt > &function_pointer_contracts)
Instruments a GOTO function by adding an extra write set parameter and inserting frame condition chec...
dfcc_instrumentt(goto_modelt &goto_model, message_handlert &message_handler, dfcc_libraryt &library, dfcc_spec_functionst &spec_functions, dfcc_contract_clauses_codegent &contract_clauses_codegen)
void instrument_decl(const irep_idt &function_id, goto_programt::targett &target, goto_programt &goto_program, dfcc_cfg_infot &cfg_info)
Instruments a DECL x instruction.
std::size_t get_max_assigns_clause_size() const
void instrument_harness_function(const irep_idt &function_id, const dfcc_loop_contract_modet loop_contract_mode, std::set< irep_idt > &function_pointer_contracts)
Instruments a GOTO function used as a proof harness.
bool do_not_instrument(const irep_idt &id) const
True iff the symbol must not be instrumented because it is an internal symbol or a CPROVER symbol.
void instrument_dead(const irep_idt &function_id, goto_programt::targett &target, goto_programt &goto_program, dfcc_cfg_infot &cfg_info)
Instruments a DEAD x instruction.
void instrument_function(const irep_idt &function_id, const dfcc_loop_contract_modet loop_contract_mode, std::set< irep_idt > &function_pointer_contracts)
Instruments a GOTO function by adding an extra write set parameter and instrumenting its body instruc...
goto_modelt & goto_model
void insert_record_dead_call(const irep_idt &function_id, const exprt &write_set, const symbol_exprt &symbol_expr, goto_programt::targett &target, goto_programt &goto_program)
Generates a guarded call to record the death of a local symbol and inserts it in the goto_program at ...
std::set< symbol_exprt > get_local_statics(const irep_idt &function_id)
Returns the set of names from the symbol table that have the static flag set to true and have a sourc...
optionalt< exprt > is_dead_object_update(const exprt &lhs, const exprt &rhs)
Checks if lhs is the dead_object, and if rhs is an if_exprt(nondet, ptr, dead_object) expression.
bool is_internal_symbol(const irep_idt &id) const
True iff the symbol an internal symbol.
dfcc_spec_functionst & spec_functions
void insert_add_decl_call(const irep_idt &function_id, const exprt &write_set, const symbol_exprt &symbol_expr, goto_programt::targett &target, goto_programt &goto_program)
Generates a guarded call to record a locally allocated symbol and inserts it in the goto_program at t...
void instrument_fptr_call_instruction_dynamic_lookup(const exprt &write_set, goto_programt::targett &target, goto_programt &goto_program)
Before calling a function pointer, performs a dynamic lookup into the map of instrumented function pr...
Class interface to library types and functions defined in cprover_contracts.c.
This class rewrites GOTO functions that use the built-ins:
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
Base class for all expressions.
Definition expr.h:56
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
A generic container class for the GOTO intermediate representation of one function.
instructionst::iterator targett
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Expression to hold a symbol (variable)
Definition std_expr.h:113
Symbol table entry.
Definition symbol.h:28
Enum type representing the contract checking and replacement modes.
This class applies the loop contract transformation to a loop in a goto function.
Enumeration representing the instrumentation mode for loop contracts.
dfcc_loop_contract_modet
Enumeration representing the instrumentation mode for loop contracts.
Concrete Goto Program.
API to expression classes.
Pre-defined types.