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