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)
55  rewrite_union_address_of(to_member_expr(expr).struct_op());
56  else if(expr.id()==ID_symbol)
57  {
58  // done!
59  }
60  else if(expr.id()==ID_dereference)
61  rewrite_union(to_dereference_expr(expr).pointer());
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 
108  if(it->has_condition())
109  {
110  exprt c = it->get_condition();
111  rewrite_union(c);
112  it->set_condition(c);
113  }
114  }
115 }
116 
117 void rewrite_union(goto_functionst &goto_functions)
118 {
119  Forall_goto_functions(it, goto_functions)
120  rewrite_union(it->second);
121 }
122 
123 void rewrite_union(goto_modelt &goto_model)
124 {
125  rewrite_union(goto_model.goto_functions);
126 }
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:1201
rewrite_union.h
Symbolic Execution.
byte_update_exprt
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
Definition: byte_operators.h:81
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:24
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:1347
union_exprt
Union constructor from single element.
Definition: std_expr.h:1567
goto_model.h
Symbol Table + CFG.
exprt
Base class for all expressions.
Definition: expr.h:53
goto_modelt
Definition: goto_model.h:26
to_union_expr
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition: std_expr.h:1613
byte_update_id
irep_idt byte_update_id()
Definition: byte_operators.cpp:30
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:81
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:2823
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
member_exprt::struct_op
const exprt & struct_op() const
Definition: std_expr.h:3435
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:418
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:281
std_code.h
Forall_goto_functions
#define Forall_goto_functions(it, functions)
Definition: goto_functions.h:117
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:1945
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:23
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: std_expr.h:2944
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:33
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
byte_extract_exprt
Expression of type type extracted from some object op starting at position offset (given in number of...
Definition: byte_operators.h:29
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3489
std_expr.h
API to expression classes.
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:254
c_types.h