Skip to content

Commit a305967

Browse files
committed
Make pointers-to-member work
Change the memory-analyze to produce correct member expressions. Iterate over the offset from gdb, e.g. `st+4` means jump to the second member component inside `st`.
1 parent dcb93ff commit a305967

File tree

2 files changed

+117
-1
lines changed

2 files changed

+117
-1
lines changed

src/memory-analyzer/analyze_symbol.cpp

Lines changed: 99 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,10 @@ Author: Malte Mues <[email protected]>
1313
#include <util/c_types_util.h>
1414
#include <util/config.h>
1515
#include <util/expr_initializer.h>
16+
#include <util/pointer_offset_size.h>
17+
#include <util/string2int.h>
1618
#include <util/string_constant.h>
19+
#include <util/string_utils.h>
1720

1821
gdb_value_extractort::gdb_value_extractort(
1922
const symbol_tablet &symbol_table,
@@ -165,6 +168,84 @@ exprt gdb_value_extractort::get_char_pointer_value(
165168
}
166169
}
167170

171+
exprt gdb_value_extractort::get_pointer_to_member_value(
172+
const exprt &expr,
173+
const pointer_valuet &pointer_value,
174+
const source_locationt &location)
175+
{
176+
PRECONDITION(expr.type().id() == ID_pointer);
177+
PRECONDITION(!is_c_char_type(expr.type().subtype()));
178+
const auto &memory_location = pointer_value.address;
179+
std::string memory_location_string = memory_location.string();
180+
PRECONDITION(memory_location_string != "0x0");
181+
PRECONDITION(!pointer_value.pointee.empty());
182+
183+
std::string struct_name;
184+
size_t member_offset;
185+
if(pointer_value.has_known_offset())
186+
{
187+
std::string member_offset_string;
188+
split_string(
189+
pointer_value.pointee, '+', struct_name, member_offset_string, true);
190+
member_offset = safe_string2size_t(member_offset_string);
191+
}
192+
else
193+
{
194+
struct_name = pointer_value.pointee;
195+
member_offset = 0;
196+
}
197+
198+
const symbolt *struct_symbol = symbol_table.lookup(struct_name);
199+
DATA_INVARIANT(struct_symbol != nullptr, "unknown struct");
200+
const auto maybe_struct_size =
201+
pointer_offset_size(struct_symbol->symbol_expr().type(), ns);
202+
bool found = false;
203+
CHECK_RETURN(maybe_struct_size.has_value());
204+
for(const auto &value_pair : values)
205+
{
206+
const auto &value_symbol_expr = value_pair.second;
207+
if(to_symbol_expr(value_symbol_expr).get_identifier() == struct_name)
208+
{
209+
found = true;
210+
break;
211+
}
212+
}
213+
214+
if(!found)
215+
{
216+
const typet target_type = expr.type().subtype();
217+
218+
symbol_exprt dummy("tmp", expr.type());
219+
code_blockt assignments;
220+
221+
auto emplace_pair = values.emplace(
222+
memory_location,
223+
allocate_objects.allocate_automatic_local_object(
224+
assignments, dummy, target_type));
225+
const symbol_exprt &new_symbol = to_symbol_expr(emplace_pair.first->second);
226+
227+
dereference_exprt dereference_expr(expr);
228+
229+
const auto zero_expr = zero_initializer(target_type, location, ns);
230+
CHECK_RETURN(zero_expr);
231+
232+
// add assignment of value to newly created symbol
233+
add_assignment(new_symbol, *zero_expr);
234+
235+
const auto &struct_symbol = values.find(memory_location);
236+
237+
const auto maybe_member_expr = get_subexpression_at_offset(
238+
struct_symbol->second, member_offset, expr.type().subtype(), ns);
239+
CHECK_RETURN(maybe_member_expr.has_value());
240+
return *maybe_member_expr;
241+
}
242+
243+
const auto maybe_member_expr = get_subexpression_at_offset(
244+
struct_symbol->symbol_expr(), member_offset, expr.type().subtype(), ns);
245+
CHECK_RETURN(maybe_member_expr.has_value());
246+
return *maybe_member_expr;
247+
}
248+
168249
exprt gdb_value_extractort::get_non_char_pointer_value(
169250
const exprt &expr,
170251
const memory_addresst &memory_location,
@@ -210,6 +291,21 @@ exprt gdb_value_extractort::get_non_char_pointer_value(
210291
}
211292
}
212293

294+
bool gdb_value_extractort::points_to_member(
295+
const pointer_valuet &pointer_value) const
296+
{
297+
if(pointer_value.has_known_offset())
298+
return true;
299+
300+
const symbolt *pointee_symbol = symbol_table.lookup(pointer_value.pointee);
301+
if(pointee_symbol == nullptr)
302+
return false;
303+
const auto &pointee_type = pointee_symbol->type;
304+
return pointee_type.id() == ID_struct_tag ||
305+
pointee_type.id() == ID_union_tag || pointee_type.id() == ID_array ||
306+
pointee_type.id() == ID_struct || pointee_type.id() == ID_union;
307+
}
308+
213309
exprt gdb_value_extractort::get_pointer_value(
214310
const exprt &expr,
215311
const exprt &zero_expr,
@@ -234,7 +330,9 @@ exprt gdb_value_extractort::get_pointer_value(
234330
else
235331
{
236332
const exprt target_expr =
237-
get_non_char_pointer_value(expr, memory_location, location);
333+
points_to_member(value)
334+
? get_pointer_to_member_value(expr, value, location)
335+
: get_non_char_pointer_value(expr, memory_location, location);
238336

239337
if(target_expr.id() == ID_nil)
240338
{

src/memory-analyzer/analyze_symbol.h

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -150,6 +150,18 @@ class gdb_value_extractort
150150
const exprt &zero_expr,
151151
const source_locationt &location);
152152

153+
/// Call \ref get_subexpression_at_offset to get the correct member
154+
/// expression.
155+
/// \param expr: the input pointer expression (needed to get the right type)
156+
/// \param pointer_value: pointer value with structure name and offset as the
157+
/// pointee member
158+
/// \param location: the source location
159+
/// \return \ref member_exprt that the \p pointer_value points to
160+
exprt get_pointer_to_member_value(
161+
const exprt &expr,
162+
const pointer_valuet &pointer_value,
163+
const source_locationt &location);
164+
153165
/// Similar to \ref get_char_pointer_value. Doesn't re-call
154166
/// \ref gdb_apit::get_memory, calls \ref get_expr_value on _dereferenced_
155167
/// \p expr (the result of which is assigned to a new symbol).
@@ -184,6 +196,12 @@ class gdb_value_extractort
184196
/// \param expr: expression to be extracted
185197
/// \return the value as a string
186198
std::string get_gdb_value(const exprt &expr);
199+
200+
/// Analyzes the \p pointer_value to decide if it point to a struct or a
201+
/// union (or array)
202+
/// \param pointer_value: pointer value to be analyzed
203+
/// \return true if pointing to a member
204+
bool points_to_member(const pointer_valuet &pointer_value) const;
187205
};
188206

189207
#endif // CPROVER_MEMORY_ANALYZER_ANALYZE_SYMBOL_H

0 commit comments

Comments
 (0)