cprover
java_types.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #ifndef CPROVER_JAVA_BYTECODE_JAVA_TYPES_H
10 #define CPROVER_JAVA_BYTECODE_JAVA_TYPES_H
11 
12 #include <util/invariant.h>
13 #include <algorithm>
14 #include <set>
15 
16 #include <util/type.h>
17 #include <util/std_types.h>
18 #include <util/c_types.h>
19 #include <util/optional.h>
20 #include <util/std_expr.h>
21 
22 class java_annotationt : public irept
23 {
24 public:
25  class valuet : public irept
26  {
27  public:
28  valuet(irep_idt name, const exprt &value) : irept(name)
29  {
30  get_sub().push_back(value);
31  }
32 
33  const irep_idt &get_name() const
34  {
35  return id();
36  }
37 
38  const exprt &get_value() const
39  {
40  return static_cast<const exprt &>(get_sub().front());
41  }
42  };
43 
44  explicit java_annotationt(const typet &type)
45  {
46  set(ID_type, type);
47  }
48 
49  const typet &get_type() const
50  {
51  return static_cast<const typet &>(find(ID_type));
52  }
53 
54  const std::vector<valuet> &get_values() const
55  {
56  // This cast should be safe as valuet doesn't add data to irept
57  return reinterpret_cast<const std::vector<valuet> &>(get_sub());
58  }
59 
60  std::vector<valuet> &get_values()
61  {
62  // This cast should be safe as valuet doesn't add data to irept
63  return reinterpret_cast<std::vector<valuet> &>(get_sub());
64  }
65 };
66 
67 class annotated_typet : public typet
68 {
69 public:
70  const std::vector<java_annotationt> &get_annotations() const
71  {
72  // This cast should be safe as java_annotationt doesn't add data to irept
73  return reinterpret_cast<const std::vector<java_annotationt> &>(
74  find(ID_C_annotations).get_sub());
75  }
76 
77  std::vector<java_annotationt> &get_annotations()
78  {
79  // This cast should be safe as java_annotationt doesn't add data to irept
80  return reinterpret_cast<std::vector<java_annotationt> &>(
81  add(ID_C_annotations).get_sub());
82  }
83 };
84 
85 inline const annotated_typet &to_annotated_type(const typet &type)
86 {
87  return static_cast<const annotated_typet &>(type);
88 }
89 
91 {
92  return static_cast<annotated_typet &>(type);
93 }
94 
95 template <>
96 inline bool can_cast_type<annotated_typet>(const typet &type)
97 {
98  return true;
99 }
100 
102 {
103  public:
104  const irep_idt &get_access() const
105  {
106  return get(ID_access);
107  }
108 
109  void set_access(const irep_idt &access)
110  {
111  return set(ID_access, access);
112  }
113 
114  bool get_final()
115  {
116  return get_bool(ID_final);
117  }
118 
119  void set_final(bool is_final)
120  {
121  set(ID_final, is_final);
122  }
123 
124  typedef std::vector<symbol_exprt> java_lambda_method_handlest;
125 
127  {
128  return (const java_lambda_method_handlest &)find(
129  ID_java_lambda_method_handles)
130  .get_sub();
131  }
132 
134  {
135  return (java_lambda_method_handlest &)add(ID_java_lambda_method_handles)
136  .get_sub();
137  }
138 
139  void add_lambda_method_handle(const irep_idt &identifier)
140  {
141  // creates a symbol_exprt for the identifier and pushes it in the vector
142  lambda_method_handles().emplace_back(identifier);
143  }
145  {
146  // creates empty symbol_exprt and pushes it in the vector
147  lambda_method_handles().emplace_back();
148  }
149 
150  const std::vector<java_annotationt> &get_annotations() const
151  {
152  return static_cast<const annotated_typet &>(
153  static_cast<const typet &>(*this)).get_annotations();
154  }
155 
156  std::vector<java_annotationt> &get_annotations()
157  {
159  static_cast<typet &>(*this)).get_annotations();
160  }
161 };
162 
163 inline const java_class_typet &to_java_class_type(const typet &type)
164 {
165  assert(type.id()==ID_struct);
166  return static_cast<const java_class_typet &>(type);
167 }
168 
170 {
171  assert(type.id()==ID_struct);
172  return static_cast<java_class_typet &>(type);
173 }
174 
175 template <>
176 inline bool can_cast_type<java_class_typet>(const typet &type)
177 {
178  return can_cast_type<class_typet>(type);
179 }
180 
191 symbol_typet java_classname(const std::string &);
192 
193 reference_typet java_array_type(const char subtype);
194 typet java_array_element_type(const symbol_typet &array_type);
195 
196 bool is_reference_type(char t);
197 
198 // i integer
199 // l long
200 // s short
201 // b byte
202 // c character
203 // f float
204 // d double
205 // z boolean
206 // a reference
207 
208 typet java_type_from_char(char t);
210  const std::string &,
211  const std::string &class_name_prefix="");
212 char java_char_from_type(const typet &type);
213 std::vector<typet> java_generic_type_from_string(
214  const std::string &,
215  const std::string &);
216 
220  const std::string src,
221  size_t starting_point = 0);
222 
223 
224 bool is_java_array_tag(const irep_idt &tag);
225 bool is_valid_java_array(const struct_typet &);
226 
227 bool equal_java_types(const typet &type1, const typet &type2);
228 
233 {
234 public:
236 
238  const irep_idt &_type_var_name,
239  const symbol_typet &_bound):
241  {
242  set(ID_C_java_generic_parameter, true);
243  type_variables().push_back(symbol_typet(_type_var_name));
244  }
245 
248  {
249  PRECONDITION(!type_variables().empty());
250  return type_variables().front();
251  }
252 
254  {
255  PRECONDITION(!type_variables().empty());
256  return const_cast<type_variablet &>(type_variables().front());
257  }
258 
259  const irep_idt get_name() const
260  {
261  return type_variable().get_identifier();
262  }
263 
264 private:
265  typedef std::vector<type_variablet> type_variablest;
267  {
268  return (const type_variablest &)(find(ID_type_variables).get_sub());
269  }
270 
272  {
273  return (type_variablest &)(add(ID_type_variables).get_sub());
274  }
275 };
276 
281 inline bool is_java_generic_parameter(const typet &type)
282 {
283  return type.get_bool(ID_C_java_generic_parameter);
284 }
285 
289  const typet &type)
290 {
292  return static_cast<const java_generic_parametert &>(type);
293 }
294 
298 {
300  return static_cast<java_generic_parametert &>(type);
301 }
302 
319 {
320 public:
321  typedef std::vector<reference_typet> generic_type_argumentst;
322 
323  explicit java_generic_typet(const typet &_type):
325  {
326  set(ID_C_java_generic_type, true);
327  }
328 
331  {
332  return (const generic_type_argumentst &)(
333  find(ID_type_variables).get_sub());
334  }
335 
338  {
339  return (generic_type_argumentst &)(
340  add(ID_type_variables).get_sub());
341  }
342 };
343 
346 inline bool is_java_generic_type(const typet &type)
347 {
348  return type.get_bool(ID_C_java_generic_type);
349 }
350 
354  const typet &type)
355 {
356  PRECONDITION(
357  type.id()==ID_pointer &&
358  is_java_generic_type(type));
359  return static_cast<const java_generic_typet &>(type);
360 }
361 
365 {
366  PRECONDITION(
367  type.id()==ID_pointer &&
368  is_java_generic_type(type));
369  return static_cast<java_generic_typet &>(type);
370 }
371 
376 {
377  public:
378  typedef std::vector<java_generic_parametert> generic_typest;
379 
381  {
382  set(ID_C_java_generics_class_type, true);
383  }
384 
386  {
387  return (const generic_typest &)(find(ID_generic_types).get_sub());
388  }
389 
391  {
392  return (generic_typest &)(add(ID_generic_types).get_sub());
393  }
394 };
395 
398 inline bool is_java_generic_class_type(const typet &type)
399 {
400  return type.get_bool(ID_C_java_generics_class_type);
401 }
402 
405 inline const java_generic_class_typet &
407 {
409  return static_cast<const java_generic_class_typet &>(type);
410 }
411 
416 {
418  return static_cast<java_generic_class_typet &>(type);
419 }
420 
426  size_t index,
427  const java_generic_typet &type)
428 {
429  const std::vector<reference_typet> &type_arguments =
430  type.generic_type_arguments();
431  PRECONDITION(index<type_arguments.size());
432  return type_arguments[index];
433 }
434 
439 inline const irep_idt &
441 {
442  const std::vector<java_generic_parametert> &gen_types=type.generic_types();
443 
444  PRECONDITION(index<gen_types.size());
445  const java_generic_parametert &gen_type=gen_types[index];
446 
447  return gen_type.type_variable().get_identifier();
448 }
449 
454 inline const typet &java_generic_class_type_bound(size_t index, const typet &t)
455 {
457  const java_generic_class_typet &type =
459  const std::vector<java_generic_parametert> &gen_types=type.generic_types();
460 
461  PRECONDITION(index<gen_types.size());
462  const java_generic_parametert &gen_type=gen_types[index];
463 
464  return gen_type.subtype();
465 }
466 
471 {
472 public:
473  typedef std::vector<java_generic_parametert> implicit_generic_typest;
474 
476  const java_class_typet &class_type,
477  const implicit_generic_typest &generic_types)
478  : java_class_typet(class_type)
479  {
480  set(ID_C_java_implicitly_generic_class_type, true);
481  for(const auto &type : generic_types)
482  {
483  implicit_generic_types().push_back(type);
484  }
485  }
486 
488  {
489  return (
491  &)(find(ID_implicit_generic_types).get_sub());
492  }
493 
495  {
496  return (
497  implicit_generic_typest &)(add(ID_implicit_generic_types).get_sub());
498  }
499 };
500 
504 {
505  return type.get_bool(ID_C_java_implicitly_generic_class_type);
506 }
507 
512 {
514  return static_cast<const java_implicitly_generic_class_typet &>(type);
515 }
516 
521 {
523  return static_cast<java_implicitly_generic_class_typet &>(type);
524 }
525 
528 class unsupported_java_class_signature_exceptiont:public std::logic_error
529 {
530 public:
532  std::logic_error(
533  "Unsupported class signature: "+type)
534  {
535  }
536 };
537 
539  const std::string &descriptor,
540  const optionalt<std::string> &signature,
541  const std::string &class_name)
542 {
543  try
544  {
545  return java_type_from_string(signature.value(), class_name);
546  }
548  {
549  return java_type_from_string(descriptor, class_name);
550  }
551 }
552 
558  const std::vector<java_generic_parametert> &gen_types,
559  const irep_idt &identifier)
560 {
561  const auto iter = std::find_if(
562  gen_types.cbegin(),
563  gen_types.cend(),
564  [&identifier](const java_generic_parametert &ref)
565  {
566  return ref.type_variable().get_identifier() == identifier;
567  });
568 
569  if(iter == gen_types.cend())
570  {
571  return {};
572  }
573 
574  return std::distance(gen_types.cbegin(), iter);
575 }
576 
578  const std::string &,
579  std::set<irep_idt> &);
581  const typet &,
582  std::set<irep_idt> &);
583 
588 {
589 public:
590  typedef std::vector<reference_typet> generic_typest;
591 
593  const symbol_typet &type,
594  const std::string &base_ref,
595  const std::string &class_name_prefix);
596 
598  {
599  return (const generic_typest &)(find(ID_generic_types).get_sub());
600  }
601 
603  {
604  return (generic_typest &)(add(ID_generic_types).get_sub());
605  }
606 
608  generic_type_index(const java_generic_parametert &type) const;
609 };
610 
613 inline bool is_java_generic_symbol_type(const typet &type)
614 {
615  return type.get_bool(ID_C_java_generic_symbol);
616 }
617 
620 inline const java_generic_symbol_typet &
622 {
624  return static_cast<const java_generic_symbol_typet &>(type);
625 }
626 
630 {
632  return static_cast<java_generic_symbol_typet &>(type);
633 }
634 
639 std::string erase_type_arguments(const std::string &);
645 std::string gather_full_class_name(const std::string &);
646 
647 // turn java type into string
648 std::string pretty_java_type(const typet &);
649 
650 // pretty signature for methods
651 std::string pretty_signature(const code_typet &);
652 
653 #endif // CPROVER_JAVA_BYTECODE_JAVA_TYPES_H
std::vector< java_annotationt > & get_annotations()
Definition: java_types.h:156
The type of an expression.
Definition: type.h:22
std::vector< typet > java_generic_type_from_string(const std::string &, const std::string &)
Converts the content of a generic class type into a vector of Java types, that is each type variable ...
Definition: java_types.cpp:610
unsupported_java_class_signature_exceptiont(std::string type)
Definition: java_types.h:531
std::vector< java_generic_parametert > implicit_generic_typest
Definition: java_types.h:473
char java_char_from_type(const typet &type)
Definition: java_types.cpp:569
java_implicitly_generic_class_typet(const java_class_typet &class_type, const implicit_generic_typest &generic_types)
Definition: java_types.h:475
Base type of functions.
Definition: std_types.h:764
symbol_typet type_variablet
Definition: java_types.h:235
std::vector< symbol_exprt > java_lambda_method_handlest
Definition: java_types.h:124
bool is_reference_type(char t)
Definition: java_types.cpp:142
std::vector< valuet > & get_values()
Definition: java_types.h:60
optionalt< size_t > generic_type_index(const java_generic_parametert &type) const
Check if this symbol has the given generic type.
Definition: java_types.cpp:882
void add_lambda_method_handle(const irep_idt &identifier)
Definition: java_types.h:139
const java_lambda_method_handlest & lambda_method_handles() const
Definition: java_types.h:126
bool is_java_generic_symbol_type(const typet &type)
Definition: java_types.h:613
const java_generic_class_typet & to_java_generic_class_type(const java_class_typet &type)
Definition: java_types.h:406
typet java_char_type()
Definition: java_types.cpp:57
generic_typest & generic_types()
Definition: java_types.h:602
bool is_java_generic_parameter(const typet &type)
Checks whether the type is a java generic parameter/variable, e.g., T in List<T>. ...
Definition: java_types.h:281
typet java_double_type()
Definition: java_types.cpp:67
const typet & java_generic_class_type_bound(size_t index, const typet &t)
Access information of the type bound of a generic java class type.
Definition: java_types.h:454
const java_generic_parametert & to_java_generic_parameter(const typet &type)
Definition: java_types.h:288
void set_final(bool is_final)
Definition: java_types.h:119
typet java_float_type()
Definition: java_types.cpp:62
auto type_checked_cast(TType &base) -> typename detail::expr_dynamic_cast_return_typet< T, TType >::type
Cast a reference to a generic typet to a specific derived class and checks that the type could be con...
Definition: expr_cast.h:198
std::string pretty_java_type(const typet &)
Definition: java_types.cpp:897
void get_dependencies_from_generic_parameters(const std::string &, std::set< irep_idt > &)
Collect information about generic type parameters from a given signature.
Definition: java_types.cpp:805
An exception that is raised for unsupported class signature.
Definition: java_types.h:528
STL namespace.
typet java_byte_type()
Definition: java_types.cpp:52
java_generic_typet(const typet &_type)
Definition: java_types.h:323
Structure type.
Definition: std_types.h:297
void set_access(const irep_idt &access)
Definition: java_types.h:109
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
java_generic_parametert(const irep_idt &_type_var_name, const symbol_typet &_bound)
Definition: java_types.h:237
bool is_valid_java_array(const struct_typet &)
Programmatic documentation of the structure of a Java array (of either primitives or references) type...
Definition: java_types.cpp:696
size_t find_closing_semi_colon_for_reference_type(const std::string src, size_t starting_point=0)
Finds the closing semi-colon ending a ClassTypeSignature that starts at starting_point.
Definition: java_types.cpp:390
typet java_type_from_string(const std::string &, const std::string &class_name_prefix="")
Transforms a string representation of a Java type into an internal type representation thereof...
Definition: java_types.cpp:428
subt & get_sub()
Definition: irep.h:245
valuet(irep_idt name, const exprt &value)
Definition: java_types.h:28
const generic_type_argumentst & generic_type_arguments() const
Definition: java_types.h:330
const irep_idt & id() const
Definition: irep.h:189
typet java_short_type()
Definition: java_types.cpp:47
const java_generic_symbol_typet & to_java_generic_symbol_type(const typet &type)
Definition: java_types.h:621
const type_variablet & type_variable() const
Definition: java_types.h:247
std::vector< reference_typet > generic_type_argumentst
Definition: java_types.h:321
bool is_java_array_tag(const irep_idt &tag)
See above.
Definition: java_types.cpp:137
Class to hold a class with generics, extends the java class type with a vector of java generic type p...
Definition: java_types.h:375
const irep_idt & get_access() const
Definition: java_types.h:104
java_lambda_method_handlest & lambda_method_handles()
Definition: java_types.h:133
std::vector< reference_typet > generic_typest
Definition: java_types.h:590
const exprt & get_value() const
Definition: java_types.h:38
A reference into the symbol table.
Definition: std_types.h:110
implicit_generic_typest & implicit_generic_types()
Definition: java_types.h:494
typet java_long_type()
Definition: java_types.cpp:42
typet java_int_type()
Definition: java_types.cpp:32
const std::vector< java_annotationt > & get_annotations() const
Definition: java_types.h:70
typet java_array_element_type(const symbol_typet &array_type)
Return the type of the elements of a given java array type.
Definition: java_types.cpp:126
symbol_typet java_classname(const std::string &)
Definition: java_types.cpp:668
nonstd::optional< T > optionalt
Definition: optional.h:35
const java_implicitly_generic_class_typet & to_java_implicitly_generic_class_type(const java_class_typet &type)
Definition: java_types.h:511
API to expression classes.
bool can_cast_type< java_class_typet >(const typet &type)
Definition: java_types.h:176
typet java_bytecode_promotion(const typet &)
Java does not support byte/short return types. These are always promoted.
Definition: java_types.cpp:166
void add_unknown_lambda_method_handle()
Definition: java_types.h:144
#define PRECONDITION(CONDITION)
Definition: invariant.h:230
const generic_typest & generic_types() const
Definition: java_types.h:597
Base class for tree-like data structures with sharing.
Definition: irep.h:86
bool is_java_generic_class_type(const typet &type)
Definition: java_types.h:398
Type for a generic symbol, extends symbol_typet with a vector of java generic types.
Definition: java_types.h:587
const irep_idt & java_generic_class_type_var(size_t index, const java_generic_class_typet &type)
Access information of type variables of a generic java class type.
Definition: java_types.h:440
reference_typet java_lang_object_type()
Definition: java_types.cpp:85
const implicit_generic_typest & implicit_generic_types() const
Definition: java_types.h:487
const typet & java_generic_get_inst_type(size_t index, const java_generic_typet &type)
Access information of type arguments of java instantiated type.
Definition: java_types.h:425
typet java_type_from_string_with_exception(const std::string &descriptor, const optionalt< std::string > &signature, const std::string &class_name)
Definition: java_types.h:538
The reference type.
Definition: std_types.h:1483
Class to hold type with generic type arguments, for example java.util.List in either a reference of t...
Definition: java_types.h:318
std::string erase_type_arguments(const std::string &)
Take a signature string and remove everything in angle brackets allowing for the type to be parsed no...
Definition: java_types.cpp:231
const irep_idt & get_name() const
Definition: java_types.h:33
const java_generic_typet & to_java_generic_type(const typet &type)
Definition: java_types.h:353
const type_variablest & type_variables() const
Definition: java_types.h:266
API to type classes.
std::vector< type_variablet > type_variablest
Definition: java_types.h:265
type_variablest & type_variables()
Definition: java_types.h:271
std::string pretty_signature(const code_typet &)
Definition: java_types.cpp:935
Base class for all expressions.
Definition: expr.h:42
std::vector< java_annotationt > & get_annotations()
Definition: java_types.h:77
bool equal_java_types(const typet &type1, const typet &type2)
Compares the types, including checking element types if both types are arrays.
Definition: java_types.cpp:733
Class to hold a Java generic type parameter (also called type variable), e.g., T in List<T>...
Definition: java_types.h:232
typet java_boolean_type()
Definition: java_types.cpp:72
const irep_idt get_name() const
Definition: java_types.h:259
java_annotationt(const typet &type)
Definition: java_types.h:44
irept & add(const irep_namet &name)
Definition: irep.cpp:306
std::string gather_full_class_name(const std::string &)
Returns the full class name, skipping over the generics.
Definition: java_types.cpp:262
generic_typest & generic_types()
Definition: java_types.h:390
const optionalt< size_t > java_generics_get_index_for_subtype(const std::vector< java_generic_parametert > &gen_types, const irep_idt &identifier)
Get the index in the subtypes array for a given component.
Definition: java_types.h:557
generic_type_argumentst & generic_type_arguments()
Definition: java_types.h:337
const std::vector< valuet > & get_values() const
Definition: java_types.h:54
typet java_type_from_char(char t)
Definition: java_types.cpp:147
bool is_java_generic_type(const typet &type)
Definition: java_types.h:346
java_generic_symbol_typet(const symbol_typet &type, const std::string &base_ref, const std::string &class_name_prefix)
Construct a generic symbol type by extending the symbol type type with generic types extracted from t...
Definition: java_types.cpp:857
bool can_cast_type< annotated_typet >(const typet &type)
Definition: java_types.h:96
C++ class type.
Definition: std_types.h:341
const typet & get_type() const
Definition: java_types.h:49
reference_typet java_reference_type(const typet &subtype)
Definition: java_types.cpp:80
bool is_java_implicitly_generic_class_type(const typet &type)
Definition: java_types.h:503
reference_typet java_array_type(const char subtype)
Definition: java_types.cpp:90
const std::vector< java_annotationt > & get_annotations() const
Definition: java_types.h:150
Type to hold a Java class that is implicitly generic, e.g., an inner class of a generic outer class o...
Definition: java_types.h:470
type_variablet & type_variable_ref()
Definition: java_types.h:253
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
const annotated_typet & to_annotated_type(const typet &type)
Definition: java_types.h:85
bool can_cast_type< class_typet >(const typet &type)
Definition: std_types.h:451
const java_class_typet & to_java_class_type(const typet &type)
Definition: java_types.h:163
const irep_idt & get_identifier() const
Definition: std_types.h:123
const generic_typest & generic_types() const
Definition: java_types.h:385
std::vector< java_generic_parametert > generic_typest
Definition: java_types.h:378