dfcc_cfg_info.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Dynamic frame condition checking for function and loop contracts.
 
Author: Qinheping Hu, qinhh@amazon.com
Author: Remi Delmas delmasrd@amazon.com
 
Date: March 2023
 
\*******************************************************************/
 
 
#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CFG_INFO_H
#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CFG_INFO_H
 
#include <util/namespace.h>
#include <util/std_expr.h>
#include <util/symbol_table.h>
 
#include <goto-programs/goto_model.h>
#include <goto-programs/goto_program.h>
 
#include <goto-instrument/contracts/loop_contract_config.h>
 
#include <map>
#include <set>
#include <unordered_set>
 
class dfcc_libraryt;
class goto_functiont;
class message_handlert;
 
class dfcc_loop_infot
{
public:
  dfcc_loop_infot(
    std::size_t loop_id,
    std::size_t cbmc_loop_id,
    const std::set<exprt> &assigns,
    exprt invariant,
    exprt::operandst decreases,
    const std::unordered_set<irep_idt> &local,
    const std::unordered_set<irep_idt> &tracked,
    std::set<std::size_t> inner_loops,
    std::set<std::size_t> outer_loops,
    symbol_exprt write_set_var,
    symbol_exprt addr_of_write_set_var)
    : loop_id(loop_id),
      cbmc_loop_id(cbmc_loop_id),
      assigns(assigns),
      invariant(invariant),
      decreases(decreases),
      local(local),
      tracked(tracked),
      inner_loops(inner_loops),
      outer_loops(outer_loops),
      write_set_var(write_set_var),
      addr_of_write_set_var(addr_of_write_set_var)
  {
  }
 
  void output(std::ostream &out) const;
 
  std::optional<goto_programt::targett>
  find_head(goto_programt &goto_program) const;
 
  // Finds the last instruction tagged as loop latch and having the same loop
  // identifier as this struct in the given program. The goto program passed as
  // argument to this method must be the program from which that dfcc_loop_infot
  // instance was initially generated. Technically it will not be the exact same
  // program because the whole point of contract instrumentation is to
  // instrument the program into a different program by adding new instructions
  // in the program and turning loops into non-loops. For an explanation of why
  // this would work please read the documentation of find head, and mentally
  // replace `head` by `latch` and `start` by `end` in the explanation.
  std::optional<goto_programt::targett>
  find_latch(goto_programt &goto_program) const;
 
  const std::size_t loop_id;
 
  const std::size_t cbmc_loop_id;
 
  const std::set<exprt> assigns;
 
  const exprt invariant;
 
  const exprt::operandst decreases;
 
  const std::unordered_set<irep_idt> local;
 
  const std::unordered_set<irep_idt> tracked;
 
  const std::set<std::size_t> inner_loops;
 
  const std::set<std::size_t> outer_loops;
 
  const symbol_exprt write_set_var;
 
  const symbol_exprt addr_of_write_set_var;
 
  const bool must_skip() const
  {
    return invariant.is_nil() && decreases.empty();
  }
};
 
class dfcc_cfg_infot
{
public:
  dfcc_cfg_infot(
    goto_modelt &goto_model,
    const irep_idt &function_id,
    goto_functiont &goto_function,
    const exprt &top_level_write_set,
    const loop_contract_configt &loop_contract_config,
    symbol_table_baset &symbol_table,
    message_handlert &message_handler,
    dfcc_libraryt &library);
 
  void output(std::ostream &out) const;
 
  const dfcc_loop_infot &get_loop_info(const std::size_t loop_id) const;
 
  const exprt &get_write_set(goto_programt::const_targett target) const;
 
  const std::unordered_set<irep_idt> &
  get_local_set(goto_programt::const_targett target) const;
 
  const std::unordered_set<irep_idt> &
  get_tracked_set(goto_programt::const_targett target) const;
 
  const exprt &get_outer_write_set(std::size_t loop_id) const;
 
  const std::vector<std::size_t> &get_loops_toposorted() const
  {
    return topsorted_loops;
  }
 
  std::size_t
  get_first_id_not_skipped_or_top_level_id(const std::size_t loop_id) const;
 
  const std::optional<std::size_t>
  get_outer_loop_identifier(const std::size_t loop_id) const;
 
  bool must_track_decl_or_dead(goto_programt::const_targett target) const;
 
  bool must_check_lhs(goto_programt::const_targett target) const;
 
  const exprt &get_top_level_write_set() const
  {
    return top_level_write_set;
  }
 
  const std::unordered_set<irep_idt> &get_top_level_tracked()
  {
    return top_level_tracked;
  }
 
private:
  const irep_idt &function_id;
  goto_functiont &goto_function;
  const exprt &top_level_write_set;
  const namespacet ns;
 
  bool is_valid_loop_or_top_level_id(const std::size_t id) const;
 
  bool is_valid_loop_id(const std::size_t id) const;
 
  bool is_top_level_id(const std::size_t id) const;
 
  size_t top_level_id() const;
 
  std::vector<std::size_t> topsorted_loops;
 
  std::vector<std::size_t> top_level_loops;
 
  std::unordered_set<irep_idt> top_level_local;
 
  std::unordered_set<irep_idt> top_level_tracked;
 
  std::map<std::size_t, dfcc_loop_infot> loop_info_map;
};
 
#endif