Merge pull request diffblue#516 from diffblue/feature/parse-bean-defi…

…nition-methods

Parse bean definition methods [SEC-545]

CMakeLists.txt

@@ -49,6 +49,8 @@ set(CMAKE_EXPORT_COMPILE_COMMANDS true)
 set(enable_security_tests on CACHE BOOL "Whether tests of the security analyser should be enabled.")
 set(enable_cbmc_tests off CACHE BOOL "Whether CBMC tests should be enabled (the default is to enable just test-gen tests)")
 
+add_definitions(-DLOCAL_IREP_IDS="../../../src/util/local_irep_ids.def")
+
 ################################################################################
 # BOOST
 

cbmc/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -1030,7 +1030,8 @@ void convert_annotations(
   const java_bytecode_parse_treet::annotationst &parsed_annotations,
   std::vector<java_annotationt> &java_annotations)
 {
-  for(const auto &annotation : parsed_annotations)
+  for(const java_bytecode_parse_treet::annotationt &annotation
+    : parsed_annotations)
   {
     java_annotations.emplace_back(annotation.type);
     std::vector<java_annotationt::valuet> &values =
@@ -1039,7 +1040,9 @@ void convert_annotations(
       annotation.element_value_pairs.begin(),
       annotation.element_value_pairs.end(),
       std::back_inserter(values),
-      [](const decltype(annotation.element_value_pairs)::value_type &value) {
+      []
+      (const java_bytecode_parse_treet::annotationt::element_value_pairt &value)
+      {
         return java_annotationt::valuet(value.element_name, value.value);
       });
   }

cbmc/jbmc/src/java_bytecode/java_bytecode_parser.cpp

@@ -125,7 +125,7 @@ class java_bytecode_parsert:public parsert
   void rRuntimeAnnotation_attribute(annotationst &);
   void rRuntimeAnnotation(annotationt &);
   void relement_value_pairs(annotationt::element_value_pairst &);
-  void relement_value_pair(annotationt::element_value_pairt &);
+  exprt get_relement_value();
   void rmethod_attribute(methodt &method);
   void rfield_attribute(fieldt &);
   void rcode_attribute(methodt &method);
@@ -1507,16 +1507,14 @@ void java_bytecode_parsert::relement_value_pairs(
   {
     u2 element_name_index=read_u2();
     element_value_pair.element_name=pool_entry(element_name_index).s;
-
-    relement_value_pair(element_value_pair);
+    element_value_pair.value = get_relement_value();
   }
 }
 
 /// Corresponds to the element_value structure
 /// Described in Java 8 specification 4.7.16.1
 /// https://docs.oracle.com/javase/specs/jvms/se8/html/jvms-4.html#jvms-4.7.16.1
-void java_bytecode_parsert::relement_value_pair(
-  annotationt::element_value_pairt &element_value_pair)
+exprt java_bytecode_parsert::get_relement_value()
 {
   u1 tag=read_u1();
 
@@ -1527,50 +1525,46 @@ void java_bytecode_parsert::relement_value_pair(
       UNUSED_u2(type_name_index);
       UNUSED_u2(const_name_index);
       // todo: enum
+      return exprt();
     }
-    break;
 
   case 'c':
     {
       u2 class_info_index = read_u2();
-      element_value_pair.value = symbol_exprt(pool_entry(class_info_index).s);
+      return symbol_exprt(pool_entry(class_info_index).s);
     }
-    break;
 
   case '@':
     {
+      // TODO: return this wrapped in an exprt
       // another annotation, recursively
       annotationt annotation;
       rRuntimeAnnotation(annotation);
+      return exprt();
     }
-    break;
 
   case '[':
     {
+      array_exprt values;
       u2 num_values=read_u2();
       for(std::size_t i=0; i<num_values; i++)
       {
-        annotationt::element_value_pairt element_value;
-        relement_value_pair(element_value); // recursive call
+        values.operands().push_back(get_relement_value());
       }
+      return values;
     }
-    break;
 
   case 's':
     {
       u2 const_value_index=read_u2();
-      element_value_pair.value=string_constantt(
-        pool_entry(const_value_index).s);
+      return string_constantt(pool_entry(const_value_index).s);
     }
-    break;
 
   default:
     {
       u2 const_value_index=read_u2();
-      element_value_pair.value=constant(const_value_index);
+      return constant(const_value_index);
     }
-
-  break;
   }
 }
 

cbmc/src/util/std_types.h

@@ -1000,6 +1000,12 @@ class code_typet:public typet
   }
 };
 
+template <>
+inline bool can_cast_type<code_typet>(const typet &type)
+{
+  return type.id() == ID_code;
+}
+
 /*! \brief Cast a generic typet to a \ref code_typet
  *
  * This is an unchecked conversion. \a type must be known to be \ref
@@ -1012,7 +1018,8 @@ class code_typet:public typet
 */
 inline const code_typet &to_code_type(const typet &type)
 {
-  PRECONDITION(type.id()==ID_code);
+  PRECONDITION(can_cast_type<code_typet>(type));
+  validate_type(type);
   return static_cast<const code_typet &>(type);
 }
 
@@ -1021,10 +1028,12 @@ inline const code_typet &to_code_type(const typet &type)
 */
 inline code_typet &to_code_type(typet &type)
 {
-  PRECONDITION(type.id()==ID_code);
+  PRECONDITION(can_cast_type<code_typet>(type));
+  validate_type(type);
   return static_cast<code_typet &>(type);
 }
 
+
 /*! \brief arrays with given size
 */
 class array_typet:public type_with_subtypet

driver/run.py

@@ -217,6 +217,10 @@ def prepare_scan(cmdline):
         configuration["detected_entry_points_path"] = \
             os.path.join(cmdline.common_dir, "detected_entry_points.json")
 
+    if not configuration["di_configuration_path"]:
+        configuration["di_configuration_path"] = \
+            os.path.join(cmdline.common_dir, "di_configuration.json")
+
     if not configuration["collected_classes_path"]:
         configuration["collected_classes_path"] = \
             os.path.join(cmdline.common_dir, "collected_classes.json")