Merge pull request #1831 from NathanJPhillips/feature/class-annotations

[SEC-179] Add annotations to java_class_typet

Author: peterschrammel

regression/cbmc-java/annotations1/ClassAnnotation.class

@@ -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()
+    {
+    }
+}

regression/cbmc-java/annotations1/FieldAnnotation.class

@@ -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.

regression/cbmc-java/annotations1/MethodAnnotation.class

@@ -9,6 +9,27 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "c_qualifiers.h"
 
 #include <ostream>
+#include <util/make_unique.h>
+
+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<qualifierst> c_qualifierst::clone() const
+{
+  auto other = util_make_unique<c_qualifierst>();
+  *other = *this;
+  return std::move(other);
+}
 
 std::string c_qualifierst::as_string() const
 {
@@ -120,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();
 }

regression/cbmc-java/annotations1/annotations.class

@@ -11,10 +11,53 @@ Author: Daniel Kroening, kroening@kroening.com
 #define CPROVER_ANSI_C_C_QUALIFIERS_H
 
 #include <iosfwd>
+#include <memory>
 
 #include <util/expr.h>
 
-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<qualifierst> 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()
@@ -28,7 +71,12 @@ class c_qualifierst
     read(src);
   }
 
-  void clear()
+protected:
+  c_qualifierst &operator=(const c_qualifierst &other);
+public:
+  virtual std::unique_ptr<qualifierst> clone() const override;
+
+  virtual void clear() override
   {
     is_constant=false;
     is_volatile=false;
@@ -50,62 +98,60 @@ 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 override;
+  virtual void read(const typet &src) override;
+  virtual void write(typet &src) const override;
 
   static void clear(typet &dest);
 
-  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<const c_qualifierst *>(&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
   }
 
-  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<const c_qualifierst *>(&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);
-  }
-
-  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<const c_qualifierst *>(&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;
   }
 
-  unsigned 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

regression/cbmc-java/annotations1/annotations.java

@@ -162,10 +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)
 {
-  c_qualifierst new_qualifiers(qualifiers);
+  std::unique_ptr<qualifierst> clone = qualifiers.clone();
+  c_qualifierst &new_qualifiers = dynamic_cast<c_qualifierst &>(*clone);
   new_qualifiers.read(src);
 
   std::string q=new_qualifiers.as_string();
@@ -736,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);
@@ -752,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)
 {

regression/cbmc-java/annotations1/show_annotation_symbol.desc

@@ -17,7 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/std_code.h>
 #include <util/std_expr.h>
 
-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);
 

src/ansi-c/c_qualifiers.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<std::string, string_hash> id_sett;
@@ -129,10 +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)
 {
-  c_qualifierst new_qualifiers(qualifiers);
+  std::unique_ptr<qualifierst> clone = qualifiers.clone();
+  qualifierst &new_qualifiers = *clone;
   new_qualifiers.read(src);
 
   const std::string d=

src/ansi-c/c_qualifiers.h

@@ -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 \

src/ansi-c/expr2c.cpp

@@ -19,12 +19,22 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #include <util/arith_tools.h>
 #include <util/ieee_float.h>
 
-#include <ansi-c/c_qualifiers.h>
 #include <ansi-c/c_misc.h>
 #include <ansi-c/expr2c_class.h>
 
+#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)
@@ -241,10 +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)
 {
-  c_qualifierst new_qualifiers(qualifiers);
+  std::unique_ptr<qualifierst> clone = qualifiers.clone();
+  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);

src/ansi-c/expr2c_class.h

@@ -20,30 +20,29 @@ 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(
-    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 qualifierst &qualifiers,
+    const std::string &declarator) override;
 
   // length of string representation of Java Char
   // representation is '\u0000'

src/cpp/expr2cpp.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,
+        type_checked_cast<annotated_typet>(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<annotated_typet &>(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<java_annotationt> &annotations)
+{
+  for(const auto &annotation : parsed_annotations)
+  {
+    annotations.emplace_back(annotation.type);
+    std::vector<java_annotationt::valuet> &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

src/java_bytecode/Makefile

@@ -29,6 +29,10 @@ bool java_bytecode_convert_class(
   java_string_library_preprocesst &string_preprocess,
   const std::unordered_set<std::string> &no_load_classes);
 
+void convert_annotations(
+  const java_bytecode_parse_treet::annotationst &parsed_annotations,
+  std::vector<java_annotationt> &annotations);
+
 void mark_java_implicitly_generic_class_type(
   const irep_idt &class_name,
   symbol_tablet &symbol_table);

src/java_bytecode/expr2java.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,
+      type_checked_cast<annotated_typet>(static_cast<typet &>(member_type))
+        .get_annotations());
+  }
+
   method_symbol.type=member_type;
   symbol_table.add(method_symbol);
 }

src/java_bytecode/expr2java.h

