byte_extract flattening over Java strings

Author: tautschnig

src/solvers/flattening/flatten_byte_operators.cpp

@@ -205,6 +205,9 @@ static exprt unpack_rec(
       }
 
       member_exprt member(src, comp.get_name(), comp.type());
+      if(src.id()==ID_struct)
+        simplify(member, ns);
+
       exprt sub=
         unpack_rec(
           member,
@@ -250,6 +253,37 @@ static exprt unpack_rec(
         array.copy_to_operands(op);
     }
   }
+  else if(src.id()==ID_string_constant ||
+          (src.id()==ID_constant && type.id()==ID_string))
+  {
+    // string constants
+    std::string value=id2string(src.get(ID_value));
+
+    // create an array of characters and unpack that one
+    array_exprt char_array(
+      array_typet(
+        unsignedbv_typet(8), from_integer(value.size(), size_type())));
+
+    exprt::operandst chars;
+    chars.reserve(value.size());
+    for(const char c : value)
+      chars.push_back(from_integer(c, unsignedbv_typet(8)));
+
+    char_array.operands().swap(chars);
+
+    if(!unpack_byte_array)
+      return char_array;
+
+    unpack_array_vector(
+      char_array,
+      to_array_type(char_array.type()).size(),
+      8,
+      little_endian,
+      offset,
+      max_bytes,
+      ns,
+      array);
+  }
   else if(type.id()!=ID_empty)
   {
     // a basic type; we turn that into extractbits while considering