Function pointer removal: create fall-back function call #6987

tautschnig · 2022-07-01T10:47:31Z

The case where a function pointer matches none of the candidate
functions now introduces a call to a new function. No implementation of
this function is provided, leaving the choice to the user in case they
choose to use goto-instrument's generate-function-body.

As doing so requires updates to goto_functions by the caller, two unused
API variants of remove_function_pointers were removed.

Fixes: #6983

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.

The case where a function pointer matches none of the candidate functions now introduces a call to a new function. No implementation of this function is provided, leaving the choice to the user in case they choose to use goto-instrument's generate-function-body. As doing so requires updates to goto_functions by the caller, two unused API variants of remove_function_pointers were removed. Fixes: diffblue#6983

codecov · 2022-07-05T18:30:15Z

Codecov Report

Merging #6987 (36edcfe) into develop (09e1041) will increase coverage by 0.01%.
The diff coverage is 92.95%.

@@             Coverage Diff             @@
##           develop    #6987      +/-   ##
===========================================
+ Coverage    77.81%   77.83%   +0.01%     
===========================================
  Files         1570     1569       -1     
  Lines       180682   180586      -96     
===========================================
- Hits        140601   140552      -49     
+ Misses       40081    40034      -47

Impacted Files	Coverage Δ
src/linking/linking.cpp	`59.36% <68.96%> (+0.65%)`	⬆️
src/goto-programs/restrict_function_pointers.cpp	`81.46% <92.30%> (+0.79%)`	⬆️
src/analyses/does_remove_const.cpp	`100.00% <100.00%> (ø)`
src/crangler/mini_c_parser.cpp	`72.58% <100.00%> (+1.55%)`	⬆️
src/goto-instrument/replace_calls.cpp	`89.70% <100.00%> (-0.15%)`	⬇️
src/goto-instrument/value_set_fi_fp_removal.cpp	`100.00% <100.00%> (ø)`
src/goto-programs/goto_program.cpp	`81.80% <100.00%> (ø)`
src/goto-programs/remove_function_pointers.cpp	`94.80% <100.00%> (+2.01%)`	⬆️
...nalyses/does_remove_const/does_expr_lose_const.cpp	`100.00% <100.00%> (ø)`
...ove_const/does_type_preserve_const_correctness.cpp	`100.00% <100.00%> (ø)`
... and 8 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 365871d...36edcfe. Read the comment docs.

martin-cs · 2022-08-14T19:47:37Z

Sorry to be That Person but can you split up the commit a bit? Maybe remove the unused APIs in a separate commit? The regression test clean ups might also be able to be separated?

celinval · 2022-09-01T19:35:11Z

Hi, I was wondering what's the status of this change: @tautschnig?

martin-cs

I'm a little unsure about the test cases. Something just feels a little bit off with the status changes. I'm not going to block this but it'd be really good if you could look at what is going on with them.

martin-cs · 2022-09-02T13:07:40Z

regression/cbmc/Function_Pointer18/test.desc

-\[main.assertion.1\] line [0-9]+ assertion x == 1: SUCCESS
+^\*\*\*\* WARNING: no body for function main::fptr_call
+^\*\*\*\* WARNING: no body for function main::fptr_call\$0
+\[f2.assertion.1\] line [0-9]+ assertion 0: FAILURE


Why is this now a failure? If I have read the right test case, there is no way f can be set to f2, so the assert in f2 cannot be reachable?

martin-cs · 2022-09-02T13:08:04Z

regression/cbmc/Function_Pointer18/test.desc

+^\*\*\*\* WARNING: no body for function main::fptr_call
+^\*\*\*\* WARNING: no body for function main::fptr_call\$0
+\[f2.assertion.1\] line [0-9]+ assertion 0: FAILURE
+\[main.assertion.1\] line [0-9]+ assertion x == 1: FAILURE


This also doesn't make sense, why does one of these fail but not the other?

martin-cs · 2022-09-02T13:10:48Z

regression/cbmc/Function_Pointer20/test.desc

+CORE
+main.c
+
+^\*\*\*\* WARNING: no body for function indirect::fptr_call


I don't get why there is a warning in this context? There is only a single thing that fn_ptr can point to?

martin-cs · 2022-09-02T13:12:10Z

regression/cbmc/Function_Pointer_Init_No_Candidate/main.c

