Unload of LVSA summaries on demand using refcounting.

Author: marek-trtik

src/taint-analysis/taint_summary.cpp

@@ -1726,12 +1726,48 @@ void taint_summarise_all_functions(
 {
   size_t processed = 0UL;
   size_t modelled = 0UL;
-  size_t skipped = 0UL;
+  std::unordered_set<irep_idt> skipped;
 
   const std::size_t topological_order_size =
     program->get_inverted_functions_topological_order().size();
 
   auto start_time=std::chrono::high_resolution_clock::now();
+
+  typedef std::pair<std::size_t, std::unordered_set<irep_idt>>
+          refcount_and_calleest;
+  std::unordered_map<irep_idt, refcount_and_calleest> lvsadb_flush_ref_counts;
+  for(const auto &fn_name :
+    program->get_inverted_functions_topological_order())
+  {
+    const auto self_it =
+      lvsadb_flush_ref_counts.insert({fn_name, {0UL, {}}}).first;
+    const auto node =
+      *program->get_directed_call_graph().get_node_index(fn_name);
+    for(const auto &succ_node :
+      program->get_directed_call_graph().get_successors(node))
+    {
+      const auto &callee_name =
+        program->get_directed_call_graph()[succ_node].function;
+      if(callee_name != fn_name) // Skip direct recursion.
+      {
+        auto it = lvsadb_flush_ref_counts.find(callee_name);
+        if(it != lvsadb_flush_ref_counts.end()) // Skip indirect recursion.
+        {
+          it->second.first += 1UL;
+          self_it->second.second.insert(callee_name);
+        }
+      }
+    }
+  }
+  for(auto &elem : lvsadb_flush_ref_counts)
+  {
+    if(elem.second.first == 0UL) // No caller -> unload yourself
+    {
+      elem.second.first = 1UL;
+      elem.second.second.insert(elem.first);
+    }
+  }
+
   for(const auto &fn_name :
     program->get_inverted_functions_topological_order())
   {
@@ -1743,7 +1779,7 @@ void taint_summarise_all_functions(
         << "["
         << std::fixed << std::setprecision(1) << std::setw(5)
         << (topological_order_size==0UL?100.0:
-              100.0*(double)(processed+skipped)/
+              100.0*(double)(processed+skipped.size())/
                     (double)topological_order_size)
         << "%] "
         << " TIMEOUT! ("
@@ -1765,7 +1801,7 @@ void taint_summarise_all_functions(
         << "["
         << std::fixed << std::setprecision(1) << std::setw(5)
         << (topological_order_size==0UL?100.0:
-              100.0*(double)(processed+skipped)/
+              100.0*(double)(processed+skipped.size())/
                     (double)topological_order_size)
         << "%] "
         << fn_name
@@ -1790,22 +1826,40 @@ void taint_summarise_all_functions(
         << "["
         << std::fixed << std::setprecision(1) << std::setw(5)
         << (topological_order_size==0UL?100.0:
-              100.0*(double)(processed+skipped)/
+              100.0*(double)(processed+skipped.size())/
                     (double)topological_order_size)
         << "%] Skipping"
         << (fn_it!=functions_map.cend() && !fn_it->second.body_available()
           ? " [function without a body]" : "")
         << ": "
         << fn_name
         << messaget::eom;
-      ++skipped;
+      skipped.insert(fn_name);
+    }
+
+    for(auto &succ : lvsadb_flush_ref_counts.at(fn_name).second)
+    {
+      auto &elem = lvsadb_flush_ref_counts.at(succ);
+      if(elem.first > 0UL)
+      {
+        --elem.first;
+        if(elem.first == 0UL)
+        {
+          std::cout << "@@@   Trying to flush: " << succ << std::endl;
+          const bool unloaded = lvsa_db.unload(succ);
+          INVARIANT(unloaded || skipped.count(succ) != 0UL,
+                    "Either the LVSA summary was unloaded or there was "
+                    "nothing to unload (the summary computation was "
+                    "skipped).");
+        }
+      }
     }
   }
   log->status()
     << "[100.0%] Summarisation of functions has finished successfully ("
     << processed << " processed, "
     << modelled << " modelled, "
-    << skipped << " skipped)."
+    << skipped.size() << " skipped)."
     << messaget::eom;
 }