Skip to content

Commit eac8e2c

Browse files
author
Daniel Kroening
authored
Merge pull request #1009 from thk123/bugfix/arrays-structs-null-pointers
Fix for arrays containing structs will null pointers
2 parents 3c896fd + 8ec1890 commit eac8e2c

File tree

39 files changed

+124
-19
lines changed

39 files changed

+124
-19
lines changed

regression/goto-analyzer/approx-array-variable-const-fp/test.desc

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,3 +14,4 @@ main.c
1414
^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f8 THEN GOTO [0-9]$
1515
^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f9 THEN GOTO [0-9]$
1616
^warning: ignoring
17+
function \w+: replacing function pointer by 9 possible targets

regression/goto-analyzer/approx-const-fp-array-variable-cast-const-fp/test.desc

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,3 +14,4 @@ main.c
1414
^\s*IF fp_tbl\[\(signed long int\)i\] == f7 THEN GOTO [0-9]$
1515
^\s*IF fp_tbl\[\(signed long int\)i\] == f8 THEN GOTO [0-9]$
1616
^\s*IF fp_tbl\[\(signed long int\)i\] == f9 THEN GOTO [0-9]$
17+
function \w+: replacing function pointer by 9 possible targets

regression/goto-analyzer/approx-const-fp-array-variable-const-fp-with-null/test.desc

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ main.c
55
^\s*IF fp == f2 THEN GOTO [0-9]$
66
^\s*IF fp == f3 THEN GOTO [0-9]$
77
^\s*IF fp == f4 THEN GOTO [0-9]$
8+
replacing function pointer by 3 possible targets
89
^SIGNAL=0$
910
--
1011
^warning: ignoring
@@ -14,3 +15,4 @@ main.c
1415
^\s*IF fp_tbl\[\(signed long int\)i\] == f7 THEN GOTO [0-9]$
1516
^\s*IF fp_tbl\[\(signed long int\)i\] == f8 THEN GOTO [0-9]$
1617
^\s*IF fp_tbl\[\(signed long int\)i\] == f9 THEN GOTO [0-9]$
18+
function \w+: replacing function pointer by 9 possible targets

regression/goto-analyzer/approx-const-fp-array-variable-const-fp/test.desc

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,3 +14,4 @@ main.c
1414
^\s*IF fp_tbl\[\(signed long int\)i\] == f7 THEN GOTO [0-9]$
1515
^\s*IF fp_tbl\[\(signed long int\)i\] == f8 THEN GOTO [0-9]$
1616
^\s*IF fp_tbl\[\(signed long int\)i\] == f9 THEN GOTO [0-9]$
17+
function \w+: replacing function pointer by 9 possible targets

regression/goto-analyzer/approx-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,3 +14,4 @@ main.c
1414
^\s*IF fp_tbl\[\(signed long int\)i\] == f7 THEN GOTO [0-9]$
1515
^\s*IF fp_tbl\[\(signed long int\)i\] == f8 THEN GOTO [0-9]$
1616
^\s*IF fp_tbl\[\(signed long int\)i\] == f9 THEN GOTO [0-9]$
17+
function \w+: replacing function pointer by 9 possible targets

regression/goto-analyzer/approx-const-fp-array-variable-const-struct-non-const-fp/test.desc

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,3 +14,4 @@ main.c
1414
^\s*IF fp_tbl\[\(signed long int\)i\] == f7 THEN GOTO [0-9]$
1515
^\s*IF fp_tbl\[\(signed long int\)i\] == f8 THEN GOTO [0-9]$
1616
^\s*IF fp_tbl\[\(signed long int\)i\] == f9 THEN GOTO [0-9]$
17+
function \w+: replacing function pointer by 9 possible targets

