ssa_step.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Symbolic Execution
 
Author: Romain Brenguier <romain.brenguier@diffblue.com>
 
*******************************************************************/
 
#ifndef CPROVER_GOTO_SYMEX_SSA_STEP_H
#define CPROVER_GOTO_SYMEX_SSA_STEP_H
 
#include <util/ssa_expr.h>
 
#include <goto-programs/goto_trace.h>
 
#include "symex_target.h"
 
class SSA_stept
{
public:
  symex_targett::sourcet source;
  goto_trace_stept::typet type;
 
  bool is_assert() const
  {
    return type == goto_trace_stept::typet::ASSERT;
  }
  bool is_assert() const {…}
 
  bool is_assume() const
  {
    return type == goto_trace_stept::typet::ASSUME;
  }
  bool is_assume() const {…}
 
  bool is_assignment() const
  {
    return type == goto_trace_stept::typet::ASSIGNMENT;
  }
  bool is_assignment() const {…}
 
  bool is_goto() const
  {
    return type == goto_trace_stept::typet::GOTO;
  }
  bool is_goto() const {…}
 
  bool is_constraint() const
  {
    return type == goto_trace_stept::typet::CONSTRAINT;
  }
  bool is_constraint() const {…}
 
  bool is_location() const
  {
    return type == goto_trace_stept::typet::LOCATION;
  }
  bool is_location() const {…}
 
  bool is_output() const
  {
    return type == goto_trace_stept::typet::OUTPUT;
  }
  bool is_output() const {…}
 
  bool is_decl() const
  {
    return type == goto_trace_stept::typet::DECL;
  }
  bool is_decl() const {…}
 
  bool is_function_call() const
  {
    return type == goto_trace_stept::typet::FUNCTION_CALL;
  }
  bool is_function_call() const {…}
 
  bool is_function_return() const
  {
    return type == goto_trace_stept::typet::FUNCTION_RETURN;
  }
  bool is_function_return() const {…}
 
  bool is_shared_read() const
  {
    return type == goto_trace_stept::typet::SHARED_READ;
  }
  bool is_shared_read() const {…}
 
  bool is_shared_write() const
  {
    return type == goto_trace_stept::typet::SHARED_WRITE;
  }
  bool is_shared_write() const {…}
 
  bool is_spawn() const
  {
    return type == goto_trace_stept::typet::SPAWN;
  }
  bool is_spawn() const {…}
 
  bool is_memory_barrier() const
  {
    return type == goto_trace_stept::typet::MEMORY_BARRIER;
  }
  bool is_memory_barrier() const {…}
 
  bool is_atomic_begin() const
  {
    return type == goto_trace_stept::typet::ATOMIC_BEGIN;
  }
  bool is_atomic_begin() const {…}
 
  bool is_atomic_end() const
  {
    return type == goto_trace_stept::typet::ATOMIC_END;
  }
  bool is_atomic_end() const {…}
 
  // we may choose to hide
  bool hidden = false;
 
  exprt guard;
  exprt guard_handle;
 
  // for ASSIGNMENT and DECL
  ssa_exprt ssa_lhs;
  exprt ssa_full_lhs, original_full_lhs;
  exprt ssa_rhs;
  symex_targett::assignment_typet assignment_type;
 
  // for ASSUME/ASSERT/GOTO/CONSTRAINT
  exprt cond_expr;
  exprt cond_handle;
  std::string comment;
  // for ASSERT (which includes loop unwinding assertions)
  irep_idt property_id;
 
  exprt get_ssa_expr() const
  {
    return ((is_shared_read() || is_shared_write()) ? ssa_lhs : cond_expr);
  }
  exprt get_ssa_expr() const {…}
 
  // for INPUT/OUTPUT
  irep_idt format_string, io_id;
  bool formatted = false;
  std::list<exprt> io_args;
  std::list<exprt> converted_io_args;
 
  // for function calls: the function that is called
  irep_idt called_function;
 
  // for function calls
  std::vector<exprt> ssa_function_arguments, converted_function_arguments;
 
  // for SHARED_READ/SHARED_WRITE and ATOMIC_BEGIN/ATOMIC_END
  unsigned atomic_section_id = 0;
 
  // for slicing
  bool ignore = false;
 
  // for incremental conversion
  bool converted = false;
 
  SSA_stept(
    const symex_targett::sourcet &_source,
    goto_trace_stept::typet _type)
    : source(_source),
      type(_type),
      hidden(false),
      guard(static_cast<const exprt &>(get_nil_irep())),
      guard_handle(false_exprt()),
      ssa_lhs(static_cast<const ssa_exprt &>(get_nil_irep())),
      ssa_full_lhs(static_cast<const exprt &>(get_nil_irep())),
      original_full_lhs(static_cast<const exprt &>(get_nil_irep())),
      ssa_rhs(static_cast<const exprt &>(get_nil_irep())),
      assignment_type(symex_targett::assignment_typet::STATE),
      cond_expr(static_cast<const exprt &>(get_nil_irep())),
      cond_handle(false_exprt()),
      formatted(false),
      atomic_section_id(0),
      ignore(false)
  {
  }
  SSA_stept( {…}
 
  void output(std::ostream &out) const;
 
  void validate(const namespacet &ns, const validation_modet vm) const;
};
class SSA_stept {…};
 
class SSA_assignment_stept : public SSA_stept
{
public:
  SSA_assignment_stept(
    symex_targett::sourcet source,
    exprt guard,
    ssa_exprt ssa_lhs,
    exprt ssa_full_lhs,
    exprt original_full_lhs,
    exprt ssa_rhs,
    symex_targett::assignment_typet assignment_type);
};
class SSA_assignment_stept : public SSA_stept {…};
 
#endif // CPROVER_GOTO_SYMEX_SSA_STEP_H