Skip to content

Commit 5f4eb14

Browse files
author
Owen Jones
committed
Refactoring: Use type contained in entryt
An entryt contains the entire expr that it represents in the field `structured_lhs`, so there is no need to pass the type to entryt::get_key() or value_sett::get_entry()
1 parent 460ef35 commit 5f4eb14

File tree

4 files changed

+15
-26
lines changed

4 files changed

+15
-26
lines changed

cbmc/src/pointer-analysis/value_set.cpp

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -53,11 +53,10 @@ bool value_sett::field_sensitive(
5353

5454
value_sett::entryt &value_sett::get_entry(
5555
const entryt &e,
56-
const typet &type,
5756
const namespacet &ns)
5857
{
5958
std::pair<valuest::iterator, bool> r =
60-
values.insert(std::pair<idt, entryt>(e.get_key(type, ns), e));
59+
values.insert(std::pair<idt, entryt>(e.get_key(ns), e));
6160

6261
return r.first->second;
6362
}
@@ -1403,7 +1402,7 @@ void value_sett::assign_rec(
14031402
if(lhs.id()==ID_symbol)
14041403
{
14051404
const irep_idt &identifier=to_symbol_expr(lhs).get_identifier();
1406-
entryt &e = get_entry(entryt(identifier, suffix, lhs), lhs.type(), ns);
1405+
entryt &e = get_entry(entryt(identifier, suffix, lhs), ns);
14071406

14081407
if(add_to_sets)
14091408
make_union(e.object_map, values_rhs);
@@ -1416,7 +1415,7 @@ void value_sett::assign_rec(
14161415
to_dynamic_object_expr(lhs);
14171416
std::string name=get_dynamic_object_name(dynamic_object);
14181417

1419-
entryt &e = get_entry(entryt(name, suffix, lhs), lhs.type(), ns);
1418+
entryt &e = get_entry(entryt(name, suffix, lhs), ns);
14201419

14211420
make_union(e.object_map, values_rhs);
14221421
}

cbmc/src/pointer-analysis/value_set.h

Lines changed: 3 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -299,9 +299,9 @@ class value_sett
299299
return !(*this==other);
300300
}
301301

302-
const irep_idt get_key(const typet &type, const namespacet &ns) const
302+
const irep_idt get_key(const namespacet &ns) const
303303
{
304-
if(field_sensitive(identifier, type, ns))
304+
if(field_sensitive(identifier, structured_lhs.type(), ns))
305305
return id2string(identifier) + suffix;
306306

307307
return identifier;
@@ -373,13 +373,8 @@ class value_sett
373373
/// `object_map` (RHS value set) will be copied; otherwise it will be
374374
/// ignored. Therefore it should probably be left blank and any RHS updates
375375
/// conducted against the returned reference.
376-
/// \param type: type of `e.identifier`, used to determine whether `e`'s
377-
/// suffix should be used to find a field-sensitive value-set or whether
378-
/// a single entry should be shared by all of symbol `e.identifier`.
379376
/// \param ns: global namespace
380-
entryt &get_entry(
381-
const entryt &e, const typet &type,
382-
const namespacet &ns);
377+
entryt &get_entry(const entryt &e, const namespacet &ns);
383378

384379
/// Pretty-print this value-set
385380
/// \param ns: global namespace

src/pointer-analysis/local_value_set.cpp

Lines changed: 7 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -535,13 +535,12 @@ void local_value_sett::demote_most_recent_dynamic_objects(
535535
to_dynamic_object_expr(entry.structured_lhs);
536536
expr_any_allocation.set_recency(false);
537537

538-
// The second and third arguments to get_entry() are only used for
539-
// field_sensitive(), and that will always returns true without using
540-
// them because name_any_allocation starts with the prefix for a
541-
// dynamic object, so we can use an empty type and namespace.
538+
// The second argument to get_entry() is only used for field_sensitive(),
539+
// and that will always returns true without using it because
540+
// name_any_allocation starts with the prefix for a dynamic object, so
541+
// we can use an empty namespace.
542542
entryt &entry_any_allocation = get_entry(
543543
entryt(name_any_allocation, entry.suffix, expr_any_allocation),
544-
nil_typet(),
545544
namespacet(symbol_tablet()));
546545

547546
// Add into the any-allocation dynamic-object's object_map
@@ -618,8 +617,8 @@ void local_value_sett::assign_rec(
618617
ns,
619618
declared_on_type,
620619
suffix_without_supertypes_ignored);
621-
entryt &e = get_entry(
622-
entryt(identifier, suffix, declared_on_type, lhs), lhs.type(), ns);
620+
entryt &e =
621+
get_entry(entryt(identifier, suffix, declared_on_type, lhs), ns);
623622

624623
if(add_to_sets)
625624
make_union(e.object_map, values_rhs);
@@ -641,8 +640,7 @@ void local_value_sett::assign_rec(
641640
declared_on_type,
642641
suffix_without_supertypes_ignored);
643642

644-
entryt &entry =
645-
get_entry(entryt(name, suffix, declared_on_type, lhs), lhs.type(), ns);
643+
entryt &entry = get_entry(entryt(name, suffix, declared_on_type, lhs), ns);
646644

647645
if(
648646
dynamic_object.get_recency() ==

src/pointer-analysis/local_value_set_analysis.cpp

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -94,8 +94,7 @@ static void add_default_evses(
9494
false);
9595
local_value_sett::entryt extsym_entry_blank(
9696
id2string(extsym_name), "", typet(), extsym_var);
97-
auto &extsym_entry =
98-
value_set.get_entry(extsym_entry_blank, extsym.type().subtype(), ns);
97+
auto &extsym_entry = value_set.get_entry(extsym_entry_blank, ns);
9998
value_set.insert(extsym_entry.object_map, extsym_var);
10099
}
101100
}
@@ -575,9 +574,7 @@ void local_value_set_analysist::transform_function_stub(
575574
lhs_fieldname.field_name,
576575
lhs_fieldname.declared_on_type,
577576
lhs_fieldname.structured_lhs);
578-
const auto &global_sym = ns.lookup(lhs_fieldname.base_name);
579-
auto &global_entry =
580-
valuesets.get_entry(global_entry_name, global_sym.type, ns);
577+
auto &global_entry = valuesets.get_entry(global_entry_name, ns);
581578
valuesets.make_union(global_entry.object_map, rhs_values);
582579
}
583580
}

0 commit comments

Comments
 (0)