cprover
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
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{
110 expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_implies);
112 expr.is_boolean(),
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 }
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(
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 {
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 {
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
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
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition: expr.cpp:51
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:42
exprt & op0()
Definition: expr.h:99
exprt & op1()
Definition: expr.h:102
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
const source_locationt & source_location() const
Definition: expr.h:230
source_locationt & add_source_location()
Definition: expr.h:235
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 & cond()
Definition: std_expr.h:2243
exprt & false_case()
Definition: std_expr.h:2263
exprt & true_case()
Definition: std_expr.h:2253
Array index operator.
Definition: std_expr.h:1328
exprt & index()
Definition: std_expr.h:1363
exprt & array()
Definition: std_expr.h:1353
bool is_not_nil() const
Definition: irep.h:380
void make_nil()
Definition: irep.h:454
void swap(irept &irep)
Definition: irep.h:442
const irep_idt & id() const
Definition: irep.h:396
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 address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:398
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:704
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 index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1391
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 if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2291
destructor_treet destructor_stack
Symbol table entry.