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 #include <cassert>
15 
16 #include <util/replace_expr.h>
17 #include <util/source_location.h>
18 #include <util/cprover_prefix.h>
19 #include <util/prefix.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  // the arguments of __noop do not get evaluated
57  if(new_function.id()==ID_symbol &&
58  to_symbol_expr(new_function).get_identifier()=="__noop")
59  {
60  new_arguments.clear();
61  }
62 
63  Forall_expr(it, new_arguments)
64  clean_expr(*it, dest, mode);
65 
66  // split on the function
67 
68  if(new_function.id()==ID_if)
69  {
71  new_lhs, to_if_expr(new_function), new_arguments, dest, mode);
72  }
73  else if(new_function.id()==ID_symbol)
74  {
76  new_lhs, to_symbol_expr(new_function), new_arguments, dest);
77  }
78  else if(new_function.id() == ID_null_object)
79  {
80  }
81  else if(new_function.id()==ID_dereference ||
82  new_function.id()=="virtual_function")
83  {
84  do_function_call_other(new_lhs, new_function, new_arguments, dest);
85  }
86  else
87  {
88  error().source_location=function.find_source_location();
89  error() << "unexpected function argument: " << new_function.id()
90  << eom;
91  throw 0;
92  }
93 }
94 
96  const exprt &lhs,
97  const if_exprt &function,
98  const exprt::operandst &arguments,
99  goto_programt &dest,
100  const irep_idt &mode)
101 {
102  // case split
103 
104  // c?f():g()
105  //--------------------
106  // v: if(!c) goto y;
107  // w: f();
108  // x: goto z;
109  // y: g();
110  // z: ;
111 
112  // do the v label
113  goto_programt tmp_v;
115 
116  // do the x label
117  goto_programt tmp_x;
119 
120  // do the z label
121  goto_programt tmp_z;
123  z->make_skip();
124 
125  // y: g();
126  goto_programt tmp_y;
128 
129  do_function_call(lhs, function.false_case(), arguments, tmp_y, mode);
130 
131  if(tmp_y.instructions.empty())
132  y=tmp_y.add_instruction(SKIP);
133  else
134  y=tmp_y.instructions.begin();
135 
136  // v: if(!c) goto y;
137  v->make_goto(y);
138  v->guard=function.cond();
139  v->guard.make_not();
140  v->source_location=function.cond().source_location();
141 
142  // w: f();
143  goto_programt tmp_w;
144 
145  do_function_call(lhs, function.true_case(), arguments, tmp_w, mode);
146 
147  if(tmp_w.instructions.empty())
148  tmp_w.add_instruction(SKIP);
149 
150  // x: goto z;
151  x->make_goto(z);
152 
153  dest.destructive_append(tmp_v);
154  dest.destructive_append(tmp_w);
155  dest.destructive_append(tmp_x);
156  dest.destructive_append(tmp_y);
157  dest.destructive_append(tmp_z);
158 }
159 
161  const exprt &lhs,
162  const exprt &function,
163  const exprt::operandst &arguments,
164  goto_programt &dest)
165 {
166  // don't know what to do with it
168 
169  code_function_callt function_call;
170  function_call.add_source_location()=function.source_location();
171  function_call.lhs()=lhs;
172  function_call.function()=function;
173  function_call.arguments()=arguments;
174 
175  t->source_location=function.source_location();
176  t->code.swap(function_call);
177 }
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:3424
bool is_nil() const
Definition: irep.h:172
const irep_idt & get_identifier() const
Definition: std_expr.h:128
void destructive_append(goto_programt &p)
Appends the given program, which is destroyed.
Definition: goto_program.h:486
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
The trinary if-then-else operator.
Definition: std_expr.h:3359
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
argumentst & arguments()
Definition: std_code.h:890
void clean_expr(exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used=true)
instructionst::iterator targett
Definition: goto_program.h:397
#define Forall_expr(it, expr)
Definition: expr.h:32
source_locationt source_location
Definition: message.h:214
Program Transformation.
void convert_function_call(const code_function_callt &code, goto_programt &dest, const irep_idt &mode)
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:403
API to expression classes.
mstreamt & error() const
Definition: message.h:302
A function call.
Definition: std_code.h:858
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
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_other(const exprt &lhs, const exprt &function, const exprt::operandst &arguments, goto_programt &dest)
std::vector< exprt > operandst
Definition: expr.h:45
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
exprt & function()
Definition: std_code.h:878
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:505
Base class for all expressions.
Definition: expr.h:42
source_locationt & add_source_location()
Definition: expr.h:130
virtual void do_function_call_if(const exprt &lhs, const if_exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)