dfcc_library.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Dynamic frame condition checking for function contracts
 
Author: Remi Delmas, delmasrd@amazon.com
 
\*******************************************************************/
 
 
#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_LIBRARY_H
#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_LIBRARY_H
 
#include <util/irep.h>
#include <util/message.h>
 
#include <goto-programs/goto_instruction_code.h>
 
#include <map>
#include <set>
 
enum class dfcc_typet
{
  CAR,
  CAR_SET,
  CAR_SET_PTR,
  PTR_PRED_CTX,
  PTR_PRED_CTX_PTR,
  OBJ_SET,
  OBJ_SET_PTR,
  WRITE_SET,
  WRITE_SET_PTR
};
 
enum class dfcc_funt
{
  CAR_CREATE,
  CAR_SET_CREATE,
  CAR_SET_INSERT,
  CAR_SET_REMOVE,
  CAR_SET_CONTAINS,
  OBJ_SET_CREATE_INDEXED_BY_OBJECT_ID,
  OBJ_SET_CREATE_APPEND,
  OBJ_SET_RELEASE,
  PTR_PRED_CTX_INIT,
  PTR_PRED_CTX_RESET,
  OBJ_SET_ADD,
  OBJ_SET_APPEND,
  OBJ_SET_REMOVE,
  OBJ_SET_CONTAINS,
  OBJ_SET_CONTAINS_EXACT,
  WRITE_SET_CREATE,
  WRITE_SET_RELEASE,
  WRITE_SET_INSERT_ASSIGNABLE,
  WRITE_SET_INSERT_OBJECT_WHOLE,
  WRITE_SET_INSERT_OBJECT_FROM,
  WRITE_SET_INSERT_OBJECT_UPTO,
  WRITE_SET_ADD_FREEABLE,
  WRITE_SET_ADD_ALLOCATED,
  WRITE_SET_ADD_DECL,
  WRITE_SET_RECORD_DEAD,
  WRITE_SET_RECORD_DEALLOCATED,
  WRITE_SET_CHECK_ALLOCATED_DEALLOCATED_IS_EMPTY,
  WRITE_SET_CHECK_ASSIGNMENT,
  WRITE_SET_CHECK_ARRAY_SET,
  WRITE_SET_CHECK_ARRAY_COPY,
  WRITE_SET_CHECK_ARRAY_REPLACE,
  WRITE_SET_CHECK_HAVOC_OBJECT,
  WRITE_SET_CHECK_DEALLOCATE,
  WRITE_SET_CHECK_ASSIGNS_CLAUSE_INCLUSION,
  WRITE_SET_CHECK_FREES_CLAUSE_INCLUSION,
  WRITE_SET_DEALLOCATE_FREEABLE,
  WRITE_SET_HAVOC_GET_ASSIGNABLE_TARGET,
  WRITE_SET_HAVOC_OBJECT_WHOLE,
  WRITE_SET_HAVOC_SLICE,
  LINK_PTR_PRED_CTX,
  LINK_ALLOCATED,
  LINK_DEALLOCATED,
  POINTER_EQUALS,
  IS_FRESH,
  POINTER_IN_RANGE_DFCC,
  IS_FREEABLE,
  WAS_FREED,
  REPLACE_ENSURES_WAS_FREED_PRECONDITIONS,
  OBEYS_CONTRACT,
};
 
class goto_modelt;
class goto_functiont;
class goto_programt;
class message_handlert;
class symbolt;
class symbol_exprt;
class typet;
 
class dfcc_libraryt
{
public:
  dfcc_libraryt(goto_modelt &goto_model, message_handlert &lmessage_handler);
 
protected:
  static bool loaded;
 
  static bool inlined;
 
  static bool specialized;
 
  static bool malloc_free_fixed;
 
  goto_modelt &goto_model;
  message_handlert &message_handler;
  messaget log;
 
  std::set<irep_idt> get_missing_funs();
 
