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