Merge branch 'master' of github.com:diffblue/cbmc

Author: Daniel Kroening

src/analyses/ai.cpp

@@ -122,7 +122,7 @@ 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'.
-  get_state(goto_program.instructions.begin()).make_top();
+  get_state(goto_program.instructions.begin()).make_entry();
 }
 
 /*******************************************************************\

src/analyses/ai.h

@@ -54,19 +54,14 @@ class ai_domain_baset
   }
 
   // no states
-  virtual void make_bottom()
-  {
-  }
+  virtual void make_bottom()=0;
 
-  // all states
-  virtual void make_top()
-  {
-  }
+  // all states -- the analysis doesn't use this,
+  // and domains may refuse to implement it.
+  virtual void make_top()=0;
 
   // a reasonable entry-point state
-  virtual void make_entry()
-  {
-  }
+  virtual void make_entry()=0;
 
   // also add
   //
@@ -273,7 +268,7 @@ class ait:public ai_baset
     return it->second;
   }
 
-  virtual void clear()
+  virtual void clear() override
   {
     state_map.clear();
     ai_baset::clear();
@@ -284,33 +279,33 @@ class ait:public ai_baset
   state_mapt state_map;
 
   // this one creates states, if need be
-  virtual statet &get_state(locationt l)
+  virtual statet &get_state(locationt l) override
   {
     return state_map[l]; // calls default constructor
   }
 
   // this one just finds states
-  virtual const statet &find_state(locationt l) const
+  virtual const statet &find_state(locationt l) const override
   {
     typename state_mapt::const_iterator it=state_map.find(l);
     if(it==state_map.end()) throw "failed to find state";
     return it->second;
   }
 
-  virtual bool merge(const statet &src, locationt from, locationt to)
+  virtual bool merge(const statet &src, locationt from, locationt to) override
   {
     statet &dest=get_state(to);
     return static_cast<domainT &>(dest).merge(static_cast<const domainT &>(src), from, to);
   }
 
-  virtual statet *make_temporary_state(const statet &s)
+  virtual statet *make_temporary_state(const statet &s) override
   {
     return new domainT(static_cast<const domainT &>(s));
   }
 
   virtual void fixedpoint(
     const goto_functionst &goto_functions,
-    const namespacet &ns)
+    const namespacet &ns) override
   {
     sequential_fixedpoint(goto_functions, ns);
   }
@@ -324,7 +319,7 @@ class ait:public ai_baset
     const statet &src,
     goto_programt::const_targett from,
     goto_programt::const_targett to,
-    const namespacet &ns)
+    const namespacet &ns) override
   {
     throw "not implemented";
   }
@@ -345,7 +340,7 @@ class concurrency_aware_ait:public ait<domainT>
     const statet &src,
     goto_programt::const_targett from,
     goto_programt::const_targett to,
-    const namespacet &ns)
+    const namespacet &ns) override
   {
     statet &dest=this->get_state(to);
     return static_cast<domainT &>(dest).merge_shared(static_cast<const domainT &>(src), from, to, ns);
@@ -354,7 +349,7 @@ class concurrency_aware_ait:public ait<domainT>
 protected:
   virtual void fixedpoint(
     const goto_functionst &goto_functions,
-    const namespacet &ns)
+    const namespacet &ns) override
   {
     this->concurrent_fixedpoint(goto_functions, ns);
   }

src/analyses/constant_propagator.h

@@ -16,8 +16,11 @@ Author: Peter Schrammel
 class constant_propagator_domaint:public ai_domain_baset
 {
 public:
-  virtual void transform(locationt, locationt, ai_baset &, const namespacet &);
-  virtual void output(std::ostream &, const ai_baset &, const namespacet &) const;
+  void transform(locationt, locationt, ai_baset &, const namespacet &) override final;
+  void output(std::ostream &, const ai_baset &, const namespacet &) const override final;
+  void make_top() override final { values.set_to_top(); }
+  void make_bottom() override final { values.set_to_bottom(); }
+  void make_entry() override final { values.set_to_top(); }
   bool merge(const constant_propagator_domaint &, locationt, locationt);
 
   struct valuest

src/analyses/custom_bitvector_analysis.h

@@ -27,32 +27,31 @@ class custom_bitvector_analysist;
 class custom_bitvector_domaint:public ai_domain_baset
 {
 public:
-  virtual void transform(
+  void transform(
     locationt from,
     locationt to,
     ai_baset &ai,
-    const namespacet &ns);
+    const namespacet &ns) final override;
 
-  virtual void output(
+  void output(
     std::ostream &out,
     const ai_baset &ai,
-    const namespacet &ns) const;
+    const namespacet &ns) const final override;
 
-  virtual void make_bottom()
+  void make_bottom() final override
   {
     may_bits.clear();
     must_bits.clear();
     is_bottom=true;
   }
 
-  virtual void make_top()
+  void make_top() final override
   {
-    may_bits.clear();
-    must_bits.clear();
-    is_bottom=false;
+    // We don't have a proper top, and refuse to do this.
+    assert(false);
   }
 
-  virtual void make_entry()
+  void make_entry() final override
   {
     may_bits.clear();
     must_bits.clear();

src/analyses/dependence_graph.cpp

@@ -368,9 +368,9 @@ void dependence_grapht::add_dep(
   goto_programt::const_targett from,
   goto_programt::const_targett to)
 {
-  const unsigned n_from=state_map[from].get_node_id();
+  const node_indext n_from=state_map[from].get_node_id();
   assert(n_from<size());
-  const unsigned n_to=state_map[to].get_node_id();
+  const node_indext n_to=state_map[to].get_node_id();
   assert(n_to<size());
 
   // add_edge is redundant as the subsequent operations also insert

src/analyses/dependence_graph.h

@@ -20,56 +20,6 @@ Date: August 2013
 
 class dependence_grapht;
 
-class dep_graph_domaint:public ai_domain_baset
-{
-public:
-  dep_graph_domaint():node_id((unsigned)-1)
-  {
-  }
-
-  bool merge(
-    const dep_graph_domaint &src,
-    goto_programt::const_targett from,
-    goto_programt::const_targett to);
-
-  void transform(
-    goto_programt::const_targett from,
-    goto_programt::const_targett to,
-    ai_baset &ai,
-    const namespacet &ns);
-
-  virtual void output(
-      std::ostream &out,
-      const ai_baset &ai,
-      const namespacet &ns) const;
-
-  void set_node_id(unsigned id)
-  {
-    node_id=id;
-  }
-
-  unsigned get_node_id() const
-  {
-    return node_id;
-  }
-
-protected:
-  unsigned node_id;
-
-  typedef std::set<goto_programt::const_targett> depst;
-  depst control_deps, data_deps;
-
-  void control_dependencies(
-    goto_programt::const_targett from,
-    goto_programt::const_targett to,
-    dependence_grapht &dep_graph);
-  void data_dependencies(
-    goto_programt::const_targett from,
-    goto_programt::const_targett to,
-    dependence_grapht &dep_graph,
-    const namespacet &ns);
-};
-
 class dep_edget
 {
 public:
@@ -114,6 +64,76 @@ struct dep_nodet:public graph_nodet<dep_edget>
   goto_programt::const_targett PC;
 };
 
+class dep_graph_domaint:public ai_domain_baset
+{
+public:
+  typedef graph<dep_nodet>::node_indext node_indext;
+
+  dep_graph_domaint():
+    node_id(std::numeric_limits<node_indext>::max())
+  {
+  }
+
+  bool merge(
+    const dep_graph_domaint &src,
+    goto_programt::const_targett from,
+    goto_programt::const_targett to);
+
+  void transform(
+    goto_programt::const_targett from,
+    goto_programt::const_targett to,
+    ai_baset &ai,
+    const namespacet &ns) final override;
+
+  void output(
+    std::ostream &out,
+    const ai_baset &ai,
+    const namespacet &ns) const final override;
+    
+  void make_top() final override
+  {
+    node_id=std::numeric_limits<node_indext>::max();
+  }
+
+  void make_bottom() final override
+  {
+    node_id=std::numeric_limits<node_indext>::max();
+  }
+
+  void make_entry() final override
+  {
+    node_id=std::numeric_limits<node_indext>::max();
+  }
+
+  void set_node_id(node_indext id)
+  {
+    node_id=id;
+  }
+
+  node_indext get_node_id() const
+  {
+    assert(node_id!=std::numeric_limits<node_indext>::max());
+    return node_id;
+  }
+
+protected:
+  node_indext node_id;
+
+  typedef std::set<goto_programt::const_targett> depst;
+  depst control_deps, data_deps;
+
+  void control_dependencies(
+    goto_programt::const_targett from,
+    goto_programt::const_targett to,
+    dependence_grapht &dep_graph);
+
+  void data_dependencies(
+    goto_programt::const_targett from,
+    goto_programt::const_targett to,
+    dependence_grapht &dep_graph,
+    const namespacet &ns);
+};
+
 class dependence_grapht:
   public ait<dep_graph_domaint>,
   public graph<dep_nodet>
@@ -161,7 +181,7 @@ class dependence_grapht:
 
     if(entry.second)
     {
-      const unsigned node_id=add_node();
+      const node_indext node_id=add_node();
       entry.first->second.set_node_id(node_id);
       nodes[node_id].PC=l;
     }

src/analyses/escape_analysis.h

@@ -32,29 +32,35 @@ class escape_domaint:public ai_domain_baset
   {
   }
 
-  virtual void transform(
+  void transform(
     locationt from,
     locationt to,
     ai_baset &ai,
-    const namespacet &ns);
+    const namespacet &ns) override final;
 
-  virtual void output(
+  void output(
     std::ostream &out,
     const ai_baset &ai,
-    const namespacet &ns) const;
+    const namespacet &ns) const override final;
 
   bool merge(
     const escape_domaint &b,
     locationt from,
     locationt to);
 
-  void make_bottom()
+  void make_bottom() override final
   {
     cleanup_map.clear();
     is_bottom=true;
   }
 
-  void make_top()
+  void make_top() override final
+  {
+    // We don't have a proper top.
+    assert(false);
+  }
+  
+  void make_entry() override final
   {
     cleanup_map.clear();
     is_bottom=false;
@@ -68,6 +74,9 @@ class escape_domaint:public ai_domain_baset
     std::set<irep_idt> cleanup_functions;
   };
 
+  // We track a set of 'cleanup functions' for specific
+  // identifiers. The cleanup functions are executed
+  // once the last pointer to an object is lost.
   typedef std::map<irep_idt, cleanupt > cleanup_mapt;
   cleanup_mapt cleanup_map;