Skip to content

Commit 5cf2b07

Browse files
committed
Make pointer flattened width configurable by bv_pointerst
In preparation of tweaking the propositional encoding, place all knowledge of the bit width of encoded pointers in bv_pointerst. Also, do not hard-code the width just once, but really look at each type.
1 parent d281545 commit 5cf2b07

File tree

2 files changed

+144
-38
lines changed

2 files changed

+144
-38
lines changed

src/solvers/flattening/bv_pointers.cpp

Lines changed: 116 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -65,7 +65,51 @@ void bv_endianness_mapt::build_big_endian(const typet &src)
6565
endianness_mapt
6666
bv_pointerst::endianness_map(const typet &type, bool little_endian) const
6767
{
68-
return bv_endianness_mapt{type, little_endian, ns, bv_width};
68+
return bv_endianness_mapt{type, little_endian, ns, bv_pointers_width};
69+
}
70+
71+
std::size_t bv_pointerst::bv_pointers_widtht::
72+
operator()(const typet &type) const
73+
{
74+
if(type.id() != ID_pointer)
75+
return boolbv_widtht::operator()(type);
76+
77+
// check or update the cache, just like boolbv_widtht does
78+
std::pair<cachet::iterator, bool> cache_result =
79+
cache.insert(std::pair<typet, entryt>(type, entryt()));
80+
81+
if(cache_result.second)
82+
{
83+
std::size_t &total_width = cache_result.first->second.total_width;
84+
85+
total_width = get_address_width(to_pointer_type(type));
86+
DATA_INVARIANT(total_width > 0, "pointer width shall be greater than zero");
87+
}
88+
89+
return cache_result.first->second.total_width;
90+
}
91+
92+
std::size_t bv_pointerst::bv_pointers_widtht::get_object_width(
93+
const pointer_typet &type) const
94+
{
95+
// not actually type-dependent for now
96+
(void)type;
97+
return config.bv_encoding.object_bits;
98+
}
99+
100+
std::size_t bv_pointerst::bv_pointers_widtht::get_offset_width(
101+
const pointer_typet &type) const
102+
{
103+
const std::size_t pointer_width = type.get_width();
104+
const std::size_t object_width = get_object_width(type);
105+
PRECONDITION(pointer_width >= object_width);
106+
return pointer_width - object_width;
107+
}
108+
109+
std::size_t bv_pointerst::bv_pointers_widtht::get_address_width(
110+
const pointer_typet &type) const
111+
{
112+
return type.get_width();
69113
}
70114

71115
literalt bv_pointerst::convert_rest(const exprt &expr)
@@ -83,8 +127,15 @@ literalt bv_pointerst::convert_rest(const exprt &expr)
83127

