cprover
Loading...
Searching...
No Matches
ssa_step.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Symbolic Execution
4
5Author: Romain Brenguier <romain.brenguier@diffblue.com>
6
7*******************************************************************/
8
9#include "ssa_step.h"
10
11#include <util/format_expr.h>
12
13void SSA_stept::output(std::ostream &out) const
14{
15 out << "Thread " << source.thread_nr;
16
17 if(source.pc->source_location().is_not_nil())
18 out << " " << source.pc->source_location() << '\n';
19 else
20 out << '\n';
21
22 switch(type)
23 {
25 out << "ASSERT " << format(cond_expr) << '\n';
26 break;
28 out << "ASSUME " << format(cond_expr) << '\n';
29 break;
31 out << "LOCATION" << '\n';
32 break;
34 out << "INPUT" << '\n';
35 break;
37 out << "OUTPUT" << '\n';
38 break;
39
41 out << "DECL" << '\n';
42 out << format(ssa_lhs) << '\n';
43 break;
44
46 out << "ASSIGNMENT (";
47 switch(assignment_type)
48 {
50 out << "HIDDEN";
51 break;
53 out << "STATE";
54 break;
56 out << "VISIBLE_ACTUAL_PARAMETER";
57 break;
59 out << "HIDDEN_ACTUAL_PARAMETER";
60 break;
62 out << "PHI";
63 break;
65 out << "GUARD";
66 break;
67 default:
68 {
69 }
70 }
71
72 out << ")\n";
73 break;
74
76 out << "DEAD\n";
77 break;
79 out << "FUNCTION_CALL\n";
80 break;
82 out << "FUNCTION_RETURN\n";
83 break;
85 out << "CONSTRAINT\n";
86 break;
88 out << "SHARED READ\n";
89 break;
91 out << "SHARED WRITE\n";
92 break;
94 out << "ATOMIC_BEGIN\n";
95 break;
97 out << "AUTOMIC_END\n";
98 break;
100 out << "SPAWN\n";
101 break;
103 out << "MEMORY_BARRIER\n";
104 break;
106 out << "IF " << format(cond_expr) << " GOTO\n";
107 break;
108
111 }
112
114 out << format(cond_expr) << '\n';
115
116 if(is_assert() || is_constraint())
117 out << comment << '\n';
118
120 out << format(ssa_lhs) << '\n';
121
122 out << "Guard: " << format(guard) << '\n';
123}
124
128void SSA_stept::validate(const namespacet &ns, const validation_modet vm) const
129{
130 validate_full_expr(guard, ns, vm);
131
132 switch(type)
133 {
139 break;
144 break;
151 vm,
153 "Type inequality in SSA assignment\nlhs-type: " +
155 "\nrhs-type: " + ssa_rhs.type().id_string());
156 break;
159 for(const auto &expr : io_args)
160 validate_full_expr(expr, ns, vm);
161 break;
163 for(const auto &expr : ssa_function_arguments)
164 validate_full_expr(expr, ns, vm);
166 {
167 const symbolt *symbol;
169 vm,
171 "unknown function identifier " + id2string(called_function));
172 }
173 break;
183 break;
184 }
185}
186
188{
190
191 irep_idt property_id;
192
193 if(source.pc->is_assert())
194 {
195 property_id = source.pc->source_location().get_property_id();
196 }
197 else if(source.pc->is_goto())
198 {
199 // this is likely an unwinding assertion
200 property_id = id2string(source.pc->source_location().get_function()) +
201 ".unwind." + std::to_string(source.pc->loop_number);
202 }
203 else if(source.pc->is_function_call())
204 {
205 // this is likely a recursion unwinding assertion
206 property_id =
207 id2string(source.pc->source_location().get_function()) + ".recursion";
208 }
209 else
210 {
212 }
213
214 return property_id;
215}
216
219 exprt _guard,
220 ssa_exprt _ssa_lhs,
221 exprt _ssa_full_lhs,
222 exprt _original_full_lhs,
223 exprt _ssa_rhs,
224 symex_targett::assignment_typet _assignment_type)
225 : SSA_stept(source, goto_trace_stept::typet::ASSIGNMENT)
226{
227 guard = std::move(_guard);
228 ssa_lhs = std::move(_ssa_lhs);
229 ssa_full_lhs = std::move(_ssa_full_lhs);
230 original_full_lhs = std::move(_original_full_lhs);
231 ssa_rhs = std::move(_ssa_rhs);
232 assignment_type = _assignment_type;
237}
SSA_assignment_stept(symex_targett::sourcet source, exprt guard, ssa_exprt ssa_lhs, exprt ssa_full_lhs, exprt original_full_lhs, exprt ssa_rhs, symex_targett::assignment_typet assignment_type)
Definition: ssa_step.cpp:217
Single SSA step in the equation.
Definition: ssa_step.h:47
irep_idt called_function
Definition: ssa_step.h:165
bool is_assume() const
Definition: ssa_step.h:57
void validate(const namespacet &ns, const validation_modet vm) const
Check that the SSA step is well-formed.
Definition: ssa_step.cpp:128
std::vector< exprt > ssa_function_arguments
Definition: ssa_step.h:168
irep_idt get_property_id() const
Returns the property ID if this is a step resulting from an ASSERT, or builds a unique name for an un...
Definition: ssa_step.cpp:187
exprt cond_expr
Definition: ssa_step.h:149
symex_targett::assignment_typet assignment_type
Definition: ssa_step.h:146
exprt ssa_full_lhs
Definition: ssa_step.h:144
goto_trace_stept::typet type
Definition: ssa_step.h:50
bool hidden
Definition: ssa_step.h:137
bool is_constraint() const
Definition: ssa_step.h:72
exprt guard
Definition: ssa_step.h:139
bool is_shared_write() const
Definition: ssa_step.h:107
exprt ssa_rhs
Definition: ssa_step.h:145
std::string comment
Definition: ssa_step.h:151
symex_targett::sourcet source
Definition: ssa_step.h:49
exprt original_full_lhs
Definition: ssa_step.h:144
bool is_shared_read() const
Definition: ssa_step.h:102
std::list< exprt > io_args
Definition: ssa_step.h:161
void output(std::ostream &out) const
Definition: ssa_step.cpp:13
bool is_assignment() const
Definition: ssa_step.h:62
ssa_exprt ssa_lhs
Definition: ssa_step.h:143
bool is_assert() const
Definition: ssa_step.h:52
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
Equality.
Definition: std_expr.h:1225
Base class for all expressions.
Definition: expr.h:54
typet & type()
Return the type of the expression.
Definition: expr.h:82
Step of the trace of a GOTO program.
Definition: goto_trace.h:50
const std::string & id_string() const
Definition: irep.h:399
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
const exprt & get_original_expr() const
Definition: ssa_expr.h:33
Symbol table entry.
Definition: symbol.h:28
The type of an expression, extends irept.
Definition: type.h:29
static format_containert< T > format(const T &o)
Definition: format.h:37
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
Identifies source in the context of symbolic execution.
Definition: symex_target.h:37
goto_programt::const_targett pc
Definition: symex_target.h:42
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
Definition: validate.h:22
void validate_full_expr(const exprt &expr, const namespacet &ns, const validation_modet vm)
Check that the given expression is well-formed (full check, including checks of all subexpressions an...
validation_modet