Skip to content

Commit 09cf08d

Browse files
authored
Merge pull request diffblue#4730 from xbauch/feature/gdb-function-pointers
Extract function pointers using memory analyzer
2 parents 891f04e + 8941f72 commit 09cf08d

File tree

8 files changed

+194
-6
lines changed

8 files changed

+194
-6
lines changed
Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
#include <assert.h>
2+
3+
int foo(int i)
4+
{
5+
return i + 1;
6+
}
7+
8+
int (*fun_ptr)(int);
9+
10+
void initialize()
11+
{
12+
fun_ptr = &foo;
13+
}
14+
15+
void checkpoint()
16+
{
17+
}
18+
19+
int main()
20+
{
21+
initialize();
22+
checkpoint();
23+
24+
assert(fun_ptr == &foo);
25+
assert((*fun_ptr)(5) == 6);
26+
assert((*fun_ptr)(5) == foo(5));
27+
return 0;
28+
}
Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
main.c
3+
fun_ptr --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
\[main.assertion.1\] line [0-9]+ assertion fun_ptr == \&foo: SUCCESS
7+
\[main.assertion.2\] line [0-9]+ assertion \(\*fun_ptr\)\(5\) == 6: SUCCESS
8+
\[main.assertion.3\] line [0-9]+ assertion \(\*fun_ptr\)\(5\) == foo\(5\): SUCCESS
9+
VERIFICATION SUCCESSFUL
10+
--
11+
^warning: ignoring
Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
1+
#include <assert.h>
2+
3+
int plus(int i)
4+
{
5+
return i + 1;
6+
}
7+
8+
int minus(int i)
9+
{
10+
return i - 1;
11+
}
12+
13+
int (*fun_ptr1)(int);
14+
int (*fun_ptr2)(int);
15+
16+
void initialize()
17+
{
18+
fun_ptr1 = &plus;
19+
fun_ptr2 = &minus;
20+
}
21+
22+
void checkpoint()
23+
{
24+
}
25+
26+
int main()
27+
{
28+
initialize();
29+
checkpoint();
30+
31+
assert(fun_ptr1 == &plus);
32+
assert((*fun_ptr1)(5) == 6);
33+
assert((*fun_ptr1)(5) == plus(5));
34+
assert(fun_ptr2 != fun_ptr1);
35+
assert((*fun_ptr2)(5) == 4);
36+
return 0;
37+
}
Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
main.c
3+
fun_ptr1,fun_ptr2 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
\[main.assertion.1\] line [0-9]+ assertion fun_ptr1 == \&plus: SUCCESS
7+
\[main.assertion.2\] line [0-9]+ assertion \(\*fun_ptr1\)\(5\) == 6: SUCCESS
8+
\[main.assertion.3\] line [0-9]+ assertion \(\*fun_ptr1\)\(5\) == plus\(5\): SUCCESS
9+
\[main.assertion.4\] line [0-9]+ assertion fun_ptr2 \!= fun_ptr1: SUCCESS
10+
\[main.assertion.5\] line [0-9]+ assertion \(\*fun_ptr2\)\(5\) == 4: SUCCESS
11+
VERIFICATION SUCCESSFUL
12+
--
13+
^warning: ignoring
Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,42 @@
1+
#include <assert.h>
2+
3+
int plus(int i)
4+
{
5+
return i + 1;
6+
}
7+
8+
int minus(int i)
9+
{
10+
return i - 1;
11+
}
12+
13+
typedef int (*fun_ptrt)(int);
14+
fun_ptrt fun_array[2];
15+
16+
fun_ptrt fun_ptr1;
17+
fun_ptrt fun_ptr2;
18+
19+
void initialize()
20+
{
21+
fun_array[0] = &plus;
22+
fun_array[1] = &minus;
23+
fun_ptr1 = *fun_array;
24+
fun_ptr2 = fun_array[1];
25+
}
26+
27+
void checkpoint()
28+
{
29+
}
30+
31+
int main()
32+
{
33+
initialize();
34+
checkpoint();
35+
36+
assert(fun_ptr1 == &plus);
37+
assert((*fun_ptr1)(5) == 6);
38+
assert((*fun_ptr1)(5) == plus(5));
39+
assert(fun_ptr2 != fun_ptr1);
40+
assert((*fun_ptr2)(5) == 4);
41+
return 0;
42+
}
Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
main.c
3+
fun_array,fun_ptr1,fun_ptr2 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
\[main.assertion.1\] line [0-9]+ assertion fun_ptr1 == \&plus: SUCCESS
7+
\[main.assertion.2\] line [0-9]+ assertion \(\*fun_ptr1\)\(5\) == 6: SUCCESS
8+
\[main.assertion.3\] line [0-9]+ assertion \(\*fun_ptr1\)\(5\) == plus\(5\): SUCCESS
9+
\[main.assertion.4\] line [0-9]+ assertion fun_ptr2 \!= fun_ptr1: SUCCESS
10+
\[main.assertion.5\] line [0-9]+ assertion \(\*fun_ptr2\)\(5\) == 4: SUCCESS
11+
VERIFICATION SUCCESSFUL
12+
--
13+
^warning: ignoring