@@ -4,9 +4,7 @@ typedef int (*other_function_type)(int n);

 void foo(other_function_type other_function)
 {
-  // returning from the function call is unreachable -> the following assertion
-  //   should succeed


So there is a semantic change for cases where function pointers are invalid / NULL / otherwise not properly defined?

martin-cs · 2022-09-02T13:17:14Z

regression/goto-analyzer/value-set-function-pointers-simple/test.desc

@@ -10,7 +10,7 @@ main.c
 ^main::1::fun1 \(\) -> value-set-begin: ptr ->\(f\) :value-set-end
 ^main::1::fun2_show \(\) -> value-set-begin: ptr ->\(f\), ptr ->\(g\) :value-set-end
 ^main::1::fun3_show \(\) -> value-set-begin: ptr ->\(f\), ptr ->\(g\) :value-set-end
-^fun_global_show \(\) -> value-set-begin: ptr ->\(f\), ptr ->\(g\) :value-set-end
+^fun_global_show \(\) -> value-set-begin: TOP :value-set-end


Looking at the test case this is slightly concerning as {f, g} is a legit and reasonable thing for it to be and it should only be set to TOP if something really wrong is occurring. This looks like we might need to be a bit careful about how this PR interacts with the abstract interpreter.

martin-cs · 2022-09-02T13:17:28Z

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

@@ -5,6 +5,7 @@ test.c
 ^SIGNAL=0$
 ^file test.c line 20 function main: replacing function pointer by 2 possible targets$
 --
+--


kroening

As mentioned out of band, I am unhappy with this PR as we are giving meaning to undefined behavior. Undefined behavior needs to stay that.

tautschnig · 2022-10-08T10:42:10Z

Closing as #7011 provided a solution without (potentially) giving meaning to undefined behaviour.

tautschnig requested review from martin-cs and chris-ryder as code owners July 1, 2022 10:47

tautschnig assigned kroening Jul 1, 2022

tautschnig requested review from peterschrammel and kroening as code owners July 1, 2022 10:47

tautschnig assigned peterschrammel, martin-cs and chris-ryder Jul 1, 2022

tautschnig mentioned this pull request Jul 1, 2022

CBMC aborts path exploration when it cannot resolve a function pointer #6983

Closed

tautschnig force-pushed the bugfixes/6983-function-pointer branch 5 times, most recently from 8c9b603 to 08c661f Compare July 5, 2022 13:27

tautschnig force-pushed the bugfixes/6983-function-pointer branch from 08c661f to 36edcfe Compare July 5, 2022 17:06

jimgrundy added aws Bugs or features of importance to AWS CBMC users aws-high labels Aug 24, 2022

peterschrammel approved these changes Aug 25, 2022

View reviewed changes

peterschrammel removed their assignment Aug 25, 2022

celinval mentioned this pull request Sep 1, 2022

Create RFC for MIR linker model-checking/kani#1600

Merged

4 tasks

tautschnig self-assigned this Sep 2, 2022

martin-cs reviewed Sep 2, 2022

View reviewed changes

kroening requested changes Sep 2, 2022

View reviewed changes

tautschnig unassigned martin-cs and chris-ryder Sep 29, 2022

tautschnig closed this Oct 8, 2022

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Function pointer removal: create fall-back function call #6987

Function pointer removal: create fall-back function call #6987

tautschnig commented Jul 1, 2022

codecov bot commented Jul 5, 2022

martin-cs commented Aug 14, 2022

celinval commented Sep 1, 2022

martin-cs left a comment

martin-cs Sep 2, 2022

martin-cs Sep 2, 2022

martin-cs Sep 2, 2022

martin-cs Sep 2, 2022

martin-cs Sep 2, 2022

martin-cs Sep 2, 2022

kroening left a comment

tautschnig commented Oct 8, 2022

Function pointer removal: create fall-back function call #6987

Function pointer removal: create fall-back function call #6987

Conversation

tautschnig commented Jul 1, 2022

codecov bot commented Jul 5, 2022

Codecov Report

martin-cs commented Aug 14, 2022

celinval commented Sep 1, 2022

martin-cs left a comment

Choose a reason for hiding this comment

martin-cs Sep 2, 2022

Choose a reason for hiding this comment

martin-cs Sep 2, 2022

Choose a reason for hiding this comment

martin-cs Sep 2, 2022

Choose a reason for hiding this comment

martin-cs Sep 2, 2022

Choose a reason for hiding this comment

martin-cs Sep 2, 2022

Choose a reason for hiding this comment

martin-cs Sep 2, 2022

Choose a reason for hiding this comment

kroening left a comment

Choose a reason for hiding this comment

tautschnig commented Oct 8, 2022