Merge pull request #945 from romainbrenguier/feature/object-get-class

Code for Object.getClass in bytecode conversion

Author: forejtv

src/java_bytecode/java_string_library_preprocess.cpp

@@ -1723,6 +1723,93 @@ codet java_string_library_preprocesst::make_string_to_char_array_code(
 
 /*******************************************************************\
 
+Function: java_string_library_preprocesst::make_object_get_class_code
+
+  Inputs:
+    type - type of the function called
+    loc - location in the source
+    symbol_table - the symbol table
+
+  Outputs: Code corresponding to
+          > Class class1;
+          > string_expr1 = substr(this->@class_identifier, 6)
+          > class1=Class.forName(string_expr1)
+          > return class1
+
+  Purpose: Used to provide our own implementation of the
+           java.lang.Object.getClass() function.
+
+\*******************************************************************/
+
+codet java_string_library_preprocesst::make_object_get_class_code(
+    const code_typet &type,
+    const source_locationt &loc,
+    symbol_tablet &symbol_table)
+{
+  code_typet::parameterst params=type.parameters();
+  exprt this_obj=symbol_exprt(params[0].get_identifier(), params[0].type());
+
+  // Code to be returned
+  code_blockt code;
+
+  // > Class class1;
+  pointer_typet class_type(symbol_table.lookup("java::java.lang.Class").type);
+  symbolt class1_sym=get_fresh_aux_symbol(
+    class_type, "class_symbol", "class_symbol", loc, ID_java, symbol_table);
+  symbol_exprt class1=class1_sym.symbol_expr();
+  code.add(code_declt(class1));
+
+  // class_identifier is this->@class_identifier
+  member_exprt class_identifier(
+    dereference_exprt(this_obj, this_obj.type().subtype()),
+    "@class_identifier",
+    string_typet());
+
+  // string_expr = cprover_string_literal(this->@class_identifier)
+  string_exprt string_expr=fresh_string_expr(loc, symbol_table, code);
+  code.add(
+    code_assign_function_to_string_expr(
+      string_expr,
+      ID_cprover_string_literal_func,
+      {class_identifier},
+      symbol_table));
+
+  // string_expr1 = substr(string_expr, 6)
+  // We do this to remove the "java::" prefix
+  string_exprt string_expr1=fresh_string_expr(loc, symbol_table, code);
+  code.add(
+    code_assign_function_to_string_expr(
+      string_expr1,
+      ID_cprover_string_substring_func,
+      {string_expr, from_integer(6, java_int_type())},
+      symbol_table));
+
+  // string1 = (String*) string_expr
+  pointer_typet string_ptr_type(
+    symbol_table.lookup("java::java.lang.String").type);
+  exprt string1=allocate_fresh_string(string_ptr_type, loc, symbol_table, code);
+  code.add(
+    code_assign_string_expr_to_new_java_string(
+      string1, string_expr1, loc, symbol_table));
+
+  // > class1 = Class.forName(string1)
+  code_function_callt fun_call;
+  fun_call.function()=symbol_exprt(
+    "java::java.lang.Class.forName:(Ljava/lang/String;)Ljava/lang/Class;");
+  fun_call.lhs()=class1;
+  fun_call.arguments().push_back(string1);
+  code_typet fun_type;
+  fun_type.return_type()=string1.type();
+  fun_call.function().type()=fun_type;
+  code.add(fun_call);
+
+  // > return class1;
+  code.add(code_returnt(class1));
+  return code;
+}
+
+/*******************************************************************\
+
 Function: java_string_library_preprocesst::make_function_from_call
 
   Inputs:
@@ -2545,4 +2632,12 @@ void java_string_library_preprocesst::initialize_conversion_table()
   cprover_equivalent_to_java_string_returning_function
     ["java::java.lang.Integer.toString:(I)Ljava/lang/String;"]=
       ID_cprover_string_of_int_func;
+  conversion_table
+    ["java::java.lang.Object.getClass:()Ljava/lang/Class;"]=
+      std::bind(
+        &java_string_library_preprocesst::make_object_get_class_code,
+        this,
+        std::placeholders::_1,
+        std::placeholders::_2,
+        std::placeholders::_3);
 }

src/java_bytecode/java_string_library_preprocess.h

@@ -151,6 +151,11 @@ class java_string_library_preprocesst:public messaget
     const source_locationt &loc,
     symbol_tablet &symbol_table);
 
+  codet make_object_get_class_code(
+    const code_typet &type,
+    const source_locationt &loc,
+    symbol_tablet &symbol_table);
+
   // Auxiliary functions
   codet code_for_scientific_notation(
     const exprt &arg,

src/solvers/refinement/string_constraint_generator_constants.cpp

@@ -13,29 +13,6 @@ Author: Romain Brenguier, [email protected]
 
 /*******************************************************************\
 
-Function: string_constraint_generatort::extract_java_string
-
-  Inputs: a symbol expression representing a java literal
-
- Outputs: a string constant
-
- Purpose: extract java string from symbol expression when they are encoded
-          inside the symbol name
-
-\*******************************************************************/
-
-irep_idt string_constraint_generatort::extract_java_string(
-  const symbol_exprt &s)
-{
-  std::string tmp=id2string(s.get_identifier());
-  std::string prefix("java::java.lang.String.Literal.");
-  assert(has_prefix(tmp, prefix));
-  std::string value=tmp.substr(prefix.length());
-  return irep_idt(value);
-}
-
-/*******************************************************************\
-
 Function: string_constraint_generatort::add_axioms_for_constant
 
   Inputs: a string constant
@@ -107,7 +84,9 @@ string_exprt string_constraint_generatort::add_axioms_for_empty_string(
 
 Function: string_constraint_generatort::add_axioms_from_literal
 
-  Inputs: function application with an argument which is a string literal
+  Inputs:
+    f - function application with an argument which is a string literal
+        that is a constant with a string value.
 
  Outputs: string expression
 
@@ -123,28 +102,7 @@ string_exprt string_constraint_generatort::add_axioms_from_literal(
   assert(args.size()==1); // Bad args to string literal?
 
   const exprt &arg=args[0];
-  irep_idt sval;
-
-  assert(arg.operands().size()==1);
-  if(arg.op0().operands().size()==2 &&
-     arg.op0().op0().id()==ID_string_constant)
-  {
-    // C string constant
-    const exprt &s=arg.op0().op0();
-    sval=to_string_constant(s).get_value();
-  }
-  else
-  {
-    // Java string constant
-    assert(false); // TODO: Check if used. On the contrary, discard else.
-    assert(arg.id()==ID_symbol);
-    const exprt &s=arg.op0();
-
-    // It seems the value of the string is lost,
-    // we need to recover it from the identifier
-    sval=extract_java_string(to_symbol_expr(s));
-  }
-
+  irep_idt sval=to_constant_expr(arg).get_value();
   const refined_string_typet &ref_type=to_refined_string_type(f.type());
   return add_axioms_for_constant(sval, ref_type);
 }