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/cprover_prefix.h>
18 
19 #include <util/c_types.h>
20 
22  const exprt &expr,
23  goto_programt &dest,
24  const irep_idt &mode)
25 {
26  const source_locationt source_location=expr.find_source_location();
27 
28  symbolt &new_symbol = get_fresh_aux_symbol(
29  expr.type(),
31  "literal",
32  source_location,
33  mode,
34  symbol_table);
35  new_symbol.is_static_lifetime=source_location.get_function().empty();
36  new_symbol.value=expr;
37 
38  // The value might depend on a variable, thus
39  // generate code for this.
40 
41  symbol_exprt result=new_symbol.symbol_expr();
42  result.add_source_location()=source_location;
43 
44  // The lifetime of compound literals is really that of
45  // the block they are in.
46  copy(code_declt(result), DECL, dest);
47 
48  code_assignt code_assign(result, expr);
49  code_assign.add_source_location()=source_location;
50  convert(code_assign, dest, mode);
51 
52  // now create a 'dead' instruction
53  if(!new_symbol.is_static_lifetime)
54  {
55  code_deadt code_dead(result);
56  targets.destructor_stack.push_back(code_dead);
57  }
58 
59  return result;
60 }
61 
63 {
64  if(expr.id()==ID_dereference ||
65  expr.id()==ID_side_effect ||
66  expr.id()==ID_compound_literal ||
67  expr.id()==ID_comma)
68  return true;
69 
70  if(expr.id()==ID_index)
71  {
72  // Will usually clean index expressions because of possible
73  // memory violation in case of out-of-bounds indices.
74  // We do an exception for "string-lit"[0], which is safe.
75  if(to_index_expr(expr).array().id()==ID_string_constant &&
76  to_index_expr(expr).index().is_zero())
77  return false;
78 
79  return true;
80  }
81 
82  // We can't flatten quantified expressions by introducing new literals for
83  // conditional expressions. This is because the body of the quantified
84  // may refer to bound variables, which are not visible outside the scope
85  // of the quantifier.
86  //
87  // For example, the following transformation would not be valid:
88  //
89  // forall (i : int) (i == 0 || i > 10)
90  //
91  // transforming to
92  //
93  // g1 = (i == 0)
94  // g2 = (i > 10)
95  // forall (i : int) (g1 || g2)
96  if(expr.id()==ID_forall || expr.id()==ID_exists)
97  return false;
98 
99  forall_operands(it, expr)
100  if(needs_cleaning(*it))
101  return true;
102 
103  return false;
104 }
105 
108 {
109  assert(expr.id()==ID_and || expr.id()==ID_or);
110 
111  if(!expr.is_boolean())
112  {
114  error() << "`" << expr.id() << "' must be Boolean, but got "
115  << expr.pretty() << eom;
116  throw 0;
117  }
118 
119  // re-write "a && b" into nested a?b:0
120  // re-write "a || b" into nested a?1:b
121 
122  exprt tmp;
123 
124  if(expr.id()==ID_and)
125  tmp=true_exprt();
126  else // ID_or
127  tmp=false_exprt();
128 
129  exprt::operandst &ops=expr.operands();
130 
131  // start with last one
132  for(exprt::operandst::reverse_iterator
133  it=ops.rbegin();
134  it!=ops.rend();
135  ++it)
136  {
137  exprt &op=*it;
138 
139  if(!op.is_boolean())
140  {
142  error() << "`" << expr.id() << "' takes Boolean "
143  << "operands only, but got " << op.pretty() << eom;
144  throw 0;
145  }
146 
147  if(expr.id()==ID_and)
148  {
149  if_exprt if_e(op, tmp, false_exprt());
150  tmp.swap(if_e);
151  }
152  else // ID_or
153  {
154  if_exprt if_e(op, true_exprt(), tmp);
155  tmp.swap(if_e);
156  }
157  }
158 
159  expr.swap(tmp);
160 }
161 
163  exprt &expr,
164  goto_programt &dest,
165  const irep_idt &mode,
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, mode, 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, mode, 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, mode, result_is_used);
234 
235  goto_programt tmp_false;
236  clean_expr(if_expr.false_case(), tmp_false, mode, 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, mode);
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, mode);
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, mode);
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  // add a (void) type cast so that is_skip catches it in case the
264  // expression is just a constant
265  code_expressiont code_expression(
266  typecast_exprt(if_expr.true_case(), empty_typet()));
267  convert(code_expression, tmp_true, mode);
268  }
269 
270  if(if_expr.false_case().is_not_nil())
271  {
272  // add a (void) type cast so that is_skip catches it in case the
273  // expression is just a constant
274  code_expressiont code_expression(
275  typecast_exprt(if_expr.false_case(), empty_typet()));
276  convert(code_expression, tmp_false, mode);
277  }
278 
279  expr=nil_exprt();
280  }
281 
282  // generate guard for argument side-effects
284  if_expr.cond(), tmp_true, tmp_false, source_location, dest, mode);
285 
286  return;
287  }
288  else if(expr.id()==ID_comma)
289  {
290  if(result_is_used)
291  {
292  exprt result;
293 
294  Forall_operands(it, expr)
295  {
296  bool last=(it==--expr.operands().end());
297 
298  // special treatment for last one
299  if(last)
300  {
301  result.swap(*it);
302  clean_expr(result, dest, mode, true);
303  }
304  else
305  {
306  clean_expr(*it, dest, mode, false);
307 
308  // remember these for later checks
309  if(it->is_not_nil())
310  convert(code_expressiont(*it), dest, mode);
311  }
312  }
313 
314  expr.swap(result);
315  }
316  else // result not used
317  {
318  Forall_operands(it, expr)
319  {
320  clean_expr(*it, dest, mode, false);
321 
322  // remember as expression statement for later checks
323  if(it->is_not_nil())
324  convert(code_expressiont(*it), dest, mode);
325  }
326 
327  expr=nil_exprt();
328  }
329 
330  return;
331  }
332  else if(expr.id()==ID_typecast)
333  {
334  if(expr.operands().size()!=1)
335  {
337  error() << "typecast takes one argument" << eom;
338  throw 0;
339  }
340 
341  // preserve 'result_is_used'
342  clean_expr(expr.op0(), dest, mode, result_is_used);
343 
344  if(expr.op0().is_nil())
345  expr.make_nil();
346 
347  return;
348  }
349  else if(expr.id()==ID_side_effect)
350  {
351  // some of the side-effects need special treatment!
352  const irep_idt statement=to_side_effect_expr(expr).get_statement();
353 
354  if(statement==ID_gcc_conditional_expression)
355  {
356  // need to do separately
357  remove_gcc_conditional_expression(expr, dest, mode);
358  return;
359  }
360  else if(statement==ID_statement_expression)
361  {
362  // need to do separately to prevent that
363  // the operands of expr get 'cleaned'
365  to_side_effect_expr(expr), dest, mode, result_is_used);
366  return;
367  }
368  else if(statement==ID_assign)
369  {
370  // we do a special treatment for x=f(...)
371  assert(expr.operands().size()==2);
372 
373  if(expr.op1().id()==ID_side_effect &&
374  to_side_effect_expr(expr.op1()).get_statement()==ID_function_call)
375  {
376  clean_expr(expr.op0(), dest, mode);
377  exprt lhs=expr.op0();
378 
379  // turn into code
380  code_assignt assignment;
381  assignment.lhs()=lhs;
382  assignment.rhs()=expr.op1();
383  assignment.add_source_location()=expr.source_location();
384  convert_assign(assignment, dest, mode);
385 
386  if(result_is_used)
387  expr.swap(lhs);
388  else
389  expr.make_nil();
390  return;
391  }
392  }
393  else if(statement==ID_function_call)
394  {
395  if(to_side_effect_expr_function_call(expr).function().id()==ID_symbol &&
398  function()).get_identifier()=="__noop")
399  {
400  // __noop needs special treatment, as arguments are not
401  // evaluated
403  }
404  }
405  }
406  else if(expr.id()==ID_forall || expr.id()==ID_exists)
407  {
408  assert(expr.operands().size()==2);
409  // check if there are side-effects
410  goto_programt tmp;
411  clean_expr(expr.op1(), tmp, mode, true);
412  if(tmp.instructions.empty())
413  {
415  error() << "no side-effects in quantified expressions allowed"
416  << eom;
417  throw 0;
418  }
419  return;
420  }
421  else if(expr.id()==ID_address_of)
422  {
423  assert(expr.operands().size()==1);
424  clean_expr_address_of(expr.op0(), dest, mode);
425  return;
426  }
427 
428  // TODO: evaluation order
429 
430  Forall_operands(it, expr)
431  clean_expr(*it, dest, mode);
432 
433  if(expr.id()==ID_side_effect)
434  {
435  remove_side_effect(to_side_effect_expr(expr), dest, mode, result_is_used);
436  }
437  else if(expr.id()==ID_compound_literal)
438  {
439  // This is simply replaced by the literal
440  assert(expr.operands().size()==1);
441  expr=expr.op0();
442  }
443 }
444 
446  exprt &expr,
447  goto_programt &dest,
448  const irep_idt &mode)
449 {
450  // The address of object constructors can be taken,
451  // which is re-written into the address of a variable.
452 
453  if(expr.id()==ID_compound_literal)
454  {
455  assert(expr.operands().size()==1);
456  clean_expr(expr.op0(), dest, mode);
457  expr = make_compound_literal(expr.op0(), dest, mode);
458  }
459  else if(expr.id()==ID_string_constant)
460  {
461  // Leave for now, but long-term these might become static symbols.
462  // LLVM appears to do precisely that.
463  }
464  else if(expr.id()==ID_index)
465  {
466  assert(expr.operands().size()==2);
467  clean_expr_address_of(expr.op0(), dest, mode);
468  clean_expr(expr.op1(), dest, mode);
469  }
470  else if(expr.id()==ID_dereference)
471  {
472  assert(expr.operands().size()==1);
473  clean_expr(expr.op0(), dest, mode);
474  }
475  else if(expr.id()==ID_comma)
476  {
477  // Yes, one can take the address of a comma expression.
478  // Treatment is similar to clean_expr() above.
479 
480  exprt result;
481 
482  Forall_operands(it, expr)
483  {
484  bool last=(it==--expr.operands().end());
485 
486  // special treatment for last one
487  if(last)
488  result.swap(*it);
489  else
490  {
491  clean_expr(*it, dest, mode, false);
492 
493  // get any side-effects
494  if(it->is_not_nil())
495  convert(code_expressiont(*it), dest, mode);
496  }
497  }
498 
499  expr.swap(result);
500 
501  // do again
502  clean_expr_address_of(expr, dest, mode);
503  }
504  else
505  Forall_operands(it, expr)
506  clean_expr_address_of(*it, dest, mode);
507 }
508 
510  exprt &expr,
511  goto_programt &dest,
512  const irep_idt &mode)
513 {
514  if(expr.operands().size()!=2)
515  {
517  error() << "conditional_expression takes two operands" << eom;
518  throw 0;
519  }
520 
521  // first remove side-effects from condition
522  clean_expr(expr.op0(), dest, mode);
523 
524  // now we can copy op0 safely
525  if_exprt if_expr;
526 
527  if_expr.cond()=expr.op0();
528  if_expr.true_case()=expr.op0();
529  if_expr.false_case()=expr.op1();
530  if_expr.type()=expr.type();
531  if_expr.add_source_location()=expr.source_location();
532 
533  if(if_expr.cond().type()!=bool_typet())
534  if_expr.cond().make_typecast(bool_typet());
535 
536  expr.swap(if_expr);
537 
538  // there might still be junk in expr.op2()
539  clean_expr(expr, dest, mode);
540 }
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:3426
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Definition: std_code.h:1392
exprt & true_case()
Definition: std_expr.h:3395
semantic type conversion
Definition: std_expr.h:2111
bool is_boolean() const
Definition: expr.cpp:156
bool is_nil() const
Definition: irep.h:102
bool is_not_nil() const
Definition: irep.h:103
exprt & op0()
Definition: expr.h:72
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
struct goto_convertt::targetst targets
void convert(const codet &code, goto_programt &dest, const irep_idt &mode)
converts &#39;code&#39; and appends the result to &#39;dest&#39;
void generate_ifthenelse(const exprt &cond, goto_programt &true_case, goto_programt &false_case, const source_locationt &, goto_programt &dest, const irep_idt &mode)
if(guard) true_case; else false_case;
Fresh auxiliary symbol creation.
bool is_false() const
Definition: expr.cpp:131
exprt value
Initial value of symbol.
Definition: symbol.h:37
The trinary if-then-else operator.
Definition: std_expr.h:3361
exprt & cond()
Definition: std_expr.h:3385
bool is_true() const
Definition: expr.cpp:124
typet & type()
Definition: expr.h:56
void clean_expr_address_of(exprt &expr, goto_programt &dest, const irep_idt &mode)
The proper Booleans.
Definition: std_types.h:34
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
An expression statement.
Definition: std_code.h:1188
bool is_static_lifetime
Definition: symbol.h:67
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1287
destructor_stackt destructor_stack
const irep_idt & id() const
Definition: irep.h:189
exprt & lhs()
Definition: std_code.h:208
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:111
The boolean constant true.
Definition: std_expr.h:4488
void clean_expr(exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used=true)
std::string tmp_symbol_prefix
A declaration of a local variable.
Definition: std_code.h:253
The NIL expression.
Definition: std_expr.h:4510
exprt & rhs()
Definition: std_code.h:213
const source_locationt & find_source_location() const
Definition: expr.cpp:246
source_locationt source_location
Definition: message.h:214
The empty type.
Definition: std_types.h:54
Program Transformation.
API to expression classes.
exprt & op1()
Definition: expr.h:75
mstreamt & error() const
Definition: message.h:302
void convert_assign(const code_assignt &code, goto_programt &dest, const irep_idt &mode)
#define forall_operands(it, expr)
Definition: expr.h:17
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
exprt & false_case()
Definition: std_expr.h:3405
The boolean constant false.
Definition: std_expr.h:4499
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
void remove_statement_expression(side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used)
static bool needs_cleaning(const exprt &expr)
mstreamt & result() const
Definition: message.h:312
exprt & index()
Definition: std_expr.h:1496
void remove_gcc_conditional_expression(exprt &expr, goto_programt &dest, const irep_idt &mode)
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_table_baset &symbol_table)
Installs a fresh-named symbol with the requested name pattern.
Base class for all expressions.
Definition: expr.h:42
symbol_exprt make_compound_literal(const exprt &expr, goto_programt &dest, const irep_idt &mode)
source_locationt & add_source_location()
Definition: type.h:102
const source_locationt & source_location() const
Definition: expr.h:125
symbolt & new_tmp_symbol(const typet &type, const std::string &suffix, goto_programt &dest, const source_locationt &, const irep_idt &mode)
exprt::operandst & arguments()
Definition: std_code.h:1371
symbol_table_baset & symbol_table
A removal of a local variable.
Definition: std_code.h:305
void make_nil()
Definition: irep.h:243
void swap(irept &irep)
Definition: irep.h:231
#define Forall_operands(it, expr)
Definition: expr.h:23
bool is_zero() const
Definition: expr.cpp:161
source_locationt & add_source_location()
Definition: expr.h:130
void remove_side_effect(side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used)
Expression to hold a symbol (variable)
Definition: std_expr.h:90
void copy(const codet &code, goto_program_instruction_typet type, goto_programt &dest)
operandst & operands()
Definition: expr.h:66
void rewrite_boolean(exprt &dest)
re-write boolean operators into ?:
exprt & array()
Definition: std_expr.h:1486
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1517
Assignment.
Definition: std_code.h:195
const irep_idt & get_statement() const
Definition: std_code.h:1253
bool simplify(exprt &expr, const namespacet &ns)