src/memory-analyzer/analyze_symbol.cpp

Lines changed: 38 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -324,6 +324,27 @@ exprt gdb_value_extractort::get_pointer_to_member_value(
324324
return *maybe_member_expr;
325325
}
326326

327+
exprt gdb_value_extractort::get_pointer_to_function_value(
328+
const exprt &expr,
329+
const pointer_valuet &pointer_value,
330+
const source_locationt &location)
331+
{
332+
PRECONDITION(expr.type().id() == ID_pointer);
333+
PRECONDITION(expr.type().subtype().id() == ID_code);
334+
PRECONDITION(!pointer_value.address.is_null());
335+
336+
const auto &function_name = pointer_value.pointee;
337+
CHECK_RETURN(!function_name.empty());
338+
const auto function_symbol = symbol_table.lookup(function_name);
339+
if(function_symbol == nullptr)
340+
{
341+
throw invalid_source_file_exceptiont{
342+
"input source code does not contain function: " + function_name};
343+
}
344+
CHECK_RETURN(function_symbol->type.id() == ID_code);
345+
return function_symbol->symbol_expr();
346+
}
347+
327348
exprt gdb_value_extractort::get_non_char_pointer_value(
328349
const exprt &expr,
329350
const pointer_valuet &value,
@@ -484,9 +505,20 @@ exprt gdb_value_extractort::get_pointer_value(
484505
const auto target_expr =
485506
get_pointer_to_member_value(expr, value, location);
486507
CHECK_RETURN(target_expr.is_not_nil());
487-
const auto result_expr = address_of_exprt(target_expr);
508+
const address_of_exprt result_expr{target_expr};
509+
CHECK_RETURN(result_expr.type() == zero_expr.type());
510+
return std::move(result_expr);
511+
}
512+
513+
// pointer to function
514+
if(expr.type().subtype().id() == ID_code)
515+
{
516+
const auto target_expr =
517+
get_pointer_to_function_value(expr, value, location);
518+
CHECK_RETURN(target_expr.is_not_nil());
519+
const address_of_exprt result_expr{target_expr};
488520
CHECK_RETURN(result_expr.type() == zero_expr.type());
489-
return result_expr;
521+
return std::move(result_expr);
490522
}
491523

492524
// non-member: split for char/non-char
@@ -513,20 +545,20 @@ exprt gdb_value_extractort::get_pointer_value(
513545
CHECK_RETURN(result_indexed_expr.has_value());
514546
if(result_indexed_expr->type() == zero_expr.type())
515547
return *result_indexed_expr;
516-
const auto result_expr = address_of_exprt{*result_indexed_expr};
548+
const address_of_exprt result_expr{*result_indexed_expr};
517549
CHECK_RETURN(result_expr.type() == zero_expr.type());
518-
return result_expr;
550+
return std::move(result_expr);
519551
}
520552

521553
// if the types match return right away
522554
if(target_expr.type() == zero_expr.type())
523555
return target_expr;
524556

525557
// otherwise the address of target should type-match
526-
const auto result_expr = address_of_exprt(target_expr);
558+
const address_of_exprt result_expr{target_expr};
527559
if(result_expr.type() != zero_expr.type())
528560
return typecast_exprt{result_expr, zero_expr.type()};
529-
return result_expr;
561+
return std::move(result_expr);
530562
}
531563

532564
return zero_expr;

src/memory-analyzer/analyze_symbol.h

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -286,6 +286,18 @@ class gdb_value_extractort
286286
const pointer_valuet &value,
287287
const source_locationt &location);
288288

289+
/// Extract the function name from \p pointer_value, check it has a symbol and
290+
/// return the associated symbol expression
291+
/// \param expr: the pointer-to-function expression
292+
/// \param pointer_value: pointer value with the function name as the pointee
293+
/// member
294+
/// \param location: the source location
295+
/// \return symbol expression for the function pointed at by \p pointer_value
296+
exprt get_pointer_to_function_value(
297+
const exprt &expr,
298+
const pointer_valuet &pointer_value,
299+
const source_locationt &location);
300+
289301
/// If \p memory_location is found among \ref values then return the symbol
290302
/// expression associated with it.
291303
/// Otherwise we add the appropriate \ref values mapping:

0 commit comments

Comments
 (0)