dfcc_contract_handler.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Dynamic frame condition checking for function contracts
 
Author: Remi Delmas, delmasrd@amazon.com
Date: August 2022
 
\*******************************************************************/
 
 
#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CONTRACT_HANDLER_H
#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CONTRACT_HANDLER_H
 
#include <ansi-c/goto-conversion/goto_convert_class.h>
 
#include <util/message.h>
#include <util/namespace.h>
#include <util/std_expr.h>
 
#include "dfcc_contract_functions.h"
 
#include <set>
 
class goto_modelt;
class message_handlert;
class dfcc_libraryt;
class dfcc_instrumentt;
class dfcc_lift_memory_predicatest;
class dfcc_spec_functionst;
class dfcc_contract_clauses_codegent;
class code_with_contract_typet;
class conditional_target_group_exprt;
 
class dfcc_contract_handlert
{
public:
  dfcc_contract_handlert(
    goto_modelt &goto_model,
    message_handlert &message_handler,
    dfcc_libraryt &library,
    dfcc_instrumentt &instrument,
    dfcc_lift_memory_predicatest &memory_predicates,
    dfcc_spec_functionst &spec_functions,
    dfcc_contract_clauses_codegent &contract_clauses_codegen);
 
  void add_contract_instructions(
    const dfcc_contract_modet contract_mode,
    const irep_idt &wrapper_id,
    const irep_idt &wrapped_id,
    const irep_idt &contract_id,
    const symbolt &wrapper_write_set_symbol,
    goto_programt &dest,
    std::set<irep_idt> &function_pointer_contracts);
 
  const std::size_t get_assigns_clause_size(const irep_idt &contract_id);
 
  const symbolt &get_pure_contract_symbol(
    const irep_idt &contract_id,
    const std::optional<irep_idt> function_id_opt = {});
 
protected:
  goto_modelt &goto_model;
  message_handlert &message_handler;
  messaget log;
  dfcc_libraryt &library;
  dfcc_instrumentt &instrument;
  dfcc_lift_memory_predicatest &memory_predicates;
  dfcc_spec_functionst &spec_functions;
  dfcc_contract_clauses_codegent &contract_clauses_codegen;
  namespacet ns;
 
  // Caches the functions generated from contracts
  static std::map<irep_idt, dfcc_contract_functionst> contract_cache;
 
  const dfcc_contract_functionst &
  get_contract_functions(const irep_idt &contract_id);
 
  void check_signature_compat(
    const irep_idt &contract_id,
    const code_typet &contract_type,
    const irep_idt &pure_contract_id,
    const code_typet &pure_contract_type);
};
 
#endif