cprover
Loading...
Searching...
No Matches
goto_clean_expr.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Program Transformation
4
5Author: 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,
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
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 {
56 targets.destructor_stack.add(std::move(code_dead));
57 }
58
59 return result;
60}
61
68{
69 if(
70 expr.id() == ID_side_effect || expr.id() == ID_compound_literal ||
71 expr.id() == ID_comma)
72 {
73 return true;
74 }
75
76 // We can't flatten quantified expressions by introducing new literals for
77 // conditional expressions. This is because the body of the quantified
78 // may refer to bound variables, which are not visible outside the scope
79 // of the quantifier.
80 //
81 // For example, the following transformation would not be valid:
82 //
83 // forall (i : int) (i == 0 || i > 10)
84 //
85 // transforming to
86 //
87 // g1 = (i == 0)
88 // g2 = (i > 10)
89 // forall (i : int) (g1 || g2)
90 if(expr.id()==ID_forall || expr.id()==ID_exists)
91 return false;
92
93 for(const auto &op : expr.operands())
94 {
95 if(needs_cleaning(op))
96 return true;
97 }
98
99 return false;
100}
101
104{
106 expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_implies);
108 expr.is_boolean(),
110 "'",
111 expr.id(),
112 "' must be Boolean, but got ",
114
115 // re-write "a ==> b" into a?b:1
116 if(auto implies = expr_try_dynamic_cast<implies_exprt>(expr))
117 {
118 expr = if_exprt{std::move(implies->lhs()),
119 std::move(implies->rhs()),
120 true_exprt{},
121 bool_typet{}};
122 return;
123 }
124
125 // re-write "a && b" into nested a?b:0
126 // re-write "a || b" into nested a?1:b
127
128 exprt tmp;
129
130 if(expr.id()==ID_and)
131 tmp=true_exprt();
132 else // ID_or
134
136
137 // start with last one
138 for(exprt::operandst::reverse_iterator
139 it=ops.rbegin();
140 it!=ops.rend();
141 ++it)
142 {
143 exprt &op=*it;
144
146 op.is_boolean(),
147 "boolean operators must have only boolean operands",
148 expr.find_source_location());
149
150 if(expr.id()==ID_and)
151 {
153 tmp.swap(if_e);
154 continue;
155 }
156 if(expr.id() == ID_or)
157 {
158 if_exprt if_e(op, true_exprt(), tmp);
159 tmp.swap(if_e);
160 continue;
161 }
163 }
164
165 expr.swap(tmp);
166}
167
169 exprt &expr,
170 goto_programt &dest,
171 const irep_idt &mode,
172 bool result_is_used)
173{
174 // this cleans:
175 // && || ==> ?: comma (control-dependency)
176 // function calls
177 // object constructors like arrays, string constants, structs
178 // ++ -- (pre and post)
179 // compound assignments
180 // compound literals
181
182 if(!needs_cleaning(expr))
183 return;
184
185 if(expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_implies)
186 {
187 // rewrite into ?:
188 rewrite_boolean(expr);
189
190 // recursive call
191 clean_expr(expr, dest, mode, result_is_used);
192 return;
193 }
194 else if(expr.id()==ID_if)
195 {
196 // first clean condition
197 clean_expr(to_if_expr(expr).cond(), dest, mode, true);
198
199 // possibly done now
200 if(!needs_cleaning(to_if_expr(expr).true_case()) &&
201 !needs_cleaning(to_if_expr(expr).false_case()))
202 return;
203
204 // copy expression
206
208 if_expr.cond().is_boolean(),
209 "condition for an 'if' must be boolean",
210 if_expr.find_source_location());
211
212 const source_locationt source_location=expr.find_source_location();
213
214 #if 0
215 // We do some constant-folding here, to mimic
216 // what typical compilers do.
217 {
218 exprt tmp_cond=if_expr.cond();
220 if(tmp_cond.is_true())
221 {
222 clean_expr(if_expr.true_case(), dest, result_is_used);
223 expr=if_expr.true_case();
224 return;
225 }
226 else if(tmp_cond.is_false())
227 {
228 clean_expr(if_expr.false_case(), dest, result_is_used);
229 expr=if_expr.false_case();
230 return;
231 }
232 }
233 #endif
234
236 clean_expr(if_expr.true_case(), tmp_true, mode, result_is_used);
237
239 clean_expr(if_expr.false_case(), tmp_false, mode, result_is_used);
240
242 {
243 symbolt &new_symbol =
244 new_tmp_symbol(expr.type(), "if_expr", dest, source_location, mode);
245
247 assignment_true.lhs()=new_symbol.symbol_expr();
248 assignment_true.rhs()=if_expr.true_case();
249 assignment_true.add_source_location()=source_location;
251
253 assignment_false.lhs()=new_symbol.symbol_expr();
254 assignment_false.rhs()=if_expr.false_case();
255 assignment_false.add_source_location()=source_location;
257
258 // overwrites expr
259 expr=new_symbol.symbol_expr();
260 }
261 else
262 {
263 // preserve the expressions for possible later checks
264 if(if_expr.true_case().is_not_nil())
265 {
266 // add a (void) type cast so that is_skip catches it in case the
267 // expression is just a constant
269 typecast_exprt(if_expr.true_case(), empty_typet()));
271 }
272
273 if(if_expr.false_case().is_not_nil())
274 {
275 // add a (void) type cast so that is_skip catches it in case the
276 // expression is just a constant
278 typecast_exprt(if_expr.false_case(), empty_typet()));
280 }
281
282 expr=nil_exprt();
283 }
284
285 // generate guard for argument side-effects
287 if_expr.cond(), tmp_true, tmp_false, source_location, dest, mode);
288
289 return;
290 }
291 else if(expr.id()==ID_comma)
292 {
294 {
296
297 Forall_operands(it, expr)
298 {
299 bool last=(it==--expr.operands().end());
300
301 // special treatment for last one
302 if(last)
303 {
304 result.swap(*it);
305 clean_expr(result, dest, mode, true);
306 }
307 else
308 {
309 clean_expr(*it, dest, mode, false);
310
311 // remember these for later checks
312 if(it->is_not_nil())
313 convert(code_expressiont(*it), dest, mode);
314 }
315 }
316
317 expr.swap(result);
318 }
319 else // result not used
320 {
321 Forall_operands(it, expr)
322 {
323 clean_expr(*it, dest, mode, false);
324
325 // remember as expression statement for later checks
326 if(it->is_not_nil())
327 convert(code_expressiont(*it), dest, mode);
328 }
329
330 expr=nil_exprt();
331 }
332
333 return;
334 }
335 else if(expr.id()==ID_typecast)
336 {
337 typecast_exprt &typecast = to_typecast_expr(expr);
338
339 // preserve 'result_is_used'
340 clean_expr(typecast.op(), dest, mode, result_is_used);
341
342 if(typecast.op().is_nil())
343 expr.make_nil();
344
345 return;
346 }
347 else if(expr.id()==ID_side_effect)
348 {
349 // some of the side-effects need special treatment!
350 const irep_idt statement=to_side_effect_expr(expr).get_statement();
351
352 if(statement==ID_gcc_conditional_expression)
353 {
354 // need to do separately
355 remove_gcc_conditional_expression(expr, dest, mode);
356 return;
357 }
358 else if(statement==ID_statement_expression)
359 {
360 // need to do separately to prevent that
361 // the operands of expr get 'cleaned'
363 to_side_effect_expr(expr), dest, mode, result_is_used);
364 return;
365 }
366 else if(statement==ID_assign)
367 {
368 // we do a special treatment for x=f(...)
369 INVARIANT(
370 expr.operands().size() == 2,
371 "side-effect assignment expressions must have two operands");
372
374
375 if(
376 side_effect_assign.rhs().id() == ID_side_effect &&
379 {
380 clean_expr(side_effect_assign.lhs(), dest, mode);
381 exprt lhs = side_effect_assign.lhs();
382
384 if(must_use_rhs)
385 {
388 dest,
389 mode,
390 true);
391 }
392
393 // turn into code
396 side_effect_assign.rhs(), new_lhs.type());
397 code_assignt assignment(std::move(new_lhs), new_rhs);
398 assignment.add_source_location()=expr.source_location();
399 convert_assign(assignment, dest, mode);
400
402 expr = must_use_rhs ? new_rhs : lhs;
403 else
404 expr.make_nil();
405 return;
406 }
407 }
408 }
409 else if(expr.id()==ID_forall || expr.id()==ID_exists)
410 {
413 "the front-end should check quantified expressions for side-effects");
414 }
415 else if(expr.id()==ID_address_of)
416 {
418 clean_expr_address_of(addr.object(), dest, mode);
419 return;
420 }
421
422 // TODO: evaluation order
423
424 Forall_operands(it, expr)
425 clean_expr(*it, dest, mode);
426
427 if(expr.id()==ID_side_effect)
428 {
430 to_side_effect_expr(expr), dest, mode, result_is_used, false);
431 }
432 else if(expr.id()==ID_compound_literal)
433 {
434 // This is simply replaced by the literal
436 expr.operands().size() == 1, "ID_compound_literal has a single operand");
437 expr = to_unary_expr(expr).op();
438 }
439}
440
442 exprt &expr,
443 goto_programt &dest,
444 const irep_idt &mode)
445{
446 // The address of object constructors can be taken,
447 // which is re-written into the address of a variable.
448
449 if(expr.id()==ID_compound_literal)
450 {
452 expr.operands().size() == 1, "ID_compound_literal has a single operand");
453 clean_expr(to_unary_expr(expr).op(), dest, mode);
454 expr = make_compound_literal(to_unary_expr(expr).op(), dest, mode);
455 }
456 else if(expr.id()==ID_string_constant)
457 {
458 // Leave for now, but long-term these might become static symbols.
459 // LLVM appears to do precisely that.
460 }
461 else if(expr.id()==ID_index)
462 {
464 clean_expr_address_of(index_expr.array(), dest, mode);
465 clean_expr(index_expr.index(), dest, mode);
466 }
467 else if(expr.id()==ID_dereference)
468 {
470 clean_expr(deref_expr.pointer(), dest, mode);
471 }
472 else if(expr.id()==ID_comma)
473 {
474 // Yes, one can take the address of a comma expression.
475 // Treatment is similar to clean_expr() above.
476
478
479 Forall_operands(it, expr)
480 {
481 bool last=(it==--expr.operands().end());
482
483 // special treatment for last one
484 if(last)
485 result.swap(*it);
486 else
487 {
488 clean_expr(*it, dest, mode, false);
489
490 // get any side-effects
491 if(it->is_not_nil())
492 convert(code_expressiont(*it), dest, mode);
493 }
494 }
495
496 expr.swap(result);
497
498 // do again
499 clean_expr_address_of(expr, dest, mode);
500 }
501 else if(expr.id() == ID_side_effect)
502 {
503 remove_side_effect(to_side_effect_expr(expr), dest, mode, true, true);
504 }
505 else
506 Forall_operands(it, expr)
507 clean_expr_address_of(*it, dest, mode);
508}
509
511 exprt &expr,
512 goto_programt &dest,
513 const irep_idt &mode)
514{
515 {
516 auto &binary_expr = to_binary_expr(expr);
517
518 // first remove side-effects from condition
519 clean_expr(to_binary_expr(expr).op0(), dest, mode);
520
521 // now we can copy op0 safely
524 binary_expr.op0(),
525 binary_expr.op1(),
526 expr.type());
527 if_expr.add_source_location() = expr.source_location();
528
529 expr.swap(if_expr);
530 }
531
532 // there might still be junk in expr.op2()
533 clean_expr(expr, dest, mode);
534}
@ AUTOMATIC_LOCAL
Allocate local objects with automatic lifetime.
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
The Boolean type.
Definition std_types.h:36
A goto_instruction_codet representing an assignment in the program.
A goto_instruction_codet representing the removal of a local variable going out of scope.
A goto_instruction_codet representing the declaration of a local variable.
codet representation of an expression statement.
Definition std_code.h:1394
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
The empty type.
Definition std_types.h:51
Base class for all expressions.
Definition expr.h:56
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition expr.cpp:147
std::vector< exprt > operandst
Definition expr.h:58
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition expr.h:216
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
const source_locationt & source_location() const
Definition expr.h:223
source_locationt & add_source_location()
Definition expr.h:228
The Boolean constant false.
Definition std_expr.h:3017
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)
Returns 'true' for expressions that may change the program state.
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 ?:
static bool assignment_lhs_needs_temporary(const exprt &lhs)
A generic container class for the GOTO intermediate representation of one function.
The trinary if-then-else operator.
Definition std_expr.h:2323
Array index operator.
Definition std_expr.h:1410
void make_nil()
Definition irep.h:454
void swap(irept &irep)
Definition irep.h:442
const irep_idt & id() const
Definition irep.h:396
mstreamt & result() const
Definition message.h:409
The NIL expression.
Definition std_expr.h:3026
const irep_idt & get_statement() const
Definition std_code.h:1472
Expression to hold a symbol (variable)
Definition std_expr.h:113
Symbol table entry.
Definition symbol.h:28
bool is_static_lifetime
Definition symbol.h:70
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:3008
Semantic type conversion.
Definition std_expr.h:2017
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2025
const exprt & op() const
Definition std_expr.h:326
#define Forall_operands(it, expr)
Definition expr.h:27
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
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
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
exprt deref_expr(const exprt &expr)
Wraps a given expression into a dereference_exprt unless it is an address_of_exprt in which case it j...
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:525
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Definition invariant.h:535
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 index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1478
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2051
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition std_expr.h:660
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:361
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2403
Symbol table entry.