Don't store generic values as comments [TG-3652]

jbmc/regression/CMakeLists.txt

@@ -11,3 +11,4 @@ add_subdirectory(janalyzer-taint)
 add_subdirectory(jbmc-concurrency)
 add_subdirectory(jbmc-inheritance)
 add_subdirectory(jbmc-cover)
+add_subdirectory(jbmc-generics)

jbmc/regression/Makefile

@@ -9,6 +9,7 @@ DIRS = janalzyer-taint \
        jbmc-strings \
        jdiff \
        string-smoke-tests \
+       jbmc-generics \
        # Empty last line
 
 # Tests under goto-gcc cannot be run on Windows, so appveyor.yml unlinks

jbmc/regression/jbmc-generics/CMakeLists.txt

@@ -0,0 +1,10 @@
+add_test_pl_tests(
+    "$<TARGET_FILE:jbmc>"
+)
+
+add_test_pl_profile(
+    "jbmc-symex-driven-lazy-loading"
+    "$<TARGET_FILE:jbmc> --symex-driven-lazy-loading"
+    "-C;-X;symex-driven-lazy-loading-expected-failure;-s;symex-driven-loading"
+    "CORE"
+)

jbmc/regression/jbmc-generics/Makefile

@@ -0,0 +1,36 @@
+default: tests.log
+
+include ../../src/config.inc
+
+test:
+	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
+	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
+
+tests.log: ../$(CPROVER_DIR)/regression/test.pl
+	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
+	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.java" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	find -name '*.out' -execdir $(RM) '{}' \;
+	find -name '*.gb' -execdir $(RM) '{}' \;
+	$(RM) tests.log
+
+%.class: %.java ../../src/org.cprover.jar
+	javac -g -cp ../../src/org.cprover.jar:. $<
+
+nondet_java_files := $(shell find . -name "Nondet*.java")
+nondet_class_files := $(patsubst %.java, %.class, $(nondet_java_files))
+
+.PHONY: nondet-class-files
+nondet-class-files: $(nondet_class_files)
+
+.PHONY: clean-nondet-class-files
+clean-nondet-class-files:
+	-rm $(nondet_class_files)

jbmc/regression/jbmc-generics/type_erasure/TestClass.java

@@ -0,0 +1,34 @@
+class Gen<T> {
+  public T t;
+}
+
+class IWrapper {
+  public int i;
+}
+
+class BWrapper {
+  public boolean b;
+}
+
+class TestClass {
+  static void testFunction() {
+    Gen<IWrapper> a = new Gen<>();
+    Gen b = a;
+    assert(b ==  a);
+    Gen<BWrapper> c;
+    c = b;
+    assert(c == b);
+    assert(c.equals(a));
+  }
+
+  static void testFunctionWithInput(Gen a, Gen<IWrapper> b, Gen<BWrapper> c) {
+    if(a != null && b != null && c != null &&
+      a.t != null && b.t != null && c.t != null)
+    {
+      b = a;
+      assert(b == a);
+      a = c;
+      assert(a == c);
+    }
+  }
+}

jbmc/regression/jbmc-generics/type_erasure/test.desc

@@ -0,0 +1,6 @@
+CORE
+TestClass.class
+--function TestClass.testFunction --classpath ../../../src/java_bytecode/library/core-models.jar:.
+EXIT=0
+SIGNAL=0
+VERIFICATION SUCCESSFUL

jbmc/regression/jbmc-generics/type_erasure/test_function_input.desc

@@ -0,0 +1,10 @@
+CORE
+TestClass.class
+--function TestClass.testFunctionWithInput
+EXIT=0
+SIGNAL=0
+VERIFICATION SUCCESSFUL
+--
+--
+Adding the core models causes a exception in convert_struct relating to the
+`monitorCount` component. See diffblue/cbmc#2307

jbmc/unit/java_bytecode/goto_program_generics/GenericFields.java

@@ -11,10 +11,10 @@ public void foo() {
 
   class MultipleGenericFields {
     Wrapper<IWrapper> field_input1;
-    Wrapper<IWrapper> field_input2;
+    Wrapper<BWrapper> field_input2;
     public void foo() {
         field_input1.field.i = 10;
-        field_input2.field.i = 20;
+        field_input2.field.b = true;
     }
   }
 

jbmc/unit/java_bytecode/goto_program_generics/GenericHelper.java

@@ -6,6 +6,14 @@ public IWrapper(int ii) {
   }
 }
 
+// boolean wrapper
+class BWrapper {
+  public boolean b;
+  public BWrapper(boolean bb) {
+    b = bb;
+  }
+}
+
 // simple generic class
 class Wrapper<T> {
   public T field;

jbmc/unit/java_bytecode/goto_program_generics/generic_parameters_test.cpp

@@ -102,6 +102,21 @@ SCENARIO(
         require_goto_statements::require_entry_point_argument_assignment(
           "this", entry_point_code);
 
+      THEN("Type of multiple generic fields should be right")
+      {
+        const typet &class_type =
+          symbol_table.lookup_ref("java::GenericFields$MultipleGenericFields")
+            .type;
+
+        const auto &component = require_type::require_component(
+          to_java_class_type(class_type), "field_input2");
+
+        const java_generic_typet &type =
+          require_type::require_java_generic_type(component.type());
+        require_type::require_pointer(
+          type.generic_type_arguments()[0], symbol_typet{"java::BWrapper"});
+      }
+
       THEN("Object 'this' has field 'field_input1' of type Wrapper")
       {
         const auto &field_input1_name =
@@ -136,13 +151,13 @@ SCENARIO(
             {},
             entry_point_code);
 
-        THEN("Object 'field_input1' has field 'field' of type IWrapper")
+        THEN("Object 'field_input2' has field 'field' of type BWrapper")
         {
           require_goto_statements::require_struct_component_assignment(
             field_input2_name,
             {},
             "field",
-            "java::IWrapper",
+            "java::BWrapper",
             {},
             entry_point_code);
         }

src/util/irep_ids.def

@@ -655,7 +655,7 @@ IREP_ID_TWO(C_java_implicitly_generic_class_type, #java_implicitly_generic_class
 IREP_ID_TWO(C_java_generic_symbol, #java_generic_symbol)
 IREP_ID_TWO(generic_types, #generic_types)
 IREP_ID_TWO(implicit_generic_types, #implicit_generic_types)
-IREP_ID_TWO(type_variables, #type_variables)
+IREP_ID_ONE(type_variables)
 IREP_ID_TWO(java_lambda_method_handle_index, lambda_method_handle_index)
 IREP_ID_TWO(java_lambda_method_handles, lambda_method_handles)
 IREP_ID_ONE(havoc_object)