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