Merge pull request #6482 from martin-cs/refactor/remove-static-analysis

Port the last user of static_analysist

Author: tautschnig

jbmc/unit/pointer-analysis/custom_value_set_analysis.cpp

@@ -198,12 +198,12 @@ SCENARIO("test_value_set_analysis",
       std::prev(test_function.instructions.end());
 
     value_set_analysist normal_analysis(ns);
-    normal_analysis(goto_model.goto_functions);
+    normal_analysis(TEST_FUNCTION_NAME, test_function, ns);
     const auto &normal_function_end_vs=
       normal_analysis[test_function_end].value_set;
 
     test_value_set_analysist test_analysis(ns);
-    test_analysis(goto_model.goto_functions);
+    test_analysis(TEST_FUNCTION_NAME, test_function, ns);
     const auto &test_function_end_vs=
       test_analysis[test_function_end].value_set;
 

regression/goto-instrument/show-value-sets/main.c

@@ -0,0 +1,41 @@
+#include <stdlib.h>
+
+#define BIG 4096
+
+int main()
+{
+  // Uninitialized pointer
+  int *u;
+
+  // Basic assignment
+  u = NULL;
+  int a;
+  u = &a;
+
+  // Test merging and the loss of correlation
+  int *p;
+  int *q;
+  int b;
+  int c;
+  int nondet;
+  if(nondet)
+  {
+    p = &b;
+    q = &c;
+  }
+  else
+  {
+    p = &c;
+    q = &b;
+  }
+
+  // Test widening
+  int array[BIG];
+  int *s = &(array[0]);
+  for(int i = 0; i < BIG; ++i)
+  {
+    s = &array[i];
+  }
+
+  return 0;
+}

regression/goto-instrument/show-value-sets/test.desc

@@ -0,0 +1,27 @@
+CORE
+main.c
+--show-value-sets
+^EXIT=0$
+^SIGNAL=0$
+main::1::u = \{ <main::1::u\$object, 0, signedbv\[32\]> \}
+main::1::u = \{ <NULL-object, 0, signedbv\[32\]> \}
+main::1::u = \{ <main::1::a, 0, signedbv\[32\]> \}
+main::1::p = \{ <main::1::b, 0, signedbv\[32\]> \}
+main::1::p = \{ <main::1::c, 0, signedbv\[32\]> \}
+main::1::q = \{ <main::1::b, 0, signedbv\[32\]>, <main::1::c, 0, signedbv\[32\]> \}
+main::1::p = \{ <main::1::b, 0, signedbv\[32\]>, <main::1::c, 0, signedbv\[32\]> \}
+main::1::s = \{ <main::1::array\[0\], \*, signedbv\[32\]> \}
+--
+--
+A few basic tests to check if value sets are being handled correctly.
+
+It would be reasonable to ask about the checks for:
+
+main::1::q = \{ <main::1::b, 0, signedbv\[32\]> \}
+main::1::q = \{ <main::1::c, 0, signedbv\[32\]> \}
+
+but as domains are stored at the start of instructions the following merge will
+over-write it on one branch or the other.  To keep the test portable it is best
+avoided.
+
+

src/analyses/Makefile

@@ -29,7 +29,6 @@ SRC = ai.cpp \
       locals.cpp \
       reaching_definitions.cpp \
       sese_regions.cpp \
-      static_analysis.cpp \
       uncaught_exceptions_analysis.cpp \
       uninitialized_domain.cpp \
       variable-sensitivity/abstract_environment.cpp \

src/analyses/README.md

@@ -8,9 +8,8 @@ static analyses that instantiate them.
 
 \section analyses-frameworks Frameworks:
 
-There are currently three abstract interpretation frameworks provided in this
-directory. \ref analyses-ait, \ref analyses-flow-insensitive-analysis, and the
-deprecated and obsolete \ref analyses-static-analysist.
+There are currently two abstract interpretation frameworks provided in this
+directory. \ref analyses-ait and \ref analyses-flow-insensitive-analysis.
 
 \subsection analyses-ait Abstract interpreter framework (ait)
 
@@ -22,14 +21,6 @@ is provided by \ref ait. This analysis framework is currently location sensitive
 run after the function pointer removal and return removal passes. There is
 ongoing work to make this framework also support context sensitivity.
 
-\subsection analyses-static-analysist Old Abstract interpreter framework (static_analysist)
-
-The obsolete static analysis framework \ref static_analysist is only used by
-\ref value_set_analysist. This abstract interpretation framework is deprecated in
-favour of \ref analyses-ait, and should not be used as the basis for new code.
-This framework is location sensitive (one domain per code location), but is able
-to be run before function pointer removal and return removal phases.
-
 \subsection analyses-flow-insensitive-analysis Flow-insensitive analysis (flow_insensitive_analysist)
 
 Framework for flow-insensitive analyses. Maintains a single global abstract

src/analyses/ai.h

@@ -280,6 +280,28 @@ class ai_baset
     const goto_programt &goto_program,
     std::ostream &out) const;
 
