Machine learning support

src/analyses/dependence_graph.h

@@ -69,6 +69,7 @@ struct dep_nodet:public graph_nodet<dep_edget>
 class dep_graph_domaint:public ai_domain_baset
 {
 public:
+  typedef std::set<goto_programt::const_targett> depst;
   typedef grapht<dep_nodet>::node_indext node_indext;
 
   dep_graph_domaint():
@@ -111,6 +112,16 @@ class dep_graph_domaint:public ai_domain_baset
     data_deps.clear();
   }
 
+  const depst& get_control_deps()
+  {
+    return control_deps;
+  }
+
+  const depst& get_data_deps()
+  {
+    return data_deps;
+  }
+
   void make_entry() final
   {
     make_top();
@@ -131,7 +142,6 @@ class dep_graph_domaint:public ai_domain_baset
   tvt has_values;
   node_indext node_id;
 
-  typedef std::set<goto_programt::const_targett> depst;
   depst control_deps, data_deps;
 
   void control_dependencies(

src/goto-programs/goto_program_template.h

@@ -22,6 +22,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/symbol_table.h>
 #include <util/source_location.h>
 #include <util/std_expr.h>
+#include <util/irep_hash.h>
 
 typedef enum
 {
@@ -263,6 +264,11 @@ class goto_program_templatet
       instruction_id_builder << type;
       return instruction_id_builder.str();
     }
+
+    std::size_t stable_hash() const
+    {
+      return hash_combine(code.stable_hash(), guard.stable_hash());
+    }
   };
 
   typedef std::list<instructiont> instructionst;

src/solvers/prop/cover_goals.cpp

@@ -50,6 +50,7 @@ void cover_goalst::mark()
        prop_conv.l_get(g.condition).is_true())
     {
       g.status=goalt::statust::COVERED;
+      g.seconds=(current_time()-start_time);
       _number_covered++;
 
       // notify observers

src/solvers/prop/cover_goals.h

@@ -10,6 +10,7 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_SOLVERS_PROP_COVER_GOALS_H
 
 #include <util/message.h>
+#include <util/time_stopping.h>
 
 #include "prop_conv.h"
 
@@ -29,6 +30,7 @@ class cover_goalst:public messaget
   explicit cover_goalst(prop_convt &_prop_conv):
     prop_conv(_prop_conv)
   {
+    start_time=current_time();
   }
 
   virtual ~cover_goalst();
@@ -41,6 +43,7 @@ class cover_goalst:public messaget
   struct goalt
   {
     literalt condition;
+    time_periodt seconds;
     enum class statust { UNKNOWN, COVERED, UNCOVERED, ERROR } status;
 
     goalt():status(statust::UNKNOWN)
@@ -92,6 +95,7 @@ class cover_goalst:public messaget
   }
 
 protected:
+  absolute_timet start_time;
   std::size_t _number_covered;
   unsigned _iterations;
   prop_convt &prop_conv;

src/util/dstring.h

@@ -158,6 +158,12 @@ inline size_t hash_string(const dstringt &s)
   return s.hash();
 }
 
+inline size_t stable_hash_string(const dstringt &s)
+{
+  return hash_string(string_container.get_string(s.get_no()));
+}
+
+
 inline std::ostream &operator<<(std::ostream &out, const dstringt &a)
 {
   return a.operator<<(out);

src/util/irep.cpp

@@ -923,6 +923,49 @@ std::size_t irept::full_hash() const
 
 /*******************************************************************\
 
+Function: irept::stable_hash
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Stable hash, hashes the actual content of the string. 
+          Can be used to identify hashes across commits 
+          (of the target software)
+
+\*******************************************************************/
+
+std::size_t irept::stable_hash() const
+{
+  const irept::subt &sub=get_sub();
+  const irept::named_subt &named_sub=get_named_sub();
+  const irept::named_subt &comments=get_comments();
+
+  std::size_t result=stable_hash_string(id());
+
+  forall_irep(it, sub) result=hash_combine(result, it->full_hash());
+
+  forall_named_irep(it, named_sub)
+  {
+    result=hash_combine(result, stable_hash_string(it->first));
+    result=hash_combine(result, it->second.full_hash());
+  }
+
+  forall_named_irep(it, comments)
+  {
+    result=hash_combine(result, stable_hash_string(it->first));
+    result=hash_combine(result, it->second.full_hash());
+  }
+
+  result=hash_finalize(
+    result,
+    named_sub.size()+sub.size()+comments.size());
+
+  return result;
+}
+
+/*******************************************************************\
+
 Function: indent
 
   Inputs:

src/util/irep.h

@@ -252,6 +252,7 @@ class irept
 
   std::size_t hash() const;
   std::size_t full_hash() const;
+  std::size_t stable_hash() const;
 
   bool full_eq(const irept &other) const;
 

src/util/source_location.cpp

@@ -10,6 +10,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "source_location.h"
 #include "file_util.h"
+#include "prefix.h"
 
 /*******************************************************************\