@@ -1726,12 +1726,61 @@ void taint_summarise_all_functions(
17261726{
17271727 size_t processed = 0UL ;
17281728 size_t modelled = 0UL ;
1729- size_t skipped = 0UL ;
1729+ std::unordered_set<irep_idt> skipped;
17301730
17311731 const std::size_t topological_order_size =
17321732 program->get_inverted_functions_topological_order ().size ();
17331733
17341734 auto start_time=std::chrono::high_resolution_clock::now ();
1735+
1736+ // In the map 'lvsadb_flush_ref_counts' there we store for each function
1737+ // in the inverted topological order two information:
1738+ // - reference count (how many callers the function has)
1739+ // - names of the callees
1740+ // where both information are considered w.r.t. the inverted topological
1741+ // order. Namely, considered are only recursive calls to predecessors in the
1742+ // topological order.
1743+ // We use the map for unloading not needed LVSA summaries from the memory
1744+ // (but they are saved on the disk). An LVSA summary of a given function
1745+ // is not needed at a given position in the inverted topological order of
1746+ // functions, if none of the remaining function (i.e. those after the position
1747+ // in the order) is a caller of the given function w.r.t the inverted
1748+ // topological order.
1749+ typedef std::pair<std::size_t , std::unordered_set<irep_idt>>
1750+ refcount_and_calleest;
1751+ std::unordered_map<irep_idt, refcount_and_calleest> lvsadb_flush_ref_counts;
1752+ for (const auto &fn_name :
1753+ program->get_inverted_functions_topological_order ())
1754+ {
1755+ const auto self_it =
1756+ lvsadb_flush_ref_counts.insert ({fn_name, {0UL , {}}}).first ;
1757+ const auto node =
1758+ *program->get_directed_call_graph ().get_node_index (fn_name);
1759+ for (const auto &succ_node :
1760+ program->get_directed_call_graph ().get_successors (node))
1761+ {
1762+ const auto &callee_name =
1763+ program->get_directed_call_graph ()[succ_node].function ;
1764+ if (callee_name != fn_name) // Skip direct recursion.
1765+ {
1766+ auto it = lvsadb_flush_ref_counts.find (callee_name);
1767+ if (it != lvsadb_flush_ref_counts.end ()) // Skip indirect recursion.
1768+ {
1769+ it->second .first += 1UL ;
1770+ self_it->second .second .insert (callee_name);
1771+ }
1772+ }
1773+ }
1774+ }
1775+ for (auto &elem : lvsadb_flush_ref_counts)
1776+ {
1777+ if (elem.second .first == 0UL ) // No caller -> unload yourself
1778+ {
1779+ elem.second .first = 1UL ;
1780+ elem.second .second .insert (elem.first );
1781+ }
1782+ }
1783+
17351784 for (const auto &fn_name :
17361785 program->get_inverted_functions_topological_order ())
17371786 {
@@ -1743,7 +1792,7 @@ void taint_summarise_all_functions(
17431792 << " ["
17441793 << std::fixed << std::setprecision (1 ) << std::setw (5 )
17451794 << (topological_order_size==0UL ?100.0 :
1746- 100.0 *(double )(processed+skipped)/
1795+ 100.0 *(double )(processed+skipped. size () )/
17471796 (double )topological_order_size)
17481797 << " %] "
17491798 << " TIMEOUT! ("
@@ -1765,7 +1814,7 @@ void taint_summarise_all_functions(
17651814 << " ["
17661815 << std::fixed << std::setprecision (1 ) << std::setw (5 )
17671816 << (topological_order_size==0UL ?100.0 :
1768- 100.0 *(double )(processed+skipped)/
1817+ 100.0 *(double )(processed+skipped. size () )/
17691818 (double )topological_order_size)
17701819 << " %] "
17711820 << fn_name
@@ -1790,22 +1839,39 @@ void taint_summarise_all_functions(
17901839 << " ["
17911840 << std::fixed << std::setprecision (1 ) << std::setw (5 )
17921841 << (topological_order_size==0UL ?100.0 :
1793- 100.0 *(double )(processed+skipped)/
1842+ 100.0 *(double )(processed+skipped. size () )/
17941843 (double )topological_order_size)
17951844 << " %] Skipping"
17961845 << (fn_it!=functions_map.cend () && !fn_it->second .body_available ()
17971846 ? " [function without a body]" : " " )
17981847 << " : "
17991848 << fn_name
18001849 << messaget::eom;
1801- ++skipped;
1850+ skipped.insert (fn_name);
1851+ }
1852+
1853+ for (auto &succ : lvsadb_flush_ref_counts.at (fn_name).second )
1854+ {
1855+ auto &elem = lvsadb_flush_ref_counts.at (succ);
1856+ if (elem.first > 0UL )
1857+ {
1858+ --elem.first ;
1859+ if (elem.first == 0UL )
1860+ {
1861+ const bool unloaded = lvsa_db.unload (succ);
1862+ INVARIANT (unloaded || skipped.count (succ) != 0UL ,
1863+ " Either the LVSA summary was unloaded or there was "
1864+ " nothing to unload (the summary computation was "
1865+ " skipped)." );
1866+ }
1867+ }
18021868 }
18031869 }
18041870 log->status ()
18051871 << " [100.0%] Summarisation of functions has finished successfully ("
18061872 << processed << " processed, "
18071873 << modelled << " modelled, "
1808- << skipped << " skipped)."
1874+ << skipped. size () << " skipped)."
18091875 << messaget::eom;
18101876}
18111877
0 commit comments