regression/goto-analyzer/approx-const-fp-array-variable-invalid-cast-const-fp/test.desc

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,3 +14,4 @@ main.c
1414
^\s*IF fp_tbl\[\(signed long int\)i\] == f7 THEN GOTO [0-9]$
1515
^\s*IF fp_tbl\[\(signed long int\)i\] == f8 THEN GOTO [0-9]$
1616
^\s*IF fp_tbl\[\(signed long int\)i\] == f9 THEN GOTO [0-9]$
17+
function \w+: replacing function pointer by 9 possible targets
Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,42 @@
1+
#include <stdio.h>
2+
3+
void f1 (void) { printf("%i\n", 1); }
4+
void f2 (void) { printf("%i\n", 2); }
5+
void f3 (void) { printf("%i\n", 3); }
6+
void f4 (void) { printf("%i\n", 4); }
7+
void f5 (void) { printf("%i\n", 5); }
8+
void f6 (void) { printf("%i\n", 6); }
9+
void f7 (void) { printf("%i\n", 7); }
10+
void f8 (void) { printf("%i\n", 8); }
11+
void f9 (void) { printf("%i\n", 9); }
12+
13+
typedef void(*void_fp)(void);
14+
15+
struct action
16+
{
17+
int x;
18+
void_fp fun;
19+
};
20+
21+
// Array with an empty final element
22+
const struct action fp_tbl[5] = {{1, f2}, {2, f3} ,{3, f4},};
23+
24+
// There is a basic check that excludes all functions that aren't used anywhere
25+
// This ensures that check can't work in this example
26+
const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
27+
28+
void func(int i)
29+
{
30+
const void_fp fp = fp_tbl[i].fun;
31+
fp();
32+
}
33+
34+
int main()
35+
{
36+
for(int i=0;i<3;i++)
37+
{
38+
func(i);
39+
}
40+
41+
return 0;
42+
}
Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
CORE
2+
main.c
3+
--show-goto-functions --verbosity 10 --pointer-check
4+
^Removing function pointers and virtual functions$
5+
^\s*IF fp == f2 THEN GOTO [0-9]$
6+
^\s*IF fp == f3 THEN GOTO [0-9]$
7+
^\s*IF fp == f4 THEN GOTO [0-9]$
8+
^\s*ASSERT FALSE // invalid function pointer$
9+
^SIGNAL=0$
10+
--
11+
^warning: ignoring
12+
^\s*IF fp == f1 THEN GOTO [0-9]$
13+
^\s*IF fp == f5 THEN GOTO [0-9]$
14+
^\s*IF fp == f6 THEN GOTO [0-9]$
15+
^\s*IF fp == f7 THEN GOTO [0-9]$
16+
^\s*IF fp == f8 THEN GOTO [0-9]$
17+
^\s*IF fp == f9 THEN GOTO [0-9]$
18+
function \w+: replacing function pointer by 9 possible targets

regression/goto-analyzer/no-match-array-literal-const-fp-null/test.desc

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,5 +4,6 @@ main.c
44
^Removing function pointers and virtual functions$
55
^\s*ASSERT FALSE // invalid function pointer$
66
^SIGNAL=0$
7+
function func: replacing function pointer by 0 possible targets
78
--
89
^warning: ignoring

regression/goto-analyzer/no-match-const-fp-const-fp-null/test.desc

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,5 +4,6 @@ main.c
44
^Removing function pointers and virtual functions$
55
^\s*ASSERT FALSE // invalid function pointer$
66
^SIGNAL=0$
7+
replacing function pointer by 0 possible targets
78
--
89
^warning: ignoring

regression/goto-analyzer/no-match-const-fp-const-pointer-const-struct-const-fp-null/test.desc

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@ main.c
33
--show-goto-functions --verbosity 10 --pointer-check
44
^Removing function pointers and virtual functions$
55
^\s*ASSERT FALSE // invalid function pointer$
6+
replacing function pointer by 9 possible targets
67
^SIGNAL=0$
78
--
89
^warning: ignoring

regression/goto-analyzer/no-match-const-fp-dereference-const-pointer-null/test.desc

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@ main.c
33
--show-goto-functions --verbosity 10 --pointer-check
44
^Removing function pointers and virtual functions$
55
^\s*ASSERT FALSE // invalid function pointer$
6+
replacing function pointer by 9 possible targets
67
^SIGNAL=0$
78
--
89
^warning: ignoring

