cprover
Loading...
Searching...
No Matches
rewrite_union.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Symbolic Execution of ANSI-C
4
5Author: 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
22static 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)
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)
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
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, c_index_type());
86 expr = make_byte_extract(op, offset, expr.type());
87 }
88 }
89 else if(expr.id()==ID_union)
90 {
92 exprt offset = from_integer(0, c_index_type());
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();
108 instruction.set_condition(c);
109 }
110 }
111}
112
113void rewrite_union(goto_functionst &goto_functions)
114{
115 for(auto &gf_entry : goto_functions.function_map)
116 rewrite_union(gf_entry.second);
117}
118
119void 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)
Expression classes for byte-level operators.
bitvector_typet c_index_type()
Definition c_types.cpp:16
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
Base class for all expressions.
Definition expr.h:54
typet & type()
Return the type of the expression.
Definition expr.h:82
const source_locationt & source_location() const
Definition expr.h:230
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:396
const exprt & struct_op() const
Definition std_expr.h:2697
A side_effect_exprt that returns a non-deterministically chosen value.
Definition std_code.h:1520
Union constructor from single element.
Definition std_expr.h:1611
#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 address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
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 index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1391
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2751
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition std_expr.h:1657
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.