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 }
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:1172
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
goto_inlinet::goto_inline_logt::goto_inline_log_infot::begin_location_number
unsigned begin_location_number
Definition: goto_inline_class.h:92
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
goto_functiont::body
goto_programt body
Definition: goto_function.h:29
json_numbert
Definition: json.h:291
source_locationt::get_comment
const irep_idt & get_comment() const
Definition: source_location.h:71
source_locationt::get_property_id
const irep_idt & get_property_id() const
Definition: source_location.h:61
goto_inlinet::log
messaget log
Definition: goto_inline_class.h:125
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1789
dstringt::c_str
const char * c_str() const
Definition: dstring.h:99
source_locationt::get_property_class
const irep_idt & get_property_class() const
Definition: source_location.h:66
typet::subtype
const typet & subtype() const
Definition: type.h:47
source_locationt::as_string
std::string as_string() const
Definition: source_location.h:26
source_locationt::set_comment
void set_comment(const irep_idt &comment)
Definition: source_location.h:141
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:25
goto_programt::make_dead
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:898
goto_inlinet::insert_function_body
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)
Definition: goto_inline_class.cpp:223
goto_inline.h
Function Inlining.
typet
The type of an expression, extends irept.
Definition: type.h:28
goto_inlinet::call_listt
std::list< callt > call_listt
Definition: goto_inline_class.h:45
goto_inlinet::goto_inline_logt::add_segment
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)
Definition: goto_inline_class.cpp:745
goto_inlinet::goto_inline_logt::goto_inline_log_infot::call_location_number
unsigned call_location_number
Definition: goto_inline_class.h:94
goto_inlinet::replace_return
void replace_return(goto_programt &body, const exprt &lhs)
Definition: goto_inline_class.cpp:157
goto_inlinet::get_call
static void get_call(goto_programt::const_targett target, exprt &lhs, exprt &function, exprt::operandst &arguments)
Definition: goto_inline_class.cpp:440
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
goto_programt::instructiont::type
goto_program_instruction_typet type
What kind of instruction?
Definition: goto_program.h:337
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
prefix.h
goto_programt::copy_from
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
Definition: goto_program.cpp:625
invariant.h
goto_programt::add
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:657
source_locationt::set_property_id
void set_property_id(const irep_idt &property_id)
Definition: source_location.h:131
goto_programt::empty
bool empty() const
Is the program empty?
Definition: goto_program.h:733
exprt
Base class for all expressions.
Definition: expr.h:54
goto_inlinet::goto_inline
void goto_inline(const irep_idt identifier, goto_functiont &goto_function, const inline_mapt &inline_map, const bool force_full=false)
Definition: goto_inline_class.cpp:474
irep_idt
dstringt irep_idt
Definition: irep.h:37
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
messaget::eom
static eomt eom
Definition: message.h:297
goto_inlinet::goto_inline_logt::cleanup
void cleanup(const goto_programt &goto_program)
Definition: goto_inline_class.cpp:724
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:81
goto_programt::make_decl
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:891
goto_inlinet::goto_inline_logt::goto_inline_log_infot::end_location_number
unsigned end_location_number
Definition: goto_inline_class.h:93
jsont
Definition: json.h:27
code_function_callt::lhs
exprt & lhs()
Definition: std_code.h:1240
goto_programt::make_assignment
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
Definition: goto_program.h:995
json_arrayt
Definition: json.h:165
json_objectt
Definition: json.h:300
goto_inlinet::adjust_function
const bool adjust_function
Definition: goto_inline_class.h:129
goto_inlinet::no_body_set
no_body_sett no_body_set
Definition: goto_inline_class.h:202
goto_inlinet::goto_inline_nontransitive
void goto_inline_nontransitive(const irep_idt identifier, goto_functiont &goto_function, const inline_mapt &inline_map, const bool force_full)
Definition: goto_inline_class.cpp:489
goto_programt::targetst
std::list< targett > targetst
Definition: goto_program.h:552
goto_inlinet::recursion_set
recursion_sett recursion_set
Definition: goto_inline_class.h:199
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1215
goto_functiont::body_available
bool body_available() const
Definition: goto_function.h:38
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:391
goto_inline_class.h
goto_functionst::function_mapt
std::map< irep_idt, goto_functiont > function_mapt
Definition: goto_functions.h:26
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
goto_programt::destructive_insert
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
Definition: goto_program.h:648
goto_programt::output_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.
Definition: goto_program.cpp:42
messaget::mstreamt::source_location
source_locationt source_location
Definition: message.h:247
language_util.h
goto_inlinet::goto_inline_logt::output_inline_log_json
jsont output_inline_log_json() const
Definition: goto_inline_class.cpp:820
goto_inlinet::caching
const bool caching
Definition: goto_inline_class.h:130
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
goto_inlinet::goto_inline_logt::log_map
log_mapt log_map
Definition: goto_inline_class.h:121
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
goto_inlinet::cache
cachet cache
Definition: goto_inline_class.h:193
goto_inlinet::parameter_destruction
void parameter_destruction(const goto_programt::targett target, const goto_functiont::parameter_identifierst &parameter_identifiers, goto_programt &dest)
Definition: goto_inline_class.cpp:131
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:190
goto_inlinet::goto_inline_logt::goto_inline_log_infot::end
goto_programt::const_targett end
Definition: goto_inline_class.h:96
OTHER
@ OTHER
Definition: goto_program.h:38
replace_location
void replace_location(source_locationt &dest, const source_locationt &new_location)
Definition: goto_inline_class.cpp:189
irept::is_nil
bool is_nil() const
Definition: irep.h:387
irept::id
const irep_idt & id() const
Definition: irep.h:407
goto_inlinet::goto_functions
goto_functionst & goto_functions
Definition: goto_inline_class.h:126
goto_programt::instructiont::is_end_function
bool is_end_function() const
Definition: goto_program.h:446
goto_inlinet::ns
const namespacet & ns
Definition: goto_inline_class.h:127
goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:27
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
dstringt::empty
bool empty() const
Definition: dstring.h:88
jsont::make_array
json_arrayt & make_array()
Definition: json.h:420
goto_inlinet::goto_inline_logt::goto_inline_log_infot
Definition: goto_inline_class.h:89
cprover_prefix.h
std_code.h
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1260
goto_functiont::is_hidden
bool is_hidden() const
Definition: goto_function.h:51
goto_programt::destructive_append
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:640
goto_inlinet::output_inline_map
void output_inline_map(std::ostream &out, const inline_mapt &inline_map)
Definition: goto_inline_class.cpp:669
goto_inlinet::inline_mapt
std::map< irep_idt, call_listt > inline_mapt
Definition: goto_inline_class.h:48
goto_inlinet::goto_inline_logt::goto_inline_log_infot::function
irep_idt function
Definition: goto_inline_class.h:95
source_locationt
Definition: source_location.h:20
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1968
goto_inlinet::parameter_assignments
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)
Definition: goto_inline_class.cpp:30
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:556
expr_util.h
Deprecated expression utility functions.
ASSIGN
@ ASSIGN
Definition: goto_program.h:47
goto_inlinet::finished_set
finished_sett finished_set
Definition: goto_inline_class.h:196
goto_inlinet::goto_inline_transitive
const goto_functiont & goto_inline_transitive(const irep_idt identifier, const goto_functiont &goto_function, const bool force_full)
Definition: goto_inline_class.cpp:541
symbolt
Symbol table entry.
Definition: symbol.h:28
goto_inlinet::expand_function_call
void expand_function_call(goto_programt &dest, const inline_mapt &inline_map, const bool transitive, const bool force_full, goto_programt::targett target)
Definition: goto_inline_class.cpp:310
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
goto_inlinet::check_inline_map
bool check_inline_map(const inline_mapt &inline_map) const
Definition: goto_inline_class.cpp:658
goto_functiont::copy_from
void copy_from(const goto_functiont &other)
Definition: goto_function.h:79
goto_inlinet::inline_log
goto_inline_logt inline_log
Definition: goto_inline_class.h:132
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
goto_functiont::parameter_identifierst
std::vector< irep_idt > parameter_identifierst
Definition: goto_function.h:31
goto_functiont::parameter_identifiers
parameter_identifierst parameter_identifiers
The identifiers of the parameters of this function.
Definition: goto_function.h:36
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:551
goto_inlinet::is_ignored
bool is_ignored(const irep_idt id) const
Definition: goto_inline_class.cpp:603
messaget::progress
mstreamt & progress() const
Definition: message.h:424
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:239
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:1781
remove_skip.h
Program Transformation.
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
LOCATION
@ LOCATION
Definition: goto_program.h:42
messaget::warning
mstreamt & warning() const
Definition: message.h:404
goto_inlinet::goto_inline_logt::copy_from
void copy_from(const goto_programt &from, const goto_programt &to)
Definition: goto_inline_class.cpp:774
comment
static std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:109
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
goto_inlinet::output_cache
void output_cache(std::ostream &out) const
Definition: goto_inline_class.cpp:712
std_expr.h
API to expression classes.
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:234
goto_programt::instructiont::nil_target
static const unsigned nil_target
Uniquely identify an invalid target or location.
Definition: goto_program.h:492
json_arrayt::push_back
jsont & push_back(const jsont &json)
Definition: json.h:212
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:550
code_function_callt::function
exprt & function()
Definition: std_code.h:1250
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:1167
code_expressiont
codet representation of an expression statement.
Definition: std_code.h:1842
goto_inlinet::goto_functiont
goto_functionst::goto_functiont goto_functiont
Definition: goto_inline_class.h:37
json_stringt
Definition: json.h:270
source_locationt::set_property_class
void set_property_class(const irep_idt &property_class)
Definition: source_location.h:136