Skip to content

Commit 384bd7c

Browse files
author
Daniel Kroening
authored
Merge pull request #716 from mariusmc92/cleanup/type-safe-dynamic-object
Removed the dynamic_object_exprt's instance()
2 parents f2f5e36 + 66481ab commit 384bd7c

10 files changed

+62
-58
lines changed

‎src/pointer-analysis/value_set.cpp

Lines changed: 9 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -799,8 +799,7 @@ void value_sett::get_value_set_rec(
799799
static_cast<const typet &>(expr.find("#type"));
800800

801801
dynamic_object_exprt dynamic_object(dynamic_type);
802-
dynamic_object.instance()=
803-
from_integer(location_number, typet(ID_natural));
802+
dynamic_object.set_instance(location_number);
804803
dynamic_object.valid()=true_exprt();
805804

806805
insert(dest, dynamic_object, 0);
@@ -812,8 +811,7 @@ void value_sett::get_value_set_rec(
812811
assert(expr_type.id()==ID_pointer);
813812

814813
dynamic_object_exprt dynamic_object(expr_type.subtype());
815-
dynamic_object.instance()=
816-
from_integer(location_number, typet(ID_natural));
814+
dynamic_object.set_instance(location_number);
817815
dynamic_object.valid()=true_exprt();
818816

819817
insert(dest, dynamic_object, 0);
@@ -897,7 +895,7 @@ void value_sett::get_value_set_rec(
897895

898896
const std::string prefix=
899897
"value_set::dynamic_object"+
900-
dynamic_object.instance().get_string(ID_value);
898+
std::to_string(dynamic_object.get_instance());
901899

902900
// first try with suffix
903901
const std::string full_name=prefix+suffix;
@@ -1392,7 +1390,7 @@ void value_sett::do_free(
13921390
const object_map_dt &object_map=value_set.read();
13931391

13941392
// find out which *instances* interest us
1395-
expr_sett to_mark;
1393+
dynamic_object_id_sett to_mark;
13961394

13971395
for(object_map_dt::const_iterator
13981396
it=object_map.begin();
@@ -1407,7 +1405,7 @@ void value_sett::do_free(
14071405
to_dynamic_object_expr(object);
14081406

14091407
if(dynamic_object.valid().is_true())
1410-
to_mark.insert(dynamic_object.instance());
1408+
to_mark.insert(dynamic_object.get_instance());
14111409
}
14121410
}
14131411

@@ -1433,10 +1431,10 @@ void value_sett::do_free(
14331431

14341432
if(object.id()==ID_dynamic_object)
14351433
{
1436-
const exprt &instance=
1437-
to_dynamic_object_expr(object).instance();
1434+
const dynamic_object_exprt &dynamic_object=
1435+
to_dynamic_object_expr(object);
14381436

1439-
if(to_mark.count(instance)==0)
1437+
if(to_mark.count(dynamic_object.get_instance())==0)
14401438
set(new_object_map, o_it);
14411439
else
14421440
{
@@ -1507,7 +1505,7 @@ void value_sett::assign_rec(
15071505

15081506
const std::string name=
15091507
"value_set::dynamic_object"+
1510-
dynamic_object.instance().get_string(ID_value);
1508+
std::to_string(dynamic_object.get_instance());
15111509

15121510
entryt &e=get_entry(entryt(name, suffix), lhs.type(), ns);
15131511

‎src/pointer-analysis/value_set.h

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -115,6 +115,8 @@ class value_sett
115115

116116
typedef std::set<exprt> expr_sett;
117117

118+
typedef std::set<unsigned int> dynamic_object_id_sett;
119+
118120
#ifdef USE_DSTRING
119121
typedef std::map<idt, entryt> valuest;
120122
#else

‎src/pointer-analysis/value_set_fi.cpp

Lines changed: 11 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -727,9 +727,8 @@ void value_set_fit::get_value_set_rec(
727727

728728
dynamic_object_exprt dynamic_object(dynamic_type);
729729
// let's make up a `unique' number for this object...
730-
dynamic_object.instance()=
731-
from_integer(
732-
(from_function << 16) | from_target_index, typet(ID_natural));
730+
dynamic_object.set_instance(
731+
(from_function << 16) | from_target_index);
733732
dynamic_object.valid()=true_exprt();
734733

735734
insert(dest, dynamic_object, 0);
@@ -742,9 +741,8 @@ void value_set_fit::get_value_set_rec(
742741
assert(expr.type().id()==ID_pointer);
743742

744743
dynamic_object_exprt dynamic_object(expr.type().subtype());
745-
dynamic_object.instance()=
746-
from_integer(
747-
(from_function << 16) | from_target_index, typet(ID_natural));
744+
dynamic_object.set_instance(
745+
(from_function << 16) | from_target_index);
748746
dynamic_object.valid()=true_exprt();
749747

750748
insert(dest, dynamic_object, 0);
@@ -776,7 +774,7 @@ void value_set_fit::get_value_set_rec(
776774

777775
const std::string name=
778776
"value_set::dynamic_object"+
779-
dynamic_object.instance().get_string(ID_value)+
777+
std::to_string(dynamic_object.get_instance())+
780778
suffix;
781779

782780
// look it up
@@ -1322,7 +1320,7 @@ void value_set_fit::do_free(
13221320
const object_map_dt &object_map=value_set.read();
13231321

13241322
// find out which *instances* interest us
1325-
expr_sett to_mark;
1323+
dynamic_object_id_sett to_mark;
13261324

13271325
forall_objects(it, object_map)
13281326
{
@@ -1334,7 +1332,7 @@ void value_set_fit::do_free(
13341332
to_dynamic_object_expr(object);
13351333

13361334
if(dynamic_object.valid().is_true())
1337-
to_mark.insert(dynamic_object.instance());
1335+
to_mark.insert(dynamic_object.get_instance());
13381336
}
13391337
}
13401338

@@ -1357,10 +1355,10 @@ void value_set_fit::do_free(
13571355

13581356
if(object.id()==ID_dynamic_object)
13591357
{
1360-
const exprt &instance=
1361-
to_dynamic_object_expr(object).instance();
1358+
const dynamic_object_exprt &dynamic_object=
1359+
to_dynamic_object_expr(object);
13621360

1363-
if(to_mark.count(instance)==0)
1361+
if(to_mark.count(dynamic_object.get_instance())==0)
13641362
set(new_object_map, o_it);
13651363
else
13661364
{
@@ -1452,7 +1450,7 @@ void value_set_fit::assign_rec(
14521450

14531451
const std::string name=
14541452
"value_set::dynamic_object"+
1455-
dynamic_object.instance().get_string(ID_value);
1453+
std::to_string(dynamic_object.get_instance());
14561454

14571455
if(make_union(get_entry(name, suffix).object_map, values_rhs))
14581456
changed = true;

‎src/pointer-analysis/value_set_fi.h

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -155,6 +155,8 @@ class value_set_fit
155155

156156
typedef std::unordered_set<exprt, irep_hash> expr_sett;
157157

158+
typedef std::unordered_set<unsigned int> dynamic_object_id_sett;
159+
158160
#ifdef USE_DSTRING
159161
typedef std::map<idt, entryt> valuest;
160162
typedef std::set<idt> flatten_seent;

‎src/pointer-analysis/value_set_fivr.cpp

Lines changed: 11 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -857,9 +857,8 @@ void value_set_fivrt::get_value_set_rec(
857857

858858
dynamic_object_exprt dynamic_object(dynamic_type);
859859
// let's make up a `unique' number for this object...
860-
dynamic_object.instance()=
861-
from_integer(
862-
(from_function << 16) | from_target_index, typet(ID_natural));
860+
dynamic_object.set_instance(
861+
(from_function << 16) | from_target_index);
863862
dynamic_object.valid()=true_exprt();
864863

865864
insert_from(dest, dynamic_object, 0);
@@ -873,9 +872,8 @@ void value_set_fivrt::get_value_set_rec(
873872

874873
dynamic_object_exprt dynamic_object(expr.type().subtype());
875874
// let's make up a unique number for this object...
876-
dynamic_object.instance()=
877-
from_integer(
878-
(from_function << 16) | from_target_index, typet(ID_natural));
875+
dynamic_object.set_instance(
876+
(from_function << 16) | from_target_index);
879877
dynamic_object.valid()=true_exprt();
880878

881879
insert_from(dest, dynamic_object, 0);
@@ -902,7 +900,7 @@ void value_set_fivrt::get_value_set_rec(
902900

903901
const std::string name=
904902
"value_set::dynamic_object"+
905-
dynamic_object.instance().get_string(ID_value)+
903+
std::to_string(dynamic_object.get_instance())+
906904
suffix;
907905

908906
// look it up
@@ -1446,7 +1444,7 @@ void value_set_fivrt::do_free(
14461444
const object_map_dt &object_map=value_set.read();
14471445

14481446
// find out which *instances* interest us
1449-
expr_sett to_mark;
1447+
dynamic_object_id_sett to_mark;
14501448

14511449
forall_objects(it, object_map)
14521450
{
@@ -1458,7 +1456,7 @@ void value_set_fivrt::do_free(
14581456
to_dynamic_object_expr(object);
14591457

14601458
if(dynamic_object.valid().is_true())
1461-
to_mark.insert(dynamic_object.instance());
1459+
to_mark.insert(dynamic_object.get_instance());
14621460
}
14631461
}
14641462

@@ -1481,10 +1479,10 @@ void value_set_fivrt::do_free(
14811479

14821480
if(object.id()==ID_dynamic_object)
14831481
{
1484-
const exprt &instance=
1485-
to_dynamic_object_expr(object).instance();
1482+
const dynamic_object_exprt &dynamic_object=
1483+
to_dynamic_object_expr(object);
14861484

1487-
if(to_mark.count(instance)==0)
1485+
if(to_mark.count(dynamic_object.get_instance())==0)
14881486
set(new_object_map, o_it);
14891487
else
14901488
{
@@ -1590,7 +1588,7 @@ void value_set_fivrt::assign_rec(
15901588

15911589
const std::string name=
15921590
"value_set::dynamic_object"+
1593-
dynamic_object.instance().get_string(ID_value);
1591+
std::to_string(dynamic_object.get_instance());
15941592

15951593
entryt &temp_entry=get_temporary_entry(name, suffix);
15961594

‎src/pointer-analysis/value_set_fivr.h

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -216,6 +216,8 @@ class value_set_fivrt
216216

217217
typedef std::unordered_set<exprt, irep_hash> expr_sett;
218218

219+
typedef std::unordered_set<unsigned int> dynamic_object_id_sett;
220+
219221
#ifdef USE_DSTRING
220222
typedef std::map<idt, entryt> valuest;
221223
typedef std::unordered_set<idt, irep_id_hash> flatten_seent;

‎src/pointer-analysis/value_set_fivrns.cpp

Lines changed: 11 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -631,9 +631,8 @@ void value_set_fivrnst::get_value_set_rec(
631631

632632
dynamic_object_exprt dynamic_object(dynamic_type);
633633
// let's make up a `unique' number for this object...
634-
dynamic_object.instance()=
635-
from_integer(
636-
(from_function << 16) | from_target_index, typet(ID_natural));
634+
dynamic_object.set_instance(
635+
(from_function << 16) | from_target_index);
637636
dynamic_object.valid()=true_exprt();
638637

639638
insert_from(dest, dynamic_object, 0);
@@ -647,9 +646,8 @@ void value_set_fivrnst::get_value_set_rec(
647646

648647
dynamic_object_exprt dynamic_object(expr.type().subtype());
649648
// let's make up a unique number for this object...
650-
dynamic_object.instance()=
651-
from_integer(
652-
(from_function << 16) | from_target_index, typet(ID_natural));
649+
dynamic_object.set_instance(
650+
(from_function << 16) | from_target_index);
653651
dynamic_object.valid()=true_exprt();
654652

655653
insert_from(dest, dynamic_object, 0);
@@ -676,7 +674,7 @@ void value_set_fivrnst::get_value_set_rec(
676674

677675
const std::string name=
678676
"value_set::dynamic_object"+
679-
dynamic_object.instance().get_string(ID_value)+
677+
std::to_string(dynamic_object.get_instance())+
680678
suffix;
681679

682680
// look it up
@@ -1105,7 +1103,7 @@ void value_set_fivrnst::do_free(
11051103
const object_map_dt &object_map=value_set.read();
11061104

11071105
// find out which *instances* interest us
1108-
expr_sett to_mark;
1106+
dynamic_object_id_sett to_mark;
11091107

11101108
forall_objects(it, object_map)
11111109
{
@@ -1117,7 +1115,7 @@ void value_set_fivrnst::do_free(
11171115
to_dynamic_object_expr(object);
11181116

11191117
if(dynamic_object.valid().is_true())
1120-
to_mark.insert(dynamic_object.instance());
1118+
to_mark.insert(dynamic_object.get_instance());
11211119
}
11221120
}
11231121

@@ -1140,10 +1138,10 @@ void value_set_fivrnst::do_free(
11401138

11411139
if(object.id()==ID_dynamic_object)
11421140
{
1143-
const exprt &instance=
1144-
to_dynamic_object_expr(object).instance();
1141+
const dynamic_object_exprt &dynamic_object=
1142+
to_dynamic_object_expr(object);
11451143

1146-
if(to_mark.count(instance)==0)
1144+
if(to_mark.count(dynamic_object.get_instance())==0)
11471145
set(new_object_map, o_it);
11481146
else
11491147
{
@@ -1225,7 +1223,7 @@ void value_set_fivrnst::assign_rec(
12251223

12261224
const std::string name=
12271225
"value_set::dynamic_object"+
1228-
dynamic_object.instance().get_string(ID_value);
1226+
std::to_string(dynamic_object.get_instance());
12291227

12301228
entryt &temp_entry = get_temporary_entry(name, suffix);
12311229

‎src/pointer-analysis/value_set_fivrns.h

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -216,6 +216,8 @@ class value_set_fivrnst
216216

217217
typedef std::unordered_set<exprt, irep_hash> expr_sett;
218218

219+
typedef std::unordered_set<unsigned int> dynamic_object_id_sett;
220+
219221
#ifdef USE_DSTRING
220222
typedef std::map<idt, entryt> valuest;
221223
#else

‎src/util/std_expr.cpp

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -61,6 +61,16 @@ exprt disjunction(const exprt::operandst &op)
6161
}
6262
}
6363

64+
void dynamic_object_exprt::set_instance(unsigned int instance)
65+
{
66+
op0()=from_integer(instance, typet(ID_natural));
67+
}
68+
69+
unsigned int dynamic_object_exprt::get_instance() const
70+
{
71+
return std::stoul(id2string(to_constant_expr(op0()).get_value()));
72+
}
73+
6474
/*******************************************************************\
6575
6676
Function: conjunction

‎src/util/std_expr.h

Lines changed: 2 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1505,15 +1505,9 @@ class dynamic_object_exprt:public exprt
15051505
op1().id(ID_unknown);
15061506
}
15071507

1508-
exprt &instance()
1509-
{
1510-
return op0();
1511-
}
1508+
void set_instance(unsigned int instance);
15121509

1513-
const exprt &instance() const
1514-
{
1515-
return op0();
1516-
}
1510+
unsigned int get_instance() const;
15171511

15181512
exprt &valid()
15191513
{

0 commit comments

Comments
 (0)