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