perf(varname): avoid calls to + and copies with std::string

include/crab/analysis/inter/bottom_up_inter_analyzer.hpp

@@ -151,17 +151,24 @@ template <typename CFG, typename AbsDomain> class summary {
     m_internal_inputs.reserve(m_inputs.size());
     m_internal_outputs.reserve(m_outputs.size());
 
-    std::string prefix = "$";
     unsigned i = 0;
     for (auto v : m_inputs) {
       auto &vfac = const_cast<varname_t *>(&(v.name()))->get_var_factory();
-      variable_t fresh_v(vfac.get(prefix + std::to_string(i)), v.get_type());
+      std::string arg_name;
+      arg_name.reserve(5+2); // expect 99999 arguments as max + 1 ($) + 1
+      arg_name.append("$");      
+      arg_name.append(std::to_string(i));
+      variable_t fresh_v(vfac.make_varname(std::move(arg_name)), v.get_type());
       m_internal_inputs.push_back(fresh_v);
       i++;
     }
     for (auto v : m_outputs) {
       auto &vfac = const_cast<varname_t *>(&(v.name()))->get_var_factory();
-      variable_t fresh_v(vfac.get(prefix + std::to_string(i)), v.get_type());
+      std::string arg_name;
+      arg_name.reserve(5+2); // expect 99999 arguments as max + 1 ($) + 1
+      arg_name.append("$");      
+      arg_name.append(std::to_string(i));
+      variable_t fresh_v(vfac.make_varname(std::move(arg_name)), v.get_type());
       m_internal_outputs.push_back(fresh_v);
       i++;
     }

include/crab/domains/array_adaptive.hpp

@@ -30,17 +30,14 @@
  *   variable. This is managed by cell_ghost_man.
  *
  * - Ghost variables are created by the same variable factory used to
- *   generate the CrabIR. We don't reuse ghost variables so there is a
- *   small risk of running out of ghost variables. If that happens, a
- *   runtime error will be reported.
+ *   generate the CrabIR. 
  *
- * - POSSIBLE BREAK OF MODULARITY of the base domain: A more important
- *   issue is that currently we pass ghost scalar variables to the
- *   base domain that can change during the analysis. If the base
- *   domain uses these ghost variables to create new ghost variables
- *   we will get into trouble. Currently, these ghost scalars are
- *   passed directly to boolean/numerical abstract domains so we
- *   should be fine with current Crab domains because they don't
+ * - POSSIBLE BREAK OF MODULARITY of the base domain: the adaptive
+ *   array domain passes ghost scalar variables to the base domain. If
+ *   the base domain uses these ghost variables to create new ghost
+ *   variables we will get into trouble. Currently, these ghost
+ *   scalars are passed directly to boolean/numerical abstract domains
+ *   so we should be fine with current Crab domains because they don't
  *   create ghost variables but this needs to be revisited anytime a
  *   new domain is plugin.
  ******************************************************************************/
@@ -626,7 +623,7 @@ template <typename Domain> class cell_ghost_man {
     std::string vname = mk_scalar_name(a.name(), c.get_offset(), c.get_size());
     variable_type_kind vtype_kind = get_array_element_type(a.get_type());
     variable_t scalar_var(
-        vfac.get(vname), vtype_kind,
+	vfac.make_varname(std::move(vname)), vtype_kind,
         (vtype_kind == BOOL_TYPE
              ? 1
              : (vtype_kind == INT_TYPE ? 8 * c.get_size() : 0)));
@@ -680,7 +677,8 @@ template <typename Domain> class cell_ghost_man {
           if (v1 != *v2) {
             assert(v1.name().str() == (*v2).name().str());
             assert(v1.get_type() == (*v2).get_type());
-            variable_t outv(vfac.get(v1.name().str()), v1.get_type());
+	    std::string name = v1.name().str();
+            variable_t outv(vfac.make_varname(std::move(name)), v1.get_type());
             old_ghost_vars_left.push_back(v1);
             old_ghost_vars_right.push_back(*v2);
             new_ghost_vars.push_back(outv);
@@ -727,7 +725,8 @@ template <typename Domain> class cell_ghost_man {
             // same key but different ghost -> create a fresh common ghost
             assert(v1.name().str() == (*v2).name().str());
             assert(v1.get_type() == (*v2).get_type());
-            variable_t outv(vfac.get(v1.name().str()), v1.get_type());
+	    std::string name = v1.name().str();	    
+            variable_t outv(vfac.make_varname(std::move(name)), v1.get_type());
             old_ghost_vars_left.push_back(v1);
             old_ghost_vars_right.push_back(*v2);
             new_ghost_vars.push_back(outv);
@@ -2478,7 +2477,7 @@ class array_adaptive_domain final
             // (summarized) variable
             auto &vfac =
                 const_cast<varname_t *>(&(a.name()))->get_var_factory();
-            variable_t tmp_var(vfac.get(), a.get_type());
+            variable_t tmp_var(vfac.make_temporary_varname(), a.get_type());
             bool found_cell_without_scalar = false;
             for (unsigned k = 0, num_cells = cells.size(); k < num_cells; ++k) {
               const cell_t &c = cells[k];

include/crab/domains/array_smashing.hpp

@@ -113,7 +113,8 @@ class array_smashing final
     // variable for the same array variable.
     auto &vfac =
         const_cast<varname_t *>(&(array_var.name()))->get_var_factory();
-    return variable_t(vfac.get(array_var.name(), ".smashed"), ghost_ty);
+    std::string suffix(".smashed");
+    return variable_t(vfac.get_or_insert_varname(array_var.name(), suffix), ghost_ty);
   }
 
   // Convert elem_size to an uint64_t
@@ -583,8 +584,7 @@ class array_smashing final
       // into a non-summarized variable lhs. Simply m_base_dom.assign(lhs,a)
       // is not sound.
       auto &vfac = const_cast<varname_t *>(&(a.name()))->get_var_factory();
-      variable_t copy_scalar_var(vfac.get(scalar_var.name(), ".copy"),
-                                 scalar_var.get_type());
+      variable_t copy_scalar_var(vfac.make_temporary_varname(), scalar_var.get_type());
       m_base_dom.expand(scalar_var, copy_scalar_var);
       auto ty = scalar_var.get_type();
       if (ty.is_bool()) {

include/crab/domains/backward_assign_operations.hpp

@@ -60,7 +60,7 @@ template <class AbsDom> class BackwardAssignOps {
     if (std::find(e.variables_begin(), e.variables_end(), x) !=
         e.variables_end()) {
       auto &vfac = const_cast<varname_t *>(&(x.name()))->get_var_factory();
-      variable_t old_x(vfac.get(), x.get_type());
+      variable_t old_x(vfac.make_temporary_varname(), x.get_type());
       std::map<variable_t, variable_t> renaming_map;
       renaming_map.insert({x, old_x});
       linear_expression_t renamed_e = e.rename(renaming_map);

include/crab/domains/fixed_tvpi_domain.hpp

@@ -83,9 +83,14 @@ class fixed_tvpi_domain
       CRAB_ERROR("Coefficient must be greater than 1");
     }
     auto &vfac = const_cast<varname_t *>(&(v.name()))->get_var_factory();
-    std::string ghost_name =
-        ".tvpi.ghost_var(" + std::to_string(coefficient) + ")";
-    return variable_t(vfac.get(v.name(), ghost_name), v.get_type());
+
+    std::string str_coefficient = std::to_string(coefficient);
+    std::string suffix;
+    suffix.reserve(std::strlen(".tvpi.var(") + str_coefficient.size() + 1 + 1); 
+    suffix.append(".tvpi.var(");
+    suffix.append(str_coefficient);
+    suffix.append(")");
+    return variable_t(vfac.get_or_insert_varname(v.name(), suffix), v.get_type());
   }
 
   // (TODO): needed for pretty-printing

include/crab/domains/region/ghost_variable_manager.hpp

@@ -118,7 +118,7 @@ class ghost_variable_manager_with_fixed_naming {
       if (role == "") {
         return name;
       } else {
-        return alloc.get(name, role);
+        return alloc.get_or_insert_varname(name, role);
       }
     };
     return ghost_variables_t::create(vfac, alloc_fn, v.name(), m_get_type(v));
@@ -173,7 +173,12 @@ class ghost_variable_manager_with_fixed_naming {
     auto &vfac = gvars.get_vfac();
     auto alloc_fn = [](GhostDomainVarAlloc &alloc, const ghost_varname_t &name,
                        const std::string &role) {
-      return alloc.get(name, role + ".dup");
+      const char* DUP = ".dup";
+      std::string s;
+      s.reserve(role.size() + std::strlen(DUP) + 1);
+      s.append(role);
+      s.append(DUP);
+      return alloc.get_or_insert_varname(name, s);
     };
     return ghost_variables_t::create(vfac, alloc_fn, gvars);
   }

include/crab/domains/term_equiv.hpp

@@ -1451,20 +1451,25 @@ class term_domain final : public abstract_domain_api<term_domain<Info, DomainPar
        /// -- tmp := f(a,i)
       term_id_t t_uf(build_function(term_of_var(a), build_linexpr(i)));
       // FIXME:
-      // 1. we are creating a fresh varname each time we are called.
-      // 2. we are creating an untyped variable. This is ok if the
+      // 1. We are creating a fresh varname each time we are called.
+      // We intentionally tell the variable factory not to remember
+      // the varname by calling make_temporary_varname() instead of
+      // make_varname(). As a result, the varname won't show up when
+      // the method get_shadow_vars() is called.
+      //  
+      // 2. We are creating an untyped variable. This is ok if the
       // underlying domain is, for instance, intervals but it will
       // fail if we use a more type-dependent numerical domain such as
       // wrapped intervals.
-      variable_t tmp(vfac.get());
+      variable_t tmp(vfac.make_temporary_varname());
       // forget tmp
-      this->operator-=(tmp);
+      this->operator-=(tmp);      
       // forget the old value for t_uf, otherwise we can get
       // incorrectly bottom when we add the constraint val == tmp.
       _impl -= domvar_of_term(t_uf);
       rebind_var(tmp, t_uf);
       /// -- assume(tmp == val)
-      this->operator+=(val == tmp);
+      this->operator+=(val == tmp);      
     }
     check_terms(__LINE__);
     CRAB_LOG("term", crab::outs() << a << "[" << i << "]:=" << val << " -- "

include/crab/types/varname_factory.hpp

@@ -47,15 +47,37 @@ template <class T> class indexed_varname : public indexable {
   variable_factory_t *m_vfac;
 
   indexed_varname() = delete;
+
   // first constructor
-  indexed_varname(ikos::index_t id, variable_factory_t *vfac,
-                  std::string name = "")
-      : m_s(boost::none), m_id(id),
-        m_name(name == "" ? nullptr : std::make_shared<std::string>(name)),
+  indexed_varname(ikos::index_t id, variable_factory_t *vfac, std::string &&name)
+      : m_s(boost::none),
+	m_id(id),
+        m_name(std::make_shared<std::string>(std::move(name))),
         m_vfac(vfac) {}
   // second constructor
+  indexed_varname(ikos::index_t id, variable_factory_t *vfac)
+      : m_s(boost::none),
+	m_id(id),
+        m_name(nullptr),
+        m_vfac(vfac) {}
+  // third constructor
+  indexed_varname(ikos::index_t id, variable_factory_t *vfac,
+		  const indexed_varname &other, const std::string &suffix)
+    : m_s(boost::none),
+      m_id(id),
+      m_name(std::make_shared<std::string>()),
+      m_vfac(vfac) {
+    std::string other_name(other.str());
+    m_name->reserve(other_name.size() + suffix.size() + 1);
+    m_name->append(other_name);
+    m_name->append(suffix);
+  }
+  // fourth constructor
   indexed_varname(T s, ikos::index_t id, variable_factory_t *vfac)
-      : m_s(s), m_id(id), m_name(nullptr), m_vfac(vfac) {}
+      : m_s(s),
+	m_id(id),
+	m_name(nullptr),
+	m_vfac(vfac) {}
 
   std::string rename(const std::string &s) const {
     auto it = m_vfac->get_renaming_map().find(s);
@@ -77,12 +99,19 @@ template <class T> class indexed_varname : public indexable {
 
   std::string str() const {
     if (m_s) {
-      return rename(crab::variable_name_traits<T>::to_string(*m_s));
-    } else if (m_name && (*m_name != "")) {
+      std::string name(crab::variable_name_traits<T>::to_string(*m_s));
+      return rename(name);
+    } else if (m_name) {
+      assert(*m_name != "");
       return rename(*m_name);
     } else {
-      // unlikely prefix
-      return rename("@V_" + std::to_string(m_id));
+      // unlikely prefix @V_
+      std::string str_id(std::to_string(m_id));
+      std::string name;
+      name.reserve(std::strlen("@V_") + str_id.size() + 1);
+      name.append("@V_");
+      name.append(str_id);
+      return rename(name);
     }
   }
 
@@ -168,7 +197,8 @@ template <class T> class variable_factory {
 
   virtual ~variable_factory() = default;
 
-  variable_factory(ikos::index_t start_id) : m_next_id(start_id) {}
+  variable_factory(ikos::index_t start_id)
+    : m_next_id(start_id) {}
 
   variable_factory(const variable_factory_t &o) = delete;
 
@@ -185,45 +215,64 @@ template <class T> class variable_factory {
     }
   }
 
-  // Generate a fresh indexed_varname's without being associated with
-  // a particular instance of T.
-  //
-  // If you are an abstract domain then do not use it unless strictly
-  // necessary because it can produce an unbounded number of
-  // indexed_varname objects.
-  virtual varname_t get(std::string name = "") {
-    varname_t iv(get_and_increment_id(), this, name);
+  /**
+   * The next five methods generate fresh indexed_varname's without
+   * being associated with a particular instance of T. These are
+   * useful for creating front-end variables, abstract domain ghost
+   * variables, etc.
+   **/
+
+
+  // The returned varname is not cached
+  virtual varname_t make_varname(std::string &&name) {
+    varname_t iv(get_and_increment_id(), this, move(name));
     m_shadow_vars.push_back(iv);
     return iv;
   }
 
-  // API for abstract domains
-  //
+  // The returned varname is not cached
+  virtual varname_t make_varname() {
+    varname_t iv(get_and_increment_id(), this);
+    m_shadow_vars.push_back(iv);
+    return iv;
+  }
+
+  // DEPRECATED: needed for backward compatibility with clam
+  virtual varname_t get() { return make_varname(); }
+
+  // The returned varname is not cached.
+  virtual varname_t make_temporary_varname() {
+    return varname_t(get_and_increment_id(), this);
+  }
+
+
   // Create a fresh indexed_varname associated to var.
-  // Given the same var and name it always return the same indexed_varname.
-  // The returned indexed_varname's name is var's name concatenated with name.
-  virtual varname_t get(const varname_t &var, std::string name) {
+  // Given the same var and suffix it always return the same indexed_varname.
+  // The returned indexed_varname's name is var's name concatenated with suffix.
+  virtual varname_t get_or_insert_varname(const varname_t &var, const std::string &suffix) {
     auto it = m_shadow_map.find(var);
     if (it == m_shadow_map.end()) {
-      varname_t iv(get_and_increment_id(), this, var.str() + name);
+      varname_t iv(get_and_increment_id(), this, var,  suffix);
       std::map<std::string, varname_t> named_shadows;
-      named_shadows.insert({name, iv});
-      m_shadow_map.insert({var, named_shadows});
+      named_shadows.insert({suffix, iv});
+      m_shadow_map.insert({var, std::move(named_shadows)});
       return iv;
-    } else {
+    } else {    
       std::map<std::string, varname_t> &named_shadows = it->second;
-      auto nit = named_shadows.find(name);
+      auto nit = named_shadows.find(suffix);
       if (nit != named_shadows.end()) {
         return nit->second;
       } else {
-        varname_t iv(get_and_increment_id(), this, var.str() + name);
-        named_shadows.insert({name, iv});
+	varname_t iv(get_and_increment_id(), this, var,  suffix);
+        named_shadows.insert({suffix, iv});
         return iv;
       }
     }
   }
 
-  // Allow temporary renaming for pretty printing
+
+
+  // Allow temporary renaming for pretty-printing
   void add_renaming_map(
       const std::unordered_map<std::string, std::string> &smap) const {
     clear_renaming_map();
@@ -236,7 +285,8 @@ template <class T> class variable_factory {
     return m_renaming_map;
   }
 
-  // return all the non-T variables created by the factory.  
+  // Return all the non-T variables created by the factory
+  // It should be only used for pretty-printing purposes.
   virtual std::vector<varname_t> get_shadow_vars() const {
     std::vector<varname_t> out(m_shadow_vars.begin(), m_shadow_vars.end());
     for (auto &kv_ : m_shadow_map) {

tests/domains/unittests-terms.cc.NOCOMPILE

@@ -131,15 +131,15 @@ int main (int argc, char** argv) {
     dom.array_load(z, a, 4, y);
 
     crab::outs() << dom << "\n";    
-    z_lin_cst_t c1 (z_lin_exp_t(z) == 42);
+    z_lin_cst_t c1 (z_lin_exp_t(z) == 5);
     crab::outs() << "Added " << c1 << "\n";
     dom += c1;
-    crab::outs() << "Result=" << dom << "\n";
+    crab::outs() << "Result=" << dom << " EXPECTED=bottom\n";
 
-    z_lin_cst_t c2 (z_lin_exp_t(z) == 5);
-    crab::outs() << "Added " << c2 << "\n";
-    dom += c2;
-    crab::outs() << "Result=" << dom << "\n";    
+    // z_lin_cst_t c2 (z_lin_exp_t(z) == 5);
+    //crab::outs() << "Added " << c2 << "\n";
+    //dom += c2;
+    //crab::outs() << "Result=" << dom << "\n";    
   }
 
   return 0;