Skip to content

Commit 875be9d

Browse files
committed
Address review comments
0: explained why floating point test is failing 1: use safe string2int conversion 2: memory_map is indexed by irep_idts 3: data in memory_scope are private and have getters 4: accessing types within this PR (and analyze_symbol.cpp) is a bit more readable 5: Checking address containment within memory scope and pointer offset distance shared the address-to-string conversion which was computed twice. It now has a separate private method so that the conversion is called only once when computing distance.
1 parent 28d16ed commit 875be9d

File tree

3 files changed

+71
-29
lines changed

3 files changed

+71
-29
lines changed

regression/snapshot-harness/static-array-float/test.desc

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,3 +11,5 @@ array,iterator1,iterator2 --harness-type initialise-with-memory-snapshot --initi
1111
VERIFICATION FAILED
1212
--
1313
unwinding assertion loop \d+: FAILURE
14+
--
15+
memory analyzer does not yet allow extract floating point values

src/memory-analyzer/analyze_symbol.cpp

Lines changed: 27 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -31,21 +31,28 @@ gdb_value_extractort::gdb_value_extractort(
3131
{
3232
}
3333

34-
bool gdb_value_extractort::memory_scopet::contains(
34+
gdb_value_extractort::memory_scopet::memory_scopet(
35+
const memory_addresst &begin,
36+
const mp_integer &byte_size,
37+
const irep_idt &name)
38+
: begin_int(safe_string2size_t(begin.address_string, 0)),
39+
byte_size(byte_size),
40+
name(name)
41+
{
42+
}
43+
44+
size_t gdb_value_extractort::memory_scopet::address2size_t(
3545
const memory_addresst &point) const
3646
{
37-
size_t begin_int = std::strtoul(begin.address_string.c_str(), NULL, 0);
38-
size_t point_int = std::strtoul(point.address_string.c_str(), NULL, 0);
39-
return point_int >= begin_int && (begin_int + byte_size) > point_int;
47+
return safe_string2size_t(point.address_string, 0);
4048
}
4149

4250
mp_integer gdb_value_extractort::memory_scopet::distance(
4351
const memory_addresst &point,
4452
mp_integer member_size) const
4553
{
46-
CHECK_RETURN(contains(point));
47-
size_t begin_int = std::strtoul(begin.address_string.c_str(), NULL, 0);
48-
size_t point_int = std::strtoul(point.address_string.c_str(), NULL, 0);
54+
auto point_int = address2size_t(point);
55+
CHECK_RETURN(check_containment(point_int));
4956
return (point_int - begin_int) / member_size;
5057
}
5158

@@ -55,7 +62,7 @@ gdb_value_extractort::find_dynamic_allocation(irep_idt name)
5562
return std::find_if(
5663
dynamically_allocated.begin(),
5764
dynamically_allocated.end(),
58-
[&name](const memory_scopet &scope) { return scope.name == name; });
65+
[&name](const memory_scopet &scope) { return scope.id() == name; });
5966
}
6067

6168
std::vector<gdb_value_extractort::memory_scopet>::iterator
@@ -75,7 +82,7 @@ optionalt<mp_integer> gdb_value_extractort::get_malloc_size(irep_idt name)
7582
if(scope_it == dynamically_allocated.end())
7683
return {};
7784
else
78-
return scope_it->byte_size;
85+
return scope_it->size();
7986
}
8087

