cprover
slice_by_trace.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Slicer for matching with trace files
4 
5 Author: Alex Groce (agroce@gmail.com)
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_SYMEX_SLICE_BY_TRACE_H
13 #define CPROVER_GOTO_SYMEX_SLICE_BY_TRACE_H
14 
15 #include "symex_target_equation.h"
16 
18 {
19 public:
20  explicit symex_slice_by_tracet(const namespacet &_ns):ns(_ns)
21  {
22  }
23 
24  void slice_by_trace(
25  std::string trace_files,
26  symex_target_equationt &equation);
27 
28  protected:
29  const namespacet &ns;
30  typedef std::set<irep_idt> alphabett;
31  alphabett alphabet;
33  std::string semantics;
34 
35  typedef std::pair<std::set<irep_idt>, bool> event_sett;
36  typedef std::vector<event_sett> event_tracet;
37 
38  event_tracet sigma;
39 
40  typedef std::vector<std::vector<irep_idt> > value_tracet;
41 
42  value_tracet sigma_vals;
43 
44  typedef std::vector<exprt> trace_conditionst;
45 
46  trace_conditionst t;
47 
48  std::set<exprt> sliced_guards;
49 
50  std::vector<exprt> merge_map_back;
51 
52  std::vector<std::pair<bool, std::set<exprt> > > merge_impl_cache_back;
53 
55 
57 
58  void read_trace(std::string filename);
59 
60  bool parse_alphabet(std::string read_line);
61 
62  void parse_events(std::string read_line);
63 
64  void compute_ts_fd(symex_target_equationt &equation);
65 
67 
68  void slice_SSA_steps(
69  symex_target_equationt &equation,
70  std::set<exprt> implications);
71 
72  bool matches(event_sett s, irep_idt event);
73 
74  void assign_merges(symex_target_equationt &equation);
75 
76  std::set<exprt> implied_guards(exprt e);
77 
78  bool implies_false(exprt e);
79 };
80 
81 #endif // CPROVER_GOTO_SYMEX_SLICE_BY_TRACE_H
std::vector< exprt > merge_map_back
bool implies_false(exprt e)
value_tracet sigma_vals
Generate Equation using Symbolic Execution.
void slice_SSA_steps(symex_target_equationt &equation, std::set< exprt > implications)
symex_slice_by_tracet(const namespacet &_ns)
std::set< exprt > sliced_guards
symbol_exprt merge_symbol
trace_conditionst t
std::vector< std::pair< bool, std::set< exprt > > > merge_impl_cache_back
std::vector< event_sett > event_tracet
TO_BE_DOCUMENTED.
Definition: namespace.h:62
std::set< exprt > implied_guards(exprt e)
std::pair< std::set< irep_idt >, bool > event_sett
std::set< irep_idt > alphabett
void read_trace(std::string filename)
bool matches(event_sett s, irep_idt event)
void assign_merges(symex_target_equationt &equation)
const namespacet & ns
Base class for all expressions.
Definition: expr.h:46
void slice_by_trace(std::string trace_files, symex_target_equationt &equation)
void compute_ts_fd(symex_target_equationt &equation)
Expression to hold a symbol (variable)
Definition: std_expr.h:82
std::vector< std::vector< irep_idt > > value_tracet
void parse_events(std::string read_line)
void compute_ts_back(symex_target_equationt &equation)
bool parse_alphabet(std::string read_line)
std::vector< exprt > trace_conditionst