cprover
goto_inline_class.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Function Inlining
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "goto_inline_class.h"
13 
14 #ifdef DEBUG
15 #include <iostream>
16 #endif
17 
18 #include <cassert>
19 
20 #include <util/prefix.h>
21 #include <util/cprover_prefix.h>
22 #include <util/base_type.h>
23 #include <util/std_code.h>
24 #include <util/std_expr.h>
25 #include <util/expr_util.h>
26 
27 #include "remove_skip.h"
28 #include "goto_inline.h"
29 
31  const goto_programt::targett target,
32  const irep_idt &function_name, // name of called function
33  const code_typet &code_type, // type of called function
34  const exprt::operandst &arguments, // arguments of call
35  goto_programt &dest)
36 {
37  assert(is_call(target));
38  assert(dest.empty());
39 
40  const source_locationt &source_location=target->source_location;
41 
42  // iterates over the operands
43  exprt::operandst::const_iterator it1=arguments.begin();
44 
45  const code_typet::parameterst &parameter_types=
46  code_type.parameters();
47 
48  // iterates over the types of the parameters
49  for(code_typet::parameterst::const_iterator
50  it2=parameter_types.begin();
51  it2!=parameter_types.end();
52  it2++)
53  {
54  const code_typet::parametert &parameter=*it2;
55 
56  // this is the type the n-th argument should be
57  const typet &par_type=ns.follow(parameter.type());
58 
59  const irep_idt &identifier=parameter.get_identifier();
60 
61  if(identifier.empty())
62  {
63  error().source_location=source_location;
64  error() << "no identifier for function parameter" << eom;
65  throw 0;
66  }
67 
68  {
69  const symbolt &symbol=ns.lookup(identifier);
70 
72  decl->make_decl();
73  decl->code=code_declt(symbol.symbol_expr());
74  decl->code.add_source_location()=source_location;
75  decl->source_location=source_location;
76  decl->function=adjust_function?target->function:function_name;
77  }
78 
79  // this is the actual parameter
80  exprt actual;
81 
82  // if you run out of actual arguments there was a mismatch
83  if(it1==arguments.end())
84  {
85  warning().source_location=source_location;
86  warning() << "call to `" << function_name << "': "
87  << "not enough arguments, "
88  << "inserting non-deterministic value" << eom;
89 
90  actual=side_effect_expr_nondett(par_type);
91  }
92  else
93  actual=*it1;
94 
95  // nil means "don't assign"
96  if(actual.is_nil())
97  {
98  }
99  else
100  {
101  // it should be the same exact type as the parameter,
102  // subject to some exceptions
103  if(!base_type_eq(par_type, actual.type(), ns))
104  {
105  const typet &f_partype=ns.follow(par_type);
106  const typet &f_acttype=ns.follow(actual.type());
107 
108  // we are willing to do some conversion
109  if((f_partype.id()==ID_pointer &&
110  f_acttype.id()==ID_pointer) ||
111  (f_partype.id()==ID_pointer &&
112  f_acttype.id()==ID_array &&
113  f_partype.subtype()==f_acttype.subtype()))
114  {
115  actual.make_typecast(par_type);
116  }
117  else if((f_partype.id()==ID_signedbv ||
118  f_partype.id()==ID_unsignedbv ||
119  f_partype.id()==ID_bool) &&
120  (f_acttype.id()==ID_signedbv ||
121  f_acttype.id()==ID_unsignedbv ||
122  f_acttype.id()==ID_bool))
123  {
124  actual.make_typecast(par_type);
125  }
126  else
127  {
129 
130  error() << "function call: argument `" << identifier
131  << "' type mismatch: argument is `"
132  // << from_type(ns, identifier, actual.type())
133  << actual.type().pretty()
134  << "', parameter is `"
135  << from_type(ns, identifier, par_type)
136  << "'" << eom;
137  throw 0;
138  }
139  }
140 
141  // adds an assignment of the actual parameter to the formal parameter
142  code_assignt assignment(symbol_exprt(identifier, par_type), actual);
143  assignment.add_source_location()=source_location;
144 
145  dest.add_instruction(ASSIGN);
146  dest.instructions.back().source_location=source_location;
147  dest.instructions.back().code.swap(assignment);
148  dest.instructions.back().function=
149  adjust_function?target->function:function_name;
150  }
151 
152  if(it1!=arguments.end())
153  ++it1;
154  }
155 
156  if(it1!=arguments.end())
157  {
158  // too many arguments -- we just ignore that, no harm done
159  }
160 }
161 
163  const goto_programt::targett target,
164  const irep_idt &function_name, // name of called function
165  const code_typet &code_type, // type of called function
166  goto_programt &dest)
167 {
168  assert(is_call(target));
169  assert(dest.empty());
170 
171  const source_locationt &source_location=target->source_location;
172 
173  const code_typet::parameterst &parameter_types=
174  code_type.parameters();
175 
176  // iterates over the types of the parameters
177  for(code_typet::parameterst::const_iterator
178  it=parameter_types.begin();
179  it!=parameter_types.end();
180  it++)
181  {
182  const code_typet::parametert &parameter=*it;
183 
184  const irep_idt &identifier=parameter.get_identifier();
185 
186  if(identifier.empty())
187  {
188  error().source_location=source_location;
189  error() << "no identifier for function parameter" << eom;
190  throw 0;
191  }
192 
193  {
194  const symbolt &symbol=ns.lookup(identifier);
195 
197  dead->make_dead();
198  dead->code=code_deadt(symbol.symbol_expr());
199  dead->code.add_source_location()=source_location;
200  dead->source_location=source_location;
201  dead->function=adjust_function?target->function:function_name;
202  }
203  }
204 }
205 
207  goto_programt &dest, // inlining this
208  const exprt &lhs, // lhs in caller
209  const exprt &constrain)
210 {
211  for(goto_programt::instructionst::iterator
212  it=dest.instructions.begin();
213  it!=dest.instructions.end();
214  it++)
215  {
216  if(it->is_return())
217  {
218  #if 0
219  if(lhs.is_not_nil())
220  {
221  if(it->code.operands().size()!=1)
222  {
223  error().source_location=it->code.find_source_location();
224  str << "return expects one operand!";
225  warning_msg();
226  continue;
227  }
228 
229  goto_programt tmp;
231 
232  code_assignt code_assign(lhs, it->code.op0());
233 
234  // this may happen if the declared return type at the call site
235  // differs from the defined return type
236  if(code_assign.lhs().type()!=
237  code_assign.rhs().type())
238  code_assign.rhs().make_typecast(code_assign.lhs().type());
239 
240  assignment->code=code_assign;
241  assignment->source_location=it->source_location;
242  assignment->function=it->function;
243 
244  if(constrain.is_not_nil() && !constrain.is_true())
245  {
246  codet constrain(ID_bp_constrain);
247  constrain.reserve_operands(2);
248  constrain.move_to_operands(assignment->code);
249  constrain.copy_to_operands(constrain);
250  }
251 
252  dest.insert_before_swap(it, *assignment);
253  it++;
254  }
255  else if(!it->code.operands().empty())
256  {
257  goto_programt tmp;
259 
260  expression->code=codet(ID_expression);
261  expression->code.move_to_operands(it->code.op0());
262  expression->source_location=it->source_location;
263  expression->function=it->function;
264 
265  dest.insert_before_swap(it, *expression);
266  it++;
267  }
268 
269  it->make_goto(--dest.instructions.end());
270  #else
271  if(lhs.is_not_nil())
272  {
273  if(it->code.operands().size()!=1)
274  {
275  warning().source_location=it->code.find_source_location();
276  warning() << "return expects one operand!\n"
277  << it->code.pretty() << eom;
278  continue;
279  }
280 
281  code_assignt code_assign(lhs, it->code.op0());
282 
283  // this may happen if the declared return type at the call site
284  // differs from the defined return type
285  if(code_assign.lhs().type()!=
286  code_assign.rhs().type())
287  code_assign.rhs().make_typecast(code_assign.lhs().type());
288 
289  if(constrain.is_not_nil() && !constrain.is_true())
290  {
291  codet constrain(ID_bp_constrain);
292  constrain.reserve_operands(2);
293  constrain.move_to_operands(code_assign);
294  constrain.copy_to_operands(constrain);
295  it->code=constrain;
296  it->type=OTHER;
297  }
298  else
299  {
300  it->code=code_assign;
301  it->type=ASSIGN;
302  }
303 
304  it++;
305  }
306  else if(!it->code.operands().empty())
307  {
308  codet expression(ID_expression);
309  expression.move_to_operands(it->code.op0());
310  it->code=expression;
311  it->type=OTHER;
312  it++;
313  }
314  #endif
315  }
316  }
317 }
318 
320  source_locationt &dest,
321  const source_locationt &new_location)
322 {
323  // we copy, and then adjust for property_id, property_class
324  // and comment, if necessary
325 
327  irep_idt property_class=dest.get_property_class();
328  irep_idt property_id=dest.get_property_id();
329 
330  dest=new_location;
331 
332  if(!comment.empty())
333  dest.set_comment(comment);
334 
335  if(!property_class.empty())
336  dest.set_property_class(property_class);
337 
338  if(!property_id.empty())
339  dest.set_property_id(property_id);
340 }
341 
343  exprt &dest,
344  const source_locationt &new_location)
345 {
346  Forall_operands(it, dest)
347  replace_location(*it, new_location);
348 
349  if(dest.find(ID_C_source_location).is_not_nil())
350  replace_location(dest.add_source_location(), new_location);
351 }
352 
354  const goto_functiont &goto_function,
355  goto_programt &dest,
356  goto_programt::targett target,
357  const exprt &lhs,
358  const symbol_exprt &function,
359  const exprt::operandst &arguments,
360  const exprt &constrain)
361 {
362  assert(is_call(target));
363  assert(!dest.empty());
364  assert(goto_function.body_available());
365 
366  const irep_idt identifier=function.get_identifier();
367 
368  goto_programt body;
369  body.copy_from(goto_function.body);
370  inline_log.copy_from(goto_function.body, body);
371 
372  goto_programt::instructiont &end=body.instructions.back();
373  assert(end.is_end_function());
374  end.type=LOCATION;
375 
376  if(adjust_function)
378  i_it->function=target->function;
379 
380  replace_return(body, lhs, constrain);
381 
382  goto_programt tmp1;
384  target,
385  identifier,
386  goto_function.type,
387  arguments,
388  tmp1);
389 
390  goto_programt tmp2;
391  parameter_destruction(target, identifier, goto_function.type, tmp2);
392 
393  goto_programt tmp;
394  tmp.destructive_append(tmp1); // par assignment
395  tmp.destructive_append(body); // body
396  tmp.destructive_append(tmp2); // par destruction
397 
399  t_it=goto_function.body.instructions.begin();
400  unsigned begin_location_number=t_it->location_number;
401  t_it=--goto_function.body.instructions.end();
402  assert(t_it->is_end_function());
403  unsigned end_location_number=t_it->location_number;
404 
405  unsigned call_location_number=target->location_number;
406 
408  tmp,
409  begin_location_number,
410  end_location_number,
411  call_location_number,
412  identifier);
413 
414 #if 0
415  if(goto_function.is_hidden())
416  {
417  source_locationt new_source_location=
418  function.find_source_location();
419 
420  if(new_source_location.is_not_nil())
421  {
422  new_source_location.set_hide();
423 
425  {
426  if(it->function==identifier)
427  {
428  // don't hide assignment to lhs
429  if(it->is_assign() && to_code_assign(it->code).lhs()==lhs)
430  {
431  }
432  else
433  {
434  replace_location(it->source_location, new_source_location);
435  replace_location(it->guard, new_source_location);
436  replace_location(it->code, new_source_location);
437  }
438 
439  it->function=target->function;
440  }
441  }
442  }
443  }
444 #endif
445 
446  // kill call
447  target->type=LOCATION;
448  target->code.clear();
449  target++;
450 
451  dest.destructive_insert(target, tmp);
452 }
453 
455  goto_programt &dest,
456  const exprt &lhs,
457  goto_programt::targett target,
458  const symbol_exprt &function,
459  const exprt::operandst &arguments)
460 {
461  assert(is_call(target));
462  assert(!dest.empty());
463 
464  const irep_idt identifier=function.get_identifier();
465 
466  if(no_body_set.insert(identifier).second) // newly inserted
467  {
468  warning().source_location=function.find_source_location();
469  warning() << "no body for function `" << identifier << "'" << eom;
470  }
471 
472  goto_programt tmp;
473 
474  // evaluate function arguments -- they might have
475  // pointer dereferencing or the like
476  forall_expr(it, arguments)
477  {
479  t->make_other(code_expressiont(*it));
480  t->source_location=target->source_location;
481  t->function=target->function;
482  }
483 
484  // return value
485  if(lhs.is_not_nil())
486  {
487  side_effect_expr_nondett rhs(lhs.type());
488  rhs.add_source_location()=target->source_location;
489 
490  code_assignt code(lhs, rhs);
491  code.add_source_location()=target->source_location;
492 
494  t->source_location=target->source_location;
495  t->function=target->function;
496  t->code.swap(code);
497  }
498 
499  // kill call
500  target->type=LOCATION;
501  target->code.clear();
502  target++;
503 
504  dest.destructive_insert(target, tmp);
505 }
506 
508  goto_programt &dest,
509  const inline_mapt &inline_map,
510  const bool transitive,
511  const bool force_full,
512  goto_programt::targett target)
513 {
514  assert(is_call(target));
515  assert(!dest.empty());
516  assert(!transitive || inline_map.empty());
517 
518 #ifdef DEBUG
519  std::cout << "Expanding call:\n";
520  dest.output_instruction(ns, "", std::cout, target);
521 #endif
522 
523  exprt lhs;
524  exprt function_expr;
525  exprt::operandst arguments;
526  exprt constrain;
527 
528  get_call(target, lhs, function_expr, arguments, constrain);
529 
530  if(function_expr.id()!=ID_symbol)
531  return;
532 
533  const symbol_exprt &function=to_symbol_expr(function_expr);
534 
535  const irep_idt identifier=function.get_identifier();
536 
537  if(is_ignored(identifier))
538  return;
539 
540  // see if we are already expanding it
541  if(recursion_set.find(identifier)!=recursion_set.end())
542  {
543  // it's recursive.
544  // Uh. Buh. Give up.
545  warning().source_location=function.find_source_location();
546  warning() << "recursion is ignored on call to `" << identifier << "'"
547  << eom;
548 
549  if(force_full)
550  target->make_skip();
551 
552  return;
553  }
554 
555  goto_functionst::function_mapt::iterator f_it=
556  goto_functions.function_map.find(identifier);
557 
558  if(f_it==goto_functions.function_map.end())
559  {
560  warning().source_location=function.find_source_location();
561  warning() << "missing function `" << identifier << "' is ignored" << eom;
562 
563  if(force_full)
564  target->make_skip();
565 
566  return;
567  }
568 
569  // function to inline
570  goto_functiont &goto_function=f_it->second;
571 
572  if(goto_function.body_available())
573  {
574  if(transitive)
575  {
576  const goto_functiont &cached=
578  identifier,
579  goto_function,
580  force_full);
581 
582  // insert 'cached' into 'dest' at 'target'
584  cached,
585  dest,
586  target,
587  lhs,
588  function,
589  arguments,
590  constrain);
591 
592  progress() << "Inserting " << identifier << " into caller" << eom;
593  progress() << "Number of instructions: "
594  << cached.body.instructions.size() << eom;
595 
596  if(!caching)
597  {
598  progress() << "Removing " << identifier << " from cache" << eom;
599  progress() << "Number of instructions: "
600  << cached.body.instructions.size() << eom;
601 
602  inline_log.cleanup(cached.body);
603  cache.erase(identifier);
604  }
605  }
606  else
607  {
608  // inline non-transitively
610  identifier,
611  goto_function,
612  inline_map,
613  force_full);
614 
615  // insert 'goto_function' into 'dest' at 'target'
617  goto_function,
618  dest,
619  target,
620  lhs,
621  function,
622  arguments,
623  constrain);
624  }
625  }
626  else // no body available
627  {
628  insert_function_nobody(dest, lhs, target, function, arguments);
629  }
630 }
631 
634  exprt &lhs,
635  exprt &function,
636  exprt::operandst &arguments,
637  exprt &constrain)
638 {
639  assert(is_call(it));
640 
641  if(it->is_function_call())
642  {
643  const code_function_callt &call=to_code_function_call(it->code);
644 
645  lhs=call.lhs();
646  function=call.function();
647  arguments=call.arguments();
648  constrain=static_cast<const exprt &>(get_nil_irep());
649  }
650  else
651  {
652  assert(is_bp_call(it));
653 
654  lhs=it->code.op0().op0();
655  function=to_symbol_expr(it->code.op0().op1().op0());
656  arguments=it->code.op0().op1().op1().operands();
657  constrain=it->code.op1();
658  }
659 }
660 
662 {
663  return it->is_function_call() || is_bp_call(it);
664 }
665 
667 {
668  if(!it->is_other())
669  return false;
670 
671  return it->code.get(ID_statement)==ID_bp_constrain &&
672  it->code.operands().size()==2 &&
673  it->code.op0().operands().size()==2 &&
674  it->code.op0().op1().get(ID_statement)==ID_function_call;
675 }
676 
678  const inline_mapt &inline_map,
679  const bool force_full)
680 {
681  assert(check_inline_map(inline_map));
682 
684  {
685  const irep_idt identifier=f_it->first;
686  assert(!identifier.empty());
687  goto_functiont &goto_function=f_it->second;
688 
689  if(!goto_function.body_available())
690  continue;
691 
692  goto_inline(identifier, goto_function, inline_map, force_full);
693  }
694 }
695 
697  const irep_idt identifier,
698  goto_functiont &goto_function,
699  const inline_mapt &inline_map,
700  const bool force_full)
701 {
702  recursion_set.clear();
703 
705  identifier,
706  goto_function,
707  inline_map,
708  force_full);
709 }
710 
712  const irep_idt identifier,
713  goto_functiont &goto_function,
714  const inline_mapt &inline_map,
715  const bool force_full)
716 {
717  assert(goto_function.body_available());
718 
719  finished_sett::const_iterator f_it=finished_set.find(identifier);
720 
721  if(f_it!=finished_set.end())
722  return;
723 
724  assert(check_inline_map(identifier, inline_map));
725 
726  goto_programt &goto_program=goto_function.body;
727 
728  const inline_mapt::const_iterator im_it=inline_map.find(identifier);
729 
730  if(im_it==inline_map.end())
731  return;
732 
733  const call_listt &call_list=im_it->second;
734 
735  if(call_list.empty())
736  return;
737 
738  recursion_set.insert(identifier);
739 
740  for(call_listt::const_iterator c_it=call_list.begin();
741  c_it!=call_list.end(); c_it++)
742  {
743  const callt &call=*c_it;
744  const bool transitive=call.second;
745 
746  const inline_mapt &new_inline_map=
747  transitive?inline_mapt():inline_map;
748 
750  goto_program,
751  new_inline_map,
752  transitive,
753  force_full,
754  call.first);
755  }
756 
757  recursion_set.erase(identifier);
758 
759  // remove_skip(goto_program);
760  // goto_program.update(); // does not change loop ids
761 
762  finished_set.insert(identifier);
763 }
764 
766  const irep_idt identifier,
767  const goto_functiont &goto_function,
768  const bool force_full)
769 {
770  assert(goto_function.body_available());
771 
772  cachet::const_iterator c_it=cache.find(identifier);
773 
774  if(c_it!=cache.end())
775  {
776  const goto_functiont &cached=c_it->second;
777  assert(cached.body_available());
778  return cached;
779  }
780 
781  goto_functiont &cached=cache[identifier];
782  assert(cached.body.empty());
783 
784  progress() << "Creating copy of " << identifier << eom;
785  progress() << "Number of instructions: "
786  << goto_function.body.instructions.size() << eom;
787 
788  cached.copy_from(goto_function); // location numbers not changed
789  inline_log.copy_from(goto_function.body, cached.body);
790 
791  goto_programt &goto_program=cached.body;
792 
793  goto_programt::targetst call_list;
794 
795  for(goto_programt::targett i_it=goto_program.instructions.begin();
796  i_it!=goto_program.instructions.end(); i_it++)
797  {
798  if(is_call(i_it))
799  call_list.push_back(i_it);
800  }
801 
802  if(call_list.empty())
803  return cached;
804 
805  recursion_set.insert(identifier);
806 
807  for(goto_programt::targetst::iterator c_it=call_list.begin();
808  c_it!=call_list.end(); c_it++)
809  {
811  goto_program,
812  inline_mapt(),
813  true,
814  force_full,
815  *c_it);
816  }
817 
818  recursion_set.erase(identifier);
819 
820  // remove_skip(goto_program);
821  // goto_program.update(); // does not change loop ids
822 
823  return cached;
824 }
825 
826 bool goto_inlinet::is_ignored(const irep_idt id) const
827 {
828  return
829  id=="__CPROVER_cleanup" ||
830  id=="__CPROVER_set_must" ||
831  id=="__CPROVER_set_may" ||
832  id=="__CPROVER_clear_must" ||
833  id=="__CPROVER_clear_may" ||
834  id=="__CPROVER_cover";
835 }
836 
838  const irep_idt identifier,
839  const inline_mapt &inline_map) const
840 {
841  goto_functionst::function_mapt::const_iterator f_it=
842  goto_functions.function_map.find(identifier);
843 
844  assert(f_it!=goto_functions.function_map.end());
845 
846  inline_mapt::const_iterator im_it=inline_map.find(identifier);
847 
848  if(im_it==inline_map.end())
849  return true;
850 
851  const call_listt &call_list=im_it->second;
852 
853  if(call_list.empty())
854  return true;
855 
856  int ln=-1;
857 
858  for(call_listt::const_iterator c_it=call_list.begin();
859  c_it!=call_list.end(); c_it++)
860  {
861  const callt &call=*c_it;
862  const goto_programt::const_targett target=call.first;
863 
864 #if 0
865  // might not hold if call was previously inlined
866  if(target->function!=identifier)
867  return false;
868 #endif
869 
870  // location numbers increasing
871  if(static_cast<int>(target->location_number)<=ln)
872  return false;
873 
874  if(!is_call(target))
875  return false;
876 
877  ln=target->location_number;
878  }
879 
880  return true;
881 }
882 
883 bool goto_inlinet::check_inline_map(const inline_mapt &inline_map) const
884 {
886  {
887  if(!check_inline_map(f_it->first, inline_map))
888  return false;
889  }
890 
891  return true;
892 }
893 
895  std::ostream &out,
896  const inline_mapt &inline_map)
897 {
898  assert(check_inline_map(inline_map));
899 
900  for(inline_mapt::const_iterator it=inline_map.begin();
901  it!=inline_map.end(); it++)
902  {
903  const irep_idt id=it->first;
904  const call_listt &call_list=it->second;
905 
906  out << "Function: " << id << "\n";
907 
908  goto_functionst::function_mapt::const_iterator f_it=
909  goto_functions.function_map.find(id);
910 
911  std::string call="-";
912 
913  if(f_it!=goto_functions.function_map.end() &&
914  !call_list.empty())
915  {
916  const goto_functiont &goto_function=f_it->second;
917  assert(goto_function.body_available());
918 
919  const goto_programt &goto_program=goto_function.body;
920 
921  for(call_listt::const_iterator c_it=call_list.begin();
922  c_it!=call_list.end(); c_it++)
923  {
924  const callt &call=*c_it;
925  const goto_programt::const_targett target=call.first;
926  bool transitive=call.second;
927 
928  out << " Call:\n";
929  goto_program.output_instruction(ns, "", out, target);
930  out << " Transitive: " << transitive << "\n";
931  }
932  }
933  else
934  {
935  out << " -\n";
936  }
937  }
938 }
939 
940 void goto_inlinet::output_cache(std::ostream &out) const
941 {
942  for(auto it=cache.begin(); it!=cache.end(); it++)
943  {
944  if(it!=cache.begin())
945  out << ", ";
946 
947  out << it->first << "\n";
948  }
949 }
950 
951 // remove segment that refer to the given goto program
953  const goto_programt &goto_program)
954 {
955  forall_goto_program_instructions(it, goto_program)
956  log_map.erase(it);
957 }
958 
960  const goto_functionst::function_mapt &function_map)
961 {
962  for(goto_functionst::function_mapt::const_iterator it=
963  function_map.begin(); it!=function_map.end(); it++)
964  {
965  const goto_functiont &goto_function=it->second;
966 
967  if(!goto_function.body_available())
968  continue;
969 
970  cleanup(goto_function.body);
971  }
972 }
973 
975  const goto_programt &goto_program,
976  const unsigned begin_location_number,
977  const unsigned end_location_number,
978  const unsigned call_location_number,
979  const irep_idt function)
980 {
981  assert(!goto_program.empty());
982  assert(!function.empty());
983  assert(end_location_number>=begin_location_number);
984 
985  goto_programt::const_targett start=goto_program.instructions.begin();
986  assert(log_map.find(start)==log_map.end());
987 
988  goto_programt::const_targett end=goto_program.instructions.end();
989  end--;
990 
992  info.begin_location_number=begin_location_number;
993  info.end_location_number=end_location_number;
994  info.call_location_number=call_location_number;
995  info.function=function;
996  info.end=end;
997 
998  log_map[start]=info;
999 }
1000 
1002  const goto_programt &from,
1003  const goto_programt &to)
1004 {
1005  assert(from.instructions.size()==to.instructions.size());
1006 
1007  goto_programt::const_targett it1=from.instructions.begin();
1009 
1010  for(; it1!=from.instructions.end(); it1++, it2++)
1011  {
1012  assert(it2!=to.instructions.end());
1013  assert(it1->location_number==it2->location_number);
1014 
1015  log_mapt::const_iterator l_it=log_map.find(it1);
1016  if(l_it!=log_map.end()) // a segment starts here
1017  {
1018  // as 'to' is a fresh copy
1019  assert(log_map.find(it2)==log_map.end());
1020 
1021  goto_inline_log_infot info=l_it->second;
1022  goto_programt::const_targett end=info.end;
1023 
1024  // find end of new
1025  goto_programt::const_targett tmp_it=it1;
1026  goto_programt::const_targett new_end=it2;
1027  while(tmp_it!=end)
1028  {
1029  new_end++;
1030  tmp_it++;
1031  }
1032 
1033  info.end=new_end;
1034 
1035  log_map[it2]=info;
1036  }
1037  }
1038 }
1039 
1040 // call after goto_functions.update()!
1042 {
1043  json_objectt json_result;
1044  json_arrayt &json_inlined=json_result["inlined"].make_array();
1045 
1046  for(log_mapt::const_iterator it=log_map.begin();
1047  it!=log_map.end(); it++)
1048  {
1049  json_objectt &object=json_inlined.push_back().make_object();
1050 
1051  goto_programt::const_targett start=it->first;
1052  const goto_inline_log_infot &info=it->second;
1054 
1055  assert(start->location_number<=end->location_number);
1056 
1057  object["call"]=json_numbert(std::to_string(info.call_location_number));
1058  object["function"]=json_stringt(info.function.c_str());
1059 
1060  json_arrayt &json_orig=object["originalSegment"].make_array();
1061  json_orig.push_back()=json_numbert(std::to_string(
1062  info.begin_location_number));
1063  json_orig.push_back()=json_numbert(std::to_string(
1064  info.end_location_number));
1065 
1066  json_arrayt &json_new=object["inlinedSegment"].make_array();
1067  json_new.push_back()=json_numbert(std::to_string(start->location_number));
1068  json_new.push_back()=json_numbert(std::to_string(end->location_number));
1069  }
1070 
1071  return json_result;
1072 }
const irept & get_nil_irep()
Definition: irep.cpp:56
std::map< irep_idt, goto_functiont > function_mapt
The type of an expression.
Definition: type.h:20
mstreamt & warning()
Definition: message.h:228
std::pair< goto_programt::targett, bool > callt
std::list< callt > call_listt
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
void add_segment(const goto_programt &goto_program, const unsigned begin_location_number, const unsigned end_location_number, const unsigned call_location_number, const irep_idt function)
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
targett add_instruction()
Adds an instruction at the end.
Base type of functions.
Definition: std_types.h:734
bool is_nil() const
Definition: irep.h:103
bool is_not_nil() const
Definition: irep.h:104
goto_inline_logt inline_log
exprt & op0()
Definition: expr.h:84
void set_property_class(const irep_idt &property_class)
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:115
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Definition: base_type.cpp:270
bool is_ignored(const irep_idt id) const
static bool is_bp_call(goto_programt::const_targett target)
instructionst instructions
The list of instructions in the goto program.
Deprecated expression utility functions.
void set_comment(const irep_idt &comment)
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:61
#define forall_expr(it, expr)
Definition: expr.h:28
Definition: json.h:21
void move_to_operands(exprt &expr)
Definition: expr.cpp:28
void cleanup(const goto_programt &goto_program)
std::vector< parametert > parameterst
Definition: std_types.h:829
const bool caching
bool is_true() const
Definition: expr.cpp:133
bool empty() const
Is the program empty?
typet & type()
Definition: expr.h:60
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
An expression statement.
Definition: std_code.h:957
static void get_call(goto_programt::const_targett target, exprt &lhs, exprt &function, exprt::operandst &arguments, exprt &constrain)
json_arrayt & make_array()
Definition: json.h:228
void set_property_id(const irep_idt &property_id)
void parameter_destruction(const goto_programt::targett target, const irep_idt &function_name, const code_typet &code_type, goto_programt &dest)
jsont & push_back(const jsont &json)
Definition: json.h:157
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:178
const irep_idt & id() const
Definition: irep.h:189
void goto_inline(const irep_idt identifier, goto_functiont &goto_function, const inline_mapt &inline_map, const bool force_full=false)
exprt & lhs()
Definition: std_code.h:157
std::map< irep_idt, call_listt > inline_mapt
instructionst::const_iterator const_targett
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:191
argumentst & arguments()
Definition: std_code.h:689
void insert_function_body(const goto_functiont &f, goto_programt &dest, goto_programt::targett target, const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, const exprt &constrain)
A declaration of a local variable.
Definition: std_code.h:192
exprt & rhs()
Definition: std_code.h:162
const source_locationt & find_source_location() const
Definition: expr.cpp:466
recursion_sett recursion_set
source_locationt source_location
Definition: message.h:175
API to expression classes.
exprt & op1()
Definition: expr.h:87
void replace_return(goto_programt &body, const exprt &lhs, const exprt &constrain)
Function Inlining.
void expand_function_call(goto_programt &dest, const inline_mapt &inline_map, const bool transitive, const bool force_full, goto_programt::targett target)
A side effect that returns a non-deterministically chosen value.
Definition: std_code.h:1037
A function call.
Definition: std_code.h:657
bool check_inline_map(const inline_mapt &inline_map) const
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
const goto_functiont & goto_inline_transitive(const irep_idt identifier, const goto_functiont &goto_function, const bool force_full)
std::vector< exprt > operandst
Definition: expr.h:49
const bool adjust_function
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
goto_functionst & goto_functions
const namespacet & ns
finished_sett finished_set
no_body_sett no_body_set
void output_cache(std::ostream &out) const
void copy_from(const goto_program_templatet< codeT, guardT > &src)
Copy a full goto program, preserving targets.
void parameter_assignments(const goto_programt::targett target, const irep_idt &function_name, const code_typet &code_type, const exprt::operandst &arguments, goto_programt &dest)
exprt & function()
Definition: std_code.h:677
Base class for all expressions.
Definition: expr.h:46
const parameterst & parameters() const
Definition: std_types.h:841
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
#define Forall_goto_functions(it, functions)
void replace_location(source_locationt &dest, const source_locationt &new_location)
void copy_from(const goto_programt &from, const goto_programt &to)
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
A removal of a local variable.
Definition: std_code.h:234
#define Forall_operands(it, expr)
Definition: expr.h:23
mstreamt & error()
Definition: message.h:223
source_locationt & add_source_location()
Definition: expr.h:147
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:73
mstreamt & progress()
Definition: message.h:248
void destructive_insert(const_targett target, goto_program_templatet< codeT, guardT > &p)
Inserts the given program at the given location.
Expression to hold a symbol (variable)
Definition: std_expr.h:82
const char * c_str() const
Definition: dstring.h:72
void destructive_append(goto_program_templatet< codeT, guardT > &p)
Appends the given program, which is destroyed.
json_objectt & make_object()
Definition: json.h:234
A statement in a programming language.
Definition: std_code.h:19
const irep_idt & get_comment() const
void goto_inline_nontransitive(const irep_idt identifier, goto_functiont &goto_function, const inline_mapt &inline_map, const bool force_full)
goto_functionst::goto_functiont goto_functiont
Base Type Computation.
const typet & subtype() const
Definition: type.h:31
Program Transformation.
#define forall_goto_functions(it, functions)
const irep_idt & get_property_id() const
static bool is_call(goto_programt::const_targett target)
operandst & operands()
Definition: expr.h:70
std::ostream & output_instruction(const class namespacet &ns, const irep_idt &identifier, std::ostream &out, instructionst::const_iterator it) const
See below.
const irep_idt & get_property_class() const
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:68
const irep_idt & get_identifier() const
Definition: std_types.h:782
bool empty() const
Definition: dstring.h:61
void make_typecast(const typet &_type)
Definition: expr.cpp:90
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
void output_inline_map(std::ostream &out, const inline_mapt &inline_map)
Assignment.
Definition: std_code.h:144
void reserve_operands(operandst::size_type n)
Definition: expr.h:108
void insert_function_nobody(goto_programt &dest, const exprt &lhs, goto_programt::targett target, const symbol_exprt &function, const exprt::operandst &arguments)
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:700