Skip to content

Commit 2325baa

Browse files
committed
Cleanup GOTO model validation of function calls
Function calls can use dereference expressions or symbol expressions, but nothing else. There is no need to make this configurable for those ought to be invariants. Fixes: #7022
1 parent 02a74fa commit 2325baa

File tree

3 files changed

+13
-91
lines changed

3 files changed

+13
-91
lines changed

src/goto-programs/validate_goto_model.cpp

Lines changed: 13 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -34,9 +34,6 @@ class validate_goto_modelt
3434
/// until they are linked.
3535
void entry_point_exists();
3636

37-
/// Check that no function calls via function pointer are present
38-
void function_pointer_calls_removed();
39-
4037
/// Check that for all:
4138
/// -# functions that are called or
4239
/// -# functions of which the address is taken
@@ -61,13 +58,7 @@ validate_goto_modelt::validate_goto_modelt(
6158
if(validation_options.entry_point_exists)
6259
entry_point_exists();
6360

64-
if(validation_options.function_pointer_calls_removed)
65-
{
66-
function_pointer_calls_removed();
67-
}
68-
69-
if(validation_options.check_called_functions)
70-
check_called_functions();
61+
check_called_functions();
7162
}
7263

7364
void validate_goto_modelt::entry_point_exists()
@@ -78,23 +69,6 @@ void validate_goto_modelt::entry_point_exists()
7869
"an entry point must exist");
7970
}
8071

81-
void validate_goto_modelt::function_pointer_calls_removed()
82-
{
83-
for(const auto &fun : function_map)
84-
{
85-
for(const auto &instr : fun.second.body.instructions)
86-
{
87-
if(instr.is_function_call())
88-
{
89-
DATA_CHECK(
90-
vm,
91-
instr.call_function().id() == ID_symbol,
92-
"no calls via function pointer should be present");
93-
}
94-
}
95-
}
96-
}
97-
9872
void validate_goto_modelt::check_called_functions()
9973
{
10074
auto test_for_function_address =
@@ -123,6 +97,18 @@ void validate_goto_modelt::check_called_functions()
12397
// check functions that are called
12498
if(instr.is_function_call())
12599
{
100+
// calls through function pointers are represented by dereference
101+
// expressions
102+
if(instr.call_function().id() == ID_dereference)
103+
continue;
104+
105+
// the only other permitted expression is a symbol
106+
DATA_CHECK(
107+
vm,
108+
instr.call_function().id() == ID_symbol &&
109+
instr.call_function().type().id() == ID_code,
110+
"function call expected to be code-typed symbol expression");
111+
126112
const irep_idt &identifier =
127113
to_symbol_expr(instr.call_function()).get_identifier();
128114

src/goto-programs/validate_goto_model.h

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -18,18 +18,13 @@ class goto_model_validation_optionst final
1818
// this check is disabled by default (not all goto programs
1919
// have an entry point)
2020
bool entry_point_exists = false;
21-
22-
bool function_pointer_calls_removed = true;
2321
bool check_returns_removed = true;
24-
bool check_called_functions = true;
2522

2623
private:
2724
void set_all_flags(bool options_value)
2825
{
2926
entry_point_exists = options_value;
30-
function_pointer_calls_removed = options_value;
3127
check_returns_removed = options_value;
32-
check_called_functions = options_value;
3328
}
3429

3530
public:

unit/goto-programs/goto_program_validate.cpp

Lines changed: 0 additions & 59 deletions
Original file line numberDiff line numberDiff line change
@@ -132,59 +132,6 @@ SCENARIO("Validation of a goto program", "[core][goto-programs][validate]")
132132
}
133133
}
134134

135-
/// check function_pointer_calls_removed()
136-
WHEN("not all function calls via fn pointer have been removed")
137-
{
138-
THEN("fail!")
139-
{
140-
// introduce function k that has a function pointer call;
141-
symbolt k;
142-
k.name = "k";
143-
k.mode = ID_C;
144-
k.type = code_typet({}, empty_typet{}); // void return, take no params
145-
146-
code_function_callt function_call{
147-
dereference_exprt{fn_ptr.symbol_expr(),
148-
pointer_typet(code_typet{{}, empty_typet{}}, 64)}};
149-
150-
code_blockt k_body{{function_call}};
151-
k.value = k_body;
152-
153-
goto_model.symbol_table.add(k);
154-
goto_convert(goto_model, null_message_handler);
155-
156-
goto_model_validation_optionst validation_options{
157-
goto_model_validation_optionst ::set_optionst::all_false};
158-
159-
validation_options.function_pointer_calls_removed = true;
160-
161-
REQUIRE_THROWS_AS(
162-
validate_goto_model(
163-
goto_model.goto_functions,
164-
validation_modet::EXCEPTION,
165-
validation_options),
166-
incorrect_goto_program_exceptiont);
167-
}
168-
}
169-
170-
WHEN("all function calls via fn pointer have been removed")
171-
{
172-
THEN("pass!")
173-
{
174-
goto_convert(goto_model, null_message_handler);
175-
176-
goto_model_validation_optionst validation_options{
177-
goto_model_validation_optionst ::set_optionst::all_false};
178-
179-
validation_options.function_pointer_calls_removed = true;
180-
181-
REQUIRE_NOTHROW(validate_goto_model(
182-
goto_model.goto_functions,
183-
validation_modet::EXCEPTION,
184-
validation_options));
185-
}
186-
}
187-
188135
WHEN("all returns have been removed")
189136
{
190137
THEN("true!")
@@ -218,8 +165,6 @@ SCENARIO("Validation of a goto program", "[core][goto-programs][validate]")
218165
goto_model_validation_optionst validation_options{
219166
goto_model_validation_optionst ::set_optionst::all_false};
220167

221-
validation_options.check_called_functions = true;
222-
223168
REQUIRE_THROWS_AS(
224169
validate_goto_model(
225170
goto_model.goto_functions,
@@ -242,8 +187,6 @@ SCENARIO("Validation of a goto program", "[core][goto-programs][validate]")
242187
goto_model_validation_optionst validation_options{
243188
goto_model_validation_optionst ::set_optionst::all_false};
244189

245-
validation_options.check_called_functions = true;
246-
247190
REQUIRE_THROWS_AS(
248191
validate_goto_model(
249192
goto_model.goto_functions,
@@ -264,8 +207,6 @@ SCENARIO("Validation of a goto program", "[core][goto-programs][validate]")
264207
goto_model_validation_optionst validation_options{
265208
goto_model_validation_optionst ::set_optionst::all_false};
266209

267-
validation_options.check_called_functions = true;
268-
269210
REQUIRE_NOTHROW(validate_goto_model(
270211
goto_model.goto_functions,
271212
validation_modet::EXCEPTION,

0 commit comments

Comments
 (0)