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 const_hash() const
+    {
+      return hash_combine(code.const_hash(), guard.const_hash());
+    }
   };
 
   typedef std::list<instructiont> instructionst;

src/langapi/language_ui.cpp

@@ -14,6 +14,9 @@ Author: Daniel Kroening, [email protected]
 #include <util/language.h>
 #include <util/cmdline.h>
 #include <util/unicode.h>
+#include <util/mp_arith.h>
+#include <util/arith_tools.h>
+#include <util/std_types.h>
 
 #include "language_ui.h"
 #include "mode.h"
@@ -345,3 +348,107 @@ void language_uit::show_symbol_table_plain(
     out << '\n' << std::flush;
   }
 }
+
+/*******************************************************************\
+
+Function: language_uit::build_array_from_static_symbol_table
+
+  Inputs: out - maps variable names to types
+
+ Outputs: N/A
+
+ Purpose: builds a list of static variables and maps them to types
+
+\*******************************************************************/
+void language_uit::build_array_from_static_symbol_table(
+    std::map<std::string, std::string>& out)
+{
+  const namespacet ns(symbol_table);
+
+  std::set<std::string> symbols;
+  forall_symbols(it, symbol_table.symbols)
+    symbols.insert(id2string(it->first));
+
+  for(const std::string &id : symbols)
+  {
+    const symbolt &symbol=ns.lookup(id);
+    languaget *ptr;
+    if(symbol.mode=="")
+      ptr=get_default_language();
+    else
+    {
+      ptr=get_language_from_mode(symbol.mode);
+      if(ptr == nullptr)
+        throw "symbol "+id2string(symbol.name)+" has unknown mode";
+    }
+
+    std::unique_ptr<languaget> p(ptr);
+    std::string type_str;
+    std::string value_str;
+
+    if(symbol.type.is_not_nil())
+      p->from_type(symbol.type, type_str, ns);
+
+    if(symbol.value.is_not_nil())
+      p->from_expr(symbol.value, value_str, ns);
+
+    if((symbol.is_static_lifetime) && (!symbol.location.is_built_in()))
+    {
+      const typet type = ns.follow(symbol.type);
+      std::stringstream buffer;
+      buffer << symbol.base_name;
+      build_entry(ns, type, p, buffer.str(), out);
+    }
+  }
+}
+
+/*******************************************************************\
+
+Function: language_uit::build_entry
+
+  Inputs: 
+
+ Outputs: N/A
+
+ Purpose: Retrieves the names and types of static variable
+          Recursively handles arrays and structures
+
+\*******************************************************************/
+void language_uit::build_entry(const namespacet ns,
+    const typet type,
+    std::unique_ptr<languaget> &p,
+    const std::string name,
+    std::map<std::string, std::string> &out)
+{
+  if(type.id() == ID_array)
+  {
+    const exprt &size_expr=static_cast<const exprt &>(type.find(ID_size));
+    mp_integer mp_count;
+    to_integer(size_expr, mp_count);
+    unsigned count=integer2unsigned(mp_count);
+    for(unsigned int i=0; i<count; i++)
+    {
+      std::stringstream buffer;
+      buffer << name  << "[" << i << "]";
+      build_entry(ns, ns.follow(type.subtype()), p, buffer.str(), out);
+    }
+  }
+  else if(type.id() == ID_struct)
+  {
+    const struct_typet &struct_type=to_struct_type(type);
+    const struct_typet::componentst &components=struct_type.components();
+    for(struct_typet::componentst::const_iterator it=components.begin();
+        it!=components.end(); ++it)
+    {
+      std::stringstream buffer;
+      buffer << name << "." << it->get_name();
+      build_entry(ns, ns.follow(type.subtype()), p, buffer.str(), out);
+    }
+  }
+  else
+  {
+    std::string type_str;
+    p->from_type(type, type_str, ns);
+    out.insert({name, type_str});
+  }
+}

src/langapi/language_ui.h

@@ -13,6 +13,10 @@ Author: Daniel Kroening, [email protected]
 #include <util/language_file.h>
 #include <util/symbol_table.h>
 #include <util/ui_message.h>
+#include <util/namespace.h>
+#include <map>
+#include <string>
+#include <memory>
 
 class cmdlinet;
 
@@ -41,6 +45,15 @@ class language_uit:public messaget
   virtual void show_symbol_table_plain(std::ostream &out, bool brief);
   virtual void show_symbol_table_xml_ui(bool brief);
 
+  virtual void build_array_from_static_symbol_table(
+      std::map<std::string, std::string>& out);
+  virtual void build_entry(
+      const namespacet ns,
+      const typet type,
+      std::unique_ptr<languaget> &p,
+      const std::string name,
+      std::map<std::string, std::string>& out);
+
   typedef ui_message_handlert::uit uit;
 
   uit get_ui()

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 const_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,47 @@ std::size_t irept::full_hash() const
 
 /*******************************************************************\
 
+Function: irept::const_hash
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+std::size_t irept::const_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=const_hash_string(id());
+
+  forall_irep(it, sub) result=hash_combine(result, it->full_hash());
+
+  forall_named_irep(it, named_sub)
+  {
+    result=hash_combine(result, const_hash_string(it->first));
+    result=hash_combine(result, it->second.full_hash());
+  }
+
+  forall_named_irep(it, comments)
+  {
+    result=hash_combine(result, const_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 const_hash() const;
 
   bool full_eq(const irept &other) const;
 

src/util/source_location.h

@@ -138,6 +138,16 @@ class source_locationt:public irept
     return get_bool(ID_hide);
   }
 
+  inline bool is_built_in() const
+  {
+    std::string file=get_file().c_str();
+    std::string built_in="<built-in-";//as in "<built-in-additions>";
+    std::string built_in2="<builtin-";//as in "<builtin-architecture-strings>";
+    bool is_built_in=!file.compare(0,built_in.length(),built_in);
+    is_built_in|=!file.compare(0,built_in2.length(),built_in2);
+    return is_built_in;
+  }
+
   static const source_locationt &nil()
   {
     return static_cast<const source_locationt &>(get_nil_irep());