cprover
path_symex_history.h
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: History for path-based symbolic simulator
4
5
Author: Daniel Kroening, kroening@kroening.com
6
7
\*******************************************************************/
8
11
12
#ifndef CPROVER_PATH_SYMEX_PATH_SYMEX_HISTORY_H
13
#define CPROVER_PATH_SYMEX_PATH_SYMEX_HISTORY_H
14
15
#include <cassert>
16
#include <limits>
17
18
#include <
util/base_exceptions.h
>
19
#include <
util/std_expr.h
>
20
21
#include "
loc_ref.h
"
22
23
class
path_symex_stept
;
24
25
// This is a reference to a path_symex_stept,
26
// and is really cheap to copy. These references are stable,
27
// even though the underlying vector is not.
28
class
path_symex_step_reft
29
{
30
public
:
31
explicit
path_symex_step_reft
(
32
class
path_symex_historyt
&_history):
33
index
(
std
::numeric_limits<
std
::size_t>::max()),
34
history
(&_history)
35
{
36
}
37
38
path_symex_step_reft
():
39
index
(
std
::numeric_limits<
std
::size_t>::max()),
history
(nullptr)
40
{
41
}
42
43
bool
is_nil
()
const
44
{
45
return
index
==std::numeric_limits<std::size_t>::max();
46
}
47
48
path_symex_historyt
&
get_history
()
const
49
{
50
INVARIANT_STRUCTURED
(
51
history
!=
nullptr
,
nullptr_exceptiont
,
"history is null"
);
52
return
*
history
;
53
}
54
55
// pre-decrement
56
path_symex_step_reft
&
operator--
();
57
58
path_symex_stept
&
operator*
()
const
{
return
get
(); }
59
path_symex_stept
*
operator->
()
const
{
return
&
get
(); }
60
61
void
generate_successor
();
62
63
// build a forward-traversable version of the history
64
void
build_history
(std::vector<path_symex_step_reft> &dest)
const
;
65
66
protected
:
67
// we use a vector to store all steps
68
std::size_t
index
;
69
class
path_symex_historyt
*
history
;
70
71
path_symex_stept
&
get
()
const
;
72
};
73
74
class
decision_proceduret
;
75
76
// the actual history node
77
class
path_symex_stept
78
{
79
public
:
80
enum
kindt
81
{
82
NON_BRANCH
,
BRANCH_TAKEN
,
BRANCH_NOT_TAKEN
83
}
branch
;
84
85
bool
is_branch_taken
()
const
86
{
87
return
branch
==
BRANCH_TAKEN
;
88
}
89
90
bool
is_branch_not_taken
()
const
91
{
92
return
branch
==
BRANCH_NOT_TAKEN
;
93
}
94
95
bool
is_branch
()
const
96
{
97
return
branch
==
BRANCH_TAKEN
||
branch
==
BRANCH_NOT_TAKEN
;
98
}
99
100
path_symex_step_reft
predecessor
;
101
102
// the thread that did the step
103
unsigned
thread_nr
;
104
105
// the instruction that was executed
106
loc_reft
pc
;
107
108
exprt
guard
,
ssa_rhs
;
109
exprt
full_lhs
;
110
symbol_exprt
ssa_lhs
;
111
112
bool
hidden
;
113
114
path_symex_stept
():
115
branch
(
NON_BRANCH
),
116
guard
(
nil_exprt
()),
117
ssa_rhs
(
nil_exprt
()),
118
full_lhs
(
nil_exprt
()),
119
hidden
(false)
120
{
121
}
122
123
// interface to solvers; this converts a single step
124
void
convert
(
decision_proceduret
&dest)
const
;
125
126
void
output
(std::ostream &)
const
;
127
};
128
129
// converts the full history
130
inline
decision_proceduret
&
operator<<
(
131
decision_proceduret
&dest,
132
path_symex_step_reft
src)
133
{
134
while
(!src.
is_nil
())
135
{
136
src->
convert
(dest);
137
--src;
138
}
139
140
return
dest;
141
}
142
143
// this stores the forest of histories
144
class
path_symex_historyt
145
{
146
public
:
147
typedef
std::vector<path_symex_stept>
step_containert
;
148
step_containert
step_container
;
149
150
// TODO: consider typedefing path_symex_historyt
151
void
clear
()
152
{
153
step_container
.clear();
154
}
155
};
156
157
inline
void
path_symex_step_reft::generate_successor
()
158
{
159
INVARIANT_STRUCTURED
(
160
history
!=
nullptr
,
nullptr_exceptiont
,
"history is null"
);
161
path_symex_step_reft
old=*
this
;
162
index
=
history
->
step_container
.size();
163
history
->
step_container
.push_back(
path_symex_stept
());
164
history
->
step_container
.back().predecessor=old;
165
}
166
167
inline
path_symex_step_reft
&
path_symex_step_reft::operator--
()
168
{
169
*
this
=
get
().predecessor;
170
return
*
this
;
171
}
172
173
inline
path_symex_stept
&
path_symex_step_reft::get
()
const
174
{
175
INVARIANT_STRUCTURED
(
176
history
!=
nullptr
,
nullptr_exceptiont
,
"history is null"
);
177
assert(!
is_nil
());
178
return
history
->
step_container
[
index
];
179
}
180
181
#endif // CPROVER_PATH_SYMEX_PATH_SYMEX_HISTORY_H
path_symex_historyt::clear
void clear()
Definition:
path_symex_history.h:151
INVARIANT_STRUCTURED
#define INVARIANT_STRUCTURED(CONDITION, TYPENAME,...)
Definition:
invariant.h:209
path_symex_stept::BRANCH_TAKEN
Definition:
path_symex_history.h:82
operator<<
decision_proceduret & operator<<(decision_proceduret &dest, path_symex_step_reft src)
Definition:
path_symex_history.h:130
path_symex_step_reft
Definition:
path_symex_history.h:28
path_symex_step_reft::build_history
void build_history(std::vector< path_symex_step_reft > &dest) const
Definition:
path_symex_history.cpp:48
path_symex_step_reft::operator--
path_symex_step_reft & operator--()
Definition:
path_symex_history.h:167
path_symex_step_reft::get
path_symex_stept & get() const
Definition:
path_symex_history.h:173
path_symex_step_reft::index
std::size_t index
Definition:
path_symex_history.h:68
nullptr_exceptiont
Definition:
base_exceptions.h:29
path_symex_stept::ssa_rhs
exprt ssa_rhs
Definition:
path_symex_history.h:108
path_symex_stept::convert
void convert(decision_proceduret &dest) const
Definition:
path_symex_history.cpp:39
std
STL namespace.
path_symex_stept::pc
loc_reft pc
Definition:
path_symex_history.h:106
path_symex_stept::NON_BRANCH
Definition:
path_symex_history.h:82
path_symex_step_reft::get_history
path_symex_historyt & get_history() const
Definition:
path_symex_history.h:48
path_symex_stept::full_lhs
exprt full_lhs
Definition:
path_symex_history.h:109
loc_reft
Definition:
loc_ref.h:17
path_symex_stept::branch
enum path_symex_stept::kindt branch
path_symex_step_reft::path_symex_step_reft
path_symex_step_reft(class path_symex_historyt &_history)
Definition:
path_symex_history.h:31
path_symex_stept::is_branch
bool is_branch() const
Definition:
path_symex_history.h:95
nil_exprt
The NIL expression.
Definition:
std_expr.h:3764
path_symex_stept::path_symex_stept
path_symex_stept()
Definition:
path_symex_history.h:114
path_symex_stept::predecessor
path_symex_step_reft predecessor
Definition:
path_symex_history.h:100
path_symex_step_reft::generate_successor
void generate_successor()
Definition:
path_symex_history.h:157
std_expr.h
API to expression classes.
path_symex_historyt::step_containert
std::vector< path_symex_stept > step_containert
Definition:
path_symex_history.h:147
path_symex_historyt::step_container
step_containert step_container
Definition:
path_symex_history.h:148
path_symex_step_reft::is_nil
bool is_nil() const
Definition:
path_symex_history.h:43
path_symex_step_reft::history
class path_symex_historyt * history
Definition:
path_symex_history.h:69
path_symex_stept::hidden
bool hidden
Definition:
path_symex_history.h:112
path_symex_step_reft::path_symex_step_reft
path_symex_step_reft()
Definition:
path_symex_history.h:38
path_symex_stept
Definition:
path_symex_history.h:77
exprt
Base class for all expressions.
Definition:
expr.h:46
path_symex_step_reft::operator*
path_symex_stept & operator*() const
Definition:
path_symex_history.h:58
path_symex_stept::BRANCH_NOT_TAKEN
Definition:
path_symex_history.h:82
path_symex_stept::is_branch_not_taken
bool is_branch_not_taken() const
Definition:
path_symex_history.h:90
path_symex_step_reft::operator->
path_symex_stept * operator->() const
Definition:
path_symex_history.h:59
path_symex_stept::output
void output(std::ostream &) const
Definition:
path_symex_history.cpp:20
path_symex_stept::thread_nr
unsigned thread_nr
Definition:
path_symex_history.h:103
path_symex_stept::kindt
kindt
Definition:
path_symex_history.h:80
decision_proceduret
Definition:
decision_procedure.h:20
symbol_exprt
Expression to hold a symbol (variable)
Definition:
std_expr.h:82
path_symex_historyt
Definition:
path_symex_history.h:144
path_symex_stept::is_branch_taken
bool is_branch_taken() const
Definition:
path_symex_history.h:85
path_symex_stept::guard
exprt guard
Definition:
path_symex_history.h:108
base_exceptions.h
Generic exception types primarily designed for use with invariants.
path_symex_stept::ssa_lhs
symbol_exprt ssa_lhs
Definition:
path_symex_history.h:110
loc_ref.h
Program Locations.
path-symex
path_symex_history.h
Generated by
1.8.14