goto_trace.h

Go to the documentation of this file.

#ifndef CPROVER_GOTO_SYMEX_GOTO_TRACE_H
#define CPROVER_GOTO_SYMEX_GOTO_TRACE_H
 
#include <fstream>
#include <goto-programs/goto_program.h>
#include <goto-symex/equation/symex_target.h>
 
#include <map>
#include <irep2/irep2.h>
#include <util/irep/migrate.h>
#include <util/config/cmdline.h>
#include <vector>
#include <string_view>
 
class goto_trace_stept
{
public:
  unsigned step_nr;
 
  // See SSA_stept.
  std::vector<stack_framet> stack_trace;
 
  bool is_assignment() const
  {
    return type == symex_targett::ASSIGNMENT;
  }
  bool is_assume() const
  {
    return type == symex_targett::ASSUME;
  }
  bool is_assert() const
  {
    return type == symex_targett::ASSERT;
  }
  bool is_output() const
  {
    return type == symex_targett::OUTPUT;
  }
  bool is_skip() const
  {
    return type == symex_targett::SKIP;
  }
  bool is_renumber() const
  {
    return type == symex_targett::RENUMBER;
  }
  bool is_branching() const
  {
    return type == symex_targett::BREANCHING;
  }
 
  symex_targett::step_typet type;
 
  goto_programt::const_targett pc;
 
  // this transition done by given thread number
  unsigned thread_nr;
 
  // for assume, assert, goto
  bool guard;
 
  // for assert
  std::string comment;
 
  // in SSA
  expr2tc lhs, rhs;
 
  // this is a constant
  expr2tc value;
 
  // original expression
  expr2tc original_lhs;
 
  /* For a violated assert: the source-level lvalues its claim reads that no
   * assignment step carries -- a field of an object the program never wrote --
   * each paired with its value in this counterexample. A witness has nothing
   * else to record them from (#7858). */
  std::list<std::pair<expr2tc, expr2tc>> nondet_reads;
 
  // for OUTPUT
  std::string format_string;
  std::list<expr2tc> output_args;
 
  void output(const class namespacet &ns, std::ostream &out) const;
  void dump() const;
 
  goto_trace_stept() : step_nr(0), thread_nr(0), guard(false)
  {
  }
};
 
class goto_tracet
{
public:
  typedef std::list<goto_trace_stept> stepst;
  typedef std::map<std::string, std::string, std::less<std::string>> mid;
  stepst steps;
  std::string mode;
 
  void clear()
  {
    mode.clear();
    steps.clear();
  }
 
  void output(const class namespacet &ns, std::ostream &out) const;
};
 
void show_goto_trace_gui(
  std::ostream &out,
  const namespacet &ns,
  const goto_tracet &goto_trace);

void show_goto_trace(
  std::ostream &out,
  const namespacet &ns,
  const goto_tracet &goto_trace,
  bool reachability_trace = false);
 
bool input_file_check(const locationt &l);
 
void show_simplified_location(std::ostream &out, const locationt &location);

void violation_graphml_goto_trace(
  optionst &options,
  const namespacet &ns,
  const goto_tracet &goto_trace,
  const std::string &output_path_override = "");

void violation_yaml_goto_trace(
  optionst &options,
  const namespacet &ns,
  const goto_tracet &goto_trace,
  const std::string &output_path_override = "");
 
void correctness_graphml_goto_trace(
  optionst &options,
  const namespacet &ns,
  const goto_tracet &goto_trace);
 
void correctness_yaml_goto_trace(
  optionst &options,
  const namespacet &ns,
  const goto_tracet &goto_trace);
 
void generate_goto_trace_in_correctness_graphml_format(
  std::string &witness_output,
  bool is_detailed_mode,
  int &specification,
  const namespacet &ns,
  const goto_tracet &goto_trace);
 
void counterexample_value(
  std::ostream &out,
  const namespacet &ns,
  const expr2tc &identifier,
  const expr2tc &value);
 
void generate_html_report(
  const std::string_view uuid,
  const namespacet &ns,
  const goto_tracet &goto_trace,
  const optionst &options);
 
void generate_json_report(
  const std::string_view uuid,
  const namespacet &ns,
  const goto_tracet &goto_trace);
 
#endif