From 0dcb773413f26521f89f59117e414531f77947f4 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 1 Jun 2017 10:31:46 +0100 Subject: [PATCH 1/4] Change the step at which we replace String methods code We now do this at the end of the bytecode conversion, in function java_bytecode_languaget::final instead of the middle of the conversion. --- src/java_bytecode/java_bytecode_language.cpp | 33 ++++++++++++++++++++ src/java_bytecode/java_bytecode_language.h | 2 ++ 2 files changed, 35 insertions(+) diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index 404ffc95c69..12c59e9d938 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -799,6 +799,36 @@ 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) +{ + for(auto &id_symbol_pair : context.symbols) + { + const irep_idt &id=id_symbol_pair.first; + symbolt &symbol=id_symbol_pair.second; + if(symbol.type.id()==ID_code) + { + 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 + symbol.value=generated_code; + } + } +} + +/*******************************************************************\ + Function: java_bytecode_languaget::final Inputs: @@ -816,6 +846,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) diff --git a/src/java_bytecode/java_bytecode_language.h b/src/java_bytecode/java_bytecode_language.h index 929cc354518..8fbf96b06e5 100644 --- a/src/java_bytecode/java_bytecode_language.h +++ b/src/java_bytecode/java_bytecode_language.h @@ -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; From ca32a0a1d1045c9d344d7e4f4ef1353d62ee9052 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 1 Jun 2017 15:23:41 +0100 Subject: [PATCH 2/4] Removing string conversion from method conversion --- src/java_bytecode/java_bytecode_convert_method.cpp | 6 ------ 1 file changed, 6 deletions(-) diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index e72ed43078a..2f9de7497ad 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -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( - id, to_code_type(symbol.type), loc, symbol_table); - symbol_table.add(symbol); } From dcf7614d4684b09ec63a9a76c638e56060e1d6d4 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 6 Jun 2017 14:54:10 +0100 Subject: [PATCH 3/4] Correcting replace_string_methods to not overwrite the map we iterate on The previous implementation was writing in the map while iterating on it which could cause some bugs. The new implementation does this in two steps to avoid the problem. --- src/java_bytecode/java_bytecode_language.cpp | 25 +++++++++++++------- 1 file changed, 16 insertions(+), 9 deletions(-) diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index 12c59e9d938..c38b8d735fa 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -812,17 +812,24 @@ Function: java_bytecode_languaget::replace_string_methods void java_bytecode_languaget::replace_string_methods( symbol_tablet &context) { - for(auto &id_symbol_pair : context.symbols) + // Symbols that have code type are potentialy to be replaced + std::list code_symbols; + forall_symbols(symbol, context.symbols) { - const irep_idt &id=id_symbol_pair.first; - symbolt &symbol=id_symbol_pair.second; - if(symbol.type.id()==ID_code) + 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()) { - 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 - symbol.value=generated_code; + // Replace body of the function by code generated by string preprocess + symbolt &symbol=context.lookup(id); + symbol.value=generated_code; } } } From 65f2e36965e310f6e8adbe0b8c7bfa700a740113 Mon Sep 17 00:00:00 2001 From: Joel Allred Date: Wed, 24 May 2017 18:05:54 +0100 Subject: [PATCH 4/4] Overwrite String type String classes that are present in a loaded model will generate a type that may be different from the internal type constructed for Java strings in cbmc. Thus we now create a String type and write it in the table, possibly overwriting a pre-existing Java string type. --- src/java_bytecode/java_bytecode_convert_class.cpp | 9 +++++---- src/java_bytecode/java_string_library_preprocess.cpp | 5 ++++- 2 files changed, 9 insertions(+), 5 deletions(-) diff --git a/src/java_bytecode/java_bytecode_convert_class.cpp b/src/java_bytecode/java_bytecode_convert_class.cpp index b16e3a74f87..c92c016bd02 100644 --- a/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/src/java_bytecode/java_bytecode_convert_class.cpp @@ -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)) + + 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); } diff --git a/src/java_bytecode/java_string_library_preprocess.cpp b/src/java_bytecode/java_string_library_preprocess.cpp index 34e5f84bfd7..199d472ea0e 100644 --- a/src/java_bytecode/java_string_library_preprocess.cpp +++ b/src/java_bytecode/java_string_library_preprocess.cpp @@ -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)); } /*******************************************************************\