Local bitvector analysis: reduce number of node visits

By using a set instead of a stack as work queue we reduce the number of
visits to each node in two ways:
1) The work queue will not contain duplicate nodes.
2) When dequeuing successor nodes, back edges will be given preference
over forward ones. Once the later (in program order) node is visited,
more information is already merged into the abstract state.

On a goto function with 160822 instruction, this reduces processing time
(just the local bitvector analysis) from 1700 seconds down to 72
seconds. The number of invocations of `local_bitvector_analysist::merge`
previously was 32815499 (204 times the number of nodes), and is now
997083 (6 times the number of nodes).

Author: tautschnig

src/analyses/local_bitvector_analysis.cpp

@@ -242,8 +242,8 @@ void local_bitvector_analysist::build()
   if(cfg.nodes.empty())
     return;
 
-  work_queuet work_queue;
-  work_queue.push(0);
+  std::set<unsigned> work_queue;
+  work_queue.insert(0);
 
   loc_infos.resize(cfg.nodes.size());
 
@@ -258,10 +258,10 @@ void local_bitvector_analysist::build()
 
   while(!work_queue.empty())
   {
-    unsigned loc_nr=work_queue.top();
+    unsigned loc_nr = *work_queue.begin();
     const local_cfgt::nodet &node=cfg.nodes[loc_nr];
     const goto_programt::instructiont &instruction=*node.t;
-    work_queue.pop();
+    work_queue.erase(work_queue.begin());
 
     auto &loc_info_src=loc_infos[loc_nr];
     auto loc_info_dest=loc_infos[loc_nr];
@@ -338,7 +338,7 @@ void local_bitvector_analysist::build()
     {
       assert(succ<loc_infos.size());
       if(merge(loc_infos[succ], (loc_info_dest)))
-        work_queue.push(succ);
+        work_queue.insert(succ);
     }
   }
 }

src/analyses/local_bitvector_analysis.h

@@ -12,8 +12,6 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_ANALYSES_LOCAL_BITVECTOR_ANALYSIS_H
 #define CPROVER_ANALYSES_LOCAL_BITVECTOR_ANALYSIS_H
 
-#include <stack>
-
 #include <util/expanding_vector.h>
 #include <util/numbering.h>
 
@@ -182,8 +180,6 @@ class local_bitvector_analysist
   const namespacet &ns;
   void build();
 
-  typedef std::stack<unsigned> work_queuet;
-
   numberingt<irep_idt> pointers;
 
   // pointers -> flagst