dfcc_swap_and_wrap.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_SWAP_AND_WRAP_H
#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_SWAP_AND_WRAP_H
 
#include <util/arith_tools.h>
#include <util/c_types.h>
#include <util/message.h>
#include <util/std_expr.h>
#include <util/std_types.h>
 
#include <ansi-c/goto-conversion/goto_convert_functions.h>
 
#include "dfcc_contract_handler.h"
#include "dfcc_instrument.h"
#include "dfcc_library.h"
#include "dfcc_spec_functions.h"
 
#include <map>
#include <set>
 
class goto_modelt;
class messaget;
class message_handlert;
class symbolt;
class conditional_target_group_exprt;
 
class dfcc_swap_and_wrapt
{
public:
  dfcc_swap_and_wrapt(
    goto_modelt &goto_model,
    message_handlert &message_handler,
    dfcc_libraryt &library,
    dfcc_instrumentt &instrument,
    dfcc_spec_functionst &spec_functions,
    dfcc_contract_handlert &contract_handler);
 
  void swap_and_wrap_check(
    const dfcc_loop_contract_modet loop_contract_mode,
    const irep_idt &function_id,
    const irep_idt &contract_id,
    std::set<irep_idt> &function_pointer_contracts,
    bool allow_recursive_calls)
  {
    swap_and_wrap(
      dfcc_contract_modet::CHECK,
      loop_contract_mode,
      function_id,
      contract_id,
      function_pointer_contracts,
      allow_recursive_calls);
  }
 
  void swap_and_wrap_replace(
    const irep_idt &function_id,
    const irep_idt &contract_id,
    std::set<irep_idt> &function_pointer_contracts)
  {
    swap_and_wrap(
      dfcc_contract_modet::REPLACE,
      dfcc_loop_contract_modet::NONE,
      function_id,
      contract_id,
      function_pointer_contracts,
      false);
  }
 
  void get_swapped_functions(std::set<irep_idt> &dest) const;
 
protected:
  goto_modelt &goto_model;
  message_handlert &message_handler;
  messaget log;
  dfcc_libraryt &library;
  dfcc_instrumentt &instrument;
  dfcc_spec_functionst &spec_functions;
  dfcc_contract_handlert &contract_handler;
  namespacet ns;
 
  static std::map<
    irep_idt,
    std::
      pair<irep_idt, std::pair<dfcc_contract_modet, dfcc_loop_contract_modet>>>
    cache;
 
  void swap_and_wrap(
    const dfcc_contract_modet contract_mode,
    const dfcc_loop_contract_modet loop_contract_mode,
    const irep_idt &function_id,
    const irep_idt &contract_id,
    std::set<irep_idt> &function_pointer_contracts,
    bool allow_recursive_calls);
 
  void check_contract(
    const dfcc_loop_contract_modet loop_contract_mode,
    const irep_idt &function_id,
    const irep_idt &contract_id,
    std::set<irep_idt> &function_pointer_contracts,
    bool allow_recursive_calls);
 
  void replace_with_contract(
    const irep_idt &function_id,
    const irep_idt &contract_id,
    std::set<irep_idt> &function_pointer_contracts);
};
#endif