Skip to content

Commit 236b7fd

Browse files
Pretty printing of java_class_typet
Added java_qualifierst that adds annotations as qualifiers to types
1 parent d612d75 commit 236b7fd

File tree

9 files changed

+263
-30
lines changed

9 files changed

+263
-30
lines changed

src/ansi-c/c_qualifiers.cpp

+21
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,27 @@ Author: Daniel Kroening, [email protected]
99
#include "c_qualifiers.h"
1010

1111
#include <ostream>
12+
#include <util/make_unique.h>
13+
14+
c_qualifierst &c_qualifierst::operator=(const c_qualifierst &other)
15+
{
16+
is_constant = other.is_constant;
17+
is_volatile = other.is_volatile;
18+
is_restricted = other.is_restricted;
19+
is_atomic = other.is_atomic;
20+
is_noreturn = other.is_noreturn;
21+
is_ptr32 = other.is_ptr32;
22+
is_ptr64 = other.is_ptr64;
23+
is_transparent_union = other.is_transparent_union;
24+
return *this;
25+
}
26+
27+
std::unique_ptr<c_qualifierst> c_qualifierst::clone() const
28+
{
29+
auto other = util_make_unique<c_qualifierst>();
30+
*other = *this;
31+
return other;
32+
}
1233

1334
std::string c_qualifierst::as_string() const
1435
{

src/ansi-c/c_qualifiers.h

+15-8
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
1111
#define CPROVER_ANSI_C_C_QUALIFIERS_H
1212

1313
#include <iosfwd>
14+
#include <memory>
1415

1516
#include <util/expr.h>
1617

@@ -28,7 +29,13 @@ class c_qualifierst
2829
read(src);
2930
}
3031

