Skip to content

Overwrite String functions in final step of bytecode conversion #983

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 4 commits into from
Jun 6, 2017
Merged

Overwrite String functions in final step of bytecode conversion #983

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
0dcb773
Change the step at which we replace String methods code
romainbrenguier Jun 1, 2017
ca32a0a
Removing string conversion from method conversion
romainbrenguier Jun 1, 2017
dcf7614
Correcting replace_string_methods to not overwrite the map we iterate on
romainbrenguier Jun 6, 2017
65f2e36
Overwrite String type
May 24, 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
9 changes: 5 additions & 4 deletions src/java_bytecode/java_bytecode_convert_class.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -45,13 +45,14 @@ class java_bytecode_convert_classt:public messaget
{
add_array_types();

if(parse_tree.loading_successful)
bool loading_success=parse_tree.loading_successful;
if(loading_success)
convert(parse_tree.parsed_class);
else if(string_preprocess.is_known_string_type(
parse_tree.parsed_class.name))

Copy link
Contributor

Choose a reason for hiding this comment

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

These changes make me a little bit anxious that the semantics of the code have changed. Before the change, the if...else if...else cascading conditional statement means that there is a single set of 3 possible consequence expressions, only 1 of which will be evaluated.

This change has essentially broken the one set (of consequent statements/expressions) into two sets, one with one consequence and the other with 2, both of which can be evaluated independently of each other, just based on their conditions.

What I mean with this, that only one consequent expression could be evaluated at a point in time (because they were exclusive due to the way the conditional statement was written), now 2 consequent expressions can be evaluated at the same time. Do we want this?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Yes we now want to replace string types even if they are loaded.
The idea behind this is that we will provide through the models-library a String class which will be loaded in the classpath, but we still want to use the type we define internally for strings.
The class still needs to be converted though, because we want to use some methods that are defined in the String.class provided.

if(string_preprocess.is_known_string_type(parse_tree.parsed_class.name))
string_preprocess.add_string_type(
parse_tree.parsed_class.name, symbol_table);
else
else if(!loading_success)
generate_class_stub(parse_tree.parsed_class.name);
}

Expand Down
6 changes: 0 additions & 6 deletions src/java_bytecode/java_bytecode_convert_method.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1550,17 +1550,11 @@ codet java_bytecode_convert_methodt::convert_instructions(
symbol.type=arg0.type();
symbol.value.make_nil();
symbol.mode=ID_java;

assign_parameter_names(
to_code_type(symbol.type),
symbol.name,
symbol_table);

// The string refinement module may provide a definition for this
// function.
symbol.value=string_preprocess.code_for_function(
Copy link
Contributor

Choose a reason for hiding this comment

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

Why is this being removed? The commit message "Removing string conversion from method conversion" is not explicit enough in this regard? It might be more apparent to someone who is already familiar with the code, but I'm not, so this is potentially changing the semantics of this code if the replace_string_methods method added below is not essentially doing the same thing at a different point in time.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

The method that is added below (replace_string_methods) does the same thing. But instead of doing it in the middle of convert_instructions it does so at the end of the bytecode conversion by going through the symbol table.
The potential change in semantics is that we now convert methods that were forgotten before because we were not getting in this particular branch of convert_instructions, but this should be an improvement.

id, to_code_type(symbol.type), loc, symbol_table);

symbol_table.add(symbol);
}

Expand Down
40 changes: 40 additions & 0 deletions src/java_bytecode/java_bytecode_language.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -799,6 +799,43 @@ void java_bytecode_languaget::convert_lazy_method(

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

Function: java_bytecode_languaget::replace_string_methods

Inputs:
context - a symbol table

Purpose: Replace methods of the String library that are in the symbol table
by code generated by string_preprocess.

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

void java_bytecode_languaget::replace_string_methods(
symbol_tablet &context)
{
// Symbols that have code type are potentialy to be replaced
std::list<symbolt> code_symbols;
forall_symbols(symbol, context.symbols)
{
if(symbol->second.type.id()==ID_code)
code_symbols.push_back(symbol->second);
}

for(const auto &symbol : code_symbols)
{
const irep_idt &id=symbol.name;
exprt generated_code=string_preprocess.code_for_function(
id, to_code_type(symbol.type), symbol.location, context);
if(generated_code.is_not_nil())
{
// Replace body of the function by code generated by string preprocess
symbolt &symbol=context.lookup(id);
symbol.value=generated_code;
}
}
}

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

Function: java_bytecode_languaget::final

Inputs:
Expand All @@ -816,6 +853,9 @@ bool java_bytecode_languaget::final(symbol_tablet &symbol_table)
*/
java_internal_additions(symbol_table);

// Replace code of String methods calls by code we generate
replace_string_methods(symbol_table);

main_function_resultt res=
get_main_symbol(symbol_table, main_class, get_message_handler());
if(res.stop_convert)
Expand Down
2 changes: 2 additions & 0 deletions src/java_bytecode/java_bytecode_language.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -49,6 +49,8 @@ class java_bytecode_languaget:public languaget
symbol_tablet &context,
const std::string &module) override;

void replace_string_methods(symbol_tablet &context);

virtual bool final(
symbol_tablet &context) override;

Expand Down
5 changes: 4 additions & 1 deletion 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 @@ -319,7 +319,10 @@ void java_string_library_preprocesst::add_string_type(
string_symbol.type=string_type;
string_symbol.is_type=true;

symbol_table.add(string_symbol);
// Overwrite any pre-existing symbol in the table, e.g. created by
// a loaded model.
symbol_table.remove(string_symbol.name);
assert(!symbol_table.add(string_symbol));
}

/*******************************************************************\
Expand Down