diff --git a/jbmc/src/java_bytecode/expr2java.cpp b/jbmc/src/java_bytecode/expr2java.cpp index cda39945d18..e477ab5cc8d 100644 --- a/jbmc/src/java_bytecode/expr2java.cpp +++ b/jbmc/src/java_bytecode/expr2java.cpp @@ -23,6 +23,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include "java_qualifiers.h" +#include "java_string_literal_expr.h" #include "java_types.h" std::string expr2javat::convert(const typet &src) @@ -414,8 +415,11 @@ std::string expr2javat::convert_with_precedence( id2string(src.get(ID_component_name)) + ")"; } - else if(src.id()==ID_java_string_literal) - return '"'+MetaString(src.get_string(ID_value))+'"'; + else if( + const auto &literal = expr_try_dynamic_cast(src)) + { + return '"' + MetaString(id2string(literal->value())) + '"'; + } else if(src.id()==ID_constant) return convert_constant(to_constant_expr(src), precedence=16); else diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index 2e2dbf19fea..44878fe8710 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "java_bytecode_convert_method_class.h" #include "java_static_initializers.h" #include "java_string_library_preprocess.h" +#include "java_string_literal_expr.h" #include "java_types.h" #include "java_utils.h" #include "pattern.h" @@ -1313,7 +1314,7 @@ code_blockt java_bytecode_convert_methodt::convert_instructions( PRECONDITION(op.empty() && results.size() == 1); INVARIANT( - arg0.id() != ID_java_string_literal && arg0.id() != ID_type, + !can_cast_expr(arg0) && arg0.id() != ID_type, "String and Class literals should have been lowered in " "generate_constant_global_variables"); diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index 31f286026f6..2ed93d3eac2 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -26,19 +26,20 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include "ci_lazy_methods.h" #include "java_bytecode_concurrency_instrumentation.h" #include "java_bytecode_convert_class.h" #include "java_bytecode_convert_method.h" -#include "java_bytecode_internal_additions.h" #include "java_bytecode_instrument.h" -#include "java_bytecode_typecheck.h" -#include "java_entry_point.h" +#include "java_bytecode_internal_additions.h" #include "java_bytecode_parser.h" +#include "java_bytecode_typecheck.h" #include "java_class_loader.h" -#include "java_string_literals.h" +#include "java_entry_point.h" #include "java_static_initializers.h" +#include "java_string_literal_expr.h" +#include "java_string_literals.h" #include "java_utils.h" -#include "ci_lazy_methods.h" #include "expr2java.h" #include "load_method_by_regex.h" @@ -417,12 +418,12 @@ static exprt get_ldc_result( address_of_exprt( get_or_create_class_literal_symbol(class_id, symbol_table)); } - else if(ldc_arg0.id() == ID_java_string_literal) + else if( + const auto &literal = + expr_try_dynamic_cast(ldc_arg0)) { - return - address_of_exprt( - get_or_create_string_literal_symbol( - ldc_arg0, symbol_table, string_refinement_enabled)); + return address_of_exprt(get_or_create_string_literal_symbol( + *literal, symbol_table, string_refinement_enabled)); } else { diff --git a/jbmc/src/java_bytecode/java_bytecode_parser.cpp b/jbmc/src/java_bytecode/java_bytecode_parser.cpp index c692592a39b..07d882cf94e 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parser.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_parser.cpp @@ -21,9 +21,10 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include "bytecode_info.h" #include "java_bytecode_parse_tree.h" +#include "java_string_literal_expr.h" #include "java_types.h" -#include "bytecode_info.h" #ifdef DEBUG #include @@ -839,9 +840,7 @@ void java_bytecode_parsert::rconstant_pool() case CONSTANT_String: { // ldc turns these into references to java.lang.String - exprt string_literal(ID_java_string_literal); - string_literal.set(ID_value, pool_entry(it->ref1).s); - it->expr=string_literal; + it->expr = java_string_literal_exprt{pool_entry(it->ref1).s}; } break; diff --git a/jbmc/src/java_bytecode/java_bytecode_typecheck_expr.cpp b/jbmc/src/java_bytecode/java_bytecode_typecheck_expr.cpp index f7d75b5f690..d815d0a1559 100644 --- a/jbmc/src/java_bytecode/java_bytecode_typecheck_expr.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_typecheck_expr.cpp @@ -17,10 +17,11 @@ Author: Daniel Kroening, kroening@kroening.com #include #include "java_pointer_casts.h" -#include "java_types.h" -#include "java_utils.h" #include "java_root_class.h" #include "java_string_library_preprocess.h" +#include "java_string_literal_expr.h" +#include "java_types.h" +#include "java_utils.h" void java_bytecode_typecheckt::typecheck_expr(exprt &expr) { @@ -39,7 +40,7 @@ void java_bytecode_typecheckt::typecheck_expr(exprt &expr) typecheck_expr(*it); INVARIANT( - expr.id() != ID_java_string_literal, + !can_cast_expr(expr), "String literals should have been converted to constant globals " "before typecheck_expr"); diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/jbmc/src/java_bytecode/java_entry_point.cpp index c4fde19ac3d..f71af068e54 100644 --- a/jbmc/src/java_bytecode/java_entry_point.cpp +++ b/jbmc/src/java_bytecode/java_entry_point.cpp @@ -135,14 +135,10 @@ static void java_static_lifetime_init( // and we can refer to them later when we initialize input values. for(const auto &val : object_factory_parameters.string_input_values) { - exprt my_literal(ID_java_string_literal); - my_literal.set(ID_value, val); // We ignore the return value of the following call, we just need to // make sure the string is in the symbol table. get_or_create_string_literal_symbol( - my_literal, - symbol_table, - string_refinement_enabled); + val, symbol_table, string_refinement_enabled); } // We need to zero out all static variables, or nondet-initialize if they're @@ -174,15 +170,13 @@ static void java_static_lifetime_init( bool class_is_array = is_java_array_tag(sym.name); - exprt name_literal(ID_java_string_literal); - name_literal.set(ID_value, to_class_type(class_symbol.type).get_tag()); - journalling_symbol_tablet journalling_table = journalling_symbol_tablet::wrap(symbol_table); - symbol_exprt class_name_literal = - get_or_create_string_literal_symbol( - name_literal, journalling_table, string_refinement_enabled); + symbol_exprt class_name_literal = get_or_create_string_literal_symbol( + to_class_type(class_symbol.type).get_tag(), + journalling_table, + string_refinement_enabled); // If that created any new symbols make sure we initialise those too: const auto &new_symbols = journalling_table.get_inserted(); diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp index 803a60fa536..abc6bcd3383 100644 --- a/jbmc/src/java_bytecode/java_object_factory.cpp +++ b/jbmc/src/java_bytecode/java_object_factory.cpp @@ -731,10 +731,8 @@ alternate_casest get_string_input_values_code( alternate_casest cases; for(const auto &val : string_input_values) { - exprt name_literal(ID_java_string_literal); - name_literal.set(ID_value, val); const symbol_exprt s = - get_or_create_string_literal_symbol(name_literal, symbol_table, true); + get_or_create_string_literal_symbol(val, symbol_table, true); cases.push_back(code_assignt(expr, s)); } return cases; diff --git a/jbmc/src/java_bytecode/java_string_literal_expr.h b/jbmc/src/java_bytecode/java_string_literal_expr.h new file mode 100644 index 00000000000..b8e3712d92f --- /dev/null +++ b/jbmc/src/java_bytecode/java_string_literal_expr.h @@ -0,0 +1,38 @@ +/*******************************************************************\ + +Module: Java Bytecode + +Author: Diffblue Ltd. + +\*******************************************************************/ + +/// \file +/// Representation of a constant Java string + +#ifndef CPROVER_JAVA_BYTECODE_JAVA_STRING_LITERAL_EXPR_H +#define CPROVER_JAVA_BYTECODE_JAVA_STRING_LITERAL_EXPR_H + +#include + +class java_string_literal_exprt : public exprt +{ +public: + explicit java_string_literal_exprt(const irep_idt &literal) + : exprt(ID_java_string_literal) + { + set(ID_value, literal); + } + + irep_idt value() const + { + return get(ID_value); + } +}; + +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_java_string_literal; +} + +#endif // CPROVER_JAVA_BYTECODE_JAVA_STRING_LITERAL_EXPR_H diff --git a/jbmc/src/java_bytecode/java_string_literals.cpp b/jbmc/src/java_bytecode/java_string_literals.cpp index e8ab62f2845..0a95e7d19ac 100644 --- a/jbmc/src/java_bytecode/java_string_literals.cpp +++ b/jbmc/src/java_bytecode/java_string_literals.cpp @@ -8,6 +8,7 @@ Author: Chris Smowton, chris.smowton@diffblue.com #include "java_string_literals.h" #include "java_root_class.h" +#include "java_string_literal_expr.h" #include "java_types.h" #include "java_utils.h" @@ -55,21 +56,12 @@ static array_exprt utf16_to_array(const std::wstring &in) return ret; } -/// Creates or gets an existing constant global symbol for a given string -/// literal. -/// \param string_expr: string literal expression to convert -/// \param symbol_table: global symbol table. If not already present, constant -/// global symbols will be added. -/// \param string_refinement_enabled: if true, string refinement's string data -/// structure will also be initialised and added to the symbol table. -/// \return a symbol_expr corresponding to the new or existing literal symbol. symbol_exprt get_or_create_string_literal_symbol( - const exprt &string_expr, + const java_string_literal_exprt &string_expr, symbol_table_baset &symbol_table, bool string_refinement_enabled) { - PRECONDITION(string_expr.id() == ID_java_string_literal); - const irep_idt value = string_expr.get(ID_value); + const irep_idt value = string_expr.value(); const struct_tag_typet string_type("java::java.lang.String"); const std::string escaped_symbol_name = escape_non_alnum(id2string(value)); @@ -215,3 +207,14 @@ symbol_exprt get_or_create_string_literal_symbol( return new_symbol.symbol_expr(); } + +symbol_exprt get_or_create_string_literal_symbol( + const irep_idt &string_value, + symbol_table_baset &symbol_table, + bool string_refinement_enabled) +{ + return get_or_create_string_literal_symbol( + java_string_literal_exprt{string_value}, + symbol_table, + string_refinement_enabled); +} diff --git a/jbmc/src/java_bytecode/java_string_literals.h b/jbmc/src/java_bytecode/java_string_literals.h index 1ec8a023557..f65e9092fc1 100644 --- a/jbmc/src/java_bytecode/java_string_literals.h +++ b/jbmc/src/java_bytecode/java_string_literals.h @@ -12,8 +12,26 @@ Author: Chris Smowton, chris.smowton@diffblue.com #include #include +class java_string_literal_exprt; + +/// Creates or gets an existing constant global symbol for a given string +/// literal. +/// \param string_expr: string literal expression to convert +/// \param symbol_table: global symbol table. If not already present, constant +/// global symbols will be added. +/// \param string_refinement_enabled: if true, string refinement's string data +/// structure will also be initialised and added to the symbol table. +/// \return a symbol_expr corresponding to the new or existing literal symbol. +symbol_exprt get_or_create_string_literal_symbol( + const java_string_literal_exprt &string_expr, + symbol_table_baset &symbol_table, + bool string_refinement_enabled); + +/// Same as +/// get_or_create_string_literal_symbol(const exprt&, symbol_table_baset&, bool) +/// except it takes an id/string parameter rather than a string literal exprt. symbol_exprt get_or_create_string_literal_symbol( - const exprt &string_expr, + const irep_idt &string_value, symbol_table_baset &symbol_table, bool string_refinement_enabled);