cprover
ssa_step.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbolic Execution
4 
5 Author: Romain Brenguier <romain.brenguier@diffblue.com>
6 
7 *******************************************************************/
8 
9 #ifndef CPROVER_GOTO_SYMEX_SSA_STEP_H
10 #define CPROVER_GOTO_SYMEX_SSA_STEP_H
11 
13 
14 #include "symex_target.h"
15 
44 class SSA_stept
45 {
46 public:
49 
50  bool is_assert() const
51  {
53  }
54 
55  bool is_assume() const
56  {
58  }
59 
60  bool is_assignment() const
61  {
63  }
64 
65  bool is_goto() const
66  {
68  }
69 
70  bool is_constraint() const
71  {
73  }
74 
75  bool is_location() const
76  {
78  }
79 
80  bool is_output() const
81  {
83  }
84 
85  bool is_decl() const
86  {
88  }
89 
90  bool is_function_call() const
91  {
93  }
94 
95  bool is_function_return() const
96  {
98  }
99 
100  bool is_shared_read() const
101  {
103  }
104 
105  bool is_shared_write() const
106  {
108  }
109 
110  bool is_spawn() const
111  {
113  }
114 
115  bool is_memory_barrier() const
116  {
118  }
119 
120  bool is_atomic_begin() const
121  {
123  }
124 
125  bool is_atomic_end() const
126  {
128  }
129 
132  irep_idt get_property_id() const;
133 
134  // we may choose to hide
135  bool hidden = false;
136 
139 
140  // for ASSIGNMENT and DECL
145 
146  // for ASSUME/ASSERT/GOTO/CONSTRAINT
149  std::string comment;
150 
152  {
153  return ((is_shared_read() || is_shared_write()) ? ssa_lhs : cond_expr);
154  }
155 
156  // for INPUT/OUTPUT
158  bool formatted = false;
159  std::list<exprt> io_args;
160  std::list<exprt> converted_io_args;
161 
162  // for function calls: the function that is called
164 
165  // for function calls
167 
168  // for SHARED_READ/SHARED_WRITE and ATOMIC_BEGIN/ATOMIC_END
169  unsigned atomic_section_id = 0;
170 
171  // for slicing
172  bool ignore = false;
173 
174  // for incremental conversion
175  bool converted = false;
176 
178  const symex_targett::sourcet &_source,
180  : source(_source),
181  type(_type),
182  hidden(false),
183  guard(static_cast<const exprt &>(get_nil_irep())),
185  ssa_lhs(static_cast<const ssa_exprt &>(get_nil_irep())),
186  ssa_full_lhs(static_cast<const exprt &>(get_nil_irep())),
187  original_full_lhs(static_cast<const exprt &>(get_nil_irep())),
188  ssa_rhs(static_cast<const exprt &>(get_nil_irep())),
189  assignment_type(symex_targett::assignment_typet::STATE),
190  cond_expr(static_cast<const exprt &>(get_nil_irep())),
192  formatted(false),
194  ignore(false)
195  {
196  }
197 
198  void output(std::ostream &out) const;
199 
200  void validate(const namespacet &ns, const validation_modet vm) const;
201 };
202 
204 {
205 public:
208  exprt guard,
212  exprt ssa_rhs,
214 };
215 
216 #endif // CPROVER_GOTO_SYMEX_SSA_STEP_H
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:45
irep_idt io_id
Definition: ssa_step.h:157
bool ignore
Definition: ssa_step.h:172
irep_idt called_function
Definition: ssa_step.h:163
bool is_assume() const
Definition: ssa_step.h:55
exprt guard_handle
Definition: ssa_step.h:138
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:166
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
bool is_location() const
Definition: ssa_step.h:75
exprt cond_expr
Definition: ssa_step.h:147
exprt cond_handle
Definition: ssa_step.h:148
unsigned atomic_section_id
Definition: ssa_step.h:169
irep_idt format_string
Definition: ssa_step.h:157
symex_targett::assignment_typet assignment_type
Definition: ssa_step.h:144
std::list< exprt > converted_io_args
Definition: ssa_step.h:160
bool is_function_return() const
Definition: ssa_step.h:95
bool formatted
Definition: ssa_step.h:158
exprt ssa_full_lhs
Definition: ssa_step.h:142
bool is_atomic_end() const
Definition: ssa_step.h:125
goto_trace_stept::typet type
Definition: ssa_step.h:48
bool hidden
Definition: ssa_step.h:135
bool is_constraint() const
Definition: ssa_step.h:70
exprt guard
Definition: ssa_step.h:137
bool is_shared_write() const
Definition: ssa_step.h:105
exprt ssa_rhs
Definition: ssa_step.h:143
std::string comment
Definition: ssa_step.h:149
bool is_goto() const
Definition: ssa_step.h:65
symex_targett::sourcet source
Definition: ssa_step.h:47
bool is_atomic_begin() const
Definition: ssa_step.h:120
exprt original_full_lhs
Definition: ssa_step.h:142
exprt get_ssa_expr() const
Definition: ssa_step.h:151
bool converted
Definition: ssa_step.h:175
bool is_shared_read() const
Definition: ssa_step.h:100
bool is_decl() const
Definition: ssa_step.h:85
std::list< exprt > io_args
Definition: ssa_step.h:159
bool is_output() const
Definition: ssa_step.h:80
bool is_function_call() const
Definition: ssa_step.h:90
void output(std::ostream &out) const
Definition: ssa_step.cpp:13
SSA_stept(const symex_targett::sourcet &_source, goto_trace_stept::typet _type)
Definition: ssa_step.h:177
bool is_memory_barrier() const
Definition: ssa_step.h:115
bool is_assignment() const
Definition: ssa_step.h:60
std::vector< exprt > converted_function_arguments
Definition: ssa_step.h:166
ssa_exprt ssa_lhs
Definition: ssa_step.h:141
bool is_spawn() const
Definition: ssa_step.h:110
bool is_assert() const
Definition: ssa_step.h:50
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
The Boolean constant false.
Definition: std_expr.h:2726
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
The interface of the target container for symbolic execution to record its symbolic steps into.
Definition: symex_target.h:26
Traces of GOTO Programs.
const irept & get_nil_irep()
Definition: irep.cpp:26
Identifies source in the context of symbolic execution.
Definition: symex_target.h:38
Generate Equation using Symbolic Execution.
validation_modet