Skip to content

Code for Object.getClass in bytecode conversion #945

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Jun 14, 2017
Merged

Code for Object.getClass in bytecode conversion #945

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
e9e3989
Providing code for Object.getClass() in bytecode conversion
romainbrenguier May 13, 2017
db1cd5f
Cleaning the initialization of string expressions from constants
romainbrenguier May 13, 2017
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
95 changes: 95 additions & 0 deletions src/java_bytecode/java_string_library_preprocess.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Copy link
Contributor

@mgudemann mgudemann Jun 12, 2017

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

what does the constant 6 represent?

Copy link
Contributor Author

@romainbrenguier romainbrenguier Jun 12, 2017

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is to remove the "java::" prefix. (see the comment on line 1778 https://github.com/diffblue/cbmc/pull/945/files/556dc9a262b23686d07d9019f5d5f69bf8fee5ab#diff-333608a53b33706cdc28c1f3c1d0ca16R1778)
Maybe std::string("java::").length() would be more explicit...

> 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());
Copy link
Contributor

@mgudemann mgudemann Jun 12, 2017

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

does this work for static functions where no this parameter exists?

Copy link
Contributor Author

@romainbrenguier romainbrenguier Jun 12, 2017

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No, this is really meant to be only used for implementing the Object.getClass() method which is not declared as static by Java.


// 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:
Expand Down Expand Up @@ -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);
}
5 changes: 5 additions & 0 deletions src/java_bytecode/java_string_library_preprocess.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
50 changes: 4 additions & 46 deletions src/solvers/refinement/string_constraint_generator_constants.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,29 +13,6 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com

/*******************************************************************\

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
Expand Down Expand Up @@ -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

Expand All @@ -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);
}