regression/goto-analyzer/no-match-const-fp-null/test.desc

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,5 +3,6 @@ main.c
33
--show-goto-functions --verbosity 10 --pointer-check
44
^Removing function pointers and virtual functions$
55
^\s*ASSERT FALSE // invalid function pointer$
6+
function func: replacing function pointer by 0 possible targets
67
--
78
^warning: ignoring

regression/goto-analyzer/no-match-const-struct-non-const-fp-null/test.desc

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,5 +4,6 @@ main.c
44
^Removing function pointers and virtual functions$
55
^\s*ASSERT FALSE // invalid function pointer$
66
^SIGNAL=0$
7+
replacing function pointer by 0 possible targets
78
--
89
^warning: ignoring

regression/goto-analyzer/precise-array-calculation-const-fp/test.desc

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,3 +6,4 @@ main.c
66
^SIGNAL=0$
77
--
88
^warning: ignoring
9+
function \w+: replacing function pointer by 9 possible targets

regression/goto-analyzer/precise-array-literal-const-fp/test.desc

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,3 +6,4 @@ main.c
66
^SIGNAL=0$
77
--
88
^warning: ignoring
9+
function \w+: replacing function pointer by 9 possible targets

regression/goto-analyzer/precise-const-fp-array-const-variable-const-fp/test.desc

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,3 +6,4 @@ main.c
66
^SIGNAL=0$
77
--
88
^warning: ignoring
9+
function \w+: replacing function pointer by 9 possible targets

regression/goto-analyzer/precise-const-fp-array-literal-const-fp-run-time/test.desc

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,3 +5,4 @@ main.c
55
^\s*f3\(\);$
66
--
77
^warning: ignoring
8+
function \w+: replacing function pointer by 9 possible targets

regression/goto-analyzer/precise-const-fp-array-literal-const-fp/test.desc

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,3 +6,4 @@ main.c
66
^SIGNAL=0$
77
--
88
^warning: ignoring
9+
function \w+: replacing function pointer by 9 possible targets

regression/goto-analyzer/precise-const-fp-array-literal-const-struct-non-const-fp/test.desc

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,3 +6,4 @@ main.c
66
^SIGNAL=0$
77
--
88
^warning: ignoring
9+
function \w+: replacing function pointer by 9 possible targets

regression/goto-analyzer/precise-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,3 +6,4 @@ main.c
66
^SIGNAL=0$
77
--
88
^warning: ignoring
9+
function \w+: replacing function pointer by 9 possible targets

regression/goto-analyzer/precise-const-fp-const-fp/test.desc

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,3 +6,4 @@ main.c
66
^SIGNAL=0$
77
--
88
^warning: ignoring
9+
function \w+: replacing function pointer by 9 possible targets

regression/goto-analyzer/precise-const-fp-const-struct-const-array-literal-fp/test.desc

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,3 +6,4 @@ main.c
66
^SIGNAL=0$
77
--
88
^warning: ignoring
9+
function \w+: replacing function pointer by 9 possible targets

regression/goto-analyzer/precise-const-fp-const-struct-non-const-array-literal-fp/test.desc

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,3 +6,4 @@ main.c
66
^SIGNAL=0$
77
--
88
^warning: ignoring
9+
function \w+: replacing function pointer by 9 possible targets

regression/goto-analyzer/precise-const-fp-const-struct-non-const-fp/test.desc

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,3 +6,4 @@ main.c
66
^SIGNAL=0$
77
--
88
^warning: ignoring
9+
function \w+: replacing function pointer by 9 possible targets

regression/goto-analyzer/precise-const-fp-dereference-const-pointer-const-fp/test.desc

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,3 +6,4 @@ main.c
66
^SIGNAL=0$
77
--
88
^warning: ignoring
9+
function \w+: replacing function pointer by 9 possible targets

