Add function pointer restriction feature #5257

danpoe · 2020-03-04T16:54:43Z

Replaces #5168

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.

hannes-steffenhagen-diffblue · 2020-03-04T18:32:09Z

doc/cprover-manual/restrict-function-pointer.md

+
+### Motivation
+
+CBMC comes with a way to resolve calls to function pointers to direct function


The documentation needs to be updated to reference goto-instrument instead of cbmc (also usage examples need to be updated to emphasise that this is a two-four step process source →binary→instrument→cbmc

thk123

On the whole - I think this is a really good PR, lots of clear names, functions do what they say. It is easy to see how it all plugs together. Also a big fan of what seems to be some very robust user error handling 👍

Got a bunch of comments that basically come in two flavours:

lots of opportunities for unit tests which would give much greater confidence on the edge cases in the code and saves 10s of regression tests!
some large blocks of code that are quite intimidating to start reading that I think a few simple refactors could greatly improve readability

I haven't yet reviewed the regression tests or documentation, but thought I'd leave the code comments so you could begin incorporating the ones you agree with

src/goto-programs/label_function_pointer_call_sites.cpp

src/util/irep.h

thk123 · 2020-03-06T14:38:02Z

src/goto-programs/restrict_function_pointers.cpp

+              assume_false_location, goto_programt::make_skip());
+            for(auto const &restriction_target : restriction.second)
+            {
+              auto new_instruction = original_function_call_instruction;


💡 This definitively should be pulled out into a separate function, independently unit tested to get an idea of what goto code it produces.

Put this into a separate function. I think it is not necessary to add unit tests as this functionality is very well tested by the regression tests already.

thk123 · 2020-03-06T14:38:57Z

src/goto-programs/restrict_function_pointers.cpp

+}
+
+template <typename Handler>
+void for_each_function_call(goto_functiont &goto_function, Handler handler)


⛏️ I'd much prefer using the range framework rather than introducing these helper functions

I didn’t even know we had that in cbmc!

I would prefer those functions actually. Kept them.

src/goto-programs/restrict_function_pointers.cpp

thk123 · 2020-03-06T14:43:18Z

src/goto-programs/restrict_function_pointers.cpp

