Library functions: mark them as compiled #8412
Conversation
tautschnig
requested review from
feliperodri,
remi-delmas-3000,
kroening and
peterschrammel
as code owners
tautschnig
assigned
tautschnig and unassigned
kroening,
remi-delmas-3000,
peterschrammel and
feliperodri
|
This PR makes a huge usability improvement in terms of reducing noise in the output of CBMC. As a user, I like this lots. |
tautschnig
force-pushed
the
library-is-compiled
branch
3 times, most recently
from
d9e83d4 to
1e687f6
Compare
Codecov ReportAttention: Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## develop #8412 +/- ##
===========================================
- Coverage 77.95% 77.93% -0.03%
===========================================
Files 1726 1726
Lines 189601 189668 +67
Branches 18250 18234 -16
===========================================
+ Hits 147796 147810 +14
- Misses 41805 41858 +53 ☔ View full report in Codecov by Sentry. |
| { | ||
| goto_convert( | ||
| missing_function, | ||
| goto_model.symbol_table, | ||
| library_model.goto_functions, | ||
| message_handler); | ||
| goto_model.symbol_table.get_writeable_ref(missing_function).set_compiled(); |
There was a problem hiding this comment.
Any intuition why our regression tests don't cover this line?
There was a problem hiding this comment.
This case would only apply when system headers ship functions marked inline. I believe we run into this on FreeBSD, but seemingly not on Linux (which is the only platform we do coverage recording on).
When adding library functions to the goto model we no longer need their function bodies as values in the symbol table. Marking them as "compiled" will make sure we don't re-convert them in any subsequent run (e.g., running cbmc after goto-instrument). Doing so would undo any application of "drop-unused-functions." This was most notable with contracts/dynamic frames, where we ended up reporting thousands of properties as "SUCCESS" in library functions that were never actually called. For some contracts examples this now reduces the number of properties reported from over a thousand to tens of properties, and in other cases this made apparent that we were spuriously reporting "SUCCESS" when we never actually invoked those functions in the first place.
tautschnig
force-pushed
the
library-is-compiled
branch
from
1e687f6 to
b42ac11
Compare
| @@ -41,5 +41,8 @@ elif echo $args_inst | grep -q -- "--dump-c" ; then | |||
|
|
|||
| rm "${name}-mod.c" | |||
| fi | |||
| if ! echo "${args_cbmc}" | grep -q -- --function ; then | |||
| $goto_instrument --drop-unused-functions "${name}-mod.gb" "${name}-mod.gb" | |||
There was a problem hiding this comment.
Should --drop-unused-functions become the default when running goto-instrument with contracts ?
When adding library functions to the goto model we no longer need their function bodies as values in the symbol table. Marking them as "compiled" will make sure we don't re-convert them in any subsequent run (e.g., running cbmc after goto-instrument). Doing so would undo any application of "drop-unused-functions." This was most notable with contracts/dynamic frames, where we ended up reporting thousands of properties as "SUCCESS" in library functions that were never actually called. For some contracts examples this now reduces the number of properties reported from over a thousand to tens of properties.