Requested updates in the review of the PR diffblue#133.

Author: marek-trtik

src/taint-slicer/instrumentation_props.cpp

@@ -23,90 +23,52 @@ instrumentation_props data structure.
 
 #include <taint-slicer/instrumentation_props.h>
 #include <goto-programs/remove_returns.h>
+#include <java_bytecode/java_types.h>
+#include <java_bytecode/expr2java.h>
 #include <util/prefix.h>
 #include <util/msgstream.h>
 #include <deque>
 
-static std::string parse_type_name(const typet &type)
+bool is_primitive_type_name(const std::string &datatype, const namespacet &ns)
 {
-  const typet * restype = &type;
-  if(type.id()==ID_pointer)
-    restype=&to_pointer_type(type).subtype();
-  else if(type.id()==ID_array)
-    restype=&to_array_type(type).subtype();
-  if(restype->id()==ID_signedbv)
-  {
-    const signedbv_typet &sbv=to_signedbv_type(*restype);
-    if(sbv.get_width()==8UL)
-      return as_string(ID_char);
-    if(sbv.get_width()==16UL)
-      return as_string(ID_short);
-    if(sbv.get_width()==32UL)
-      return as_string(ID_int);
-    if(sbv.get_width()==64UL)
-      return as_string(ID_long);
-    throw std::logic_error(
-            msgstream() << "ERROR: unexpected bit-width '"
-                        << sbv.get_width() << "' of signedbv type. Valid sizes "
-                        << "are 8, 16, 32, and 64.");
-  }
-  if(restype->id()==ID_unsignedbv)
-  {
-    const unsignedbv_typet &ubv=to_unsignedbv_type(*restype);
-    if(ubv.get_width()==8UL)
-      return as_string(ID_byte);
-    if(ubv.get_width()==16UL)
-      return as_string(ID_unsigned_short_int);
-    if(ubv.get_width()==32UL)
-      return as_string(ID_unsigned_int);
-    if(ubv.get_width()==64UL)
-      return as_string(ID_unsigned_long_int);
-    throw std::logic_error(
-            msgstream() << "ERROR: unexpected bit-width '"
-                        << ubv.get_width() << "' of unsignedbv type. Valid "
-                        << "sizes are 8, 16, 32 and 64.");
-  }
-  if(restype->id()!=ID_symbol)
-    throw std::logic_error(
-            msgstream() << "ERROR: expecting the '"
-                        << as_string(ID_symbol) << "' type id, but received '"
-                        << as_string(restype->id()) << "'.");
-  return as_string(to_symbol_type(*restype).get_identifier());
+  return datatype==type2java(java_boolean_type(), ns) ||
+         datatype==type2java(java_boolean_type(), ns) ||
+         datatype==type2java(java_byte_type(), ns) ||
+         datatype==type2java(java_char_type(), ns) ||
+         datatype==type2java(java_short_type(), ns) ||
+         datatype==type2java(java_int_type(), ns) ||
+         datatype==type2java(java_long_type(), ns) ||
+         datatype==type2java(java_float_type(), ns) ||
+         datatype==type2java(java_double_type(), ns) ;
 }
 
-bool is_primitive_type_name(const std::string &datatype)
+static std::string parse_type_name(const typet &type, const namespacet &ns)
 {
-  static const std::set<std::string> names=
-  {
-    as_string(ID_bool),
-    as_string(ID_byte),
-    as_string(ID_char),
-    as_string(ID_unsigned_char),
-    as_string(ID_short),
-    as_string(ID_unsigned_short_int),
-    as_string(ID_int),
-    as_string(ID_unsigned_int),
-    as_string(ID_long),
-    as_string(ID_unsigned_long_int),
-    as_string(ID_unsigned_long_long_int),
-    as_string(ID_unsigned_int128),
-    as_string(ID_float),
-    as_string(ID_double),
-    as_string(ID_long_double)
-  };
-  return names.count(datatype)==1UL;
+  if(type.id()==ID_pointer)
+    return parse_type_name(to_pointer_type(type).subtype(), ns);
+  if(type.id()==ID_array)
+    return parse_type_name(to_array_type(type).subtype(), ns);
+  if(type.id()==ID_symbol)
+    return as_string(to_symbol_type(type).get_identifier());
+  const std::string result=type2java(type, ns);
+  if(!is_primitive_type_name(result, ns))
+    throw std::logic_error(
+            msgstream() << "ERROR: expecting a primitive data type, "
+                           "but received '" << result << "'.");
+  return result;
 }
 
 bool is_java_array_type_name(const std::string &datatype)
 {
   return has_prefix(datatype, "java::array[") && *datatype.rbegin()==']';
 }
 