@@ -0,0 +1,415 @@
+/*******************************************************************\


This file is pretty big - I'd be tempted to split up the command line option parsing / error checking from the goto code transformation stuff

450 lines is still within reasonable bounds IMO

thk123

It is hard to see exactly what the tests are testing, I think a short sentence at the foot of each desc describing it's purpose, so appologies if there are tests for the following:

writing to a json file (I saw the code - not sure how it is to be used in this PR)
multiple distinct function pointer calls replaced
a function pointer call that isn't replaced
multiple calls to the same function pointer being replaced by different fps
parsing a mismatched type (though think we should test all of the error checks fully through unit tests - this would just be to check the validation code is indeed being used)

thk123 · 2020-03-06T14:58:20Z

regression/goto-instrument/restrict-function-pointer-to-complex-expression/test.desc

+\[use_fg.assertion.2\] line \d+ assertion \(choice \? fptr : gptr\)\(10\) == 10 \+ choice: SUCCESS
+\[use_fg.assertion.1\] line \d+ dereferenced function pointer at use_fg.function_pointer_call.1 must be one of \[(f|g), (f|g)\]: SUCCESS
+^EXIT=0$
+^SIGNAL=0$


🚫 Please add explanations for each test into the desc file

thk123 · 2020-03-06T15:01:36Z

doc/cprover-manual/restrict-function-pointer.md

+### Motivation
+
+The CPROVER framework includes a goto program transformation pass
+`remove_function_pointers()` to resolve calls to function pointers to direct
+function calls. The pass is needed by `cbmc`, as symbolic execution itself can't
+handle calls to function pointers. In practice, the transformation pass works as
+follows:


💡 this is kind of an impl detail - and as such I'd be tempted to bury it at the bottom of the docs

Will leave refactoring the documentation to the next PR as it changes some things.

thk123 · 2020-03-06T15:04:05Z

regression/goto-instrument/restrict-function-pointer-to-complex-expression/test.desc

@@ -0,0 +1,7 @@
+CORE
+test.c
+--restrict-function-pointer "use_fg.function_pointer_call.1/f,g"


❓ What is the point of function_pointer_call, why isn't the syntax just use_fg.1/f,g?
❓ Can I specify more all calls? e.g. use_fg/f,g for all calls inside use_fg?

This could be shortened, yes.

No, but something similar is in a follow up PR

Will defer 1 to the next PR.

regression/goto-instrument/restrict-function-pointer-to-complex-expression/test.c

regression/goto-instrument/restrict-function-pointer-to-multiple-functions-code-check/test.desc

.../restrict-function-pointer-to-multiple-functions-via-file-and-command-line-options/test.desc

hannes-steffenhagen-diffblue

Addressing some of Thomas’s comments.

hannes-steffenhagen-diffblue · 2020-03-09T10:29:26Z

regression/goto-instrument/restrict-function-pointer-to-complex-expression/test.desc

@@ -0,0 +1,7 @@
+CORE
+test.c
+--restrict-function-pointer "use_fg.function_pointer_call.1/f,g"


This could be shortened, yes.

No, but something similar is in a follow up PR

regression/goto-instrument/restrict-function-pointer-to-complex-expression/test.c

regression/goto-instrument/restrict-function-pointer-to-multiple-functions-code-check/test.desc

.../restrict-function-pointer-to-multiple-functions-via-file-and-command-line-options/test.desc

src/goto-programs/label_function_pointer_call_sites.cpp

src/goto-programs/restrict_function_pointers.cpp

hannes-steffenhagen-diffblue · 2020-03-09T10:41:23Z

src/goto-programs/restrict_function_pointers.cpp

+}
+
+template <typename Handler>
+void for_each_function_call(goto_functiont &goto_function, Handler handler)


I didn’t even know we had that in cbmc!

src/goto-programs/restrict_function_pointers.h

smowton · 2020-03-09T11:39:04Z

Looks like there's a ton of comments to look at-- let me know when this / its successor PR are in final-ish state and waiting on code owners?

smowton

Only skimmed the code, didn't review the docs or tests

smowton · 2020-03-13T16:12:08Z

src/goto-programs/label_function_pointer_call_sites.cpp

+          goto_model.symbol_table.lookup_ref(goto_function.first).mode;
+
+        auto const call_site_symbol_name =
+          irep_idt{id2string(goto_function.first) + ".function_pointer_call." +


May be best not to use . since it delimits members, and this isn't one ($ has been used elsewhere for a reserved character that doesn't mean anything in C)

Agreed. This will change in the next PR anyways so I'll leave this as is for now.

smowton · 2020-03-13T16:18:37Z

src/goto-programs/restrict_function_pointers.cpp

+
+    for_each_function_call(
+      goto_function,
+      std::bind(


This is one verbose way to write

[&](const goto_programt::targett &location) { handle_call(goto_function, goto_model, restrictions, location); }

This adds a new option, --restrict-function-pointer, to goto-instrument. This lets a user specify a list of possible pointer targets for specific function pointer call sites, rather than have remove_function_pointers guess possible values. The intended purpose behind this is to prevent excessive symex time wasted on exploring paths the user knows the program can never actually take.

Update to reflect that the feature is now a goto-instrument analysis

codecov-io · 2020-03-14T15:49:00Z

Codecov Report

Merging #5257 into develop will increase coverage by 0.03%.
The diff coverage is 85.2%.

@@             Coverage Diff             @@
##           develop    #5257      +/-   ##
===========================================
+ Coverage    67.46%   67.49%   +0.03%     
===========================================
  Files         1164     1167       +3     
  Lines        95850    96045     +195     
===========================================
+ Hits         64661    64827     +166     
- Misses       31189    31218      +29

Flag	Coverage Δ
#cproversmt2	`42.49% <ø> (ø)`	⬆️
#regression	`63.99% <78.46%> (+0.02%)`	⬆️
#unit	`31.79% <42.4%> (+0.09%)`	⬆️

Impacted Files	Coverage Δ
...rc/goto-instrument/goto_instrument_parse_options.h	`100% <ø> (ø)`	⬆️
src/goto-programs/goto_program.h	`91.87% <100%> (+0.16%)`	⬆️
...oto-programs/label_function_pointer_call_sites.cpp	`100% <100%> (ø)`
.../goto-instrument/goto_instrument_parse_options.cpp	`58.03% <100%> (+0.23%)`	⬆️
src/goto-programs/restrict_function_pointers.h	`100% <100%> (ø)`
src/goto-programs/restrict_function_pointers.cpp	`81.41% <81.41%> (ø)`

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 c7bb936...a694533. Read the comment docs.

danpoe requested review from chrisr-diffblue, hannes-steffenhagen-diffblue, kroening, martin-cs, peterschrammel, pkesseli, smowton and tautschnig as code owners March 4, 2020 16:54

danpoe added the aws Bugs or features of importance to AWS CBMC users label Mar 4, 2020

danpoe force-pushed the feature/restrict-function-pointers branch from ade1ce9 to 031dd8e Compare March 4, 2020 17:51

hannes-steffenhagen-diffblue reviewed Mar 4, 2020

View reviewed changes

thk123 reviewed Mar 6, 2020

View reviewed changes

danpoe mentioned this pull request Mar 7, 2020

Restrict function pointers by name #5262

Merged

5 tasks

hannes-steffenhagen-diffblue reviewed Mar 9, 2020

View reviewed changes

danpoe force-pushed the feature/restrict-function-pointers branch 5 times, most recently from 6a36eaa to 36ffcfd Compare March 12, 2020 17:55

Label function pointer call sites

ac1e482

danpoe force-pushed the feature/restrict-function-pointers branch 5 times, most recently from 4559d89 to 5285bb0 Compare March 13, 2020 16:02

smowton approved these changes Mar 13, 2020

View reviewed changes

danpoe force-pushed the feature/restrict-function-pointers branch 2 times, most recently from 37f059e to 2c4e416 Compare March 13, 2020 17:12

danpoe force-pushed the feature/restrict-function-pointers branch from 2c4e416 to a694533 Compare March 14, 2020 14:42

danpoe and others added 8 commits March 14, 2020 14:43

Add unit tests for label function pointer call sites

0efdb37

Add function pointer restriction regression tests

7e4cdd5

Add function pointer restriction documentation

2f16977

Update restrict function pointer documentation

69ef07a

Update to reflect that the feature is now a goto-instrument analysis

Refactor restrict function pointers regression tests

fede34a

Refactorings and cleanups for the function pointer restriction feature

aa4ed95

Add unit tests for restrict function pointers feature

a694533

danpoe merged commit f34e4f2 into diffblue:develop Mar 14, 2020

hannes-steffenhagen-diffblue mentioned this pull request Apr 23, 2020

Porting of the function pointer restriction feature to variable sensitivity domain branch. #5309

Merged

7 tasks

danpoe deleted the feature/restrict-function-pointers branch June 2, 2020 17:06


		### Motivation

		CBMC comes with a way to resolve calls to function pointers to direct function

		@@ -0,0 +1,415 @@
		/*******************************************************************\

Add function pointer restriction feature #5257

Add function pointer restriction feature #5257

Uh oh!

Conversation

danpoe commented Mar 4, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

thk123 left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

thk123 left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

danpoe Mar 13, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

hannes-steffenhagen-diffblue left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

smowton commented Mar 9, 2020

Uh oh!

smowton left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

danpoe commented Mar 4, 2020 •

edited

Loading

danpoe Mar 13, 2020 •

edited

Loading

codecov-io commented Mar 14, 2020 •

edited

Loading