From e66f76f5a2d86b00dc77ec98918c147832ee7d98 Mon Sep 17 00:00:00 2001 From: svorenova Date: Wed, 25 Jul 2018 13:58:41 +0100 Subject: [PATCH 1/4] Add a check functions for (multi-dimensional) array types --- jbmc/src/java_bytecode/java_types.cpp | 19 +++++++++++++++++++ jbmc/src/java_bytecode/java_types.h | 2 ++ 2 files changed, 21 insertions(+) diff --git a/jbmc/src/java_bytecode/java_types.cpp b/jbmc/src/java_bytecode/java_types.cpp index 0203a678bb6..dd76f1a7875 100644 --- a/jbmc/src/java_bytecode/java_types.cpp +++ b/jbmc/src/java_bytecode/java_types.cpp @@ -140,6 +140,25 @@ typet &java_array_element_type(symbol_typet &array_symbol) return array_symbol.add_type(ID_C_element_type); } +/// Checks whether the given type is an array pointer type +bool is_java_array_type(const typet &type) +{ + if(!(type.id() == ID_pointer && type.subtype().id() == ID_symbol)) + return false; + const auto &subtype_symbol = to_symbol_type(type.subtype()); + return is_java_array_tag(subtype_symbol.get_identifier()); +} + +/// Checks whether the given type is a multi-dimensional array pointer type, +// i.e., a pointer to an array type with element type also being a pointer to an +/// array type. +bool is_multidim_java_array_type(const typet &type) +{ + return is_java_array_type(type) && + is_java_array_type( + java_array_element_type(to_symbol_type(type.subtype()))); +} + /// See above /// \par parameters: Struct tag 'tag' /// \return True if the given struct is a Java array diff --git a/jbmc/src/java_bytecode/java_types.h b/jbmc/src/java_bytecode/java_types.h index 6eb93456a99..c205537818e 100644 --- a/jbmc/src/java_bytecode/java_types.h +++ b/jbmc/src/java_bytecode/java_types.h @@ -247,6 +247,8 @@ symbol_typet java_classname(const std::string &); reference_typet java_array_type(const char subtype); const typet &java_array_element_type(const symbol_typet &array_symbol); typet &java_array_element_type(symbol_typet &array_symbol); +bool is_java_array_type(const typet &type); +bool is_multidim_java_array_type(const typet &type); bool is_reference_type(char t); From b72b968a2e7c39e221fca4334a07999a762094c1 Mon Sep 17 00:00:00 2001 From: svorenova Date: Wed, 25 Jul 2018 15:34:46 +0100 Subject: [PATCH 2/4] Remove unused function --- jbmc/src/java_bytecode/java_types.cpp | 5 ----- jbmc/src/java_bytecode/java_types.h | 2 -- 2 files changed, 7 deletions(-) diff --git a/jbmc/src/java_bytecode/java_types.cpp b/jbmc/src/java_bytecode/java_types.cpp index dd76f1a7875..976107fc691 100644 --- a/jbmc/src/java_bytecode/java_types.cpp +++ b/jbmc/src/java_bytecode/java_types.cpp @@ -167,11 +167,6 @@ bool is_java_array_tag(const irep_idt& tag) return has_prefix(id2string(tag), "java::array["); } -bool is_reference_type(const char t) -{ - return 'a'==t; -} - typet java_type_from_char(char t) { switch(t) diff --git a/jbmc/src/java_bytecode/java_types.h b/jbmc/src/java_bytecode/java_types.h index c205537818e..2cdfe84c575 100644 --- a/jbmc/src/java_bytecode/java_types.h +++ b/jbmc/src/java_bytecode/java_types.h @@ -250,8 +250,6 @@ typet &java_array_element_type(symbol_typet &array_symbol); bool is_java_array_type(const typet &type); bool is_multidim_java_array_type(const typet &type); -bool is_reference_type(char t); - // i integer // l long // s short From a1ab7a6071dc0a0db61248ca093b79b1ed888886 Mon Sep 17 00:00:00 2001 From: svorenova Date: Wed, 25 Jul 2018 15:38:50 +0100 Subject: [PATCH 3/4] Improve documentation for java array types --- jbmc/src/java_bytecode/java_types.cpp | 19 +++++++++++++++++-- jbmc/src/java_bytecode/java_types.h | 10 ---------- 2 files changed, 17 insertions(+), 12 deletions(-) diff --git a/jbmc/src/java_bytecode/java_types.cpp b/jbmc/src/java_bytecode/java_types.cpp index 976107fc691..1cc5d13964a 100644 --- a/jbmc/src/java_bytecode/java_types.cpp +++ b/jbmc/src/java_bytecode/java_types.cpp @@ -87,6 +87,10 @@ reference_typet java_lang_object_type() return java_reference_type(symbol_typet("java::java.lang.Object")); } +/// Construct an array pointer type. It is a pointer to a symbol with identifier +/// java::array[]. Its ID_C_element_type is set to the corresponding primitive +/// type, or void* for arrays of references. +/// \param subtype Character indicating the type of array reference_typet java_array_type(const char subtype) { std::string subtype_str; @@ -160,13 +164,24 @@ bool is_multidim_java_array_type(const typet &type) } /// See above -/// \par parameters: Struct tag 'tag' -/// \return True if the given struct is a Java array +/// \param tag Tag of a struct +/// \return True if the given string is a Java array tag, i.e., has a prefix +/// of java::array[ bool is_java_array_tag(const irep_idt& tag) { return has_prefix(id2string(tag), "java::array["); } +/// Constructs a type indicated by the given character: +/// - i integer +/// - l long +/// - s short +/// - b byte +/// - c character +/// - f float +/// - d double +/// - z boolean +/// - a reference typet java_type_from_char(char t) { switch(t) diff --git a/jbmc/src/java_bytecode/java_types.h b/jbmc/src/java_bytecode/java_types.h index 2cdfe84c575..fa696ed49e3 100644 --- a/jbmc/src/java_bytecode/java_types.h +++ b/jbmc/src/java_bytecode/java_types.h @@ -250,16 +250,6 @@ typet &java_array_element_type(symbol_typet &array_symbol); bool is_java_array_type(const typet &type); bool is_multidim_java_array_type(const typet &type); -// i integer -// l long -// s short -// b byte -// c character -// f float -// d double -// z boolean -// a reference - typet java_type_from_char(char t); typet java_type_from_string( const std::string &, From c57286633b9a398c9ab414df806b63fc4b105cb5 Mon Sep 17 00:00:00 2001 From: svorenova Date: Wed, 25 Jul 2018 15:45:07 +0100 Subject: [PATCH 4/4] Use can_cast_type instead of raw type id check --- jbmc/src/java_bytecode/java_types.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/jbmc/src/java_bytecode/java_types.cpp b/jbmc/src/java_bytecode/java_types.cpp index 1cc5d13964a..ef8a36b9a4e 100644 --- a/jbmc/src/java_bytecode/java_types.cpp +++ b/jbmc/src/java_bytecode/java_types.cpp @@ -147,8 +147,12 @@ typet &java_array_element_type(symbol_typet &array_symbol) /// Checks whether the given type is an array pointer type bool is_java_array_type(const typet &type) { - if(!(type.id() == ID_pointer && type.subtype().id() == ID_symbol)) + if( + !can_cast_type(type) || + !can_cast_type(type.subtype())) + { return false; + } const auto &subtype_symbol = to_symbol_type(type.subtype()); return is_java_array_tag(subtype_symbol.get_identifier()); }