|
| 1 | +/*******************************************************************\ |
| 2 | +
|
| 3 | + Module: MODULE NAME |
| 4 | +
|
| 5 | + Author: DiffBlue Limited. All rights reserved. |
| 6 | +
|
| 7 | +\*******************************************************************/ |
| 8 | +#include "generate_java_generic_type.h" |
| 9 | +#include <util/namespace.h> |
| 10 | +#include <java_bytecode/java_types.h> |
| 11 | +#include <java_bytecode/java_utils.h> |
| 12 | + |
| 13 | +#include <iostream> |
| 14 | +#include <sstream> |
| 15 | + |
| 16 | +generate_java_generic_typet::generate_java_generic_typet( |
| 17 | + symbol_tablet &symbol_table, |
| 18 | + message_handlert &message_handler): |
| 19 | + symbol_table(symbol_table), |
| 20 | + message_handler(message_handler) |
| 21 | +{} |
| 22 | + |
| 23 | +symbolt generate_java_generic_typet::operator()( |
| 24 | + const java_type_with_generic_typet &existing_generic_type) |
| 25 | +{ |
| 26 | + namespacet ns(symbol_table); |
| 27 | + |
| 28 | + const typet &pointer_subtype=ns.follow(existing_generic_type.subtype()); |
| 29 | + |
| 30 | + INVARIANT( |
| 31 | + pointer_subtype.id()==ID_struct, "Only pointers to classes in java"); |
| 32 | + |
| 33 | + const java_class_typet &java_class=to_java_class_type(pointer_subtype); |
| 34 | + |
| 35 | + java_class_typet replacement_type=java_class; |
| 36 | + replacement_type.components().clear(); |
| 37 | + |
| 38 | + const irep_idt new_tag=build_generic_tag(existing_generic_type, java_class); |
| 39 | + replacement_type.set_tag(new_tag); |
| 40 | + |
| 41 | + for(const struct_union_typet::componentt &component_type : |
| 42 | + java_class.components()) |
| 43 | + { |
| 44 | + if(!is_java_generic_type(component_type.type())) |
| 45 | + { |
| 46 | + replacement_type.components().push_back(component_type); |
| 47 | + continue; |
| 48 | + } |
| 49 | + |
| 50 | + INVARIANT( |
| 51 | + existing_generic_type.type_parameters.size()==1, |
| 52 | + "Must have a type parameter"); |
| 53 | + |
| 54 | + struct_union_typet::componentt replacement_comp=component_type; |
| 55 | + replacement_comp.type()=existing_generic_type.type_parameters[0]; |
| 56 | + |
| 57 | + replacement_type.components().push_back(replacement_comp); |
| 58 | + |
| 59 | + } |
| 60 | + INVARIANT( |
| 61 | + replacement_type.components().size()==java_class.components().size(), |
| 62 | + "All components in the original class should be in the new class"); |
| 63 | + |
| 64 | + generate_class_stub(new_tag, symbol_table, message_handler); |
| 65 | + INVARIANT(symbol_table.has_symbol("java::"+id2string(new_tag)), "New class not created"); |
| 66 | + return symbol_table.lookup("java::"+id2string(new_tag)); |
| 67 | +} |
| 68 | + |
| 69 | +irep_idt generate_java_generic_typet::build_generic_tag( |
| 70 | + const java_type_with_generic_typet &existing_generic_type, |
| 71 | + const java_class_typet &original_class) |
| 72 | +{ |
| 73 | + std::ostringstream new_tag_buffer; |
| 74 | + new_tag_buffer << original_class.get_tag(); |
| 75 | + new_tag_buffer << "<"; |
| 76 | + bool first=true; |
| 77 | + for(const typet ¶m : existing_generic_type.type_parameters) |
| 78 | + { |
| 79 | + if(!first) |
| 80 | + new_tag_buffer << ", "; |
| 81 | + first=false; |
| 82 | + |
| 83 | + INVARIANT( |
| 84 | + is_java_inst_generic_type(param), |
| 85 | + "Only create full concretized generic types"); |
| 86 | + new_tag_buffer << param.subtype().get(ID_identifier); |
| 87 | + } |
| 88 | + |
| 89 | + new_tag_buffer << ">"; |
| 90 | + |
| 91 | + return new_tag_buffer.str(); |
| 92 | +} |
0 commit comments