CBMC
goto_convert_function_call.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Program Transformation
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "goto_convert_class.h"
13 
14 #include <util/expr_util.h>
15 #include <util/source_location.h>
16 #include <util/std_expr.h>
17 
18 #include "destructor.h"
19 
21  const code_function_callt &function_call,
22  goto_programt &dest,
23  const irep_idt &mode)
24 {
26  function_call.lhs(),
27  function_call.function(),
28  function_call.arguments(),
29  dest,
30  mode);
31 }
32 
34  const exprt &lhs,
35  const exprt &function,
36  const exprt::operandst &arguments,
37  goto_programt &dest,
38  const irep_idt &mode)
39 {
40  // make it all side effect free
41 
42  exprt new_lhs = lhs, new_function = function;
43 
44  exprt::operandst new_arguments = arguments;
45 
46  clean_expr_resultt side_effects;
47 
48  if(!new_lhs.is_nil())
49  side_effects.add(clean_expr(new_lhs, mode));
50 
51  side_effects.add(clean_expr(new_function, mode));
52 
53  for(auto &new_argument : new_arguments)
54  side_effects.add(clean_expr(new_argument, mode));
55 
56  dest.destructive_append(side_effects.side_effects);
57 
58  // split on the function
59 
60  if(new_function.id() == ID_if)
61  {
63  new_lhs, to_if_expr(new_function), new_arguments, dest, mode);
64  }
65  else if(new_function.id() == ID_symbol)
66  {
68  new_lhs, to_symbol_expr(new_function), new_arguments, dest, mode);
69  }
70  else if(new_function.id() == ID_null_object)
71  {
72  }
73  else if(
74  new_function.id() == ID_dereference ||
75  new_function.id() == "virtual_function")
76  {
77  do_function_call_other(new_lhs, new_function, new_arguments, dest);
78  }
79  else
80  {
82  false,
83  "unexpected function argument",
84  new_function.id(),
85  function.find_source_location());
86  }
87 
88  destruct_locals(side_effects.temporaries, dest, ns);
89 }
90 
92  const exprt &lhs,
93  const if_exprt &function,
94  const exprt::operandst &arguments,
95  goto_programt &dest,
96  const irep_idt &mode)
97 {
98  // case split
99 
100  // c?f():g()
101  //--------------------
102  // v: if(!c) goto y;
103  // w: f();
104  // x: goto z;
105  // y: g();
106  // z: ;
107 
108  // do the v label
109  goto_programt tmp_v;
111  boolean_negate(function.cond()), function.cond().source_location()));
112 
113  // do the x label
114  goto_programt tmp_x;
117 
118  // do the z label
119  goto_programt tmp_z;
121 
122  // y: g();
123  goto_programt tmp_y;
125 
126  do_function_call(lhs, function.false_case(), arguments, tmp_y, mode);
127 
128  if(tmp_y.instructions.empty())
129  y = tmp_y.add(goto_programt::make_skip());
130  else
131  y = tmp_y.instructions.begin();
132 
133  // v: if(!c) goto y;
134  v->complete_goto(y);
135 
136  // w: f();
137  goto_programt tmp_w;
138 
139  do_function_call(lhs, function.true_case(), arguments, tmp_w, mode);
140 
141  if(tmp_w.instructions.empty())
142  tmp_w.add(goto_programt::make_skip());
143 
144  // x: goto z;
145  x->complete_goto(z);
146 
147  dest.destructive_append(tmp_v);
148  dest.destructive_append(tmp_w);
149  dest.destructive_append(tmp_x);
150  dest.destructive_append(tmp_y);
151  dest.destructive_append(tmp_z);
152 }
153 
155  const exprt &lhs,
156  const exprt &function,
157  const exprt::operandst &arguments,
158  goto_programt &dest)
159 {
160  // don't know what to do with it
161  code_function_callt function_call(lhs, function, arguments);
162  function_call.add_source_location() = function.source_location();
164  function_call, function.source_location()));
165 }
goto_instruction_codet representation of a function call statement.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Base class for all expressions.
Definition: expr.h:56
std::vector< exprt > operandst
Definition: expr.h:58
source_locationt & add_source_location()
Definition: expr.h:236
virtual void do_function_call_if(const exprt &lhs, const if_exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)
virtual void do_function_call(const exprt &lhs, const exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)
void convert_function_call(const code_function_callt &code, goto_programt &dest, const irep_idt &mode)
virtual void do_function_call_symbol(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)
add function calls to function queue for later processing
virtual void do_function_call_other(const exprt &lhs, const exprt &function, const exprt::operandst &arguments, goto_programt &dest)
clean_expr_resultt clean_expr(exprt &expr, const irep_idt &mode, bool result_is_used=true)
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:622
instructionst::iterator targett
Definition: goto_program.h:614
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:722
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:891
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:739
static instructiont make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())
The trinary if-then-else operator.
Definition: std_expr.h:2370
bool is_nil() const
Definition: irep.h:368
The Boolean constant true.
Definition: std_expr.h:3063
void destruct_locals(const std::list< irep_idt > &vars, goto_programt &dest, const namespacet &ns)
Definition: destructor.cpp:62
Destructor Calls.
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition: expr_util.cpp:103
Deprecated expression utility functions.
Program Transformation.
#define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Same as invariant, with one or more diagnostics attached Diagnostics can be of any type that has a sp...
Definition: invariant.h:437
API to expression classes.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2450
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:272
std::list< irep_idt > temporaries
Identifiers of temporaries introduced while cleaning an expression.
void add(clean_expr_resultt &&other)
goto_programt side_effects
Statements implementing side effects of the expression that was subject to cleaning.