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
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
SSA_assignment_stept::SSA_assignment_stept
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
symex_targett::assignment_typet
assignment_typet
Definition: symex_target.h:70
SSA_stept::validate
void validate(const namespacet &ns, const validation_modet vm) const
Check that the SSA step is well-formed.
Definition: ssa_step.cpp:128
goto_trace_stept::typet::LOCATION
@ LOCATION
SSA_stept::cond_handle
exprt cond_handle
Definition: ssa_step.h:148
SSA_stept::output
void output(std::ostream &out) const
Definition: ssa_step.cpp:13
goto_trace_stept::typet::ASSUME
@ ASSUME
SSA_stept::comment
std::string comment
Definition: ssa_step.h:149
SSA_stept::get_ssa_expr
exprt get_ssa_expr() const
Definition: ssa_step.h:151
SSA_stept::atomic_section_id
unsigned atomic_section_id
Definition: ssa_step.h:169
SSA_stept::converted_function_arguments
std::vector< exprt > converted_function_arguments
Definition: ssa_step.h:166
SSA_stept
Single SSA step in the equation.
Definition: ssa_step.h:45
SSA_stept::is_assert
bool is_assert() const
Definition: ssa_step.h:50
SSA_stept::is_function_return
bool is_function_return() const
Definition: ssa_step.h:95
SSA_stept::assignment_type
symex_targett::assignment_typet assignment_type
Definition: ssa_step.h:144
exprt
Base class for all expressions.
Definition: expr.h:53
SSA_stept::is_location
bool is_location() const
Definition: ssa_step.h:75
SSA_stept::formatted
bool formatted
Definition: ssa_step.h:158
SSA_stept::guard
exprt guard
Definition: ssa_step.h:137
SSA_stept::source
symex_targett::sourcet source
Definition: ssa_step.h:47
SSA_stept::called_function
irep_idt called_function
Definition: ssa_step.h:163
SSA_stept::ssa_function_arguments
std::vector< exprt > ssa_function_arguments
Definition: ssa_step.h:166
SSA_stept::is_memory_barrier
bool is_memory_barrier() const
Definition: ssa_step.h:115
SSA_stept::is_constraint
bool is_constraint() const
Definition: ssa_step.h:70
SSA_stept::is_shared_write
bool is_shared_write() const
Definition: ssa_step.h:105
SSA_stept::is_shared_read
bool is_shared_read() const
Definition: ssa_step.h:100
goto_trace.h
Traces of GOTO Programs.
SSA_stept::io_args
std::list< exprt > io_args
Definition: ssa_step.h:159
SSA_stept::converted
bool converted
Definition: ssa_step.h:175
ssa_exprt
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
goto_trace_stept::typet::OUTPUT
@ OUTPUT
goto_trace_stept::typet::FUNCTION_RETURN
@ FUNCTION_RETURN
SSA_stept::io_id
irep_idt io_id
Definition: ssa_step.h:157
SSA_assignment_stept
Definition: ssa_step.h:204
goto_trace_stept::typet::DECL
@ DECL
goto_trace_stept::typet
typet
Definition: goto_trace.h:75
SSA_stept::ssa_lhs
ssa_exprt ssa_lhs
Definition: ssa_step.h:141
SSA_stept::is_atomic_begin
bool is_atomic_begin() const
Definition: ssa_step.h:120
goto_trace_stept::typet::ASSERT
@ ASSERT
SSA_stept::ssa_full_lhs
exprt ssa_full_lhs
Definition: ssa_step.h:142
SSA_stept::cond_expr
exprt cond_expr
Definition: ssa_step.h:147
SSA_stept::is_atomic_end
bool is_atomic_end() const
Definition: ssa_step.h:125
SSA_stept::is_decl
bool is_decl() const
Definition: ssa_step.h:85
goto_trace_stept::typet::ASSIGNMENT
@ ASSIGNMENT
SSA_stept::is_output
bool is_output() const
Definition: ssa_step.h:80
validation_modet
validation_modet
Definition: validation_mode.h:13
false_exprt
The Boolean constant false.
Definition: std_expr.h:3964
goto_trace_stept::typet::ATOMIC_END
@ ATOMIC_END
SSA_stept::ignore
bool ignore
Definition: ssa_step.h:172
SSA_stept::is_goto
bool is_goto() const
Definition: ssa_step.h:65
SSA_stept::hidden
bool hidden
Definition: ssa_step.h:135
goto_trace_stept::typet::SPAWN
@ SPAWN
goto_trace_stept::typet::MEMORY_BARRIER
@ MEMORY_BARRIER
goto_trace_stept::typet::SHARED_WRITE
@ SHARED_WRITE
goto_trace_stept::typet::GOTO
@ GOTO
SSA_stept::original_full_lhs
exprt original_full_lhs
Definition: ssa_step.h:142
SSA_stept::SSA_stept
SSA_stept(const symex_targett::sourcet &_source, goto_trace_stept::typet _type)
Definition: ssa_step.h:177
SSA_stept::type
goto_trace_stept::typet type
Definition: ssa_step.h:48
SSA_stept::is_assignment
bool is_assignment() const
Definition: ssa_step.h:60
SSA_stept::ssa_rhs
exprt ssa_rhs
Definition: ssa_step.h:143
goto_trace_stept::typet::ATOMIC_BEGIN
@ ATOMIC_BEGIN
SSA_stept::guard_handle
exprt guard_handle
Definition: ssa_step.h:138
SSA_stept::format_string
irep_idt format_string
Definition: ssa_step.h:157
SSA_stept::is_spawn
bool is_spawn() const
Definition: ssa_step.h:110
get_nil_irep
const irept & get_nil_irep()
Definition: irep.cpp:26
goto_trace_stept::typet::SHARED_READ
@ SHARED_READ
symex_targett::sourcet
Identifies source in the context of symbolic execution.
Definition: symex_target.h:38
goto_trace_stept::typet::FUNCTION_CALL
@ FUNCTION_CALL
SSA_stept::get_property_id
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
symex_target.h
Generate Equation using Symbolic Execution.
symex_targett
The interface of the target container for symbolic execution to record its symbolic steps into.
Definition: symex_target.h:26
SSA_stept::is_function_call
bool is_function_call() const
Definition: ssa_step.h:90
goto_trace_stept::typet::CONSTRAINT
@ CONSTRAINT
SSA_stept::is_assume
bool is_assume() const
Definition: ssa_step.h:55
SSA_stept::converted_io_args
std::list< exprt > converted_io_args
Definition: ssa_step.h:160