cprover
Loading...
Searching...
No Matches
java_bytecode_convert_class.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: JAVA Bytecode Language Conversion
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
13
14#ifdef DEBUG
15#include <iostream>
16#endif
17
18#include "ci_lazy_methods.h"
20#include "java_root_class.h"
21#include "java_types.h"
22#include "java_utils.h"
23
24#include <util/arith_tools.h>
26#include <util/namespace.h>
27#include <util/prefix.h>
28#include <util/std_expr.h>
29
31{
32public:
48
66 {
67 PRECONDITION(!parse_trees.empty());
68 const java_bytecode_parse_treet &parse_tree = parse_trees.front();
69
70 // Add array types to the symbol table
72
73 const bool loading_success =
74 parse_tree.loading_successful &&
75 !no_load_classes.count(id2string(parse_tree.parsed_class.name));
77 {
79 for(auto overlay_class_it = std::next(parse_trees.begin());
82 {
83 overlay_classes.push_front(std::cref(overlay_class_it->parsed_class));
84 }
86 }
87
88 // Add as string type if relevant
89 const irep_idt &class_name = parse_tree.parsed_class.name;
92 else if(!loading_success)
93 // Generate stub if couldn't load from bytecode and wasn't string type
95 class_name,
99 }
100
105
106private:
109 const size_t max_array_length;
112
113 // conversion
114 typedef std::list<std::reference_wrapper<const classt>> overlay_classest;
115 void convert(const classt &c, const overlay_classest &overlay_classes);
116 void convert(symbolt &class_symbol, const fieldt &f);
117
133 static bool is_overlay_method(const methodt &method)
134 {
135 return method.has_annotation(ID_overlay_method);
136 }
137
158 static bool is_ignored_method(
159 const irep_idt &class_name, const methodt &method)
160 {
161 static irep_idt org_cprover_CProver_name = "org.cprover.CProver";
162 return
163 (class_name == org_cprover_CProver_name &&
164 cprover_methods_to_ignore.count(id2string(method.name)) != 0) ||
166 }
167
169 const fieldt &field,
171 const struct_union_typet::componentst &fields) const;
172
173 std::unordered_set<std::string> no_load_classes;
174};
175
188{
189 if(signature.has_value())
190 {
191 // skip the (potential) list of generic parameters at the beginning of the
192 // signature
193 const size_t start =
194 signature.value().front() == '<'
195 ? find_closing_delimiter(signature.value(), 0, '<', '>') + 1
196 : 0;
197
198 // extract the superclass reference
199 const size_t end =
201 const std::string superclass_ref =
202 signature.value().substr(start, (end - start) + 1);
203
204 // if the superclass is generic then the reference is of form
205 // `Lsuperclass-name<generic-types;>;` if it is implicitly generic, then the
206 // reference is of the form
207 // `Lsuperclass-name<Tgeneric-types;>.Innerclass-Name`
208 if(superclass_ref.find('<') != std::string::npos)
209 return superclass_ref;
210 }
211 return {};
212}
213
227 const optionalt<std::string> &signature,
228 const std::string &interface_name)
229{
230 if(signature.has_value())
231 {
232 // skip the (potential) list of generic parameters at the beginning of the
233 // signature
234 size_t start =
235 signature.value().front() == '<'
236 ? find_closing_delimiter(signature.value(), 0, '<', '>') + 1
237 : 0;
238
239 // skip the superclass reference (if there is at least one interface
240 // reference in the signature, then there is a superclass reference)
241 start =
243
244 // if the interface name includes package name, convert dots to slashes
246 std::replace(
249 '.',
250 '/');
251
252 start =
253 signature.value().find("L" + interface_name_slash_to_dot + "<", start);
254 if(start != std::string::npos)
255 {
256 const size_t &end =
258 return signature.value().substr(start, (end - start) + 1);
259 }
260 }
261 return {};
262}
263
268 const classt &c,
270{
271 std::string qualified_classname="java::"+id2string(c.name);
273 {
274 log.debug() << "Skip class " << c.name << " (already loaded)"
275 << messaget::eom;
276 return;
277 }
278
280 if(c.signature.has_value() && c.signature.value()[0]=='<')
281 {
283#ifdef DEBUG
284 std::cout << "INFO: found generic class signature "
285 << c.signature.value()
286 << " in parsed class "
287 << c.name << "\n";
288#endif
289 try
290 {
291 const std::vector<typet> &generic_types=java_generic_type_from_string(
292 id2string(c.name),
293 c.signature.value());
294 for(const typet &t : generic_types)
295 {
296 generic_class_type.generic_types()
297 .push_back(to_java_generic_parameter(t));
298 }
300 }
302 {
303 log.debug() << "Class: " << c.name
304 << "\n could not parse signature: " << c.signature.value()
305 << "\n " << e.what()
306 << "\n ignoring that the class is generic" << messaget::eom;
307 }
308 }
309
310 class_type.set_tag(c.name);
311 class_type.set_inner_name(c.inner_name);
312 class_type.set_abstract(c.is_abstract);
313 class_type.set_is_annotation(c.is_annotation);
314 class_type.set_interface(c.is_interface);
315 class_type.set_synthetic(c.is_synthetic);
316 class_type.set_final(c.is_final);
317 class_type.set_is_inner_class(c.is_inner_class);
318 class_type.set_is_static_class(c.is_static_class);
319 class_type.set_is_anonymous_class(c.is_anonymous_class);
320 class_type.set_outer_class(c.outer_class);
321 class_type.set_super_class(c.super_class);
322 if(c.is_enum)
323 {
324 if(max_array_length != 0 && c.enum_elements > max_array_length)
325 {
326 log.warning() << "Java Enum " << c.name
327 << " won't work properly because max "
328 << "array length (" << max_array_length
329 << ") is less than the "
330 << "enum size (" << c.enum_elements << ")" << messaget::eom;
331 }
332 class_type.set(
334 std::to_string(c.enum_elements+1));
335 class_type.set_is_enumeration(true);
336 }
337
338 if(c.is_public)
339 class_type.set_access(ID_public);
340 else if(c.is_protected)
341 class_type.set_access(ID_protected);
342 else if(c.is_private)
343 class_type.set_access(ID_private);
344 else
345 class_type.set_access(ID_default);
346
347 if(!c.super_class.empty())
348 {
349 const struct_tag_typet base("java::" + id2string(c.super_class));
350
351 // if the superclass is generic then the class has the superclass reference
352 // including the generic info in its signature
353 // e.g., signature for class 'A<T>' that extends
354 // 'Generic<Integer>' is '<T:Ljava/lang/Object;>LGeneric<LInteger;>;'
357 if(superclass_ref.has_value())
358 {
359 try
360 {
362 base, superclass_ref.value(), qualified_classname);
363 class_type.add_base(generic_base);
364 }
366 {
367 log.debug() << "Superclass: " << c.super_class
368 << " of class: " << c.name
369 << "\n could not parse signature: "
370 << superclass_ref.value() << "\n " << e.what()
371 << "\n ignoring that the superclass is generic"
372 << messaget::eom;
373 class_type.add_base(base);
374 }
375 }
376 else
377 {
378 class_type.add_base(base);
379 }
381 base_class_field.type() = class_type.bases().at(0).type();
382 base_class_field.set_name("@" + id2string(c.super_class));
383 base_class_field.set_base_name("@" + id2string(c.super_class));
384 base_class_field.set_pretty_name("@" + id2string(c.super_class));
385 class_type.components().push_back(base_class_field);
386 }
387
388 // interfaces are recorded as bases
389 for(const auto &interface : c.implements)
390 {
391 const struct_tag_typet base("java::" + id2string(interface));
392
393 // if the interface is generic then the class has the interface reference
394 // including the generic info in its signature
395 // e.g., signature for class 'A implements GenericInterface<Integer>' is
396 // 'Ljava/lang/Object;LGenericInterface<LInteger;>;'
399 if(interface_ref.has_value())
400 {
401 try
402 {
404 base, interface_ref.value(), qualified_classname);
405 class_type.add_base(generic_base);
406 }
408 {
409 log.debug() << "Interface: " << interface << " of class: " << c.name
410 << "\n could not parse signature: " << interface_ref.value()
411 << "\n " << e.what()
412 << "\n ignoring that the interface is generic"
413 << messaget::eom;
414 class_type.add_base(base);
415 }
416 }
417 else
418 {
419 class_type.add_base(base);
420 }
421 }
422
423 // now do lambda method handles (bootstrap methods)
424 for(const auto &lambda_entry : c.lambda_method_handle_map)
425 {
426 // if the handle is of unknown type, we still need to store it to preserve
427 // the correct indexing (invokedynamic instructions will retrieve
428 // method handles by index)
429 lambda_entry.second.is_unknown_handle()
430 ? class_type.add_unknown_lambda_method_handle()
431 : class_type.add_lambda_method_handle(
432 lambda_entry.second.get_method_descriptor(),
433 lambda_entry.second.handle_type);
434 }
435
436 // Load annotations
437 if(!c.annotations.empty())
438 convert_annotations(c.annotations, class_type.get_annotations());
439
440 // the base name is the name of the class without the package
441 const irep_idt base_name = [](const std::string &full_name) {
442 const size_t last_dot = full_name.find_last_of('.');
443 return last_dot == std::string::npos
444 ? full_name
445 : std::string(full_name, last_dot + 1, std::string::npos);
446 }(id2string(c.name));
447
448 // produce class symbol
449 symbolt new_symbol;
450 new_symbol.base_name = base_name;
451 new_symbol.pretty_name=c.name;
452 new_symbol.name=qualified_classname;
453 class_type.set_name(new_symbol.name);
454 new_symbol.type=class_type;
455 new_symbol.mode=ID_java;
456 new_symbol.is_type=true;
457
458 symbolt *class_symbol;
459
460 // add before we do members
461 log.debug() << "Adding symbol: class '" << c.name << "'" << messaget::eom;
462 if(symbol_table.move(new_symbol, class_symbol))
463 {
464 log.error() << "failed to add class symbol " << new_symbol.name
465 << messaget::eom;
466 throw 0;
467 }
468
469 // Now do fields
470 const class_typet::componentst &fields =
471 to_class_type(class_symbol->type).components();
472 // Include fields from overlay classes as they will be required by the
473 // methods defined there
474 for(auto overlay_class : overlay_classes)
475 {
476 for(const auto &field : overlay_class.get().fields)
477 {
478 std::string field_id = qualified_classname + "." + id2string(field.name);
479 if(check_field_exists(field, field_id, fields))
480 {
481 std::string err =
482 "Duplicate field definition for " + field_id + " in overlay class";
483 // TODO: This could just be a warning if the types match
484 log.error() << err << messaget::eom;
485 throw err.c_str();
486 }
487 log.debug() << "Adding symbol from overlay class: field '" << field.name
488 << "'" << messaget::eom;
489 convert(*class_symbol, field);
490 POSTCONDITION(check_field_exists(field, field_id, fields));
491 }
492 }
493 for(const auto &field : c.fields)
494 {
495 std::string field_id = qualified_classname + "." + id2string(field.name);
496 if(check_field_exists(field, field_id, fields))
497 {
498 // TODO: This could be a warning if the types match
499 log.error() << "Field definition for " << field_id
500 << " already loaded from overlay class" << messaget::eom;
501 continue;
502 }
503 log.debug() << "Adding symbol: field '" << field.name << "'"
504 << messaget::eom;
505 convert(*class_symbol, field);
506 POSTCONDITION(check_field_exists(field, field_id, fields));
507 }
508
509 // Now do methods
510 std::set<irep_idt> overlay_methods;
511 for(auto overlay_class : overlay_classes)
512 {
513 for(const methodt &method : overlay_class.get().methods)
514 {
515 const irep_idt method_identifier =
516 qualified_classname + "." + id2string(method.name)
517 + ":" + method.descriptor;
518 if(is_ignored_method(c.name, method))
519 {
520 log.debug() << "Ignoring method: '" << method_identifier << "'"
521 << messaget::eom;
522 continue;
523 }
524 if(method_bytecode.contains_method(method_identifier))
525 {
526 // This method has already been discovered and added to method_bytecode
527 // while parsing an overlay class that appears later in the classpath
528 // (we're working backwards)
529 // Warn the user if the definition already found was not an overlay,
530 // otherwise simply don't load this earlier definition
531 if(overlay_methods.count(method_identifier) == 0)
532 {
533 // This method was defined in a previous class definition without
534 // being marked as an overlay method
535 log.warning()
536 << "Method " << method_identifier
537 << " exists in an overlay class without being marked as an "
538 "overlay and also exists in another overlay class that appears "
539 "earlier in the classpath"
540 << messaget::eom;
541 }
542 continue;
543 }
544 // Always run the lazy pre-stage, as it symbol-table
545 // registers the function.
546 log.debug() << "Adding symbol from overlay class: method '"
547 << method_identifier << "'" << messaget::eom;
548 java_bytecode_convert_method_lazy(
549 *class_symbol,
550 method_identifier,
551 method,
552 symbol_table,
553 log.get_message_handler());
554 method_bytecode.add(qualified_classname, method_identifier, method);
555 if(is_overlay_method(method))
556 overlay_methods.insert(method_identifier);
557 }
558 }
559 for(const methodt &method : c.methods)
560 {
561 const irep_idt method_identifier=
562 qualified_classname + "." + id2string(method.name)
563 + ":" + method.descriptor;
564 if(is_ignored_method(c.name, method))
565 {
566 log.debug() << "Ignoring method: '" << method_identifier << "'"
567 << messaget::eom;
568 continue;
569 }
570 if(method_bytecode.contains_method(method_identifier))
571 {
572 // This method has already been discovered while parsing an overlay
573 // class
574 // If that definition is an overlay then we simply don't load this
575 // original definition and we remove it from the list of overlays
576 if(overlay_methods.erase(method_identifier) == 0)
577 {
578 // This method was defined in a previous class definition without
579 // being marked as an overlay method
580 log.warning()
581 << "Method " << method_identifier
582 << " exists in an overlay class without being marked as an overlay "
583 "and also exists in the underlying class"
584 << messaget::eom;
585 }
586 continue;
587 }
588 // Always run the lazy pre-stage, as it symbol-table
589 // registers the function.
590 log.debug() << "Adding symbol: method '" << method_identifier << "'"
591 << messaget::eom;
592 java_bytecode_convert_method_lazy(
593 *class_symbol,
594 method_identifier,
595 method,
596 symbol_table,
597 log.get_message_handler());
598 method_bytecode.add(qualified_classname, method_identifier, method);
599 if(is_overlay_method(method))
600 {
601 log.warning()
602 << "Method " << method_identifier
603 << " marked as an overlay where defined in the underlying class"
604 << messaget::eom;
605 }
606 }
607 if(!overlay_methods.empty())
608 {
609 log.error()
610 << "Overlay methods defined in overlay classes did not exist in the "
611 "underlying class:\n";
612 for(const irep_idt &method_id : overlay_methods)
613 log.error() << " " << method_id << "\n";
614 log.error() << messaget::eom;
615 }
616
617 // is this a root class?
618 if(c.super_class.empty())
619 java_root_class(*class_symbol);
620}
621
622bool java_bytecode_convert_classt::check_field_exists(
623 const java_bytecode_parse_treet::fieldt &field,
624 const irep_idt &qualified_fieldname,
625 const struct_union_typet::componentst &fields) const
626{
627 if(field.is_static)
628 return symbol_table.has_symbol(qualified_fieldname);
629
630 auto existing_field = std::find_if(
631 fields.begin(),
632 fields.end(),
633 [&field](const struct_union_typet::componentt &f)
634 {
635 return f.get_name() == field.name;
636 });
637 return existing_field != fields.end();
638}
639
643void java_bytecode_convert_classt::convert(
644 symbolt &class_symbol,
645 const fieldt &f)
646{
647 typet field_type;
648 if(f.signature.has_value())
649 {
650 field_type = *java_type_from_string_with_exception(
651 f.descriptor, f.signature, id2string(class_symbol.name));
652
654 if(is_java_generic_parameter(field_type))
655 {
656#ifdef DEBUG
657 std::cout << "fieldtype: generic "
658 << to_java_generic_parameter(field_type).type_variable()
659 .get_identifier()
660 << " name " << f.name << "\n";
661#endif
662 }
663
666 else if(is_java_generic_type(field_type))
667 {
668 java_generic_typet &with_gen_type=
669 to_java_generic_type(field_type);
670#ifdef DEBUG
671 std::cout << "fieldtype: generic container type "
672 << std::to_string(with_gen_type.generic_type_arguments().size())
673 << " type " << with_gen_type.id()
674 << " name " << f.name
675 << " subtype id " << with_gen_type.subtype().id() << "\n";
676#endif
677 field_type=with_gen_type;
678 }
679 }
680 else
681 field_type = *java_type_from_string(f.descriptor);
682
683 // determine access
684 irep_idt access;
685
686 if(f.is_private)
687 access = ID_private;
688 else if(f.is_protected)
689 access = ID_protected;
690 else if(f.is_public)
691 access = ID_public;
692 else
693 access = ID_default;
694
695 auto &class_type = to_java_class_type(class_symbol.type);
696
697 // is this a static field?
698 if(f.is_static)
699 {
700 const irep_idt field_identifier =
701 id2string(class_symbol.name) + "." + id2string(f.name);
702
703 class_type.static_members().emplace_back();
704 auto &component = class_type.static_members().back();
705
706 component.set_name(field_identifier);
707 component.set_base_name(f.name);
708 component.set_pretty_name(f.name);
709 component.set_access(access);
710 component.set_is_final(f.is_final);
711 component.type() = field_type;
712
713 // Create the symbol
714 symbolt new_symbol;
715
716 new_symbol.is_static_lifetime=true;
717 new_symbol.is_lvalue=true;
718 new_symbol.is_state_var=true;
719 new_symbol.name=id2string(class_symbol.name)+"."+id2string(f.name);
720 new_symbol.base_name=f.name;
721 new_symbol.type=field_type;
722 // Provide a static field -> class link, like
723 // java_bytecode_convert_method::convert does for method -> class.
724 set_declaring_class(new_symbol, class_symbol.name);
725 new_symbol.type.set(ID_C_field, f.name);
726 new_symbol.type.set(ID_C_constant, f.is_final);
727 new_symbol.pretty_name=id2string(class_symbol.pretty_name)+
728 "."+id2string(f.name);
729 new_symbol.mode=ID_java;
730 new_symbol.is_type=false;
731
732 // These annotations use `ID_C_access` instead of `ID_access` like methods
733 // to avoid type clashes in expressions like `some_static_field = 0`, where
734 // with ID_access the constant '0' would need to have an access modifier
735 // too, or else appear to have incompatible type.
736 if(f.is_public)
737 new_symbol.type.set(ID_C_access, ID_public);
738 else if(f.is_protected)
739 new_symbol.type.set(ID_C_access, ID_protected);
740 else if(f.is_private)
741 new_symbol.type.set(ID_C_access, ID_private);
742 else
743 new_symbol.type.set(ID_C_access, ID_default);
744
745 const namespacet ns(symbol_table);
746 const auto value = zero_initializer(field_type, class_symbol.location, ns);
747 if(!value.has_value())
748 {
749 log.error().source_location = class_symbol.location;
750 log.error() << "failed to zero-initialize " << f.name << messaget::eom;
751 throw 0;
752 }
753 new_symbol.value = *value;
754
755 // Load annotations
756 if(!f.annotations.empty())
757 {
758 convert_annotations(
759 f.annotations,
760 type_checked_cast<annotated_typet>(new_symbol.type).get_annotations());
761 }
762
763 // Do we have the static field symbol already?
764 const auto s_it=symbol_table.symbols.find(new_symbol.name);
765 if(s_it!=symbol_table.symbols.end())
766 symbol_table.erase(s_it); // erase, we stubbed it
767
768 if(symbol_table.add(new_symbol))
769 assert(false && "failed to add static field symbol");
770 }
771 else
772 {
773 class_type.components().emplace_back();
774 auto &component = class_type.components().back();
775
776 component.set_name(f.name);
777 component.set_base_name(f.name);
778 component.set_pretty_name(f.name);
779 component.set_access(access);
780 component.set_is_final(f.is_final);
781 component.type() = field_type;
782
783 // Load annotations
784 if(!f.annotations.empty())
785 {
786 convert_annotations(
787 f.annotations,
788 static_cast<annotated_typet &>(component.type()).get_annotations());
789 }
790 }
791}
792
793void add_java_array_types(symbol_tablet &symbol_table)
794{
795 const std::string letters="ijsbcfdza";
796
797 for(const char l : letters)
798 {
799 struct_tag_typet struct_tag_type =
800 to_struct_tag_type(java_array_type(l).subtype());
801
802 const irep_idt &struct_tag_type_identifier =
803 struct_tag_type.get_identifier();
804 if(symbol_table.has_symbol(struct_tag_type_identifier))
805 return;
806
807 java_class_typet class_type;
808 // we have the base class, java.lang.Object, length and data
809 // of appropriate type
810 class_type.set_tag(struct_tag_type_identifier);
811 // Note that non-array types don't have "java::" at the beginning of their
812 // tag, and their name is "java::" + their tag. Since arrays do have
813 // "java::" at the beginning of their tag we set the name to be the same as
814 // the tag.
815 class_type.set_name(struct_tag_type_identifier);
816
817 class_type.components().reserve(3);
818 java_class_typet::componentt base_class_component(
819 "@java.lang.Object", struct_tag_typet("java::java.lang.Object"));
820 base_class_component.set_pretty_name("@java.lang.Object");
821 base_class_component.set_base_name("@java.lang.Object");
822 class_type.components().push_back(base_class_component);
823
824 java_class_typet::componentt length_component("length", java_int_type());
825 length_component.set_pretty_name("length");
826 length_component.set_base_name("length");
827 class_type.components().push_back(length_component);
828
829 java_class_typet::componentt data_component(
830 "data", java_reference_type(java_type_from_char(l)));
831 data_component.set_pretty_name("data");
832 data_component.set_base_name("data");
833 class_type.components().push_back(data_component);
834
835 if(l == 'a')
836 {
837 // This is a reference array (java::array[reference]). Add extra fields to
838 // carry the innermost element type and array dimension.
839 java_class_typet::componentt array_element_classid_component(
840 JAVA_ARRAY_ELEMENT_CLASSID_FIELD_NAME, string_typet());
841 array_element_classid_component.set_pretty_name(
842 JAVA_ARRAY_ELEMENT_CLASSID_FIELD_NAME);
843 array_element_classid_component.set_base_name(
844 JAVA_ARRAY_ELEMENT_CLASSID_FIELD_NAME);
845 class_type.components().push_back(array_element_classid_component);
846
847 java_class_typet::componentt array_dimension_component(
848 JAVA_ARRAY_DIMENSION_FIELD_NAME, java_int_type());
849 array_dimension_component.set_pretty_name(
850 JAVA_ARRAY_DIMENSION_FIELD_NAME);
851 array_dimension_component.set_base_name(JAVA_ARRAY_DIMENSION_FIELD_NAME);
852 class_type.components().push_back(array_dimension_component);
853 }
854
855 class_type.add_base(struct_tag_typet("java::java.lang.Object"));
856
857 INVARIANT(
858 is_valid_java_array(class_type),
859 "Constructed a new type representing a Java Array "
860 "object that doesn't match expectations");
861
862 symbolt symbol;
863 symbol.name = struct_tag_type_identifier;
864 symbol.base_name = struct_tag_type.get(ID_C_base_name);
865 symbol.is_type=true;
866 symbol.type = class_type;
867 symbol.mode = ID_java;
868 symbol_table.add(symbol);
869
870 // Also provide a clone method:
871 // ----------------------------
872
873 const irep_idt clone_name =
874 id2string(struct_tag_type_identifier) + ".clone:()Ljava/lang/Object;";
875 java_method_typet::parametert this_param(
876 java_reference_type(struct_tag_type));
877 this_param.set_identifier(id2string(clone_name)+"::this");
878 this_param.set_base_name(ID_this);
879 this_param.set_this();
880 const java_method_typet clone_type({this_param}, java_lang_object_type());
881
882 parameter_symbolt this_symbol;
883 this_symbol.name=this_param.get_identifier();
884 this_symbol.base_name=this_param.get_base_name();
885 this_symbol.pretty_name=this_symbol.base_name;
886 this_symbol.type=this_param.type();
887 this_symbol.mode=ID_java;
888 symbol_table.add(this_symbol);
889
890 const irep_idt local_name=
891 id2string(clone_name)+"::cloned_array";
892 auxiliary_symbolt local_symbol;
893 local_symbol.name=local_name;
894 local_symbol.base_name="cloned_array";
895 local_symbol.pretty_name=local_symbol.base_name;
896 local_symbol.type = java_reference_type(struct_tag_type);
897 local_symbol.mode=ID_java;
898 symbol_table.add(local_symbol);
899 const auto local_symexpr = local_symbol.symbol_expr();
900
901 code_declt declare_cloned(local_symexpr);
902
903 source_locationt location;
904 location.set_function(local_name);
905 side_effect_exprt java_new_array(
906 ID_java_new_array, java_reference_type(struct_tag_type), location);
907 dereference_exprt old_array{this_symbol.symbol_expr()};
908 dereference_exprt new_array{local_symexpr};
909 member_exprt old_length(
910 old_array, length_component.get_name(), length_component.type());
911 java_new_array.copy_to_operands(old_length);
912 code_frontend_assignt create_blank(local_symexpr, java_new_array);
913
914 codet copy_type_information = code_skipt();
915 if(l == 'a')
916 {
917 // Reference arrays carry additional type information in their classids
918 // which should be copied:
919 const auto &array_dimension_component =
920 class_type.get_component(JAVA_ARRAY_DIMENSION_FIELD_NAME);
921 const auto &array_element_classid_component =
922 class_type.get_component(JAVA_ARRAY_ELEMENT_CLASSID_FIELD_NAME);
923
924 member_exprt old_array_dimension(old_array, array_dimension_component);
925 member_exprt old_array_element_classid(
926 old_array, array_element_classid_component);
927
928 member_exprt new_array_dimension(new_array, array_dimension_component);
929 member_exprt new_array_element_classid(
930 new_array, array_element_classid_component);
931
932 copy_type_information = code_blockt{
933 {code_frontend_assignt(new_array_dimension, old_array_dimension),
934 code_frontend_assignt(
935 new_array_element_classid, old_array_element_classid)}};
936 }
937
938 member_exprt old_data(
939 old_array, data_component.get_name(), data_component.type());
940 member_exprt new_data(
941 new_array, data_component.get_name(), data_component.type());
942
943 /*
944 // TODO use this instead of a loop.
945 codet array_copy;
946 array_copy.set_statement(ID_array_copy);
947 array_copy.add_to_operands(std::move(new_data), std::move(old_data));
948 clone_body.add_to_operands(std::move(array_copy));
949 */
950
951 // Begin for-loop to replace:
952
953 const irep_idt index_name=
954 id2string(clone_name)+"::index";
955 auxiliary_symbolt index_symbol;
956 index_symbol.name=index_name;
957 index_symbol.base_name="index";
958 index_symbol.pretty_name=index_symbol.base_name;
959 index_symbol.type = length_component.type();
960 index_symbol.mode=ID_java;
961 symbol_table.add(index_symbol);
962 const auto &index_symexpr=index_symbol.symbol_expr();
963
964 code_declt declare_index(index_symexpr);
965
966 dereference_exprt old_cell(
967 plus_exprt(old_data, index_symexpr), old_data.type().subtype());
968 dereference_exprt new_cell(
969 plus_exprt(new_data, index_symexpr), new_data.type().subtype());
970
971 const code_fort copy_loop = code_fort::from_index_bounds(
972 from_integer(0, index_symexpr.type()),
973 old_length,
974 index_symexpr,
975 code_frontend_assignt(std::move(new_cell), std::move(old_cell)),
976 location);
977
978 member_exprt new_base_class(
979 new_array, base_class_component.get_name(), base_class_component.type());
980 address_of_exprt retval(new_base_class);
981 code_returnt return_inst(retval);
982
983 const code_blockt clone_body({declare_cloned,
984 create_blank,
985 copy_type_information,
986 declare_index,
987 copy_loop,
988 return_inst});
989
990 symbolt clone_symbol;
991 clone_symbol.name=clone_name;
992 clone_symbol.pretty_name =
993 id2string(struct_tag_type_identifier) + ".clone:()";
994 clone_symbol.base_name="clone";
995 clone_symbol.type=clone_type;
996 clone_symbol.value=clone_body;
997 clone_symbol.mode=ID_java;
998 symbol_table.add(clone_symbol);
999 }
1000}
1001
1002bool java_bytecode_convert_class(
1003 const java_class_loadert::parse_tree_with_overlayst &parse_trees,
1004 symbol_tablet &symbol_table,
1005 message_handlert &message_handler,
1006 size_t max_array_length,
1007 method_bytecodet &method_bytecode,
1008 java_string_library_preprocesst &string_preprocess,
1009 const std::unordered_set<std::string> &no_load_classes)
1010{
1011 java_bytecode_convert_classt java_bytecode_convert_class(
1012 symbol_table,
1013 message_handler,
1014 max_array_length,
1015 method_bytecode,
1016 string_preprocess,
1017 no_load_classes);
1018
1019 try
1020 {
1021 java_bytecode_convert_class(parse_trees);
1022 return false;
1023 }
1024
1025 catch(int)
1026 {
1027 }
1028
1029 catch(const char *e)
1030 {
1031 messaget log{message_handler};
1032 log.error() << e << messaget::eom;
1033 }
1034
1035 catch(const std::string &e)
1036 {
1037 messaget log{message_handler};
1038 log.error() << e << messaget::eom;
1039 }
1040
1041 return true;
1042}
1043
1044static std::string get_final_name_component(const std::string &name)
1045{
1046 return name.substr(name.rfind("::") + 2);
1047}
1048
1049static std::string get_without_final_name_component(const std::string &name)
1050{
1051 return name.substr(0, name.rfind("::"));
1052}
1053
1066static void find_and_replace_parameter(
1067 java_generic_parametert &parameter,
1068 const std::vector<java_generic_parametert> &replacement_parameters)
1069{
1070 // get the name of the parameter, e.g., `T` from `java::Class::T`
1071 const std::string &parameter_full_name =
1072 id2string(parameter.type_variable_ref().get_identifier());
1073 const std::string parameter_name =
1074 get_final_name_component(parameter_full_name);
1075
1076 // check if there is a replacement parameter with the same name
1077 const auto replacement_parameter_it = std::find_if(
1078 replacement_parameters.begin(),
1079 replacement_parameters.end(),
1080 [&parameter_name](const java_generic_parametert &replacement_param) {
1081 return parameter_name ==
1082 get_final_name_component(
1083 id2string(replacement_param.type_variable().get_identifier()));
1084 });
1085 if(replacement_parameter_it == replacement_parameters.end())
1086 return;
1087
1088 // A replacement parameter was found, update the identifier
1089 const std::string &replacement_parameter_full_name =
1090 id2string(replacement_parameter_it->type_variable().get_identifier());
1091
1092 // Check the replacement parameter comes from an outer class
1093 PRECONDITION(has_prefix(
1094 replacement_parameter_full_name,
1095 get_without_final_name_component(parameter_full_name)));
1096
1097 parameter.type_variable_ref().set_identifier(replacement_parameter_full_name);
1098}
1099
1105static void find_and_replace_parameters(
1106 typet &type,
1107 const std::vector<java_generic_parametert> &replacement_parameters)
1108{
1109 if(is_java_generic_parameter(type))
1110 {
1111 find_and_replace_parameter(
1112 to_java_generic_parameter(type), replacement_parameters);
1113 }
1114 else if(is_java_generic_type(type))
1115 {
1116 java_generic_typet &generic_type = to_java_generic_type(type);
1117 std::vector<reference_typet> &arguments =
1118 generic_type.generic_type_arguments();
1119 for(auto &argument : arguments)
1120 {
1121 find_and_replace_parameters(argument, replacement_parameters);
1122 }
1123 }
1124 else if(is_java_generic_struct_tag_type(type))
1125 {
1126 java_generic_struct_tag_typet &generic_base =
1127 to_java_generic_struct_tag_type(type);
1128 std::vector<reference_typet> &gen_types = generic_base.generic_types();
1129 for(auto &gen_type : gen_types)
1130 {
1131 find_and_replace_parameters(gen_type, replacement_parameters);
1132 }
1133 }
1134}
1135
1139void convert_annotations(
1140 const java_bytecode_parse_treet::annotationst &parsed_annotations,
1141 std::vector<java_annotationt> &java_annotations)
1142{
1143 for(const auto &annotation : parsed_annotations)
1144 {
1145 java_annotations.emplace_back(annotation.type);
1146 std::vector<java_annotationt::valuet> &values =
1147 java_annotations.back().get_values();
1148 std::transform(
1149 annotation.element_value_pairs.begin(),
1150 annotation.element_value_pairs.end(),
1151 std::back_inserter(values),
1152 [](const decltype(annotation.element_value_pairs)::value_type &value) {
1153 return java_annotationt::valuet(value.element_name, value.value);
1154 });
1155 }
1156}
1157
1162void convert_java_annotations(
1163 const std::vector<java_annotationt> &java_annotations,
1164 java_bytecode_parse_treet::annotationst &annotations)
1165{
1166 for(const auto &java_annotation : java_annotations)
1167 {
1168 annotations.emplace_back(java_bytecode_parse_treet::annotationt());
1169 auto &annotation = annotations.back();
1170 annotation.type = java_annotation.get_type();
1171
1172 std::transform(
1173 java_annotation.get_values().begin(),
1174 java_annotation.get_values().end(),
1175 std::back_inserter(annotation.element_value_pairs),
1176 [](const java_annotationt::valuet &value)
1177 -> java_bytecode_parse_treet::annotationt::element_value_pairt {
1178 return {value.get_name(), value.get_value()};
1179 });
1180 }
1181}
1182
1187void mark_java_implicitly_generic_class_type(
1188 const irep_idt &class_name,
1189 symbol_tablet &symbol_table)
1190{
1191 const std::string qualified_class_name = "java::" + id2string(class_name);
1192 PRECONDITION(symbol_table.has_symbol(qualified_class_name));
1193 // This will have its type changed
1194 symbolt &class_symbol = symbol_table.get_writeable_ref(qualified_class_name);
1195 const java_class_typet &class_type = to_java_class_type(class_symbol.type);
1196
1197 // the class must be an inner non-static class, i.e., have a field this$*
1198 // TODO this should be simplified once static inner classes are marked
1199 // during parsing
1200 bool no_this_field = std::none_of(
1201 class_type.components().begin(),
1202 class_type.components().end(),
1203 [](const struct_union_typet::componentt &component)
1204 {
1205 return id2string(component.get_name()).substr(0, 5) == "this$";
1206 });
1207 if(no_this_field)
1208 {
1209 return;
1210 }
1211
1212 // create a vector of all generic type parameters of all outer classes, in
1213 // the order from the outer-most inwards
1214 std::vector<java_generic_parametert> implicit_generic_type_parameters;
1215 std::string::size_type outer_class_delimiter =
1216 qualified_class_name.rfind('$');
1217 while(outer_class_delimiter != std::string::npos)
1218 {
1219 std::string outer_class_name =
1220 qualified_class_name.substr(0, outer_class_delimiter);
1221 if(symbol_table.has_symbol(outer_class_name))
1222 {
1223 const symbolt &outer_class_symbol =
1224 symbol_table.lookup_ref(outer_class_name);
1225 const java_class_typet &outer_class_type =
1226 to_java_class_type(outer_class_symbol.type);
1227 if(is_java_generic_class_type(outer_class_type))
1228 {
1229 for(const java_generic_parametert &outer_generic_type_parameter :
1230 to_java_generic_class_type(outer_class_type).generic_types())
1231 {
1232 // Create a new generic type parameter with name in the form:
1233 // java::Outer$Inner::Outer::T
1234 irep_idt identifier = qualified_class_name + "::" +
1235 id2string(strip_java_namespace_prefix(
1236 outer_generic_type_parameter.get_name()));
1237 java_generic_parameter_tagt bound = to_java_generic_parameter_tag(
1238 outer_generic_type_parameter.base_type());
1239 bound.type_variable_ref().set_identifier(identifier);
1240 implicit_generic_type_parameters.emplace_back(identifier, bound);
1241 }
1242 }
1243 outer_class_delimiter = outer_class_name.rfind('$');
1244 }
1245 else
1246 {
1247 throw missing_outer_class_symbol_exceptiont(
1248 outer_class_name, qualified_class_name);
1249 }
1250 }
1251
1252 // if there are any implicit generic type parameters, mark the class
1253 // implicitly generic and update identifiers of type parameters used in fields
1254 if(!implicit_generic_type_parameters.empty())
1255 {
1256 java_implicitly_generic_class_typet new_class_type(
1257 class_type, implicit_generic_type_parameters);
1258
1259 // Prepend existing parameters so choose those above any inherited
1260 if(is_java_generic_class_type(class_type))
1261 {
1262 const java_generic_class_typet::generic_typest &class_type_params =
1263 to_java_generic_class_type(class_type).generic_types();
1264 implicit_generic_type_parameters.insert(
1265 implicit_generic_type_parameters.begin(),
1266 class_type_params.begin(),
1267 class_type_params.end());
1268 }
1269
1270 for(auto &field : new_class_type.components())
1271 {
1272 find_and_replace_parameters(
1273 field.type(), implicit_generic_type_parameters);
1274 }
1275
1276 for(auto &base : new_class_type.bases())
1277 {
1278 find_and_replace_parameters(
1279 base.type(), implicit_generic_type_parameters);
1280 }
1281
1282 class_symbol.type = new_class_type;
1283 }
1284}
Collect methods needed to be loaded using the lazy method.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
static bool is_overlay_method(const methodt &method)
Check if a method is an overlay method by searching for ID_overlay_method in its list of annotations.
void operator()(const java_class_loadert::parse_tree_with_overlayst &parse_trees)
Converts all the class parse trees into a class symbol and adds it to the symbol table.
java_bytecode_parse_treet::methodt methodt
java_bytecode_parse_treet::fieldt fieldt
std::unordered_set< std::string > no_load_classes
java_string_library_preprocesst & string_preprocess
java_bytecode_convert_classt(symbol_tablet &_symbol_table, message_handlert &_message_handler, size_t _max_array_length, method_bytecodet &method_bytecode, java_string_library_preprocesst &_string_preprocess, const std::unordered_set< std::string > &no_load_classes)
java_bytecode_parse_treet::annotationt annotationt
java_bytecode_parse_treet::classt classt
void convert(const classt &c, const overlay_classest &overlay_classes)
Convert a class, adding symbols to the symbol table for its members.
std::list< std::reference_wrapper< const classt > > overlay_classest
bool check_field_exists(const fieldt &field, const irep_idt &qualified_fieldname, const struct_union_typet::componentst &fields) const
static bool is_ignored_method(const irep_idt &class_name, const methodt &method)
Check if a method is an ignored method, by one of two mechanisms:
std::list< java_bytecode_parse_treet > parse_tree_with_overlayst
A list of parse trees supporting overlay classes.
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
Class to hold type with generic type arguments, for example java.util.List in either a reference of t...
Definition java_types.h:858
void add_string_type(const irep_idt &class_name, symbol_tablet &symbol_table)
Add to the symbol table type declaration for a String-like Java class.
bool is_known_string_type(irep_idt class_name)
Check whether a class name is known as a string type.
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
mstreamt & debug() const
Definition message.h:429
message_handlert & get_message_handler()
Definition message.h:184
mstreamt & warning() const
Definition message.h:404
static eomt eom
Definition message.h:297
A struct tag type, i.e., struct_typet with an identifier.
Definition std_types.h:449
std::vector< componentt > componentst
Definition std_types.h:140
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
The symbol table.
Symbol table entry.
Definition symbol.h:28
The type of an expression, extends irept.
Definition type.h:29
An exception that is raised for unsupported class signature.
Expression Initialization.
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
void add_java_array_types(symbol_tablet &symbol_table)
Register in the symbol_table new symbols for the objects java::array[X] where X is byte,...
static optionalt< std::string > extract_generic_interface_reference(const optionalt< std::string > &signature, const std::string &interface_name)
Auxiliary function to extract the generic interface reference of an interface with the specified name...
static optionalt< std::string > extract_generic_superclass_reference(const optionalt< std::string > &signature)
Auxiliary function to extract the generic superclass reference from the class signature.
JAVA Bytecode Language Conversion.
JAVA Bytecode Language Conversion.
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.
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 ...
const java_generic_parametert & to_java_generic_parameter(const typet &type)
Definition java_types.h:827
const std::unordered_set< std::string > cprover_methods_to_ignore
Methods belonging to the class org.cprover.CProver that should be ignored (not converted),...
void generate_class_stub(const irep_idt &class_name, symbol_table_baset &symbol_table, message_handlert &message_handler, const struct_union_typet::componentst &componentst)
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.
#define PRECONDITION(CONDITION)
Definition invariant.h:463
API to expression classes.
bool has_annotation(const irep_idt &annotation_id) const