Skip to content

Commit cc8495a

Browse files
author
Owen Jones
committed
Replace objectt in value_set_fivr.*
typedef optional<mp_integer> to offsett and use that instead of objectt. This reduces code and gets rid of an unintuitive class name.
1 parent 5ecee62 commit cc8495a

File tree

2 files changed

+78
-99
lines changed

2 files changed

+78
-99
lines changed

‎src/pointer-analysis/value_set_fivr.cpp

+53-59
Original file line numberDiff line numberDiff line change
@@ -143,8 +143,8 @@ void value_set_fivrt::output(
143143
{
144144
result+=from_expr(ns, identifier, o)+", ";
145145

146-
if(o_it->second.offset_is_set)
147-
result+=integer2string(o_it->second.offset)+"";
146+
if(o_it->second)
147+
result += integer2string(*o_it->second) + "";
148148
else
149149
result+='*';
150150

@@ -301,13 +301,12 @@ void value_set_fivrt::flatten_rec(
301301
t_it!=temp.write().end();
302302
t_it++)
303303
{
304-
if(t_it->second.offset_is_set &&
305-
it->second.offset_is_set)
304+
if(t_it->second && it->second)
306305
{
307-
t_it->second.offset += it->second.offset;
306+
*t_it->second += *it->second;
308307
}
309308
else
310-
t_it->second.offset_is_set=false;
309+
t_it->second.reset();
311310
}
312311

313312
forall_objects(oit, temp.read())
@@ -325,7 +324,7 @@ void value_set_fivrt::flatten_rec(
325324
{
326325
Forall_objects(it, dest.write())
327326
{
328-
it->second.offset_is_set=false;
327+
it->second.reset();
329328
for(std::list<const object_map_dt::vrange_listt*>::const_iterator vit =
330329
add_ranges.begin();
331330
vit!=add_ranges.end();
@@ -355,8 +354,8 @@ exprt value_set_fivrt::to_expr(object_map_dt::const_iterator it) const
355354

356355
od.object()=object;
357356

358-
if(it->second.offset_is_set)
359-
od.offset()=from_integer(it->second.offset, index_type());
357+
if(it->second)
358+
od.offset() = from_integer(*it->second, index_type());
360359

361360
od.type()=od.object().type();
362361

@@ -436,13 +435,12 @@ void value_set_fivrt::get_value_set(
436435
t_it!=temp.write().end();
437436
t_it++)
438437
{
439-
if(t_it->second.offset_is_set &&
440-
it->second.offset_is_set)
438+
if(t_it->second && it->second)
441439
{
442-
t_it->second.offset += it->second.offset;
440+
*t_it->second += *it->second;
443441
}
444442
else
445-
t_it->second.offset_is_set=false;
443+
t_it->second.reset();
446444

447445
flat_map.write()[t_it->first]=t_it->second;
448446
}
@@ -690,32 +688,31 @@ void value_set_fivrt::get_value_set_rec(
690688

691689
forall_objects(it, pointer_expr_set.read())
692690
{
693-
objectt object=it->second;
691+
offsett offset = it->second;
694692

695-
if(object.offset_is_zero() &&
696-
expr.operands().size()==2)
693+
if(offset_is_zero(offset) && expr.operands().size() == 2)
697694
{
698695
if(expr.op0().type().id()!=ID_pointer)
699696
{
700697
mp_integer i;
701698
if(to_integer(expr.op0(), i))
702-
object.offset_is_set=false;
699+
offset.reset();
703700
else
704-
object.offset=(expr.id()==ID_plus)? i : -i;
701+
*offset = (expr.id() == ID_plus) ? i : -i;
705702
}
706703
else
707704
{
708705
mp_integer i;
709706
if(to_integer(expr.op1(), i))
710-
object.offset_is_set=false;
707+
offset.reset();
711708
else
712-
object.offset=(expr.id()==ID_plus)? i : -i;
709+
*offset = (expr.id() == ID_plus) ? i : -i;
713710
}
714711
}
715712
else
716-
object.offset_is_set=false;
713+
offset.reset();
717714

718-
insert_from(dest, it->first, object);
715+
insert_from(dest, it->first, offset);
719716
}
720717

721718
return;
@@ -850,13 +847,12 @@ void value_set_fivrt::get_reference_set(
850847
t_it!=omt.write().end();
851848
t_it++)
852849
{
853-
if(t_it->second.offset_is_set &&
854-
it->second.offset_is_set)
850+
if(t_it->second && it->second)
855851
{
856-
t_it->second.offset += it->second.offset;
852+
*t_it->second += *it->second;
857853
}
858854
else
859-
t_it->second.offset_is_set=false;
855+
t_it->second.reset();
860856
}
861857

862858
forall_objects(it, omt.read())
@@ -939,13 +935,12 @@ void value_set_fivrt::get_reference_set_sharing_rec(
939935
t_it!=t2.write().end();
940936
t_it++)
941937
{
942-
if(t_it->second.offset_is_set &&
943-
it->second.offset_is_set)
938+
if(t_it->second && it->second)
944939
{
945-
t_it->second.offset += it->second.offset;
940+
*t_it->second += *it->second;
946941
}
947942
else
948-
t_it->second.offset_is_set=false;
943+
t_it->second.reset();
949944
}
950945

951946
forall_objects(it2, t2.read())
@@ -1002,17 +997,16 @@ void value_set_fivrt::get_reference_set_sharing_rec(
1002997
ns.follow(object.type())!=array_type)
1003998
index_expr.make_typecast(array.type());
1004999

1005-
objectt o=a_it->second;
1000+
offsett o = a_it->second;
10061001
mp_integer i;
10071002

10081003
if(offset.is_zero())
10091004
{
10101005
}
1011-
else if(!to_integer(offset, i) &&
1012-
o.offset_is_zero())
1013-
o.offset=i;
1006+
else if(!to_integer(offset, i) && offset_is_zero(o))
1007+
*o = i;
10141008
else
1015-
o.offset_is_set=false;
1009+
o.reset();
10161010

10171011
insert_from(dest, index_expr, o);
10181012
}
@@ -1051,7 +1045,7 @@ void value_set_fivrt::get_reference_set_sharing_rec(
10511045
}
10521046
else
10531047
{
1054-
objectt o=it->second;
1048+
offsett o = it->second;
10551049

10561050
exprt member_expr(ID_member, expr.type());
10571051
member_expr.copy_to_operands(object);
@@ -1300,7 +1294,7 @@ void value_set_fivrt::do_free(
13001294
else
13011295
{
13021296
// adjust
1303-
objectt o=o_it->second;
1297+
offsett o = o_it->second;
13041298
exprt tmp(object);
13051299
to_dynamic_object_expr(tmp).valid()=exprt(ID_unknown);
13061300
insert_to(new_object_map, tmp, o);
@@ -1675,39 +1669,39 @@ void value_set_fivrt::apply_code(
16751669
bool value_set_fivrt::insert_to(
16761670
object_mapt &dest,
16771671
object_numberingt::number_type n,
1678-
const objectt &object) const
1672+
const offsett &offset) const
16791673
{
16801674
object_map_dt &map=dest.write();
16811675
if(map.find(n)==map.end())
16821676
{
1683-
// std::cout << "NEW(" << n << "): " << object_numbering[n] << '\n';
1677+
// std::cout << "NEW(" << n << "): " << object_numbering[n] << '\n';
16841678
// new
1685-
map[n]=object;
1679+
map[n] = offset;
16861680
map.set_valid_at(n, to_function, to_target_index);
16871681
return true;
16881682
}
16891683
else
16901684
{
1691-
// std::cout << "UPD " << n << '\n';
1692-
objectt &old=map[n];
1685+
// std::cout << "UPD " << n << '\n';
1686+
offsett &old_offset = map[n];
16931687

1694-
bool res=map.set_valid_at(n, to_function, to_target_index);
1688+
bool res = map.set_valid_at(n, to_function, to_target_index);
16951689

1696-
if(old.offset_is_set && object.offset_is_set)
1690+
if(old_offset && offset)
16971691
{
1698-
if(old.offset==object.offset)
1692+
if(*old_offset == *offset)
16991693
return res;
17001694
else
17011695
{
1702-
old.offset_is_set=false;
1696+
old_offset.reset();
17031697
return true;
17041698
}
17051699
}
1706-
else if(!old.offset_is_set)
1700+
else if(!old_offset)
17071701
return res;
17081702
else
17091703
{
1710-
old.offset_is_set=false;
1704+
old_offset.reset();
17111705
return true;
17121706
}
17131707
}
@@ -1716,39 +1710,39 @@ bool value_set_fivrt::insert_to(
17161710
bool value_set_fivrt::insert_from(
17171711
object_mapt &dest,
17181712
object_numberingt::number_type n,
1719-
const objectt &object) const
1713+
const offsett &offset) const
17201714
{
17211715
object_map_dt &map=dest.write();
17221716
if(map.find(n)==map.end())
17231717
{
1724-
// std::cout << "NEW(" << n << "): " << object_numbering[n] << '\n';
1718+
// std::cout << "NEW(" << n << "): " << object_numbering[n] << '\n';
17251719
// new
1726-
map[n]=object;
1720+
map[n] = offset;
17271721
map.set_valid_at(n, from_function, from_target_index);
17281722
return true;
17291723
}
17301724
else
17311725
{
1732-
// std::cout << "UPD " << n << '\n';
1733-
objectt &old=map[n];
1726+
// std::cout << "UPD " << n << '\n';
1727+
offsett &old_offset = map[n];
17341728

1735-
bool res=map.set_valid_at(n, from_function, from_target_index);
1729+
bool res = map.set_valid_at(n, from_function, from_target_index);
17361730

1737-
if(old.offset_is_set && object.offset_is_set)
1731+
if(old_offset && offset)
17381732
{
1739-
if(old.offset==object.offset)
1733+
if(*old_offset == *offset)
17401734
return res;
17411735
else
17421736
{
1743-
old.offset_is_set=false;
1737+
old_offset.reset();
17441738
return true;
17451739
}
17461740
}
1747-
else if(!old.offset_is_set)
1741+
else if(!old_offset)
17481742
return res;
17491743
else
17501744
{
1751-
old.offset_is_set=false;
1745+
old_offset.reset();
17521746
return true;
17531747
}
17541748
}

0 commit comments

Comments
 (0)