From 86cb32a3cc6d7858f5d782091fd9a51646cd0109 Mon Sep 17 00:00:00 2001 From: martin Date: Wed, 27 Jul 2022 20:25:08 +0100 Subject: [PATCH 1/4] Explicitly mark some options as legacy and suggest modern versions --- src/goto-analyzer/goto_analyzer_parse_options.cpp | 5 +++++ src/goto-analyzer/goto_analyzer_parse_options.h | 5 ++++- 2 files changed, 9 insertions(+), 1 deletion(-) diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 9d76e8b93dd..39f6d2f44f2 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -160,6 +160,7 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options) "simplify-slicing", !(cmdline.isset("no-simplify-slicing"))); } + // Legacy options else if(cmdline.isset("show-intervals")) { // For backwards compatibility @@ -167,6 +168,8 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options) options.set_option("general-analysis", true); options.set_option("intervals", true); options.set_option("domain set", true); + log.status() << "--show-intervals is deprecated," + << "please use --show --intervals" << messaget::eom; } else if(cmdline.isset("show-non-null")) { @@ -175,6 +178,8 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options) options.set_option("general-analysis", true); options.set_option("non-null", true); options.set_option("domain set", true); + log.status() << "--show-non-null is deprecated," + << "please use --show --non-null" << messaget::eom; } else if(cmdline.isset("intervals") || cmdline.isset("non-null")) { diff --git a/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h index beda0d3a2d3..f451134dd1c 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.h +++ b/src/goto-analyzer/goto_analyzer_parse_options.h @@ -144,6 +144,9 @@ class optionst; "(taint):(show-taint)" \ "(show-local-may-alias)" +#define GOTO_ANALYZER_OPTIONS_LEGACY \ + "(show-intervals)(show-non-null)" \ + #define GOTO_ANALYSER_OPTIONS \ OPT_FUNCTIONS \ OPT_CONFIG_C_CPP \ @@ -159,7 +162,6 @@ class optionst; OPT_VALIDATE \ GOTO_ANALYSER_OPTIONS_TASKS \ "(no-simplify-slicing)" \ - "(show-intervals)(show-non-null)" \ GOTO_ANALYSER_OPTIONS_AI \ "(location-sensitive)(concurrent)" \ GOTO_ANALYSER_OPTIONS_HISTORY \ @@ -168,6 +170,7 @@ class optionst; GOTO_ANALYSER_OPTIONS_STORAGE \ GOTO_ANALYSER_OPTIONS_OUTPUT \ GOTO_ANALYSER_OPTIONS_SPECIFIC_ANALYSES \ + GOTO_ANALYZER_OPTIONS_LEGACY \ // clang-format on class goto_analyzer_parse_optionst: public parse_options_baset From 98b598cb5e6953ae4bdc595452cfea473bfbe6c7 Mon Sep 17 00:00:00 2001 From: martin Date: Wed, 27 Jul 2022 20:41:45 +0100 Subject: [PATCH 2/4] Move --dependence-graph to goto-analyzer It is already supported, tested and documented so this is straight-forward. The biggest change is migrating and updating tests. --- .../data-flow1/main.c | 0 .../data-flow1/test.desc | 2 +- .../dependence-graph1/main.c | 0 .../dependence-graph1/test.desc | 2 +- .../goto_rw_pointer_handling-2/main.c | 0 .../goto_rw_pointer_handling-2/test.desc | 3 +-- .../goto_instrument_parse_options.cpp | 15 ++++----------- .../goto_instrument_parse_options.h | 9 +++++++-- 8 files changed, 14 insertions(+), 17 deletions(-) rename regression/{goto-instrument => goto-analyzer}/data-flow1/main.c (100%) rename regression/{goto-instrument => goto-analyzer}/data-flow1/test.desc (78%) rename regression/{goto-instrument => goto-analyzer}/dependence-graph1/main.c (100%) rename regression/{goto-instrument => goto-analyzer}/dependence-graph1/test.desc (67%) rename regression/{goto-instrument => goto-analyzer}/goto_rw_pointer_handling-2/main.c (100%) rename regression/{goto-instrument => goto-analyzer}/goto_rw_pointer_handling-2/test.desc (87%) diff --git a/regression/goto-instrument/data-flow1/main.c b/regression/goto-analyzer/data-flow1/main.c similarity index 100% rename from regression/goto-instrument/data-flow1/main.c rename to regression/goto-analyzer/data-flow1/main.c diff --git a/regression/goto-instrument/data-flow1/test.desc b/regression/goto-analyzer/data-flow1/test.desc similarity index 78% rename from regression/goto-instrument/data-flow1/test.desc rename to regression/goto-analyzer/data-flow1/test.desc index eb4fc8394e4..a3b8168157a 100644 --- a/regression/goto-instrument/data-flow1/test.desc +++ b/regression/goto-analyzer/data-flow1/test.desc @@ -1,6 +1,6 @@ CORE main.c ---show-dependence-graph +--show --dependence-graph ^EXIT=0$ ^SIGNAL=0$ Data dependencies: *[0-9]+,[0-9]+,[0-9]+ diff --git a/regression/goto-instrument/dependence-graph1/main.c b/regression/goto-analyzer/dependence-graph1/main.c similarity index 100% rename from regression/goto-instrument/dependence-graph1/main.c rename to regression/goto-analyzer/dependence-graph1/main.c diff --git a/regression/goto-instrument/dependence-graph1/test.desc b/regression/goto-analyzer/dependence-graph1/test.desc similarity index 67% rename from regression/goto-instrument/dependence-graph1/test.desc rename to regression/goto-analyzer/dependence-graph1/test.desc index caef399aa9c..af398be8c70 100644 --- a/regression/goto-instrument/dependence-graph1/test.desc +++ b/regression/goto-analyzer/dependence-graph1/test.desc @@ -1,6 +1,6 @@ CORE main.c ---show-dependence-graph +--show --dependence-graph ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-instrument/goto_rw_pointer_handling-2/main.c b/regression/goto-analyzer/goto_rw_pointer_handling-2/main.c similarity index 100% rename from regression/goto-instrument/goto_rw_pointer_handling-2/main.c rename to regression/goto-analyzer/goto_rw_pointer_handling-2/main.c diff --git a/regression/goto-instrument/goto_rw_pointer_handling-2/test.desc b/regression/goto-analyzer/goto_rw_pointer_handling-2/test.desc similarity index 87% rename from regression/goto-instrument/goto_rw_pointer_handling-2/test.desc rename to regression/goto-analyzer/goto_rw_pointer_handling-2/test.desc index 11b2f05b272..3867a20597a 100644 --- a/regression/goto-instrument/goto_rw_pointer_handling-2/test.desc +++ b/regression/goto-analyzer/goto_rw_pointer_handling-2/test.desc @@ -1,9 +1,8 @@ CORE main.c ---show-dependence-graph +--show --dependence-graph ^EXIT=0$ ^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ ^Data dependencies: \d+$ -- ^warning: ignoring diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 79716cd3767..5a44d8e4f87 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -55,7 +55,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include @@ -568,15 +567,10 @@ int goto_instrument_parse_optionst::doit() if(cmdline.isset("show-dependence-graph")) { - do_indirect_call_and_rtti_removal(); - - const namespacet ns(goto_model.symbol_table); - dependence_grapht dependence_graph(ns); - dependence_graph(goto_model); - dependence_graph.output(goto_model, std::cout); - dependence_graph.output_dot(std::cout); - - return CPROVER_EXIT_SUCCESS; + log.status() << "--show-dependence-graph is deprecated, " + << "use goto-analyzer --show --dependence-graph" + << messaget::eom; + return CPROVER_EXIT_USAGE_ERROR; } if(cmdline.isset("count-eloc")) @@ -1813,7 +1807,6 @@ void goto_instrument_parse_optionst::help() " --show-rw-set show read-write sets\n" " --show-call-sequences show function call sequences\n" " --show-reaching-definitions show reaching definitions\n" - " --show-dependence-graph show program-dependence graph\n" " --show-sese-regions show single-entry-single-exit regions\n" "\n" "Safety checks:\n" diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 905e7d191f1..92082b32b1f 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -45,7 +45,12 @@ Author: Daniel Kroening, kroening@kroening.com #include "wmm/weak_memory.h" // clang-format off -#define GOTO_INSTRUMENT_OPTIONS \ +// Options that have been moved to goto-analyzer +#define GOTO_INSTRUMENT_MIGRATED_OPTIONS \ + "(show-dependence-graph)" \ + // empty last line + +#define GOTO_INSTRUMENT_OPTIONS \ OPT_DOCUMENT_PROPERTIES \ OPT_DUMP_C \ "(dot)(xml)" \ @@ -93,7 +98,7 @@ Author: Daniel Kroening, kroening@kroening.com "(show-call-sequences)(check-call-sequence)" \ "(interpreter)(show-reaching-definitions)" \ "(list-symbols)(list-undefined-functions)" \ - "(z3)(add-library)(show-dependence-graph)" \ + "(z3)(add-library)" \ "(horn)(skip-loops):(model-argc-argv):" \ "(" FLAG_LOOP_CONTRACTS ")" \ "(" FLAG_REPLACE_CALL "):" \ From 480260a56c4a0a35de400990ce40ce66350da6bc Mon Sep 17 00:00:00 2001 From: martin Date: Wed, 27 Jul 2022 21:17:46 +0100 Subject: [PATCH 3/4] Move --show-intervals to goto-analyzer There is not much to do as this is already supported, tested and documented in goto-analyzer and there are no tests for this in goto-instrument. --- .../goto_instrument_parse_options.cpp | 17 ++++------------- .../goto_instrument_parse_options.h | 3 ++- 2 files changed, 6 insertions(+), 14 deletions(-) diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 5a44d8e4f87..61538e4ee8e 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -58,7 +58,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include @@ -487,17 +486,10 @@ int goto_instrument_parse_optionst::doit() if(cmdline.isset("show-intervals")) { - do_indirect_call_and_rtti_removal(); - - // recalculate numbers, etc. - goto_model.goto_functions.update(); - - log.status() << "Interval Analysis" << messaget::eom; - namespacet ns(goto_model.symbol_table); - ait interval_analysis; - interval_analysis(goto_model); - interval_analysis.output(goto_model, std::cout); - return CPROVER_EXIT_SUCCESS; + log.status() << "--show-intervals is deprecated, " + << "use goto-analyzer --show --intervals" + << messaget::eom; + return CPROVER_EXIT_USAGE_ERROR; } if(cmdline.isset("show-call-sequences")) @@ -1801,7 +1793,6 @@ void goto_instrument_parse_optionst::help() " --show-custom-bitvector-analysis\n" " show results of configurable bitvector analysis\n" // NOLINT(*) " --interval-analysis perform interval analysis\n" - " --show-intervals show results of interval analysis\n" " --show-uninitialized show maybe-uninitialized variables\n" " --show-points-to show points-to information\n" " --show-rw-set show read-write sets\n" diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 92082b32b1f..5b9e8d84b7a 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -48,6 +48,7 @@ Author: Daniel Kroening, kroening@kroening.com // Options that have been moved to goto-analyzer #define GOTO_INSTRUMENT_MIGRATED_OPTIONS \ "(show-dependence-graph)" \ + "(show-intervals)" \ // empty last line #define GOTO_INSTRUMENT_OPTIONS \ @@ -79,7 +80,7 @@ Author: Daniel Kroening, kroening@kroening.com "(show-local-bitvector-analysis)(show-custom-bitvector-analysis)" \ "(show-escape-analysis)(escape-analysis)" \ "(custom-bitvector-analysis)" \ - "(show-struct-alignment)(interval-analysis)(show-intervals)" \ + "(show-struct-alignment)(interval-analysis)" \ "(show-uninitialized)(show-locations)" \ "(full-slice)(reachability-slice)(slice-global-inits)" \ "(fp-reachability-slice):" \ From ffb9246c9e0dab2ed6572ff1daaf1efa53b57271 Mon Sep 17 00:00:00 2001 From: martin Date: Sun, 11 Sep 2022 15:39:46 +0100 Subject: [PATCH 4/4] Move --constant-propagator to goto-analyzer The functionality is already present and tested so there is not much to do. --- .../constant-propagation-function-call/main.c | 1 + .../constant-propagation-function-call/test.desc | 11 ++++------- .../constant-propagation1/main.c | 0 .../goto-analyzer/constant-propagation1/test.desc | 8 ++++++++ .../constant-propagation2/main.c | 0 .../goto-analyzer/constant-propagation2/test.desc | 8 ++++++++ .../constant_propagator_unreachable/test.c | 0 .../constant_propagator_unreachable/test.desc | 4 ++-- .../constant-propagation1/test.desc | 8 -------- .../constant-propagation2/test.desc | 8 -------- .../goto_instrument_parse_options.cpp | 15 +++++++-------- .../goto_instrument_parse_options.h | 3 ++- 12 files changed, 32 insertions(+), 34 deletions(-) rename regression/{goto-instrument => goto-analyzer}/constant-propagation-function-call/main.c (92%) rename regression/{goto-instrument => goto-analyzer}/constant-propagation-function-call/test.desc (62%) rename regression/{goto-instrument => goto-analyzer}/constant-propagation1/main.c (100%) create mode 100644 regression/goto-analyzer/constant-propagation1/test.desc rename regression/{goto-instrument => goto-analyzer}/constant-propagation2/main.c (100%) create mode 100644 regression/goto-analyzer/constant-propagation2/test.desc rename regression/{goto-instrument => goto-analyzer}/constant_propagator_unreachable/test.c (100%) rename regression/{goto-instrument => goto-analyzer}/constant_propagator_unreachable/test.desc (77%) delete mode 100644 regression/goto-instrument/constant-propagation1/test.desc delete mode 100644 regression/goto-instrument/constant-propagation2/test.desc diff --git a/regression/goto-instrument/constant-propagation-function-call/main.c b/regression/goto-analyzer/constant-propagation-function-call/main.c similarity index 92% rename from regression/goto-instrument/constant-propagation-function-call/main.c rename to regression/goto-analyzer/constant-propagation-function-call/main.c index b9a8e69e2de..abe0f893634 100644 --- a/regression/goto-instrument/constant-propagation-function-call/main.c +++ b/regression/goto-analyzer/constant-propagation-function-call/main.c @@ -13,5 +13,6 @@ int main() int b; b = nondet(); a = f(a); + assert(a == 4); assert(!(0 <= a && a < 5 && 0 <= b && b < 5)); } diff --git a/regression/goto-instrument/constant-propagation-function-call/test.desc b/regression/goto-analyzer/constant-propagation-function-call/test.desc similarity index 62% rename from regression/goto-instrument/constant-propagation-function-call/test.desc rename to regression/goto-analyzer/constant-propagation-function-call/test.desc index 21fbb5366cd..a252d75e939 100644 --- a/regression/goto-instrument/constant-propagation-function-call/test.desc +++ b/regression/goto-analyzer/constant-propagation-function-call/test.desc @@ -1,15 +1,12 @@ CORE main.c ---constant-propagator -^EXIT=10$ +--verify --constants +^EXIT=0$ ^SIGNAL=0$ -Removing returns -VERIFICATION FAILED -ASSIGN main\:\:1\:\:a \:\= 4 -ASSERT ¬\(main::1::b ≥ 0\) ∨ main::1::b ≥ 5 +\[main.assertion.1\] line 16 assertion a == 4: SUCCESS +\[main.assertion.2\] line 17 assertion !\(0 <= a && a < 5 && 0 <= b && b < 5\): UNKNOWN -- ^warning: ignoring -ASSERT true -- This tests that constants are propagated through function calls, correctly taking into account the return value. Constant propagation should result in diff --git a/regression/goto-instrument/constant-propagation1/main.c b/regression/goto-analyzer/constant-propagation1/main.c similarity index 100% rename from regression/goto-instrument/constant-propagation1/main.c rename to regression/goto-analyzer/constant-propagation1/main.c diff --git a/regression/goto-analyzer/constant-propagation1/test.desc b/regression/goto-analyzer/constant-propagation1/test.desc new file mode 100644 index 00000000000..34337143a42 --- /dev/null +++ b/regression/goto-analyzer/constant-propagation1/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--verify --constants --recursive-interprocedural --loop-unwind 4 --one-domain-per-history +^EXIT=0$ +^SIGNAL=0$ +\[main.assertion.1\] line 17 assertion i \!= n: UNKNOWN +-- +^warning: ignoring diff --git a/regression/goto-instrument/constant-propagation2/main.c b/regression/goto-analyzer/constant-propagation2/main.c similarity index 100% rename from regression/goto-instrument/constant-propagation2/main.c rename to regression/goto-analyzer/constant-propagation2/main.c diff --git a/regression/goto-analyzer/constant-propagation2/test.desc b/regression/goto-analyzer/constant-propagation2/test.desc new file mode 100644 index 00000000000..d25a1d09f6c --- /dev/null +++ b/regression/goto-analyzer/constant-propagation2/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--verify --constants +^EXIT=0$ +^SIGNAL=0$ +\[main.assertion.1\] line 7 assertion \*p == 0: SUCCESS +-- +^warning: ignoring diff --git a/regression/goto-instrument/constant_propagator_unreachable/test.c b/regression/goto-analyzer/constant_propagator_unreachable/test.c similarity index 100% rename from regression/goto-instrument/constant_propagator_unreachable/test.c rename to regression/goto-analyzer/constant_propagator_unreachable/test.c diff --git a/regression/goto-instrument/constant_propagator_unreachable/test.desc b/regression/goto-analyzer/constant_propagator_unreachable/test.desc similarity index 77% rename from regression/goto-instrument/constant_propagator_unreachable/test.desc rename to regression/goto-analyzer/constant_propagator_unreachable/test.desc index 8e31fca8820..635d2a4ebad 100644 --- a/regression/goto-instrument/constant_propagator_unreachable/test.desc +++ b/regression/goto-analyzer/constant_propagator_unreachable/test.desc @@ -1,9 +1,9 @@ CORE test.c ---constant-propagator + --verify --constants ^EXIT=0$ ^SIGNAL=0$ -VERIFICATION SUCCESSFUL +SUCCESS \(unreachable\) -- failed to find state -- diff --git a/regression/goto-instrument/constant-propagation1/test.desc b/regression/goto-instrument/constant-propagation1/test.desc deleted file mode 100644 index e67a04dedf6..00000000000 --- a/regression/goto-instrument/constant-propagation1/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -CORE -main.c ---constant-propagator --unwind 3 -^EXIT=10$ -^SIGNAL=0$ -^VERIFICATION FAILED$ --- -^warning: ignoring diff --git a/regression/goto-instrument/constant-propagation2/test.desc b/regression/goto-instrument/constant-propagation2/test.desc deleted file mode 100644 index 8d7df7fddb6..00000000000 --- a/regression/goto-instrument/constant-propagation2/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -CORE -main.c ---constant-propagator -^EXIT=0$ -^SIGNAL=0$ -VERIFICATION SUCCESSFUL --- -^warning: ignoring diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 61538e4ee8e..c586ef01880 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1270,13 +1270,13 @@ void goto_instrument_parse_optionst::instrument_goto_program() if(cmdline.isset("constant-propagator")) { - do_indirect_call_and_rtti_removal(); - do_remove_returns(); - - log.status() << "Propagating Constants" << messaget::eom; - - constant_propagator_ait constant_propagator_ai(goto_model); - remove_skip(goto_model); + log.status() << "--constant-propagator is deprecated, " + << "'goto-analyzer --simplify out.gb " + << "--vsd --vsd-value constants'" + << " is the recommended replacement but " + << "'goto-analyzer --simplify out.gb --constants'" + << " should provide backwards compatability" + << messaget::eom; } if(cmdline.isset("generate-function-body")) @@ -1841,7 +1841,6 @@ void goto_instrument_parse_optionst::help() " single edge back to the loop head\n" " --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*) HELP_REMOVE_POINTERS - " --constant-propagator propagate constants and simplify expressions\n" // NOLINT(*) " --inline perform full inlining\n" " --partial-inline perform partial inlining\n" " --function-inline transitively inline all calls makes\n" // NOLINT(*) diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 5b9e8d84b7a..1e06abefa63 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -47,6 +47,7 @@ Author: Daniel Kroening, kroening@kroening.com // clang-format off // Options that have been moved to goto-analyzer #define GOTO_INSTRUMENT_MIGRATED_OPTIONS \ + "(constant-propagator)" \ "(show-dependence-graph)" \ "(show-intervals)" \ // empty last line @@ -94,7 +95,7 @@ Author: Daniel Kroening, kroening@kroening.com OPT_TIMESTAMP \ "(show-natural-loops)(show-lexical-loops)(accelerate)(havoc-loops)" \ "(verbosity):(version)(xml-ui)(json-ui)" \ - "(accelerate)(constant-propagator)" \ + "(accelerate)" \ "(k-induction):(step-case)(base-case)" \ "(show-call-sequences)(check-call-sequence)" \ "(interpreter)(show-reaching-definitions)" \