Refactor/move abstract interpreter functionality into goto analyzer 1

regression/goto-instrument/constant-propagation-function-call/main.c → 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));
 }

regression/goto-instrument/constant-propagation-function-call/test.desc → 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

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

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

regression/goto-instrument/constant_propagator_unreachable/test.desc → 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
 --

regression/goto-instrument/data-flow1/test.desc → 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]+

regression/goto-instrument/dependence-graph1/test.desc → regression/goto-analyzer/dependence-graph1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---show-dependence-graph
+--show --dependence-graph
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/goto-instrument/goto_rw_pointer_handling-2/test.desc → 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

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -160,13 +160,16 @@ 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
     options.set_option("show", true);
     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"))
   {

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

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -55,11 +55,9 @@ Author: Daniel Kroening, [email protected]
 #include <analyses/call_graph.h>
 #include <analyses/constant_propagator.h>
 #include <analyses/custom_bitvector_analysis.h>
-#include <analyses/dependence_graph.h>
 #include <analyses/escape_analysis.h>
 #include <analyses/global_may_alias.h>
 #include <analyses/interval_analysis.h>
-#include <analyses/interval_domain.h>
 #include <analyses/is_threaded.h>
 #include <analyses/lexical_loops.h>
 #include <analyses/local_bitvector_analysis.h>
@@ -488,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_domaint> 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"))
@@ -568,15 +559,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"))
@@ -1284,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"))
@@ -1807,13 +1793,11 @@ 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"
     " --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"
@@ -1857,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 <function> transitively inline all calls <function> makes\n" // NOLINT(*)

src/goto-instrument/goto_instrument_parse_options.h

@@ -45,7 +45,14 @@ Author: Daniel Kroening, [email protected]
 #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 \
+  "(constant-propagator)" \
+  "(show-dependence-graph)" \
+  "(show-intervals)" \
+  // empty last line
+
+#define GOTO_INSTRUMENT_OPTIONS                 \
   OPT_DOCUMENT_PROPERTIES \
   OPT_DUMP_C \
   "(dot)(xml)" \
@@ -74,7 +81,7 @@ Author: Daniel Kroening, [email protected]
   "(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):" \
@@ -88,12 +95,12 @@ Author: Daniel Kroening, [email protected]
   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)" \
   "(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 "):" \