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 
48  exprt &expr,
49  const namespacet &ns)
50 {
51  if(!have_to_rewrite_union(expr, ns))
52  return;
53 
54  Forall_operands(it, expr)
55  rewrite_union(*it, ns);
56 
57  if(expr.id()==ID_member)
58  {
59  const exprt &op=to_member_expr(expr).struct_op();
60  const typet &op_type=ns.follow(op.type());
61 
62  if(op_type.id()==ID_union)
63  {
64  exprt offset=from_integer(0, index_type());
65  byte_extract_exprt tmp(byte_extract_id(), op, offset, expr.type());
66  expr=tmp;
67  }
68  }
69  else if(expr.id()==ID_union)
70  {
71  const union_exprt &union_expr=to_union_expr(expr);
72  exprt offset=from_integer(0, index_type());
73  side_effect_expr_nondett nondet(expr.type());
75  byte_update_id(), nondet, offset, union_expr.op());
76  expr=tmp;
77  }
78 }
79 
80 static void rewrite_union(
81  goto_functionst::goto_functiont &goto_function,
82  const namespacet &ns)
83 {
84  Forall_goto_program_instructions(it, goto_function.body)
85  {
86  rewrite_union(it->code, ns);
87  rewrite_union(it->guard, ns);
88  }
89 }
90 
92  goto_functionst &goto_functions,
93  const namespacet &ns)
94 {
95  Forall_goto_functions(it, goto_functions)
96  rewrite_union(it->second, ns);
97 }
98 
99 void rewrite_union(goto_modelt &goto_model)
100 {
101  namespacet ns(goto_model.symbol_table);
102  rewrite_union(goto_model.goto_functions, ns);
103 }
The type of an expression.
Definition: type.h:20
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
const exprt & op() const
Definition: std_expr.h:258
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3302
typet & type()
Definition: expr.h:60
symbol_tablet symbol_table
Definition: goto_model.h:25
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:1389
API to expression classes.
irep_idt byte_extract_id()
TO_BE_DOCUMENTED.
Definition: namespace.h:62
A side effect that returns a non-deterministically chosen value.
Definition: std_code.h:1037
#define forall_operands(it, expr)
Definition: expr.h:17
const union_exprt & to_union_expr(const exprt &expr)
Cast a generic exprt to a union_exprt.
Definition: std_expr.h:1441
bitvector_typet index_type()
Definition: c_types.cpp:15
goto_function_templatet< goto_programt > goto_functiont
Symbolic Execution.
Base class for all expressions.
Definition: expr.h:46
const exprt & struct_op() const
Definition: std_expr.h:3270
#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:73
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)
goto_functionst goto_functions
Definition: goto_model.h:26
static bool have_to_rewrite_union(const exprt &expr, const namespacet &ns)
irep_idt byte_update_id()