31-
void clear()
32+
c_qualifierst(const c_qualifierst &other) = delete;
33+
virtual c_qualifierst &operator=(const c_qualifierst &other);
34+
virtual std::unique_ptr<c_qualifierst> clone() const;
35+
36+
virtual ~c_qualifierst() = default;
37+
38+
virtual void clear()
3239
{
3340
is_constant=false;
3441
is_volatile=false;
@@ -50,13 +57,13 @@ class c_qualifierst
5057

5158
// will likely add alignment here as well
5259

53-
std::string as_string() const;
54-
void read(const typet &src);
55-
void write(typet &src) const;
60+
virtual std::string as_string() const;
61+
virtual void read(const typet &src);
62+
virtual void write(typet &src) const;
5663

5764
static void clear(typet &dest);
5865

59-
bool is_subset_of(const c_qualifierst &q) const
66+
virtual bool is_subset_of(const c_qualifierst &q) const
6067
{
6168
return (!is_constant || q.is_constant) &&
6269
(!is_volatile || q.is_volatile) &&
@@ -69,7 +76,7 @@ class c_qualifierst
6976
// is_transparent_union isn't checked
7077
}
7178

72-
bool operator==(const c_qualifierst &other) const
79+
virtual bool operator==(const c_qualifierst &other) const
7380
{
7481
return is_constant==other.is_constant &&
7582
is_volatile==other.is_volatile &&
@@ -86,7 +93,7 @@ class c_qualifierst
8693
return !(*this==other);
8794
}
8895

89-
c_qualifierst &operator+=(const c_qualifierst &b)
96+
virtual c_qualifierst &operator+=(const c_qualifierst &b)
9097
{
9198
is_constant|=b.is_constant;
9299
is_volatile|=b.is_volatile;
@@ -99,7 +106,7 @@ class c_qualifierst
99106
return *this;
100107
}
101108

102-
unsigned count() const
109+
virtual std::size_t count() const
103110
{
104111
return is_constant+is_volatile+is_restricted+is_atomic+
105112
is_ptr32+is_ptr64+is_noreturn;

src/ansi-c/expr2c.cpp

+2-1
Original file line numberDiff line numberDiff line change
@@ -165,7 +165,8 @@ std::string expr2ct::convert_rec(
165165
const c_qualifierst &qualifiers,
166166
const std::string &declarator)
167167
{
168-
c_qualifierst new_qualifiers(qualifiers);
168+
std::unique_ptr<c_qualifierst> clone = qualifiers.clone();
169+
c_qualifierst &new_qualifiers = *clone;
169170
new_qualifiers.read(src);
170171

171172
std::string q=new_qualifiers.as_string();

src/cpp/expr2cpp.cpp

+2-1
Original file line numberDiff line numberDiff line change
@@ -132,7 +132,8 @@ std::string expr2cppt::convert_rec(
132132
const c_qualifierst &qualifiers,
133133
const std::string &declarator)
134134
{
135-
c_qualifierst new_qualifiers(qualifiers);
135+
std::unique_ptr<c_qualifierst> clone = qualifiers.clone();
136+
c_qualifierst &new_qualifiers = *clone;
136137
new_qualifiers.read(src);
137138

138139
const std::string d=

src/java_bytecode/Makefile

+1
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,7 @@ SRC = bytecode_info.cpp \
2323
java_local_variable_table.cpp \
2424
java_object_factory.cpp \
2525
java_pointer_casts.cpp \
26+
java_qualifiers.cpp \
2627
java_root_class.cpp \
2728
java_static_initializers.cpp \
2829
java_string_library_preprocess.cpp \

src/java_bytecode/expr2java.cpp

+14-3
Original file line numberDiff line numberDiff line change
@@ -19,12 +19,22 @@ Author: Daniel Kroening, [email protected]
1919
#include <util/arith_tools.h>
2020
#include <util/ieee_float.h>
2121

22-
#include <ansi-c/c_qualifiers.h>
2322
#include <ansi-c/c_misc.h>
2423
#include <ansi-c/expr2c_class.h>
2524

25+
#include "java_qualifiers.h"
2626
#include "java_types.h"
2727

28+
std::string expr2javat::convert(const typet &src)
29+
{
30+
return convert_rec(src, java_qualifierst(ns), "");
31+
}
32+
33+
std::string expr2javat::convert(const exprt &src)
34+
{
35+
return expr2ct::convert(src);
36+
}
37+
2838
std::string expr2javat::convert_code_function_call(
2939
const code_function_callt &src,
3040
unsigned indent)
@@ -244,7 +254,8 @@ std::string expr2javat::convert_rec(
244254
const c_qualifierst &qualifiers,
245255
const std::string &declarator)
246256
{
247-
c_qualifierst new_qualifiers(qualifiers);
257+
std::unique_ptr<c_qualifierst> clone = qualifiers.clone();
258+
c_qualifierst &new_qualifiers = *clone;
248259
new_qualifiers.read(src);
249260

250261
const std::string d=
@@ -307,7 +318,7 @@ std::string expr2javat::convert_rec(
307318
const typet &return_type=code_type.return_type();
308319
dest+=" -> "+convert(return_type);
309320

310-
return dest;
321+
return q + dest;
311322
}
312323
else
313324
return expr2ct::convert_rec(src, qualifiers, declarator);

src/java_bytecode/expr2java.h

+16-17
Original file line numberDiff line numberDiff line change
@@ -20,30 +20,29 @@ class expr2javat:public expr2ct
2020
{
2121
public:
2222
explicit expr2javat(const namespacet &_ns):expr2ct(_ns) { }
23+
virtual std::string convert(const typet &src) override;
24+
virtual std::string convert(const exprt &src) override;
25+
2326
protected:
2427
virtual std::string convert_with_precedence(
25-
const exprt &src, unsigned &precedence);
26-
virtual std::string convert_java_this(const exprt &src, unsigned precedence);
27-
virtual std::string convert_java_instanceof(
28-
const exprt &src,
29-
unsigned precedence);
30-
virtual std::string convert_java_new(const exprt &src, unsigned precedence);
31-
virtual std::string convert_code_java_delete(
32-
const exprt &src,
33-
unsigned precedence);
34-
virtual std::string convert_struct(const exprt &src, unsigned &precedence);
35-
virtual std::string convert_code(const codet &src, unsigned indent);
28+
const exprt &src, unsigned &precedence) override;
29+
std::string convert_java_this(const exprt &src, unsigned precedence);
30+
std::string convert_java_instanceof(const exprt &src, unsigned precedence);
31+
std::string convert_java_new(const exprt &src, unsigned precedence);
32+
std::string convert_code_java_delete(const exprt &src, unsigned precedence);
33+
virtual std::string convert_struct(
34+
const exprt &src, unsigned &precedence) override;
35+
virtual std::string convert_code(const codet &src, unsigned indent) override;
3636
virtual std::string convert_constant(
37-
const constant_exprt &src,
38-
unsigned &precedence);
39-
virtual std::string convert_code_function_call(
40-
const code_function_callt &src,
41-
unsigned indent);
37+
const constant_exprt &src, unsigned &precedence) override;
38+
// Hides base class version
39+
std::string convert_code_function_call(
40+
const code_function_callt &src, unsigned indent);
4241

4342
virtual std::string convert_rec(
4443
const typet &src,
4544
const c_qualifierst &qualifiers,
46-
const std::string &declarator);
45+
const std::string &declarator) override;
4746

4847
// length of string representation of Java Char
4948
// representation is '\u0000'

src/java_bytecode/java_qualifiers.cpp

+154
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,154 @@
1+
// Author: Diffblue Ltd.
2+
3+
/// \file
4+
/// Java-specific type qualifiers
5+
6+
#include "java_qualifiers.h"
7+
#include <sstream>
8+
#include <util/make_unique.h>
9+
#include "expr2java.h"
10+
11+
java_qualifierst::java_qualifierst(const namespacet &ns) : ns(ns)
12+
{
13+
}
14+
15+
java_qualifierst &java_qualifierst::operator=(const java_qualifierst &other)
16+
{
17+
INVARIANT(
18+
&other.ns == &ns,
19+
"Can only assign from a java_qualifierst using the same namespace");
20+
annotations = other.annotations;
21+
c_qualifierst::operator=(other);
22+
return *this;
23+
}
24+
25+
java_qualifierst &java_qualifierst::operator=(java_qualifierst &&other)
26+
{
27+
INVARIANT(
28+
&other.ns == &ns,
29+
"Can only assign from a java_qualifierst using the same namespace");
30+
annotations = std::move(other.annotations);
31+
c_qualifierst::operator=(other);
32+
return *this;
33+
}
34+
35+
c_qualifierst &java_qualifierst::operator=(const c_qualifierst &c_other)
36+
{
37+
auto other = dynamic_cast<const java_qualifierst *>(&c_other);
38+
if(other != nullptr)
39+
*this = *other;
40+
else
41+
{
42+
annotations.clear();
43+
c_qualifierst::operator=(c_other);
44+
}
45+
return *this;
46+
}
47+
48+
std::unique_ptr<c_qualifierst> java_qualifierst::clone() const
49+
{
50+
auto other = util_make_unique<java_qualifierst>(ns);
51+
*other = *this;
52+
return std::move(other);
53+
}
54+
55+
const std::vector<java_annotationt> &java_qualifierst::get_annotations() const
56+
{
57+
return annotations;
58+
}
59+
60+
std::size_t java_qualifierst::count() const
61+
{
62+
return c_qualifierst::count() + annotations.size();
63+
}
64+
65+
void java_qualifierst::clear()
66+
{
67+
c_qualifierst::clear();
68+
annotations.clear();
69+
}
70+
71+
void java_qualifierst::read(const typet &src)
72+
{
73+
c_qualifierst::read(src);
74+
auto &annotated_type = static_cast<const annotated_typet &>(src);
75+
annotations = annotated_type.get_annotations();
76+
}
77+
78+
void java_qualifierst::write(typet &src) const
79+
{
80+
c_qualifierst::write(src);
81+
auto &annotated_type = static_cast<annotated_typet &>(src);
82+
annotated_type.get_annotations() = annotations;
83+
}
84+
85+
c_qualifierst &java_qualifierst::operator+=(const c_qualifierst &c_other)
86+
{
87+
c_qualifierst::operator+=(c_other);
88+
auto other = dynamic_cast<const java_qualifierst *>(&c_other);
89+
if(other != nullptr)
90+
{
91+
std::copy(
92+
other->annotations.begin(),
93+
other->annotations.end(),
94+
std::back_inserter(annotations));
95+
}
96+
return *this;
97+
}
98+
99+
bool java_qualifierst::operator==(const c_qualifierst &c_other) const
100+
{
101+
auto other = dynamic_cast<const java_qualifierst *>(&c_other);
102+
if(other == nullptr)
103+
return false;
104+
return
105+
c_qualifierst::operator==(c_other) && annotations == other->annotations;
106+
}
107+
108+
bool java_qualifierst::is_subset_of(const c_qualifierst &c_other) const
109+
{
110+
if(!c_qualifierst::is_subset_of(c_other))
111+
return false;
112+
auto other = dynamic_cast<const java_qualifierst *>(&c_other);
113+
if(other == nullptr)
114+
return annotations.empty();
115+
auto &other_a = other->annotations;
116+
for(const auto &annotation : annotations)
117+
{
118+
if(std::find(other_a.begin(), other_a.end(), annotation) == other_a.end())
119+
return false;
120+
}
121+
return true;
122+
}
123+
124+
std::string java_qualifierst::as_string() const
125+
{
126+
std::stringstream out;
127+
for(const java_annotationt &annotation : annotations)
128+
{
129+
out << '@';
130+
out << annotation.get_type().subtype().get(ID_identifier);
131+
132+
if(!annotation.get_values().empty())
133+
{
134+
out << '(';
135+
136+
bool first = true;
137+
for(const java_annotationt::valuet &value : annotation.get_values())
138+
{
139+
if(first)
140+
first = false;
141+
else
142+
out << ", ";
143+
144+
out << '"' << value.get_name() << '"' << '=';
145+
out << expr2java(value.get_value(), ns);
146+
}
147+
148+
out << ')';
149+
}
150+
out << ' ';
151+
}
152+
out << c_qualifierst::as_string();
153+
return out.str();
154+
}

0 commit comments

Comments
 (0)