regression/goto-analyzer/precise-const-fp/test.desc

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,3 +5,4 @@ main.c
55
^\s*f2\(\);
66
--
77
^warning: ignoring
8+
function \w+: replacing function pointer by 9 possible targets

regression/goto-analyzer/precise-const-pointer-const-struct-fp/test.desc

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,3 +6,4 @@ main.c
66
^SIGNAL=0$
77
--
88
^warning: ignoring
9+
function \w+: replacing function pointer by 9 possible targets

regression/goto-analyzer/precise-const-struct-non-const-fp/test.desc

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,3 +6,4 @@ main.c
66
^SIGNAL=0$
77
--
88
^warning: ignoring
9+
function \w+: replacing function pointer by 9 possible targets

regression/goto-analyzer/precise-derefence-const-pointer-const-fp/test.desc

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,3 +6,4 @@ main.c
66
^SIGNAL=0$
77
--
88
^warning: ignoring
9+
function \w+: replacing function pointer by 9 possible targets

regression/goto-analyzer/precise-derefence/test.desc

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,3 +5,4 @@ main.c
55
^\s*f2\(\);
66
--
77
^warning: ignoring
8+
function \w+: replacing function pointer by 9 possible targets

regression/goto-analyzer/precise-dereference-address-pointer-const-fp/test.desc

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,3 +6,4 @@ main.c
66
^SIGNAL=0$
77
--
88
^warning: ignoring
9+
function \w+: replacing function pointer by 9 possible targets

regression/goto-analyzer/precise-dereference-const-struct-const-pointer-const-fp/test.desc

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,3 +6,4 @@ main.c
66
^SIGNAL=0$
77
--
88
^warning: ignoring
9+
function \w+: replacing function pointer by 9 possible targets

regression/goto-analyzer/precise-dereference-const-struct-const-pointer-const-struct-const-fp/test.desc

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,3 +6,4 @@ main.c
66
^SIGNAL=0$
77
--
88
^warning: ignoring
9+
function \w+: replacing function pointer by 9 possible targets

regression/goto-analyzer/precise-dereference-const-struct-pointer-const-fp/test.desc

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,3 +6,4 @@ main.c
66
^SIGNAL=0$
77
--
88
^warning: ignoring
9+
function \w+: replacing function pointer by 9 possible targets

src/goto-programs/remove_const_function_pointers.cpp

Lines changed: 20 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -9,29 +9,26 @@ Author: Thomas Kiley, thomas.kiley@diffblue.com
99
/// \file
1010
/// Goto Programs
1111

12+
#include "remove_const_function_pointers.h"
13+
1214
#include <ansi-c/c_qualifiers.h>
1315
#include <util/simplify_expr.h>
1416
#include <util/arith_tools.h>
1517

16-
#include "remove_const_function_pointers.h"
17-
1818
#define LOG(message, irep) \
1919
debug() << "Case " << __LINE__ << " : " << message << "\n" \
2020
<< irep.pretty() << eom;
2121

