From ce1f4d2147b7d86c5cee6bad6804d0e69864d7f2 Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Fri, 2 Feb 2018 12:19:21 +0000 Subject: [PATCH 1/7] Add annotations to java_class_typet, its methods and fields Add the annotations parsed from the byte code to classes/fields/methods and static fields (globals) in the symbol table --- .../java_bytecode_convert_class.cpp | 46 +++++++++++- .../java_bytecode_convert_class.h | 4 + .../java_bytecode_convert_method.cpp | 9 +++ src/java_bytecode/java_types.h | 75 +++++++++++++++++++ src/util/irep_ids.def | 1 + 5 files changed, 134 insertions(+), 1 deletion(-) diff --git a/src/java_bytecode/java_bytecode_convert_class.cpp b/src/java_bytecode/java_bytecode_convert_class.cpp index 33912bd85b7..f4a237be8c9 100644 --- a/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/src/java_bytecode/java_bytecode_convert_class.cpp @@ -103,6 +103,7 @@ class java_bytecode_convert_classt:public messaget typedef java_bytecode_parse_treet::classt classt; typedef java_bytecode_parse_treet::fieldt fieldt; typedef java_bytecode_parse_treet::methodt methodt; + typedef java_bytecode_parse_treet::annotationt annotationt; private: symbol_tablet &symbol_table; @@ -372,6 +373,10 @@ void java_bytecode_convert_classt::convert( "java::" + id2string(lambda_entry.second.lambda_method_ref)); } + // Load annotations + if(!c.annotations.empty()) + convert_annotations(c.annotations, class_type.get_annotations()); + // produce class symbol symbolt new_symbol; new_symbol.base_name=c.name; @@ -638,6 +643,14 @@ void java_bytecode_convert_classt::convert( ns, get_message_handler()); + // Load annotations + if(!f.annotations.empty()) + { + convert_annotations( + f.annotations, + static_cast(new_symbol.type).get_annotations()); + } + // Do we have the static field symbol already? const auto s_it=symbol_table.symbols.find(new_symbol.name); if(s_it!=symbol_table.symbols.end()) @@ -650,7 +663,7 @@ void java_bytecode_convert_classt::convert( { class_typet &class_type=to_class_type(class_symbol.type); - class_type.components().push_back(class_typet::componentt()); + class_type.components().emplace_back(); class_typet::componentt &component=class_type.components().back(); component.set_name(f.name); @@ -666,6 +679,14 @@ void java_bytecode_convert_classt::convert( component.set_access(ID_public); else component.set_access(ID_default); + + // Load annotations + if(!f.annotations.empty()) + { + convert_annotations( + f.annotations, + static_cast(component.type()).get_annotations()); + } } } @@ -979,6 +1000,29 @@ static void find_and_replace_parameters( } } +/// Convert parsed annotations into the symbol table +/// \param parsed_annotations: The parsed annotations to convert +/// \param annotations: The java_annotationt collection to populate +void convert_annotations( + const java_bytecode_parse_treet::annotationst &parsed_annotations, + std::vector &annotations) +{ + for(const auto &annotation : parsed_annotations) + { + annotations.emplace_back(annotation.type); + std::vector &values = + annotations.back().get_values(); + std::transform( + annotation.element_value_pairs.begin(), + annotation.element_value_pairs.end(), + std::back_inserter(values), + [](const decltype(annotation.element_value_pairs)::value_type &value) + { + return java_annotationt::valuet(value.element_name, value.value); + }); + } +} + /// Checks if the class is implicitly generic, i.e., it is an inner class of /// any generic class. All uses of the implicit generic type parameters within /// the inner class are updated to point to the type parameters of the diff --git a/src/java_bytecode/java_bytecode_convert_class.h b/src/java_bytecode/java_bytecode_convert_class.h index 5cb021f946a..3693290491f 100644 --- a/src/java_bytecode/java_bytecode_convert_class.h +++ b/src/java_bytecode/java_bytecode_convert_class.h @@ -29,6 +29,10 @@ bool java_bytecode_convert_class( java_string_library_preprocesst &string_preprocess, const std::unordered_set &no_load_classes); +void convert_annotations( + const java_bytecode_parse_treet::annotationst &parsed_annotations, + std::vector &annotations); + void mark_java_implicitly_generic_class_type( const irep_idt &class_name, symbol_tablet &symbol_table); diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index f1e5b8f51a3..7bf488ecc43 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -387,6 +387,15 @@ void java_bytecode_convert_method_lazy( parameters.insert(parameters.begin(), this_p); } + // Load annotations + if(!m.annotations.empty()) + { + convert_annotations( + m.annotations, + static_cast(static_cast(member_type)) + .get_annotations()); + } + method_symbol.type=member_type; symbol_table.add(method_symbol); } diff --git a/src/java_bytecode/java_types.h b/src/java_bytecode/java_types.h index 56c7e14efe3..659ce06e165 100644 --- a/src/java_bytecode/java_types.h +++ b/src/java_bytecode/java_types.h @@ -19,6 +19,69 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +class java_annotationt : public irept +{ +public: + class valuet : public irept + { + public: + valuet(irep_idt name, const exprt &value) : irept(name) + { + get_sub().push_back(value); + } + + const irep_idt &get_name() const + { + return id(); + } + + const exprt &get_value() const + { + return static_cast(get_sub().front()); + } + }; + + explicit java_annotationt(const typet &type) + { + set(ID_type, type); + } + + const typet &get_type() const + { + return static_cast(find(ID_type)); + } + + const std::vector &get_values() const + { + // This cast should be safe as valuet doesn't add data to irept + return reinterpret_cast &>(get_sub()); + } + + std::vector &get_values() + { + // This cast should be safe as valuet doesn't add data to irept + return reinterpret_cast &>(get_sub()); + } +}; + +class annotated_typet : public typet +{ +public: + const std::vector &get_annotations() const + { + // This cast should be safe as java_annotationt doesn't add data to irept + return reinterpret_cast &>( + find(ID_annotations).get_sub()); + } + + std::vector &get_annotations() + { + // This cast should be safe as java_annotationt doesn't add data to irept + return reinterpret_cast &>( + add(ID_annotations).get_sub()); + } +}; + class java_class_typet:public class_typet { public: @@ -57,6 +120,18 @@ class java_class_typet:public class_typet // creates empty symbol_exprt and pushes it in the vector lambda_method_handles().emplace_back(); } + + const std::vector &get_annotations() const + { + return static_cast( + static_cast(*this)).get_annotations(); + } + + std::vector &get_annotations() + { + return static_cast( + static_cast(*this)).get_annotations(); + } }; inline const java_class_typet &to_java_class_type(const typet &type) diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index 33b961653b8..1ed93c0b2a0 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -844,6 +844,7 @@ IREP_ID_TWO(overflow_shl, overflow-shl) IREP_ID_TWO(C_no_initialization_required, #no_initialization_required) IREP_ID_TWO(overlay_class, java::com.diffblue.OverlayClassImplementation) IREP_ID_TWO(overlay_method, java::com.diffblue.OverlayMethodImplementation) +IREP_ID_ONE(annotations) #undef IREP_ID_ONE #undef IREP_ID_TWO From 3ac6d1710087c8a2c0a5c2902d958cecfe0982a8 Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Tue, 27 Feb 2018 15:21:42 +0000 Subject: [PATCH 2/7] Add type_dynamic_cast and friends for java_class_typet Add type_dynamic_cast and friends for struct_typet, class_typet and java_class_typet --- src/java_bytecode/java_types.h | 6 ++++++ src/util/std_types.h | 12 ++++++++++++ 2 files changed, 18 insertions(+) diff --git a/src/java_bytecode/java_types.h b/src/java_bytecode/java_types.h index 659ce06e165..fcf8048635b 100644 --- a/src/java_bytecode/java_types.h +++ b/src/java_bytecode/java_types.h @@ -146,6 +146,12 @@ inline java_class_typet &to_java_class_type(typet &type) return static_cast(type); } +template <> +inline bool can_cast_type(const typet &type) +{ + return can_cast_type(type); +} + typet java_int_type(); typet java_long_type(); typet java_short_type(); diff --git a/src/util/std_types.h b/src/util/std_types.h index ae323dff374..f7e6189245f 100644 --- a/src/util/std_types.h +++ b/src/util/std_types.h @@ -328,6 +328,12 @@ inline struct_typet &to_struct_type(typet &type) return static_cast(type); } +template <> +inline bool can_cast_type(const typet &type) +{ + return type.id() == ID_struct; +} + /*! \brief C++ class type */ class class_typet:public struct_typet @@ -432,6 +438,12 @@ inline class_typet &to_class_type(typet &type) return static_cast(type); } +template <> +inline bool can_cast_type(const typet &type) +{ + return can_cast_type(type) && type.get_bool(ID_C_class); +} + /*! \brief The union type */ class union_typet:public struct_union_typet From e22b95b17eb1761feb92b482ff2e1bfeb4e8b5cc Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Mon, 12 Mar 2018 17:33:26 +0000 Subject: [PATCH 3/7] Fix spurious virtual function related keywords Remove virtual keyword from methods that are specific to this class Add comment on method that hides a non-virtual base method and remove virtual keyword from it Mark overrides with override --- src/java_bytecode/expr2java.h | 31 ++++++++++++++----------------- 1 file changed, 14 insertions(+), 17 deletions(-) diff --git a/src/java_bytecode/expr2java.h b/src/java_bytecode/expr2java.h index a0c9b828e6c..795d488a72b 100644 --- a/src/java_bytecode/expr2java.h +++ b/src/java_bytecode/expr2java.h @@ -20,30 +20,27 @@ class expr2javat:public expr2ct { public: explicit expr2javat(const namespacet &_ns):expr2ct(_ns) { } + protected: virtual std::string convert_with_precedence( - const exprt &src, unsigned &precedence); - virtual std::string convert_java_this(const exprt &src, unsigned precedence); - virtual std::string convert_java_instanceof( - const exprt &src, - unsigned precedence); - virtual std::string convert_java_new(const exprt &src, unsigned precedence); - virtual std::string convert_code_java_delete( - const exprt &src, - unsigned precedence); - virtual std::string convert_struct(const exprt &src, unsigned &precedence); - virtual std::string convert_code(const codet &src, unsigned indent); + const exprt &src, unsigned &precedence) override; + std::string convert_java_this(const exprt &src, unsigned precedence); + std::string convert_java_instanceof(const exprt &src, unsigned precedence); + std::string convert_java_new(const exprt &src, unsigned precedence); + std::string convert_code_java_delete(const exprt &src, unsigned precedence); + virtual std::string convert_struct( + const exprt &src, unsigned &precedence) override; + virtual std::string convert_code(const codet &src, unsigned indent) override; virtual std::string convert_constant( - const constant_exprt &src, - unsigned &precedence); - virtual std::string convert_code_function_call( - const code_function_callt &src, - unsigned indent); + const constant_exprt &src, unsigned &precedence) override; + // Hides base class version + std::string convert_code_function_call( + const code_function_callt &src, unsigned indent); virtual std::string convert_rec( const typet &src, const c_qualifierst &qualifiers, - const std::string &declarator); + const std::string &declarator) override; // length of string representation of Java Char // representation is '\u0000' From e6fb3bf8a31b94cbb2afdfe5b37420904f3155ea Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Tue, 27 Feb 2018 15:23:51 +0000 Subject: [PATCH 4/7] Pretty printing of java_class_typet Added java_qualifierst that adds annotations as qualifiers to types --- src/ansi-c/c_qualifiers.cpp | 21 ++++ src/ansi-c/c_qualifiers.h | 23 ++-- src/ansi-c/expr2c.cpp | 3 +- src/cpp/expr2cpp.cpp | 3 +- src/java_bytecode/Makefile | 1 + src/java_bytecode/expr2java.cpp | 17 ++- src/java_bytecode/expr2java.h | 2 + src/java_bytecode/java_qualifiers.cpp | 146 ++++++++++++++++++++++++++ src/java_bytecode/java_qualifiers.h | 47 +++++++++ 9 files changed, 250 insertions(+), 13 deletions(-) create mode 100644 src/java_bytecode/java_qualifiers.cpp create mode 100644 src/java_bytecode/java_qualifiers.h diff --git a/src/ansi-c/c_qualifiers.cpp b/src/ansi-c/c_qualifiers.cpp index 0802d144391..6820b749f09 100644 --- a/src/ansi-c/c_qualifiers.cpp +++ b/src/ansi-c/c_qualifiers.cpp @@ -9,6 +9,27 @@ Author: Daniel Kroening, kroening@kroening.com #include "c_qualifiers.h" #include +#include + +c_qualifierst &c_qualifierst::operator=(const c_qualifierst &other) +{ + is_constant = other.is_constant; + is_volatile = other.is_volatile; + is_restricted = other.is_restricted; + is_atomic = other.is_atomic; + is_noreturn = other.is_noreturn; + is_ptr32 = other.is_ptr32; + is_ptr64 = other.is_ptr64; + is_transparent_union = other.is_transparent_union; + return *this; +} + +std::unique_ptr c_qualifierst::clone() const +{ + auto other = util_make_unique(); + *other = *this; + return other; +} std::string c_qualifierst::as_string() const { diff --git a/src/ansi-c/c_qualifiers.h b/src/ansi-c/c_qualifiers.h index 2e9948e31e9..5be174d3b98 100644 --- a/src/ansi-c/c_qualifiers.h +++ b/src/ansi-c/c_qualifiers.h @@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_ANSI_C_C_QUALIFIERS_H #include +#include #include @@ -28,7 +29,13 @@ class c_qualifierst read(src); } - void clear() + c_qualifierst(const c_qualifierst &other) = delete; + virtual c_qualifierst &operator=(const c_qualifierst &other); + virtual std::unique_ptr clone() const; + + virtual ~c_qualifierst() = default; + + virtual void clear() { is_constant=false; is_volatile=false; @@ -50,13 +57,13 @@ class c_qualifierst // will likely add alignment here as well - std::string as_string() const; - void read(const typet &src); - void write(typet &src) const; + virtual std::string as_string() const; + virtual void read(const typet &src); + virtual void write(typet &src) const; static void clear(typet &dest); - bool is_subset_of(const c_qualifierst &q) const + virtual bool is_subset_of(const c_qualifierst &q) const { return (!is_constant || q.is_constant) && (!is_volatile || q.is_volatile) && @@ -69,7 +76,7 @@ class c_qualifierst // is_transparent_union isn't checked } - bool operator==(const c_qualifierst &other) const + virtual bool operator==(const c_qualifierst &other) const { return is_constant==other.is_constant && is_volatile==other.is_volatile && @@ -86,7 +93,7 @@ class c_qualifierst return !(*this==other); } - c_qualifierst &operator+=(const c_qualifierst &b) + virtual c_qualifierst &operator+=(const c_qualifierst &b) { is_constant|=b.is_constant; is_volatile|=b.is_volatile; @@ -99,7 +106,7 @@ class c_qualifierst return *this; } - unsigned count() const + virtual std::size_t count() const { return is_constant+is_volatile+is_restricted+is_atomic+ is_ptr32+is_ptr64+is_noreturn; diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index a0b79883fad..24c7b89aded 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -165,7 +165,8 @@ std::string expr2ct::convert_rec( const c_qualifierst &qualifiers, const std::string &declarator) { - c_qualifierst new_qualifiers(qualifiers); + std::unique_ptr clone = qualifiers.clone(); + c_qualifierst &new_qualifiers = *clone; new_qualifiers.read(src); std::string q=new_qualifiers.as_string(); diff --git a/src/cpp/expr2cpp.cpp b/src/cpp/expr2cpp.cpp index 7327811ac5c..3d7daacb08a 100644 --- a/src/cpp/expr2cpp.cpp +++ b/src/cpp/expr2cpp.cpp @@ -132,7 +132,8 @@ std::string expr2cppt::convert_rec( const c_qualifierst &qualifiers, const std::string &declarator) { - c_qualifierst new_qualifiers(qualifiers); + std::unique_ptr clone = qualifiers.clone(); + c_qualifierst &new_qualifiers = *clone; new_qualifiers.read(src); const std::string d= diff --git a/src/java_bytecode/Makefile b/src/java_bytecode/Makefile index b9371e734f1..f42ce024d7f 100644 --- a/src/java_bytecode/Makefile +++ b/src/java_bytecode/Makefile @@ -23,6 +23,7 @@ SRC = bytecode_info.cpp \ java_local_variable_table.cpp \ java_object_factory.cpp \ java_pointer_casts.cpp \ + java_qualifiers.cpp \ java_root_class.cpp \ java_static_initializers.cpp \ java_string_library_preprocess.cpp \ diff --git a/src/java_bytecode/expr2java.cpp b/src/java_bytecode/expr2java.cpp index cf6bb8a897a..6e4a9d932c5 100644 --- a/src/java_bytecode/expr2java.cpp +++ b/src/java_bytecode/expr2java.cpp @@ -19,12 +19,22 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include -#include #include #include +#include "java_qualifiers.h" #include "java_types.h" +std::string expr2javat::convert(const typet &src) +{ + return convert_rec(src, java_qualifierst(ns), ""); +} + +std::string expr2javat::convert(const exprt &src) +{ + return expr2ct::convert(src); +} + std::string expr2javat::convert_code_function_call( const code_function_callt &src, unsigned indent) @@ -244,7 +254,8 @@ std::string expr2javat::convert_rec( const c_qualifierst &qualifiers, const std::string &declarator) { - c_qualifierst new_qualifiers(qualifiers); + std::unique_ptr clone = qualifiers.clone(); + c_qualifierst &new_qualifiers = *clone; new_qualifiers.read(src); const std::string d= @@ -307,7 +318,7 @@ std::string expr2javat::convert_rec( const typet &return_type=code_type.return_type(); dest+=" -> "+convert(return_type); - return dest; + return q + dest; } else return expr2ct::convert_rec(src, qualifiers, declarator); diff --git a/src/java_bytecode/expr2java.h b/src/java_bytecode/expr2java.h index 795d488a72b..ff2975d40c4 100644 --- a/src/java_bytecode/expr2java.h +++ b/src/java_bytecode/expr2java.h @@ -20,6 +20,8 @@ class expr2javat:public expr2ct { public: explicit expr2javat(const namespacet &_ns):expr2ct(_ns) { } + virtual std::string convert(const typet &src) override; + virtual std::string convert(const exprt &src) override; protected: virtual std::string convert_with_precedence( diff --git a/src/java_bytecode/java_qualifiers.cpp b/src/java_bytecode/java_qualifiers.cpp new file mode 100644 index 00000000000..9fd67220d95 --- /dev/null +++ b/src/java_bytecode/java_qualifiers.cpp @@ -0,0 +1,146 @@ +// Author: Diffblue Ltd. + +/// \file +/// Java-specific type qualifiers + +#include "java_qualifiers.h" +#include +#include +#include "expr2java.h" + + +java_qualifierst &java_qualifierst::operator=(const java_qualifierst &other) +{ + INVARIANT( + &other.ns == &ns, + "Can only assign from a java_qualifierst using the same namespace"); + annotations = other.annotations; + c_qualifierst::operator=(other); + return *this; +} + +java_qualifierst &java_qualifierst::operator=(java_qualifierst &&other) +{ + INVARIANT( + &other.ns == &ns, + "Can only assign from a java_qualifierst using the same namespace"); + annotations = std::move(other.annotations); + c_qualifierst::operator=(other); + return *this; +} + +c_qualifierst &java_qualifierst::operator=(const c_qualifierst &c_other) +{ + auto other = dynamic_cast(&c_other); + if(other != nullptr) + *this = *other; + else + { + annotations.clear(); + c_qualifierst::operator=(c_other); + } + return *this; +} + +std::unique_ptr java_qualifierst::clone() const +{ + auto other = util_make_unique(ns); + *other = *this; + return std::move(other); +} + +std::size_t java_qualifierst::count() const +{ + return c_qualifierst::count() + annotations.size(); +} + +void java_qualifierst::clear() +{ + c_qualifierst::clear(); + annotations.clear(); +} + +void java_qualifierst::read(const typet &src) +{ + c_qualifierst::read(src); + auto &annotated_type = static_cast(src); + annotations = annotated_type.get_annotations(); +} + +void java_qualifierst::write(typet &src) const +{ + c_qualifierst::write(src); + auto &annotated_type = static_cast(src); + annotated_type.get_annotations() = annotations; +} + +c_qualifierst &java_qualifierst::operator+=(const c_qualifierst &c_other) +{ + c_qualifierst::operator+=(c_other); + auto other = dynamic_cast(&c_other); + if(other != nullptr) + { + std::copy( + other->annotations.begin(), + other->annotations.end(), + std::back_inserter(annotations)); + } + return *this; +} + +bool java_qualifierst::operator==(const c_qualifierst &c_other) const +{ + auto other = dynamic_cast(&c_other); + if(other == nullptr) + return false; + return + c_qualifierst::operator==(c_other) && annotations == other->annotations; +} + +bool java_qualifierst::is_subset_of(const c_qualifierst &c_other) const +{ + if(!c_qualifierst::is_subset_of(c_other)) + return false; + auto other = dynamic_cast(&c_other); + if(other == nullptr) + return annotations.empty(); + auto &other_a = other->annotations; + for(const auto &annotation : annotations) + { + if(std::find(other_a.begin(), other_a.end(), annotation) == other_a.end()) + return false; + } + return true; +} + +std::string java_qualifierst::as_string() const +{ + std::stringstream out; + for(const java_annotationt &annotation : annotations) + { + out << '@'; + out << annotation.get_type().subtype().get(ID_identifier); + + if(!annotation.get_values().empty()) + { + out << '('; + + bool first = true; + for(const java_annotationt::valuet &value : annotation.get_values()) + { + if(first) + first = false; + else + out << ", "; + + out << '"' << value.get_name() << '"' << '='; + out << expr2java(value.get_value(), ns); + } + + out << ')'; + } + out << ' '; + } + out << c_qualifierst::as_string(); + return out.str(); +} diff --git a/src/java_bytecode/java_qualifiers.h b/src/java_bytecode/java_qualifiers.h new file mode 100644 index 00000000000..cd9862a868a --- /dev/null +++ b/src/java_bytecode/java_qualifiers.h @@ -0,0 +1,47 @@ +// Author: Diffblue Ltd. + +/// \file +/// Java-specific type qualifiers + +#ifndef CPROVER_JAVA_BYTECODE_JAVA_QUALIFIERS_H +#define CPROVER_JAVA_BYTECODE_JAVA_QUALIFIERS_H + +#include "java_types.h" +#include + +class java_qualifierst : public c_qualifierst +{ +private: + const namespacet &ns; + std::vector annotations; + +public: + explicit java_qualifierst(const namespacet &ns) + : ns(ns) + {} + + java_qualifierst &operator=(const java_qualifierst &other); + java_qualifierst &operator=(java_qualifierst &&other); + virtual c_qualifierst &operator=(const c_qualifierst &other) override; + virtual std::unique_ptr clone() const override; + + virtual c_qualifierst &operator+=(const c_qualifierst &other) override; + + const std::vector &get_annotations() const + { + return annotations; + } + virtual std::size_t count() const override; + + virtual void clear() override; + + virtual void read(const typet &src) override; + virtual void write(typet &src) const override; + + virtual bool is_subset_of(const c_qualifierst &other) const override; + virtual bool operator==(const c_qualifierst &other) const override; + + virtual std::string as_string() const override; +}; + +#endif // CPROVER_JAVA_BYTECODE_JAVA_QUALIFIERS_H From b06a27de119c49539b55c922fe06871279f83c3f Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Fri, 23 Mar 2018 16:18:11 +0000 Subject: [PATCH 5/7] Introduce abstract qualifierst base class --- src/ansi-c/c_qualifiers.cpp | 10 +- src/ansi-c/c_qualifiers.h | 127 +++++++++++++++++--------- src/ansi-c/expr2c.cpp | 10 +- src/ansi-c/expr2c_class.h | 8 +- src/cpp/expr2cpp.cpp | 8 +- src/java_bytecode/expr2java.cpp | 6 +- src/java_bytecode/expr2java.h | 2 +- src/java_bytecode/java_qualifiers.cpp | 56 ++++-------- src/java_bytecode/java_qualifiers.h | 12 +-- 9 files changed, 126 insertions(+), 113 deletions(-) diff --git a/src/ansi-c/c_qualifiers.cpp b/src/ansi-c/c_qualifiers.cpp index 6820b749f09..c574cf15b49 100644 --- a/src/ansi-c/c_qualifiers.cpp +++ b/src/ansi-c/c_qualifiers.cpp @@ -24,11 +24,11 @@ c_qualifierst &c_qualifierst::operator=(const c_qualifierst &other) return *this; } -std::unique_ptr c_qualifierst::clone() const +std::unique_ptr c_qualifierst::clone() const { auto other = util_make_unique(); *other = *this; - return other; + return std::move(other); } std::string c_qualifierst::as_string() const @@ -141,9 +141,7 @@ void c_qualifierst::clear(typet &dest) } /// pretty-print the qualifiers -std::ostream &operator << ( - std::ostream &out, - const c_qualifierst &c_qualifiers) +std::ostream &operator<<(std::ostream &out, const qualifierst &qualifiers) { - return out << c_qualifiers.as_string(); + return out << qualifiers.as_string(); } diff --git a/src/ansi-c/c_qualifiers.h b/src/ansi-c/c_qualifiers.h index 5be174d3b98..934845ae8bb 100644 --- a/src/ansi-c/c_qualifiers.h +++ b/src/ansi-c/c_qualifiers.h @@ -15,7 +15,49 @@ Author: Daniel Kroening, kroening@kroening.com #include -class c_qualifierst +class qualifierst +{ +protected: + // Only derived classes can construct + qualifierst() = default; + +public: + // Copy/move construction/assignment is deleted here and in derived classes + qualifierst(const qualifierst &) = delete; + qualifierst(qualifierst &&) = delete; + qualifierst &operator=(const qualifierst &) = delete; + qualifierst &operator=(qualifierst &&) = delete; + + // Destruction is virtual + virtual ~qualifierst() = default; + +public: + virtual std::unique_ptr clone() const = 0; + + virtual qualifierst &operator+=(const qualifierst &b) = 0; + + virtual std::size_t count() const = 0; + + virtual void clear() = 0; + + virtual void read(const typet &src) = 0; + virtual void write(typet &src) const = 0; + + // Comparisons + virtual bool is_subset_of(const qualifierst &q) const = 0; + virtual bool operator==(const qualifierst &other) const = 0; + bool operator!=(const qualifierst &other) const + { + return !(*this == other); + } + + // String conversion + virtual std::string as_string() const = 0; + friend std::ostream &operator<<(std::ostream &, const qualifierst &); +}; + + +class c_qualifierst : public qualifierst { public: c_qualifierst() @@ -29,13 +71,12 @@ class c_qualifierst read(src); } - c_qualifierst(const c_qualifierst &other) = delete; - virtual c_qualifierst &operator=(const c_qualifierst &other); - virtual std::unique_ptr clone() const; - - virtual ~c_qualifierst() = default; +protected: + c_qualifierst &operator=(const c_qualifierst &other); +public: + virtual std::unique_ptr clone() const override; - virtual void clear() + virtual void clear() override { is_constant=false; is_volatile=false; @@ -57,62 +98,60 @@ class c_qualifierst // will likely add alignment here as well - virtual std::string as_string() const; - virtual void read(const typet &src); - virtual void write(typet &src) const; + virtual std::string as_string() const override; + virtual void read(const typet &src) override; + virtual void write(typet &src) const override; static void clear(typet &dest); - virtual bool is_subset_of(const c_qualifierst &q) const + virtual bool is_subset_of(const qualifierst &other) const override { - return (!is_constant || q.is_constant) && - (!is_volatile || q.is_volatile) && - (!is_restricted || q.is_restricted) && - (!is_atomic || q.is_atomic) && - (!is_ptr32 || q.is_ptr32) && - (!is_ptr64 || q.is_ptr64) && - (!is_noreturn || q.is_noreturn); + const c_qualifierst *cq = dynamic_cast(&other); + return + (!is_constant || cq->is_constant) && + (!is_volatile || cq->is_volatile) && + (!is_restricted || cq->is_restricted) && + (!is_atomic || cq->is_atomic) && + (!is_ptr32 || cq->is_ptr32) && + (!is_ptr64 || cq->is_ptr64) && + (!is_noreturn || cq->is_noreturn); // is_transparent_union isn't checked } - virtual bool operator==(const c_qualifierst &other) const + virtual bool operator==(const qualifierst &other) const override { - return is_constant==other.is_constant && - is_volatile==other.is_volatile && - is_restricted==other.is_restricted && - is_atomic==other.is_atomic && - is_ptr32==other.is_ptr32 && - is_ptr64==other.is_ptr64 && - is_transparent_union==other.is_transparent_union && - is_noreturn==other.is_noreturn; + const c_qualifierst *cq = dynamic_cast(&other); + return + is_constant == cq->is_constant && + is_volatile == cq->is_volatile && + is_restricted == cq->is_restricted && + is_atomic == cq->is_atomic && + is_ptr32 == cq->is_ptr32 && + is_ptr64 == cq->is_ptr64 && + is_transparent_union == cq->is_transparent_union && + is_noreturn == cq->is_noreturn; } - bool operator!=(const c_qualifierst &other) const + virtual qualifierst &operator+=(const qualifierst &other) override { - return !(*this==other); - } - - virtual c_qualifierst &operator+=(const c_qualifierst &b) - { - is_constant|=b.is_constant; - is_volatile|=b.is_volatile; - is_restricted|=b.is_restricted; - is_atomic|=b.is_atomic; - is_ptr32|=b.is_ptr32; - is_ptr64|=b.is_ptr64; - is_transparent_union|=b.is_transparent_union; - is_noreturn|=b.is_noreturn; + const c_qualifierst *cq = dynamic_cast(&other); + is_constant |= cq->is_constant; + is_volatile |= cq->is_volatile; + is_restricted |= cq->is_restricted; + is_atomic |= cq->is_atomic; + is_ptr32 |= cq->is_ptr32; + is_ptr64 |= cq->is_ptr64; + is_transparent_union |= cq->is_transparent_union; + is_noreturn |= cq->is_noreturn; return *this; } - virtual std::size_t count() const + virtual std::size_t count() const override { return is_constant+is_volatile+is_restricted+is_atomic+ is_ptr32+is_ptr64+is_noreturn; } }; -std::ostream &operator << (std::ostream &, const c_qualifierst &); - #endif // CPROVER_ANSI_C_C_QUALIFIERS_H diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 24c7b89aded..665b438dab5 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -162,11 +162,11 @@ std::string expr2ct::convert(const typet &src) std::string expr2ct::convert_rec( const typet &src, - const c_qualifierst &qualifiers, + const qualifierst &qualifiers, const std::string &declarator) { - std::unique_ptr clone = qualifiers.clone(); - c_qualifierst &new_qualifiers = *clone; + std::unique_ptr clone = qualifiers.clone(); + c_qualifierst &new_qualifiers = dynamic_cast(*clone); new_qualifiers.read(src); std::string q=new_qualifiers.as_string(); @@ -737,7 +737,7 @@ std::string expr2ct::convert_struct_type( /// \return A C-like type declaration of an array std::string expr2ct::convert_array_type( const typet &src, - const c_qualifierst &qualifiers, + const qualifierst &qualifiers, const std::string &declarator_str) { return convert_array_type(src, qualifiers, declarator_str, true); @@ -753,7 +753,7 @@ std::string expr2ct::convert_array_type( /// \return A C-like type declaration of an array std::string expr2ct::convert_array_type( const typet &src, - const c_qualifierst &qualifiers, + const qualifierst &qualifiers, const std::string &declarator_str, bool inc_size_if_possible) { diff --git a/src/ansi-c/expr2c_class.h b/src/ansi-c/expr2c_class.h index 6dafa1cd84c..0886fb2f523 100644 --- a/src/ansi-c/expr2c_class.h +++ b/src/ansi-c/expr2c_class.h @@ -17,7 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -class c_qualifierst; +class qualifierst; class namespacet; class expr2ct @@ -36,7 +36,7 @@ class expr2ct virtual std::string convert_rec( const typet &src, - const c_qualifierst &qualifiers, + const qualifierst &qualifiers, const std::string &declarator); virtual std::string convert_struct_type( @@ -53,12 +53,12 @@ class expr2ct virtual std::string convert_array_type( const typet &src, - const c_qualifierst &qualifiers, + const qualifierst &qualifiers, const std::string &declarator_str); std::string convert_array_type( const typet &src, - const c_qualifierst &qualifiers, + const qualifierst &qualifiers, const std::string &declarator_str, bool inc_size_if_possible); diff --git a/src/cpp/expr2cpp.cpp b/src/cpp/expr2cpp.cpp index 3d7daacb08a..f10307f1f2b 100644 --- a/src/cpp/expr2cpp.cpp +++ b/src/cpp/expr2cpp.cpp @@ -41,7 +41,7 @@ class expr2cppt:public expr2ct std::string convert_rec( const typet &src, - const c_qualifierst &qualifiers, + const qualifierst &qualifiers, const std::string &declarator) override; typedef std::unordered_set id_sett; @@ -129,11 +129,11 @@ std::string expr2cppt::convert_constant( std::string expr2cppt::convert_rec( const typet &src, - const c_qualifierst &qualifiers, + const qualifierst &qualifiers, const std::string &declarator) { - std::unique_ptr clone = qualifiers.clone(); - c_qualifierst &new_qualifiers = *clone; + std::unique_ptr clone = qualifiers.clone(); + qualifierst &new_qualifiers = *clone; new_qualifiers.read(src); const std::string d= diff --git a/src/java_bytecode/expr2java.cpp b/src/java_bytecode/expr2java.cpp index 6e4a9d932c5..51bb43ad82b 100644 --- a/src/java_bytecode/expr2java.cpp +++ b/src/java_bytecode/expr2java.cpp @@ -251,11 +251,11 @@ std::string expr2javat::convert_constant( std::string expr2javat::convert_rec( const typet &src, - const c_qualifierst &qualifiers, + const qualifierst &qualifiers, const std::string &declarator) { - std::unique_ptr clone = qualifiers.clone(); - c_qualifierst &new_qualifiers = *clone; + std::unique_ptr clone = qualifiers.clone(); + qualifierst &new_qualifiers = *clone; new_qualifiers.read(src); const std::string d= diff --git a/src/java_bytecode/expr2java.h b/src/java_bytecode/expr2java.h index ff2975d40c4..2adb417eb03 100644 --- a/src/java_bytecode/expr2java.h +++ b/src/java_bytecode/expr2java.h @@ -41,7 +41,7 @@ class expr2javat:public expr2ct virtual std::string convert_rec( const typet &src, - const c_qualifierst &qualifiers, + const qualifierst &qualifiers, const std::string &declarator) override; // length of string representation of Java Char diff --git a/src/java_bytecode/java_qualifiers.cpp b/src/java_bytecode/java_qualifiers.cpp index 9fd67220d95..fef9e389f0a 100644 --- a/src/java_bytecode/java_qualifiers.cpp +++ b/src/java_bytecode/java_qualifiers.cpp @@ -19,30 +19,7 @@ java_qualifierst &java_qualifierst::operator=(const java_qualifierst &other) return *this; } -java_qualifierst &java_qualifierst::operator=(java_qualifierst &&other) -{ - INVARIANT( - &other.ns == &ns, - "Can only assign from a java_qualifierst using the same namespace"); - annotations = std::move(other.annotations); - c_qualifierst::operator=(other); - return *this; -} - -c_qualifierst &java_qualifierst::operator=(const c_qualifierst &c_other) -{ - auto other = dynamic_cast(&c_other); - if(other != nullptr) - *this = *other; - else - { - annotations.clear(); - c_qualifierst::operator=(c_other); - } - return *this; -} - -std::unique_ptr java_qualifierst::clone() const +std::unique_ptr java_qualifierst::clone() const { auto other = util_make_unique(ns); *other = *this; @@ -74,37 +51,36 @@ void java_qualifierst::write(typet &src) const annotated_type.get_annotations() = annotations; } -c_qualifierst &java_qualifierst::operator+=(const c_qualifierst &c_other) +qualifierst &java_qualifierst::operator+=(const qualifierst &other) { - c_qualifierst::operator+=(c_other); - auto other = dynamic_cast(&c_other); - if(other != nullptr) + c_qualifierst::operator+=(other); + auto jq = dynamic_cast(&other); + if(jq != nullptr) { std::copy( - other->annotations.begin(), - other->annotations.end(), + jq->annotations.begin(), + jq->annotations.end(), std::back_inserter(annotations)); } return *this; } -bool java_qualifierst::operator==(const c_qualifierst &c_other) const +bool java_qualifierst::operator==(const qualifierst &other) const { - auto other = dynamic_cast(&c_other); - if(other == nullptr) + auto jq = dynamic_cast(&other); + if(jq == nullptr) return false; - return - c_qualifierst::operator==(c_other) && annotations == other->annotations; + return c_qualifierst::operator==(other) && annotations == jq->annotations; } -bool java_qualifierst::is_subset_of(const c_qualifierst &c_other) const +bool java_qualifierst::is_subset_of(const qualifierst &other) const { - if(!c_qualifierst::is_subset_of(c_other)) + if(!c_qualifierst::is_subset_of(other)) return false; - auto other = dynamic_cast(&c_other); - if(other == nullptr) + auto jq = dynamic_cast(&other); + if(jq == nullptr) return annotations.empty(); - auto &other_a = other->annotations; + auto &other_a = jq->annotations; for(const auto &annotation : annotations) { if(std::find(other_a.begin(), other_a.end(), annotation) == other_a.end()) diff --git a/src/java_bytecode/java_qualifiers.h b/src/java_bytecode/java_qualifiers.h index cd9862a868a..e85bbfa6d93 100644 --- a/src/java_bytecode/java_qualifiers.h +++ b/src/java_bytecode/java_qualifiers.h @@ -20,12 +20,12 @@ class java_qualifierst : public c_qualifierst : ns(ns) {} +protected: java_qualifierst &operator=(const java_qualifierst &other); - java_qualifierst &operator=(java_qualifierst &&other); - virtual c_qualifierst &operator=(const c_qualifierst &other) override; - virtual std::unique_ptr clone() const override; +public: + virtual std::unique_ptr clone() const override; - virtual c_qualifierst &operator+=(const c_qualifierst &other) override; + virtual qualifierst &operator+=(const qualifierst &other) override; const std::vector &get_annotations() const { @@ -38,8 +38,8 @@ class java_qualifierst : public c_qualifierst virtual void read(const typet &src) override; virtual void write(typet &src) const override; - virtual bool is_subset_of(const c_qualifierst &other) const override; - virtual bool operator==(const c_qualifierst &other) const override; + virtual bool is_subset_of(const qualifierst &other) const override; + virtual bool operator==(const qualifierst &other) const override; virtual std::string as_string() const override; }; From ca77b4ead25f9fe9123c2f7f7f8161d1f4c558ef Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Wed, 7 Feb 2018 15:37:09 +0000 Subject: [PATCH 6/7] Add test for added annotations --- .../annotations1/ClassAnnotation.class | Bin 0 -> 146 bytes .../annotations1/FieldAnnotation.class | Bin 0 -> 146 bytes .../annotations1/MethodAnnotation.class | Bin 0 -> 147 bytes .../cbmc-java/annotations1/annotations.class | Bin 0 -> 409 bytes .../cbmc-java/annotations1/annotations.java | 23 ++++++++++++++++++ .../annotations1/show_annotation_symbol.desc | 12 +++++++++ 6 files changed, 35 insertions(+) create mode 100644 regression/cbmc-java/annotations1/ClassAnnotation.class create mode 100644 regression/cbmc-java/annotations1/FieldAnnotation.class create mode 100644 regression/cbmc-java/annotations1/MethodAnnotation.class create mode 100644 regression/cbmc-java/annotations1/annotations.class create mode 100644 regression/cbmc-java/annotations1/annotations.java create mode 100644 regression/cbmc-java/annotations1/show_annotation_symbol.desc diff --git a/regression/cbmc-java/annotations1/ClassAnnotation.class b/regression/cbmc-java/annotations1/ClassAnnotation.class new file mode 100644 index 0000000000000000000000000000000000000000..c5dbfca92fdbb06b62210139b16987567db4aa7b GIT binary patch literal 146 zcmX^0Z`VEs1_l!bPId-1b_RBK1`b9BuHgLAqU2P!%$!t427$!9y!?{HlFac; literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/annotations1/MethodAnnotation.class b/regression/cbmc-java/annotations1/MethodAnnotation.class new file mode 100644 index 0000000000000000000000000000000000000000..471b9576871250d2d06014e2b2b4dda2ab5acfb2 GIT binary patch literal 147 zcmX^0Z`VEs1_l!bPId-1b_RBK1`b9BuHgLAqU2P!%$!t427$!9y!?{HlFaS6ot=CZDP}EfBXRv7w*)B-MCW(DHIA(LB;)~9dt@Efo4+lv0Mo*d;lLx zJjtT1x|nlj?tJ&2nXm7UPXK4w2~k5Yz*c~5fxK{y1p9Y|btcs#J2$zB6MbcE=9Dv; z%>~_PXmm1J*3Q}WD)29iHSSVSJ34+8tPQe>7PKQ{^-Yn+diJ0=iWjLeR?v&CwR_Hf z&k66dVm8)8Q-U3}j6I#Ixhk^=qgb1ffg^?$XJ!~tFC^^rN%i_A?T9@>?5 I7S%5B1BAUv>i_@% literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/annotations1/annotations.java b/regression/cbmc-java/annotations1/annotations.java new file mode 100644 index 00000000000..5fd8a36fd99 --- /dev/null +++ b/regression/cbmc-java/annotations1/annotations.java @@ -0,0 +1,23 @@ +@interface ClassAnnotation { +} + +@interface MethodAnnotation { +} + +@interface FieldAnnotation { +} + +@ClassAnnotation +public class annotations +{ + @FieldAnnotation + public int x; + + @FieldAnnotation + public static int y; + + @MethodAnnotation + public void main() + { + } +} diff --git a/regression/cbmc-java/annotations1/show_annotation_symbol.desc b/regression/cbmc-java/annotations1/show_annotation_symbol.desc new file mode 100644 index 00000000000..778e1104824 --- /dev/null +++ b/regression/cbmc-java/annotations1/show_annotation_symbol.desc @@ -0,0 +1,12 @@ +CORE +annotations.class +--verbosity 10 --show-symbol-table +^EXIT=0$ +^SIGNAL=0$ +^Type\.\.\.\.\.\.\.\.: @java::ClassAnnotation struct annotations +^Type\.\.\.\.\.\.\.\.: @java::MethodAnnotation \(struct annotations \*\) -> void$ +^Type\.\.\.\.\.\.\.\.: @java::FieldAnnotation int$ +-- +-- +The purpose of the test is ensuring that annotations can be shown in the symbol +table. \ No newline at end of file From 9a8d937e480047d1d54240767b08d58b2e5f55b4 Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Wed, 14 Mar 2018 10:24:33 +0000 Subject: [PATCH 7/7] Add to_annotated_type and enable type_checked_cast for annotated_typet --- .../java_bytecode_convert_class.cpp | 2 +- .../java_bytecode_convert_method.cpp | 2 +- src/java_bytecode/java_qualifiers.cpp | 3 +-- src/java_bytecode/java_types.h | 18 +++++++++++++++++- 4 files changed, 20 insertions(+), 5 deletions(-) diff --git a/src/java_bytecode/java_bytecode_convert_class.cpp b/src/java_bytecode/java_bytecode_convert_class.cpp index f4a237be8c9..877252f5e12 100644 --- a/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/src/java_bytecode/java_bytecode_convert_class.cpp @@ -648,7 +648,7 @@ void java_bytecode_convert_classt::convert( { convert_annotations( f.annotations, - static_cast(new_symbol.type).get_annotations()); + type_checked_cast(new_symbol.type).get_annotations()); } // Do we have the static field symbol already? diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index 7bf488ecc43..e535620a535 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -392,7 +392,7 @@ void java_bytecode_convert_method_lazy( { convert_annotations( m.annotations, - static_cast(static_cast(member_type)) + type_checked_cast(static_cast(member_type)) .get_annotations()); } diff --git a/src/java_bytecode/java_qualifiers.cpp b/src/java_bytecode/java_qualifiers.cpp index fef9e389f0a..a9f2f0bdacb 100644 --- a/src/java_bytecode/java_qualifiers.cpp +++ b/src/java_bytecode/java_qualifiers.cpp @@ -47,8 +47,7 @@ void java_qualifierst::read(const typet &src) void java_qualifierst::write(typet &src) const { c_qualifierst::write(src); - auto &annotated_type = static_cast(src); - annotated_type.get_annotations() = annotations; + type_checked_cast(src).get_annotations() = annotations; } qualifierst &java_qualifierst::operator+=(const qualifierst &other) diff --git a/src/java_bytecode/java_types.h b/src/java_bytecode/java_types.h index fcf8048635b..e731915e64a 100644 --- a/src/java_bytecode/java_types.h +++ b/src/java_bytecode/java_types.h @@ -82,6 +82,22 @@ class annotated_typet : public typet } }; +inline const annotated_typet &to_annotated_type(const typet &type) +{ + return static_cast(type); +} + +inline annotated_typet &to_annotated_type(typet &type) +{ + return static_cast(type); +} + +template <> +inline bool can_cast_type(const typet &type) +{ + return true; +} + class java_class_typet:public class_typet { public: @@ -129,7 +145,7 @@ class java_class_typet:public class_typet std::vector &get_annotations() { - return static_cast( + return type_checked_cast( static_cast(*this)).get_annotations(); } };