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  return signedbv_typet(32);
35 }
36 
38 {
39  return void_typet();
40 }
41 
43 {
44  return signedbv_typet(64);
45 }
46 
48 {
49  return signedbv_typet(16);
50 }
51 
53 {
54  return signedbv_typet(8);
55 }
56 
58 {
59  return unsignedbv_typet(16);
60 }
61 
63 {
65 }
66 
68 {
70 }
71 
73 {
74  // The Java standard doesn't really prescribe the width
75  // of a boolean. However, JNI suggests that it's 8 bits.
76  // http://docs.oracle.com/javase/7/docs/technotes/guides/jni/spec/types.html
77  return c_bool_typet(8);
78 }
79 
81 {
82  return reference_type(subtype);
83 }
84 
86 {
87  return java_reference_type(struct_tag_typet("java::java.lang.Object"));
88 }
89 
94 reference_typet java_array_type(const char subtype)
95 {
96  std::string subtype_str;
97 
98  switch(subtype)
99  {
100  case 'b': subtype_str="byte"; break;
101  case 'f': subtype_str="float"; break;
102  case 'd': subtype_str="double"; break;
103  case 'i': subtype_str="int"; break;
104  case 'c': subtype_str="char"; break;
105  case 's': subtype_str="short"; break;
106  case 'z': subtype_str="boolean"; break;
107  case 'v': subtype_str="void"; break;
108  case 'j': subtype_str="long"; break;
109  case 'l': subtype_str="long"; break;
110  case 'a': subtype_str="reference"; break;
111  default:
112 #ifdef DEBUG
113  std::cout << "Unrecognised subtype str: " << subtype << std::endl;
114 #endif
115  UNREACHABLE;
116  }
117 
118  irep_idt class_name="array["+subtype_str+"]";
119 
120  struct_tag_typet struct_tag_type("java::" + id2string(class_name));
121  struct_tag_type.set(ID_C_base_name, class_name);
122  struct_tag_type.set(ID_element_type, java_type_from_char(subtype));
123 
124  return java_reference_type(struct_tag_type);
125 }
126 
129 const typet &java_array_element_type(const struct_tag_typet &array_symbol)
130 {
132  is_java_array_tag(array_symbol.get_identifier()),
133  "Symbol should have array tag");
134  return array_symbol.find_type(ID_element_type);
135 }
136 
140 {
142  is_java_array_tag(array_symbol.get_identifier()),
143  "Symbol should have array tag");
144  return array_symbol.add_type(ID_element_type);
145 }
146 
148 bool is_java_array_type(const typet &type)
149 {
150  if(
153  {
154  return false;
155  }
156  const auto &subtype_struct_tag = to_struct_tag_type(type.subtype());
157  return is_java_array_tag(subtype_struct_tag.get_identifier());
158 }
159 
161 // i.e., a pointer to an array type with element type also being a pointer to an
164 {
166  to_struct_tag_type(type.subtype())));
167 }
168 
173 bool is_java_array_tag(const irep_idt& tag)
174 {
175  return has_prefix(id2string(tag), "java::array[");
176 }
177 
189 {
190  switch(t)
191  {
192  case 'i': return java_int_type();
193  case 'j': return java_long_type();
194  case 'l': return java_long_type();
195  case 's': return java_short_type();
196  case 'b': return java_byte_type();
197  case 'c': return java_char_type();
198  case 'f': return java_float_type();
199  case 'd': return java_double_type();
200  case 'z': return java_boolean_type();
201  case 'a': return java_reference_type(void_typet());
202  default: UNREACHABLE; return nil_typet();
203  }
204 }
205 
208 {
209  if(type==java_boolean_type() ||
210  type==java_char_type() ||
211  type==java_byte_type() ||
212  type==java_short_type())
213  return java_int_type();
214 
215  return type;
216 }
217 
220 {
221  typet new_type=java_bytecode_promotion(expr.type());
222 
223  if(new_type==expr.type())
224  return expr;
225  else
226  return typecast_exprt(expr, new_type);
227 }
228 
238  java_generic_typet &generic_type,
239  const std::string &type_arguments,
240  const std::string &class_name_prefix)
241 {
242  PRECONDITION(type_arguments.size() >= 2);
243  PRECONDITION(type_arguments[0] == '<');
244  PRECONDITION(type_arguments[type_arguments.size() - 1] == '>');
245 
246  // Parse contained arguments, can be either type parameters (`TT;`)
247  // or instantiated types - either generic types (`LList<LInteger;>;`) or
248  // just references (`Ljava/lang/Foo;`)
249  std::vector<typet> type_arguments_types =
250  parse_list_types(type_arguments, class_name_prefix, '<', '>');
251 
252  // We should have at least one generic type argument
253  CHECK_RETURN(!type_arguments_types.empty());
254 
255  // Add the type arguments to the generic type
256  std::transform(
257  type_arguments_types.begin(),
258  type_arguments_types.end(),
259  std::back_inserter(generic_type.generic_type_arguments()),
260  [](const typet &type) -> reference_typet
261  {
262  INVARIANT(
263  is_reference(type), "All generic type arguments should be references");
264  return to_reference_type(type);
265  });
266 }
267 
272 std::string erase_type_arguments(const std::string &src)
273 {
274  std::string class_name = src;
275  std::size_t f_pos = class_name.find('<', 1);
276 
277  while(f_pos != std::string::npos)
278  {
279  std::size_t e_pos = find_closing_delimiter(class_name, f_pos, '<', '>');
280  if(e_pos == std::string::npos)
281  {
283  "Failed to find generic signature closing delimiter (or recursive "
284  "generic): " +
285  src);
286  }
287 
288  // erase generic information between brackets
289  class_name.erase(f_pos, e_pos - f_pos + 1);
290 
291  // Search the remainder of the string for generic signature
292  f_pos = class_name.find('<', f_pos + 1);
293  }
294  return class_name;
295 }
296 
303 std::string gather_full_class_name(const std::string &src)
304 {
305  PRECONDITION(src.size() >= 2);
306  PRECONDITION(src[0] == 'L');
307  PRECONDITION(src[src.size() - 1] == ';');
308 
309  std::string class_name = src.substr(1, src.size() - 2);
310 
311  class_name = erase_type_arguments(class_name);
312 
313  std::replace(class_name.begin(), class_name.end(), '.', '$');
314  std::replace(class_name.begin(), class_name.end(), '/', '.');
315  return class_name;
316 }
317 
330 std::vector<typet> parse_list_types(
331  const std::string src,
332  const std::string class_name_prefix,
333  const char opening_bracket,
334  const char closing_bracket)
335 {
336  // Loop over the types in the given string, parsing each one in turn
337  // and adding to the type_list
338  std::vector<typet> type_list;
339  for(const std::string &raw_type :
340  parse_raw_list_types(src, opening_bracket, closing_bracket))
341  {
342  const typet new_type = java_type_from_string(raw_type, class_name_prefix);
343  INVARIANT(new_type != nil_typet(), "Failed to parse type");
344  type_list.push_back(new_type);
345  }
346  return type_list;
347 }
348 
357 std::vector<std::string> parse_raw_list_types(
358  const std::string src,
359  const char opening_bracket,
360  const char closing_bracket)
361 {
362  PRECONDITION(src.size() >= 2);
363  PRECONDITION(src[0] == opening_bracket);
364  PRECONDITION(src[src.size() - 1] == closing_bracket);
365 
366  // Loop over the types in the given string, parsing each one in turn
367  // and adding to the type_list
368  std::vector<std::string> type_list;
369  for(std::size_t i = 1; i < src.size() - 1; i++)
370  {
371  size_t start = i;
372  while(i < src.size())
373  {
374  // type is an object type or instantiated generic type
375  if(src[i] == 'L')
376  {
378  break;
379  }
380 
381  // type is an array
382  else if(src[i] == '[')
383  i++;
384 
385  // type is a type variable/parameter
386  else if(src[i] == 'T')
387  i = src.find(';', i); // ends on ;
388 
389  // type is an atomic type (just one character)
390  else
391  {
392  break;
393  }
394  }
395 
396  std::string sub_str = src.substr(start, i - start + 1);
397  type_list.emplace_back(sub_str);
398  }
399  return type_list;
400 }
401 
410 build_class_name(const std::string &src, const std::string &class_name_prefix)
411 {
412  PRECONDITION(src[0] == 'L');
413 
414  // All reference types must end on a ;
415  PRECONDITION(src[src.size() - 1] == ';');
416 
417  std::string container_class = gather_full_class_name(src);
418  std::string identifier = "java::" + container_class;
419  struct_tag_typet struct_tag_type(identifier);
420  struct_tag_type.set(ID_C_base_name, container_class);
421 
422  std::size_t f_pos = src.find('<', 1);
423  if(f_pos != std::string::npos)
424  {
425  java_generic_typet result(struct_tag_type);
426  // get generic type information
427  do
428  {
429  std::size_t e_pos = find_closing_delimiter(src, f_pos, '<', '>');
430  if(e_pos == std::string::npos)
432  "Parsing type with unmatched generic bracket: " + src);
433 
435  result, src.substr(f_pos, e_pos - f_pos + 1), class_name_prefix);
436 
437  // Look for the next generic type info (if it exists)
438  f_pos = src.find('<', e_pos + 1);
439  } while(f_pos != std::string::npos);
440  return std::move(result);
441  }
442 
443  return java_reference_type(struct_tag_type);
444 }
445 
455  const std::string src,
456  size_t starting_point)
457 {
458  PRECONDITION(src[starting_point] == 'L');
459  size_t next_semi_colon = src.find(';', starting_point);
460  INVARIANT(
461  next_semi_colon != std::string::npos,
462  "There must be a semi-colon somewhere in the input");
463  size_t next_angle_bracket = src.find('<', starting_point);
464 
465  while(next_angle_bracket < next_semi_colon)
466  {
467  size_t end_bracket =
468  find_closing_delimiter(src, next_angle_bracket, '<', '>');
469  INVARIANT(
470  end_bracket != std::string::npos, "Must find matching angle bracket");
471 
472  next_semi_colon = src.find(';', end_bracket + 1);
473  next_angle_bracket = src.find('<', end_bracket + 1);
474  }
475 
476  return next_semi_colon;
477 }
478 
493  const std::string &src,
494  const std::string &class_name_prefix)
495 {
496  if(src.empty())
497  return nil_typet();
498 
499  // a java type is encoded in different ways
500  // - a method type is encoded as '(...)R' where the parenthesis include the
501  // parameter types and R is the type of the return value
502  // - atomic types are encoded as single characters
503  // - array types are encoded as '[' followed by the type of the array
504  // content
505  // - object types are named with prefix 'L' and suffix ';', e.g.,
506  // Ljava/lang/Object;
507  // - type variables are similar to object types but have the prefix 'T'
508  switch(src[0])
509  {
510  case '<':
511  {
512  // The method signature can optionally have a collection of formal
513  // type parameters (e.g. on generic methods on non-generic classes
514  // or generic static methods). For now we skip over this part of the
515  // signature and continue parsing the rest of the signature as normal
516  // So for example, the following java method:
517  // static void <T, U> foo(T t, U u, int x);
518  // Would have a signature that looks like:
519  // <T:Ljava/lang/Object;U:Ljava/lang/Object;>(TT;TU;I)V
520  // So we skip all inside the angle brackets and parse the rest of the
521  // string:
522  // (TT;TU;I)V
523  size_t closing_generic=find_closing_delimiter(src, 0, '<', '>');
524  if(closing_generic==std::string::npos)
525  {
527  "Failed to find generic signature closing delimiter");
528  }
529 
530  // If there are any bounds between '<' and '>' then we cannot currently
531  // parse them, so we give up. This only happens when parsing the
532  // signature, so we'll fall back to the result of parsing the
533  // descriptor, which will respect the bounds correctly.
534  const size_t colon_pos = src.find(':');
535  if(colon_pos != std::string::npos && colon_pos < closing_generic)
536  {
538  "Cannot currently parse bounds on generic types");
539  }
540 
541  const typet &method_type=java_type_from_string(
542  src.substr(closing_generic+1, std::string::npos), class_name_prefix);
543 
544  // This invariant being violated means that tkiley has not understood
545  // part of the signature spec.
546  // Only class and method signatures can start with a '<' and classes are
547  // handled separately.
548  INVARIANT(
549  method_type.id()==ID_code,
550  "This should correspond to method signatures only");
551 
552  return method_type;
553  }
554  case '(': // function type
555  {
556  std::size_t e_pos=src.rfind(')');
557  if(e_pos==std::string::npos)
558  return nil_typet();
559 
560  typet return_type = java_type_from_string(
561  std::string(src, e_pos + 1, std::string::npos), class_name_prefix);
562 
563  std::vector<typet> param_types =
564  parse_list_types(src.substr(0, e_pos + 1), class_name_prefix, '(', ')');
565 
566  // create parameters for each type
568  std::transform(
569  param_types.begin(),
570  param_types.end(),
571  std::back_inserter(parameters),
572  [](const typet &type) { return java_method_typet::parametert(type); });
573 
574  return java_method_typet(std::move(parameters), std::move(return_type));
575  }
576 
577  case '[': // array type
578  {
579  // If this is a reference array, we generate a plain array[reference]
580  // with void* members, but note the real type in ID_element_type.
581  if(src.size()<=1)
582  return nil_typet();
583  char subtype_letter=src[1];
584  const typet subtype=
585  java_type_from_string(src.substr(1, std::string::npos),
586  class_name_prefix);
587  if(subtype_letter=='L' || // [L denotes a reference array of some sort.
588  subtype_letter=='[' || // Array-of-arrays
589  subtype_letter=='T') // Array of generic types
590  subtype_letter='A';
591  typet tmp=java_array_type(std::tolower(subtype_letter));
592  tmp.subtype().set(ID_element_type, subtype);
593  return tmp;
594  }
595 
596  case 'B': return java_byte_type();
597  case 'F': return java_float_type();
598  case 'D': return java_double_type();
599  case 'I': return java_int_type();
600  case 'C': return java_char_type();
601  case 'S': return java_short_type();
602  case 'Z': return java_boolean_type();
603  case 'V': return java_void_type();
604  case 'J': return java_long_type();
605  case 'T':
606  {
607  // parse name of type variable
608  INVARIANT(src[src.size()-1]==';', "Generic type name must end on ';'.");
609  PRECONDITION(!class_name_prefix.empty());
610  irep_idt type_var_name(class_name_prefix+"::"+src.substr(1, src.size()-2));
612  type_var_name,
614  java_type_from_string("Ljava/lang/Object;").subtype()));
615  }
616  case 'L':
617  {
618  return build_class_name(src, class_name_prefix);
619  }
620  case '*':
621  case '+':
622  case '-':
623  {
624 #ifdef DEBUG
625  std::cout << class_name_prefix << std::endl;
626 #endif
627  throw unsupported_java_class_signature_exceptiont("wild card generic");
628  }
629  default:
630  return nil_typet();
631  }
632 }
633 
634 char java_char_from_type(const typet &type)
635 {
636  const irep_idt &id=type.id();
637 
638  if(id==ID_signedbv)
639  {
640  const size_t width=to_signedbv_type(type).get_width();
641  if(to_signedbv_type(java_int_type()).get_width()==width)
642  return 'i';
643  else if(to_signedbv_type(java_long_type()).get_width()==width)
644  return 'l';
645  else if(to_signedbv_type(java_short_type()).get_width()==width)
646  return 's';
647  else if(to_signedbv_type(java_byte_type()).get_width()==width)
648  return 'b';
649  }
650  else if(id==ID_unsignedbv)
651  return 'c';
652  else if(id==ID_floatbv)
653  {
654  const size_t width(to_floatbv_type(type).get_width());
655  if(to_floatbv_type(java_float_type()).get_width()==width)
656  return 'f';
657  else if(to_floatbv_type(java_double_type()).get_width()==width)
658  return 'd';
659  }
660  else if(id==ID_c_bool)
661  return 'z';
662 
663  return 'a';
664 }
665 
675 std::vector<typet> java_generic_type_from_string(
676  const std::string &class_name,
677  const std::string &src)
678 {
681  size_t signature_end = find_closing_delimiter(src, 0, '<', '>');
682  INVARIANT(
683  src[0]=='<' && signature_end!=std::string::npos,
684  "Class signature has unexpected format");
685  std::string signature(src.substr(1, signature_end-1));
686 
687  if(signature.find(";:")!=std::string::npos)
688  throw unsupported_java_class_signature_exceptiont("multiple bounds");
689 
690  PRECONDITION(signature[signature.size()-1]==';');
691 
692  std::vector<typet> types;
693  size_t var_sep=signature.find(';');
694  while(var_sep!=std::string::npos)
695  {
696  size_t bound_sep=signature.find(':');
697  INVARIANT(bound_sep!=std::string::npos, "No bound for type variable.");
698 
699  // is bound an interface?
700  // in this case the separator is '::'
701  if(signature[bound_sep + 1] == ':')
702  {
703  INVARIANT(
704  signature[bound_sep + 2] != ':', "Unknown bound for type variable.");
705  bound_sep++;
706  }
707 
708  std::string type_var_name(
709  "java::"+class_name+"::"+signature.substr(0, bound_sep));
710  std::string bound_type(signature.substr(bound_sep+1, var_sep-bound_sep));
711 
712  java_generic_parametert type_var_type(
713  type_var_name,
715  java_type_from_string(bound_type, class_name).subtype()));
716 
717  types.push_back(type_var_type);
718  signature=signature.substr(var_sep+1, std::string::npos);
719  var_sep=signature.find(';');
720  }
721  return types;
722 }
723 
724 // java/lang/Object -> java.lang.Object
725 static std::string slash_to_dot(const std::string &src)
726 {
727  std::string result=src;
728  for(std::string::iterator it=result.begin(); it!=result.end(); it++)
729  if(*it=='/')
730  *it='.';
731  return result;
732 }
733 
734 struct_tag_typet java_classname(const std::string &id)
735 {
736  if(!id.empty() && id[0]=='[')
737  return to_struct_tag_type(java_type_from_string(id).subtype());
738 
739  std::string class_name=id;
740 
741  class_name=slash_to_dot(class_name);
742  irep_idt identifier="java::"+class_name;
743  struct_tag_typet struct_tag_type(identifier);
744  struct_tag_type.set(ID_C_base_name, class_name);
745 
746  return struct_tag_type;
747 }
748 
763 {
764  bool correct_num_components=type.components().size()==3;
765  if(!correct_num_components)
766  return false;
767 
768  // First component, the base class (Object) data
769  const struct_union_typet::componentt base_class_component=
770  type.components()[0];
771 
772  bool base_component_valid=true;
773  base_component_valid&=base_class_component.get_name()=="@java.lang.Object";
774 
775  bool length_component_valid=true;
776  const struct_union_typet::componentt length_component=
777  type.components()[1];
778  length_component_valid&=length_component.get_name()=="length";
779  length_component_valid&=length_component.type()==java_int_type();
780 
781  bool data_component_valid=true;
782  const struct_union_typet::componentt data_component=
783  type.components()[2];
784  data_component_valid&=data_component.get_name()=="data";
785  data_component_valid&=data_component.type().id()==ID_pointer;
786 
787  return correct_num_components &&
788  base_component_valid &&
789  length_component_valid &&
790  data_component_valid;
791 }
792 
799 bool equal_java_types(const typet &type1, const typet &type2)
800 {
801  bool arrays_with_same_element_type = true;
802  if(
803  type1.id() == ID_pointer && type2.id() == ID_pointer &&
804  type1.subtype().id() == ID_struct_tag &&
805  type2.subtype().id() == ID_struct_tag)
806  {
807  const auto &subtype_symbol1 = to_struct_tag_type(type1.subtype());
808  const auto &subtype_symbol2 = to_struct_tag_type(type2.subtype());
809  if(
810  subtype_symbol1.get_identifier() == subtype_symbol2.get_identifier() &&
811  is_java_array_tag(subtype_symbol1.get_identifier()))
812  {
813  const typet &array_element_type1 =
814  java_array_element_type(subtype_symbol1);
815  const typet &array_element_type2 =
816  java_array_element_type(subtype_symbol2);
817 
818  arrays_with_same_element_type =
819  equal_java_types(array_element_type1, array_element_type2);
820  }
821  }
822  return (type1 == type2 && arrays_with_same_element_type);
823 }
824 
826  const typet &t,
827  std::set<irep_idt> &refs)
828 {
829  // Java generic type that holds different types in its type arguments
830  if(is_java_generic_type(t))
831  {
832  for(const auto type_arg : to_java_generic_type(t).generic_type_arguments())
834  }
835 
836  // Java reference type
837  else if(t.id() == ID_pointer)
838  {
840  }
841 
842  // method type with parameters and return value
843  else if(t.id() == ID_code)
844  {
847  for(const auto &param : c.parameters())
849  }
850 
851  // struct tag
852  else if(t.id() == ID_struct_tag)
853  {
854  const auto &struct_tag_type = to_struct_tag_type(t);
855  const irep_idt class_name(struct_tag_type.get_identifier());
856  if(is_java_array_tag(class_name))
857  {
859  java_array_element_type(struct_tag_type), refs);
860  }
861  else
862  refs.insert(strip_java_namespace_prefix(class_name));
863  }
864 }
865 
873  const std::string &signature,
874  std::set<irep_idt> &refs)
875 {
876  try
877  {
878  // class signature with bounds
879  if(signature[0] == '<')
880  {
881  const std::vector<typet> types = java_generic_type_from_string(
882  erase_type_arguments(signature), signature);
883 
884  for(const auto &t : types)
886  }
887 
888  // class signature without bounds and without wildcards
889  else if(signature.find('*') == std::string::npos)
890  {
892  java_type_from_string(signature, erase_type_arguments(signature)),
893  refs);
894  }
895  }
897  {
898  // skip for now, if we cannot parse it, we cannot detect which additional
899  // classes should be loaded as dependencies
900  }
901 }
902 
909  const typet &t,
910  std::set<irep_idt> &refs)
911 {
913 }
914 
925  const struct_tag_typet &type,
926  const std::string &base_ref,
927  const std::string &class_name_prefix)
928  : struct_tag_typet(type)
929 {
930  set(ID_C_java_generic_symbol, true);
931  const typet &base_type = java_type_from_string(base_ref, class_name_prefix);
933  const java_generic_typet &gen_base_type = to_java_generic_type(base_type);
934  INVARIANT(
935  type.get_identifier() ==
936  to_struct_tag_type(gen_base_type.subtype()).get_identifier(),
937  "identifier of " + type.pretty() + "\n and identifier of type " +
938  gen_base_type.subtype().pretty() +
939  "\ncreated by java_type_from_string for " + base_ref +
940  " should be equal");
941  generic_types().insert(
942  generic_types().end(),
943  gen_base_type.generic_type_arguments().begin(),
944  gen_base_type.generic_type_arguments().end());
945 }
946 
952  const java_generic_parametert &type) const
953 {
954  const auto &type_variable = type.get_name();
955  const auto &generics = generic_types();
956  for(std::size_t i = 0; i < generics.size(); ++i)
957  {
958  if(
959  is_java_generic_parameter(generics[i]) &&
960  to_java_generic_parameter(generics[i]).get_name() == type_variable)
961  return i;
962  }
963  return {};
964 }
965 
966 std::string pretty_java_type(const typet &type)
967 {
968  if(type == java_void_type())
969  return "void";
970  if(type == java_int_type())
971  return "int";
972  else if(type == java_long_type())
973  return "long";
974  else if(type == java_short_type())
975  return "short";
976  else if(type == java_byte_type())
977  return "byte";
978  else if(type == java_char_type())
979  return "char";
980  else if(type == java_float_type())
981  return "float";
982  else if(type == java_double_type())
983  return "double";
984  else if(type == java_boolean_type())
985  return "boolean";
986  else if(type == java_byte_type())
987  return "byte";
988  else if(is_reference(type))
989  {
990  if(type.subtype().id() == ID_struct_tag)
991  {
992  const auto &struct_tag_type = to_struct_tag_type(type.subtype());
993  const irep_idt &id = struct_tag_type.get_identifier();
994  if(is_java_array_tag(id))
995  return pretty_java_type(java_array_element_type(struct_tag_type)) +
996  "[]";
997  else
999  }
1000  else
1001  return "?";
1002  }
1003  else
1004  return "?";
1005 }
1006 
1007 std::string pretty_signature(const java_method_typet &method_type)
1008 {
1009  std::ostringstream result;
1010  result << '(';
1011 
1012  bool first = true;
1013  for(const auto p : method_type.parameters())
1014  {
1015  if(p.get_this())
1016  continue;
1017 
1018  if(first)
1019  first = false;
1020  else
1021  result << ", ";
1022 
1023  result << pretty_java_type(p.type());
1024  }
1025 
1026  result << ')';
1027  return result.str();
1028 }
tag_typet::get_identifier
const irep_idt & get_identifier() const
Definition: std_types.h:479
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:205
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:825
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
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:872
java_char_from_type
char java_char_from_type(const typet &type)
Definition: java_types.cpp:634
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
typet::subtype
const typet & subtype() const
Definition: type.h:38
java_generic_typet
Class to hold type with generic type arguments, for example java.util.List in either a reference of t...
Definition: java_types.h:483
java_reference_type
reference_typet java_reference_type(const typet &subtype)
Definition: java_types.cpp:80
java_double_type
typet java_double_type()
Definition: java_types.cpp:67
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:485
java_int_type
typet java_int_type()
Definition: java_types.cpp:32
reference_typet
The reference type.
Definition: std_types.h:1565
typet
The type of an expression, extends irept.
Definition: type.h:27
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:640
java_boolean_type
typet java_boolean_type()
Definition: java_types.cpp:72
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:129
unsupported_java_class_signature_exceptiont
An exception that is raised for unsupported class signature.
Definition: java_types.h:695
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,.
Definition: java_types.cpp:163
java_classname
struct_tag_typet java_classname(const std::string &id)
Definition: java_types.cpp:734
nil_typet
The NIL type, i.e., an invalid type, no value.
Definition: std_types.h:39
prefix.h
java_long_type
typet java_long_type()
Definition: java_types.cpp:42
replace
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
Definition: string_constraint.cpp:65
java_generic_parametert
Class to hold a Java generic type parameter (also called type variable), e.g., T in List<T>.
Definition: java_types.h:397
java_method_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:754
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:762
exprt
Base class for all expressions.
Definition: expr.h:54
is_java_array_tag
bool is_java_array_tag(const irep_idt &tag)
See above.
Definition: java_types.cpp:173
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:400
struct_tag_typet
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:517
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:357
java_generic_struct_tag_typet::java_generic_struct_tag_typet
java_generic_struct_tag_typet(const struct_tag_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:924
invariant.h
to_reference_type
const reference_typet & to_reference_type(const typet &type)
Cast a typet to a reference_typet.
Definition: std_types.h:1593
java_lang_object_type
reference_typet java_lang_object_type()
Definition: java_types.cpp:85
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:951
java_generic_struct_tag_typet::generic_types
const generic_typest & generic_types() const
Definition: java_types.h:764
java_array_type
reference_typet java_array_type(const char subtype)
Construct an array pointer type.
Definition: java_types.cpp:94
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
unsignedbv_typet
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1223
c_bool_typet
The C/C++ Booleans.
Definition: std_types.h:1611
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:294
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:272
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:195
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
java_generic_parametert::get_name
const irep_idt get_name() const
Definition: java_types.h:424
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:799
java_type_from_char
typet java_type_from_char(char t)
Constructs a type indicated by the given character:
Definition: java_types.cpp:188
ieee_float_spect::double_precision
static ieee_float_spect double_precision()
Definition: ieee_float.h:80
void_typet
The void type, the same as empty_typet.
Definition: std_types.h:57
base_type
void base_type(typet &type, const namespacet &ns)
Definition: base_type.cpp:135
java_generic_typet::generic_type_arguments
const generic_type_argumentst & generic_type_arguments() const
Definition: java_types.h:495
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:132
java_type_from_string
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:492
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:454
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:530
ieee_float_spect::to_type
class floatbv_typet to_type() const
Definition: ieee_float.cpp:26
java_byte_type
typet java_byte_type()
Definition: java_types.cpp:52
is_java_generic_parameter
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:446
signedbv_typet
Fixed-width bit-vector with two's complement interpretation.
Definition: std_types.h:1278
std_types.h
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:410
is_java_generic_type
bool is_java_generic_type(const typet &type)
Definition: java_types.h:517
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:148
pretty_java_type
std::string pretty_java_type(const typet &type)
Definition: java_types.cpp:966
pretty_signature
std::string pretty_signature(const java_method_typet &method_type)
Definition: java_types.cpp:1007
irept::id
const irep_idt & id() const
Definition: irep.h:259
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:543
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:893
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:330
to_java_generic_type
const java_generic_typet & to_java_generic_type(const typet &type)
Definition: java_types.h:524
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
java_short_type
typet java_short_type()
Definition: java_types.cpp:47
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:1117
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:1526
reference_type
reference_typet reference_type(const typet &subtype)
Definition: c_types.cpp:248
struct_union_typet::componentt
Definition: std_types.h:121
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:276
to_java_generic_parameter
const java_generic_parametert & to_java_generic_parameter(const typet &type)
Definition: java_types.h:453
is_reference
bool is_reference(const typet &type)
Returns true if the type is a reference.
Definition: std_types.cpp:132
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:303
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
ieee_float.h
slash_to_dot
static std::string slash_to_dot(const std::string &src)
Definition: java_types.cpp:725
to_signedbv_type
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
Definition: std_types.h:1316
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:207
code_typet::parametert
Definition: std_types.h:788
to_floatbv_type
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition: std_types.h:1442
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:883
java_char_type
typet java_char_type()
Definition: java_types.cpp:57
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:72
java_types.h
java_void_type
typet java_void_type()
Definition: java_types.cpp:37
to_java_method_type
const java_method_typet & to_java_method_type(const typet &type)
Definition: java_types.h:338
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2277
typet::find_type
const typet & find_type(const irep_namet &name) const
Definition: type.h:77
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:675
std_expr.h
ieee_float_spect::single_precision
static ieee_float_spect single_precision()
Definition: ieee_float.h:74
java_method_typet
Definition: java_types.h:264
c_types.h
validation_modet::INVARIANT
java_float_type
typet java_float_type()
Definition: java_types.cpp:62
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:470
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:237