Skip to content

Commit 0c31a7f

Browse files
Petr BauchPetr Bauch
Petr Bauch
authored and
Petr Bauch
committed
Make pointers-to-struct-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`. Then modify test to be executed.
1 parent dbff82c commit 0c31a7f

File tree

4 files changed

+49
-4
lines changed

4 files changed

+49
-4
lines changed

regression/snapshot-harness/pointer_to_struct_01/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,8 +5,8 @@ st,p,q --harness-type initialise-with-memory-snapshot --initial-location main:4
55
^SIGNAL=0$
66
\[main.assertion.1\] line [0-9]+ assertion p == \&st: SUCCESS
77
\[main.assertion.2\] line [0-9]+ assertion p-\>next == \&st: SUCCESS
8-
\[main.assertion.3\] line [0-9]+ assertion p != q: SUCCESS
9-
\[main.assertion.4\] line [0-9]+ assertion p == q: SUCCESS
8+
\[main.assertion.3\] line [0-9]+ assertion p \!= q: SUCCESS
9+
\[main.assertion.4\] line [0-9]+ assertion p == q-\>next: SUCCESS
1010
VERIFICATION SUCCESSFUL
1111
--
1212
^warning: ignoring

regression/snapshot-harness/structs_01/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
CORE
22
main.c
33
st,p --harness-type initialise-with-memory-snapshot --initial-location main:4
44
^EXIT=0$

src/memory-analyzer/analyze_symbol.cpp

Lines changed: 34 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,34 @@ 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+
std::string member_offset_string;
210+
split_string(
211+
pointer_value.pointee, '+', struct_name, member_offset_string, true);
212+
size_t member_offset = safe_string2size_t(member_offset_string);
213+
214+
const symbolt *struct_symbol = symbol_table.lookup(struct_name);
215+
DATA_INVARIANT(struct_symbol != nullptr, "unknown struct");
216+
217+
const auto maybe_member_expr = get_subexpression_at_offset(
218+
struct_symbol->symbol_expr(), member_offset, expr.type().subtype(), ns);
219+
if(maybe_member_expr.has_value())
220+
return *maybe_member_expr;
221+
222+
UNREACHABLE;
223+
}
224+
194225
exprt symbol_analyzert::get_non_char_pointer_value(
195226
const exprt &expr,
196227
const std::string memory_location,
@@ -262,7 +293,9 @@ exprt symbol_analyzert::get_pointer_value(
262293
else
263294
{
264295
const exprt target_expr =
265-
get_non_char_pointer_value(expr, memory_location, location);
296+
(value.pointee.find("+") == std::string::npos)
297+
? get_non_char_pointer_value(expr, memory_location, location)
298+
: get_pointer_to_member_value(expr, value, location);
266299

267300
if(target_expr.id() == ID_nil)
268301
{

src/memory-analyzer/analyze_symbol.h

Lines changed: 12 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).

0 commit comments

Comments
 (0)