Add class for randomly selecting a concrete child of an abstract class

When generating a pointer to an abstract type, replace it with a pointer
to a concrete type that derives from that abstract type.

Author: thk123

src/java_bytecode/Makefile

@@ -2,6 +2,7 @@ SRC = bytecode_info.cpp \
       character_refine_preprocess.cpp \
       ci_lazy_methods.cpp \
       expr2java.cpp \
+      get_concrete_class_at_random.cpp \
       jar_file.cpp \
       java_bytecode_convert_class.cpp \
       java_bytecode_convert_method.cpp \

src/java_bytecode/get_concrete_class_at_random.cpp

@@ -0,0 +1,100 @@
+// Copyright 2016-2017 DiffBlue Limited. All Rights Reserved.
+
+/// \file
+/// Java Bytecode Language Conversion
+
+#include "get_concrete_class_at_random.h"
+
+#include <algorithm>
+#include <random>
+
+#include <util/namespace.h>
+#include <util/std_types.h>
+#include <util/symbol_table.h>
+
+#include <goto-programs/class_hierarchy.h>
+
+/// Get type the pointer is pointing to, replacing it with a concrete
+/// implementation when it is abstract.
+/// \param `pointer_type`: The type of the pointer
+/// \return The subtype of the pointer. If this is an abstract class then we
+///   will randomly select a concrete child class.
+typet get_concrete_class_at_randomt::operator()(
+  const pointer_typet &pointer_type)
+{
+  const typet &subtype=ns.follow(pointer_type.subtype());
+  if(subtype.id()==ID_struct)
+  {
+    const class_typet &class_type=to_class_type(subtype);
+
+    if(class_type.is_class() && class_type.is_abstract())
+    {
+      return select_concrete_type(class_type);
+    }
+  }
+
+  // Here we must return the original subtype as if it is a pointer to a java
+  // array java_object_factoryt::gen_nondet_array_init relies on the subtype
+  // being a ID_symbol, here we have followed the symbol to its resolution.
+  // Perhaps java_object_factoryt::gen_nondet_array_init should support this
+  // Perhaps select_concrete_type when it fails should also ensure it doesn't
+  // modify the subtype (currently if no concrete implementations we'd do the same
+  // - swap a symbol to a struct
+  return pointer_type.subtype();
+}
+
+/// Randomly select a concrete sub-class of an abstract class or interface This
+/// can be then used when analyzing the function.
+/// \param `abstract_type`: an class type that is abstract (i.e. either an
+/// interface or a abstract class).
+/// \return A class_typet that the GOTO code should instantiate to fill this
+///   type. This will be a concrete type unless no concrete types are found that
+///   inherit from the abstract_type. `
+class_typet get_concrete_class_at_randomt::select_concrete_type(
+  const class_typet &abstract_type)
+{
+  if(!abstract_type.is_abstract())
+    throw std::invalid_argument("abstract_type");
+
+  const symbol_tablet &symbol_table=ns.get_symbol_table();
+  // abstract class - we should find a derived class ideally to test with
+  class_hierarchyt class_hierachy;
+  class_hierachy(symbol_table);
+  class_hierarchyt::idst child_ids=
+    class_hierachy.get_children_trans(abstract_type.get_string(ID_name));
+
+  // filter out abstract classes
+  class_hierarchyt::idst concrete_childen;
+  std::copy_if(
+    child_ids.begin(),
+    child_ids.end(),
+    std::back_inserter(concrete_childen),
+    [&] (const irep_idt &child_class_id)
+    {
+      const symbolt &type_symbol=symbol_table.lookup(child_class_id);
+      const class_typet &child_type=to_class_type(type_symbol.type);
+      return child_type.is_class() && !child_type.is_abstract();
+    });
+
+
+  if(concrete_childen.size()>0)
+  {
+    //Will be used to obtain a seed for the random number engine
+    std::random_device rd;
+    //Standard mersenne_twister_engine seeded with rd()
+    std::mt19937 gen(rd());
+    std::uniform_int_distribution<unsigned long> class_selector(
+      0, concrete_childen.size()-1);
+    unsigned long selected_class_index=class_selector(gen);
+    const symbolt &type_symbol=
+      symbol_table.lookup(concrete_childen[selected_class_index]);
+    const class_typet &child_type=to_class_type(type_symbol.type);
+    return child_type;
+  }
+  else
+  {
+    // else no children in the symbol table - here the best we can do is
+    // mock the interface/abstract object
+    return abstract_type;
+  }
+}

src/java_bytecode/get_concrete_class_at_random.h

@@ -0,0 +1,32 @@
+/*******************************************************************\
+
+Module: Java Bytecode Language Conversion
+
+Author: DiffBlue Limited. All rights reserved.
+
+\*******************************************************************/
+
+/// \file
+/// Java Bytecode Language Conversion
+
+#ifndef CPROVER_JAVA_BYTECODE_GET_CONCRETE_CLASS_AT_RANDOM_H
+#define CPROVER_JAVA_BYTECODE_GET_CONCRETE_CLASS_AT_RANDOM_H
+
+#include <util/std_types.h>
+
+class namespacet;
+
+class get_concrete_class_at_randomt
+{
+public:
+  explicit get_concrete_class_at_randomt (const namespacet &ns):ns(ns)
+  {}
+
+  typet operator()(const pointer_typet &pointer_type);
+
+private:
+  const namespacet& ns;
+  class_typet select_concrete_type(const class_typet &abstract_type);
+};
+
+#endif // CPROVER_JAVA_BYTECODE_GET_CONCRETE_CLASS_AT_RANDOM_H

src/java_bytecode/java_object_factory.cpp

@@ -27,6 +27,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <goto-programs/goto_functions.h>
 
+#include <java_bytecode/get_concrete_class_at_random.h>
+
 #include "java_types.h"
 #include "java_utils.h"
 
@@ -396,6 +398,7 @@ void java_object_factoryt::gen_nondet_pointer_init(
   {
     const struct_typet &struct_type=to_struct_type(subtype);
     const irep_idt &struct_tag=struct_type.get_tag();
+
     // If this is a recursive type of some kind, set null.
     if(!recursion_set.insert(struct_tag).second)
     {
@@ -854,12 +857,23 @@ exprt object_factory(
   irep_idt identifier=id2string(goto_functionst::entry_point())+
     "::"+id2string(base_name);
 
+  typet real_type=type;
+  if(type.id()==ID_pointer && type.subtype().id()==ID_symbol)
+  {
+    const pointer_typet &pointer_type=to_pointer_type(type);
+    const namespacet ns(symbol_table);
+    get_concrete_class_at_randomt get_concrete_class_at_random(ns);
+    const typet &resolved_type=
+      get_concrete_class_at_random(pointer_type);
+    real_type.subtype()=resolved_type;
+  }
+
   auxiliary_symbolt main_symbol;
   main_symbol.mode=ID_java;
   main_symbol.is_static_lifetime=false;
   main_symbol.name=identifier;
   main_symbol.base_name=base_name;
-  main_symbol.type=type;
+  main_symbol.type=real_type;
   main_symbol.location=loc;
 
   exprt object=main_symbol.symbol_expr();
@@ -871,7 +885,7 @@ exprt object_factory(
   std::vector<const symbolt *> symbols_created;
   symbols_created.push_back(main_symbol_ptr);
 
-  symbolt &aux_symbol=new_tmp_symbol(symbol_table, loc, type);
+  symbolt &aux_symbol=new_tmp_symbol(symbol_table, loc, real_type);
   aux_symbol.is_static_lifetime=true;
 
   java_object_factoryt state(