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/std_expr.h>
16 #include <util/std_code.h>
17 #include <util/byte_operators.h>
18 
20 
21 #include <util/c_types.h>
22 
24  const exprt &expr,
25  const namespacet &ns)
26 {
27  if(expr.id()==ID_member)
28  {
29  const exprt &op=to_member_expr(expr).struct_op();
30  const typet &op_type=ns.follow(op.type());
31 
32  if(op_type.id()==ID_union)
33  return true;
34  }
35  else if(expr.id()==ID_union)
36  return true;
37 
38  forall_operands(it, expr)
39  if(have_to_rewrite_union(*it, ns))
40  return true;
41 
42  return false;
43 }
44 
45 // inside an address of (&x), unions can simply
46 // be type casts and don't have to be re-written!
48  exprt &expr,
49  const namespacet &ns)
50 {
51  if(!have_to_rewrite_union(expr, ns))
52  return;
53 
54  if(expr.id()==ID_index)
55  {
56  rewrite_union_address_of(to_index_expr(expr).array(), ns);
57  rewrite_union(to_index_expr(expr).index(), ns);
58  }
59  else if(expr.id()==ID_member)
61  else if(expr.id()==ID_symbol)
62  {
63  // done!
64  }
65  else if(expr.id()==ID_dereference)
67 }
68 
72  exprt &expr,
73  const namespacet &ns)
74 {
75  if(expr.id()==ID_address_of)
76  {
77  rewrite_union_address_of(to_address_of_expr(expr).object(), ns);
78  return;
79  }
80 
81  if(!have_to_rewrite_union(expr, ns))
82  return;
83 
84  Forall_operands(it, expr)
85  rewrite_union(*it, ns);
86 
87  if(expr.id()==ID_member)
88  {
89  const exprt &op=to_member_expr(expr).struct_op();
90  const typet &op_type=ns.follow(op.type());
91 
92  if(op_type.id()==ID_union)
93  {
94  exprt offset=from_integer(0, index_type());
95  byte_extract_exprt tmp(byte_extract_id(), op, offset, expr.type());
96  expr=tmp;
97  }
98  }
99  else if(expr.id()==ID_union)
100  {
101  const union_exprt &union_expr=to_union_expr(expr);
102  exprt offset=from_integer(0, index_type());
103  side_effect_expr_nondett nondet(expr.type());
104  byte_update_exprt tmp(
105  byte_update_id(), nondet, offset, union_expr.op());
106  expr=tmp;
107  }
108 }
109 
111  goto_functionst::goto_functiont &goto_function,
112  const namespacet &ns)
113 {
114  Forall_goto_program_instructions(it, goto_function.body)
115  {
116  rewrite_union(it->code, ns);
117  rewrite_union(it->guard, ns);
118  }
119 }
120 
122  goto_functionst &goto_functions,
123  const namespacet &ns)
124 {
125  Forall_goto_functions(it, goto_functions)
126  rewrite_union(it->second, ns);
127 }
128 
129 void rewrite_union(goto_modelt &goto_model)
130 {
131  namespacet ns(goto_model.symbol_table);
132  rewrite_union(goto_model.goto_functions, ns);
133 }
The type of an expression.
Definition: type.h:22
const exprt & op() const
Definition: std_expr.h:340
typet & type()
Definition: expr.h:56
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast a generic exprt to an address_of_exprt.
Definition: std_expr.h:3201
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast a generic exprt to a dereference_exprt.
Definition: std_expr.h:3328
const irep_idt & id() const
Definition: irep.h:189
Symbol Table + CFG.
Expression classes for byte-level operators.
union constructor from single element
Definition: std_expr.h:1730
API to expression classes.
irep_idt byte_extract_id()
TO_BE_DOCUMENTED.
Definition: namespace.h:74
::goto_functiont goto_functiont
void rewrite_union_address_of(exprt &expr, const namespacet &ns)
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3955
A side effect that returns a non-deterministically chosen value.
Definition: std_code.h:1301
#define forall_operands(it, expr)
Definition: expr.h:17
const typet & follow(const typet &) const
Definition: namespace.cpp:55
bitvector_typet index_type()
Definition: c_types.cpp:16
Symbolic Execution.
Base class for all expressions.
Definition: expr.h:42
exprt & pointer()
Definition: std_expr.h:3307
const exprt & struct_op() const
Definition: std_expr.h:3911
const union_exprt & to_union_expr(const exprt &expr)
Cast a generic exprt to a union_exprt.
Definition: std_expr.h:1782
#define Forall_goto_functions(it, functions)
#define Forall_operands(it, expr)
Definition: expr.h:23
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:740
TO_BE_DOCUMENTED.
void rewrite_union(exprt &expr, const namespacet &ns)
We rewrite u.c for unions u into byte_extract(u, 0), and { .c = v } into byte_update(NIL, 0, v)
TO_BE_DOCUMENTED.
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1517
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
static bool have_to_rewrite_union(const exprt &expr, const namespacet &ns)
irep_idt byte_update_id()