cprover
boolbv_update.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "boolbv.h"
10 
11 #include <util/std_types.h>
12 #include <util/std_expr.h>
13 #include <util/arith_tools.h>
14 #include <util/base_type.h>
15 #include <util/config.h>
17 
18 #include <util/c_types.h>
19 
21 {
22  const exprt::operandst &ops=expr.operands();
23 
24  if(ops.size()!=3)
25  throw "update takes at three operands";
26 
27  std::size_t width=boolbv_width(expr.type());
28 
29  if(width==0)
30  return conversion_failed(expr);
31 
32  bvt bv=convert_bv(ops[0]);
33 
34  if(bv.size()!=width)
35  throw "update: unexpected operand 0 width";
36 
37  // start the recursion
39  expr.op1().operands(), 0, expr.type(), 0, expr.op2(), bv);
40 
41  return bv;
42 }
43 
45  const exprt::operandst &designators,
46  std::size_t d,
47  const typet &type,
48  std::size_t offset,
49  const exprt &new_value,
50  bvt &bv)
51 {
52  if(type.id()==ID_symbol)
54  designators, d, ns.follow(type), offset, new_value, bv);
55 
56  if(d>=designators.size())
57  {
58  // done
59  bvt new_value_bv=convert_bv(new_value);
60  std::size_t new_value_width=boolbv_width(type);
61 
62  if(new_value_width!=new_value_bv.size())
63  throw "convert_update_rec: unexpected new_value size";
64 
65  // update
66  for(std::size_t i=0; i<new_value_width; i++)
67  {
68  assert(offset+i<bv.size());
69  bv[offset+i]=new_value_bv[i];
70  }
71 
72  return;
73  }
74 
75  const exprt &designator=designators[d];
76 
77  if(designator.id()==ID_index_designator)
78  {
79  if(type.id()!=ID_array)
80  throw "update: index designator needs array";
81 
82  if(designator.operands().size()!=1)
83  throw "update: index designator takes one operand";
84 
85  bvt index_bv=convert_bv(designator.op0());
86 
87  const array_typet &array_type=to_array_type(type);
88 
89  const typet &subtype=ns.follow(array_type.subtype());
90 
91  std::size_t element_size=boolbv_width(subtype);
92 
93  // iterate over array
94  mp_integer size;
95  if(to_integer(array_type.size(), size))
96  throw "update: failed to get array size";
97 
98  bvt tmp_bv=bv;
99 
100  for(std::size_t i=0; i!=integer2size_t(size); ++i)
101  {
102  std::size_t new_offset=offset+i*element_size;
103 
105  designators, d+1, subtype, new_offset, new_value, tmp_bv);
106 
107  bvt const_bv=bv_utils.build_constant(i, index_bv.size());
108  literalt equal=bv_utils.equal(const_bv, index_bv);
109 
110  for(std::size_t j=0; j<element_size; j++)
111  {
112  std::size_t idx=new_offset+j;
113  assert(idx<bv.size());
114  bv[idx]=prop.lselect(equal, tmp_bv[idx], bv[idx]);
115  }
116  }
117  }
118  else if(designator.id()==ID_member_designator)
119  {
120  const irep_idt &component_name=designator.get(ID_component_name);
121 
122  if(type.id()==ID_struct)
123  {
124  const struct_typet &struct_type=
125  to_struct_type(type);
126 
127  std::size_t struct_offset=0;
128 
129  struct_typet::componentt component;
130  component.make_nil();
131 
132  const struct_typet::componentst &components=
133  struct_type.components();
134 
135  for(struct_typet::componentst::const_iterator
136  it=components.begin();
137  it!=components.end();
138  it++)
139  {
140  const typet &subtype=it->type();
141  std::size_t sub_width=boolbv_width(subtype);
142 
143  if(it->get_name()==component_name)
144  {
145  component=*it;
146  break; // done
147  }
148 
149  struct_offset+=sub_width;
150  }
151 
152  if(component.is_nil())
153  throw "update: failed to find struct component";
154 
155  const typet &new_type=ns.follow(component.type());
156 
157  std::size_t new_offset=offset+struct_offset;
158 
159  // recursive call
161  designators, d+1, new_type, new_offset, new_value, bv);
162  }
163  else if(type.id()==ID_union)
164  {
165  const union_typet &union_type=
166  to_union_type(type);
167 
168  const union_typet::componentt &component=
169  union_type.get_component(component_name);
170 
171  if(component.is_nil())
172  throw "update: failed to find union component";
173 
174  // this only adjusts the type, the offset stays as-is
175 
176  const typet &new_type=ns.follow(component.type());
177 
178  // recursive call
180  designators, d+1, new_type, offset, new_value, bv);
181  }
182  else
183  throw "update: member designator needs struct or union";
184  }
185  else
186  throw "update: unexpected designator";
187 }
The type of an expression.
Definition: type.h:20
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
bv_utilst bv_utils
Definition: boolbv.h:93
BigInt mp_integer
Definition: mp_arith.h:19
bool is_nil() const
Definition: irep.h:103
exprt & op0()
Definition: expr.h:84
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
Definition: bv_utils.cpp:1089
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
Definition: std_types.h:442
boolbv_widtht boolbv_width
Definition: boolbv.h:90
std::vector< componentt > componentst
Definition: std_types.h:240
const componentst & components() const
Definition: std_types.h:242
typet & type()
Definition: expr.h:60
Structure type.
Definition: std_types.h:296
virtual bvt convert_update(const exprt &expr)
const irep_idt & id() const
Definition: irep.h:189
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:946
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:115
API to expression classes.
exprt & op1()
Definition: expr.h:87
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:108
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
const namespacet & ns
std::vector< exprt > operandst
Definition: expr.h:49
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:317
Pointer Logic.
void convert_update_rec(const exprt::operandst &designator, std::size_t d, const typet &type, std::size_t offset, const exprt &new_value, bvt &bv)
API to type classes.
Base class for all expressions.
Definition: expr.h:46
The union type.
Definition: std_types.h:424
void make_nil()
Definition: irep.h:243
arrays with given size
Definition: std_types.h:901
exprt & op2()
Definition: expr.h:90
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:18
virtual literalt lselect(literalt a, literalt b, literalt c)=0
std::size_t integer2size_t(const mp_integer &n)
Definition: mp_arith.cpp:195
Base Type Computation.
operandst & operands()
Definition: expr.h:70
std::vector< literalt > bvt
Definition: literal.h:197
bvt build_constant(const mp_integer &i, std::size_t width)
Definition: bv_utils.cpp:15
const componentt & get_component(const irep_idt &component_name) const
Definition: std_types.cpp:51