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):
21  ns(_ns),
22  alphabet_parity(false)
23  {
24  }
25 
26  void slice_by_trace(
27  std::string trace_files,
28  symex_target_equationt &equation);
29 
30  protected:
31  const namespacet &ns;
32  typedef std::set<irep_idt> alphabett;
35  std::string semantics;
36 
37  typedef std::pair<std::set<irep_idt>, bool> event_sett;
38  typedef std::vector<event_sett> event_tracet;
39 
41 
42  typedef std::vector<std::vector<irep_idt> > value_tracet;
43 
45 
46  typedef std::vector<exprt> trace_conditionst;
47 
49 
50  std::set<exprt> sliced_guards;
51 
52  std::vector<exprt> merge_map_back;
53 
54  std::vector<std::pair<bool, std::set<exprt> > > merge_impl_cache_back;
55 
57 
59 
60  void read_trace(std::string filename);
61 
62  bool parse_alphabet(std::string read_line);
63 
64  void parse_events(std::string read_line);
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
symex_slice_by_tracet::t
trace_conditionst t
Definition: slice_by_trace.h:48
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
symex_target_equation.h
symex_slice_by_tracet::compute_ts_back
void compute_ts_back(symex_target_equationt &equation)
Definition: slice_by_trace.cpp:235
symex_slice_by_tracet::alphabet
alphabett alphabet
Definition: slice_by_trace.h:33
symex_slice_by_tracet::parse_alphabet
bool parse_alphabet(std::string read_line)
Definition: slice_by_trace.cpp:166
exprt
Base class for all expressions.
Definition: expr.h:54
symex_slice_by_tracet::sigma_vals
value_tracet sigma_vals
Definition: slice_by_trace.h:44
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:143
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
symex_slice_by_tracet::alphabet_parity
bool alphabet_parity
Definition: slice_by_trace.h:34
symex_slice_by_tracet::merge_symbol
symbol_exprt merge_symbol
Definition: slice_by_trace.h:58
symex_slice_by_tracet::merge_impl_cache_back
std::vector< std::pair< bool, std::set< exprt > > > merge_impl_cache_back
Definition: slice_by_trace.h:54
symex_slice_by_tracet::event_sett
std::pair< std::set< irep_idt >, bool > event_sett
Definition: slice_by_trace.h:37
symex_slice_by_tracet::assign_merges
void assign_merges(symex_target_equationt &equation)
Definition: slice_by_trace.cpp:496
symex_slice_by_tracet::event_tracet
std::vector< event_sett > event_tracet
Definition: slice_by_trace.h:38
symex_slice_by_tracet::ns
const namespacet & ns
Definition: slice_by_trace.h:31
symex_slice_by_tracet::trace_conditionst
std::vector< exprt > trace_conditionst
Definition: slice_by_trace.h:46
symex_slice_by_tracet::value_tracet
std::vector< std::vector< irep_idt > > value_tracet
Definition: slice_by_trace.h:42
symex_slice_by_tracet::implied_guards
std::set< exprt > implied_guards(exprt e)
Definition: slice_by_trace.cpp:525
symex_slice_by_tracet::read_trace
void read_trace(std::string filename)
Definition: slice_by_trace.cpp:120
symex_target_equationt
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
Definition: symex_target_equation.h:35
symex_slice_by_tracet::slice_by_trace
void slice_by_trace(std::string trace_files, symex_target_equationt &equation)
Definition: slice_by_trace.cpp:28
symex_slice_by_tracet::matches
bool matches(event_sett s, irep_idt event)
Definition: slice_by_trace.cpp:488
symex_slice_by_tracet::semantics
std::string semantics
Definition: slice_by_trace.h:35
symex_slice_by_tracet::alphabett
std::set< irep_idt > alphabett
Definition: slice_by_trace.h:32
symex_slice_by_tracet::implies_false
bool implies_false(exprt e)
Definition: slice_by_trace.cpp:610
symex_slice_by_tracet::parse_events
void parse_events(std::string read_line)
Definition: slice_by_trace.cpp:186
symex_slice_by_tracet::sliced_guards
std::set< exprt > sliced_guards
Definition: slice_by_trace.h:50
symex_slice_by_tracet
Definition: slice_by_trace.h:17
symex_slice_by_tracet::symex_slice_by_tracet
symex_slice_by_tracet(const namespacet &_ns)
Definition: slice_by_trace.h:20
symex_slice_by_tracet::merge_identifier
irep_idt merge_identifier
Definition: slice_by_trace.h:56
symex_slice_by_tracet::sigma
event_tracet sigma
Definition: slice_by_trace.h:40
symex_slice_by_tracet::slice_SSA_steps
void slice_SSA_steps(symex_target_equationt &equation, std::set< exprt > implications)
Definition: slice_by_trace.cpp:374
symex_slice_by_tracet::merge_map_back
std::vector< exprt > merge_map_back
Definition: slice_by_trace.h:52