8188
optionalt<std::string> gdb_value_extractort::get_malloc_pointee(
@@ -87,7 +94,7 @@ optionalt<std::string> gdb_value_extractort::get_malloc_pointee(
8794
return {};
8895

8996
const auto pointer_distance = scope_it->distance(point, member_size);
90-
return id2string(scope_it->name) +
97+
return id2string(scope_it->id()) +
9198
(pointer_distance > 0 ? "+" + integer2string(pointer_distance) : "");
9299
}
93100

@@ -113,14 +120,13 @@ void gdb_value_extractort::analyze_symbols(const std::vector<irep_idt> &symbols)
113120
values.insert({value.address, symbol_expr});
114121

115122
const symbolt &symbol = ns.lookup(id);
116-
const symbol_exprt actual_expr = symbol.symbol_expr();
117-
if(actual_expr.type().id() != ID_pointer)
123+
if(symbol.type.id() != ID_pointer)
118124
{
119-
memory_map[id2string(id)] = value;
125+
memory_map[id] = value;
120126
continue;
121127
}
122128

123-
const std::string c_symbol = c_converter.convert(actual_expr);
129+
const std::string c_symbol = c_converter.convert(symbol.symbol_expr());
124130
const pointer_valuet &symbol_value = gdb_api.get_memory(c_symbol);
125131
size_t symbol_size = gdb_api.query_malloc_size(c_symbol);
126132

@@ -285,29 +291,30 @@ exprt gdb_value_extractort::get_pointer_to_member_value(
285291
const symbolt *struct_symbol = symbol_table.lookup(struct_name);
286292
DATA_INVARIANT(struct_symbol != nullptr, "unknown struct");
287293

288-
if(memory_map.count(struct_name) == 0)
294+
if(!has_known_memory_location(struct_name))
289295
{
290296
memory_map[struct_name] = gdb_api.get_memory(struct_name);
291297
analyze_symbol(irep_idt{struct_name});
292298
}
293299

294-
if(struct_symbol->symbol_expr().type().id() == ID_array)
300+
const auto &struct_symbol_expr = struct_symbol->symbol_expr();
301+
if(struct_symbol->type.id() == ID_array)
295302
{
296303
return index_exprt{
297-
struct_symbol->symbol_expr(),
304+
struct_symbol_expr,
298305
from_integer(
299306
member_offset / get_type_size(expr.type().subtype()), index_type())};
300307
}
301-
if(struct_symbol->symbol_expr().type().id() == ID_pointer)
308+
if(struct_symbol->type.id() == ID_pointer)
302309
{
303310
return dereference_exprt{
304-
plus_exprt{struct_symbol->symbol_expr(),
311+
plus_exprt{struct_symbol_expr,
305312
from_integer(member_offset, size_type()),
306313
expr.type()}};
307314
}
308315

309316
const auto maybe_member_expr = get_subexpression_at_offset(
310-
struct_symbol->symbol_expr(), member_offset, expr.type().subtype(), ns);
317+
struct_symbol_expr, member_offset, expr.type().subtype(), ns);
311318
DATA_INVARIANT(
312319
maybe_member_expr.has_value(), "structure doesn't have member");
313320

src/memory-analyzer/analyze_symbol.h

Lines changed: 42 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -93,37 +93,70 @@ class gdb_value_extractort
9393

9494
struct memory_scopet
9595
{
96-
memory_addresst begin;
96+
private:
97+
size_t begin_int;
9798
mp_integer byte_size;
9899
irep_idt name;
99100

100-
memory_scopet() = delete;
101-
memory_scopet(
102-
const memory_addresst &begin,
103-
mp_integer byte_size,
104-
irep_idt name)
105-
: begin(begin), byte_size(byte_size), name(name)
101+
/// Convert base-16 memory address to a natural number
102+
/// \param point: the memory address to be converted
103+
/// \return base-10 unsigned integer equal in value to \p point
104+
size_t address2size_t(const memory_addresst &point) const;
105+
106+
/// Helper function that check if a point in memory points inside this scope
107+
/// \param point_int: memory point as natural number
108+
/// \return true if the point is inside this scope
109+
bool check_containment(const size_t &point_int) const
106110
{
111+
return point_int >= begin_int && (begin_int + byte_size) > point_int;
107112
}
108113

114+
public:
115+
memory_scopet(
116+
const memory_addresst &begin,
117+
const mp_integer &byte_size,
118+
const irep_idt &name);
119+
109120
/// Check if \p point points somewhere in this memory scope
110121
/// \param point: memory address to be check for presence
111122
/// \return true if \p point is inside *this
112-
bool contains(const memory_addresst &point) const;
123+
bool contains(const memory_addresst &point) const
124+
{
125+
return check_containment(address2size_t(point));
126+
}
113127

114128
/// Compute the distance of \p point from the beginning of this scope
115129
/// \param point: memory address to have the offset computed
116130
/// \param member_size: size of one element of this scope in bytes
117131
/// \return `n' such that \p point is the n-th element of this scope
118132
mp_integer
119133
distance(const memory_addresst &point, mp_integer member_size) const;
134+
135+
/// Getter for the name of this memory scope
136+
/// \return the name as irep id
137+
irep_idt id() const
138+
{
139+
return name;
140+
}
141+
142+
/// Getter for the allocation size of this memory scope
143+
/// \return the size in bytes
144+
mp_integer size() const
145+
{
146+
return byte_size;
147+
}
120148
};
121149

122150
/// Keep track of the dynamically allocated memory
123151
std::vector<memory_scopet> dynamically_allocated;
124152

125153
/// Keep track of the memory location for the analyzed symbols
126-
std::map<std::string, pointer_valuet> memory_map;
154+
std::map<irep_idt, pointer_valuet> memory_map;
155+
156+
bool has_known_memory_location(const irep_idt &id) const
157+
{
158+
return memory_map.count(id) != 0;
159+
}
127160

128161
/// Search for a memory scope allocated under \p name
129162
/// \param name: name of the pointer used during allocation

0 commit comments

Comments
 (0)