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 #include <util/std_expr.h>
20 
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  for(auto &instruction : goto_function.body.instructions)
105  {
106  rewrite_union(instruction.code);
107 
108  if(instruction.has_condition())
109  {
110  exprt c = instruction.get_condition();
111  rewrite_union(c);
112  instruction.set_condition(c);
113  }
114  }
115 }
116 
117 void rewrite_union(goto_functionst &goto_functions)
118 {
119  for(auto &gf_entry : goto_functions.function_map)
120  rewrite_union(gf_entry.second);
121 }
122 
123 void rewrite_union(goto_modelt &goto_model)
124 {
125  rewrite_union(goto_model.goto_functions);
126 }
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
Expression of type type extracted from some object op starting at position offset (given in number of...
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
Base class for all expressions.
Definition: expr.h:54
const source_locationt & source_location() const
Definition: expr.h:234
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:2558
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1968
const exprt & op() const
Definition: std_expr.h:294
Union constructor from single element.
Definition: std_expr.h:1517
#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:312
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:237
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.
API to expression classes.
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition: std_expr.h:1563
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2612
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1297
irep_idt byte_extract_id()
irep_idt byte_update_id()