Merge pull request diffblue#505 from diffblue/feature/in-memory-lvsa-summaries

In-memory LVSA summaries

Author: NathanJPhillips

src/driver/sec_driver_parse_options.cpp

@@ -349,9 +349,7 @@ int sec_driver_parse_optionst::doit()
       return CPROVER_EXIT_USAGE_ERROR;
     }
 
-    json_map_serializert<irep_idt, lvsaa_single_external_set_summaryt>
-      serializer(dbpath, id2string, get_message_handler());
-    local_value_set_analysist::dbt summarydb(serializer, 30);
+    local_value_set_analysist::dbt summarydb;
     namespacet ns(goto_model.symbol_table);
 
     // The last parameter of LVSA's constructor creates LVSA in debug mode,

src/pointer-analysis/local_value_set_analysis.h

@@ -6,14 +6,14 @@
 #ifndef LOCAL_VALUE_SET_ANALYSIS_H
 #define LOCAL_VALUE_SET_ANALYSIS_H
 
-#include <pointer-analysis/value_set_analysis.h>
 #include "local_value_set.h"
 #include "local_value_set_domain.h"
+#include <goto-programs/class_hierarchy.h>
 #include <pointer-analysis/external_value_set_expr.h>
+#include <pointer-analysis/value_set_analysis.h>
 #include <summaries/summary.h>
+#include <util/in_memory_map.h>
 #include <util/message.h>
-#include <util/cached_map.h>
-#include <goto-programs/class_hierarchy.h>
 
 /// Represents a local-value-set-analysis function summary.
 /// This is a set of simultaneous assignments, of the form:
