Merge pull request #1487 from martin-cs/goto-analyzer-6-part2

Goto analyzer 6 part2

Author: Matthias Güdemann

regression/goto-analyzer/sensitivity-function-call-recursive/main.c

@@ -0,0 +1,56 @@
+#include <assert.h>
+
+int bar(int other)
+{
+  if(other > 0)
+  {
+    int value = bar(other - 1);
+    return value + 1;
+  }
+  else
+  {
+    return 0;
+  }
+}
+
+int bar_clean(int other)
+{
+  if(other > 0)
+  {
+    int value = bar_clean(other - 1);
+    return value + 1;
+  }
+  else
+  {
+    return 0;
+  }
+}
+
+int fun(int changing, int constant)
+{
+  if(changing > 0)
+  {
+    int value = fun(changing - 1, constant);
+    return value;
+  }
+  else
+  {
+    return constant;
+  }
+}
+
+int main(int argc, char *argv[])
+{
+  int x=3;
+  int y=bar(x+1);
+  assert(y==4); // Unknown in the constants domain
+
+  int y2 = bar(0);
+  assert(y2==0); // Unknown since we are not sensitive to call domain
+
+  int z = bar_clean(0);
+  assert(z==0); // Unknown as the function has parameter as top
+
+  int w = fun(5, 18);
+  assert(w==18);
+}

regression/goto-analyzer/sensitivity-function-call-recursive/test.desc

@@ -0,0 +1,11 @@
+KNOWNBUG
+main.c
+--variable --pointers --arrays --structs --verify
+^EXIT=0$
+^SIGNAL=0$
+^\[main\.assertion\.1\] .* assertion y==4: Unknown$
+^\[main\.assertion\.2\] .* assertion y2==0: Unknown$
+^\[main\.assertion\.3\] .* assertion z==0: Success$
+^\[main\.assertion\.4\] .* assertion w==18: Success$
+--
+^warning: ignoring

src/analyses/ai.cpp

@@ -37,7 +37,7 @@ xmlt ai_domain_baset::output_xml(
 {
   std::ostringstream out;
   output(out, ai, ns);
-  xmlt xml("domain");
+  xmlt xml("abstract_state");
   xml.data=out.str();
   return xml;
 }
@@ -170,7 +170,7 @@ jsont ai_baset::output_json(
       json_numbert(std::to_string(i_it->location_number));
     location["sourceLocation"]=
       json_stringt(i_it->source_location.as_string());
-    location["domain"]=find_state(i_it).output_json(*this, ns);
+    location["abstractState"]=find_state(i_it).output_json(*this, ns);
 
     // Ideally we need output_instruction_json
     std::ostringstream out;
@@ -431,7 +431,12 @@ bool ai_baset::do_function_call(
     assert(l_end->is_end_function());
 
     // do edge from end of function to instruction after call
-    std::unique_ptr<statet> tmp_state(make_temporary_state(get_state(l_end)));
+    const statet &end_state=get_state(l_end);
+
+    if(end_state.is_bottom())
+      return false; // function exit point not reachable
+
+    std::unique_ptr<statet> tmp_state(make_temporary_state(end_state));
     tmp_state->transform(l_end, l_return, *this, ns);
 
     // Propagate those
@@ -454,14 +459,6 @@ bool ai_baset::do_function_call_rec(
   {
     const irep_idt &identifier=function.get(ID_identifier);
 
-    if(recursion_set.find(identifier)!=recursion_set.end())
-    {
-      // recursion detected!
-      return new_data;
-    }
-    else
-      recursion_set.insert(identifier);
-
     goto_functionst::function_mapt::const_iterator it=
       goto_functions.function_map.find(identifier);
 
@@ -474,8 +471,6 @@ bool ai_baset::do_function_call_rec(
       it,
       arguments,
       ns);
-
-    recursion_set.erase(identifier);
   }
   else if(function.id()==ID_if)
   {

src/analyses/ai.h

@@ -80,6 +80,10 @@ class ai_domain_baset
   // a reasonable entry-point state
   virtual void make_entry()=0;
 
+  virtual bool is_bottom() const=0;
+
+  virtual bool is_top() const=0;
+
   // also add
   //
   //   bool merge(const T &b, locationt from, locationt to);
@@ -158,6 +162,17 @@ class ai_baset
     fixedpoint(goto_function.body, goto_functions, ns);
   }
 
+  /// Returns the abstract state before the given instruction
+  virtual const ai_domain_baset & abstract_state_before(
+    goto_programt::const_targett t) const = 0;
+
+  /// Returns the abstract state after the given instruction
+  virtual const ai_domain_baset & abstract_state_after(
+    goto_programt::const_targett t) const
+  {
+    return abstract_state_before(std::next(t));
+  }
+
   virtual void clear()
   {
   }
@@ -307,9 +322,6 @@ class ai_baset
     const goto_functionst &goto_functions,
     const namespacet &ns);
 
-  typedef std::set<irep_idt> recursion_sett;
-  recursion_sett recursion_set;
-
   // function calls
   bool do_function_call_rec(
     locationt l_call, locationt l_return,
@@ -369,6 +381,12 @@ class ait:public ai_baset
     return it->second;
   }
 
+  const ai_domain_baset & abstract_state_before(
+    goto_programt::const_targett t) const override
+  {
+    return (*this)[t];
+  }
+
   void clear() override
   {
     state_map.clear();

src/analyses/constant_propagator.h

@@ -25,7 +25,7 @@ class constant_propagator_domaint:public ai_domain_baset
     locationt from,
     locationt to,
     ai_baset &ai_base,
-    const namespacet &ns) override;
+    const namespacet &ns) final override;
 
   virtual void output(
     std::ostream &out,
@@ -39,23 +39,33 @@ class constant_propagator_domaint:public ai_domain_baset
 
   virtual bool ai_simplify(
     exprt &condition,
-    const namespacet &ns) const override;
+    const namespacet &ns) const final override;
 
-  virtual void make_bottom() override
+  virtual void make_bottom() final override
   {
     values.set_to_bottom();
   }
 
-  virtual void make_top() override
+  virtual void make_top() final override
   {
     values.set_to_top();
   }
 
-  virtual void make_entry() override
+  virtual void make_entry() final override
   {
     make_top();
   }
 
+  virtual bool is_bottom() const final override
+  {
+    return values.is_bot();
+  }
+
+  virtual bool is_top() const final override
+  {
+    return values.is_top();
+  }
+
   struct valuest
   {
   public:
@@ -70,27 +80,37 @@ class constant_propagator_domaint:public ai_domain_baset
 
     // set whole state
 
-    inline void set_to_bottom()
+    void set_to_bottom()
     {
       replace_const.clear();
       is_bottom=true;
     }
 
-    inline void set_to_top()
+    void set_to_top()
     {
       replace_const.clear();
       is_bottom=false;
     }
 
+    bool is_bot() const
+    {
+      return is_bottom && replace_const.empty();
+    }
+
+    bool is_top() const
+    {
+      return !is_bottom && replace_const.empty();
+    }
+
     // set single identifier
 
-    inline void set_to(const irep_idt &lhs, const exprt &rhs)
+    void set_to(const irep_idt &lhs, const exprt &rhs)
     {
       replace_const.expr_map[lhs]=rhs;
       is_bottom=false;
     }
 
-    inline void set_to(const symbol_exprt &lhs, const exprt &rhs)
+    void set_to(const symbol_exprt &lhs, const exprt &rhs)
     {
       set_to(lhs.get_identifier(), rhs);
     }

src/analyses/custom_bitvector_analysis.h

@@ -27,32 +27,48 @@ class custom_bitvector_domaint:public ai_domain_baset
     locationt from,
     locationt to,
     ai_baset &ai,
-    const namespacet &ns) final;
+    const namespacet &ns) final override;
 
   void output(
     std::ostream &out,
     const ai_baset &ai,
-    const namespacet &ns) const final;
+    const namespacet &ns) const final override;
 
