cprover
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 
15 #include <util/cprover_prefix.h>
16 #include <util/expr_util.h>
17 #include <util/prefix.h>
18 #include <util/replace_expr.h>
19 #include <util/source_location.h>
20 #include <util/std_expr.h>
21 
22 #include <util/c_types.h>
23 
25  const code_function_callt &function_call,
26  goto_programt &dest,
27  const irep_idt &mode)
28 {
30  function_call.lhs(),
31  function_call.function(),
32  function_call.arguments(),
33  dest,
34  mode);
35 }
36 
38  const exprt &lhs,
39  const exprt &function,
40  const exprt::operandst &arguments,
41  goto_programt &dest,
42  const irep_idt &mode)
43 {
44  // make it all side effect free
45 
46  exprt new_lhs=lhs,
47  new_function=function;
48 
49  exprt::operandst new_arguments=arguments;
50 
51  if(!new_lhs.is_nil())
52  clean_expr(new_lhs, dest, mode);
53 
54  clean_expr(new_function, dest, mode);
55 
56  for(auto &new_argument : new_arguments)
57  clean_expr(new_argument, dest, mode);
58 
59  // split on the function
60 
61  if(new_function.id()==ID_if)
62  {
64  new_lhs, to_if_expr(new_function), new_arguments, dest, mode);
65  }
66  else if(new_function.id()==ID_symbol)
67  {
69  new_lhs, to_symbol_expr(new_function), new_arguments, dest);
70  }
71  else if(new_function.id() == ID_null_object)
72  {
73  }
74  else if(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 
90  const exprt &lhs,
91  const if_exprt &function,
92  const exprt::operandst &arguments,
93  goto_programt &dest,
94  const irep_idt &mode)
95 {
96  // case split
97 
98  // c?f():g()
99  //--------------------
100  // v: if(!c) goto y;
101  // w: f();
102  // x: goto z;
103  // y: g();
104  // z: ;
105 
106  // do the v label
107  goto_programt tmp_v;
109  boolean_negate(function.cond()), function.cond().source_location()));
110 
111  // do the x label
112  goto_programt tmp_x;
115 
116  // do the z label
117  goto_programt tmp_z;
119 
120  // y: g();
121  goto_programt tmp_y;
123 
124  do_function_call(lhs, function.false_case(), arguments, tmp_y, mode);
125 
126  if(tmp_y.instructions.empty())
127  y = tmp_y.add(goto_programt::make_skip());
128  else
129  y=tmp_y.instructions.begin();
130 
131  // v: if(!c) goto y;
132  v->complete_goto(y);
133 
134  // w: f();
135  goto_programt tmp_w;
136 
137  do_function_call(lhs, function.true_case(), arguments, tmp_w, mode);
138 
139  if(tmp_w.instructions.empty())
140  tmp_w.add(goto_programt::make_skip());
141 
142  // x: goto z;
143  x->complete_goto(z);
144 
145  dest.destructive_append(tmp_v);
146  dest.destructive_append(tmp_w);
147  dest.destructive_append(tmp_x);
148  dest.destructive_append(tmp_y);
149  dest.destructive_append(tmp_z);
150 }
151 
153  const exprt &lhs,
154  const exprt &function,
155  const exprt::operandst &arguments,
156  goto_programt &dest)
157 {
158  // don't know what to do with it
159  code_function_callt function_call(lhs, function, arguments);
160  function_call.add_source_location()=function.source_location();
162  function_call, function.source_location()));
163 }
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
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
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)
virtual void do_function_call_symbol(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
add function calls to function queue for later processing
void convert_function_call(const code_function_callt &code, goto_programt &dest, const irep_idt &mode)
void clean_expr(exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used=true)
virtual void do_function_call_other(const exprt &lhs, const exprt &function, const exprt::operandst &arguments, goto_programt &dest)
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
instructionst::iterator targett
Definition: goto_program.h:550
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:640
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:822
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:657
static instructiont make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:938
The trinary if-then-else operator.
Definition: std_expr.h:2087
bool is_nil() const
Definition: irep.h:387
The Boolean constant true.
Definition: std_expr.h:2717
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition: expr_util.cpp:128
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:438
API to expression classes.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2152
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:190