CBMC
dfcc_library.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Dynamic frame condition checking for function contracts
4 
5 Author: Remi Delmas, delmasrd@amazon.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_LIBRARY_H
13 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_LIBRARY_H
14 
15 #include <util/irep.h>
16 #include <util/message.h>
17 
19 
20 #include <map>
21 #include <set>
22 
26 enum class dfcc_typet
27 {
29  CAR,
31  CAR_SET,
35  OBJ_SET,
39  WRITE_SET,
42 };
43 
47 enum class dfcc_funt
48 {
50  CAR_CREATE,
130  IS_FRESH,
134  IS_FREEABLE,
136  WAS_FREED,
141 };
142 
143 class goto_modelt;
144 class goto_functiont;
145 class goto_programt;
146 class message_handlert;
147 class symbolt;
148 class symbol_exprt;
149 class typet;
150 
154 {
155 public:
158  message_handlert &lmessage_handler);
159 
160 protected:
162  static bool loaded;
163 
165  static bool inlined;
166 
169  static bool specialized;
170 
172  static bool malloc_free_fixed;
173 
177 
180  std::set<irep_idt> get_missing_funs();
181 
183  void inline_functions();
184 
188  void fix_malloc_free_calls();
189 
190 private:
192  const std::map<dfcc_typet, irep_idt> dfcc_type_to_name;
193 
195  const std::map<irep_idt, dfcc_typet> dfcc_name_to_type;
196 
198  const std::map<dfcc_funt, irep_idt> dfcc_fun_to_name;
199 
200  // Swapped dfcc_fun_to_name
201  const std::map<irep_idt, dfcc_funt> dfcc_name_to_fun;
202 
204  const std::map<irep_idt, dfcc_funt> dfcc_hook;
205 
207  const std::map<irep_idt, dfcc_funt> havoc_hook;
208 
210  const std::set<irep_idt> assignable_builtin_names;
211 
212 public:
214  std::map<dfcc_typet, typet> dfcc_type;
215 
217  std::map<dfcc_funt, symbolt> dfcc_fun_symbol;
218 
222  void load(std::set<irep_idt> &to_instrument);
223 
225  std::optional<dfcc_funt> get_dfcc_fun(const irep_idt &id) const;
226 
228  const irep_idt &get_dfcc_fun_name(dfcc_funt fun) const;
229 
231  bool is_dfcc_library_symbol(const irep_idt &id) const;
232 
236  void specialize(const std::size_t contract_assigns_size_hint);
237 
248 
251  void disable_checks();
252 
256  bool is_front_end_builtin(const irep_idt &function_id) const;
257 
261  dfcc_funt get_hook(const irep_idt &function_id) const;
262 
266  std::optional<dfcc_funt> get_havoc_hook(const irep_idt &function_id) const;
267 
276 
280  const std::set<irep_idt> &instrumented_functions,
281  const source_locationt &source_location,
282  goto_programt &dest);
283 
286  const exprt &write_set_ptr,
287  const exprt &contract_assigns_size,
288  const exprt &contract_frees_size,
289  const exprt &assume_requires_ctx,
290  const exprt &assert_requires_ctx,
291  const exprt &assume_ensures_ctx,
292  const exprt &assert_ensures_ctx,
293  const exprt &allow_allocate,
294  const exprt &allow_deallocate,
295  const source_locationt &source_location);
296 
299  const exprt &write_set_ptr,
300  const exprt &contract_assigns_size,
301  const source_locationt &source_location);
302 
305  const exprt &write_set_ptr,
306  const source_locationt &source_location);
307 
310  const exprt &write_set_ptr,
311  const exprt &ptr,
312  const source_locationt &source_location);
313 
316  const exprt &write_set_ptr,
317  const exprt &ptr,
318  const source_locationt &source_location);
319 
322  const exprt &write_set_ptr,
323  const exprt &ptr,
324  const source_locationt &source_location);
325 
329  const exprt &write_set_ptr,
330  const exprt &ptr,
331  const source_locationt &source_location);
332 
336  const exprt &check_var,
337  const exprt &write_set_ptr,
338  const source_locationt &source_location);
339 
343  const exprt &check_var,
344  const exprt &write_set_ptr,
345  const exprt &ptr,
346  const exprt &size,
347  const source_locationt &source_location);
348 
352  const exprt &check_var,
353  const exprt &write_set_ptr,
354  const exprt &dest,
355  const source_locationt &source_location);
356 
360  const exprt &check_var,
361  const exprt &write_set_ptr,
362  const exprt &dest,
363  const source_locationt &source_location);
364 
368  const exprt &check_var,
369  const exprt &write_set_ptr,
370  const exprt &dest,
371  const exprt &src,
372  const source_locationt &source_location);
373 
377  const exprt &check_var,
378  const exprt &write_set_ptr,
379  const exprt &ptr,
380  const source_locationt &source_location);
381 
385  const exprt &check_var,
386  const exprt &write_set_ptr,
387  const exprt &ptr,
388  const source_locationt &source_location);
389 
393  const exprt &check_var,
394  const exprt &reference_write_set_ptr,
395  const exprt &candidate_write_set_ptr,
396  const source_locationt &source_location);
397 
401  const exprt &check_var,
402  const exprt &reference_write_set_ptr,
403  const exprt &candidate_write_set_ptr,
404  const source_locationt &source_location);
405 
409  const exprt &write_set_ptr,
410  const exprt &target_write_set_ptr,
411  const source_locationt &source_location);
412 
416  const exprt &write_set_ptr,
417  const exprt &is_fresh_obj_set_ptr,
418  const source_locationt &source_location);
419 
423  const exprt &write_set_postconditions_ptr,
424  const exprt &write_set_to_link_ptr,
425  const source_locationt &source_location);
426 
430  const exprt &write_set_postconditions_ptr,
431  const exprt &write_set_to_link_ptr,
432  const source_locationt &source_location);
433 
437  const exprt &ptr,
438  const exprt &write_set_ptr,
439  const source_locationt &source_location);
440 
444  const exprt &obj_set_ptr,
445  const source_locationt &source_location);
446 
450  const exprt &obj_set_ptr,
451  const source_locationt &source_location);
452 };
453 
454 #endif
goto_instruction_codet representation of a function call statement.
Class interface to library types and functions defined in cprover_contracts.c.
Definition: dfcc_library.h:154
const code_function_callt write_set_record_dead_call(const exprt &write_set_ptr, const exprt &ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_record_dead.
const std::map< irep_idt, dfcc_funt > havoc_hook
Maps front-end functions to library functions giving their havoc semantics.
Definition: dfcc_library.h:207
const code_function_callt write_set_check_allocated_deallocated_is_empty_call(const exprt &check_var, const exprt &write_set_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_check_allocated_deallocated_is_empty.
const code_function_callt obj_set_create_indexed_by_object_id_call(const exprt &obj_set_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_obj_set_create_indexed_by_object_id.
static bool inlined
True iff the library functions are inlined.
Definition: dfcc_library.h:165
const std::map< irep_idt, dfcc_funt > dfcc_hook
Maps built-in function names to enums to use for instrumentation.
Definition: dfcc_library.h:204
const code_function_callt write_set_check_assignment_call(const exprt &check_var, const exprt &write_set_ptr, const exprt &ptr, const exprt &size, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_check_assignment.
static bool loaded
True iff the contracts library symbols are loaded.
Definition: dfcc_library.h:162
dfcc_libraryt(goto_modelt &goto_model, message_handlert &lmessage_handler)
Class constructor.
void fix_malloc_free_calls()
Fixes function calls to malloc and free in library functions.
static bool malloc_free_fixed
True iff the library functions uses of malloc and free are fixed.
Definition: dfcc_library.h:172
bool is_front_end_builtin(const irep_idt &function_id) const
Returns true iff the given function_id is one of __CPROVER_assignable, __CPROVER_object_whole,...
const code_function_callt link_allocated_call(const exprt &write_set_postconditions_ptr, const exprt &write_set_to_link_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_link_allocated.
const std::map< irep_idt, dfcc_typet > dfcc_name_to_type
Swapped dfcc_type_to_name.
Definition: dfcc_library.h:195
const code_function_callt write_set_record_deallocated_call(const exprt &write_set_ptr, const exprt &ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_record_deallocated.
const code_function_callt write_set_add_decl_call(const exprt &write_set_ptr, const exprt &ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_add_decl.
void inline_functions()
Inlines library functions that need to be inlined before use.
const code_function_callt write_set_check_array_copy_call(const exprt &check_var, const exprt &write_set_ptr, const exprt &dest, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_check_array_copy.
const code_function_callt write_set_add_allocated_call(const exprt &write_set_ptr, const exprt &ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_add_allocated.
std::optional< dfcc_funt > get_dfcc_fun(const irep_idt &id) const
Returns the dfcc_funt that corresponds to the given id if any.
const std::set< irep_idt > assignable_builtin_names
All built-in function names (front-end and instrumentation hooks)
Definition: dfcc_library.h:210
void add_instrumented_functions_map_init_instructions(const std::set< irep_idt > &instrumented_functions, const source_locationt &source_location, goto_programt &dest)
Generates instructions to initialize the instrumented function map symbol from the given set of instr...
const std::map< dfcc_typet, irep_idt > dfcc_type_to_name
Enum to type name mapping.
Definition: dfcc_library.h:192
const symbolt & get_instrumented_functions_map_symbol()
Returns the "__dfcc_instrumented_functions" symbol or creates it if it does not exist already.
const std::map< dfcc_funt, irep_idt > dfcc_fun_to_name
enum to function name mapping
Definition: dfcc_library.h:198
const std::map< irep_idt, dfcc_funt > dfcc_name_to_fun
Definition: dfcc_library.h:201
messaget log
Definition: dfcc_library.h:176
const code_function_callt write_set_check_array_set_call(const exprt &check_var, const exprt &write_set_ptr, const exprt &dest, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_check_array_set.
const code_function_callt write_set_check_array_replace_call(const exprt &check_var, const exprt &write_set_ptr, const exprt &dest, const exprt &src, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_check_array_replace.
const code_function_callt write_set_release_call(const exprt &write_set_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_release.
void inhibit_front_end_builtins()
Adds an ASSERT(false) body to all front-end functions __CPROVER_object_whole __CPROVER_object_upto __...
const code_function_callt obj_set_release_call(const exprt &obj_set_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_obj_set_release.
const irep_idt & get_dfcc_fun_name(dfcc_funt fun) const
Returns the name of the given dfcc_funt.
dfcc_funt get_hook(const irep_idt &function_id) const
Returns the library instrumentation hook for the given front-end function.
bool is_dfcc_library_symbol(const irep_idt &id) const
True iff the given id is one of the library symbols.
const code_function_callt write_set_check_deallocate_call(const exprt &check_var, const exprt &write_set_ptr, const exprt &ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_check_deallocate.
const code_function_callt link_deallocated_call(const exprt &write_set_postconditions_ptr, const exprt &write_set_to_link_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_link_deallocated.
goto_modelt & goto_model
Definition: dfcc_library.h:174
const code_function_callt write_set_check_assigns_clause_inclusion_call(const exprt &check_var, const exprt &reference_write_set_ptr, const exprt &candidate_write_set_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_check_assigns_clause_inclusion.
const code_function_callt link_is_fresh_call(const exprt &write_set_ptr, const exprt &is_fresh_obj_set_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_link_is_fresh.
message_handlert & message_handler
Definition: dfcc_library.h:175
std::map< dfcc_typet, typet > dfcc_type
Maps enum values to the actual types (dynamically loaded)
Definition: dfcc_library.h:214
std::set< irep_idt > get_missing_funs()
Collects the names of all library functions currently missing from the goto_model into missing.
const code_function_callt write_set_create_call(const exprt &write_set_ptr, const exprt &contract_assigns_size, const exprt &contract_frees_size, const exprt &assume_requires_ctx, const exprt &assert_requires_ctx, const exprt &assume_ensures_ctx, const exprt &assert_ensures_ctx, const exprt &allow_allocate, const exprt &allow_deallocate, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_create.
const code_function_callt write_set_check_frees_clause_inclusion_call(const exprt &check_var, const exprt &reference_write_set_ptr, const exprt &candidate_write_set_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_check_frees_clause_inclusion.
const code_function_callt write_set_check_havoc_object_call(const exprt &check_var, const exprt &write_set_ptr, const exprt &ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_check_havoc_object.
void disable_checks()
Adds "checked" pragmas to instructions of all library functions instructions.
const code_function_callt check_replace_ensures_was_freed_preconditions_call(const exprt &ptr, const exprt &write_set_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_check_replace_ensures_was_freed_preconditions.
const code_function_callt write_set_deallocate_freeable_call(const exprt &write_set_ptr, const exprt &target_write_set_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_deallocate_freeable.
void specialize(const std::size_t contract_assigns_size_hint)
Specializes the library by unwinding loops in library functions to the given assigns clause size.
std::map< dfcc_funt, symbolt > dfcc_fun_symbol
Maps enum values to the actual function symbols (dynamically loaded)
Definition: dfcc_library.h:217
std::optional< dfcc_funt > get_havoc_hook(const irep_idt &function_id) const
Returns the library instrumentation hook for the given built-in.
void load(std::set< irep_idt > &to_instrument)
After calling this function, all library types and functions are present in the the goto_model.
static bool specialized
True iff the library functions are specialized to a particular contract.
Definition: dfcc_library.h:169
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Base class for all expressions.
Definition: expr.h:56
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:24
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:154
Expression to hold a symbol (variable)
Definition: std_expr.h:131
Symbol table entry.
Definition: symbol.h:28
The type of an expression, extends irept.
Definition: type.h:29
dfcc_funt
One enum value per function defined by the cprover_dfcc.c library file.
Definition: dfcc_library.h:48
@ WRITE_SET_INSERT_OBJECT_UPTO
@ CAR_SET_CONTAINS
@ WRITE_SET_CHECK_ASSIGNMENT
@ WRITE_SET_INSERT_ASSIGNABLE
@ WRITE_SET_CHECK_FREES_CLAUSE_INCLUSION
@ POINTER_IN_RANGE_DFCC
@ OBJ_SET_CREATE_APPEND
@ WRITE_SET_RELEASE
@ WRITE_SET_INSERT_OBJECT_WHOLE
@ WRITE_SET_DEALLOCATE_FREEABLE
@ WRITE_SET_CHECK_ARRAY_REPLACE
@ LINK_DEALLOCATED
@ WRITE_SET_CHECK_HAVOC_OBJECT
@ OBJ_SET_CREATE_INDEXED_BY_OBJECT_ID
@ WRITE_SET_CHECK_DEALLOCATE
@ WRITE_SET_CHECK_ALLOCATED_DEALLOCATED_IS_EMPTY
@ WRITE_SET_CHECK_ARRAY_SET
@ WRITE_SET_RECORD_DEAD
@ WRITE_SET_HAVOC_SLICE
@ WRITE_SET_CHECK_ASSIGNS_CLAUSE_INCLUSION
@ WRITE_SET_HAVOC_GET_ASSIGNABLE_TARGET
@ OBJ_SET_CONTAINS
@ WRITE_SET_CREATE
@ WRITE_SET_CHECK_ARRAY_COPY
@ WRITE_SET_ADD_FREEABLE
@ REPLACE_ENSURES_WAS_FREED_PRECONDITIONS
@ WRITE_SET_ADD_DECL
@ WRITE_SET_RECORD_DEALLOCATED
@ OBJ_SET_CONTAINS_EXACT
@ WRITE_SET_ADD_ALLOCATED
@ WRITE_SET_HAVOC_OBJECT_WHOLE
@ WRITE_SET_INSERT_OBJECT_FROM
dfcc_typet
One enum value per type defined by the cprover_dfcc.c library file.
Definition: dfcc_library.h:27
@ WRITE_SET
type of descriptors of assignable/freeable sets of locations
@ CAR_SET_PTR
type of pointers to sets of CAR
@ CAR_SET
type of sets of CAR
@ OBJ_SET_PTR
type of pointers to sets of object identifiers
@ OBJ_SET
type of sets of object identifiers
@ WRITE_SET_PTR
type of pointers to descriptors of assignable/freeable sets of locations
@ CAR
type of descriptors of conditionally assignable ranges of bytes