cprover
rewrite_union.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbolic Execution of ANSI-C
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "rewrite_union.h"
13 
14 #include <util/arith_tools.h>
15 #include <util/byte_operators.h>
16 #include <util/c_types.h>
17 #include <util/pointer_expr.h>
18 #include <util/std_code.h>
19 
21 
22 static bool have_to_rewrite_union(const exprt &expr)
23 {
24  if(expr.id()==ID_member)
25  {
26  const exprt &op=to_member_expr(expr).struct_op();
27 
28  if(op.type().id() == ID_union_tag || op.type().id() == ID_union)
29  return true;
30  }
31  else if(expr.id()==ID_union)
32  return true;
33 
34  forall_operands(it, expr)
35  if(have_to_rewrite_union(*it))
36  return true;
37 
38  return false;
39 }
40 
41 // inside an address of (&x), unions can simply
42 // be type casts and don't have to be re-written!
44 {
45  if(!have_to_rewrite_union(expr))
46  return;
47 
48  if(expr.id()==ID_index)
49  {
51  rewrite_union(to_index_expr(expr).index());
52  }
53  else if(expr.id()==ID_member)
54  rewrite_union_address_of(to_member_expr(expr).struct_op());
55  else if(expr.id()==ID_symbol)
56  {
57  // done!
58  }
59  else if(expr.id()==ID_dereference)
60  rewrite_union(to_dereference_expr(expr).pointer());
61 }
62 
65 void rewrite_union(exprt &expr)
66 {
67  if(expr.id()==ID_address_of)
68  {
70  return;
71  }
72 
73  if(!have_to_rewrite_union(expr))
74  return;
75 
76  Forall_operands(it, expr)
77  rewrite_union(*it);
78 
79  if(expr.id()==ID_member)
80  {
81  const exprt &op=to_member_expr(expr).struct_op();
82 
83  if(op.type().id() == ID_union_tag || op.type().id() == ID_union)
84  {
85  exprt offset=from_integer(0, index_type());
86  expr = make_byte_extract(op, offset, expr.type());
87  }
88  }
89  else if(expr.id()==ID_union)
90  {
91  const union_exprt &union_expr=to_union_expr(expr);
92  exprt offset=from_integer(0, index_type());
93  side_effect_expr_nondett nondet(expr.type(), expr.source_location());
94  expr = make_byte_update(nondet, offset, union_expr.op());
95  }
96 }
97 
99 {
100  for(auto &instruction : goto_function.body.instructions)
101  {
102  rewrite_union(instruction.code_nonconst());
103 
104  if(instruction.has_condition())
105  {
106  exprt c = instruction.get_condition();
107  rewrite_union(c);
108  instruction.set_condition(c);
109  }
110  }
111 }
112 
113 void rewrite_union(goto_functionst &goto_functions)
114 {
115  for(auto &gf_entry : goto_functions.function_map)
116  rewrite_union(gf_entry.second);
117 }
118 
119 void rewrite_union(goto_modelt &goto_model)
120 {
121  rewrite_union(goto_model.goto_functions);
122 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
Expression classes for byte-level operators.
bitvector_typet index_type()
Definition: c_types.cpp:16
Base class for all expressions.
Definition: expr.h:54
const source_locationt & source_location() const
Definition: expr.h:230
typet & type()
Return the type of the expression.
Definition: expr.h:82
A collection of goto functions.
function_mapt function_map
::goto_functiont goto_functiont
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
const irep_idt & id() const
Definition: irep.h:407
const exprt & struct_op() const
Definition: std_expr.h:2643
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1966
const exprt & op() const
Definition: std_expr.h:293
Union constructor from single element.
Definition: std_expr.h:1602
#define forall_operands(it, expr)
Definition: expr.h:18
#define Forall_operands(it, expr)
Definition: expr.h:25
Symbol Table + CFG.
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:684
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:378
static bool have_to_rewrite_union(const exprt &expr)
void rewrite_union_address_of(exprt &expr)
void rewrite_union(exprt &expr)
We rewrite u.c for unions u into byte_extract(u, 0), and { .c = v } into byte_update(NIL,...
Symbolic Execution.
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition: std_expr.h:1648
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2697
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1382
byte_update_exprt make_byte_update(const exprt &_op, const exprt &_offset, const exprt &_value)
Construct a byte_update_exprt with endianness and byte width matching the current configuration.
byte_extract_exprt make_byte_extract(const exprt &_op, const exprt &_offset, const typet &_type)
Construct a byte_extract_exprt with endianness and byte width matching the current configuration.