goto_symex_state.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Symbolic Execution
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
 
#ifndef CPROVER_GOTO_SYMEX_GOTO_SYMEX_STATE_H
#define CPROVER_GOTO_SYMEX_GOTO_SYMEX_STATE_H
 
#include <functional>
#include <memory>
 
#include <analyses/guard.h>
 
#include <util/invariant.h>
#include <util/nodiscard.h>
#include <util/ssa_expr.h>
#include <util/std_expr.h>
 
#include "call_stack.h"
#include "field_sensitivity.h"
#include "goto_state.h"
#include "renaming_level.h"
#include "symex_target_equation.h"
 
class incremental_dirtyt;
 
class goto_symex_statet final : public goto_statet
{
public:
  goto_symex_statet(
    const symex_targett::sourcet &,
    std::size_t max_field_sensitive_array_size,
    bool should_simplify,
    guard_managert &manager,
    std::function<std::size_t(const irep_idt &)> fresh_l2_name_provider);
  ~goto_symex_statet();
 
  explicit goto_symex_statet(
    const goto_symex_statet &other,
    symex_target_equationt *const target)
    : goto_symex_statet(other) // NOLINT
  {
    symex_target = target;
  }
 
  symex_targett::sourcet source;
 
  symbol_tablet symbol_table;
 
  // Manager is required to be able to resize the thread vector
  guard_managert &guard_manager;
  symex_target_equationt *symex_target;
 
  symex_level1t level1;
 
  template <levelt level = L2>
  NODISCARD renamedt<exprt, level> rename(exprt expr, const namespacet &ns);
 
  template <levelt level>
  NODISCARD renamedt<ssa_exprt, level>
  rename_ssa(ssa_exprt ssa, const namespacet &ns);
 
  template <levelt level = L2>
  void rename(typet &type, const irep_idt &l1_identifier, const namespacet &ns);
 
  NODISCARD exprt l2_rename_rvalues(exprt lvalue, const namespacet &ns);
 
  NODISCARD renamedt<ssa_exprt, L2> assignment(
    ssa_exprt lhs,    // L0/L1
    const exprt &rhs, // L2
    const namespacet &ns,
    bool rhs_is_simplified,
    bool record_value,
    bool allow_pointer_unsoundness = false);
 
  field_sensitivityt field_sensitivity;
 
protected:
  template <levelt>
  void rename_address(exprt &expr, const namespacet &ns);
 
  template <levelt level>
  NODISCARD renamedt<ssa_exprt, level>
  set_indices(ssa_exprt expr, const namespacet &ns);
 
  // this maps L1 names to (L2) types
  typedef std::unordered_map<irep_idt, typet> l1_typest;
  l1_typest l1_types;
 
public:
  // guards
  static irep_idt guard_identifier()
  {
    static irep_idt id = "goto_symex::\\guard";
    return id;
  }
 
  call_stackt &call_stack()
  {
    PRECONDITION(source.thread_nr < threads.size());
    return threads[source.thread_nr].call_stack;
  }
 
  const call_stackt &call_stack() const
  {
    PRECONDITION(source.thread_nr < threads.size());
    return threads[source.thread_nr].call_stack;
  }
 
  ssa_exprt add_object(
    const symbol_exprt &expr,
    std::function<std::size_t(const irep_idt &)> index_generator,
    const namespacet &ns);
 
  ssa_exprt declare(ssa_exprt ssa, const namespacet &ns);
 
  void print_backtrace(std::ostream &) const;
 
  // threads
  typedef std::pair<unsigned, std::list<guardt> > a_s_r_entryt;
  typedef std::list<guardt> a_s_w_entryt;
  std::unordered_map<ssa_exprt, a_s_r_entryt, irep_hash> read_in_atomic_section;
  std::unordered_map<ssa_exprt, a_s_w_entryt, irep_hash>
    written_in_atomic_section;
 
  struct threadt
  {
    goto_programt::const_targett pc;
    irep_idt function_id;
    guardt guard;
    call_stackt call_stack;
    std::map<irep_idt, unsigned> function_frame;
    unsigned atomic_section_id = 0;
    explicit threadt(guard_managert &guard_manager)
      : guard(true_exprt(), guard_manager)
    {
    }
  };
 
  std::vector<threadt> threads;
 
  enum class write_is_shared_resultt
  {
    NOT_SHARED,
    IN_ATOMIC_SECTION,
    SHARED
  };
 
  bool l2_thread_read_encoding(ssa_exprt &expr, const namespacet &ns);
  bool l2_thread_write_encoding(const ssa_exprt &expr, const namespacet &ns);
  write_is_shared_resultt
  write_is_shared(const ssa_exprt &expr, const namespacet &ns) const;
 
  std::stack<bool> record_events;
 
  const incremental_dirtyt *dirty = nullptr;
 
  goto_programt::const_targett saved_target;
 
  bool has_saved_jump_target;
 
  bool has_saved_next_instruction;
 
  bool run_validation_checks;
 
  unsigned total_vccs = 0;
  unsigned remaining_vccs = 0;
 
  void drop_existing_l1_name(const irep_idt &l1_identifier)
  {
    level2.current_names.erase(l1_identifier);
  }
 
  void drop_l1_name(const irep_idt &l1_identifier)
  {
    level2.current_names.erase_if_exists(l1_identifier);
  }
 
  std::function<std::size_t(const irep_idt &)> get_l2_name_provider() const
  {
    return fresh_l2_name_provider;
  }
 
  static bool is_read_only_object(const exprt &lvalue)
  {
    // Note ID_constant can occur due to a partial write to a string constant,
    // (i.e. something like byte_extract int from "hello" offset 2), which
    // simplifies to a plain constant.
    return lvalue.id() == ID_string_constant || lvalue.id() == ID_null_object ||
           lvalue.id() == "zero_string" || lvalue.id() == "is_zero_string" ||
           lvalue.id() == "zero_string_length" || lvalue.id() == ID_constant ||
           lvalue.id() == ID_array;
  }
 
private:
  std::function<std::size_t(const irep_idt &)> fresh_l2_name_provider;
 
  goto_symex_statet(const goto_symex_statet &other) = default;
};
 
#endif // CPROVER_GOTO_SYMEX_GOTO_SYMEX_STATE_H