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