goto-instrument: function pointer removal with value_set_fi #5436

polgreen · 2020-07-29T18:46:40Z

This adds a new option to goto-instrument for removing function pointers.
The points-to analysis is done using flow-insensitive value sets, which is
more precise than using the signature of the function to identify the
points-to set.

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
[n/a] My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
[n/a ] White-space or formatting changes outside the feature-related changed lines are in commits of their own.

regression/goto-instrument/value-set-fi-fp-removal/test.c

codecov · 2020-08-10T04:01:17Z

Codecov Report

Merging #5436 into develop will increase coverage by 0.05%.
The diff coverage is 87.95%.

@@             Coverage Diff             @@
##           develop    #5436      +/-   ##
===========================================
+ Coverage    68.25%   68.30%   +0.05%     
===========================================
  Files         1180     1181       +1     
  Lines        97722    97814      +92     
===========================================
+ Hits         66698    66811     +113     
+ Misses       31024    31003      -21

Flag	Coverage Δ
#cproversmt2	`42.81% <ø> (ø)`
#regression	`65.48% <87.95%> (+0.05%)`	⬆️
#unit	`32.23% <ø> (ø)`

Flags with carried forward coverage won't be shown. Click here to find out more.

Impacted Files	Coverage Δ
...rc/goto-instrument/goto_instrument_parse_options.h	`100.00% <ø> (ø)`
src/goto-instrument/value_set_fi_fp_removal.cpp	`87.50% <87.50%> (ø)`
.../goto-instrument/goto_instrument_parse_options.cpp	`58.65% <100.00%> (+0.17%)`	⬆️
src/goto-programs/goto_program.h	`92.23% <0.00%> (+0.35%)`	⬆️
src/pointer-analysis/value_set_fi.cpp	`63.49% <0.00%> (+2.21%)`	⬆️
src/analyses/flow_insensitive_analysis.h	`59.09% <0.00%> (+9.09%)`	⬆️
src/analyses/flow_insensitive_analysis.cpp	`71.42% <0.00%> (+10.20%)`	⬆️
src/pointer-analysis/value_set_domain_fi.h	`28.57% <0.00%> (+14.28%)`	⬆️
src/pointer-analysis/value_set_analysis_fi.h	`100.00% <0.00%> (+72.72%)`	⬆️

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update a6feed2...2960187. Read the comment docs.

polgreen · 2020-08-13T16:01:07Z

I think this is now ready to merge, is anyone available to review it?

smowton · 2020-08-14T09:23:50Z

I'll get to this this weekend

polgreen · 2020-08-17T16:12:48Z

Is anyone free to review this please?

martin-cs · 2020-08-17T16:16:27Z

@polgreen sorry for the lag, will try to look tomorrow.

src/goto-instrument/goto_instrument_parse_options.cpp

src/goto-instrument/value_set_fi_fp_removal.cpp

src/goto-instrument/goto_instrument_parse_options.cpp

src/goto-instrument/goto_instrument_parse_options.h

src/goto-instrument/value_set_fi_fp_removal.cpp

polgreen · 2020-08-20T16:11:04Z

I think all changes requested are now made

hannes-steffenhagen-diffblue · 2020-08-13T15:01:34Z

src/goto-instrument/value_set_fi_fp_removal.cpp

+#include <util/std_code.h>
+#include <util/union_find.h>
+
+#ifdef USE_STD_STRING


Not quite sure what this is for?

Needed for one of the CI tests, which compiles with this flag and needs this include to compile

hannes-steffenhagen-diffblue · 2020-08-13T15:02:10Z

src/goto-instrument/value_set_fi_fp_removal.cpp

