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 {
29  function_call.lhs(),
30  function_call.function(),
31  function_call.arguments(),
32  dest);
33 }
34 
36  const exprt &lhs,
37  const exprt &function,
38  const exprt::operandst &arguments,
39  goto_programt &dest)
40 {
41  // make it all side effect free
42 
43  exprt new_lhs=lhs,
44  new_function=function;
45 
46  exprt::operandst new_arguments=arguments;
47 
48  if(!new_lhs.is_nil())
49  clean_expr(new_lhs, dest);
50 
51  clean_expr(new_function, dest);
52 
53  // the arguments of __noop do not get evaluated
54  if(new_function.id()==ID_symbol &&
55  to_symbol_expr(new_function).get_identifier()=="__noop")
56  {
57  new_arguments.clear();
58  }
59 
60  Forall_expr(it, new_arguments)
61  clean_expr(*it, dest);
62 
63  // split on the function
64 
65  if(new_function.id()==ID_if)
66  {
67  do_function_call_if(new_lhs, to_if_expr(new_function), new_arguments, dest);
68  }
69  else if(new_function.id()==ID_symbol)
70  {
72  new_lhs, to_symbol_expr(new_function), new_arguments, dest);
73  }
74  else if(new_function.id()=="NULL-object")
75  {
76  }
77  else if(new_function.id()==ID_dereference ||
78  new_function.id()=="virtual_function")
79  {
80  do_function_call_other(new_lhs, new_function, new_arguments, dest);
81  }
82  else
83  {
84  error().source_location=function.find_source_location();
85  error() << "unexpected function argument: " << new_function.id()
86  << eom;
87  throw 0;
88  }
89 }
90 
92  const exprt &lhs,
93  const if_exprt &function,
94  const exprt::operandst &arguments,
95  goto_programt &dest)
96 {
97  // case split
98 
99  // c?f():g()
100  //--------------------
101  // v: if(!c) goto y;
102  // w: f();
103  // x: goto z;
104  // y: g();
105  // z: ;
106 
107  // do the v label
108  goto_programt tmp_v;
110 
111  // do the x label
112  goto_programt tmp_x;
114 
115  // do the z label
116  goto_programt tmp_z;
118  z->make_skip();
119 
120  // y: g();
121  goto_programt tmp_y;
123 
124  do_function_call(lhs, function.false_case(), arguments, tmp_y);
125 
126  if(tmp_y.instructions.empty())
127  y=tmp_y.add_instruction(SKIP);
128  else
129  y=tmp_y.instructions.begin();
130 
131  // v: if(!c) goto y;
132  v->make_goto(y);
133  v->guard=function.cond();
134  v->guard.make_not();
135  v->source_location=function.cond().source_location();
136 
137  // w: f();
138  goto_programt tmp_w;
139 
140  do_function_call(lhs, function.true_case(), arguments, tmp_w);
141 
142  if(tmp_w.instructions.empty())
143  tmp_w.add_instruction(SKIP);
144 
145  // x: goto z;
146  x->make_goto(z);
147 
148  dest.destructive_append(tmp_v);
149  dest.destructive_append(tmp_w);
150  dest.destructive_append(tmp_x);
151  dest.destructive_append(tmp_y);
152  dest.destructive_append(tmp_z);
153 }
154 
156  const exprt &lhs,
157  const exprt &function,
158  const exprt::operandst &arguments,
159  goto_programt &dest)
160 {
161  // don't know what to do with it
163 
164  code_function_callt function_call;
165  function_call.add_source_location()=function.source_location();
166  function_call.lhs()=lhs;
167  function_call.function()=function;
168  function_call.arguments()=arguments;
169 
170  t->source_location=function.source_location();
171  t->code.swap(function_call);
172 }
targett add_instruction()
Adds an instruction at the end.
bool is_nil() const
Definition: irep.h:103
virtual void do_function_call(const exprt &lhs, const exprt &function, const exprt::operandst &arguments, goto_programt &dest)
instructionst instructions
The list of instructions in the goto program.
const irep_idt & get_identifier() const
Definition: std_expr.h:120
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:2771
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
argumentst & arguments()
Definition: std_code.h:689
#define Forall_expr(it, expr)
Definition: expr.h:32
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:2836
source_locationt source_location
Definition: message.h:175
Program Transformation.
API to expression classes.
A function call.
Definition: std_code.h:657
void clean_expr(exprt &expr, goto_programt &dest, bool result_is_used=true)
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:49
void convert_function_call(const code_function_callt &code, goto_programt &dest)
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
virtual void do_function_call_if(const exprt &lhs, const if_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
exprt & function()
Definition: std_code.h:677
Base class for all expressions.
Definition: expr.h:46
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
mstreamt & error()
Definition: message.h:223
source_locationt & add_source_location()
Definition: expr.h:147
void destructive_append(goto_program_templatet< codeT, guardT > &p)
Appends the given program, which is destroyed.