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/std_expr.h>
20 #include <util/string_utils.h>
22 
23 #include "loop_utils.h"
24 
25 void parse_unwindset(const std::string &us, unwind_sett &unwind_set)
26 {
27  assert(unwind_set.empty());
28 
29  std::vector<std::string> result;
30  split_string(us, ',', result, true, true);
31  assert(!result.empty());
32 
33  if(result.front().empty()) // allow empty string as unwindset
34  return;
35 
36  for(std::vector<std::string>::const_iterator it=result.begin();
37  it!=result.end(); it++)
38  {
39  std::string loop;
40  std::string bound;
41 
42  split_string(*it, ':', loop, bound, true);
43 
44  std::string func;
45  std::string id;
46 
47  split_string(loop, '.', func, id, true);
48 
49  unsigned loop_id=std::stoi(id);
50  int loop_bound=std::stoi(bound);
51 
52  if(loop_bound<-1)
53  throw "given unwind bound < -1";
54 
55  unwind_set[func][loop_id]=loop_bound;
56  }
57 }
58 
60  const goto_programt::const_targett start,
61  const goto_programt::const_targett end, // exclusive
62  goto_programt &goto_program) // result
63 {
64  assert(start->location_number<end->location_number);
65  assert(goto_program.empty());
66 
67  // build map for branch targets inside the loop
68  typedef std::map<goto_programt::const_targett, unsigned> target_mapt;
69  target_mapt target_map;
70 
71  unsigned i=0;
72 
73  for(goto_programt::const_targett t=start; t!=end; t++, i++)
74  target_map[t]=i;
75 
76  // make a copy
77  std::vector<goto_programt::targett> target_vector;
78  target_vector.reserve(target_map.size());
79  assert(target_vector.empty());
80 
81  for(goto_programt::const_targett t=start; t!=end; t++)
82  {
83  goto_programt::targett t_new=goto_program.add_instruction();
84  *t_new=*t;
85  unwind_log.insert(t_new, t->location_number);
86  target_vector.push_back(t_new); // store copied instruction
87  }
88 
89  assert(goto_program.instructions.size()==target_vector.size());
90 
91  // adjust intra-segment gotos
92  for(std::size_t i=0; i<target_vector.size(); i++)
93  {
94  goto_programt::targett t=target_vector[i];
95 
96  if(!t->is_goto())
97  continue;
98 
99  goto_programt::const_targett tgt=t->get_target();
100 
101  target_mapt::const_iterator m_it=target_map.find(tgt);
102 
103  if(m_it!=target_map.end())
104  {
105  unsigned j=m_it->second;
106 
107  assert(j<target_vector.size());
108  t->set_target(target_vector[j]);
109  }
110  }
111 }
112 
114  goto_programt &goto_program,
115  const goto_programt::const_targett loop_head,
116  const goto_programt::const_targett loop_exit,
117  const unsigned k,
118  const unwind_strategyt unwind_strategy)
119 {
120  std::vector<goto_programt::targett> iteration_points;
121  unwind(goto_program, loop_head, loop_exit, k, unwind_strategy,
122  iteration_points);
123 }
124 
126  goto_programt &goto_program,
127  const goto_programt::const_targett loop_head,
128  const goto_programt::const_targett loop_exit,
129  const unsigned k,
130  const unwind_strategyt unwind_strategy,
131  std::vector<goto_programt::targett> &iteration_points)
132 {
133  assert(iteration_points.empty());
134  assert(loop_head->location_number<loop_exit->location_number);
135 
136  // rest program after unwound part
137  goto_programt rest_program;
138 
139  if(unwind_strategy==unwind_strategyt::PARTIAL)
140  {
141  goto_programt::targett t=rest_program.add_instruction();
142  unwind_log.insert(t, loop_head->location_number);
143 
144  t->make_skip();
145  t->source_location=loop_head->source_location;
146  t->function=loop_head->function;
147  t->location_number=loop_head->location_number;
148  }
149  else if(unwind_strategy==unwind_strategyt::CONTINUE)
150  {
151  copy_segment(loop_head, loop_exit, rest_program);
152  }
153  else
154  {
155  goto_programt::const_targett t=loop_exit;
156  t--;
157  assert(t->is_backwards_goto());
158 
159  exprt exit_cond;
160  exit_cond.make_false(); // default is false
161 
162  if(!t->guard.is_true()) // cond in backedge
163  {
164  exit_cond=t->guard;
165  exit_cond.make_not();
166  }
167  else if(loop_head->is_goto())
168  {
169  if(loop_head->get_target()==loop_exit) // cond in forward edge
170  exit_cond=loop_head->guard;
171  }
172 
173  goto_programt::targett new_t=rest_program.add_instruction();
174 
175  if(unwind_strategy==unwind_strategyt::ASSERT)
176  new_t->make_assertion(exit_cond);
177  else if(unwind_strategy==unwind_strategyt::ASSUME)
178  new_t->make_assumption(exit_cond);
179  else
180  assert(false);
181 
182  new_t->source_location=loop_head->source_location;
183  new_t->function=loop_head->function;
184  new_t->location_number=loop_head->location_number;
185  unwind_log.insert(new_t, loop_head->location_number);
186  }
187 
188  assert(!rest_program.empty());
189 
190  // to be filled with copies of the loop body
191  goto_programt copies;
192 
193  if(k!=0)
194  {
195  iteration_points.resize(k);
196 
197  // add a goto before the loop exit to guard against 'fall-out'
198 
199  goto_programt::const_targett t_before=loop_exit;
200  t_before--;
201 
202  if(!t_before->is_goto() || !t_before->guard.is_true())
203  {
204  goto_programt::targett t_goto=goto_program.insert_before(loop_exit);
205  unwind_log.insert(t_goto, loop_exit->location_number);
206 
207  t_goto->make_goto(goto_program.const_cast_target(loop_exit));
208  t_goto->source_location=loop_exit->source_location;
209  t_goto->function=loop_exit->function;
210  t_goto->guard=true_exprt();
211  t_goto->location_number=loop_exit->location_number;
212  }
213 
214  // add a skip before the loop exit
215 
216  goto_programt::targett t_skip=goto_program.insert_before(loop_exit);
217  unwind_log.insert(t_skip, loop_exit->location_number);
218 
219  t_skip->make_skip();
220  t_skip->source_location=loop_head->source_location;
221  t_skip->function=loop_head->function;
222  t_skip->location_number=loop_head->location_number;
223 
224  // where to go for the next iteration
225  goto_programt::targett loop_iter=t_skip;
226 
227  // record the exit point of first iteration
228  iteration_points[0]=loop_iter;
229 
230  // re-direct any branches that go to loop_head to loop_iter
231 
233  t=goto_program.const_cast_target(loop_head);
234  t!=loop_iter; t++)
235  {
236  if(!t->is_goto())
237  continue;
238 
239  if(t->get_target()==loop_head)
240  t->set_target(loop_iter);
241  }
242 
243  // k-1 additional copies
244  for(unsigned i=1; i<k; i++)
245  {
246  goto_programt tmp_program;
247  copy_segment(loop_head, loop_exit, tmp_program);
248  assert(!tmp_program.instructions.empty());
249 
250  iteration_points[i]=--tmp_program.instructions.end();
251 
252  copies.destructive_append(tmp_program);
253  }
254  }
255  else
256  {
257  // insert skip for loop body
258 
259  goto_programt::targett t_skip=goto_program.insert_before(loop_head);
260  unwind_log.insert(t_skip, loop_head->location_number);
261 
262  t_skip->make_skip();
263  t_skip->source_location=loop_head->source_location;
264  t_skip->function=loop_head->function;
265  t_skip->location_number=loop_head->location_number;
266 
267  // redirect gotos into loop body
268  Forall_goto_program_instructions(i_it, goto_program)
269  {
270  if(!i_it->is_goto())
271  continue;
272 
273  goto_programt::const_targett t=i_it->get_target();
274 
275  if(t->location_number>=loop_head->location_number &&
276  t->location_number<loop_exit->location_number)
277  {
278  i_it->set_target(t_skip);
279  }
280  }
281 
282  // delete loop body
283  goto_program.instructions.erase(loop_head, loop_exit);
284  }
285 
286  // after unwound part
287  copies.destructive_append(rest_program);
288 
289  // now insert copies before loop_exit
290  goto_program.destructive_insert(loop_exit, copies);
291 }
292 
294  const irep_idt func,
295  const unsigned loop_id,
296  const int global_k,
297  const unwind_sett &unwind_set) const
298 {
299  assert(global_k>=-1);
300 
301  unwind_sett::const_iterator f_it=unwind_set.find(func);
302  if(f_it==unwind_set.end())
303  return global_k;
304 
305  const std::map<unsigned, int> &m=f_it->second;
306  std::map<unsigned, int>::const_iterator l_it=m.find(loop_id);
307  if(l_it==m.end())
308  return global_k;
309 
310  int k=l_it->second;
311  assert(k>=-1);
312 
313  return k;
314 }
315 
317  goto_programt &goto_program,
318  const unwind_sett &unwind_set,
319  const int k,
320  const unwind_strategyt unwind_strategy)
321 {
322  assert(k>=-1);
323 
324  for(goto_programt::const_targett i_it=goto_program.instructions.begin();
325  i_it!=goto_program.instructions.end();)
326  {
327 #ifdef DEBUG
328  symbol_tablet st;
329  namespacet ns(st);
330  std::cout << "Instruction:\n";
331  goto_program.output_instruction(ns, "", std::cout, i_it);
332 #endif
333 
334  if(!i_it->is_backwards_goto())
335  {
336  i_it++;
337  continue;
338  }
339 
340  const irep_idt func=i_it->function;
341  assert(!func.empty());
342 
343  unsigned loop_number=i_it->loop_number;
344 
345  int final_k=get_k(func, loop_number, k, unwind_set);
346 
347  if(final_k==-1)
348  {
349  i_it++;
350  continue;
351  }
352 
353  goto_programt::const_targett loop_head=i_it->get_target();
354  goto_programt::const_targett loop_exit=i_it;
355  loop_exit++;
356  assert(loop_exit!=goto_program.instructions.end());
357 
358  unwind(goto_program, loop_head, loop_exit, final_k, unwind_strategy);
359 
360  // necessary as we change the goto program in the previous line
361  i_it=loop_exit;
362  }
363 }
364 
366  goto_functionst &goto_functions,
367  const unwind_sett &unwind_set,
368  const int k,
369  const unwind_strategyt unwind_strategy)
370 {
371  assert(k>=-1);
372 
373  Forall_goto_functions(it, goto_functions)
374  {
375  goto_functionst::goto_functiont &goto_function=it->second;
376 
377  if(!goto_function.body_available())
378  continue;
379 
380 #ifdef DEBUG
381  std::cout << "Function: " << it->first << '\n';
382 #endif
383 
384  goto_programt &goto_program=goto_function.body;
385 
386  unwind(goto_program, unwind_set, k, unwind_strategy);
387  }
388 }
389 
390 // call after calling goto_functions.update()!
392 {
393  json_objectt json_result;
394  json_arrayt &json_unwound=json_result["unwound"].make_array();
395 
396  for(location_mapt::const_iterator it=location_map.begin();
397  it!=location_map.end(); it++)
398  {
399  json_objectt &object=json_unwound.push_back().make_object();
400 
401  goto_programt::const_targett target=it->first;
402  unsigned location_number=it->second;
403 
404  object["originalLocationNumber"]=json_numbert(std::to_string(
405  location_number));
406  object["newLocationNumber"]=json_numbert(std::to_string(
407  target->location_number));
408  }
409 
410  return json_result;
411 }
targett add_instruction()
Adds an instruction at the end.
void insert(const goto_programt::const_targett target, const unsigned location_number)
Definition: unwind.h:98
instructionst instructions
The list of instructions in the goto program.
void parse_unwindset(const std::string &us, unwind_sett &unwind_set)
Definition: unwind.cpp:25
Goto Programs with Functions.
Definition: json.h:21
bool empty() const
Is the program empty?
void operator()(goto_functionst &goto_functions, const unsigned k, const unwind_strategyt unwind_strategy=unwind_strategyt::PARTIAL)
Definition: unwind.h:59
json_arrayt & make_array()
Definition: json.h:228
unwind_strategyt
Definition: unwind.h:30
jsont & push_back(const jsont &json)
Definition: json.h:157
instructionst::const_iterator const_targett
The boolean constant true.
Definition: std_expr.h:3742
API to expression classes.
The symbol table.
Definition: symbol_table.h:52
TO_BE_DOCUMENTED.
Definition: namespace.h:62
targett const_cast_target(const_targett t)
Convert a const_targett to a targett - use with care and avoid whenever possible. ...
void copy_segment(const goto_programt::const_targett start, const goto_programt::const_targett end, goto_programt &goto_program)
Definition: unwind.cpp:59
Helper functions for k-induction and loop invariants.
Loop unwinding.
targett insert_before(const_targett target)
Insertion before the given target.
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
int get_k(const irep_idt func, const unsigned loop_id, const int global_k, const unwind_sett &unwind_set) const
Definition: unwind.cpp:293
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
Base class for all expressions.
Definition: expr.h:46
jsont output_log_json() const
Definition: unwind.cpp:391
void make_false()
Definition: expr.cpp:159
#define Forall_goto_functions(it, functions)
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:73
void destructive_insert(const_targett target, goto_program_templatet< codeT, guardT > &p)
Inserts the given program at the given location.
unwind_logt unwind_log
Definition: unwind.h:110
std::map< irep_idt, std::map< unsigned, int > > unwind_sett
Definition: unwind.h:20
json_objectt & make_object()
Definition: json.h:234
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:113
std::ostream & output_instruction(const class namespacet &ns, const irep_idt &identifier, std::ostream &out, instructionst::const_iterator it) const
See below.
bool empty() const
Definition: dstring.h:61