+
+void value_set_fi_fp_removal(goto_modelt &goto_model)
+{
+  std::cout << "Doing FI value set analysis\n";


Should take a messaget and use that instead I’d think?

that's outdated, it's changed in the latest commit

hannes-steffenhagen-diffblue · 2020-08-13T15:04:32Z

src/goto-instrument/value_set_fi_fp_removal.cpp

+  new_code.destructive_append(final_skip);
+
+  // set locations
+  Forall_goto_program_instructions(it, new_code)


This could be done without macros:

for(auto const &instruction : new_code.instructions)

Would need to drop the const in that.

Are the macros now deprecated? Because couldn't everything that is written using the macro also be written without?

They have been deprecated for some time now in favour of the new-style for loops. As to why...

martin-cs · 2020-08-21T15:37:02Z

@polgreen I will review next.

martin-cs · 2020-08-21T15:38:16Z

regression/goto-instrument/value-set-fi-fp-removal/test.desc

+^SIGNAL=0$
+^  function: f$
+--
+^  function: g$


Negative as well as positive tests are good.

martin-cs

I have Opinions on how function pointer removal should be done but I will spare you those. I think this is a step in the right direction. Thank you especially for the detailed test cases.

regression/goto-instrument/value-set-fi-fp-removal4/test.c

martin-cs · 2020-08-21T15:41:27Z

regression/goto-instrument/value-set-fi-fp-removal5/test.c

+int main(void)
+{
+  fp_t fp;
+  fp();


Again, anything that happens after this seems a bit dubious to me.

i've flipped the order of the delcarations now

regression/goto-instrument/value-set-fi-fp-removal5/test.c

martin-cs · 2020-08-21T15:46:09Z

src/goto-instrument/value_set_fi_fp_removal.cpp

+  new_code.destructive_append(final_skip);
+
+  // set locations
+  Forall_goto_program_instructions(it, new_code)


They have been deprecated for some time now in favour of the new-style for loops. As to why...

martin-cs · 2020-08-21T15:46:35Z

src/goto-instrument/value_set_fi_fp_removal.cpp

+    code_assignt(old_lhs, typecast_exprt(tmp_symbol_expr, old_lhs.type()))));
+}
+
+void remove_function_pointer(


It is good to see this bit of functionality broken out.

If the macros are deprecated, perhaps they should be marked as deprecated in the goto_program.h?

There was a move to simply replace them all in one go which would have basically caused a number of forks, I think the compromise was the linter would flag them in new code and they would be deprecated 'at some point'. I guess the linter doesn't so... yeah, yeah it would be a good idea.

peterschrammel · 2020-08-21T16:04:17Z

src/pointer-analysis/value_set_fi.cpp

@@ -1197,6 +1197,9 @@ void value_set_fit::assign_rec(
  {
    const typet &type = to_index_expr(lhs).array().type();

+    if(type.id() != ID_array)


❓ This makes the second part of the condition in the data invariant below unreachable.

I've removed this from the PR

This adds a new option to goto-instrument for removing function pointers. The points-to analysis is done using flow-insensitive value sets, which is more precise than using the signature of the function to identify the points-to set. Co-authored-by: Elizabeth Polgreen [email protected]

polgreen · 2020-08-25T18:02:03Z

I've now addressed all of the comments in the reviews

martin-cs · 2020-08-25T18:10:28Z

Thanks @polgreen ! @peterschrammel and @hannes-steffenhagen-diffblue do you have further comments or can this be merged as it is?

polgreen requested review from chrisr-diffblue, danpoe, hannes-steffenhagen-diffblue, martin-cs, peterschrammel and smowton as code owners July 29, 2020 18:46

polgreen marked this pull request as draft July 29, 2020 18:46

polgreen force-pushed the value_set_fi_fp_removal branch 5 times, most recently from 3bb4f5c to d09b28c Compare August 2, 2020 01:08

hannes-steffenhagen-diffblue reviewed Aug 6, 2020

View reviewed changes

regression/goto-instrument/value-set-fi-fp-removal/test.c Show resolved Hide resolved

polgreen force-pushed the value_set_fi_fp_removal branch 4 times, most recently from 1e4db2b to 100d938 Compare August 10, 2020 03:38

polgreen marked this pull request as ready for review August 10, 2020 03:38

polgreen force-pushed the value_set_fi_fp_removal branch 5 times, most recently from e98cce3 to 443c0ea Compare August 10, 2020 23:21

polgreen requested a review from hannes-steffenhagen-diffblue August 11, 2020 20:15

polgreen force-pushed the value_set_fi_fp_removal branch 4 times, most recently from 8645143 to afdffc7 Compare August 14, 2020 02:29

smowton reviewed Aug 17, 2020

View reviewed changes

polgreen force-pushed the value_set_fi_fp_removal branch from afdffc7 to f0d68fc Compare August 19, 2020 03:36

smowton reviewed Aug 19, 2020

View reviewed changes

src/goto-instrument/goto_instrument_parse_options.cpp Outdated Show resolved Hide resolved

src/goto-instrument/goto_instrument_parse_options.h Outdated Show resolved Hide resolved

src/goto-instrument/value_set_fi_fp_removal.cpp Outdated Show resolved Hide resolved

polgreen force-pushed the value_set_fi_fp_removal branch 5 times, most recently from e379fbd to da91cea Compare August 19, 2020 18:58

hannes-steffenhagen-diffblue reviewed Aug 21, 2020

View reviewed changes

martin-cs reviewed Aug 21, 2020

View reviewed changes

polgreen requested a review from smowton August 21, 2020 15:46

martin-cs approved these changes Aug 21, 2020

View reviewed changes

peterschrammel reviewed Aug 21, 2020

View reviewed changes

smowton approved these changes Aug 21, 2020

View reviewed changes

polgreen force-pushed the value_set_fi_fp_removal branch from da91cea to 7486abb Compare August 24, 2020 23:56

polgreen requested review from kroening and tautschnig as code owners August 24, 2020 23:56

polgreen force-pushed the value_set_fi_fp_removal branch from 7486abb to 1c31179 Compare August 25, 2020 15:22

polgreen force-pushed the value_set_fi_fp_removal branch from 1c31179 to 2960187 Compare August 25, 2020 15:37

martin-cs merged commit 0740ac2 into diffblue:develop Aug 27, 2020

polgreen deleted the value_set_fi_fp_removal branch August 27, 2020 21:08

tautschnig mentioned this pull request Oct 10, 2022

More precise function pointer removal [depends-on: #2504] #2620

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

goto-instrument: function pointer removal with value_set_fi #5436

goto-instrument: function pointer removal with value_set_fi #5436

polgreen commented Jul 29, 2020 •

edited

Loading

codecov bot commented Aug 10, 2020 •

edited

Loading

polgreen commented Aug 13, 2020

smowton commented Aug 14, 2020

polgreen commented Aug 17, 2020

martin-cs commented Aug 17, 2020

polgreen commented Aug 20, 2020

hannes-steffenhagen-diffblue Aug 13, 2020

polgreen Aug 21, 2020 •

edited

Loading

hannes-steffenhagen-diffblue Aug 13, 2020

polgreen Aug 21, 2020

hannes-steffenhagen-diffblue Aug 13, 2020

polgreen Aug 21, 2020

martin-cs Aug 21, 2020

martin-cs commented Aug 21, 2020

martin-cs Aug 21, 2020

martin-cs left a comment

martin-cs Aug 21, 2020

polgreen Aug 25, 2020

martin-cs Aug 21, 2020

martin-cs Aug 21, 2020

polgreen Aug 21, 2020

martin-cs Aug 21, 2020

peterschrammel Aug 21, 2020

polgreen Aug 25, 2020

polgreen commented Aug 25, 2020

martin-cs commented Aug 25, 2020

goto-instrument: function pointer removal with value_set_fi #5436

goto-instrument: function pointer removal with value_set_fi #5436

Conversation

polgreen commented Jul 29, 2020 • edited Loading

codecov bot commented Aug 10, 2020 • edited Loading

Codecov Report

polgreen commented Aug 13, 2020

smowton commented Aug 14, 2020

polgreen commented Aug 17, 2020

martin-cs commented Aug 17, 2020

polgreen commented Aug 20, 2020

Choose a reason for hiding this comment

polgreen Aug 21, 2020 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

martin-cs commented Aug 21, 2020

Choose a reason for hiding this comment

martin-cs left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

polgreen commented Aug 25, 2020

martin-cs commented Aug 25, 2020

polgreen commented Jul 29, 2020 •

edited

Loading

codecov bot commented Aug 10, 2020 •

edited

Loading

polgreen Aug 21, 2020 •

edited

Loading