Make signal handlers safer
authorAndres Notzli <andres.noetzli@gmail.com>
Fri, 31 Mar 2017 21:27:05 +0000 (14:27 -0700)
committerAndres Nötzli <andres.noetzli@gmail.com>
Fri, 12 May 2017 15:50:36 +0000 (08:50 -0700)
commit31681c7ff2a1469f5efc325fc1b3a406e3a85949
tree8a3a677f6520baf1429297d36c2e19518a7e545c
parentb045d1d06f2d28957ccca6ed7d9e6458b4a96b79
Make signal handlers safer

As reported in bug 769, the signal handlers currently use unsafe
functions such as dynamic memory allocations and fprintf. This commit
fixes the issue by introducing functions for printing statistics in
signal handlers (functions with the `safe` prefix). It also avoids
copying statistics, which further avoids dynamic memory allocation. The
safe printing of statistics has some limitations (it does not support
SExprStats or printing CVC4::Result), which should not matter much in
practice. Printing statistics in a non-signal handler is not affected by
these changes as that uses a separate code path (the functions without
the `safe` prefix).

Additional changes:
- Remove ListStat as it is not used anywhere
- Add unit test for safe printing statistics
15 files changed:
src/expr/expr_manager_template.cpp
src/expr/expr_manager_template.h
src/main/command_executor.h
src/main/driver_unified.cpp
src/main/util.cpp
src/smt/smt_engine.cpp
src/smt/smt_engine.h
src/util/Makefile.am
src/util/safe_print.cpp [new file with mode: 0644]
src/util/safe_print.h [new file with mode: 0644]
src/util/statistics.cpp
src/util/statistics.h
src/util/statistics_registry.cpp
src/util/statistics_registry.h
test/unit/util/stats_black.h