Move expr2bits, bits2expr, try_get_string_data_array to simplify_utils

They do not have any dependency on the simplify_exprt class (and thus
don't need to be class members). Similarly, try_get_string_data_array
has nothing to do with the simplify_exprt functions.

Author: tautschnig

src/goto-symex/goto_symex.cpp

@@ -22,6 +22,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/mathematical_types.h>
 #include <util/pointer_offset_size.h>
 #include <util/simplify_expr.h>
+#include <util/simplify_utils.h>
 #include <util/string_expr.h>
 #include <util/string_utils.h>
 

src/util/simplify_expr.cpp

@@ -10,11 +10,9 @@ Author: Daniel Kroening, [email protected]
 
 #include <algorithm>
 
-#include "arith_tools.h"
 #include "byte_operators.h"
 #include "c_types.h"
 #include "config.h"
-#include "endianness_map.h"
 #include "expr_util.h"
 #include "fixedbv.h"
 #include "invariant.h"
@@ -27,9 +25,7 @@ Author: Daniel Kroening, [email protected]
 #include "rational_tools.h"
 #include "simplify_utils.h"
 #include "std_expr.h"
-#include "string_constant.h"
 #include "string_expr.h"
-#include "symbol.h"
 
 // #define DEBUGX
 
@@ -1564,313 +1560,6 @@ simplify_exprt::resultt<> simplify_exprt::simplify_object(const exprt &expr)
   return unchanged(expr);
 }
 
