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