cprover
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 if(width==0)
22 return conversion_failed(expr);
23
24 bvt bv=convert_bv(ops[0]);
25
26 if(bv.size()!=width)
27 throw "update: unexpected operand 0 width";
28
29 // start the recursion
31 expr.op1().operands(), 0, expr.type(), 0, expr.op2(), bv);
32
33 return bv;
34}
35
37 const exprt::operandst &designators,
38 std::size_t d,
39 const typet &type,
40 std::size_t offset,
41 const exprt &new_value,
42 bvt &bv)
43{
44 if(d>=designators.size())
45 {
46 // done
47 bvt new_value_bv=convert_bv(new_value);
48 std::size_t new_value_width=boolbv_width(type);
49
50 if(new_value_width!=new_value_bv.size())
51 throw "convert_update_rec: unexpected new_value size";
52
53 // update
54 for(std::size_t i=0; i<new_value_width; i++)
55 {
56 assert(offset+i<bv.size());
57 bv[offset+i]=new_value_bv[i];
58 }
59
60 return;
61 }
62
63 const exprt &designator=designators[d];
64
65 if(designator.id()==ID_index_designator)
66 {
67 if(type.id()!=ID_array)
68 throw "update: index designator needs array";
69
70 if(designator.operands().size()!=1)
71 throw "update: index designator takes one operand";
72
73 bvt index_bv = convert_bv(to_index_designator(designator).index());
74
75 const array_typet &array_type=to_array_type(type);
76 const typet &subtype = array_type.element_type();
77 const exprt &size_expr = array_type.size();
78
79 std::size_t element_size=boolbv_width(subtype);
80
82 size_expr.id() == ID_constant,
83 "array in update expression should be constant-sized");
84
85 // iterate over array
86 const std::size_t size =
87 numeric_cast_v<std::size_t>(to_constant_expr(size_expr));
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(ns.follow(type).id() == ID_struct)
114 {
115 const struct_typet &struct_type = to_struct_type(ns.follow(type));
116
117 std::size_t struct_offset=0;
118
120 component.make_nil();
121
122 const struct_typet::componentst &components=
123 struct_type.components();
124
125 for(const auto &c : components)
126 {
127 const typet &subtype = c.type();
128 std::size_t sub_width=boolbv_width(subtype);
129
130 if(c.get_name() == component_name)
131 {
132 component = c;
133 break; // done
134 }
135
136 struct_offset+=sub_width;
137 }
138
139 if(component.is_nil())
140 throw "update: failed to find struct component";
141
142 const typet &new_type = component.type();
143
144 std::size_t new_offset=offset+struct_offset;
145
146 // recursive call
148 designators, d+1, new_type, new_offset, new_value, bv);
149 }
150 else if(ns.follow(type).id() == ID_union)
151 {
152 const union_typet &union_type = to_union_type(ns.follow(type));
153
155 union_type.get_component(component_name);
156
157 if(component.is_nil())
158 throw "update: failed to find union component";
159
160 // this only adjusts the type, the offset stays as-is
161
162 const typet &new_type = component.type();
163
164 // recursive call
166 designators, d+1, new_type, offset, new_value, bv);
167 }
168 else
169 throw "update: member designator needs struct or union";
170 }
171 else
172 throw "update: unexpected designator";
173}
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: c_types.h:162
Arrays with given size.
Definition: std_types.h:763
const exprt & size() const
Definition: std_types.h:790
const typet & element_type() const
The type of the elements of the array.
Definition: std_types.h:777
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 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:40
virtual bvt convert_update(const update_exprt &)
bv_utilst bv_utils
Definition: boolbv.h:114
bvt conversion_failed(const exprt &expr)
Print that the expression of x has failed conversion, then return a vector of x's width.
Definition: boolbv.cpp:84
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:11
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
Definition: bv_utils.cpp:1103
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:45
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:57
std::vector< componentt > componentst
Definition: std_types.h:140
exprt & op1()
Definition: expr.h:102
exprt & op2()
Definition: expr.h:105
The type of an expression, extends irept.
Definition: type.h:29
The union type.
Definition: c_types.h:125
Operator to update elements in structs and arrays.
Definition: std_expr.h:2496
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:510
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:48
const index_designatort & to_index_designator(const exprt &expr)
Cast an exprt to an index_designatort.
Definition: std_expr.h:2427
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2840
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:832