Complete string solver rework

This devides string_exprt into two types:
  * refined_string_exprt which is used in the preprocessing to pass
    arguments to string primitives
  * array_string_exprt  which is used by the string solver

The solver therefore now works with arrays in the back end.
This commit contains a lot of renaming from string_exprt to one of the
two new expression type, and the solver procedure is adapted for
working on finite arrays.

Author: romainbrenguier

src/java_bytecode/java_bytecode_typecheck_expr.cpp

@@ -13,6 +13,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <iomanip>
 
+#include <util/std_expr.h>
+#include <util/prefix.h>
 #include <util/arith_tools.h>
 #include <util/unicode.h>
 
@@ -22,6 +24,7 @@ Author: Daniel Kroening, [email protected]
 #include "java_types.h"
 #include "java_utils.h"
 #include "java_root_class.h"
+#include "java_string_library_preprocess.h"
 
 void java_bytecode_typecheckt::typecheck_expr(exprt &expr)
 {
@@ -95,7 +98,8 @@ static std::string escape_non_alnum(const std::string &toescape)
 static array_exprt utf16_to_array(const std::wstring &in)
 {
   const auto jchar=java_char_type();
-  array_exprt ret(array_typet(jchar, infinity_exprt(java_int_type())));
+  array_exprt ret(
+    array_typet(jchar, from_integer(in.length(), java_int_type())));
   for(const auto c : in)
     ret.copy_to_operands(from_integer(c, jchar));
   return ret;
@@ -141,33 +145,51 @@ void java_bytecode_typecheckt::typecheck_expr_java_string_literal(exprt &expr)
   {
     struct_exprt literal_init(new_symbol.type);
     literal_init.move_to_operands(jlo_init);
+    literal_init.copy_to_operands(
+      from_integer(id2string(value).size(), jls_struct.components()[1].type()));
 
     // Initialize the string with a constant utf-16 array:
     symbolt array_symbol;
     array_symbol.name=escaped_symbol_name+"_constarray";
-    array_symbol.type=array_typet(
-      java_char_type(), infinity_exprt(java_int_type()));
     array_symbol.base_name="Literal_constarray";
+    // TODO: this should be obtained from java_string_library_preprocess
     array_symbol.pretty_name=value;
     array_symbol.mode=ID_java;
     array_symbol.is_type=false;
     array_symbol.is_lvalue=true;
     // These are basically const global data:
     array_symbol.is_static_lifetime=true;
     array_symbol.is_state_var=true;
-    auto literal_array=utf16_to_array(
-      utf8_to_utf16_little_endian(id2string(value)));
-    array_symbol.value=literal_array;
+    array_symbol.value =
+      utf16_to_array(utf8_to_utf16_little_endian(id2string(value)));
+    array_symbol.type = array_symbol.value.type();
 
     if(symbol_table.add(array_symbol))
       throw "failed to add constarray symbol to symbol table";
 
-    literal_init.copy_to_operands(
-      from_integer(literal_array.operands().size(),
-                   jls_struct.components()[1].type()));
-    literal_init.copy_to_operands(
-      address_of_exprt(array_symbol.symbol_expr()));
-
+    const symbol_exprt array_expr = array_symbol.symbol_expr();
+    const address_of_exprt first_index(
+      index_exprt(array_expr, from_integer(0, java_int_type())));
+    literal_init.copy_to_operands(first_index);
+
+    // Associate array with pointer
+    symbolt return_symbol;
+    return_symbol.name = "return_value_" + escaped_symbol_name;
+    return_symbol.base_name = escaped_symbol_name;
+    return_symbol.pretty_name = "return_value";
+    return_symbol.mode = ID_java;
+    return_symbol.is_type = false;
+    return_symbol.is_lvalue = true;
+    return_symbol.is_static_lifetime = true;
+    return_symbol.is_state_var = true;
+    return_symbol.value = make_function_application(
+      ID_cprover_associate_array_to_pointer_func,
+      {array_symbol.value, first_index},
+      java_int_type(),
+      symbol_table);
+    return_symbol.type = return_symbol.value.type();
+    if(symbol_table.add(return_symbol))
+      throw "failed to add return symbol to symbol table";
     new_symbol.value=literal_init;
   }
   else if(jls_struct.components().size()>=1 &&