cprover
path_search.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Path-based Symbolic Execution
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_SYMEX_PATH_SEARCH_H
13 #define CPROVER_SYMEX_PATH_SEARCH_H
14 
15 #include <util/time_stopping.h>
16 #include <util/expanding_vector.h>
17 
19 
21 
22 #include <limits>
23 
25 {
26 public:
27  explicit path_searcht(const namespacet &_ns):
28  safety_checkert(_ns),
29  show_vcc(false),
30  eager_infeasibility(false),
31  depth_limit(std::numeric_limits<unsigned>::max()),
32  context_bound(std::numeric_limits<unsigned>::max()),
33  branch_bound(std::numeric_limits<unsigned>::max()),
34  unwind_limit(std::numeric_limits<unsigned>::max()),
35  time_limit(std::numeric_limits<unsigned>::max()),
37  {
38  }
39 
40  virtual resultt operator()(
41  const goto_functionst &goto_functions);
42 
43  void set_depth_limit(int limit)
44  {
45  depth_limit=limit;
46  }
47 
48  void set_context_bound(int limit)
49  {
50  context_bound=limit;
51  }
52 
53  void set_branch_bound(int limit)
54  {
55  branch_bound=limit;
56  }
57 
58  void set_unwind_limit(int limit)
59  {
60  unwind_limit=limit;
61  }
62 
63  void set_time_limit(int limit)
64  {
65  time_limit=limit;
66  }
67 
68  bool show_vcc;
70 
71  // statistics
73  std::size_t number_of_paths;
74  std::size_t number_of_steps;
77  std::size_t number_of_VCCs;
80  std::size_t number_of_locs;
83 
85 
87  {
92 
93  bool is_success() const { return status==SUCCESS; }
94  bool is_failure() const { return status==FAILURE; }
95  bool is_not_reached() const { return status==NOT_REACHED; }
96  };
97 
101 
102  typedef std::map<irep_idt, property_entryt> property_mapt;
103  property_mapt property_map;
104 
105 protected:
107 
108  // State queue. Iterators are stable.
109  // The states most recently executed are at the head.
110  typedef std::list<statet> queuet;
111  queuet queue;
112 
113  // search heuristic
114  void pick_state();
115 
116  struct loc_datat
117  {
118  bool visited;
119  loc_datat():visited(false) { }
120  };
121 
123 
124  bool execute(queuet::iterator state);
125 
126  void check_assertion(statet &state);
127  bool is_feasible(statet &state);
128  void do_show_vcc(statet &state);
129 
130  bool drop_state(const statet &state);
131 
132  void report_statistics();
133 
135  const goto_functionst &goto_functions);
136 
137  unsigned depth_limit;
138  unsigned context_bound;
139  unsigned branch_bound;
140  unsigned unwind_limit;
141  unsigned time_limit;
142 
143  enum class search_heuristict { DFS, BFS, LOCS } search_heuristic;
144 
146 };
147 
148 #endif // CPROVER_SYMEX_PATH_SEARCH_H
std::size_t number_of_infeasible_paths
Definition: path_search.h:76
property_mapt property_map
Definition: path_search.h:103
unsigned context_bound
Definition: path_search.h:138
std::map< irep_idt, property_entryt > property_mapt
Definition: path_search.h:102
std::size_t number_of_locs
Definition: path_search.h:80
void set_branch_bound(int limit)
Definition: path_search.h:53
path_searcht(const namespacet &_ns)
Definition: path_search.h:27
virtual resultt operator()(const goto_functionst &goto_functions)
Definition: path_search.cpp:23
source_locationt source_location
Definition: path_search.h:91
std::size_t number_of_dropped_states
Definition: path_search.h:72
std::size_t number_of_paths
Definition: path_search.h:73
STL namespace.
void initialize_property_map(const goto_functionst &goto_functions)
unsigned time_limit
Definition: path_search.h:141
void report_statistics()
std::size_t number_of_feasible_paths
Definition: path_search.h:75
bool drop_state(const statet &state)
decide whether to drop a state
void pick_state()
time_periodt sat_time
Definition: path_search.h:82
source_locationt last_source_location
Definition: path_search.h:145
path_symex_statet statet
Definition: path_search.h:106
unsigned depth_limit
Definition: path_search.h:137
void set_dfs()
Definition: path_search.h:98
TO_BE_DOCUMENTED.
Definition: namespace.h:62
std::size_t number_of_steps
Definition: path_search.h:74
Time Stopping.
void set_time_limit(int limit)
Definition: path_search.h:63
void set_depth_limit(int limit)
Definition: path_search.h:43
bool is_feasible(statet &state)
bool eager_infeasibility
Definition: path_search.h:69
unsigned unwind_limit
Definition: path_search.h:140
void set_bfs()
Definition: path_search.h:99
std::list< statet > queuet
Definition: path_search.h:110
void set_unwind_limit(int limit)
Definition: path_search.h:58
std::size_t number_of_VCCs_after_simplification
Definition: path_search.h:78
std::size_t number_of_failed_properties
Definition: path_search.h:79
Safety Checker Interface.
State of path-based symbolic simulator.
void do_show_vcc(statet &state)
void set_context_bound(int limit)
Definition: path_search.h:48
queuet queue
Definition: path_search.h:111
unsigned branch_bound
Definition: path_search.h:139
void set_locs()
Definition: path_search.h:100
absolute_timet start_time
Definition: path_search.h:81
enum path_searcht::search_heuristict search_heuristic
bool execute(queuet::iterator state)
TO_BE_DOCUMENTED.
Definition: goto_trace.h:146
void check_assertion(statet &state)
expanding_vectort< loc_datat > loc_data
Definition: path_search.h:122
std::size_t number_of_VCCs
Definition: path_search.h:77