+  /// Output the abstract states for a single function as JSON
+  /// \param ns: The namespace
+  /// \param goto_program: The goto program
+  /// \param function_id: The identifier used to find a symbol to
+  ///   identify the source language
+  /// \return The JSON object
+  virtual jsont output_json(
+    const namespacet &ns,
+    const irep_idt &function_id,
+    const goto_programt &goto_program) const;
+
+  /// Output the abstract states for a single function as XML
+  /// \param ns: The namespace
+  /// \param goto_program: The goto program
+  /// \param function_id: The identifier used to find a symbol to
+  ///   identify the source language
+  /// \return The XML object
+  virtual xmlt output_xml(
+    const namespacet &ns,
+    const irep_idt &function_id,
+    const goto_programt &goto_program) const;
+
   /// Output the abstract states for a whole program
   virtual void output(
     const namespacet &ns,
@@ -389,28 +411,6 @@ class ai_baset
   /// entry state required by the analysis
   trace_ptrt entry_state(const goto_functionst &goto_functions);
 
-  /// Output the abstract states for a single function as JSON
-  /// \param ns: The namespace
-  /// \param goto_program: The goto program
-  /// \param function_id: The identifier used to find a symbol to
-  ///   identify the source language
-  /// \return The JSON object
-  virtual jsont output_json(
-    const namespacet &ns,
-    const irep_idt &function_id,
-    const goto_programt &goto_program) const;
-
-  /// Output the abstract states for a single function as XML
-  /// \param ns: The namespace
-  /// \param goto_program: The goto program
-  /// \param function_id: The identifier used to find a symbol to
-  ///   identify the source language
-  /// \return The XML object
-  virtual xmlt output_xml(
-    const namespacet &ns,
-    const irep_idt &function_id,
-    const goto_programt &goto_program) const;
-
   /// The work queue, sorted using the history's ordering operator
   typedef trace_sett working_sett;
 

src/analyses/ai_domain.h

@@ -113,12 +113,16 @@ class ai_domain_baset
   /// no states
   virtual void make_bottom() = 0;
 
-  /// all states -- the analysis doesn't use this,
+  /// all states -- the analysis doesn't use this directly (see make_entry)
   /// and domains may refuse to implement it.
   virtual void make_top() = 0;
 
   /// Make this domain a reasonable entry-point state
-  virtual void make_entry() = 0;
+  /// For most domains top is sufficient
+  virtual void make_entry()
+  {
+    make_top();
+  }
 
   virtual bool is_bottom() const = 0;
 
@@ -231,4 +235,21 @@ class ai_domain_factory_default_constructort
   }
 };
 
+template <typename domainT>
+class ai_domain_factory_location_constructort
+  : public ai_domain_factoryt<domainT>
+{
+public:
+  typedef ai_domain_factory_baset::statet statet;
+  typedef ai_domain_factory_baset::locationt locationt;
+  typedef ai_domain_factory_baset::trace_ptrt trace_ptrt;
+
+  std::unique_ptr<statet> make(locationt l) const override
+  {
+    auto d = util_make_unique<domainT>(l);
+    CHECK_RETURN(d->is_bottom());
+    return std::unique_ptr<statet>(d.release());
+  }
+};
+
 #endif

src/analyses/constant_propagator.h

@@ -65,11 +65,6 @@ class constant_propagator_domaint:public ai_domain_baset
     values.set_to_top();
   }
 
-  virtual void make_entry() final override
-  {
-    make_top();
-  }
-
   virtual bool is_bottom() const final override
   {
     return values.is_bot();

src/analyses/custom_bitvector_analysis.h

@@ -50,11 +50,6 @@ class custom_bitvector_domaint:public ai_domain_baset
     has_values=tvt(true);
   }
 
-  void make_entry() final override
-  {
-    make_top();
-  }
-
   bool is_bottom() const final override
   {
     DATA_INVARIANT(!has_values.is_false() ||

src/analyses/escape_analysis.h

@@ -71,11 +71,6 @@ class escape_domaint:public ai_domain_baset
     return has_values.is_true();
   }
 
-  void make_entry() override final
-  {
-    make_top();
-  }
-
   typedef union_find<irep_idt> aliasest;
   aliasest aliases;