Skip to content

Commit 0d8e005

Browse files
committed
Function pointer restrictions: refactor pointer-name parsing
No changes in behaviour: this commit just moves the pointer-name parsing introduced in 771a153 to a function of its own. This is to prepare for a fix of #6609: the same name parsing also needs to be added to function-pointer-restriction parsing from JSON files. To enable this code move, the exception class is moved to the global scope.
1 parent 5917ab4 commit 0d8e005

File tree

3 files changed

+85
-68
lines changed

3 files changed

+85
-68
lines changed

src/goto-programs/restrict_function_pointers.cpp

Lines changed: 66 additions & 49 deletions
Original file line numberDiff line numberDiff line change
@@ -84,14 +84,14 @@ static void restrict_function_pointer(
8484
}
8585
} // namespace
8686

87-
function_pointer_restrictionst::invalid_restriction_exceptiont::
88-
invalid_restriction_exceptiont(std::string reason, std::string correct_format)
87+
invalid_restriction_exceptiont::invalid_restriction_exceptiont(
88+
std::string reason,
89+
std::string correct_format)
8990
: reason(std::move(reason)), correct_format(std::move(correct_format))
9091
{
9192
}
9293

93-
std::string
94-
function_pointer_restrictionst::invalid_restriction_exceptiont::what() const
94+
std::string invalid_restriction_exceptiont::what() const
9595
{
9696
std::string res;
9797

@@ -291,6 +291,66 @@ function_pointer_restrictionst::parse_function_pointer_restrictions_from_file(
291291
return merged_restrictions;
292292
}
293293

294+
/// Parse \p candidate to distinguish whether it refers to a function pointer
295+
/// symbol directly (as produced by \ref label_function_pointer_call_sites), or
296+
/// a source location via its statement label. In the latter case, resolve the
297+
/// name to the underlying function pointer symbol.
298+
static std::string resolve_pointer_name(
299+
const std::string &candidate,
300+
const goto_modelt &goto_model)
301+
{
302+
const auto last_dot = candidate.rfind('.');
303+
if(
304+
last_dot == std::string::npos || last_dot + 1 == candidate.size() ||
305+
isdigit(candidate[last_dot + 1]))
306+
{
307+
return candidate;
308+
}
309+
310+
std::string pointer_name = candidate;
311+
312+
const auto function_id = pointer_name.substr(0, last_dot);
313+
const auto label = pointer_name.substr(last_dot + 1);
314+
315+
bool found = false;
316+
const auto it = goto_model.goto_functions.function_map.find(function_id);
317+
if(it != goto_model.goto_functions.function_map.end())
318+
{
319+
optionalt<source_locationt> location;
320+
for(const auto &instruction : it->second.body.instructions)
321+
{
322+
if(
323+
std::find(
324+
instruction.labels.begin(), instruction.labels.end(), label) !=
325+
instruction.labels.end())
326+
{
327+
location = instruction.source_location();
328+
}
329+
330+
if(
331+
instruction.is_function_call() &&
332+
instruction.call_function().id() == ID_dereference &&
333+
location.has_value() && instruction.source_location() == *location)
334+
{
335+
auto const &called_function_pointer =
336+
to_dereference_expr(instruction.call_function()).pointer();
337+
pointer_name =
338+
id2string(to_symbol_expr(called_function_pointer).get_identifier());
339+
found = true;
340+
break;
341+
}
342+
}
343+
}
344+
if(!found)
345+
{
346+
throw invalid_restriction_exceptiont{
347+
"non-existent pointer name " + pointer_name,
348+
"pointers should be identifiers or <function_name>.<label>"};
349+
}
350+
351+
return pointer_name;
352+
}
353+
294354
function_pointer_restrictionst::restrictiont
295355
function_pointer_restrictionst::parse_function_pointer_restriction(
296356
const std::string &restriction_opt,
@@ -324,51 +384,8 @@ function_pointer_restrictionst::parse_function_pointer_restriction(
324384
"couldn't find target name before '/' in `" + restriction_opt + "'"};
325385
}
326386

327-
auto pointer_name = restriction_opt.substr(0, pointer_name_end);
328-
const auto last_dot = pointer_name.rfind('.');
329-
if(
330-
last_dot != std::string::npos && last_dot + 1 != pointer_name.size() &&
331-
!isdigit(pointer_name[last_dot + 1]))
332-
{
333-
const auto function_id = pointer_name.substr(0, last_dot);
334-
const auto label = pointer_name.substr(last_dot + 1);
335-
336-
bool found = false;
337-
const auto it = goto_model.goto_functions.function_map.find(function_id);
338-
if(it != goto_model.goto_functions.function_map.end())
339-
{
340-
optionalt<source_locationt> location;
341-
for(const auto &instruction : it->second.body.instructions)
342-
{
343-
if(
344-
std::find(
345-
instruction.labels.begin(), instruction.labels.end(), label) !=
346-
instruction.labels.end())
347-
{
348-
location = instruction.source_location();
349-
}
350-
351-
if(
352-
instruction.is_function_call() &&
353-
instruction.call_function().id() == ID_dereference &&
354-
location.has_value() && instruction.source_location() == *location)
355-
{
356-
auto const &called_function_pointer =
357-
to_dereference_expr(instruction.call_function()).pointer();
358-
pointer_name =
359-
id2string(to_symbol_expr(called_function_pointer).get_identifier());
360-
found = true;
361-
break;
362-
}
363-
}
364-
}
365-
if(!found)
366-
{
367-
throw invalid_restriction_exceptiont{"non-existent pointer name " +
368-
pointer_name,
369-
restriction_format_message};
370-
}
371-
}
387+
std::string pointer_name = resolve_pointer_name(
388+
restriction_opt.substr(0, pointer_name_end), goto_model);
372389

373390
auto const target_names_substring =
374391
restriction_opt.substr(pointer_name_end + 1);

src/goto-programs/restrict_function_pointers.h

Lines changed: 13 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -64,6 +64,19 @@ void parse_function_pointer_restriction_options_from_cmdline(
6464
const cmdlinet &cmdline,
6565
optionst &options);
6666

67+
class invalid_restriction_exceptiont : public cprover_exception_baset
68+
{
69+
public:
70+
explicit invalid_restriction_exceptiont(
71+
std::string reason,
72+
std::string correct_format = "");
73+
74+
std::string what() const override;
75+
76+
std::string reason;
77+
std::string correct_format;
78+
};
79+
6780
class function_pointer_restrictionst
6881
{
6982
public:
@@ -89,19 +102,6 @@ class function_pointer_restrictionst
89102
void write_to_file(const std::string &filename) const;
90103

91104
protected:
92-
class invalid_restriction_exceptiont : public cprover_exception_baset
93-
{
94-
public:
95-
explicit invalid_restriction_exceptiont(
96-
std::string reason,
97-
std::string correct_format = "");
98-
99-
std::string what() const override;
100-
101-
std::string reason;
102-
std::string correct_format;
103-
};
104-
105105
static void typecheck_function_pointer_restrictions(
106106
const goto_modelt &goto_model,
107107
const restrictionst &restrictions);

unit/goto-programs/restrict_function_pointers.cpp

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -46,32 +46,32 @@ void restriction_parsing_test()
4646
REQUIRE_THROWS_AS(
4747
fp_restrictionst::parse_function_pointer_restriction(
4848
"func", "test", goto_model),
49-
fp_restrictionst::invalid_restriction_exceptiont);
49+
invalid_restriction_exceptiont);
5050

5151
REQUIRE_THROWS_AS(
5252
fp_restrictionst::parse_function_pointer_restriction(
5353
"/func", "test", goto_model),
54-
fp_restrictionst::invalid_restriction_exceptiont);
54+
invalid_restriction_exceptiont);
5555

5656
REQUIRE_THROWS_AS(
5757
fp_restrictionst::parse_function_pointer_restriction(
5858
"func/", "test", goto_model),
59-
fp_restrictionst::invalid_restriction_exceptiont);
59+
invalid_restriction_exceptiont);
6060

6161
REQUIRE_THROWS_AS(
6262
fp_restrictionst::parse_function_pointer_restriction(
6363
"func/,", "test", goto_model),
64-
fp_restrictionst::invalid_restriction_exceptiont);
64+
invalid_restriction_exceptiont);
6565

6666
REQUIRE_THROWS_AS(
6767
fp_restrictionst::parse_function_pointer_restriction(
6868
"func1/func2,", "test", goto_model),
69-
fp_restrictionst::invalid_restriction_exceptiont);
69+
invalid_restriction_exceptiont);
7070

7171
REQUIRE_THROWS_AS(
7272
fp_restrictionst::parse_function_pointer_restriction(
7373
"func1/,func2", "test", goto_model),
74-
fp_restrictionst::invalid_restriction_exceptiont);
74+
invalid_restriction_exceptiont);
7575
}
7676

7777
void merge_restrictions_test()

0 commit comments

Comments
 (0)