symex_target_equation.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_EQUATION_H
#define CPROVER_GOTO_SYMEX_SYMEX_TARGET_EQUATION_H
 
#include <algorithm>
#include <iosfwd>
#include <list>
 
#include <util/invariant.h>
#include <util/merge_irep.h>
#include <util/message.h>
#include <util/narrow.h>
 
#include "ssa_step.h"
#include "symex_target.h"
 
class decision_proceduret;
class namespacet;
 
class symex_target_equationt:public symex_targett
{
public:
  explicit symex_target_equationt(message_handlert &message_handler)
    : log(message_handler)
  {
  }
 
  virtual ~symex_target_equationt() = default;
 
  virtual void shared_read(
    const exprt &guard,
    const ssa_exprt &ssa_object,
    unsigned atomic_section_id,
    const sourcet &source);
 
  virtual void shared_write(
    const exprt &guard,
    const ssa_exprt &ssa_object,
    unsigned atomic_section_id,
    const sourcet &source);
 
  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);
 
  virtual void decl(
    const exprt &guard,
    const ssa_exprt &ssa_lhs,
    const exprt &initializer,
    const sourcet &source,
    assignment_typet assignment_type);
 
  virtual void dead(
    const exprt &guard,
    const ssa_exprt &ssa_lhs,
    const sourcet &source);
 
  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);
 
  virtual void function_return(
    const exprt &guard,
    const irep_idt &function_id,
    const sourcet &source,
    bool hidden);
 
  virtual void location(
    const exprt &guard,
    const sourcet &source);
 
  virtual void output(
    const exprt &guard,
    const sourcet &source,
    const irep_idt &output_id,
    const std::list<renamedt<exprt, L2>> &args);
 
  virtual void output_fmt(
    const exprt &guard,
    const sourcet &source,
    const irep_idt &output_id,
    const irep_idt &fmt,
    const std::list<exprt> &args);
 
  virtual void input(
    const exprt &guard,
    const sourcet &source,
    const irep_idt &input_id,
    const std::list<exprt> &args);
 
  virtual void assumption(
    const exprt &guard,
    const exprt &cond,
    const sourcet &source);
 
  virtual void assertion(
    const exprt &guard,
    const exprt &cond,
    const std::string &msg,
    const sourcet &source);
 
  virtual void goto_instruction(
    const exprt &guard,
    const renamedt<exprt, L2> &cond,
    const sourcet &source);
 
  virtual void constraint(
    const exprt &cond,
    const std::string &msg,
    const sourcet &source);
 
  virtual void spawn(
    const exprt &guard,
    const sourcet &source);
 
  virtual void memory_barrier(
    const exprt &guard,
    const sourcet &source);
 
  virtual void atomic_begin(
    const exprt &guard,
    unsigned atomic_section_id,
    const sourcet &source);
 
  virtual void atomic_end(
    const exprt &guard,
    unsigned atomic_section_id,
    const sourcet &source);
 
  void convert(decision_proceduret &decision_procedure);
 
  void convert_without_assertions(decision_proceduret &decision_procedure);
 
  void convert_assignments(decision_proceduret &decision_procedure);
 
  void convert_decls(decision_proceduret &decision_procedure);
 
  void convert_assumptions(decision_proceduret &decision_procedure);
 
  void convert_assertions(
    decision_proceduret &decision_procedure,
    bool optimized_for_single_assertions = true);
 
  void convert_constraints(decision_proceduret &decision_procedure);
 
  void convert_goto_instructions(decision_proceduret &decision_procedure);
 
  void convert_guards(decision_proceduret &decision_procedure);
 
  void convert_function_calls(decision_proceduret &decision_procedure);
 
  void convert_io(decision_proceduret &decision_procedure);
 
  exprt make_expression() const;
 
  std::size_t count_assertions() const
  {
    return narrow_cast<std::size_t>(std::count_if(
      SSA_steps.begin(), SSA_steps.end(), [](const SSA_stept &step) {
        return step.is_assert() && !step.ignore && !step.converted;
      }));
  }
 
  std::size_t count_ignored_SSA_steps() const
  {
    return narrow_cast<std::size_t>(std::count_if(
      SSA_steps.begin(), SSA_steps.end(), [](const SSA_stept &step) {
        return step.ignore;
      }));
  }
 
  typedef std::list<SSA_stept> SSA_stepst;
  SSA_stepst SSA_steps;
 
  SSA_stepst::iterator get_SSA_step(std::size_t s)
  {
    SSA_stepst::iterator it=SSA_steps.begin();
    for(; s!=0; s--)
    {
      PRECONDITION(it != SSA_steps.end());
      it++;
    }
    return it;
  }
 
  void output(std::ostream &out) const;
 
  void clear()
  {
    SSA_steps.clear();
  }
 
  bool has_threads() const
  {
    return std::any_of(
      SSA_steps.begin(), SSA_steps.end(), [](const SSA_stept &step) {
        return step.source.thread_nr != 0;
      });
  }
 
  void validate(const namespacet &ns, const validation_modet vm) const
  {
    for(const SSA_stept &step : SSA_steps)
      step.validate(ns, vm);
  }
 
protected:
  messaget log;
 
  // for enforcing sharing in the expressions stored
  merge_irept merge_irep;
  void merge_ireps(SSA_stept &SSA_step);
 
  // for unique I/O identifiers
  std::size_t io_count = 0;
 
  // for unique function call argument identifiers
  std::size_t argument_count = 0;
};
 
inline bool operator<(
  const symex_target_equationt::SSA_stepst::const_iterator a,
  const symex_target_equationt::SSA_stepst::const_iterator b)
{
  return &(*a)<&(*b);
}
 
#endif // CPROVER_GOTO_SYMEX_SYMEX_TARGET_EQUATION_H