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  warning().source_location=source_location;
68  warning() << "call to '" << function_name << "': "
69  << "not enough arguments, "
70  << "inserting non-deterministic value" << 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  const auto &code_return = it->get_return();
169 
170  if(lhs.is_not_nil())
171  {
172  if(!code_return.has_return_value())
173  {
174  warning().source_location=it->code.find_source_location();
175  warning() << "return expects one operand!\n"
176  << it->code.pretty() << eom;
177  continue;
178  }
179 
180  // a typecast may be necessary if the declared return type at the call
181  // site differs from the defined return type
182  it->code = code_assignt(
183  lhs,
185  code_return.return_value(), lhs.type()));
186  it->type=ASSIGN;
187 
188  it++;
189  }
190  else if(code_return.has_return_value())
191  {
192  it->code = code_expressiont(code_return.return_value());
193  it->type=OTHER;
194  it++;
195  }
196  }
197  }
198 }
199 
201  source_locationt &dest,
202  const source_locationt &new_location)
203 {
204  // we copy, and then adjust for property_id, property_class
205  // and comment, if necessary
206 
208  irep_idt property_class=dest.get_property_class();
209  irep_idt property_id=dest.get_property_id();
210 
211  dest=new_location;
212 
213  if(!comment.empty())
214  dest.set_comment(comment);
215 
216  if(!property_class.empty())
217  dest.set_property_class(property_class);
218 
219  if(!property_id.empty())
220  dest.set_property_id(property_id);
221 }
222 
224  exprt &dest,
225  const source_locationt &new_location)
226 {
227  Forall_operands(it, dest)
228  replace_location(*it, new_location);
229 
230  if(dest.find(ID_C_source_location).is_not_nil())
231  replace_location(dest.add_source_location(), new_location);
232 }
233 
235  const goto_functiont &goto_function,
236  goto_programt &dest,
237  goto_programt::targett target,
238  const exprt &lhs,
239  const symbol_exprt &function,
240  const exprt::operandst &arguments)
241 {
242  PRECONDITION(target->is_function_call());
243  PRECONDITION(!dest.empty());
244  PRECONDITION(goto_function.body_available());
245 
246  const irep_idt identifier=function.get_identifier();
247 
248  goto_programt body;
249  body.copy_from(goto_function.body);
250  inline_log.copy_from(goto_function.body, body);
251 
252  goto_programt::instructiont &end=body.instructions.back();
254  end.is_end_function(),
255  "final instruction of a function must be an END_FUNCTION");
256  end.type=LOCATION;
257 
258  // make sure the inlined function does not introduce hiding
259  if(ns.lookup(identifier).is_hidden())
260  {
261  for(auto &instruction : body.instructions)
262  instruction.labels.remove(CPROVER_PREFIX "HIDE");
263  }
264 
265  replace_return(body, lhs);
266 
267  goto_programt tmp1;
269  target, identifier, goto_function.parameter_identifiers, arguments, tmp1);
270 
271  goto_programt tmp2;
272  parameter_destruction(target, goto_function.parameter_identifiers, tmp2);
273 
274  goto_programt tmp;
275  tmp.destructive_append(tmp1); // par assignment
276  tmp.destructive_append(body); // body
277  tmp.destructive_append(tmp2); // par destruction
278 
280  t_it=goto_function.body.instructions.begin();
281  unsigned begin_location_number=t_it->location_number;
282  t_it=--goto_function.body.instructions.end();
284  t_it->is_end_function(),
285  "final instruction of a function must be an END_FUNCTION");
286  unsigned end_location_number=t_it->location_number;
287 
288  unsigned call_location_number=target->location_number;
289 
291  tmp,
292  begin_location_number,
293  end_location_number,
294  call_location_number,
295  identifier);
296 
297  if(adjust_function)
298  {
300  {
301  replace_location(it->source_location, target->source_location);
302  replace_location(it->code, target->source_location);
303 
304  if(it->has_condition())
305  {
306  exprt c = it->get_condition();
307  replace_location(c, target->source_location);
308  it->set_condition(c);
309  }
310  }
311  }
312 
313  // kill call
314  target->type=LOCATION;
315  target->code.clear();
316  target++;
317 
318  dest.destructive_insert(target, tmp);
319 }
320 
322  goto_programt &dest,
323  const inline_mapt &inline_map,
324  const bool transitive,
325  const bool force_full,
326  goto_programt::targett target)
327 {
328  PRECONDITION(target->is_function_call());
329  PRECONDITION(!dest.empty());
330  PRECONDITION(!transitive || inline_map.empty());
331 
332 #ifdef DEBUG
333  std::cout << "Expanding call:\n";
334  dest.output_instruction(ns, irep_idt(), std::cout, *target);
335 #endif
336 
337  exprt lhs;
338  exprt function_expr;
339  exprt::operandst arguments;
340 
341  get_call(target, lhs, function_expr, arguments);
342 
343  if(function_expr.id()!=ID_symbol)
344  return;
345 
346  const symbol_exprt &function=to_symbol_expr(function_expr);
347 
348  const irep_idt identifier=function.get_identifier();
349 
350  if(is_ignored(identifier))
351  return;
352 
353  // see if we are already expanding it
354  if(recursion_set.find(identifier)!=recursion_set.end())
355  {
356  // it's recursive.
357  // Uh. Buh. Give up.
358  warning().source_location=function.find_source_location();
359  warning() << "recursion is ignored on call to '" << identifier << "'"
360  << eom;
361 
362  if(force_full)
363  target->turn_into_skip();
364 
365  return;
366  }
367 
368  goto_functionst::function_mapt::iterator f_it=
369  goto_functions.function_map.find(identifier);
370 
371  if(f_it==goto_functions.function_map.end())
372  {
373  warning().source_location=function.find_source_location();
374  warning() << "missing function '" << identifier << "' is ignored" << eom;
375 
376  if(force_full)
377  target->turn_into_skip();
378 
379  return;
380  }
381 
382  // function to inline
383  goto_functiont &goto_function=f_it->second;
384 
385  if(goto_function.body_available())
386  {
387  if(transitive)
388  {
389  const goto_functiont &cached=
391  identifier,
392  goto_function,
393  force_full);
394 
395  // insert 'cached' into 'dest' at 'target'
397  cached,
398  dest,
399  target,
400  lhs,
401  function,
402  arguments);
403 
404  progress() << "Inserting " << identifier << " into caller" << eom;
405  progress() << "Number of instructions: "
406  << cached.body.instructions.size() << eom;
407 
408  if(!caching)
409  {
410  progress() << "Removing " << identifier << " from cache" << eom;
411  progress() << "Number of instructions: "
412  << cached.body.instructions.size() << eom;
413 
414  inline_log.cleanup(cached.body);
415  cache.erase(identifier);
416  }
417  }
418  else
419  {
420  // inline non-transitively
422  identifier,
423  goto_function,
424  inline_map,
425  force_full);
426 
427  // insert 'goto_function' into 'dest' at 'target'
429  goto_function,
430  dest,
431  target,
432  lhs,
433  function,
434  arguments);
435  }
436  }
437  else // no body available
438  {
439  if(no_body_set.insert(identifier).second) // newly inserted
440  {
441  warning().source_location = function.find_source_location();
442  warning() << "no body for function '" << identifier << "'" << eom;
443  }
444  }
445 }
446 
449  exprt &lhs,
450  exprt &function,
451  exprt::operandst &arguments)
452 {
453  PRECONDITION(it->is_function_call());
454 
455  const code_function_callt &call = it->get_function_call();
456 
457  lhs=call.lhs();
458  function=call.function();
459  arguments=call.arguments();
460 }
461 
463  const inline_mapt &inline_map,
464  const bool force_full)
465 {
466  PRECONDITION(check_inline_map(inline_map));
467 
469  {
470  const irep_idt identifier=f_it->first;
471  DATA_INVARIANT(!identifier.empty(), "function name must not be empty");
472  goto_functiont &goto_function=f_it->second;
473 
474  if(!goto_function.body_available())
475  continue;
476 
477  goto_inline(identifier, goto_function, inline_map, force_full);
478  }
479 }
480 
482  const irep_idt identifier,
483  goto_functiont &goto_function,
484  const inline_mapt &inline_map,
485  const bool force_full)
486 {
487  recursion_set.clear();
488 
490  identifier,
491  goto_function,
492  inline_map,
493  force_full);
494 }
495 
497  const irep_idt identifier,
498  goto_functiont &goto_function,
499  const inline_mapt &inline_map,
500  const bool force_full)
501 {
502  PRECONDITION(goto_function.body_available());
503 
504  finished_sett::const_iterator f_it=finished_set.find(identifier);
505 
506  if(f_it!=finished_set.end())
507  return;
508 
509  PRECONDITION(check_inline_map(identifier, inline_map));
510 
511  goto_programt &goto_program=goto_function.body;
512 
513  const inline_mapt::const_iterator im_it=inline_map.find(identifier);
514 
515  if(im_it==inline_map.end())
516  return;
517 
518  const call_listt &call_list=im_it->second;
519 
520  if(call_list.empty())
521  return;
522 
523  recursion_set.insert(identifier);
524 
525  for(const auto &call : call_list)
526  {
527  const bool transitive=call.second;
528 
529  const inline_mapt &new_inline_map=
530  transitive?inline_mapt():inline_map;
531 
533  goto_program,
534  new_inline_map,
535  transitive,
536  force_full,
537  call.first);
538  }
539 
540  recursion_set.erase(identifier);
541 
542  // remove_skip(goto_program);
543  // goto_program.update(); // does not change loop ids
544 
545  finished_set.insert(identifier);
546 }
547 
549  const irep_idt identifier,
550  const goto_functiont &goto_function,
551  const bool force_full)
552 {
553  PRECONDITION(goto_function.body_available());
554 
555  cachet::const_iterator c_it=cache.find(identifier);
556 
557  if(c_it!=cache.end())
558  {
559  const goto_functiont &cached=c_it->second;
561  cached.body_available(),
562  "body of cached functions must be available");
563  return cached;
564  }
565 
566  goto_functiont &cached=cache[identifier];
568  cached.body.empty(), "body of new function in cache must be empty");
569 
570  progress() << "Creating copy of " << identifier << eom;
571  progress() << "Number of instructions: "
572  << goto_function.body.instructions.size() << eom;
573 
574  cached.copy_from(goto_function); // location numbers not changed
575  inline_log.copy_from(goto_function.body, cached.body);
576 
577  goto_programt &goto_program=cached.body;
578 
579  goto_programt::targetst call_list;
580 
581  Forall_goto_program_instructions(i_it, goto_program)
582  {
583  if(i_it->is_function_call())
584  call_list.push_back(i_it);
585  }
586 
587  if(call_list.empty())
588  return cached;
589 
590  recursion_set.insert(identifier);
591 
592  for(const auto &call : call_list)
593  {
595  goto_program,
596  inline_mapt(),
597  true,
598  force_full,
599  call);
600  }
601 
602  recursion_set.erase(identifier);
603 
604  // remove_skip(goto_program);
605  // goto_program.update(); // does not change loop ids
606 
607  return cached;
608 }
609 
610 bool goto_inlinet::is_ignored(const irep_idt id) const
611 {
612  return id == CPROVER_PREFIX "cleanup" || id == CPROVER_PREFIX "set_must" ||
613  id == CPROVER_PREFIX "set_may" || id == CPROVER_PREFIX "clear_must" ||
614  id == CPROVER_PREFIX "clear_may" || id == CPROVER_PREFIX "cover";
615 }
616 
618  const irep_idt identifier,
619  const inline_mapt &inline_map) const
620 {
621  goto_functionst::function_mapt::const_iterator f_it=
622  goto_functions.function_map.find(identifier);
623 
625 
626  inline_mapt::const_iterator im_it=inline_map.find(identifier);
627 
628  if(im_it==inline_map.end())
629  return true;
630 
631  const call_listt &call_list=im_it->second;
632 
633  if(call_list.empty())
634  return true;
635 
637 
638  for(const auto &call : call_list)
639  {
640  const goto_programt::const_targett target=call.first;
641 
642  #if 0
643  // might not hold if call was previously inlined
644  if(target->function!=identifier)
645  return false;
646  #endif
647 
648  // location numbers increasing
649  if(
651  target->location_number <= ln)
652  {
653  return false;
654  }
655 
656  if(!target->is_function_call())
657  return false;
658 
659  ln=target->location_number;
660  }
661 
662  return true;
663 }
664 
665 bool goto_inlinet::check_inline_map(const inline_mapt &inline_map) const
666 {
668  {
669  if(!check_inline_map(f_it->first, inline_map))
670  return false;
671  }
672 
673  return true;
674 }
675 
677  std::ostream &out,
678  const inline_mapt &inline_map)
679 {
680  PRECONDITION(check_inline_map(inline_map));
681 
682  for(const auto &it : inline_map)
683  {
684  const irep_idt &id=it.first;
685  const call_listt &call_list=it.second;
686 
687  out << "Function: " << id << "\n";
688 
689  goto_functionst::function_mapt::const_iterator f_it=
690  goto_functions.function_map.find(id);
691 
692  if(f_it!=goto_functions.function_map.end() &&
693  !call_list.empty())
694  {
695  const goto_functiont &goto_function=f_it->second;
697  goto_function.body_available(),
698  "cannot inline function with empty body");
699 
700  const goto_programt &goto_program=goto_function.body;
701 
702  for(const auto &call : call_list)
703  {
704  const goto_programt::const_targett target=call.first;
705  bool transitive=call.second;
706 
707  out << " Call:\n";
708  goto_program.output_instruction(ns, id, out, *target);
709  out << " Transitive: " << transitive << "\n";
710  }
711  }
712  else
713  {
714  out << " -\n";
715  }
716  }
717 }
718 
719 void goto_inlinet::output_cache(std::ostream &out) const
720 {
721  for(auto it=cache.begin(); it!=cache.end(); it++)
722  {
723  if(it!=cache.begin())
724  out << ", ";
725 
726  out << it->first << "\n";
727  }
728 }
729 
730 // remove segment that refer to the given goto program
732  const goto_programt &goto_program)
733 {
734  forall_goto_program_instructions(it, goto_program)
735  log_map.erase(it);
736 }
737 
739  const goto_functionst::function_mapt &function_map)
740 {
741  for(const auto &it : function_map)
742  {
743  const goto_functiont &goto_function=it.second;
744 
745  if(!goto_function.body_available())
746  continue;
747 
748  cleanup(goto_function.body);
749  }
750 }
751 
753  const goto_programt &goto_program,
754  const unsigned begin_location_number,
755  const unsigned end_location_number,
756  const unsigned call_location_number,
757  const irep_idt function)
758 {
759  PRECONDITION(!goto_program.empty());
760  PRECONDITION(!function.empty());
761  PRECONDITION(end_location_number >= begin_location_number);
762 
763  goto_programt::const_targett start=goto_program.instructions.begin();
764  INVARIANT(
765  log_map.find(start) == log_map.end(),
766  "inline function should be registered once in map of inline functions");
767 
768  goto_programt::const_targett end=goto_program.instructions.end();
769  end--;
770 
772  info.begin_location_number=begin_location_number;
773  info.end_location_number=end_location_number;
774  info.call_location_number=call_location_number;
775  info.function=function;
776  info.end=end;
777 
778  log_map[start]=info;
779 }
780 
782  const goto_programt &from,
783  const goto_programt &to)
784 {
785  PRECONDITION(from.instructions.size() == to.instructions.size());
786 
789 
790  for(; it1!=from.instructions.end(); it1++, it2++)
791  {
793  it2 != to.instructions.end(),
794  "'to' target function is not allowed to be empty");
796  it1->location_number == it2->location_number,
797  "both functions' instruction should point to the same source");
798 
799  log_mapt::const_iterator l_it=log_map.find(it1);
800  if(l_it!=log_map.end()) // a segment starts here
801  {
802  // as 'to' is a fresh copy
804  log_map.find(it2) == log_map.end(),
805  "'to' target is not expected to be in the log_map");
806 
807  goto_inline_log_infot info=l_it->second;
809 
810  // find end of new
811  goto_programt::const_targett tmp_it=it1;
812  goto_programt::const_targett new_end=it2;
813  while(tmp_it!=end)
814  {
815  new_end++;
816  tmp_it++;
817  }
818 
819  info.end=new_end;
820 
821  log_map[it2]=info;
822  }
823  }
824 }
825 
826 // call after goto_functions.update()!
828 {
829  json_objectt json_result;
830  json_arrayt &json_inlined=json_result["inlined"].make_array();
831 
832  for(const auto &it : log_map)
833  {
834  goto_programt::const_targett start=it.first;
835  const goto_inline_log_infot &info=it.second;
837 
838  PRECONDITION(start->location_number <= end->location_number);
839 
840  json_arrayt json_orig{
843  json_arrayt json_new{json_numbert(std::to_string(start->location_number)),
844  json_numbert(std::to_string(end->location_number))};
845 
846  json_objectt object{
848  {"function", json_stringt(info.function.c_str())},
849  {"originalSegment", std::move(json_orig)},
850  {"inlinedSegment", std::move(json_new)}};
851 
852  json_inlined.push_back(std::move(object));
853  }
854 
855  return std::move(json_result);
856 }
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:1201
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:30
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
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2021
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:24
goto_programt::make_dead
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:927
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:234
goto_inline.h
Function Inlining.
typet
The type of an expression, extends irept.
Definition: type.h:29
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:752
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:447
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:272
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:626
invariant.h
goto_programt::add
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:686
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:762
exprt
Base class for all expressions.
Definition: expr.h:53
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:481
irep_idt
dstringt irep_idt
Definition: irep.h:32
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:731
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:82
goto_programt::make_decl
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:920
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:1208
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:1024
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:128
goto_inlinet::no_body_set
no_body_sett no_body_set
Definition: goto_inline_class.h:201
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:496
goto_programt::targetst
std::list< targett > targetst
Definition: goto_program.h:581
goto_inlinet::recursion_set
recursion_sett recursion_set
Definition: goto_inline_class.h:198
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
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:1183
goto_functiont::body_available
bool body_available() const
Definition: goto_function.h:44
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:402
coverage_criteriont::LOCATION
@ LOCATION
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:677
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:41
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:827
goto_inlinet::caching
const bool caching
Definition: goto_inline_class.h:129
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:192
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:177
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:37
replace_location
void replace_location(source_locationt &dest, const source_locationt &new_location)
Definition: goto_inline_class.cpp:200
irept::is_nil
bool is_nil() const
Definition: irep.h:398
irept::id
const irep_idt & id() const
Definition: irep.h:418
goto_inlinet::goto_functions
goto_functionst & goto_functions
Definition: goto_inline_class.h:125
goto_programt::instructiont::is_end_function
bool is_end_function() const
Definition: goto_program.h:475
goto_inlinet::ns
const namespacet & ns
Definition: goto_inline_class.h:126
goto_functiont
A goto function, consisting of function type (see type), function body (see body),...
Definition: goto_function.h:28
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
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:1228
Forall_goto_functions
#define Forall_goto_functions(it, functions)
Definition: goto_functions.h:117
goto_programt::destructive_append
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:669
goto_inlinet::output_inline_map
void output_inline_map(std::ostream &out, const inline_mapt &inline_map)
Definition: goto_inline_class.cpp:676
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:1945
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:585
expr_util.h
Deprecated expression utility functions.
ASSIGN
@ ASSIGN
Definition: goto_program.h:46
goto_inlinet::finished_set
finished_sett finished_set
Definition: goto_inline_class.h:195
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:548
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:321
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:665
goto_functiont::copy_from
void copy_from(const goto_functiont &other)
Definition: goto_function.h:93
goto_inlinet::inline_log
goto_inline_logt inline_log
Definition: goto_inline_class.h:131
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
goto_functiont::parameter_identifierst
std::vector< irep_idt > parameter_identifierst
Definition: goto_function.h:36
forall_goto_functions
#define forall_goto_functions(it, functions)
Definition: goto_functions.h:122
goto_functiont::parameter_identifiers
parameter_identifierst parameter_identifiers
The identifiers of the parameters of this function.
Definition: goto_function.h:42
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:580
goto_inlinet::is_ignored
bool is_ignored(const irep_idt id) const
Definition: goto_inline_class.cpp:610
messaget::progress
mstreamt & progress() const
Definition: message.h:424
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:259
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2013
remove_skip.h
Program Transformation.
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
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:781
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:179
goto_inlinet::output_cache
void output_cache(std::ostream &out) const
Definition: goto_inline_class.cpp:719
std_expr.h
API to expression classes.
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:254
goto_programt::instructiont::nil_target
static const unsigned nil_target
Uniquely identify an invalid target or location.
Definition: goto_program.h:521
json_arrayt::push_back
jsont & push_back(const jsont &json)
Definition: json.h:212
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:579
code_function_callt::function
exprt & function()
Definition: std_code.h:1218
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:1196
validation_modet::INVARIANT
@ INVARIANT
code_expressiont
codet representation of an expression statement.
Definition: std_code.h:1810
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