Refactor string_refinementt::concretize_string()

Author: Lukasz A.J. Wrona

src/solvers/refinement/string_refinement.cpp

@@ -289,6 +289,22 @@ bool string_refinementt::add_axioms_for_string_assigns(
   return true;
 }
 
+template<typename T>
+T expr_cast(const exprt&);
+
+template<>
+std::size_t expr_cast<std::size_t>(const exprt& val_expr)
+{
+  mp_integer val_mb;
+  if(!to_integer(val_expr, val_mb))
+    throw std::bad_cast();
+  if(!val_mb.is_long())
+    throw std::bad_cast();
+  if(val_mb<0)
+    throw std::bad_cast();
+  return val_mb.to_long();
+}
+
 /// If the expression is of type string, then adds constants to the index set to
 /// force the solver to pick concrete values for each character, and fill the
 /// maps `found_length` and `found_content`.
@@ -304,70 +320,44 @@ void string_refinementt::concretize_string(const exprt &expr)
 {
   if(refined_string_typet::is_refined_string_type(expr.type()))
   {
-    string_exprt str=to_string_expr(expr);
-    exprt length=get(str.length());
+    const string_exprt str=to_string_expr(expr);
+    const exprt length=get(str.length());
     exprt content=str.content();
     replace_expr(symbol_resolve, content);
     found_length[content]=length;
-    mp_integer found_length;
-    if(!to_integer(length, found_length))
-    {
-      INVARIANT(
-        found_length.is_long(),
-        string_refinement_invariantt("the length of a string should be a "
-          "long"));
-      INVARIANT(
-        found_length>=0,
-        string_refinement_invariantt("the length of a string should be >= 0"));
-      size_t concretize_limit=found_length.to_long();
-      INVARIANT(
-        concretize_limit<=generator.max_string_length,
-        string_refinement_invariantt("string length must be less than the max "
-          "length"));
-      exprt content_expr=str.content();
-      std::vector<exprt> result;
-
-      if(index_set[str.content()].empty())
-        return;
+    const auto string_length=expr_cast<std::size_t>(length);
+    INVARIANT(
+      string_length<=generator.max_string_length,
+      string_refinement_invariantt("string length must be less than the max "
+        "length"));
+    if(index_set[str.content()].empty())
+      return;
 
-      // Use the last index as the default character value
-      exprt last_concretized=simplify_expr(
-        get(str[minus_exprt(length, from_integer(1, length.type()))]), ns);
-      result.resize(concretize_limit, last_concretized);
+    // Use the last index as the default character value
+    const exprt last_concretized=simplify_expr(
+      get(str[minus_exprt(length, from_integer(1, length.type()))]), ns);
 
-      // Keep track of the indexes for which we have actual values
-      std::set<std::size_t> initialized;
+    std::map<std::size_t, exprt> map;
 
-      for(const auto &i : index_set[str.content()])
+    for(const auto &i : index_set[str.content()])
+    {
+      const exprt simple_i=simplify_expr(get(i), ns);
+      try
       {
-        mp_integer mp_index;
-        exprt simple_i=simplify_expr(get(i), ns);
-        if(to_integer(simple_i, mp_index) ||
-           mp_index<0 ||
-           mp_index>=concretize_limit)
-        {
-          debug() << "concretize_string: ignoring out of bound index: "
-                  << from_expr(ns, "", simple_i) << eom;
-        }
-        else
-        {
-          // Add an entry in the result vector
-          size_t index=mp_index.to_long();
-          exprt str_i=simplify_expr(str[simple_i], ns);
-          exprt value=simplify_expr(get(str_i), ns);
-          result[index]=value;
-          initialized.insert(index);
-        }
+        const auto index=expr_cast<std::size_t>(simple_i);
+        const exprt str_i=simplify_expr(str[simple_i], ns);
+        const exprt value=simplify_expr(get(str_i), ns);
+        map.emplace(index, value);
+      }
+      catch(const std::bad_cast &)
+      {
+        debug() << "concretize_string: ignoring out of bound index: "
+                << from_expr(ns, "", simple_i) << eom;
       }
-
-      // Pad the concretized values to the left to assign the uninitialized
-      // values of result. The indices greater than concretize_limit are
-      // already assigned to last_concretized.
-      fill_in_vector(result, initialized);
 
       array_exprt arr(to_array_type(content.type()));
-      arr.operands()=result;
-      debug() << "Concretized " << from_expr(ns, "", content_expr)
+      arr.operands()=fill_in_map_as_vector(map);
+      debug() << "Concretized " << from_expr(ns, "", str.content())
               << " = " << from_expr(ns, "", arr) << eom;
       found_content[content]=arr;
     }