[SEC-179] Add annotations to java_class_typet

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

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.

src/ansi-c/c_qualifiers.cpp

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

src/ansi-c/c_qualifiers.h

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

src/ansi-c/expr2c.cpp

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

src/ansi-c/expr2c_class.h

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

src/java_bytecode/expr2java.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);