Require bottom/top to be implemented by ai domains

Domains without bottom would not be able to distinguish states being
uninitialized from ones being empty/the smallest element. Thus even the
very first merge into such a state possibly had no effect, which in turn
would cause functions not being entered. Thus effects, such as
assignments to global variables, would not be seen.

Als use and enforce the implementation of make_entry.
ai_baset::entry_point now uses make_entry; implementations may still use
make_top to implement make_entry.

Fixes #325

Author: tautschnig

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();
 }
 

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> &);