perf(fixpoint): more move magic to reduce copies

seahorn · Apr 20, 2023 · 08b69f7 · 08b69f7
1 parent f224502
commit 08b69f7
Show file tree

Hide file tree

Showing 5 changed files with 22 additions and 12 deletions.
diff --git a/include/crab/analysis/abs_transformer.hpp b/include/crab/analysis/abs_transformer.hpp
@@ -368,8 +368,13 @@ class intra_abs_transformer
 
   void set_abs_value(abs_dom_t &&inv) { m_inv = std::move(inv); }
 
-  abs_dom_t get_abs_value() const { return m_inv; }
-  abs_dom_t &get_abs_value() { return m_inv; }
+  abs_dom_t &get_abs_value() {
+    return m_inv;
+  }
+
+  const abs_dom_t &get_abs_value() const {
+    return m_inv;
+  }
 
   virtual void exec(bin_op_t &stmt) override {
     bool pre_bot = false;

diff --git a/include/crab/analysis/fwd_analyzer.hpp b/include/crab/analysis/fwd_analyzer.hpp
@@ -86,7 +86,7 @@ class fwd_analyzer : public ikos::interleaved_fwd_fixpoint_iterator<
     for (auto &s : b) {
       s.accept(&*m_abs_tr);
     }
-    abs_dom_t &res = m_abs_tr->get_abs_value();
+    abs_dom_t res = std::move(m_abs_tr->get_abs_value());
     prune_dead_variables(node, res);
     return res;
   }

diff --git a/include/crab/checkers/assertion.hpp b/include/crab/checkers/assertion.hpp
@@ -73,7 +73,7 @@ class assert_property_checker : public property_checker<Analyzer> {
       crab::crab_string_os os;
       if (this->m_verbose >= 3) {
         os << "Property : " << cst << "\n";
-        auto &inv = this->m_abs_tr->get_abs_value();
+        auto const &inv = this->m_abs_tr->get_abs_value();
         os << "Invariant: " << inv << "\n";
         os << "Note: it was proven by the forward+backward analysis";
       }
@@ -84,15 +84,15 @@ class assert_property_checker : public property_checker<Analyzer> {
           crab::crab_string_os os;
           if (this->m_verbose >= 3) {
             os << "Property : " << cst << "\n";
-            auto &inv = this->m_abs_tr->get_abs_value();
+            auto const &inv = this->m_abs_tr->get_abs_value();
             os << "Invariant: " << inv;
           }
           this->add_safe(os.str(), &s);
         } else {
           crab::crab_string_os os;
           if (this->m_verbose >= 2) {
             os << "Property : " << cst << "\n";
-            auto &inv = this->m_abs_tr->get_abs_value();
+            auto const &inv = this->m_abs_tr->get_abs_value();
             os << "Invariant: " << inv;
           }
           this->add_warning(os.str(), &s);
@@ -105,7 +105,7 @@ class assert_property_checker : public property_checker<Analyzer> {
         return;
       }
 
-      const abs_dom_t &inv = this->m_abs_tr->get_abs_value();
+      auto const &inv = this->m_abs_tr->get_abs_value();
       if (entails(inv, cst)) {
         crab::crab_string_os os;
         if (this->m_verbose >= 3) {

diff --git a/include/crab/checkers/div_zero.hpp b/include/crab/checkers/div_zero.hpp
@@ -41,7 +41,7 @@ class div_zero_property_checker : public property_checker<Analyzer> {
     if (s.op() == cfg::BINOP_SDIV || s.op() == cfg::BINOP_UDIV ||
         s.op() == cfg::BINOP_SREM || s.op() == cfg::BINOP_UREM) {
 
-      auto &inv = this->m_abs_tr->get_abs_value();
+      auto const &inv = this->m_abs_tr->get_abs_value();
       if (inv.is_bottom()) {
         this->m_db.add(_UNREACH, s.get_debug_info());
         return;
@@ -56,7 +56,7 @@ class div_zero_property_checker : public property_checker<Analyzer> {
           this->m_db.add(_SAFE, s.get_debug_info());
         }
       } else if (auto var = divisor_expr.get_variable()) {
-        interval_t divisor_intv = inv[(*var)];
+        interval_t divisor_intv = inv.at(*var);
         if (auto divisor = divisor_intv.singleton()) {
           if (*divisor == number_t(0)) {
             lin_cst_t e_cst(*var != number_t(0));

diff --git a/include/crab/fixpoint/interleaved_fixpoint_iterator.hpp b/include/crab/fixpoint/interleaved_fixpoint_iterator.hpp
@@ -441,7 +441,7 @@ class wto_iterator : public wto_component_visitor<CFG> {
     }
   }
 
-  inline void compute_post(basic_block_label_t node, AbstractValue inv) {
+  inline void compute_post(AbstractValue &&inv, basic_block_label_t node) {
     { 
       FIXPOINT_SCOPED_STATS("Fixpo.computePost");
       CRAB_VERBOSE_IF(
@@ -452,12 +452,17 @@ class wto_iterator : public wto_component_visitor<CFG> {
         crab::outs() << " size=" << n.size() << "\n";);
 
       CRAB_VERBOSE_IF(4, crab::outs() << "PRE Invariants:\n" << inv << "\n");
-      inv = m_iterator->analyze(node, std::move(inv));
+      inv = std::move(m_iterator->analyze(node, std::move(inv)));
       CRAB_VERBOSE_IF(3, crab::outs() << "POST Invariants:\n" << inv << "\n");
     }
     m_iterator->set_post(node, std::move(inv));
   }
 
+  // inv passed by value because it will be used after the call to compute_post
+  inline void compute_post(basic_block_label_t node, AbstractValue inv) {
+    compute_post(std::move(inv), node);
+  }
+
   // Simple visitor to check if node is a member of the wto component.
   class member_component_visitor : public wto_component_visitor<CFG> {
     basic_block_label_t _node;
@@ -541,7 +546,7 @@ class wto_iterator : public wto_component_visitor<CFG> {
       m_iterator->set_pre(node, pre);
     }
 
-    compute_post(node, pre);
+    compute_post(std::move(pre), node);
   }
 
   virtual void visit(wto_cycle_t &cycle) override {