perf: avoid unnecessary copies

include/crab/analysis/bwd_analyzer.hpp

@@ -102,13 +102,14 @@ class necessary_preconditions_fixpoint_iterator
   }
 
   virtual void process_pre(const bb_label_t & /*node*/,
-                           AbsDom /*postcond*/) override {}
+                           const AbsDom &/*postcond*/) override {}
 
   /**
    *  Store necessary preconditions
    **/
-  virtual void process_post(const bb_label_t &node, AbsDom precond) override {
-    m_preconditions.insert(std::make_pair(node, precond));
+  virtual void process_post(const bb_label_t &node, const AbsDom &precond) override {
+    AbsDom copy_precond(precond);
+    m_preconditions.insert({node, std::move(copy_precond)});
   }
 
 public:

include/crab/analysis/fwd_analyzer.hpp

@@ -86,9 +86,9 @@ class fwd_analyzer : public ikos::interleaved_fwd_fixpoint_iterator<
     return res;
   }
 
-  void process_pre(const basic_block_label_t &node, abs_dom_t inv) override {}
+  void process_pre(const basic_block_label_t &node, const abs_dom_t &inv) override {}
 
-  void process_post(const basic_block_label_t &node, abs_dom_t inv) override {}
+  void process_post(const basic_block_label_t &node, const abs_dom_t &inv) override {}
 
   void init_fwd_analyzer() {
     assert(m_abs_tr);

include/crab/fixpoint/fixpoint_iterators_api.hpp

@@ -49,9 +49,9 @@ template <typename CFG, typename AbstractValue> class fixpoint_iterator {
   virtual AbstractValue analyze(const basic_block_label_t &,
                                 AbstractValue &&) = 0;
 
-  virtual void process_pre(const basic_block_label_t &, AbstractValue) = 0;
+  virtual void process_pre(const basic_block_label_t &, const AbstractValue&) = 0;
 
-  virtual void process_post(const basic_block_label_t &, AbstractValue) = 0;
+  virtual void process_post(const basic_block_label_t &, const AbstractValue&) = 0;
 
   virtual ~fixpoint_iterator() {}
 

include/crab/fixpoint/interleaved_fixpoint_iterator.hpp

@@ -145,8 +145,8 @@ class interleaved_fwd_fixpoint_iterator
     }
   }
 
-  inline AbstractValue get(const invariant_table_t &table,
-                           basic_block_label_t node) const {
+  inline const AbstractValue& get(const invariant_table_t &table,
+				  basic_block_label_t node) const {
     FIXPOINT_SCOPED_STATS("Fixpo.invLookup");
     return table.at(node);
   }
@@ -265,10 +265,10 @@ class interleaved_fwd_fixpoint_iterator
   const wto_t &get_wto() const { return m_wto; }
 
   /* Begin access methods for getting invariants */
-  AbstractValue get_pre(basic_block_label_t node) const {
+  const AbstractValue &get_pre(basic_block_label_t node) const {
     return get(m_pre, node);
   }
-  AbstractValue get_post(basic_block_label_t node) const {
+  const AbstractValue &get_post(basic_block_label_t node) const {
     return get(m_post, node);
   }
   const invariant_table_t &get_pre_invariants() const { return m_pre; }
@@ -405,7 +405,7 @@ class wto_iterator : public wto_component_visitor<CFG> {
 
   inline AbstractValue make_bottom() const { return m_absval_fac.make_bottom(); }
 
-  inline AbstractValue strengthen(basic_block_label_t n, AbstractValue inv) {
+  inline void strengthen(AbstractValue &inv, basic_block_label_t n) {
     FIXPOINT_SCOPED_STATS("Fixpo.strengthen");
 
     if (m_assumptions) {
@@ -414,12 +414,11 @@ class wto_iterator : public wto_component_visitor<CFG> {
         CRAB_VERBOSE_IF(3, crab::outs() << "Before assumption at " << n << ":"
                                         << inv << "\n");
 
-        inv = inv & it->second;
+        inv &= it->second;
         CRAB_VERBOSE_IF(3, crab::outs() << "After assumption at " << n << ":"
                                         << inv << "\n");
       }
     }
-    return inv;
   }
 
   inline void compute_post(basic_block_label_t node, AbstractValue inv) {
@@ -503,7 +502,7 @@ class wto_iterator : public wto_component_visitor<CFG> {
       pre = m_iterator->get_pre(node);
       if (m_assumptions && !m_assumptions->empty()) {
         // no necessary but it might avoid copies
-        pre = strengthen(node, pre);
+        strengthen(pre, node);
         m_iterator->set_pre(node, pre);
       }
     } else {
@@ -517,7 +516,7 @@ class wto_iterator : public wto_component_visitor<CFG> {
       }
       if (m_assumptions && !m_assumptions->empty()) {
         // no necessary but it might avoid copies
-        pre = strengthen(node, pre);
+        strengthen(pre, node);
       }
       m_iterator->set_pre(node, pre);
     }
@@ -590,8 +589,7 @@ class wto_iterator : public wto_component_visitor<CFG> {
       }
     }
     if (m_assumptions && !m_assumptions->empty()) {
-      // no necessary but it might avoid copies
-      pre = strengthen(head, pre);
+      strengthen(pre, head);
     }
 
     for (unsigned int iteration = 1;; ++iteration) {