Restrict function pointers by name #5262

danpoe · 2020-03-07T19:47:47Z

Replaces #5174.

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-09T14:11:48Z

src/goto-programs/restrict_function_pointers.cpp

        restriction_format_message};
    }
    if(pointer_name_end == 0)
    {
      throw invalid_command_line_argument_exceptiont{
        "couldn't find target name before '/' in `" + restriction_opt + "'",
-        "--" RESTRICT_FUNCTION_POINTER_OPT};
+        option_name};


🚫 option

hannes-steffenhagen-diffblue · 2020-03-09T14:23:08Z

src/goto-programs/restrict_function_pointers.cpp

@@ -328,22 +349,83 @@ parse_function_pointer_restrictions_from_file(
  }
  return merged_restrictions;
 }
+
+function_pointer_restrictionst::restrictionst


The purpose of this needs to be documented, I am fairly sure I wrote this and it took me like 5 minutes trying to figure out what this was doing and why

thk123

Will review tests after lunch.

Note to other reviews: it is easier to review all at once rather than by commit

src/goto-instrument/goto_instrument_parse_options.cpp

src/goto-programs/restrict_function_pointers.cpp

src/goto-instrument/goto_instrument_parse_options.cpp

src/goto-programs/restrict_function_pointers.cpp

thk123

🚫 need a test that assigns a fp on a line a few lines before the call

regression/goto-instrument/restrict-function-pointer-by-name-global/test.c

thk123 · 2020-03-19T14:17:30Z

regression/goto-instrument/restrict-function-pointer-by-name-local/test.c

+
+void main()
+{
+  fp_t fp = f;


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

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

 }

-fptr_t get_f(void)


I guess all this deletion would be clearer if put in its own commit explaining why

regression/goto-instrument/restrict-function-pointer-by-name-local/test.desc

unit/goto-programs/restrict_function_pointers.cpp

This works similar to restrict-function-pointer, but for names of individual function pointer variables (globals, locals, parameters) rather than call sites. This isn't applicable to all situations (for example, calling function pointers in structs or function pointers returned from functions), but is more readily applicable to some common use scenarios (e.g. global function pointers loaded at start time like in OpenGL).

danpoe · 2020-03-24T12:34:47Z

