[TG-3581] Better Support for Enums in JBMC

jbmc/regression/jbmc/enum_switch/com/diffblue/regression/Foo.java

@@ -0,0 +1,16 @@
+package com.diffblue.regression;
+
+public class Foo {
+  public int foo(MyEnum e) {
+    if (e == null) return 0;
+    switch (e) {
+      case A:
+        return 1;
+      case B:
+        return 2;
+      case C:
+        return 3;
+    }
+    return 5;
+  }
+}

jbmc/regression/jbmc/enum_switch/com/diffblue/regression/MyEnum.java

@@ -0,0 +1,5 @@
+package com.diffblue.regression;
+
+enum MyEnum {
+ A, B, C, D;
+}

jbmc/regression/jbmc/enum_switch/test.desc

@@ -0,0 +1,10 @@
+CORE symex-driven-lazy-loading-expected-failure
+com/diffblue/regression/Foo.class
+--trace --cover location --depth 1024 --java-max-vla-length 16 --refine-strings --max-nondet-string-length 20 --string-printable --unwind 10 --function "com.diffblue.regression.Foo.foo" --java-unwind-enum-static
+line 8.*SATISFIED
+line 10.*SATISFIED
+line 12.*SATISFIED
+line 14.*SATISFIED
+^EXIT=0$
+^SIGNAL=0$
+--

jbmc/regression/jbmc/enum_values_clone/com/diffblue/regression/EnumIter.java

@@ -0,0 +1,8 @@
+package com.diffblue.regression;
+public class EnumIter {
+    int f() {
+        MyEnum[] a = MyEnum.values();
+        int num = a[2].ordinal() + a[3].ordinal();
+        return num ;
+    }
+}

jbmc/regression/jbmc/enum_values_clone/com/diffblue/regression/MyEnum.java

@@ -0,0 +1,5 @@
+package com.diffblue.regression;
+
+enum MyEnum {
+ A, B, C, D;
+}

jbmc/regression/jbmc/enum_values_clone/test.desc

@@ -0,0 +1,7 @@
+CORE symex-driven-lazy-loading-expected-failure
+com/diffblue/regression/EnumIter.class
+--trace  --cover location --depth 1024  --java-max-vla-length 16 --refine-strings --max-nondet-string-length 20 --string-printable --unwind 2 --function "com.diffblue.regression.EnumIter.f" --java-unwind-enum-static
+\d+ of \d+ covered \(100\.0%\)
+^EXIT=0$
+^SIGNAL=0$
+--

jbmc/regression/jbmc/enum_values_clone_name/com/diffblue/regression/EnumIter.java

@@ -0,0 +1,7 @@
+package com.diffblue.regression;
+public class EnumIter {
+    String f() {
+        MyEnum[] a = MyEnum.values();
+        return a[2].name() + a[3].name();
+    }
+}

jbmc/regression/jbmc/enum_values_clone_name/com/diffblue/regression/MyEnum.java

@@ -0,0 +1,5 @@
+package com.diffblue.regression;
+
+enum MyEnum {
+ A, B, C, D;
+}

jbmc/regression/jbmc/enum_values_clone_name/test.desc

@@ -0,0 +1,7 @@
+CORE symex-driven-lazy-loading-expected-failure
+com/diffblue/regression/EnumIter.class
+--trace --cover location --depth 1024 --java-max-vla-length 16 --refine-strings --max-nondet-string-length 20 --string-printable --unwind 2 --function "com.diffblue.regression.EnumIter.f" --java-unwind-enum-static
+\d+ of \d+ covered \(100\.0%\)
+^EXIT=0$
+^SIGNAL=0$
+--

jbmc/src/java_bytecode/Makefile

@@ -20,6 +20,7 @@ SRC = bytecode_info.cpp \
       java_bytecode_typecheck_type.cpp \
       java_class_loader.cpp \
       java_class_loader_limit.cpp \
