Pretty printing of java_class_typet

Added java_qualifierst that adds annotations as qualifiers to types

Author: NathanJPhillips

src/ansi-c/c_qualifiers.cpp

@@ -9,6 +9,27 @@ Author: Daniel Kroening, [email protected]
 #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<c_qualifierst> c_qualifierst::clone() const
+{
+  auto other = util_make_unique<c_qualifierst>();
+  *other = *this;
+  return other;
+}
 
 std::string c_qualifierst::as_string() const
 {

src/ansi-c/c_qualifiers.h

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_ANSI_C_C_QUALIFIERS_H
 
 #include <iosfwd>
+#include <memory>
 
 #include <util/expr.h>
 
@@ -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<c_qualifierst> 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;

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<c_qualifierst> clone = qualifiers.clone();
+  c_qualifierst &new_qualifiers = *clone;
   new_qualifiers.read(src);
 
   std::string q=new_qualifiers.as_string();

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<c_qualifierst> clone = qualifiers.clone();
+  c_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, [email protected]
 #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)
@@ -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<c_qualifierst> 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);

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(

src/java_bytecode/java_qualifiers.cpp

@@ -0,0 +1,146 @@
+// 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;
+}
+
+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<const java_qualifierst *>(&c_other);
+  if(other != nullptr)
+    *this = *other;
+  else
+  {
+    annotations.clear();
+    c_qualifierst::operator=(c_other);
+  }
+  return *this;
+}
+
+std::unique_ptr<c_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);
+  auto &annotated_type = static_cast<annotated_typet &>(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<const java_qualifierst *>(&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<const java_qualifierst *>(&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<const java_qualifierst *>(&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();
+}

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 <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)
+  {}
+
+  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<c_qualifierst> clone() const override;
+
+  virtual c_qualifierst &operator+=(const c_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 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