From 440d19f2f009edf126f6a5319ecae7bd8874f923 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Sat, 12 Aug 2017 18:40:46 +0100 Subject: [PATCH 1/2] Adding string max input length option --- .../max_input_length/MemberTest.class | Bin 0 -> 712 bytes .../max_input_length/MemberTest.desc | 7 ++ .../max_input_length/MemberTest.java | 9 ++ src/cbmc/cbmc_parse_options.cpp | 15 ++- src/cbmc/cbmc_parse_options.h | 1 + src/goto-programs/convert_nondet.cpp | 24 ++--- src/goto-programs/convert_nondet.h | 12 +-- src/java_bytecode/java_bytecode_language.cpp | 13 +-- src/java_bytecode/java_bytecode_language.h | 24 ++++- src/java_bytecode/java_entry_point.cpp | 27 ++--- src/java_bytecode/java_entry_point.h | 7 +- src/java_bytecode/java_object_factory.cpp | 96 +++++++++++------- src/java_bytecode/java_object_factory.h | 13 +-- 13 files changed, 141 insertions(+), 107 deletions(-) create mode 100644 regression/strings-smoke-tests/max_input_length/MemberTest.class create mode 100644 regression/strings-smoke-tests/max_input_length/MemberTest.desc create mode 100644 regression/strings-smoke-tests/max_input_length/MemberTest.java diff --git a/regression/strings-smoke-tests/max_input_length/MemberTest.class b/regression/strings-smoke-tests/max_input_length/MemberTest.class new file mode 100644 index 0000000000000000000000000000000000000000..cbb5dcfdbbd4bfb5916f4bd046d9421035deeb40 GIT binary patch literal 712 zcmaJKyYu7Mm#+YtSk-WGQsGnqr!^eR7okxTb4J3m z3JV$q={Tpch$V&dgv`q@Bve{E-dk_Y_k#XfJBe)2zeAW=^5WP;i4BAJfsMV6Z+ZmU zCgj&`V3WH%U0;4q$Zmu^LnyUuV4e(iJ0^N2&0N^^Y(SW7CtmmUruXJBU0Cn>hXA@A z4x+AkWTm~dY0_a6Czphei)mB{<-fTR>X)xvz1F;b>a&ozdi4}2gTW1CNt zQkosLzTi=TTRniYRmlvIZGA*;54FZ;#dxwbw6t;#aeiK9|MV#Vk!PQV$ z;lF2&qavK2SX6KnCytL6HPhw5bVcuDVh<|&9@)$%::max() #define MAX_NONDET_TREE_DEPTH 5 class symbolt; @@ -59,6 +60,23 @@ enum lazy_methods_modet LAZY_METHODS_MODE_CONTEXT_SENSITIVE }; +struct object_factory_parameterst final +{ + /// Maximum value for the non-deterministically-chosen length of an array. + size_t max_nondet_array_length=MAX_NONDET_ARRAY_LENGTH_DEFAULT; + + /// Maximum value for the non-deterministically-chosen length of a string. + size_t max_nondet_string_length=MAX_NONDET_STRING_LENGTH; + + /// Maximum depth for object hierarchy on input. + /// Used to prevent object factory to loop infinitely during the + /// generation of code that allocates/initializes data structures of recursive + /// data types or unbounded depth. We bound the maximum number of times we + /// dereference a pointer using a 'depth counter'. We set a pointer to null if + /// such depth becomes >= than this maximum value. + size_t max_nondet_tree_depth=MAX_NONDET_TREE_DEPTH; +}; + typedef std::pair< const symbolt *, const java_bytecode_parse_treet::methodt *> @@ -95,8 +113,7 @@ class java_bytecode_languaget:public languaget java_bytecode_languaget( std::unique_ptr pointer_type_selector): assume_inputs_non_null(false), - max_nondet_array_length(MAX_NONDET_ARRAY_LENGTH_DEFAULT), - max_nondet_tree_depth(MAX_NONDET_TREE_DEPTH), + object_factory_parameters(), max_user_array_length(0), lazy_methods_mode(lazy_methods_modet::LAZY_METHODS_MODE_EAGER), string_refinement_enabled(false), @@ -149,8 +166,7 @@ class java_bytecode_languaget:public languaget std::vector main_jar_classes; java_class_loadert java_class_loader; bool assume_inputs_non_null; // assume inputs variables to be non-null - size_t max_nondet_array_length; // maximal length for non-det array creation - size_t max_nondet_tree_depth; // maximal depth for object tree in non-det creation + object_factory_parameterst object_factory_parameters; size_t max_user_array_length; // max size for user code created arrays lazy_methodst lazy_methods; lazy_methods_modet lazy_methods_mode; diff --git a/src/java_bytecode/java_entry_point.cpp b/src/java_bytecode/java_entry_point.cpp index 12e806b8e2f..e456556c258 100644 --- a/src/java_bytecode/java_entry_point.cpp +++ b/src/java_bytecode/java_entry_point.cpp @@ -90,8 +90,7 @@ void java_static_lifetime_init( symbol_tablet &symbol_table, const source_locationt &source_location, bool assume_init_pointers_not_null, - unsigned max_nondet_array_length, - unsigned max_nondet_tree_depth, + const object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector) { symbolt &initialize_symbol=symbol_table.lookup(INITIALIZE); @@ -132,8 +131,7 @@ void java_static_lifetime_init( code_block, allow_null, symbol_table, - max_nondet_array_length, - max_nondet_tree_depth, + object_factory_parameters, allocation_typet::GLOBAL, source_location, pointer_type_selector); @@ -164,8 +162,7 @@ exprt::operandst java_build_arguments( code_blockt &init_code, symbol_tablet &symbol_table, bool assume_init_pointers_not_null, - size_t max_nondet_array_length, - size_t max_nondet_tree_depth, + object_factory_parameterst object_factory_parameters, const select_pointer_typet &pointer_type_selector) { const code_typet::parameterst ¶meters= @@ -221,8 +218,7 @@ exprt::operandst java_build_arguments( init_code, allow_null, symbol_table, - max_nondet_array_length, - max_nondet_tree_depth, + object_factory_parameters, allocation_typet::LOCAL, function.location, pointer_type_selector); @@ -481,8 +477,7 @@ bool java_entry_point( const irep_idt &main_class, message_handlert &message_handler, bool assume_init_pointers_not_null, - size_t max_nondet_array_length, - size_t max_nondet_tree_depth, + const object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector) { // check if the entry point is already there @@ -506,8 +501,7 @@ bool java_entry_point( symbol_table, symbol.location, assume_init_pointers_not_null, - max_nondet_array_length, - max_nondet_tree_depth, + object_factory_parameters, pointer_type_selector); return generate_java_start_function( @@ -515,8 +509,7 @@ bool java_entry_point( symbol_table, message_handler, assume_init_pointers_not_null, - max_nondet_array_length, - max_nondet_tree_depth, + object_factory_parameters, pointer_type_selector); } @@ -538,8 +531,7 @@ bool generate_java_start_function( symbol_tablet &symbol_table, message_handlert &message_handler, bool assume_init_pointers_not_null, - size_t max_nondet_array_length, - size_t max_nondet_tree_depth, + const object_factory_parameterst& object_factory_parameters, const select_pointer_typet &pointer_type_selector) { messaget message(message_handler); @@ -618,8 +610,7 @@ bool generate_java_start_function( init_code, symbol_table, assume_init_pointers_not_null, - max_nondet_array_length, - max_nondet_tree_depth, + object_factory_parameters, pointer_type_selector); call_main.arguments()=main_arguments; diff --git a/src/java_bytecode/java_entry_point.h b/src/java_bytecode/java_entry_point.h index cc03e8480b5..9461a4a826d 100644 --- a/src/java_bytecode/java_entry_point.h +++ b/src/java_bytecode/java_entry_point.h @@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #define JAVA_ENTRY_POINT_RETURN_SYMBOL "return'" #define JAVA_ENTRY_POINT_EXCEPTION_SYMBOL "uncaught_exception'" @@ -22,8 +23,7 @@ bool java_entry_point( const irep_idt &main_class, class message_handlert &message_handler, bool assume_init_pointers_not_null, - size_t max_nondet_array_length, - size_t max_nondet_tree_depth, + const object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector); typedef struct @@ -45,8 +45,7 @@ bool generate_java_start_function( class symbol_tablet &symbol_table, class message_handlert &message_handler, bool assume_init_pointers_not_null, - size_t max_nondet_array_length, - size_t max_nondet_tree_depth, + const object_factory_parameterst& object_factory_parameters, const select_pointer_typet &pointer_type_selector); #endif // CPROVER_JAVA_BYTECODE_JAVA_ENTRY_POINT_H diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp index b9e3da19651..ff2ae2784eb 100644 --- a/src/java_bytecode/java_object_factory.cpp +++ b/src/java_bytecode/java_object_factory.cpp @@ -58,15 +58,7 @@ class java_object_factoryt /// methods in this class. const source_locationt &loc; - /// Maximum value for the non-deterministically-chosen length of an array. - const size_t max_nondet_array_length; - - /// Used to prevent the methods in this class to loop infinitely during the - /// generation of code that allocates/initializes data structures of recursive - /// data types or unbounded depth. We bound the maximum number of times we - /// dereference a pointer using a 'depth counter'. We set a pointer to null if - /// such depth becomes >= than this maximum value. - const size_t max_nondet_tree_depth; + const object_factory_parameterst object_factory_parameters; /// This is employed in conjunction with the depth above. Every time the /// non-det generator visits a type, the type is added to this set. We forbid @@ -107,14 +99,12 @@ class java_object_factoryt java_object_factoryt( std::vector &_symbols_created, const source_locationt &loc, - size_t _max_nondet_array_length, - size_t _max_nondet_tree_depth, + const object_factory_parameterst _object_factory_parameters, symbol_tablet &_symbol_table, const select_pointer_typet &pointer_type_selector): symbols_created(_symbols_created), loc(loc), - max_nondet_array_length(_max_nondet_array_length), - max_nondet_tree_depth(_max_nondet_tree_depth), + object_factory_parameters(_object_factory_parameters), symbol_table(_symbol_table), ns(_symbol_table), pointer_type_selector(pointer_type_selector) @@ -591,7 +581,7 @@ void java_object_factoryt::gen_nondet_pointer_init( // If this is a recursive type of some kind AND the depth is exceeded, set // the pointer to null. if(!recursion_set_entry.insert_entry(struct_tag) && - depth>=max_nondet_tree_depth) + depth>=object_factory_parameters.max_nondet_tree_depth) { if(update_in_place==update_in_placet::NO_UPDATE_IN_PLACE) { @@ -760,6 +750,19 @@ symbol_exprt java_object_factoryt::gen_nondet_subtype_pointer_init( return new_symbol.symbol_expr(); } +/// Get max value for an integral type +/// \param type: +/// Type to find maximum value for +/// \return Maximum integral valu +static size_t max_value(const typet& type) +{ + if(type.id()==ID_signedbv) + return std::numeric_limits::max(); + else if(type.id()==ID_unsignedbv) + return std::numeric_limits::max(); + UNREACHABLE; +} + /// Initializes an object tree rooted at `expr`, allocating child objects as /// necessary and nondet-initializes their members, or if MUST_UPDATE_IN_PLACE /// is set, re-initializes already-allocated objects. @@ -863,6 +866,30 @@ void java_object_factoryt::gen_nondet_struct_init( true, // allow_null always true for sub-objects depth, substruct_in_place); + + if(name=="length") + { + if(class_identifier=="java.lang.String" || + class_identifier=="java.lang.StringBuffer" || + class_identifier=="java.lang.StringBuilder") + { + if(object_factory_parameters.max_nondet_string_length <= + max_value(me.type())) + { + exprt max_length=from_integer( + object_factory_parameters.max_nondet_string_length, me.type()); + assignments.add(code_assumet( + binary_relation_exprt(me, ID_le, max_length))); + } + } + else + { + INVARIANT( + class_identifier!="java.lang.CharSequence" && + class_identifier!="java.lang.AbstractStringBuilder", + "Trying to initialize abstract class"); + } + } } } } @@ -1043,7 +1070,8 @@ void java_object_factoryt::gen_nondet_array_init( const typet &element_type= static_cast(expr.type().subtype().find(ID_C_element_type)); - auto max_length_expr=from_integer(max_nondet_array_length, java_int_type()); + auto max_length_expr=from_integer( + object_factory_parameters.max_nondet_array_length, java_int_type()); // In NO_UPDATE_IN_PLACE mode we allocate a new array and recursively // initialize its elements @@ -1198,8 +1226,7 @@ exprt object_factory( code_blockt &init_code, bool allow_null, symbol_tablet &symbol_table, - size_t max_nondet_array_length, - size_t max_nondet_tree_depth, + const object_factory_parameterst ¶meters, allocation_typet alloc_type, const source_locationt &loc, const select_pointer_typet &pointer_type_selector) @@ -1226,8 +1253,7 @@ exprt object_factory( java_object_factoryt state( symbols_created, loc, - max_nondet_array_length, - max_nondet_tree_depth, + parameters, symbol_table, pointer_type_selector); code_blockt assignments; @@ -1279,12 +1305,8 @@ exprt object_factory( /// when \p allow_null is false (as this parameter is not inherited by /// subsequent recursive calls). Has no effect when \p expr is not /// pointer-typed. -/// \param max_nondet_array_length: -/// Upper bound on size of initialized arrays. -/// \param max_nondet_tree_depth: -/// Maximum depth in the object hirearchy (counted as the number of times a -/// pointer is deferenced) created by the initialization code that will be -/// emitted here. +/// \param object_factory_parameters: +/// Parameters for the generation of non deterministic objects. /// \param pointer_type_selector: /// The pointer_selector to use to resolve pointer types where required. /// \param update_in_place: @@ -1304,8 +1326,7 @@ void gen_nondet_init( bool skip_classid, allocation_typet alloc_type, bool allow_null, - size_t max_nondet_array_length, - size_t max_nondet_tree_depth, + const object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, update_in_placet update_in_place) { @@ -1314,8 +1335,7 @@ void gen_nondet_init( java_object_factoryt state( symbols_created, loc, - max_nondet_array_length, - max_nondet_tree_depth, + object_factory_parameters, symbol_table, pointer_type_selector); code_blockt assignments; @@ -1338,13 +1358,13 @@ void gen_nondet_init( } /// Call object_factory() above with a default (identity) pointer_type_selector -exprt object_factory(const typet &type, +exprt object_factory( + const typet &type, const irep_idt base_name, code_blockt &init_code, bool allow_null, symbol_tablet &symbol_table, - size_t max_nondet_array_length, - size_t max_nondet_tree_depth, + const object_factory_parameterst &object_factory_parameters, allocation_typet alloc_type, const source_locationt &location) { @@ -1355,23 +1375,22 @@ exprt object_factory(const typet &type, init_code, allow_null, symbol_table, - max_nondet_array_length, - max_nondet_tree_depth, + object_factory_parameters, alloc_type, location, pointer_type_selector); } /// Call gen_nondet_init() above with a default (identity) pointer_type_selector -void gen_nondet_init(const exprt &expr, +void gen_nondet_init( + const exprt &expr, code_blockt &init_code, symbol_tablet &symbol_table, const source_locationt &loc, bool skip_classid, allocation_typet alloc_type, bool allow_null, - size_t max_nondet_array_length, - size_t max_nondet_tree_depth, + const object_factory_parameterst &object_factory_parameters, update_in_placet update_in_place) { select_pointer_typet pointer_type_selector; @@ -1383,8 +1402,7 @@ void gen_nondet_init(const exprt &expr, skip_classid, alloc_type, allow_null, - max_nondet_array_length, - max_nondet_tree_depth, + object_factory_parameters, pointer_type_selector, update_in_place); } diff --git a/src/java_bytecode/java_object_factory.h b/src/java_bytecode/java_object_factory.h index c08b6341877..3e1c06c52e1 100644 --- a/src/java_bytecode/java_object_factory.h +++ b/src/java_bytecode/java_object_factory.h @@ -73,6 +73,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include /// Selects the kind of allocation used by java_object_factory et al. enum class allocation_typet @@ -91,8 +92,7 @@ exprt object_factory( code_blockt &init_code, bool allow_null, symbol_tablet &symbol_table, - size_t max_nondet_array_length, - size_t max_nondet_tree_depth, + const object_factory_parameterst ¶meters, allocation_typet alloc_type, const source_locationt &location, const select_pointer_typet &pointer_type_selector); @@ -103,8 +103,7 @@ exprt object_factory( code_blockt &init_code, bool allow_null, symbol_tablet &symbol_table, - size_t max_nondet_array_length, - size_t max_nondet_tree_depth, + const object_factory_parameterst &object_factory_parameters, allocation_typet alloc_type, const source_locationt &location); @@ -123,8 +122,7 @@ void gen_nondet_init( bool skip_classid, allocation_typet alloc_type, bool allow_null, - size_t max_nondet_array_length, - size_t max_nondet_tree_depth, + const object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, update_in_placet update_in_place); @@ -136,8 +134,7 @@ void gen_nondet_init( bool skip_classid, allocation_typet alloc_type, bool allow_null, - size_t max_nondet_array_length, - size_t max_nondet_tree_depth, + const object_factory_parameterst &object_factory_parameters, update_in_placet update_in_place); exprt allocate_dynamic_object( From 621da873a8d7be3eb47a10a6251d7a6779dc18d7 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 11 Aug 2017 15:16:29 +0100 Subject: [PATCH 2/2] Tests for new option string-max-input-length --- .../max_input_length/Test.class | Bin 0 -> 644 bytes .../max_input_length/Test.java | 11 +++++++++++ .../max_input_length/test.desc | 7 +++++++ .../max_input_length/test1.desc | 7 +++++++ .../max_input_length/test2.desc | 7 +++++++ 5 files changed, 32 insertions(+) create mode 100644 regression/strings-smoke-tests/max_input_length/Test.class create mode 100644 regression/strings-smoke-tests/max_input_length/Test.java create mode 100644 regression/strings-smoke-tests/max_input_length/test.desc create mode 100644 regression/strings-smoke-tests/max_input_length/test1.desc create mode 100644 regression/strings-smoke-tests/max_input_length/test2.desc diff --git a/regression/strings-smoke-tests/max_input_length/Test.class b/regression/strings-smoke-tests/max_input_length/Test.class new file mode 100644 index 0000000000000000000000000000000000000000..d01720ffa38de67cc43d1af484757e4e9fcfda97 GIT binary patch literal 644 zcmaKqNl)8Q5Xb-HEKVE)Az=x$EMW~f5NN|vfvO^)Ql+p+K}c|OlBe*%ILLPRFu8H+ zxgaGHNbQ}^giz;MK-3<%yqV{j`OVD#`SJPwH-I8?1`^2V7>QxjfQAoo#PLyiV>-qS z=qfm2U=mp!Q-t)4<$1#OWyA4yq-RxZQ6tbPA-X9Y>3=1Jatp_V@OGmn2z@2#i2dee zMYu;QnFE)WbO?jF(z$hQ6>Q6?7s|dXo%)8V>nZzI^an`HTi1Ss0{{W?!Wqa;e64>H*qGD%3%^bc;v} z1Nk= 30) + // This should not happen when string-max-input length is smaller + // than 30 + assert false; + } +} diff --git a/regression/strings-smoke-tests/max_input_length/test.desc b/regression/strings-smoke-tests/max_input_length/test.desc new file mode 100644 index 00000000000..0fddf482a9c --- /dev/null +++ b/regression/strings-smoke-tests/max_input_length/test.desc @@ -0,0 +1,7 @@ +CORE +Test.class +--refine-strings --string-max-length 30 +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- diff --git a/regression/strings-smoke-tests/max_input_length/test1.desc b/regression/strings-smoke-tests/max_input_length/test1.desc new file mode 100644 index 00000000000..00bda639119 --- /dev/null +++ b/regression/strings-smoke-tests/max_input_length/test1.desc @@ -0,0 +1,7 @@ +CORE +Test.class +--refine-strings --string-max-length 45 --string-max-input-length 31 +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- diff --git a/regression/strings-smoke-tests/max_input_length/test2.desc b/regression/strings-smoke-tests/max_input_length/test2.desc new file mode 100644 index 00000000000..8aaaf205c92 --- /dev/null +++ b/regression/strings-smoke-tests/max_input_length/test2.desc @@ -0,0 +1,7 @@ +CORE +Test.class +--refine-strings --string-max-length 45 --string-max-input-length 20 +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +--