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/expr_util.h>
15 #include <util/fresh_symbol.h>
16 #include <util/pointer_expr.h>
17 #include <util/std_expr.h>
18 #include <util/symbol.h>
19 
21  const exprt &expr,
22  goto_programt &dest,
23  const irep_idt &mode)
24 {
25  const source_locationt source_location=expr.find_source_location();
26 
27  symbolt &new_symbol = get_fresh_aux_symbol(
28  expr.type(),
30  "literal",
31  source_location,
32  mode,
33  symbol_table);
35  new_symbol.value=expr;
36 
37  // The value might depend on a variable, thus
38  // generate code for this.
39 
40  symbol_exprt result=new_symbol.symbol_expr();
41  result.add_source_location()=source_location;
42 
43  // The lifetime of compound literals is really that of
44  // the block they are in.
45  if(!new_symbol.is_static_lifetime)
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.add(std::move(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  PRECONDITION(
110  expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_implies);
112  expr.is_boolean(),
113  expr.find_source_location(),
114  "'",
115  expr.id(),
116  "' must be Boolean, but got ",
118 
119  // re-write "a ==> b" into a?b:1
120  if(auto implies = expr_try_dynamic_cast<implies_exprt>(expr))
121  {
122  expr = if_exprt{std::move(implies->lhs()),
123  std::move(implies->rhs()),
124  true_exprt{},
125  bool_typet{}};
126  return;
127  }
128 
129  // re-write "a && b" into nested a?b:0
130  // re-write "a || b" into nested a?1:b
131 
132  exprt tmp;
133 
134  if(expr.id()==ID_and)
135  tmp=true_exprt();
136  else // ID_or
137  tmp=false_exprt();
138 
139  exprt::operandst &ops=expr.operands();
140 
141  // start with last one
142  for(exprt::operandst::reverse_iterator
143  it=ops.rbegin();
144  it!=ops.rend();
145  ++it)
146  {
147  exprt &op=*it;
148 
150  op.is_boolean(),
151  "boolean operators must have only boolean operands",
152  expr.find_source_location());
153 
154  if(expr.id()==ID_and)
155  {
156  if_exprt if_e(op, tmp, false_exprt());
157  tmp.swap(if_e);
158  continue;
159  }
160  if(expr.id() == ID_or)
161  {
162  if_exprt if_e(op, true_exprt(), tmp);
163  tmp.swap(if_e);
164  continue;
165  }
166  UNREACHABLE;
167  }
168 
169  expr.swap(tmp);
170 }
171 
173  exprt &expr,
174  goto_programt &dest,
175  const irep_idt &mode,
176  bool result_is_used)
177 {
178  // this cleans:
179  // && || ==> ?: comma (control-dependency)
180  // function calls
181  // object constructors like arrays, string constants, structs
182  // ++ -- (pre and post)
183  // compound assignments
184  // compound literals
185 
186  if(!needs_cleaning(expr))
187  return;
188 
189  if(expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_implies)
190  {
191  // rewrite into ?:
192  rewrite_boolean(expr);
193 
194  // recursive call
195  clean_expr(expr, dest, mode, result_is_used);
196  return;
197  }
198  else if(expr.id()==ID_if)
199  {
200  // first clean condition
201  clean_expr(to_if_expr(expr).cond(), dest, mode, true);
202 
203  // possibly done now
204  if(!needs_cleaning(to_if_expr(expr).true_case()) &&
205  !needs_cleaning(to_if_expr(expr).false_case()))
206  return;
207 
208  // copy expression
209  if_exprt if_expr=to_if_expr(expr);
210 
212  if_expr.cond().is_boolean(),
213  "condition for an 'if' must be boolean",
214  if_expr.find_source_location());
215 
216  const source_locationt source_location=expr.find_source_location();
217 
218  #if 0
219  // We do some constant-folding here, to mimic
220  // what typical compilers do.
221  {
222  exprt tmp_cond=if_expr.cond();
223  simplify(tmp_cond, ns);
224  if(tmp_cond.is_true())
225  {
226  clean_expr(if_expr.true_case(), dest, result_is_used);
227  expr=if_expr.true_case();
228  return;
229  }
230  else if(tmp_cond.is_false())
231  {
232  clean_expr(if_expr.false_case(), dest, result_is_used);
233  expr=if_expr.false_case();
234  return;
235  }
236  }
237  #endif
238 
239  goto_programt tmp_true;
240  clean_expr(if_expr.true_case(), tmp_true, mode, result_is_used);
241 
242  goto_programt tmp_false;
243  clean_expr(if_expr.false_case(), tmp_false, mode, result_is_used);
244 
245  if(result_is_used)
246  {
247  symbolt &new_symbol =
248  new_tmp_symbol(expr.type(), "if_expr", dest, source_location, mode);
249 
250  code_assignt assignment_true;
251  assignment_true.lhs()=new_symbol.symbol_expr();
252  assignment_true.rhs()=if_expr.true_case();
253  assignment_true.add_source_location()=source_location;
254  convert(assignment_true, tmp_true, mode);
255 
256  code_assignt assignment_false;
257  assignment_false.lhs()=new_symbol.symbol_expr();
258  assignment_false.rhs()=if_expr.false_case();
259  assignment_false.add_source_location()=source_location;
260  convert(assignment_false, tmp_false, mode);
261 
262  // overwrites expr
263  expr=new_symbol.symbol_expr();
264  }
265  else
266  {
267  // preserve the expressions for possible later checks
268  if(if_expr.true_case().is_not_nil())
269  {
270  // add a (void) type cast so that is_skip catches it in case the
271  // expression is just a constant
272  code_expressiont code_expression(
273  typecast_exprt(if_expr.true_case(), empty_typet()));
274  convert(code_expression, tmp_true, mode);
275  }
276 
277  if(if_expr.false_case().is_not_nil())
278  {
279  // add a (void) type cast so that is_skip catches it in case the
280  // expression is just a constant
281  code_expressiont code_expression(
282  typecast_exprt(if_expr.false_case(), empty_typet()));
283  convert(code_expression, tmp_false, mode);
284  }
285 
286  expr=nil_exprt();
287  }
288 
289  // generate guard for argument side-effects
291  if_expr.cond(), tmp_true, tmp_false, source_location, dest, mode);
292 
293  return;
294  }
295  else if(expr.id()==ID_comma)
296  {
297  if(result_is_used)
298  {
299  exprt result;
300 
301  Forall_operands(it, expr)
302  {
303  bool last=(it==--expr.operands().end());
304 
305  // special treatment for last one
306  if(last)
307  {
308  result.swap(*it);
309  clean_expr(result, dest, mode, true);
310  }
311  else
312  {
313  clean_expr(*it, dest, mode, false);
314 
315  // remember these for later checks
316  if(it->is_not_nil())
317  convert(code_expressiont(*it), dest, mode);
318  }
319  }
320 
321  expr.swap(result);
322  }
323  else // result not used
324  {
325  Forall_operands(it, expr)
326  {
327  clean_expr(*it, dest, mode, false);
328 
329  // remember as expression statement for later checks
330  if(it->is_not_nil())
331  convert(code_expressiont(*it), dest, mode);
332  }
333 
334  expr=nil_exprt();
335  }
336 
337  return;
338  }
339  else if(expr.id()==ID_typecast)
340  {
341  typecast_exprt &typecast = to_typecast_expr(expr);
342 
343  // preserve 'result_is_used'
344  clean_expr(typecast.op(), dest, mode, result_is_used);
345 
346  if(typecast.op().is_nil())
347  expr.make_nil();
348 
349  return;
350  }
351  else if(expr.id()==ID_side_effect)
352  {
353  // some of the side-effects need special treatment!
354  const irep_idt statement=to_side_effect_expr(expr).get_statement();
355 
356  if(statement==ID_gcc_conditional_expression)
357  {
358  // need to do separately
359  remove_gcc_conditional_expression(expr, dest, mode);
360  return;
361  }
362  else if(statement==ID_statement_expression)
363  {
364  // need to do separately to prevent that
365  // the operands of expr get 'cleaned'
367  to_side_effect_expr(expr), dest, mode, result_is_used);
368  return;
369  }
370  else if(statement==ID_assign)
371  {
372  // we do a special treatment for x=f(...)
373  INVARIANT(
374  expr.operands().size() == 2,
375  "side-effect assignment expressions must have two operands");
376 
377  auto &side_effect_assign = to_side_effect_expr_assign(expr);
378 
379  if(
380  side_effect_assign.rhs().id() == ID_side_effect &&
381  to_side_effect_expr(side_effect_assign.rhs()).get_statement() ==
382  ID_function_call)
383  {
384  clean_expr(side_effect_assign.lhs(), dest, mode);
385  exprt lhs = side_effect_assign.lhs();
386 
387  const bool must_use_rhs = needs_cleaning(lhs);
388  if(must_use_rhs)
389  {
391  to_side_effect_expr_function_call(side_effect_assign.rhs()),
392  dest,
393  mode,
394  true);
395  }
396 
397  // turn into code
398  code_assignt assignment;
399  assignment.lhs()=lhs;
400  assignment.rhs() = side_effect_assign.rhs();
401  assignment.add_source_location()=expr.source_location();
402  convert_assign(assignment, dest, mode);
403 
404  if(result_is_used)
405  expr = must_use_rhs ? side_effect_assign.rhs() : lhs;
406  else
407  expr.make_nil();
408  return;
409  }
410  }
411  }
412  else if(expr.id()==ID_forall || expr.id()==ID_exists)
413  {
415  !has_subexpr(expr, ID_side_effect),
416  "the front-end should check quantified expressions for side-effects");
417  }
418  else if(expr.id()==ID_address_of)
419  {
420  address_of_exprt &addr = to_address_of_expr(expr);
421  clean_expr_address_of(addr.object(), dest, mode);
422  return;
423  }
424 
425  // TODO: evaluation order
426 
427  Forall_operands(it, expr)
428  clean_expr(*it, dest, mode);
429 
430  if(expr.id()==ID_side_effect)
431  {
433  to_side_effect_expr(expr), dest, mode, result_is_used, false);
434  }
435  else if(expr.id()==ID_compound_literal)
436  {
437  // This is simply replaced by the literal
439  expr.operands().size() == 1, "ID_compound_literal has a single operand");
440  expr = to_unary_expr(expr).op();
441  }
442 }
443 
445  exprt &expr,
446  goto_programt &dest,
447  const irep_idt &mode)
448 {
449  // The address of object constructors can be taken,
450  // which is re-written into the address of a variable.
451 
452  if(expr.id()==ID_compound_literal)
453  {
455  expr.operands().size() == 1, "ID_compound_literal has a single operand");
456  clean_expr(to_unary_expr(expr).op(), dest, mode);
457  expr = make_compound_literal(to_unary_expr(expr).op(), 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  index_exprt &index_expr = to_index_expr(expr);
467  clean_expr_address_of(index_expr.array(), dest, mode);
468  clean_expr(index_expr.index(), dest, mode);
469  }
470  else if(expr.id()==ID_dereference)
471  {
472  dereference_exprt &deref_expr = to_dereference_expr(expr);
473  clean_expr(deref_expr.pointer(), 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 if(expr.id() == ID_side_effect)
505  {
506  remove_side_effect(to_side_effect_expr(expr), dest, mode, true, true);
507  }
508  else
509  Forall_operands(it, expr)
510  clean_expr_address_of(*it, dest, mode);
511 }
512 
514  exprt &expr,
515  goto_programt &dest,
516  const irep_idt &mode)
517 {
518  {
519  auto &binary_expr = to_binary_expr(expr);
520 
521  // first remove side-effects from condition
522  clean_expr(to_binary_expr(expr).op0(), dest, mode);
523 
524  // now we can copy op0 safely
525  if_exprt if_expr(
526  typecast_exprt::conditional_cast(binary_expr.op0(), bool_typet()),
527  binary_expr.op0(),
528  binary_expr.op1(),
529  expr.type());
530  if_expr.add_source_location() = expr.source_location();
531 
532  expr.swap(if_expr);
533  }
534 
535  // there might still be junk in expr.op2()
536  clean_expr(expr, dest, mode);
537 }
@ AUTOMATIC_LOCAL
Allocate local objects with automatic lifetime.
Operator to return the address of an object.
Definition: pointer_expr.h:361
exprt & object()
Definition: pointer_expr.h:370
The Boolean type.
Definition: std_types.h:36
A codet representing an assignment in the program.
A codet representing the removal of a local variable going out of scope.
A codet representing the declaration of a local variable.
codet representation of an expression statement.
Definition: std_code.h:1394
Operator to dereference a pointer.
Definition: pointer_expr.h:648
void add(const codet &destructor)
Adds a destructor to the current stack, attaching itself to the current node.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
The empty type.
Definition: std_types.h:51
Base class for all expressions.
Definition: expr.h:54
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:165
std::vector< exprt > operandst
Definition: expr.h:56
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:33
exprt & op1()
Definition: expr.h:102
source_locationt & add_source_location()
Definition: expr.h:235
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition: expr.cpp:51
const source_locationt & source_location() const
Definition: expr.h:230
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:42
typet & type()
Return the type of the expression.
Definition: expr.h:82
exprt & op0()
Definition: expr.h:99
operandst & operands()
Definition: expr.h:92
The Boolean constant false.
Definition: std_expr.h:2865
void remove_function_call(side_effect_expr_function_callt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used)
symbol_table_baset & symbol_table
void convert_assign(const code_assignt &code, goto_programt &dest, const irep_idt &mode)
void copy(const codet &code, goto_program_instruction_typet type, goto_programt &dest)
std::string tmp_symbol_prefix
void remove_side_effect(side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used, bool address_taken)
struct goto_convertt::targetst targets
symbolt & new_tmp_symbol(const typet &type, const std::string &suffix, goto_programt &dest, const source_locationt &, const irep_idt &mode)
void remove_statement_expression(side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used)
symbol_exprt make_compound_literal(const exprt &expr, goto_programt &dest, const irep_idt &mode)
void clean_expr(exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used=true)
static bool needs_cleaning(const exprt &expr)
void clean_expr_address_of(exprt &expr, goto_programt &dest, const irep_idt &mode)
void convert(const codet &code, goto_programt &dest, const irep_idt &mode)
converts 'code' and appends the result to 'dest'
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;
void remove_gcc_conditional_expression(exprt &expr, goto_programt &dest, const irep_idt &mode)
void rewrite_boolean(exprt &dest)
re-write boolean operators into ?:
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
The trinary if-then-else operator.
Definition: std_expr.h:2226
exprt & true_case()
Definition: std_expr.h:2253
exprt & false_case()
Definition: std_expr.h:2263
exprt & cond()
Definition: std_expr.h:2243
Array index operator.
Definition: std_expr.h:1328
exprt & array()
Definition: std_expr.h:1353
exprt & index()
Definition: std_expr.h:1363
bool is_not_nil() const
Definition: irep.h:380
const irep_idt & id() const
Definition: irep.h:396
void make_nil()
Definition: irep.h:454
void swap(irept &irep)
Definition: irep.h:442
bool is_nil() const
Definition: irep.h:376
mstreamt & result() const
Definition: message.h:409
The NIL expression.
Definition: std_expr.h:2874
const irep_idt & get_statement() const
Definition: std_code.h:1472
Expression to hold a symbol (variable)
Definition: std_expr.h:80
Symbol table entry.
Definition: symbol.h:28
bool is_static_lifetime
Definition: symbol.h:65
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
exprt value
Initial value of symbol.
Definition: symbol.h:34
The Boolean constant true.
Definition: std_expr.h:2856
Semantic type conversion.
Definition: std_expr.h:1920
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1928
const exprt & op() const
Definition: std_expr.h:293
#define forall_operands(it, expr)
Definition: expr.h:18
#define Forall_operands(it, expr)
Definition: expr.h:25
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:138
Deprecated expression utility functions.
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, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Fresh auxiliary symbol creation.
Program Transformation.
@ DECL
Definition: goto_program.h:47
API to expression classes for Pointers.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:704
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:398
bool simplify(exprt &expr, const namespacet &ns)
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
Definition: invariant.h:464
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Definition: invariant.h:511
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1506
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Definition: std_code.h:1739
side_effect_expr_assignt & to_side_effect_expr_assign(exprt &expr)
Definition: std_code.h:1618
API to expression classes.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2291
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1954
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:627
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:328
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1391
destructor_treet destructor_stack
Symbol table entry.