memory_predicates.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Predicates to specify memory footprint in function contracts.
 
Author: Felipe R. Monteiro
 
Date: July 2021
 
\*******************************************************************/

 
#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_MEMORY_PREDICATES_H
#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_MEMORY_PREDICATES_H
 
#include <util/symbol.h>
 
#include <goto-programs/goto_program.h>
 
class goto_functionst;
class goto_modelt;
class message_handlert;
 
class is_fresh_baset
{
public:
  is_fresh_baset(
    goto_modelt &goto_model,
    message_handlert &message_handler,
    const irep_idt &_fun_id)
    : goto_model(goto_model), message_handler(message_handler), fun_id(_fun_id)
  {
  }
 
  void update_requires(goto_programt &requires_);
  void update_ensures(goto_programt &ensures);
 
  virtual void create_declarations() = 0;
 
  void add_memory_map_decl(goto_programt &program);
  void add_memory_map_dead(goto_programt &program);
 
protected:
  void add_declarations(const std::string &decl_string);
  void update_fn_call(
    goto_programt::targett &target,
    const std::string &name,
    bool add_address_of);
 
  virtual void create_requires_fn_call(goto_programt::targett &target) = 0;
  virtual void create_ensures_fn_call(goto_programt::targett &target) = 0;
 
  goto_modelt &goto_model;
  message_handlert &message_handler;
  const irep_idt &fun_id;
 
  // written by the child classes.
  std::string memmap_name;
  std::string requires_fn_name;
  std::string ensures_fn_name;
  symbolt memmap_symbol;
 
  array_typet get_memmap_type();
};
 
class is_fresh_enforcet : public is_fresh_baset
{
public:
  is_fresh_enforcet(
    goto_modelt &goto_model,
    message_handlert &message_handler,
    const irep_idt &_fun_id);
 
  virtual void create_declarations();
 
protected:
  virtual void create_requires_fn_call(goto_programt::targett &target);
  virtual void create_ensures_fn_call(goto_programt::targett &target);
};
 
class is_fresh_replacet : public is_fresh_baset
{
public:
  is_fresh_replacet(
    goto_modelt &goto_model,
    message_handlert &message_handler,
    const irep_idt &_fun_id);
 
  virtual void create_declarations();
 
protected:
  virtual void create_requires_fn_call(goto_programt::targett &target);
  virtual void create_ensures_fn_call(goto_programt::targett &target);
};

class find_is_fresh_calls_visitort
{
public:
  find_is_fresh_calls_visitort()
  {
  }
 
  // \brief return the set of functions invoked by
  // the call graph of this program.
  std::set<goto_programt::targett, goto_programt::target_less_than> &
  is_fresh_calls();
  void clear_set();
  void operator()(goto_programt &prog);
 
protected:
  std::set<goto_programt::targett, goto_programt::target_less_than>
    function_set;
};

class functions_in_scope_visitort
{
public:
  functions_in_scope_visitort(
    const goto_functionst &goto_functions,
    message_handlert &message_handler)
    : goto_functions(goto_functions), message_handler(message_handler)
  {
  }
 
  // \brief return the set of functions invoked by
  // the call graph of this program.
  std::set<irep_idt> &function_calls();
  void operator()(const goto_programt &prog);
 
protected:
  const goto_functionst &goto_functions;
  message_handlert &message_handler;
  std::set<irep_idt> function_set;
};
 
class function_binding_visitort : const_expr_visitort
{
public:
  function_binding_visitort() : const_expr_visitort()
  {
  }
 
  void operator()(const exprt &exp) override
  {
  }
};
 
#endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_MEMORY_PREDICATES_H