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 
23 static bool have_to_rewrite_union(const exprt &expr)
24 {
25  if(expr.id()==ID_member)
26  {
27  const exprt &op=to_member_expr(expr).struct_op();
28 
29  if(op.type().id() == ID_union_tag || op.type().id() == ID_union)
30  return true;
31  }
32  else if(expr.id()==ID_union)
33  return true;
34 
35  forall_operands(it, expr)
36  if(have_to_rewrite_union(*it))
37  return true;
38 
39  return false;
40 }
41 
42 // inside an address of (&x), unions can simply
43 // be type casts and don't have to be re-written!
45 {
46  if(!have_to_rewrite_union(expr))
47  return;
48 
49  if(expr.id()==ID_index)
50  {
52  rewrite_union(to_index_expr(expr).index());
53  }
54  else if(expr.id()==ID_member)
56  else if(expr.id()==ID_symbol)
57  {
58  // done!
59  }
60  else if(expr.id()==ID_dereference)
62 }
63 
66 void rewrite_union(exprt &expr)
67 {
68  if(expr.id()==ID_address_of)
69  {
71  return;
72  }
73 
74  if(!have_to_rewrite_union(expr))
75  return;
76 
77  Forall_operands(it, expr)
78  rewrite_union(*it);
79 
80  if(expr.id()==ID_member)
81  {
82  const exprt &op=to_member_expr(expr).struct_op();
83 
84  if(op.type().id() == ID_union_tag || op.type().id() == ID_union)
85  {
86  exprt offset=from_integer(0, index_type());
87  byte_extract_exprt tmp(byte_extract_id(), op, offset, expr.type());
88  expr=tmp;
89  }
90  }
91  else if(expr.id()==ID_union)
92  {
93  const union_exprt &union_expr=to_union_expr(expr);
94  exprt offset=from_integer(0, index_type());
95  side_effect_expr_nondett nondet(expr.type(), expr.source_location());
97  byte_update_id(), nondet, offset, union_expr.op());
98  expr=tmp;
99  }
100 }
101 
103 {
104  Forall_goto_program_instructions(it, goto_function.body)
105  {
106  rewrite_union(it->code);
107  rewrite_union(it->guard);
108  }
109 }
110 
111 void rewrite_union(goto_functionst &goto_functions)
112 {
113  Forall_goto_functions(it, goto_functions)
114  rewrite_union(it->second);
115 }
116 
117 void rewrite_union(goto_modelt &goto_model)
118 {
119  rewrite_union(goto_model.goto_functions);
120 }
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:809
rewrite_union.h
byte_update_exprt
TO_BE_DOCUMENTED.
Definition: byte_operators.h:70
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:26
arith_tools.h
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1648
union_exprt
Union constructor from single element.
Definition: std_expr.h:1840
goto_model.h
exprt
Base class for all expressions.
Definition: expr.h:54
goto_modelt
Definition: goto_model.h:24
to_union_expr
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition: std_expr.h:1890
byte_update_id
irep_idt byte_update_id()
Definition: byte_operators.cpp:28
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
byte_extract_id
irep_idt byte_extract_id()
Definition: byte_operators.cpp:13
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
byte_operators.h
Expression classes for byte-level operators.
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: std_expr.h:3282
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:20
member_exprt::struct_op
const exprt & struct_op() const
Definition: std_expr.h:3931
dereference_exprt::pointer
exprt & pointer()
Definition: std_expr.h:3380
rewrite_union
void rewrite_union(exprt &expr)
We rewrite u.c for unions u into byte_extract(u, 0), and { .c = v } into byte_update(NIL,...
Definition: rewrite_union.cpp:66
irept::id
const irep_idt & id() const
Definition: irep.h:259
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:371
std_code.h
Forall_goto_functions
#define Forall_goto_functions(it, functions)
Definition: goto_functions.h:144
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1633
have_to_rewrite_union
static bool have_to_rewrite_union(const exprt &expr)
Definition: rewrite_union.cpp:23
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:22
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: std_expr.h:3397
rewrite_union_address_of
void rewrite_union_address_of(exprt &expr)
Definition: rewrite_union.cpp:44
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:123
byte_extract_exprt
TO_BE_DOCUMENTED.
Definition: byte_operators.h:25
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3959
std_expr.h
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:228
c_types.h