Skip to content

Commit eb4de71

Browse files
Petr BauchPetr Bauch
authored andcommitted
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 f23cb27 commit eb4de71

File tree

2 files changed

+79
-1
lines changed

2 files changed

+79
-1
lines changed

src/memory-analyzer/analyze_symbol.cpp

Lines changed: 61 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -35,10 +35,13 @@ Author: Malte Mues <[email protected]>
3535
#include <util/expr_initializer.h>
3636
#include <util/irep.h>
3737
#include <util/mp_arith.h>
38+
#include <util/pointer_offset_size.h>
3839
#include <util/std_code.h>
3940
#include <util/std_expr.h>
4041
#include <util/std_types.h>
4142
#include <util/string_constant.h>
43+
#include <util/string_utils.h>
44+
#include <util/string2int.h>
4245

4346
symbol_analyzert::symbol_analyzert(
4447
const symbol_tablet &symbol_table,
@@ -191,6 +194,43 @@ exprt symbol_analyzert::get_char_pointer_value(
191194
}
192195
}
193196

197+
exprt symbol_analyzert::get_pointer_to_member_value(
198+
const exprt &expr,
199+
const pointer_valuet &pointer_value,
200+
const source_locationt &location)
201+
{
202+
PRECONDITION(expr.type().id() == ID_pointer);
203+
PRECONDITION(!is_c_char(expr.type().subtype()));
204+
std::string memory_location = pointer_value.address;
205+
PRECONDITION(memory_location != "0x0");
206+
PRECONDITION(!pointer_value.pointee.empty());
207+
208+
std::string struct_name;
209+
size_t member_offset;
210+
if(pointer_value.pointee.find("+") != std::string::npos)
211+
{
212+
std::string member_offset_string;
213+
split_string(
214+
pointer_value.pointee, '+', struct_name, member_offset_string, true);
215+
member_offset = safe_string2size_t(member_offset_string);
216+
}
217+
else
218+
{
219+
struct_name = pointer_value.pointee;
220+
member_offset = 0;
221+
}
222+
223+
const symbolt *struct_symbol = symbol_table.lookup(struct_name);
224+
DATA_INVARIANT(struct_symbol != nullptr, "unknown struct");
225+
226+
const auto maybe_member_expr = get_subexpression_at_offset(
227+
struct_symbol->symbol_expr(), member_offset, expr.type().subtype(), ns);
228+
if(maybe_member_expr.has_value())
229+
return *maybe_member_expr;
230+
231+
UNREACHABLE;
232+
}
233+
194234
exprt symbol_analyzert::get_non_char_pointer_value(
195235
const exprt &expr,
196236
const std::string memory_location,
@@ -236,6 +276,24 @@ exprt symbol_analyzert::get_non_char_pointer_value(
236276
}
237277
}
238278

279+
bool symbol_analyzert::points_to_member(
280+
const pointer_valuet &pointer_value) const
281+
{
282+
if(pointer_value.pointee.find("+") != std::string::npos)
283+
return true;
284+
285+
const symbolt *pointee_symbol = symbol_table.lookup(pointer_value.pointee);
286+
if(pointee_symbol == nullptr)
287+
return false;
288+
const auto pointee_type = pointee_symbol->type;
289+
if(
290+
pointee_type.id() == ID_struct_tag || pointee_type.id() == ID_union_tag ||
291+
pointee_type.id() == ID_array || pointee_type.id() == ID_struct ||
292+
pointee_type.id() == ID_union)
293+
return true;
294+
return false;
295+
}
296+
239297
exprt symbol_analyzert::get_pointer_value(
240298
const exprt &expr,
241299
const exprt &zero_expr,
@@ -260,7 +318,9 @@ exprt symbol_analyzert::get_pointer_value(
260318
else
261319
{
262320
const exprt target_expr =
263-
get_non_char_pointer_value(expr, memory_location, location);
321+
points_to_member(value)
322+
? get_pointer_to_member_value(expr, value, location)
323+
: get_non_char_pointer_value(expr, memory_location, location);
264324

265325
if(target_expr.id() == ID_nil)
266326
{

src/memory-analyzer/analyze_symbol.h

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -145,6 +145,18 @@ class symbol_analyzert
145145
const exprt &zero_expr,
146146
const source_locationt &location);
147147

148+
/// Call \ref get_subexpression_at_offset to get the correct member
149+
/// expression.
150+
/// \param expr: the input pointer expression (needed to get the right type)
151+
/// \param pointer_value: pointer value with structure name and offset as the
152+
/// pointee member
153+
/// \param location: the source location
154+
/// \return \ref member_exprt that the \p pointer_value points to
155+
exprt get_pointer_to_member_value(
156+
const exprt &expr,
157+
const pointer_valuet &pointer_value,
158+
const source_locationt &location);
159+
148160
/// Similar to \ref get_char_pointer_value. Doesn't re-call
149161
/// \ref gdb_apit::get_memory, calls \ref get_expr_value on _dereferenced_
150162
/// \p expr (the result of which is assigned to a new symbol).
@@ -174,6 +186,12 @@ class symbol_analyzert
174186

175187
/// Call \ref add_assignment for each pair in \ref outstanding_assignments
176188
void process_outstanding_assignments();
189+
190+
/// Analyzes the \p pointer_value to decide if it point to a struct or a
191+
/// union (or array)
192+
/// \param pointer_value: pointer value to be analyzed
193+
/// \return true if pointing to a member
194+
bool points_to_member(const pointer_valuet &pointer_value) const;
177195
};
178196

179197
#endif // CPROVER_MEMORY_ANALYZER_ANALYZE_SYMBOL_H

0 commit comments

Comments
 (0)