Skip to content

Commit ba5748c

Browse files
committed
Re-implement points_to_member query
To account for the possibility of the pointee to be dynamically allocated.
1 parent c0ad089 commit ba5748c

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(const std::vector<irep_idt> &symbols)
95102
{
96103
// record addresses of given symbols
@@ -431,11 +438,22 @@ exprt gdb_value_extractort::get_non_char_pointer_value(
431438
}
432439

433440
bool gdb_value_extractort::points_to_member(
434-
const pointer_valuet &pointer_value) const
441+
pointer_valuet &pointer_value,
442+
const typet &expected_type)
435443
{
436444
if(pointer_value.has_known_offset())
437445
return true;
438446

447+
if(pointer_value.pointee.empty())
448+
{
449+
const auto maybe_pointee = get_malloc_pointee(
450+
pointer_value.address, get_type_size(expected_type.subtype()));
451+
if(maybe_pointee.has_value())
452+
pointer_value.pointee = *maybe_pointee;
453+
if(pointer_value.pointee.find("+") != std::string::npos)
454+
return true;
455+
}
456+
439457
const symbolt *pointee_symbol = symbol_table.lookup(pointer_value.pointee);
440458
if(pointee_symbol == nullptr)
441459
return false;
@@ -465,7 +483,7 @@ exprt gdb_value_extractort::get_pointer_value(
465483
if(!memory_location.is_null())
466484
{
467485
// pointers-to-char can point to members as well, e.g. char[]
468-
if(points_to_member(value))
486+
if(points_to_member(value, expr.type()))
469487
{
470488
const auto target_expr =
471489
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)