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