From e3b44c7009d19d3b8e5da235881a2d4668799fd2 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 31 May 2017 17:46:57 +0100 Subject: [PATCH 1/2] Avoid copies of string preprocess objects Only one instance of this class should exist for a program. --- src/java_bytecode/java_bytecode_convert_class.cpp | 6 +++--- src/java_bytecode/java_bytecode_convert_class.h | 2 +- src/java_bytecode/java_bytecode_convert_method.cpp | 2 +- src/java_bytecode/java_bytecode_convert_method.h | 4 ++-- src/java_bytecode/java_bytecode_convert_method_class.h | 4 ++-- src/java_bytecode/java_string_library_preprocess.h | 3 +++ 6 files changed, 12 insertions(+), 9 deletions(-) diff --git a/src/java_bytecode/java_bytecode_convert_class.cpp b/src/java_bytecode/java_bytecode_convert_class.cpp index 29be4f70617..b16e3a74f87 100644 --- a/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/src/java_bytecode/java_bytecode_convert_class.cpp @@ -31,7 +31,7 @@ class java_bytecode_convert_classt:public messaget size_t _max_array_length, lazy_methodst& _lazy_methods, lazy_methods_modet _lazy_methods_mode, - const java_string_library_preprocesst &_string_preprocess): + java_string_library_preprocesst &_string_preprocess): messaget(_message_handler), symbol_table(_symbol_table), max_array_length(_max_array_length), @@ -63,7 +63,7 @@ class java_bytecode_convert_classt:public messaget const size_t max_array_length; lazy_methodst &lazy_methods; lazy_methods_modet lazy_methods_mode; - java_string_library_preprocesst string_preprocess; + java_string_library_preprocesst &string_preprocess; // conversion void convert(const classt &c); @@ -477,7 +477,7 @@ bool java_bytecode_convert_class( size_t max_array_length, lazy_methodst &lazy_methods, lazy_methods_modet lazy_methods_mode, - const java_string_library_preprocesst &string_preprocess) + java_string_library_preprocesst &string_preprocess) { java_bytecode_convert_classt java_bytecode_convert_class( symbol_table, diff --git a/src/java_bytecode/java_bytecode_convert_class.h b/src/java_bytecode/java_bytecode_convert_class.h index 3bf4e59c85f..b3b71426b1d 100644 --- a/src/java_bytecode/java_bytecode_convert_class.h +++ b/src/java_bytecode/java_bytecode_convert_class.h @@ -22,6 +22,6 @@ bool java_bytecode_convert_class( size_t max_array_length, lazy_methodst &, lazy_methods_modet, - const java_string_library_preprocesst &string_preprocess); + java_string_library_preprocesst &string_preprocess); #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_CLASS_H diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index 63cfb1a9cd5..e72ed43078a 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -2777,7 +2777,7 @@ void java_bytecode_convert_method( message_handlert &message_handler, size_t max_array_length, safe_pointer lazy_methods, - const java_string_library_preprocesst &string_preprocess) + java_string_library_preprocesst &string_preprocess) { static const std::unordered_set methods_to_ignore { diff --git a/src/java_bytecode/java_bytecode_convert_method.h b/src/java_bytecode/java_bytecode_convert_method.h index 78dd9226f76..43c1cdec380 100644 --- a/src/java_bytecode/java_bytecode_convert_method.h +++ b/src/java_bytecode/java_bytecode_convert_method.h @@ -26,7 +26,7 @@ void java_bytecode_convert_method( message_handlert &message_handler, size_t max_array_length, safe_pointer lazy_methods, - const java_string_library_preprocesst &string_preprocess); + java_string_library_preprocesst &string_preprocess); inline void java_bytecode_convert_method( const symbolt &class_symbol, @@ -34,7 +34,7 @@ inline void java_bytecode_convert_method( symbol_tablet &symbol_table, message_handlert &message_handler, size_t max_array_length, - const java_string_library_preprocesst &string_preprocess) + java_string_library_preprocesst &string_preprocess) { java_bytecode_convert_method( class_symbol, diff --git a/src/java_bytecode/java_bytecode_convert_method_class.h b/src/java_bytecode/java_bytecode_convert_method_class.h index cf3c66b8661..67cc175c184 100644 --- a/src/java_bytecode/java_bytecode_convert_method_class.h +++ b/src/java_bytecode/java_bytecode_convert_method_class.h @@ -33,7 +33,7 @@ class java_bytecode_convert_methodt:public messaget message_handlert &_message_handler, size_t _max_array_length, safe_pointer _lazy_methods, - const java_string_library_preprocesst &_string_preprocess): + java_string_library_preprocesst &_string_preprocess): messaget(_message_handler), symbol_table(_symbol_table), max_array_length(_max_array_length), @@ -61,7 +61,7 @@ class java_bytecode_convert_methodt:public messaget irep_idt method_id; irep_idt current_method; typet method_return_type; - java_string_library_preprocesst string_preprocess; + java_string_library_preprocesst &string_preprocess; public: struct holet diff --git a/src/java_bytecode/java_string_library_preprocess.h b/src/java_bytecode/java_string_library_preprocess.h index beeed0145ff..6c0ad1a5da8 100644 --- a/src/java_bytecode/java_string_library_preprocess.h +++ b/src/java_bytecode/java_string_library_preprocess.h @@ -47,6 +47,9 @@ class java_string_library_preprocesst:public messaget bool is_known_string_type(irep_idt class_name); private: + // We forbid copies of the object by making the copy operator private. + java_string_library_preprocesst(const java_string_library_preprocesst &); + static bool java_type_matches_tag(const typet &type, const std::string &tag); static bool is_java_string_pointer_type(const typet &type); static bool is_java_string_type(const typet &type); From 0cc5ae662e2a4394bc71d771ea31c3e7bd4e3fe4 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 5 Jun 2017 11:59:21 +0100 Subject: [PATCH 2/2] Using delete to forbid copies of objects --- src/java_bytecode/java_string_library_preprocess.h | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/java_bytecode/java_string_library_preprocess.h b/src/java_bytecode/java_string_library_preprocess.h index 6c0ad1a5da8..f9bfb8cffc6 100644 --- a/src/java_bytecode/java_string_library_preprocess.h +++ b/src/java_bytecode/java_string_library_preprocess.h @@ -47,8 +47,9 @@ class java_string_library_preprocesst:public messaget bool is_known_string_type(irep_idt class_name); private: - // We forbid copies of the object by making the copy operator private. - java_string_library_preprocesst(const java_string_library_preprocesst &); + // We forbid copies of the object + java_string_library_preprocesst( + const java_string_library_preprocesst &)=delete; static bool java_type_matches_tag(const typet &type, const std::string &tag); static bool is_java_string_pointer_type(const typet &type);