symex_target.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Generate Equation using Symbolic Execution
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
 
#ifndef CPROVER_GOTO_SYMEX_SYMEX_TARGET_H
#define CPROVER_GOTO_SYMEX_SYMEX_TARGET_H
 
#include <goto-programs/goto_program.h>
 
#include "renamed.h"
 
class ssa_exprt;
 
class symex_targett
{
public:
  symex_targett()
  {
  }
 
  virtual ~symex_targett() { }
 
  struct sourcet
  {
    unsigned thread_nr;
    irep_idt function_id;
    // The program counter is an iterator which indicates where the execution
    // is in its program sequence
    goto_programt::const_targett pc;
 
    sourcet(const irep_idt &_function_id, goto_programt::const_targett _pc)
      : thread_nr(0), function_id(_function_id), pc(_pc)
    {
    }
 
    explicit sourcet(
      const irep_idt &_function_id,
      const goto_programt &_goto_program)
      : thread_nr(0),
        function_id(_function_id),
        pc(_goto_program.instructions.begin())
    {
    }
 
    sourcet(sourcet &&other) noexcept
      : thread_nr(other.thread_nr), function_id(other.function_id), pc(other.pc)
    {
    }
 
    sourcet(const sourcet &other) = default;
    sourcet &operator=(const sourcet &other) = default;
    sourcet &operator=(sourcet &&other) = default;
  };
 
  enum class assignment_typet
  {
    STATE,
    HIDDEN,
    VISIBLE_ACTUAL_PARAMETER,
    HIDDEN_ACTUAL_PARAMETER,
    PHI,
    GUARD,
  };
 
  virtual void shared_read(
    const exprt &guard,
    const ssa_exprt &ssa_object,
    unsigned atomic_section_id,
    const sourcet &source) = 0;
 
  virtual void shared_write(
    const exprt &guard,
    const ssa_exprt &ssa_object,
    unsigned atomic_section_id,
    const sourcet &source) = 0;
 
  virtual void assignment(
    const exprt &guard,
    const ssa_exprt &ssa_lhs,
    const exprt &ssa_full_lhs,
    const exprt &original_full_lhs,
    const exprt &ssa_rhs,
    const sourcet &source,
    assignment_typet assignment_type)=0;
 
  virtual void decl(
    const exprt &guard,
    const ssa_exprt &ssa_lhs,
    const exprt &initializer,
    const sourcet &source,
    assignment_typet assignment_type) = 0;
 
  virtual void dead(
    const exprt &guard,
    const ssa_exprt &ssa_lhs,
    const sourcet &source)=0;
 
  virtual void function_call(
    const exprt &guard,
    const irep_idt &function_id,
    const std::vector<renamedt<exprt, L2>> &ssa_function_arguments,
    const sourcet &source,
    bool hidden) = 0;
 
  virtual void function_return(
    const exprt &guard,
    const irep_idt &function_id,
    const sourcet &source,
    bool hidden) = 0;
 
  virtual void location(
    const exprt &guard,
    const sourcet &source)=0;
 
  virtual void output(
    const exprt &guard,
    const sourcet &source,
    const irep_idt &output_id,
    const std::list<renamedt<exprt, L2>> &args) = 0;
 
  virtual void output_fmt(
    const exprt &guard,
    const sourcet &source,
    const irep_idt &output_id,
    const irep_idt &fmt,
    const std::list<exprt> &args)=0;
 
  virtual void input(
    const exprt &guard,
    const sourcet &source,
    const irep_idt &input_id,
    const std::list<exprt> &args)=0;
 
  virtual void assumption(
    const exprt &guard,
    const exprt &cond,
    const sourcet &source)=0;
 
  virtual void assertion(
    const exprt &guard,
    const exprt &cond,
    const std::string &msg,
    const sourcet &source)=0;
 
  virtual void goto_instruction(
    const exprt &guard,
    const renamedt<exprt, L2> &cond,
    const sourcet &source) = 0;
 
  virtual void constraint(
    const exprt &cond,
    const std::string &msg,
    const sourcet &source)=0;
 
  virtual void spawn(
    const exprt &guard,
    const sourcet &source)=0;
 
  virtual void memory_barrier(
    const exprt &guard,
    const sourcet &source)=0;
 
  virtual void atomic_begin(
    const exprt &guard,
    unsigned atomic_section_id,
    const sourcet &source)=0;
 
  virtual void atomic_end(
    const exprt &guard,
    unsigned atomic_section_id,
    const sourcet &source)=0;
};
 
bool operator < (
  const symex_targett::sourcet &a,
  const symex_targett::sourcet &b);
 
#endif // CPROVER_GOTO_SYMEX_SYMEX_TARGET_H