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/cprover_prefix.h>
15 #include <util/exception_utils.h>
16 #include <util/expr_util.h>
17 #include <util/fresh_symbol.h>
18 #include <util/simplify_expr.h>
19 #include <util/std_expr.h>
20 
21 #include <util/c_types.h>
22 
24  const exprt &expr,
25  goto_programt &dest,
26  const irep_idt &mode)
27 {
28  const source_locationt source_location=expr.find_source_location();
29 
30  symbolt &new_symbol = get_fresh_aux_symbol(
31  expr.type(),
33  "literal",
34  source_location,
35  mode,
36  symbol_table);
37  new_symbol.is_static_lifetime=source_location.get_function().empty();
38  new_symbol.value=expr;
39 
40  // The value might depend on a variable, thus
41  // generate code for this.
42 
43  symbol_exprt result=new_symbol.symbol_expr();
44  result.add_source_location()=source_location;
45 
46  // The lifetime of compound literals is really that of
47  // the block they are in.
48  copy(code_declt(result), DECL, dest);
49 
50  code_assignt code_assign(result, expr);
51  code_assign.add_source_location()=source_location;
52  convert(code_assign, dest, mode);
53 
54  // now create a 'dead' instruction
55  if(!new_symbol.is_static_lifetime)
56  {
57  code_deadt code_dead(result);
58  targets.destructor_stack.push_back(code_dead);
59  }
60 
61  return result;
62 }
63 
65 {
66  if(expr.id()==ID_dereference ||
67  expr.id()==ID_side_effect ||
68  expr.id()==ID_compound_literal ||
69  expr.id()==ID_comma)
70  return true;
71 
72  if(expr.id()==ID_index)
73  {
74  // Will usually clean index expressions because of possible
75  // memory violation in case of out-of-bounds indices.
76  // We do an exception for "string-lit"[0], which is safe.
77  if(to_index_expr(expr).array().id()==ID_string_constant &&
78  to_index_expr(expr).index().is_zero())
79  return false;
80 
81  return true;
82  }
83 
84  // We can't flatten quantified expressions by introducing new literals for
85  // conditional expressions. This is because the body of the quantified
86  // may refer to bound variables, which are not visible outside the scope
87  // of the quantifier.
88  //
89  // For example, the following transformation would not be valid:
90  //
91  // forall (i : int) (i == 0 || i > 10)
92  //
93  // transforming to
94  //
95  // g1 = (i == 0)
96  // g2 = (i > 10)
97  // forall (i : int) (g1 || g2)
98  if(expr.id()==ID_forall || expr.id()==ID_exists)
99  return false;
100 
101  forall_operands(it, expr)
102  if(needs_cleaning(*it))
103  return true;
104 
105  return false;
106 }
107 
110 {
111  PRECONDITION(expr.id() == ID_and || expr.id() == ID_or);
113  expr.is_boolean(),
114  expr.find_source_location(),
115  "'",
116  expr.id(),
117  "' must be Boolean, but got ",
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 
141  op.is_boolean(),
142  "boolean operators must have only boolean operands",
143  expr.find_source_location());
144 
145  if(expr.id()==ID_and)
146  {
147  if_exprt if_e(op, tmp, false_exprt());
148  tmp.swap(if_e);
149  }
150  else // ID_or
151  {
152  if_exprt if_e(op, true_exprt(), tmp);
153  tmp.swap(if_e);
154  }
155  }
156 
157  expr.swap(tmp);
158 }
159 
161  exprt &expr,
162  goto_programt &dest,
163  const irep_idt &mode,
164  bool result_is_used)
165 {
166  // this cleans:
167  // && || ?: comma (control-dependency)
168  // function calls
169  // object constructors like arrays, string constants, structs
170  // ++ -- (pre and post)
171  // compound assignments
172  // compound literals
173 
174  if(!needs_cleaning(expr))
175  return;
176 
177  if(expr.id()==ID_and || expr.id()==ID_or)
178  {
179  // rewrite into ?:
180  rewrite_boolean(expr);
181 
182  // recursive call
183  clean_expr(expr, dest, mode, result_is_used);
184  return;
185  }
186  else if(expr.id()==ID_if)
187  {
188  // first clean condition
189  clean_expr(to_if_expr(expr).cond(), dest, mode, true);
190 
191  // possibly done now
192  if(!needs_cleaning(to_if_expr(expr).true_case()) &&
193  !needs_cleaning(to_if_expr(expr).false_case()))
194  return;
195 
196  // copy expression
197  if_exprt if_expr=to_if_expr(expr);
198 
200  if_expr.cond().is_boolean(),
201  "condition for an 'if' must be boolean",
202  if_expr.find_source_location());
203 
204  const source_locationt source_location=expr.find_source_location();
205 
206  #if 0
207  // We do some constant-folding here, to mimic
208  // what typical compilers do.
209  {
210  exprt tmp_cond=if_expr.cond();
211  simplify(tmp_cond, ns);
212  if(tmp_cond.is_true())
213  {
214  clean_expr(if_expr.true_case(), dest, result_is_used);
215  expr=if_expr.true_case();
216  return;
217  }
218  else if(tmp_cond.is_false())
219  {
220  clean_expr(if_expr.false_case(), dest, result_is_used);
221  expr=if_expr.false_case();
222  return;
223  }
224  }
225  #endif
226 
227  goto_programt tmp_true;
228  clean_expr(if_expr.true_case(), tmp_true, mode, result_is_used);
229 
230  goto_programt tmp_false;
231  clean_expr(if_expr.false_case(), tmp_false, mode, result_is_used);
232 
233  if(result_is_used)
234  {
235  symbolt &new_symbol =
236  new_tmp_symbol(expr.type(), "if_expr", dest, source_location, mode);
237 
238  code_assignt assignment_true;
239  assignment_true.lhs()=new_symbol.symbol_expr();
240  assignment_true.rhs()=if_expr.true_case();
241  assignment_true.add_source_location()=source_location;
242  convert(assignment_true, tmp_true, mode);
243 
244  code_assignt assignment_false;
245  assignment_false.lhs()=new_symbol.symbol_expr();
246  assignment_false.rhs()=if_expr.false_case();
247  assignment_false.add_source_location()=source_location;
248  convert(assignment_false, tmp_false, mode);
249 
250  // overwrites expr
251  expr=new_symbol.symbol_expr();
252  }
253  else
254  {
255  // preserve the expressions for possible later checks
256  if(if_expr.true_case().is_not_nil())
257  {
258  // add a (void) type cast so that is_skip catches it in case the
259  // expression is just a constant
260  code_expressiont code_expression(
261  typecast_exprt(if_expr.true_case(), empty_typet()));
262  convert(code_expression, tmp_true, mode);
263  }
264 
265  if(if_expr.false_case().is_not_nil())
266  {
267  // add a (void) type cast so that is_skip catches it in case the
268  // expression is just a constant
269  code_expressiont code_expression(
270  typecast_exprt(if_expr.false_case(), empty_typet()));
271  convert(code_expression, tmp_false, mode);
272  }
273 
274  expr=nil_exprt();
275  }
276 
277  // generate guard for argument side-effects
279  if_expr.cond(), tmp_true, tmp_false, source_location, dest, mode);
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, mode, true);
298  }
299  else
300  {
301  clean_expr(*it, dest, mode, false);
302 
303  // remember these for later checks
304  if(it->is_not_nil())
305  convert(code_expressiont(*it), dest, mode);
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, mode, false);
316 
317  // remember as expression statement for later checks
318  if(it->is_not_nil())
319  convert(code_expressiont(*it), dest, mode);
320  }
321 
322  expr=nil_exprt();
323  }
324 
325  return;
326  }
327  else if(expr.id()==ID_typecast)
328  {
329  typecast_exprt &typecast = to_typecast_expr(expr);
330 
331  // preserve 'result_is_used'
332  clean_expr(typecast.op(), dest, mode, result_is_used);
333 
334  if(typecast.op().is_nil())
335  expr.make_nil();
336 
337  return;
338  }
339  else if(expr.id()==ID_side_effect)
340  {
341  // some of the side-effects need special treatment!
342  const irep_idt statement=to_side_effect_expr(expr).get_statement();
343 
344  if(statement==ID_gcc_conditional_expression)
345  {
346  // need to do separately
347  remove_gcc_conditional_expression(expr, dest, mode);
348  return;
349  }
350  else if(statement==ID_statement_expression)
351  {
352  // need to do separately to prevent that
353  // the operands of expr get 'cleaned'
355  to_side_effect_expr(expr), dest, mode, result_is_used);
356  return;
357  }
358  else if(statement==ID_assign)
359  {
360  // we do a special treatment for x=f(...)
361  INVARIANT(
362  expr.operands().size() == 2,
363  "side-effect assignment expressions must have two operands");
364 
365  if(expr.op1().id()==ID_side_effect &&
366  to_side_effect_expr(expr.op1()).get_statement()==ID_function_call)
367  {
368  clean_expr(expr.op0(), dest, mode);
369  exprt lhs=expr.op0();
370 
371  // turn into code
372  code_assignt assignment;
373  assignment.lhs()=lhs;
374  assignment.rhs()=expr.op1();
375  assignment.add_source_location()=expr.source_location();
376  convert_assign(assignment, dest, mode);
377 
378  if(result_is_used)
379  expr.swap(lhs);
380  else
381  expr.make_nil();
382  return;
383  }
384  }
385  else if(statement==ID_function_call)
386  {
387  if(to_side_effect_expr_function_call(expr).function().id()==ID_symbol &&
390  function()).get_identifier()=="__noop")
391  {
392  // __noop needs special treatment, as arguments are not
393  // evaluated
395  }
396  }
397  }
398  else if(expr.id()==ID_forall || expr.id()==ID_exists)
399  {
401  !has_subexpr(expr, ID_side_effect),
402  "the front-end should check quantified expressions for side-effects");
403  }
404  else if(expr.id()==ID_address_of)
405  {
406  address_of_exprt &addr = to_address_of_expr(expr);
407  clean_expr_address_of(addr.object(), dest, mode);
408  return;
409  }
410 
411  // TODO: evaluation order
412 
413  Forall_operands(it, expr)
414  clean_expr(*it, dest, mode);
415 
416  if(expr.id()==ID_side_effect)
417  {
418  remove_side_effect(to_side_effect_expr(expr), dest, mode, result_is_used);
419  }
420  else if(expr.id()==ID_compound_literal)
421  {
422  // This is simply replaced by the literal
424  expr.operands().size() == 1, "ID_compound_literal has a single operand");
425  expr=expr.op0();
426  }
427 }
428 
430  exprt &expr,
431  goto_programt &dest,
432  const irep_idt &mode)
433 {
434  // The address of object constructors can be taken,
435  // which is re-written into the address of a variable.
436 
437  if(expr.id()==ID_compound_literal)
438  {
440  expr.operands().size() == 1, "ID_compound_literal has a single operand");
441  clean_expr(expr.op0(), dest, mode);
442  expr = make_compound_literal(expr.op0(), dest, mode);
443  }
444  else if(expr.id()==ID_string_constant)
445  {
446  // Leave for now, but long-term these might become static symbols.
447  // LLVM appears to do precisely that.
448  }
449  else if(expr.id()==ID_index)
450  {
451  index_exprt &index_expr = to_index_expr(expr);
452  clean_expr_address_of(index_expr.array(), dest, mode);
453  clean_expr(index_expr.index(), dest, mode);
454  }
455  else if(expr.id()==ID_dereference)
456  {
457  dereference_exprt &deref_expr = to_dereference_expr(expr);
458  clean_expr(deref_expr.pointer(), dest, mode);
459  }
460  else if(expr.id()==ID_comma)
461  {
462  // Yes, one can take the address of a comma expression.
463  // Treatment is similar to clean_expr() above.
464 
465  exprt result;
466 
467  Forall_operands(it, expr)
468  {
469  bool last=(it==--expr.operands().end());
470 
471  // special treatment for last one
472  if(last)
473  result.swap(*it);
474  else
475  {
476  clean_expr(*it, dest, mode, false);
477 
478  // get any side-effects
479  if(it->is_not_nil())
480  convert(code_expressiont(*it), dest, mode);
481  }
482  }
483 
484  expr.swap(result);
485 
486  // do again
487  clean_expr_address_of(expr, dest, mode);
488  }
489  else
490  Forall_operands(it, expr)
491  clean_expr_address_of(*it, dest, mode);
492 }
493 
495  exprt &expr,
496  goto_programt &dest,
497  const irep_idt &mode)
498 {
500  expr.operands().size() == 2,
501  "gcc conditional expressions must have two operands");
502 
503  // first remove side-effects from condition
504  clean_expr(expr.op0(), dest, mode);
505 
506  // now we can copy op0 safely
507  if_exprt if_expr;
508 
509  if_expr.cond()=expr.op0();
510  if_expr.true_case()=expr.op0();
511  if_expr.false_case()=expr.op1();
512  if_expr.type()=expr.type();
513  if_expr.add_source_location()=expr.source_location();
514 
515  if(if_expr.cond().type()!=bool_typet())
516  if_expr.cond().make_typecast(bool_typet());
517 
518  expr.swap(if_expr);
519 
520  // there might still be junk in expr.op2()
521  clean_expr(expr, dest, mode);
522 }
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3482
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Definition: std_code.h:1775
exprt & true_case()
Definition: std_expr.h:3455
Semantic type conversion.
Definition: std_expr.h:2277
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition: expr.cpp:117
bool is_nil() const
Definition: irep.h:172
bool is_not_nil() const
Definition: irep.h:173
exprt & object()
Definition: std_expr.h:3265
exprt & op0()
Definition: expr.h:84
struct goto_convertt::targetst targets
void convert(const codet &code, goto_programt &dest, const irep_idt &mode)
converts 'code' and appends the result to 'dest'
const exprt & op() const
Definition: std_expr.h:371
Deprecated expression utility functions.
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
Return whether the expression is a constant representing false.
Definition: expr.cpp:99
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
Definition: invariant.h:439
exprt value
Initial value of symbol.
Definition: symbol.h:34
The trinary if-then-else operator.
Definition: std_expr.h:3427
exprt & cond()
Definition: std_expr.h:3445
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:90
typet & type()
Return the type of the expression.
Definition: expr.h:68
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: std_expr.h:3282
void clean_expr_address_of(exprt &expr, goto_programt &dest, const irep_idt &mode)
The Boolean type.
Definition: std_types.h:28
Symbol table entry.
Definition: symbol.h:27
codet representation of an expression statement.
Definition: std_code.h:1504
bool is_static_lifetime
Definition: symbol.h:65
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: std_expr.h:3397
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1620
destructor_stackt destructor_stack
const irep_idt & id() const
Definition: irep.h:259
exprt & lhs()
Definition: std_code.h:269
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
The Boolean constant true.
Definition: std_expr.h:4443
void clean_expr(exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used=true)
std::string tmp_symbol_prefix
A codet representing the declaration of a local variable.
Definition: std_code.h:352
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
Definition: expr_util.cpp:139
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Definition: invariant.h:486
The NIL expression.
Definition: std_expr.h:4461
exprt & rhs()
Definition: std_code.h:274
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:229
The empty type.
Definition: std_types.h:48
Operator to dereference a pointer.
Definition: std_expr.h:3355
Program Transformation.
API to expression classes.
exprt & op1()
Definition: expr.h:87
void convert_assign(const code_assignt &code, goto_programt &dest, const irep_idt &mode)
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
#define forall_operands(it, expr)
Definition: expr.h:20
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
Operator to return the address of an object.
Definition: std_expr.h:3255
exprt & false_case()
Definition: std_expr.h:3465
The Boolean constant false.
Definition: std_expr.h:4452
std::vector< exprt > operandst
Definition: expr.h:57
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
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:396
exprt & index()
Definition: std_expr.h:1631
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:54
exprt & pointer()
Definition: std_expr.h:3380
symbol_exprt make_compound_literal(const exprt &expr, goto_programt &dest, const irep_idt &mode)
source_locationt & add_source_location()
Definition: type.h:67
const source_locationt & source_location() const
Definition: expr.h:228
symbolt & new_tmp_symbol(const typet &type, const std::string &suffix, goto_programt &dest, const source_locationt &, const irep_idt &mode)
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2306
exprt::operandst & arguments()
Definition: std_code.h:1754
symbol_table_baset & symbol_table
A codet representing the removal of a local variable going out of scope.
Definition: std_code.h:424
void make_nil()
Definition: irep.h:315
void swap(irept &irep)
Definition: irep.h:303
#define Forall_operands(it, expr)
Definition: expr.h:26
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:130
source_locationt & add_source_location()
Definition: expr.h:233
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:143
void copy(const codet &code, goto_program_instruction_typet type, goto_programt &dest)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:485
operandst & operands()
Definition: expr.h:78
void rewrite_boolean(exprt &dest)
re-write boolean operators into ?:
exprt & array()
Definition: std_expr.h:1621
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1648
A codet representing an assignment in the program.
Definition: std_code.h:256
const irep_idt & get_statement() const
Definition: std_code.h:1586
bool simplify(exprt &expr, const namespacet &ns)
Array index operator.
Definition: std_expr.h:1595