dfcc_instrument.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_INSTRUMENT_H
#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_INSTRUMENT_H
 
#include <util/arith_tools.h>
#include <util/c_types.h>
#include <util/message.h>
#include <util/namespace.h>
#include <util/std_expr.h>
#include <util/std_types.h>
 
#include <goto-programs/goto_program.h>
 
#include <goto-instrument/contracts/loop_contract_config.h>
 
#include "dfcc_contract_mode.h"
#include "dfcc_instrument_loop.h"
 
#include <map>
#include <set>
 
class goto_modelt;
class message_handlert;
class symbolt;
class conditional_target_group_exprt;
class dfcc_libraryt;
class dfcc_spec_functionst;
class dfcc_contract_clauses_codegent;
class dfcc_cfg_infot;
 
class dfcc_instrumentt
{
public:
  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);
 
  bool is_internal_symbol(const irep_idt &id) const;
 
  bool do_not_instrument(const irep_idt &id) const;
 
  void instrument_harness_function(
    const irep_idt &function_id,
    const loop_contract_configt &loop_contract_config,
    std::set<irep_idt> &function_pointer_contracts);
 
  void instrument_function(
    const irep_idt &function_id,
    const loop_contract_configt &loop_contract_config,
    std::set<irep_idt> &function_pointer_contracts);
 
  void instrument_wrapped_function(
    const irep_idt &wrapped_function_id,
    const irep_idt &initial_function_id,
    const loop_contract_configt &loop_contract_config,
    std::set<irep_idt> &function_pointer_contracts);
 
  void instrument_goto_program(
    const irep_idt &function_id,
    goto_programt &goto_program,
    const exprt &write_set,
    std::set<irep_idt> &function_pointer_contracts);
 
  void get_instrumented_functions(std::set<irep_idt> &dest) const;
 
  std::size_t get_max_assigns_clause_size() const;
 
protected:
  goto_modelt &goto_model;
  message_handlert &message_handler;
  messaget log;
  dfcc_libraryt &library;
  dfcc_spec_functionst &spec_functions;
  dfcc_contract_clauses_codegent &contract_clauses_codegen;
  dfcc_instrument_loopt instrument_loop;
  namespacet ns;
 
  static std::set<irep_idt> function_cache;
 
  std::set<irep_idt> internal_symbols;
 
  std::set<symbol_exprt> get_local_statics(const irep_idt &function_id);
 
  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);
 
  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);
 
  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 loop_contract_configt &loop_contract_config,
    std::set<irep_idt> &function_pointer_contracts);
 
  void instrument_instructions(
    const irep_idt &function_id,
    goto_programt &goto_program,
    goto_programt::targett first_instruction,
    const goto_programt::targett &last_instruction, // excluding the last
    dfcc_cfg_infot &cfg_info,
    std::set<irep_idt> &function_pointer_contracts);
 
  void instrument_decl(
    const irep_idt &function_id,
    goto_programt::targett &target,
    goto_programt &goto_program,
    dfcc_cfg_infot &cfg_info);
 
  void instrument_dead(
    const irep_idt &function_id,
    goto_programt::targett &target,
    goto_programt &goto_program,
    dfcc_cfg_infot &cfg_info);
 
  void instrument_lhs(
    const irep_idt &function_id,
    goto_programt::targett &target,
    const exprt &lhs,
    goto_programt &goto_program,
    dfcc_cfg_infot &cfg_info);
 
  std::optional<exprt>
  is_dead_object_update(const exprt &lhs, const exprt &rhs);
 
  void instrument_assign(
    const irep_idt &function_id,
    goto_programt::targett &target,
    goto_programt &goto_program,
    dfcc_cfg_infot &cfg_info);
 
  void instrument_call_instruction(
    const exprt &write_set,
    goto_programt::targett &target,
    goto_programt &goto_program);
 
  void instrument_fptr_call_instruction_dynamic_lookup(
    const exprt &write_set,
    goto_programt::targett &target,
    goto_programt &goto_program);
 
  void instrument_deallocate_call(
    const irep_idt &function_id,
    const exprt &write_set,
    goto_programt::targett &target,
    goto_programt &goto_program);
 
  void instrument_function_call(
    const irep_idt &function_id,
    goto_programt::targett &target,
    goto_programt &goto_program,
    dfcc_cfg_infot &cfg_info);
 
  void instrument_other(
    const irep_idt &function_id,
    goto_programt::targett &target,
    goto_programt &goto_program,
    dfcc_cfg_infot &cfg_info);
 
  void apply_loop_contracts(
    const irep_idt &function_id,
    goto_functiont &goto_function,
    dfcc_cfg_infot &cfg_info,
    const loop_contract_configt &loop_contract_config,
    const std::set<symbol_exprt> &local_statics,
    std::set<irep_idt> &function_pointer_contracts);
};
 
#endif