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/cprover_prefix.h>
19 #include <util/invariant.h>
20 #include <util/std_code.h>
21 #include <util/symbol.h>
22 
24  const goto_programt::targett target,
25  const irep_idt &function_name, // name of called function
26  const goto_functiont::parameter_identifierst &parameter_identifiers,
27  const exprt::operandst &arguments, // arguments of call
28  goto_programt &dest)
29 {
30  PRECONDITION(target->is_function_call());
31  PRECONDITION(dest.empty());
32 
33  const source_locationt &source_location=target->source_location;
34 
35  // iterates over the operands
36  exprt::operandst::const_iterator it1=arguments.begin();
37 
38  // iterates over the parameters
39  for(const auto &identifier : parameter_identifiers)
40  {
42  !identifier.empty(),
43  source_location.as_string() + ": no identifier for function parameter");
44 
45  const symbolt &symbol = ns.lookup(identifier);
46 
47  // this is the type the n-th argument should have
48  const typet &parameter_type = symbol.type;
49 
51  dest.add(goto_programt::make_decl(symbol.symbol_expr(), source_location));
52  decl->code_nonconst().add_source_location() = source_location;
53 
54  // this is the actual parameter
55  exprt actual;
56 
57  // if you run out of actual arguments there was a mismatch
58  if(it1==arguments.end())
59  {
60  log.warning().source_location = source_location;
61  log.warning() << "call to '" << function_name << "': "
62  << "not enough arguments, "
63  << "inserting non-deterministic value" << messaget::eom;
64 
65  actual = side_effect_expr_nondett(parameter_type, source_location);
66  }
67  else
68  actual=*it1;
69 
70  // nil means "don't assign"
71  if(actual.is_nil())
72  {
73  }
74  else
75  {
76  // it should be the same exact type as the parameter,
77  // subject to some exceptions
78  if(parameter_type != actual.type())
79  {
80  const typet &f_partype = parameter_type;
81  const typet &f_acttype = actual.type();
82 
83  // we are willing to do some conversion
84  if((f_partype.id()==ID_pointer &&
85  f_acttype.id()==ID_pointer) ||
86  (f_partype.id()==ID_pointer &&
87  f_acttype.id()==ID_array &&
88  f_partype.subtype()==f_acttype.subtype()))
89  {
90  actual = typecast_exprt(actual, f_partype);
91  }
92  else if((f_partype.id()==ID_signedbv ||
93  f_partype.id()==ID_unsignedbv ||
94  f_partype.id()==ID_bool) &&
95  (f_acttype.id()==ID_signedbv ||
96  f_acttype.id()==ID_unsignedbv ||
97  f_acttype.id()==ID_bool))
98  {
99  actual = typecast_exprt(actual, f_partype);
100  }
101  else
102  {
103  UNREACHABLE;
104  }
105  }
106 
107  // adds an assignment of the actual parameter to the formal parameter
108  code_assignt assignment(symbol_exprt(identifier, parameter_type), actual);
109  assignment.add_source_location()=source_location;
110 
111  dest.add(goto_programt::make_assignment(assignment, source_location));
112  }
113 
114  if(it1!=arguments.end())
115  ++it1;
116  }
117 
118  if(it1!=arguments.end())
119  {
120  // too many arguments -- we just ignore that, no harm done
121  }
122 }
123 
125  const goto_programt::targett target,
126  const goto_functiont::parameter_identifierst &parameter_identifiers,
127  goto_programt &dest)
128 {
129  PRECONDITION(target->is_function_call());
130  PRECONDITION(dest.empty());
131 
132  const source_locationt &source_location=target->source_location;
133 
134  for(const auto &identifier : parameter_identifiers)
135  {
136  INVARIANT(
137  !identifier.empty(),
138  source_location.as_string() + ": no identifier for function parameter");
139 
140  {
141  const symbolt &symbol=ns.lookup(identifier);
142 
143  goto_programt::targett dead = dest.add(
144  goto_programt::make_dead(symbol.symbol_expr(), source_location));
145  dead->code_nonconst().add_source_location() = source_location;
146  }
147  }
148 }
149 
151  goto_programt &dest, // inlining this
152  const exprt &lhs) // lhs in caller
153 {
154  for(goto_programt::instructionst::iterator
155  it=dest.instructions.begin();
156  it!=dest.instructions.end();
157  it++)
158  {
159  if(it->is_set_return_value())
160  {
161  if(lhs.is_not_nil())
162  {
163  // a typecast may be necessary if the declared return type at the call
164  // site differs from the defined return type
165  it->code_nonconst() = code_assignt(
166  lhs,
167  typecast_exprt::conditional_cast(it->return_value(), lhs.type()));
168  it->type=ASSIGN;
169  }
170  else
171  {
172  it->code_nonconst() = code_expressiont(it->return_value());
173  it->type=OTHER;
174  }
175  }
176  }
177 }
178 
180  source_locationt &dest,
181  const source_locationt &new_location)
182 {
183  // we copy, and then adjust for property_id, property_class
184  // and comment, if necessary
185 
187  irep_idt property_class=dest.get_property_class();
188  irep_idt property_id=dest.get_property_id();
189 
190  dest=new_location;
191 
192  if(!comment.empty())
193  dest.set_comment(comment);
194 
195  if(!property_class.empty())
196  dest.set_property_class(property_class);
197 
198  if(!property_id.empty())
199  dest.set_property_id(property_id);
200 }
201 
203  exprt &dest,
204  const source_locationt &new_location)
205 {
206  Forall_operands(it, dest)
207  replace_location(*it, new_location);
208 
209  if(dest.find(ID_C_source_location).is_not_nil())
210  replace_location(dest.add_source_location(), new_location);
211 }
212 
214  const goto_functiont &goto_function,
215  goto_programt &dest,
216  goto_programt::targett target,
217  const exprt &lhs,
218  const symbol_exprt &function,
219  const exprt::operandst &arguments)
220 {
221  PRECONDITION(target->is_function_call());
222  PRECONDITION(!dest.empty());
223  PRECONDITION(goto_function.body_available());
224 
225  const irep_idt identifier=function.get_identifier();
226 
227  goto_programt body;
228  body.copy_from(goto_function.body);
229  inline_log.copy_from(goto_function.body, body);
230 
231  goto_programt::instructiont &end=body.instructions.back();
233  end.is_end_function(),
234  "final instruction of a function must be an END_FUNCTION");
235  end.type=LOCATION;
236 
237  // make sure the inlined function does not introduce hiding
238  if(goto_function.is_hidden())
239  {
240  for(auto &instruction : body.instructions)
241  instruction.labels.remove(CPROVER_PREFIX "HIDE");
242  }
243 
244  replace_return(body, lhs);
245 
246  goto_programt tmp1;
248  target, identifier, goto_function.parameter_identifiers, arguments, tmp1);
249 
250  goto_programt tmp2;
251  parameter_destruction(target, goto_function.parameter_identifiers, tmp2);
252 
253  goto_programt tmp;
254  tmp.destructive_append(tmp1); // par assignment
255  tmp.destructive_append(body); // body
256  tmp.destructive_append(tmp2); // par destruction
257 
259  t_it=goto_function.body.instructions.begin();
260  unsigned begin_location_number=t_it->location_number;
261  t_it=--goto_function.body.instructions.end();
263  t_it->is_end_function(),
264  "final instruction of a function must be an END_FUNCTION");
265  unsigned end_location_number=t_it->location_number;
266 
267  unsigned call_location_number=target->location_number;
268 
270  tmp,
271  begin_location_number,
272  end_location_number,
273  call_location_number,
274  identifier);
275 
276  if(adjust_function)
277  {
278  for(auto &instruction : tmp.instructions)
279  {
280  replace_location(instruction.source_location, target->source_location);
281  replace_location(instruction.code_nonconst(), target->source_location);
282 
283  if(instruction.has_condition())
284  {
285  exprt c = instruction.get_condition();
286  replace_location(c, target->source_location);
287  instruction.set_condition(c);
288  }
289  }
290  }
291 
292  // kill call
293  target->type=LOCATION;
294  target->code_nonconst().clear();
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  dest.output_instruction(ns, irep_idt(), std::cout, *target);
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 irep_idt identifier,
493  goto_functiont &goto_function,
494  const inline_mapt &inline_map,
495  const bool force_full)
496 {
497  PRECONDITION(goto_function.body_available());
498 
499  finished_sett::const_iterator f_it=finished_set.find(identifier);
500 
501  if(f_it!=finished_set.end())
502  return;
503 
504  PRECONDITION(check_inline_map(identifier, inline_map));
505 
506  goto_programt &goto_program=goto_function.body;
507 
508  const inline_mapt::const_iterator im_it=inline_map.find(identifier);
509 
510  if(im_it==inline_map.end())
511  return;
512 
513  const call_listt &call_list=im_it->second;
514 
515  if(call_list.empty())
516  return;
517 
518  recursion_set.insert(identifier);
519 
520  for(const auto &call : call_list)
521  {
522  const bool transitive=call.second;
523 
524  const inline_mapt &new_inline_map=
525  transitive?inline_mapt():inline_map;
526 
528  goto_program,
529  new_inline_map,
530  transitive,
531  force_full,
532  call.first);
533  }
534 
535  recursion_set.erase(identifier);
536 
537  // remove_skip(goto_program);
538  // goto_program.update(); // does not change loop ids
539 
540  finished_set.insert(identifier);
541 }
542 
544  const irep_idt identifier,
545  const goto_functiont &goto_function,
546  const bool force_full)
547 {
548  PRECONDITION(goto_function.body_available());
549 
550  cachet::const_iterator c_it=cache.find(identifier);
551 
552  if(c_it!=cache.end())
553  {
554  const goto_functiont &cached=c_it->second;
556  cached.body_available(),
557  "body of cached functions must be available");
558  return cached;
559  }
560 
561  goto_functiont &cached=cache[identifier];
563  cached.body.empty(), "body of new function in cache must be empty");
564 
565  log.progress() << "Creating copy of " << identifier << messaget::eom;
566  log.progress() << "Number of instructions: "
567  << goto_function.body.instructions.size() << messaget::eom;
568 
569  cached.copy_from(goto_function); // location numbers not changed
570  inline_log.copy_from(goto_function.body, cached.body);
571 
572  goto_programt &goto_program=cached.body;
573 
574  goto_programt::targetst call_list;
575 
576  Forall_goto_program_instructions(i_it, goto_program)
577  {
578  if(i_it->is_function_call())
579  call_list.push_back(i_it);
580  }
581 
582  if(call_list.empty())
583  return cached;
584 
585  recursion_set.insert(identifier);
586 
587  for(const auto &call : call_list)
588  {
590  goto_program,
591  inline_mapt(),
592  true,
593  force_full,
594  call);
595  }
596 
597  recursion_set.erase(identifier);
598 
599  // remove_skip(goto_program);
600  // goto_program.update(); // does not change loop ids
601 
602  return cached;
603 }
604 
605 bool goto_inlinet::is_ignored(const irep_idt id) const
606 {
607  return id == CPROVER_PREFIX "cleanup" || id == CPROVER_PREFIX "set_must" ||
608  id == CPROVER_PREFIX "set_may" || id == CPROVER_PREFIX "clear_must" ||
609  id == CPROVER_PREFIX "clear_may" || id == CPROVER_PREFIX "cover";
610 }
611 
613  const irep_idt identifier,
614  const inline_mapt &inline_map) const
615 {
616  goto_functionst::function_mapt::const_iterator f_it=
617  goto_functions.function_map.find(identifier);
618 
620 
621  inline_mapt::const_iterator im_it=inline_map.find(identifier);
622 
623  if(im_it==inline_map.end())
624  return true;
625 
626  const call_listt &call_list=im_it->second;
627 
628  if(call_list.empty())
629  return true;
630 
632 
633  for(const auto &call : call_list)
634  {
635  const goto_programt::const_targett target=call.first;
636 
637  #if 0
638  // might not hold if call was previously inlined
639  if(target->function!=identifier)
640  return false;
641  #endif
642 
643  // location numbers increasing
644  if(
646  target->location_number <= ln)
647  {
648  return false;
649  }
650 
651  if(!target->is_function_call())
652  return false;
653 
654  ln=target->location_number;
655  }
656 
657  return true;
658 }
659 
660 bool goto_inlinet::check_inline_map(const inline_mapt &inline_map) const
661 {
662  for(const auto &gf_entry : goto_functions.function_map)
663  {
664  if(!check_inline_map(gf_entry.first, inline_map))
665  return false;
666  }
667 
668  return true;
669 }
670 
672  std::ostream &out,
673  const inline_mapt &inline_map)
674 {
675  PRECONDITION(check_inline_map(inline_map));
676 
677  for(const auto &it : inline_map)
678  {
679  const irep_idt &id=it.first;
680  const call_listt &call_list=it.second;
681 
682  out << "Function: " << id << "\n";
683 
684  goto_functionst::function_mapt::const_iterator f_it=
685  goto_functions.function_map.find(id);
686 
687  if(f_it!=goto_functions.function_map.end() &&
688  !call_list.empty())
689  {
690  const goto_functiont &goto_function=f_it->second;
692  goto_function.body_available(),
693  "cannot inline function with empty body");
694 
695  const goto_programt &goto_program=goto_function.body;
696 
697  for(const auto &call : call_list)
698  {
699  const goto_programt::const_targett target=call.first;
700  bool transitive=call.second;
701 
702  out << " Call:\n";
703  goto_program.output_instruction(ns, id, out, *target);
704  out << " Transitive: " << transitive << "\n";
705  }
706  }
707  else
708  {
709  out << " -\n";
710  }
711  }
712 }
713 
714 void goto_inlinet::output_cache(std::ostream &out) const
715 {
716  for(auto it=cache.begin(); it!=cache.end(); it++)
717  {
718  if(it!=cache.begin())
719  out << ", ";
720 
721  out << it->first << "\n";
722  }
723 }
724 
725 // remove segment that refer to the given goto program
727  const goto_programt &goto_program)
728 {
729  forall_goto_program_instructions(it, goto_program)
730  log_map.erase(it);
731 }
732 
734  const goto_functionst::function_mapt &function_map)
735 {
736  for(const auto &it : function_map)
737  {
738  const goto_functiont &goto_function=it.second;
739 
740  if(!goto_function.body_available())
741  continue;
742 
743  cleanup(goto_function.body);
744  }
745 }
746 
748  const goto_programt &goto_program,
749  const unsigned begin_location_number,
750  const unsigned end_location_number,
751  const unsigned call_location_number,
752  const irep_idt function)
753 {
754  PRECONDITION(!goto_program.empty());
755  PRECONDITION(!function.empty());
756  PRECONDITION(end_location_number >= begin_location_number);
757 
758  goto_programt::const_targett start=goto_program.instructions.begin();
759  INVARIANT(
760  log_map.find(start) == log_map.end(),
761  "inline function should be registered once in map of inline functions");
762 
763  goto_programt::const_targett end=goto_program.instructions.end();
764  end--;
765 
767  info.begin_location_number=begin_location_number;
768  info.end_location_number=end_location_number;
769  info.call_location_number=call_location_number;
770  info.function=function;
771  info.end=end;
772 
773  log_map[start]=info;
774 }
775 
777  const goto_programt &from,
778  const goto_programt &to)
779 {
780  PRECONDITION(from.instructions.size() == to.instructions.size());
781 
784 
785  for(; it1!=from.instructions.end(); it1++, it2++)
786  {
788  it2 != to.instructions.end(),
789  "'to' target function is not allowed to be empty");
791  it1->location_number == it2->location_number,
792  "both functions' instruction should point to the same source");
793 
794  log_mapt::const_iterator l_it=log_map.find(it1);
795  if(l_it!=log_map.end()) // a segment starts here
796  {
797  // as 'to' is a fresh copy
799  log_map.find(it2) == log_map.end(),
800  "'to' target is not expected to be in the log_map");
801 
802  goto_inline_log_infot info=l_it->second;
804 
805  // find end of new
806  goto_programt::const_targett tmp_it=it1;
807  goto_programt::const_targett new_end=it2;
808  while(tmp_it!=end)
809  {
810  new_end++;
811  tmp_it++;
812  }
813 
814  info.end=new_end;
815 
816  log_map[it2]=info;
817  }
818  }
819 }
820 
821 // call after goto_functions.update()!
823 {
824  json_objectt json_result;
825  json_arrayt &json_inlined=json_result["inlined"].make_array();
826 
827  for(const auto &it : log_map)
828  {
829  goto_programt::const_targett start=it.first;
830  const goto_inline_log_infot &info=it.second;
832 
833  PRECONDITION(start->location_number <= end->location_number);
834 
835  json_arrayt json_orig{
838  json_arrayt json_new{json_numbert(std::to_string(start->location_number)),
839  json_numbert(std::to_string(end->location_number))};
840 
841  json_objectt object{
843  {"function", json_stringt(info.function.c_str())},
844  {"originalSegment", std::move(json_orig)},
845  {"inlinedSegment", std::move(json_new)}};
846 
847  json_inlined.push_back(std::move(object));
848  }
849 
850  return std::move(json_result);
851 }
A codet representing an assignment in the program.
Definition: std_code.h:293
codet representation of an expression statement.
Definition: std_code.h:1840
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
const char * c_str() const
Definition: dstring.h:99
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
source_locationt & add_source_location()
Definition: expr.h:235
const source_locationt & source_location() const
Definition: expr.h:230
typet & type()
Return the type of the expression.
Definition: expr.h:82
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:178
goto_program_instruction_typet type
What kind of instruction?
Definition: goto_program.h:434
static const unsigned nil_target
Uniquely identify an invalid target or location.
Definition: goto_program.h:588
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:71
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:652
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:985
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
Definition: goto_program.h:744
instructionst::iterator targett
Definition: goto_program.h:646
instructionst::const_iterator const_targett
Definition: goto_program.h:647
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:736
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:753
bool empty() const
Is the program empty?
Definition: goto_program.h:826
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:978
std::list< targett > targetst
Definition: goto_program.h:648
const irept & find(const irep_namet &name) const
Definition: irep.cpp:106
bool is_not_nil() const
Definition: irep.h:391
const irep_idt & id() const
Definition: irep.h:407
bool is_nil() const
Definition: irep.h:387
jsont & push_back(const jsont &json)
Definition: json.h:212
Definition: json.h:27
json_arrayt & make_array()
Definition: json.h:420
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:138
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1966
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:80
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:1866
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1874
The type of an expression, extends irept.
Definition: type.h:28
const typet & subtype() const
Definition: type.h:47
#define CPROVER_PREFIX
#define Forall_operands(it, expr)
Definition: expr.h:25
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)
@ ASSIGN
Definition: goto_program.h:44
@ OTHER
Definition: goto_program.h:35
dstringt irep_idt
Definition: irep.h:37
static std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:109
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
#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:189
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Symbol table entry.