cprover
Loading...
Searching...
No Matches
symex_target_equation.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Generate Equation using Symbolic Execution
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_GOTO_SYMEX_SYMEX_TARGET_EQUATION_H
13#define CPROVER_GOTO_SYMEX_SYMEX_TARGET_EQUATION_H
14
15#include <algorithm>
16#include <iosfwd>
17#include <list>
18
19#include <util/invariant.h>
20#include <util/merge_irep.h>
21#include <util/message.h>
22#include <util/narrow.h>
23
24#include "ssa_step.h"
25#include "symex_target.h"
26
28class namespacet;
29
34{
35public:
36 explicit symex_target_equationt(message_handlert &message_handler)
37 : log(message_handler)
38 {
39 }
40
41 virtual ~symex_target_equationt() = default;
42
44 virtual void shared_read(
45 const exprt &guard,
46 const ssa_exprt &ssa_object,
47 unsigned atomic_section_id,
48 const sourcet &source);
49
51 virtual void shared_write(
52 const exprt &guard,
53 const ssa_exprt &ssa_object,
54 unsigned atomic_section_id,
55 const sourcet &source);
56
58 virtual void assignment(
59 const exprt &guard,
60 const ssa_exprt &ssa_lhs,
61 const exprt &ssa_full_lhs,
62 const exprt &original_full_lhs,
63 const exprt &ssa_rhs,
64 const sourcet &source,
65 assignment_typet assignment_type);
66
68 virtual void decl(
69 const exprt &guard,
70 const ssa_exprt &ssa_lhs,
71 const exprt &initializer,
72 const sourcet &source,
73 assignment_typet assignment_type);
74
76 virtual void dead(
77 const exprt &guard,
78 const ssa_exprt &ssa_lhs,
79 const sourcet &source);
80
82 virtual void function_call(
83 const exprt &guard,
84 const irep_idt &function_id,
85 const std::vector<renamedt<exprt, L2>> &ssa_function_arguments,
86 const sourcet &source,
87 bool hidden);
88
90 virtual void function_return(
91 const exprt &guard,
92 const irep_idt &function_id,
93 const sourcet &source,
94 bool hidden);
95
97 virtual void location(
98 const exprt &guard,
99 const sourcet &source);
100
102 virtual void output(
103 const exprt &guard,
104 const sourcet &source,
105 const irep_idt &output_id,
106 const std::list<renamedt<exprt, L2>> &args);
107
109 virtual void output_fmt(
110 const exprt &guard,
111 const sourcet &source,
112 const irep_idt &output_id,
113 const irep_idt &fmt,
114 const std::list<exprt> &args);
115
117 virtual void input(
118 const exprt &guard,
119 const sourcet &source,
120 const irep_idt &input_id,
121 const std::list<exprt> &args);
122
124 virtual void assumption(
125 const exprt &guard,
126 const exprt &cond,
127 const sourcet &source);
128
130 virtual void assertion(
131 const exprt &guard,
132 const exprt &cond,
133 const std::string &msg,
134 const sourcet &source);
135
137 virtual void goto_instruction(
138 const exprt &guard,
139 const renamedt<exprt, L2> &cond,
140 const sourcet &source);
141
143 virtual void constraint(
144 const exprt &cond,
145 const std::string &msg,
146 const sourcet &source);
147
149 virtual void spawn(
150 const exprt &guard,
151 const sourcet &source);
152
154 virtual void memory_barrier(
155 const exprt &guard,
156 const sourcet &source);
157
159 virtual void atomic_begin(
160 const exprt &guard,
161 unsigned atomic_section_id,
162 const sourcet &source);
163
165 virtual void atomic_end(
166 const exprt &guard,
167 unsigned atomic_section_id,
168 const sourcet &source);
169
174 void convert(decision_proceduret &decision_procedure);
175
183 void convert_without_assertions(decision_proceduret &decision_procedure);
184
188 void convert_assignments(decision_proceduret &decision_procedure);
189
194 void convert_decls(decision_proceduret &decision_procedure);
195
198 void convert_assumptions(decision_proceduret &decision_procedure);
199
205 decision_proceduret &decision_procedure,
206 bool optimized_for_single_assertions = true);
207
210 void convert_constraints(decision_proceduret &decision_procedure);
211
215 void convert_goto_instructions(decision_proceduret &decision_procedure);
216
219 void convert_guards(decision_proceduret &decision_procedure);
220
224 void convert_function_calls(decision_proceduret &decision_procedure);
225
229 void convert_io(decision_proceduret &decision_procedure);
230
232
233 std::size_t count_assertions() const
234 {
235 return narrow_cast<std::size_t>(std::count_if(
236 SSA_steps.begin(), SSA_steps.end(), [](const SSA_stept &step) {
237 return step.is_assert() && !step.ignore && !step.converted;
238 }));
239 }
240
241 std::size_t count_ignored_SSA_steps() const
242 {
243 return narrow_cast<std::size_t>(std::count_if(
244 SSA_steps.begin(), SSA_steps.end(), [](const SSA_stept &step) {
245 return step.ignore;
246 }));
247 }
248
249 typedef std::list<SSA_stept> SSA_stepst;
251
252 SSA_stepst::iterator get_SSA_step(std::size_t s)
253 {
254 SSA_stepst::iterator it=SSA_steps.begin();
255 for(; s!=0; s--)
256 {
257 PRECONDITION(it != SSA_steps.end());
258 it++;
259 }
260 return it;
261 }
262
263 void output(std::ostream &out) const;
264
265 void clear()
266 {
267 SSA_steps.clear();
268 }
269
270 bool has_threads() const
271 {
272 return std::any_of(
273 SSA_steps.begin(), SSA_steps.end(), [](const SSA_stept &step) {
274 return step.source.thread_nr != 0;
275 });
276 }
277
278 void validate(const namespacet &ns, const validation_modet vm) const
279 {
280 for(const SSA_stept &step : SSA_steps)
281 step.validate(ns, vm);
282 }
283
284protected:
286
287 // for enforcing sharing in the expressions stored
289 void merge_ireps(SSA_stept &SSA_step);
290
291 // for unique I/O identifiers
292 std::size_t io_count = 0;
293
294 // for unique function call argument identifiers
295 std::size_t argument_count = 0;
296};
297
298inline bool operator<(
299 const symex_target_equationt::SSA_stepst::const_iterator a,
300 const symex_target_equationt::SSA_stepst::const_iterator b)
301{
302 return &(*a)<&(*b);
303}
304
305#endif // CPROVER_GOTO_SYMEX_SYMEX_TARGET_EQUATION_H
Single SSA step in the equation.
Definition: ssa_step.h:47
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
Wrapper for expressions or types which have been renamed up to a given level.
Definition: renamed.h:33
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
virtual void constraint(const exprt &cond, const std::string &msg, const sourcet &source)
Record a global constraint: there is no guard limiting its scope.
virtual void shared_read(const exprt &guard, const ssa_exprt &ssa_object, unsigned atomic_section_id, const sourcet &source)
Read from a shared variable ssa_object (which is both the left- and the right–hand side of assignment...
virtual void input(const exprt &guard, const sourcet &source, const irep_idt &input_id, const std::list< exprt > &args)
Record an input.
exprt make_expression() const
std::size_t count_assertions() const
SSA_stepst::iterator get_SSA_step(std::size_t s)
void convert_decls(decision_proceduret &decision_procedure)
Converts declarations: these are effectively ignored by the decision procedure.
void convert_assumptions(decision_proceduret &decision_procedure)
Converts assumptions: convert the expression the assumption represents.
std::size_t count_ignored_SSA_steps() const
void convert_without_assertions(decision_proceduret &decision_procedure)
Interface method to initiate the conversion into a decision procedure format.
virtual void assumption(const exprt &guard, const exprt &cond, const sourcet &source)
Record an assumption.
void validate(const namespacet &ns, const validation_modet vm) const
virtual void atomic_begin(const exprt &guard, unsigned atomic_section_id, const sourcet &source)
Record a beginning of an atomic section.
std::list< SSA_stept > SSA_stepst
virtual void spawn(const exprt &guard, const sourcet &source)
Record spawning a new thread.
virtual void shared_write(const exprt &guard, const ssa_exprt &ssa_object, unsigned atomic_section_id, const sourcet &source)
Write to a shared variable ssa_object: we effectively assign a value from this thread to be visible b...
virtual void output_fmt(const exprt &guard, const sourcet &source, const irep_idt &output_id, const irep_idt &fmt, const std::list< exprt > &args)
Record formatted output.
virtual void function_return(const exprt &guard, const irep_idt &function_id, const sourcet &source, bool hidden)
Record return from a function.
virtual void atomic_end(const exprt &guard, unsigned atomic_section_id, const sourcet &source)
Record ending an atomic section.
void convert_assignments(decision_proceduret &decision_procedure)
Converts assignments: set the equality lhs==rhs to True.
virtual void assertion(const exprt &guard, const exprt &cond, const std::string &msg, const sourcet &source)
Record an assertion.
void merge_ireps(SSA_stept &SSA_step)
Merging causes identical ireps to be shared.
void convert_guards(decision_proceduret &decision_procedure)
Converts guards: convert the expression the guard represents.
virtual void goto_instruction(const exprt &guard, const renamedt< exprt, L2 > &cond, const sourcet &source)
Record a goto instruction.
symex_target_equationt(message_handlert &message_handler)
void convert(decision_proceduret &decision_procedure)
Interface method to initiate the conversion into a decision procedure format.
virtual ~symex_target_equationt()=default
virtual void dead(const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source)
Remove a variable from the scope.
virtual void location(const exprt &guard, const sourcet &source)
Record a location.
void convert_io(decision_proceduret &decision_procedure)
Converts I/O: for each argument build an equality between its symbol and the argument itself.
virtual void assignment(const exprt &guard, const ssa_exprt &ssa_lhs, const exprt &ssa_full_lhs, const exprt &original_full_lhs, const exprt &ssa_rhs, const sourcet &source, assignment_typet assignment_type)
Write to a local variable.
void convert_function_calls(decision_proceduret &decision_procedure)
Converts function calls: for each argument build an equality between its symbol and the argument itse...
void convert_constraints(decision_proceduret &decision_procedure)
Converts constraints: set the represented condition to True.
virtual void function_call(const exprt &guard, const irep_idt &function_id, const std::vector< renamedt< exprt, L2 > > &ssa_function_arguments, const sourcet &source, bool hidden)
Record a function call.
virtual void output(const exprt &guard, const sourcet &source, const irep_idt &output_id, const std::list< renamedt< exprt, L2 > > &args)
Record an output.
void convert_goto_instructions(decision_proceduret &decision_procedure)
Converts goto instructions: convert the expression representing the condition of this goto.
virtual void memory_barrier(const exprt &guard, const sourcet &source)
Record creating a memory barrier.
virtual void decl(const exprt &guard, const ssa_exprt &ssa_lhs, const exprt &initializer, const sourcet &source, assignment_typet assignment_type)
Declare a fresh variable.
void convert_assertions(decision_proceduret &decision_procedure, bool optimized_for_single_assertions=true)
Converts assertions: build a disjunction of negated assertions.
The interface of the target container for symbolic execution to record its symbolic steps into.
Definition: symex_target.h:25
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
Identifies source in the context of symbolic execution.
Definition: symex_target.h:37
Generate Equation using Symbolic Execution.
bool operator<(const symex_target_equationt::SSA_stepst::const_iterator a, const symex_target_equationt::SSA_stepst::const_iterator b)
validation_modet