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 
90 reference_typet java_array_type(const char subtype)
91 {
92  std::string subtype_str;
93 
94  switch(subtype)
95  {
96  case 'b': subtype_str="byte"; break;
97  case 'f': subtype_str="float"; break;
98  case 'd': subtype_str="double"; break;
99  case 'i': subtype_str="int"; break;
100  case 'c': subtype_str="char"; break;
101  case 's': subtype_str="short"; break;
102  case 'z': subtype_str="boolean"; break;
103  case 'v': subtype_str="void"; break;
104  case 'j': subtype_str="long"; break;
105  case 'l': subtype_str="long"; break;
106  case 'a': subtype_str="reference"; break;
107  default:
108 #ifdef DEBUG
109  std::cout << "Unrecognised subtype str: " << subtype << std::endl;
110 #endif
111  UNREACHABLE;
112  }
113 
114  irep_idt class_name="array["+subtype_str+"]";
115 
116  symbol_typet symbol_type("java::"+id2string(class_name));
117  symbol_type.set(ID_C_base_name, class_name);
118  symbol_type.set(ID_C_element_type, java_type_from_char(subtype));
119 
120  return java_reference_type(symbol_type);
121 }
122 
127 {
128  INVARIANT(
129  is_java_array_tag(array_type.get_identifier()),
130  "Symbol should have array tag");
131  return array_type.find_type(ID_C_element_type);
132 }
133 
137 bool is_java_array_tag(const irep_idt& tag)
138 {
139  return has_prefix(id2string(tag), "java::array[");
140 }
141 
142 bool is_reference_type(const char t)
143 {
144  return 'a'==t;
145 }
146 
148 {
149  switch(t)
150  {
151  case 'i': return java_int_type();
152  case 'j': return java_long_type();
153  case 'l': return java_long_type();
154  case 's': return java_short_type();
155  case 'b': return java_byte_type();
156  case 'c': return java_char_type();
157  case 'f': return java_float_type();
158  case 'd': return java_double_type();
159  case 'z': return java_boolean_type();
160  case 'a': return java_reference_type(void_typet());
161  default: UNREACHABLE; return nil_typet();
162  }
163 }
164 
167 {
168  if(type==java_boolean_type() ||
169  type==java_char_type() ||
170  type==java_byte_type() ||
171  type==java_short_type())
172  return java_int_type();
173 
174  return type;
175 }
176 
179 {
180  typet new_type=java_bytecode_promotion(expr.type());
181 
182  if(new_type==expr.type())
183  return expr;
184  else
185  return typecast_exprt(expr, new_type);
186 }
187 
197  java_generic_typet &generic_type,
198  const std::string &type_arguments,
199  const std::string &class_name_prefix)
200 {
201  PRECONDITION(type_arguments.size() >= 2);
202  PRECONDITION(type_arguments[0] == '<');
203  PRECONDITION(type_arguments[type_arguments.size() - 1] == '>');
204 
205  // Parse contained arguments, can be either type parameters (`TT;`)
206  // or instantiated types - either generic types (`LList<LInteger;>;`) or
207  // just references (`Ljava/lang/Foo;`)
208  std::vector<typet> type_arguments_types =
209  parse_list_types(type_arguments, class_name_prefix, '<', '>');
210 
211  // We should have at least one generic type argument
212  CHECK_RETURN(!type_arguments_types.empty());
213 
214  // Add the type arguments to the generic type
215  std::transform(
216  type_arguments_types.begin(),
217  type_arguments_types.end(),
218  std::back_inserter(generic_type.generic_type_arguments()),
219  [](const typet &type) -> reference_typet
220  {
221  INVARIANT(
222  is_reference(type), "All generic type arguments should be references");
223  return to_reference_type(type);
224  });
225 }
226 
231 std::string erase_type_arguments(const std::string &src)
232 {
233  std::string class_name = src;
234  std::size_t f_pos = class_name.find('<', 1);
235 
236  while(f_pos != std::string::npos)
237  {
238  std::size_t e_pos = find_closing_delimiter(class_name, f_pos, '<', '>');
239  if(e_pos == std::string::npos)
240  {
242  "Failed to find generic signature closing delimiter (or recursive "
243  "generic): " +
244  src);
245  }
246 
247  // erase generic information between brackets
248  class_name.erase(f_pos, e_pos - f_pos + 1);
249 
250  // Search the remainder of the string for generic signature
251  f_pos = class_name.find('<', f_pos + 1);
252  }
253  return class_name;
254 }
255 
262 std::string gather_full_class_name(const std::string &src)
263 {
264  PRECONDITION(src.size() >= 2);
265  PRECONDITION(src[0] == 'L');
266  PRECONDITION(src[src.size() - 1] == ';');
267 
268  std::string class_name = src.substr(1, src.size() - 2);
269 
270  class_name = erase_type_arguments(class_name);
271 
272  std::replace(class_name.begin(), class_name.end(), '.', '$');
273  std::replace(class_name.begin(), class_name.end(), '/', '.');
274  return class_name;
275 }
276 
289 std::vector<typet> parse_list_types(
290  const std::string src,
291  const std::string class_name_prefix,
292  const char opening_bracket,
293  const char closing_bracket)
294 {
295  PRECONDITION(src.size() >= 2);
296  PRECONDITION(src[0] == opening_bracket);
297  PRECONDITION(src[src.size() - 1] == closing_bracket);
298 
299  // Loop over the types in the given string, parsing each one in turn
300  // and adding to the type_list
301  std::vector<typet> type_list;
302  for(std::size_t i = 1; i < src.size() - 1; i++)
303  {
304  size_t start = i;
305  while(i < src.size())
306  {
307  // type is an object type or instantiated generic type
308  if(src[i] == 'L')
309  {
311  break;
312  }
313 
314  // type is an array
315  else if(src[i] == '[')
316  i++;
317 
318  // type is a type variable/parameter
319  else if(src[i] == 'T')
320  i = src.find(';', i); // ends on ;
321 
322  // type is an atomic type (just one character)
323  else
324  {
325  break;
326  }
327  }
328 
329  std::string sub_str = src.substr(start, i - start + 1);
330  const typet &new_type = java_type_from_string(sub_str, class_name_prefix);
331  INVARIANT(new_type != nil_typet(), "Failed to parse type");
332 
333  type_list.push_back(new_type);
334  }
335  return type_list;
336 }
337 
346 build_class_name(const std::string &src, const std::string &class_name_prefix)
347 {
348  PRECONDITION(src[0] == 'L');
349 
350  // All reference types must end on a ;
351  PRECONDITION(src[src.size() - 1] == ';');
352 
353  std::string container_class = gather_full_class_name(src);
354  std::string identifier = "java::" + container_class;
355  symbol_typet symbol_type(identifier);
356  symbol_type.set(ID_C_base_name, container_class);
357 
358  std::size_t f_pos = src.find('<', 1);
359  if(f_pos != std::string::npos)
360  {
361  java_generic_typet result(symbol_type);
362  // get generic type information
363  do
364  {
365  std::size_t e_pos = find_closing_delimiter(src, f_pos, '<', '>');
366  if(e_pos == std::string::npos)
368  "Parsing type with unmatched generic bracket: " + src);
369 
371  result, src.substr(f_pos, e_pos - f_pos + 1), class_name_prefix);
372 
373  // Look for the next generic type info (if it exists)
374  f_pos = src.find('<', e_pos + 1);
375  } while(f_pos != std::string::npos);
376  return result;
377  }
378 
379  return java_reference_type(symbol_type);
380 }
381 
391  const std::string src,
392  size_t starting_point)
393 {
394  PRECONDITION(src[starting_point] == 'L');
395  size_t next_semi_colon = src.find(';', starting_point);
396  INVARIANT(
397  next_semi_colon != std::string::npos,
398  "There must be a semi-colon somewhere in the input");
399  size_t next_angle_bracket = src.find('<', starting_point);
400 
401  while(next_angle_bracket < next_semi_colon)
402  {
403  size_t end_bracket =
404  find_closing_delimiter(src, next_angle_bracket, '<', '>');
405  INVARIANT(
406  end_bracket != std::string::npos, "Must find matching angle bracket");
407 
408  next_semi_colon = src.find(';', end_bracket + 1);
409  next_angle_bracket = src.find('<', end_bracket + 1);
410  }
411 
412  return next_semi_colon;
413 }
414 
429  const std::string &src,
430  const std::string &class_name_prefix)
431 {
432  if(src.empty())
433  return nil_typet();
434 
435  // a java type is encoded in different ways
436  // - a method type is encoded as '(...)R' where the parenthesis include the
437  // parameter types and R is the type of the return value
438  // - atomic types are encoded as single characters
439  // - array types are encoded as '[' followed by the type of the array
440  // content
441  // - object types are named with prefix 'L' and suffix ';', e.g.,
442  // Ljava/lang/Object;
443  // - type variables are similar to object types but have the prefix 'T'
444  switch(src[0])
445  {
446  case '<':
447  {
448  // The method signature can optionally have a collection of formal
449  // type parameters (e.g. on generic methods on non-generic classes
450  // or generic static methods). For now we skip over this part of the
451  // signature and continue parsing the rest of the signature as normal
452  // So for example, the following java method:
453  // static void <T, U> foo(T t, U u, int x);
454  // Would have a signature that looks like:
455  // <T:Ljava/lang/Object;U:Ljava/lang/Object;>(TT;TU;I)V
456  // So we skip all inside the angle brackets and parse the rest of the
457  // string:
458  // (TT;TU;I)V
459  size_t closing_generic=find_closing_delimiter(src, 0, '<', '>');
460  if(closing_generic==std::string::npos)
461  {
463  "Failed to find generic signature closing delimiter");
464  }
465 
466  // If there are any bounds between '<' and '>' then we cannot currently
467  // parse them, so we give up. This only happens when parsing the
468  // signature, so we'll fall back to the result of parsing the
469  // descriptor, which will respect the bounds correctly.
470  const size_t colon_pos = src.find(':');
471  if(colon_pos != std::string::npos && colon_pos < closing_generic)
472  {
474  "Cannot currently parse bounds on generic types");
475  }
476 
477  const typet &method_type=java_type_from_string(
478  src.substr(closing_generic+1, std::string::npos), class_name_prefix);
479 
480  // This invariant being violated means that tkiley has not understood
481  // part of the signature spec.
482  // Only class and method signatures can start with a '<' and classes are
483  // handled separately.
484  INVARIANT(
485  method_type.id()==ID_code,
486  "This should correspond to method signatures only");
487 
488  return method_type;
489  }
490  case '(': // function type
491  {
492  std::size_t e_pos=src.rfind(')');
493  if(e_pos==std::string::npos)
494  return nil_typet();
495 
496  typet return_type = java_type_from_string(
497  std::string(src, e_pos + 1, std::string::npos), class_name_prefix);
498 
499  std::vector<typet> param_types =
500  parse_list_types(src.substr(0, e_pos + 1), class_name_prefix, '(', ')');
501 
502  // create parameters for each type
503  code_typet::parameterst parameters;
504  std::transform(
505  param_types.begin(),
506  param_types.end(),
507  std::back_inserter(parameters),
508  [](const typet &type) { return code_typet::parametert(type); });
509 
510  return code_typet(std::move(parameters), std::move(return_type));
511  }
512 
513  case '[': // array type
514  {
515  // If this is a reference array, we generate a plain array[reference]
516  // with void* members, but note the real type in ID_C_element_type.
517  if(src.size()<=1)
518  return nil_typet();
519  char subtype_letter=src[1];
520  const typet subtype=
521  java_type_from_string(src.substr(1, std::string::npos),
522  class_name_prefix);
523  if(subtype_letter=='L' || // [L denotes a reference array of some sort.
524  subtype_letter=='[' || // Array-of-arrays
525  subtype_letter=='T') // Array of generic types
526  subtype_letter='A';
527  typet tmp=java_array_type(std::tolower(subtype_letter));
528  tmp.subtype().set(ID_C_element_type, subtype);
529  return tmp;
530  }
531 
532  case 'B': return java_byte_type();
533  case 'F': return java_float_type();
534  case 'D': return java_double_type();
535  case 'I': return java_int_type();
536  case 'C': return java_char_type();
537  case 'S': return java_short_type();
538  case 'Z': return java_boolean_type();
539  case 'V': return java_void_type();
540  case 'J': return java_long_type();
541  case 'T':
542  {
543  // parse name of type variable
544  INVARIANT(src[src.size()-1]==';', "Generic type name must end on ';'.");
545  PRECONDITION(!class_name_prefix.empty());
546  irep_idt type_var_name(class_name_prefix+"::"+src.substr(1, src.size()-2));
548  type_var_name,
549  to_symbol_type(java_type_from_string("Ljava/lang/Object;").subtype()));
550  }
551  case 'L':
552  {
553  return build_class_name(src, class_name_prefix);
554  }
555  case '*':
556  case '+':
557  case '-':
558  {
559 #ifdef DEBUG
560  std::cout << class_name_prefix << std::endl;
561 #endif
562  throw unsupported_java_class_signature_exceptiont("wild card generic");
563  }
564  default:
565  return nil_typet();
566  }
567 }
568 
569 char java_char_from_type(const typet &type)
570 {
571  const irep_idt &id=type.id();
572 
573  if(id==ID_signedbv)
574  {
575  const size_t width=to_signedbv_type(type).get_width();
576  if(to_signedbv_type(java_int_type()).get_width()==width)
577  return 'i';
578  else if(to_signedbv_type(java_long_type()).get_width()==width)
579  return 'l';
580  else if(to_signedbv_type(java_short_type()).get_width()==width)
581  return 's';
582  else if(to_signedbv_type(java_byte_type()).get_width()==width)
583  return 'b';
584  }
585  else if(id==ID_unsignedbv)
586  return 'c';
587  else if(id==ID_floatbv)
588  {
589  const size_t width(to_floatbv_type(type).get_width());
590  if(to_floatbv_type(java_float_type()).get_width()==width)
591  return 'f';
592  else if(to_floatbv_type(java_double_type()).get_width()==width)
593  return 'd';
594  }
595  else if(id==ID_c_bool)
596  return 'z';
597 
598  return 'a';
599 }
600 
610 std::vector<typet> java_generic_type_from_string(
611  const std::string &class_name,
612  const std::string &src)
613 {
616  size_t signature_end = find_closing_delimiter(src, 0, '<', '>');
617  INVARIANT(
618  src[0]=='<' && signature_end!=std::string::npos,
619  "Class signature has unexpected format");
620  std::string signature(src.substr(1, signature_end-1));
621 
622  if(signature.find(";:")!=std::string::npos)
623  throw unsupported_java_class_signature_exceptiont("multiple bounds");
624 
625  PRECONDITION(signature[signature.size()-1]==';');
626 
627  std::vector<typet> types;
628  size_t var_sep=signature.find(';');
629  while(var_sep!=std::string::npos)
630  {
631  size_t bound_sep=signature.find(':');
632  INVARIANT(bound_sep!=std::string::npos, "No bound for type variable.");
633 
634  // is bound an interface?
635  // in this case the separator is '::'
636  if(signature[bound_sep + 1] == ':')
637  {
638  INVARIANT(
639  signature[bound_sep + 2] != ':', "Unknown bound for type variable.");
640  bound_sep++;
641  }
642 
643  std::string type_var_name(
644  "java::"+class_name+"::"+signature.substr(0, bound_sep));
645  std::string bound_type(signature.substr(bound_sep+1, var_sep-bound_sep));
646 
647  java_generic_parametert type_var_type(
648  type_var_name,
649  to_symbol_type(java_type_from_string(bound_type, class_name).subtype()));
650 
651  types.push_back(type_var_type);
652  signature=signature.substr(var_sep+1, std::string::npos);
653  var_sep=signature.find(';');
654  }
655  return types;
656 }
657 
658 // java/lang/Object -> java.lang.Object
659 static std::string slash_to_dot(const std::string &src)
660 {
661  std::string result=src;
662  for(std::string::iterator it=result.begin(); it!=result.end(); it++)
663  if(*it=='/')
664  *it='.';
665  return result;
666 }
667 
668 symbol_typet java_classname(const std::string &id)
669 {
670  if(!id.empty() && id[0]=='[')
671  return to_symbol_type(java_type_from_string(id).subtype());
672 
673  std::string class_name=id;
674 
675  class_name=slash_to_dot(class_name);
676  irep_idt identifier="java::"+class_name;
677  symbol_typet symbol_type(identifier);
678  symbol_type.set(ID_C_base_name, class_name);
679 
680  return symbol_type;
681 }
682 
697 {
698  bool correct_num_components=type.components().size()==3;
699  if(!correct_num_components)
700  return false;
701 
702  // First component, the base class (Object) data
703  const struct_union_typet::componentt base_class_component=
704  type.components()[0];
705 
706  bool base_component_valid=true;
707  base_component_valid&=base_class_component.get_name()=="@java.lang.Object";
708 
709  bool length_component_valid=true;
710  const struct_union_typet::componentt length_component=
711  type.components()[1];
712  length_component_valid&=length_component.get_name()=="length";
713  length_component_valid&=length_component.type()==java_int_type();
714 
715  bool data_component_valid=true;
716  const struct_union_typet::componentt data_component=
717  type.components()[2];
718  data_component_valid&=data_component.get_name()=="data";
719  data_component_valid&=data_component.type().id()==ID_pointer;
720 
721  return correct_num_components &&
722  base_component_valid &&
723  length_component_valid &&
724  data_component_valid;
725 }
726 
733 bool equal_java_types(const typet &type1, const typet &type2)
734 {
735  bool arrays_with_same_element_type = true;
736  if(
737  type1.id() == ID_pointer && type2.id() == ID_pointer &&
738  type1.subtype().id() == ID_symbol && type2.subtype().id() == ID_symbol)
739  {
740  const symbol_typet &subtype_symbol1 = to_symbol_type(type1.subtype());
741  const symbol_typet &subtype_symbol2 = to_symbol_type(type2.subtype());
742  if(
743  subtype_symbol1.get_identifier() == subtype_symbol2.get_identifier() &&
744  is_java_array_tag(subtype_symbol1.get_identifier()))
745  {
746  const typet &array_element_type1 =
747  java_array_element_type(subtype_symbol1);
748  const typet &array_element_type2 =
749  java_array_element_type(subtype_symbol2);
750 
751  arrays_with_same_element_type =
752  equal_java_types(array_element_type1, array_element_type2);
753  }
754  }
755  return (type1 == type2 && arrays_with_same_element_type);
756 }
757 
759  const typet &t,
760  std::set<irep_idt> &refs)
761 {
762  // Java generic type that holds different types in its type arguments
763  if(is_java_generic_type(t))
764  {
765  for(const auto type_arg : to_java_generic_type(t).generic_type_arguments())
767  }
768 
769  // Java reference type
770  else if(t.id() == ID_pointer)
771  {
773  }
774 
775  // method type with parameters and return value
776  else if(t.id() == ID_code)
777  {
778  const code_typet &c = to_code_type(t);
780  for(const auto &param : c.parameters())
782  }
783 
784  // symbol type
785  else if(t.id() == ID_symbol)
786  {
787  const symbol_typet &symbol_type = to_symbol_type(t);
788  const irep_idt class_name(symbol_type.get_identifier());
789  if(is_java_array_tag(class_name))
790  {
792  java_array_element_type(symbol_type), refs);
793  }
794  else
795  refs.insert(strip_java_namespace_prefix(class_name));
796  }
797 }
798 
806  const std::string &signature,
807  std::set<irep_idt> &refs)
808 {
809  try
810  {
811  // class signature with bounds
812  if(signature[0] == '<')
813  {
814  const std::vector<typet> types = java_generic_type_from_string(
815  erase_type_arguments(signature), signature);
816 
817  for(const auto &t : types)
819  }
820 
821  // class signature without bounds and without wildcards
822  else if(signature.find('*') == std::string::npos)
823  {
825  java_type_from_string(signature, erase_type_arguments(signature)),
826  refs);
827  }
828  }
830  {
831  // skip for now, if we cannot parse it, we cannot detect which additional
832  // classes should be loaded as dependencies
833  }
834 }
835 
842  const typet &t,
843  std::set<irep_idt> &refs)
844 {
846 }
847 
858  const symbol_typet &type,
859  const std::string &base_ref,
860  const std::string &class_name_prefix)
861  : symbol_typet(type)
862 {
863  set(ID_C_java_generic_symbol, true);
864  const typet &base_type = java_type_from_string(base_ref, class_name_prefix);
866  const java_generic_typet &gen_base_type = to_java_generic_type(base_type);
867  INVARIANT(
868  type.get_identifier() == to_symbol_type(gen_base_type.subtype()).get_identifier(),
869  "identifier of "+type.pretty()+"\n and identifier of type "+
870  gen_base_type.subtype().pretty()+"\ncreated by java_type_from_string for "+
871  base_ref+" should be equal");
872  generic_types().insert(
873  generic_types().end(),
874  gen_base_type.generic_type_arguments().begin(),
875  gen_base_type.generic_type_arguments().end());
876 }
877 
883  const java_generic_parametert &type) const
884 {
885  const auto &type_variable = type.get_name();
886  const auto &generics = generic_types();
887  for(std::size_t i = 0; i < generics.size(); ++i)
888  {
889  if(
890  is_java_generic_parameter(generics[i]) &&
891  to_java_generic_parameter(generics[i]).get_name() == type_variable)
892  return i;
893  }
894  return {};
895 }
896 
897 std::string pretty_java_type(const typet &type)
898 {
899  if(type == java_int_type())
900  return "int";
901  else if(type == java_long_type())
902  return "long";
903  else if(type == java_short_type())
904  return "short";
905  else if(type == java_byte_type())
906  return "byte";
907  else if(type == java_char_type())
908  return "char";
909  else if(type == java_float_type())
910  return "float";
911  else if(type == java_double_type())
912  return "double";
913  else if(type == java_boolean_type())
914  return "boolean";
915  else if(type == java_byte_type())
916  return "byte";
917  else if(is_reference(type))
918  {
919  if(type.subtype().id() == ID_symbol)
920  {
921  const auto &symbol_type = to_symbol_type(type.subtype());
922  const irep_idt &id = symbol_type.get_identifier();
923  if(is_java_array_tag(id))
924  return pretty_java_type(java_array_element_type(symbol_type)) + "[]";
925  else
927  }
928  else
929  return "?";
930  }
931  else
932  return "?";
933 }
934 
935 std::string pretty_signature(const code_typet &code_type)
936 {
937  std::ostringstream result;
938  result << '(';
939 
940  bool first = true;
941  for(const auto p : code_type.parameters())
942  {
943  if(p.get_this())
944  continue;
945 
946  if(first)
947  first = false;
948  else
949  result << ", ";
950 
951  result << pretty_java_type(p.type());
952  }
953 
954  result << ')';
955  return result.str();
956 }
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:1220
semantic type conversion
Definition: std_expr.h:2111
Base type of functions.
Definition: std_types.h:764
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
void get_dependencies_from_generic_parameters_rec(const typet &t, std::set< irep_idt > &refs)
Definition: java_types.cpp:758
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a generic typet to a signedbv_typet.
Definition: std_types.h:1287
optionalt< size_t > generic_type_index(const java_generic_parametert &type) const
Check if this symbol has the given generic type.
Definition: java_types.cpp:882
void 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:805
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:1503
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
typet java_double_type()
Definition: java_types.cpp:67
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:987
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:281
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
Definition: std_types.h:139
std::vector< parametert > parameterst
Definition: std_types.h:767
const java_generic_parametert & to_java_generic_parameter(const typet &type)
Definition: java_types.h:288
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:528
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:245
Structure type.
Definition: std_types.h:297
reference_typet java_array_type(const char subtype)
Definition: java_types.cpp:90
bool is_java_array_tag(const irep_idt &tag)
See above.
Definition: java_types.cpp:137
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:696
reference_typet java_lang_object_type()
Definition: java_types.cpp:85
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:205
static ieee_float_spect double_precision()
Definition: ieee_float.h:80
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:200
bool equal_java_types(const typet &type1, const typet &type2)
Compares the types, including checking element types if both types are arrays.
Definition: java_types.cpp:733
const generic_type_argumentst & generic_type_arguments() const
Definition: java_types.h:330
const irep_idt & id() const
Definition: irep.h:189
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:428
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:301
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:231
Fixed-width bit-vector with two&#39;s complement interpretation.
Definition: std_types.h:1262
typet java_type_from_char(char t)
Definition: java_types.cpp:147
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:346
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:897
static ieee_float_spect single_precision()
Definition: ieee_float.h:74
#define PRECONDITION(CONDITION)
Definition: invariant.h:230
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:390
const generic_typest & generic_types() const
Definition: java_types.h:597
typet java_byte_type()
Definition: java_types.cpp:52
typet java_short_type()
Definition: java_types.cpp:47
bool is_reference_type(const char t)
Definition: java_types.cpp:142
std::size_t get_width() const
Definition: std_types.h:1129
The reference type.
Definition: std_types.h:1483
Class to hold type with generic type arguments, for example java.util.List in either a reference of t...
Definition: java_types.h:318
std::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:289
const java_generic_typet & to_java_generic_type(const typet &type)
Definition: java_types.h:353
std::string gather_full_class_name(const std::string &src)
Returns the full class name, skipping over the generics.
Definition: java_types.cpp:262
API to type classes.
static std::string slash_to_dot(const std::string &src)
Definition: java_types.cpp:659
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
Definition: std_types.h:1373
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:232
const irep_idt get_name() const
Definition: java_types.h:259
#define UNREACHABLE
Definition: invariant.h:250
void base_type(typet &type, const namespacet &ns)
Definition: base_type.cpp:135
typet java_array_element_type(const symbol_typet &array_type)
Return the type of the elements of a given java array type.
Definition: java_types.cpp:126
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:166
bool is_java_generic_type(const typet &type)
Definition: java_types.h:346
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:610
java_generic_symbol_typet(const symbol_typet &type, const std::string &base_ref, const std::string &class_name_prefix)
Construct a generic symbol type by extending the symbol type type with generic types extracted from t...
Definition: java_types.cpp:857
typet java_char_type()
Definition: java_types.cpp:57
The C/C++ Booleans.
Definition: std_types.h:1529
const typet & subtype() const
Definition: type.h:33
symbol_typet java_classname(const std::string &id)
Definition: java_types.cpp:668
typet java_float_type()
Definition: java_types.cpp:62
const typet & return_type() const
Definition: std_types.h:895
const irep_idt & get_identifier() const
Definition: std_types.h:123
char java_char_from_type(const typet &type)
Definition: java_types.cpp:569
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
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:196
std::string pretty_signature(const code_typet &code_type)
Definition: java_types.cpp:935