@@ -1726,12 +1726,61 @@ void taint_summarise_all_functions(
1726
1726
{
1727
1727
size_t processed = 0UL ;
1728
1728
size_t modelled = 0UL ;
1729
- size_t skipped = 0UL ;
1729
+ std::unordered_set<irep_idt> skipped;
1730
1730
1731
1731
const std::size_t topological_order_size =
1732
1732
program->get_inverted_functions_topological_order ().size ();
1733
1733
1734
1734
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
+
1735
1784
for (const auto &fn_name :
1736
1785
program->get_inverted_functions_topological_order ())
1737
1786
{
@@ -1743,7 +1792,7 @@ void taint_summarise_all_functions(
1743
1792
<< " ["
1744
1793
<< std::fixed << std::setprecision (1 ) << std::setw (5 )
1745
1794
<< (topological_order_size==0UL ?100.0 :
1746
- 100.0 *(double )(processed+skipped)/
1795
+ 100.0 *(double )(processed+skipped. size () )/
1747
1796
(double )topological_order_size)
1748
1797
<< " %] "
1749
1798
<< " TIMEOUT! ("
@@ -1765,7 +1814,7 @@ void taint_summarise_all_functions(
1765
1814
<< " ["
1766
1815
<< std::fixed << std::setprecision (1 ) << std::setw (5 )
1767
1816
<< (topological_order_size==0UL ?100.0 :
1768
- 100.0 *(double )(processed+skipped)/
1817
+ 100.0 *(double )(processed+skipped. size () )/
1769
1818
(double )topological_order_size)
1770
1819
<< " %] "
1771
1820
<< fn_name
@@ -1790,22 +1839,39 @@ void taint_summarise_all_functions(
1790
1839
<< " ["
1791
1840
<< std::fixed << std::setprecision (1 ) << std::setw (5 )
1792
1841
<< (topological_order_size==0UL ?100.0 :
1793
- 100.0 *(double )(processed+skipped)/
1842
+ 100.0 *(double )(processed+skipped. size () )/
1794
1843
(double )topological_order_size)
1795
1844
<< " %] Skipping"
1796
1845
<< (fn_it!=functions_map.cend () && !fn_it->second .body_available ()
1797
1846
? " [function without a body]" : " " )
1798
1847
<< " : "
1799
1848
<< fn_name
1800
1849
<< 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
+ }
1802
1868
}
1803
1869
}
1804
1870
log ->status ()
1805
1871
<< " [100.0%] Summarisation of functions has finished successfully ("
1806
1872
<< processed << " processed, "
1807
1873
<< modelled << " modelled, "
1808
- << skipped << " skipped)."
1874
+ << skipped. size () << " skipped)."
1809
1875
<< messaget::eom;
1810
1876
}
1811
1877
0 commit comments