  void inline_functions();
 
  void fix_malloc_free_calls();
 
private:
  const std::map<dfcc_typet, irep_idt> dfcc_type_to_name;
 
  const std::map<irep_idt, dfcc_typet> dfcc_name_to_type;
 
  const std::map<dfcc_funt, irep_idt> dfcc_fun_to_name;
 
  // Swapped dfcc_fun_to_name
  const std::map<irep_idt, dfcc_funt> dfcc_name_to_fun;
 
  const std::map<irep_idt, dfcc_funt> dfcc_hook;
 
  const std::map<irep_idt, dfcc_funt> havoc_hook;
 
  const std::set<irep_idt> assignable_builtin_names;
 
public:
  std::map<dfcc_typet, typet> dfcc_type;
 
  std::map<dfcc_funt, symbolt> dfcc_fun_symbol;
 
  void load(std::set<irep_idt> &to_instrument);
 
  std::optional<dfcc_funt> get_dfcc_fun(const irep_idt &id) const;
 
  const irep_idt &get_dfcc_fun_name(dfcc_funt fun) const;
 
  bool is_dfcc_library_symbol(const irep_idt &id) const;
 
  void specialize(const std::size_t contract_assigns_size_hint);
 
  void inhibit_front_end_builtins();
 
  void disable_checks();
 
  bool is_front_end_builtin(const irep_idt &function_id) const;
 
  dfcc_funt get_hook(const irep_idt &function_id) const;
 
  std::optional<dfcc_funt> get_havoc_hook(const irep_idt &function_id) const;
 
  const symbolt &get_instrumented_functions_map_symbol();
 
  void add_instrumented_functions_map_init_instructions(
    const std::set<irep_idt> &instrumented_functions,
    const source_locationt &source_location,
    goto_programt &dest);
 
  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);
 
  const code_function_callt write_set_create_call(
    const exprt &write_set_ptr,
    const exprt &contract_assigns_size,
    const source_locationt &source_location);
 
  const code_function_callt write_set_release_call(
    const exprt &write_set_ptr,
    const source_locationt &source_location);
 
  const code_function_callt write_set_add_allocated_call(
    const exprt &write_set_ptr,
    const exprt &ptr,
    const source_locationt &source_location);
 
  const code_function_callt write_set_add_decl_call(
    const exprt &write_set_ptr,
    const exprt &ptr,
    const source_locationt &source_location);
 
  const code_function_callt write_set_record_dead_call(
    const exprt &write_set_ptr,
    const exprt &ptr,
    const source_locationt &source_location);
 
  const code_function_callt write_set_record_deallocated_call(
    const exprt &write_set_ptr,
    const exprt &ptr,
    const source_locationt &source_location);
 
  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);
 
  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);
 
  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);
 
  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);
 
  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);
 
  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);
 
  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);
 
  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);
 
  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);
 
  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);
 
  const code_function_callt link_ptr_pred_ctx_call(
    const exprt &write_set_ptr,
    const exprt &ptr_pred_ctx_ptr,
    const source_locationt &source_location);
 
  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);
 
  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);
 
  const code_function_callt check_replace_ensures_was_freed_preconditions_call(
    const exprt &ptr,
    const exprt &write_set_ptr,
    const source_locationt &source_location);
 
  const code_function_callt obj_set_create_indexed_by_object_id_call(
    const exprt &obj_set_ptr,
    const source_locationt &source_location);
 
  const code_function_callt obj_set_release_call(
    const exprt &obj_set_ptr,
    const source_locationt &source_location);
 
  const code_function_callt ptr_pred_ctx_init_call(
    const exprt &ptr_pred_ctx_ptr,
    const source_locationt &source_location);
 
  const code_function_callt ptr_pred_ctx_reset_call(
    const exprt &ptr_pred_ctx_ptr,
    const source_locationt &source_location);
};
 
#endif