dfcc_wrapper_program.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_WRAPPER_PROGRAM_H
#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_WRAPPER_PROGRAM_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 "dfcc_contract_mode.h"
 
#include <set>
 
class goto_modelt;
class messaget;
class message_handlert;
class dfcc_instrumentt;
class dfcc_libraryt;
class dfcc_lift_memory_predicatest;
class code_with_contract_typet;
class conditional_target_group_exprt;
 
class dfcc_wrapper_programt
{
public:
  dfcc_wrapper_programt(
    const dfcc_contract_modet contract_mode,
    const symbolt &wrapper_symbol,
    const symbolt &wrapped_symbol,
    const dfcc_contract_functionst &contract_functions,
    const symbolt &caller_write_set_symbol,
    goto_modelt &goto_model,
    message_handlert &message_handler,
    dfcc_libraryt &library,
    dfcc_instrumentt &instrument,
    dfcc_lift_memory_predicatest &memory_predicates);
 
  void add_to_dest(goto_programt &dest, std::set<irep_idt> &dest_fp_contracts);
 
protected:
  const dfcc_contract_modet contract_mode;
  const symbolt &wrapper_symbol;
  const symbolt &wrapped_symbol;
  const dfcc_contract_functionst &contract_functions;
  const symbolt &contract_symbol;
  const code_with_contract_typet &contract_code_type;
  const symbol_exprt caller_write_set;
 
  const source_locationt wrapper_sl;
 
  std::optional<symbol_exprt> return_value_opt;
 
  const symbol_exprt contract_write_set;
 
  const symbol_exprt addr_of_contract_write_set;
 
  const symbol_exprt requires_write_set;
 
  const symbol_exprt addr_of_requires_write_set;
 
  const symbol_exprt ensures_write_set;
 
  const symbol_exprt addr_of_ensures_write_set;
 
  const symbol_exprt ptr_pred_ctx;
 
  const symbol_exprt addr_of_ptr_pred_ctx;
 
  std::set<irep_idt> function_pointer_contracts;
 
  goto_modelt &goto_model;
  message_handlert &message_handler;
  messaget log;
  dfcc_libraryt &library;
  dfcc_instrumentt &instrument;
  dfcc_lift_memory_predicatest &memory_predicates;
  namespacet ns;
  goto_convertt converter;
 
  exprt::operandst contract_lambda_parameters;
 
  // The body of a wrapper function is decomposed in different sections.
  // Each type of contract clause may add instructions to multiple sections.
  // The sections then get added to the target program by \ref add_to_dest
  // in the declaration order below.
 
  goto_programt preamble;
  goto_programt link_ptr_pred_ctx;
  goto_programt preconditions;
  goto_programt history;
  goto_programt write_set_checks;
  goto_programt function_call;
  goto_programt link_allocated_caller;
  goto_programt link_deallocated_contract;
  goto_programt postconditions;
  goto_programt postamble;
 
  void add_to_dest(goto_programt &dest);
 
  void encode_requires_write_set();
 
  void encode_ensures_write_set();
 
  void encode_contract_write_set();
 
  void encode_ptr_pred_ctx();
 
  void encode_requires_clauses();
 
  void encode_ensures_clauses();
 
  void encode_function_call();
 
  void encode_checked_function_call();
 
  void encode_havoced_function_call();
};
class dfcc_wrapper_programt {…};
 
#endif