Preserve existing details of string types

Previously the lambda handles, methods and similar were removed when all we need for the string
solver is to ensure the type has a <length, data> member pair in the manner of an array type.

Author: smowton

jbmc/regression/jbmc/lambda-defined-on-string-type/Test.class

@@ -0,0 +1,8 @@
+public class Test {
+
+  public static void testme() {
+    assert String.usesLambdas(1) == 2;
+    assert false; // Check we got here
+  }
+
+}

jbmc/regression/jbmc/lambda-defined-on-string-type/Test.java

@@ -0,0 +1,14 @@
+package java.lang;
+
+public class String {
+
+  interface FunctionalIf {
+    public int f(int x);
+  }
+
+  public static int usesLambdas(int x) {
+    FunctionalIf lambda = (n -> n + 1);
+    return lambda.f(x);
+  }
+
+}

jbmc/regression/jbmc/lambda-defined-on-string-type/java/lang/String$FunctionalIf.class

@@ -0,0 +1,13 @@
+CORE
+Test
+--function Test.testme --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+line 4 assertion at file Test\.java line 4 function java::Test\.testme:\(\)V bytecode-index 9: SUCCESS
+line 5 assertion at file Test\.java line 5 function java::Test\.testme:\(\)V bytecode-index 15: FAILURE
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+This checks that a lambda functions work when defined on a string type (String, StringBuilder, StringBuffer,
+CharSequence, i.e. the types that the string solver may define or redefine)
+We use a dummy String type because the typical example in the wild, CharSequence.chars(), requires much
+more of the JDK than the tiny fragment present in jbmc's models library at present.

jbmc/regression/jbmc/lambda-defined-on-string-type/java/lang/String.class

@@ -209,9 +209,43 @@ java_string_library_preprocesst::get_string_type_base_classes(
 void java_string_library_preprocesst::add_string_type(
   const irep_idt &class_name, symbol_tablet &symbol_table)
 {
-  java_class_typet string_type;
-  string_type.set_tag(class_name);
-  string_type.set_name("java::" + id2string(class_name));
+  irep_idt class_symbol_name = "java::" + id2string(class_name);
+  symbolt tmp_string_symbol;
+  tmp_string_symbol.name = class_symbol_name;
+  symbolt *string_symbol = nullptr;
+  bool already_exists = symbol_table.move(tmp_string_symbol, string_symbol);
+
+  if(already_exists)
+  {
+    // A library has already defined this type -- we'll replace its
+    // components with those required for internal string modelling, but
+    // otherwise leave it alone.
+    to_java_class_type(string_symbol->type).components().clear();
+  }
+  else
+  {
+    // No definition of this type exists -- define it as it usually occurs in
+    // the JDK:
+    java_class_typet new_string_type;
+    new_string_type.set_tag(class_name);
+    new_string_type.set_name(class_symbol_name);
+    new_string_type.set_access(ID_public);
+    new_string_type.add_base(struct_tag_typet("java::java.lang.Object"));
+
+    std::vector<irep_idt> bases = get_string_type_base_classes(class_name);
+    for(const irep_idt &base_name : bases)
+      new_string_type.add_base(
+        struct_tag_typet("java::" + id2string(base_name)));
+
+    string_symbol->base_name = id2string(class_name);
+    string_symbol->pretty_name = id2string(class_name);
+    string_symbol->type = new_string_type;
+    string_symbol->is_type = true;
+    string_symbol->mode = ID_java;
+  }
+
+  auto &string_type = to_java_class_type(string_symbol->type);
+
   string_type.components().resize(3);
   string_type.components()[0].set_name("@java.lang.Object");
   string_type.components()[0].set_pretty_name("@java.lang.Object");
@@ -223,22 +257,6 @@ void java_string_library_preprocesst::add_string_type(
   string_type.components()[2].set_name("data");
   string_type.components()[2].set_pretty_name("data");
   string_type.components()[2].type() = pointer_type(java_char_type());
-  string_type.set_access(ID_public);
-  string_type.add_base(struct_tag_typet("java::java.lang.Object"));
-
-  std::vector<irep_idt> bases = get_string_type_base_classes(class_name);
-  for(const irep_idt &base_name : bases)
-    string_type.add_base(struct_tag_typet("java::" + id2string(base_name)));
-
-  symbolt tmp_string_symbol;
-  tmp_string_symbol.name="java::"+id2string(class_name);
-  symbolt *string_symbol=nullptr;
-  symbol_table.move(tmp_string_symbol, string_symbol);
-  string_symbol->base_name=id2string(class_name);
-  string_symbol->pretty_name=id2string(class_name);
-  string_symbol->type=string_type;
-  string_symbol->is_type=true;
-  string_symbol->mode = ID_java;
 }
 
 /// calls string_refine_preprocesst::process_operands with a list of parameters.

jbmc/regression/jbmc/lambda-defined-on-string-type/java/lang/String.java

@@ -43,6 +43,7 @@ SCENARIO(
 
     // Add java.lang.String to symbol table
     java_string_library_preprocesst preprocess;
+    preprocess.initialize_known_type_table();
     preprocess.add_string_type("java.lang.String", symbol_table);
     namespacet ns(symbol_table);
 

jbmc/regression/jbmc/lambda-defined-on-string-type/test.desc

@@ -39,6 +39,7 @@ TEST_CASE("Convert exprt to string exprt")
     namespacet ns(symbol_table);
     code_blockt code;
     java_string_library_preprocesst preprocess;
+    preprocess.initialize_known_type_table();
     preprocess.add_string_type("java.lang.String", symbol_table);
     struct_tag_typet java_string_type("java::java.lang.String");
     symbol_exprt expr("a", pointer_type(java_string_type));