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 #include <util/c_types.h>
13 
15 {
16  const exprt::operandst &ops=expr.operands();
17 
18  std::size_t width=boolbv_width(expr.type());
19 
20  if(width==0)
21  return conversion_failed(expr);
22 
23  bvt bv=convert_bv(ops[0]);
24 
25  if(bv.size()!=width)
26  throw "update: unexpected operand 0 width";
27 
28  // start the recursion
30  expr.op1().operands(), 0, expr.type(), 0, expr.op2(), bv);
31 
32  return bv;
33 }
34 
36  const exprt::operandst &designators,
37  std::size_t d,
38  const typet &type,
39  std::size_t offset,
40  const exprt &new_value,
41  bvt &bv)
42 {
43  if(d>=designators.size())
44  {
45  // done
46  bvt new_value_bv=convert_bv(new_value);
47  std::size_t new_value_width=boolbv_width(type);
48 
49  if(new_value_width!=new_value_bv.size())
50  throw "convert_update_rec: unexpected new_value size";
51 
52  // update
53  for(std::size_t i=0; i<new_value_width; i++)
54  {
55  assert(offset+i<bv.size());
56  bv[offset+i]=new_value_bv[i];
57  }
58 
59  return;
60  }
61 
62  const exprt &designator=designators[d];
63 
64  if(designator.id()==ID_index_designator)
65  {
66  if(type.id()!=ID_array)
67  throw "update: index designator needs array";
68 
69  if(designator.operands().size()!=1)
70  throw "update: index designator takes one operand";
71 
72  bvt index_bv = convert_bv(to_index_designator(designator).index());
73 
74  const array_typet &array_type=to_array_type(type);
75  const typet &subtype = array_type.subtype();
76  const exprt &size_expr = array_type.size();
77 
78  std::size_t element_size=boolbv_width(subtype);
79 
81  size_expr.id() == ID_constant,
82  "array in update expression should be constant-sized");
83 
84  // iterate over array
85  const std::size_t size =
86  numeric_cast_v<std::size_t>(to_constant_expr(size_expr));
87 
88  bvt tmp_bv=bv;
89 
90  for(std::size_t i = 0; i != size; ++i)
91  {
92  std::size_t new_offset=offset+i*element_size;
93 
95  designators, d+1, subtype, new_offset, new_value, tmp_bv);
96 
97  bvt const_bv=bv_utils.build_constant(i, index_bv.size());
98  literalt equal=bv_utils.equal(const_bv, index_bv);
99 
100  for(std::size_t j=0; j<element_size; j++)
101  {
102  std::size_t idx=new_offset+j;
103  assert(idx<bv.size());
104  bv[idx]=prop.lselect(equal, tmp_bv[idx], bv[idx]);
105  }
106  }
107  }
108  else if(designator.id()==ID_member_designator)
109  {
110  const irep_idt &component_name=designator.get(ID_component_name);
111 
112  if(ns.follow(type).id() == ID_struct)
113  {
114  const struct_typet &struct_type = to_struct_type(ns.follow(type));
115 
116  std::size_t struct_offset=0;
117 
119  component.make_nil();
120 
121  const struct_typet::componentst &components=
122  struct_type.components();
123 
124  for(const auto &c : components)
125  {
126  const typet &subtype = c.type();
127  std::size_t sub_width=boolbv_width(subtype);
128 
129  if(c.get_name() == component_name)
130  {
131  component = c;
132  break; // done
133  }
134 
135  struct_offset+=sub_width;
136  }
137 
138  if(component.is_nil())
139  throw "update: failed to find struct component";
140 
141  const typet &new_type = component.type();
142 
143  std::size_t new_offset=offset+struct_offset;
144 
145  // recursive call
147  designators, d+1, new_type, new_offset, new_value, bv);
148  }
149  else if(ns.follow(type).id() == ID_union)
150  {
151  const union_typet &union_type = to_union_type(ns.follow(type));
152 
154  union_type.get_component(component_name);
155 
156  if(component.is_nil())
157  throw "update: failed to find union component";
158 
159  // this only adjusts the type, the offset stays as-is
160 
161  const typet &new_type = component.type();
162 
163  // recursive call
165  designators, d+1, new_type, offset, new_value, bv);
166  }
167  else
168  throw "update: member designator needs struct or union";
169  }
170  else
171  throw "update: unexpected designator";
172 }
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:141
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
to_union_type
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: c_types.h:149
typet::subtype
const typet & subtype() const
Definition: type.h:47
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:302
ternary_exprt::op2
exprt & op2()
Definition: expr.h:109
typet
The type of an expression, extends irept.
Definition: type.h:28
bvt
std::vector< literalt > bvt
Definition: literal.h:201
ternary_exprt::op1
exprt & op1()
Definition: expr.h:106
exprt
Base class for all expressions.
Definition: expr.h:54
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:134
component
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:55
array_typet::size
const exprt & size() const
Definition: std_types.h:765
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
boolbvt::conversion_failed
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:126
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
boolbvt::boolbv_width
virtual std::size_t boolbv_width(const typet &type) const
Definition: boolbv.h:96
arrayst::ns
const namespacet & ns
Definition: arrays.h:54
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:35
irept::id
const irep_idt & id() const
Definition: irep.h:407
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
union_typet
The union type.
Definition: c_types.h:112
boolbvt::convert_bv
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
Definition: boolbv.cpp:47
update_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:2356
struct_union_typet::componentt
Definition: std_types.h:63
bv_utilst::build_constant
static bvt build_constant(const mp_integer &i, std::size_t width)
Definition: bv_utils.cpp:13
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:225
array_typet
Arrays with given size.
Definition: std_types.h:757
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:52
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
boolbvt::bv_utils
bv_utilst bv_utils
Definition: boolbv.h:111
literalt
Definition: literal.h:26
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:807
boolbv.h
exprt::operands
operandst & operands()
Definition: expr.h:96
bv_utilst::equal
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
Definition: bv_utils.cpp:1105
propt::lselect
virtual literalt lselect(literalt a, literalt b, literalt c)=0
c_types.h
prop_conv_solvert::prop
propt & prop
Definition: prop_conv_solver.h:128
boolbvt::convert_update
virtual bvt convert_update(const update_exprt &)
Definition: boolbv_update.cpp:14
to_index_designator
const index_designatort & to_index_designator(const exprt &expr)
Cast an exprt to an index_designatort.
Definition: std_expr.h:2287
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2700