cprover
java_bytecode_parser.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "java_bytecode_parser.h"
10 
11 #include <algorithm>
12 #include <fstream>
13 #include <map>
14 #include <string>
15 
16 #include <util/arith_tools.h>
17 #include <util/ieee_float.h>
18 #include <util/parser.h>
19 #include <util/prefix.h>
20 #include <util/std_expr.h>
21 #include <util/string_constant.h>
22 #include <util/optional.h>
23 
24 #include "bytecode_info.h"
27 #include "java_types.h"
28 
29 class java_bytecode_parsert final : public parsert
30 {
31 public:
34  {
35  }
36 
37  bool parse() override;
38 
39  struct pool_entryt
40  {
41  u1 tag = 0;
42  u2 ref1 = 0;
43  u2 ref2 = 0;
45  u8 number = 0;
47  };
48 
50 
51 private:
61 
62  using constant_poolt = std::vector<pool_entryt>;
63 
65 
66  const bool skip_instructions = false;
67 
69  {
70  if(index==0 || index>=constant_pool.size())
71  {
72  error() << "invalid constant pool index (" << index << ")" << eom;
73  error() << "constant pool size: " << constant_pool.size() << eom;
74  throw 0;
75  }
76 
77  return constant_pool[index];
78  }
79 
80  exprt &constant(u2 index)
81  {
82  return pool_entry(index).expr;
83  }
84 
85  const typet type_entry(u2 index)
86  {
87  return *java_type_from_string(id2string(pool_entry(index).s));
88  }
89 
90  void rClassFile();
91  void rconstant_pool();
92  void rinterfaces();
93  void rfields();
94  void rmethods();
95  void rmethod();
96  void rinner_classes_attribute(const u4 &attribute_length);
97  std::vector<irep_idt> rexceptions_attribute();
98  void rclass_attribute();
99  void rRuntimeAnnotation_attribute(std::vector<annotationt> &);
103  void rmethod_attribute(methodt &method);
104  void rfield_attribute(fieldt &);
105  void rcode_attribute(methodt &method);
106  void read_verification_type_info(methodt::verification_type_infot &);
107  void rbytecode(std::vector<instructiont> &);
108  void get_class_refs();
109  void get_class_refs_rec(const typet &);
110  void get_annotation_class_refs(const std::vector<annotationt> &annotations);
111  void get_annotation_value_class_refs(const exprt &value);
114  parse_method_handle(const class method_handle_infot &entry);
116 
117  void skip_bytes(std::size_t bytes)
118  {
119  for(std::size_t i=0; i<bytes; i++)
120  {
121  if(!*in)
122  {
123  error() << "unexpected end of bytecode file" << eom;
124  throw 0;
125  }
126  in->get();
127  }
128  }
129 
130  template <typename T>
131  T read()
132  {
133  static_assert(
134  std::is_unsigned<T>::value, "T should be an unsigned integer");
135  const constexpr size_t bytes = sizeof(T);
136  u8 result = 0;
137  for(size_t i = 0; i < bytes; i++)
138  {
139  if(!*in)
140  {
141  error() << "unexpected end of bytecode file" << eom;
142  throw 0;
143  }
144  result <<= 8u;
145  result |= static_cast<u1>(in->get());
146  }
147  return narrow_cast<T>(result);
148  }
149 
151  size_t bootstrap_method_index,
152  std::vector<u2> u2_values);
153 };
154 
155 #define CONSTANT_Class 7
156 #define CONSTANT_Fieldref 9
157 #define CONSTANT_Methodref 10
158 #define CONSTANT_InterfaceMethodref 11
159 #define CONSTANT_String 8
160 #define CONSTANT_Integer 3
161 #define CONSTANT_Float 4
162 #define CONSTANT_Long 5
163 #define CONSTANT_Double 6
164 #define CONSTANT_NameAndType 12
165 #define CONSTANT_Utf8 1
166 #define CONSTANT_MethodHandle 15
167 #define CONSTANT_MethodType 16
168 #define CONSTANT_InvokeDynamic 18
169 
170 #define VTYPE_INFO_TOP 0
171 #define VTYPE_INFO_INTEGER 1
172 #define VTYPE_INFO_FLOAT 2
173 #define VTYPE_INFO_LONG 3
174 #define VTYPE_INFO_DOUBLE 4
175 #define VTYPE_INFO_ITEM_NULL 5
176 #define VTYPE_INFO_UNINIT_THIS 6
177 #define VTYPE_INFO_OBJECT 7
178 #define VTYPE_INFO_UNINIT 8
179 
181 {
182 public:
184  using pool_entry_lookupt = std::function<pool_entryt &(u2)>;
185 
186  explicit structured_pool_entryt(const pool_entryt &entry) : tag(entry.tag)
187  {
188  }
189 
190  u1 get_tag() const
191  {
192  return tag;
193  }
194 
195 protected:
196  static std::string read_utf8_constant(const pool_entryt &entry)
197  {
198  INVARIANT(
199  entry.tag == CONSTANT_Utf8, "Name entry must be a constant UTF-8");
200  return id2string(entry.s);
201  }
202 
203 private:
205 };
206 
210 {
211 public:
212  explicit class_infot(const pool_entryt &entry) : structured_pool_entryt(entry)
213  {
214  PRECONDITION(entry.tag == CONSTANT_Class);
215  name_index = entry.ref1;
216  }
217 
218  std::string get_name(const pool_entry_lookupt &pool_entry) const
219  {
220  const pool_entryt &name_entry = pool_entry(name_index);
221  return read_utf8_constant(name_entry);
222  }
223 
224 private:
226 };
227 
231 {
232 public:
233  explicit name_and_type_infot(const pool_entryt &entry)
234  : structured_pool_entryt(entry)
235  {
237  name_index = entry.ref1;
238  descriptor_index = entry.ref2;
239  }
240 
241  std::string get_name(const pool_entry_lookupt &pool_entry) const
242  {
243  const pool_entryt &name_entry = pool_entry(name_index);
244  return read_utf8_constant(name_entry);
245  }
246 
247  std::string get_descriptor(const pool_entry_lookupt &pool_entry) const
248  {
249  const pool_entryt &descriptor_entry = pool_entry(descriptor_index);
250  return read_utf8_constant(descriptor_entry);
251  }
252 
253 private:
256 };
257 
259 {
260 public:
261  explicit base_ref_infot(const pool_entryt &entry)
262  : structured_pool_entryt(entry)
263  {
264  PRECONDITION(
265  entry.tag == CONSTANT_Fieldref || entry.tag == CONSTANT_Methodref ||
267  class_index = entry.ref1;
268  name_and_type_index = entry.ref2;
269  }
270 
272  {
273  return class_index;
274  }
276  {
277  return name_and_type_index;
278  }
279 
281  get_name_and_type(const pool_entry_lookupt &pool_entry) const
282  {
283  const pool_entryt &name_and_type_entry = pool_entry(name_and_type_index);
284 
285  INVARIANT(
286  name_and_type_entry.tag == CONSTANT_NameAndType,
287  "name_and_typeindex did not correspond to a name_and_type in the "
288  "constant pool");
289 
290  return name_and_type_infot{name_and_type_entry};
291  }
292 
293  class_infot get_class(const pool_entry_lookupt &pool_entry) const
294  {
295  const pool_entryt &class_entry = pool_entry(class_index);
296 
297  return class_infot{class_entry};
298  }
299 
300 private:
303 };
304 
306 {
307 public:
312  {
313  REF_getField = 1,
314  REF_getStatic = 2,
315  REF_putField = 3,
316  REF_putStatic = 4,
317  REF_invokeVirtual = 5,
318  REF_invokeStatic = 6,
319  REF_invokeSpecial = 7,
322  };
323 
324  explicit method_handle_infot(const pool_entryt &entry)
325  : structured_pool_entryt(entry)
326  {
328  PRECONDITION(entry.ref1 > 0 && entry.ref1 < 10); // Java 8 spec 4.4.8
329  reference_kind = static_cast<method_handle_kindt>(entry.ref1);
330  reference_index = entry.ref2;
331  }
332 
334  {
335  const base_ref_infot ref_entry{pool_entry(reference_index)};
336 
337  // validate the correctness of the constant pool entry
338  switch(reference_kind)
339  {
344  {
345  INVARIANT(ref_entry.get_tag() == CONSTANT_Fieldref, "4.4.2");
346  break;
347  }
350  {
351  INVARIANT(ref_entry.get_tag() == CONSTANT_Methodref, "4.4.2");
352  break;
353  }
356  {
357  INVARIANT(
358  ref_entry.get_tag() == CONSTANT_Methodref ||
359  ref_entry.get_tag() == CONSTANT_InterfaceMethodref,
360  "4.4.2");
361  break;
362  }
364  {
365  INVARIANT(ref_entry.get_tag() == CONSTANT_InterfaceMethodref, "4.4.8");
366  break;
367  }
368  }
369 
370  return ref_entry;
371  }
372 
373 private:
376 };
377 
379 {
380  try
381  {
382  rClassFile();
383  }
384 
385  catch(const char *message)
386  {
387  error() << message << eom;
388  return true;
389  }
390 
391  catch(const std::string &message)
392  {
393  error() << message << eom;
394  return true;
395  }
396 
397  catch(...)
398  {
399  error() << "parsing error" << eom;
400  return true;
401  }
402 
403  return false;
404 }
405 
406 #define ACC_PUBLIC 0x0001u
407 #define ACC_PRIVATE 0x0002u
408 #define ACC_PROTECTED 0x0004u
409 #define ACC_STATIC 0x0008u
410 #define ACC_FINAL 0x0010u
411 #define ACC_SYNCHRONIZED 0x0020u
412 #define ACC_BRIDGE 0x0040u
413 #define ACC_NATIVE 0x0100u
414 #define ACC_INTERFACE 0x0200u
415 #define ACC_ABSTRACT 0x0400u
416 #define ACC_STRICT 0x0800u
417 #define ACC_SYNTHETIC 0x1000u
418 #define ACC_ANNOTATION 0x2000u
419 #define ACC_ENUM 0x4000u
420 
421 #define UNUSED_u2(x) \
422  { \
423  const u2 x = read<u2>(); \
424  (void)x; \
425  } \
426  (void)0
427 
429 {
431 
432  const u4 magic = read<u4>();
433  UNUSED_u2(minor_version);
434  const u2 major_version = read<u2>();
435 
436  if(magic!=0xCAFEBABE)
437  {
438  error() << "wrong magic" << eom;
439  throw 0;
440  }
441 
442  if(major_version<44)
443  {
444  error() << "unexpected major version" << eom;
445  throw 0;
446  }
447 
448  rconstant_pool();
449 
450  classt &parsed_class=parse_tree.parsed_class;
451 
452  const u2 access_flags = read<u2>();
453  const u2 this_class = read<u2>();
454  const u2 super_class = read<u2>();
455 
456  parsed_class.is_abstract=(access_flags&ACC_ABSTRACT)!=0;
457  parsed_class.is_enum=(access_flags&ACC_ENUM)!=0;
458  parsed_class.is_public=(access_flags&ACC_PUBLIC)!=0;
459  parsed_class.is_protected=(access_flags&ACC_PROTECTED)!=0;
460  parsed_class.is_private=(access_flags&ACC_PRIVATE)!=0;
461  parsed_class.is_final = (access_flags & ACC_FINAL) != 0;
462  parsed_class.is_interface = (access_flags & ACC_INTERFACE) != 0;
463  parsed_class.is_synthetic = (access_flags & ACC_SYNTHETIC) != 0;
464  parsed_class.is_annotation = (access_flags & ACC_ANNOTATION) != 0;
465  parsed_class.name=
466  constant(this_class).type().get(ID_C_base_name);
467 
468  if(super_class!=0)
469  parsed_class.super_class = constant(super_class).type().get(ID_C_base_name);
470 
471  rinterfaces();
472  rfields();
473  rmethods();
474 
475  // count elements of enum
476  if(parsed_class.is_enum)
477  for(fieldt &field : parse_tree.parsed_class.fields)
478  if(field.is_enum)
480 
481  const u2 attributes_count = read<u2>();
482 
483  for(std::size_t j=0; j<attributes_count; j++)
485 
486  get_class_refs();
487 
489 }
490 
493 {
494  for(const auto &c : constant_pool)
495  {
496  switch(c.tag)
497  {
498  case CONSTANT_Class:
499  get_class_refs_rec(c.expr.type());
500  break;
501 
505  break;
506 
507  default: {}
508  }
509  }
510 
512 
513  for(const auto &field : parse_tree.parsed_class.fields)
514  {
515  get_annotation_class_refs(field.annotations);
516 
517  if(field.signature.has_value())
518  {
520  field.descriptor,
521  field.signature,
522  "java::" + id2string(parse_tree.parsed_class.name));
523 
524  // add generic type args to class refs as dependencies, same below for
525  // method types and entries from the local variable type table
527  field_type, parse_tree.class_refs);
528  get_class_refs_rec(field_type);
529  }
530  else
531  {
532  get_class_refs_rec(*java_type_from_string(field.descriptor));
533  }
534  }
535 
536  for(const auto &method : parse_tree.parsed_class.methods)
537  {
538  get_annotation_class_refs(method.annotations);
539  for(const auto &parameter_annotations : method.parameter_annotations)
540  get_annotation_class_refs(parameter_annotations);
541 
542  if(method.signature.has_value())
543  {
545  method.descriptor,
546  method.signature,
547  "java::" + id2string(parse_tree.parsed_class.name));
549  method_type, parse_tree.class_refs);
550  get_class_refs_rec(method_type);
551  }
552  else
553  {
554  get_class_refs_rec(*java_type_from_string(method.descriptor));
555  }
556 
557  for(const auto &var : method.local_variable_table)
558  {
559  if(var.signature.has_value())
560  {
562  var.descriptor,
563  var.signature,
564  "java::" + id2string(parse_tree.parsed_class.name));
566  var_type, parse_tree.class_refs);
567  get_class_refs_rec(var_type);
568  }
569  else
570  {
571  get_class_refs_rec(*java_type_from_string(var.descriptor));
572  }
573  }
574  }
575 }
576 
578 {
579  if(src.id()==ID_code)
580  {
581  const java_method_typet &ct = to_java_method_type(src);
582  const typet &rt=ct.return_type();
583  get_class_refs_rec(rt);
584  for(const auto &p : ct.parameters())
585  get_class_refs_rec(p.type());
586  }
587  else if(src.id() == ID_struct_tag)
588  {
589  const struct_tag_typet &struct_tag_type = to_struct_tag_type(src);
590  if(is_java_array_tag(struct_tag_type.get_identifier()))
592  else
593  parse_tree.class_refs.insert(src.get(ID_C_base_name));
594  }
595  else if(src.id()==ID_struct)
596  {
597  const struct_typet &struct_type=to_struct_type(src);
598  for(const auto &c : struct_type.components())
599  get_class_refs_rec(c.type());
600  }
601  else if(src.id()==ID_pointer)
603 }
604 
608  const std::vector<annotationt> &annotations)
609 {
610  for(const auto &annotation : annotations)
611  {
612  get_class_refs_rec(annotation.type);
613  for(const auto &element_value_pair : annotation.element_value_pairs)
614  get_annotation_value_class_refs(element_value_pair.value);
615  }
616 }
617 
622 {
623  if(const auto &symbol_expr = expr_try_dynamic_cast<symbol_exprt>(value))
624  {
625  const irep_idt &value_id = symbol_expr->get_identifier();
627  }
628  else if(const auto &array_expr = expr_try_dynamic_cast<array_exprt>(value))
629  {
630  for(const exprt &operand : array_expr->operands())
632  }
633  // TODO: enum and nested annotation cases (once these are correctly parsed by
634  // get_relement_value).
635  // Note that in the cases where expr is a string or primitive type, no
636  // additional class references are needed.
637 }
638 
640 {
641  const u2 constant_pool_count = read<u2>();
642  if(constant_pool_count==0)
643  {
644  error() << "invalid constant_pool_count" << eom;
645  throw 0;
646  }
647 
648  constant_pool.resize(constant_pool_count);
649 
650  for(auto it = std::next(constant_pool.begin()); it != constant_pool.end();
651  it++)
652  {
653  it->tag = read<u1>();
654 
655  switch(it->tag)
656  {
657  case CONSTANT_Class:
658  it->ref1 = read<u2>();
659  break;
660 
661  case CONSTANT_Fieldref:
662  case CONSTANT_Methodref:
666  it->ref1 = read<u2>();
667  it->ref2 = read<u2>();
668  break;
669 
670  case CONSTANT_String:
671  case CONSTANT_MethodType:
672  it->ref1 = read<u2>();
673  break;
674 
675  case CONSTANT_Integer:
676  case CONSTANT_Float:
677  it->number = read<u4>();
678  break;
679 
680  case CONSTANT_Long:
681  case CONSTANT_Double:
682  it->number = read<u8>();
683  // Eight-byte constants take up two entries in the constant_pool table.
684  if(it==constant_pool.end())
685  {
686  error() << "invalid double entry" << eom;
687  throw 0;
688  }
689  it++;
690  it->tag=0;
691  break;
692 
693  case CONSTANT_Utf8:
694  {
695  const u2 bytes = read<u2>();
696  std::string s;
697  s.resize(bytes);
698  for(auto &ch : s)
699  ch = read<u1>();
700  it->s = s; // Add to string table
701  }
702  break;
703 
705  it->ref1 = read<u1>();
706  it->ref2 = read<u2>();
707  break;
708 
709  default:
710  error() << "unknown constant pool entry (" << it->tag << ")"
711  << eom;
712  throw 0;
713  }
714  }
715 
716  // we do a bit of post-processing after we have them all
717  std::for_each(
718  std::next(constant_pool.begin()),
719  constant_pool.end(),
720  [&](constant_poolt::value_type &entry) {
721  switch(entry.tag)
722  {
723  case CONSTANT_Class:
724  {
725  const std::string &s = id2string(pool_entry(entry.ref1).s);
726  entry.expr = type_exprt(java_classname(s));
727  }
728  break;
729 
730  case CONSTANT_Fieldref:
731  {
732  const pool_entryt &nameandtype_entry = pool_entry(entry.ref2);
733  const pool_entryt &name_entry=pool_entry(nameandtype_entry.ref1);
734  const pool_entryt &class_entry = pool_entry(entry.ref1);
735  const pool_entryt &class_name_entry=pool_entry(class_entry.ref1);
736  typet type=type_entry(nameandtype_entry.ref2);
737 
738  auto class_tag = java_classname(id2string(class_name_entry.s));
739 
740  fieldref_exprt fieldref(type, name_entry.s, class_tag.get_identifier());
741 
742  entry.expr = fieldref;
743  }
744  break;
745 
746  case CONSTANT_Methodref:
747  case CONSTANT_InterfaceMethodref:
748  {
749  const pool_entryt &nameandtype_entry = pool_entry(entry.ref2);
750  const pool_entryt &name_entry=pool_entry(nameandtype_entry.ref1);
751  const pool_entryt &class_entry = pool_entry(entry.ref1);
752  const pool_entryt &class_name_entry=pool_entry(class_entry.ref1);
753  typet type=type_entry(nameandtype_entry.ref2);
754 
755  auto class_tag = java_classname(id2string(class_name_entry.s));
756 
757  irep_idt mangled_method_name =
758  id2string(name_entry.s) + ":" +
759  id2string(pool_entry(nameandtype_entry.ref2).s);
760 
761  irep_idt class_id = class_tag.get_identifier();
762 
763  entry.expr = class_method_descriptor_exprt{
764  type, mangled_method_name, class_id, name_entry.s};
765  }
766  break;
767 
768  case CONSTANT_String:
769  {
770  // ldc turns these into references to java.lang.String
771  entry.expr = java_string_literal_exprt{pool_entry(entry.ref1).s};
772  }
773  break;
774 
775  case CONSTANT_Integer:
776  entry.expr = from_integer(entry.number, java_int_type());
777  break;
778 
779  case CONSTANT_Float:
780  {
781  ieee_floatt value(ieee_float_spect::single_precision());
782  value.unpack(entry.number);
783  entry.expr = value.to_expr();
784  }
785  break;
786 
787  case CONSTANT_Long:
788  entry.expr = from_integer(entry.number, java_long_type());
789  break;
790 
791  case CONSTANT_Double:
792  {
793  ieee_floatt value(ieee_float_spect::double_precision());
794  value.unpack(entry.number);
795  entry.expr = value.to_expr();
796  }
797  break;
798 
799  case CONSTANT_NameAndType:
800  {
801  entry.expr.id("nameandtype");
802  }
803  break;
804 
805  case CONSTANT_MethodHandle:
806  {
807  entry.expr.id("methodhandle");
808  }
809  break;
810 
811  case CONSTANT_MethodType:
812  {
813  entry.expr.id("methodtype");
814  }
815  break;
816 
817  case CONSTANT_InvokeDynamic:
818  {
819  entry.expr.id("invokedynamic");
820  const pool_entryt &nameandtype_entry = pool_entry(entry.ref2);
821  typet type=type_entry(nameandtype_entry.ref2);
822  type.set(ID_java_lambda_method_handle_index, entry.ref1);
823  entry.expr.type() = type;
824  }
825  break;
826  }
827  });
828 }
829 
831 {
832  const u2 interfaces_count = read<u2>();
833 
834  for(std::size_t i=0; i<interfaces_count; i++)
836  constant(read<u2>()).type().get(ID_C_base_name));
837 }
838 
840 {
841  const u2 fields_count = read<u2>();
842 
843  for(std::size_t i=0; i<fields_count; i++)
844  {
846 
847  const u2 access_flags = read<u2>();
848  const u2 name_index = read<u2>();
849  const u2 descriptor_index = read<u2>();
850  const u2 attributes_count = read<u2>();
851 
852  field.name=pool_entry(name_index).s;
853  field.is_static=(access_flags&ACC_STATIC)!=0;
854  field.is_final=(access_flags&ACC_FINAL)!=0;
855  field.is_enum=(access_flags&ACC_ENUM)!=0;
856 
857  field.descriptor=id2string(pool_entry(descriptor_index).s);
858  field.is_public=(access_flags&ACC_PUBLIC)!=0;
859  field.is_protected=(access_flags&ACC_PROTECTED)!=0;
860  field.is_private=(access_flags&ACC_PRIVATE)!=0;
861  const auto flags = (field.is_public ? 1 : 0) +
862  (field.is_protected?1:0)+
863  (field.is_private?1:0);
864  DATA_INVARIANT(flags<=1, "at most one of public, protected, private");
865 
866  for(std::size_t j=0; j<attributes_count; j++)
867  rfield_attribute(field);
868  }
869 }
870 
871 #define T_BOOLEAN 4
872 #define T_CHAR 5
873 #define T_FLOAT 6
874 #define T_DOUBLE 7
875 #define T_BYTE 8
876 #define T_SHORT 9
877 #define T_INT 10
878 #define T_LONG 11
879 
880 void java_bytecode_parsert::rbytecode(std::vector<instructiont> &instructions)
881 {
882  const u4 code_length = read<u4>();
883 
884  u4 address;
885  size_t bytecode_index=0; // index of bytecode instruction
886 
887  for(address=0; address<code_length; address++)
888  {
889  bool wide_instruction=false;
890  u4 start_of_instruction=address;
891 
892  u1 bytecode = read<u1>();
893 
894  if(bytecode == BC_wide)
895  {
896  wide_instruction=true;
897  address++;
898  bytecode = read<u1>();
899  // The only valid instructions following a wide byte are
900  // [ifald]load, [ifald]store, ret and iinc
901  // All of these have either format of v, or V
902  INVARIANT(
903  bytecode_info[bytecode].format == 'v' ||
904  bytecode_info[bytecode].format == 'V',
905  std::string("Unexpected wide instruction: ") +
906  bytecode_info[bytecode].mnemonic);
907  }
908 
909  instructions.emplace_back();
910  instructiont &instruction=instructions.back();
911  instruction.bytecode = bytecode;
912  instruction.address=start_of_instruction;
913  instruction.source_location
914  .set_java_bytecode_index(std::to_string(bytecode_index));
915 
916  switch(bytecode_info[bytecode].format)
917  {
918  case ' ': // no further bytes
919  break;
920 
921  case 'c': // a constant_pool index (one byte)
922  if(wide_instruction)
923  {
924  instruction.args.push_back(constant(read<u2>()));
925  address+=2;
926  }
927  else
928  {
929  instruction.args.push_back(constant(read<u1>()));
930  address+=1;
931  }
932  break;
933 
934  case 'C': // a constant_pool index (two bytes)
935  instruction.args.push_back(constant(read<u2>()));
936  address+=2;
937  break;
938 
939  case 'b': // a signed byte
940  {
941  const s1 c = read<u1>();
942  instruction.args.push_back(from_integer(c, signedbv_typet(8)));
943  }
944  address+=1;
945  break;
946 
947  case 'o': // two byte branch offset, signed
948  {
949  const s2 offset = read<u2>();
950  // By converting the signed offset into an absolute address (by adding
951  // the current address) the number represented becomes unsigned.
952  instruction.args.push_back(
953  from_integer(address+offset, unsignedbv_typet(16)));
954  }
955  address+=2;
956  break;
957 
958  case 'O': // four byte branch offset, signed
959  {
960  const s4 offset = read<u4>();
961  // By converting the signed offset into an absolute address (by adding
962  // the current address) the number represented becomes unsigned.
963  instruction.args.push_back(
964  from_integer(address+offset, unsignedbv_typet(32)));
965  }
966  address+=4;
967  break;
968 
969  case 'v': // local variable index (one byte)
970  {
971  if(wide_instruction)
972  {
973  const u2 v = read<u2>();
974  instruction.args.push_back(from_integer(v, unsignedbv_typet(16)));
975  address += 2;
976  }
977  else
978  {
979  const u1 v = read<u1>();
980  instruction.args.push_back(from_integer(v, unsignedbv_typet(8)));
981  address += 1;
982  }
983  }
984 
985  break;
986 
987  case 'V':
988  // local variable index (two bytes) plus two signed bytes
989  if(wide_instruction)
990  {
991  const u2 v = read<u2>();
992  instruction.args.push_back(from_integer(v, unsignedbv_typet(16)));
993  const s2 c = read<u2>();
994  instruction.args.push_back(from_integer(c, signedbv_typet(16)));
995  address+=4;
996  }
997  else // local variable index (one byte) plus one signed byte
998  {
999  const u1 v = read<u1>();
1000  instruction.args.push_back(from_integer(v, unsignedbv_typet(8)));
1001  const s1 c = read<u1>();
1002  instruction.args.push_back(from_integer(c, signedbv_typet(8)));
1003  address+=2;
1004  }
1005  break;
1006 
1007  case 'I': // two byte constant_pool index plus two bytes
1008  {
1009  const u2 c = read<u2>();
1010  instruction.args.push_back(constant(c));
1011  const u1 b1 = read<u1>();
1012  instruction.args.push_back(from_integer(b1, unsignedbv_typet(8)));
1013  const u1 b2 = read<u1>();
1014  instruction.args.push_back(from_integer(b2, unsignedbv_typet(8)));
1015  }
1016  address+=4;
1017  break;
1018 
1019  case 'L': // lookupswitch
1020  {
1021  u4 base_offset=address;
1022 
1023  // first a pad to 32-bit align
1024  while(((address + 1u) & 3u) != 0)
1025  {
1026  read<u1>();
1027  address++;
1028  }
1029 
1030  // now default value
1031  const s4 default_value = read<u4>();
1032  // By converting the signed offset into an absolute address (by adding
1033  // the current address) the number represented becomes unsigned.
1034  instruction.args.push_back(
1035  from_integer(base_offset+default_value, unsignedbv_typet(32)));
1036  address+=4;
1037 
1038  // number of pairs
1039  const u4 npairs = read<u4>();
1040  address+=4;
1041 
1042  for(std::size_t i=0; i<npairs; i++)
1043  {
1044  const s4 match = read<u4>();
1045  const s4 offset = read<u4>();
1046  instruction.args.push_back(
1047  from_integer(match, signedbv_typet(32)));
1048  // By converting the signed offset into an absolute address (by adding
1049  // the current address) the number represented becomes unsigned.
1050  instruction.args.push_back(
1051  from_integer(base_offset+offset, unsignedbv_typet(32)));
1052  address+=8;
1053  }
1054  }
1055  break;
1056 
1057  case 'T': // tableswitch
1058  {
1059  size_t base_offset=address;
1060 
1061  // first a pad to 32-bit align
1062  while(((address + 1u) & 3u) != 0)
1063  {
1064  read<u1>();
1065  address++;
1066  }
1067 
1068  // now default value
1069  const s4 default_value = read<u4>();
1070  instruction.args.push_back(
1071  from_integer(base_offset+default_value, signedbv_typet(32)));
1072  address+=4;
1073 
1074  // now low value
1075  const s4 low_value = read<u4>();
1076  address+=4;
1077 
1078  // now high value
1079  const s4 high_value = read<u4>();
1080  address+=4;
1081 
1082  // there are high-low+1 offsets, and they are signed
1083  for(s4 i=low_value; i<=high_value; i++)
1084  {
1085  s4 offset = read<u4>();
1086  instruction.args.push_back(from_integer(i, signedbv_typet(32)));
1087  // By converting the signed offset into an absolute address (by adding
1088  // the current address) the number represented becomes unsigned.
1089  instruction.args.push_back(
1090  from_integer(base_offset+offset, unsignedbv_typet(32)));
1091  address+=4;
1092  }
1093  }
1094  break;
1095 
1096  case 'm': // multianewarray: constant-pool index plus one unsigned byte
1097  {
1098  const u2 c = read<u2>(); // constant-pool index
1099  instruction.args.push_back(constant(c));
1100  const u1 dimensions = read<u1>(); // number of dimensions
1101  instruction.args.push_back(
1102  from_integer(dimensions, unsignedbv_typet(8)));
1103  address+=3;
1104  }
1105  break;
1106 
1107  case 't': // array subtype, one byte
1108  {
1109  typet t;
1110  switch(read<u1>())
1111  {
1112  case T_BOOLEAN: t.id(ID_bool); break;
1113  case T_CHAR: t.id(ID_char); break;
1114  case T_FLOAT: t.id(ID_float); break;
1115  case T_DOUBLE: t.id(ID_double); break;
1116  case T_BYTE: t.id(ID_byte); break;
1117  case T_SHORT: t.id(ID_short); break;
1118  case T_INT: t.id(ID_int); break;
1119  case T_LONG: t.id(ID_long); break;
1120  default:{};
1121  }
1122  instruction.args.push_back(type_exprt(t));
1123  }
1124  address+=1;
1125  break;
1126 
1127  case 's': // a signed short
1128  {
1129  const s2 s = read<u2>();
1130  instruction.args.push_back(from_integer(s, signedbv_typet(16)));
1131  }
1132  address+=2;
1133  break;
1134 
1135  default:
1136  throw "unknown JVM bytecode instruction";
1137  }
1138  bytecode_index++;
1139  }
1140 
1141  if(address!=code_length)
1142  {
1143  error() << "bytecode length mismatch" << eom;
1144  throw 0;
1145  }
1146 }
1147 
1149 {
1150  const u2 attribute_name_index = read<u2>();
1151  const u4 attribute_length = read<u4>();
1152 
1153  irep_idt attribute_name=pool_entry(attribute_name_index).s;
1154 
1155  if(attribute_name == "Code")
1156  {
1157  UNUSED_u2(max_stack);
1158  UNUSED_u2(max_locals);
1159 
1160  if(skip_instructions)
1161  skip_bytes(read<u4>());
1162  else
1163  rbytecode(method.instructions);
1164 
1165  const u2 exception_table_length = read<u2>();
1166  if(skip_instructions)
1167  skip_bytes(exception_table_length * 8u);
1168  else
1169  {
1170  method.exception_table.resize(exception_table_length);
1171 
1172  for(std::size_t e = 0; e < exception_table_length; e++)
1173  {
1174  const u2 start_pc = read<u2>();
1175  const u2 end_pc = read<u2>();
1176 
1177  // From the class file format spec ("4.7.3. The Code Attribute" for
1178  // Java8)
1179  INVARIANT(
1180  start_pc < end_pc,
1181  "The start_pc must be less than the end_pc as this is the range the "
1182  "exception is active");
1183 
1184  const u2 handler_pc = read<u2>();
1185  const u2 catch_type = read<u2>();
1186  method.exception_table[e].start_pc = start_pc;
1187  method.exception_table[e].end_pc = end_pc;
1188  method.exception_table[e].handler_pc = handler_pc;
1189  if(catch_type != 0)
1190  method.exception_table[e].catch_type =
1191  to_struct_tag_type(pool_entry(catch_type).expr.type());
1192  }
1193  }
1194 
1195  u2 attributes_count = read<u2>();
1196 
1197  for(std::size_t j=0; j<attributes_count; j++)
1198  rcode_attribute(method);
1199 
1200  // method name
1202  "java::" + id2string(parse_tree.parsed_class.name) + "." +
1203  id2string(method.name) + ":" + method.descriptor);
1204 
1205  irep_idt line_number;
1206 
1207  // add missing line numbers
1208  for(auto &instruction : method.instructions)
1209  {
1210  if(!instruction.source_location.get_line().empty())
1211  line_number = instruction.source_location.get_line();
1212  else if(!line_number.empty())
1213  instruction.source_location.set_line(line_number);
1214  instruction.source_location.set_function(
1215  method.source_location.get_function());
1216  }
1217 
1218  // line number of method (the first line number available)
1219  const auto it = std::find_if(
1220  method.instructions.begin(),
1221  method.instructions.end(),
1222  [&](const instructiont &instruction) {
1223  return !instruction.source_location.get_line().empty();
1224  });
1225  if(it != method.instructions.end())
1226  method.source_location.set_line(it->source_location.get_line());
1227  }
1228  else if(attribute_name=="Signature")
1229  {
1230  const u2 signature_index = read<u2>();
1231  method.signature=id2string(pool_entry(signature_index).s);
1232  }
1233  else if(attribute_name=="RuntimeInvisibleAnnotations" ||
1234  attribute_name=="RuntimeVisibleAnnotations")
1235  {
1237  }
1238  else if(
1239  attribute_name == "RuntimeInvisibleParameterAnnotations" ||
1240  attribute_name == "RuntimeVisibleParameterAnnotations")
1241  {
1242  const u1 parameter_count = read<u1>();
1243  // There may be attributes for both runtime-visible and runtime-invisible
1244  // annotations, the length of either array may be longer than the other as
1245  // trailing parameters without annotations are omitted.
1246  // Extend our parameter_annotations if this one is longer than the one
1247  // previously recorded (if any).
1248  if(method.parameter_annotations.size() < parameter_count)
1249  method.parameter_annotations.resize(parameter_count);
1250  for(u2 param_no = 0; param_no < parameter_count; ++param_no)
1252  }
1253  else if(attribute_name == "Exceptions")
1254  {
1256  }
1257  else
1258  skip_bytes(attribute_length);
1259 }
1260 
1262 {
1263  const u2 attribute_name_index = read<u2>();
1264  const u4 attribute_length = read<u4>();
1265 
1266  irep_idt attribute_name=pool_entry(attribute_name_index).s;
1267 
1268  if(attribute_name=="Signature")
1269  {
1270  const u2 signature_index = read<u2>();
1271  field.signature=id2string(pool_entry(signature_index).s);
1272  }
1273  else if(attribute_name=="RuntimeInvisibleAnnotations" ||
1274  attribute_name=="RuntimeVisibleAnnotations")
1275  {
1277  }
1278  else
1279  skip_bytes(attribute_length);
1280 }
1281 
1283 {
1284  const u2 attribute_name_index = read<u2>();
1285  const u4 attribute_length = read<u4>();
1286 
1287  irep_idt attribute_name=pool_entry(attribute_name_index).s;
1288 
1289  if(attribute_name=="LineNumberTable")
1290  {
1291  std::map<unsigned, std::reference_wrapper<instructiont>> instruction_map;
1292  for(auto &instruction : method.instructions)
1293  instruction_map.emplace(instruction.address, instruction);
1294 
1295  const u2 line_number_table_length = read<u2>();
1296 
1297  for(std::size_t i=0; i<line_number_table_length; i++)
1298  {
1299  const u2 start_pc = read<u2>();
1300  const u2 line_number = read<u2>();
1301 
1302  // annotate the bytecode program
1303  auto it = instruction_map.find(start_pc);
1304 
1305  if(it!=instruction_map.end())
1306  it->second.get().source_location.set_line(line_number);
1307  }
1308  }
1309  else if(attribute_name=="LocalVariableTable")
1310  {
1311  const u2 local_variable_table_length = read<u2>();
1312 
1313  method.local_variable_table.resize(local_variable_table_length);
1314 
1315  for(std::size_t i=0; i<local_variable_table_length; i++)
1316  {
1317  const u2 start_pc = read<u2>();
1318  const u2 length = read<u2>();
1319  const u2 name_index = read<u2>();
1320  const u2 descriptor_index = read<u2>();
1321  const u2 index = read<u2>();
1322 
1323  method.local_variable_table[i].index=index;
1324  method.local_variable_table[i].name=pool_entry(name_index).s;
1325  method.local_variable_table[i].descriptor=
1326  id2string(pool_entry(descriptor_index).s);
1327  method.local_variable_table[i].start_pc=start_pc;
1328  method.local_variable_table[i].length=length;
1329  }
1330  }
1331  else if(attribute_name=="LocalVariableTypeTable")
1332  {
1334  }
1335  else if(attribute_name=="StackMapTable")
1336  {
1337  const u2 stack_map_entries = read<u2>();
1338 
1339  method.stack_map_table.resize(stack_map_entries);
1340 
1341  for(size_t i=0; i<stack_map_entries; i++)
1342  {
1343  const u1 frame_type = read<u1>();
1344  if(frame_type<=63)
1345  {
1347  method.stack_map_table[i].locals.resize(0);
1348  method.stack_map_table[i].stack.resize(0);
1349  }
1350  else if(64<=frame_type && frame_type<=127)
1351  {
1352  method.stack_map_table[i].type=
1354  method.stack_map_table[i].locals.resize(0);
1355  method.stack_map_table[i].stack.resize(1);
1356  methodt::verification_type_infot verification_type_info;
1357  read_verification_type_info(verification_type_info);
1358  method.stack_map_table[i].stack[0]=verification_type_info;
1359  }
1360  else if(frame_type==247)
1361  {
1362  method.stack_map_table[i].type=
1364  method.stack_map_table[i].locals.resize(0);
1365  method.stack_map_table[i].stack.resize(1);
1366  methodt::verification_type_infot verification_type_info;
1367  const u2 offset_delta = read<u2>();
1368  read_verification_type_info(verification_type_info);
1369  method.stack_map_table[i].stack[0]=verification_type_info;
1370  method.stack_map_table[i].offset_delta=offset_delta;
1371  }
1372  else if(248<=frame_type && frame_type<=250)
1373  {
1375  method.stack_map_table[i].locals.resize(0);
1376  method.stack_map_table[i].stack.resize(0);
1377  const u2 offset_delta = read<u2>();
1378  method.stack_map_table[i].offset_delta=offset_delta;
1379  }
1380  else if(frame_type==251)
1381  {
1382  method.stack_map_table[i].type
1384  method.stack_map_table[i].locals.resize(0);
1385  method.stack_map_table[i].stack.resize(0);
1386  const u2 offset_delta = read<u2>();
1387  method.stack_map_table[i].offset_delta=offset_delta;
1388  }
1389  else if(252<=frame_type && frame_type<=254)
1390  {
1391  size_t new_locals = frame_type - 251;
1393  method.stack_map_table[i].locals.resize(new_locals);
1394  method.stack_map_table[i].stack.resize(0);
1395  const u2 offset_delta = read<u2>();
1396  method.stack_map_table[i].offset_delta=offset_delta;
1397  for(size_t k=0; k<new_locals; k++)
1398  {
1399  method.stack_map_table[i].locals
1400  .push_back(methodt::verification_type_infot());
1402  method.stack_map_table[i].locals.back();
1404  }
1405  }
1406  else if(frame_type==255)
1407  {
1409  const u2 offset_delta = read<u2>();
1410  method.stack_map_table[i].offset_delta=offset_delta;
1411  const u2 number_locals = read<u2>();
1412  method.stack_map_table[i].locals.resize(number_locals);
1413  for(size_t k=0; k<(size_t) number_locals; k++)
1414  {
1415  method.stack_map_table[i].locals
1416  .push_back(methodt::verification_type_infot());
1418  method.stack_map_table[i].locals.back();
1420  }
1421  const u2 number_stack_items = read<u2>();
1422  method.stack_map_table[i].stack.resize(number_stack_items);
1423  for(size_t k=0; k<(size_t) number_stack_items; k++)
1424  {
1425  method.stack_map_table[i].stack
1426  .push_back(methodt::verification_type_infot());
1428  method.stack_map_table[i].stack.back();
1430  }
1431  }
1432  else
1433  throw "error: unknown stack frame type encountered";
1434  }
1435  }
1436  else
1437  skip_bytes(attribute_length);
1438 }
1439 
1442 {
1443  const u1 tag = read<u1>();
1444  switch(tag)
1445  {
1446  case VTYPE_INFO_TOP:
1448  break;
1449  case VTYPE_INFO_INTEGER:
1451  break;
1452  case VTYPE_INFO_FLOAT:
1454  break;
1455  case VTYPE_INFO_LONG:
1457  break;
1458  case VTYPE_INFO_DOUBLE:
1460  break;
1461  case VTYPE_INFO_ITEM_NULL:
1463  break;
1466  break;
1467  case VTYPE_INFO_OBJECT:
1469  v.cpool_index = read<u2>();
1470  break;
1471  case VTYPE_INFO_UNINIT:
1473  v.offset = read<u2>();
1474  break;
1475  default:
1476  throw "error: unknown verification type info encountered";
1477  }
1478 }
1479 
1481  std::vector<annotationt> &annotations)
1482 {
1483  const u2 num_annotations = read<u2>();
1484 
1485  for(u2 number=0; number<num_annotations; number++)
1486  {
1487  annotationt annotation;
1488  rRuntimeAnnotation(annotation);
1489  annotations.push_back(annotation);
1490  }
1491 }
1492 
1494  annotationt &annotation)
1495 {
1496  const u2 type_index = read<u2>();
1497  annotation.type=type_entry(type_index);
1499 }
1500 
1502  annotationt::element_value_pairst &element_value_pairs)
1503 {
1504  const u2 num_element_value_pairs = read<u2>();
1505  element_value_pairs.resize(num_element_value_pairs);
1506 
1507  for(auto &element_value_pair : element_value_pairs)
1508  {
1509  const u2 element_name_index = read<u2>();
1510  element_value_pair.element_name=pool_entry(element_name_index).s;
1511  element_value_pair.value = get_relement_value();
1512  }
1513 }
1514 
1522 {
1523  const u1 tag = read<u1>();
1524 
1525  switch(tag)
1526  {
1527  case 'e':
1528  {
1529  UNUSED_u2(type_name_index);
1530  UNUSED_u2(const_name_index);
1531  // todo: enum
1532  return exprt();
1533  }
1534 
1535  case 'c':
1536  {
1537  const u2 class_info_index = read<u2>();
1538  return symbol_exprt::typeless(pool_entry(class_info_index).s);
1539  }
1540 
1541  case '@':
1542  {
1543  // TODO: return this wrapped in an exprt
1544  // another annotation, recursively
1545  annotationt annotation;
1546  rRuntimeAnnotation(annotation);
1547  return exprt();
1548  }
1549 
1550  case '[':
1551  {
1552  const u2 num_values = read<u2>();
1553  exprt::operandst values;
1554  values.reserve(num_values);
1555  for(std::size_t i=0; i<num_values; i++)
1556  {
1557  values.push_back(get_relement_value());
1558  }
1559  return array_exprt(std::move(values), array_typet(typet(), exprt()));
1560  }
1561 
1562  case 's':
1563  {
1564  const u2 const_value_index = read<u2>();
1565  return string_constantt(pool_entry(const_value_index).s);
1566  }
1567 
1568  default:
1569  {
1570  const u2 const_value_index = read<u2>();
1571  return constant(const_value_index);
1572  }
1573  }
1574 }
1575 
1588  const u4 &attribute_length)
1589 {
1590  classt &parsed_class = parse_tree.parsed_class;
1591  std::string name = parsed_class.name.c_str();
1592  const u2 number_of_classes = read<u2>();
1593  const u4 number_of_bytes_to_be_read = number_of_classes * 8 + 2;
1594  INVARIANT(
1595  number_of_bytes_to_be_read == attribute_length,
1596  "The number of bytes to be read for the InnerClasses attribute does not "
1597  "match the attribute length.");
1598 
1599  const auto pool_entry_lambda = [this](u2 index) -> pool_entryt & {
1600  return pool_entry(index);
1601  };
1602  const auto remove_separator_char = [](std::string str, char ch) {
1603  str.erase(std::remove(str.begin(), str.end(), ch), str.end());
1604  return str;
1605  };
1606 
1607  for(int i = 0; i < number_of_classes; i++)
1608  {
1609  const u2 inner_class_info_index = read<u2>();
1610  const u2 outer_class_info_index = read<u2>();
1611  const u2 inner_name_index = read<u2>();
1612  const u2 inner_class_access_flags = read<u2>();
1613 
1614  std::string inner_class_info_name =
1615  class_infot(pool_entry(inner_class_info_index))
1616  .get_name(pool_entry_lambda);
1617  bool is_private = (inner_class_access_flags & ACC_PRIVATE) != 0;
1618  bool is_public = (inner_class_access_flags & ACC_PUBLIC) != 0;
1619  bool is_protected = (inner_class_access_flags & ACC_PROTECTED) != 0;
1620  bool is_static = (inner_class_access_flags & ACC_STATIC) != 0;
1621 
1622  // If the original parsed class name matches the inner class name,
1623  // the parsed class is an inner class, so overwrite the parsed class'
1624  // access information and mark it as an inner class.
1625  bool is_inner_class = remove_separator_char(id2string(parsed_class.name), '.') ==
1626  remove_separator_char(inner_class_info_name, '/');
1627  if(!is_inner_class)
1628  continue;
1629  parsed_class.is_inner_class = is_inner_class;
1630  parsed_class.is_static_class = is_static;
1631  // This is a marker that a class is anonymous.
1632  if(inner_name_index == 0)
1633  parsed_class.is_anonymous_class = true;
1634  else
1635  parsed_class.inner_name = pool_entry_lambda(inner_name_index).s;
1636  // Note that if outer_class_info_index == 0, the inner class is an anonymous
1637  // or local class, and is treated as private.
1638  if(outer_class_info_index == 0)
1639  {
1640  parsed_class.is_private = true;
1641  parsed_class.is_protected = false;
1642  parsed_class.is_public = false;
1643  }
1644  else
1645  {
1646  std::string outer_class_info_name =
1647  class_infot(pool_entry(outer_class_info_index))
1648  .get_name(pool_entry_lambda);
1649  parsed_class.outer_class =
1650  constant(outer_class_info_index).type().get(ID_C_base_name);
1651  parsed_class.is_private = is_private;
1652  parsed_class.is_protected = is_protected;
1653  parsed_class.is_public = is_public;
1654  }
1655  }
1656 }
1657 
1664 {
1665  const u2 number_of_exceptions = read<u2>();
1666 
1667  std::vector<irep_idt> exceptions;
1668  for(size_t i = 0; i < number_of_exceptions; i++)
1669  {
1670  const u2 exception_index_table = read<u2>();
1671  const irep_idt exception_name =
1672  constant(exception_index_table).type().get(ID_C_base_name);
1673  exceptions.push_back(exception_name);
1674  }
1675  return exceptions;
1676 }
1677 
1679 {
1680  classt &parsed_class = parse_tree.parsed_class;
1681 
1682  const u2 attribute_name_index = read<u2>();
1683  const u4 attribute_length = read<u4>();
1684 
1685  irep_idt attribute_name=pool_entry(attribute_name_index).s;
1686 
1687  if(attribute_name=="SourceFile")
1688  {
1689  const u2 sourcefile_index = read<u2>();
1690  irep_idt sourcefile_name;
1691 
1692  const std::string &fqn(id2string(parsed_class.name));
1693  size_t last_index = fqn.find_last_of('.');
1694  if(last_index==std::string::npos)
1695  sourcefile_name=pool_entry(sourcefile_index).s;
1696  else
1697  {
1698  std::string package_name=fqn.substr(0, last_index+1);
1699  std::replace(package_name.begin(), package_name.end(), '.', '/');
1700  const std::string &full_file_name=
1701  package_name+id2string(pool_entry(sourcefile_index).s);
1702  sourcefile_name=full_file_name;
1703  }
1704 
1705  for(auto &method : parsed_class.methods)
1706  {
1707  method.source_location.set_file(sourcefile_name);
1708  for(auto &instruction : method.instructions)
1709  {
1710  if(!instruction.source_location.get_line().empty())
1711  instruction.source_location.set_file(sourcefile_name);
1712  }
1713  }
1714  }
1715  else if(attribute_name=="Signature")
1716  {
1717  const u2 signature_index = read<u2>();
1718  parsed_class.signature=id2string(pool_entry(signature_index).s);
1720  parsed_class.signature.value(),
1722  }
1723  else if(attribute_name=="RuntimeInvisibleAnnotations" ||
1724  attribute_name=="RuntimeVisibleAnnotations")
1725  {
1727  }
1728  else if(attribute_name == "BootstrapMethods")
1729  {
1730  // for this attribute
1731  // cf. https://docs.oracle.com/javase/specs/jvms/se8/html/jvms-4.html#jvms-4.7.23
1732  INVARIANT(
1733  !parsed_class.attribute_bootstrapmethods_read,
1734  "only one BootstrapMethods argument is allowed in a class file");
1735 
1736  // mark as read in parsed class
1737  parsed_class.attribute_bootstrapmethods_read = true;
1739  }
1740  else if(attribute_name == "InnerClasses")
1741  {
1743  }
1744  else
1745  skip_bytes(attribute_length);
1746 }
1747 
1749 {
1750  const u2 methods_count = read<u2>();
1751 
1752  for(std::size_t j=0; j<methods_count; j++)
1753  rmethod();
1754 }
1755 
1756 #define ACC_PUBLIC 0x0001u
1757 #define ACC_PRIVATE 0x0002u
1758 #define ACC_PROTECTED 0x0004u
1759 #define ACC_STATIC 0x0008u
1760 #define ACC_FINAL 0x0010u
1761 #define ACC_VARARGS 0x0080u
1762 #define ACC_SUPER 0x0020u
1763 #define ACC_VOLATILE 0x0040u
1764 #define ACC_TRANSIENT 0x0080u
1765 #define ACC_INTERFACE 0x0200u
1766 #define ACC_ABSTRACT 0x0400u
1767 #define ACC_SYNTHETIC 0x1000u
1768 #define ACC_ANNOTATION 0x2000u
1769 #define ACC_ENUM 0x4000u
1772 {
1774 
1775  const u2 access_flags = read<u2>();
1776  const u2 name_index = read<u2>();
1777  const u2 descriptor_index = read<u2>();
1778 
1779  method.is_final=(access_flags&ACC_FINAL)!=0;
1780  method.is_static=(access_flags&ACC_STATIC)!=0;
1781  method.is_abstract=(access_flags&ACC_ABSTRACT)!=0;
1782  method.is_public=(access_flags&ACC_PUBLIC)!=0;
1783  method.is_protected=(access_flags&ACC_PROTECTED)!=0;
1784  method.is_private=(access_flags&ACC_PRIVATE)!=0;
1785  method.is_synchronized=(access_flags&ACC_SYNCHRONIZED)!=0;
1786  method.is_native=(access_flags&ACC_NATIVE)!=0;
1787  method.is_bridge = (access_flags & ACC_BRIDGE) != 0;
1788  method.is_varargs = (access_flags & ACC_VARARGS) != 0;
1789  method.is_synthetic = (access_flags & ACC_SYNTHETIC) != 0;
1790  method.name=pool_entry(name_index).s;
1791  method.base_name=pool_entry(name_index).s;
1792  method.descriptor=id2string(pool_entry(descriptor_index).s);
1793 
1794  const auto flags = (method.is_public ? 1 : 0) +
1795  (method.is_protected?1:0)+
1796  (method.is_private?1:0);
1797  DATA_INVARIANT(flags<=1, "at most one of public, protected, private");
1798  const u2 attributes_count = read<u2>();
1799 
1800  for(std::size_t j=0; j<attributes_count; j++)
1801  rmethod_attribute(method);
1802 }
1803 
1805  std::istream &istream,
1806  const irep_idt &class_name,
1807  message_handlert &message_handler,
1808  bool skip_instructions)
1809 {
1810  java_bytecode_parsert java_bytecode_parser(skip_instructions);
1811  java_bytecode_parser.in=&istream;
1812  java_bytecode_parser.set_message_handler(message_handler);
1813 
1814  bool parser_result=java_bytecode_parser.parse();
1815 
1816  if(
1817  parser_result ||
1818  java_bytecode_parser.parse_tree.parsed_class.name != class_name)
1819  {
1820  return {};
1821  }
1822 
1823  return std::move(java_bytecode_parser.parse_tree);
1824 }
1825 
1827  const std::string &file,
1828  const irep_idt &class_name,
1829  message_handlert &message_handler,
1830  bool skip_instructions)
1831 {
1832  std::ifstream in(file, std::ios::binary);
1833 
1834  if(!in)
1835  {
1836  return {};
1837  }
1838 
1839  return java_bytecode_parse(
1840  in, class_name, message_handler, skip_instructions);
1841 }
1842 
1847 {
1848  const u2 local_variable_type_table_length = read<u2>();
1849 
1850  INVARIANT(
1851  local_variable_type_table_length<=method.local_variable_table.size(),
1852  "Local variable type table cannot have more elements "
1853  "than the local variable table.");
1854  for(std::size_t i=0; i<local_variable_type_table_length; i++)
1855  {
1856  const u2 start_pc = read<u2>();
1857  const u2 length = read<u2>();
1858  const u2 name_index = read<u2>();
1859  const u2 signature_index = read<u2>();
1860  const u2 index = read<u2>();
1861 
1862  bool found=false;
1863  for(auto &lvar : method.local_variable_table)
1864  {
1865  // compare to entry in LVT
1866  if(lvar.index==index &&
1867  lvar.name==pool_entry(name_index).s &&
1868  lvar.start_pc==start_pc &&
1869  lvar.length==length)
1870  {
1871  found=true;
1872  lvar.signature=id2string(pool_entry(signature_index).s);
1873  break;
1874  }
1875  }
1876  INVARIANT(
1877  found,
1878  "Entry in LocalVariableTypeTable must be present in LVT");
1879  }
1880 }
1881 
1889 {
1890  const std::function<pool_entryt &(u2)> pool_entry_lambda =
1891  [this](u2 index) -> pool_entryt & { return pool_entry(index); };
1892 
1893  const base_ref_infot &ref_entry = entry.get_reference(pool_entry_lambda);
1894 
1895  const class_infot &class_entry = ref_entry.get_class(pool_entry_lambda);
1896  const name_and_type_infot &name_and_type =
1897  ref_entry.get_name_and_type(pool_entry_lambda);
1898 
1899  std::string class_name = class_entry.get_name(pool_entry_lambda);
1900  // replace '.' for '$' (inner classes)
1901  std::replace(class_name.begin(), class_name.end(), '.', '$');
1902  // replace '/' for '.' (package)
1903  std::replace(class_name.begin(), class_name.end(), '/', '.');
1904  const std::string method_ref =
1905  class_name + "." + name_and_type.get_name(pool_entry_lambda) + ':' +
1906  name_and_type.get_descriptor(pool_entry_lambda);
1907 
1908  lambda_method_handlet lambda_method_handle;
1909 
1910  if(has_prefix(name_and_type.get_name(pool_entry_lambda), "lambda$"))
1911  {
1912  // names seem to be lambda$POSTFIX$NUM
1913  // where POSTFIX is FUN for a function name in which the lambda is define
1914  // "static" when it is a static member of the class
1915  // "new" when it is a class variable, instantiated in <init>
1916  lambda_method_handle.lambda_method_name =
1917  name_and_type.get_name(pool_entry_lambda);
1918  lambda_method_handle.lambda_method_ref = method_ref;
1919  lambda_method_handle.handle_type =
1921 
1922  return lambda_method_handle;
1923  }
1924 
1925  return {};
1926 }
1927 
1930 {
1931  const u2 num_bootstrap_methods = read<u2>();
1932  for(size_t bootstrap_method_index = 0;
1933  bootstrap_method_index < num_bootstrap_methods;
1934  ++bootstrap_method_index)
1935  {
1936  const u2 bootstrap_methodhandle_ref = read<u2>();
1937  const pool_entryt &entry = pool_entry(bootstrap_methodhandle_ref);
1938 
1939  method_handle_infot method_handle{entry};
1940 
1941  const u2 num_bootstrap_arguments = read<u2>();
1942  debug() << "INFO: parse BootstrapMethod handle " << num_bootstrap_arguments
1943  << " #args" << eom;
1944 
1945  // read u2 values of entry into vector
1946  std::vector<u2> u2_values(num_bootstrap_arguments);
1947  for(size_t i = 0; i < num_bootstrap_arguments; i++)
1948  u2_values[i] = read<u2>();
1949 
1950  // try parsing bootstrap method handle
1951  // each entry contains a MethodHandle structure
1952  // u2 tag
1953  // u2 reference kind which must be in the range from 1 to 9
1954  // u2 reference index into the constant pool
1955  //
1956  // reference kinds use the following
1957  // 1 to 4 must point to a CONSTANT_Fieldref structure
1958  // 5 or 8 must point to a CONSTANT_Methodref structure
1959  // 6 or 7 must point to a CONSTANT_Methodref or
1960  // CONSTANT_InterfaceMethodref structure, if the class file version
1961  // number is 52.0 or above, to a CONSTANT_Methodref only in the case
1962  // of less than 52.0
1963  // 9 must point to a CONSTANT_InterfaceMethodref structure
1964 
1965  // the index must point to a CONSTANT_String
1966  // CONSTANT_Class
1967  // CONSTANT_Integer
1968  // CONSTANT_Long
1969  // CONSTANT_Float
1970  // CONSTANT_Double
1971  // CONSTANT_MethodHandle
1972  // CONSTANT_MethodType
1973 
1974  // We read the three arguments here to see whether they correspond to
1975  // our hypotheses for this being a lambda function entry.
1976 
1977  // Need at least 3 arguments, the interface type, the method hanlde
1978  // and the method_type, otherwise it doesn't look like a call that we
1979  // understand
1980  if(num_bootstrap_arguments < 3)
1981  {
1982  store_unknown_method_handle(bootstrap_method_index, std::move(u2_values));
1983  debug()
1984  << "format of BootstrapMethods entry not recognized: too few arguments"
1985  << eom;
1986  continue;
1987  }
1988 
1989  u2 interface_type_index = u2_values[0];
1990  u2 method_handle_index = u2_values[1];
1991  u2 method_type_index = u2_values[2];
1992 
1993  // The additional arguments for the altmetafactory call are skipped,
1994  // as they are currently not used. We verify though that they are of
1995  // CONSTANT_Integer type, cases where this does not hold will be
1996  // analyzed further.
1997  bool recognized = true;
1998  for(size_t i = 3; i < num_bootstrap_arguments; i++)
1999  {
2000  u2 skipped_argument = u2_values[i];
2001  recognized &= pool_entry(skipped_argument).tag == CONSTANT_Integer;
2002  }
2003 
2004  if(!recognized)
2005  {
2006  debug() << "format of BootstrapMethods entry not recognized: extra "
2007  "arguments of wrong type"
2008  << eom;
2009  store_unknown_method_handle(bootstrap_method_index, std::move(u2_values));
2010  continue;
2011  }
2012 
2013  const pool_entryt &interface_type_argument =
2014  pool_entry(interface_type_index);
2015  const pool_entryt &method_handle_argument = pool_entry(method_handle_index);
2016  const pool_entryt &method_type_argument = pool_entry(method_type_index);
2017 
2018  if(
2019  interface_type_argument.tag != CONSTANT_MethodType ||
2020  method_handle_argument.tag != CONSTANT_MethodHandle ||
2021  method_type_argument.tag != CONSTANT_MethodType)
2022  {
2023  debug() << "format of BootstrapMethods entry not recognized: arguments "
2024  "wrong type"
2025  << eom;
2026  store_unknown_method_handle(bootstrap_method_index, std::move(u2_values));
2027  continue;
2028  }
2029 
2030  debug() << "INFO: parse lambda handle" << eom;
2031  optionalt<lambda_method_handlet> lambda_method_handle =
2032  parse_method_handle(method_handle_infot{method_handle_argument});
2033 
2034  if(!lambda_method_handle.has_value())
2035  {
2036  debug() << "format of BootstrapMethods entry not recognized: method "
2037  "handle not recognised"
2038  << eom;
2039  store_unknown_method_handle(bootstrap_method_index, std::move(u2_values));
2040  continue;
2041  }
2042 
2043  // If parse_method_handle can't parse the lambda method, it should return {}
2044  POSTCONDITION(
2045  lambda_method_handle->handle_type != method_handle_typet::UNKNOWN_HANDLE);
2046 
2047  lambda_method_handle->interface_type =
2048  pool_entry(interface_type_argument.ref1).s;
2049  lambda_method_handle->method_type = pool_entry(method_type_argument.ref1).s;
2050  lambda_method_handle->u2_values = std::move(u2_values);
2051  debug() << "lambda function reference "
2052  << id2string(lambda_method_handle->lambda_method_name)
2053  << " in class \"" << parse_tree.parsed_class.name << "\""
2054  << "\n interface type is "
2055  << id2string(pool_entry(interface_type_argument.ref1).s)
2056  << "\n method type is "
2057  << id2string(pool_entry(method_type_argument.ref1).s) << eom;
2059  bootstrap_method_index, *lambda_method_handle);
2060  }
2061 }
2062 
2068  size_t bootstrap_method_index,
2069  std::vector<u2> u2_values)
2070 {
2071  const lambda_method_handlet lambda_method_handle(std::move(u2_values));
2073  bootstrap_method_index, lambda_method_handle);
2074 }
ACC_NATIVE
#define ACC_NATIVE
Definition: java_bytecode_parser.cpp:413
CONSTANT_InterfaceMethodref
#define CONSTANT_InterfaceMethodref
Definition: java_bytecode_parser.cpp:158
tag_typet::get_identifier
const irep_idt & get_identifier() const
Definition: std_types.h:451
java_bytecode_parse_treet::classt::implements
implementst implements
Definition: java_bytecode_parse_tree.h:270
java_bytecode_parse_treet::loading_successful
bool loading_successful
Definition: java_bytecode_parse_tree.h:313
java_bytecode_parsert::get_relement_value
exprt get_relement_value()
Corresponds to the element_value structure Described in Java 8 specification 4.7.16....
Definition: java_bytecode_parser.cpp:1521
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:142
java_bytecode_parse_treet::instructiont::args
argst args
Definition: java_bytecode_parse_tree.h:61
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
java_bytecode_parse_treet::methodt::throws_exception_table
std::vector< irep_idt > throws_exception_table
Definition: java_bytecode_parse_tree.h:124
get_dependencies_from_generic_parameters
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.
Definition: java_types.cpp:989
java_bytecode_parse_treet::membert::signature
optionalt< std::string > signature
Definition: java_bytecode_parse_tree.h:67
source_locationt::get_function
const irep_idt & get_function() const
Definition: source_location.h:56
class_infot::get_name
std::string get_name(const pool_entry_lookupt &pool_entry) const
Definition: java_bytecode_parser.cpp:218
format
static format_containert< T > format(const T &o)
Definition: format.h:35
method_handle_infot::method_handle_kindt::REF_getField
@ REF_getField
dstringt::c_str
const char * c_str() const
Definition: dstring.h:99
java_bytecode_parsert::pool_entry
pool_entryt & pool_entry(u2 index)
Definition: java_bytecode_parser.cpp:68
java_bytecode_parse_treet::classt::add_method_handle
void add_method_handle(size_t bootstrap_index, const lambda_method_handlet &handle)
Definition: java_bytecode_parse_tree.h:290
ACC_VARARGS
#define ACC_VARARGS
Definition: java_bytecode_parser.cpp:1761
typet::subtype
const typet & subtype() const
Definition: type.h:47
java_bytecode_parse_treet::methodt::verification_type_infot::ITEM_NULL
@ ITEM_NULL
Definition: java_bytecode_parse_tree.h:142
method_handle_infot::method_handle_kindt::REF_invokeStatic
@ REF_invokeStatic
java_bytecode_parse_treet::membert::is_final
bool is_final
Definition: java_bytecode_parse_tree.h:69
java_bytecode_parse_treet::annotationt::element_value_pairs
element_value_pairst element_value_pairs
Definition: java_bytecode_parse_tree.h:44
java_bytecode_parsert::rexceptions_attribute
std::vector< irep_idt > rexceptions_attribute()
Corresponds to the element_value structure Described in Java 8 specification 4.7.5 https://docs....
Definition: java_bytecode_parser.cpp:1663
ACC_PROTECTED
#define ACC_PROTECTED
Definition: java_bytecode_parser.cpp:1758
java_bytecode_parsert::pool_entryt
Definition: java_bytecode_parser.cpp:40
java_bytecode_parse_treet::classt::is_annotation
bool is_annotation
Definition: java_bytecode_parse_tree.h:219
structured_pool_entryt::get_tag
u1 get_tag() const
Definition: java_bytecode_parser.cpp:190
arith_tools.h
java_bytecode_parsert::read_bootstrapmethods_entry
void read_bootstrapmethods_entry()
Read all entries of the BootstrapMethods attribute of a class file.
Definition: java_bytecode_parser.cpp:1929
source_locationt::set_function
void set_function(const irep_idt &function)
Definition: source_location.h:126
structured_pool_entryt::tag
u1 tag
Definition: java_bytecode_parser.cpp:204
java_bytecode_parse_treet::methodt::is_abstract
bool is_abstract
Definition: java_bytecode_parse_tree.h:87
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
java_bytecode_parse_treet::membert::annotations
annotationst annotations
Definition: java_bytecode_parse_tree.h:70
java_bytecode_parsert::rfield_attribute
void rfield_attribute(fieldt &)
Definition: java_bytecode_parser.cpp:1261
method_handle_infot::method_handle_kindt::REF_getStatic
@ REF_getStatic
base_ref_infot::get_class
class_infot get_class(const pool_entry_lookupt &pool_entry) const
Definition: java_bytecode_parser.cpp:293
java_bytecode_parse_treet
Definition: java_bytecode_parse_tree.h:23
java_bytecode_parse_treet::methodt::verification_type_infot::TOP
@ TOP
Definition: java_bytecode_parse_tree.h:141
java_bytecode_parse_treet::methodt::verification_type_infot::OBJECT
@ OBJECT
Definition: java_bytecode_parse_tree.h:143
T_FLOAT
#define T_FLOAT
Definition: java_bytecode_parser.cpp:873
CONSTANT_InvokeDynamic
#define CONSTANT_InvokeDynamic
Definition: java_bytecode_parser.cpp:168
VTYPE_INFO_DOUBLE
#define VTYPE_INFO_DOUBLE
Definition: java_bytecode_parser.cpp:174
ACC_ABSTRACT
#define ACC_ABSTRACT
Definition: java_bytecode_parser.cpp:1766
method_handle_infot::method_handle_kindt::REF_invokeSpecial
@ REF_invokeSpecial
typet
The type of an expression, extends irept.
Definition: type.h:29
u2
uint16_t u2
Definition: bytecode_info.h:56
java_bytecode_parse_treet::methodt
Definition: java_bytecode_parse_tree.h:85
java_bytecode_parsert::parse_tree
java_bytecode_parse_treet parse_tree
Definition: java_bytecode_parser.cpp:49
base_ref_infot::get_name_and_type
name_and_type_infot get_name_and_type(const pool_entry_lookupt &pool_entry) const
Definition: java_bytecode_parser.cpp:281
u8
uint64_t u8
Definition: bytecode_info.h:58
java_bytecode_parse
optionalt< 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.
Definition: java_bytecode_parser.cpp:1804
java_bytecode_parsert::methodt
java_bytecode_parse_treet::methodt methodt
Definition: java_bytecode_parser.cpp:53
optional.h
java_array_element_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.
Definition: java_types.cpp:145
java_bytecode_parse_treet::methodt::stack_map_table_entryt::CHOP
@ CHOP
Definition: java_bytecode_parse_tree.h:155
java_bytecode_parse_treet::methodt::local_variable_table
local_variable_tablet local_variable_table
Definition: java_bytecode_parse_tree.h:137
java_bytecode_parsert::pool_entryt::number
u8 number
Definition: java_bytecode_parser.cpp:45
name_and_type_infot::name_and_type_infot
name_and_type_infot(const pool_entryt &entry)
Definition: java_bytecode_parser.cpp:233
java_bytecode_parsert::rClassFile
void rClassFile()
Definition: java_bytecode_parser.cpp:428
symbol_exprt::typeless
static symbol_exprt typeless(const irep_idt &id)
Generate a symbol_exprt without a proper type.
Definition: std_expr.h:101
base_ref_infot
Definition: java_bytecode_parser.cpp:259
CONSTANT_Methodref
#define CONSTANT_Methodref
Definition: java_bytecode_parser.cpp:157
java_bytecode_parse_treet::instructiont::bytecode
u8 bytecode
Definition: java_bytecode_parse_tree.h:59
java_bytecode_parse_treet::classt::is_synthetic
bool is_synthetic
Definition: java_bytecode_parse_tree.h:218
prefix.h
replace
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
Definition: string_constraint.cpp:67
file
Definition: kdev_t.h:19
java_bytecode_parse_treet::classt::lambda_method_handlet::lambda_method_name
irep_idt lambda_method_name
Definition: java_bytecode_parse_tree.h:237
java_string_literal_expr.h
method_handle_infot::reference_kind
method_handle_kindt reference_kind
Definition: java_bytecode_parser.cpp:374
java_bytecode_parse_treet::methodt::verification_type_infot::UNINITIALIZED
@ UNINITIALIZED
Definition: java_bytecode_parse_tree.h:143
s1
int8_t s1
Definition: bytecode_info.h:59
java_bytecode_parse_treet::instructiont
Definition: java_bytecode_parse_tree.h:56
source_locationt::set_java_bytecode_index
void set_java_bytecode_index(const irep_idt &index)
Definition: source_location.h:152
java_bytecode_parse_treet::instructiont::address
unsigned address
Definition: java_bytecode_parse_tree.h:58
java_bytecode_parse_treet::classt::attribute_bootstrapmethods_read
bool attribute_bootstrapmethods_read
Definition: java_bytecode_parse_tree.h:223
java_bytecode_parsert::rfields
void rfields()
Definition: java_bytecode_parser.cpp:839
string_constant.h
java_bytecode_parsert::skip_instructions
const bool skip_instructions
Definition: java_bytecode_parser.cpp:66
base_ref_infot::get_name_and_type_index
u2 get_name_and_type_index() const
Definition: java_bytecode_parser.cpp:275
exprt
Base class for all expressions.
Definition: expr.h:53
java_bytecode_parse_treet::methodt::verification_type_infot::INTEGER
@ INTEGER
Definition: java_bytecode_parse_tree.h:141
java_bytecode_parsert::fieldt
java_bytecode_parse_treet::fieldt fieldt
Definition: java_bytecode_parser.cpp:54
is_java_array_tag
bool is_java_array_tag(const irep_idt &tag)
See above.
Definition: java_types.cpp:232
java_bytecode_parsert::relement_value_pairs
void relement_value_pairs(annotationt::element_value_pairst &)
Definition: java_bytecode_parser.cpp:1501
struct_tag_typet
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:490
java_bytecode_parse_treet::classt::is_final
bool is_final
Definition: java_bytecode_parse_tree.h:216
java_bytecode_parsert::pool_entryt::s
irep_idt s
Definition: java_bytecode_parser.cpp:44
java_bytecode_parse_treet::classt::is_inner_class
bool is_inner_class
Definition: java_bytecode_parse_tree.h:220
VTYPE_INFO_LONG
#define VTYPE_INFO_LONG
Definition: java_bytecode_parser.cpp:173
CONSTANT_MethodHandle
#define CONSTANT_MethodHandle
Definition: java_bytecode_parser.cpp:166
CONSTANT_Integer
#define CONSTANT_Integer
Definition: java_bytecode_parser.cpp:160
java_bytecode_parsert::java_bytecode_parsert
java_bytecode_parsert(bool skip_instructions)
Definition: java_bytecode_parser.cpp:32
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
ACC_BRIDGE
#define ACC_BRIDGE
Definition: java_bytecode_parser.cpp:412
class_infot::name_index
u2 name_index
Definition: java_bytecode_parser.cpp:225
messaget::eom
static eomt eom
Definition: message.h:283
base_ref_infot::class_index
u2 class_index
Definition: java_bytecode_parser.cpp:301
CONSTANT_Fieldref
#define CONSTANT_Fieldref
Definition: java_bytecode_parser.cpp:156
CONSTANT_Long
#define CONSTANT_Long
Definition: java_bytecode_parser.cpp:162
java_bytecode_parse_treet::methodt::parameter_annotations
std::vector< annotationst > parameter_annotations
Java annotations that were applied to parameters of this method.
Definition: java_bytecode_parse_tree.h:106
base_ref_infot::name_and_type_index
u2 name_and_type_index
Definition: java_bytecode_parser.cpp:302
string_constantt
Definition: string_constant.h:16
java_bytecode_parsert::constant
exprt & constant(u2 index)
Definition: java_bytecode_parser.cpp:80
ACC_FINAL
#define ACC_FINAL
Definition: java_bytecode_parser.cpp:1760
java_bytecode_parse_treet::methodt::stack_map_table_entryt::SAME
@ SAME
Definition: java_bytecode_parse_tree.h:154
CONSTANT_Class
#define CONSTANT_Class
Definition: java_bytecode_parser.cpp:155
method_handle_infot::method_handle_kindt
method_handle_kindt
Correspond to the different valid values for field reference_kind From Java 8 spec 4....
Definition: java_bytecode_parser.cpp:312
unsignedbv_typet
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1216
java_bytecode_parse_treet::classt::lambda_method_handlet
Definition: java_bytecode_parse_tree.h:235
method_handle_infot::method_handle_infot
method_handle_infot(const pool_entryt &entry)
Definition: java_bytecode_parser.cpp:324
java_bytecode_parse_treet::annotationt::element_value_pairst
std::vector< element_value_pairt > element_value_pairst
Definition: java_bytecode_parse_tree.h:43
VTYPE_INFO_UNINIT
#define VTYPE_INFO_UNINIT
Definition: java_bytecode_parser.cpp:178
java_type_from_string_with_exception
optionalt< typet > java_type_from_string_with_exception(const std::string &descriptor, const optionalt< std::string > &signature, const std::string &class_name)
Definition: java_types.h:1084
java_bytecode_parse_treet::methodt::verification_type_infot::FLOAT
@ FLOAT
Definition: java_bytecode_parse_tree.h:141
ACC_PRIVATE
#define ACC_PRIVATE
Definition: java_bytecode_parser.cpp:1757
java_bytecode_parse_treet::classt::annotations
annotationst annotations
Definition: java_bytecode_parse_tree.h:276
ACC_SYNTHETIC
#define ACC_SYNTHETIC
Definition: java_bytecode_parser.cpp:1767
java_bytecode_parse_treet::membert::descriptor
std::string descriptor
Definition: java_bytecode_parse_tree.h:66
java_bytecode_parse_treet::instructiont::source_location
source_locationt source_location
Definition: java_bytecode_parse_tree.h:57
ACC_SYNCHRONIZED
#define ACC_SYNCHRONIZED
Definition: java_bytecode_parser.cpp:411
java_bytecode_parse_treet::methodt::verification_type_infot::DOUBLE
@ DOUBLE
Definition: java_bytecode_parse_tree.h:141
java_bytecode_parse_treet::classt::is_public
bool is_public
Definition: java_bytecode_parse_tree.h:215
source_locationt::set_line
void set_line(const irep_idt &line)
Definition: source_location.h:106
method_handle_infot::get_reference
base_ref_infot get_reference(const pool_entry_lookupt &pool_entry) const
Definition: java_bytecode_parser.cpp:333
message
static const char * message(const static_verifier_resultt::statust &status)
Makes a status message string from a status.
Definition: static_verifier.cpp:74
java_bytecode_parsert::read
T read()
Definition: java_bytecode_parser.cpp:131
java_bytecode_parse_treet::methodt::verification_type_infot::type
verification_type_info_type type
Definition: java_bytecode_parse_tree.h:144
method_handle_infot::reference_index
u2 reference_index
Definition: java_bytecode_parser.cpp:375
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
java_bytecode_parse_treet::methodt::verification_type_infot
Definition: java_bytecode_parse_tree.h:140
java_bytecode_parsert::parse_local_variable_type_table
void parse_local_variable_type_table(methodt &method)
Parses the local variable type table of a method.
Definition: java_bytecode_parser.cpp:1846
CONSTANT_Utf8
#define CONSTANT_Utf8
Definition: java_bytecode_parser.cpp:165
structured_pool_entryt::structured_pool_entryt
structured_pool_entryt(const pool_entryt &entry)
Definition: java_bytecode_parser.cpp:186
CONSTANT_Float
#define CONSTANT_Float
Definition: java_bytecode_parser.cpp:161
java_bytecode_parsert::parse
bool parse() override
Definition: java_bytecode_parser.cpp:378
java_bytecode_parse_treet::classt::enum_elements
size_t enum_elements
Definition: java_bytecode_parse_tree.h:225
java_bytecode_parsert::rRuntimeAnnotation_attribute
void rRuntimeAnnotation_attribute(std::vector< annotationt > &)
Definition: java_bytecode_parser.cpp:1480
VTYPE_INFO_ITEM_NULL
#define VTYPE_INFO_ITEM_NULL
Definition: java_bytecode_parser.cpp:175
java_bytecode_parsert::pool_entryt::ref2
u2 ref2
Definition: java_bytecode_parser.cpp:43
messaget::result
mstreamt & result() const
Definition: message.h:395
messaget::error
mstreamt & error() const
Definition: message.h:385
T_INT
#define T_INT
Definition: java_bytecode_parser.cpp:877
class_infot::class_infot
class_infot(const pool_entryt &entry)
Definition: java_bytecode_parser.cpp:212
java_bytecode_parsert::rclass_attribute
void rclass_attribute()
Definition: java_bytecode_parser.cpp:1678
java_bytecode_parsert::store_unknown_method_handle
void store_unknown_method_handle(size_t bootstrap_method_index, std::vector< u2 > u2_values)
Creates an unknown method handle and puts it into the parsed_class.
Definition: java_bytecode_parser.cpp:2067
java_bytecode_parse_treet::membert::is_static
bool is_static
Definition: java_bytecode_parse_tree.h:69
parsert::in
std::istream * in
Definition: parser.h:26
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
method_handle_infot::method_handle_kindt::REF_invokeVirtual
@ REF_invokeVirtual
require_parse_tree::methodt
java_bytecode_parse_treet::methodt methodt
Definition: require_parse_tree.h:30
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
T_DOUBLE
#define T_DOUBLE
Definition: java_bytecode_parser.cpp:874
java_bytecode_parse_treet::classt::is_enum
bool is_enum
Definition: java_bytecode_parse_tree.h:214
java_bytecode_parse_treet::annotationt
Definition: java_bytecode_parse_tree.h:33
java_bytecode_parse_treet::methodt::source_location
source_locationt source_location
Definition: java_bytecode_parse_tree.h:89
T_LONG
#define T_LONG
Definition: java_bytecode_parser.cpp:878
CONSTANT_Double
#define CONSTANT_Double
Definition: java_bytecode_parser.cpp:163
java_bytecode_parse_treet::classt::name
irep_idt name
Definition: java_bytecode_parse_tree.h:212
java_bytecode_parse_treet::methodt::stack_map_table_entryt::SAME_LOCALS_ONE_STACK
@ SAME_LOCALS_ONE_STACK
Definition: java_bytecode_parse_tree.h:154
T_BYTE
#define T_BYTE
Definition: java_bytecode_parser.cpp:875
java_bytecode_parse_treet::methodt::instructions
instructionst instructions
Definition: java_bytecode_parse_tree.h:92
java_bytecode_parsert::get_class_refs_rec
void get_class_refs_rec(const typet &)
Definition: java_bytecode_parser.cpp:577
java_bytecode_parse_treet::classt::lambda_method_handlet::handle_type
method_handle_typet handle_type
Definition: java_bytecode_parse_tree.h:236
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
java_bytecode_parse_tree.h
CONSTANT_String
#define CONSTANT_String
Definition: java_bytecode_parser.cpp:159
signedbv_typet
Fixed-width bit-vector with two's complement interpretation.
Definition: std_types.h:1265
java_bytecode_parse_treet::methodt::verification_type_infot::LONG
@ LONG
Definition: java_bytecode_parse_tree.h:141
java_bytecode_parse_treet::class_refs
class_refst class_refs
Definition: java_bytecode_parse_tree.h:311
VTYPE_INFO_FLOAT
#define VTYPE_INFO_FLOAT
Definition: java_bytecode_parser.cpp:172
bytecode_info.h
messaget::set_message_handler
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:176
java_bytecode_parse_treet::methodt::base_name
irep_idt base_name
Definition: java_bytecode_parse_tree.h:86
java_bytecode_parsert
Definition: java_bytecode_parser.cpp:30
VTYPE_INFO_UNINIT_THIS
#define VTYPE_INFO_UNINIT_THIS
Definition: java_bytecode_parser.cpp:176
java_bytecode_parse_treet::classt::add_method
methodt & add_method()
Definition: java_bytecode_parse_tree.h:284
irept::id
const irep_idt & id() const
Definition: irep.h:418
message_handlert
Definition: message.h:27
java_bytecode_parse_treet::methodt::stack_map_table_entryt::FULL
@ FULL
Definition: java_bytecode_parse_tree.h:155
to_struct_tag_type
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:515
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
dstringt::empty
bool empty() const
Definition: dstring.h:88
java_bytecode_parse_treet::classt::is_private
bool is_private
Definition: java_bytecode_parse_tree.h:215
java_bytecode_parse_treet::membert::is_public
bool is_public
Definition: java_bytecode_parse_tree.h:69
method_handle_infot::method_handle_kindt::REF_invokeInterface
@ REF_invokeInterface
parsert
Definition: parser.h:24
CONSTANT_NameAndType
#define CONSTANT_NameAndType
Definition: java_bytecode_parser.cpp:164
ACC_PUBLIC
#define ACC_PUBLIC
Definition: java_bytecode_parser.cpp:1756
VTYPE_INFO_TOP
#define VTYPE_INFO_TOP
Definition: java_bytecode_parser.cpp:170
java_bytecode_parse_treet::classt::methods
methodst methods
Definition: java_bytecode_parse_tree.h:275
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:857
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
java_type_from_string
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.
Definition: java_types.cpp:560
java_bytecode_parsert::constant_pool
constant_poolt constant_pool
Definition: java_bytecode_parser.cpp:64
java_bytecode_parse_treet::classt::fields
fieldst fields
Definition: java_bytecode_parse_tree.h:274
java_bytecode_parsert::rmethod
void rmethod()
Definition: java_bytecode_parser.cpp:1771
method_handle_infot::method_handle_kindt::REF_putField
@ REF_putField
java_bytecode_parse_treet::methodt::stack_map_table_entryt::APPEND
@ APPEND
Definition: java_bytecode_parse_tree.h:155
java_bytecode_parsert::rbytecode
void rbytecode(std::vector< instructiont > &)
Definition: java_bytecode_parser.cpp:880
java_bytecode_parse_treet::classt::method_handle_typet::LAMBDA_METHOD_HANDLE
@ LAMBDA_METHOD_HANDLE
ACC_ANNOTATION
#define ACC_ANNOTATION
Definition: java_bytecode_parser.cpp:1768
java_bytecode_parsert::skip_bytes
void skip_bytes(std::size_t bytes)
Definition: java_bytecode_parser.cpp:117
java_bytecode_parse_treet::methodt::is_synthetic
bool is_synthetic
Definition: java_bytecode_parse_tree.h:88
java_bytecode_parsert::constant_poolt
std::vector< pool_entryt > constant_poolt
Definition: java_bytecode_parser.cpp:62
java_bytecode_parsert::rmethod_attribute
void rmethod_attribute(methodt &method)
Definition: java_bytecode_parser.cpp:1148
java_bytecode_parse_treet::classt::is_protected
bool is_protected
Definition: java_bytecode_parse_tree.h:215
base_ref_infot::base_ref_infot
base_ref_infot(const pool_entryt &entry)
Definition: java_bytecode_parser.cpp:261
java_bytecode_parse_treet::classt::method_handle_typet
method_handle_typet
Definition: java_bytecode_parse_tree.h:228
java_bytecode_parse_treet::methodt::stack_map_table
stack_map_tablet stack_map_table
Definition: java_bytecode_parse_tree.h:172
method_handle_infot::method_handle_kindt::REF_putStatic
@ REF_putStatic
java_bytecode_parse_treet::methodt::verification_type_infot::cpool_index
u2 cpool_index
Definition: java_bytecode_parse_tree.h:146
ACC_ENUM
#define ACC_ENUM
Definition: java_bytecode_parser.cpp:1769
name_and_type_infot::get_descriptor
std::string get_descriptor(const pool_entry_lookupt &pool_entry) const
Definition: java_bytecode_parser.cpp:247
java_bytecode_parsert::read_verification_type_info
void read_verification_type_info(methodt::verification_type_infot &)
Definition: java_bytecode_parser.cpp:1440
class_infot
Corresponds to the CONSTANT_Class_info Structure Described in Java 8 specification 4....
Definition: java_bytecode_parser.cpp:210
java_bytecode_parse_treet::parsed_class
classt parsed_class
Definition: java_bytecode_parse_tree.h:305
structured_pool_entryt
Definition: java_bytecode_parser.cpp:181
java_bytecode_parsert::pool_entryt::tag
u1 tag
Definition: java_bytecode_parser.cpp:41
type_exprt
An expression denoting a type.
Definition: std_expr.h:3899
POSTCONDITION
#define POSTCONDITION(CONDITION)
Definition: invariant.h:480
java_bytecode_parse_treet::membert::name
irep_idt name
Definition: java_bytecode_parse_tree.h:68
name_and_type_infot::name_index
u2 name_index
Definition: java_bytecode_parser.cpp:254
require_parse_tree::lambda_method_handlet
java_bytecode_parse_treet::classt::lambda_method_handlet lambda_method_handlet
Definition: require_parse_tree.h:23
name_and_type_infot::descriptor_index
u2 descriptor_index
Definition: java_bytecode_parser.cpp:255
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:226
array_typet
Arrays with given size.
Definition: std_types.h:965
java_bytecode_parse_treet::membert::is_protected
bool is_protected
Definition: java_bytecode_parse_tree.h:69
T_CHAR
#define T_CHAR
Definition: java_bytecode_parser.cpp:872
java_bytecode_parsert::rmethods
void rmethods()
Definition: java_bytecode_parser.cpp:1748
u1
uint8_t u1
Definition: bytecode_info.h:55
T_BOOLEAN
#define T_BOOLEAN
Definition: java_bytecode_parser.cpp:871
java_bytecode_parse_treet::membert::is_private
bool is_private
Definition: java_bytecode_parse_tree.h:69
java_bytecode_parse_treet::classt::method_handle_typet::UNKNOWN_HANDLE
@ UNKNOWN_HANDLE
parser.h
java_bytecode_parse_treet::methodt::is_native
bool is_native
Definition: java_bytecode_parse_tree.h:87
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
java_bytecode_parsert::rinner_classes_attribute
void rinner_classes_attribute(const u4 &attribute_length)
Corresponds to the element_value structure Described in Java 8 specification 4.7.6 https://docs....
Definition: java_bytecode_parser.cpp:1587
java_bytecode_parse_treet::methodt::is_bridge
bool is_bridge
Definition: java_bytecode_parse_tree.h:88
java_bytecode_parsert::get_annotation_value_class_refs
void get_annotation_value_class_refs(const exprt &value)
See java_bytecode_parsert::get_annotation_class_refs.
Definition: java_bytecode_parser.cpp:621
java_bytecode_parse_treet::methodt::exception_table
exception_tablet exception_table
Definition: java_bytecode_parse_tree.h:122
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
ieee_float.h
java_bytecode_parsert::get_class_refs
void get_class_refs()
Get the class references for the benefit of a dependency analysis.
Definition: java_bytecode_parser.cpp:492
ACC_STATIC
#define ACC_STATIC
Definition: java_bytecode_parser.cpp:1759
java_bytecode_parse_treet::classt::is_static_class
bool is_static_class
Definition: java_bytecode_parse_tree.h:221
method_handle_infot
Definition: java_bytecode_parser.cpp:306
java_bytecode_parse_treet::methodt::is_varargs
bool is_varargs
Definition: java_bytecode_parse_tree.h:88
java_bytecode_parse_treet::methodt::is_synchronized
bool is_synchronized
Definition: java_bytecode_parse_tree.h:87
ACC_INTERFACE
#define ACC_INTERFACE
Definition: java_bytecode_parser.cpp:1765
java_bytecode_parse_treet::classt::signature
optionalt< std::string > signature
Definition: java_bytecode_parse_tree.h:271
binary
static std::string binary(const constant_exprt &src)
Definition: json_expr.cpp:204
java_bytecode_parse_treet::fieldt
Definition: java_bytecode_parse_tree.h:186
VTYPE_INFO_INTEGER
#define VTYPE_INFO_INTEGER
Definition: java_bytecode_parser.cpp:171
java_bytecode_parse_treet::methodt::verification_type_infot::UNINITIALIZED_THIS
@ UNINITIALIZED_THIS
Definition: java_bytecode_parse_tree.h:142
java_bytecode_parse_treet::classt
Definition: java_bytecode_parse_tree.h:197
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:847
java_bytecode_parsert::rconstant_pool
void rconstant_pool()
Definition: java_bytecode_parser.cpp:639
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
java_bytecode_parsert::rinterfaces
void rinterfaces()
Definition: java_bytecode_parser.cpp:830
exprt::operands
operandst & operands()
Definition: expr.h:95
messaget::debug
mstreamt & debug() const
Definition: message.h:415
u4
uint32_t u4
Definition: bytecode_info.h:57
java_types.h
to_java_method_type
const java_method_typet & to_java_method_type(const typet &type)
Definition: java_types.h:186
s2
int16_t s2
Definition: bytecode_info.h:60
java_bytecode_parse_treet::classt::lambda_method_handlet::lambda_method_ref
irep_idt lambda_method_ref
Definition: java_bytecode_parse_tree.h:238
java_bytecode_parse_treet::fieldt::is_enum
bool is_enum
Definition: java_bytecode_parse_tree.h:187
bytecode_info
struct bytecode_infot const bytecode_info[]
Definition: bytecode_info.cpp:16
name_and_type_infot::get_name
std::string get_name(const pool_entry_lookupt &pool_entry) const
Definition: java_bytecode_parser.cpp:241
s4
int32_t s4
Definition: bytecode_info.h:61
java_bytecode_parse_treet::classt::add_field
fieldt & add_field()
Definition: java_bytecode_parse_tree.h:278
java_bytecode_parse_treet::methodt::verification_type_infot::offset
u2 offset
Definition: java_bytecode_parse_tree.h:147
java_bytecode_parsert::parse_method_handle
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...
Definition: java_bytecode_parser.cpp:1888
java_bytecode_parse_treet::classt::is_interface
bool is_interface
Definition: java_bytecode_parse_tree.h:217
java_bytecode_parsert::type_entry
const typet type_entry(u2 index)
Definition: java_bytecode_parser.cpp:85
structured_pool_entryt::pool_entry_lookupt
std::function< pool_entryt &(u2)> pool_entry_lookupt
Definition: java_bytecode_parser.cpp:184
java_bytecode_parsert::annotationt
java_bytecode_parse_treet::annotationt annotationt
Definition: java_bytecode_parser.cpp:56
UNUSED_u2
#define UNUSED_u2(x)
Definition: java_bytecode_parser.cpp:421
std_expr.h
java_bytecode_parse_treet::classt::is_abstract
bool is_abstract
Definition: java_bytecode_parse_tree.h:213
T_SHORT
#define T_SHORT
Definition: java_bytecode_parser.cpp:876
java_method_typet
Definition: java_types.h:103
array_exprt
Array constructor from list of elements.
Definition: std_expr.h:1438
java_bytecode_parse_treet::classt::inner_name
irep_idt inner_name
Definition: java_bytecode_parse_tree.h:212
VTYPE_INFO_OBJECT
#define VTYPE_INFO_OBJECT
Definition: java_bytecode_parser.cpp:177
java_bytecode_parse_treet::classt::outer_class
irep_idt outer_class
Definition: java_bytecode_parse_tree.h:224
java_bytecode_parse_treet::classt::is_anonymous_class
bool is_anonymous_class
Definition: java_bytecode_parse_tree.h:222
java_bytecode_parse_treet::classt::super_class
irep_idt super_class
Definition: java_bytecode_parse_tree.h:212
structured_pool_entryt::read_utf8_constant
static std::string read_utf8_constant(const pool_entryt &entry)
Definition: java_bytecode_parser.cpp:196
java_bytecode_parse_treet::methodt::stack_map_table_entryt::SAME_LOCALS_ONE_STACK_EXTENDED
@ SAME_LOCALS_ONE_STACK_EXTENDED
Definition: java_bytecode_parse_tree.h:154
java_bytecode_parsert::rRuntimeAnnotation
void rRuntimeAnnotation(annotationt &)
Definition: java_bytecode_parser.cpp:1493
method_handle_infot::method_handle_kindt::REF_newInvokeSpecial
@ REF_newInvokeSpecial
CONSTANT_MethodType
#define CONSTANT_MethodType
Definition: java_bytecode_parser.cpp:167
java_bytecode_parsert::rcode_attribute
void rcode_attribute(methodt &method)
Definition: java_bytecode_parser.cpp:1282
java_bytecode_parsert::pool_entryt::ref1
u2 ref1
Definition: java_bytecode_parser.cpp:42
validation_modet::INVARIANT
@ INVARIANT
java_bytecode_parsert::pool_entryt::expr
exprt expr
Definition: java_bytecode_parser.cpp:46
java_bytecode_parser.h
name_and_type_infot
Corresponds to the CONSTANT_NameAndType_info Structure Described in Java 8 specification 4....
Definition: java_bytecode_parser.cpp:231
java_bytecode_parse_treet::annotationt::type
typet type
Definition: java_bytecode_parse_tree.h:34
java_bytecode_parsert::get_annotation_class_refs
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 ...
Definition: java_bytecode_parser.cpp:607
BC_wide
#define BC_wide
Definition: bytecode_info.h:261
base_ref_infot::get_class_index
u2 get_class_index() const
Definition: java_bytecode_parser.cpp:271
java_bytecode_parse_treet::methodt::stack_map_table_entryt::SAME_EXTENDED
@ SAME_EXTENDED
Definition: java_bytecode_parse_tree.h:155