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
20#include "destructor.h"
21
23 const exprt &expr,
24 goto_programt &dest,
25 const irep_idt &mode)
26{
27 const source_locationt source_location = expr.find_source_location();
28
29 symbolt &new_symbol = get_fresh_aux_symbol(
30 expr.type(),
32 "literal",
33 source_location,
34 mode,
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 if(!new_symbol.is_static_lifetime)
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.scope_stack.add(std::move(code_dead), {});
59 }
60
61 return result;
62}
63
70{
71 if(
72 expr.id() == ID_side_effect || expr.id() == ID_compound_literal ||
73 expr.id() == ID_comma)
74 {
75 return true;
76 }
77
78 // We can't flatten quantified expressions by introducing new literals for
79 // conditional expressions. This is because the body of the quantified
80 // may refer to bound variables, which are not visible outside the scope
81 // of the quantifier.
82 //
83 // For example, the following transformation would not be valid:
84 //
85 // forall (i : int) (i == 0 || i > 10)
86 //
87 // transforming to
88 //
89 // g1 = (i == 0)
90 // g2 = (i > 10)
91 // forall (i : int) (g1 || g2)
92 if(expr.id() == ID_forall || expr.id() == ID_exists)
93 return false;
94
95 for(const auto &op : expr.operands())
96 {
97 if(needs_cleaning(op))
98 return true;
99 }
100
101 return false;
102}
103
106{
108 expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_implies);
110 expr.is_boolean(),
112 "'",
113 expr.id(),
114 "' must be Boolean, but got ",
116
117 // re-write "a ==> b" into a?b:1
118 if(auto implies = expr_try_dynamic_cast<implies_exprt>(expr))
119 {
120 expr = if_exprt{
121 std::move(implies->lhs()),
122 std::move(implies->rhs()),
123 true_exprt{},
124 bool_typet{}};
125 return;
126 }
127
128 // re-write "a && b" into nested a?b:0
129 // re-write "a || b" into nested a?1:b
130
131 exprt tmp;
132
133 if(expr.id() == ID_and)
134 tmp = true_exprt();
135 else // ID_or
136 tmp = false_exprt();
137
138 exprt::operandst &ops = expr.operands();
139
140 // start with last one
141 for(exprt::operandst::reverse_iterator it = ops.rbegin(); it != ops.rend();
142 ++it)
143 {
144 exprt &op = *it;
145
147 op.is_boolean(),
148 "boolean operators must have only boolean operands",
149 expr.find_source_location());
150
151 if(expr.id() == ID_and)
152 {
153 if_exprt if_e(op, tmp, false_exprt());
154 tmp.swap(if_e);
155 continue;
156 }
157 if(expr.id() == ID_or)
158 {
159 if_exprt if_e(op, true_exprt(), tmp);
160 tmp.swap(if_e);
161 continue;
162 }
164 }
165
166 expr.swap(tmp);
167}
168
170 exprt &expr,
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 return clean_expr(expr, mode, result_is_used);
192 }
193 else if(expr.id() == ID_if)
194 {
195 // first clean condition
196 clean_expr_resultt side_effects =
197 clean_expr(to_if_expr(expr).cond(), mode, true);
198
199 // possibly done now
200 if(
201 !needs_cleaning(to_if_expr(expr).true_case()) &&
202 !needs_cleaning(to_if_expr(expr).false_case()))
203 {
204 return side_effects;
205 }
206
207 // copy expression
208 if_exprt if_expr = to_if_expr(expr);
209
211 if_expr.cond().is_boolean(),
212 "condition for an 'if' must be boolean",
213 if_expr.find_source_location());
214
215 const source_locationt source_location = expr.find_source_location();
216
217#if 0
218 // We do some constant-folding here, to mimic
219 // what typical compilers do.
220 {
221 exprt tmp_cond=if_expr.cond();
222 simplify(tmp_cond, ns);
223 if(tmp_cond.is_true())
224 {
225 clean_expr(if_expr.true_case(), dest, result_is_used);
226 expr=if_expr.true_case();
227 return;
228 }
229 else if(tmp_cond.is_false())
230 {
231 clean_expr(if_expr.false_case(), dest, result_is_used);
232 expr=if_expr.false_case();
233 return;
234 }
235 }
236#endif
237
238 clean_expr_resultt tmp_true(
239 clean_expr(if_expr.true_case(), mode, result_is_used));
240
241 clean_expr_resultt tmp_false(
242 clean_expr(if_expr.false_case(), mode, result_is_used));
243
244 if(result_is_used)
245 {
246 symbolt &new_symbol = new_tmp_symbol(
247 expr.type(),
248 "if_expr",
249 side_effects.side_effects,
250 source_location,
251 mode);
252
253 code_assignt assignment_true;
254 assignment_true.lhs() = new_symbol.symbol_expr();
255 assignment_true.rhs() = if_expr.true_case();
256 assignment_true.add_source_location() = source_location;
257 convert(assignment_true, tmp_true.side_effects, mode);
258
259 code_assignt assignment_false;
260 assignment_false.lhs() = new_symbol.symbol_expr();
261 assignment_false.rhs() = if_expr.false_case();
262 assignment_false.add_source_location() = source_location;
263 convert(assignment_false, tmp_false.side_effects, mode);
264
265 // overwrites expr
266 expr = new_symbol.symbol_expr();
267 }
268 else
269 {
270 // preserve the expressions for possible later checks
271 if(if_expr.true_case().is_not_nil())
272 {
273 // add a (void) type cast so that is_skip catches it in case the
274 // expression is just a constant
275 code_expressiont code_expression(
276 typecast_exprt(if_expr.true_case(), empty_typet()));
277 convert(code_expression, tmp_true.side_effects, mode);
278 }
279
280 if(if_expr.false_case().is_not_nil())
281 {
282 // add a (void) type cast so that is_skip catches it in case the
283 // expression is just a constant
284 code_expressiont code_expression(
286 convert(code_expression, tmp_false.side_effects, mode);
287 }
288
289 expr = nil_exprt();
290 }
291
292 // generate guard for argument side-effects
294 if_expr.cond(),
295 source_location,
296 tmp_true.side_effects,
297 if_expr.true_case().source_location(),
298 tmp_false.side_effects,
299 if_expr.false_case().source_location(),
300 side_effects.side_effects,
301 mode);
302
303 destruct_locals(tmp_false.temporaries, side_effects.side_effects, ns);
304 destruct_locals(tmp_true.temporaries, side_effects.side_effects, ns);
305 destruct_locals(side_effects.temporaries, side_effects.side_effects, ns);
306 side_effects.temporaries.clear();
307
308 if(expr.is_not_nil())
309 side_effects.add_temporary(to_symbol_expr(expr).get_identifier());
310
311 return side_effects;
312 }
313 else if(expr.id() == ID_comma)
314 {
315 clean_expr_resultt side_effects;
316
317 if(result_is_used)
318 {
320
321 Forall_operands(it, expr)
322 {
323 bool last = (it == --expr.operands().end());
324
325 // special treatment for last one
326 if(last)
327 {
328 result.swap(*it);
329 side_effects.add(clean_expr(result, mode, true));
330 }
331 else
332 {
333 side_effects.add(clean_expr(*it, mode, false));
334
335 // remember these for later checks
336 if(it->is_not_nil())
337 convert(code_expressiont(*it), side_effects.side_effects, mode);
338 }
339 }
340
341 expr.swap(result);
342 }
343 else // result not used
344 {
345 Forall_operands(it, expr)
346 {
347 side_effects.add(clean_expr(*it, mode, false));
348
349 // remember as expression statement for later checks
350 if(it->is_not_nil())
351 convert(code_expressiont(*it), side_effects.side_effects, mode);
352 }
353
354 expr = nil_exprt();
355 }
356
357 return side_effects;
358 }
359 else if(expr.id() == ID_typecast)
360 {
361 typecast_exprt &typecast = to_typecast_expr(expr);
362
363 // preserve 'result_is_used'
364 clean_expr_resultt side_effects =
365 clean_expr(typecast.op(), mode, result_is_used);
366
367 if(typecast.op().is_nil())
368 expr.make_nil();
369
370 return side_effects;
371 }
372 else if(expr.id() == ID_side_effect)
373 {
374 // some of the side-effects need special treatment!
375 const irep_idt statement = to_side_effect_expr(expr).get_statement();
376
377 if(statement == ID_gcc_conditional_expression)
378 {
379 // need to do separately
380 return remove_gcc_conditional_expression(expr, mode);
381 }
382 else if(statement == ID_statement_expression)
383 {
384 // need to do separately to prevent that
385 // the operands of expr get 'cleaned'
387 to_side_effect_expr(expr), mode, result_is_used);
388 }
389 else if(statement == ID_assign)
390 {
391 // we do a special treatment for x=f(...)
392 INVARIANT(
393 expr.operands().size() == 2,
394 "side-effect assignment expressions must have two operands");
395
396 auto &side_effect_assign = to_side_effect_expr_assign(expr);
397
398 if(
399 side_effect_assign.rhs().id() == ID_side_effect &&
400 to_side_effect_expr(side_effect_assign.rhs()).get_statement() ==
401 ID_function_call)
402 {
403 clean_expr_resultt side_effects =
404 clean_expr(side_effect_assign.lhs(), mode);
405 exprt lhs = side_effect_assign.lhs();
406
407 const bool must_use_rhs = assignment_lhs_needs_temporary(lhs);
408 if(must_use_rhs)
409 {
410 side_effects.add(remove_function_call(
411 to_side_effect_expr_function_call(side_effect_assign.rhs()),
412 mode,
413 true));
414 }
415
416 // turn into code
417 exprt new_lhs = skip_typecast(lhs);
419 side_effect_assign.rhs(), new_lhs.type());
420 code_assignt assignment(std::move(new_lhs), new_rhs);
421 assignment.add_source_location() = expr.source_location();
422 convert_assign(assignment, side_effects.side_effects, mode);
423
424 if(result_is_used)
425 expr = must_use_rhs ? new_rhs : lhs;
426 else
427 expr.make_nil();
428
429 return side_effects;
430 }
431 }
432 }
433 else if(expr.id() == ID_forall || expr.id() == ID_exists)
434 {
436 !has_subexpr(expr, ID_side_effect),
437 "the front-end should check quantified expressions for side-effects");
438 }
439 else if(expr.id() == ID_address_of)
440 {
442 return clean_expr_address_of(addr.object(), mode);
443 }
444
445 clean_expr_resultt side_effects;
446
447 // TODO: evaluation order
448
449 Forall_operands(it, expr)
450 side_effects.add(clean_expr(*it, mode));
451
452 if(expr.id() == ID_side_effect)
453 {
454 side_effects.add(remove_side_effect(
455 to_side_effect_expr(expr), mode, result_is_used, false));
456 }
457 else if(expr.id() == ID_compound_literal)
458 {
459 // This is simply replaced by the literal
461 expr.operands().size() == 1, "ID_compound_literal has a single operand");
462 expr = to_unary_expr(expr).op();
463 }
464
465 return side_effects;
466}
467
470{
471 clean_expr_resultt side_effects;
472
473 // The address of object constructors can be taken,
474 // which is re-written into the address of a variable.
475
476 if(expr.id() == ID_compound_literal)
477 {
479 expr.operands().size() == 1, "ID_compound_literal has a single operand");
480 side_effects.add(clean_expr(to_unary_expr(expr).op(), mode));
482 to_unary_expr(expr).op(), side_effects.side_effects, mode);
483 }
484 else if(expr.id() == ID_string_constant)
485 {
486 // Leave for now, but long-term these might become static symbols.
487 // LLVM appears to do precisely that.
488 }
489 else if(expr.id() == ID_index)
490 {
491 index_exprt &index_expr = to_index_expr(expr);
492 side_effects.add(clean_expr_address_of(index_expr.array(), mode));
493 side_effects.add(clean_expr(index_expr.index(), mode));
494 }
495 else if(expr.id() == ID_dereference)
496 {
498 side_effects.add(clean_expr(deref_expr.pointer(), mode));
499 }
500 else if(expr.id() == ID_comma)
501 {
502 // Yes, one can take the address of a comma expression.
503 // Treatment is similar to clean_expr() above.
504
506
507 Forall_operands(it, expr)
508 {
509 bool last = (it == --expr.operands().end());
510
511 // special treatment for last one
512 if(last)
513 result.swap(*it);
514 else
515 {
516 side_effects.add(clean_expr(*it, mode, false));
517
518 // get any side-effects
519 if(it->is_not_nil())
520 convert(code_expressiont(*it), side_effects.side_effects, mode);
521 }
522 }
523
524 expr.swap(result);
525
526 // do again
527 side_effects.add(clean_expr_address_of(expr, mode));
528 }
529 else if(expr.id() == ID_side_effect)
530 {
531 side_effects.add(
532 remove_side_effect(to_side_effect_expr(expr), mode, true, true));
533 }
534 else
535 Forall_operands(it, expr)
536 side_effects.add(clean_expr_address_of(*it, mode));
537
538 return side_effects;
539}
540
543 exprt &expr,
544 const irep_idt &mode)
545{
546 clean_expr_resultt side_effects;
547
548 {
549 auto &binary_expr = to_binary_expr(expr);
550
551 // first remove side-effects from condition
552 side_effects = clean_expr(to_binary_expr(expr).op0(), mode);
553
554 // now we can copy op0 safely
555 if_exprt if_expr(
556 typecast_exprt::conditional_cast(binary_expr.op0(), bool_typet()),
557 binary_expr.op0(),
558 binary_expr.op1(),
559 expr.type());
560 if_expr.add_source_location() = expr.source_location();
561
562 expr.swap(if_expr);
563 }
564
565 // there might still be junk in expr.op2()
566 side_effects.add(clean_expr(expr, mode));
567
568 return side_effects;
569}
@ AUTOMATIC_LOCAL
Allocate local objects with automatic lifetime.
Operator to return the address of an object.
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:38
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_true() const
Return whether the expression is a constant representing true.
Definition expr.cpp:27
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition expr.h:224
bool is_false() const
Return whether the expression is a constant representing false.
Definition expr.cpp:34
exprt & op0()
Definition expr.h:133
exprt & op1()
Definition expr.h:136
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:231
source_locationt & add_source_location()
Definition expr.h:236
The Boolean constant false.
Definition std_expr.h:3064
clean_expr_resultt clean_expr_address_of(exprt &expr, const irep_idt &mode)
symbol_table_baset & symbol_table
void convert_assign(const code_assignt &code, goto_programt &dest, const irep_idt &mode)
clean_expr_resultt remove_gcc_conditional_expression(exprt &expr, const irep_idt &mode)
void copy(const codet &code, goto_program_instruction_typet type, goto_programt &dest)
void generate_ifthenelse(const exprt &cond, const source_locationt &, goto_programt &true_case, const source_locationt &, goto_programt &false_case, const source_locationt &, goto_programt &dest, const irep_idt &mode)
if(guard) true_case; else false_case;
std::string tmp_symbol_prefix
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)
symbol_exprt make_compound_literal(const exprt &expr, goto_programt &dest, const irep_idt &mode)
clean_expr_resultt remove_side_effect(side_effect_exprt &expr, const irep_idt &mode, bool result_is_used, bool address_taken)
static bool needs_cleaning(const exprt &expr)
Returns 'true' for expressions that may change the program state.
void convert(const codet &code, goto_programt &dest, const irep_idt &mode)
converts 'code' and appends the result to 'dest'
clean_expr_resultt remove_function_call(side_effect_expr_function_callt &expr, const irep_idt &mode, bool result_is_used)
clean_expr_resultt remove_statement_expression(side_effect_exprt &expr, const irep_idt &mode, bool result_is_used)
clean_expr_resultt clean_expr(exprt &expr, const irep_idt &mode, bool result_is_used=true)
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:2370
exprt & cond()
Definition std_expr.h:2387
exprt & false_case()
Definition std_expr.h:2407
exprt & true_case()
Definition std_expr.h:2397
Array index operator.
Definition std_expr.h:1465
exprt & index()
Definition std_expr.h:1505
exprt & array()
Definition std_expr.h:1495
bool is_not_nil() const
Definition irep.h:372
void make_nil()
Definition irep.h:446
void swap(irept &irep)
Definition irep.h:434
const irep_idt & id() const
Definition irep.h:388
bool is_nil() const
Definition irep.h:368
mstreamt & result() const
Definition message.h:401
The NIL expression.
Definition std_expr.h:3073
void add(const codet &destructor, std::optional< goto_programt::targett > declaration)
Adds a destructor/declaration pair to the current stack, attaching it to the current node.
const irep_idt & get_statement() const
Definition std_code.h:1472
Expression to hold a symbol (variable)
Definition std_expr.h:131
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:3055
Semantic type conversion.
Definition std_expr.h:2068
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2076
const exprt & op() const
Definition std_expr.h:391
void destruct_locals(const std::list< irep_idt > &vars, goto_programt &dest, const namespacet &ns)
Destructor Calls.
#define Forall_operands(it, expr)
Definition expr.h:27
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
Definition expr_cast.h:81
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:1533
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2102
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition std_expr.h:715
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:426
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2450
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
std::list< irep_idt > temporaries
Identifiers of temporaries introduced while cleaning an expression.
void add(clean_expr_resultt &&other)
void add_temporary(const irep_idt &id)
goto_programt side_effects
Statements implementing side effects of the expression that was subject to cleaning.
Symbol table entry.