From 37ea9be6c36c03c32520789dc692f063d5c2ca6a Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Tue, 20 Feb 2018 15:56:46 +0000 Subject: [PATCH 01/18] Remove Java refs from ANSI-C docs --- src/ansi-c/README.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ansi-c/README.md b/src/ansi-c/README.md index a1d73685e69..74aeb23517e 100644 --- a/src/ansi-c/README.md +++ b/src/ansi-c/README.md @@ -25,7 +25,7 @@ various threading interfaces. \section preprocessing Preprocessing & Parsing -In the \ref ansi-c and \ref java_bytecode directories +In the \ref ansi-c directories **Key classes:** * \ref languaget and its subclasses @@ -46,7 +46,7 @@ digraph G { \section type-checking Type-checking -In the \ref ansi-c and \ref java_bytecode directories. +In the \ref ansi-c directories. **Key classes:** * \ref languaget and its subclasses From 7994e9f160fd3f0aa82f8f3ed41de31a151548bf Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sat, 17 Mar 2018 13:21:30 +0000 Subject: [PATCH 02/18] Move replace_java_nondet to java_bytecode --- src/goto-programs/Makefile | 1 - src/java_bytecode/Makefile | 1 + .../replace_java_nondet.cpp | 149 ++++++++++-------- .../replace_java_nondet.h | 6 +- src/jbmc/jbmc_parse_options.cpp | 2 +- 5 files changed, 86 insertions(+), 73 deletions(-) rename src/{goto-programs => java_bytecode}/replace_java_nondet.cpp (61%) rename src/{goto-programs => java_bytecode}/replace_java_nondet.h (83%) diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile index 6ac8abfae36..3161a193594 100644 --- a/src/goto-programs/Makefile +++ b/src/goto-programs/Makefile @@ -52,7 +52,6 @@ SRC = basic_blocks.cpp \ remove_unused_functions.cpp \ remove_vector.cpp \ remove_virtual_functions.cpp \ - replace_java_nondet.cpp \ resolve_inherited_component.cpp \ safety_checker.cpp \ set_properties.cpp \ diff --git a/src/java_bytecode/Makefile b/src/java_bytecode/Makefile index b9371e734f1..28e5ac643f7 100644 --- a/src/java_bytecode/Makefile +++ b/src/java_bytecode/Makefile @@ -30,6 +30,7 @@ SRC = bytecode_info.cpp \ java_types.cpp \ java_utils.cpp \ mz_zip_archive.cpp \ + replace_java_nondet.cpp \ select_pointer_type.cpp \ # Empty last line diff --git a/src/goto-programs/replace_java_nondet.cpp b/src/java_bytecode/replace_java_nondet.cpp similarity index 61% rename from src/goto-programs/replace_java_nondet.cpp rename to src/java_bytecode/replace_java_nondet.cpp index 431acc0efb2..176715d421c 100644 --- a/src/goto-programs/replace_java_nondet.cpp +++ b/src/java_bytecode/replace_java_nondet.cpp @@ -9,38 +9,51 @@ Author: Reuben Thomas, reuben.thomas@diffblue.com /// \file /// Replace Java Nondet expressions -#include "goto-programs/replace_java_nondet.h" -#include "goto-programs/goto_convert.h" -#include "goto-programs/goto_model.h" -#include "goto-programs/remove_skip.h" - -#include "util/irep_ids.h" +#include "replace_java_nondet.h" #include #include +#include +#include +#include + +#include + /// Holds information about any discovered nondet methods, with extreme type- /// safety. class nondet_instruction_infot final { public: - enum class is_nondett:bool { FALSE, TRUE }; - enum class is_nullablet:bool { FALSE, TRUE }; + enum class is_nondett : bool + { + FALSE, + TRUE + }; + enum class is_nullablet : bool + { + FALSE, + TRUE + }; - nondet_instruction_infot(): - is_nondet(is_nondett::FALSE), - is_nullable(is_nullablet::FALSE) + nondet_instruction_infot() + : is_nondet(is_nondett::FALSE), is_nullable(is_nullablet::FALSE) { } - explicit nondet_instruction_infot(is_nullablet is_nullable): - is_nondet(is_nondett::TRUE), - is_nullable(is_nullable) + explicit nondet_instruction_infot(is_nullablet is_nullable) + : is_nondet(is_nondett::TRUE), is_nullable(is_nullable) { } - is_nondett get_instruction_type() const { return is_nondet; } - is_nullablet get_nullable_type() const { return is_nullable; } + is_nondett get_instruction_type() const + { + return is_nondet; + } + is_nullablet get_nullable_type() const + { + return is_nullable; + } private: is_nondett is_nondet; @@ -52,11 +65,11 @@ class nondet_instruction_infot final /// \return A structure detailing whether the function call appears to be one of /// our nondet library methods, and if so, whether or not it allows null /// results. -static nondet_instruction_infot is_nondet_returning_object( - const code_function_callt &function_call) +static nondet_instruction_infot +is_nondet_returning_object(const code_function_callt &function_call) { - const auto &function_symbol=to_symbol_expr(function_call.function()); - const auto function_name=id2string(function_symbol.get_identifier()); + const auto &function_symbol = to_symbol_expr(function_call.function()); + const auto function_name = id2string(function_symbol.get_identifier()); const std::regex reg( R"(.*org\.cprover\.CProver\.nondet)" R"((?:Boolean|Byte|Char|Short|Int|Long|Float|Double|With(out)?Null.*))"); @@ -74,19 +87,19 @@ static nondet_instruction_infot is_nondet_returning_object( /// recognised nondet library methods, and return some information about it. /// \param instr: A goto-program instruction to check. /// \return A structure detailing the properties of the nondet method. -static nondet_instruction_infot get_nondet_instruction_info( - const goto_programt::const_targett &instr) +static nondet_instruction_infot +get_nondet_instruction_info(const goto_programt::const_targett &instr) { - if(!(instr->is_function_call() && instr->code.id()==ID_code)) + if(!(instr->is_function_call() && instr->code.id() == ID_code)) { return nondet_instruction_infot(); } - const auto &code=to_code(instr->code); - if(code.get_statement()!=ID_function_call) + const auto &code = to_code(instr->code); + if(code.get_statement() != ID_function_call) { return nondet_instruction_infot(); } - const auto &function_call=to_code_function_call(code); + const auto &function_call = to_code_function_call(code); return is_nondet_returning_object(function_call); } @@ -94,10 +107,10 @@ static nondet_instruction_infot get_nondet_instruction_info( /// \param expr: The expression which may be a symbol. /// \param identifier: Some identifier. /// \return True if the expression is a symbol with the specified identifier. -static bool is_symbol_with_id(const exprt& expr, const irep_idt& identifier) +static bool is_symbol_with_id(const exprt &expr, const irep_idt &identifier) { - return expr.id()==ID_symbol && - to_symbol_expr(expr).get_identifier()==identifier; + return expr.id() == ID_symbol && + to_symbol_expr(expr).get_identifier() == identifier; } /// Return whether the expression is a typecast with the specified identifier. @@ -105,20 +118,20 @@ static bool is_symbol_with_id(const exprt& expr, const irep_idt& identifier) /// \param identifier: Some identifier. /// \return True if the expression is a typecast with one operand, and the /// typecast's identifier matches the specified identifier. -static bool is_typecast_with_id(const exprt& expr, const irep_idt& identifier) +static bool is_typecast_with_id(const exprt &expr, const irep_idt &identifier) { - if(!(expr.id()==ID_typecast && expr.operands().size()==1)) + if(!(expr.id() == ID_typecast && expr.operands().size() == 1)) { return false; } - const auto &typecast=to_typecast_expr(expr); - if(!(typecast.op().id()==ID_symbol && !typecast.op().has_operands())) + const auto &typecast = to_typecast_expr(expr); + if(!(typecast.op().id() == ID_symbol && !typecast.op().has_operands())) { return false; } - const auto &op_symbol=to_symbol_expr(typecast.op()); + const auto &op_symbol = to_symbol_expr(typecast.op()); // Return whether the typecast has the expected operand - return op_symbol.get_identifier()==identifier; + return op_symbol.get_identifier() == identifier; } /// Return whether the instruction is an assignment, and the rhs is a symbol or @@ -136,7 +149,7 @@ static bool is_assignment_from( { return false; } - const auto &rhs=to_code_assign(instr.code).rhs(); + const auto &rhs = to_code_assign(instr.code).rhs(); return is_symbol_with_id(rhs, identifier) || is_typecast_with_id(rhs, identifier); } @@ -153,10 +166,11 @@ static goto_programt::targett check_and_replace_target( const goto_programt::targett &target) { // Check whether this is a nondet library method, and return if not - const auto instr_info=get_nondet_instruction_info(target); - const auto next_instr=std::next(target); - if(instr_info.get_instruction_type()== - nondet_instruction_infot::is_nondett::FALSE) + const auto instr_info = get_nondet_instruction_info(target); + const auto next_instr = std::next(target); + if( + instr_info.get_instruction_type() == + nondet_instruction_infot::is_nondett::FALSE) { return next_instr; } @@ -164,55 +178,55 @@ static goto_programt::targett check_and_replace_target( // Look at the next instruction, ensure that it is an assignment assert(next_instr->is_assign()); // Get the name of the LHS of the assignment - const auto &next_instr_assign_lhs=to_code_assign(next_instr->code).lhs(); - if(!(next_instr_assign_lhs.id()==ID_symbol && - !next_instr_assign_lhs.has_operands())) + const auto &next_instr_assign_lhs = to_code_assign(next_instr->code).lhs(); + if( + !(next_instr_assign_lhs.id() == ID_symbol && + !next_instr_assign_lhs.has_operands())) { return next_instr; } - const auto return_identifier= + const auto return_identifier = to_symbol_expr(next_instr_assign_lhs).get_identifier(); - auto &instructions=goto_program.instructions; - const auto end=instructions.end(); + auto &instructions = goto_program.instructions; + const auto end = instructions.end(); // Look for an instruction where this name is on the RHS of an assignment - const auto matching_assignment=std::find_if( + const auto matching_assignment = std::find_if( next_instr, end, - [&return_identifier](const goto_programt::instructiont &instr) - { + [&return_identifier]( + const goto_programt::instructiont &instr) { // NOLINT (*) return is_assignment_from(instr, return_identifier); }); - assert(matching_assignment!=end); + assert(matching_assignment != end); // Assume that the LHS of *this* assignment is the actual nondet variable - const auto &code_assign=to_code_assign(matching_assignment->code); - const auto nondet_var=code_assign.lhs(); - const auto source_loc=target->source_location; + const auto &code_assign = to_code_assign(matching_assignment->code); + const auto nondet_var = code_assign.lhs(); + const auto source_loc = target->source_location; // Erase from the nondet function call to the assignment - const auto after_matching_assignment=std::next(matching_assignment); - assert(after_matching_assignment!=end); + const auto after_matching_assignment = std::next(matching_assignment); + assert(after_matching_assignment != end); std::for_each( target, after_matching_assignment, - [](goto_programt::instructiont &instr) - { + [](goto_programt::instructiont &instr) { // NOLINT (*) instr.make_skip(); }); - const auto inserted=goto_program.insert_before(after_matching_assignment); + const auto inserted = goto_program.insert_before(after_matching_assignment); inserted->make_assignment(); side_effect_expr_nondett inserted_expr(nondet_var.type()); inserted_expr.set_nullable( - instr_info.get_nullable_type()== + instr_info.get_nullable_type() == nondet_instruction_infot::is_nullablet::TRUE); - inserted->code=code_assignt(nondet_var, inserted_expr); - inserted->code.add_source_location()=source_loc; - inserted->source_location=source_loc; + inserted->code = code_assignt(nondet_var, inserted_expr); + inserted->code.add_source_location() = source_loc; + inserted->source_location = source_loc; goto_program.update(); @@ -225,13 +239,12 @@ static goto_programt::targett check_and_replace_target( /// \param goto_program: The goto program to modify. static void replace_java_nondet(goto_programt &goto_program) { - for(auto instruction_iterator=goto_program.instructions.begin(), - end=goto_program.instructions.end(); - instruction_iterator!=end;) + for(auto instruction_iterator = goto_program.instructions.begin(), + end = goto_program.instructions.end(); + instruction_iterator != end;) { - instruction_iterator=check_and_replace_target( - goto_program, - instruction_iterator); + instruction_iterator = + check_and_replace_target(goto_program, instruction_iterator); } } diff --git a/src/goto-programs/replace_java_nondet.h b/src/java_bytecode/replace_java_nondet.h similarity index 83% rename from src/goto-programs/replace_java_nondet.h rename to src/java_bytecode/replace_java_nondet.h index 3653908588d..e7b7bc43558 100644 --- a/src/goto-programs/replace_java_nondet.h +++ b/src/java_bytecode/replace_java_nondet.h @@ -9,8 +9,8 @@ Author: Reuben Thomas, reuben.thomas@diffblue.com /// \file /// Replace Java Nondet expressions -#ifndef CPROVER_GOTO_PROGRAMS_REPLACE_JAVA_NONDET_H -#define CPROVER_GOTO_PROGRAMS_REPLACE_JAVA_NONDET_H +#ifndef CPROVER_JAVA_BYTECODE_REPLACE_JAVA_NONDET_H +#define CPROVER_JAVA_BYTECODE_REPLACE_JAVA_NONDET_H class goto_modelt; class goto_functionst; @@ -28,4 +28,4 @@ void replace_java_nondet(goto_functionst &); /// \param function: The goto program to modify. void replace_java_nondet(goto_model_functiont &function); -#endif +#endif // CPROVER_JAVA_BYTECODE_REPLACE_JAVA_NONDET_H diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp index 25cce4cacd1..196e2ca567f 100644 --- a/src/jbmc/jbmc_parse_options.cpp +++ b/src/jbmc/jbmc_parse_options.cpp @@ -38,7 +38,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include @@ -56,6 +55,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include From a7db2220a8ffc0557d42f81b176de43bcae13449 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sat, 17 Mar 2018 13:43:27 +0000 Subject: [PATCH 03/18] Replace asserts by invariants --- src/java_bytecode/replace_java_nondet.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/java_bytecode/replace_java_nondet.cpp b/src/java_bytecode/replace_java_nondet.cpp index 176715d421c..9fb78ad8b8a 100644 --- a/src/java_bytecode/replace_java_nondet.cpp +++ b/src/java_bytecode/replace_java_nondet.cpp @@ -19,6 +19,7 @@ Author: Reuben Thomas, reuben.thomas@diffblue.com #include #include +#include /// Holds information about any discovered nondet methods, with extreme type- /// safety. @@ -176,7 +177,7 @@ static goto_programt::targett check_and_replace_target( } // Look at the next instruction, ensure that it is an assignment - assert(next_instr->is_assign()); + INVARIANT(next_instr->is_assign(), "expected assign instruction"); // Get the name of the LHS of the assignment const auto &next_instr_assign_lhs = to_code_assign(next_instr->code).lhs(); if( @@ -200,7 +201,7 @@ static goto_programt::targett check_and_replace_target( return is_assignment_from(instr, return_identifier); }); - assert(matching_assignment != end); + CHECK_RETURN(matching_assignment != end); // Assume that the LHS of *this* assignment is the actual nondet variable const auto &code_assign = to_code_assign(matching_assignment->code); @@ -209,7 +210,7 @@ static goto_programt::targett check_and_replace_target( // Erase from the nondet function call to the assignment const auto after_matching_assignment = std::next(matching_assignment); - assert(after_matching_assignment != end); + CHECK_RETURN(after_matching_assignment != end); std::for_each( target, From 26bcab8019dd35cda4d3128fc46e6b48ca60f93c Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 15 Mar 2018 15:44:24 +0000 Subject: [PATCH 04/18] Remove unnecessary include --- src/cbmc/bmc.h | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h index d4feb6847e0..cd4a131789d 100644 --- a/src/cbmc/bmc.h +++ b/src/cbmc/bmc.h @@ -19,8 +19,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include - #include #include #include From 7172e25bc7059f662b874f7b20b404147264484d Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sat, 17 Mar 2018 11:29:25 +0000 Subject: [PATCH 05/18] Bugfix: Java array symbols must have mode ID_java --- src/java_bytecode/java_bytecode_convert_class.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/java_bytecode/java_bytecode_convert_class.cpp b/src/java_bytecode/java_bytecode_convert_class.cpp index 711bba8949e..53c2bd1818d 100644 --- a/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/src/java_bytecode/java_bytecode_convert_class.cpp @@ -543,6 +543,7 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table) symbol.base_name=symbol_type.get(ID_C_base_name); symbol.is_type=true; symbol.type = class_type; + symbol.mode = ID_java; symbol_table.add(symbol); // Also provide a clone method: From 8e16c2852ca13362e96f57e5e16e899765d08491 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Tue, 10 Apr 2018 21:22:04 +0100 Subject: [PATCH 06/18] Bugfix: Java symbol types must have mode ID_java --- src/java_bytecode/java_bytecode_typecheck_type.cpp | 1 + src/java_bytecode/java_string_library_preprocess.cpp | 1 + 2 files changed, 2 insertions(+) diff --git a/src/java_bytecode/java_bytecode_typecheck_type.cpp b/src/java_bytecode/java_bytecode_typecheck_type.cpp index aa92d9333cf..79fb175db96 100644 --- a/src/java_bytecode/java_bytecode_typecheck_type.cpp +++ b/src/java_bytecode/java_bytecode_typecheck_type.cpp @@ -57,5 +57,6 @@ void java_bytecode_typecheckt::typecheck_type_symbol(symbolt &symbol) { assert(symbol.is_type); + symbol.mode = ID_java; typecheck_type(symbol.type); } diff --git a/src/java_bytecode/java_string_library_preprocess.cpp b/src/java_bytecode/java_string_library_preprocess.cpp index 1f2ce3365d6..2c474b861cc 100644 --- a/src/java_bytecode/java_string_library_preprocess.cpp +++ b/src/java_bytecode/java_string_library_preprocess.cpp @@ -247,6 +247,7 @@ void java_string_library_preprocesst::add_string_type( string_symbol->pretty_name=id2string(class_name); string_symbol->type=string_type; string_symbol->is_type=true; + string_symbol->mode = ID_java; } /// add a symbol in the table with static lifetime and name containing From b90eebb4135e307c688d99e61b56558a5bd6f11e Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sat, 17 Mar 2018 12:56:31 +0000 Subject: [PATCH 07/18] Replace asserts by invariants --- .../java_bytecode_typecheck_type.cpp | 21 ++++++++----------- 1 file changed, 9 insertions(+), 12 deletions(-) diff --git a/src/java_bytecode/java_bytecode_typecheck_type.cpp b/src/java_bytecode/java_bytecode_typecheck_type.cpp index 79fb175db96..49195d2b3b6 100644 --- a/src/java_bytecode/java_bytecode_typecheck_type.cpp +++ b/src/java_bytecode/java_bytecode_typecheck_type.cpp @@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "java_bytecode_typecheck.h" #include +#include void java_bytecode_typecheckt::typecheck_type(typet &type) { @@ -19,17 +20,12 @@ void java_bytecode_typecheckt::typecheck_type(typet &type) { irep_idt identifier=to_symbol_type(type).get_identifier(); - symbol_tablet::symbolst::const_iterator s_it= - symbol_table.symbols.find(identifier); - - // must exist already in the symbol table - if(s_it==symbol_table.symbols.end()) - { - error() << "failed to find type symbol "<< identifier << eom; - throw 0; - } - - assert(s_it->second.is_type); + auto type_symbol = symbol_table.lookup(identifier); + DATA_INVARIANT( + type_symbol, "symbol " + id2string(identifier) + " must exist already"); + DATA_INVARIANT( + type_symbol->is_type, + "symbol " + id2string(identifier) + " must exist already"); } else if(type.id()==ID_pointer) { @@ -55,7 +51,8 @@ void java_bytecode_typecheckt::typecheck_type(typet &type) void java_bytecode_typecheckt::typecheck_type_symbol(symbolt &symbol) { - assert(symbol.is_type); + DATA_INVARIANT( + symbol.is_type, "symbol " + id2string(symbol.name) + " must exist already"); symbol.mode = ID_java; typecheck_type(symbol.type); From b97a923eaebc799e1c4ac2dff4ea32d4c4dc3d00 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 18 Mar 2018 15:22:50 +0000 Subject: [PATCH 08/18] Set mode in goto_convert auxiliary symbols --- src/goto-programs/builtin_functions.cpp | 27 +++++++++---------- src/goto-programs/goto_clean_expr.cpp | 4 +-- src/goto-programs/goto_convert.cpp | 22 +++++++-------- src/goto-programs/goto_convert_class.h | 3 ++- .../goto_convert_side_effect.cpp | 14 +++++----- 5 files changed, 36 insertions(+), 34 deletions(-) diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index 35e67c16b5e..6306ab3bf84 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -468,8 +468,8 @@ void goto_convertt::do_cpp_new( assert(code_type.parameters().size()==1 || code_type.parameters().size()==2); - const symbolt &tmp_symbol= - new_tmp_symbol(return_type, "new", dest, rhs.source_location()); + const symbolt &tmp_symbol = + new_tmp_symbol(return_type, "new", dest, rhs.source_location(), ID_cpp); tmp_symbol_expr=tmp_symbol.symbol_expr(); @@ -499,8 +499,8 @@ void goto_convertt::do_cpp_new( assert(code_type.parameters().size()==2 || code_type.parameters().size()==3); - const symbolt &tmp_symbol= - new_tmp_symbol(return_type, "new", dest, rhs.source_location()); + const symbolt &tmp_symbol = + new_tmp_symbol(return_type, "new", dest, rhs.source_location(), ID_cpp); tmp_symbol_expr=tmp_symbol.symbol_expr(); @@ -663,13 +663,10 @@ void goto_convertt::do_java_new_array( // Must directly assign the new array to a temporary // because goto-symex will notice `x=side_effect_exprt` but not // `x=typecast_exprt(side_effect_exprt(...))` - symbol_exprt new_array_data_symbol= + symbol_exprt new_array_data_symbol = new_tmp_symbol( - data_java_new_expr.type(), - "new_array_data", - dest, - location) - .symbol_expr(); + data_java_new_expr.type(), "new_array_data", dest, location, ID_java) + .symbol_expr(); goto_programt::targett t_p2=dest.add_instruction(ASSIGN); t_p2->code=code_assignt(new_array_data_symbol, data_java_new_expr); t_p2->source_location=location; @@ -707,8 +704,9 @@ void goto_convertt::do_java_new_array( goto_programt tmp; - symbol_exprt tmp_i= - new_tmp_symbol(length.type(), "index", tmp, location).symbol_expr(); + symbol_exprt tmp_i = + new_tmp_symbol(length.type(), "index", tmp, location, ID_java) + .symbol_expr(); code_fort for_loop; @@ -730,8 +728,9 @@ void goto_convertt::do_java_new_array( plus_exprt(data, tmp_i), data.type().subtype()); code_blockt for_body; - symbol_exprt init_sym= - new_tmp_symbol(sub_type, "subarray_init", tmp, location).symbol_expr(); + symbol_exprt init_sym = + new_tmp_symbol(sub_type, "subarray_init", tmp, location, ID_java) + .symbol_expr(); code_assignt init_subarray(init_sym, sub_java_new); code_assignt assign_subarray( diff --git a/src/goto-programs/goto_clean_expr.cpp b/src/goto-programs/goto_clean_expr.cpp index ad5fea6ac5f..3a6dc4e81ee 100644 --- a/src/goto-programs/goto_clean_expr.cpp +++ b/src/goto-programs/goto_clean_expr.cpp @@ -237,8 +237,8 @@ void goto_convertt::clean_expr( if(result_is_used) { - symbolt &new_symbol= - new_tmp_symbol(expr.type(), "if_expr", dest, source_location); + symbolt &new_symbol = new_tmp_symbol( + expr.type(), "if_expr", dest, source_location, expr.get(ID_mode)); code_assignt assignment_true; assignment_true.lhs()=new_symbol.symbol_expr(); diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index 7f8095c2a05..0b524acd69c 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -2029,16 +2029,16 @@ symbolt &goto_convertt::new_tmp_symbol( const typet &type, const std::string &suffix, goto_programt &dest, - const source_locationt &source_location) + const source_locationt &source_location, + const irep_idt &mode) { - symbolt &new_symbol= - get_fresh_aux_symbol( - type, - tmp_symbol_prefix, - "tmp_"+suffix, - source_location, - irep_idt(), - symbol_table); + symbolt &new_symbol = get_fresh_aux_symbol( + type, + tmp_symbol_prefix, + "tmp_" + suffix, + source_location, + mode, + symbol_table); code_declt decl; decl.symbol()=new_symbol.symbol_expr(); @@ -2055,8 +2055,8 @@ void goto_convertt::make_temp_symbol( { const source_locationt source_location=expr.find_source_location(); - symbolt &new_symbol= - new_tmp_symbol(expr.type(), suffix, dest, source_location); + symbolt &new_symbol = new_tmp_symbol( + expr.type(), suffix, dest, source_location, expr.get(ID_mode)); code_assignt assignment; assignment.lhs()=new_symbol.symbol_expr(); diff --git a/src/goto-programs/goto_convert_class.h b/src/goto-programs/goto_convert_class.h index 4c5541a0108..1cf46ce783c 100644 --- a/src/goto-programs/goto_convert_class.h +++ b/src/goto-programs/goto_convert_class.h @@ -61,7 +61,8 @@ class goto_convertt:public messaget const typet &type, const std::string &suffix, goto_programt &dest, - const source_locationt &); + const source_locationt &, + const irep_idt &mode); symbol_exprt make_compound_literal( const exprt &expr, diff --git a/src/goto-programs/goto_convert_side_effect.cpp b/src/goto-programs/goto_convert_side_effect.cpp index d0cfa2c9b2f..befe4336885 100644 --- a/src/goto-programs/goto_convert_side_effect.cpp +++ b/src/goto-programs/goto_convert_side_effect.cpp @@ -519,10 +519,8 @@ void goto_convertt::remove_temporary_object( throw 0; } - symbolt &new_symbol= - new_tmp_symbol(expr.type(), "obj", dest, expr.find_source_location()); - - new_symbol.mode=expr.get(ID_mode); + symbolt &new_symbol = new_tmp_symbol( + expr.type(), "obj", dest, expr.find_source_location(), expr.get(ID_mode)); if(expr.operands().size()==1) { @@ -596,8 +594,12 @@ void goto_convertt::remove_statement_expression( source_locationt source_location=last.find_source_location(); - symbolt &new_symbol= - new_tmp_symbol(expr.type(), "statement_expression", dest, source_location); + symbolt &new_symbol = new_tmp_symbol( + expr.type(), + "statement_expression", + dest, + source_location, + expr.get(ID_mode)); symbol_exprt tmp_symbol_expr(new_symbol.name, new_symbol.type); tmp_symbol_expr.add_source_location()=source_location; From 8827265cb2e4461ba579d5a9dd6c34d532402d4a Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sat, 17 Mar 2018 15:00:09 +0000 Subject: [PATCH 09/18] Bugfix: use proper language registration in unit tests --- unit/testing-utils/load_java_class.cpp | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/unit/testing-utils/load_java_class.cpp b/unit/testing-utils/load_java_class.cpp index f198008dff4..217a3bb25d7 100644 --- a/unit/testing-utils/load_java_class.cpp +++ b/unit/testing-utils/load_java_class.cpp @@ -16,6 +16,8 @@ #include +#include + #include #include @@ -37,11 +39,13 @@ symbol_tablet load_java_class_lazy( free_form_cmdlinet lazy_command_line; lazy_command_line.add_flag("lazy-methods"); + register_language(new_java_bytecode_language); + return load_java_class( java_class_name, class_path, main, - new_java_bytecode_language(), + get_language_from_mode(ID_java), lazy_command_line); } @@ -59,8 +63,10 @@ symbol_tablet load_java_class( const std::string &class_path, const std::string &main) { + register_language(new_java_bytecode_language); + return load_java_class( - java_class_name, class_path, main, new_java_bytecode_language()); + java_class_name, class_path, main, get_language_from_mode(ID_java)); } /// Go through the process of loading, type-checking and finalising loading a From e48bf058671dad9702442e772d9825fd2bfc8cf0 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sat, 17 Mar 2018 13:14:10 +0000 Subject: [PATCH 10/18] Utility functions to get mode and language --- src/langapi/language_util.cpp | 32 +++++++--------------------- src/langapi/mode.cpp | 39 ++++++++++++++++++++++++++++++----- src/langapi/mode.h | 7 +++++++ 3 files changed, 49 insertions(+), 29 deletions(-) diff --git a/src/langapi/language_util.cpp b/src/langapi/language_util.cpp index 7a2e691af38..b6a6e5918d1 100644 --- a/src/langapi/language_util.cpp +++ b/src/langapi/language_util.cpp @@ -17,32 +17,13 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include "language.h" #include "mode.h" -static std::unique_ptr get_language( - const namespacet &ns, - const irep_idt &identifier) -{ - const symbolt *symbol; - - if(identifier=="" || - ns.lookup(identifier, symbol) || - symbol->mode=="") - return get_default_language(); - - std::unique_ptr ptr=get_language_from_mode(symbol->mode); - - if(ptr==nullptr) - throw "symbol `"+id2string(symbol->name)+ - "' has unknown mode '"+id2string(symbol->mode)+"'"; - - return ptr; -} - std::string from_expr( const namespacet &ns, const irep_idt &identifier, const exprt &expr) { - std::unique_ptr p(get_language(ns, identifier)); + std::unique_ptr p( + get_language_from_identifier(ns, identifier)); std::string result; p->from_expr(expr, result, ns); @@ -55,7 +36,8 @@ std::string from_type( const irep_idt &identifier, const typet &type) { - std::unique_ptr p(get_language(ns, identifier)); + std::unique_ptr p( + get_language_from_identifier(ns, identifier)); std::string result; p->from_type(type, result, ns); @@ -68,7 +50,8 @@ std::string type_to_name( const irep_idt &identifier, const typet &type) { - std::unique_ptr p(get_language(ns, identifier)); + std::unique_ptr p( + get_language_from_identifier(ns, identifier)); std::string result; p->type_to_name(type, result, ns); @@ -93,7 +76,8 @@ exprt to_expr( const irep_idt &identifier, const std::string &src) { - std::unique_ptr p(get_language(ns, identifier)); + std::unique_ptr p( + get_language_from_identifier(ns, identifier)); null_message_handlert null_message_handler; p->set_message_handler(null_message_handler); diff --git a/src/langapi/mode.cpp b/src/langapi/mode.cpp index dd12882c544..a668da49d35 100644 --- a/src/langapi/mode.cpp +++ b/src/langapi/mode.cpp @@ -18,6 +18,9 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include "language.h" +#include +#include + struct language_entryt { language_factoryt factory; @@ -39,15 +42,41 @@ void register_language(language_factoryt factory) std::unique_ptr get_language_from_mode(const irep_idt &mode) { - for(languagest::const_iterator it=languages.begin(); - it!=languages.end(); - it++) - if(mode==it->mode) - return it->factory(); + for(const auto &language : languages) + if(mode == language.mode) + return language.factory(); return nullptr; } +const irep_idt &get_mode_from_identifier( + const namespacet &ns, + const irep_idt &identifier) +{ + if(identifier.empty()) + return ID_unknown; + const symbolt *symbol; + if(ns.lookup(identifier, symbol)) + return ID_unknown; + return symbol->mode; +} + +std::unique_ptr get_language_from_identifier( + const namespacet &ns, + const irep_idt &identifier) +{ + const irep_idt &mode = get_mode_from_identifier(ns, identifier); + if(mode == ID_unknown) + return get_default_language(); + + std::unique_ptr language = get_language_from_mode(mode); + INVARIANT( + language, + "symbol `" + id2string(identifier) + "' has unknown mode '" + + id2string(mode) + "'"); + return language; +} + std::unique_ptr get_language_from_filename( const std::string &filename) { diff --git a/src/langapi/mode.h b/src/langapi/mode.h index 3edb7a30be8..5ca1e862a6f 100644 --- a/src/langapi/mode.h +++ b/src/langapi/mode.h @@ -15,8 +15,15 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include // unique_ptr class languaget; +class namespacet; std::unique_ptr get_language_from_mode(const irep_idt &mode); +const irep_idt &get_mode_from_identifier( + const namespacet &ns, + const irep_idt &identifier); +std::unique_ptr get_language_from_identifier( + const namespacet &ns, + const irep_idt &identifier); std::unique_ptr get_language_from_filename( const std::string &filename); std::unique_ptr get_default_language(); From f0af631b1f1ffaf3e17ebb5f3f4ace006e3736b2 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sat, 17 Mar 2018 13:15:57 +0000 Subject: [PATCH 11/18] Remove java_bytecode dependency from remove_instanceof --- src/ansi-c/ansi_c_language.h | 6 ++++ src/cpp/cpp_language.h | 6 ++++ src/goto-programs/remove_instanceof.cpp | 31 ++++++++++++-------- src/java_bytecode/java_bytecode_language.cpp | 5 ++++ src/java_bytecode/java_bytecode_language.h | 2 ++ src/jsil/jsil_language.h | 6 ++++ src/langapi/language.h | 3 ++ 7 files changed, 46 insertions(+), 13 deletions(-) diff --git a/src/ansi-c/ansi_c_language.h b/src/ansi-c/ansi_c_language.h index b23bdad6469..628c5bab08c 100644 --- a/src/ansi-c/ansi_c_language.h +++ b/src/ansi-c/ansi_c_language.h @@ -63,6 +63,12 @@ class ansi_c_languaget:public languaget exprt &expr, const namespacet &ns) override; + symbol_typet root_base_class_type() override + { + // does not exist + UNREACHABLE; + } + std::unique_ptr new_language() override { return util_make_unique(); } diff --git a/src/cpp/cpp_language.h b/src/cpp/cpp_language.h index 3f474005f15..a3db8124f44 100644 --- a/src/cpp/cpp_language.h +++ b/src/cpp/cpp_language.h @@ -75,6 +75,12 @@ class cpp_languaget:public languaget exprt &expr, const namespacet &ns) override; + symbol_typet root_base_class_type() override + { + // TODO: need a synthetic wrapper with a member that holds the type_info + UNIMPLEMENTED; + } + std::unique_ptr new_language() override { return util_make_unique(); } diff --git a/src/goto-programs/remove_instanceof.cpp b/src/goto-programs/remove_instanceof.cpp index 50166e33d03..61122159a57 100644 --- a/src/goto-programs/remove_instanceof.cpp +++ b/src/goto-programs/remove_instanceof.cpp @@ -14,8 +14,10 @@ Author: Chris Smowton, chris.smowton@diffblue.com #include "class_hierarchy.h" #include "class_identifier.h" +#include +#include + #include -#include #include @@ -94,18 +96,21 @@ std::size_t remove_instanceoft::lower_instanceof( // We actually insert the assignment instruction after the existing one. // This will briefly be ill-formed (use before def of instanceof_tmp) but the // two will subsequently switch places. This makes sure that the inserted - // assignement doesn't end up before any labels pointing at this instruction. - symbol_typet jlo=to_symbol_type(java_lang_object_type().subtype()); - exprt object_clsid=get_class_identifier_field(check_ptr, jlo, ns); - - symbolt &newsym= - get_fresh_aux_symbol( - object_clsid.type(), - "instanceof_tmp", - "instanceof_tmp", - source_locationt(), - ID_java, - symbol_table); + // assignment doesn't end up before any labels pointing at this instruction. + const irep_idt &mode = get_mode_from_identifier( + ns, to_symbol_type(target_type).get_identifier()); + const auto language = get_language_from_mode(mode); + CHECK_RETURN(language); + exprt object_clsid = + get_class_identifier_field(check_ptr, language->root_base_class_type(), ns); + + symbolt &newsym = get_fresh_aux_symbol( + object_clsid.type(), + "instanceof_tmp", + "instanceof_tmp", + source_locationt(), + mode, + symbol_table); auto newinst=goto_program.insert_after(this_inst); newinst->make_assignment(); diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index 4f62931d7d8..3fc5ec51d1a 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -1069,6 +1069,11 @@ bool java_bytecode_languaget::to_expr( return true; // fail for now } +symbol_typet java_bytecode_languaget::root_base_class_type() +{ + return to_symbol_type(java_lang_object_type().subtype()); +} + java_bytecode_languaget::~java_bytecode_languaget() { } diff --git a/src/java_bytecode/java_bytecode_language.h b/src/java_bytecode/java_bytecode_language.h index 9db26385d8f..7ee03bef208 100644 --- a/src/java_bytecode/java_bytecode_language.h +++ b/src/java_bytecode/java_bytecode_language.h @@ -127,6 +127,8 @@ class java_bytecode_languaget:public languaget exprt &expr, const namespacet &ns) override; + symbol_typet root_base_class_type() override; + std::unique_ptr new_language() override { return util_make_unique(); } diff --git a/src/jsil/jsil_language.h b/src/jsil/jsil_language.h index 8b902b86ded..b1419f5a9f7 100644 --- a/src/jsil/jsil_language.h +++ b/src/jsil/jsil_language.h @@ -60,6 +60,12 @@ class jsil_languaget:public languaget exprt &expr, const namespacet &ns) override; + virtual symbol_typet root_base_class_type() override + { + // unused + UNREACHABLE; + } + virtual std::unique_ptr new_language() override { return util_make_unique(); } diff --git a/src/langapi/language.h b/src/langapi/language.h index 06d145965f0..074aba9301a 100644 --- a/src/langapi/language.h +++ b/src/langapi/language.h @@ -137,6 +137,9 @@ class languaget:public messaget exprt &expr, const namespacet &ns)=0; + /// returns the class type that contains RTTI + virtual symbol_typet root_base_class_type() = 0; + virtual std::unique_ptr new_language()=0; void set_should_generate_opaque_method_stubs(bool should_generate_stubs); From 8009d41f78eebe406e1eae391c9eb28c43aee203 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sat, 17 Mar 2018 13:17:10 +0000 Subject: [PATCH 12/18] Remove Java dependency from remove_virtual_functions --- src/goto-programs/remove_virtual_functions.cpp | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp index fad271b0d27..d397089e39a 100644 --- a/src/goto-programs/remove_virtual_functions.cpp +++ b/src/goto-programs/remove_virtual_functions.cpp @@ -16,6 +16,9 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include +#include + #include #include #include @@ -317,6 +320,10 @@ void remove_virtual_functionst::get_child_functions_rec( if(findit==class_hierarchy.class_map.end()) return; + const auto language = get_language_from_identifier(ns, this_id); + CHECK_RETURN(language); + const irep_idt root_base_class_type_name = + language->root_base_class_type().get_identifier(); for(const auto &child : findit->second.children) { // Skip if we have already visited this and we found a function call that @@ -326,7 +333,7 @@ void remove_virtual_functionst::get_child_functions_rec( it != entry_map.end() && !has_prefix( id2string(it->second.symbol_expr.get_identifier()), - "java::java.lang.Object")) + id2string(root_base_class_type_name))) { continue; } From baffe6dba9f4f60e3c55e47a8d0e12d984ce05e3 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 18 Mar 2018 15:29:51 +0000 Subject: [PATCH 13/18] Call expr/type to json via languaget --- src/analyses/dependence_graph.cpp | 1 + src/cbmc/bmc_cover.cpp | 4 +- src/cbmc/show_vcc.cpp | 2 +- src/goto-analyzer/static_verifier.cpp | 5 +- .../unreachable_instructions.cpp | 5 +- src/goto-diff/goto_diff_base.cpp | 5 +- src/goto-programs/json_goto_trace.cpp | 78 +++++++--------- src/goto-programs/json_goto_trace.h | 9 +- src/goto-programs/loop_ids.cpp | 3 +- .../show_goto_functions_json.cpp | 2 +- src/goto-programs/show_properties.cpp | 2 +- src/java_bytecode/java_bytecode_language.cpp | 20 +++++ src/java_bytecode/java_bytecode_language.h | 10 +++ src/java_bytecode/java_json_expr.cpp | 54 ++++++++++++ src/java_bytecode/java_json_expr.h | 44 ++++++++++ src/langapi/language.cpp | 20 +++++ src/langapi/language.h | 11 +++ src/langapi/language_util.cpp | 34 +++++++ src/langapi/language_util.h | 20 ++++- src/solvers/Makefile | 2 +- src/util/CMakeLists.txt | 2 +- src/util/json_expr.cpp | 88 ++++++++----------- src/util/json_expr.h | 25 ++++-- src/util/ui_message.cpp | 2 +- 24 files changed, 324 insertions(+), 124 deletions(-) create mode 100644 src/java_bytecode/java_json_expr.cpp create mode 100644 src/java_bytecode/java_json_expr.h diff --git a/src/analyses/dependence_graph.cpp b/src/analyses/dependence_graph.cpp index dd9a770d837..3aa90133198 100644 --- a/src/analyses/dependence_graph.cpp +++ b/src/analyses/dependence_graph.cpp @@ -272,6 +272,7 @@ jsont dep_graph_domaint::output_json( const namespacet &ns) const { json_arrayt graph; + json_exprt json; for(const auto &cd : control_deps) { diff --git a/src/cbmc/bmc_cover.cpp b/src/cbmc/bmc_cover.cpp index 72d64a184a5..2fdfa3f730d 100644 --- a/src/cbmc/bmc_cover.cpp +++ b/src/cbmc/bmc_cover.cpp @@ -359,7 +359,7 @@ bool bmc_covert::operator()() json_result["description"] = json_stringt(goal.description); if(goal.source_location.is_not_nil()) - json_result["sourceLocation"] = json(goal.source_location); + json_result["sourceLocation"] = json(bmc.ns, goal.source_location.get_function(), goal.source_location); } json_result["totalGoals"]=json_numbert(std::to_string(goal_map.size())); json_result["goalsCovered"]=json_numbert(std::to_string(goals_covered)); @@ -385,7 +385,7 @@ bool bmc_covert::operator()() json_input["id"]=json_stringt(id2string(step.io_id)); if(step.io_args.size()==1) json_input["value"]= - json(step.io_args.front(), bmc.ns, ID_unknown); + json(bmc.ns, step.pc->function, step.io_args.front()); json_test.push_back(json_input); } } diff --git a/src/cbmc/show_vcc.cpp b/src/cbmc/show_vcc.cpp index 620ace0bb99..9a0d7c87ffd 100644 --- a/src/cbmc/show_vcc.cpp +++ b/src/cbmc/show_vcc.cpp @@ -97,7 +97,7 @@ void bmct::show_vcc_json(std::ostream &out) const source_locationt &source_location=s_it->source.pc->source_location; if(source_location.is_not_nil()) - object["sourceLocation"]=json(source_location); + object["sourceLocation"] = json(ns, s_it->source.pc->function, source_location); const std::string &s=s_it->comment; if(!s.empty()) diff --git a/src/goto-analyzer/static_verifier.cpp b/src/goto-analyzer/static_verifier.cpp index 660d20bd37e..98e2a7efa2e 100644 --- a/src/goto-analyzer/static_verifier.cpp +++ b/src/goto-analyzer/static_verifier.cpp @@ -11,7 +11,8 @@ Author: Martin Brain, martin.brain@cs.ox.ac.uk #include #include #include -#include + +#include /// Runs the analyzer and then prints out the domain @@ -78,7 +79,7 @@ bool static_verifier( ++unknown; } - j["sourceLocation"]=json(i_it->source_location); + j["sourceLocation"] = json(ns, i_it->function, i_it->source_location); } } m.status() << "Writing JSON report" << messaget::eom; diff --git a/src/goto-analyzer/unreachable_instructions.cpp b/src/goto-analyzer/unreachable_instructions.cpp index 0e783baaba5..7ca7312901c 100644 --- a/src/goto-analyzer/unreachable_instructions.cpp +++ b/src/goto-analyzer/unreachable_instructions.cpp @@ -16,10 +16,11 @@ Date: April 2016 #include #include -#include #include #include +#include + #include #include @@ -157,7 +158,7 @@ static void add_to_json( // print info for file actually with full path json_objectt &i_entry=dead_ins.push_back().make_object(); const source_locationt &l=it->second->source_location; - i_entry["sourceLocation"]=json(l); + i_entry["sourceLocation"] = json(ns, it->second->function, l); i_entry["statement"]=json_stringt(s); } } diff --git a/src/goto-diff/goto_diff_base.cpp b/src/goto-diff/goto_diff_base.cpp index 49f79b9858d..9433f2f69c5 100644 --- a/src/goto-diff/goto_diff_base.cpp +++ b/src/goto-diff/goto_diff_base.cpp @@ -13,9 +13,10 @@ Author: Peter Schrammel #include -#include #include +#include + /// Output diff result void goto_difft::output_functions() const { @@ -136,7 +137,7 @@ void goto_difft::convert_function_json( const symbolt &symbol = ns.lookup(function_name); result["name"] = json_stringt(id2string(function_name)); - result["sourceLocation"] = json(symbol.location); + result["sourceLocation"] = json(ns, function_name, symbol.location); if(options.get_bool_option("show-properties")) { diff --git a/src/goto-programs/json_goto_trace.cpp b/src/goto-programs/json_goto_trace.cpp index 1095a3ad281..a94c39b7647 100644 --- a/src/goto-programs/json_goto_trace.cpp +++ b/src/goto-programs/json_goto_trace.cpp @@ -23,6 +23,7 @@ Author: Daniel Kroening #include #include #include +#include /// Convert an ASSERT goto_trace step. /// \param [out] json_failure: The JSON object that @@ -123,39 +124,28 @@ void convert_decl( full_lhs_string = from_expr(ns, identifier, simplified); - const symbolt *symbol; irep_idt base_name, display_name; - if(!ns.lookup(identifier, symbol)) - { - base_name = symbol->base_name; - display_name = symbol->display_name(); - if(type_string == "") - type_string = from_type(ns, identifier, symbol->type); - - json_assignment["mode"] = json_stringt(id2string(symbol->mode)); - exprt simplified = simplify_expr(step.full_lhs_value, ns); + const symbolt *symbol; + bool not_found = ns.lookup(identifier, symbol); + CHECK_RETURN(!not_found); + base_name = symbol->base_name; + display_name = symbol->display_name(); - full_lhs_value = json(simplified, ns, symbol->mode); - } - else - { - DATA_INVARIANT( - step.full_lhs_value.is_not_nil(), - "full_lhs_value in assignment must not be nil"); - full_lhs_value = json(step.full_lhs_value, ns, ID_unknown); - } + json_assignment["mode"] = json_stringt(id2string(symbol->mode)); - json_assignment["value"] = full_lhs_value; - json_assignment["lhs"] = json_stringt(full_lhs_string); + const exprt value_simplified = simplify_expr(step.full_lhs_value, ns); + json_assignment["value"] = json(ns, identifier, value_simplified); + json_assignment["lhs"]=json_stringt(full_lhs_string); if(trace_options.json_full_lhs) { // Not language specific, still mangled, fully-qualified name of lhs - json_assignment["rawLhs"] = json_irept(true).convert_from_irep(simplified); + json_assignment["rawLhs"] = + json_irept(true).convert_from_irep(simplified); } - json_assignment["hidden"] = jsont::json_boolean(step.hidden); - json_assignment["internal"] = jsont::json_boolean(step.internal); - json_assignment["thread"] = json_numbert(std::to_string(step.thread_nr)); + json_assignment["hidden"]=jsont::json_boolean(step.hidden); + json_assignment["internal"]=jsont::json_boolean(step.internal); + json_assignment["thread"]=json_numbert(std::to_string(step.thread_nr)); json_assignment["assignmentType"] = json_stringt( step.assignment_type == goto_trace_stept::assignment_typet::ACTUAL_PARAMETER @@ -186,20 +176,17 @@ void convert_output( json_output["outputID"] = json_stringt(id2string(step.io_id)); // Recovering the mode from the function - irep_idt mode; - const symbolt *function_name; - if(ns.lookup(source_location.get_function(), function_name)) - // Failed to find symbol - mode = ID_unknown; - else - mode = function_name->mode; + const irep_idt mode = + get_mode_from_identifier(ns, source_location.get_function()); json_output["mode"] = json_stringt(id2string(mode)); - json_arrayt &json_values = json_output["values"].make_array(); + json_arrayt &json_values=json_output["values"].make_array(); for(const auto &arg : step.io_args) { - arg.is_nil() ? json_values.push_back(json_stringt("")) - : json_values.push_back(json(arg, ns, mode)); + if(arg.is_nil()) + json_values.push_back(json_stringt("")); + else + json_values.push_back(json(ns, source_location.get_function(), arg)); } if(!location.is_null()) @@ -229,20 +216,17 @@ void convert_input( json_input["inputID"] = json_stringt(id2string(step.io_id)); // Recovering the mode from the function - irep_idt mode; - const symbolt *function_name; - if(ns.lookup(source_location.get_function(), function_name)) - // Failed to find symbol - mode = ID_unknown; - else - mode = function_name->mode; - json_input["mode"] = json_stringt(id2string(mode)); - json_arrayt &json_values = json_input["values"].make_array(); + const irep_idt mode = + get_mode_from_identifier(ns, source_location.get_function()); + json_input["mode"]=json_stringt(id2string(mode)); + json_arrayt &json_values=json_input["values"].make_array(); for(const auto &arg : step.io_args) { - arg.is_nil() ? json_values.push_back(json_stringt("")) - : json_values.push_back(json(arg, ns, mode)); + if(arg.is_nil()) + json_values.push_back(json_stringt("")); + else + json_values.push_back(json(ns, source_location.get_function(), arg)); } if(!location.is_null()) @@ -277,7 +261,7 @@ void convert_return( json_objectt &json_function = json_call_return["function"].make_object(); json_function["displayName"] = json_stringt(id2string(symbol.display_name())); json_function["identifier"] = json_stringt(id2string(step.identifier)); - json_function["sourceLocation"] = json(symbol.location); + json_function["sourceLocation"] = json(ns, step.identifier, symbol.location); if(!location.is_null()) json_call_return["sourceLocation"] = location; diff --git a/src/goto-programs/json_goto_trace.h b/src/goto-programs/json_goto_trace.h index 820de78ee78..7bd020f0813 100644 --- a/src/goto-programs/json_goto_trace.h +++ b/src/goto-programs/json_goto_trace.h @@ -21,6 +21,9 @@ Date: November 2005 #include #include +#include +#include + /// This is structure is here to facilitate /// passing arguments to the conversion /// functions. @@ -127,8 +130,10 @@ void convert( jsont json_location; - source_location.is_not_nil() && !source_location.get_file().empty() - ? json_location = json(source_location) + source_location.is_not_nil() && + !source_location.get_file().empty() && + !source_location.get_function().empty() + ? json_location = json(ns, source_location.get_function(), source_location) : json_location = json_nullt(); // NOLINTNEXTLINE(whitespace/braces) diff --git a/src/goto-programs/loop_ids.cpp b/src/goto-programs/loop_ids.cpp index 86deb73eb43..20741d281f6 100644 --- a/src/goto-programs/loop_ids.cpp +++ b/src/goto-programs/loop_ids.cpp @@ -87,7 +87,7 @@ void show_loop_ids_json( json_objectt &loop=loops.push_back().make_object(); loop["name"]=json_stringt(id); - loop["sourceLocation"]=json(it->source_location); + loop["sourceLocation"] = json_exprt()(it->source_location); } } } @@ -110,6 +110,7 @@ void show_loop_ids( forall_goto_functions(it, goto_functions) show_loop_ids_json(ui, it->second.body, loops); + //TODO: this needs clean up std::cout << ",\n" << json_result; break; } diff --git a/src/goto-programs/show_goto_functions_json.cpp b/src/goto-programs/show_goto_functions_json.cpp index bfedc6250c2..5e8821f3fcf 100644 --- a/src/goto-programs/show_goto_functions_json.cpp +++ b/src/goto-programs/show_goto_functions_json.cpp @@ -76,7 +76,7 @@ json_objectt show_goto_functions_jsont::convert( if(instruction.code.source_location().is_not_nil()) { instruction_entry["sourceLocation"]= - json(instruction.code.source_location()); + json(ns, instruction.function, instruction.code.source_location()); } std::ostringstream instruction_builder; diff --git a/src/goto-programs/show_properties.cpp b/src/goto-programs/show_properties.cpp index 6df2f69bf33..ae686dc8a3d 100644 --- a/src/goto-programs/show_properties.cpp +++ b/src/goto-programs/show_properties.cpp @@ -137,7 +137,7 @@ void convert_properties_json( json_property["coveredLines"]= json_stringt( id2string(source_location.get_basic_block_covered_lines())); - json_property["sourceLocation"]=json(source_location); + json_property["sourceLocation"] = json(ns, identifier, source_location); json_property["description"]=json_stringt(id2string(description)); json_property["expression"]= json_stringt(from_expr(ns, identifier, ins.guard)); diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index 3fc5ec51d1a..57cf5d55a0b 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -34,6 +34,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "java_static_initializers.h" #include "java_utils.h" #include +#include "java_json_expr.h" #include "expr2java.h" @@ -1069,6 +1070,25 @@ bool java_bytecode_languaget::to_expr( return true; // fail for now } +json_objectt java_bytecode_languaget::json( + const exprt &expr, + const namespacet &ns) +{ + return java_json_exprt()(expr, ns); +} + +json_objectt java_bytecode_languaget::json( + const typet &type, + const namespacet &ns) +{ + return java_json_exprt()(type, ns); +} + +json_objectt java_bytecode_languaget::json(const source_locationt &source_location) +{ + return java_json_exprt()(source_location); +} + symbol_typet java_bytecode_languaget::root_base_class_type() { return to_symbol_type(java_lang_object_type().subtype()); diff --git a/src/java_bytecode/java_bytecode_language.h b/src/java_bytecode/java_bytecode_language.h index 7ee03bef208..c7b6ce159fc 100644 --- a/src/java_bytecode/java_bytecode_language.h +++ b/src/java_bytecode/java_bytecode_language.h @@ -127,6 +127,16 @@ class java_bytecode_languaget:public languaget exprt &expr, const namespacet &ns) override; + json_objectt json( + const exprt &, + const namespacet &) override; + + json_objectt json( + const typet &, + const namespacet &) override; + + json_objectt json(const source_locationt &) override; + symbol_typet root_base_class_type() override; std::unique_ptr new_language() override diff --git a/src/java_bytecode/java_json_expr.cpp b/src/java_bytecode/java_json_expr.cpp new file mode 100644 index 00000000000..00e75722ca2 --- /dev/null +++ b/src/java_bytecode/java_json_expr.cpp @@ -0,0 +1,54 @@ +/*******************************************************************\ + +Module: Expressions in JSON for Java + +Author: Peter Schrammel + +\*******************************************************************/ + +/// \file +/// Expressions in JSON for Java + +#include "java_json_expr.h" + +#include + +#include + +/// Output a Java source location in json. +/// \param location: a source location +/// \return a json object +json_objectt java_json_exprt::operator()(const source_locationt &location) +{ + json_objectt result = json_exprt()(location); + + if(!location.get_java_bytecode_index().empty()) + result["bytecodeIndex"]= + json_stringt(id2string(location.get_java_bytecode_index())); + + return result; +} + +/// Output a Java constant expression as a string. +/// \param expr: a constant expression +/// \return a string +std::string java_json_exprt::from_constant( + const namespacet &ns, + const constant_exprt &expr) +{ + std::string result; + language->from_expr(expr, result, ns); + return result; +} + +/// Output a Java type as a string. +/// \param type: an type +/// \return a string +std::string java_json_exprt::from_type( + const namespacet &ns, + const typet &type) +{ + std::string result; + language->from_type(type, result, ns); + return result; +} diff --git a/src/java_bytecode/java_json_expr.h b/src/java_bytecode/java_json_expr.h new file mode 100644 index 00000000000..15073d54d10 --- /dev/null +++ b/src/java_bytecode/java_json_expr.h @@ -0,0 +1,44 @@ +/*******************************************************************\ + +Module: Expressions in JSON for Java + +Author: Peter Schrammel + +\*******************************************************************/ + +/// \file +/// Expressions in JSON for Java + +#ifndef CPROVER_JAVA_BYTECODE_JAVA_JSON_EXPR_H +#define CPROVER_JAVA_BYTECODE_JAVA_JSON_EXPR_H + +#include + +#include + +class java_json_exprt : public json_exprt +{ +public: + json_objectt operator()( + const exprt &expr, + const namespacet &ns) override + { + return json_exprt::operator()(expr, ns); + } + + json_objectt operator()( + const typet &type, + const namespacet &ns) override + { + return json_exprt::operator()(type, ns); + } + + json_objectt operator()(const source_locationt &) override; + +protected: + std::unique_ptr language = get_language_from_mode(ID_java); + std::string from_constant(const namespacet &ns, const constant_exprt &) override; + std::string from_type(const namespacet &ns, const typet &) override; +}; + +#endif // CPROVER_JAVA_BYTECODE_JAVA_JSON_EXPR_H diff --git a/src/langapi/language.cpp b/src/langapi/language.cpp index 443062dce08..90abe415c13 100644 --- a/src/langapi/language.cpp +++ b/src/langapi/language.cpp @@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "language.h" #include +#include #include #include #include @@ -52,6 +53,25 @@ bool languaget::from_type( return false; } +json_objectt languaget::json( + const exprt &expr, + const namespacet &ns) +{ + return json_exprt()(expr, ns); +} + +json_objectt languaget::json( + const typet &type, + const namespacet &ns) +{ + return json_exprt()(type, ns); +} + +json_objectt languaget::json(const source_locationt &source_location) +{ + return json_exprt()(source_location); +} + bool languaget::type_to_name( const typet &type, std::string &name, diff --git a/src/langapi/language.h b/src/langapi/language.h index 074aba9301a..d83c3c51c3d 100644 --- a/src/langapi/language.h +++ b/src/langapi/language.h @@ -31,6 +31,7 @@ class exprt; class namespacet; class typet; class cmdlinet; +class json_objectt; #define OPT_FUNCTIONS \ "(function):" @@ -126,6 +127,16 @@ class languaget:public messaget std::string &code, const namespacet &ns); + virtual json_objectt json( + const exprt &, + const namespacet &); + + virtual json_objectt json( + const typet &, + const namespacet &); + + virtual json_objectt json(const source_locationt &); + virtual bool type_to_name( const typet &type, std::string &name, diff --git a/src/langapi/language_util.cpp b/src/langapi/language_util.cpp index b6a6e5918d1..8c3da434096 100644 --- a/src/langapi/language_util.cpp +++ b/src/langapi/language_util.cpp @@ -45,6 +45,29 @@ std::string from_type( return result; } +json_objectt json( + const namespacet &ns, + const irep_idt &identifier, + const exprt &expr) +{ + std::unique_ptr p( + get_language_from_identifier(ns, identifier)); + + std::string result; + return p->json(expr, ns); +} + +json_objectt json( + const namespacet &ns, + const irep_idt &identifier, + const typet &type) +{ + std::unique_ptr p( + get_language_from_identifier(ns, identifier)); + + return p->json(type, ns); +} + std::string type_to_name( const namespacet &ns, const irep_idt &identifier, @@ -97,3 +120,14 @@ std::string type_to_name(const typet &type) symbol_tablet symbol_table; return type_to_name(namespacet(symbol_table), "", type); } + +json_objectt json( + const namespacet &ns, + const irep_idt &identifier, + const source_locationt &source_location) +{ + std::unique_ptr p( + get_language_from_identifier(ns, identifier)); + + return p->json(source_location); +} diff --git a/src/langapi/language_util.h b/src/langapi/language_util.h index 9893aea4b68..0d954eaead2 100644 --- a/src/langapi/language_util.h +++ b/src/langapi/language_util.h @@ -15,6 +15,8 @@ Author: Daniel Kroening, kroening@cs.cmu.edu class exprt; class namespacet; class typet; +class json_objectt; +class source_locationt; std::string from_expr( const namespacet &ns, @@ -23,6 +25,11 @@ std::string from_expr( std::string from_expr(const exprt &expr); +json_objectt json( + const namespacet &ns, + const irep_idt &identifier, + const exprt &expr); + std::string from_type( const namespacet &ns, const irep_idt &identifier, @@ -30,6 +37,11 @@ std::string from_type( std::string from_type(const typet &type); +json_objectt json( + const namespacet &ns, + const irep_idt &identifier, + const typet &type); + exprt to_expr( const namespacet &ns, const irep_idt &identifier, @@ -37,9 +49,13 @@ exprt to_expr( std::string type_to_name( const namespacet &ns, - const irep_idt &identifier, - const typet &type); + const irep_idt &identifier, const typet &type); std::string type_to_name(const typet &type); +json_objectt json( + const namespacet &ns, + const irep_idt &identifier, + const source_locationt &source_location); + #endif // CPROVER_LANGAPI_LANGUAGE_UTIL_H diff --git a/src/solvers/Makefile b/src/solvers/Makefile index 3d1a572eb36..5f0f27fe9d8 100644 --- a/src/solvers/Makefile +++ b/src/solvers/Makefile @@ -219,5 +219,5 @@ solvers$(LIBEXT): $(OBJ) $(SOLVER_LIB) $(LINKLIB) $(LIBSOLVER) smt2_solver$(EXEEXT): $(OBJ) smt2/smt2_solver$(OBJEXT) \ - ../util/util$(LIBEXT) ../langapi/langapi$(LIBEXT) ../big-int/big-int$(LIBEXT) $(SOLVER_LIB) + ../util/util$(LIBEXT) ../big-int/big-int$(LIBEXT) $(SOLVER_LIB) $(LINKBIN) $(LIBSOLVER) diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index 055eabc7891..19e7810aba2 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -3,4 +3,4 @@ add_library(util ${sources}) generic_includes(util) -target_link_libraries(util big-int langapi) +target_link_libraries(util big-int) diff --git a/src/util/json_expr.cpp b/src/util/json_expr.cpp index aa8b63a0dc7..80a2a53db6a 100644 --- a/src/util/json_expr.cpp +++ b/src/util/json_expr.cpp @@ -21,11 +21,13 @@ Author: Peter Schrammel #include "config.h" #include "identifier.h" #include "invariant.h" - -#include -#include +#include "format.h" +#include "format_type.h" +#include "format_expr.h" +#include "format_constant.h" #include +#include static exprt simplify_json_expr( const exprt &src, @@ -80,7 +82,7 @@ static exprt simplify_json_expr( return src; } -json_objectt json(const source_locationt &location) +json_objectt json_exprt::operator()(const source_locationt &location) { json_objectt result; @@ -100,27 +102,19 @@ json_objectt json(const source_locationt &location) if(!location.get_function().empty()) result["function"]=json_stringt(id2string(location.get_function())); - if(!location.get_java_bytecode_index().empty()) - result["bytecodeIndex"]= - json_stringt(id2string(location.get_java_bytecode_index())); - return result; } /// Output a CBMC type in json. -/// The `mode` argument is used to correctly report types. /// \param type: a type /// \param ns: a namespace -/// \param mode: language in which the code was written; for now ID_C and -/// ID_java are supported /// \return a json object -json_objectt json( +json_objectt json_exprt::operator()( const typet &type, - const namespacet &ns, - const irep_idt &mode) + const namespacet &ns) { if(type.id()==ID_symbol) - return json(ns.follow(type), ns, mode); + return (*this)(ns.follow(type), ns); json_objectt result; @@ -156,7 +150,7 @@ json_objectt json( else if(type.id()==ID_c_enum_tag) { // we return the base type - return json(ns.follow_tag(to_c_enum_tag_type(type)).subtype(), ns, mode); + return (*this)(ns.follow_tag(to_c_enum_tag_type(type)).subtype(), ns); } else if(type.id()==ID_fixedbv) { @@ -167,7 +161,7 @@ json_objectt json( else if(type.id()==ID_pointer) { result["name"]=json_stringt("pointer"); - result["subtype"]=json(type.subtype(), ns, mode); + result["subtype"] = (*this)(type.subtype(), ns); } else if(type.id()==ID_bool) { @@ -176,13 +170,13 @@ json_objectt json( else if(type.id()==ID_array) { result["name"]=json_stringt("array"); - result["subtype"]=json(type.subtype(), ns, mode); + result["subtype"] = (*this)(type.subtype(), ns); } else if(type.id()==ID_vector) { result["name"]=json_stringt("vector"); - result["subtype"]=json(type.subtype(), ns, mode); - result["size"]=json(to_vector_type(type).size(), ns, mode); + result["subtype"] = (*this)(type.subtype(), ns); + result["size"] = (*this)(to_vector_type(type).size(), ns); } else if(type.id()==ID_struct) { @@ -194,7 +188,7 @@ json_objectt json( { json_objectt &e=members.push_back().make_object(); e["name"]=json_stringt(id2string(component.get_name())); - e["type"]=json(component.type(), ns, mode); + e["type"] = (*this)(component.type(), ns); } } else if(type.id()==ID_union) @@ -207,7 +201,7 @@ json_objectt json( { json_objectt &e=members.push_back().make_object(); e["name"]=json_stringt(id2string(component.get_name())); - e["type"]=json(component.type(), ns, mode); + e["type"] = (*this)(component.type(), ns); } } else @@ -216,17 +210,27 @@ json_objectt json( return result; } +std::string json_exprt::from_constant( + const namespacet &ns, + const constant_exprt &expr) +{ + return format_constantt()(expr); +} + +std::string json_exprt::from_type(const namespacet &ns, const typet &type) +{ + std::stringstream ss; + ss << format(ns.follow(type)); + return ss.str(); +} + /// Output a CBMC expression in json. -/// The mode is used to correctly report types. /// \param expr: an expression /// \param ns: a namespace -/// \param mode: language in which the code was written; for now ID_C and -/// ID_java are supported /// \return a json object -json_objectt json( +json_objectt json_exprt::operator()( const exprt &expr, - const namespacet &ns, - const irep_idt &mode) + const namespacet &ns) { json_objectt result; @@ -234,28 +238,14 @@ json_objectt json( if(expr.id()==ID_constant) { - std::unique_ptr lang; - if(mode==ID_unknown) - lang=std::unique_ptr(get_default_language()); - else - { - lang=std::unique_ptr(get_language_from_mode(mode)); - if(!lang) - lang=std::unique_ptr(get_default_language()); - } - const typet &underlying_type= type.id()==ID_c_bit_field?type.subtype(): type; - std::string type_string; - bool error=lang->from_type(underlying_type, type_string, ns); - CHECK_RETURN(!error); - - std::string value_string; - lang->from_expr(expr, value_string, ns); - + std::string type_string = from_type(ns, underlying_type); const constant_exprt &constant_expr=to_constant_expr(expr); + std::string value_string = from_constant(ns, constant_expr); + if(type.id()==ID_unsignedbv || type.id()==ID_signedbv || type.id()==ID_c_bit_field) @@ -281,7 +271,7 @@ json_objectt json( constant_exprt tmp; tmp.type()=ns.follow_tag(to_c_enum_tag_type(type)); tmp.set_value(to_constant_expr(expr).get_value()); - return json(tmp, ns, mode); + result = (*this)(tmp, ns); } else if(type.id()==ID_bv) { @@ -359,7 +349,7 @@ json_objectt json( { json_objectt &e=elements.push_back().make_object(); e["index"]=json_numbert(std::to_string(index)); - e["value"]=json(*it, ns, mode); + e["value"] = (*this)(*it, ns); index++; } } @@ -380,7 +370,7 @@ json_objectt json( for(std::size_t m=0; m Date: Sat, 7 Apr 2018 11:55:00 +0100 Subject: [PATCH 14/18] Unify temporary counters --- src/goto-programs/goto_convert_class.h | 2 -- src/goto-programs/goto_convert_functions.cpp | 1 - src/goto-programs/goto_convert_side_effect.cpp | 9 ++++++--- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/goto-programs/goto_convert_class.h b/src/goto-programs/goto_convert_class.h index 1cf46ce783c..84a90cb59cf 100644 --- a/src/goto-programs/goto_convert_class.h +++ b/src/goto-programs/goto_convert_class.h @@ -34,7 +34,6 @@ class goto_convertt:public messaget messaget(_message_handler), symbol_table(_symbol_table), ns(_symbol_table), - temporary_counter(0), tmp_symbol_prefix("goto_convertt") { } @@ -46,7 +45,6 @@ class goto_convertt:public messaget protected: symbol_table_baset &symbol_table; namespacet ns; - unsigned temporary_counter; std::string tmp_symbol_prefix; void goto_convert_rec(const codet &code, goto_programt &dest); diff --git a/src/goto-programs/goto_convert_functions.cpp b/src/goto-programs/goto_convert_functions.cpp index f4edab30c47..502fd2e6740 100644 --- a/src/goto-programs/goto_convert_functions.cpp +++ b/src/goto-programs/goto_convert_functions.cpp @@ -147,7 +147,6 @@ void goto_convert_functionst::convert_function( // make tmp variables local to function tmp_symbol_prefix=id2string(symbol.name)+"::$tmp::"; - temporary_counter=0; reset_temporary_counter(); f.type=to_code_type(symbol.type); diff --git a/src/goto-programs/goto_convert_side_effect.cpp b/src/goto-programs/goto_convert_side_effect.cpp index befe4336885..def8d98b170 100644 --- a/src/goto-programs/goto_convert_side_effect.cpp +++ b/src/goto-programs/goto_convert_side_effect.cpp @@ -379,7 +379,7 @@ void goto_convertt::remove_function_call( new_base_name+='_'; new_base_name+=id2string(symbol.base_name); - new_base_name+="$"+std::to_string(++temporary_counter); + new_base_name += "$0"; new_symbol.base_name=new_base_name; new_symbol.mode=symbol.mode; @@ -387,6 +387,7 @@ void goto_convertt::remove_function_call( new_symbol.name=tmp_symbol_prefix+id2string(new_symbol.base_name); + // ensure that the name is unique new_name(new_symbol); { @@ -429,10 +430,11 @@ void goto_convertt::remove_cpp_new( auxiliary_symbolt new_symbol; - new_symbol.base_name="new_ptr$"+std::to_string(++temporary_counter); + new_symbol.base_name = "new_ptr$0"; new_symbol.type=expr.type(); new_symbol.name=tmp_symbol_prefix+id2string(new_symbol.base_name); + // ensure that the name is unique new_name(new_symbol); code_declt decl; @@ -480,11 +482,12 @@ void goto_convertt::remove_malloc( { auxiliary_symbolt new_symbol; - new_symbol.base_name="malloc_value$"+std::to_string(++temporary_counter); + new_symbol.base_name = "malloc_value$0"; new_symbol.type=expr.type(); new_symbol.name=tmp_symbol_prefix+id2string(new_symbol.base_name); new_symbol.location=expr.source_location(); + // ensure that the name is unique new_name(new_symbol); code_declt decl; From 35865739510ed3f64576966f0af8ac423f524bf1 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Mon, 9 Apr 2018 08:25:33 +0100 Subject: [PATCH 15/18] Associate dynamic objects with respective language mode --- src/goto-symex/symex_builtin_functions.cpp | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp index c000c3c5c0f..b66a5357f9e 100644 --- a/src/goto-symex/symex_builtin_functions.cpp +++ b/src/goto-symex/symex_builtin_functions.cpp @@ -66,6 +66,9 @@ void goto_symext::symex_allocate( exprt size=code.op0(); typet object_type=nil_typet(); + auto function_symbol = outer_symbol_table.lookup(state.source.pc->function); + INVARIANT(function_symbol, "function associated with instruction not found"); + const irep_idt &mode = function_symbol->mode; // is the type given? if(code.type().id()==ID_pointer && code.type().subtype().id()!=ID_empty) @@ -142,7 +145,7 @@ void goto_symext::symex_allocate( size_symbol.name="symex_dynamic::"+id2string(size_symbol.base_name); size_symbol.is_lvalue=true; size_symbol.type=tmp_size.type(); - size_symbol.mode=ID_C; + size_symbol.mode = mode; state.symbol_table.add(size_symbol); @@ -161,7 +164,7 @@ void goto_symext::symex_allocate( value_symbol.is_lvalue=true; value_symbol.type=object_type; value_symbol.type.set("#dynamic", true); - value_symbol.mode=ID_C; + value_symbol.mode = mode; state.symbol_table.add(value_symbol); @@ -401,7 +404,6 @@ void goto_symext::symex_cpp_new( if(code.type().id()!=ID_pointer) throw "new expected to return pointer"; - do_array = (code.get(ID_statement) == ID_cpp_new_array || code.get(ID_statement) == ID_java_new_array_data); From f0d695a36ce14b888d94a1d2b5417977fc2b3d72 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sat, 7 Apr 2018 12:08:23 +0100 Subject: [PATCH 16/18] remove_java_new --- src/goto-programs/builtin_functions.cpp | 210 ------------ src/goto-programs/goto_convert.cpp | 32 +- src/java_bytecode/Makefile | 1 + src/java_bytecode/remove_java_new.cpp | 408 ++++++++++++++++++++++++ src/java_bytecode/remove_java_new.h | 42 +++ 5 files changed, 453 insertions(+), 240 deletions(-) create mode 100644 src/java_bytecode/remove_java_new.cpp create mode 100644 src/java_bytecode/remove_java_new.h diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index 6306ab3bf84..5d4070b8681 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -539,216 +539,6 @@ void goto_convertt::do_cpp_new( dest.destructive_append(tmp_initializer); } -void goto_convertt::do_java_new( - const exprt &lhs, - const side_effect_exprt &rhs, - goto_programt &dest) -{ - PRECONDITION(!lhs.is_nil()); - PRECONDITION(rhs.operands().empty()); - PRECONDITION(rhs.type().id() == ID_pointer); - source_locationt location=rhs.source_location(); - typet object_type=rhs.type().subtype(); - - // build size expression - exprt object_size=size_of_expr(object_type, ns); - CHECK_RETURN(object_size.is_not_nil()); - - // we produce a malloc side-effect, which stays - side_effect_exprt malloc_expr(ID_allocate, rhs.type()); - malloc_expr.copy_to_operands(object_size); - // could use true and get rid of the code below - malloc_expr.copy_to_operands(false_exprt()); - - goto_programt::targett t_n=dest.add_instruction(ASSIGN); - t_n->code=code_assignt(lhs, malloc_expr); - t_n->source_location=location; - - // zero-initialize the object - dereference_exprt deref(lhs, object_type); - exprt zero_object= - zero_initializer(object_type, location, ns, get_message_handler()); - set_class_identifier( - to_struct_expr(zero_object), ns, to_symbol_type(object_type)); - goto_programt::targett t_i=dest.add_instruction(ASSIGN); - t_i->code=code_assignt(deref, zero_object); - t_i->source_location=location; -} - -void goto_convertt::do_java_new_array( - const exprt &lhs, - const side_effect_exprt &rhs, - goto_programt &dest) -{ - PRECONDITION(!lhs.is_nil()); // do_java_new_array without lhs not implemented - PRECONDITION(rhs.operands().size() >= 1); // one per dimension - PRECONDITION(rhs.type().id() == ID_pointer); - - source_locationt location=rhs.source_location(); - typet object_type=rhs.type().subtype(); - PRECONDITION(ns.follow(object_type).id() == ID_struct); - - // build size expression - exprt object_size=size_of_expr(object_type, ns); - - CHECK_RETURN(!object_size.is_nil()); - - // we produce a malloc side-effect, which stays - side_effect_exprt malloc_expr(ID_allocate, rhs.type()); - malloc_expr.copy_to_operands(object_size); - // code use true and get rid of the code below - malloc_expr.copy_to_operands(false_exprt()); - - goto_programt::targett t_n=dest.add_instruction(ASSIGN); - t_n->code=code_assignt(lhs, malloc_expr); - t_n->source_location=location; - - const struct_typet &struct_type=to_struct_type(ns.follow(object_type)); - - // Ideally we would have a check for `is_valid_java_array(struct_type)` but - // `is_valid_java_array is part of the java_bytecode module and we cannot - // introduce such dependencies. We do this simple check instead: - PRECONDITION(struct_type.components().size()==3); - - // Init base class: - dereference_exprt deref(lhs, object_type); - exprt zero_object= - zero_initializer(object_type, location, ns, get_message_handler()); - set_class_identifier( - to_struct_expr(zero_object), ns, to_symbol_type(object_type)); - goto_programt::targett t_i=dest.add_instruction(ASSIGN); - t_i->code=code_assignt(deref, zero_object); - t_i->source_location=location; - - // if it's an array, we need to set the length field - member_exprt length( - deref, - struct_type.components()[1].get_name(), - struct_type.components()[1].type()); - goto_programt::targett t_s=dest.add_instruction(ASSIGN); - t_s->code=code_assignt(length, rhs.op0()); - t_s->source_location=location; - - // we also need to allocate space for the data - member_exprt data( - deref, - struct_type.components()[2].get_name(), - struct_type.components()[2].type()); - - // Allocate a (struct realtype**) instead of a (void**) if possible. - const irept &given_element_type=object_type.find(ID_C_element_type); - typet allocate_data_type; - if(given_element_type.is_not_nil()) - { - allocate_data_type= - pointer_type(static_cast(given_element_type)); - } - else - allocate_data_type=data.type(); - - side_effect_exprt data_java_new_expr( - ID_java_new_array_data, allocate_data_type); - - // The instruction may specify a (hopefully small) upper bound on the - // array size, in which case we allocate a fixed-length array that may - // be larger than the `length` member rather than use a true variable- - // length array, which produces a more complex formula in the current - // backend. - const irept size_bound=rhs.find(ID_length_upper_bound); - if(size_bound.is_nil()) - data_java_new_expr.set(ID_size, rhs.op0()); - else - data_java_new_expr.set(ID_size, size_bound); - - // Must directly assign the new array to a temporary - // because goto-symex will notice `x=side_effect_exprt` but not - // `x=typecast_exprt(side_effect_exprt(...))` - symbol_exprt new_array_data_symbol = - new_tmp_symbol( - data_java_new_expr.type(), "new_array_data", dest, location, ID_java) - .symbol_expr(); - goto_programt::targett t_p2=dest.add_instruction(ASSIGN); - t_p2->code=code_assignt(new_array_data_symbol, data_java_new_expr); - t_p2->source_location=location; - - goto_programt::targett t_p=dest.add_instruction(ASSIGN); - exprt cast_java_new=new_array_data_symbol; - if(cast_java_new.type()!=data.type()) - cast_java_new=typecast_exprt(cast_java_new, data.type()); - t_p->code=code_assignt(data, cast_java_new); - t_p->source_location=location; - - // zero-initialize the data - if(!rhs.get_bool(ID_skip_initialize)) - { - exprt zero_element= - zero_initializer( - data.type().subtype(), - location, - ns, - get_message_handler()); - codet array_set(ID_array_set); - array_set.copy_to_operands(new_array_data_symbol, zero_element); - goto_programt::targett t_d=dest.add_instruction(OTHER); - t_d->code=array_set; - t_d->source_location=location; - } - - // multi-dimensional? - - if(rhs.operands().size()>=2) - { - // produce - // for(int i=0; i(rhs.type().subtype().find("#element_type")); - assert(sub_type.id()==ID_pointer); - sub_java_new.type()=sub_type; - - side_effect_exprt inc(ID_assign); - inc.operands().resize(2); - inc.op0()=tmp_i; - inc.op1()=plus_exprt(tmp_i, from_integer(1, tmp_i.type())); - - dereference_exprt deref_expr( - plus_exprt(data, tmp_i), data.type().subtype()); - - code_blockt for_body; - symbol_exprt init_sym = - new_tmp_symbol(sub_type, "subarray_init", tmp, location, ID_java) - .symbol_expr(); - - code_assignt init_subarray(init_sym, sub_java_new); - code_assignt assign_subarray( - deref_expr, - typecast_exprt(init_sym, deref_expr.type())); - for_body.move_to_operands(init_subarray); - for_body.move_to_operands(assign_subarray); - - for_loop.init()=code_assignt(tmp_i, from_integer(0, tmp_i.type())); - for_loop.cond()=binary_relation_exprt(tmp_i, ID_lt, rhs.op0()); - for_loop.iter()=inc; - for_loop.body()=for_body; - - convert(for_loop, tmp); - dest.destructive_append(tmp); - } -} - /// builds a goto program for object initialization after new void goto_convertt::cpp_new_initializer( const exprt &lhs, diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index 0b524acd69c..c22bda75330 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -754,43 +754,15 @@ void goto_convertt::convert_assign( Forall_operands(it, rhs) clean_expr(*it, dest); + // TODO: This should be done in a separate pass do_cpp_new(lhs, to_side_effect_expr(rhs), dest); } - else if(rhs.id()==ID_side_effect && - rhs.get(ID_statement)==ID_java_new) - { - Forall_operands(it, rhs) - clean_expr(*it, dest); - - do_java_new(lhs, to_side_effect_expr(rhs), dest); - } - else if(rhs.id()==ID_side_effect && - rhs.get(ID_statement)==ID_java_new_array) - { - Forall_operands(it, rhs) - clean_expr(*it, dest); - - do_java_new_array(lhs, to_side_effect_expr(rhs), dest); - } - else if( - rhs.id() == ID_side_effect && - (rhs.get(ID_statement) == ID_allocate || - rhs.get(ID_statement) == ID_java_new_array_data)) + else { // just preserve Forall_operands(it, rhs) clean_expr(*it, dest); - code_assignt new_assign(code); - new_assign.lhs()=lhs; - new_assign.rhs()=rhs; - - copy(new_assign, ASSIGN, dest); - } - else - { - clean_expr(rhs, dest); - if(lhs.id()==ID_typecast) { assert(lhs.operands().size()==1); diff --git a/src/java_bytecode/Makefile b/src/java_bytecode/Makefile index 28e5ac643f7..26bb72ba723 100644 --- a/src/java_bytecode/Makefile +++ b/src/java_bytecode/Makefile @@ -30,6 +30,7 @@ SRC = bytecode_info.cpp \ java_types.cpp \ java_utils.cpp \ mz_zip_archive.cpp \ + remove_java_new.cpp \ replace_java_nondet.cpp \ select_pointer_type.cpp \ # Empty last line diff --git a/src/java_bytecode/remove_java_new.cpp b/src/java_bytecode/remove_java_new.cpp new file mode 100644 index 00000000000..70b7b3b886f --- /dev/null +++ b/src/java_bytecode/remove_java_new.cpp @@ -0,0 +1,408 @@ +/*******************************************************************\ + +Module: Remove Java New Operators + +Author: Peter Schrammel + +\*******************************************************************/ + +/// \file +/// Remove Java New Operators + +#include "remove_java_new.h" + +#include +#include + +#include + +#include +#include +#include +#include +#include +#include + +class remove_java_newt : public messaget +{ +public: + remove_java_newt( + symbol_table_baset &symbol_table, + message_handlert &_message_handler) + : messaget(_message_handler), + symbol_table(symbol_table), + ns(symbol_table) + { + } + + // Lower java_new for a single function + bool lower_java_new(goto_programt &); + + // Lower java_new for a single instruction + bool lower_java_new(goto_programt &, goto_programt::targett); + +protected: + symbol_table_baset &symbol_table; + namespacet ns; + + void lower_java_new( + const exprt &lhs, + const side_effect_exprt &rhs, + goto_programt &, + goto_programt::targett); + + void lower_java_new_array( + const exprt &lhs, + const side_effect_exprt &rhs, + goto_programt &, + goto_programt::targett); +}; + +void remove_java_newt::lower_java_new( + const exprt &lhs, + const side_effect_exprt &rhs, + goto_programt &dest, + goto_programt::targett target) +{ + PRECONDITION(!lhs.is_nil()); + PRECONDITION(rhs.operands().empty()); + PRECONDITION(rhs.type().id() == ID_pointer); + source_locationt location=rhs.source_location(); + typet object_type=rhs.type().subtype(); + + // build size expression + exprt object_size=size_of_expr(object_type, ns); + CHECK_RETURN(object_size.is_not_nil()); + + // we produce a malloc side-effect, which stays + side_effect_exprt malloc_expr(ID_allocate, rhs.type()); + malloc_expr.copy_to_operands(object_size); + // could use true and get rid of the code below + malloc_expr.copy_to_operands(false_exprt()); + + target->make_assignment(code_assignt(lhs, malloc_expr)); + target->source_location = location; + + // zero-initialize the object + dereference_exprt deref(lhs, object_type); + exprt zero_object= + zero_initializer(object_type, location, ns, get_message_handler()); + set_class_identifier( + to_struct_expr(zero_object), ns, to_symbol_type(object_type)); + goto_programt::targett t_i=dest.insert_after(target); + t_i->make_assignment(code_assignt(deref, zero_object)); + t_i->source_location=location; +} + +void remove_java_newt::lower_java_new_array( + const exprt &lhs, + const side_effect_exprt &rhs, + goto_programt &dest, + goto_programt::targett target) +{ + // lower_java_new_array without lhs not implemented + PRECONDITION(!lhs.is_nil()); + PRECONDITION(rhs.operands().size() >= 1); // one per dimension + PRECONDITION(rhs.type().id() == ID_pointer); + + source_locationt location=rhs.source_location(); + typet object_type=rhs.type().subtype(); + PRECONDITION(ns.follow(object_type).id() == ID_struct); + + // build size expression + exprt object_size=size_of_expr(object_type, ns); + + CHECK_RETURN(!object_size.is_nil()); + + // we produce a malloc side-effect, which stays + side_effect_exprt malloc_expr(ID_allocate, rhs.type()); + malloc_expr.copy_to_operands(object_size); + // code use true and get rid of the code below + malloc_expr.copy_to_operands(false_exprt()); + + target->make_assignment(code_assignt(lhs, malloc_expr)); + target->source_location=location; + goto_programt::targett next = std::next(target); + + const struct_typet &struct_type=to_struct_type(ns.follow(object_type)); + + // Ideally we would have a check for `is_valid_java_array(struct_type)` but + // `is_valid_java_array is part of the java_bytecode module and we cannot + // introduce such dependencies. We do this simple check instead: + PRECONDITION(struct_type.components().size()==3); + + // Init base class: + dereference_exprt deref(lhs, object_type); + exprt zero_object= + zero_initializer(object_type, location, ns, get_message_handler()); + set_class_identifier( + to_struct_expr(zero_object), ns, to_symbol_type(object_type)); + goto_programt::targett t_i=dest.insert_before(next); + t_i->make_assignment(code_assignt(deref, zero_object)); + t_i->source_location=location; + + // if it's an array, we need to set the length field + member_exprt length( + deref, + struct_type.components()[1].get_name(), + struct_type.components()[1].type()); + goto_programt::targett t_s=dest.insert_before(next); + t_s->make_assignment(code_assignt(length, rhs.op0())); + t_s->source_location=location; + + // we also need to allocate space for the data + member_exprt data( + deref, + struct_type.components()[2].get_name(), + struct_type.components()[2].type()); + + // Allocate a (struct realtype**) instead of a (void**) if possible. + const irept &given_element_type=object_type.find(ID_C_element_type); + typet allocate_data_type; + if(given_element_type.is_not_nil()) + { + allocate_data_type= + pointer_type(static_cast(given_element_type)); + } + else + allocate_data_type=data.type(); + + side_effect_exprt data_java_new_expr( + ID_java_new_array_data, allocate_data_type); + + // The instruction may specify a (hopefully small) upper bound on the + // array size, in which case we allocate a fixed-length array that may + // be larger than the `length` member rather than use a true variable- + // length array, which produces a more complex formula in the current + // backend. + const irept size_bound=rhs.find(ID_length_upper_bound); + if(size_bound.is_nil()) + data_java_new_expr.set(ID_size, rhs.op0()); + else + data_java_new_expr.set(ID_size, size_bound); + + // Must directly assign the new array to a temporary + // because goto-symex will notice `x=side_effect_exprt` but not + // `x=typecast_exprt(side_effect_exprt(...))` + symbol_exprt new_array_data_symbol = get_fresh_aux_symbol( + data_java_new_expr.type(), + "goto_convertt::tmp_new_data_array", + "tmp_new_data_array", + location, + ID_java, + symbol_table).symbol_expr(); + code_declt array_decl(new_array_data_symbol); + array_decl.add_source_location() = location; + goto_programt::targett t_array_decl =dest.insert_before(next); + t_array_decl->make_decl(array_decl); + t_array_decl->source_location = location; + goto_programt::targett t_p2=dest.insert_before(next); + t_p2->make_assignment(code_assignt(new_array_data_symbol, data_java_new_expr)); + t_p2->source_location=location; + + goto_programt::targett t_p=dest.insert_before(next); + exprt cast_java_new=new_array_data_symbol; + if(cast_java_new.type()!=data.type()) + cast_java_new=typecast_exprt(cast_java_new, data.type()); + t_p->make_assignment(code_assignt(data, cast_java_new)); + t_p->source_location=location; + + // zero-initialize the data + if(!rhs.get_bool(ID_skip_initialize)) + { + exprt zero_element= + zero_initializer( + data.type().subtype(), + location, + ns, + get_message_handler()); + codet array_set(ID_array_set); + array_set.copy_to_operands(new_array_data_symbol, zero_element); + goto_programt::targett t_d=dest.insert_before(next); + t_d->make_other(array_set); + t_d->source_location=location; + } + + // multi-dimensional? + + if(rhs.operands().size()>=2) + { + // produce + // for(int i=0; imake_decl(decl); + t_decl->source_location = location; + + code_fort for_loop; + + side_effect_exprt sub_java_new=rhs; + sub_java_new.operands().erase(sub_java_new.operands().begin()); + + assert(rhs.type().id()==ID_pointer); + typet sub_type= + static_cast(rhs.type().subtype().find("#element_type")); + assert(sub_type.id()==ID_pointer); + sub_java_new.type()=sub_type; + + side_effect_exprt inc(ID_assign); + inc.operands().resize(2); + inc.op0()=tmp_i; + inc.op1()=plus_exprt(tmp_i, from_integer(1, tmp_i.type())); + + dereference_exprt deref_expr( + plus_exprt(data, tmp_i), data.type().subtype()); + + code_blockt for_body; + symbol_exprt init_sym = get_fresh_aux_symbol( + length.type(), + "goto_convertt::subarray_init", + "subarray_init", + location, + ID_java, + symbol_table).symbol_expr(); + code_declt init_decl(init_sym); + init_decl.add_source_location() = location; + for_body.move_to_operands(init_decl); + + code_assignt init_subarray(init_sym, sub_java_new); + code_assignt assign_subarray( + deref_expr, + typecast_exprt(init_sym, deref_expr.type())); + for_body.move_to_operands(init_subarray); + for_body.move_to_operands(assign_subarray); + + for_loop.init()=code_assignt(tmp_i, from_integer(0, tmp_i.type())); + for_loop.cond()=binary_relation_exprt(tmp_i, ID_lt, rhs.op0()); + for_loop.iter()=inc; + for_loop.body()=for_body; + + goto_convert(for_loop, symbol_table, tmp, get_message_handler()); + dest.destructive_insert(next, tmp); + } +} + +/// Replace every java_new or java_new_array by a malloc side-effect +/// and zero initialization. +/// \param goto_program: program to process +/// \param target: instruction to check for java_new expressions +/// \return true if a replacement has been made +bool remove_java_newt::lower_java_new( + goto_programt &goto_program, + goto_programt::targett target) +{ + const auto &maybe_code_assign = expr_try_dynamic_cast(target->code); + if(!maybe_code_assign) + return false; + + const exprt &lhs = maybe_code_assign->lhs(); + const exprt &rhs = maybe_code_assign->rhs(); + + if(rhs.id()==ID_side_effect && + rhs.get(ID_statement)==ID_java_new) + { + lower_java_new(lhs, to_side_effect_expr(rhs), goto_program, target); + return true; + } + + if(rhs.id()==ID_side_effect && + rhs.get(ID_statement)==ID_java_new_array) + { + lower_java_new_array(lhs, to_side_effect_expr(rhs), goto_program, target); + return true; + } + + return false; +} + +/// Replace every java_new or java_new_array by a malloc side-effect +/// and zero initialization. +/// Extra auxiliary variables may be introduced into symbol_table. +/// \param goto_program: The function body to work on. +/// \return true if one or more java_new expressions have been replaced +bool remove_java_newt::lower_java_new(goto_programt &goto_program) +{ + bool changed=false; + for(goto_programt::instructionst::iterator target= + goto_program.instructions.begin(); + target!=goto_program.instructions.end(); + ++target) + { + changed=lower_java_new(goto_program, target) || changed; + } + if(!changed) + return false; + goto_program.update(); + return true; +} + +/// Replace every java_new or java_new_array by a malloc side-effect +/// and zero initialization. +/// \remarks Extra auxiliary variables may be introduced into symbol_table. +/// \param target: The instruction to work on. +/// \param goto_program: The function body containing the instruction. +/// \param symbol_table: The symbol table to add symbols to. +void remove_java_new( + goto_programt::targett target, + goto_programt &goto_program, + symbol_table_baset &symbol_table, + message_handlert &message_handler) +{ + remove_java_newt rem(symbol_table, message_handler); + rem.lower_java_new(goto_program, target); +} + +/// Replace every java_new or java_new_array by a malloc side-effect +/// and zero initialization. +/// \remarks Extra auxiliary variables may be introduced into symbol_table. +/// \param function: The function to work on. +/// \param symbol_table: The symbol table to add symbols to. +void remove_java_new( + goto_functionst::goto_functiont &function, + symbol_table_baset &symbol_table, + message_handlert &message_handler) +{ + remove_java_newt rem(symbol_table, message_handler); + rem.lower_java_new(function.body); +} + +/// Replace every java_new or java_new_array by a malloc side-effect +/// and zero initialization. +/// \remarks Extra auxiliary variables may be introduced into symbol_table. +/// \param goto_functions: The functions to work on. +/// \param symbol_table: The symbol table to add symbols to. +void remove_java_new( + goto_functionst &goto_functions, + symbol_table_baset &symbol_table, + message_handlert &message_handler) +{ + remove_java_newt rem(symbol_table, message_handler); + bool changed=false; + for(auto &f : goto_functions.function_map) + changed=rem.lower_java_new(f.second.body) || changed; + if(changed) + goto_functions.compute_location_numbers(); +} + +/// Replace every java_new or java_new_array by a malloc side-effect +/// and zero initialization. +/// \remarks Extra auxiliary variables may be introduced into symbol_table. +/// \param goto_model: The functions to work on and the symbol table to add +/// symbols to. +void remove_java_new(goto_modelt &goto_model, + message_handlert &message_handler) +{ + remove_java_new(goto_model.goto_functions, goto_model.symbol_table, message_handler); +} diff --git a/src/java_bytecode/remove_java_new.h b/src/java_bytecode/remove_java_new.h new file mode 100644 index 00000000000..4bccea06697 --- /dev/null +++ b/src/java_bytecode/remove_java_new.h @@ -0,0 +1,42 @@ +/*******************************************************************\ + +Module: Remove Java New Operators + +Author: Peter Schrammel + +\*******************************************************************/ + +/// \file +/// Remove Java New Operators + +#ifndef CPROVER_GOTO_PROGRAMS_REMOVE_JAVA_NEW_H +#define CPROVER_GOTO_PROGRAMS_REMOVE_JAVA_NEW_H + +#include + +#include +#include + +class message_handlert; + +void remove_java_new( + goto_programt::targett target, + goto_programt &goto_program, + symbol_table_baset &symbol_table, + message_handlert &_message_handler); + +void remove_java_new( + goto_functionst::goto_functiont &function, + symbol_table_baset &symbol_table, + message_handlert &_message_handler); + +void remove_java_new( + goto_functionst &goto_functions, + symbol_table_baset &symbol_table, + message_handlert &_message_handler); + +void remove_java_new( + goto_modelt &model, + message_handlert &_message_handler); + +#endif // CPROVER_GOTO_PROGRAMS_REMOVE_JAVA_NEW_H From 1b96488b117384110e21c78df8cb240bd3bbef23 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sat, 7 Apr 2018 13:02:08 +0100 Subject: [PATCH 17/18] Use remove_java_new --- src/jbmc/jbmc_parse_options.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp index 196e2ca567f..926e896ff78 100644 --- a/src/jbmc/jbmc_parse_options.cpp +++ b/src/jbmc/jbmc_parse_options.cpp @@ -56,6 +56,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include @@ -711,6 +712,8 @@ void jbmc_parse_optionst::process_goto_function( try { + // Replace Java new side effects + remove_java_new(goto_function, symbol_table, get_message_handler()); // Removal of RTTI inspection: remove_instanceof(goto_function, symbol_table); // Java virtual functions -> explicit dispatch tables: From d146ddf3ce946d3959b4e00238a5c085b7e0bcd3 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sat, 7 Apr 2018 12:51:06 +0100 Subject: [PATCH 18/18] Remove java_bytecode deps from Makefiles --- src/cbmc/CMakeLists.txt | 1 - src/cbmc/Makefile | 1 - src/clobber/CMakeLists.txt | 1 - src/clobber/Makefile | 2 +- src/goto-cc/CMakeLists.txt | 1 - src/goto-cc/Makefile | 1 - src/goto-cc/goto_cc_languages.cpp | 2 -- 7 files changed, 1 insertion(+), 8 deletions(-) diff --git a/src/cbmc/CMakeLists.txt b/src/cbmc/CMakeLists.txt index cf0034f5484..b1cae0f8b01 100644 --- a/src/cbmc/CMakeLists.txt +++ b/src/cbmc/CMakeLists.txt @@ -16,7 +16,6 @@ target_link_libraries(cbmc-lib goto-instrument-lib goto-programs goto-symex - java_bytecode json langapi linking diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile index c1d88efa6be..9da2d96efc2 100644 --- a/src/cbmc/Makefile +++ b/src/cbmc/Makefile @@ -17,7 +17,6 @@ SRC = all_properties.cpp \ OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../cpp/cpp$(LIBEXT) \ - ../java_bytecode/java_bytecode$(LIBEXT) \ ../linking/linking$(LIBEXT) \ ../big-int/big-int$(LIBEXT) \ ../goto-programs/goto-programs$(LIBEXT) \ diff --git a/src/clobber/CMakeLists.txt b/src/clobber/CMakeLists.txt index 384ae51824e..2e4803df7e2 100644 --- a/src/clobber/CMakeLists.txt +++ b/src/clobber/CMakeLists.txt @@ -25,7 +25,6 @@ target_link_libraries(clobber-lib ) add_if_library(clobber-lib bv_refinement) -add_if_library(clobber-lib java_bytecode) add_if_library(clobber-lib specc) add_if_library(clobber-lib php) diff --git a/src/clobber/Makefile b/src/clobber/Makefile index 74a133782c6..d9b9f09de1c 100644 --- a/src/clobber/Makefile +++ b/src/clobber/Makefile @@ -1,9 +1,9 @@ SRC = clobber_main.cpp \ clobber_parse_options.cpp \ # Empty last line + OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../cpp/cpp$(LIBEXT) \ - ../java_bytecode/java_bytecode$(LIBEXT) \ ../linking/linking$(LIBEXT) \ ../big-int/big-int$(LIBEXT) \ ../goto-programs/goto-programs$(LIBEXT) \ diff --git a/src/goto-cc/CMakeLists.txt b/src/goto-cc/CMakeLists.txt index 8259d960561..75b8a7f860c 100644 --- a/src/goto-cc/CMakeLists.txt +++ b/src/goto-cc/CMakeLists.txt @@ -19,7 +19,6 @@ target_link_libraries(goto-cc-lib langapi ) -add_if_library(goto-cc-lib java_bytecode) add_if_library(goto-cc-lib jsil) # Executable diff --git a/src/goto-cc/Makefile b/src/goto-cc/Makefile index 374ed507b44..6874910fbcc 100644 --- a/src/goto-cc/Makefile +++ b/src/goto-cc/Makefile @@ -24,7 +24,6 @@ OBJ += ../big-int/big-int$(LIBEXT) \ ../linking/linking$(LIBEXT) \ ../ansi-c/ansi-c$(LIBEXT) \ ../cpp/cpp$(LIBEXT) \ - ../java_bytecode/java_bytecode$(LIBEXT) \ ../xmllang/xmllang$(LIBEXT) \ ../assembler/assembler$(LIBEXT) \ ../langapi/langapi$(LIBEXT) \ diff --git a/src/goto-cc/goto_cc_languages.cpp b/src/goto-cc/goto_cc_languages.cpp index 12ea70c04e7..c3246b5b8f1 100644 --- a/src/goto-cc/goto_cc_languages.cpp +++ b/src/goto-cc/goto_cc_languages.cpp @@ -15,7 +15,6 @@ Author: CM Wintersteiger #include #include -#include #include #ifdef HAVE_SPECC @@ -26,7 +25,6 @@ void goto_cc_modet::register_languages() { register_language(new_ansi_c_language); register_language(new_cpp_language); - register_language(new_java_bytecode_language); register_language(new_jsil_language); #ifdef HAVE_SPECC