@@ -0,0 +1,121 @@
+// Author: Diffblue Ltd.
+
+/// \file
+/// Java-specific type qualifiers
+
+#include "java_qualifiers.h"
+#include <sstream>
+#include <util/make_unique.h>
+#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;
+}
+
+std::unique_ptr<qualifierst> java_qualifierst::clone() const
+{
+  auto other = util_make_unique<java_qualifierst>(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<const annotated_typet &>(src);
+  annotations = annotated_type.get_annotations();
+}
+
+void java_qualifierst::write(typet &src) const
+{
+  c_qualifierst::write(src);
+  type_checked_cast<annotated_typet>(src).get_annotations() = annotations;
+}
+
+qualifierst &java_qualifierst::operator+=(const qualifierst &other)
+{
+  c_qualifierst::operator+=(other);
+  auto jq = dynamic_cast<const java_qualifierst *>(&other);
+  if(jq != nullptr)
+  {
+    std::copy(
+      jq->annotations.begin(),
+      jq->annotations.end(),
+      std::back_inserter(annotations));
+  }
+  return *this;
+}
+
+bool java_qualifierst::operator==(const qualifierst &other) const
+{
+  auto jq = dynamic_cast<const java_qualifierst *>(&other);
+  if(jq == nullptr)
+    return false;
+  return c_qualifierst::operator==(other) && annotations == jq->annotations;
+}
+
+bool java_qualifierst::is_subset_of(const qualifierst &other) const
+{
+  if(!c_qualifierst::is_subset_of(other))
+    return false;
+  auto jq = dynamic_cast<const java_qualifierst *>(&other);
+  if(jq == nullptr)
+    return annotations.empty();
+  auto &other_a = jq->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();
+}

src/java_bytecode/java_bytecode_convert_class.cpp

@@ -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 <ansi-c/c_qualifiers.h>
+
+class java_qualifierst : public c_qualifierst
+{
+private:
+  const namespacet &ns;
+  std::vector<java_annotationt> annotations;
+
+public:
+  explicit java_qualifierst(const namespacet &ns)
+    : ns(ns)
+  {}
+
+protected:
+  java_qualifierst &operator=(const java_qualifierst &other);
+public:
+  virtual std::unique_ptr<qualifierst> clone() const override;
+
+  virtual qualifierst &operator+=(const qualifierst &other) override;
+
+  const std::vector<java_annotationt> &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 qualifierst &other) const override;
+  virtual bool operator==(const qualifierst &other) const override;
+
+  virtual std::string as_string() const override;
+};
+
+#endif // CPROVER_JAVA_BYTECODE_JAVA_QUALIFIERS_H

src/java_bytecode/java_bytecode_convert_class.h

@@ -19,6 +19,85 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/optional.h>
 #include <util/std_expr.h>
 
+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<const exprt &>(get_sub().front());
+    }
+  };
+
+  explicit java_annotationt(const typet &type)
+  {
+    set(ID_type, type);
+  }
+
+  const typet &get_type() const
+  {
+    return static_cast<const typet &>(find(ID_type));
+  }
+
+  const std::vector<valuet> &get_values() const
+  {
+    // This cast should be safe as valuet doesn't add data to irept
+    return reinterpret_cast<const std::vector<valuet> &>(get_sub());
+  }
+
+  std::vector<valuet> &get_values()
+  {
+    // This cast should be safe as valuet doesn't add data to irept
+    return reinterpret_cast<std::vector<valuet> &>(get_sub());
+  }
+};
+
+class annotated_typet : public typet
+{
+public:
+  const std::vector<java_annotationt> &get_annotations() const
+  {
+    // This cast should be safe as java_annotationt doesn't add data to irept
+    return reinterpret_cast<const std::vector<java_annotationt> &>(
+      find(ID_annotations).get_sub());
+  }
+
+  std::vector<java_annotationt> &get_annotations()
+  {
+    // This cast should be safe as java_annotationt doesn't add data to irept
+    return reinterpret_cast<std::vector<java_annotationt> &>(
+      add(ID_annotations).get_sub());
+  }
+};
+
+inline const annotated_typet &to_annotated_type(const typet &type)
+{
+  return static_cast<const annotated_typet &>(type);
+}
+
+inline annotated_typet &to_annotated_type(typet &type)
+{
+  return static_cast<annotated_typet &>(type);
+}
+
+template <>
+inline bool can_cast_type<annotated_typet>(const typet &type)
+{
+  return true;
+}
+
 class java_class_typet:public class_typet
 {
  public:
@@ -57,6 +136,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<java_annotationt> &get_annotations() const
+  {
+    return static_cast<const annotated_typet &>(
+      static_cast<const typet &>(*this)).get_annotations();
+  }
+
+  std::vector<java_annotationt> &get_annotations()
+  {
+    return type_checked_cast<annotated_typet>(
+      static_cast<typet &>(*this)).get_annotations();
+  }
 };
 
 inline const java_class_typet &to_java_class_type(const typet &type)
@@ -71,6 +162,12 @@ inline java_class_typet &to_java_class_type(typet &type)
   return static_cast<java_class_typet &>(type);
 }
 
+template <>
+inline bool can_cast_type<java_class_typet>(const typet &type)
+{
+  return can_cast_type<class_typet>(type);
+}
+
 typet java_int_type();
 typet java_long_type();
 typet java_short_type();

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -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

src/java_bytecode/java_qualifiers.cpp

@@ -328,6 +328,12 @@ inline struct_typet &to_struct_type(typet &type)
   return static_cast<struct_typet &>(type);
 }
 
+template <>
+inline bool can_cast_type<struct_typet>(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<class_typet &>(type);
 }
 
+template <>
+inline bool can_cast_type<class_typet>(const typet &type)
+{
+  return can_cast_type<struct_typet>(type) && type.get_bool(ID_C_class);
+}
+
 /*! \brief The union type
 */
 class union_typet:public struct_union_typet