dfcc.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_H
#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_H
 
#include <util/exception_utils.h>
#include <util/irep.h>
#include <util/message.h>
 
#include "dfcc_contract_clauses_codegen.h"
#include "dfcc_contract_handler.h"
#include "dfcc_instrument.h"
#include "dfcc_library.h"
#include "dfcc_lift_memory_predicates.h"
#include "dfcc_spec_functions.h"
#include "dfcc_swap_and_wrap.h"
 
#include <map>
#include <set>
 
class goto_modelt;
class messaget;
class message_handlert;
class symbolt;
class conditional_target_group_exprt;
class optionst;
 
#define FLAG_DFCC "dfcc"
#define OPT_DFCC "(" FLAG_DFCC "):"
 
#define HELP_DFCC                                                              \
  " {y--dfcc} {uharness} \t "                                                  \
  "activate dynamic frame condition checking for contracts using the given "   \
  "harness as entry point\n"
 
#define FLAG_ENFORCE_CONTRACT_REC "enforce-contract-rec"
#define OPT_ENFORCE_CONTRACT_REC "(" FLAG_ENFORCE_CONTRACT_REC "):"
#define HELP_ENFORCE_CONTRACT_REC                                              \
  " {y--enforce-contract-rec} {ufunction}[{y/}{ucontract}] \t "                \
  "wrap {ufunction} with an assertion of the contract and assume recursive "   \
  "calls to "                                                                  \
  "{ufunction} satisfy the contract\n"
 
class invalid_function_contract_pair_exceptiont : public cprover_exception_baset
{
public:
  explicit invalid_function_contract_pair_exceptiont(
    std::string reason,
    std::string correct_format = "");
 
  std::string what() const override;
 
  std::string correct_format;
};
 
void dfcc(
  const optionst &options,
  goto_modelt &goto_model,
  const irep_idt &harness_id,
  const std::optional<irep_idt> &to_check,
  const bool allow_recursive_calls,
  const std::set<irep_idt> &to_replace,
  const loop_contract_configt loop_contract_config,
  const std::set<std::string> &to_exclude_from_nondet_static,
  message_handlert &message_handler);
 
class dfcct
{
public:
  dfcct(
    const optionst &options,
    goto_modelt &goto_model,
    const irep_idt &harness_id,
    const std::optional<std::pair<irep_idt, irep_idt>> &to_check,
    const bool allow_recursive_calls,
    const std::map<irep_idt, irep_idt> &to_replace,
    const loop_contract_configt loop_contract_config,
    message_handlert &message_handler,
    const std::set<std::string> &to_exclude_from_nondet_static);
 
  void transform_goto_model();
 
protected:
  const optionst &options;
  goto_modelt &goto_model;
  const irep_idt &harness_id;
  const std::optional<std::pair<irep_idt, irep_idt>> &to_check;
  const bool allow_recursive_calls;
  const std::map<irep_idt, irep_idt> &to_replace;
  const loop_contract_configt loop_contract_config;
  const std::set<std::string> &to_exclude_from_nondet_static;
  message_handlert &message_handler;
  messaget log;
 
  // Singletons that hold the global state of the program transformation
  // (caches etc.)
  dfcc_libraryt library;
  namespacet ns;
  dfcc_spec_functionst spec_functions;
  dfcc_contract_clauses_codegent contract_clauses_codegen;
  dfcc_instrumentt instrument;
  dfcc_lift_memory_predicatest memory_predicates;
  dfcc_contract_handlert contract_handler;
  dfcc_swap_and_wrapt swap_and_wrap;
 
  std::size_t max_assigns_clause_size;
 
  // partition the set of functions of the goto_model
  std::set<irep_idt> pure_contract_symbols;
  std::set<irep_idt> other_symbols;
  std::set<irep_idt> function_pointer_contracts;
 
  void check_transform_goto_model_preconditions();
 
  void partition_function_symbols(
    std::set<irep_idt> &pure_contract_symbols,
    std::set<irep_idt> &other_symbols);
 
  void link_model_and_load_dfcc_library();
  void instrument_harness_function();
  void lift_memory_predicates();
  void wrap_checked_function();
  void wrap_replaced_functions();
  void wrap_discovered_function_pointer_contracts();
  void instrument_other_functions();
 
  void reinitialize_model();
};
 
#endif