@thk123 A test that assigns a function pointer a few lines before the call is not necessary. The reason we look for those assignments is because the label_function_pointer_calls pass inserts them, and it always does so immediately before the call. (I've also removed the loops that search for these assignments and replaced them by a check of just the previous instruction)

thk123 · 2020-03-24T15:52:36Z

src/goto-programs/restrict_function_pointers.cpp

+  if(!can_cast_expr<dereference_exprt>(function))
+    return {};
+
+  auto const &function_pointer_call_site = to_symbol_expr(


💡 Even a comment here:

// function pointer guarateed to be a symbol by the function-pointer-label pass

Where function-pointer-label should be an actual file/folder/function that can be searched for!

unit/goto-programs/restrict_function_pointers.cpp

thk123

Looks good from a code perspective.

Call me a Luddite, but even knowing the code doesn't rely on an assignment from a few lines before, I think it would be good to add the test, since not obvious to me that this is true.

I also would feel better about the test without it having distinct regexes so we know it remains doing something

Other than that, lgtm 👍 thanks for addressing comments

smowton

Only reviewed the main changed, not the tests

…eature

- remove unnecessary loop - make it return the restriction instead of inserting it into the map

thk123

Dan pointed out that all the tests that don't have a local variable are testing what I was referring to.

codecov-io · 2020-03-24T18:22:51Z

Codecov Report

Merging #5262 into develop will decrease coverage by 35.74%.
The diff coverage is 35.86%.

@@             Coverage Diff              @@
##           develop    #5262       +/-   ##
============================================
- Coverage    67.50%   31.76%   -35.75%     
============================================
  Files         1170      918      -252     
  Lines        96287    80144    -16143     
============================================
- Hits         65003    25460    -39543     
- Misses       31284    54684    +23400

Flag	Coverage Δ
#cproversmt2	`?`
#regression	`?`
#unit	`31.76% <35.86%> (+0.02%)`	⬆️

Impacted Files	Coverage Δ
src/goto-programs/restrict_function_pointers.cpp	`39.10% <35.16%> (-42.31%)`	⬇️
src/goto-programs/restrict_function_pointers.h	`100.00% <100.00%> (ø)`
src/cpp/cpp_id.h	`0.00% <0.00%> (-100.00%)`	⬇️
src/cpp/cpp_scope.h	`0.00% <0.00%> (-100.00%)`	⬇️
src/cpp/cpp_token.h	`0.00% <0.00%> (-100.00%)`	⬇️
src/cpp/cpp_name.cpp	`0.00% <0.00%> (-100.00%)`	⬇️
src/cpp/cpp_util.cpp	`0.00% <0.00%> (-100.00%)`	⬇️
src/util/identifier.h	`0.00% <0.00%> (-100.00%)`	⬇️
src/xmllang/graphml.h	`0.00% <0.00%> (-100.00%)`	⬇️
src/cpp/cpp_is_pod.cpp	`0.00% <0.00%> (-100.00%)`	⬇️
... and 890 more

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 094fc97...3528195. 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 7, 2020 19:47

danpoe changed the title ~~Restrict function pointer by name feature~~ Restrict function pointer by name feature [depends-on: #5257] Mar 7, 2020

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

danpoe changed the title ~~Restrict function pointer by name feature [depends-on: #5257]~~ Restrict function pointers by name [depends-on: #5257] Mar 7, 2020

danpoe force-pushed the feature/restrict-function-pointer-by-name branch from 0c1597e to 354cb01 Compare March 7, 2020 19:56

hannes-steffenhagen-diffblue reviewed Mar 9, 2020

View reviewed changes

danpoe force-pushed the feature/restrict-function-pointer-by-name branch from 354cb01 to f55f636 Compare March 16, 2020 16:08

danpoe changed the title ~~Restrict function pointers by name [depends-on: #5257]~~ Restrict function pointers by name Mar 16, 2020

danpoe force-pushed the feature/restrict-function-pointer-by-name branch 4 times, most recently from 49f01cc to 4677cf6 Compare March 18, 2020 19:02

thk123 reviewed Mar 19, 2020

View reviewed changes

hannes-steffenhagen-diffblue and others added 2 commits March 23, 2020 10:40

Pass command line option to parse_function_pointer_restriction()

19040a4

danpoe force-pushed the feature/restrict-function-pointer-by-name branch 4 times, most recently from 9262c73 to cbffdd8 Compare March 23, 2020 17:02

danpoe force-pushed the feature/restrict-function-pointer-by-name branch from cbffdd8 to c8ecc1a Compare March 24, 2020 15:51

thk123 reviewed Mar 24, 2020

View reviewed changes

smowton approved these changes Mar 24, 2020

View reviewed changes

danpoe force-pushed the feature/restrict-function-pointer-by-name branch from c8ecc1a to 8c64c36 Compare March 24, 2020 16:54

danpoe added 2 commits March 24, 2020 16:56

Refactorings and cleanups for the restrict function pointer by name f…

84054d5

…eature

Update restrict function pointer by name regression tests

0e659f9

danpoe force-pushed the feature/restrict-function-pointer-by-name branch from 8c64c36 to 9545831 Compare March 24, 2020 17:06

Add unit tests for the restrict function pointers by name feature

0744710

danpoe force-pushed the feature/restrict-function-pointer-by-name branch from 9545831 to 677442a Compare March 24, 2020 17:16

Refactor get_by_name_restriction()

9917b20

- remove unnecessary loop - make it return the restriction instead of inserting it into the map

danpoe force-pushed the feature/restrict-function-pointer-by-name branch from 677442a to 3528195 Compare March 24, 2020 17:59

thk123 approved these changes Mar 24, 2020

View reviewed changes

danpoe force-pushed the feature/restrict-function-pointer-by-name branch from 3528195 to 8154f23 Compare March 24, 2020 19:30

Refactor error handling of function pointer restriction

8154f23

danpoe merged commit 7e27cb2 into diffblue:develop Mar 24, 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-pointer-by-name branch June 2, 2020 17:06

		}

		fptr_t get_f(void)

Restrict function pointers by name #5262

Restrict function pointers by name #5262

Uh oh!

Conversation

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

Uh oh!

Uh oh!

hannes-steffenhagen-diffblue Mar 9, 2020

Choose a reason for hiding this comment

Uh oh!

hannes-steffenhagen-diffblue Mar 9, 2020

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!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

thk123 left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

thk123 Mar 19, 2020

Choose a reason for hiding this comment

Uh oh!

thk123 Mar 19, 2020

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

danpoe commented Mar 24, 2020

Uh oh!

thk123 Mar 24, 2020

Choose a reason for hiding this comment

Uh oh!

Uh oh!

thk123 left a comment

Choose a reason for hiding this comment

Uh oh!

smowton left a comment

Choose a reason for hiding this comment

Uh oh!

thk123 left a comment

Choose a reason for hiding this comment

Uh oh!

codecov-io commented Mar 24, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

Uh oh!

danpoe commented Mar 7, 2020 •

edited

Loading

codecov-io commented Mar 24, 2020 •

edited

Loading