Merge pull request #327 from tautschnig/fix-325

Data-flow analysis must always enter new function

Author: Daniel Kroening

regression/goto-instrument/data-flow1/main.c

@@ -0,0 +1,18 @@
+int d=0;
+
+void f1()
+{
+  d=1;
+}
+
+int main()
+{
+  int x=2;
+  int y=3;
+
+  f1();
+
+  if(x && y && d)
+    return 0;
+}
+

regression/goto-instrument/data-flow1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+"--show-dependence-graph"
+^EXIT=0$
+^SIGNAL=0$
+Data dependencies: .*33.*
+--
+^warning: ignoring

src/analyses/ai.cpp

@@ -120,8 +120,7 @@ Function: ai_baset::entry_state
 
 void ai_baset::entry_state(const goto_programt &goto_program)
 {
-  // The first instruction of 'goto_program' is the entry point,
-  // and we make that 'top'.
+  // The first instruction of 'goto_program' is the entry point
   get_state(goto_program.instructions.begin()).make_entry();
 }
 
@@ -226,9 +225,11 @@ bool ai_baset::fixedpoint(
 {
   working_sett working_set;
 
-  // We will put all locations at least once into the working set.
-  forall_goto_program_instructions(i_it, goto_program)
-    put_in_working_set(working_set, i_it);
+  // Put the first location in the working set
+  if(!goto_program.empty())
+    put_in_working_set(
+      working_set,
+      goto_program.instructions.begin());
 
   bool new_data=false;
 

src/analyses/custom_bitvector_analysis.cpp

@@ -326,6 +326,8 @@ void custom_bitvector_domaint::transform(
   ai_baset &ai,
   const namespacet &ns)
 {
+  if(has_values.is_false()) return;
+
   // upcast of ai
   custom_bitvector_analysist &cba=
     static_cast<custom_bitvector_analysist &>(ai);
@@ -565,8 +567,11 @@ void custom_bitvector_domaint::output(
   const ai_baset &ai,
   const namespacet &ns) const
 {
-  if(is_bottom)
-    out << "BOTTOM\n";
+  if(has_values.is_known())
+  {
+    out << has_values.to_string() << '\n';
+    return;
+  }
 
   const custom_bitvector_analysist &cba=
     static_cast<const custom_bitvector_analysist &>(ai);
@@ -625,10 +630,10 @@ bool custom_bitvector_domaint::merge(
   locationt from,
   locationt to)
 {
-  if(b.is_bottom)
+  if(b.has_values.is_false())
     return false; // no change
 
-  if(is_bottom)
+  if(has_values.is_false())
   {
     *this=b;
     return true; // change
@@ -858,7 +863,7 @@ void custom_bitvector_analysist::check(
         if(!custom_bitvector_domaint::has_get_must_or_may(i_it->guard))
           continue;
 
-        if(operator[](i_it).is_bottom) continue;
+        if(operator[](i_it).has_values.is_false()) continue;
 
         exprt tmp=eval(i_it->guard, i_it);
         result=simplify_expr(tmp, ns);

src/analyses/custom_bitvector_analysis.h

@@ -10,6 +10,7 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_ANALYSES_CUSTOM_BITVECTOR_ANALYSIS_H
 
 #include <util/numbering.h>
+#include <util/threeval.h>
 
 #include "ai.h"
 #include "local_may_alias.h"
@@ -42,20 +43,19 @@ class custom_bitvector_domaint:public ai_domain_baset
   {
     may_bits.clear();
     must_bits.clear();
-    is_bottom=true;
+    has_values=tvt(false);
   }
 
   void make_top() final override
   {
-    // We don't have a proper top, and refuse to do this.
-    assert(false);
+    may_bits.clear();
+    must_bits.clear();
+    has_values=tvt(true);
   }
 
   void make_entry() final override
   {
-    may_bits.clear();
-    must_bits.clear();
-    is_bottom=false;
+    make_top();
   }
 
   bool merge(
@@ -90,9 +90,9 @@ class custom_bitvector_domaint:public ai_domain_baset
   vectorst get_rhs(const exprt &) const;
   vectorst get_rhs(const irep_idt &) const;
 
-  bool is_bottom;
+  tvt has_values;
 
-  custom_bitvector_domaint():is_bottom(true)
+  custom_bitvector_domaint():has_values(true)
   {
   }
 

src/analyses/dependence_graph.cpp

@@ -32,7 +32,8 @@ bool dep_graph_domaint::merge(
   goto_programt::const_targett from,
   goto_programt::const_targett to)
 {
-  bool change=false;
+  bool changed=has_values.is_false();
+  has_values=tvt::unknown();
 
   depst::iterator it=control_deps.begin();
   for(depst::const_iterator ito=src.control_deps.begin();
@@ -44,7 +45,7 @@ bool dep_graph_domaint::merge(
     if(it==control_deps.end() || *ito<*it)
     {
       control_deps.insert(it, *ito);
-      change=true;
+      changed=true;
     }
     else if(it!=control_deps.end())
       ++it;
@@ -60,13 +61,13 @@ bool dep_graph_domaint::merge(
     if(it==data_deps.end() || *ito<*it)
     {
       data_deps.insert(it, *ito);
-      change=true;
+      changed=true;
     }
     else if(it!=data_deps.end())
       ++it;
   }
 
-  return change;
+  return changed;
 }
 
 /*******************************************************************\

src/analyses/dependence_graph.h

@@ -13,6 +13,7 @@ Date: August 2013
 #define CPROVER_ANALYSES_DEPENDENCE_GRAPH_H
 
 #include <util/graph.h>
+#include <util/threeval.h>
 
 #include "ai.h"
 #include "cfg_dominators.h"
@@ -70,6 +71,7 @@ class dep_graph_domaint:public ai_domain_baset
   typedef graph<dep_nodet>::node_indext node_indext;
 
   dep_graph_domaint():
+    has_values(false),
     node_id(std::numeric_limits<node_indext>::max())
   {
   }
@@ -89,20 +91,22 @@ class dep_graph_domaint:public ai_domain_baset
     std::ostream &out,
     const ai_baset &ai,
     const namespacet &ns) const final override;
-    
+
   void make_top() final override
   {
+    has_values=tvt(true);
     node_id=std::numeric_limits<node_indext>::max();
   }
 
   void make_bottom() final override
   {
+    has_values=tvt(false);
     node_id=std::numeric_limits<node_indext>::max();
   }
 
   void make_entry() final override
   {
-    node_id=std::numeric_limits<node_indext>::max();
+    make_top();
   }
 
   void set_node_id(node_indext id)
@@ -117,6 +121,7 @@ class dep_graph_domaint:public ai_domain_baset
   }
 
 protected:
+  tvt has_values;
   node_indext node_id;
 
   typedef std::set<goto_programt::const_targett> depst;

src/analyses/escape_analysis.cpp

@@ -266,6 +266,8 @@ void escape_domaint::transform(
   ai_baset &ai,
   const namespacet &ns)
 {
+  if(has_values.is_false()) return;
+
   // upcast of ai
   //escape_analysist &ea=
   //  static_cast<escape_analysist &>(ai);
@@ -364,9 +366,9 @@ void escape_domaint::output(
   const ai_baset &ai,
   const namespacet &ns) const
 {
-  if(is_bottom)
+  if(has_values.is_known())
   {
-    out << "BOTTOM\n";
+    out << has_values.to_string() << '\n';
     return;
   }
 
@@ -422,10 +424,10 @@ bool escape_domaint::merge(
   locationt from,
   locationt to)
 {
-  if(b.is_bottom)
+  if(b.has_values.is_false())
     return false; // no change
 
-  if(is_bottom)
+  if(has_values.is_false())
   {
     *this=b;
     return true; // change

src/analyses/escape_analysis.h

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_ANALYSES_ESCAPE_ANALYSIS_H
 
 #include <util/numbering.h>
+#include <util/threeval.h>
 #include <util/union_find.h>
 
 #include "ai.h"
@@ -28,7 +29,7 @@ class escape_analysist;
 class escape_domaint:public ai_domain_baset
 {
 public:
-  escape_domaint():is_bottom(true)
+  escape_domaint():has_values(false)
   {
   }
 
@@ -51,19 +52,20 @@ class escape_domaint:public ai_domain_baset
   void make_bottom() override final
   {
     cleanup_map.clear();
-    is_bottom=true;
+    aliases.clear();
+    has_values=tvt(false);
   }
 
   void make_top() override final
   {
-    // We don't have a proper top.
-    assert(false);
+    cleanup_map.clear();
+    aliases.clear();
+    has_values=tvt(true);
   }
-  
+
   void make_entry() override final
   {
-    cleanup_map.clear();
-    is_bottom=false;
+    make_top();
   }
 
   typedef union_find<irep_idt> aliasest;
@@ -80,9 +82,9 @@ class escape_domaint:public ai_domain_baset
   typedef std::map<irep_idt, cleanupt > cleanup_mapt;
   cleanup_mapt cleanup_map;
 
-  bool is_bottom;
-
 protected:
+  tvt has_values;
+
   void assign_lhs_cleanup(const exprt &, const std::set<irep_idt> &);
   void get_rhs_cleanup(const exprt &, std::set<irep_idt> &);
   void assign_lhs_aliases(const exprt &, const std::set<irep_idt> &);

src/analyses/global_may_alias.cpp

@@ -130,6 +130,8 @@ void global_may_alias_domaint::transform(
   ai_baset &ai,
   const namespacet &ns)
 {
+  if(has_values.is_false()) return;
+
   const goto_programt::instructiont &instruction=*from;
 
   switch(instruction.type)
@@ -179,6 +181,12 @@ void global_may_alias_domaint::output(
   const ai_baset &ai,
   const namespacet &ns) const
 {
+  if(has_values.is_known())
+  {
+    out << has_values.to_string() << '\n';
+    return;
+  }
+
   for(aliasest::const_iterator a_it1=aliases.begin();
       a_it1!=aliases.end();
       a_it1++)
@@ -218,7 +226,8 @@ bool global_may_alias_domaint::merge(
   locationt from,
   locationt to)
 {
-  bool changed=false;
+  bool changed=has_values.is_false();
+  has_values=tvt::unknown();
 
   // do union
   for(aliasest::const_iterator it=b.aliases.begin();

src/analyses/global_may_alias.h

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_ANALYSES_GLOBAL_MAY_ALIAS_H
 
 #include <util/numbering.h>
+#include <util/threeval.h>
 #include <util/union_find.h>
 
 #include "ai.h"
@@ -28,6 +29,10 @@ class global_may_alias_analysist;
 class global_may_alias_domaint:public ai_domain_baset
 {
 public:
+  global_may_alias_domaint():has_values(false)
+  {
+  }
+
   void transform(
     locationt from,
     locationt to,
@@ -47,23 +52,26 @@ class global_may_alias_domaint:public ai_domain_baset
   void make_bottom() final override
   {
     aliases.clear();
+    has_values=tvt(false);
   }
 
   void make_top() final override
   {
-    // We don't have a proper top.
-    assert(false);
+    aliases.clear();
+    has_values=tvt(true);
   }
 
   void make_entry() final override
   {
-    aliases.clear();
+    make_top();
   }
 
   typedef union_find<irep_idt> aliasest;
   aliasest aliases;
 
 protected:
+  tvt has_values;
+
   void assign_lhs_aliases(const exprt &, const std::set<irep_idt> &);
   void get_rhs_aliases(const exprt &, std::set<irep_idt> &);
   void get_rhs_aliases_address_of(const exprt &, std::set<irep_idt> &);