86 error() <<
"invalid constant pool index (" << index <<
")" <<
eom;
111 bytecodes[p->opcode].mnemonic=p->mnemonic;
144 for(std::size_t i=0; i<bytes; i++)
148 error() <<
"unexpected end of bytecode file" <<
eom;
158 for(
size_t i=0; i<bytes; i++)
162 error() <<
"unexpected end of bytecode file" <<
eom;
193 size_t bootstrap_method_index,
197 #define CONSTANT_Class 7 198 #define CONSTANT_Fieldref 9 199 #define CONSTANT_Methodref 10 200 #define CONSTANT_InterfaceMethodref 11 201 #define CONSTANT_String 8 202 #define CONSTANT_Integer 3 203 #define CONSTANT_Float 4 204 #define CONSTANT_Long 5 205 #define CONSTANT_Double 6 206 #define CONSTANT_NameAndType 12 207 #define CONSTANT_Utf8 1 208 #define CONSTANT_MethodHandle 15 209 #define CONSTANT_MethodType 16 210 #define CONSTANT_InvokeDynamic 18 212 #define VTYPE_INFO_TOP 0 213 #define VTYPE_INFO_INTEGER 1 214 #define VTYPE_INFO_FLOAT 2 215 #define VTYPE_INFO_LONG 3 216 #define VTYPE_INFO_DOUBLE 4 217 #define VTYPE_INFO_ITEM_NULL 5 218 #define VTYPE_INFO_UNINIT_THIS 6 219 #define VTYPE_INFO_OBJECT 7 220 #define VTYPE_INFO_UNINIT 8 235 typedef std::function<java_bytecode_parsert::pool_entryt &(u2)>
329 "name_and_typeindex did not correspond to a name_and_type in the " 427 catch(
const char *message)
433 catch(
const std::string &message)
448 #define ACC_PUBLIC 0x0001 449 #define ACC_PRIVATE 0x0002 450 #define ACC_PROTECTED 0x0004 451 #define ACC_STATIC 0x0008 452 #define ACC_FINAL 0x0010 453 #define ACC_SYNCHRONIZED 0x0020 454 #define ACC_BRIDGE 0x0040 455 #define ACC_VARARGS 0x0080 456 #define ACC_NATIVE 0x0100 457 #define ACC_INTERFACE 0x0200 458 #define ACC_ABSTRACT 0x0400 459 #define ACC_STRICT 0x0800 460 #define ACC_SYNTHETIC 0x1000 461 #define ACC_ANNOTATION 0x2000 462 #define ACC_ENUM 0x4000 464 #define UNUSED_u2(x) { const u2 x = read_u2(); (void)x; } (void)0 474 if(magic!=0xCAFEBABE)
482 error() <<
"unexpected major version" <<
eom;
521 for(std::size_t j=0; j<attributes_count; j++)
556 if(field.signature.has_value())
577 if(method.signature.has_value())
590 for(
const auto &var : method.local_variable_table)
593 if(var.signature.has_value())
611 if(src.
id()==ID_code)
619 else if(src.
id()==ID_symbol)
624 const typet &element_type =
625 static_cast<const typet &
>(src.
find(ID_element_type));
631 else if(src.
id()==ID_struct)
637 else if(src.
id()==ID_pointer)
644 if(constant_pool_count==0)
646 error() <<
"invalid constant_pool_count" <<
eom;
652 for(constant_poolt::iterator
695 error() <<
"invalid double entry" <<
eom;
707 for(std::string::iterator s_it=s.begin(); s_it!=s.end(); s_it++)
719 error() <<
"unknown constant pool entry (" << it->tag <<
")" 726 for(constant_poolt::iterator
784 exprt virtual_function(ID_virtual_function, type);
785 virtual_function.
set(ID_component_name, component_name);
786 virtual_function.
set(ID_C_class, class_name);
787 virtual_function.
set(ID_C_base_name, name_entry.
s);
788 virtual_function.
set(ID_identifier, identifier);
790 it->expr=virtual_function;
797 exprt string_literal(ID_java_string_literal);
799 it->expr=string_literal;
829 it->expr.id(
"nameandtype");
835 it->expr.id(
"methodhandle");
841 it->expr.id(
"methodtype");
847 it->expr.id(
"invokedynamic");
850 type.
set(ID_java_lambda_method_handle_index, it->ref1);
851 it->expr.type()=type;
864 for(std::size_t i=0; i<interfaces_count; i++)
873 for(std::size_t i=0; i<fields_count; i++)
891 const auto flags = (field.
is_public ? 1 : 0) +
894 DATA_INVARIANT(flags<=1,
"at most one of public, protected, private");
896 for(std::size_t j=0; j<attributes_count; j++)
916 size_t bytecode_index=0;
918 for(address=0; address<code_length; address++)
920 bool wide_instruction=
false;
921 u4 start_of_instruction=address;
927 wide_instruction=
true;
935 "Unexpected wide instruction: " +
942 instruction.
address=start_of_instruction;
982 instruction.
args.push_back(
993 instruction.
args.push_back(
1001 if(wide_instruction)
1019 if(wide_instruction)
1051 u4 base_offset=address;
1054 while(((address+1)&3)!=0) {
read_u1(); address++; }
1060 instruction.
args.push_back(
1068 for(std::size_t i=0; i<npairs; i++)
1072 instruction.
args.push_back(
1076 instruction.
args.push_back(
1085 size_t base_offset=address;
1088 while(((address+1)&3)!=0) {
read_u1(); address++; }
1092 instruction.
args.push_back(
1105 for(
s4 i=low_value; i<=high_value; i++)
1111 instruction.
args.push_back(
1123 instruction.
args.push_back(
1140 case T_INT: t.
id(ID_int);
break;
1158 throw "unknown JVM bytecode instruction";
1163 if(address!=code_length)
1165 error() <<
"bytecode length mismatch" <<
eom;
1177 if(attribute_name==
"Code")
1187 for(std::size_t e=0; e<exception_table_length; e++)
1195 "The start_pc must be less than the end_pc as this is the range the " 1196 "exception is active");
1210 for(std::size_t j=0; j<attributes_count; j++)
1216 for(methodt::instructionst::iterator
1221 if(!it->source_location.get_line().empty())
1222 line_number=it->source_location.get_line();
1223 else if(!line_number.
empty())
1224 it->source_location.set_line(line_number);
1234 method.
instructions.begin()->source_location.get_line());
1236 else if(attribute_name==
"Signature")
1241 else if(attribute_name==
"RuntimeInvisibleAnnotations" ||
1242 attribute_name==
"RuntimeVisibleAnnotations")
1246 else if(attribute_name ==
"Exceptions")
1261 if(attribute_name==
"Signature")
1266 else if(attribute_name==
"RuntimeInvisibleAnnotations" ||
1267 attribute_name==
"RuntimeVisibleAnnotations")
1282 if(attribute_name==
"LineNumberTable")
1285 typedef std::map<unsigned,
1286 methodt::instructionst::iterator> instruction_mapt;
1287 instruction_mapt instruction_map;
1289 for(methodt::instructionst::iterator
1294 instruction_map[it->address]=it;
1299 for(std::size_t i=0; i<line_number_table_length; i++)
1305 instruction_mapt::const_iterator it=
1306 instruction_map.find(start_pc);
1308 if(it!=instruction_map.end())
1309 it->second->source_location.set_line(line_number);
1312 else if(attribute_name==
"LocalVariableTable")
1314 u2 local_variable_table_length=
read_u2();
1318 for(std::size_t i=0; i<local_variable_table_length; i++)
1334 else if(attribute_name==
"LocalVariableTypeTable")
1338 else if(attribute_name==
"StackMapTable")
1344 for(
size_t i=0; i<stack_map_entries; i++)
1353 else if(64<=frame_type && frame_type<=127)
1363 else if(frame_type==247)
1375 else if(248<=frame_type && frame_type<=250)
1383 else if(frame_type==251)
1392 else if(252<=frame_type && frame_type<=254)
1394 size_t new_locals=(size_t) (frame_type-251);
1400 for(
size_t k=0; k<new_locals; k++)
1409 else if(frame_type==255)
1416 for(
size_t k=0; k<(size_t) number_locals; k++)
1426 for(
size_t k=0; k<(size_t) number_stack_items; k++)
1436 throw "error: unknown stack frame type encountered";
1479 throw "error: unknown verification type info encountered";
1488 for(
u2 number=0; number<num_annotations; number++)
1492 annotations.push_back(annotation);
1508 element_value_pairs.resize(num_element_value_pairs);
1510 for(
auto &element_value_pair : element_value_pairs)
1513 element_value_pair.element_name=
pool_entry(element_name_index).
s;
1555 for(std::size_t i=0; i<num_values; i++)
1594 const u4 &attribute_length)
1596 std::string name = parsed_class.
name.
c_str();
1598 u4 number_of_bytes_to_be_read = number_of_classes * 8 + 2;
1600 number_of_bytes_to_be_read == attribute_length,
1601 "The number of bytes to be read for the InnerClasses attribute does not " 1602 "match the attribute length.");
1604 const auto pool_entry_lambda = [
this](
u2 index) ->
pool_entryt & {
1607 const auto remove_separator_char = [](std::string str,
char ch) {
1608 str.erase(std::remove(str.begin(), str.end(), ch), str.end());
1612 for(
int i = 0; i < number_of_classes; i++)
1617 u2 inner_class_access_flags =
read_u2();
1619 std::string inner_class_info_name =
1622 bool is_private = (inner_class_access_flags &
ACC_PRIVATE) != 0;
1623 bool is_public = (inner_class_access_flags &
ACC_PUBLIC) != 0;
1624 bool is_protected = (inner_class_access_flags &
ACC_PROTECTED) != 0;
1625 bool is_static = (inner_class_access_flags &
ACC_STATIC) != 0;
1630 bool is_inner_class = remove_separator_char(
id2string(parsed_class.
name),
'.') ==
1631 remove_separator_char(inner_class_info_name,
'/');
1638 if(inner_name_index == 0)
1642 if(outer_class_info_index == 0)
1650 std::string outer_class_info_name =
1671 std::vector<irep_idt> exceptions;
1672 for(
size_t i = 0; i < number_of_exceptions; i++)
1677 exceptions.push_back(exception_name);
1689 if(attribute_name==
"SourceFile")
1695 size_t last_index=fqn.find_last_of(
".");
1696 if(last_index==std::string::npos)
1700 std::string package_name=fqn.substr(0, last_index+1);
1701 std::replace(package_name.begin(), package_name.end(),
'.',
'/');
1702 const std::string &full_file_name=
1704 sourcefile_name=full_file_name;
1707 for(methodst::iterator m_it=parsed_class.
methods.begin();
1708 m_it!=parsed_class.
methods.end();
1711 m_it->source_location.set_file(sourcefile_name);
1712 for(instructionst::iterator i_it=m_it->instructions.begin();
1713 i_it!=m_it->instructions.end();
1716 if(!i_it->source_location.get_line().empty())
1717 i_it->source_location.set_file(sourcefile_name);
1721 else if(attribute_name==
"Signature")
1729 else if(attribute_name==
"RuntimeInvisibleAnnotations" ||
1730 attribute_name==
"RuntimeVisibleAnnotations")
1734 else if(attribute_name ==
"BootstrapMethods")
1740 "only one BootstrapMethods argument is allowed in a class file");
1746 else if(attribute_name ==
"InnerClasses")
1749 parsed_class, attribute_length);
1759 for(std::size_t j=0; j<methods_count; j++)
1763 #define ACC_PUBLIC 0x0001 1764 #define ACC_PRIVATE 0x0002 1765 #define ACC_PROTECTED 0x0004 1766 #define ACC_STATIC 0x0008 1767 #define ACC_FINAL 0x0010 1768 #define ACC_SUPER 0x0020 1769 #define ACC_VOLATILE 0x0040 1770 #define ACC_TRANSIENT 0x0080 1771 #define ACC_INTERFACE 0x0200 1772 #define ACC_ABSTRACT 0x0400 1773 #define ACC_SYNTHETIC 0x1000 1774 #define ACC_ANNOTATION 0x2000 1775 #define ACC_ENUM 0x4000 1798 const auto flags = (method.
is_public ? 1 : 0) +
1801 DATA_INVARIANT(flags<=1,
"at most one of public, protected, private");
1804 for(std::size_t j=0; j<attributes_count; j++)
1812 java_bytecode_parser.
in=&istream;
1815 bool parser_result=java_bytecode_parser.
parse();
1822 return std::move(java_bytecode_parser.
parse_tree);
1828 std::ifstream in(
file, std::ios::binary);
1833 message.
error() <<
"failed to open input file `" 1846 u2 local_variable_type_table_length=
read_u2();
1850 "Local variable type table cannot have more elements " 1851 "than the local variable table.");
1852 for(std::size_t i=0; i<local_variable_type_table_length; i++)
1864 if(lvar.index==index &&
1866 lvar.start_pc==start_pc &&
1867 lvar.length==length)
1876 "Entry in LocalVariableTypeTable must be present in LVT");
1888 const std::function<pool_entryt &(u2)> pool_entry_lambda =
1897 std::string class_name = class_entry.
get_name(pool_entry_lambda);
1899 std::replace(class_name.begin(), class_name.end(),
'.',
'$');
1901 std::replace(class_name.begin(), class_name.end(),
'/',
'.');
1902 const std::string method_ref =
1903 class_name +
"." + name_and_type.
get_name(pool_entry_lambda) +
':' +
1915 name_and_type.
get_name(pool_entry_lambda);
1920 return lambda_method_handle;
1932 for(
size_t bootstrap_method_index = 0;
1933 bootstrap_method_index < num_bootstrap_methods;
1934 ++bootstrap_method_index)
1936 u2 bootstrap_methodhandle_ref =
read_u2();
1942 debug() <<
"INFO: parse BootstrapMethod handle " << num_bootstrap_arguments
1946 u2_valuest u2_values(num_bootstrap_arguments);
1947 for(
size_t i = 0; i < num_bootstrap_arguments; i++)
1980 if(num_bootstrap_arguments < 3)
1983 parsed_class, bootstrap_method_index, std::move(u2_values));
1985 <<
"format of BootstrapMethods entry not recognized: too few arguments" 1990 u2 interface_type_index = u2_values[0];
1991 u2 method_handle_index = u2_values[1];
1992 u2 method_type_index = u2_values[2];
1998 bool recognized =
true;
1999 for(
size_t i = 3; i < num_bootstrap_arguments; i++)
2001 u2 skipped_argument = u2_values[i];
2007 debug() <<
"format of BootstrapMethods entry not recognized: extra " 2008 "arguments of wrong type" 2011 parsed_class, bootstrap_method_index, std::move(u2_values));
2025 debug() <<
"format of BootstrapMethods entry not recognized: arguments " 2029 parsed_class, bootstrap_method_index, std::move(u2_values));
2033 debug() <<
"INFO: parse lambda handle" <<
eom;
2037 if(!lambda_method_handle.has_value())
2039 debug() <<
"format of BootstrapMethods entry not recognized: method " 2040 "handle not recognised" 2043 parsed_class, bootstrap_method_index, std::move(u2_values));
2051 lambda_method_handle->interface_type =
2053 lambda_method_handle->method_type =
pool_entry(method_type_argument.
ref1).
s;
2054 lambda_method_handle->u2_values = std::move(u2_values);
2055 debug() <<
"lambda function reference " 2056 <<
id2string(lambda_method_handle->lambda_method_name)
2057 <<
" in class \"" << parsed_class.
name <<
"\"" 2058 <<
"\n interface type is " 2060 <<
"\n method type is " 2063 bootstrap_method_index, *lambda_method_handle);
2074 size_t bootstrap_method_index,
#define VTYPE_INFO_OBJECT
The type of an expression.
java_bytecode_parse_treet::classt::lambda_method_handlet lambda_method_handlet
Fixed-width bit-vector with unsigned binary interpretation.
void rinterfaces(classt &parsed_class)
void store_unknown_method_handle(classt &parsed_class, size_t bootstrap_method_index, u2_valuest u2_values) const
Creates an unknown method handle and puts it into the parsed_class.
const std::string & id2string(const irep_idt &d)
void set_java_bytecode_index(const irep_idt &index)
static lambda_method_handlet create_unknown_handle(const u2_valuest params)
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.
java_bytecode_parse_treet::classt::u2_valuest u2_valuest
optionalt< std::string > signature
void rRuntimeAnnotation_attribute(annotationst &)
#define CONSTANT_Methodref
std::list< fieldt > fieldst
constant_exprt to_expr() const
#define CONSTANT_MethodType
void rinner_classes_attribute(classt &parsed_class, const u4 &attribute_length)
Corresponds to the element_value structure Described in Java 8 specification 4.7.6 https://docs...
std::vector< instructiont > instructionst
pool_entryt & pool_entry(u2 index)
void rmethod(classt &parsed_class)
method_handle_kindt
Correspond to the different valid values for field reference_kind From Java 8 spec 4...
java_bytecode_parse_treet::annotationst annotationst
void rmethods(classt &parsed_class)
#define CONSTANT_InterfaceMethodref
struct bytecode_infot const bytecode_info[]
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
bool attribute_bootstrapmethods_read
An expression denoting a type.
java_bytecode_parse_treet parse_tree
#define VTYPE_INFO_DOUBLE
const componentst & components() const
method_handle_typet handle_type
optionalt< std::string > signature
#define CONSTANT_Fieldref
Represents the argument of an instruction that uses a CONSTANT_Fieldref This is used for example as a...
Corresponds to the CONSTANT_Class_info Structure Described in Java 8 specification 4...
std::vector< annotationt > annotationst
class_infot(const pool_entryt &entry)
exprt & constant(u2 index)
#define VTYPE_INFO_ITEM_NULL
static mstreamt & eom(mstreamt &m)
#define POSTCONDITION(CONDITION)
std::string get_name(pool_entry_lookupt pool_entry) const
#define INVARIANT(CONDITION, REASON)
static ieee_float_spect double_precision()
class_infot get_class(pool_entry_lookupt pool_entry) const
void relement_value_pairs(annotationt::element_value_pairst &)
#define CONSTANT_MethodHandle
java_bytecode_parsert::pool_entryt pool_entryt
const irep_idt & id() const
irep_idt lambda_method_name
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...
java_bytecode_parse_treet::instructiont instructiont
source_locationt source_location
optionalt< java_bytecode_parse_treet > java_bytecode_parse(std::istream &istream, message_handlert &message_handler)
void unpack(const mp_integer &i)
A reference into the symbol table.
std::vector< pool_entryt > constant_poolt
name_and_type_infot get_name_and_type(pool_entry_lookupt pool_entry) const
#define VTYPE_INFO_UNINIT
#define CONSTANT_NameAndType
Fixed-width bit-vector with two's complement interpretation.
u2 get_class_index() const
void parse_local_variable_type_table(methodt &method)
Parses the local variable type table of a method.
void add_method_handle(size_t bootstrap_index, lambda_method_handlet handle)
nonstd::optional< T > optionalt
java_bytecode_parse_treet::classt classt
API to expression classes.
const irep_idt & get(const irep_namet &name) const
void set_line(const irep_idt &line)
static ieee_float_spect single_precision()
name_and_type_infot(java_bytecode_parsert::pool_entryt entry)
base_ref_infot get_reference(pool_entry_lookupt pool_entry) const
#define PRECONDITION(CONDITION)
#define VTYPE_INFO_UNINIT_THIS
bool has_prefix(const std::string &s, const std::string &prefix)
base_ref_infot(pool_entryt entry)
virtual void set_message_handler(message_handlert &_message_handler)
void rbytecode(methodt::instructionst &)
void skip_bytes(std::size_t bytes)
u8 read_bytes(size_t bytes)
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
irep_idt lambda_method_ref
void rclass_attribute(classt &parsed_class)
void rmethod_attribute(methodt &method)
void get_class_refs_rec(const typet &)
typet java_type_from_string_with_exception(const std::string &descriptor, const optionalt< std::string > &signature, const std::string &class_name)
stack_map_tablet stack_map_table
std::vector< element_value_pairt > element_value_pairst
void relement_value_pair(annotationt::element_value_pairt &)
Corresponds to the element_value structure Described in Java 8 specification 4.7.16.1 https://docs.oracle.com/javase/specs/jvms/se8/html/jvms-4.html#jvms-4.7.16.1.
std::string get_name(pool_entry_lookupt pool_entry) const
std::vector< u2 > u2_valuest
java_bytecode_parse_treet::classt::fieldst fieldst
method_handle_kindt reference_kind
void rfields(classt &parsed_class)
element_value_pairst element_value_pairs
std::vector< bytecodet > bytecodes
const java_method_typet & to_java_method_type(const typet &type)
java_bytecode_parse_treet::annotationt annotationt
mstreamt & result() const
constant_poolt constant_pool
instructionst instructions
std::function< java_bytecode_parsert::pool_entryt &(u2)> pool_entry_lookupt
structured_pool_entryt(java_bytecode_parsert::pool_entryt entry)
Base class for all expressions.
#define VTYPE_INFO_INTEGER
java_bytecode_parse_treet::methodt::instructionst instructionst
const parameterst & parameters() const
void read_bootstrapmethods_entry(classt &)
Read all entries of the BootstrapMethods attribute of a class file.
java_bytecode_parse_treet::fieldt fieldt
source_locationt source_location
void read_verification_type_info(methodt::verification_type_infot &)
u2 get_name_and_type_index() const
std::string to_string(const string_constraintt &expr)
Used for debug printing.
verification_type_info_type type
exception_tablet exception_table
method_handle_infot(java_bytecode_parsert::pool_entryt entry)
java_bytecode_parse_treet::methodt methodt
const typet type_entry(u2 index)
void rcode_attribute(methodt &method)
Corresponds to the CONSTANT_NameAndType_info Structure Described in Java 8 specification 4...
Expression to hold a symbol (variable)
std::list< methodt > methodst
const char * c_str() const
goto_programt coverage_criteriont message_handlert & message_handler
void rRuntimeAnnotation(annotationt &)
const typet & subtype() const
#define DATA_INVARIANT(CONDITION, REASON)
local_variable_tablet local_variable_table
java_bytecode_parse_treet::classt::methodst methodst
symbol_typet java_classname(const std::string &id)
std::string get_descriptor(pool_entry_lookupt pool_entry) const
java_bytecode_parse_treet::classt::method_handle_typet method_handle_typet
const irept & find(const irep_namet &name) const
std::vector< irep_idt > rexceptions_attribute()
Corresponds to the element_value structure Described in Java 8 specification 4.7.5 https://docs...
#define CONSTANT_InvokeDynamic
const typet & return_type() const
void rfield_attribute(fieldt &)
static std::string read_utf8_constant(const pool_entryt &entry)
const irep_idt & get_identifier() const
void set(const irep_namet &name, const irep_idt &value)
optionalt< lambda_method_handlet > parse_method_handle(const class method_handle_infot &entry)
Read method handle pointed to from constant pool entry at index, return type of method handle and nam...
std::vector< irep_idt > throws_exception_table