@@ -134,7 +134,7 @@ class local_value_set_analysist
 {
 public:
   typedef value_set_analysis_templatet<local_value_set_domaint> baset;
-  typedef cached_mapt<irep_idt, lvsaa_single_external_set_summaryt> dbt;
+  typedef in_memory_mapt<irep_idt, lvsaa_single_external_set_summaryt> dbt;
 
   /// Counts calls to `transform_function_stub`
   size_t nstubs;

src/taint-analysis/taint_security_scanner.cpp

@@ -111,13 +111,7 @@ bool taint_do_security_scan(
   std::shared_ptr<taint_serializer_traitst> traits =
     std::make_shared<taint_serializer_traitst>(numbering, named_tokens);
 
-  json_map_serializert<irep_idt, lvsaa_single_external_set_summaryt>
-    lvsa_serializer(
-      config.get_lvsa_summaries_root_directory(),
-      id2string,
-      logger.get_message_handler());
-  lvsa_serializer.set_traits(traits);
-  local_value_set_analysist::dbt lvsa_summaries(lvsa_serializer, 100000);
+  local_value_set_analysist::dbt lvsa_summaries;
 
   statistics.end_loading_lvsa_database();
 

src/util/cached_map.h

@@ -212,7 +212,7 @@ class cached_mapt final
   Class: gen_iteratort
 
   Purpose:
-    An iterator implementation for cached_map.
+    An iterator implementation for cached_mapt.
 
   \*******************************************************************/
   template<bool is_const>

src/util/in_memory_map.h

@@ -0,0 +1,196 @@
+// Copyright 2016-2017 Diffblue Limited. All Rights Reserved.
+
+/// \file
+/// A map-like data structure that holds all entries in memory and implements
+/// the same interface as cached_mapt.
+
+#ifndef CPROVER_UTIL_IN_MEMORY_MAP_H
+#define CPROVER_UTIL_IN_MEMORY_MAP_H
+
+#include "virtual_map.h"
+#include <boost/range/adaptor/map.hpp>
+#include <map>
+#include <memory>
+
+/// A map that holds all entries in memory and implements the same interface as
+/// cached_mapt
+/// \tparam keyt: The type of keys of the map.
+/// \tparam valuet: The type of values of the map.
+template <typename keyt, typename valuet>
+class in_memory_mapt final
+{
+public:
+  // NOLINTNEXTLINE(readability/identifiers)  - name matches those used in STL
+  typedef keyt key_type;
+  // NOLINTNEXTLINE(readability/identifiers)  - name matches those used in STL
+  typedef valuet mapped_type;
+  // NOLINTNEXTLINE(readability/identifiers)  - name matches those used in STL
+  typedef std::pair<const key_type, std::shared_ptr<mapped_type>> value_type;
+  // NOLINTNEXTLINE(readability/identifiers)  - name matches those used in STL
+  typedef value_type &reference;
+  // NOLINTNEXTLINE(readability/identifiers)  - name matches those used in STL
+  typedef const value_type &const_reference;
+  // NOLINTNEXTLINE(readability/identifiers)  - name matches those used in STL
+  typedef value_type *pointer;
+  // NOLINTNEXTLINE(readability/identifiers)  - name matches those used in STL
+  typedef const value_type *const_pointer;
+  typedef std::unordered_map<key_type, std::shared_ptr<mapped_type>> storet;
+  // NOLINTNEXTLINE(readability/identifiers)  - name matches those used in STL
+  typedef typename storet::size_type size_type;
+
+private:
+  mutable storet store;
+
+private:
+  in_memory_mapt(const in_memory_mapt &) = delete;
+  in_memory_mapt &operator=(const in_memory_mapt &) = delete;
+
+public:
+  /// Creates a in_memory_mapt.
+  in_memory_mapt()
+  {
+  }
+
+  /// Returns the size of the cache.
+  /// \returns The size of the cache.
+  size_type cache_size() const
+  {
+    return store.size();
+  }
+
+  /// Returns the number of locked elements, equal to the size in this class.
+  /// \returns The number of locked elements.
+  size_type locked_count() const
+  {
+    return store.size();
+  }
+
+  /// Returns the size of the map.
+  /// \returns The size of the map.
+  size_type size() const
+  {
+    return store.size();
+  }
+
+  /// Returns all the keys in the map.
+  /// \returns The set of all keys in the map.
+  typename virtual_mapt<key_type, mapped_type>::keys_ranget keys() const
+  {
+    return store.keys();
+  }
+
+  // NOLINTNEXTLINE(readability/identifiers)  - name matches those used in STL
+  typedef typename storet::iterator iterator;
+  // NOLINTNEXTLINE(readability/identifiers)  - name matches those used in STL
+  typedef typename storet::const_iterator const_iterator;
+
+  iterator begin()
+  {
+    return store.begin();
+  }
+
+  iterator end()
+  {
+    return store.end();
+  }
+
+  const_iterator begin() const
+  {
+    return store.begin();
+  }
+
+  const_iterator end() const
+  {
+    return store.end();
+  }
+
+  /// Checks whether a given key exists in the map.
+  /// \param key: The key to search for.
+  /// \returns True if the map contains the given key.
+  bool contains(const key_type &key) const
+  {
+    return store.count(key) != 0;
+  }
+
+  /// Adds a key-value pair to the map.
+  /// \param key: The key of the key-value pair to add.
+  /// \param value: The value of the key-value pair to add.
+  /// \returns
+  ///   A pair, the first element of which is a shared_pointer to the value
+  ///   corresponding to key now in the map and the second element of which
+  ///   is true if and only if the key did not already exist in the map and the
+  ///   new element has been added.
+  /// \remarks
+  ///   If the value argument is an r-value at the call site it will be moved
+  ///   into the cache. Otherwise you need a copy constructor on mapped_type.
+  std::pair<std::shared_ptr<mapped_type>, bool> insert(
+    const key_type &key, mapped_type value)
+  {
+    auto it = store.find(key);
+    if(it != store.end())
+      return { it->second, false };
+    // Create and return shared pointer
+    std::shared_ptr<mapped_type> elt_shared_ptr =
+      std::make_shared(std::move(value));
+    store.insert({ key, elt_shared_ptr });
+    return { elt_shared_ptr, true };
+  }
+
+  /// Gets the value corresponding to a given key, inserting a new key-value
+  /// pair if one does not already exist.
+  /// \param key: The key to search for.
+  /// \returns A shared_pointer to the corresponding to the given key.
+  /// \remarks Requires a default constructor on mapped_type.
+  std::shared_ptr<mapped_type> operator[](const key_type &key)
+  {
+    auto it = store.find(key);
+    if(it != store.end())
+      return it->second;
+    // Create and return shared pointer
+    auto elt_shared_ptr = std::make_shared<mapped_type>();
+    store.insert({ key, elt_shared_ptr });
+    return elt_shared_ptr;
+  }
+
+  /// Gets the value corresponding to a given key.
+  /// \param key: The key to search for.
+  /// \returns A shared_pointer to the value corresponding to the given key.
+  std::shared_ptr<mapped_type> at(const key_type &key) const
+  {
+    return store.at(key);
+  }
+
+  /// Removes a key-value pair from the map.
+  /// \param key: The key of the key-value pair to remove.
+  /// \returns Whether the key-value pair could be deleted.
+  /// \remarks: If this function returns false, no changes are made to the map.
+  bool erase(const key_type &key)
+  {
+    store.erase(key);
+    return true;
+  }
+
+  /// Removes all key-value pairs from the map.
+  /// \returns Whether the map could be cleared.
+  /// \remarks: If this function returns false, no changes are made to the map.
+  bool clear()
+  {
+    store.clear();
+    return true;
+  }
+
+  /// No effect in this class.
+  void flush()
+  {
+  }
+
+  /// Totally removes an element from the map.
+  /// \param key: A key whose corresponding value should be unloaded.
+  /// \returns True, if the referenced element was unloaded, and false otherwise.
+  bool unload(const key_type &key)
+  {
+    return erase(key);
+  }
+};
+
+#endif