-  void make_bottom() final
+  void make_bottom() final override
   {
     may_bits.clear();
     must_bits.clear();
     has_values=tvt(false);
   }
 
-  void make_top() final
+  void make_top() final override
   {
     may_bits.clear();
     must_bits.clear();
     has_values=tvt(true);
   }
 
-  void make_entry() final
+  void make_entry() final override
   {
     make_top();
   }
 
+  bool is_bottom() const final override
+  {
+    DATA_INVARIANT(!has_values.is_false() ||
+                   (may_bits.empty() && must_bits.empty()),
+                   "If the domain is bottom, it must have no bits set");
+    return has_values.is_false();
+  }
+
+  bool is_top() const final override
+  {
+    DATA_INVARIANT(!has_values.is_true() ||
+                   (may_bits.empty() && must_bits.empty()),
+                   "If the domain is top, it must have no bits set");
+    return has_values.is_true();
+  }
+
   bool merge(
     const custom_bitvector_domaint &b,
     locationt from,

src/analyses/dependence_graph.h

@@ -83,40 +83,66 @@ class dep_graph_domaint:public ai_domain_baset
     goto_programt::const_targett from,
     goto_programt::const_targett to,
     ai_baset &ai,
-    const namespacet &ns) final;
+    const namespacet &ns) final override;
 
   void output(
     std::ostream &out,
     const ai_baset &ai,
-    const namespacet &ns) const final;
+    const namespacet &ns) const final override;
 
   jsont output_json(
     const ai_baset &ai,
     const namespacet &ns) const override;
 
   void make_top() final override
   {
-    assert(node_id!=std::numeric_limits<node_indext>::max());
+    DATA_INVARIANT(node_id!=std::numeric_limits<node_indext>::max(),
+                   "node_id must not be valid");
 
     has_values=tvt(true);
     control_deps.clear();
     data_deps.clear();
   }
 
-  void make_bottom() final
+  void make_bottom() final override
   {
-    assert(node_id!=std::numeric_limits<node_indext>::max());
+    DATA_INVARIANT(node_id!=std::numeric_limits<node_indext>::max(),
+                   "node_id must be valid");
 
     has_values=tvt(false);
     control_deps.clear();
     data_deps.clear();
   }
 
-  void make_entry() final
+  void make_entry() final override
   {
     make_top();
   }
 
+  bool is_top() const final override
+  {
+    DATA_INVARIANT(node_id!=std::numeric_limits<node_indext>::max(),
+                   "node_id must be valid");
+
+    DATA_INVARIANT(!has_values.is_true() ||
+                   (control_deps.empty() && data_deps.empty()),
+                   "If the domain is top, it must have no dependencies");
+
+    return has_values.is_true();
+  }
+
+  bool is_bottom() const final override
+  {
+    DATA_INVARIANT(node_id!=std::numeric_limits<node_indext>::max(),
+                   "node_id must be valid");
+
+    DATA_INVARIANT(!has_values.is_false() ||
+                   (control_deps.empty() && data_deps.empty()),
+                   "If the domain is bottom, it must have no dependencies");
+
+    return has_values.is_false();
+  }
+
   void set_node_id(node_indext id)
   {
     node_id=id;