cprover
unwind.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Loop unwinding
4 
5 Author: Daniel Kroening, kroening@kroening.com
6  Daniel Poetzl
7 
8 \*******************************************************************/
9 
12 
13 #include "unwind.h"
14 
15 #ifdef DEBUG
16 #include <iostream>
17 #endif
18 
19 #include <util/expr_util.h>
20 #include <util/std_expr.h>
21 #include <util/string_utils.h>
22 
24 
25 #include "loop_utils.h"
26 
28  const goto_programt::const_targett start,
29  const goto_programt::const_targett end, // exclusive
30  goto_programt &goto_program) // result
31 {
32  assert(start->location_number<end->location_number);
33  assert(goto_program.empty());
34 
35  // build map for branch targets inside the loop
36  typedef std::map<goto_programt::const_targett, unsigned> target_mapt;
37  target_mapt target_map;
38 
39  unsigned i=0;
40 
41  for(goto_programt::const_targett t=start; t!=end; t++, i++)
42  target_map[t]=i;
43 
44  // make a copy
45  std::vector<goto_programt::targett> target_vector;
46  target_vector.reserve(target_map.size());
47  assert(target_vector.empty());
48 
49  for(goto_programt::const_targett t=start; t!=end; t++)
50  {
51  goto_programt::targett t_new=goto_program.add_instruction();
52  *t_new=*t;
53  unwind_log.insert(t_new, t->location_number);
54  target_vector.push_back(t_new); // store copied instruction
55  }
56 
57  assert(goto_program.instructions.size()==target_vector.size());
58 
59  // adjust intra-segment gotos
60  for(std::size_t target_index = 0; target_index < target_vector.size();
61  target_index++)
62  {
63  goto_programt::targett t = target_vector[target_index];
64 
65  if(!t->is_goto())
66  continue;
67 
68  goto_programt::const_targett tgt=t->get_target();
69 
70  target_mapt::const_iterator m_it=target_map.find(tgt);
71 
72  if(m_it!=target_map.end())
73  {
74  unsigned j=m_it->second;
75 
76  assert(j<target_vector.size());
77  t->set_target(target_vector[j]);
78  }
79  }
80 }
81 
83  goto_programt &goto_program,
84  const goto_programt::const_targett loop_head,
85  const goto_programt::const_targett loop_exit,
86  const unsigned k,
87  const unwind_strategyt unwind_strategy)
88 {
89  std::vector<goto_programt::targett> iteration_points;
90  unwind(goto_program, loop_head, loop_exit, k, unwind_strategy,
91  iteration_points);
92 }
93 
95  goto_programt &goto_program,
96  const goto_programt::const_targett loop_head,
97  const goto_programt::const_targett loop_exit,
98  const unsigned k,
99  const unwind_strategyt unwind_strategy,
100  std::vector<goto_programt::targett> &iteration_points)
101 {
102  assert(iteration_points.empty());
103  assert(loop_head->location_number<loop_exit->location_number);
104 
105  // rest program after unwound part
106  goto_programt rest_program;
107 
108  if(unwind_strategy==unwind_strategyt::PARTIAL)
109  {
110  goto_programt::targett t=rest_program.add_instruction();
111  unwind_log.insert(t, loop_head->location_number);
112 
113  t->make_skip();
114  t->source_location=loop_head->source_location;
115  t->function=loop_head->function;
116  t->location_number=loop_head->location_number;
117  }
118  else if(unwind_strategy==unwind_strategyt::CONTINUE)
119  {
120  copy_segment(loop_head, loop_exit, rest_program);
121  }
122  else
123  {
124  goto_programt::const_targett t=loop_exit;
125  t--;
126  assert(t->is_backwards_goto());
127 
128  exprt exit_cond = false_exprt(); // default is false
129 
130  if(!t->guard.is_true()) // cond in backedge
131  {
132  exit_cond = boolean_negate(t->guard);
133  }
134  else if(loop_head->is_goto())
135  {
136  if(loop_head->get_target()==loop_exit) // cond in forward edge
137  exit_cond=loop_head->guard;
138  }
139 
140  goto_programt::targett new_t=rest_program.add_instruction();
141 
142  if(unwind_strategy==unwind_strategyt::ASSERT)
143  new_t->make_assertion(exit_cond);
144  else if(unwind_strategy==unwind_strategyt::ASSUME)
145  new_t->make_assumption(exit_cond);
146  else
147  UNREACHABLE;
148 
149  new_t->source_location=loop_head->source_location;
150  new_t->function=loop_head->function;
151  new_t->location_number=loop_head->location_number;
152  unwind_log.insert(new_t, loop_head->location_number);
153  }
154 
155  assert(!rest_program.empty());
156 
157  // to be filled with copies of the loop body
158  goto_programt copies;
159 
160  if(k!=0)
161  {
162  iteration_points.resize(k);
163 
164  // add a goto before the loop exit to guard against 'fall-out'
165 
166  goto_programt::const_targett t_before=loop_exit;
167  t_before--;
168 
169  if(!t_before->is_goto() || !t_before->guard.is_true())
170  {
171  goto_programt::targett t_goto=goto_program.insert_before(loop_exit);
172  unwind_log.insert(t_goto, loop_exit->location_number);
173 
174  t_goto->make_goto(goto_program.const_cast_target(loop_exit));
175  t_goto->source_location=loop_exit->source_location;
176  t_goto->function=loop_exit->function;
177  t_goto->guard=true_exprt();
178  t_goto->location_number=loop_exit->location_number;
179  }
180 
181  // add a skip before the loop exit
182 
183  goto_programt::targett t_skip=goto_program.insert_before(loop_exit);
184  unwind_log.insert(t_skip, loop_exit->location_number);
185 
186  t_skip->make_skip();
187  t_skip->source_location=loop_head->source_location;
188  t_skip->function=loop_head->function;
189  t_skip->location_number=loop_head->location_number;
190 
191  // where to go for the next iteration
192  goto_programt::targett loop_iter=t_skip;
193 
194  // record the exit point of first iteration
195  iteration_points[0]=loop_iter;
196 
197  // re-direct any branches that go to loop_head to loop_iter
198 
200  t=goto_program.const_cast_target(loop_head);
201  t!=loop_iter; t++)
202  {
203  if(!t->is_goto())
204  continue;
205 
206  if(t->get_target()==loop_head)
207  t->set_target(loop_iter);
208  }
209 
210  // k-1 additional copies
211  for(unsigned i=1; i<k; i++)
212  {
213  goto_programt tmp_program;
214  copy_segment(loop_head, loop_exit, tmp_program);
215  assert(!tmp_program.instructions.empty());
216 
217  iteration_points[i]=--tmp_program.instructions.end();
218 
219  copies.destructive_append(tmp_program);
220  }
221  }
222  else
223  {
224  // insert skip for loop body
225 
226  goto_programt::targett t_skip=goto_program.insert_before(loop_head);
227  unwind_log.insert(t_skip, loop_head->location_number);
228 
229  t_skip->make_skip();
230  t_skip->source_location=loop_head->source_location;
231  t_skip->function=loop_head->function;
232  t_skip->location_number=loop_head->location_number;
233 
234  // redirect gotos into loop body
235  Forall_goto_program_instructions(i_it, goto_program)
236  {
237  if(!i_it->is_goto())
238  continue;
239 
240  goto_programt::const_targett t=i_it->get_target();
241 
242  if(t->location_number>=loop_head->location_number &&
243  t->location_number<loop_exit->location_number)
244  {
245  i_it->set_target(t_skip);
246  }
247  }
248 
249  // delete loop body
250  goto_program.instructions.erase(loop_head, loop_exit);
251  }
252 
253  // after unwound part
254  copies.destructive_append(rest_program);
255 
256  // now insert copies before loop_exit
257  goto_program.destructive_insert(loop_exit, copies);
258 }
259 
261  goto_programt &goto_program,
262  const unwindsett &unwindset,
263  const unwind_strategyt unwind_strategy)
264 {
265  for(goto_programt::const_targett i_it=goto_program.instructions.begin();
266  i_it!=goto_program.instructions.end();)
267  {
268 #ifdef DEBUG
269  symbol_tablet st;
270  namespacet ns(st);
271  std::cout << "Instruction:\n";
272  goto_program.output_instruction(ns, "", std::cout, *i_it);
273 #endif
274 
275  if(!i_it->is_backwards_goto())
276  {
277  i_it++;
278  continue;
279  }
280 
281  const irep_idt func=i_it->function;
282  assert(!func.empty());
283 
284  const irep_idt loop_id=
285  id2string(func) + "." + std::to_string(i_it->loop_number);
286 
287  auto limit=unwindset.get_limit(loop_id, 0);
288 
289  if(!limit.has_value())
290  {
291  // no unwinding given
292  i_it++;
293  continue;
294  }
295 
296  goto_programt::const_targett loop_head=i_it->get_target();
297  goto_programt::const_targett loop_exit=i_it;
298  loop_exit++;
299  assert(loop_exit!=goto_program.instructions.end());
300 
301  unwind(goto_program, loop_head, loop_exit, *limit, unwind_strategy);
302 
303  // necessary as we change the goto program in the previous line
304  i_it=loop_exit;
305  }
306 }
307 
309  goto_functionst &goto_functions,
310  const unwindsett &unwindset,
311  const unwind_strategyt unwind_strategy)
312 {
313  Forall_goto_functions(it, goto_functions)
314  {
315  goto_functionst::goto_functiont &goto_function=it->second;
316 
317  if(!goto_function.body_available())
318  continue;
319 
320 #ifdef DEBUG
321  std::cout << "Function: " << it->first << '\n';
322 #endif
323 
324  goto_programt &goto_program=goto_function.body;
325 
326  unwind(goto_program, unwindset, unwind_strategy);
327  }
328 }
329 
330 // call after calling goto_functions.update()!
332 {
333  json_objectt json_result;
334  json_arrayt &json_unwound=json_result["unwound"].make_array();
335 
336  for(location_mapt::const_iterator it=location_map.begin();
337  it!=location_map.end(); it++)
338  {
339  json_objectt &object=json_unwound.push_back().make_object();
340 
341  goto_programt::const_targett target=it->first;
342  unsigned location_number=it->second;
343 
344  object["originalLocationNumber"]=json_numbert(std::to_string(
345  location_number));
346  object["newLocationNumber"]=json_numbert(std::to_string(
347  target->location_number));
348  }
349 
350  return std::move(json_result);
351 }
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:809
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
json_numbert
Definition: json.h:235
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
goto_unwindt::unwind_strategyt
unwind_strategyt
Definition: unwind.h:27
string_utils.h
goto_unwindt::unwind_strategyt::CONTINUE
goto_programt::empty
bool empty() const
Is the program empty?
Definition: goto_program.h:626
exprt
Base class for all expressions.
Definition: expr.h:54
goto_unwindt::unwind_strategyt::ASSERT
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:53
jsont::make_object
json_objectt & make_object()
Definition: json.h:290
jsont
Definition: json.h:23
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
json_arrayt
Definition: json.h:146
goto_unwindt::unwind_strategyt::PARTIAL
json_objectt
Definition: json.h:244
unwindsett::get_limit
optionalt< unsigned > get_limit(const irep_idt &loop, unsigned thread_id) const
Definition: unwindset.cpp:64
goto_unwindt::unwind_strategyt::ASSUME
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
goto_programt::add_instruction
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:541
goto_programt::insert_before
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:510
goto_unwindt::unwind_logt::insert
void insert(const goto_programt::const_targett target, const unsigned location_number)
Definition: unwind.h:92
goto_programt::destructive_insert
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
Definition: goto_program.h:532
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
goto_programt::output_instruction
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
Definition: goto_program.cpp:37
unwindsett
Definition: unwindset.h:21
goto_unwindt::unwind_logt::output_log_json
jsont output_log_json() const
Definition: unwind.cpp:331
unwind.h
goto_unwindt::unwind
void unwind(goto_programt &goto_program, const goto_programt::const_targett loop_head, const goto_programt::const_targett loop_exit, const unsigned k, const unwind_strategyt unwind_strategy)
Definition: unwind.cpp:82
boolean_negate
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition: expr_util.cpp:127
goto_unwindt::operator()
void operator()(goto_functionst &, const unwindsett &unwindset, const unwind_strategyt unwind_strategy=unwind_strategyt::PARTIAL)
Definition: unwind.cpp:308
dstringt::empty
bool empty() const
Definition: dstring.h:75
jsont::make_array
json_arrayt & make_array()
Definition: json.h:284
false_exprt
The Boolean constant false.
Definition: std_expr.h:4452
goto_unwindt::unwind_logt::location_map
location_mapt location_map
Definition: unwind.h:101
Forall_goto_functions
#define Forall_goto_functions(it, functions)
Definition: goto_functions.h:144
loop_utils.h
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:420
expr_util.h
Deprecated expression utility functions.
goto_unwindt::copy_segment
void copy_segment(const goto_programt::const_targett start, const goto_programt::const_targett end, goto_programt &goto_program)
Definition: unwind.cpp:27
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:22
goto_programt::const_cast_target
targett const_cast_target(const_targett t)
Convert a const_targett to a targett - use with care and avoid whenever possible.
Definition: goto_program.h:424
goto_functions.h
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:415
true_exprt
The Boolean constant true.
Definition: std_expr.h:4443
std_expr.h
json_arrayt::push_back
jsont & push_back(const jsont &json)
Definition: json.h:163
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:414
goto_unwindt::unwind_log
unwind_logt unwind_log
Definition: unwind.h:104