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