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_type)
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  const std::size_t size = numeric_cast_v<std::size_t>(array_type.size());
88 
89  bvt tmp_bv=bv;
90 
91  for(std::size_t i = 0; i != size; ++i)
92  {
93  std::size_t new_offset=offset+i*element_size;
94 
96  designators, d+1, subtype, new_offset, new_value, tmp_bv);
97 
98  bvt const_bv=bv_utils.build_constant(i, index_bv.size());
99  literalt equal=bv_utils.equal(const_bv, index_bv);
100 
101  for(std::size_t j=0; j<element_size; j++)
102  {
103  std::size_t idx=new_offset+j;
104  assert(idx<bv.size());
105  bv[idx]=prop.lselect(equal, tmp_bv[idx], bv[idx]);
106  }
107  }
108  }
109  else if(designator.id()==ID_member_designator)
110  {
111  const irep_idt &component_name=designator.get(ID_component_name);
112 
113  if(type.id()==ID_struct)
114  {
115  const struct_typet &struct_type=
116  to_struct_type(type);
117 
118  std::size_t struct_offset=0;
119 
121  component.make_nil();
122 
123  const struct_typet::componentst &components=
124  struct_type.components();
125 
126  for(const auto &c : components)
127  {
128  const typet &subtype = c.type();
129  std::size_t sub_width=boolbv_width(subtype);
130 
131  if(c.get_name() == component_name)
132  {
133  component = c;
134  break; // done
135  }
136 
137  struct_offset+=sub_width;
138  }
139 
140  if(component.is_nil())
141  throw "update: failed to find struct component";
142 
143  const typet &new_type=ns.follow(component.type());
144 
145  std::size_t new_offset=offset+struct_offset;
146 
147  // recursive call
149  designators, d+1, new_type, new_offset, new_value, bv);
150  }
151  else if(type.id()==ID_union)
152  {
153  const union_typet &union_type=
154  to_union_type(type);
155 
157  union_type.get_component(component_name);
158 
159  if(component.is_nil())
160  throw "update: failed to find union component";
161 
162  // this only adjusts the type, the offset stays as-is
163 
164  const typet &new_type=ns.follow(component.type());
165 
166  // recursive call
168  designators, d+1, new_type, offset, new_value, bv);
169  }
170  else
171  throw "update: member designator needs struct or union";
172  }
173  else
174  throw "update: unexpected designator";
175 }
exprt::op2
exprt & op2()
Definition: expr.h:90
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:205
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
arith_tools.h
struct_union_typet::get_component
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
Definition: std_types.cpp:53
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:349
typet
The type of an expression, extends irept.
Definition: type.h:27
bvt
std::vector< literalt > bvt
Definition: literal.h:200
boolbvt::convert_update
virtual bvt convert_update(const exprt &expr)
Definition: boolbv_update.cpp:13
exprt
Base class for all expressions.
Definition: expr.h:54
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:203
exprt::op0
exprt & op0()
Definition: expr.h:84
component
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:173
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
boolbvt::boolbv_width
boolbv_widtht boolbv_width
Definition: boolbv.h:92
boolbvt::conversion_failed
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:110
exprt::op1
exprt & op1()
Definition: expr.h:87
boolbvt::convert_update_rec
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)
Definition: boolbv_update.cpp:37
decision_proceduret::ns
const namespacet & ns
Definition: decision_procedure.h:61
irept::id
const irep_idt & id() const
Definition: irep.h:259
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:57
union_typet
The union type.
Definition: std_types.h:425
boolbvt::convert_bv
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Definition: boolbv.cpp:112
struct_union_typet::componentt
Definition: std_types.h:121
bv_utilst::build_constant
bvt build_constant(const mp_integer &i, std::size_t width)
Definition: bv_utils.cpp:15
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:276
array_typet
Arrays with given size.
Definition: std_types.h:1000
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
boolbvt::bv_utils
bv_utilst bv_utils
Definition: boolbv.h:95
literalt
Definition: literal.h:24
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1048
boolbv.h
exprt::operands
operandst & operands()
Definition: expr.h:78
to_union_type
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: std_types.h:450
bv_utilst::equal
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
Definition: bv_utils.cpp:1116
propt::lselect
virtual literalt lselect(literalt a, literalt b, literalt c)=0
prop_conv_solvert::prop
propt & prop
Definition: prop_conv.h:152