cprover
java_bytecode_language.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
10 
11 #include <string>
12 
13 #include <util/cmdline.h>
14 #include <util/config.h>
15 #include <util/expr_iterator.h>
16 #include <util/invariant.h>
18 #include <util/options.h>
19 #include <util/string2int.h>
20 #include <util/suffix.h>
21 #include <util/symbol_table.h>
23 
24 #include <json/json_parser.h>
25 
27 
34 #include "java_entry_point.h"
35 #include "java_bytecode_parser.h"
36 #include "java_class_loader.h"
37 #include "java_string_literals.h"
39 #include "java_utils.h"
40 #include "ci_lazy_methods.h"
41 
42 #include "expr2java.h"
43 #include "load_method_by_regex.h"
44 
48 void parse_java_language_options(const cmdlinet &cmd, optionst &options)
49 {
50  options.set_option(
51  "java-assume-inputs-non-null", cmd.isset("java-assume-inputs-non-null"));
52  options.set_option(
53  "throw-runtime-exceptions", cmd.isset("throw-runtime-exceptions"));
54  options.set_option(
55  "uncaught-exception-check", !cmd.isset("disable-uncaught-exception-check"));
56  options.set_option(
57  "throw-assertion-error", cmd.isset("throw-assertion-error"));
58  options.set_option("java-threading", cmd.isset("java-threading"));
59 
60  if(cmd.isset("java-max-vla-length"))
61  {
62  options.set_option(
63  "java-max-vla-length", cmd.get_value("java-max-vla-length"));
64  }
65 
66  options.set_option(
67  "symex-driven-lazy-loading", cmd.isset("symex-driven-lazy-loading"));
68 
69  if(cmd.isset("java-load-class"))
70  options.set_option("java-load-class", cmd.get_values("java-load-class"));
71 
72  if(cmd.isset("java-no-load-class"))
73  {
74  options.set_option(
75  "java-no-load-class", cmd.get_values("java-no-load-class"));
76  }
77  if(cmd.isset("lazy-methods-extra-entry-point"))
78  {
79  options.set_option(
80  "lazy-methods-extra-entry-point",
81  cmd.get_values("lazy-methods-extra-entry-point"));
82  }
83  if(cmd.isset("java-cp-include-files"))
84  {
85  options.set_option(
86  "java-cp-include-files", cmd.get_value("java-cp-include-files"));
87  }
88 }
89 
92 {
94 
96  options.get_bool_option("java-assume-inputs-non-null");
97  string_refinement_enabled = options.get_bool_option("refine-strings");
99  options.get_bool_option("throw-runtime-exceptions");
101  options.get_bool_option("uncaught-exception-check");
102  throw_assertion_error = options.get_bool_option("throw-assertion-error");
103  threading_support = options.get_bool_option("java-threading");
105  options.get_unsigned_int_option("java-max-vla-length");
106 
107  if(options.get_bool_option("symex-driven-lazy-loading"))
109  else if(options.get_bool_option("lazy-methods"))
111  else
113 
115  {
116  java_load_classes.insert(
117  java_load_classes.end(),
118  exception_needed_classes.begin(),
120  }
121 
122  if(options.is_set("java-load-class"))
123  {
124  const auto &load_values = options.get_list_option("java-load-class");
125  java_load_classes.insert(
126  java_load_classes.end(), load_values.begin(), load_values.end());
127  }
128  if(options.is_set("java-no-load-class"))
129  {
130  const auto &no_load_values = options.get_list_option("java-no-load-class");
131  no_load_classes = {no_load_values.begin(), no_load_values.end()};
132  }
133  const std::list<std::string> &extra_entry_points =
134  options.get_list_option("lazy-methods-extra-entry-point");
135  std::transform(
136  extra_entry_points.begin(),
137  extra_entry_points.end(),
138  std::back_inserter(extra_methods),
140  const auto &new_points = build_extra_entry_points(options);
141  extra_methods.insert(
142  extra_methods.end(), new_points.begin(), new_points.end());
143 
144  java_cp_include_files = options.get_option("java-cp-include-files");
145  if(!java_cp_include_files.empty())
146  {
147  // load file list from JSON file
148  if(java_cp_include_files[0]=='@')
149  {
150  jsont json_cp_config;
151  if(parse_json(
152  java_cp_include_files.substr(1),
154  json_cp_config))
155  throw "cannot read JSON input configuration for JAR loading";
156 
157  if(!json_cp_config.is_object())
158  throw "the JSON file has a wrong format";
159  jsont include_files=json_cp_config["jar"];
160  if(!include_files.is_array())
161  throw "the JSON file has a wrong format";
162 
163  // add jars from JSON config file to classpath
164  for(const jsont &file_entry : include_files.array)
165  {
167  file_entry.is_string() && has_suffix(file_entry.value, ".jar"),
168  "classpath entry must be jar filename, but '" + file_entry.value +
169  "' found");
170  config.java.classpath.push_back(file_entry.value);
171  }
172  }
173  }
174  else
176 
177  nondet_static = options.get_bool_option("nondet-static");
178 
180 }
181 
182 std::set<std::string> java_bytecode_languaget::extensions() const
183 {
184  return { "class", "jar" };
185 }
186 
187 void java_bytecode_languaget::modules_provided(std::set<std::string> &)
188 {
189  // modules.insert(translation_unit(parse_path));
190 }
191 
194  std::istream &,
195  const std::string &,
196  std::ostream &)
197 {
198  // there is no preprocessing!
199  return true;
200 }
201 
212  std::istream &,
213  const std::string &path)
214 {
216 
218 
219  for(const auto &p : config.java.classpath)
221 
226  {
228 
229  auto get_string_base_classes = [this](const irep_idt &id) {
231  };
232 
233  java_class_loader.set_extra_class_refs_function(get_string_base_classes);
234  }
235 
236  // look at extension
237  if(has_suffix(path, ".class"))
238  {
239  // override main_class
241  }
242  else if(has_suffix(path, ".jar"))
243  {
244  // build an object to potentially limit which classes are loaded
245  java_class_loader_limitt class_loader_limit(
249  {
250  const std::string &entry_method = config.main;
251  // If we have an entry method, we can derive a main class.
252  if(!entry_method.empty())
253  {
254  const auto last_dot_position = entry_method.find_last_of('.');
255  main_class = entry_method.substr(0, last_dot_position);
256  }
257  else
258  {
259  auto manifest = java_class_loader.jar_pool(path).get_manifest();
260  std::string manifest_main_class = manifest["Main-Class"];
261 
262  // if the manifest declares a Main-Class line, we got a main class
263  if(!manifest_main_class.empty())
264  main_class = manifest_main_class;
265  }
266  }
267  else
269 
270  // do we have one now?
271  if(main_class.empty())
272  {
273  status() << "JAR file without entry point: loading class files" << eom;
274  const auto classes = java_class_loader.load_entire_jar(path);
275  for(const auto &c : classes)
276  main_jar_classes.push_back(c);
277  }
278  else
280  }
281  else
282  UNREACHABLE;
283 
284  if(!main_class.empty())
285  {
286  status() << "Java main class: " << main_class << eom;
288  }
289 
290  return false;
291 }
292 
302  const java_bytecode_parse_treet &parse_tree,
303  symbol_tablet &symbol_table)
304 {
305  namespacet ns(symbol_table);
306  for(const auto &method : parse_tree.parsed_class.methods)
307  {
308  for(const java_bytecode_parse_treet::instructiont &instruction :
309  method.instructions)
310  {
311  if(instruction.statement == "getfield" ||
312  instruction.statement == "putfield")
313  {
314  const exprt &fieldref = instruction.args[0];
315  irep_idt class_symbol_id = fieldref.get(ID_class);
316  const symbolt *class_symbol = symbol_table.lookup(class_symbol_id);
317  INVARIANT(
318  class_symbol != nullptr,
319  "all types containing fields should have been loaded");
320 
321  const java_class_typet *class_type =
322  &to_java_class_type(class_symbol->type);
323  const irep_idt &component_name = fieldref.get(ID_component_name);
324  while(!class_type->has_component(component_name))
325  {
326  if(class_type->get_is_stub())
327  {
328  // Accessing a field of an incomplete (opaque) type.
329  symbolt &writable_class_symbol =
330  symbol_table.get_writeable_ref(class_symbol_id);
331  auto &components =
332  to_struct_type(writable_class_symbol.type).components();
333  components.emplace_back(component_name, fieldref.type());
334  components.back().set_base_name(component_name);
335  components.back().set_pretty_name(component_name);
336  break;
337  }
338  else
339  {
340  // Not present here: check the superclass.
341  INVARIANT(
342  !class_type->bases().empty(),
343  "class '" + id2string(class_symbol->name)
344  + "' (which was missing a field '" + id2string(component_name)
345  + "' referenced from method '" + id2string(method.name)
346  + "') should have an opaque superclass");
347  const auto &superclass_type = class_type->bases().front().type();
348  class_symbol_id = superclass_type.get_identifier();
349  class_type = &to_java_class_type(ns.follow(superclass_type));
350  }
351  }
352  }
353  }
354  }
355 }
356 
363  const irep_idt &class_id, symbol_tablet &symbol_table)
364 {
365  struct_tag_typet java_lang_Class("java::java.lang.Class");
366  symbol_exprt symbol_expr(
368  java_lang_Class);
369  if(!symbol_table.has_symbol(symbol_expr.get_identifier()))
370  {
371  symbolt new_class_symbol;
372  new_class_symbol.name = symbol_expr.get_identifier();
373  new_class_symbol.type = symbol_expr.type();
374  INVARIANT(
375  has_prefix(id2string(new_class_symbol.name), "java::"),
376  "class identifier should have 'java::' prefix");
377  new_class_symbol.base_name =
378  id2string(new_class_symbol.name).substr(6);
379  new_class_symbol.mode = ID_java;
380  new_class_symbol.is_lvalue = true;
381  new_class_symbol.is_state_var = true;
382  new_class_symbol.is_static_lifetime = true;
383  new_class_symbol.type.set(ID_C_no_nondet_initialization, true);
384  symbol_table.add(new_class_symbol);
385  }
386 
387  return symbol_expr;
388 }
389 
405  const exprt &ldc_arg0,
406  symbol_tablet &symbol_table,
407  bool string_refinement_enabled)
408 {
409  if(ldc_arg0.id() == ID_type)
410  {
411  const irep_idt &class_id = ldc_arg0.type().get(ID_identifier);
412  return
414  get_or_create_class_literal_symbol(class_id, symbol_table));
415  }
416  else if(ldc_arg0.id() == ID_java_string_literal)
417  {
418  return
421  ldc_arg0, symbol_table, string_refinement_enabled));
422  }
423  else
424  {
425  INVARIANT(
426  ldc_arg0.id() == ID_constant,
427  "ldc argument should be constant, string literal or class literal");
428  return ldc_arg0;
429  }
430 }
431 
442  java_bytecode_parse_treet &parse_tree,
443  symbol_tablet &symbol_table,
444  bool string_refinement_enabled)
445 {
446  for(auto &method : parse_tree.parsed_class.methods)
447  {
448  for(java_bytecode_parse_treet::instructiont &instruction :
449  method.instructions)
450  {
451  // ldc* instructions are Java bytecode "load constant" ops, which can
452  // retrieve a numeric constant, String literal, or Class literal.
453  if(instruction.statement == "ldc" ||
454  instruction.statement == "ldc2" ||
455  instruction.statement == "ldc_w" ||
456  instruction.statement == "ldc2_w")
457  {
458  INVARIANT(
459  instruction.args.size() != 0,
460  "ldc instructions should have an argument");
461  instruction.args[0] =
463  instruction.args[0],
464  symbol_table,
465  string_refinement_enabled);
466  }
467  }
468  }
469 }
470 
483  symbol_table_baset &symbol_table,
484  const irep_idt &symbol_id,
485  const irep_idt &symbol_basename,
486  const typet &symbol_type,
487  const irep_idt &class_id,
488  bool force_nondet_init)
489 {
490  symbolt new_symbol;
491  new_symbol.is_static_lifetime = true;
492  new_symbol.is_lvalue = true;
493  new_symbol.is_state_var = true;
494  new_symbol.name = symbol_id;
495  new_symbol.base_name = symbol_basename;
496  new_symbol.type = symbol_type;
497  new_symbol.type.set(ID_C_class, class_id);
498  // Public access is a guess; it encourages merging like-typed static fields,
499  // whereas a more restricted visbility would encourage separating them.
500  // Neither is correct, as without the class file we can't know the truth.
501  new_symbol.type.set(ID_C_access, ID_public);
502  new_symbol.pretty_name = new_symbol.name;
503  new_symbol.mode = ID_java;
504  new_symbol.is_type = false;
505  // If pointer-typed, initialise to null and a static initialiser will be
506  // created to initialise on first reference. If primitive-typed, specify
507  // nondeterministic initialisation by setting a nil value.
508  if(symbol_type.id() == ID_pointer && !force_nondet_init)
509  new_symbol.value = null_pointer_exprt(to_pointer_type(symbol_type));
510  else
511  new_symbol.value.make_nil();
512  bool add_failed = symbol_table.add(new_symbol);
513  INVARIANT(
514  !add_failed, "caller should have checked symbol not already in table");
515 }
516 
526  const irep_idt &start_class_id,
527  const symbol_tablet &symbol_table,
528  const class_hierarchyt &class_hierarchy)
529 {
530  // Depth-first search: return the first stub ancestor, or irep_idt() if none
531  // found.
532  std::vector<irep_idt> classes_to_check;
533  classes_to_check.push_back(start_class_id);
534 
535  while(!classes_to_check.empty())
536  {
537  irep_idt to_check = classes_to_check.back();
538  classes_to_check.pop_back();
539 
540  // Exclude java.lang.Object because it can
541  if(
542  to_java_class_type(symbol_table.lookup_ref(to_check).type)
543  .get_is_stub() &&
544  to_check != "java::java.lang.Object")
545  {
546  return to_check;
547  }
548 
549  const class_hierarchyt::idst &parents =
550  class_hierarchy.class_map.at(to_check).parents;
551  classes_to_check.insert(
552  classes_to_check.end(), parents.begin(), parents.end());
553  }
554 
555  return irep_idt();
556 }
557 
568  const java_bytecode_parse_treet &parse_tree,
569  symbol_table_baset &symbol_table,
570  const class_hierarchyt &class_hierarchy,
571  messaget &log)
572 {
573  namespacet ns(symbol_table);
574  for(const auto &method : parse_tree.parsed_class.methods)
575  {
576  for(const java_bytecode_parse_treet::instructiont &instruction :
577  method.instructions)
578  {
579  if(instruction.statement == "getstatic" ||
580  instruction.statement == "putstatic")
581  {
582  INVARIANT(
583  instruction.args.size() > 0,
584  "get/putstatic should have at least one argument");
585  irep_idt component = instruction.args[0].get_string(ID_component_name);
586  INVARIANT(
587  !component.empty(), "get/putstatic should specify a component");
588  irep_idt class_id = instruction.args[0].get_string(ID_class);
589  INVARIANT(
590  !class_id.empty(), "get/putstatic should specify a class");
591 
592  // The final 'true' parameter here includes interfaces, as they can
593  // define static fields.
596  class_id,
597  component,
598  symbol_table,
599  class_hierarchy,
600  true);
601  if(!referred_component.is_valid())
602  {
603  // Create a new stub global on an arbitrary incomplete ancestor of the
604  // class that was referred to. This is just a guess, but we have no
605  // better information to go on.
606  irep_idt add_to_class_id =
608  class_id, symbol_table, class_hierarchy);
609 
610  // If there are no incomplete ancestors to ascribe the missing field
611  // to, we must have an incomplete model of a class or simply a
612  // version mismatch of some kind. Normally this would be an error, but
613  // our models library currently triggers this error in some cases
614  // (notably java.lang.System, which is missing System.in/out/err).
615  // Therefore for this case we ascribe the missing field to the class
616  // it was directly referenced from, and fall back to initialising the
617  // field in __CPROVER_initialize, rather than try to create or augment
618  // a clinit method for a non-stub class.
619 
620  bool no_incomplete_ancestors = add_to_class_id.empty();
621  if(no_incomplete_ancestors)
622  {
623  add_to_class_id = class_id;
624 
625  // TODO forbid this again once the models library has been checked
626  // for missing static fields.
627  log.warning() << "Stub static field " << component << " found for "
628  << "non-stub type " << class_id << ". In future this "
629  << "will be a fatal error." << messaget::eom;
630  }
631 
632  irep_idt identifier =
633  id2string(add_to_class_id) + "." + id2string(component);
634 
636  symbol_table,
637  identifier,
638  component,
639  instruction.args[0].type(),
640  add_to_class_id,
641  no_incomplete_ancestors);
642  }
643  }
644  }
645  }
646 }
647 
649  symbol_tablet &symbol_table,
650  const std::string &)
651 {
653 
654  java_internal_additions(symbol_table);
655 
658 
659  // Must load java.lang.Object first to avoid stubbing
660  // This ordering could alternatively be enforced by
661  // moving the code below to the class loader.
662  java_class_loadert::parse_tree_with_overridest_mapt::const_iterator it =
663  java_class_loader.get_class_with_overlays_map().find("java.lang.Object");
665  {
666  if(
668  it->second,
669  symbol_table,
675  {
676  return true;
677  }
678  }
679 
680  // first generate a new struct symbol for each class and a new function symbol
681  // for every method
682  for(const auto &class_trees : java_class_loader.get_class_with_overlays_map())
683  {
684  if(class_trees.second.front().parsed_class.name.empty())
685  continue;
686 
687  if(
689  class_trees.second,
690  symbol_table,
696  {
697  return true;
698  }
699  }
700 
701  // Now that all classes have been created in the symbol table we can populate
702  // the class hierarchy:
703  class_hierarchy(symbol_table);
704 
705  // find and mark all implicitly generic class types
706  // this can only be done once all the class symbols have been created
707  for(const auto &c : java_class_loader.get_class_with_overlays_map())
708  {
709  if(c.second.front().parsed_class.name.empty())
710  continue;
711  try
712  {
714  c.second.front().parsed_class.name, symbol_table);
715  }
717  {
719  << "Not marking class " << c.first
720  << " implicitly generic due to missing outer class symbols"
721  << messaget::eom;
722  }
723  }
724 
725  // Infer fields on opaque types based on the method instructions just loaded.
726  // For example, if we don't have bytecode for field x of class A, but we can
727  // see an int-typed getfield instruction referring to it, add that field now.
728  for(auto &class_to_trees : java_class_loader.get_class_with_overlays_map())
729  {
730  for(const java_bytecode_parse_treet &parse_tree : class_to_trees.second)
731  infer_opaque_type_fields(parse_tree, symbol_table);
732  }
733 
734  // Create global variables for constants (String and Class literals) up front.
735  // This means that when running with lazy loading, we will be aware of these
736  // literal globals' existence when __CPROVER_initialize is generated in
737  // `generate_support_functions`.
738  const std::size_t before_constant_globals_size = symbol_table.symbols.size();
739  for(auto &class_to_trees : java_class_loader.get_class_with_overlays_map())
740  {
741  for(java_bytecode_parse_treet &parse_tree : class_to_trees.second)
742  {
744  parse_tree, symbol_table, string_refinement_enabled);
745  }
746  }
747  status() << "Java: added "
748  << (symbol_table.symbols.size() - before_constant_globals_size)
749  << " String or Class constant symbols"
750  << messaget::eom;
751 
752  // For each reference to a stub global (that is, a global variable declared on
753  // a class we don't have bytecode for, and therefore don't know the static
754  // initialiser for), create a synthetic static initialiser (clinit method)
755  // to nondet initialise it.
756  // Note this must be done before making static initialiser wrappers below, as
757  // this makes a Classname.clinit method, then the next pass makes a wrapper
758  // that ensures it is only run once, and that static initialisation happens
759  // in class-graph topological order.
760 
761  {
762  journalling_symbol_tablet symbol_table_journal =
763  journalling_symbol_tablet::wrap(symbol_table);
764  for(auto &class_to_trees : java_class_loader.get_class_with_overlays_map())
765  {
766  for(const java_bytecode_parse_treet &parse_tree : class_to_trees.second)
767  {
769  parse_tree, symbol_table_journal, class_hierarchy, *this);
770  }
771  }
772 
774  symbol_table, symbol_table_journal.get_inserted(), synthetic_methods);
775  }
776 
777  // For each class that will require a static initializer wrapper, create a
778  // function named package.classname::clinit_wrapper, and a corresponding
779  // global tracking whether it has run or not:
781  symbol_table, synthetic_methods, threading_support);
782 
783  // Now incrementally elaborate methods
784  // that are reachable from this entry point.
785  switch(lazy_methods_mode)
786  {
788  // ci = context-insensitive
790  return true;
791  break;
793  {
794  symbol_table_buildert symbol_table_builder =
795  symbol_table_buildert::wrap(symbol_table);
796 
797  journalling_symbol_tablet journalling_symbol_table =
798  journalling_symbol_tablet::wrap(symbol_table_builder);
799 
800  // Convert all synthetic methods:
801  for(const auto &function_id_and_type : synthetic_methods)
802  {
804  function_id_and_type.first, journalling_symbol_table);
805  }
806  // Convert all methods for which we have bytecode now
807  for(const auto &method_sig : method_bytecode)
808  {
809  convert_single_method(method_sig.first, journalling_symbol_table);
810  }
811  // Now convert all newly added string methods
812  for(const auto &fn_name : journalling_symbol_table.get_inserted())
813  {
815  convert_single_method(fn_name, symbol_table);
816  }
817  }
818  break;
819  default:
820  // Our caller is in charge of elaborating methods on demand.
821  break;
822  }
823 
824  // now instrument runtime exceptions
826  symbol_table,
829 
830  // now typecheck all
831  bool res = java_bytecode_typecheck(
833 
834  // now instrument thread-blocks and synchronized methods.
836  {
837  convert_threadblock(symbol_table);
839  }
840 
841  return res;
842 }
843 
845  symbol_tablet &symbol_table)
846 {
848 
849  symbol_table_buildert symbol_table_builder =
850  symbol_table_buildert::wrap(symbol_table);
851 
854  if(!res.is_success())
855  return res.is_error();
856 
857  // Load the main function into the symbol table to get access to its
858  // parameter names
859  convert_lazy_method(res.main_function.name, symbol_table_builder);
860 
861  // generate the test harness in __CPROVER__start and a call the entry point
862  return java_entry_point(
863  symbol_table_builder,
864  main_class,
871 }
872 
887  symbol_tablet &symbol_table,
888  method_bytecodet &method_bytecode)
889 {
890  symbol_table_buildert symbol_table_builder =
891  symbol_table_buildert::wrap(symbol_table);
892 
893  const method_convertert method_converter =
894  [this, &symbol_table_builder](
895  const irep_idt &function_id,
896  ci_lazy_methods_neededt lazy_methods_needed) {
897  return convert_single_method(
898  function_id, symbol_table_builder, std::move(lazy_methods_needed));
899  };
900 
901  ci_lazy_methodst method_gather(
902  symbol_table,
903  main_class,
911 
912  return method_gather(symbol_table, method_bytecode, method_converter);
913 }
914 
915 const select_pointer_typet &
917 {
918  PRECONDITION(pointer_type_selector.get()!=nullptr);
919  return *pointer_type_selector;
920 }
921 
928  std::unordered_set<irep_idt> &methods) const
929 {
930  const std::string cprover_class_prefix = "java::org.cprover.CProver.";
931 
932  // Add all string solver methods to map
934  // Add all concrete methods to map
935  for(const auto &kv : method_bytecode)
936  {
937  const std::string &method_id = id2string(kv.first);
938 
939  // Avoid advertising org.cprover.CProver methods that the Java frontend will
940  // never provide bodies for (java_bytecode_convert_method always leaves them
941  // bodyless with intent for the driver program to stub them):
942  if(has_prefix(method_id, cprover_class_prefix))
943  {
944  std::size_t method_name_end_offset =
945  method_id.find(':', cprover_class_prefix.length());
946  INVARIANT(
947  method_name_end_offset != std::string::npos,
948  "org.cprover.CProver method should have a postfix type descriptor");
949 
950  const std::string method_name =
951  method_id.substr(
952  cprover_class_prefix.length(),
953  method_name_end_offset - cprover_class_prefix.length());
954 
955  if(cprover_methods_to_ignore.count(method_name))
956  continue;
957  }
958  methods.insert(kv.first);
959  }
960  // Add all synthetic methods to map
961  for(const auto &kv : synthetic_methods)
962  methods.insert(kv.first);
963 }
964 
974  const irep_idt &function_id,
975  symbol_table_baset &symtab)
976 {
977  const symbolt &symbol = symtab.lookup_ref(function_id);
978  if(symbol.value.is_not_nil())
979  return;
980 
981  journalling_symbol_tablet symbol_table=
983 
984  convert_single_method(function_id, symbol_table);
985 
986  // Instrument runtime exceptions (unless symbol is a stub)
987  if(symbol.value.is_not_nil())
988  {
990  symbol_table,
991  symbol_table.get_writeable_ref(function_id),
994  }
995 
996  // now typecheck this function
999 }
1000 
1008  const codet &function_body,
1009  optionalt<ci_lazy_methods_neededt> needed_lazy_methods)
1010 {
1011  if(needed_lazy_methods)
1012  {
1013  for(const_depth_iteratort it = function_body.depth_cbegin();
1014  it != function_body.depth_cend();
1015  ++it)
1016  {
1017  if(it->id() == ID_code)
1018  {
1019  const auto fn_call = expr_try_dynamic_cast<code_function_callt>(*it);
1020  if(!fn_call)
1021  continue;
1022  // Only support non-virtual function calls for now, if string solver
1023  // starts to introduce virtual function calls then we will need to
1024  // duplicate the behavior of java_bytecode_convert_method where it
1025  // handles the invokevirtual instruction
1026  const symbol_exprt &fn_sym =
1027  expr_dynamic_cast<symbol_exprt>(fn_call->function());
1028  needed_lazy_methods->add_needed_method(fn_sym.get_identifier());
1029  }
1030  }
1031  }
1032 }
1033 
1044  const irep_idt &function_id,
1045  symbol_table_baset &symbol_table,
1046  optionalt<ci_lazy_methods_neededt> needed_lazy_methods)
1047 {
1048  const symbolt &symbol = symbol_table.lookup_ref(function_id);
1049 
1050  // Nothing to do if body is already loaded
1051  if(symbol.value.is_not_nil())
1052  return false;
1053 
1054  // Get bytecode for specified function if we have it
1055  method_bytecodet::opt_reft cmb = method_bytecode.get(function_id);
1056 
1057  synthetic_methods_mapt::iterator synthetic_method_it;
1058 
1059  // Check if have a string solver implementation
1060  if(string_preprocess.implements_function(function_id))
1061  {
1062  symbolt &symbol = symbol_table.get_writeable_ref(function_id);
1063  // Load parameter names from any extant bytecode before filling in body
1064  if(cmb)
1065  {
1067  symbol, cmb->get().method.local_variable_table, symbol_table);
1068  }
1069  // Populate body of the function with code generated by string preprocess
1070  const codet generated_code =
1071  string_preprocess.code_for_function(symbol, symbol_table);
1072  // String solver can make calls to functions that haven't yet been seen.
1073  // Add these to the needed_lazy_methods collection
1074  notify_static_method_calls(generated_code, needed_lazy_methods);
1075  symbol.value = std::move(generated_code);
1076  return false;
1077  }
1078  else if(
1079  (synthetic_method_it = synthetic_methods.find(function_id)) !=
1080  synthetic_methods.end())
1081  {
1082  // Synthetic method (i.e. one generated by the Java frontend and which
1083  // doesn't occur in the source bytecode):
1084  symbolt &symbol = symbol_table.get_writeable_ref(function_id);
1085  switch(synthetic_method_it->second)
1086  {
1088  if(threading_support)
1090  function_id,
1091  symbol_table,
1092  nondet_static,
1095  else
1096  symbol.value = get_clinit_wrapper_body(
1097  function_id,
1098  symbol_table,
1099  nondet_static,
1102  break;
1104  symbol.value =
1106  function_id,
1107  symbol_table,
1110  break;
1111  }
1112  // Notify lazy methods of static calls made from the newly generated
1113  // function:
1114  notify_static_method_calls(to_code(symbol.value), needed_lazy_methods);
1115  return false;
1116  }
1117 
1118  // No string solver or static init wrapper implementation;
1119  // check if have bytecode for it
1120  if(cmb)
1121  {
1123  symbol_table.lookup_ref(cmb->get().class_id),
1124  cmb->get().method,
1125  symbol_table,
1129  std::move(needed_lazy_methods),
1133  return false;
1134  }
1135 
1136  // The return of an opaque function is a source of an otherwise invisible
1137  // instantiation, so here we ensure we've loaded the appropriate classes.
1138  const java_method_typet function_type = to_java_method_type(symbol.type);
1139  if(
1140  const pointer_typet *pointer_return_type =
1141  type_try_dynamic_cast<pointer_typet>(function_type.return_type()))
1142  {
1143  // If the return type is abstract, we won't forcibly instantiate it here
1144  // otherwise this can cause abstract methods to be explictly called
1145  // TODO(tkiley): Arguably no abstract class should ever be added to
1146  // TODO(tkiley): ci_lazy_methods_neededt, but this needs further
1147  // TODO(tkiley): investigation
1148  namespacet ns{symbol_table};
1149  const java_class_typet &underlying_type =
1150  to_java_class_type(ns.follow(pointer_return_type->subtype()));
1151 
1152  if(!underlying_type.is_abstract())
1153  needed_lazy_methods->add_all_needed_classes(*pointer_return_type);
1154  }
1155 
1156  return true;
1157 }
1158 
1160 {
1162  return false;
1163 }
1164 
1166 {
1169  parse_trees.front().output(out);
1170  if(parse_trees.size() > 1)
1171  {
1172  out << "\n\nClass has the following overlays:\n\n";
1173  for(auto parse_tree_it = std::next(parse_trees.begin());
1174  parse_tree_it != parse_trees.end();
1175  ++parse_tree_it)
1176  {
1177  parse_tree_it->output(out);
1178  }
1179  out << "End of class overlays.\n";
1180  }
1181 }
1182 
1183 std::unique_ptr<languaget> new_java_bytecode_language()
1184 {
1185  return util_make_unique<java_bytecode_languaget>();
1186 }
1187 
1189  const exprt &expr,
1190  std::string &code,
1191  const namespacet &ns)
1192 {
1193  code=expr2java(expr, ns);
1194  return false;
1195 }
1196 
1198  const typet &type,
1199  std::string &code,
1200  const namespacet &ns)
1201 {
1202  code=type2java(type, ns);
1203  return false;
1204 }
1205 
1207  const std::string &code,
1208  const std::string &module,
1209  exprt &expr,
1210  const namespacet &ns)
1211 {
1212 #if 0
1213  expr.make_nil();
1214 
1215  // no preprocessing yet...
1216 
1217  std::istringstream i_preprocessed(code);
1218 
1219  // parsing
1220 
1221  java_bytecode_parser.clear();
1222  java_bytecode_parser.filename="";
1223  java_bytecode_parser.in=&i_preprocessed;
1224  java_bytecode_parser.set_message_handler(message_handler);
1225  java_bytecode_parser.grammar=java_bytecode_parsert::EXPRESSION;
1226  java_bytecode_parser.mode=java_bytecode_parsert::GCC;
1227  java_bytecode_scanner_init();
1228 
1229  bool result=java_bytecode_parser.parse();
1230 
1231  if(java_bytecode_parser.parse_tree.items.empty())
1232  result=true;
1233  else
1234  {
1235  expr=java_bytecode_parser.parse_tree.items.front().value();
1236 
1237  result=java_bytecode_convert(expr, "", message_handler);
1238 
1239  // typecheck it
1240  if(!result)
1242  }
1243 
1244  // save some memory
1245  java_bytecode_parser.clear();
1246 
1247  return result;
1248 #else
1249  // unused parameters
1250  (void)code;
1251  (void)module;
1252  (void)expr;
1253  (void)ns;
1254 #endif
1255 
1256  return true; // fail for now
1257 }
1258 
1260 {
1261 }
1262 
1266 std::vector<load_extra_methodst>
1268 {
1269  (void)options; // unused parameter
1270  return {};
1271 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:144
java_class_loader_baset::jar_pool
jar_poolt jar_pool
a cache for jar_filet, by path name
Definition: java_class_loader_base.h:38
java_static_initializers.h
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:205
method_bytecodet
Definition: ci_lazy_methods.h:33
java_bytecode_parse_treet::instructiont::args
argst args
Definition: java_bytecode_parse_tree.h:63
symbol_table_baset::has_symbol
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
Definition: symbol_table_base.h:78
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
java_bytecode_languaget::method_bytecode
method_bytecodet method_bytecode
Definition: java_bytecode_language.h:184
JAVA_CLASS_MODEL_SUFFIX
#define JAVA_CLASS_MODEL_SUFFIX
Definition: java_bytecode_language.h:86
synthetic_method_typet::STATIC_INITIALIZER_WRAPPER
@ STATIC_INITIALIZER_WRAPPER
A static initializer wrapper (code of the form if(!already_run) clinit(); already_run = true;) These ...
convert_synchronized_methods
void convert_synchronized_methods(symbol_tablet &symbol_table, message_handlert &message_handler)
Iterate through the symbol table to find and instrument synchronized methods.
Definition: java_bytecode_concurrency_instrumentation.cpp:565
java_bytecode_languaget::extensions
std::set< std::string > extensions() const override
Definition: java_bytecode_language.cpp:182
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
symbolt::is_state_var
bool is_state_var
Definition: symbol.h:62
java_class_loader_baset::file_to_class_name
static std::string file_to_class_name(const std::string &)
Convert a file name to the class name.
Definition: java_class_loader_base.cpp:38
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
exprt::depth_cbegin
const_depth_iteratort depth_cbegin() const
Definition: expr.cpp:290
create_static_initializer_wrappers
void create_static_initializer_wrappers(symbol_tablet &symbol_table, synthetic_methods_mapt &synthetic_methods, const bool thread_safe)
Create static initializer wrappers for all classes that need them.
Definition: java_static_initializers.cpp:701
symbol_table_baset::lookup_ref
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:96
configt::javat::main_class
irep_idt main_class
Definition: config.h:157
LAZY_METHODS_MODE_EAGER
@ LAZY_METHODS_MODE_EAGER
Definition: java_bytecode_language.h:81
get_clinit_wrapper_body
code_ifthenelset get_clinit_wrapper_body(const irep_idt &function_id, symbol_table_baset &symbol_table, const bool nondet_static, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector)
Produces the static initializer wrapper body for the given function.
Definition: java_static_initializers.cpp:638
class_hierarchyt
Non-graph-based representation of the class hierarchy.
Definition: class_hierarchy.h:42
resolve_inherited_componentt::inherited_componentt::is_valid
bool is_valid() const
Use to check if this inherited_componentt has been fully constructed.
Definition: resolve_inherited_component.cpp:108
java_bytecode_language.h
parse_java_language_options
void parse_java_language_options(const cmdlinet &cmd, optionst &options)
Parse options that are java bytecode specific.
Definition: java_bytecode_language.cpp:48
journalling_symbol_tablet::wrap
static journalling_symbol_tablet wrap(symbol_table_baset &base_symbol_table)
Definition: journalling_symbol_table.h:80
cmdlinet::isset
virtual bool isset(char option) const
Definition: cmdline.cpp:27
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:349
main_function_resultt::main_function
symbolt main_function
Definition: java_entry_point.h:40
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:485
java_bytecode_languaget::pointer_type_selector
const std::unique_ptr< const select_pointer_typet > pointer_type_selector
Definition: java_bytecode_language.h:200
class_typet::is_abstract
bool is_abstract() const
Definition: std_types.h:386
java_bytecode_parse_treet
Definition: java_bytecode_parse_tree.h:22
optionst
Definition: options.h:22
irept::make_nil
void make_nil()
Definition: irep.h:315
java_string_literals.h
java_bytecode_languaget::synthetic_methods
synthetic_methods_mapt synthetic_methods
Maps synthetic method names on to the particular type of synthetic method (static initializer,...
Definition: java_bytecode_language.h:205
java_bytecode_languaget::to_expr
bool to_expr(const std::string &code, const std::string &module, exprt &expr, const namespacet &ns) override
Parses the given string into an expression.
Definition: java_bytecode_language.cpp:1206
typet
The type of an expression, extends irept.
Definition: type.h:27
optionst::get_option
const std::string get_option(const std::string &option) const
Definition: options.cpp:65
languaget::language_options_initialized
bool language_options_initialized
Definition: language.h:190
messaget::status
mstreamt & status() const
Definition: message.h:401
java_bytecode_languaget::extra_methods
std::vector< load_extra_methodst > extra_methods
Definition: java_bytecode_language.h:211
get_main_symbol
main_function_resultt get_main_symbol(const symbol_table_baset &symbol_table, const irep_idt &main_class, message_handlert &message_handler)
Figures out the entry point of the code to verify.
Definition: java_entry_point.cpp:516
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
java_bytecode_languaget::do_ci_lazy_method_conversion
bool do_ci_lazy_method_conversion(symbol_tablet &, method_bytecodet &)
Uses a simple context-insensitive ('ci') analysis to determine which methods may be reachable from th...
Definition: java_bytecode_language.cpp:886
java_bytecode_languaget::methods_provided
virtual void methods_provided(std::unordered_set< irep_idt > &methods) const override
Provide feedback to language_filest so that when asked for a lazy method, it can delegate to this ins...
Definition: java_bytecode_language.cpp:927
configt::main
std::string main
Definition: config.h:172
load_method_by_regex.h
method_bytecodet::opt_reft
optionalt< std::reference_wrapper< const class_method_and_bytecodet > > opt_reft
Definition: ci_lazy_methods.h:45
java_class_loadert::load_entire_jar
std::vector< irep_idt > load_entire_jar(const std::string &jar_path)
Load all class files from a .jar file.
Definition: java_class_loader.cpp:186
new_java_bytecode_language
std::unique_ptr< languaget > new_java_bytecode_language()
Definition: java_bytecode_language.cpp:1183
method_bytecodet::get
opt_reft get(const irep_idt &method_id)
Definition: ci_lazy_methods.h:81
java_bytecode_parse_treet::instructiont
Definition: java_bytecode_parse_tree.h:57
java_bytecode_languaget::main_class
irep_idt main_class
Definition: java_bytecode_language.h:177
notify_static_method_calls
static void notify_static_method_calls(const codet &function_body, optionalt< ci_lazy_methods_neededt > needed_lazy_methods)
Notify ci_lazy_methods, if present, of any static function calls made by the given function body.
Definition: java_bytecode_language.cpp:1007
java_bytecode_languaget::convert_single_method
void convert_single_method(const irep_idt &function_id, symbol_table_baset &symbol_table)
Definition: java_bytecode_language.h:162
exprt
Base class for all expressions.
Definition: expr.h:54
resolve_inherited_componentt::inherited_componentt
Definition: resolve_inherited_component.h:27
java_string_library_preprocesst::implements_function
bool implements_function(const irep_idt &function_id) const
Definition: java_string_library_preprocess.cpp:1761
infer_opaque_type_fields
static void infer_opaque_type_fields(const java_bytecode_parse_treet &parse_tree, symbol_tablet &symbol_table)
Infer fields that must exist on opaque types from field accesses against them.
Definition: java_bytecode_language.cpp:301
journalling_symbol_table.h
Author: Diffblue Ltd.
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
struct_tag_typet
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:517
java_bytecode_languaget::from_type
bool from_type(const typet &type, std::string &code, const namespacet &ns) override
Formats the given type in a language-specific way.
Definition: java_bytecode_language.cpp:1197
convert_threadblock
void convert_threadblock(symbol_tablet &symbol_table)
Iterate through the symbol table to find and appropriately instrument thread-blocks.
Definition: java_bytecode_concurrency_instrumentation.cpp:454
options.h
invariant.h
component
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:173
java_string_library_preprocesst::initialize_known_type_table
void initialize_known_type_table()
Definition: java_string_library_preprocess.cpp:1848
optionst::set_option
void set_option(const std::string &option, const bool value)
Definition: options.cpp:26
irep_idt
dstringt irep_idt
Definition: irep.h:32
messaget::eom
static eomt eom
Definition: message.h:284
method_convertert
std::function< bool(const irep_idt &function_id, ci_lazy_methods_neededt)> method_convertert
Definition: ci_lazy_methods.h:92
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:143
has_suffix
bool has_suffix(const std::string &s, const std::string &suffix)
Definition: suffix.h:15
java_bytecode_languaget::final
virtual bool final(symbol_table_baset &context) override
Final adjustments, e.g.
Definition: java_bytecode_language.cpp:1159
jsont
Definition: json.h:23
java_bytecode_languaget::parse
bool parse(std::istream &instream, const std::string &path) override
We set the main class (i.e. class to start the class loading analysis from, see java_class_loadert) d...
Definition: java_bytecode_language.cpp:211
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
configt::javat::classpath
classpatht classpath
Definition: config.h:156
missing_outer_class_symbol_exceptiont
An exception that is raised checking whether a class is implicitly generic if a symbol for an outer c...
Definition: java_bytecode_convert_class.h:46
java_string_library_preprocesst::get_string_type_base_classes
std::vector< irep_idt > get_string_type_base_classes(const irep_idt &class_name)
Gets the base classes for known String and String-related types, or returns an empty list for other t...
Definition: java_string_library_preprocess.cpp:182
java_bytecode_languaget::throw_runtime_exceptions
bool throw_runtime_exceptions
Definition: java_bytecode_language.h:187
java_bytecode_languaget::stub_global_initializer_factory
stub_global_initializer_factoryt stub_global_initializer_factory
Definition: java_bytecode_language.h:206
main_function_resultt::is_error
bool is_error() const
Definition: java_entry_point.h:59
main_function_resultt::is_success
bool is_success() const
Definition: java_entry_point.h:55
symbolt::pretty_name
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
java_class_typet
Definition: java_types.h:101
to_code
const codet & to_code(const exprt &expr)
Definition: std_code.h:136
json_parser.h
get_any_incomplete_ancestor_for_stub_static_field
static irep_idt get_any_incomplete_ancestor_for_stub_static_field(const irep_idt &start_class_id, const symbol_tablet &symbol_table, const class_hierarchyt &class_hierarchy)
Find any incomplete ancestor of a given class that can have a stub static field attached to it.
Definition: java_bytecode_language.cpp:525
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
java_bytecode_convert_method
void java_bytecode_convert_method(const symbolt &class_symbol, const java_bytecode_parse_treet::methodt &method, symbol_table_baset &symbol_table, message_handlert &message_handler, size_t max_array_length, bool throw_assertion_error, optionalt< ci_lazy_methods_neededt > needed_lazy_methods, java_string_library_preprocesst &string_preprocess, const class_hierarchyt &class_hierarchy, bool threading_support)
Definition: java_bytecode_convert_method.cpp:3065
create_stub_global_symbol
static void create_stub_global_symbol(symbol_table_baset &symbol_table, const irep_idt &symbol_id, const irep_idt &symbol_basename, const typet &symbol_type, const irep_idt &class_id, bool force_nondet_init)
Add a stub global symbol to the symbol table, initialising pointer-typed symbols with null and primit...
Definition: java_bytecode_language.cpp:482
string2int.h
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
const_depth_iteratort
Definition: expr_iterator.h:224
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:173
java_bytecode_languaget::set_language_options
void set_language_options(const optionst &) override
Consume options that are java bytecode specific.
Definition: java_bytecode_language.cpp:91
cmdlinet
Definition: cmdline.h:19
java_bytecode_languaget::build_extra_entry_points
virtual std::vector< load_extra_methodst > build_extra_entry_points(const optionst &) const
This method should be overloaded to provide alternative approaches for specifying extra entry points.
Definition: java_bytecode_language.cpp:1267
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
messaget::result
mstreamt & result() const
Definition: message.h:396
java_bytecode_languaget::string_refinement_enabled
bool string_refinement_enabled
Definition: java_bytecode_language.h:186
java_class_loadert::parse_tree_with_overlayst
std::list< java_bytecode_parse_treet > parse_tree_with_overlayst
A list of parse trees supporting overlay classes.
Definition: java_class_loader.h:30
java_bytecode_languaget::main_jar_classes
std::vector< irep_idt > main_jar_classes
Definition: java_bytecode_language.h:178
java_class_loadert::set_java_cp_include_files
void set_java_cp_include_files(const std::string &java_cp_include_files)
Set the argument of the class loader limit java_class_loader_limitt.
Definition: java_class_loader.h:52
null_pointer_exprt
The null pointer constant.
Definition: std_expr.h:4471
symbol_table_baset::get_writeable_ref
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
Definition: symbol_table_base.h:110
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
java_bytecode_languaget::~java_bytecode_languaget
virtual ~java_bytecode_languaget()
Definition: java_bytecode_language.cpp:1259
get_ldc_result
static exprt get_ldc_result(const exprt &ldc_arg0, symbol_tablet &symbol_table, bool string_refinement_enabled)
Get result of a Java load-constant (ldc) instruction.
Definition: java_bytecode_language.cpp:404
java_bytecode_languaget::java_class_loader
java_class_loadert java_class_loader
Definition: java_bytecode_language.h:179
java_bytecode_languaget::threading_support
bool threading_support
Definition: java_bytecode_language.h:180
get_inherited_component
resolve_inherited_componentt::inherited_componentt get_inherited_component(const irep_idt &component_class_id, const irep_idt &component_name, const symbol_tablet &symbol_table, const class_hierarchyt &class_hierarchy, bool include_interfaces)
Finds an inherited component (method or field), taking component visibility into account.
Definition: java_utils.cpp:335
mark_java_implicitly_generic_class_type
void mark_java_implicitly_generic_class_type(const irep_idt &class_name, symbol_tablet &symbol_table)
Checks if the class is implicitly generic, i.e., it is an inner class of any generic class.
Definition: java_bytecode_convert_class.cpp:1122
optionst::is_set
bool is_set(const std::string &option) const
N.B. opts.is_set("foo") does not imply opts.get_bool_option("foo")
Definition: options.cpp:60
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:176
jsont::is_string
bool is_string() const
Definition: json.h:39
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:21
java_string_library_preprocesst::get_all_function_names
void get_all_function_names(std::unordered_set< irep_idt > &methods) const
Definition: java_string_library_preprocess.cpp:1785
java_bytecode_languaget::show_parse
void show_parse(std::ostream &out) override
Definition: java_bytecode_language.cpp:1165
java_class_loader.h
java_string_library_preprocesst::code_for_function
codet code_for_function(const symbolt &symbol, symbol_table_baset &symbol_table)
Should be called to provide code for string functions that are used in the code but for which no impl...
Definition: java_string_library_preprocess.cpp:1800
java_bytecode_languaget::lazy_methods_mode
lazy_methods_modet lazy_methods_mode
Definition: java_bytecode_language.h:185
java_bytecode_languaget::generate_support_functions
bool generate_support_functions(symbol_tablet &symbol_table) override
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
Definition: java_bytecode_language.cpp:844
cmdlinet::get_value
std::string get_value(char option) const
Definition: cmdline.cpp:45
java_bytecode_internal_additions.h
java_entry_point.h
java_bytecode_languaget::nondet_static
bool nondet_static
Definition: java_bytecode_language.h:192
select_pointer_typet
Definition: select_pointer_type.h:28
messaget::set_message_handler
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:169
java_bytecode_languaget::assert_uncaught_exceptions
bool assert_uncaught_exceptions
Definition: java_bytecode_language.h:188
struct_typet::bases
const basest & bases() const
Get the collection of base classes/structs.
Definition: std_types.h:303
create_stub_global_symbols
static void create_stub_global_symbols(const java_bytecode_parse_treet &parse_tree, symbol_table_baset &symbol_table, const class_hierarchyt &class_hierarchy, messaget &log)
Search for getstatic and putstatic instructions in a class' bytecode and create stub symbols for any ...
Definition: java_bytecode_language.cpp:567
java_bytecode_languaget::convert_lazy_method
virtual void convert_lazy_method(const irep_idt &function_id, symbol_table_baset &symbol_table) override
Promote a lazy-converted method (one whose type is known but whose body hasn't been converted) into a...
Definition: java_bytecode_language.cpp:973
java_class_loader_baset::add_classpath_entry
void add_classpath_entry(const std::string &)
Appends an entry to the class path, used for loading classes.
Definition: java_class_loader_base.cpp:19
java_bytecode_typecheck_updated_symbols
void java_bytecode_typecheck_updated_symbols(journalling_symbol_tablet &symbol_table, message_handlert &message_handler, bool string_refinement_enabled)
Definition: java_bytecode_typecheck.cpp:78
struct_union_typet::has_component
bool has_component(const irep_idt &component_name) const
Definition: std_types.h:215
irept::id
const irep_idt & id() const
Definition: irep.h:259
java_bytecode_languaget::throw_assertion_error
bool throw_assertion_error
Definition: java_bytecode_language.h:189
class_hierarchyt::idst
std::vector< irep_idt > idst
Definition: class_hierarchy.h:45
java_bytecode_convert_method.h
class_hierarchyt::class_map
class_mapt class_map
Definition: class_hierarchy.h:55
dstringt::empty
bool empty() const
Definition: dstring.h:75
java_bytecode_languaget::modules_provided
void modules_provided(std::set< std::string > &modules) override
Definition: java_bytecode_language.cpp:187
cprover_methods_to_ignore
const std::unordered_set< std::string > cprover_methods_to_ignore
Methods belonging to the class org.cprover.CProver that should be ignored (not converted),...
Definition: java_utils.cpp:421
java_bytecode_languaget::string_preprocess
java_string_library_preprocesst string_preprocess
Definition: java_bytecode_language.h:190
java_bytecode_parse_treet::classt::methods
methodst methods
Definition: java_bytecode_parse_tree.h:279
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1544
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
java_class_loadert::set_extra_class_refs_function
void set_extra_class_refs_function(get_extra_class_refs_functiont func)
Sets a function that provides extra dependencies for a particular class.
Definition: java_class_loader.h:60
optionst::get_unsigned_int_option
unsigned int get_unsigned_int_option(const std::string &option) const
Definition: options.cpp:54
main_function_resultt
Definition: java_entry_point.h:32
build_load_method_by_regex
std::function< std::vector< irep_idt >const symbol_tablet &symbol_table)> build_load_method_by_regex(const std::string &pattern)
Create a lambda that returns the symbols that the given pattern should be loaded.If the pattern doesn...
Definition: load_method_by_regex.cpp:57
ci_lazy_methods.h
config
configt config
Definition: config.cpp:24
java_bytecode_concurrency_instrumentation.h
object_factory_parameterst::set
void set(const optionst &)
Assigns the parameters from given options.
Definition: object_factory_parameters.cpp:14
java_bytecode_instrument
void java_bytecode_instrument(symbol_tablet &symbol_table, const bool throw_runtime_exceptions, message_handlert &message_handler)
Instruments all the code in the symbol_table with runtime exceptions or corresponding assertions.
Definition: java_bytecode_instrument.cpp:611
java_class_loader_limitt
Class representing a filter for class file loading.
Definition: java_class_loader_limit.h:22
symbol_table_baset::add
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Definition: symbol_table_base.cpp:18
java_bytecode_languaget::from_expr
bool from_expr(const exprt &expr, std::string &code, const namespacet &ns) override
Formats the given expression in a language-specific way.
Definition: java_bytecode_language.cpp:1188
java_bytecode_languaget::assume_inputs_non_null
bool assume_inputs_non_null
Definition: java_bytecode_language.h:181
java_bytecode_parse_treet::parsed_class
classt parsed_class
Definition: java_bytecode_parse_tree.h:309
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
messaget::get_message_handler
message_handlert & get_message_handler()
Definition: message.h:174
class_hierarchy.h
java_bytecode_languaget::get_pointer_type_selector
const select_pointer_typet & get_pointer_type_selector() const
Definition: java_bytecode_language.cpp:916
java_bytecode_languaget::class_hierarchy
class_hierarchyt class_hierarchy
Definition: java_bytecode_language.h:207
java_internal_additions
void java_internal_additions(symbol_table_baset &dest)
Definition: java_bytecode_internal_additions.cpp:18
synthetic_method_typet::STUB_CLASS_STATIC_INITIALIZER
@ STUB_CLASS_STATIC_INITIALIZER
A generated (synthetic) static initializer function for a stub type.
java_entry_point
bool java_entry_point(symbol_table_baset &symbol_table, const irep_idt &main_class, message_handlert &message_handler, bool assume_init_pointers_not_null, bool assert_uncaught_exceptions, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, bool string_refinement_enabled)
Given the symbol_table and the main_class to test, this function generates a new function __CPROVER__...
Definition: java_entry_point.cpp:610
messaget::message_handler
message_handlert * message_handler
Definition: message.h:426
java_bytecode_languaget::typecheck
bool typecheck(symbol_tablet &context, const std::string &module) override
Definition: java_bytecode_language.cpp:648
stub_global_initializer_factoryt::get_stub_initializer_body
code_blockt get_stub_initializer_body(const irep_idt &function_id, symbol_table_baset &symbol_table, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector)
Create the body of a synthetic static initializer (clinit method), which initialise stub globals in t...
Definition: java_static_initializers.cpp:830
expr_iterator.h
java_bytecode_languaget::java_cp_include_files
std::string java_cp_include_files
Definition: java_bytecode_language.h:191
java_class_loadert::add_load_classes
void add_load_classes(const std::vector< irep_idt > &classes)
Adds the list of classes to the load queue, forcing them to be loaded even without explicit reference...
Definition: java_class_loader.h:67
suffix.h
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
stub_global_initializer_factoryt::create_stub_global_initializer_symbols
void create_stub_global_initializer_symbols(symbol_tablet &symbol_table, const std::unordered_set< irep_idt > &stub_globals_set, synthetic_methods_mapt &synthetic_methods)
Create static initializer symbols for each distinct class that has stub globals.
Definition: java_static_initializers.cpp:746
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
exprt::depth_cend
const_depth_iteratort depth_cend() const
Definition: expr.cpp:292
jsont::array
arrayt array
Definition: json.h:129
get_thread_safe_clinit_wrapper_body
code_blockt get_thread_safe_clinit_wrapper_body(const irep_idt &function_id, symbol_table_baset &symbol_table, const bool nondet_static, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector)
Thread safe version of the static initializer.
Definition: java_static_initializers.cpp:448
java_class_loadert::get_class_with_overlays_map
fixed_keys_map_wrappert< parse_tree_with_overridest_mapt > get_class_with_overlays_map()
Map from class names to the bytecode parse trees.
Definition: java_class_loader.h:77
cmdline.h
java_bytecode_languaget::java_load_classes
std::vector< irep_idt > java_load_classes
Definition: java_bytecode_language.h:195
exception_needed_classes
const std::vector< std::string > exception_needed_classes
Definition: java_bytecode_instrument.cpp:79
ci_lazy_methodst
Definition: ci_lazy_methods.h:97
symbolt
Symbol table entry.
Definition: symbol.h:27
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
symbol_table_buildert::wrap
static symbol_table_buildert wrap(symbol_table_baset &base_symbol_table)
Definition: symbol_table_builder.h:42
java_bytecode_languaget::id
std::string id() const override
Definition: java_bytecode_language.h:150
get_or_create_class_literal_symbol
static symbol_exprt get_or_create_class_literal_symbol(const irep_idt &class_id, symbol_tablet &symbol_table)
Create if necessary, then return the constant global java.lang.Class symbol for a given class id.
Definition: java_bytecode_language.cpp:362
optionst::get_bool_option
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
symbol_table_buildert
Author: Diffblue Ltd.
Definition: symbol_table_builder.h:13
symbol_table_baset::symbols
const symbolst & symbols
Definition: symbol_table_base.h:27
symbolt::is_type
bool is_type
Definition: symbol.h:61
jsont::is_array
bool is_array() const
Definition: json.h:54
generate_constant_global_variables
static void generate_constant_global_variables(java_bytecode_parse_treet &parse_tree, symbol_tablet &symbol_table, bool string_refinement_enabled)
Creates global variables for constants mentioned in a given method.
Definition: java_bytecode_language.cpp:441
java_bytecode_languaget::max_user_array_length
size_t max_user_array_length
Definition: java_bytecode_language.h:183
java_bytecode_parse_treet::instructiont::statement
irep_idt statement
Definition: java_bytecode_parse_tree.h:61
configt::java
struct configt::javat java
type2java
std::string type2java(const typet &type, const namespacet &ns)
Definition: expr2java.cpp:448
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
LAZY_METHODS_MODE_CONTEXT_INSENSITIVE
@ LAZY_METHODS_MODE_CONTEXT_INSENSITIVE
Definition: java_bytecode_language.h:82
java_bytecode_languaget::object_factory_parameters
java_object_factory_parameterst object_factory_parameters
Definition: java_bytecode_language.h:182
config.h
expr2java
std::string expr2java(const exprt &expr, const namespacet &ns)
Definition: expr2java.cpp:441
symbol_table_baset::lookup
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:86
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:883
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
java_bytecode_instrument_symbol
void java_bytecode_instrument_symbol(symbol_table_baset &symbol_table, symbolt &symbol, const bool throw_runtime_exceptions, message_handlert &message_handler)
Instruments the code attached to symbol with runtime exceptions or corresponding assertions.
Definition: java_bytecode_instrument.cpp:561
ci_lazy_methods_neededt
Definition: ci_lazy_methods_needed.h:24
get_or_create_string_literal_symbol
symbol_exprt get_or_create_string_literal_symbol(const exprt &string_expr, symbol_table_baset &symbol_table, bool string_refinement_enabled)
Creates or gets an existing constant global symbol for a given string literal.
Definition: java_string_literals.cpp:66
java_string_library_preprocesst::initialize_conversion_table
void initialize_conversion_table()
fill maps with correspondence from java method names to conversion functions
Definition: java_string_library_preprocess.cpp:1857
java_bytecode_typecheck
bool java_bytecode_typecheck(symbol_table_baset &symbol_table, message_handlert &message_handler, bool string_refinement_enabled)
Definition: java_bytecode_typecheck.cpp:68
jsont::is_object
bool is_object() const
Definition: json.h:49
symbolt::is_lvalue
bool is_lvalue
Definition: symbol.h:66
to_java_class_type
const java_class_typet & to_java_class_type(const typet &type)
Definition: java_types.h:246
journalling_symbol_tablet::get_inserted
const changesett & get_inserted() const
Definition: journalling_symbol_table.h:143
java_class_loader_baset::clear_classpath
void clear_classpath()
Clear all classpath entries.
Definition: java_class_loader_base.h:22
expr2java.h
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:3255
to_java_method_type
const java_method_typet & to_java_method_type(const typet &type)
Definition: java_types.h:338
java_class_typet::get_is_stub
bool get_is_stub() const
Definition: java_types.h:179
java_bytecode_instrument.h
symbol_table.h
Author: Diffblue Ltd.
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1507
LAZY_METHODS_MODE_EXTERNAL_DRIVER
@ LAZY_METHODS_MODE_EXTERNAL_DRIVER
Definition: java_bytecode_language.h:83
java_utils.h
symbol_table_builder.h
messaget::warning
mstreamt & warning() const
Definition: message.h:391
java_bytecode_languaget::preprocess
virtual bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream) override
ANSI-C preprocessing.
Definition: java_bytecode_language.cpp:193
cmdlinet::get_values
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:110
parse_json
bool parse_json(std::istream &in, const std::string &filename, message_handlert &message_handler, jsont &dest)
Definition: json_parser.cpp:16
journalling_symbol_tablet
A symbol table wrapper that records which entries have been updated/removed.
Definition: journalling_symbol_table.h:35
java_method_typet
Definition: java_types.h:264
optionst::get_list_option
const value_listt & get_list_option(const std::string &option) const
Definition: options.cpp:78
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
java_bytecode_convert_class
bool java_bytecode_convert_class(const java_class_loadert::parse_tree_with_overlayst &parse_trees, 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)
See class java_bytecode_convert_classt.
Definition: java_bytecode_convert_class.cpp:937
java_bytecode_initialize_parameter_names
void java_bytecode_initialize_parameter_names(symbolt &method_symbol, const java_bytecode_parse_treet::methodt::local_variable_tablet &local_variable_table, symbol_table_baset &symbol_table)
This uses a cut-down version of the logic in java_bytecode_convert_methodt::convert to initialize sym...
Definition: java_bytecode_convert_method.cpp:2987
java_bytecode_typecheck.h
validation_modet::INVARIANT
@ INVARIANT
java_bytecode_convert_class.h
java_bytecode_parser.h
jsont::value
std::string value
Definition: json.h:137
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:34
java_bytecode_languaget::no_load_classes
std::unordered_set< std::string > no_load_classes
Definition: java_bytecode_language.h:209