New goto-instrument option: --print-global-state-size #2190
Conversation
tautschnig
requested review from
chrisr-diffblue,
kroening,
martin-cs,
peterschrammel and
smowton
as code owners
| } | ||
|
|
||
| const mp_integer bits = pointer_offset_bits(symbol.type, ns); | ||
| if(bits > 0) |
There was a problem hiding this comment.
It seems to me that if the total is too large, the next thing someone will ask is "what's taking up all of the space", so could we have, possibly at verbose or debug, something that prints out the size and the name?
There was a problem hiding this comment.
I did consider doing so, but now that's done in #2184 during symbolic execution.
| if(cmdline.isset("print-global-state-size")) | ||
| { | ||
| print_global_state_size(goto_model); | ||
| return CPROVER_EXIT_SUCCESS; |
There was a problem hiding this comment.
Probably a stupid question but what is the use-case for this? Is bits necessarily the most useful piece of information?
There was a problem hiding this comment.
A question that has come up is "what is the size of the state space?" (let's not discuss whether that is even a meaningful question). The output here does provide guidance: if the non-constant part of global variables is in the order of millions of bits you'll likely run into trouble (even when just a few instructions are to be executed).
There was a problem hiding this comment.
... this is true ... I wonder if we could give any more meaningful stats for the same effort / with the same code.
src/goto-instrument/count_eloc.cpp
Outdated
| if(ins.is_assign()) | ||
| { | ||
| const code_assignt &code_assign = to_code_assign(ins.code); | ||
| const symbol_exprt &symbol_expr = to_symbol_expr(code_assign.lhs()); |
There was a problem hiding this comment.
The LHS of an assign statement isn't always a symbol in __CPROVER_initialize -- for example, Java code will produce code such as global_init->fieldname = NONDET(int);.
There was a problem hiding this comment.
To that end you should probably add a couple of regression tests, or this will be vulnerable to moulding
There was a problem hiding this comment.
Both of the above comments are finally addressed.
tautschnig
assigned tautschnig and unassigned smowton, kroening, peterschrammel and chrisr-diffblue
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: d46a55c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/76792954
tautschnig
assigned smowton, kroening, peterschrammel and chrisr-diffblue and unassigned tautschnig
8a7893c Merge pull request diffblue#2375 from diffblue/unit-dependencies 9258284 fix build depenencies of unit test binary f7cd161 Merge pull request diffblue#2371 from diffblue/fix-tests2 82753bc make test independent of index type f5f32da Merge pull request diffblue#2364 from smowton/smowton/fix/autodetect-default-cxx-dialect d437f60 Merge pull request diffblue#2368 from polgreen/doc_replace_func_bodies 6048517 Merge pull request diffblue#2353 from tautschnig/g++8-fixes2 e2e6d82 Merge pull request diffblue#2190 from tautschnig/more-stats 7210136 Make it clearer that <=> will always be stringified 560f82b Travis: test more g++ and clang versions d46a55c Add new goto-instrument option print-global-state-size 961b29a Silence GCC 8's warning about using realloc/memmove on non-POD ca1b03c Documentation wording for replace function bodies d8c5a98 Cleanup options handling of count-eloc, list-eloc, print-path-lengths 6cd6d31 Unit test framwork: use references when catching exceptions 6882da6 Merge pull request diffblue#2367 from diffblue/fix-tests bcc3bef make regression/cbmc/bounds_check1 independent of types used 4de4538 switch regression/cbmc/Typecast2 to preprocessed code 91a9c64 Amend two tests that explicitly target C++98 2b2b797 goto-gcc: select default language standard depending on emulated compiler 52a8afc Merge pull request diffblue#1898 from tautschnig/always-inline cbe691b Merge pull request diffblue#2363 from diffblue/Makefile-TAR 9d40a9e Merge pull request diffblue#2365 from diffblue/solaris_errno 9efd705 add model for ___errno for Solaris 11 eaa2e05 update Solaris instructions 2f142d5 allow customizing the tar command for solver download 8cc1848 Merge pull request diffblue#1860 from tautschnig/restore-irept-sharing fea5db0 Merge pull request diffblue#2361 from diffblue/fix-goto2 7c0d750 Merge pull request diffblue#2362 from smowton/smowton/fix/tolerate-cxx-namespace-attribute e440a25 introduce INCOMPLETE_GOTO and turn guarded goto into a stateless pass 1f1835b C++ frontend: tolerate namespace attributes cbce4bc Unit test of irept's public API abdb044 Unit test to check that irept implements sharing d58fd18 Silence the linter on assert in irep.h 3d64070 Partially revert "Use small intrusive pointer in irep" 688a0ab Macros are not needed outside translation units 9c93f59 Fully interpret __attribute__((always_inline)) d1f617b Apply symbol replacement in type_arg members git-subtree-dir: cbmc git-subtree-split: 8a7893c
Also clean up option handling for all other count_eloc.{h,cpp} members.