cprover
java_types.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include <cctype>
10 #include <iterator>
11 
12 #include <util/prefix.h>
13 #include <util/std_types.h>
14 #include <util/c_types.h>
15 #include <util/std_expr.h>
16 #include <util/ieee_float.h>
17 #include <util/invariant.h>
18 
19 #include "java_types.h"
20 #include "java_utils.h"
21 
22 #ifdef DEBUG
23 #include <iostream>
24 #endif
25 
26 std::vector<typet> parse_list_types(
27  const std::string src,
28  const std::string class_name_prefix,
29  const char opening_bracket,
30  const char closing_bracket);
31 
33 {
34  static const auto result = signedbv_typet(32);
35  return result;
36 }
37 
39 {
40  static const auto result = empty_typet();
41  return result;
42 }
43 
45 {
46  static const auto result = signedbv_typet(64);
47  return result;
48 }
49 
51 {
52  static const auto result = signedbv_typet(16);
53  return result;
54 }
55 
57 {
58  static const auto result = signedbv_typet(8);
59  return result;
60 }
61 
63 {
64  static const auto result = unsignedbv_typet(16);
65  return result;
66 }
67 
69 {
70  static const auto result = ieee_float_spect::single_precision().to_type();
71  return result;
72 }
73 
75 {
76  static const auto result = ieee_float_spect::double_precision().to_type();
77  return result;
78 }
79 
81 {
82  // The Java standard doesn't really prescribe the width
83  // of a boolean. However, JNI suggests that it's 8 bits.
84  // http://docs.oracle.com/javase/7/docs/technotes/guides/jni/spec/types.html
85  static const auto result = c_bool_typet(8);
86  return result;
87 }
88 
90 {
91  return reference_type(subtype);
92 }
93 
95 {
96  return to_java_reference_type(reference_type(subtype));
97 }
98 
100 {
101  static const auto result =
102  java_reference_type(struct_tag_typet("java::java.lang.Object"));
103  return result;
104 }
105 
111 {
112  std::string subtype_str;
113 
114  switch(subtype)
115  {
116  case 'b': subtype_str="byte"; break;
117  case 'f': subtype_str="float"; break;
118  case 'd': subtype_str="double"; break;
119  case 'i': subtype_str="int"; break;
120  case 'c': subtype_str="char"; break;
121  case 's': subtype_str="short"; break;
122  case 'z': subtype_str="boolean"; break;
123  case 'v': subtype_str="void"; break;
124  case 'j': subtype_str="long"; break;
125  case 'l': subtype_str="long"; break;
126  case 'a': subtype_str="reference"; break;
127  default:
128 #ifdef DEBUG
129  std::cout << "Unrecognised subtype str: " << subtype << std::endl;
130 #endif
131  UNREACHABLE;
132  }
133 
134  irep_idt class_name="array["+subtype_str+"]";
135 
136  struct_tag_typet struct_tag_type("java::" + id2string(class_name));
137  struct_tag_type.set(ID_C_base_name, class_name);
138  struct_tag_type.set(ID_element_type, java_type_from_char(subtype));
139 
140  return java_reference_type(struct_tag_type);
141 }
142 
145 const typet &java_array_element_type(const struct_tag_typet &array_symbol)
146 {
148  is_java_array_tag(array_symbol.get_identifier()),
149  "Symbol should have array tag");
150  return array_symbol.find_type(ID_element_type);
151 }
152 
156 {
158  is_java_array_tag(array_symbol.get_identifier()),
159  "Symbol should have array tag");
160  return array_symbol.add_type(ID_element_type);
161 }
162 
164 bool is_java_array_type(const typet &type)
165 {
166  if(
169  {
170  return false;
171  }
172  const auto &subtype_struct_tag = to_struct_tag_type(type.subtype());
173  return is_java_array_tag(subtype_struct_tag.get_identifier());
174 }
175 
180 {
182  to_struct_tag_type(type.subtype())));
183 }
184 
187 std::pair<typet, std::size_t>
189 {
190  std::size_t array_dimensions = 0;
191  typet underlying_type;
192  for(underlying_type = java_reference_type(type);
193  is_java_array_type(underlying_type);
194  underlying_type =
196  {
197  ++array_dimensions;
198  }
199 
200  return {underlying_type, array_dimensions};
201 }
202 
206 {
207  PRECONDITION(pointer.type().id() == ID_pointer);
208 
213 }
214 
218 {
219  PRECONDITION(pointer.type().id() == ID_pointer);
220 
224  return member_exprt(
226 }
227 
232 bool is_java_array_tag(const irep_idt& tag)
233 {
234  return has_prefix(id2string(tag), "java::array[");
235 }
236 
248 {
249  switch(t)
250  {
251  case 'i': return java_int_type();
252  case 'j': return java_long_type();
253  case 'l': return java_long_type();
254  case 's': return java_short_type();
255  case 'b': return java_byte_type();
256  case 'c': return java_char_type();
257  case 'f': return java_float_type();
258  case 'd': return java_double_type();
259  case 'z': return java_boolean_type();
260  case 'a':
262  default:
263  UNREACHABLE;
264  }
265 }
266 
269 {
270  if(type==java_boolean_type() ||
271  type==java_char_type() ||
272  type==java_byte_type() ||
273  type==java_short_type())
274  return java_int_type();
275 
276  return type;
277 }
278 
281 {
282  typet new_type=java_bytecode_promotion(expr.type());
283 
284  if(new_type==expr.type())
285  return expr;
286  else
287  return typecast_exprt(expr, new_type);
288 }
289 
299  java_generic_typet &generic_type,
300  const std::string &type_arguments,
301  const std::string &class_name_prefix)
302 {
303  PRECONDITION(type_arguments.size() >= 2);
304  PRECONDITION(type_arguments[0] == '<');
305  PRECONDITION(type_arguments[type_arguments.size() - 1] == '>');
306 
307  // Parse contained arguments, can be either type parameters (`TT;`)
308  // or instantiated types - either generic types (`LList<LInteger;>;`) or
309  // just references (`Ljava/lang/Foo;`)
310  std::vector<typet> type_arguments_types =
311  parse_list_types(type_arguments, class_name_prefix, '<', '>');
312 
313  // We should have at least one generic type argument
314  CHECK_RETURN(!type_arguments_types.empty());
315 
316  // Add the type arguments to the generic type
317  std::transform(
318  type_arguments_types.begin(),
319  type_arguments_types.end(),
320  std::back_inserter(generic_type.generic_type_arguments()),
321  [](const typet &type) -> reference_typet
322  {
323  INVARIANT(
324  is_reference(type), "All generic type arguments should be references");
325  return to_reference_type(type);
326  });
327 }
328 
333 std::string erase_type_arguments(const std::string &src)
334 {
335  std::string class_name = src;
336  std::size_t f_pos = class_name.find('<', 1);
337 
338  while(f_pos != std::string::npos)
339  {
340  std::size_t e_pos = find_closing_delimiter(class_name, f_pos, '<', '>');
341  if(e_pos == std::string::npos)
342  {
344  "Failed to find generic signature closing delimiter (or recursive "
345  "generic): " +
346  src);
347  }
348 
349  // erase generic information between brackets
350  class_name.erase(f_pos, e_pos - f_pos + 1);
351 
352  // Search the remainder of the string for generic signature
353  f_pos = class_name.find('<', f_pos + 1);
354  }
355  return class_name;
356 }
357 
364 std::string gather_full_class_name(const std::string &src)
365 {
366  PRECONDITION(src.size() >= 2);
367  PRECONDITION(src[0] == 'L');
368  PRECONDITION(src[src.size() - 1] == ';');
369 
370  std::string class_name = src.substr(1, src.size() - 2);
371 
372  class_name = erase_type_arguments(class_name);
373 
374  std::replace(class_name.begin(), class_name.end(), '.', '$');
375  std::replace(class_name.begin(), class_name.end(), '/', '.');
376  return class_name;
377 }
378 
391 std::vector<typet> parse_list_types(
392  const std::string src,
393  const std::string class_name_prefix,
394  const char opening_bracket,
395  const char closing_bracket)
396 {
397  // Loop over the types in the given string, parsing each one in turn
398  // and adding to the type_list
399  std::vector<typet> type_list;
400  for(const std::string &raw_type :
401  parse_raw_list_types(src, opening_bracket, closing_bracket))
402  {
403  auto new_type = java_type_from_string(raw_type, class_name_prefix);
404  INVARIANT(new_type.has_value(), "Failed to parse type");
405  type_list.push_back(std::move(*new_type));
406  }
407  return type_list;
408 }
409 
418 std::vector<std::string> parse_raw_list_types(
419  const std::string src,
420  const char opening_bracket,
421  const char closing_bracket)
422 {
423  PRECONDITION(src.size() >= 2);
424  PRECONDITION(src[0] == opening_bracket);
425  PRECONDITION(src[src.size() - 1] == closing_bracket);
426 
427  // Loop over the types in the given string, parsing each one in turn
428  // and adding to the type_list
429  std::vector<std::string> type_list;
430  for(std::size_t i = 1; i < src.size() - 1; i++)
431  {
432  size_t start = i;
433  while(i < src.size())
434  {
435  // type is an object type or instantiated generic type
436  if(src[i] == 'L')
437  {
439  break;
440  }
441 
442  // type is an array
443  else if(src[i] == '[')
444  i++;
445 
446  // type is a type variable/parameter
447  else if(src[i] == 'T')
448  i = src.find(';', i); // ends on ;
449 
450  // type is an atomic type (just one character)
451  else
452  {
453  break;
454  }
455  }
456 
457  std::string sub_str = src.substr(start, i - start + 1);
458  type_list.emplace_back(sub_str);
459  }
460  return type_list;
461 }
462 
471 build_class_name(const std::string &src, const std::string &class_name_prefix)
472 {
473  PRECONDITION(src[0] == 'L');
474 
475  // All reference types must end on a ;
476  PRECONDITION(src[src.size() - 1] == ';');
477 
478  std::string container_class = gather_full_class_name(src);
479  std::string identifier = "java::" + container_class;
480  struct_tag_typet struct_tag_type(identifier);
481  struct_tag_type.set(ID_C_base_name, container_class);
482 
483  std::size_t f_pos = src.find('<', 1);
484  if(f_pos != std::string::npos)
485  {
486  java_generic_typet result(struct_tag_type);
487  // get generic type information
488  do
489  {
490  std::size_t e_pos = find_closing_delimiter(src, f_pos, '<', '>');
491  if(e_pos == std::string::npos)
493  "Parsing type with unmatched generic bracket: " + src);
494 
496  result, src.substr(f_pos, e_pos - f_pos + 1), class_name_prefix);
497 
498  // Look for the next generic type info (if it exists)
499  f_pos = src.find('<', e_pos + 1);
500  } while(f_pos != std::string::npos);
501  return std::move(result);
502  }
503 
504  return java_reference_type(struct_tag_type);
505 }
506 
516  const std::string src,
517  size_t starting_point)
518 {
519  PRECONDITION(src[starting_point] == 'L');
520  size_t next_semi_colon = src.find(';', starting_point);
521  INVARIANT(
522  next_semi_colon != std::string::npos,
523  "There must be a semi-colon somewhere in the input");
524  size_t next_angle_bracket = src.find('<', starting_point);
525 
526  while(next_angle_bracket < next_semi_colon)
527  {
528  size_t end_bracket =
529  find_closing_delimiter(src, next_angle_bracket, '<', '>');
530  INVARIANT(
531  end_bracket != std::string::npos, "Must find matching angle bracket");
532 
533  next_semi_colon = src.find(';', end_bracket + 1);
534  next_angle_bracket = src.find('<', end_bracket + 1);
535  }
536 
537  return next_semi_colon;
538 }
539 
541 {
543  result.subtype().set(ID_element_type, java_reference_type(subtype));
544  return result;
545 }
546 
561  const std::string &src,
562  const std::string &class_name_prefix)
563 {
564  if(src.empty())
565  return {};
566 
567  // a java type is encoded in different ways
568  // - a method type is encoded as '(...)R' where the parenthesis include the
569  // parameter types and R is the type of the return value
570  // - atomic types are encoded as single characters
571  // - array types are encoded as '[' followed by the type of the array
572  // content
573  // - object types are named with prefix 'L' and suffix ';', e.g.,
574  // Ljava/lang/Object;
575  // - type variables are similar to object types but have the prefix 'T'
576  switch(src[0])
577  {
578  case '<':
579  {
580  // The method signature can optionally have a collection of formal
581  // type parameters (e.g. on generic methods on non-generic classes
582  // or generic static methods). For now we skip over this part of the
583  // signature and continue parsing the rest of the signature as normal
584  // So for example, the following java method:
585  // static void <T, U> foo(T t, U u, int x);
586  // Would have a signature that looks like:
587  // <T:Ljava/lang/Object;U:Ljava/lang/Object;>(TT;TU;I)V
588  // So we skip all inside the angle brackets and parse the rest of the
589  // string:
590  // (TT;TU;I)V
591  size_t closing_generic=find_closing_delimiter(src, 0, '<', '>');
592  if(closing_generic==std::string::npos)
593  {
595  "Failed to find generic signature closing delimiter");
596  }
597 
598  // If there are any bounds between '<' and '>' then we cannot currently
599  // parse them, so we give up. This only happens when parsing the
600  // signature, so we'll fall back to the result of parsing the
601  // descriptor, which will respect the bounds correctly.
602  const size_t colon_pos = src.find(':');
603  if(colon_pos != std::string::npos && colon_pos < closing_generic)
604  {
606  "Cannot currently parse bounds on generic types");
607  }
608 
609  auto method_type = java_type_from_string(
610  src.substr(closing_generic + 1, std::string::npos), class_name_prefix);
611 
612  // This invariant being violated means that tkiley has not understood
613  // part of the signature spec.
614  // Only class and method signatures can start with a '<' and classes are
615  // handled separately.
616  INVARIANT(
617  method_type.has_value() && method_type->id() == ID_code,
618  "This should correspond to method signatures only");
619 
620  return method_type;
621  }
622  case '(': // function type
623  {
624  std::size_t e_pos=src.rfind(')');
625  if(e_pos==std::string::npos)
626  return {};
627 
628  auto return_type = java_type_from_string(
629  std::string(src, e_pos + 1, std::string::npos), class_name_prefix);
630 
631  std::vector<typet> param_types =
632  parse_list_types(src.substr(0, e_pos + 1), class_name_prefix, '(', ')');
633 
634  // create parameters for each type
636  std::transform(
637  param_types.begin(),
638  param_types.end(),
639  std::back_inserter(parameters),
640  [](const typet &type) { return java_method_typet::parametert(type); });
641 
642  return java_method_typet(std::move(parameters), std::move(*return_type));
643  }
644 
645  case '[': // array type
646  {
647  // If this is a reference array, we generate a plain array[reference]
648  // with void* members, but note the real type in ID_element_type.
649  if(src.size()<=1)
650  return {};
651  char subtype_letter=src[1];
652  auto subtype = java_type_from_string(
653  src.substr(1, std::string::npos), class_name_prefix);
654  if(subtype_letter=='L' || // [L denotes a reference array of some sort.
655  subtype_letter=='[' || // Array-of-arrays
656  subtype_letter=='T') // Array of generic types
657  subtype_letter='A';
658  subtype_letter = std::tolower(subtype_letter);
659  if(subtype_letter == 'a')
660  {
662  to_struct_tag_type(subtype->subtype()));
663  }
664  else
665  return java_array_type(subtype_letter);
666  }
667 
668  case 'B': return java_byte_type();
669  case 'F': return java_float_type();
670  case 'D': return java_double_type();
671  case 'I': return java_int_type();
672  case 'C': return java_char_type();
673  case 'S': return java_short_type();
674  case 'Z': return java_boolean_type();
675  case 'V': return java_void_type();
676  case 'J': return java_long_type();
677  case 'T':
678  {
679  // parse name of type variable
680  INVARIANT(src[src.size()-1]==';', "Generic type name must end on ';'.");
681  PRECONDITION(!class_name_prefix.empty());
682  irep_idt type_var_name(class_name_prefix+"::"+src.substr(1, src.size()-2));
684  type_var_name,
686  java_type_from_string("Ljava/lang/Object;")->subtype()));
687  }
688  case 'L':
689  {
690  return build_class_name(src, class_name_prefix);
691  }
692  case '*':
693  case '+':
694  case '-':
695  {
696 #ifdef DEBUG
697  std::cout << class_name_prefix << std::endl;
698 #endif
699  throw unsupported_java_class_signature_exceptiont("wild card generic");
700  }
701  default:
702  return {};
703  }
704 }
705 
706 char java_char_from_type(const typet &type)
707 {
708  const irep_idt &id=type.id();
709 
710  if(id==ID_signedbv)
711  {
712  const size_t width=to_signedbv_type(type).get_width();
713  if(java_int_type().get_width() == width)
714  return 'i';
715  else if(java_long_type().get_width() == width)
716  return 'l';
717  else if(java_short_type().get_width() == width)
718  return 's';
719  else if(java_byte_type().get_width() == width)
720  return 'b';
721  }
722  else if(id==ID_unsignedbv)
723  return 'c';
724  else if(id==ID_floatbv)
725  {
726  const size_t width(to_floatbv_type(type).get_width());
727  if(java_float_type().get_width() == width)
728  return 'f';
729  else if(java_double_type().get_width() == width)
730  return 'd';
731  }
732  else if(id==ID_c_bool)
733  return 'z';
734 
735  return 'a';
736 }
737 
747 std::vector<typet> java_generic_type_from_string(
748  const std::string &class_name,
749  const std::string &src)
750 {
753  size_t signature_end = find_closing_delimiter(src, 0, '<', '>');
754  INVARIANT(
755  src[0]=='<' && signature_end!=std::string::npos,
756  "Class signature has unexpected format");
757  std::string signature(src.substr(1, signature_end-1));
758 
759  if(signature.find(";:")!=std::string::npos)
760  throw unsupported_java_class_signature_exceptiont("multiple bounds");
761 
762  PRECONDITION(signature[signature.size()-1]==';');
763 
764  std::vector<typet> types;
765  size_t var_sep=signature.find(';');
766  while(var_sep!=std::string::npos)
767  {
768  size_t bound_sep=signature.find(':');
769  INVARIANT(bound_sep!=std::string::npos, "No bound for type variable.");
770 
771  // is bound an interface?
772  // in this case the separator is '::'
773  if(signature[bound_sep + 1] == ':')
774  {
775  INVARIANT(
776  signature[bound_sep + 2] != ':', "Unknown bound for type variable.");
777  bound_sep++;
778  }
779 
780  std::string type_var_name(
781  "java::"+class_name+"::"+signature.substr(0, bound_sep));
782  std::string bound_type(signature.substr(bound_sep+1, var_sep-bound_sep));
783 
784  java_generic_parametert type_var_type(
785  type_var_name,
787  java_type_from_string(bound_type, class_name)->subtype()));
788 
789  types.push_back(type_var_type);
790  signature=signature.substr(var_sep+1, std::string::npos);
791  var_sep=signature.find(';');
792  }
793  return types;
794 }
795 
796 // java/lang/Object -> java.lang.Object
797 static std::string slash_to_dot(const std::string &src)
798 {
799  std::string result=src;
800  for(std::string::iterator it=result.begin(); it!=result.end(); it++)
801  if(*it=='/')
802  *it='.';
803  return result;
804 }
805 
806 struct_tag_typet java_classname(const std::string &id)
807 {
808  if(!id.empty() && id[0]=='[')
809  return to_struct_tag_type(java_type_from_string(id)->subtype());
810 
811  std::string class_name=id;
812 
813  class_name=slash_to_dot(class_name);
814  irep_idt identifier="java::"+class_name;
815  struct_tag_typet struct_tag_type(identifier);
816  struct_tag_type.set(ID_C_base_name, class_name);
817 
818  return struct_tag_type;
819 }
820 
835 {
836  bool correct_num_components =
837  type.components().size() ==
838  (type.get_tag() == JAVA_REFERENCE_ARRAY_CLASSID ? 5 : 3);
839  if(!correct_num_components)
840  return false;
841 
842  // First component, the base class (Object) data
843  const struct_union_typet::componentt base_class_component=
844  type.components()[0];
845 
846  if(base_class_component.get_name() != "@java.lang.Object")
847  return false;
848 
849  const struct_union_typet::componentt length_component=
850  type.components()[1];
851  if(length_component.get_name() != "length")
852  return false;
853  if(length_component.type() != java_int_type())
854  return false;
855 
856  const struct_union_typet::componentt data_component=
857  type.components()[2];
858  if(data_component.get_name() != "data")
859  return false;
860  if(data_component.type().id() != ID_pointer)
861  return false;
862 
864  {
865  const struct_union_typet::componentt array_element_type_component =
866  type.components()[3];
867  if(
868  array_element_type_component.get_name() !=
870  return false;
871  if(array_element_type_component.type() != string_typet())
872  return false;
873 
874  const struct_union_typet::componentt array_dimension_component =
875  type.components()[4];
876  if(array_dimension_component.get_name() != JAVA_ARRAY_DIMENSION_FIELD_NAME)
877  return false;
878  if(array_dimension_component.type() != java_int_type())
879  return false;
880  }
881 
882  return true;
883 }
884 
891 bool equal_java_types(const typet &type1, const typet &type2)
892 {
893  bool arrays_with_same_element_type = true;
894  if(
895  type1.id() == ID_pointer && type2.id() == ID_pointer &&
896  type1.subtype().id() == ID_struct_tag &&
897  type2.subtype().id() == ID_struct_tag)
898  {
899  const auto &subtype_symbol1 = to_struct_tag_type(type1.subtype());
900  const auto &subtype_symbol2 = to_struct_tag_type(type2.subtype());
901  if(
902  subtype_symbol1.get_identifier() == subtype_symbol2.get_identifier() &&
903  is_java_array_tag(subtype_symbol1.get_identifier()))
904  {
905  const typet &array_element_type1 =
906  java_array_element_type(subtype_symbol1);
907  const typet &array_element_type2 =
908  java_array_element_type(subtype_symbol2);
909 
910  arrays_with_same_element_type =
911  equal_java_types(array_element_type1, array_element_type2);
912  }
913  }
914  return (type1 == type2 && arrays_with_same_element_type);
915 }
916 
917 std::vector<java_generic_parametert>
919 {
920  std::vector<java_generic_parametert> generic_parameters;
922  {
923  const java_implicitly_generic_class_typet &implicitly_generic_class =
925  generic_parameters.insert(
926  generic_parameters.end(),
927  implicitly_generic_class.implicit_generic_types().begin(),
928  implicitly_generic_class.implicit_generic_types().end());
929  }
931  {
932  const java_generic_class_typet &generic_class =
934  generic_parameters.insert(
935  generic_parameters.end(),
936  generic_class.generic_types().begin(),
937  generic_class.generic_types().end());
938  }
939  return generic_parameters;
940 }
941 
943  const typet &t,
944  std::set<irep_idt> &refs)
945 {
946  // Java generic type that holds different types in its type arguments
947  if(is_java_generic_type(t))
948  {
949  for(const auto &type_arg : to_java_generic_type(t).generic_type_arguments())
951  }
952 
953  // Java reference type
954  else if(t.id() == ID_pointer)
955  {
957  }
958 
959  // method type with parameters and return value
960  else if(t.id() == ID_code)
961  {
964  for(const auto &param : c.parameters())
966  }
967 
968  // struct tag
969  else if(t.id() == ID_struct_tag)
970  {
971  const auto &struct_tag_type = to_struct_tag_type(t);
972  const irep_idt class_name(struct_tag_type.get_identifier());
973  if(is_java_array_tag(class_name))
974  {
976  java_array_element_type(struct_tag_type), refs);
977  }
978  else
979  refs.insert(strip_java_namespace_prefix(class_name));
980  }
981 }
982 
990  const std::string &signature,
991  std::set<irep_idt> &refs)
992 {
993  try
994  {
995  // class signature with bounds
996  if(signature[0] == '<')
997  {
998  const std::vector<typet> types = java_generic_type_from_string(
999  erase_type_arguments(signature), signature);
1000 
1001  for(const auto &t : types)
1003  }
1004 
1005  // class signature without bounds and without wildcards
1006  else if(signature.find('*') == std::string::npos)
1007  {
1008  auto type_from_string =
1009  java_type_from_string(signature, erase_type_arguments(signature));
1010  get_dependencies_from_generic_parameters_rec(*type_from_string, refs);
1011  }
1012  }
1014  {
1015  // skip for now, if we cannot parse it, we cannot detect which additional
1016  // classes should be loaded as dependencies
1017  }
1018 }
1019 
1026  const typet &t,
1027  std::set<irep_idt> &refs)
1028 {
1030 }
1031 
1042  const struct_tag_typet &type,
1043  const std::string &base_ref,
1044  const std::string &class_name_prefix)
1045  : struct_tag_typet(type)
1046 {
1047  set(ID_C_java_generic_symbol, true);
1048  const auto base_type = java_type_from_string(base_ref, class_name_prefix);
1050  const java_generic_typet &gen_base_type = to_java_generic_type(*base_type);
1051  INVARIANT(
1052  type.get_identifier() ==
1053  to_struct_tag_type(gen_base_type.subtype()).get_identifier(),
1054  "identifier of " + type.pretty() + "\n and identifier of type " +
1055  gen_base_type.subtype().pretty() +
1056  "\ncreated by java_type_from_string for " + base_ref +
1057  " should be equal");
1058  generic_types().insert(
1059  generic_types().end(),
1060  gen_base_type.generic_type_arguments().begin(),
1061  gen_base_type.generic_type_arguments().end());
1062 }
1063 
1069  const java_generic_parametert &type) const
1070 {
1071  const auto &type_variable = type.get_name();
1072  const auto &generics = generic_types();
1073  for(std::size_t i = 0; i < generics.size(); ++i)
1074  {
1075  auto param = type_try_dynamic_cast<java_generic_parametert>(generics[i]);
1076  if(param && param->get_name() == type_variable)
1077  return i;
1078  }
1079  return {};
1080 }
1081 
1082 std::string pretty_java_type(const typet &type)
1083 {
1084  if(type == java_void_type())
1085  return "void";
1086  if(type == java_int_type())
1087  return "int";
1088  else if(type == java_long_type())
1089  return "long";
1090  else if(type == java_short_type())
1091  return "short";
1092  else if(type == java_byte_type())
1093  return "byte";
1094  else if(type == java_char_type())
1095  return "char";
1096  else if(type == java_float_type())
1097  return "float";
1098  else if(type == java_double_type())
1099  return "double";
1100  else if(type == java_boolean_type())
1101  return "boolean";
1102  else if(type == java_byte_type())
1103  return "byte";
1104  else if(is_reference(type))
1105  {
1106  if(type.subtype().id() == ID_struct_tag)
1107  {
1108  const auto &struct_tag_type = to_struct_tag_type(type.subtype());
1109  const irep_idt &id = struct_tag_type.get_identifier();
1110  if(is_java_array_tag(id))
1111  return pretty_java_type(java_array_element_type(struct_tag_type)) +
1112  "[]";
1113  else
1115  }
1116  else
1117  return "?";
1118  }
1119  else
1120  return "?";
1121 }
1122 
1123 std::string pretty_signature(const java_method_typet &method_type)
1124 {
1125  std::ostringstream result;
1126  result << '(';
1127 
1128  bool first = true;
1129  for(const auto &p : method_type.parameters())
1130  {
1131  if(p.get_this())
1132  continue;
1133 
1134  if(first)
1135  first = false;
1136  else
1137  result << ", ";
1138 
1139  result << pretty_java_type(p.type());
1140  }
1141 
1142  result << ')';
1143  return result.str();
1144 }
tag_typet::get_identifier
const irep_idt & get_identifier() const
Definition: std_types.h:451
is_java_generic_class_type
bool is_java_generic_class_type(const typet &type)
Definition: java_types.h:995
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:142
get_dependencies_from_generic_parameters_rec
void get_dependencies_from_generic_parameters_rec(const typet &t, std::set< irep_idt > &refs)
Definition: java_types.cpp:942
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
JAVA_ARRAY_ELEMENT_CLASSID_FIELD_NAME
#define JAVA_ARRAY_ELEMENT_CLASSID_FIELD_NAME
Definition: java_types.h:673
get_dependencies_from_generic_parameters
void get_dependencies_from_generic_parameters(const std::string &signature, std::set< irep_idt > &refs)
Collect information about generic type parameters from a given signature.
Definition: java_types.cpp:989
java_char_from_type
char java_char_from_type(const typet &type)
Definition: java_types.cpp:706
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2021
typet::subtype
const typet & subtype() const
Definition: type.h:47
java_generic_typet
Reference that points to a java_generic_struct_tag_typet.
Definition: java_types.h:916
JAVA_ARRAY_DIMENSION_FIELD_NAME
#define JAVA_ARRAY_DIMENSION_FIELD_NAME
Definition: java_types.h:671
java_reference_type
reference_typet java_reference_type(const typet &subtype)
Definition: java_types.cpp:89
get_array_dimension_field
exprt get_array_dimension_field(const exprt &pointer)
Definition: java_types.cpp:205
reference_typet
The reference type.
Definition: std_types.h:1553
java_implicitly_generic_class_typet::implicit_generic_types
const implicit_generic_typest & implicit_generic_types() const
Definition: java_types.h:1084
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
typet
The type of an expression, extends irept.
Definition: type.h:29
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:488
java_long_type
signedbv_typet java_long_type()
Definition: java_types.cpp:44
java_array_element_type
const typet & java_array_element_type(const struct_tag_typet &array_symbol)
Return a const reference to the element type of a given java array type.
Definition: java_types.cpp:145
dereference_exprt
Operator to dereference a pointer.
Definition: std_expr.h:2888
unsupported_java_class_signature_exceptiont
An exception that is raised for unsupported class signature.
Definition: java_types.h:1132
floatbv_typet
Fixed-width bit-vector with IEEE floating-point interpretation.
Definition: std_types.h:1379
is_multidim_java_array_type
bool is_multidim_java_array_type(const typet &type)
Checks whether the given type is a multi-dimensional array pointer type, i.e., a pointer to an array ...
Definition: java_types.cpp:179
java_classname
struct_tag_typet java_classname(const std::string &id)
Definition: java_types.cpp:806
prefix.h
replace
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
Definition: string_constraint.cpp:67
java_generic_parametert
Reference that points to a java_generic_parameter_tagt.
Definition: java_types.h:778
invariant.h
java_method_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:738
is_valid_java_array
bool is_valid_java_array(const struct_typet &type)
Programmatic documentation of the structure of a Java array (of either primitives or references) type...
Definition: java_types.cpp:834
exprt
Base class for all expressions.
Definition: expr.h:53
is_java_array_tag
bool is_java_array_tag(const irep_idt &tag)
See above.
Definition: java_types.cpp:232
struct_tag_typet
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:490
parse_raw_list_types
std::vector< std::string > parse_raw_list_types(const std::string src, const char opening_bracket, const char closing_bracket)
Given a substring of a descriptor or signature that contains one or more types parse out the individu...
Definition: java_types.cpp:418
is_java_implicitly_generic_class_type
bool is_java_implicitly_generic_class_type(const typet &type)
Definition: java_types.h:1100
to_java_generic_class_type
const java_generic_class_typet & to_java_generic_class_type(const java_class_typet &type)
Definition: java_types.h:1003
java_generic_struct_tag_typet::generic_type_index
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:1068
java_generic_struct_tag_typet::generic_types
const generic_typest & generic_types() const
Definition: java_types.h:874
unsignedbv_typet
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1216
java_generic_class_typet::generic_types
const generic_typest & generic_types() const
Definition: java_types.h:982
c_bool_typet
The C/C++ Booleans.
Definition: std_types.h:1604
strip_java_namespace_prefix
irep_idt strip_java_namespace_prefix(const irep_idt &to_strip)
Strip java:: prefix from given identifier.
Definition: java_utils.cpp:417
erase_type_arguments
std::string erase_type_arguments(const std::string &src)
Take a signature string and remove everything in angle brackets allowing for the type to be parsed no...
Definition: java_types.cpp:333
find_closing_delimiter
size_t find_closing_delimiter(const std::string &src, size_t open_pos, char open_char, char close_char)
Finds the corresponding closing delimiter to the given opening delimiter.
Definition: java_utils.cpp:312
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
java_generic_parametert::get_name
const irep_idt get_name() const
Definition: java_types.h:801
struct_union_typet::get_tag
irep_idt get_tag() const
Definition: std_types.h:163
equal_java_types
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:891
java_type_from_char
typet java_type_from_char(char t)
Constructs a type indicated by the given character:
Definition: java_types.cpp:247
messaget::result
mstreamt & result() const
Definition: message.h:409
java_generic_struct_tag_typet::java_generic_struct_tag_typet
java_generic_struct_tag_typet(const struct_tag_typet &type)
Definition: java_types.h:863
ieee_float_spect::double_precision
static ieee_float_spect double_precision()
Definition: ieee_float.h:80
empty_typet
The empty type.
Definition: std_types.h:46
base_type
void base_type(typet &type, const namespacet &ns)
Definition: base_type.cpp:109
java_generic_typet::generic_type_arguments
const generic_type_argumentst & generic_type_arguments() const
Definition: java_types.h:927
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
struct_union_typet::componentt::get_name
const irep_idt & get_name() const
Definition: std_types.h:74
find_closing_semi_colon_for_reference_type
size_t find_closing_semi_colon_for_reference_type(const std::string src, size_t starting_point)
Finds the closing semi-colon ending a ClassTypeSignature that starts at starting_point.
Definition: java_types.cpp:515
can_cast_type< struct_tag_typet >
bool can_cast_type< struct_tag_typet >(const typet &type)
Check whether a reference to a typet is a struct_tag_typet.
Definition: std_types.h:502
ieee_float_spect::to_type
class floatbv_typet to_type() const
Definition: ieee_float.cpp:25
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
signedbv_typet
Fixed-width bit-vector with two's complement interpretation.
Definition: std_types.h:1265
to_java_reference_type
const java_reference_typet & to_java_reference_type(const typet &type)
Definition: java_types.h:632
std_types.h
Pre-defined types.
java_array_type
java_reference_typet java_array_type(const char subtype)
Construct an array pointer type.
Definition: java_types.cpp:110
build_class_name
reference_typet build_class_name(const std::string &src, const std::string &class_name_prefix)
For parsing a class type reference.
Definition: java_types.cpp:471
is_java_generic_type
bool is_java_generic_type(const typet &type)
Definition: java_types.h:947
java_implicitly_generic_class_typet
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:1068
is_java_array_type
bool is_java_array_type(const typet &type)
Checks whether the given type is an array pointer type.
Definition: java_types.cpp:164
pretty_java_type
std::string pretty_java_type(const typet &type)
Definition: java_types.cpp:1082
pretty_signature
std::string pretty_signature(const java_method_typet &method_type)
Definition: java_types.cpp:1123
irept::id
const irep_idt & id() const
Definition: irep.h:418
to_struct_tag_type
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:515
java_reference_array_type
java_reference_typet java_reference_array_type(const struct_tag_typet &subtype)
Definition: java_types.cpp:540
java_int_type
signedbv_typet java_int_type()
Definition: java_types.cpp:32
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:857
parse_list_types
std::vector< typet > parse_list_types(const std::string src, const std::string class_name_prefix, const char opening_bracket, const char closing_bracket)
Given a substring of a descriptor or signature that contains one or more types parse out the individu...
Definition: java_types.cpp:391
java_lang_object_type
java_reference_typet java_lang_object_type()
Definition: java_types.cpp:99
to_java_generic_type
const java_generic_typet & to_java_generic_type(const typet &type)
Definition: java_types.h:954
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
java_type_from_string
optionalt< typet > java_type_from_string(const std::string &src, const std::string &class_name_prefix)
Transforms a string representation of a Java type into an internal type representation thereof.
Definition: java_types.cpp:560
get_all_generic_parameters
std::vector< java_generic_parametert > get_all_generic_parameters(const typet &type)
Definition: java_types.cpp:918
java_short_type
signedbv_typet java_short_type()
Definition: java_types.cpp:50
java_byte_type
signedbv_typet java_byte_type()
Definition: java_types.cpp:56
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:1041
can_cast_type< pointer_typet >
bool can_cast_type< pointer_typet >(const typet &type)
Check whether a reference to a typet is a pointer_typet.
Definition: std_types.h:1513
reference_type
reference_typet reference_type(const typet &subtype)
Definition: c_types.cpp:248
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3405
struct_union_typet::componentt
Definition: std_types.h:64
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:226
java_double_type
floatbv_typet java_double_type()
Definition: java_types.cpp:74
is_reference
bool is_reference(const typet &type)
Returns true if the type is a reference.
Definition: std_types.cpp:133
gather_full_class_name
std::string gather_full_class_name(const std::string &src)
Returns the full class name, skipping over the generics.
Definition: java_types.cpp:364
JAVA_REFERENCE_ARRAY_CLASSID
#define JAVA_REFERENCE_ARRAY_CLASSID
Definition: java_types.h:658
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:442
ieee_float.h
java_char_type
unsignedbv_typet java_char_type()
Definition: java_types.cpp:62
slash_to_dot
static std::string slash_to_dot(const std::string &src)
Definition: java_types.cpp:797
string_typet
String type.
Definition: std_types.h:1655
to_signedbv_type
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
Definition: std_types.h:1298
java_bytecode_promotion
typet java_bytecode_promotion(const typet &type)
Java does not support byte/short return types. These are always promoted.
Definition: java_types.cpp:268
to_java_implicitly_generic_class_type
const java_implicitly_generic_class_typet & to_java_implicitly_generic_class_type(const java_class_typet &type)
Definition: java_types.h:1108
to_floatbv_type
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition: std_types.h:1424
java_boolean_type
c_bool_typet java_boolean_type()
Definition: java_types.cpp:80
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:847
java_array_dimension_and_element_type
std::pair< typet, std::size_t > java_array_dimension_and_element_type(const struct_tag_typet &type)
Returns the underlying element type and array dimensionality of Java struct type.
Definition: java_types.cpp:188
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
typet::add_type
typet & add_type(const irep_namet &name)
Definition: type.h:81
java_reference_typet
This is a specialization of reference_typet.
Definition: java_types.h:605
java_generic_class_typet
Class to hold a class with generics, extends the java class type with a vector of java generic type p...
Definition: java_types.h:973
to_java_class_type
const java_class_typet & to_java_class_type(const typet &type)
Definition: java_types.h:584
java_types.h
to_java_method_type
const java_method_typet & to_java_method_type(const typet &type)
Definition: java_types.h:186
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2013
get_array_element_type_field
exprt get_array_element_type_field(const exprt &pointer)
Definition: java_types.cpp:217
typet::find_type
const typet & find_type(const irep_namet &name) const
Definition: type.h:86
java_void_type
empty_typet java_void_type()
Definition: java_types.cpp:38
java_utils.h
java_generic_type_from_string
std::vector< typet > java_generic_type_from_string(const std::string &class_name, const std::string &src)
Converts the content of a generic class type into a vector of Java types, that is each type variable ...
Definition: java_types.cpp:747
std_expr.h
API to expression classes.
ieee_float_spect::single_precision
static ieee_float_spect single_precision()
Definition: ieee_float.h:74
java_method_typet
Definition: java_types.h:103
c_types.h
java_float_type
floatbv_typet java_float_type()
Definition: java_types.cpp:68
validation_modet::INVARIANT
@ INVARIANT
add_generic_type_information
void add_generic_type_information(java_generic_typet &generic_type, const std::string &type_arguments, const std::string &class_name_prefix)
Take a list of generic type arguments and parse them into the generic type.
Definition: java_types.cpp:298