cprover
slice.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Slicer for symex traces
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "slice.h"
13 
14 #include <util/std_expr.h>
15 
16 #include "symex_slice_class.h"
17 
19 {
20  get_symbols(expr.type());
21 
22  forall_operands(it, expr)
23  get_symbols(*it);
24 
25  if(expr.id()==ID_symbol)
26  depends.insert(to_symbol_expr(expr).get_identifier());
27 }
28 
30 {
31  // TODO
32 }
33 
35  symex_target_equationt &equation,
36  const std::list<exprt> &exprs)
37 {
38  // collect dependencies
39  for(const auto &expr : exprs)
40  get_symbols(expr);
41 
42  slice(equation);
43 }
44 
46 {
47  for(symex_target_equationt::SSA_stepst::reverse_iterator
48  it=equation.SSA_steps.rbegin();
49  it!=equation.SSA_steps.rend();
50  it++)
51  slice(*it);
52 }
53 
55 {
56  get_symbols(SSA_step.guard);
57 
58  switch(SSA_step.type)
59  {
61  get_symbols(SSA_step.cond_expr);
62  break;
63 
65  get_symbols(SSA_step.cond_expr);
66  break;
67 
69  get_symbols(SSA_step.cond_expr);
70  break;
71 
73  // ignore
74  break;
75 
77  slice_assignment(SSA_step);
78  break;
79 
81  slice_decl(SSA_step);
82  break;
83 
86  break;
87 
89  // ignore for now
90  break;
91 
99  // ignore for now
100  break;
101 
104  // ignore for now
105  break;
106 
107  default:
108  UNREACHABLE;
109  }
110 }
111 
114 {
115  PRECONDITION(SSA_step.ssa_lhs.id() == ID_symbol);
116  const irep_idt &id=SSA_step.ssa_lhs.get_identifier();
117 
118  if(depends.find(id)==depends.end())
119  {
120  // we don't really need it
121  SSA_step.ignore=true;
122  }
123  else
124  get_symbols(SSA_step.ssa_rhs);
125 }
126 
129 {
130  const irep_idt &id = to_symbol_expr(SSA_step.ssa_lhs).get_identifier();
131 
132  if(depends.find(id)==depends.end())
133  {
134  // we don't really need it
135  SSA_step.ignore=true;
136  }
137 }
138 
145  const symex_target_equationt &equation,
146  symbol_sett &open_variables)
147 {
148  symbol_sett lhs;
149 
150  for(symex_target_equationt::SSA_stepst::const_iterator
151  it=equation.SSA_steps.begin();
152  it!=equation.SSA_steps.end();
153  it++)
154  {
155  const symex_target_equationt::SSA_stept &SSA_step=*it;
156 
157  get_symbols(SSA_step.guard);
158 
159  switch(SSA_step.type)
160  {
162  get_symbols(SSA_step.cond_expr);
163  break;
164 
166  get_symbols(SSA_step.cond_expr);
167  break;
168 
170  // ignore
171  break;
172 
174  get_symbols(SSA_step.ssa_rhs);
175  lhs.insert(SSA_step.ssa_lhs.get_identifier());
176  break;
177 
182  break;
183 
194  // ignore for now
195  break;
196 
197  default:
198  UNREACHABLE;
199  }
200  }
201 
202  open_variables=depends;
203 
204  // remove the ones that are defined
205  open_variables.erase(lhs.begin(), lhs.end());
206 }
207 
209 {
210  symex_slicet symex_slice;
211  symex_slice.slice(equation);
212 }
213 
220  const symex_target_equationt &equation,
221  symbol_sett &open_variables)
222 {
223  symex_slicet symex_slice;
224  symex_slice.collect_open_variables(equation, open_variables);
225 }
226 
231 void slice(
232  symex_target_equationt &equation,
233  const std::list<exprt> &expressions)
234 {
235  symex_slicet symex_slice;
236  symex_slice.slice(equation, expressions);
237 }
238 
240 {
241  // just find the last assertion
242  symex_target_equationt::SSA_stepst::iterator
243  last_assertion=equation.SSA_steps.end();
244 
245  for(symex_target_equationt::SSA_stepst::iterator
246  it=equation.SSA_steps.begin();
247  it!=equation.SSA_steps.end();
248  it++)
249  if(it->is_assert())
250  last_assertion=it;
251 
252  // slice away anything after it
253 
254  symex_target_equationt::SSA_stepst::iterator s_it=
255  last_assertion;
256 
257  if(s_it!=equation.SSA_steps.end())
258  {
259  for(s_it++;
260  s_it!=equation.SSA_steps.end();
261  s_it++)
262  s_it->ignore=true;
263  }
264 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
symex_target_equationt::SSA_stept::ssa_rhs
exprt ssa_rhs
Definition: symex_target_equation.h:291
symex_slice_class.h
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
goto_trace_stept::typet::LOCATION
@ LOCATION
symex_slicet::slice_assignment
void slice_assignment(symex_target_equationt::SSA_stept &SSA_step)
Definition: slice.cpp:112
symex_target_equationt::SSA_stept::guard
exprt guard
Definition: symex_target_equation.h:285
goto_trace_stept::typet::ASSUME
@ ASSUME
typet
The type of an expression, extends irept.
Definition: type.h:27
symex_slicet
Definition: symex_slice_class.h:18
symex_target_equationt::SSA_stept::type
goto_trace_stept::typet type
Definition: symex_target_equation.h:247
symex_target_equationt::SSA_stept
Single SSA step in the equation.
Definition: symex_target_equation.h:243
exprt
Base class for all expressions.
Definition: expr.h:54
simple_slice
void simple_slice(symex_target_equationt &equation)
Definition: slice.cpp:239
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
goto_trace_stept::typet::OUTPUT
@ OUTPUT
goto_trace_stept::typet::FUNCTION_RETURN
@ FUNCTION_RETURN
goto_trace_stept::typet::DECL
@ DECL
goto_trace_stept::typet::ASSERT
@ ASSERT
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:20
goto_trace_stept::typet::NONE
@ NONE
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:176
symex_slicet::slice
void slice(symex_target_equationt &equation)
Definition: slice.cpp:45
goto_trace_stept::typet::ASSIGNMENT
@ ASSIGNMENT
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
irept::id
const irep_idt & id() const
Definition: irep.h:259
goto_trace_stept::typet::INPUT
@ INPUT
goto_trace_stept::typet::ATOMIC_END
@ ATOMIC_END
goto_trace_stept::typet::SPAWN
@ SPAWN
symex_target_equationt
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
Definition: symex_target_equation.h:35
symex_slicet::collect_open_variables
void collect_open_variables(const symex_target_equationt &equation, symbol_sett &open_variables)
Collect the open variables, i.e., variables that are used in RHS but never written in LHS.
Definition: slice.cpp:144
goto_trace_stept::typet::MEMORY_BARRIER
@ MEMORY_BARRIER
goto_trace_stept::typet::SHARED_WRITE
@ SHARED_WRITE
symex_target_equationt::SSA_stept::ignore
bool ignore
Definition: symex_target_equation.h:316
symbol_sett
std::unordered_set< irep_idt > symbol_sett
Definition: slice.h:32
goto_trace_stept::typet::GOTO
@ GOTO
symex_slicet::depends
symbol_sett depends
Definition: symex_slice_class.h:30
collect_open_variables
void collect_open_variables(const symex_target_equationt &equation, symbol_sett &open_variables)
Collect the open variables, i.e.
Definition: slice.cpp:219
symex_target_equationt::SSA_steps
SSA_stepst SSA_steps
Definition: symex_target_equation.h:369
goto_trace_stept::typet::ATOMIC_BEGIN
@ ATOMIC_BEGIN
symex_target_equationt::SSA_stept::cond_expr
exprt cond_expr
Definition: symex_target_equation.h:295
goto_trace_stept::typet::SHARED_READ
@ SHARED_READ
goto_trace_stept::typet::FUNCTION_CALL
@ FUNCTION_CALL
symex_target_equationt::SSA_stept::ssa_lhs
ssa_exprt ssa_lhs
Definition: symex_target_equation.h:289
symex_slicet::get_symbols
void get_symbols(const exprt &expr)
Definition: slice.cpp:18
slice.h
std_expr.h
symex_slicet::slice_decl
void slice_decl(symex_target_equationt::SSA_stept &SSA_step)
Definition: slice.cpp:127
goto_trace_stept::typet::DEAD
@ DEAD
goto_trace_stept::typet::CONSTRAINT
@ CONSTRAINT
slice
void slice(symex_target_equationt &equation)
Definition: slice.cpp:208