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(symbol_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  symbol_typet symbol_type("java::"+id2string(class_name));
121  symbol_type.set(ID_C_base_name, class_name);
122  symbol_type.set(ID_element_type, java_type_from_char(subtype));
123 
124  return java_reference_type(symbol_type);
125 }
126 
129 const typet &java_array_element_type(const symbol_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_symbol = to_symbol_type(type.subtype());
157  return is_java_array_tag(subtype_symbol.get_identifier());
158 }
159 
161 // i.e., a pointer to an array type with element type also being a pointer to an
164 {
165  return is_java_array_type(type) &&
168 }
169 
174 bool is_java_array_tag(const irep_idt& tag)
175 {
176  return has_prefix(id2string(tag), "java::array[");
177 }
178 
190 {
191  switch(t)
192  {
193  case 'i': return java_int_type();
194  case 'j': return java_long_type();
195  case 'l': return java_long_type();
196  case 's': return java_short_type();
197  case 'b': return java_byte_type();
198  case 'c': return java_char_type();
199  case 'f': return java_float_type();
200  case 'd': return java_double_type();
201  case 'z': return java_boolean_type();
202  case 'a': return java_reference_type(void_typet());
203  default: UNREACHABLE; return nil_typet();
204  }
205 }
206 
209 {
210  if(type==java_boolean_type() ||
211  type==java_char_type() ||
212  type==java_byte_type() ||
213  type==java_short_type())
214  return java_int_type();
215 
216  return type;
217 }
218 
221 {
222  typet new_type=java_bytecode_promotion(expr.type());
223 
224  if(new_type==expr.type())
225  return expr;
226  else
227  return typecast_exprt(expr, new_type);
228 }
229 
239  java_generic_typet &generic_type,
240  const std::string &type_arguments,
241  const std::string &class_name_prefix)
242 {
243  PRECONDITION(type_arguments.size() >= 2);
244  PRECONDITION(type_arguments[0] == '<');
245  PRECONDITION(type_arguments[type_arguments.size() - 1] == '>');
246 
247  // Parse contained arguments, can be either type parameters (`TT;`)
248  // or instantiated types - either generic types (`LList<LInteger;>;`) or
249  // just references (`Ljava/lang/Foo;`)
250  std::vector<typet> type_arguments_types =
251  parse_list_types(type_arguments, class_name_prefix, '<', '>');
252 
253  // We should have at least one generic type argument
254  CHECK_RETURN(!type_arguments_types.empty());
255 
256  // Add the type arguments to the generic type
257  std::transform(
258  type_arguments_types.begin(),
259  type_arguments_types.end(),
260  std::back_inserter(generic_type.generic_type_arguments()),
261  [](const typet &type) -> reference_typet
262  {
263  INVARIANT(
264  is_reference(type), "All generic type arguments should be references");
265  return to_reference_type(type);
266  });
267 }
268 
273 std::string erase_type_arguments(const std::string &src)
274 {
275  std::string class_name = src;
276  std::size_t f_pos = class_name.find('<', 1);
277 
278  while(f_pos != std::string::npos)
279  {
280  std::size_t e_pos = find_closing_delimiter(class_name, f_pos, '<', '>');
281  if(e_pos == std::string::npos)
282  {
284  "Failed to find generic signature closing delimiter (or recursive "
285  "generic): " +
286  src);
287  }
288 
289  // erase generic information between brackets
290  class_name.erase(f_pos, e_pos - f_pos + 1);
291 
292  // Search the remainder of the string for generic signature
293  f_pos = class_name.find('<', f_pos + 1);
294  }
295  return class_name;
296 }
297 
304 std::string gather_full_class_name(const std::string &src)
305 {
306  PRECONDITION(src.size() >= 2);
307  PRECONDITION(src[0] == 'L');
308  PRECONDITION(src[src.size() - 1] == ';');
309 
310  std::string class_name = src.substr(1, src.size() - 2);
311 
312  class_name = erase_type_arguments(class_name);
313 
314  std::replace(class_name.begin(), class_name.end(), '.', '$');
315  std::replace(class_name.begin(), class_name.end(), '/', '.');
316  return class_name;
317 }
318 
331 std::vector<typet> parse_list_types(
332  const std::string src,
333  const std::string class_name_prefix,
334  const char opening_bracket,
335  const char closing_bracket)
336 {
337  PRECONDITION(src.size() >= 2);
338  PRECONDITION(src[0] == opening_bracket);
339  PRECONDITION(src[src.size() - 1] == closing_bracket);
340 
341  // Loop over the types in the given string, parsing each one in turn
342  // and adding to the type_list
343  std::vector<typet> type_list;
344  for(std::size_t i = 1; i < src.size() - 1; i++)
345  {
346  size_t start = i;
347  while(i < src.size())
348  {
349  // type is an object type or instantiated generic type
350  if(src[i] == 'L')
351  {
353  break;
354  }
355 
356  // type is an array
357  else if(src[i] == '[')
358  i++;
359 
360  // type is a type variable/parameter
361  else if(src[i] == 'T')
362  i = src.find(';', i); // ends on ;
363 
364  // type is an atomic type (just one character)
365  else
366  {
367  break;
368  }
369  }
370 
371  std::string sub_str = src.substr(start, i - start + 1);
372  const typet &new_type = java_type_from_string(sub_str, class_name_prefix);
373  INVARIANT(new_type != nil_typet(), "Failed to parse type");
374 
375  type_list.push_back(new_type);
376  }
377  return type_list;
378 }
379 
388 build_class_name(const std::string &src, const std::string &class_name_prefix)
389 {
390  PRECONDITION(src[0] == 'L');
391 
392  // All reference types must end on a ;
393  PRECONDITION(src[src.size() - 1] == ';');
394 
395  std::string container_class = gather_full_class_name(src);
396  std::string identifier = "java::" + container_class;
397  symbol_typet symbol_type(identifier);
398  symbol_type.set(ID_C_base_name, container_class);
399 
400  std::size_t f_pos = src.find('<', 1);
401  if(f_pos != std::string::npos)
402  {
403  java_generic_typet result(symbol_type);
404  // get generic type information
405  do
406  {
407  std::size_t e_pos = find_closing_delimiter(src, f_pos, '<', '>');
408  if(e_pos == std::string::npos)
410  "Parsing type with unmatched generic bracket: " + src);
411 
413  result, src.substr(f_pos, e_pos - f_pos + 1), class_name_prefix);
414 
415  // Look for the next generic type info (if it exists)
416  f_pos = src.find('<', e_pos + 1);
417  } while(f_pos != std::string::npos);
418  return result;
419  }
420 
421  return java_reference_type(symbol_type);
422 }
423 
433  const std::string src,
434  size_t starting_point)
435 {
436  PRECONDITION(src[starting_point] == 'L');
437  size_t next_semi_colon = src.find(';', starting_point);
438  INVARIANT(
439  next_semi_colon != std::string::npos,
440  "There must be a semi-colon somewhere in the input");
441  size_t next_angle_bracket = src.find('<', starting_point);
442 
443  while(next_angle_bracket < next_semi_colon)
444  {
445  size_t end_bracket =
446  find_closing_delimiter(src, next_angle_bracket, '<', '>');
447  INVARIANT(
448  end_bracket != std::string::npos, "Must find matching angle bracket");
449 
450  next_semi_colon = src.find(';', end_bracket + 1);
451  next_angle_bracket = src.find('<', end_bracket + 1);
452  }
453 
454  return next_semi_colon;
455 }
456 
471  const std::string &src,
472  const std::string &class_name_prefix)
473 {
474  if(src.empty())
475  return nil_typet();
476 
477  // a java type is encoded in different ways
478  // - a method type is encoded as '(...)R' where the parenthesis include the
479  // parameter types and R is the type of the return value
480  // - atomic types are encoded as single characters
481  // - array types are encoded as '[' followed by the type of the array
482  // content
483  // - object types are named with prefix 'L' and suffix ';', e.g.,
484  // Ljava/lang/Object;
485  // - type variables are similar to object types but have the prefix 'T'
486  switch(src[0])
487  {
488  case '<':
489  {
490  // The method signature can optionally have a collection of formal
491  // type parameters (e.g. on generic methods on non-generic classes
492  // or generic static methods). For now we skip over this part of the
493  // signature and continue parsing the rest of the signature as normal
494  // So for example, the following java method:
495  // static void <T, U> foo(T t, U u, int x);
496  // Would have a signature that looks like:
497  // <T:Ljava/lang/Object;U:Ljava/lang/Object;>(TT;TU;I)V
498  // So we skip all inside the angle brackets and parse the rest of the
499  // string:
500  // (TT;TU;I)V
501  size_t closing_generic=find_closing_delimiter(src, 0, '<', '>');
502  if(closing_generic==std::string::npos)
503  {
505  "Failed to find generic signature closing delimiter");
506  }
507 
508  // If there are any bounds between '<' and '>' then we cannot currently
509  // parse them, so we give up. This only happens when parsing the
510  // signature, so we'll fall back to the result of parsing the
511  // descriptor, which will respect the bounds correctly.
512  const size_t colon_pos = src.find(':');
513  if(colon_pos != std::string::npos && colon_pos < closing_generic)
514  {
516  "Cannot currently parse bounds on generic types");
517  }
518 
519  const typet &method_type=java_type_from_string(
520  src.substr(closing_generic+1, std::string::npos), class_name_prefix);
521 
522  // This invariant being violated means that tkiley has not understood
523  // part of the signature spec.
524  // Only class and method signatures can start with a '<' and classes are
525  // handled separately.
526  INVARIANT(
527  method_type.id()==ID_code,
528  "This should correspond to method signatures only");
529 
530  return method_type;
531  }
532  case '(': // function type
533  {
534  std::size_t e_pos=src.rfind(')');
535  if(e_pos==std::string::npos)
536  return nil_typet();
537 
538  typet return_type = java_type_from_string(
539  std::string(src, e_pos + 1, std::string::npos), class_name_prefix);
540 
541  std::vector<typet> param_types =
542  parse_list_types(src.substr(0, e_pos + 1), class_name_prefix, '(', ')');
543 
544  // create parameters for each type
546  std::transform(
547  param_types.begin(),
548  param_types.end(),
549  std::back_inserter(parameters),
550  [](const typet &type) { return java_method_typet::parametert(type); });
551 
552  return java_method_typet(std::move(parameters), std::move(return_type));
553  }
554 
555  case '[': // array type
556  {
557  // If this is a reference array, we generate a plain array[reference]
558  // with void* members, but note the real type in ID_element_type.
559  if(src.size()<=1)
560  return nil_typet();
561  char subtype_letter=src[1];
562  const typet subtype=
563  java_type_from_string(src.substr(1, std::string::npos),
564  class_name_prefix);
565  if(subtype_letter=='L' || // [L denotes a reference array of some sort.
566  subtype_letter=='[' || // Array-of-arrays
567  subtype_letter=='T') // Array of generic types
568  subtype_letter='A';
569  typet tmp=java_array_type(std::tolower(subtype_letter));
570  tmp.subtype().set(ID_element_type, subtype);
571  return tmp;
572  }
573 
574  case 'B': return java_byte_type();
575  case 'F': return java_float_type();
576  case 'D': return java_double_type();
577  case 'I': return java_int_type();
578  case 'C': return java_char_type();
579  case 'S': return java_short_type();
580  case 'Z': return java_boolean_type();
581  case 'V': return java_void_type();
582  case 'J': return java_long_type();
583  case 'T':
584  {
585  // parse name of type variable
586  INVARIANT(src[src.size()-1]==';', "Generic type name must end on ';'.");
587  PRECONDITION(!class_name_prefix.empty());
588  irep_idt type_var_name(class_name_prefix+"::"+src.substr(1, src.size()-2));
590  type_var_name,
591  to_symbol_type(java_type_from_string("Ljava/lang/Object;").subtype()));
592  }
593  case 'L':
594  {
595  return build_class_name(src, class_name_prefix);
596  }
597  case '*':
598  case '+':
599  case '-':
600  {
601 #ifdef DEBUG
602  std::cout << class_name_prefix << std::endl;
603 #endif
604  throw unsupported_java_class_signature_exceptiont("wild card generic");
605  }
606  default:
607  return nil_typet();
608  }
609 }
610 
611 char java_char_from_type(const typet &type)
612 {
613  const irep_idt &id=type.id();
614 
615  if(id==ID_signedbv)
616  {
617  const size_t width=to_signedbv_type(type).get_width();
618  if(to_signedbv_type(java_int_type()).get_width()==width)
619  return 'i';
620  else if(to_signedbv_type(java_long_type()).get_width()==width)
621  return 'l';
622  else if(to_signedbv_type(java_short_type()).get_width()==width)
623  return 's';
624  else if(to_signedbv_type(java_byte_type()).get_width()==width)
625  return 'b';
626  }
627  else if(id==ID_unsignedbv)
628  return 'c';
629  else if(id==ID_floatbv)
630  {
631  const size_t width(to_floatbv_type(type).get_width());
632  if(to_floatbv_type(java_float_type()).get_width()==width)
633  return 'f';
634  else if(to_floatbv_type(java_double_type()).get_width()==width)
635  return 'd';
636  }
637  else if(id==ID_c_bool)
638  return 'z';
639 
640  return 'a';
641 }
642 
652 std::vector<typet> java_generic_type_from_string(
653  const std::string &class_name,
654  const std::string &src)
655 {
658  size_t signature_end = find_closing_delimiter(src, 0, '<', '>');
659  INVARIANT(
660  src[0]=='<' && signature_end!=std::string::npos,
661  "Class signature has unexpected format");
662  std::string signature(src.substr(1, signature_end-1));
663 
664  if(signature.find(";:")!=std::string::npos)
665  throw unsupported_java_class_signature_exceptiont("multiple bounds");
666 
667  PRECONDITION(signature[signature.size()-1]==';');
668 
669  std::vector<typet> types;
670  size_t var_sep=signature.find(';');
671  while(var_sep!=std::string::npos)
672  {
673  size_t bound_sep=signature.find(':');
674  INVARIANT(bound_sep!=std::string::npos, "No bound for type variable.");
675 
676  // is bound an interface?
677  // in this case the separator is '::'
678  if(signature[bound_sep + 1] == ':')
679  {
680  INVARIANT(
681  signature[bound_sep + 2] != ':', "Unknown bound for type variable.");
682  bound_sep++;
683  }
684 
685  std::string type_var_name(
686  "java::"+class_name+"::"+signature.substr(0, bound_sep));
687  std::string bound_type(signature.substr(bound_sep+1, var_sep-bound_sep));
688 
689  java_generic_parametert type_var_type(
690  type_var_name,
691  to_symbol_type(java_type_from_string(bound_type, class_name).subtype()));
692 
693  types.push_back(type_var_type);
694  signature=signature.substr(var_sep+1, std::string::npos);
695  var_sep=signature.find(';');
696  }
697  return types;
698 }
699 
700 // java/lang/Object -> java.lang.Object
701 static std::string slash_to_dot(const std::string &src)
702 {
703  std::string result=src;
704  for(std::string::iterator it=result.begin(); it!=result.end(); it++)
705  if(*it=='/')
706  *it='.';
707  return result;
708 }
709 
710 symbol_typet java_classname(const std::string &id)
711 {
712  if(!id.empty() && id[0]=='[')
713  return to_symbol_type(java_type_from_string(id).subtype());
714 
715  std::string class_name=id;
716 
717  class_name=slash_to_dot(class_name);
718  irep_idt identifier="java::"+class_name;
719  symbol_typet symbol_type(identifier);
720  symbol_type.set(ID_C_base_name, class_name);
721 
722  return symbol_type;
723 }
724 
739 {
740  bool correct_num_components=type.components().size()==3;
741  if(!correct_num_components)
742  return false;
743 
744  // First component, the base class (Object) data
745  const struct_union_typet::componentt base_class_component=
746  type.components()[0];
747 
748  bool base_component_valid=true;
749  base_component_valid&=base_class_component.get_name()=="@java.lang.Object";
750 
751  bool length_component_valid=true;
752  const struct_union_typet::componentt length_component=
753  type.components()[1];
754  length_component_valid&=length_component.get_name()=="length";
755  length_component_valid&=length_component.type()==java_int_type();
756 
757  bool data_component_valid=true;
758  const struct_union_typet::componentt data_component=
759  type.components()[2];
760  data_component_valid&=data_component.get_name()=="data";
761  data_component_valid&=data_component.type().id()==ID_pointer;
762 
763  return correct_num_components &&
764  base_component_valid &&
765  length_component_valid &&
766  data_component_valid;
767 }
768 
775 bool equal_java_types(const typet &type1, const typet &type2)
776 {
777  bool arrays_with_same_element_type = true;
778  if(
779  type1.id() == ID_pointer && type2.id() == ID_pointer &&
780  type1.subtype().id() == ID_symbol && type2.subtype().id() == ID_symbol)
781  {
782  const symbol_typet &subtype_symbol1 = to_symbol_type(type1.subtype());
783  const symbol_typet &subtype_symbol2 = to_symbol_type(type2.subtype());
784  if(
785  subtype_symbol1.get_identifier() == subtype_symbol2.get_identifier() &&
786  is_java_array_tag(subtype_symbol1.get_identifier()))
787  {
788  const typet &array_element_type1 =
789  java_array_element_type(subtype_symbol1);
790  const typet &array_element_type2 =
791  java_array_element_type(subtype_symbol2);
792 
793  arrays_with_same_element_type =
794  equal_java_types(array_element_type1, array_element_type2);
795  }
796  }
797  return (type1 == type2 && arrays_with_same_element_type);
798 }
799 
801  const typet &t,
802  std::set<irep_idt> &refs)
803 {
804  // Java generic type that holds different types in its type arguments
805  if(is_java_generic_type(t))
806  {
807  for(const auto type_arg : to_java_generic_type(t).generic_type_arguments())
809  }
810 
811  // Java reference type
812  else if(t.id() == ID_pointer)
813  {
815  }
816 
817  // method type with parameters and return value
818  else if(t.id() == ID_code)
819  {
822  for(const auto &param : c.parameters())
824  }
825 
826  // symbol type
827  else if(t.id() == ID_symbol)
828  {
829  const symbol_typet &symbol_type = to_symbol_type(t);
830  const irep_idt class_name(symbol_type.get_identifier());
831  if(is_java_array_tag(class_name))
832  {
834  java_array_element_type(symbol_type), refs);
835  }
836  else
837  refs.insert(strip_java_namespace_prefix(class_name));
838  }
839 }
840 
848  const std::string &signature,
849  std::set<irep_idt> &refs)
850 {
851  try
852  {
853  // class signature with bounds
854  if(signature[0] == '<')
855  {
856  const std::vector<typet> types = java_generic_type_from_string(
857  erase_type_arguments(signature), signature);
858 
859  for(const auto &t : types)
861  }
862 
863  // class signature without bounds and without wildcards
864  else if(signature.find('*') == std::string::npos)
865  {
867  java_type_from_string(signature, erase_type_arguments(signature)),
868  refs);
869  }
870  }
872  {
873  // skip for now, if we cannot parse it, we cannot detect which additional
874  // classes should be loaded as dependencies
875  }
876 }
877 
884  const typet &t,
885  std::set<irep_idt> &refs)
886 {
888 }
889 
900  const symbol_typet &type,
901  const std::string &base_ref,
902  const std::string &class_name_prefix)
903  : symbol_typet(type)
904 {
905  set(ID_C_java_generic_symbol, true);
906  const typet &base_type = java_type_from_string(base_ref, class_name_prefix);
908  const java_generic_typet &gen_base_type = to_java_generic_type(base_type);
909  INVARIANT(
910  type.get_identifier() == to_symbol_type(gen_base_type.subtype()).get_identifier(),
911  "identifier of "+type.pretty()+"\n and identifier of type "+
912  gen_base_type.subtype().pretty()+"\ncreated by java_type_from_string for "+
913  base_ref+" should be equal");
914  generic_types().insert(
915  generic_types().end(),
916  gen_base_type.generic_type_arguments().begin(),
917  gen_base_type.generic_type_arguments().end());
918 }
919 
925  const java_generic_parametert &type) const
926 {
927  const auto &type_variable = type.get_name();
928  const auto &generics = generic_types();
929  for(std::size_t i = 0; i < generics.size(); ++i)
930  {
931  if(
932  is_java_generic_parameter(generics[i]) &&
933  to_java_generic_parameter(generics[i]).get_name() == type_variable)
934  return i;
935  }
936  return {};
937 }
938 
939 std::string pretty_java_type(const typet &type)
940 {
941  if(type == java_int_type())
942  return "int";
943  else if(type == java_long_type())
944  return "long";
945  else if(type == java_short_type())
946  return "short";
947  else if(type == java_byte_type())
948  return "byte";
949  else if(type == java_char_type())
950  return "char";
951  else if(type == java_float_type())
952  return "float";
953  else if(type == java_double_type())
954  return "double";
955  else if(type == java_boolean_type())
956  return "boolean";
957  else if(type == java_byte_type())
958  return "byte";
959  else if(is_reference(type))
960  {
961  if(type.subtype().id() == ID_symbol)
962  {
963  const auto &symbol_type = to_symbol_type(type.subtype());
964  const irep_idt &id = symbol_type.get_identifier();
965  if(is_java_array_tag(id))
966  return pretty_java_type(java_array_element_type(symbol_type)) + "[]";
967  else
969  }
970  else
971  return "?";
972  }
973  else
974  return "?";
975 }
976 
977 std::string pretty_signature(const java_method_typet &method_type)
978 {
979  std::ostringstream result;
980  result << '(';
981 
982  bool first = true;
983  for(const auto p : method_type.parameters())
984  {
985  if(p.get_this())
986  continue;
987 
988  if(first)
989  first = false;
990  else
991  result << ", ";
992 
993  result << pretty_java_type(p.type());
994  }
995 
996  result << ')';
997  return result.str();
998 }
The void type.
Definition: std_types.h:64
const irep_idt & get_name() const
Definition: std_types.h:182
The type of an expression.
Definition: type.h:22
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1229
semantic type conversion
Definition: std_expr.h:2111
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
std::vector< parametert > parameterst
Definition: std_types.h:767
void get_dependencies_from_generic_parameters_rec(const typet &t, std::set< irep_idt > &refs)
Definition: java_types.cpp:800
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a generic typet to a signedbv_typet.
Definition: std_types.h:1296
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:924
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:847
typet java_boolean_type()
Definition: java_types.cpp:72
const reference_typet & to_reference_type(const typet &type)
Cast a generic typet to a reference_typet.
Definition: std_types.h:1512
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
typet java_double_type()
Definition: java_types.cpp:67
reference_typet java_reference_type(const typet &subtype)
Definition: java_types.cpp:80
typet java_int_type()
Definition: java_types.cpp:32
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:392
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
Definition: std_types.h:139
const typet & java_array_element_type(const symbol_typet &array_symbol)
Return a const reference to the element type of a given java array type.
Definition: java_types.cpp:129
const java_generic_parametert & to_java_generic_parameter(const typet &type)
Definition: java_types.h:399
const componentst & components() const
Definition: std_types.h:245
typet java_long_type()
Definition: java_types.cpp:42
typet & type()
Definition: expr.h:56
An exception that is raised for unsupported class signature.
Definition: java_types.h:639
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
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:266
Structure type.
Definition: std_types.h:297
reference_typet java_array_type(const char subtype)
Construct an array pointer type.
Definition: java_types.cpp:94
bool is_java_array_tag(const irep_idt &tag)
See above.
Definition: java_types.cpp:174
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:738
reference_typet java_lang_object_type()
Definition: java_types.cpp:85
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:204
static ieee_float_spect double_precision()
Definition: ieee_float.h:80
bool can_cast_type< pointer_typet >(const typet &type)
Definition: std_types.h:1479
class floatbv_typet to_type() const
Definition: ieee_float.cpp:26
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:197
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:775
const generic_type_argumentst & generic_type_arguments() const
Definition: java_types.h:441
const irep_idt & id() const
Definition: irep.h:259
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:470
A reference into the symbol table.
Definition: std_types.h:110
reference_typet reference_type(const typet &subtype)
Definition: c_types.cpp:248
irep_idt strip_java_namespace_prefix(const irep_idt &to_strip)
Strip java:: prefix from given identifier.
Definition: java_utils.cpp:298
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:273
Fixed-width bit-vector with two&#39;s complement interpretation.
Definition: std_types.h:1271
typet java_type_from_char(char t)
Constructs a type indicated by the given character:
Definition: java_types.cpp:189
nonstd::optional< T > optionalt
Definition: optional.h:35
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:388
bool is_java_array_type(const typet &type)
Checks whether the given type is an array pointer type.
Definition: java_types.cpp:148
API to expression classes.
bool is_reference(const typet &type)
TO_BE_DOCUMENTED.
Definition: std_types.cpp:105
std::string pretty_java_type(const typet &type)
Definition: java_types.cpp:939
static ieee_float_spect single_precision()
Definition: ieee_float.h:74
#define PRECONDITION(CONDITION)
Definition: invariant.h:242
std::string pretty_signature(const java_method_typet &method_type)
Definition: java_types.cpp:977
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
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:432
const generic_typest & generic_types() const
Definition: java_types.h:708
typet java_byte_type()
Definition: java_types.cpp:52
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
typet java_short_type()
Definition: java_types.cpp:47
std::size_t get_width() const
Definition: std_types.h:1138
The reference type.
Definition: std_types.h:1492
Class to hold type with generic type arguments, for example java.util.List in either a reference of t...
Definition: java_types.h:429
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:331
const java_generic_typet & to_java_generic_type(const typet &type)
Definition: java_types.h:464
std::string gather_full_class_name(const std::string &src)
Returns the full class name, skipping over the generics.
Definition: java_types.cpp:304
API to type classes.
const java_method_typet & to_java_method_type(const typet &type)
Definition: java_types.h:289
static std::string slash_to_dot(const std::string &src)
Definition: java_types.cpp:701
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
Definition: std_types.h:1382
Base class for all expressions.
Definition: expr.h:42
const typet & find_type(const irep_namet &name) const
Definition: type.h:112
const parameterst & parameters() const
Definition: std_types.h:905
Class to hold a Java generic type parameter (also called type variable), e.g., T in List<T>...
Definition: java_types.h:343
const irep_idt get_name() const
Definition: java_types.h:370
#define UNREACHABLE
Definition: invariant.h:271
void base_type(typet &type, const namespacet &ns)
Definition: base_type.cpp:135
typet & add_type(const irep_namet &name)
Definition: type.h:107
The NIL type.
Definition: std_types.h:44
typet java_void_type()
Definition: java_types.cpp:37
typet java_bytecode_promotion(const typet &type)
Java does not support byte/short return types. These are always promoted.
Definition: java_types.cpp:208
bool is_java_generic_type(const typet &type)
Definition: java_types.h:457
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:652
java_generic_symbol_typet(const symbol_typet &type, const std::string &base_ref, const std::string &class_name_prefix)
Construct a generic symbol type by extending the symbol type type with generic types extracted from t...
Definition: java_types.cpp:899
typet java_char_type()
Definition: java_types.cpp:57
The C/C++ Booleans.
Definition: std_types.h:1538
const typet & subtype() const
Definition: type.h:33
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:278
symbol_typet java_classname(const std::string &id)
Definition: java_types.cpp:710
typet java_float_type()
Definition: java_types.cpp:62
const typet & return_type() const
Definition: std_types.h:895
bool can_cast_type< symbol_typet >(const typet &type)
Definition: std_types.h:155
const irep_idt & get_identifier() const
Definition: std_types.h:123
char java_char_from_type(const typet &type)
Definition: java_types.cpp:611
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
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:238