cprover
goto_clean_expr.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/fresh_symbol.h>
15 #include <util/simplify_expr.h>
16 #include <util/std_expr.h>
17 #include <util/rename.h>
18 #include <util/cprover_prefix.h>
19 
20 #include <util/c_types.h>
21 
23  const exprt &expr,
24  goto_programt &dest)
25 {
26  const source_locationt source_location=expr.find_source_location();
27 
28  symbolt &new_symbol=
30  expr.type(),
32  "literal",
33  source_location,
34  irep_idt(),
35  symbol_table);
36  new_symbol.is_static_lifetime=source_location.get_function().empty();
37  new_symbol.value=expr;
38 
39  // The value might depend on a variable, thus
40  // generate code for this.
41 
42  symbol_exprt result=new_symbol.symbol_expr();
43  result.add_source_location()=source_location;
44 
45  // The lifetime of compound literals is really that of
46  // the block they are in.
47  copy(code_declt(result), DECL, dest);
48 
49  code_assignt code_assign(result, expr);
50  code_assign.add_source_location()=source_location;
51  convert(code_assign, dest);
52 
53  // now create a 'dead' instruction
54  if(!new_symbol.is_static_lifetime)
55  {
56  code_deadt code_dead(result);
57  targets.destructor_stack.push_back(code_dead);
58  }
59 
60  return result;
61 }
62 
64 {
65  if(expr.id()==ID_dereference ||
66  expr.id()==ID_side_effect ||
67  expr.id()==ID_compound_literal ||
68  expr.id()==ID_comma)
69  return true;
70 
71  if(expr.id()==ID_index)
72  {
73  // Will usually clean index expressions because of possible
74  // memory violation in case of out-of-bounds indices.
75  // We do an exception for "string-lit"[0], which is safe.
76  if(to_index_expr(expr).array().id()==ID_string_constant &&
77  to_index_expr(expr).index().is_zero())
78  return false;
79 
80  return true;
81  }
82 
83  // We can't flatten quantified expressions by introducing new literals for
84  // conditional expressions. This is because the body of the quantified
85  // may refer to bound variables, which are not visible outside the scope
86  // of the quantifier.
87  //
88  // For example, the following transformation would not be valid:
89  //
90  // forall (i : int) (i == 0 || i > 10)
91  //
92  // transforming to
93  //
94  // g1 = (i == 0)
95  // g2 = (i > 10)
96  // forall (i : int) (g1 || g2)
97  if(expr.id()==ID_forall || expr.id()==ID_exists)
98  return false;
99 
100  forall_operands(it, expr)
101  if(needs_cleaning(*it))
102  return true;
103 
104  return false;
105 }
106 
109 {
110  assert(expr.id()==ID_and || expr.id()==ID_or);
111 
112  if(!expr.is_boolean())
113  {
115  error() << "`" << expr.id() << "' must be Boolean, but got "
116  << expr.pretty() << eom;
117  throw 0;
118  }
119 
120  // re-write "a && b" into nested a?b:0
121  // re-write "a || b" into nested a?1:b
122 
123  exprt tmp;
124 
125  if(expr.id()==ID_and)
126  tmp=true_exprt();
127  else // ID_or
128  tmp=false_exprt();
129 
130  exprt::operandst &ops=expr.operands();
131 
132  // start with last one
133  for(exprt::operandst::reverse_iterator
134  it=ops.rbegin();
135  it!=ops.rend();
136  ++it)
137  {
138  exprt &op=*it;
139 
140  if(!op.is_boolean())
141  {
143  error() << "`" << expr.id() << "' takes Boolean "
144  << "operands only, but got " << op.pretty() << eom;
145  throw 0;
146  }
147 
148  if(expr.id()==ID_and)
149  {
150  if_exprt if_e(op, tmp, false_exprt());
151  tmp.swap(if_e);
152  }
153  else // ID_or
154  {
155  if_exprt if_e(op, true_exprt(), tmp);
156  tmp.swap(if_e);
157  }
158  }
159 
160  expr.swap(tmp);
161 }
162 
164  exprt &expr,
165  goto_programt &dest,
166  bool result_is_used)
167 {
168  // this cleans:
169  // && || ?: comma (control-dependency)
170  // function calls
171  // object constructors like arrays, string constants, structs
172  // ++ -- (pre and post)
173  // compound assignments
174  // compound literals
175 
176  if(!needs_cleaning(expr))
177  return;
178 
179  if(expr.id()==ID_and || expr.id()==ID_or)
180  {
181  // rewrite into ?:
182  rewrite_boolean(expr);
183 
184  // recursive call
185  clean_expr(expr, dest, result_is_used);
186  return;
187  }
188  else if(expr.id()==ID_if)
189  {
190  // first clean condition
191  clean_expr(to_if_expr(expr).cond(), dest, true);
192 
193  // possibly done now
194  if(!needs_cleaning(to_if_expr(expr).true_case()) &&
195  !needs_cleaning(to_if_expr(expr).false_case()))
196  return;
197 
198  // copy expression
199  if_exprt if_expr=to_if_expr(expr);
200 
201  if(!if_expr.cond().is_boolean())
202  {
204  error() << "first argument of `if' must be boolean, but got "
205  << if_expr.cond().pretty() << eom;
206  throw 0;
207  }
208 
209  const source_locationt source_location=expr.find_source_location();
210 
211  #if 0
212  // We do some constant-folding here, to mimic
213  // what typical compilers do.
214  {
215  exprt tmp_cond=if_expr.cond();
216  simplify(tmp_cond, ns);
217  if(tmp_cond.is_true())
218  {
219  clean_expr(if_expr.true_case(), dest, result_is_used);
220  expr=if_expr.true_case();
221  return;
222  }
223  else if(tmp_cond.is_false())
224  {
225  clean_expr(if_expr.false_case(), dest, result_is_used);
226  expr=if_expr.false_case();
227  return;
228  }
229  }
230  #endif
231 
232  goto_programt tmp_true;
233  clean_expr(if_expr.true_case(), tmp_true, result_is_used);
234 
235  goto_programt tmp_false;
236  clean_expr(if_expr.false_case(), tmp_false, result_is_used);
237 
238  if(result_is_used)
239  {
240  symbolt &new_symbol=
241  new_tmp_symbol(expr.type(), "if_expr", dest, source_location);
242 
243  code_assignt assignment_true;
244  assignment_true.lhs()=new_symbol.symbol_expr();
245  assignment_true.rhs()=if_expr.true_case();
246  assignment_true.add_source_location()=source_location;
247  convert(assignment_true, tmp_true);
248 
249  code_assignt assignment_false;
250  assignment_false.lhs()=new_symbol.symbol_expr();
251  assignment_false.rhs()=if_expr.false_case();
252  assignment_false.add_source_location()=source_location;
253  convert(assignment_false, tmp_false);
254 
255  // overwrites expr
256  expr=new_symbol.symbol_expr();
257  }
258  else
259  {
260  // preserve the expressions for possible later checks
261  if(if_expr.true_case().is_not_nil())
262  {
263  code_expressiont code_expression(if_expr.true_case());
264  convert(code_expression, tmp_true);
265  }
266 
267  if(if_expr.false_case().is_not_nil())
268  {
269  code_expressiont code_expression(if_expr.false_case());
270  convert(code_expression, tmp_false);
271  }
272 
273  expr=nil_exprt();
274  }
275 
276  // generate guard for argument side-effects
278  if_expr.cond(), tmp_true, tmp_false,
279  source_location, dest);
280 
281  return;
282  }
283  else if(expr.id()==ID_comma)
284  {
285  if(result_is_used)
286  {
287  exprt result;
288 
289  Forall_operands(it, expr)
290  {
291  bool last=(it==--expr.operands().end());
292 
293  // special treatment for last one
294  if(last)
295  {
296  result.swap(*it);
297  clean_expr(result, dest, true);
298  }
299  else
300  {
301  clean_expr(*it, dest, false);
302 
303  // remember these for later checks
304  if(it->is_not_nil())
305  convert(code_expressiont(*it), dest);
306  }
307  }
308 
309  expr.swap(result);
310  }
311  else // result not used
312  {
313  Forall_operands(it, expr)
314  {
315  clean_expr(*it, dest, false);
316 
317  // remember as expression statement for later checks
318  if(it->is_not_nil())
319  convert(code_expressiont(*it), dest);
320  }
321 
322  expr=nil_exprt();
323  }
324 
325  return;
326  }
327  else if(expr.id()==ID_typecast)
328  {
329  if(expr.operands().size()!=1)
330  {
332  error() << "typecast takes one argument" << eom;
333  throw 0;
334  }
335 
336  // preserve 'result_is_used'
337  clean_expr(expr.op0(), dest, result_is_used);
338 
339  if(expr.op0().is_nil())
340  expr.make_nil();
341 
342  return;
343  }
344  else if(expr.id()==ID_side_effect)
345  {
346  // some of the side-effects need special treatment!
347  const irep_idt statement=to_side_effect_expr(expr).get_statement();
348 
349  if(statement==ID_gcc_conditional_expression)
350  {
351  // need to do separately
353  return;
354  }
355  else if(statement==ID_statement_expression)
356  {
357  // need to do separately to prevent that
358  // the operands of expr get 'cleaned'
360  to_side_effect_expr(expr), dest, result_is_used);
361  return;
362  }
363  else if(statement==ID_assign)
364  {
365  // we do a special treatment for x=f(...)
366  assert(expr.operands().size()==2);
367 
368  if(expr.op1().id()==ID_side_effect &&
369  to_side_effect_expr(expr.op1()).get_statement()==ID_function_call)
370  {
371  clean_expr(expr.op0(), dest);
372  exprt lhs=expr.op0();
373 
374  // turn into code
375  code_assignt assignment;
376  assignment.lhs()=lhs;
377  assignment.rhs()=expr.op1();
378  assignment.add_source_location()=expr.source_location();
379  convert_assign(assignment, dest);
380 
381  if(result_is_used)
382  expr.swap(lhs);
383  else
384  expr.make_nil();
385  return;
386  }
387  }
388  else if(statement==ID_function_call)
389  {
390  if(to_side_effect_expr_function_call(expr).function().id()==ID_symbol &&
393  function()).get_identifier()=="__noop")
394  {
395  // __noop needs special treatment, as arguments are not
396  // evaluated
398  }
399  }
400  }
401  else if(expr.id()==ID_forall || expr.id()==ID_exists)
402  {
403  assert(expr.operands().size()==2);
404  // check if there are side-effects
405  goto_programt tmp;
406  clean_expr(expr.op1(), tmp, true);
407  if(tmp.instructions.empty())
408  {
410  error() << "no side-effects in quantified expressions allowed"
411  << eom;
412  throw 0;
413  }
414  return;
415  }
416  else if(expr.id()==ID_address_of)
417  {
418  assert(expr.operands().size()==1);
419  clean_expr_address_of(expr.op0(), dest);
420  return;
421  }
422 
423  // TODO: evaluation order
424 
425  Forall_operands(it, expr)
426  clean_expr(*it, dest);
427 
428  if(expr.id()==ID_side_effect)
429  {
430  remove_side_effect(to_side_effect_expr(expr), dest, result_is_used);
431  }
432  else if(expr.id()==ID_compound_literal)
433  {
434  // This is simply replaced by the literal
435  assert(expr.operands().size()==1);
436  expr=expr.op0();
437  }
438 }
439 
441  exprt &expr,
442  goto_programt &dest)
443 {
444  // The address of object constructors can be taken,
445  // which is re-written into the address of a variable.
446 
447  if(expr.id()==ID_compound_literal)
448  {
449  assert(expr.operands().size()==1);
450  clean_expr(expr.op0(), dest);
451  expr=make_compound_literal(expr.op0(), dest);
452  }
453  else if(expr.id()==ID_string_constant)
454  {
455  // Leave for now, but long-term these might become static symbols.
456  // LLVM appears to do precisely that.
457  }
458  else if(expr.id()==ID_index)
459  {
460  assert(expr.operands().size()==2);
461  clean_expr_address_of(expr.op0(), dest);
462  clean_expr(expr.op1(), dest);
463  }
464  else if(expr.id()==ID_dereference)
465  {
466  assert(expr.operands().size()==1);
467  clean_expr(expr.op0(), dest);
468  }
469  else if(expr.id()==ID_comma)
470  {
471  // Yes, one can take the address of a comma expression.
472  // Treatment is similar to clean_expr() above.
473 
474  exprt result;
475 
476  Forall_operands(it, expr)
477  {
478  bool last=(it==--expr.operands().end());
479 
480  // special treatment for last one
481  if(last)
482  result.swap(*it);
483  else
484  {
485  clean_expr(*it, dest, false);
486 
487  // get any side-effects
488  if(it->is_not_nil())
489  convert(code_expressiont(*it), dest);
490  }
491  }
492 
493  expr.swap(result);
494 
495  // do again
496  clean_expr_address_of(expr, dest);
497  }
498  else
499  Forall_operands(it, expr)
500  clean_expr_address_of(*it, dest);
501 }
502 
504  exprt &expr,
505  goto_programt &dest)
506 {
507  if(expr.operands().size()!=2)
508  {
510  error() << "conditional_expression takes two operands" << eom;
511  throw 0;
512  }
513 
514  // first remove side-effects from condition
515  clean_expr(expr.op0(), dest);
516 
517  // now we can copy op0 safely
518  if_exprt if_expr;
519 
520  if_expr.cond()=expr.op0();
521  if_expr.true_case()=expr.op0();
522  if_expr.false_case()=expr.op1();
523  if_expr.type()=expr.type();
524  if_expr.add_source_location()=expr.source_location();
525 
526  if(if_expr.cond().type()!=bool_typet())
527  if_expr.cond().make_typecast(bool_typet());
528 
529  expr.swap(if_expr);
530 
531  // there might still be junk in expr.op2()
532  clean_expr(expr, dest);
533 }
symbol_exprt make_compound_literal(const exprt &expr, goto_programt &dest)
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Definition: std_code.h:1083
mstreamt & result()
Definition: message.h:233
exprt & true_case()
Definition: std_expr.h:2805
bool is_boolean() const
Definition: expr.cpp:231
bool is_nil() const
Definition: irep.h:103
bool is_not_nil() const
Definition: irep.h:104
void convert(const codet &code, goto_programt &dest)
converts &#39;code&#39; and appends the result to &#39;dest&#39;
symbol_tablet & symbol_table
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, symbol_tablet &symbol_table)
Installs a fresh-named symbol with the requested name pattern.
exprt & op0()
Definition: expr.h:84
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
struct goto_convertt::targetst targets
Fresh auxiliary symbol creation.
bool is_false() const
Definition: expr.cpp:140
void convert_assign(const code_assignt &code, goto_programt &dest)
exprt value
Initial value of symbol.
Definition: symbol.h:40
The trinary if-then-else operator.
Definition: std_expr.h:2771
exprt & cond()
Definition: std_expr.h:2795
bool is_true() const
Definition: expr.cpp:133
typet & type()
Definition: expr.h:60
The proper Booleans.
Definition: std_types.h:33
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
An expression statement.
Definition: std_code.h:957
void remove_statement_expression(side_effect_exprt &expr, goto_programt &dest, bool result_is_used)
bool is_static_lifetime
Definition: symbol.h:70
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1023
destructor_stackt destructor_stack
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1229
const irep_idt & id() const
Definition: irep.h:189
exprt & lhs()
Definition: std_code.h:157
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:191
The boolean constant true.
Definition: std_expr.h:3742
std::string tmp_symbol_prefix
A declaration of a local variable.
Definition: std_code.h:192
void clean_expr_address_of(exprt &expr, goto_programt &dest)
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:2836
The NIL expression.
Definition: std_expr.h:3764
exprt & rhs()
Definition: std_code.h:162
const source_locationt & find_source_location() const
Definition: expr.cpp:466
source_locationt source_location
Definition: message.h:175
Program Transformation.
API to expression classes.
void remove_gcc_conditional_expression(exprt &expr, goto_programt &dest)
exprt & op1()
Definition: expr.h:87
#define forall_operands(it, expr)
Definition: expr.h:17
void clean_expr(exprt &expr, goto_programt &dest, bool result_is_used=true)
exprt & false_case()
Definition: std_expr.h:2815
The boolean constant false.
Definition: std_expr.h:3753
std::vector< exprt > operandst
Definition: expr.h:49
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
static bool needs_cleaning(const exprt &expr)
void remove_side_effect(side_effect_exprt &expr, goto_programt &dest, bool result_is_used)
exprt & index()
Definition: std_expr.h:1208
symbolt & new_tmp_symbol(const typet &type, const std::string &suffix, goto_programt &dest, const source_locationt &)
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
source_locationt & add_source_location()
Definition: type.h:100
const source_locationt & source_location() const
Definition: expr.h:142
exprt::operandst & arguments()
Definition: std_code.h:1071
A removal of a local variable.
Definition: std_code.h:234
void make_nil()
Definition: irep.h:243
void swap(irept &irep)
Definition: irep.h:231
#define Forall_operands(it, expr)
Definition: expr.h:23
mstreamt & error()
Definition: message.h:223
bool is_zero() const
Definition: expr.cpp:236
source_locationt & add_source_location()
Definition: expr.h:147
Expression to hold a symbol (variable)
Definition: std_expr.h:82
void copy(const codet &code, goto_program_instruction_typet type, goto_programt &dest)
dstringt irep_idt
Definition: irep.h:32
operandst & operands()
Definition: expr.h:70
void rewrite_boolean(exprt &dest)
re-write boolean operators into ?:
exprt & array()
Definition: std_expr.h:1198
Assignment.
Definition: std_code.h:144
const irep_idt & get_statement() const
Definition: std_code.h:1012
bool simplify(exprt &expr, const namespacet &ns)
void generate_ifthenelse(const exprt &cond, goto_programt &true_case, goto_programt &false_case, const source_locationt &, goto_programt &dest)
if(guard) true_case; else false_case;