37 bool parse()
override;
71 log.
error() <<
"invalid constant pool index (" << index <<
")"
108 void rbytecode(std::vector<instructiont> &);
114 std::optional<lambda_method_handlet>
120 for(std::size_t i=0; i<bytes; i++)
131 template <
typename T>
135 std::is_unsigned<T>::value || std::is_signed<T>::value,
136 "T should be a signed or unsigned integer");
137 const constexpr size_t bytes =
sizeof(T);
145 return static_cast<T
>(
in->get());
148 for(
size_t i = 0; i < bytes; i++)
156 result |=
static_cast<u1>(
in->get());
164#define CONSTANT_Class 7
165#define CONSTANT_Fieldref 9
166#define CONSTANT_Methodref 10
167#define CONSTANT_InterfaceMethodref 11
168#define CONSTANT_String 8
169#define CONSTANT_Integer 3
170#define CONSTANT_Float 4
171#define CONSTANT_Long 5
172#define CONSTANT_Double 6
173#define CONSTANT_NameAndType 12
174#define CONSTANT_Utf8 1
175#define CONSTANT_MethodHandle 15
176#define CONSTANT_MethodType 16
177#define CONSTANT_InvokeDynamic 18
179#define VTYPE_INFO_TOP 0
180#define VTYPE_INFO_INTEGER 1
181#define VTYPE_INFO_FLOAT 2
182#define VTYPE_INFO_LONG 3
183#define VTYPE_INFO_DOUBLE 4
184#define VTYPE_INFO_ITEM_NULL 5
185#define VTYPE_INFO_UNINIT_THIS 6
186#define VTYPE_INFO_OBJECT 7
187#define VTYPE_INFO_UNINIT 8
296 "name_and_typeindex did not correspond to a name_and_type in the "
399 catch(
const char *message)
405 catch(
const std::string &message)
420#define ACC_PUBLIC 0x0001u
421#define ACC_PRIVATE 0x0002u
422#define ACC_PROTECTED 0x0004u
423#define ACC_STATIC 0x0008u
424#define ACC_FINAL 0x0010u
425#define ACC_SYNCHRONIZED 0x0020u
426#define ACC_BRIDGE 0x0040u
427#define ACC_NATIVE 0x0100u
428#define ACC_INTERFACE 0x0200u
429#define ACC_ABSTRACT 0x0400u
430#define ACC_STRICT 0x0800u
431#define ACC_SYNTHETIC 0x1000u
432#define ACC_ANNOTATION 0x2000u
433#define ACC_ENUM 0x4000u
435#define UNUSED_u2(x) \
437 const u2 x = read<u2>(); \
450 if(magic!=0xCAFEBABE)
531 if(
field.signature.has_value())
553 for(
const auto ¶meter_annotations : method.parameter_annotations)
556 if(method.signature.has_value())
571 for(
const auto &var : method.local_variable_table)
573 if(var.signature.has_value())
598 for(
const auto &p :
ct.parameters())
622 const std::vector<annotationt> &annotations)
624 for(
const auto &annotation : annotations)
724 log.
error() <<
"unknown constant pool entry (" << it->tag <<
")"
734 [&](constant_poolt::value_type &entry) {
739 const std::string &s = id2string(pool_entry(entry.ref1).s);
740 entry.expr = type_exprt(java_classname(s));
744 case CONSTANT_Fieldref:
746 const pool_entryt &nameandtype_entry = pool_entry(entry.ref2);
747 const pool_entryt &name_entry=pool_entry(nameandtype_entry.ref1);
748 const pool_entryt &class_entry = pool_entry(entry.ref1);
749 const pool_entryt &class_name_entry=pool_entry(class_entry.ref1);
750 typet type=type_entry(nameandtype_entry.ref2);
752 auto class_tag = java_classname(id2string(class_name_entry.s));
754 fieldref_exprt fieldref(type, name_entry.s, class_tag.get_identifier());
756 entry.expr = fieldref;
760 case CONSTANT_Methodref:
761 case CONSTANT_InterfaceMethodref:
763 const pool_entryt &nameandtype_entry = pool_entry(entry.ref2);
764 const pool_entryt &name_entry=pool_entry(nameandtype_entry.ref1);
765 const pool_entryt &class_entry = pool_entry(entry.ref1);
766 const pool_entryt &class_name_entry=pool_entry(class_entry.ref1);
767 typet type=type_entry(nameandtype_entry.ref2);
769 auto class_tag = java_classname(id2string(class_name_entry.s));
771 irep_idt mangled_method_name =
772 id2string(name_entry.s) +
":" +
773 id2string(pool_entry(nameandtype_entry.ref2).s);
775 irep_idt class_id = class_tag.get_identifier();
777 entry.expr = class_method_descriptor_exprt{
778 type, mangled_method_name, class_id, name_entry.s};
782 case CONSTANT_String:
785 entry.expr = java_string_literal_exprt{pool_entry(entry.ref1).s};
789 case CONSTANT_Integer:
790 entry.expr = from_integer(entry.number, java_int_type());
795 ieee_float_valuet value(ieee_float_spect::single_precision());
796 value.unpack(entry.number);
797 entry.expr = value.to_expr();
802 entry.expr = from_integer(entry.number, java_long_type());
805 case CONSTANT_Double:
807 ieee_float_valuet value(ieee_float_spect::double_precision());
808 value.unpack(entry.number);
809 entry.expr = value.to_expr();
813 case CONSTANT_NameAndType:
815 entry.expr.id(
"nameandtype");
819 case CONSTANT_MethodHandle:
821 entry.expr.id(
"methodhandle");
825 case CONSTANT_MethodType:
827 entry.expr.id(
"methodtype");
831 case CONSTANT_InvokeDynamic:
833 entry.expr.id(
"invokedynamic");
834 const pool_entryt &nameandtype_entry = pool_entry(entry.ref2);
835 typet type=type_entry(nameandtype_entry.ref2);
836 type.set(ID_java_lambda_method_handle_index, entry.ref1);
837 entry.expr.type() = type;
875 const auto flags = (
field.is_public ? 1 : 0) +
876 (
field.is_protected?1:0)+
877 (
field.is_private?1:0);
878 DATA_INVARIANT(flags<=1,
"at most one of public, protected, private");
919 std::string(
"Unexpected wide instruction: ") +
923 instructions.emplace_back();
966 instruction.
args.push_back(
977 instruction.
args.push_back(
1038 while(((address + 1u) & 3u) != 0)
1048 instruction.
args.push_back(
1056 for(std::size_t i=0; i<
npairs; i++)
1060 instruction.
args.push_back(
1064 instruction.
args.push_back(
1076 while(((address + 1u) & 3u) != 0)
1084 instruction.
args.push_back(
1103 instruction.
args.push_back(
1115 instruction.
args.push_back(
1150 throw "unknown JVM bytecode instruction";
1195 "The start_pc must be less than the end_pc as this is the range the "
1196 "exception is active");
1224 if(!instruction.source_location.get_line().empty())
1225 line_number = instruction.source_location.get_line();
1226 else if(!line_number.
empty())
1227 instruction.source_location.set_line(line_number);
1228 instruction.source_location.set_function(
1233 const auto it = std::find_if(
1237 return !instruction.source_location.get_line().empty();
1305 std::map<unsigned, std::reference_wrapper<instructiont>>
instruction_map;
1320 it->second.get().source_location.set_line(line_number);
1367 methodt::stack_map_table_entryt::SAME_LOCALS_ONE_STACK;
1377 methodt::stack_map_table_entryt::SAME_LOCALS_ONE_STACK_EXTENDED;
1397 =methodt::stack_map_table_entryt::SAME_EXTENDED;
1406 method.
stack_map_table[i].type=methodt::stack_map_table_entryt::APPEND;
1447 throw "error: unknown stack frame type encountered";
1461 v.
type=methodt::verification_type_infot::TOP;
1464 v.
type=methodt::verification_type_infot::INTEGER;
1467 v.
type=methodt::verification_type_infot::FLOAT;
1470 v.
type=methodt::verification_type_infot::LONG;
1473 v.
type=methodt::verification_type_infot::DOUBLE;
1476 v.
type=methodt::verification_type_infot::ITEM_NULL;
1479 v.
type=methodt::verification_type_infot::UNINITIALIZED_THIS;
1482 v.
type=methodt::verification_type_infot::OBJECT;
1486 v.
type=methodt::verification_type_infot::UNINITIALIZED;
1490 throw "error: unknown verification type info encountered";
1495 std::vector<annotationt> &annotations)
1503 annotations.push_back(annotation);
1605 std::string name = parsed_class.
name.
c_str();
1610 "The number of bytes to be read for the InnerClasses attribute does not "
1611 "match the attribute length.");
1617 str.erase(std::remove(str.begin(), str.end(),
ch), str.end());
1719 for(
auto &method : parsed_class.
methods)
1722 for(
auto &instruction : method.instructions)
1724 if(!instruction.source_location.get_line().empty())
1748 "only one BootstrapMethods argument is allowed in a class file");
1770#define ACC_PUBLIC 0x0001u
1771#define ACC_PRIVATE 0x0002u
1772#define ACC_PROTECTED 0x0004u
1773#define ACC_STATIC 0x0008u
1774#define ACC_FINAL 0x0010u
1775#define ACC_VARARGS 0x0080u
1776#define ACC_SUPER 0x0020u
1777#define ACC_VOLATILE 0x0040u
1778#define ACC_TRANSIENT 0x0080u
1779#define ACC_INTERFACE 0x0200u
1780#define ACC_ABSTRACT 0x0400u
1781#define ACC_SYNTHETIC 0x1000u
1782#define ACC_ANNOTATION 0x2000u
1783#define ACC_ENUM 0x4000u
1808 const auto flags = (method.
is_public ? 1 : 0) +
1811 DATA_INVARIANT(flags<=1,
"at most one of public, protected, private");
1819 std::istream &istream,
1822 bool skip_instructions)
1825 skip_instructions, message_handler);
1841 const std::string &file,
1844 bool skip_instructions)
1846 std::ifstream in(file, std::ios::binary);
1854 in, class_name, message_handler, skip_instructions);
1866 "Local variable type table cannot have more elements "
1867 "than the local variable table.");
1880 if(
lvar.index==index &&
1882 lvar.start_pc==start_pc &&
1883 lvar.length==length)
1892 "Entry in LocalVariableTypeTable must be present in LVT");
1929std::optional<java_bytecode_parsert::lambda_method_handlet>
1996 log.
debug() <<
"INFO: parse BootstrapMethod handle "
2038 <<
"format of BootstrapMethods entry not recognized: too few arguments"
2060 log.
debug() <<
"format of BootstrapMethods entry not recognized: extra "
2061 "arguments of wrong type"
2078 <<
"format of BootstrapMethods entry not recognized: arguments "
2091 log.
debug() <<
"format of BootstrapMethods entry not recognized: method "
2092 "handle not recognised"
2103 <<
"lambda function reference "
2107 <<
"\n interface type is "
2109 <<
"\n method type is "
struct bytecode_infot const bytecode_info[]
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Array constructor from list of elements.
class_infot get_class(const pool_entry_lookupt &pool_entry) const
name_and_type_infot get_name_and_type(const pool_entry_lookupt &pool_entry) const
u2 get_class_index() const
u2 get_name_and_type_index() const
base_ref_infot(const pool_entryt &entry)
Corresponds to the CONSTANT_Class_info Structure Described in Java 8 specification 4....
class_infot(const pool_entryt &entry)
std::string get_name(const pool_entry_lookupt &pool_entry) const
An expression describing a method on a class.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const char * c_str() const
Base class for all expressions.
std::vector< exprt > operandst
typet & type()
Return the type of the expression.
const irep_idt & get(const irep_idt &name) const
const irep_idt & id() const
pool_entryt & pool_entry(u2 index)
void get_annotation_class_refs(const std::vector< annotationt > &annotations)
For each of the given annotations, get a reference to its class and recursively get class references ...
void store_unknown_method_handle(size_t bootstrap_method_index)
Creates an unknown method handle and puts it into the parsed_class.
exprt get_relement_value()
Corresponds to the element_value structure Described in Java 8 specification 4.7.16....
java_bytecode_parse_treet::annotationt annotationt
java_bytecode_parse_treet::methodt methodt
void rRuntimeAnnotation_attribute(std::vector< annotationt > &)
const typet type_entry(u2 index)
void rfield_attribute(fieldt &)
void rbytecode(std::vector< instructiont > &)
void rcode_attribute(methodt &method)
void read_bootstrapmethods_entry()
Read all entries of the BootstrapMethods attribute of a class file.
void get_class_refs()
Get the class references for the benefit of a dependency analysis.
void get_annotation_value_class_refs(const exprt &value)
See java_bytecode_parsert::get_annotation_class_refs.
java_bytecode_parse_treet parse_tree
std::vector< pool_entryt > constant_poolt
java_bytecode_parsert(bool skip_instructions, message_handlert &message_handler)
void skip_bytes(std::size_t bytes)
void read_verification_type_info(methodt::verification_type_infot &)
java_bytecode_parse_treet::fieldt fieldt
constant_poolt constant_pool
void get_class_refs_rec(const typet &)
void parse_local_variable_type_table(methodt &method)
Parses the local variable type table of a method.
const bool skip_instructions
void rRuntimeAnnotation(annotationt &)
std::optional< 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...
void relement_value_pairs(annotationt::element_value_pairst &)
exprt & constant(u2 index)
void rinner_classes_attribute(const u4 &attribute_length)
Corresponds to the element_value structure Described in Java 8 specification 4.7.6 https://docs....
std::vector< irep_idt > rexceptions_attribute()
Corresponds to the element_value structure Described in Java 8 specification 4.7.5 https://docs....
void rmethod_attribute(methodt &method)
method_handle_kindt
Indicates what sort of code should be synthesised for a lambda call:
@ LAMBDA_STATIC_METHOD_HANDLE
Direct call to the given method.
@ LAMBDA_VIRTUAL_METHOD_HANDLE
Virtual call to the given interface or method.
@ UNKNOWN_HANDLE
Can't be called.
@ LAMBDA_CONSTRUCTOR_HANDLE
Instantiate the needed type then call a constructor.
method_handle_infot(const pool_entryt &entry)
base_ref_infot get_reference(const pool_entry_lookupt &pool_entry) const
method_handle_kindt handle_kind
method_handle_kindt get_handle_kind() const
method_handle_kindt
Correspond to the different valid values for field handle_kind From Java 8 spec 4....
Corresponds to the CONSTANT_NameAndType_info Structure Described in Java 8 specification 4....
name_and_type_infot(const pool_entryt &entry)
std::string get_descriptor(const pool_entry_lookupt &pool_entry) const
std::string get_name(const pool_entry_lookupt &pool_entry) const
Fixed-width bit-vector with two's complement interpretation.
const irep_idt & get_function() const
void set_java_bytecode_index(const irep_idt &index)
void set_line(const irep_idt &line)
void set_function(const irep_idt &function)
A struct tag type, i.e., struct_typet with an identifier.
Structure type, corresponds to C style structs.
std::function< pool_entryt &(u2)> pool_entry_lookupt
static std::string read_utf8_constant(const pool_entryt &entry)
structured_pool_entryt(const pool_entryt &entry)
static symbol_exprt typeless(const irep_idt &id)
Generate a symbol_exprt without a proper type.
const irep_idt & get_identifier() const
An expression denoting a type.
The type of an expression, extends irept.
Fixed-width bit-vector with unsigned binary interpretation.
const std::string & id2string(const irep_idt &d)
#define CONSTANT_Fieldref
#define VTYPE_INFO_DOUBLE
#define CONSTANT_InvokeDynamic
#define CONSTANT_Methodref
#define CONSTANT_NameAndType
#define VTYPE_INFO_OBJECT
std::optional< java_bytecode_parse_treet > java_bytecode_parse(std::istream &istream, const irep_idt &class_name, message_handlert &message_handler, bool skip_instructions)
Attempt to parse a Java class from the given stream.
#define CONSTANT_MethodType
#define VTYPE_INFO_INTEGER
static java_class_typet::method_handle_kindt get_method_handle_type(method_handle_infot::method_handle_kindt java_handle_kind)
Translate the lambda method reference kind in a class file into the kind of handling the method requi...
#define VTYPE_INFO_UNINIT
#define CONSTANT_InterfaceMethodref
#define VTYPE_INFO_UNINIT_THIS
#define CONSTANT_MethodHandle
#define VTYPE_INFO_ITEM_NULL
Representation of a constant Java string.
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.
struct_tag_typet java_classname(const std::string &id)
std::optional< 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.
bool is_java_array_tag(const irep_idt &tag)
See above.
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.
const java_method_typet & to_java_method_type(const typet &type)
std::optional< typet > java_type_from_string_with_exception(const std::string &descriptor, const std::optional< std::string > &signature, const std::string &class_name)
static std::optional< java_class_typet::java_lambda_method_handlet > lambda_method_handle(const symbol_table_baset &symbol_table, const irep_idt &method_identifier, const java_method_typet &dynamic_method_type)
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
#define POSTCONDITION(CONDITION)
API to expression classes.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
std::vector< element_value_pairt > element_value_pairst
element_value_pairst element_value_pairs
static lambda_method_handlet get_unknown_handle()
std::optional< std::string > signature
bool attribute_bootstrapmethods_read
void add_method_handle(size_t bootstrap_index, const lambda_method_handlet &handle)
source_locationt source_location
std::optional< std::string > signature
verification_type_info_type type
exception_tablet exception_table
std::vector< annotationst > parameter_annotations
Java annotations that were applied to parameters of this method.
source_locationt source_location
stack_map_tablet stack_map_table
instructionst instructions
local_variable_tablet local_variable_table
std::vector< irep_idt > throws_exception_table