renaming_level.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Symbolic Execution
 
Author: Romain Brenguier, romain.brenguier@diffblue.com
 
\*******************************************************************/
 
 
#ifndef CPROVER_GOTO_SYMEX_RENAMING_LEVEL_H
#define CPROVER_GOTO_SYMEX_RENAMING_LEVEL_H
 
#include <util/irep.h>
#include <util/sharing_map.h>
 
#include "renamed.h"
 
using symex_renaming_levelt =
  sharing_mapt<irep_idt, std::pair<ssa_exprt, std::size_t>>;
 
renamedt<ssa_exprt, L0>
symex_level0(ssa_exprt ssa_expr, const namespacet &ns, std::size_t thread_nr);
 
struct symex_level1t
{
  void insert(const renamedt<ssa_exprt, L0> &ssa, std::size_t index);
 
  std::optional<std::pair<ssa_exprt, std::size_t>>
  insert_or_replace(const renamedt<ssa_exprt, L0> &ssa, std::size_t index);
 
  bool has(const renamedt<ssa_exprt, L0> &ssa) const;
 
  renamedt<ssa_exprt, L1> operator()(renamedt<ssa_exprt, L0> l0_expr) const;
 
  void restore_from(const symex_level1t &other);
 
private:
  symex_renaming_levelt current_names;
};
 
struct symex_level2t
{
  symex_renaming_levelt current_names;
 
  renamedt<ssa_exprt, L2> operator()(renamedt<ssa_exprt, L1> l1_expr) const;
 
  unsigned latest_index(const irep_idt &identifier) const;
 
  std::size_t increase_generation(
    const irep_idt &l1_identifier,
    const ssa_exprt &lhs,
    std::function<std::size_t(const irep_idt &)> fresh_l2_name_provider);
};
 
exprt get_original_name(exprt expr);
 
typet get_original_name(typet type);
 
bool check_renaming(const exprt &expr);
 
bool check_renaming_l1(const exprt &expr);
 
bool check_renaming(const typet &type);
 
#endif // CPROVER_GOTO_SYMEX_RENAMING_LEVEL_H