Skip to content

Commit 33d0a79

Browse files
committed
Re-implement points_to_member query
To account for the possibility of the pointee to be dynamically allocated.
1 parent 2b89941 commit 33d0a79

File tree

2 files changed

+28
-3
lines changed

2 files changed

+28
-3
lines changed

src/memory-analyzer/analyze_symbol.cpp

Lines changed: 20 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -91,6 +91,13 @@ optionalt<std::string> gdb_value_extractort::get_malloc_pointee(
9191
(pointer_distance > 0 ? "+" + integer2string(pointer_distance) : "");
9292
}
9393

94+
mp_integer gdb_value_extractort::get_type_size(const typet &type) const
95+
{
96+
const auto maybe_size = pointer_offset_bits(type, ns);
97+
CHECK_RETURN(maybe_size.has_value());
98+
return *maybe_size / 8;
99+
}
100+
94101
void gdb_value_extractort::analyze_symbols(
95102
const std::vector<std::string> &symbols)
96103
{
@@ -433,11 +440,22 @@ exprt gdb_value_extractort::get_non_char_pointer_value(
433440
}
434441

435442
bool gdb_value_extractort::points_to_member(
436-
const pointer_valuet &pointer_value) const
443+
pointer_valuet &pointer_value,
444+
const typet &expected_type)
437445
{
438446
if(pointer_value.pointee.find("+") != std::string::npos)
439447
return true;
440448

449+
if(pointer_value.pointee.empty())
450+
{
451+
const auto maybe_pointee = get_malloc_pointee(
452+
pointer_value.address, get_type_size(expected_type.subtype()));
453+
if(maybe_pointee.has_value())
454+
pointer_value.pointee = *maybe_pointee;
455+
if(pointer_value.pointee.find("+") != std::string::npos)
456+
return true;
457+
}
458+
441459
const symbolt *pointee_symbol = symbol_table.lookup(pointer_value.pointee);
442460
if(pointee_symbol == nullptr)
443461
return false;
@@ -470,7 +488,7 @@ exprt gdb_value_extractort::get_pointer_value(
470488
if(!memory_location.is_null())
471489
{
472490
// pointers-to-char can point to members as well, e.g. char[]
473-
if(points_to_member(value))
491+
if(points_to_member(value, expr.type()))
474492
{
475493
const auto target_expr =
476494
get_pointer_to_member_value(expr, value, location);

src/memory-analyzer/analyze_symbol.h

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -155,6 +155,11 @@ class gdb_value_extractort
155155
optionalt<std::string>
156156
get_malloc_pointee(const memory_addresst &point, mp_integer member_size);
157157

158+
/// Wrapper for call get_offset_pointer_bits
159+
/// \param type: type to get the size of
160+
/// \return the size of the type in bytes
161+
mp_integer get_type_size(const typet &type) const;
162+
158163
/// Assign the gdb-extracted value for \p symbol_name to its symbol
159164
/// expression and then process outstanding assignments that this
160165
/// extraction introduced.
@@ -274,8 +279,10 @@ class gdb_value_extractort
274279
/// Analyzes the \p pointer_value to decide if it point to a struct or a
275280
/// union (or array)
276281
/// \param pointer_value: pointer value to be analyzed
282+
/// \param expected_type: type of the potential member
277283
/// \return true if pointing to a member
278-
bool points_to_member(const pointer_valuet &pointer_value) const;
284+
bool
285+
points_to_member(pointer_valuet &pointer_value, const typet &expected_type);
279286
};
280287

281288
#endif // CPROVER_MEMORY_ANALYZER_ANALYZE_SYMBOL_H

0 commit comments

Comments
 (0)