From e8ec160168f598b4377934762a42421477969d88 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Wed, 22 Mar 2017 09:54:11 +0000 Subject: [PATCH 1/3] Add --drop-unused-functions option The default behaviour of CBMC for the options --show-goto-functions, --show-properties and --cover is to consider all functions. This is particularly annoying for --cover where coverage goals are reported from functions that are trivially unreachable from the entry point. Also, --show-reachable-properties has been introduced in the past to hide such properties. We could change the default behaviour to slicing away everything that is trivially unreachable from the entry point. However, this would require an extra option to be able to view all functions and properties. This commit preserves the default behaviour and enables focussing the output of --show-goto-functions --show-properties and --cover on functions that are not trivially unreachable using --drop-unused-functions. --- src/cbmc/cbmc_parse_options.cpp | 9 ++++++++- src/cbmc/cbmc_parse_options.h | 1 + src/symex/symex_parse_options.cpp | 9 +++++++++ src/symex/symex_parse_options.h | 1 + 4 files changed, 19 insertions(+), 1 deletion(-) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index e33e700e0ca..f5241ed48b1 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -952,8 +952,14 @@ bool cbmc_parse_optionst::process_goto_program( // add loop ids goto_functions.compute_loop_numbers(); - // instrument cover goals + if(cmdline.isset("drop-unused-functions")) + { + // Entry point will have been set before and function pointers removed + status() << "Removing Unused Functions" << eom; + remove_unused_functions(goto_functions, ui_message_handler); + } + // instrument cover goals if(cmdline.isset("cover")) { std::list criteria_strings= @@ -1099,6 +1105,7 @@ void cbmc_parse_optionst::help() " --property id only check one specific property\n" " --stop-on-fail stop analysis once a failed property is detected\n" // NOLINT(*) " --trace give a counterexample trace for failed properties\n" //NOLINT(*) + " --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*) "\n" "C/C++ frontend options:\n" " -I path set include path (C/C++)\n" diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index a3fc5e7e7d3..bcc3b8ac749 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -42,6 +42,7 @@ class optionst; "(show-goto-functions)(show-loops)" \ "(show-symbol-table)(show-parse-tree)(show-vcc)" \ "(show-claims)(claim):(show-properties)(show-reachable-properties)" \ + "(drop-unused-functions)" \ "(property):(stop-on-fail)(trace)" \ "(error-label):(verbosity):(no-library)" \ "(nondet-static)" \ diff --git a/src/symex/symex_parse_options.cpp b/src/symex/symex_parse_options.cpp index 54aa9382759..04135b96d9c 100644 --- a/src/symex/symex_parse_options.cpp +++ b/src/symex/symex_parse_options.cpp @@ -34,6 +34,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include @@ -383,6 +384,13 @@ bool symex_parse_optionst::process_goto_program(const optionst &options) // add loop ids goto_model.goto_functions.compute_loop_numbers(); + if(cmdline.isset("drop-unused-functions")) + { + // Entry point will have been set before and function pointers removed + status() << "Removing Unused Functions" << eom; + remove_unused_functions(goto_model.goto_functions, ui_message_handler); + } + if(cmdline.isset("cover")) { std::string criterion=cmdline.get_value("cover"); @@ -683,6 +691,7 @@ void symex_parse_optionst::help() " --stop-on-fail stop analysis once a failed property is detected\n" // NOLINTNEXTLINE(whitespace/line_length) " --trace give a counterexample trace for failed properties\n" + " --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*) "\n" "Frontend options:\n" " -I path set include path (C/C++)\n" diff --git a/src/symex/symex_parse_options.h b/src/symex/symex_parse_options.h index a67469d71e5..5e178eec14e 100644 --- a/src/symex/symex_parse_options.h +++ b/src/symex/symex_parse_options.h @@ -41,6 +41,7 @@ class optionst; "(string-abstraction)(no-arch)(arch):(floatbv)(fixedbv)" \ "(round-to-nearest)(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \ "(show-locs)(show-vcc)(show-properties)" \ + "(drop-unused-functions)" \ OPT_SHOW_GOTO_FUNCTIONS \ "(property):(trace)(show-trace)(stop-on-fail)(eager-infeasibility)" \ "(no-simplify)(no-unwinding-assertions)(no-propagation)" From a35731baa6e38343d75ece15a78acc5846e73875 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 23 Mar 2017 18:44:09 +0000 Subject: [PATCH 2/3] Remove -show-reachable-properties The same effect can now be achieved by --show-properties --drop-unused-functions --- src/cbmc/cbmc_parse_options.cpp | 13 ------------- src/cbmc/cbmc_parse_options.h | 2 +- 2 files changed, 1 insertion(+), 14 deletions(-) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index f5241ed48b1..657e4531429 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -540,19 +540,6 @@ int cbmc_parse_optionst::doit() return 0; // should contemplate EX_OK from sysexits.h } - // may replace --show-properties - if(cmdline.isset("show-reachable-properties")) - { - const namespacet ns(symbol_table); - - // Entry point will have been set before and function pointers removed - status() << "Removing Unused Functions" << eom; - remove_unused_functions(goto_functions, ui_message_handler); - - show_properties(ns, get_ui(), goto_functions); - return 0; // should contemplate EX_OK from sysexits.h - } - if(set_properties(goto_functions)) return 7; // should contemplate EX_USAGE from sysexits.h diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index bcc3b8ac749..5fe9cdd9bf8 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -41,7 +41,7 @@ class optionst; "(little-endian)(big-endian)" \ "(show-goto-functions)(show-loops)" \ "(show-symbol-table)(show-parse-tree)(show-vcc)" \ - "(show-claims)(claim):(show-properties)(show-reachable-properties)" \ + "(show-claims)(claim):(show-properties)" \ "(drop-unused-functions)" \ "(property):(stop-on-fail)(trace)" \ "(error-label):(verbosity):(no-library)" \ From 5e5bbca1d2f1ddf044c4e8d440bfe61ce64f864c Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Wed, 22 Mar 2017 10:42:04 +0000 Subject: [PATCH 3/3] Correctly align description of option --- src/goto-programs/show_goto_functions.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/goto-programs/show_goto_functions.h b/src/goto-programs/show_goto_functions.h index 5bb7320963e..a496682961e 100644 --- a/src/goto-programs/show_goto_functions.h +++ b/src/goto-programs/show_goto_functions.h @@ -19,7 +19,7 @@ class goto_modelt; "(show-goto-functions)" #define HELP_SHOW_GOTO_FUNCTIONS \ - " --show-goto-functions show goto program\n" + " --show-goto-functions show goto program\n" void show_goto_functions( const namespacet &ns,