84128
if(!bv.empty())
85129
{
130+
const pointer_typet &type = to_pointer_type(operands[0].type());
131+
86132
bvt invalid_bv;
87-
encode(pointer_logic.get_invalid_object(), invalid_bv);
133+
encode(pointer_logic.get_invalid_object(), type, invalid_bv);
134+
135+
const std::size_t object_bits =
136+
bv_pointers_width.get_object_width(type);
137+
const std::size_t offset_bits =
138+
bv_pointers_width.get_offset_width(type);
88139

89140
bvt equal_invalid_bv;
90141
equal_invalid_bv.resize(object_bits);
@@ -139,12 +190,9 @@ bv_pointerst::bv_pointerst(
139190
message_handlert &message_handler,
140191
bool get_array_constraints)
141192
: boolbvt(_ns, _prop, message_handler, get_array_constraints),
142-
pointer_logic(_ns)
193+
pointer_logic(_ns),
194+
bv_pointers_width(_ns)
143195
{
144-
object_bits=config.bv_encoding.object_bits;
145-
std::size_t pointer_width = boolbv_width(pointer_type(empty_typet()));
146-
offset_bits=pointer_width-object_bits;
147-
bits=pointer_width;
148196
}
149197

150198
bool bv_pointerst::convert_address_of_rec(
@@ -163,7 +211,8 @@ bool bv_pointerst::convert_address_of_rec(
163211
}
164212
else if(expr.id() == ID_null_object)
165213
{
166-
encode(pointer_logic.get_null_object(), bv);
214+
pointer_typet pt = pointer_type(expr.type());
215+
encode(pointer_logic.get_null_object(), pt, bv);
167216
return false;
168217
}
169218
else if(expr.id()==ID_index)
@@ -173,6 +222,9 @@ bool bv_pointerst::convert_address_of_rec(
173222
const exprt &index=index_expr.index();
174223
const typet &array_type = array.type();
175224

225+
pointer_typet type = pointer_type(expr.type());
226+
const std::size_t bits = boolbv_width(type);
227+
176228
// recursive call
177229
if(array_type.id()==ID_pointer)
178230
{
@@ -194,7 +246,7 @@ bool bv_pointerst::convert_address_of_rec(
194246
auto size = pointer_offset_size(array_type.subtype(), ns);
195247
CHECK_RETURN(size.has_value() && *size >= 0);
196248

197-
offset_arithmetic(bv, *size, index);
249+
offset_arithmetic(type, bv, *size, index);
198250
CHECK_RETURN(bv.size()==bits);
199251
return false;
200252
}
@@ -207,9 +259,11 @@ bool bv_pointerst::convert_address_of_rec(
207259
if(convert_address_of_rec(byte_extract_expr.op(), bv))
208260
return true;
209261

262+
pointer_typet type = pointer_type(expr.type());
263+
const std::size_t bits = boolbv_width(type);
210264
CHECK_RETURN(bv.size()==bits);
211265

212-
offset_arithmetic(bv, 1, byte_extract_expr.offset());
266+
offset_arithmetic(type, bv, 1, byte_extract_expr.offset());
213267
CHECK_RETURN(bv.size()==bits);
214268
return false;
215269
}
@@ -230,7 +284,8 @@ bool bv_pointerst::convert_address_of_rec(
230284
CHECK_RETURN(offset.has_value());
231285

232286
// add offset
233-
offset_arithmetic(bv, *offset);
287+
pointer_typet type = pointer_type(expr.type());
288+
offset_arithmetic(type, bv, *offset);
234289
}
235290
else
236291
{
@@ -273,15 +328,13 @@ bool bv_pointerst::convert_address_of_rec(
273328

274329
bvt bv_pointerst::convert_pointer_type(const exprt &expr)
275330
{
276-
PRECONDITION(expr.type().id() == ID_pointer);
331+
const pointer_typet &type = to_pointer_type(expr.type());
277332

278-
// make sure the config hasn't been changed
279-
PRECONDITION(bits==boolbv_width(expr.type()));
333+
const std::size_t bits = boolbv_width(expr.type());
280334

281335
if(expr.id()==ID_symbol)
282336
{
283337
const irep_idt &identifier=to_symbol_expr(expr).get_identifier();
284-
const typet &type=expr.type();
285338

286339
return map.get_literals(identifier, type, bits);
287340
}
@@ -352,7 +405,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
352405
bv.resize(bits);
353406

354407
if(value==ID_NULL)
355-
encode(pointer_logic.get_null_object(), bv);
408+
encode(pointer_logic.get_null_object(), type, bv);
356409
else
357410
{
358411
mp_integer i = bvrep2integer(value, bits, false);
@@ -433,7 +486,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
433486
sum=bv_utils.add(sum, op);
434487
}
435488

436-
offset_arithmetic(bv, size, sum);
489+
offset_arithmetic(type, bv, size, sum);
437490

438491
return bv;
439492
}
@@ -476,7 +529,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
476529
element_size = *element_size_opt;
477530
}
478531

479-
offset_arithmetic(bv, element_size, neg_op1);
532+
offset_arithmetic(type, bv, element_size, neg_op1);
480533

481534
return bv;
482535
}
@@ -556,18 +609,20 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
556609
expr.id() == ID_pointer_offset &&
557610
to_unary_expr(expr).op().type().id() == ID_pointer)
558611
{
559-
bvt op0 = convert_bv(to_unary_expr(expr).op());
612+
const exprt &op0 = to_unary_expr(expr).op();
613+
bvt op0_bv = convert_bv(op0);
560614

561615
std::size_t width=boolbv_width(expr.type());
562616

563617
if(width==0)
564618
return conversion_failed(expr);
565619

566620
// we need to strip off the object part
567-
op0.resize(offset_bits);
621+
op0_bv.resize(
622+
bv_pointers_width.get_offset_width(to_pointer_type(op0.type())));
568623

569624
// we do a sign extension to permit negative offsets
570-
return bv_utils.sign_extension(op0, width);
625+
return bv_utils.sign_extension(op0_bv, width);
571626
}
572627
else if(
573628
expr.id() == ID_object_size &&
@@ -594,7 +649,8 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
594649
expr.id() == ID_pointer_object &&
595650
to_unary_expr(expr).op().type().id() == ID_pointer)
596651
{
597-
bvt op0 = convert_bv(to_unary_expr(expr).op());
652+
const exprt &op0 = to_unary_expr(expr).op();
653+
bvt op0_bv = convert_bv(op0);
598654

599655
std::size_t width=boolbv_width(expr.type());
600656

@@ -603,9 +659,12 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
603659

604660
// erase offset bits
605661

606-
op0.erase(op0.begin()+0, op0.begin()+offset_bits);
662+
op0_bv.erase(
663+
op0_bv.begin() + 0,
664+
op0_bv.begin() +
665+
bv_pointers_width.get_offset_width(to_pointer_type(op0.type())));
607666

608-
return bv_utils.zero_extension(op0, width);
667+
return bv_utils.zero_extension(op0_bv, width);
609668
}
610669
else if(
611670
expr.id() == ID_typecast &&
@@ -638,6 +697,9 @@ exprt bv_pointerst::bv_get_rec(
638697

639698
std::string value_addr, value_offset, value;
640699

700+
const std::size_t bits = boolbv_width(to_pointer_type(type));
701+
const std::size_t offset_bits =
702+
bv_pointers_width.get_offset_width(to_pointer_type(type));
641703
for(std::size_t i=0; i<bits; i++)
642704
{
643705
char ch=0;
@@ -681,9 +743,13 @@ exprt bv_pointerst::bv_get_rec(
681743
return std::move(result);
682744
}
683745

684-
void bv_pointerst::encode(std::size_t addr, bvt &bv)
746+
void bv_pointerst::encode(std::size_t addr, const pointer_typet &type, bvt &bv)
747+
const
685748
{
686-
bv.resize(bits);
749+
const std::size_t offset_bits = bv_pointers_width.get_offset_width(type);
750+
const std::size_t object_bits = bv_pointers_width.get_object_width(type);
751+
752+
bv.resize(boolbv_width(type));
687753

688754
// set offset to zero
689755
for(std::size_t i=0; i<offset_bits; i++)
@@ -694,8 +760,13 @@ void bv_pointerst::encode(std::size_t addr, bvt &bv)
694760
bv[offset_bits+i]=const_literal((addr&(std::size_t(1)<<i))!=0);
695761
}
696762

697-
void bv_pointerst::offset_arithmetic(bvt &bv, const mp_integer &x)
763+
void bv_pointerst::offset_arithmetic(
764+
const pointer_typet &type,
765+
bvt &bv,
766+
const mp_integer &x)
698767
{
768+
const std::size_t offset_bits = bv_pointers_width.get_offset_width(type);
769+
699770
bvt bv1=bv;
700771
bv1.resize(offset_bits); // strip down
701772

@@ -709,6 +780,7 @@ void bv_pointerst::offset_arithmetic(bvt &bv, const mp_integer &x)
709780
}
710781

711782
void bv_pointerst::offset_arithmetic(
783+
const pointer_typet &type,
712784
bvt &bv,
713785
const mp_integer &factor,
714786
const exprt &index)
@@ -719,12 +791,14 @@ void bv_pointerst::offset_arithmetic(
719791
index.type().id()==ID_signedbv?bv_utilst::representationt::SIGNED:
720792
bv_utilst::representationt::UNSIGNED;
721793

794+
const std::size_t offset_bits = bv_pointers_width.get_offset_width(type);
722795
bv_index=bv_utils.extension(bv_index, offset_bits, rep);
723796

724-
offset_arithmetic(bv, factor, bv_index);
797+
offset_arithmetic(type, bv, factor, bv_index);
725798
}
726799

727800
void bv_pointerst::offset_arithmetic(
801+
const pointer_typet &type,
728802
bvt &bv,
729803
const mp_integer &factor,
730804
const bvt &index)
@@ -744,6 +818,7 @@ void bv_pointerst::offset_arithmetic(
744818
bvt bv_tmp=bv_utils.add(bv, bv_index);
745819

746820
// copy lower parts of result
821+
const std::size_t offset_bits = bv_pointers_width.get_offset_width(type);
747822
for(std::size_t i=0; i<offset_bits; i++)
748823
bv[i]=bv_tmp[i];
749824
}
@@ -752,6 +827,8 @@ void bv_pointerst::add_addr(const exprt &expr, bvt &bv)
752827
{
753828
std::size_t a=pointer_logic.add_object(expr);
754829

830+
const pointer_typet type = pointer_type(expr.type());
831+
const std::size_t object_bits = bv_pointers_width.get_object_width(type);
755832
const std::size_t max_objects=std::size_t(1)<<object_bits;
756833

757834
if(a==max_objects)
@@ -761,14 +838,17 @@ void bv_pointerst::add_addr(const exprt &expr, bvt &bv)
761838
"); " +
762839
"use the `--object-bits n` option to increase the maximum number");
763840

764-
encode(a, bv);
841+
encode(a, type, bv);
765842
}
766843

767844
void bv_pointerst::do_postponed(
768845
const postponedt &postponed)
769846
{
770847
if(postponed.expr.id() == ID_is_dynamic_object)
771848
{
849+
const std::size_t offset_bits = bv_pointers_width.get_offset_width(
850+
to_pointer_type(to_unary_expr(postponed.expr).op().type()));
851+
772852
const auto &objects = pointer_logic.objects;
773853
std::size_t number=0;
774854

@@ -780,7 +860,8 @@ void bv_pointerst::do_postponed(
780860

781861
// only compare object part
782862
bvt bv;
783-
encode(number, bv);
863+
pointer_typet pt = pointer_type(expr.type());
864+
encode(number, pt, bv);
784865

785866
bv.erase(bv.begin(), bv.begin()+offset_bits);
786867

@@ -801,6 +882,9 @@ void bv_pointerst::do_postponed(
801882
}
802883
else if(postponed.expr.id()==ID_object_size)
803884
{
885+
const std::size_t offset_bits = bv_pointers_width.get_offset_width(
886+
to_pointer_type(to_unary_expr(postponed.expr).op().type()));
887+
804888
const auto &objects = pointer_logic.objects;
805889
std::size_t number=0;
806890

@@ -821,7 +905,8 @@ void bv_pointerst::do_postponed(
821905

822906
// only compare object part
823907
bvt bv;
824-
encode(number, bv);
908+
pointer_typet pt = pointer_type(expr.type());
909+
encode(number, pt, bv);
825910

826911
bv.erase(bv.begin(), bv.begin()+offset_bits);
827912

0 commit comments

Comments
 (0)