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