-optionalt<exprt> simplify_exprt::bits2expr(
-  const std::string &bits,
-  const typet &type,
-  bool little_endian)
-{
-  // bits start at lowest memory address
-  auto type_bits = pointer_offset_bits(type, ns);
-
-  if(!type_bits.has_value() || *type_bits != bits.size())
-    return {};
-
-  if(
-    type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
-    type.id() == ID_floatbv || type.id() == ID_fixedbv ||
-    type.id() == ID_c_bit_field || type.id() == ID_pointer ||
-    type.id() == ID_bv)
-  {
-    endianness_mapt map(type, little_endian, ns);
-
-    std::string tmp=bits;
-    for(std::string::size_type i=0; i<bits.size(); ++i)
-      tmp[i]=bits[map.map_bit(i)];
-
-    std::reverse(tmp.begin(), tmp.end());
-
-    mp_integer i = binary2integer(tmp, false);
-    return constant_exprt(integer2bvrep(i, bits.size()), type);
-  }
-  else if(type.id()==ID_c_enum)
-  {
-    auto val = bits2expr(bits, to_c_enum_type(type).subtype(), little_endian);
-    if(val.has_value())
-    {
-      val->type() = type;
-      return *val;
-    }
-    else
-      return {};
-  }
-  else if(type.id()==ID_c_enum_tag)
-  {
-    auto val =
-      bits2expr(bits, ns.follow_tag(to_c_enum_tag_type(type)), little_endian);
-    if(val.has_value())
-    {
-      val->type() = type;
-      return *val;
-    }
-    else
-      return {};
-  }
-  else if(type.id()==ID_union)
-  {
-    // find a suitable member
-    const union_typet &union_type=to_union_type(type);
-    const union_typet::componentst &components=
-      union_type.components();
-
-    for(const auto &component : components)
-    {
-      auto val = bits2expr(bits, component.type(), little_endian);
-      if(!val.has_value())
-        continue;
-
-      return union_exprt(component.get_name(), *val, type);
-    }
-  }
-  else if(type.id() == ID_union_tag)
-  {
-    auto val =
-      bits2expr(bits, ns.follow_tag(to_union_tag_type(type)), little_endian);
-    if(val.has_value())
-    {
-      val->type() = type;
-      return *val;
-    }
-    else
-      return {};
-  }
-  else if(type.id()==ID_struct)
-  {
-    const struct_typet &struct_type=to_struct_type(type);
-    const struct_typet::componentst &components=
-      struct_type.components();
-
-    struct_exprt result({}, type);
-    result.reserve_operands(components.size());
-
-    mp_integer m_offset_bits=0;
-    for(const auto &component : components)
-    {
-      const auto m_size = pointer_offset_bits(component.type(), ns);
-      CHECK_RETURN(m_size.has_value() && *m_size>=0);
-
-      std::string comp_bits = std::string(
-        bits,
-        numeric_cast_v<std::size_t>(m_offset_bits),
-        numeric_cast_v<std::size_t>(*m_size));
-
-      auto comp = bits2expr(comp_bits, component.type(), little_endian);
-      if(!comp.has_value())
-        return {};
-      result.add_to_operands(std::move(*comp));
-
-      m_offset_bits += *m_size;
-    }
-
-    return std::move(result);
-  }
-  else if(type.id() == ID_struct_tag)
-  {
-    auto val =
-      bits2expr(bits, ns.follow_tag(to_struct_tag_type(type)), little_endian);
-    if(val.has_value())
-    {
-      val->type() = type;
-      return *val;
-    }
-    else
-      return {};
-  }
-  else if(type.id()==ID_array)
-  {
-    const array_typet &array_type=to_array_type(type);
-    const auto &size_expr = array_type.size();
-
-    PRECONDITION(size_expr.is_constant());
-
-    const std::size_t number_of_elements =
-      numeric_cast_v<std::size_t>(to_constant_expr(size_expr));
-
-    const auto el_size_opt = pointer_offset_bits(array_type.subtype(), ns);
-    CHECK_RETURN(el_size_opt.has_value() && *el_size_opt > 0);
-
-    const std::size_t el_size = numeric_cast_v<std::size_t>(*el_size_opt);
-
-    array_exprt result({}, array_type);
-    result.reserve_operands(number_of_elements);
-
-    for(std::size_t i = 0; i < number_of_elements; ++i)
-    {
-      std::string el_bits=std::string(bits, i*el_size, el_size);
-      auto el = bits2expr(el_bits, array_type.subtype(), little_endian);
-      if(!el.has_value())
-        return {};
-      result.add_to_operands(std::move(*el));
-    }
-
-    return std::move(result);
-  }
-  else if(type.id() == ID_vector)
-  {
-    const vector_typet &vector_type = to_vector_type(type);
-
-    const std::size_t n_el = numeric_cast_v<std::size_t>(vector_type.size());
-
-    const auto el_size_opt = pointer_offset_bits(vector_type.subtype(), ns);
-    CHECK_RETURN(el_size_opt.has_value() && *el_size_opt > 0);
-
-    const std::size_t el_size = numeric_cast_v<std::size_t>(*el_size_opt);
-
-    vector_exprt result({}, vector_type);
-    result.reserve_operands(n_el);
-
-    for(std::size_t i = 0; i < n_el; ++i)
-    {
-      std::string el_bits = std::string(bits, i * el_size, el_size);
-      auto el = bits2expr(el_bits, vector_type.subtype(), little_endian);
-      if(!el.has_value())
-        return {};
-      result.add_to_operands(std::move(*el));
-    }
-
-    return std::move(result);
-  }
-  else if(type.id() == ID_complex)
-  {
-    const complex_typet &complex_type = to_complex_type(type);
-
-    const auto sub_size_opt = pointer_offset_bits(complex_type.subtype(), ns);
-    CHECK_RETURN(sub_size_opt.has_value() && *sub_size_opt > 0);
-
-    const std::size_t sub_size = numeric_cast_v<std::size_t>(*sub_size_opt);
-
-    auto real = bits2expr(
-      bits.substr(0, sub_size), complex_type.subtype(), little_endian);
-    auto imag =
-      bits2expr(bits.substr(sub_size), complex_type.subtype(), little_endian);
-    if(!real.has_value() || !imag.has_value())
-      return {};
-
-    return complex_exprt(*real, *imag, complex_type);
-  }
-
-  return {};
-}
-
-optionalt<std::string> simplify_exprt::expr2bits(
-  const exprt &expr,
-  bool little_endian)
-{
-  // extract bits from lowest to highest memory address
-  const typet &type = expr.type();
-
-  if(expr.id()==ID_constant)
-  {
-    const auto &value = to_constant_expr(expr).get_value();
-
-    if(
-      type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
-      type.id() == ID_floatbv || type.id() == ID_fixedbv ||
-      type.id() == ID_c_bit_field || type.id() == ID_bv)
-    {
-      const auto width = to_bitvector_type(type).get_width();
-
-      endianness_mapt map(type, little_endian, ns);
-
-      std::string result(width, ' ');
-
-      for(std::string::size_type i = 0; i < width; ++i)
-        result[map.map_bit(i)] = get_bvrep_bit(value, width, i) ? '1' : '0';
-
-      return result;
-    }
-    else if(type.id() == ID_pointer)
-    {
-      if(value == ID_NULL && config.ansi_c.NULL_is_zero)
-        return std::string('0', to_bitvector_type(type).get_width());
-      else
-        return {};
-    }
-    else if(type.id() == ID_c_enum_tag)
-    {
-      const auto &c_enum_type = ns.follow_tag(to_c_enum_tag_type(type));
-      return expr2bits(constant_exprt(value, c_enum_type), little_endian);
-    }
-    else if(type.id() == ID_c_enum)
-    {
-      return expr2bits(
-        constant_exprt(value, to_c_enum_type(type).subtype()), little_endian);
-    }
-  }
-  else if(expr.id() == ID_string_constant)
-  {
-    return expr2bits(to_string_constant(expr).to_array_expr(), little_endian);
-  }
-  else if(expr.id()==ID_union)
-  {
-    return expr2bits(to_union_expr(expr).op(), little_endian);
-  }
-  else if(
-    expr.id() == ID_struct || expr.id() == ID_array || expr.id() == ID_vector ||
-    expr.id() == ID_complex)
-  {
-    std::string result;
-    forall_operands(it, expr)
-    {
-      auto tmp=expr2bits(*it, little_endian);
-      if(!tmp.has_value())
-        return {}; // failed
-      result+=tmp.value();
-    }
-
-    return result;
-  }
-
-  return {};
-}
-
-optionalt<std::reference_wrapper<const array_exprt>>
-try_get_string_data_array(const exprt &content, const namespacet &ns)
-{
-  if(content.id() != ID_address_of)
-  {
-    return {};
-  }
-
-  const auto &array_pointer = to_address_of_expr(content);
-
-  if(array_pointer.object().id() != ID_index)
-  {
-    return {};
-  }
-
-  const auto &array_start = to_index_expr(array_pointer.object());
-
-  if(array_start.array().id() != ID_symbol ||
-     array_start.array().type().id() != ID_array)
-  {
-    return {};
-  }
-
-  const auto &array = to_symbol_expr(array_start.array());
-
-  const symbolt *symbol_ptr = nullptr;
-
-  if(ns.lookup(array.get_identifier(), symbol_ptr) ||
-     symbol_ptr->value.id() != ID_array)
-  {
-    return {};
-  }
-
-  const auto &char_seq = to_array_expr(symbol_ptr->value);
-
-  return optionalt<std::reference_wrapper<const array_exprt>>(char_seq);
-}
-
 simplify_exprt::resultt<>
 simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr)
 {
@@ -1958,9 +1647,10 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr)
   if(expr.op().id()==ID_array_of &&
      to_array_of_expr(expr.op()).op().id()==ID_constant)
   {
-    const auto const_bits_opt=
-      expr2bits(to_array_of_expr(expr.op()).op(),
-                byte_extract_id()==ID_byte_extract_little_endian);
+    const auto const_bits_opt = expr2bits(
+      to_array_of_expr(expr.op()).op(),
+      byte_extract_id() == ID_byte_extract_little_endian,
+      ns);
 
     if(!const_bits_opt.has_value())
       return unchanged(expr);
@@ -1979,7 +1669,7 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr)
       numeric_cast_v<std::size_t>(*el_size));
 
     auto tmp = bits2expr(
-      el_bits, expr.type(), expr.id() == ID_byte_extract_little_endian);
+      el_bits, expr.type(), expr.id() == ID_byte_extract_little_endian, ns);
 
     if(tmp.has_value())
       return std::move(*tmp);
@@ -1998,8 +1688,8 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr)
   }
 
   // extract bits of a constant
-  const auto bits=
-    expr2bits(expr.op(), expr.id()==ID_byte_extract_little_endian);
+  const auto bits =
+    expr2bits(expr.op(), expr.id() == ID_byte_extract_little_endian, ns);
 
   // make sure we don't lose bits with structs containing flexible array members
   const bool struct_has_flexible_array_member = has_subtype(
@@ -2028,7 +1718,7 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr)
       numeric_cast_v<std::size_t>(*el_size));
 
     auto tmp = bits2expr(
-      bits_cut, expr.type(), expr.id() == ID_byte_extract_little_endian);
+      bits_cut, expr.type(), expr.id() == ID_byte_extract_little_endian, ns);
 
     if(tmp.has_value())
       return std::move(*tmp);