2222
/// To take a function call on a function pointer, and if possible resolve it to
2323
/// a small collection of possible values.
2424
/// \param message_handler: The message handler for messaget
25-
/// \param base_expression: The function call through a function pointer
2625
/// \param ns: The namespace to use to resolve types
2726
/// \param symbol_table: The symbol table to look up symbols in
2827
remove_const_function_pointerst::remove_const_function_pointerst(
2928
message_handlert &message_handler,
30-
const exprt &base_expression,
3129
const namespacet &ns,
3230
const symbol_tablet &symbol_table):
3331
messaget(message_handler),
34-
original_expression(base_expression),
3532
ns(ns),
3633
symbol_table(symbol_table)
3734
{}
@@ -41,16 +38,18 @@ remove_const_function_pointerst::remove_const_function_pointerst(
4138
/// that are const and: - assigned directly to a function - assigned to a value
4239
/// in an array of functions - assigned to a const struct component Or
4340
/// variations within.
41+
/// \param base_expression: The function call through a function pointer
4442
/// \param out_functions: The functions that (symbols of type ID_code) the base
4543
/// expression could take.
4644
/// \return Returns true if it was able to resolve the call, false if not. If it
4745
/// returns true, out_functions will be populated by all the possible values
4846
/// the function pointer could be.
4947
bool remove_const_function_pointerst::operator()(
48+
const exprt &base_expression,
5049
functionst &out_functions)
5150
{
5251
// Replace all const symbols with their values
53-
exprt non_symbol_expression=replace_const_symbols(original_expression);
52+
exprt non_symbol_expression=replace_const_symbols(base_expression);
5453
return try_resolve_function_call(non_symbol_expression, out_functions);
5554
}
5655

@@ -165,6 +164,20 @@ bool remove_const_function_pointerst::try_resolve_function_call(
165164
resolved=false;
166165
}
167166
}
167+
else if(simplified_expr.id()==ID_constant)
168+
{
169+
if(simplified_expr.is_zero())
170+
{
171+
// We have the null pointer - no need to throw everything away
172+
// but we don't add any functions either
173+
resolved=true;
174+
}
175+
else
176+
{
177+
LOG("Non-zero constant value found", simplified_expr);
178+
resolved=false;
179+
}
180+
}
168181
else
169182
{
170183
LOG("Unrecognised expression", simplified_expr);
@@ -556,10 +569,7 @@ bool remove_const_function_pointerst::try_resolve_index_of(
556569

557570
for(const exprt &resolved_array_entry : array_contents)
558571
{
559-
if(!resolved_array_entry.is_zero())
560-
{
561-
out_expressions.push_back(resolved_array_entry);
562-
}
572+
out_expressions.push_back(resolved_array_entry);
563573
}
564574
}
565575
}

src/goto-programs/remove_const_function_pointers.h

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -27,11 +27,10 @@ class remove_const_function_pointerst:public messaget
2727
typedef std::list<exprt> expressionst;
2828
remove_const_function_pointerst(
2929
message_handlert &message_handler,
30-
const exprt &base_expression,
3130
const namespacet &ns,
3231
const symbol_tablet &symbol_table);
3332

34-
bool operator()(functionst &out_functions);
33+
bool operator()(const exprt &base_expression, functionst &out_functions);
3534

3635
private:
3736
exprt replace_const_symbols(const exprt &expression) const;
@@ -93,7 +92,6 @@ class remove_const_function_pointerst:public messaget
9392
exprt get_component_value(
9493
const struct_exprt &struct_expr, const member_exprt &member_expr);
9594

96-
const exprt original_expression;
9795
const namespacet &ns;
9896
const symbol_tablet &symbol_table;
9997
};

src/goto-programs/remove_function_pointers.cpp

Lines changed: 8 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com
2020
#include <util/base_type.h>
2121
#include <ansi-c/c_qualifiers.h>
2222
#include <analyses/does_remove_const.h>
23+
#include <util/invariant.h>
2324

2425
#include <util/c_types.h>
2526

@@ -292,14 +293,15 @@ void remove_function_pointerst::remove_function_pointer(
292293
else
293294
{
294295
remove_const_function_pointerst fpr(
295-
get_message_handler(), pointer, ns, symbol_table);
296+
get_message_handler(), ns, symbol_table);
296297

297-
found_functions=fpr(functions);
298+
found_functions=fpr(pointer, functions);
298299

299-
// Either found_functions is true therefore the functions should not
300-
// be empty
301-
// Or found_functions is false therefore the functions should be empty
302-
assert(found_functions != functions.empty());
300+
// if found_functions is false, functions should be empty
301+
// however, it is possible for found_functions to be true and functions
302+
// to be empty (this happens if the pointer can only resolve to the null
303+
// pointer)
304+
CHECK_RETURN(found_functions || functions.empty());
303305

304306
if(functions.size()==1)
305307
{

0 commit comments

Comments
 (0)