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/base_type.h>
21 #include <util/cprover_prefix.h>
22 #include <util/expr_util.h>
23 #include <util/invariant.h>
24 #include <util/prefix.h>
25 #include <util/std_code.h>
26 #include <util/std_expr.h>
27 
28 #include <langapi/language_util.h>
29 
30 #include "remove_skip.h"
31 #include "goto_inline.h"
32 
34  const goto_programt::targett target,
35  const irep_idt &function_name, // name of called function
36  const code_typet &code_type, // type of called function
37  const exprt::operandst &arguments, // arguments of call
38  goto_programt &dest)
39 {
40  PRECONDITION(target->is_function_call());
41  PRECONDITION(dest.empty());
42 
43  const source_locationt &source_location=target->source_location;
44 
45  // iterates over the operands
46  exprt::operandst::const_iterator it1=arguments.begin();
47 
48  const code_typet::parameterst &parameter_types=
49  code_type.parameters();
50 
51  // iterates over the types of the parameters
52  for(const auto &parameter : parameter_types)
53  {
54  // this is the type the n-th argument should be
55  const typet &par_type=ns.follow(parameter.type());
56 
57  const irep_idt &identifier=parameter.get_identifier();
58 
59  if(identifier.empty())
60  {
61  error().source_location=source_location;
62  error() << "no identifier for function parameter" << eom;
63  throw 0;
64  }
65 
66  {
67  const symbolt &symbol=ns.lookup(identifier);
68 
70  decl->make_decl();
71  decl->code=code_declt(symbol.symbol_expr());
72  decl->code.add_source_location()=source_location;
73  decl->source_location=source_location;
74  decl->function=adjust_function?target->function:function_name;
75  }
76 
77  // this is the actual parameter
78  exprt actual;
79 
80  // if you run out of actual arguments there was a mismatch
81  if(it1==arguments.end())
82  {
83  warning().source_location=source_location;
84  warning() << "call to `" << function_name << "': "
85  << "not enough arguments, "
86  << "inserting non-deterministic value" << eom;
87 
88  actual=side_effect_expr_nondett(par_type);
89  }
90  else
91  actual=*it1;
92 
93  // nil means "don't assign"
94  if(actual.is_nil())
95  {
96  }
97  else
98  {
99  // it should be the same exact type as the parameter,
100  // subject to some exceptions
101  if(!base_type_eq(par_type, actual.type(), ns))
102  {
103  const typet &f_partype=ns.follow(par_type);
104  const typet &f_acttype=ns.follow(actual.type());
105 
106  // we are willing to do some conversion
107  if((f_partype.id()==ID_pointer &&
108  f_acttype.id()==ID_pointer) ||
109  (f_partype.id()==ID_pointer &&
110  f_acttype.id()==ID_array &&
111  f_partype.subtype()==f_acttype.subtype()))
112  {
113  actual.make_typecast(par_type);
114  }
115  else if((f_partype.id()==ID_signedbv ||
116  f_partype.id()==ID_unsignedbv ||
117  f_partype.id()==ID_bool) &&
118  (f_acttype.id()==ID_signedbv ||
119  f_acttype.id()==ID_unsignedbv ||
120  f_acttype.id()==ID_bool))
121  {
122  actual.make_typecast(par_type);
123  }
124  else
125  {
127 
128  error() << "function call: argument `" << identifier
129  << "' type mismatch: argument is `"
130  // << from_type(ns, identifier, actual.type())
131  << actual.type().pretty()
132  << "', parameter is `"
133  << from_type(ns, identifier, par_type)
134  << "'" << eom;
135  throw 0;
136  }
137  }
138 
139  // adds an assignment of the actual parameter to the formal parameter
140  code_assignt assignment(symbol_exprt(identifier, par_type), actual);
141  assignment.add_source_location()=source_location;
142 
143  dest.add_instruction(ASSIGN);
144  dest.instructions.back().source_location=source_location;
145  dest.instructions.back().code.swap(assignment);
146  dest.instructions.back().function=
147  adjust_function?target->function:function_name;
148  }
149 
150  if(it1!=arguments.end())
151  ++it1;
152  }
153 
154  if(it1!=arguments.end())
155  {
156  // too many arguments -- we just ignore that, no harm done
157  }
158 }
159 
161  const goto_programt::targett target,
162  const irep_idt &function_name, // name of called function
163  const code_typet &code_type, // type of called function
164  goto_programt &dest)
165 {
166  PRECONDITION(target->is_function_call());
167  PRECONDITION(dest.empty());
168 
169  const source_locationt &source_location=target->source_location;
170 
171  const code_typet::parameterst &parameter_types=
172  code_type.parameters();
173 
174  // iterates over the types of the parameters
175  for(const auto &parameter : parameter_types)
176  {
177  const irep_idt &identifier=parameter.get_identifier();
178 
179  if(identifier.empty())
180  {
181  error().source_location=source_location;
182  error() << "no identifier for function parameter" << eom;
183  throw 0;
184  }
185 
186  {
187  const symbolt &symbol=ns.lookup(identifier);
188 
190  dead->make_dead();
191  dead->code=code_deadt(symbol.symbol_expr());
192  dead->code.add_source_location()=source_location;
193  dead->source_location=source_location;
194  dead->function=adjust_function?target->function:function_name;
195  }
196  }
197 }
198 
200  goto_programt &dest, // inlining this
201  const exprt &lhs) // lhs in caller
202 {
203  for(goto_programt::instructionst::iterator
204  it=dest.instructions.begin();
205  it!=dest.instructions.end();
206  it++)
207  {
208  if(it->is_return())
209  {
210  if(lhs.is_not_nil())
211  {
212  if(it->code.operands().size()!=1)
213  {
214  warning().source_location=it->code.find_source_location();
215  warning() << "return expects one operand!\n"
216  << it->code.pretty() << eom;
217  continue;
218  }
219 
220  code_assignt code_assign(lhs, it->code.op0());
221 
222  // this may happen if the declared return type at the call site
223  // differs from the defined return type
224  if(code_assign.lhs().type()!=
225  code_assign.rhs().type())
226  code_assign.rhs().make_typecast(code_assign.lhs().type());
227 
228  it->code=code_assign;
229  it->type=ASSIGN;
230 
231  it++;
232  }
233  else if(!it->code.operands().empty())
234  {
235  it->code=code_expressiont(it->code.op0());
236  it->type=OTHER;
237  it++;
238  }
239  }
240  }
241 }
242 
244  source_locationt &dest,
245  const source_locationt &new_location)
246 {
247  // we copy, and then adjust for property_id, property_class
248  // and comment, if necessary
249 
251  irep_idt property_class=dest.get_property_class();
252  irep_idt property_id=dest.get_property_id();
253 
254  dest=new_location;
255 
256  if(!comment.empty())
257  dest.set_comment(comment);
258 
259  if(!property_class.empty())
260  dest.set_property_class(property_class);
261 
262  if(!property_id.empty())
263  dest.set_property_id(property_id);
264 }
265 
267  exprt &dest,
268  const source_locationt &new_location)
269 {
270  Forall_operands(it, dest)
271  replace_location(*it, new_location);
272 
273  if(dest.find(ID_C_source_location).is_not_nil())
274  replace_location(dest.add_source_location(), new_location);
275 }
276 
278  const goto_functiont &goto_function,
279  goto_programt &dest,
280  goto_programt::targett target,
281  const exprt &lhs,
282  const symbol_exprt &function,
283  const exprt::operandst &arguments)
284 {
285  PRECONDITION(target->is_function_call());
286  PRECONDITION(!dest.empty());
287  PRECONDITION(goto_function.body_available());
288 
289  const irep_idt identifier=function.get_identifier();
290 
291  goto_programt body;
292  body.copy_from(goto_function.body);
293  inline_log.copy_from(goto_function.body, body);
294 
295  goto_programt::instructiont &end=body.instructions.back();
297  end.is_end_function(),
298  "final instruction of a function must be an END_FUNCTION");
299  end.type=LOCATION;
300 
301  if(adjust_function)
302  for(auto &instruction : body.instructions)
303  instruction.function=target->function;
304 
305  replace_return(body, lhs);
306 
307  goto_programt tmp1;
309  target,
310  identifier,
311  goto_function.type,
312  arguments,
313  tmp1);
314 
315  goto_programt tmp2;
316  parameter_destruction(target, identifier, goto_function.type, tmp2);
317 
318  goto_programt tmp;
319  tmp.destructive_append(tmp1); // par assignment
320  tmp.destructive_append(body); // body
321  tmp.destructive_append(tmp2); // par destruction
322 
324  t_it=goto_function.body.instructions.begin();
325  unsigned begin_location_number=t_it->location_number;
326  t_it=--goto_function.body.instructions.end();
328  t_it->is_end_function(),
329  "final instruction of a function must be an END_FUNCTION");
330  unsigned end_location_number=t_it->location_number;
331 
332  unsigned call_location_number=target->location_number;
333 
335  tmp,
336  begin_location_number,
337  end_location_number,
338  call_location_number,
339  identifier);
340 
341 #if 0
342  if(goto_function.is_hidden())
343  {
344  source_locationt new_source_location=
345  function.find_source_location();
346 
347  if(new_source_location.is_not_nil())
348  {
349  new_source_location.set_hide();
350 
352  {
353  if(it->function==identifier)
354  {
355  // don't hide assignment to lhs
356  if(it->is_assign() && to_code_assign(it->code).lhs()==lhs)
357  {
358  }
359  else
360  {
361  replace_location(it->source_location, new_source_location);
362  replace_location(it->guard, new_source_location);
363  replace_location(it->code, new_source_location);
364  }
365 
366  it->function=target->function;
367  }
368  }
369  }
370  }
371 #endif
372 
373  // kill call
374  target->type=LOCATION;
375  target->code.clear();
376  target++;
377 
378  dest.destructive_insert(target, tmp);
379 }
380 
382  goto_programt &dest,
383  const inline_mapt &inline_map,
384  const bool transitive,
385  const bool force_full,
386  goto_programt::targett target)
387 {
388  PRECONDITION(target->is_function_call());
389  PRECONDITION(!dest.empty());
390  PRECONDITION(!transitive || inline_map.empty());
391 
392 #ifdef DEBUG
393  std::cout << "Expanding call:\n";
394  dest.output_instruction(ns, "", std::cout, *target);
395 #endif
396 
397  exprt lhs;
398  exprt function_expr;
399  exprt::operandst arguments;
400 
401  get_call(target, lhs, function_expr, arguments);
402 
403  if(function_expr.id()!=ID_symbol)
404  return;
405 
406  const symbol_exprt &function=to_symbol_expr(function_expr);
407 
408  const irep_idt identifier=function.get_identifier();
409 
410  if(is_ignored(identifier))
411  return;
412 
413  // see if we are already expanding it
414  if(recursion_set.find(identifier)!=recursion_set.end())
415  {
416  // it's recursive.
417  // Uh. Buh. Give up.
418  warning().source_location=function.find_source_location();
419  warning() << "recursion is ignored on call to `" << identifier << "'"
420  << eom;
421 
422  if(force_full)
423  target->make_skip();
424 
425  return;
426  }
427 
428  goto_functionst::function_mapt::iterator f_it=
429  goto_functions.function_map.find(identifier);
430 
431  if(f_it==goto_functions.function_map.end())
432  {
433  warning().source_location=function.find_source_location();
434  warning() << "missing function `" << identifier << "' is ignored" << eom;
435 
436  if(force_full)
437  target->make_skip();
438 
439  return;
440  }
441 
442  // function to inline
443  goto_functiont &goto_function=f_it->second;
444 
445  if(goto_function.body_available())
446  {
447  if(transitive)
448  {
449  const goto_functiont &cached=
451  identifier,
452  goto_function,
453  force_full);
454 
455  // insert 'cached' into 'dest' at 'target'
457  cached,
458  dest,
459  target,
460  lhs,
461  function,
462  arguments);
463 
464  progress() << "Inserting " << identifier << " into caller" << eom;
465  progress() << "Number of instructions: "
466  << cached.body.instructions.size() << eom;
467 
468  if(!caching)
469  {
470  progress() << "Removing " << identifier << " from cache" << eom;
471  progress() << "Number of instructions: "
472  << cached.body.instructions.size() << eom;
473 
474  inline_log.cleanup(cached.body);
475  cache.erase(identifier);
476  }
477  }
478  else
479  {
480  // inline non-transitively
482  identifier,
483  goto_function,
484  inline_map,
485  force_full);
486 
487  // insert 'goto_function' into 'dest' at 'target'
489  goto_function,
490  dest,
491  target,
492  lhs,
493  function,
494  arguments);
495  }
496  }
497  else // no body available
498  {
499  const irep_idt identifier = function.get_identifier();
500 
501  if(no_body_set.insert(identifier).second) // newly inserted
502  {
503  warning().source_location = function.find_source_location();
504  warning() << "no body for function `" << identifier << "'" << eom;
505  }
506  }
507 }
508 
511  exprt &lhs,
512  exprt &function,
513  exprt::operandst &arguments)
514 {
515  PRECONDITION(it->is_function_call());
516 
517  const code_function_callt &call=to_code_function_call(it->code);
518 
519  lhs=call.lhs();
520  function=call.function();
521  arguments=call.arguments();
522 }
523 
525  const inline_mapt &inline_map,
526  const bool force_full)
527 {
528  PRECONDITION(check_inline_map(inline_map));
529 
531  {
532  const irep_idt identifier=f_it->first;
533  DATA_INVARIANT(!identifier.empty(), "function name must not be empty");
534  goto_functiont &goto_function=f_it->second;
535 
536  if(!goto_function.body_available())
537  continue;
538 
539  goto_inline(identifier, goto_function, inline_map, force_full);
540  }
541 }
542 
544  const irep_idt identifier,
545  goto_functiont &goto_function,
546  const inline_mapt &inline_map,
547  const bool force_full)
548 {
549  recursion_set.clear();
550 
552  identifier,
553  goto_function,
554  inline_map,
555  force_full);
556 }
557 
559  const irep_idt identifier,
560  goto_functiont &goto_function,
561  const inline_mapt &inline_map,
562  const bool force_full)
563 {
564  PRECONDITION(goto_function.body_available());
565 
566  finished_sett::const_iterator f_it=finished_set.find(identifier);
567 
568  if(f_it!=finished_set.end())
569  return;
570 
571  PRECONDITION(check_inline_map(identifier, inline_map));
572 
573  goto_programt &goto_program=goto_function.body;
574 
575  const inline_mapt::const_iterator im_it=inline_map.find(identifier);
576 
577  if(im_it==inline_map.end())
578  return;
579 
580  const call_listt &call_list=im_it->second;
581 
582  if(call_list.empty())
583  return;
584 
585  recursion_set.insert(identifier);
586 
587  for(const auto &call : call_list)
588  {
589  const bool transitive=call.second;
590 
591  const inline_mapt &new_inline_map=
592  transitive?inline_mapt():inline_map;
593 
595  goto_program,
596  new_inline_map,
597  transitive,
598  force_full,
599  call.first);
600  }
601 
602  recursion_set.erase(identifier);
603 
604  // remove_skip(goto_program);
605  // goto_program.update(); // does not change loop ids
606 
607  finished_set.insert(identifier);
608 }
609 
611  const irep_idt identifier,
612  const goto_functiont &goto_function,
613  const bool force_full)
614 {
615  PRECONDITION(goto_function.body_available());
616 
617  cachet::const_iterator c_it=cache.find(identifier);
618 
619  if(c_it!=cache.end())
620  {
621  const goto_functiont &cached=c_it->second;
623  cached.body_available(),
624  "body of cached functions must be available");
625  return cached;
626  }
627 
628  goto_functiont &cached=cache[identifier];
629  INVARIANT(
630  cached.body.empty(),
631  "body of new function in cache must be empty");
632 
633  progress() << "Creating copy of " << identifier << eom;
634  progress() << "Number of instructions: "
635  << goto_function.body.instructions.size() << eom;
636 
637  cached.copy_from(goto_function); // location numbers not changed
638  inline_log.copy_from(goto_function.body, cached.body);
639 
641 
642  goto_programt::targetst call_list;
643 
645  {
646  if(i_it->is_function_call())
647  call_list.push_back(i_it);
648  }
649 
650  if(call_list.empty())
651  return cached;
652 
653  recursion_set.insert(identifier);
654 
655  for(const auto &call : call_list)
656  {
658  goto_program,
659  inline_mapt(),
660  true,
661  force_full,
662  call);
663  }
664 
665  recursion_set.erase(identifier);
666 
667  // remove_skip(goto_program);
668  // goto_program.update(); // does not change loop ids
669 
670  return cached;
671 }
672 
673 bool goto_inlinet::is_ignored(const irep_idt id) const
674 {
675  return
676  id=="__CPROVER_cleanup" ||
677  id=="__CPROVER_set_must" ||
678  id=="__CPROVER_set_may" ||
679  id=="__CPROVER_clear_must" ||
680  id=="__CPROVER_clear_may" ||
681  id=="__CPROVER_cover";
682 }
683 
685  const irep_idt identifier,
686  const inline_mapt &inline_map) const
687 {
688  goto_functionst::function_mapt::const_iterator f_it=
689  goto_functions.function_map.find(identifier);
690 
692 
693  inline_mapt::const_iterator im_it=inline_map.find(identifier);
694 
695  if(im_it==inline_map.end())
696  return true;
697 
698  const call_listt &call_list=im_it->second;
699 
700  if(call_list.empty())
701  return true;
702 
703  int ln=-1;
704 
705  for(const auto &call : call_list)
706  {
707  const goto_programt::const_targett target=call.first;
708 
709  #if 0
710  // might not hold if call was previously inlined
711  if(target->function!=identifier)
712  return false;
713  #endif
714 
715  // location numbers increasing
716  if(static_cast<int>(target->location_number)<=ln)
717  return false;
718 
719  if(!target->is_function_call())
720  return false;
721 
722  ln=target->location_number;
723  }
724 
725  return true;
726 }
727 
728 bool goto_inlinet::check_inline_map(const inline_mapt &inline_map) const
729 {
731  {
732  if(!check_inline_map(f_it->first, inline_map))
733  return false;
734  }
735 
736  return true;
737 }
738 
740  std::ostream &out,
741  const inline_mapt &inline_map)
742 {
743  PRECONDITION(check_inline_map(inline_map));
744 
745  for(const auto &it : inline_map)
746  {
747  const irep_idt &id=it.first;
748  const call_listt &call_list=it.second;
749 
750  out << "Function: " << id << "\n";
751 
752  goto_functionst::function_mapt::const_iterator f_it=
753  goto_functions.function_map.find(id);
754 
755  std::string call="-";
756 
757  if(f_it!=goto_functions.function_map.end() &&
758  !call_list.empty())
759  {
760  const goto_functiont &goto_function=f_it->second;
761  PRECONDITION(goto_function.body_available());
762 
763  const goto_programt &goto_program=goto_function.body;
764 
765  for(const auto &call : call_list)
766  {
767  const goto_programt::const_targett target=call.first;
768  bool transitive=call.second;
769 
770  out << " Call:\n";
771  goto_program.output_instruction(ns, "", out, *target);
772  out << " Transitive: " << transitive << "\n";
773  }
774  }
775  else
776  {
777  out << " -\n";
778  }
779  }
780 }
781 
782 void goto_inlinet::output_cache(std::ostream &out) const
783 {
784  for(auto it=cache.begin(); it!=cache.end(); it++)
785  {
786  if(it!=cache.begin())
787  out << ", ";
788 
789  out << it->first << "\n";
790  }
791 }
792 
793 // remove segment that refer to the given goto program
796 {
798  log_map.erase(it);
799 }
800 
802  const goto_functionst::function_mapt &function_map)
803 {
804  for(const auto &it : function_map)
805  {
806  const goto_functiont &goto_function=it.second;
807 
808  if(!goto_function.body_available())
809  continue;
810 
811  cleanup(goto_function.body);
812  }
813 }
814 
817  const unsigned begin_location_number,
818  const unsigned end_location_number,
819  const unsigned call_location_number,
820  const irep_idt function)
821 {
823  PRECONDITION(!function.empty());
824  PRECONDITION(end_location_number>=begin_location_number);
825 
827  PRECONDITION(log_map.find(start)==log_map.end());
828 
830  end--;
831 
833  info.begin_location_number=begin_location_number;
834  info.end_location_number=end_location_number;
835  info.call_location_number=call_location_number;
836  info.function=function;
837  info.end=end;
838 
839  log_map[start]=info;
840 }
841 
843  const goto_programt &from,
844  const goto_programt &to)
845 {
846  PRECONDITION(from.instructions.size()==to.instructions.size());
847 
850 
851  for(; it1!=from.instructions.end(); it1++, it2++)
852  {
853  assert(it2!=to.instructions.end());
854  assert(it1->location_number==it2->location_number);
855 
856  log_mapt::const_iterator l_it=log_map.find(it1);
857  if(l_it!=log_map.end()) // a segment starts here
858  {
859  // as 'to' is a fresh copy
860  assert(log_map.find(it2)==log_map.end());
861 
862  goto_inline_log_infot info=l_it->second;
864 
865  // find end of new
866  goto_programt::const_targett tmp_it=it1;
867  goto_programt::const_targett new_end=it2;
868  while(tmp_it!=end)
869  {
870  new_end++;
871  tmp_it++;
872  }
873 
874  info.end=new_end;
875 
876  log_map[it2]=info;
877  }
878  }
879 }
880 
881 // call after goto_functions.update()!
883 {
884  json_objectt json_result;
885  json_arrayt &json_inlined=json_result["inlined"].make_array();
886 
887  for(const auto &it : log_map)
888  {
889  json_objectt &object=json_inlined.push_back().make_object();
890 
891  goto_programt::const_targett start=it.first;
892  const goto_inline_log_infot &info=it.second;
894 
895  assert(start->location_number<=end->location_number);
896 
897  object["call"]=json_numbert(std::to_string(info.call_location_number));
898  object["function"]=json_stringt(info.function.c_str());
899 
900  json_arrayt &json_orig=object["originalSegment"].make_array();
902  info.begin_location_number));
903  json_orig.push_back()=json_numbert(std::to_string(
904  info.end_location_number));
905 
906  json_arrayt &json_new=object["inlinedSegment"].make_array();
907  json_new.push_back()=json_numbert(std::to_string(start->location_number));
908  json_new.push_back()=json_numbert(std::to_string(end->location_number));
909  }
910 
911  return json_result;
912 }
The type of an expression.
Definition: type.h:22
std::list< callt > call_listt
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)
Base type of functions.
Definition: std_types.h:764
bool is_nil() const
Definition: irep.h:102
bool is_not_nil() const
Definition: irep.h:103
std::list< targett > targetst
Definition: goto_program.h:399
goto_inline_logt inline_log
exprt & op0()
Definition: expr.h:72
void set_property_class(const irep_idt &property_class)
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
mstreamt & progress() const
Definition: message.h:327
std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:107
goto_program_instruction_typet type
What kind of instruction?
Definition: goto_program.h:185
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Definition: base_type.cpp:326
bool is_ignored(const irep_idt id) const
Deprecated expression utility functions.
void set_comment(const irep_idt &comment)
goto_programt body
Definition: goto_function.h:23
Definition: json.h:23
void cleanup(const goto_programt &goto_program)
std::vector< parametert > parameterst
Definition: std_types.h:767
const bool caching
void destructive_append(goto_programt &p)
Appends the given program, which is destroyed.
Definition: goto_program.h:486
function_mapt function_map
typet & type()
Definition: expr.h:56
void replace_return(goto_programt &body, const exprt &lhs)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
An expression statement.
Definition: std_code.h:1188
json_arrayt & make_array()
Definition: json.h:284
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:205
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)
mstreamt & warning() const
Definition: message.h:307
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:173
jsont & push_back(const jsont &json)
Definition: json.h:163
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:239
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:208
std::map< irep_idt, call_listt > inline_mapt
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:111
instructionst::iterator targett
Definition: goto_program.h:397
A declaration of a local variable.
Definition: std_code.h:253
exprt & rhs()
Definition: std_code.h:213
const source_locationt & find_source_location() const
Definition: expr.cpp:246
recursion_sett recursion_set
source_locationt source_location
Definition: message.h:214
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:403
API to expression classes.
instructionst::const_iterator const_targett
Definition: goto_program.h:398
mstreamt & error() const
Definition: message.h:302
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)
#define PRECONDITION(CONDITION)
Definition: invariant.h:230
A side effect that returns a non-deterministically chosen value.
Definition: std_code.h:1301
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program at the given location.
Definition: goto_program.h:495
A function call.
Definition: std_code.h:828
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
bool check_inline_map(const inline_mapt &inline_map) const
std::map< irep_idt, goto_functiont > function_mapt
void copy_from(const goto_functiont &other)
Definition: goto_function.h:75
code_typet type
Definition: goto_function.h:24
const typet & follow(const typet &) const
Definition: namespace.cpp:55
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)
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)
static void get_call(goto_programt::const_targett target, exprt &lhs, exprt &function, exprt::operandst &arguments)
std::vector< exprt > operandst
Definition: expr.h:45
const bool adjust_function
bool is_hidden() const
Definition: goto_function.h:39
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
goto_functionst & goto_functions
const namespacet & ns
finished_sett finished_set
no_body_sett no_body_set
void output_cache(std::ostream &out) const
bool body_available() const
Definition: goto_function.h:29
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &it) const
Output a single instruction.
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)
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:505
Base class for all expressions.
Definition: expr.h:42
const parameterst & parameters() const
Definition: std_types.h:905
std::string to_string(const string_constraintt &expr)
Used for debug printing.
#define Forall_goto_functions(it, functions)
bool empty() const
Is the program empty?
Definition: goto_program.h:590
void replace_location(source_locationt &dest, const source_locationt &new_location)
void copy_from(const goto_programt &from, const goto_programt &to)
A removal of a local variable.
Definition: std_code.h:305
#define Forall_operands(it, expr)
Definition: expr.h:23
goto_programt & goto_program
Definition: cover.cpp:63
source_locationt & add_source_location()
Definition: expr.h:130
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:740
Expression to hold a symbol (variable)
Definition: std_expr.h:90
const char * c_str() const
Definition: dstring.h:72
json_objectt & make_object()
Definition: json.h:290
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:33
Program Transformation.
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:257
#define forall_goto_functions(it, functions)
const irep_idt & get_property_id() const
const irep_idt & get_property_class() const
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:735
bool empty() const
Definition: dstring.h:61
void make_typecast(const typet &_type)
Definition: expr.cpp:84
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
void output_inline_map(std::ostream &out, const inline_mapt &inline_map)
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:130
Assignment.
Definition: std_code.h:195
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:879