Add missing DECL and DEAD instructions in function pointer call site labelling #6535
Conversation
remi-delmas-3000
added
aws
remi-delmas-3000
requested review from
kroening and
peterschrammel
as code owners
There was a problem hiding this comment.
Since you touched this code, would you mind adding the following cleanup:
- The lambda inserting the symbol into the symbol table should also set
is_thread_localandis_file_localtotrue. - Instead of the repeated and long-winded
goto_model.symbol_table.lookup_refcould you please introduce anamespacet ns{goto_model.symbol_table}early on and replace thegoto_model.symbol_table.lookup_refbyns.lookup?
Also, would it be possible to include a test, for example by adding patterns to regression/goto-instrument/restrict-function-pointer-by-name-local/test.desc that check for the existence of the new DECL/DEAD instructions?
| /// | ||
| /// Turns: | ||
| /// ``` | ||
| /// ...->[a]->... | ||
| /// ^ | ||
| /// target | ||
| /// ``` | ||
| /// | ||
| /// Into: | ||
| /// ``` | ||
| /// ...->[i]->[a]->... | ||
| /// ^ | ||
| /// target | ||
| /// ``` | ||
| /// | ||
| /// So that jumps to `a` now jump to the newly inserted `i`. |
There was a problem hiding this comment.
Thank you! But then: would you mind putting this in a commit of its own?
| auto decl_instruction = | ||
| goto_programt::make_decl(new_function_pointer, source_location); | ||
| goto_function.second.body.insert_before_swap(it, decl_instruction); | ||
| it++; |
There was a problem hiding this comment.
Nit picking: ++it (which the compiler will likely take care of for you, but why rely on compiler optimisations...).
| it++; | ||
|
|
||
| // transform original call into a call to the new variable | ||
| to_code_function_call(it->code_nonconst()).function() = |
There was a problem hiding this comment.
it->call_function() = would be a shorter version thereof.
remi-delmas-3000
force-pushed
the
function-pointer-call-site-add-decl-dead
branch
from
52311df to
bd9372b
Compare
…ites. Previously, function pointer call site labelling introduced ASSIGNS and CALL instructions to a fresh function pointer variable in the goto program without adding corresponding DECL and DEAD instructions which made them look like global variables when they really are local to the function.
… illustrate "preserves jumps to target".
remi-delmas-3000
force-pushed
the
function-pointer-call-site-add-decl-dead
branch
from
bd9372b to
6642254
Compare
Codecov Report
@@ Coverage Diff @@
## develop #6535 +/- ##
========================================
Coverage 75.98% 75.99%
========================================
Files 1578 1578
Lines 180919 180944 +25
========================================
+ Hits 137476 137500 +24
- Misses 43443 43444 +1
Continue to review full report at Codecov.
|
No change in functionality or performance is expected.
Previously, function pointer call site labelling introduced ASSIGNS and CALL instructions to a fresh function pointer variable in the goto program without adding corresponding DECL and DEAD instructions, which made them look like global variables when they really are local to the function.
This caused problems with function contracts checking, because a function would appear to be writing to a global that is not mentioned in its assigns clause.
We also add a small diagram to document what it means for
goto_programt::insert_before_swapto preserve jumps to target.