-bool does_instrumentation_of_type_require_subclass(const std::string &datatype)
+bool does_instrumentation_of_type_require_subclass(
+  const std::string &datatype, const namespacet &ns)
 {
-  return is_primitive_type_name(datatype) ||
-         is_java_array_type_name(datatype)
-          || datatype=="java::java.lang.Object";
+  return is_primitive_type_name(datatype, ns) ||
+         is_java_array_type_name(datatype) ||
+         datatype=="java::java.lang.Object";
 }
 
 static std::string get_return_type_name_from_function_name(
@@ -116,7 +78,7 @@ static std::string get_return_type_name_from_function_name(
   typet t=symbol_table.lookup(fname+RETURN_VALUE_SUFFIX).type;
   if(t.id()==ID_pointer)
     t=to_pointer_type(t).subtype();
-  return parse_type_name(t);
+  return parse_type_name(t, namespacet(symbol_table));
 }
 
 /*******************************************************************\
@@ -254,9 +216,10 @@ void taint_instrumentation_propst::build_map_from_typenames_to_tokennames(
       else
       {
         datatype=parse_type_name(
-          fn_type.parameters().at(arg_token.get_argidx()).type());
+          fn_type.parameters().at(arg_token.get_argidx()).type(),
+          program.get_namespace());
       }
-      assert(is_primitive_type_name(datatype)
+      assert(is_primitive_type_name(datatype, program.get_namespace())
              || program.get_symbol_table().has_symbol(datatype));
       datatypes[datatype].insert(arg_token.get_token_name());
     }
@@ -374,7 +337,10 @@ void taint_build_instrumentation_props(
   }
 }
 
-void dump_as_json(const taint_instrumentation_propst &props, json_objectt &out)
+void dump_as_json(
+  const taint_instrumentation_propst &props,
+  json_objectt &out,
+  const namespacet &ns)
 {
   {
     json_arrayt out_types;
@@ -386,7 +352,7 @@ void dump_as_json(const taint_instrumentation_propst &props, json_objectt &out)
       json_objectt out_type_props;
       out_type_props["type_name"]=json_stringt(elem.first);
       out_type_props["shadow_vars"]=out_tokens;
-      if(does_instrumentation_of_type_require_subclass(elem.first))
+      if(does_instrumentation_of_type_require_subclass(elem.first, ns))
         out_type_props["make_subclass"]=json_truet();
       else
         out_type_props["make_subclass"]=json_falset();

src/taint-slicer/instrumentation_props.h

@@ -125,10 +125,14 @@ void taint_build_instrumentation_props(
   std::vector<taint_instrumentation_propst> &output);
 
 
-bool is_primitive_type_name(const std::string &datatype);
+bool is_primitive_type_name(const std::string &datatype, const namespacet &ns);
 bool is_java_array_type_name(const std::string &datatype);
-bool does_instrumentation_of_type_require_subclass(const std::string &datatype);
+bool does_instrumentation_of_type_require_subclass(
+  const std::string &datatype, const namespacet &ns);
 
-void dump_as_json(const taint_instrumentation_propst &props, json_objectt &out);
+void dump_as_json(
+  const taint_instrumentation_propst &props,
+  json_objectt &out,
+  const namespacet &ns);
 
 #endif

src/taint-slicer/slicer.cpp

@@ -94,7 +94,7 @@ void taint_slicert::compute_slice()
   for(std::size_t i=0U; i!=instrumentation_props.size(); ++i)
   {
     json_objectt jobj;
-    dump_as_json(instrumentation_props.at(i),jobj);
+    dump_as_json(instrumentation_props.at(i), jobj, program->get_namespace());
     std::ofstream  ostr(
       fileutl_concatenate_file_paths(
         results_dir,