Skip to content

Commit 1b45cc3

Browse files
tautschnigtautschnig
committed
Implement the new pointer encoding for SMT1/2 back ends
1 parent fca8c4b commit 1b45cc3

File tree

2 files changed

+96
-99
lines changed

2 files changed

+96
-99
lines changed

‎src/solvers/smt1/smt1_conv.cpp

Lines changed: 51 additions & 45 deletions
Original file line numberDiff line numberDiff line change
@@ -142,20 +142,22 @@ exprt smt1_convt::ce_value(
142142
else if(type.id()==ID_pointer)
143143
{
144144
assert(value.size()==boolbv_width(type));
145+
std::size_t object_bits=pointer_logic.get_object_width();
146+
std::size_t offset_bits=pointer_logic.get_offset_width();
145147

146148
constant_exprt result(type);
147-
result.set_value(value);
149+
result.set_value(value.substr(0, object_bits+offset_bits));
148150

149151
// add the elaborated expression as operand
150152

151153
pointer_logict::pointert p;
152-
p.object=integer2unsigned(
153-
binary2integer(
154-
value.substr(0, config.bv_encoding.object_bits), false));
154+
p.object=
155+
integer2size_t(
156+
binary2integer(value.substr(0, object_bits), false));
155157

156158
p.offset=
157159
binary2integer(
158-
value.substr(config.bv_encoding.object_bits, std::string::npos), true);
160+
value.substr(object_bits, offset_bits), true);
159161

160162
result.copy_to_operands(
161163
pointer_logic.pointer_expr(p, to_pointer_type(type)));
@@ -255,13 +257,18 @@ void smt1_convt::convert_address_of_rec(
255257
expr.id()==ID_string_constant ||
256258
expr.id()==ID_label)
257259
{
260+
std::string addr=
261+
expr.id()==ID_symbol?
262+
expr.get_string(ID_identifier)+"$address":
263+
"bv0["+std::to_string(pointer_logic.get_address_width())+"]";
264+
258265
out
266+
<< "(concat "
259267
<< "(concat"
260-
<< " bv" << pointer_logic.add_object(expr) << "["
261-
<< config.bv_encoding.object_bits << "]"
262-
<< " bv0["
263-
<< boolbv_width(result_type)-config.bv_encoding.object_bits << "]"
264-
<< ")";
268+
<< " bv" << pointer_logic.add_object(expr)
269+
<< "[" << pointer_logic.get_object_width() << "]"
270+
<< " bv0[" << pointer_logic.get_offset_width() << "]"
271+
<< ") " << addr << ")";
265272
}
266273
else if(expr.id()==ID_index)
267274
{
@@ -886,33 +893,26 @@ void smt1_convt::convert_expr(const exprt &expr, bool bool_as_bv)
886893
{
887894
assert(expr.operands().size()==1);
888895
assert(expr.op0().type().id()==ID_pointer);
889-
std::size_t op_width=boolbv_width(expr.op0().type());
890-
out << "(zero_extend[" << config.bv_encoding.object_bits << "] (extract["
891-
<< (op_width-1-config.bv_encoding.object_bits)
892-
<< ":0] ";
896+
std::size_t object_bits=pointer_logic.get_object_width();
897+
std::size_t offset_bits=pointer_logic.get_offset_width();
898+
out << "(extract["
899+
<< object_bits+offset_bits-1 << ":"
900+
<< object_bits << "] ";
893901
convert_expr(expr.op0(), true);
894-
out << "))";
895-
assert(boolbv_width(expr.type())==op_width);
902+
out << ")";
903+
DATA_INVARIANT(
904+
boolbv_width(expr.type()) == offset_bits, "offset encoding mismatch");
896905
}
897906
else if(expr.id()==ID_pointer_object)
898907
{
899908
assert(expr.operands().size()==1);
900909
assert(expr.op0().type().id()==ID_pointer);
901-
std::size_t op_width=boolbv_width(expr.op0().type());
902-
signed int ext=boolbv_width(expr.type())-config.bv_encoding.object_bits;
903-
904-
if(ext>0)
905-
out << "(zero_extend[" << ext << "] ";
906-
907-
out << "(extract["
908-
<< (op_width-1)
909-
<< ":"
910-
<< op_width-1-config.bv_encoding.object_bits << "] ";
910+
std::size_t object_bits=pointer_logic.get_object_width();
911+
out << "(extract[" << object_bits-1 << ":0] ";
911912
convert_expr(expr.op0(), true);
912913
out << ")";
913-
914-
if(ext>0)
915-
out << ")";
914+
DATA_INVARIANT(
915+
boolbv_width(expr.type()) == object_bits, "object encoding mismatch");
916916
}
917917
else if(expr.id()=="is_dynamic_object")
918918
{
@@ -924,17 +924,15 @@ void smt1_convt::convert_expr(const exprt &expr, bool bool_as_bv)
924924

925925
assert(expr.operands().size()==1);
926926
assert(expr.op0().type().id()==ID_pointer);
927-
std::size_t op_width=boolbv_width(expr.op0().type());
927+
std::size_t object_bits=pointer_logic.get_object_width();
928928

929929
// this may have to be converted
930930
from_bool_begin(type, bool_as_bv);
931931

932-
out << "(= (extract["
933-
<< (op_width-1)
934-
<< ":" << op_width-config.bv_encoding.object_bits << "] ";
932+
out << "(= (extract[" << object_bits-1 << ":0] ";
935933
convert_expr(expr.op0(), true);
936934
out << ") bv" << pointer_logic.get_invalid_object()
937-
<< "[" << config.bv_encoding.object_bits << "])";
935+
<< "[" << object_bits << "])";
938936

939937
// this may have to be converted
940938
from_bool_end(type, bool_as_bv);
@@ -1849,12 +1847,14 @@ void smt1_convt::convert_constant(
18491847
if(value==ID_NULL)
18501848
{
18511849
assert(boolbv_width(expr.type())!=0);
1852-
out << "(concat"
1850+
out << "(concat "
1851+
<< "(concat"
18531852
<< " bv" << pointer_logic.get_null_object()
1854-
<< "[" << config.bv_encoding.object_bits << "]"
1855-
<< " bv0[" << boolbv_width(expr.type())-config.bv_encoding.object_bits
1856-
<< "]"
1857-
<< ")"; // concat
1853+
<< "[" << pointer_logic.get_object_width() << "]"
1854+
<< " bv0[" << pointer_logic.get_offset_width() << "]"
1855+
<< ") "
1856+
<< "bv0[" << pointer_logic.get_address_width() << "]"
1857+
<< ")";
18581858
}
18591859
else
18601860
throw "unknown pointer constant: "+id2string(value);
@@ -1930,7 +1930,7 @@ void smt1_convt::convert_is_dynamic_object(
19301930

19311931
assert(expr.operands().size()==1);
19321932
assert(expr.op0().type().id()==ID_pointer);
1933-
std::size_t op_width=boolbv_width(expr.op0().type());
1933+
std::size_t object_bits=pointer_logic.get_object_width();
19341934

19351935
// this may have to be converted
19361936
from_bool_begin(expr.type(), bool_as_bv);
@@ -1941,24 +1941,22 @@ void smt1_convt::convert_is_dynamic_object(
19411941
{
19421942
// let is only allowed in formulas
19431943

1944-
out << "(let (?obj (extract["
1945-
<< (op_width-1)
1946-
<< ":" << op_width-config.bv_encoding.object_bits << "] ";
1944+
out << "(let (?obj (extract[" << object_bits-1 << ":0] ";
19471945
convert_expr(expr.op0(), true);
19481946
out << ")) ";
19491947

19501948
if(dynamic_objects.size()==1)
19511949
{
19521950
out << "(= bv" << dynamic_objects.front()
1953-
<< "[" << config.bv_encoding.object_bits << "] ?obj)";
1951+
<< "[" << object_bits << "] ?obj)";
19541952
}
19551953
else
19561954
{
19571955
out << "(or";
19581956

19591957
for(const auto &obj : dynamic_objects)
19601958
out << " (= bv" << obj
1961-
<< "[" << config.bv_encoding.object_bits << "] ?obj)";
1959+
<< "[" << object_bits << "] ?obj)";
19621960

19631961
out << ")"; // or
19641962
}
@@ -2839,6 +2837,14 @@ void smt1_convt::find_symbols(const exprt &expr)
28392837
convert_type(type);
28402838
out << "))" << "\n";
28412839
}
2840+
2841+
std::string address_id=id2string(identifier)+"$address";
2842+
2843+
out << ":extrafuns(("
2844+
<< convert_identifier(address_id)
2845+
<< " ";
2846+
convert_type(size_type());
2847+
out << "))\n";
28422848
}
28432849
}
28442850
else if(expr.id()==ID_array_of)

‎src/solvers/smt2/smt2_conv.cpp

Lines changed: 45 additions & 54 deletions
Original file line numberDiff line numberDiff line change
@@ -136,34 +136,28 @@ void smt2_convt::define_object_size(
136136
const exprt &expr)
137137
{
138138
assert(expr.id()==ID_object_size);
139-
const exprt &ptr = expr.op0();
140-
std::size_t size_width = boolbv_width(expr.type());
141-
std::size_t pointer_width = boolbv_width(ptr.type());
142-
std::size_t number = 0;
143-
std::size_t h=pointer_width-1;
144-
std::size_t l=pointer_width-config.bv_encoding.object_bits;
139+
const exprt &ptr=expr.op0();
140+
std::size_t size_width=boolbv_width(expr.type());
141+
std::size_t number=0;
142+
std::size_t object_bits=pointer_logic.get_object_width();
145143

146144
for(const auto &o : pointer_logic.objects)
147145
{
148-
const typet &type = ns.follow(o.type());
149-
exprt size_expr = size_of_expr(type, ns);
150-
mp_integer object_size;
146+
const typet &type=ns.follow(o.type());
147+
mp_integer object_size=pointer_offset_size(type, ns);
151148

152-
if(o.id()!=ID_symbol ||
153-
size_expr.is_nil() ||
154-
to_integer(size_expr, object_size))
149+
if(o.id()!=ID_symbol || object_size<=0)
155150
{
156151
++number;
157152
continue;
158153
}
159154

160155
out << "(assert (implies (= " <<
161-
"((_ extract " << h << " " << l << ") ";
156+
"((_ extract " << object_bits-1 << " 0) ";
162157
convert_expr(ptr);
163-
out << ") (_ bv" << number << " "
164-
<< config.bv_encoding.object_bits << "))"
165-
<< "(= " << id << " (_ bv" << object_size.to_ulong() << " "
166-
<< size_width << "))))\n";
158+
out << ") (_ bv" << number << " " << object_bits << "))" <<
159+
"(= " << id << " (_ bv" << object_size.to_ulong() << " " <<
160+
size_width << "))))\n";
167161

168162
++number;
169163
}
@@ -474,10 +468,12 @@ exprt smt2_convt::parse_rec(const irept &src, const typet &_type)
474468
to_integer(bv_expr, v);
475469

476470
// split into object and offset
477-
mp_integer pow=power(2, width-config.bv_encoding.object_bits);
471+
std::size_t object_bits=pointer_logic.get_object_width();
472+
std::size_t offset_bits=pointer_logic.get_offset_width();
473+
mp_integer pow=power(2, object_bits);
478474
pointer_logict::pointert ptr;
479-
ptr.object=integer2size_t(v/pow);
480-
ptr.offset=v%pow;
475+
ptr.object=integer2size_t(v%pow);
476+
ptr.offset=(v%power(2, object_bits+offset_bits))/pow;
481477
return pointer_logic.pointer_expr(ptr, to_pointer_type(type));
482478
}
483479
else if(type.id()==ID_struct)
@@ -505,12 +501,18 @@ void smt2_convt::convert_address_of_rec(
505501
expr.id()==ID_string_constant ||
506502
expr.id()==ID_label)
507503
{
504+
std::string addr=
505+
expr.id()==ID_symbol?
506+
expr.get_string(ID_identifier)+"$address":
507+
"(_ bv0 "+std::to_string(pointer_logic.get_address_width())+")";
508+
508509
out
509-
<< "(concat (_ bv"
510-
<< pointer_logic.add_object(expr) << " "
511-
<< config.bv_encoding.object_bits << ")"
512-
<< " (_ bv0 "
513-
<< boolbv_width(result_type)-config.bv_encoding.object_bits << "))";
510+
<< "(concat "
511+
<< "(concat "
512+
<< "(_ bv" << pointer_logic.add_object(expr)
513+
<< " " << pointer_logic.get_object_width() << ") "
514+
<< "(_ bv0 " << pointer_logic.get_offset_width() << ")) "
515+
<< addr << ")";
514516
}
515517
else if(expr.id()==ID_index)
516518
{
@@ -1329,38 +1331,32 @@ void smt2_convt::convert_expr(const exprt &expr)
13291331
{
13301332
assert(expr.operands().size()==1);
13311333
assert(expr.op0().type().id()==ID_pointer);
1332-
std::size_t offset_bits=
1333-
boolbv_width(expr.op0().type())-config.bv_encoding.object_bits;
1334-
std::size_t result_width=boolbv_width(expr.type());
1334+
std::size_t object_bits=pointer_logic.get_object_width();
1335+
std::size_t offset_bits=pointer_logic.get_offset_width();
1336+
std::size_t ext=boolbv_width(expr.type())-offset_bits;
13351337

1336-
// max extract width
1337-
if(offset_bits>result_width)
1338-
offset_bits=result_width;
1339-
1340-
// too few bits?
1341-
if(result_width>offset_bits)
1342-
out << "((_ zero_extend " << result_width-offset_bits << ") ";
1338+
if(ext>0)
1339+
out << "((_ zero_extend " << ext << ") ";
13431340

1344-
out << "((_ extract " << offset_bits-1 << " 0) ";
1341+
out << "((_ extract " << object_bits+offset_bits-1
1342+
<< " " << object_bits << ") ";
13451343
convert_expr(expr.op0());
13461344
out << ")";
13471345

1348-
if(result_width>offset_bits)
1346+
if(ext>0)
13491347
out << ")"; // zero_extend
13501348
}
13511349
else if(expr.id()==ID_pointer_object)
13521350
{
13531351
assert(expr.operands().size()==1);
13541352
assert(expr.op0().type().id()==ID_pointer);
1355-
std::size_t ext=boolbv_width(expr.type())-config.bv_encoding.object_bits;
1356-
std::size_t pointer_width=boolbv_width(expr.op0().type());
1353+
std::size_t object_bits=pointer_logic.get_object_width();
1354+
std::size_t ext=boolbv_width(expr.type())-object_bits;
13571355

13581356
if(ext>0)
13591357
out << "((_ zero_extend " << ext << ") ";
13601358

1361-
out << "((_ extract "
1362-
<< pointer_width-1 << " "
1363-
<< pointer_width-config.bv_encoding.object_bits << ") ";
1359+
out << "((_ extract " << object_bits-1 << " 0) ";
13641360
convert_expr(expr.op0());
13651361
out << ")";
13661362

@@ -1374,14 +1370,12 @@ void smt2_convt::convert_expr(const exprt &expr)
13741370
else if(expr.id()==ID_invalid_pointer)
13751371
{
13761372
assert(expr.operands().size()==1);
1373+
std::size_t object_bits=pointer_logic.get_object_width();
13771374

1378-
std::size_t pointer_width=boolbv_width(expr.op0().type());
1379-
out << "(= ((_ extract "
1380-
<< pointer_width-1 << " "
1381-
<< pointer_width-config.bv_encoding.object_bits << ") ";
1375+
out << "(= ((_ extract " << object_bits-1 << " 0) ";
13821376
convert_expr(expr.op0());
13831377
out << ") (_ bv" << pointer_logic.get_invalid_object()
1384-
<< " " << config.bv_encoding.object_bits << "))";
1378+
<< " " << object_bits << "))";
13851379
}
13861380
else if(expr.id()=="pointer_object_has_type")
13871381
{
@@ -2751,31 +2745,28 @@ void smt2_convt::convert_is_dynamic_object(const exprt &expr)
27512745
pointer_logic.get_dynamic_objects(dynamic_objects);
27522746

27532747
assert(expr.operands().size()==1);
2748+
std::size_t object_bits=pointer_logic.get_object_width();
27542749

27552750
if(dynamic_objects.empty())
27562751
out << "false";
27572752
else
27582753
{
2759-
std::size_t pointer_width=boolbv_width(expr.op0().type());
2760-
2761-
out << "(let ((?obj ((_ extract "
2762-
<< pointer_width-1 << " "
2763-
<< pointer_width-config.bv_encoding.object_bits << ") ";
2754+
out << "(let ((?obj ((_ extract " << object_bits << " 0) ";
27642755
convert_expr(expr.op0());
27652756
out << "))) ";
27662757

27672758
if(dynamic_objects.size()==1)
27682759
{
27692760
out << "(= (_ bv" << dynamic_objects.front()
2770-
<< " " << config.bv_encoding.object_bits << ") ?obj)";
2761+
<< " " << object_bits << ") ?obj)";
27712762
}
27722763
else
27732764
{
27742765
out << "(or";
27752766

27762767
for(const auto &object : dynamic_objects)
27772768
out << " (= (_ bv" << object
2778-
<< " " << config.bv_encoding.object_bits << ") ?obj)";
2769+
<< " " << object_bits << ") ?obj)";
27792770

27802771
out << ")"; // or
27812772
}

0 commit comments

Comments
 (0)