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