+      java_enum_array_clone_unwind_handler.cpp \
       java_enum_static_init_unwind_handler.cpp \
       java_entry_point.cpp \
       java_local_variable_table.cpp \

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -115,9 +115,6 @@ class java_bytecode_convert_classt:public messaget
   void convert(const classt &c, const overlay_classest &overlay_classes);
   void convert(symbolt &class_symbol, const fieldt &f);
 
-  // see definition below for more info
-  static void add_array_types(symbol_tablet &symbol_table);
-
   static bool is_overlay_method(const methodt &method)
   {
     return method.has_annotation(ID_overlay_method);
@@ -717,182 +714,6 @@ void java_bytecode_convert_classt::convert(
   }
 }
 
-/// Register in the \p symbol_table new symbols for the objects
-/// java::array[X] where X is byte, float, int, char...
-void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
-{
-  const std::string letters="ijsbcfdza";
-
-  for(const char l : letters)
-  {
-    symbol_typet symbol_type=
-      to_symbol_type(java_array_type(l).subtype());
-
-    const irep_idt &symbol_type_identifier=symbol_type.get_identifier();
-    if(symbol_table.has_symbol(symbol_type_identifier))
-      return;
-
-    java_class_typet class_type;
-    // we have the base class, java.lang.Object, length and data
-    // of appropriate type
-    class_type.set_tag(symbol_type_identifier);
-    // Note that non-array types don't have "java::" at the beginning of their
-    // tag, and their name is "java::" + their tag. Since arrays do have
-    // "java::" at the beginning of their tag we set the name to be the same as
-    // the tag.
-    class_type.set_name(symbol_type_identifier);
-
-    class_type.components().reserve(3);
-    class_typet::componentt base_class_component(
-      "@java.lang.Object", symbol_typet("java::java.lang.Object"));
-    base_class_component.set_pretty_name("@java.lang.Object");
-    base_class_component.set_base_name("@java.lang.Object");
-    class_type.components().push_back(base_class_component);
-
-    class_typet::componentt length_component("length", java_int_type());
-    length_component.set_pretty_name("length");
-    length_component.set_base_name("length");
-    class_type.components().push_back(length_component);
-
-    class_typet::componentt data_component(
-      "data", java_reference_type(java_type_from_char(l)));
-    data_component.set_pretty_name("data");
-    data_component.set_base_name("data");
-    class_type.components().push_back(data_component);
-
-    class_type.add_base(symbol_typet("java::java.lang.Object"));
-
-    INVARIANT(
-      is_valid_java_array(class_type),
-      "Constructed a new type representing a Java Array "
-      "object that doesn't match expectations");
-
-    symbolt symbol;
-    symbol.name=symbol_type_identifier;
-    symbol.base_name=symbol_type.get(ID_C_base_name);
-    symbol.is_type=true;
-    symbol.type = class_type;
-    symbol.mode = ID_java;
-    symbol_table.add(symbol);
-
-    // Also provide a clone method:
-    // ----------------------------
-
-    const irep_idt clone_name=
-      id2string(symbol_type_identifier)+".clone:()Ljava/lang/Object;";
-    code_typet::parametert this_param;
-    this_param.set_identifier(id2string(clone_name)+"::this");
-    this_param.set_base_name("this");
-    this_param.set_this();
-    this_param.type()=java_reference_type(symbol_type);
-    const code_typet clone_type({this_param}, java_lang_object_type());
-
-    parameter_symbolt this_symbol;
-    this_symbol.name=this_param.get_identifier();
-    this_symbol.base_name=this_param.get_base_name();
-    this_symbol.pretty_name=this_symbol.base_name;
-    this_symbol.type=this_param.type();
-    this_symbol.mode=ID_java;
-    symbol_table.add(this_symbol);
-
-    const irep_idt local_name=
-      id2string(clone_name)+"::cloned_array";
-    auxiliary_symbolt local_symbol;
-    local_symbol.name=local_name;
-    local_symbol.base_name="cloned_array";
-    local_symbol.pretty_name=local_symbol.base_name;
-    local_symbol.type=java_reference_type(symbol_type);
-    local_symbol.mode=ID_java;
-    symbol_table.add(local_symbol);
-    const auto &local_symexpr=local_symbol.symbol_expr();
-
-    code_blockt clone_body;
-
-    code_declt declare_cloned(local_symexpr);
-    clone_body.move_to_operands(declare_cloned);
-
-    side_effect_exprt java_new_array(
-      ID_java_new_array,
-      java_reference_type(symbol_type));
-    dereference_exprt old_array(this_symbol.symbol_expr(), symbol_type);
-    dereference_exprt new_array(local_symexpr, symbol_type);
-    member_exprt old_length(
-      old_array, length_component.get_name(), length_component.type());
-    java_new_array.copy_to_operands(old_length);
-    code_assignt create_blank(local_symexpr, java_new_array);
-    clone_body.move_to_operands(create_blank);
-
-    member_exprt old_data(
-      old_array, data_component.get_name(), data_component.type());
-    member_exprt new_data(
-      new_array, data_component.get_name(), data_component.type());
-
-    /*
-      // TODO use this instead of a loop.
-    codet array_copy;
-    array_copy.set_statement(ID_array_copy);
-    array_copy.move_to_operands(new_data);
-    array_copy.move_to_operands(old_data);
-    clone_body.move_to_operands(array_copy);
-    */
-
-    // Begin for-loop to replace:
-
-    const irep_idt index_name=
-      id2string(clone_name)+"::index";
-    auxiliary_symbolt index_symbol;
-    index_symbol.name=index_name;
-    index_symbol.base_name="index";
-    index_symbol.pretty_name=index_symbol.base_name;
-    index_symbol.type = length_component.type();
-    index_symbol.mode=ID_java;
-    symbol_table.add(index_symbol);
-    const auto &index_symexpr=index_symbol.symbol_expr();
-
-    code_declt declare_index(index_symexpr);
-    clone_body.move_to_operands(declare_index);
-
-    code_fort copy_loop;
-
-    copy_loop.init()=
-      code_assignt(index_symexpr, from_integer(0, index_symexpr.type()));
-    copy_loop.cond()=
-      binary_relation_exprt(index_symexpr, ID_lt, old_length);
-
-    side_effect_exprt inc(ID_assign);
-    inc.operands().resize(2);
-    inc.op0()=index_symexpr;
-    inc.op1()=plus_exprt(index_symexpr, from_integer(1, index_symexpr.type()));
-    copy_loop.iter()=inc;
-
-    dereference_exprt old_cell(
-      plus_exprt(old_data, index_symexpr), old_data.type().subtype());
-    dereference_exprt new_cell(
-      plus_exprt(new_data, index_symexpr), new_data.type().subtype());
-    code_assignt copy_cell(new_cell, old_cell);
-    copy_loop.body()=copy_cell;
-
-    // End for-loop
-    clone_body.move_to_operands(copy_loop);
-
-    member_exprt new_base_class(
-      new_array, base_class_component.get_name(), base_class_component.type());
-    address_of_exprt retval(new_base_class);
-    code_returnt return_inst(retval);
-    clone_body.move_to_operands(return_inst);
-
-    symbolt clone_symbol;
-    clone_symbol.name=clone_name;
-    clone_symbol.pretty_name=
-      id2string(symbol_type_identifier)+".clone:()";
-    clone_symbol.base_name="clone";
-    clone_symbol.type=clone_type;
-    clone_symbol.value=clone_body;
-    clone_symbol.mode=ID_java;
-    symbol_table.add(clone_symbol);
-  }
-}
-
 bool java_bytecode_convert_class(
   const java_class_loadert::parse_tree_with_overlayst &parse_trees,
   symbol_tablet &symbol_table,