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