From 6b519ad0293ad520962cc518c1368ccfaad47a33 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 25 Sep 2017 07:52:39 +0100 Subject: [PATCH 01/10] Add identifier and rename statement to java_new_array_data This will be used as an alternative to java_new_array. This is to distinguish the statement before and after symex: java_new_array is used before symex, it is then transformed into some instrtuction containing a java_new_array_data by symex. Symex use to add a new java_new_array statement which was confusing. --- src/goto-programs/builtin_functions.cpp | 3 ++- src/goto-programs/goto_convert.cpp | 6 ++++-- src/goto-symex/symex_assign.cpp | 6 +++--- src/goto-symex/symex_builtin_functions.cpp | 7 ++++--- src/util/irep_ids.def | 1 + 5 files changed, 14 insertions(+), 9 deletions(-) diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index 2baf2cdbb31..0bc565ea1d2 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -705,7 +705,8 @@ void goto_convertt::do_java_new_array( else allocate_data_type=data.type(); - side_effect_exprt data_java_new_expr(ID_java_new_array, allocate_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 diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index 430a583e69a..c96e3941cf3 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -760,8 +760,10 @@ void goto_convertt::convert_assign( do_java_new_array(lhs, to_side_effect_expr(rhs), dest); } - else if(rhs.id()==ID_side_effect && - rhs.get(ID_statement)==ID_malloc) + else if( + rhs.id() == ID_side_effect && + (rhs.get(ID_statement) == ID_malloc || + rhs.get(ID_statement) == ID_java_new_array_data)) { // just preserve Forall_operands(it, rhs) diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp index 518df75b954..f8db5a92442 100644 --- a/src/goto-symex/symex_assign.cpp +++ b/src/goto-symex/symex_assign.cpp @@ -59,9 +59,9 @@ void goto_symext::symex_assign( throw "symex_assign: unexpected function call: "+id2string(identifier); } - else if(statement==ID_cpp_new || - statement==ID_cpp_new_array || - statement==ID_java_new_array) + else if( + statement == ID_cpp_new || statement == ID_cpp_new_array || + statement == ID_java_new_array_data) symex_cpp_new(state, lhs, side_effect_expr); else if(statement==ID_malloc) symex_malloc(state, lhs, side_effect_expr); diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp index aede4347214..abd1b23729c 100644 --- a/src/goto-symex/symex_builtin_functions.cpp +++ b/src/goto-symex/symex_builtin_functions.cpp @@ -376,8 +376,9 @@ 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); + do_array = + (code.get(ID_statement) == ID_cpp_new_array || + code.get(ID_statement) == ID_java_new_array_data); dynamic_counter++; @@ -393,7 +394,7 @@ void goto_symext::symex_cpp_new( if(code.get(ID_statement)==ID_cpp_new_array || code.get(ID_statement)==ID_cpp_new) symbol.mode=ID_cpp; - else if(code.get(ID_statement)==ID_java_new_array) + else if(code.get(ID_statement) == ID_java_new_array_data) symbol.mode=ID_java; else INVARIANT_WITH_IREP(false, "Unexpected side effect expression", code); diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index ac1f75b7f60..e72c603e4e1 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -217,6 +217,7 @@ IREP_ID_TWO(cpp_new_array, cpp_new[]) IREP_ID_TWO(cpp_delete_array, cpp_delete[]) IREP_ID_ONE(java_new) IREP_ID_ONE(java_new_array) +IREP_ID_ONE(java_new_array_data) IREP_ID_ONE(java_string_literal) IREP_ID_ONE(printf) IREP_ID_ONE(input) From e36d7d8a84ed995fe9d95fc7ada519efb5f1b895 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 26 Sep 2017 15:41:09 +0100 Subject: [PATCH 02/10] Check if object is nil before writing trace We were accessing fields of the expression without first checking that it is not nil which could lead to invalid memory access --- src/goto-programs/goto_trace.cpp | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp index 15749d2012d..ccc0cdfcf6a 100644 --- a/src/goto-programs/goto_trace.cpp +++ b/src/goto-programs/goto_trace.cpp @@ -91,7 +91,7 @@ void goto_trace_stept::output( out << "\n"; - if(pc->is_other() || pc->is_assign()) + if((pc->is_other() && lhs_object.is_not_nil()) || pc->is_assign()) { irep_idt identifier=lhs_object.get_object_name(); out << " " << from_expr(ns, identifier, lhs_object.get_original_expr()) @@ -386,14 +386,8 @@ void show_goto_trace( break; case goto_trace_stept::typet::CONSTRAINT: - UNREACHABLE; - break; - case goto_trace_stept::typet::SHARED_READ: case goto_trace_stept::typet::SHARED_WRITE: - UNREACHABLE; - break; - default: UNREACHABLE; } From fe2efa742f474af52642be8dcec8ea6e0f1895d7 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 26 Sep 2017 15:43:30 +0100 Subject: [PATCH 03/10] Style: Replace assert by appropriate macros --- src/goto-programs/builtin_functions.cpp | 60 +++++-------------------- 1 file changed, 10 insertions(+), 50 deletions(-) diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index 0bc565ea1d2..e998fb3ab8a 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -569,35 +569,15 @@ void goto_convertt::do_java_new( const side_effect_exprt &rhs, goto_programt &dest) { - if(lhs.is_nil()) - { - error().source_location=lhs.find_source_location(); - error() << "do_java_new without lhs is yet to be implemented" << eom; - throw 0; - } - + PRECONDITION(!lhs.is_nil()); + PRECONDITION(rhs.operands().empty()); + PRECONDITION(rhs.type().id() == ID_pointer); source_locationt location=rhs.source_location(); - - assert(rhs.operands().empty()); - - if(rhs.type().id()!=ID_pointer) - { - error().source_location=rhs.find_source_location(); - error() << "do_java_new returns pointer" << eom; - throw 0; - } - typet object_type=rhs.type().subtype(); // build size expression exprt object_size=size_of_expr(object_type, ns); - - if(object_size.is_nil()) - { - error().source_location=rhs.find_source_location(); - error() << "do_java_new got nil object_size" << eom; - throw 0; - } + CHECK_RETURN(object_size.is_not_nil()); // we produce a malloc side-effect, which stays side_effect_exprt malloc_expr(ID_malloc); @@ -624,36 +604,18 @@ void goto_convertt::do_java_new_array( const side_effect_exprt &rhs, goto_programt &dest) { - if(lhs.is_nil()) - { - error().source_location=lhs.find_source_location(); - error() << "do_java_new_array without lhs is yet to be implemented" - << eom; - throw 0; - } + 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(); - - assert(rhs.operands().size()>=1); // one per dimension - - if(rhs.type().id()!=ID_pointer) - { - error().source_location=rhs.find_source_location(); - error() << "do_java_new_array returns pointer" << eom; - throw 0; - } - 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); - if(object_size.is_nil()) - { - error().source_location=rhs.find_source_location(); - error() << "do_java_new_array got nil object_size" << eom; - throw 0; - } + CHECK_RETURN(!object_size.is_nil()); // we produce a malloc side-effect, which stays side_effect_exprt malloc_expr(ID_malloc); @@ -664,9 +626,8 @@ void goto_convertt::do_java_new_array( t_n->code=code_assignt(lhs, malloc_expr); t_n->source_location=location; - assert(ns.follow(object_type).id()==ID_struct); const struct_typet &struct_type=to_struct_type(ns.follow(object_type)); - assert(struct_type.components().size()==3); + PRECONDITION(struct_type.components().size() == 3); // Init base class: dereference_exprt deref(lhs, object_type); @@ -696,7 +657,6 @@ void goto_convertt::do_java_new_array( // 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; - exprt cast_data_member; if(given_element_type.is_not_nil()) { allocate_data_type= From 465e5dc961c7ac7d005673f0327d29007194e63a Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 26 Sep 2017 15:43:55 +0100 Subject: [PATCH 04/10] Style: improve documentation in interpreter evaluate --- src/goto-programs/interpreter_evaluate.cpp | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp index 72c1429d2aa..71eed0c7bf8 100644 --- a/src/goto-programs/interpreter_evaluate.cpp +++ b/src/goto-programs/interpreter_evaluate.cpp @@ -21,8 +21,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -/// reads a memory address and loads it into the dest variable marks cell as -/// read before written if cell has never been written +/// Reads a memory address and loads it into the `dest` variable. +/// Marks cell as `READ_BEFORE_WRITTEN` if cell has never been written. void interpretert::read( const mp_integer &address, mp_vectort &dest) const @@ -102,7 +102,9 @@ void interpretert::clear_input_flags() } } -/// \return Number of leaf primitive types; returns true on error +/// \param ty: a type +/// \param [out] result: Number of leaf primitive types in `ty` +/// \return returns true on error bool interpretert::count_type_leaves(const typet &ty, mp_integer &result) { if(ty.id()==ID_struct) @@ -299,6 +301,9 @@ bool interpretert::memory_offset_to_byte_offset( } } +/// Evaluate an expression +/// \param expr: expression to evaluate +/// \param [out] dest: vector in which the result of the evaluation is stored void interpretert::evaluate( const exprt &expr, mp_vectort &dest) From 42c079d15331f9792efc44f298a127dc8c83cc95 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 2 Oct 2017 09:26:19 +0100 Subject: [PATCH 05/10] Use existing function for checking object is array --- src/goto-programs/builtin_functions.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index e998fb3ab8a..d6a22dea593 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -31,6 +31,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include "format_strings.h" @@ -627,7 +628,7 @@ void goto_convertt::do_java_new_array( t_n->source_location=location; const struct_typet &struct_type=to_struct_type(ns.follow(object_type)); - PRECONDITION(struct_type.components().size() == 3); + PRECONDITION(is_valid_java_array(struct_type)); // Init base class: dereference_exprt deref(lhs, object_type); From fc363b30955adb20842cecf816b2466e241a05b6 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 2 Oct 2017 09:26:45 +0100 Subject: [PATCH 06/10] Typo in goto_trace output --- src/goto-programs/goto_trace.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp index ccc0cdfcf6a..b6649e97ffc 100644 --- a/src/goto-programs/goto_trace.cpp +++ b/src/goto-programs/goto_trace.cpp @@ -47,7 +47,9 @@ void goto_trace_stept::output( case goto_trace_stept::typet::DEAD: out << "DEAD"; break; case goto_trace_stept::typet::OUTPUT: out << "OUTPUT"; break; case goto_trace_stept::typet::INPUT: out << "INPUT"; break; - case goto_trace_stept::typet::ATOMIC_BEGIN: out << "ATOMC_BEGIN"; break; + case goto_trace_stept::typet::ATOMIC_BEGIN: + out << "ATOMIC_BEGIN"; + break; case goto_trace_stept::typet::ATOMIC_END: out << "ATOMIC_END"; break; case goto_trace_stept::typet::SHARED_READ: out << "SHARED_READ"; break; case goto_trace_stept::typet::SHARED_WRITE: out << "SHARED WRITE"; break; From 5a0343f56465ef9fe07793859f9bf95247452a85 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 2 Oct 2017 09:45:26 +0100 Subject: [PATCH 07/10] Doc: Summary for count_type_leaves --- src/goto-programs/interpreter_evaluate.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp index 71eed0c7bf8..5a379a880f5 100644 --- a/src/goto-programs/interpreter_evaluate.cpp +++ b/src/goto-programs/interpreter_evaluate.cpp @@ -102,6 +102,9 @@ void interpretert::clear_input_flags() } } +/// Count the number of leaf subtypes of `ty`, a leaf type is a type that is +/// not an array or a struct. For instance the count for a type such as +/// `struct { (int[3])[5]; int }` would be 16 = (3 * 5 + 1). /// \param ty: a type /// \param [out] result: Number of leaf primitive types in `ty` /// \return returns true on error From 435958f358994d19483fe7292904aec25d782d13 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 2 Oct 2017 09:28:25 +0100 Subject: [PATCH 08/10] Unit test for goto_trace::output --- unit/goto-programs/goto_trace_output.cpp | 26 ++++++++++++++++++++++++ 1 file changed, 26 insertions(+) create mode 100644 unit/goto-programs/goto_trace_output.cpp diff --git a/unit/goto-programs/goto_trace_output.cpp b/unit/goto-programs/goto_trace_output.cpp new file mode 100644 index 00000000000..2e9d43df63c --- /dev/null +++ b/unit/goto-programs/goto_trace_output.cpp @@ -0,0 +1,26 @@ +/*******************************************************************\ + + Module: Unit tests for goto_trace_stept::output + + Author: Diffblue Limited. All rights reserved. + +\*******************************************************************/ + +#include +#include +#include +#include + +SCENARIO( + "Output trace with nil lhs object", + "[core][goto-programs][goto_trace]") +{ + symbol_tablet symbol_table; + namespacet ns(symbol_table); + goto_programt::instructionst instructions; + instructions.emplace_back(goto_program_instruction_typet::OTHER); + goto_trace_stept step; + step.pc = instructions.begin(); + step.type = goto_trace_stept::typet::ATOMIC_BEGIN; + step.output(ns, std::cout); +} From 0dafac2774164e68d0e2fed3eefd0a75b98cc426 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 11 Oct 2017 07:39:29 +0100 Subject: [PATCH 09/10] Add unit test for goto_trace_output in Makefile --- unit/Makefile | 1 + 1 file changed, 1 insertion(+) diff --git a/unit/Makefile b/unit/Makefile index 9cef527c3e8..1eb519b64fe 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -16,6 +16,7 @@ SRC += unit_tests.cpp \ analyses/does_remove_const/does_expr_lose_const.cpp \ analyses/does_remove_const/does_type_preserve_const_correctness.cpp \ analyses/does_remove_const/is_type_at_least_as_const_as.cpp \ + goto-programs/goto_trace_output.cpp \ java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp \ java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp \ java_bytecode/java_object_factory/gen_nondet_string_init.cpp \ From 1fa64a99845dfa21cb5dfc6ca9e7630fbf575842 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 27 Oct 2017 08:09:48 +0100 Subject: [PATCH 10/10] Avoid using is_valid_java_array in builin_functions This is part of another module and we should avoid dependencies. In particular cmake fails in some cases. --- src/goto-programs/builtin_functions.cpp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index d6a22dea593..bf5b6cf3a3d 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -31,7 +31,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include "format_strings.h" @@ -628,7 +627,11 @@ void goto_convertt::do_java_new_array( t_n->source_location=location; const struct_typet &struct_type=to_struct_type(ns.follow(object_type)); - PRECONDITION(is_valid_java_array(struct_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);