From c8cf10086767b71c5b075f9eea4082c2ff4850f6 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Tue, 20 Feb 2018 15:56:46 +0000 Subject: [PATCH 1/4] 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..4625559f11c 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 directory **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 directory **Key classes:** * \ref languaget and its subclasses From 9a8c2924303104328444d07e510369130512c04f Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 15 Mar 2018 15:44:24 +0000 Subject: [PATCH 2/4] 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 994a3b10be3..0f394199fe0 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 2eb3714afd85c75d7e894e8f008eb54ea125f35c Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sat, 21 Apr 2018 21:19:43 +0100 Subject: [PATCH 3/4] Move replace_java_nondet to java_bytecode --- src/goto-programs/Makefile | 1 - src/java_bytecode/Makefile | 1 + .../replace_java_nondet.cpp | 9 ++++----- .../replace_java_nondet.h | 4 ++-- src/jbmc/jbmc_parse_options.cpp | 2 +- .../java_bytecode/java_replace_nondet/replace_nondet.cpp | 2 +- 6 files changed, 9 insertions(+), 10 deletions(-) rename src/{goto-programs => java_bytecode}/replace_java_nondet.cpp (98%) rename src/{goto-programs => java_bytecode}/replace_java_nondet.h (88%) diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile index 35f5c01050e..c16ba9f9ae0 100644 --- a/src/goto-programs/Makefile +++ b/src/goto-programs/Makefile @@ -50,7 +50,6 @@ SRC = basic_blocks.cpp \ remove_unused_functions.cpp \ remove_vector.cpp \ remove_virtual_functions.cpp \ - replace_java_nondet.cpp \ generate_function_bodies.cpp \ resolve_inherited_component.cpp \ safety_checker.cpp \ diff --git a/src/java_bytecode/Makefile b/src/java_bytecode/Makefile index e07faa26343..cf6d7a5cc9d 100644 --- a/src/java_bytecode/Makefile +++ b/src/java_bytecode/Makefile @@ -31,6 +31,7 @@ SRC = bytecode_info.cpp \ java_types.cpp \ java_utils.cpp \ mz_zip_archive.cpp \ + replace_java_nondet.cpp \ remove_exceptions.cpp \ remove_instanceof.cpp \ select_pointer_type.cpp \ diff --git a/src/goto-programs/replace_java_nondet.cpp b/src/java_bytecode/replace_java_nondet.cpp similarity index 98% rename from src/goto-programs/replace_java_nondet.cpp rename to src/java_bytecode/replace_java_nondet.cpp index 19adc917fbe..5054ef5b027 100644 --- a/src/goto-programs/replace_java_nondet.cpp +++ b/src/java_bytecode/replace_java_nondet.cpp @@ -9,12 +9,11 @@ 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 "replace_java_nondet.h" -#include "util/irep_ids.h" +#include +#include +#include #include #include diff --git a/src/goto-programs/replace_java_nondet.h b/src/java_bytecode/replace_java_nondet.h similarity index 88% rename from src/goto-programs/replace_java_nondet.h rename to src/java_bytecode/replace_java_nondet.h index 3653908588d..4a0b00c3b1e 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; diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp index 93306e74a03..0a80a382b94 100644 --- a/src/jbmc/jbmc_parse_options.cpp +++ b/src/jbmc/jbmc_parse_options.cpp @@ -36,7 +36,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 #include diff --git a/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp b/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp index 5995ce9a288..7c5ec5860c5 100644 --- a/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp +++ b/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp @@ -13,9 +13,9 @@ #include #include #include -#include #include +#include #include #include From a079f4628092c9c86b10412574dde00ffb4cd118 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sat, 21 Apr 2018 21:29:38 +0100 Subject: [PATCH 4/4] Clang-format moved file --- src/java_bytecode/replace_java_nondet.cpp | 109 ++++++++++++---------- 1 file changed, 60 insertions(+), 49 deletions(-) diff --git a/src/java_bytecode/replace_java_nondet.cpp b/src/java_bytecode/replace_java_nondet.cpp index 5054ef5b027..264de82328b 100644 --- a/src/java_bytecode/replace_java_nondet.cpp +++ b/src/java_bytecode/replace_java_nondet.cpp @@ -23,23 +23,35 @@ Author: Reuben Thomas, reuben.thomas@diffblue.com 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; @@ -51,11 +63,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.*))"); @@ -73,19 +85,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); } @@ -93,10 +105,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. @@ -104,20 +116,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 @@ -135,7 +147,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); } @@ -164,10 +176,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; } @@ -226,8 +239,8 @@ static goto_programt::targett check_and_replace_target( // Assume that the LHS of *this* assignment is the actual nondet variable const auto &code_assign = to_code_assign(assignment_instruction->code); - const auto nondet_var=code_assign.lhs(); - const auto source_loc=target->source_location; + 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(assignment_instruction); @@ -238,20 +251,19 @@ static goto_programt::targett check_and_replace_target( 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(); @@ -264,13 +276,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); } }