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 <fstream>
12 #include <string>
13 
15 
16 #include <util/cmdline.h>
17 #include <util/config.h>
18 #include <util/expr_iterator.h>
19 #include <util/invariant.h>
21 #include <util/options.h>
22 #include <util/prefix.h>
23 #include <util/string2int.h>
24 #include <util/suffix.h>
25 #include <util/symbol_table.h>
27 
28 #include <json/json_parser.h>
29 
31 
32 #include "ci_lazy_methods.h"
39 #include "java_bytecode_parser.h"
41 #include "java_class_loader.h"
42 #include "java_entry_point.h"
45 #include "java_string_literals.h"
46 #include "java_utils.h"
47 #include "lambda_synthesis.h"
48 #include "lift_clinit_calls.h"
49 
50 #include "expr2java.h"
51 #include "load_method_by_regex.h"
52 
56 void parse_java_language_options(const cmdlinet &cmd, optionst &options)
57 {
58  options.set_option(
59  "java-assume-inputs-non-null", cmd.isset("java-assume-inputs-non-null"));
60  options.set_option(
61  "throw-runtime-exceptions", cmd.isset("throw-runtime-exceptions"));
62  options.set_option(
63  "uncaught-exception-check", !cmd.isset("disable-uncaught-exception-check"));
64  options.set_option(
65  "throw-assertion-error", cmd.isset("throw-assertion-error"));
66  options.set_option(
67  "assert-no-exceptions-thrown", cmd.isset("assert-no-exceptions-thrown"));
68  options.set_option("java-threading", cmd.isset("java-threading"));
69 
70  if(cmd.isset("java-max-vla-length"))
71  {
72  options.set_option(
73  "java-max-vla-length", cmd.get_value("java-max-vla-length"));
74  }
75 
76  options.set_option(
77  "symex-driven-lazy-loading", cmd.isset("symex-driven-lazy-loading"));
78 
79  options.set_option(
80  "ignore-manifest-main-class", cmd.isset("ignore-manifest-main-class"));
81 
82  if(cmd.isset("context-include"))
83  options.set_option("context-include", cmd.get_values("context-include"));
84 
85  if(cmd.isset("context-exclude"))
86  options.set_option("context-exclude", cmd.get_values("context-exclude"));
87 
88  if(cmd.isset("java-load-class"))
89  options.set_option("java-load-class", cmd.get_values("java-load-class"));
90 
91  if(cmd.isset("java-no-load-class"))
92  {
93  options.set_option(
94  "java-no-load-class", cmd.get_values("java-no-load-class"));
95  }
96  if(cmd.isset("lazy-methods-extra-entry-point"))
97  {
98  options.set_option(
99  "lazy-methods-extra-entry-point",
100  cmd.get_values("lazy-methods-extra-entry-point"));
101  }
102  if(cmd.isset("java-cp-include-files"))
103  {
104  options.set_option(
105  "java-cp-include-files", cmd.get_value("java-cp-include-files"));
106  }
107  if(cmd.isset("static-values"))
108  {
109  options.set_option("static-values", cmd.get_value("static-values"));
110  }
111  options.set_option(
112  "java-lift-clinit-calls", cmd.isset("java-lift-clinit-calls"));
113 }
114 
116 {
117  std::vector<std::string> context_include;
118  std::vector<std::string> context_exclude;
119  for(const auto &include : options.get_list_option("context-include"))
120  context_include.push_back("java::" + include);
121  for(const auto &exclude : options.get_list_option("context-exclude"))
122  context_exclude.push_back("java::" + exclude);
123  return prefix_filtert(std::move(context_include), std::move(context_exclude));
124 }
125 
126 std::unordered_multimap<irep_idt, symbolt> &
128 {
129  if(!initialized)
130  {
131  map = class_to_declared_symbols(symbol_table);
132  initialized = true;
133  }
134  return map;
135 }
136 
138 {
139  initialized = false;
140  map.clear();
141 }
142 
144  const optionst &options,
145  messaget &log)
146 {
148  options.get_bool_option("java-assume-inputs-non-null");
149  string_refinement_enabled = options.get_bool_option("refine-strings");
151  options.get_bool_option("throw-runtime-exceptions");
153  options.get_bool_option("uncaught-exception-check");
154  throw_assertion_error = options.get_bool_option("throw-assertion-error");
156  options.get_bool_option("assert-no-exceptions-thrown");
157  threading_support = options.get_bool_option("java-threading");
159  options.get_unsigned_int_option("java-max-vla-length");
160 
161  if(options.get_bool_option("symex-driven-lazy-loading"))
163  else if(options.get_bool_option("lazy-methods"))
165  else
167 
169  {
170  java_load_classes.insert(
171  java_load_classes.end(),
172  exception_needed_classes.begin(),
174  }
175 
176  if(options.is_set("java-load-class"))
177  {
178  const auto &load_values = options.get_list_option("java-load-class");
179  java_load_classes.insert(
180  java_load_classes.end(), load_values.begin(), load_values.end());
181  }
182  if(options.is_set("java-no-load-class"))
183  {
184  const auto &no_load_values = options.get_list_option("java-no-load-class");
185  no_load_classes = {no_load_values.begin(), no_load_values.end()};
186  }
187  const std::list<std::string> &extra_entry_points =
188  options.get_list_option("lazy-methods-extra-entry-point");
189  std::transform(
190  extra_entry_points.begin(),
191  extra_entry_points.end(),
192  std::back_inserter(extra_methods),
194 
195  java_cp_include_files = options.get_option("java-cp-include-files");
196  if(!java_cp_include_files.empty())
197  {
198  // load file list from JSON file
199  if(java_cp_include_files[0]=='@')
200  {
201  jsont json_cp_config;
202  if(parse_json(
203  java_cp_include_files.substr(1),
204  log.get_message_handler(),
205  json_cp_config))
206  throw "cannot read JSON input configuration for JAR loading";
207 
208  if(!json_cp_config.is_object())
209  throw "the JSON file has a wrong format";
210  jsont include_files=json_cp_config["jar"];
211  if(!include_files.is_array())
212  throw "the JSON file has a wrong format";
213 
214  // add jars from JSON config file to classpath
215  for(const jsont &file_entry : to_json_array(include_files))
216  {
218  file_entry.is_string() && has_suffix(file_entry.value, ".jar"),
219  "classpath entry must be jar filename, but '" + file_entry.value +
220  "' found");
221  config.java.classpath.push_back(file_entry.value);
222  }
223  }
224  }
225  else
227 
228  nondet_static = options.get_bool_option("nondet-static");
229  if(options.is_set("static-values"))
230  {
231  const std::string filename = options.get_option("static-values");
232  jsont tmp_json;
233  if(parse_json(filename, log.get_message_handler(), tmp_json))
234  {
235  log.warning()
236  << "Provided JSON file for static-values cannot be parsed; it"
237  << " will be ignored." << messaget::eom;
238  }
239  else
240  {
241  if(!tmp_json.is_object())
242  {
243  log.warning() << "Provided JSON file for static-values is not a JSON "
244  << "object; it will be ignored." << messaget::eom;
245  }
246  else
247  static_values_json = std::move(to_json_object(tmp_json));
248  }
249  }
250 
252  options.get_bool_option("ignore-manifest-main-class");
253 
254  if(options.is_set("context-include") || options.is_set("context-exclude"))
255  method_context = get_context(options);
256 
257  should_lift_clinit_calls = options.get_bool_option("java-lift-clinit-calls");
258 }
259 
262 {
265  const auto &new_points = build_extra_entry_points(options);
266  language_options->extra_methods.insert(
267  language_options->extra_methods.end(),
268  new_points.begin(),
269  new_points.end());
270 }
271 
272 std::set<std::string> java_bytecode_languaget::extensions() const
273 {
274  return { "class", "jar" };
275 }
276 
277 void java_bytecode_languaget::modules_provided(std::set<std::string> &)
278 {
279  // modules.insert(translation_unit(parse_path));
280 }
281 
284  std::istream &,
285  const std::string &,
286  std::ostream &)
287 {
288  // there is no preprocessing!
289  return true;
290 }
291 
293  message_handlert &message_handler)
294 {
297 }
298 
300 {
302 
303  for(const auto &p : config.java.classpath)
305 
307  language_options->java_cp_include_files);
309  if(language_options->string_refinement_enabled)
310  {
312 
313  auto get_string_base_classes = [this](const irep_idt &id) {
315  };
316 
317  java_class_loader.set_extra_class_refs_function(get_string_base_classes);
318  }
319 }
320 
321 static void throwMainClassLoadingError(const std::string &main_class)
322 {
324  "Error: Could not find or load main class " + main_class);
325 }
326 
328 {
329  if(!main_class.empty())
330  {
331  // Try to load class
332  status() << "Trying to load Java main class: " << main_class << eom;
334  {
335  // Try to extract class name and load class
336  const auto maybe_class_name =
338  if(!maybe_class_name)
339  {
341  return;
342  }
343  status() << "Trying to load Java main class: " << maybe_class_name.value()
344  << eom;
345  if(!java_class_loader.can_load_class(maybe_class_name.value()))
346  {
348  return;
349  }
350  // Everything went well. We have a loadable main class.
351  // The entry point ('main') will be checked later.
353  main_class = maybe_class_name.value();
354  }
355  status() << "Found Java main class: " << main_class << eom;
356  // Now really load it.
357  const auto &parse_trees = java_class_loader(main_class);
358  if(parse_trees.empty() || !parse_trees.front().loading_successful)
359  {
361  }
362  }
363 }
364 
368 {
369  PRECONDITION(language_options.has_value());
373  return false;
374 }
375 
383  std::istream &instream,
384  const std::string &path)
385 {
386  PRECONDITION(language_options.has_value());
388 
389  // look at extension
390  if(has_suffix(path, ".jar"))
391  {
392  std::ifstream jar_file(path);
393  if(!jar_file.good())
394  {
396  "Error: Unable to access jarfile " + path);
397  }
398 
399  // build an object to potentially limit which classes are loaded
400  java_class_loader_limitt class_loader_limit(
401  get_message_handler(), language_options->java_cp_include_files);
403  {
404  // If we have an entry method, we can derive a main class.
405  if(config.main.has_value())
406  {
407  const std::string &entry_method = config.main.value();
408  const auto last_dot_position = entry_method.find_last_of('.');
409  main_class = entry_method.substr(0, last_dot_position);
410  }
411  else
412  {
413  auto manifest = java_class_loader.jar_pool(path).get_manifest();
414  std::string manifest_main_class = manifest["Main-Class"];
415 
416  // if the manifest declares a Main-Class line, we got a main class
417  if(
418  !manifest_main_class.empty() &&
419  !language_options->ignore_manifest_main_class)
420  {
421  main_class = manifest_main_class;
422  }
423  }
424  }
425  else
427 
428  // do we have one now?
429  if(main_class.empty())
430  {
431  status() << "JAR file without entry point: loading class files" << eom;
432  const auto classes = java_class_loader.load_entire_jar(path);
433  for(const auto &c : classes)
434  main_jar_classes.push_back(c);
435  }
436  else
438  }
439  else
441 
443  return false;
444 }
445 
456  const java_bytecode_parse_treet &parse_tree,
457  symbol_tablet &symbol_table)
458 {
459  namespacet ns(symbol_table);
460  for(const auto &method : parse_tree.parsed_class.methods)
461  {
462  for(const java_bytecode_parse_treet::instructiont &instruction :
463  method.instructions)
464  {
465  const std::string statement =
466  bytecode_info[instruction.bytecode].mnemonic;
467  if(statement == "getfield" || statement == "putfield")
468  {
469  const fieldref_exprt &fieldref =
470  expr_dynamic_cast<fieldref_exprt>(instruction.args[0]);
471  irep_idt class_symbol_id = fieldref.class_name();
472  const symbolt *class_symbol = symbol_table.lookup(class_symbol_id);
473  INVARIANT(
474  class_symbol != nullptr,
475  "all types containing fields should have been loaded");
476 
477  const java_class_typet *class_type =
478  &to_java_class_type(class_symbol->type);
479  const irep_idt &component_name = fieldref.component_name();
480  while(!class_type->has_component(component_name))
481  {
482  if(class_type->get_is_stub())
483  {
484  // Accessing a field of an incomplete (opaque) type.
485  symbolt &writable_class_symbol =
486  symbol_table.get_writeable_ref(class_symbol_id);
487  auto &components =
488  to_java_class_type(writable_class_symbol.type).components();
489  components.emplace_back(component_name, fieldref.type());
490  components.back().set_base_name(component_name);
491  components.back().set_pretty_name(component_name);
492  components.back().set_is_final(true);
493  break;
494  }
495  else
496  {
497  // Not present here: check the superclass.
498  INVARIANT(
499  !class_type->bases().empty(),
500  "class '" + id2string(class_symbol->name) +
501  "' (which was missing a field '" + id2string(component_name) +
502  "' referenced from method '" + id2string(method.name) +
503  "' of class '" + id2string(parse_tree.parsed_class.name) +
504  "') should have an opaque superclass");
505  const auto &superclass_type = class_type->bases().front().type();
506  class_symbol_id = superclass_type.get_identifier();
507  class_type = &to_java_class_type(ns.follow(superclass_type));
508  }
509  }
510  }
511  }
512  }
513 }
514 
521  const irep_idt &class_id, symbol_tablet &symbol_table)
522 {
523  struct_tag_typet java_lang_Class("java::java.lang.Class");
524  symbol_exprt symbol_expr(
526  java_lang_Class);
527  if(!symbol_table.has_symbol(symbol_expr.get_identifier()))
528  {
529  symbolt new_class_symbol;
530  new_class_symbol.name = symbol_expr.get_identifier();
531  new_class_symbol.type = symbol_expr.type();
532  INVARIANT(
533  has_prefix(id2string(new_class_symbol.name), "java::"),
534  "class identifier should have 'java::' prefix");
535  new_class_symbol.base_name =
536  id2string(new_class_symbol.name).substr(6);
537  new_class_symbol.mode = ID_java;
538  new_class_symbol.is_lvalue = true;
539  new_class_symbol.is_state_var = true;
540  new_class_symbol.is_static_lifetime = true;
541  new_class_symbol.type.set(ID_C_no_nondet_initialization, true);
542  symbol_table.add(new_class_symbol);
543  }
544 
545  return symbol_expr;
546 }
547 
563  const exprt &ldc_arg0,
564  symbol_tablet &symbol_table,
565  bool string_refinement_enabled)
566 {
567  if(ldc_arg0.id() == ID_type)
568  {
569  const irep_idt &class_id = ldc_arg0.type().get(ID_identifier);
570  return
572  get_or_create_class_literal_symbol(class_id, symbol_table));
573  }
574  else if(
575  const auto &literal =
576  expr_try_dynamic_cast<java_string_literal_exprt>(ldc_arg0))
577  {
579  *literal, symbol_table, string_refinement_enabled));
580  }
581  else
582  {
583  INVARIANT(
584  ldc_arg0.id() == ID_constant,
585  "ldc argument should be constant, string literal or class literal");
586  return ldc_arg0;
587  }
588 }
589 
600  java_bytecode_parse_treet &parse_tree,
601  symbol_tablet &symbol_table,
602  bool string_refinement_enabled)
603 {
604  for(auto &method : parse_tree.parsed_class.methods)
605  {
606  for(java_bytecode_parse_treet::instructiont &instruction :
607  method.instructions)
608  {
609  // ldc* instructions are Java bytecode "load constant" ops, which can
610  // retrieve a numeric constant, String literal, or Class literal.
611  const std::string statement =
612  bytecode_info[instruction.bytecode].mnemonic;
613  // clang-format off
614  if(statement == "ldc" ||
615  statement == "ldc2" ||
616  statement == "ldc_w" ||
617  statement == "ldc2_w")
618  {
619  // clang-format on
620  INVARIANT(
621  instruction.args.size() != 0,
622  "ldc instructions should have an argument");
623  instruction.args[0] =
625  instruction.args[0],
626  symbol_table,
627  string_refinement_enabled);
628  }
629  }
630  }
631 }
632 
645  symbol_table_baset &symbol_table,
646  const irep_idt &symbol_id,
647  const irep_idt &symbol_basename,
648  const typet &symbol_type,
649  const irep_idt &class_id,
650  bool force_nondet_init)
651 {
652  symbolt new_symbol;
653  new_symbol.is_static_lifetime = true;
654  new_symbol.is_lvalue = true;
655  new_symbol.is_state_var = true;
656  new_symbol.name = symbol_id;
657  new_symbol.base_name = symbol_basename;
658  new_symbol.type = symbol_type;
659  set_declaring_class(new_symbol, class_id);
660  // Public access is a guess; it encourages merging like-typed static fields,
661  // whereas a more restricted visbility would encourage separating them.
662  // Neither is correct, as without the class file we can't know the truth.
663  new_symbol.type.set(ID_C_access, ID_public);
664  // We set the field as final to avoid assuming they can be overridden.
665  new_symbol.type.set(ID_C_constant, true);
666  new_symbol.pretty_name = new_symbol.name;
667  new_symbol.mode = ID_java;
668  new_symbol.is_type = false;
669  // If pointer-typed, initialise to null and a static initialiser will be
670  // created to initialise on first reference. If primitive-typed, specify
671  // nondeterministic initialisation by setting a nil value.
672  if(symbol_type.id() == ID_pointer && !force_nondet_init)
673  new_symbol.value = null_pointer_exprt(to_pointer_type(symbol_type));
674  else
675  new_symbol.value.make_nil();
676  bool add_failed = symbol_table.add(new_symbol);
677  INVARIANT(
678  !add_failed, "caller should have checked symbol not already in table");
679 }
680 
690  const irep_idt &start_class_id,
691  const symbol_tablet &symbol_table,
692  const class_hierarchyt &class_hierarchy)
693 {
694  // Depth-first search: return the first stub ancestor, or irep_idt() if none
695  // found.
696  std::vector<irep_idt> classes_to_check;
697  classes_to_check.push_back(start_class_id);
698 
699  while(!classes_to_check.empty())
700  {
701  irep_idt to_check = classes_to_check.back();
702  classes_to_check.pop_back();
703 
704  // Exclude java.lang.Object because it can
705  if(
706  to_java_class_type(symbol_table.lookup_ref(to_check).type)
707  .get_is_stub() &&
708  to_check != "java::java.lang.Object")
709  {
710  return to_check;
711  }
712 
713  const class_hierarchyt::idst &parents =
714  class_hierarchy.class_map.at(to_check).parents;
715  classes_to_check.insert(
716  classes_to_check.end(), parents.begin(), parents.end());
717  }
718 
719  return irep_idt();
720 }
721 
732  const java_bytecode_parse_treet &parse_tree,
733  symbol_table_baset &symbol_table,
734  const class_hierarchyt &class_hierarchy,
735  messaget &log)
736 {
737  namespacet ns(symbol_table);
738  for(const auto &method : parse_tree.parsed_class.methods)
739  {
740  for(const java_bytecode_parse_treet::instructiont &instruction :
741  method.instructions)
742  {
743  const std::string statement =
744  bytecode_info[instruction.bytecode].mnemonic;
745  if(statement == "getstatic" || statement == "putstatic")
746  {
747  INVARIANT(
748  instruction.args.size() > 0,
749  "get/putstatic should have at least one argument");
750  const fieldref_exprt &field_ref =
751  expr_dynamic_cast<fieldref_exprt>(instruction.args[0]);
752  irep_idt component = field_ref.component_name();
753  irep_idt class_id = field_ref.class_name();
754 
755  // The final 'true' parameter here includes interfaces, as they can
756  // define static fields.
757  const auto referred_component =
758  get_inherited_component(class_id, component, symbol_table, true);
759  if(!referred_component)
760  {
761  // Create a new stub global on an arbitrary incomplete ancestor of the
762  // class that was referred to. This is just a guess, but we have no
763  // better information to go on.
764  irep_idt add_to_class_id =
766  class_id, symbol_table, class_hierarchy);
767 
768  // If there are no incomplete ancestors to ascribe the missing field
769  // to, we must have an incomplete model of a class or simply a
770  // version mismatch of some kind. Normally this would be an error, but
771  // our models library currently triggers this error in some cases
772  // (notably java.lang.System, which is missing System.in/out/err).
773  // Therefore for this case we ascribe the missing field to the class
774  // it was directly referenced from, and fall back to initialising the
775  // field in __CPROVER_initialize, rather than try to create or augment
776  // a clinit method for a non-stub class.
777 
778  bool no_incomplete_ancestors = add_to_class_id.empty();
779  if(no_incomplete_ancestors)
780  {
781  add_to_class_id = class_id;
782 
783  // TODO forbid this again once the models library has been checked
784  // for missing static fields.
785  log.warning() << "Stub static field " << component << " found for "
786  << "non-stub type " << class_id << ". In future this "
787  << "will be a fatal error." << messaget::eom;
788  }
789 
790  irep_idt identifier =
791  id2string(add_to_class_id) + "." + id2string(component);
792 
794  symbol_table,
795  identifier,
796  component,
797  instruction.args[0].type(),
798  add_to_class_id,
799  no_incomplete_ancestors);
800  }
801  }
802  }
803  }
804 }
805 
807  symbol_tablet &symbol_table,
808  const std::string &)
809 {
810  PRECONDITION(language_options.has_value());
811  // There are various cases in the Java front-end where pre-existing symbols
812  // from a previous load are not handled. We just rule this case out for now;
813  // a user wishing to ensure a particular class is loaded should use
814  // --java-load-class (to force class-loading) or
815  // --lazy-methods-extra-entry-point (to ensure a method body is loaded)
816  // instead of creating two instances of the front-end.
817  INVARIANT(
818  symbol_table.begin() == symbol_table.end(),
819  "the Java front-end should only be used with an empty symbol table");
820 
821  java_internal_additions(symbol_table);
822  create_java_initialize(symbol_table);
823 
824  if(language_options->string_refinement_enabled)
826 
827  // Must load java.lang.Object first to avoid stubbing
828  // This ordering could alternatively be enforced by
829  // moving the code below to the class loader.
830  java_class_loadert::parse_tree_with_overridest_mapt::const_iterator it =
831  java_class_loader.get_class_with_overlays_map().find("java.lang.Object");
833  {
835  it->second,
836  symbol_table,
838  language_options->max_user_array_length,
841  language_options->no_load_classes))
842  {
843  return true;
844  }
845  }
846 
847  // first generate a new struct symbol for each class and a new function symbol
848  // for every method
849  for(const auto &class_trees : java_class_loader.get_class_with_overlays_map())
850  {
851  if(class_trees.second.front().parsed_class.name.empty())
852  continue;
853 
855  class_trees.second,
856  symbol_table,
858  language_options->max_user_array_length,
861  language_options->no_load_classes))
862  {
863  return true;
864  }
865  }
866 
867  // Register synthetic method that replaces a real definition if one is
868  // available:
869  if(symbol_table.has_symbol(get_create_array_with_type_name()))
870  {
873  }
874 
875  // Now add synthetic classes for every invokedynamic instruction found (it
876  // makes this easier that all interface types and their methods have been
877  // created above):
878  for(const auto &id_and_symbol : symbol_table)
879  {
880  const auto &symbol = id_and_symbol.second;
881  const auto &id = symbol.name;
882  if(can_cast_type<code_typet>(symbol.type) && method_bytecode.get(id))
883  {
885  id,
886  method_bytecode.get(id)->get().method.instructions,
887  symbol_table,
890  }
891  }
892 
893  // Now that all classes have been created in the symbol table we can populate
894  // the class hierarchy:
895  class_hierarchy(symbol_table);
896 
897  // find and mark all implicitly generic class types
898  // this can only be done once all the class symbols have been created
899  for(const auto &c : java_class_loader.get_class_with_overlays_map())
900  {
901  if(c.second.front().parsed_class.name.empty())
902  continue;
903  try
904  {
906  c.second.front().parsed_class.name, symbol_table);
907  }
909  {
911  << "Not marking class " << c.first
912  << " implicitly generic due to missing outer class symbols"
913  << messaget::eom;
914  }
915  }
916 
917  // Infer fields on opaque types based on the method instructions just loaded.
918  // For example, if we don't have bytecode for field x of class A, but we can
919  // see an int-typed getfield instruction referring to it, add that field now.
920  for(auto &class_to_trees : java_class_loader.get_class_with_overlays_map())
921  {
922  for(const java_bytecode_parse_treet &parse_tree : class_to_trees.second)
923  infer_opaque_type_fields(parse_tree, symbol_table);
924  }
925 
926  // Create global variables for constants (String and Class literals) up front.
927  // This means that when running with lazy loading, we will be aware of these
928  // literal globals' existence when __CPROVER_initialize is generated in
929  // `generate_support_functions`.
930  const std::size_t before_constant_globals_size = symbol_table.symbols.size();
931  for(auto &class_to_trees : java_class_loader.get_class_with_overlays_map())
932  {
933  for(java_bytecode_parse_treet &parse_tree : class_to_trees.second)
934  {
936  parse_tree, symbol_table, language_options->string_refinement_enabled);
937  }
938  }
939  status() << "Java: added "
940  << (symbol_table.symbols.size() - before_constant_globals_size)
941  << " String or Class constant symbols"
942  << messaget::eom;
943 
944  // For each reference to a stub global (that is, a global variable declared on
945  // a class we don't have bytecode for, and therefore don't know the static
946  // initialiser for), create a synthetic static initialiser (clinit method)
947  // to nondet initialise it.
948  // Note this must be done before making static initialiser wrappers below, as
949  // this makes a Classname.clinit method, then the next pass makes a wrapper
950  // that ensures it is only run once, and that static initialisation happens
951  // in class-graph topological order.
952 
953  {
954  journalling_symbol_tablet symbol_table_journal =
955  journalling_symbol_tablet::wrap(symbol_table);
956  for(auto &class_to_trees : java_class_loader.get_class_with_overlays_map())
957  {
958  for(const java_bytecode_parse_treet &parse_tree : class_to_trees.second)
959  {
961  parse_tree, symbol_table_journal, class_hierarchy, *this);
962  }
963  }
964 
966  symbol_table, symbol_table_journal.get_inserted(), synthetic_methods);
967  }
968 
970  symbol_table,
972  language_options->threading_support,
973  language_options->static_values_json.has_value());
974 
976 
977  // Now incrementally elaborate methods
978  // that are reachable from this entry point.
979  switch(language_options->lazy_methods_mode)
980  {
982  // ci = context-insensitive
983  if(do_ci_lazy_method_conversion(symbol_table))
984  return true;
985  break;
987  {
988  symbol_table_buildert symbol_table_builder =
989  symbol_table_buildert::wrap(symbol_table);
990 
991  journalling_symbol_tablet journalling_symbol_table =
992  journalling_symbol_tablet::wrap(symbol_table_builder);
993 
994  // Convert all synthetic methods:
995  for(const auto &function_id_and_type : synthetic_methods)
996  {
998  function_id_and_type.first,
999  journalling_symbol_table,
1001  }
1002  // Convert all methods for which we have bytecode now
1003  for(const auto &method_sig : method_bytecode)
1004  {
1006  method_sig.first, journalling_symbol_table, class_to_declared_symbols);
1007  }
1009  INITIALIZE_FUNCTION, journalling_symbol_table, class_to_declared_symbols);
1010  // Now convert all newly added string methods
1011  for(const auto &fn_name : journalling_symbol_table.get_inserted())
1012  {
1014  convert_single_method(fn_name, symbol_table, class_to_declared_symbols);
1015  }
1016  }
1017  break;
1019  // Our caller is in charge of elaborating methods on demand.
1020  break;
1021  }
1022 
1023  // now instrument runtime exceptions
1025  symbol_table,
1026  language_options->throw_runtime_exceptions,
1028 
1029  // now typecheck all
1030  bool res = java_bytecode_typecheck(
1031  symbol_table,
1033  language_options->string_refinement_enabled);
1034 
1035  // now instrument thread-blocks and synchronized methods.
1036  if(language_options->threading_support)
1037  {
1038  convert_threadblock(symbol_table);
1040  }
1041 
1042  return res;
1043 }
1044 
1046  symbol_tablet &symbol_table)
1047 {
1048  PRECONDITION(language_options.has_value());
1049 
1050  symbol_table_buildert symbol_table_builder =
1051  symbol_table_buildert::wrap(symbol_table);
1052 
1055  if(!res.is_success())
1056  return res.is_error();
1057 
1058  // Load the main function into the symbol table to get access to its
1059  // parameter names
1060  convert_lazy_method(res.main_function.name, symbol_table_builder);
1061 
1062  const symbolt &symbol =
1063  symbol_table_builder.lookup_ref(res.main_function.name);
1064  if(symbol.value.is_nil())
1065  {
1067  "the program has no entry point",
1068  "function",
1069  "Check that the specified entry point is included by your "
1070  "--context-include or --context-exclude options");
1071  }
1072 
1073  // generate the test harness in __CPROVER__start and a call the entry point
1074  return java_entry_point(
1075  symbol_table_builder,
1076  main_class,
1078  language_options->assume_inputs_non_null,
1079  language_options->assert_uncaught_exceptions,
1082  language_options->string_refinement_enabled,
1083  [&](const symbolt &function, symbol_table_baset &symbol_table) {
1084  return java_build_arguments(
1085  function,
1086  symbol_table,
1087  language_options->assume_inputs_non_null,
1088  object_factory_parameters,
1089  get_pointer_type_selector(),
1090  get_message_handler());
1091  });
1092 }
1093 
1106  symbol_tablet &symbol_table)
1107 {
1108  symbol_table_buildert symbol_table_builder =
1109  symbol_table_buildert::wrap(symbol_table);
1110 
1112 
1113  const method_convertert method_converter =
1114  [this, &symbol_table_builder, &class_to_declared_symbols](
1115  const irep_idt &function_id,
1116  ci_lazy_methods_neededt lazy_methods_needed) {
1117  return convert_single_method(
1118  function_id,
1119  symbol_table_builder,
1120  std::move(lazy_methods_needed),
1122  };
1123 
1124  ci_lazy_methodst method_gather(
1125  symbol_table,
1126  main_class,
1128  language_options->extra_methods,
1130  language_options->java_load_classes,
1134 
1135  return method_gather(symbol_table, method_bytecode, method_converter);
1136 }
1137 
1138 const select_pointer_typet &
1140 {
1141  PRECONDITION(pointer_type_selector.get()!=nullptr);
1142  return *pointer_type_selector;
1143 }
1144 
1151  std::unordered_set<irep_idt> &methods) const
1152 {
1153  const std::string cprover_class_prefix = "java::org.cprover.CProver.";
1154 
1155  // Add all string solver methods to map
1157  // Add all concrete methods to map
1158  for(const auto &kv : method_bytecode)
1159  methods.insert(kv.first);
1160  // Add all synthetic methods to map
1161  for(const auto &kv : synthetic_methods)
1162  methods.insert(kv.first);
1163  methods.insert(INITIALIZE_FUNCTION);
1164 }
1165 
1175  const irep_idt &function_id,
1176  symbol_table_baset &symtab)
1177 {
1178  const symbolt &symbol = symtab.lookup_ref(function_id);
1179  if(symbol.value.is_not_nil())
1180  return;
1181 
1182  journalling_symbol_tablet symbol_table=
1184 
1186  convert_single_method(function_id, symbol_table, class_to_declared_symbols);
1187 
1188  // Instrument runtime exceptions (unless symbol is a stub or is the
1189  // INITIALISE_FUNCTION).
1190  if(symbol.value.is_not_nil() && function_id != INITIALIZE_FUNCTION)
1191  {
1193  symbol_table,
1194  symbol_table.get_writeable_ref(function_id),
1195  language_options->throw_runtime_exceptions,
1197  }
1198 
1199  // now typecheck this function
1201  symbol_table,
1203  language_options->string_refinement_enabled);
1204 }
1205 
1213  const codet &function_body,
1214  optionalt<ci_lazy_methods_neededt> needed_lazy_methods)
1215 {
1216  if(needed_lazy_methods)
1217  {
1218  for(const_depth_iteratort it = function_body.depth_cbegin();
1219  it != function_body.depth_cend();
1220  ++it)
1221  {
1222  if(it->id() == ID_code)
1223  {
1224  const auto fn_call = expr_try_dynamic_cast<code_function_callt>(*it);
1225  if(!fn_call)
1226  continue;
1227  // Only support non-virtual function calls for now, if string solver
1228  // starts to introduce virtual function calls then we will need to
1229  // duplicate the behavior of java_bytecode_convert_method where it
1230  // handles the invokevirtual instruction
1231  const symbol_exprt &fn_sym =
1232  expr_dynamic_cast<symbol_exprt>(fn_call->function());
1233  needed_lazy_methods->add_needed_method(fn_sym.get_identifier());
1234  }
1235  else if(
1236  it->id() == ID_side_effect &&
1237  to_side_effect_expr(*it).get_statement() == ID_function_call)
1238  {
1239  const auto &call_expr = to_side_effect_expr_function_call(*it);
1240  const symbol_exprt &fn_sym =
1241  expr_dynamic_cast<symbol_exprt>(call_expr.function());
1242  needed_lazy_methods->add_needed_method(fn_sym.get_identifier());
1243  }
1244  }
1245  }
1246 }
1247 
1261  const irep_idt &function_id,
1262  symbol_table_baset &symbol_table,
1263  optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
1265 {
1266  const symbolt &symbol = symbol_table.lookup_ref(function_id);
1267 
1268  // Nothing to do if body is already loaded
1269  if(symbol.value.is_not_nil())
1270  return false;
1271 
1272  if(function_id == INITIALIZE_FUNCTION)
1273  {
1275  symbol_table,
1276  symbol.location,
1277  language_options->assume_inputs_non_null,
1280  language_options->string_refinement_enabled,
1282  return false;
1283  }
1284 
1285  INVARIANT(declaring_class(symbol), "Method must have a declaring class.");
1286 
1287  bool ret = convert_single_method_code(
1288  function_id, symbol_table, needed_lazy_methods, class_to_declared_symbols);
1289 
1290  if(symbol.value.is_not_nil() && language_options->should_lift_clinit_calls)
1291  {
1292  auto &writable_symbol = symbol_table.get_writeable_ref(function_id);
1293  writable_symbol.value =
1294  lift_clinit_calls(std::move(to_code(writable_symbol.value)));
1295  }
1296 
1297  INVARIANT(declaring_class(symbol), "Method must have a declaring class.");
1298 
1299  return ret;
1300 }
1301 
1314  const irep_idt &function_id,
1315  symbol_table_baset &symbol_table,
1316  optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
1318 {
1319  const auto &symbol = symbol_table.lookup_ref(function_id);
1320  PRECONDITION(symbol.value.is_nil());
1321 
1322  // Get bytecode for specified function if we have it
1323  method_bytecodet::opt_reft cmb = method_bytecode.get(function_id);
1324 
1325  synthetic_methods_mapt::iterator synthetic_method_it;
1326 
1327  // Check if have a string solver implementation
1328  if(string_preprocess.implements_function(function_id))
1329  {
1330  symbolt &writable_symbol = symbol_table.get_writeable_ref(function_id);
1331  // Load parameter names from any extant bytecode before filling in body
1332  if(cmb)
1333  {
1335  writable_symbol, cmb->get().method.local_variable_table, symbol_table);
1336  }
1337  // Populate body of the function with code generated by string preprocess
1338  codet generated_code =
1339  string_preprocess.code_for_function(writable_symbol, symbol_table);
1340  // String solver can make calls to functions that haven't yet been seen.
1341  // Add these to the needed_lazy_methods collection
1342  notify_static_method_calls(generated_code, needed_lazy_methods);
1343  writable_symbol.value = std::move(generated_code);
1344  return false;
1345  }
1346  else if(
1347  (synthetic_method_it = synthetic_methods.find(function_id)) !=
1348  synthetic_methods.end())
1349  {
1350  // Synthetic method (i.e. one generated by the Java frontend and which
1351  // doesn't occur in the source bytecode):
1352  symbolt &writable_symbol = symbol_table.get_writeable_ref(function_id);
1353  switch(synthetic_method_it->second)
1354  {
1356  if(language_options->threading_support)
1357  writable_symbol.value = get_thread_safe_clinit_wrapper_body(
1358  function_id,
1359  symbol_table,
1360  language_options->nondet_static,
1361  language_options->static_values_json.has_value(),
1365  else
1366  writable_symbol.value = get_clinit_wrapper_body(
1367  function_id,
1368  symbol_table,
1369  language_options->nondet_static,
1370  language_options->static_values_json.has_value(),
1374  break;
1376  {
1377  const auto class_name =
1378  declaring_class(symbol_table.lookup_ref(function_id));
1379  INVARIANT(
1380  class_name, "user_specified_clinit must be declared by a class.");
1381  INVARIANT(
1382  language_options->static_values_json.has_value(),
1383  "static-values JSON must be available");
1384  writable_symbol.value = get_user_specified_clinit_body(
1385  *class_name,
1386  *language_options->static_values_json,
1387  symbol_table,
1388  needed_lazy_methods,
1389  language_options->max_user_array_length,
1390  references,
1391  class_to_declared_symbols.get(symbol_table));
1392  break;
1393  }
1395  writable_symbol.value =
1397  function_id,
1398  symbol_table,
1402  break;
1404  writable_symbol.value = invokedynamic_synthetic_constructor(
1405  function_id, symbol_table, get_message_handler());
1406  break;
1408  writable_symbol.value = invokedynamic_synthetic_method(
1409  function_id, symbol_table, get_message_handler());
1410  break;
1412  {
1413  INVARIANT(
1414  cmb,
1415  "CProver.createArrayWithType should only be registered if "
1416  "we have a real implementation available");
1418  writable_symbol, cmb->get().method.local_variable_table, symbol_table);
1419  writable_symbol.value = create_array_with_type_body(
1420  function_id, symbol_table, get_message_handler());
1421  break;
1422  }
1423  }
1424  // Notify lazy methods of static calls made from the newly generated
1425  // function:
1427  to_code(writable_symbol.value), needed_lazy_methods);
1428  return false;
1429  }
1430 
1431  // No string solver or static init wrapper implementation;
1432  // check if have bytecode for it
1433  if(cmb)
1434  {
1436  symbol_table.lookup_ref(cmb->get().class_id),
1437  cmb->get().method,
1438  symbol_table,
1440  language_options->max_user_array_length,
1441  language_options->throw_assertion_error,
1442  std::move(needed_lazy_methods),
1445  language_options->threading_support,
1446  language_options->method_context,
1447  language_options->assert_no_exceptions_thrown);
1448  return false;
1449  }
1450 
1451  if(needed_lazy_methods)
1452  {
1453  // The return of an opaque function is a source of an otherwise invisible
1454  // instantiation, so here we ensure we've loaded the appropriate classes.
1455  const java_method_typet function_type = to_java_method_type(symbol.type);
1456  if(
1457  const pointer_typet *pointer_return_type =
1458  type_try_dynamic_cast<pointer_typet>(function_type.return_type()))
1459  {
1460  // If the return type is abstract, we won't forcibly instantiate it here
1461  // otherwise this can cause abstract methods to be explictly called
1462  // TODO(tkiley): Arguably no abstract class should ever be added to
1463  // TODO(tkiley): ci_lazy_methods_neededt, but this needs further
1464  // TODO(tkiley): investigation
1465  namespacet ns{symbol_table};
1466  const java_class_typet &underlying_type =
1467  to_java_class_type(ns.follow(pointer_return_type->subtype()));
1468 
1469  if(!underlying_type.is_abstract())
1470  needed_lazy_methods->add_all_needed_classes(*pointer_return_type);
1471  }
1472  }
1473 
1474  return true;
1475 }
1476 
1478 {
1479  PRECONDITION(language_options.has_value());
1480  return false;
1481 }
1482 
1484 {
1487  parse_trees.front().output(out);
1488  if(parse_trees.size() > 1)
1489  {
1490  out << "\n\nClass has the following overlays:\n\n";
1491  for(auto parse_tree_it = std::next(parse_trees.begin());
1492  parse_tree_it != parse_trees.end();
1493  ++parse_tree_it)
1494  {
1495  parse_tree_it->output(out);
1496  }
1497  out << "End of class overlays.\n";
1498  }
1499 }
1500 
1501 std::unique_ptr<languaget> new_java_bytecode_language()
1502 {
1503  return util_make_unique<java_bytecode_languaget>();
1504 }
1505 
1507  const exprt &expr,
1508  std::string &code,
1509  const namespacet &ns)
1510 {
1511  code=expr2java(expr, ns);
1512  return false;
1513 }
1514 
1516  const typet &type,
1517  std::string &code,
1518  const namespacet &ns)
1519 {
1520  code=type2java(type, ns);
1521  return false;
1522 }
1523 
1525  const std::string &code,
1526  const std::string &module,
1527  exprt &expr,
1528  const namespacet &ns)
1529 {
1530 #if 0
1531  expr.make_nil();
1532 
1533  // no preprocessing yet...
1534 
1535  std::istringstream i_preprocessed(code);
1536 
1537  // parsing
1538 
1539  java_bytecode_parser.clear();
1540  java_bytecode_parser.filename="";
1541  java_bytecode_parser.in=&i_preprocessed;
1542  java_bytecode_parser.set_message_handler(message_handler);
1543  java_bytecode_parser.grammar=java_bytecode_parsert::EXPRESSION;
1544  java_bytecode_parser.mode=java_bytecode_parsert::GCC;
1545  java_bytecode_scanner_init();
1546 
1547  bool result=java_bytecode_parser.parse();
1548 
1549  if(java_bytecode_parser.parse_tree.items.empty())
1550  result=true;
1551  else
1552  {
1553  expr=java_bytecode_parser.parse_tree.items.front().value();
1554 
1555  result=java_bytecode_convert(expr, "", message_handler);
1556 
1557  // typecheck it
1558  if(!result)
1560  }
1561 
1562  // save some memory
1563  java_bytecode_parser.clear();
1564 
1565  return result;
1566 #else
1567  // unused parameters
1568  (void)code;
1569  (void)module;
1570  (void)expr;
1571  (void)ns;
1572 #endif
1573 
1574  return true; // fail for now
1575 }
1576 
1578 {
1579 }
1580 
1584 std::vector<load_extra_methodst>
1586 {
1587  (void)options; // unused parameter
1588  return {};
1589 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:152
create_array_with_type_body
codet create_array_with_type_body(const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler)
Returns the internal implementation for org.cprover.CProver.createArrayWithType.
Definition: create_array_with_type_intrinsic.cpp:39
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
java_bytecode_parse_treet::instructiont::args
argst args
Definition: java_bytecode_parse_tree.h:61
symbol_table_baset::has_symbol
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
Definition: symbol_table_base.h:87
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
java_bytecode_languaget::method_bytecode
method_bytecodet method_bytecode
Definition: java_bytecode_language.h:382
java_bytecode_languaget::convert_single_method_code
bool convert_single_method_code(const irep_idt &function_id, symbol_table_baset &symbol_table, optionalt< ci_lazy_methods_neededt > needed_lazy_methods, lazy_class_to_declared_symbols_mapt &class_to_declared_symbols)
Convert a method (one whose type is known but whose body hasn't been converted) but don't run typeche...
Definition: java_bytecode_language.cpp:1313
JAVA_CLASS_MODEL_SUFFIX
#define JAVA_CLASS_MODEL_SUFFIX
Definition: java_bytecode_language.h:272
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:272
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 bool replace_clinit, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, message_handlert &message_handler)
Produces the static initializer wrapper body for the given function.
Definition: java_static_initializers.cpp:712
lazy_class_to_declared_symbols_mapt::reinitialize
void reinitialize()
Definition: java_bytecode_language.cpp:137
symbolt::is_state_var
bool is_state_var
Definition: symbol.h:62
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
exprt::depth_cbegin
const_depth_iteratort depth_cbegin() const
Definition: expr.cpp:339
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:104
configt::javat::main_class
irep_idt main_class
Definition: config.h:158
LAZY_METHODS_MODE_EAGER
@ LAZY_METHODS_MODE_EAGER
Definition: java_bytecode_language.h:186
java_bytecode_language_optionst::method_context
optionalt< prefix_filtert > method_context
If set, method bodies are only elaborated if they pass the filter.
Definition: java_bytecode_language.h:261
to_side_effect_expr_function_call
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Definition: std_code.h:2192
class_hierarchyt
Non-graph-based representation of the class hierarchy.
Definition: class_hierarchy.h:43
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, message_handlert &message_handler)
Create the body of a synthetic static initializer (clinit method), which initialise stub globals in t...
Definition: java_static_initializers.cpp:999
java_bytecode_language.h
invokedynamic_synthetic_method
codet invokedynamic_synthetic_method(const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler)
Create invokedynamic synthetic method.
Definition: lambda_synthesis.cpp:441
bytecode_infot::mnemonic
const char * mnemonic
Definition: bytecode_info.h:46
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:56
journalling_symbol_tablet::wrap
static journalling_symbol_tablet wrap(symbol_table_baset &base_symbol_table)
Definition: journalling_symbol_table.h:80
lift_clinit_calls
codet lift_clinit_calls(codet input)
file Static initializer call lifting
Definition: lift_clinit_calls.cpp:19
cmdlinet::isset
virtual bool isset(char option) const
Definition: cmdline.cpp:28
main_function_resultt::main_function
symbolt main_function
Definition: java_entry_point.h:94
java_bytecode_languaget::pointer_type_selector
const std::unique_ptr< const select_pointer_typet > pointer_type_selector
Definition: java_bytecode_language.h:388
prefix_filtert
Provides filtering of strings vai inclusion/exclusion lists of prefixes.
Definition: prefix_filter.h:20
class_typet::is_abstract
bool is_abstract() const
Definition: std_types.h:353
java_bytecode_parse_treet
Definition: java_bytecode_parse_tree.h:23
set_declaring_class
void set_declaring_class(symbolt &symbol, const irep_idt &declaring_class)
Sets the identifier of the class which declared a given symbol to declaring_class.
Definition: java_utils.cpp:506
java_bytecode_language_optionst::should_lift_clinit_calls
bool should_lift_clinit_calls
Should we lift clinit calls in function bodies to the top? For example, turning if(x) A....
Definition: java_bytecode_language.h:266
optionst
Definition: options.h:23
irept::make_nil
void make_nil()
Definition: irep.h:475
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:393
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:1524
typet
The type of an expression, extends irept.
Definition: type.h:29
optionst::get_option
const std::string get_option(const std::string &option) const
Definition: options.cpp:67
messaget::status
mstreamt & status() const
Definition: message.h:400
java_bytecode_language_optionst::java_bytecode_language_optionst
java_bytecode_language_optionst()=default
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:514
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
lazy_class_to_declared_symbols_mapt::initialized
bool initialized
Definition: java_bytecode_language.h:212
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:1150
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 bool replace_clinit, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, message_handlert &message_handler)
Thread safe version of the static initializer.
Definition: java_static_initializers.cpp:516
fieldref_exprt
Represents the argument of an instruction that uses a CONSTANT_Fieldref This is used for example as a...
Definition: java_bytecode_parse_tree.h:329
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_bytecode_languaget::language_options
optionalt< java_bytecode_language_optionst > language_options
Definition: java_bytecode_language.h:377
java_bytecode_parse_treet::instructiont::bytecode
u8 bytecode
Definition: java_bytecode_parse_tree.h:59
create_invokedynamic_synthetic_classes
void create_invokedynamic_synthetic_classes(const irep_idt &method_identifier, const java_bytecode_parse_treet::methodt::instructionst &instructions, symbol_tablet &symbol_table, synthetic_methods_mapt &synthetic_methods, message_handlert &message_handler)
Definition: lambda_synthesis.cpp:297
declaring_class
optionalt< irep_idt > declaring_class(const symbolt &symbol)
Gets the identifier of the class which declared a given symbol.
Definition: java_utils.cpp:500
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:202
prefix.h
new_java_bytecode_language
std::unique_ptr< languaget > new_java_bytecode_language()
Definition: java_bytecode_language.cpp:1501
configt::main
optionalt< std::string > main
Definition: config.h:173
invariant.h
java_string_literal_expr.h
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:56
java_bytecode_languaget::main_class
irep_idt main_class
Definition: java_bytecode_language.h:378
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:1212
synthetic_method_typet::INVOKEDYNAMIC_CAPTURE_CONSTRUCTOR
@ INVOKEDYNAMIC_CAPTURE_CONSTRUCTOR
A generated constructor for a class capturing the parameters of an invokedynamic instruction.
synthetic_method_typet::INVOKEDYNAMIC_METHOD
@ INVOKEDYNAMIC_METHOD
A generated method for a class capturing the parameters of an invokedynamic instruction.
exprt
Base class for all expressions.
Definition: expr.h:53
java_string_library_preprocesst::implements_function
bool implements_function(const irep_idt &function_id) const
Definition: java_string_library_preprocess.cpp:1374
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:455
journalling_symbol_table.h
Author: Diffblue Ltd.
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
create_static_initializer_symbols
void create_static_initializer_symbols(symbol_tablet &symbol_table, synthetic_methods_mapt &synthetic_methods, const bool thread_safe, const bool is_user_clinit_needed)
Create static initializer wrappers and possibly user-specified functions for initial static field val...
Definition: java_static_initializers.cpp:867
java_bytecode_languaget::references
std::unordered_map< std::string, object_creation_referencet > references
Map used in all calls to functions that deterministically create objects (currently only assign_from_...
Definition: java_bytecode_language.h:401
struct_tag_typet
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:490
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:1515
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
invalid_source_file_exceptiont
Thrown when we can't handle something in an input source file.
Definition: exception_utils.h:171
options.h
component
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:192
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, const optionalt< prefix_filtert > &method_context, bool assert_no_exceptions_thrown)
Definition: java_bytecode_convert_method.cpp:3225
java_string_library_preprocesst::initialize_known_type_table
void initialize_known_type_table()
Definition: java_string_library_preprocess.cpp:1461
optionst::set_option
void set_option(const std::string &option, const bool value)
Definition: options.cpp:28
fieldref_exprt::component_name
irep_idt component_name() const
Definition: java_bytecode_parse_tree.h:346
irep_idt
dstringt irep_idt
Definition: irep.h:32
messaget::eom
static eomt eom
Definition: message.h:283
to_side_effect_expr
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1941
method_convertert
std::function< bool(const irep_idt &function_id, ci_lazy_methods_neededt)> method_convertert
Definition: ci_lazy_methods.h:92
to_json_array
json_arrayt & to_json_array(jsont &json)
Definition: json.h:424
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
get_or_create_string_literal_symbol
symbol_exprt get_or_create_string_literal_symbol(const java_string_literal_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:38
has_suffix
bool has_suffix(const std::string &s, const std::string &suffix)
Definition: suffix.h:17
java_bytecode_languaget::final
virtual bool final(symbol_table_baset &context) override
Final adjustments, e.g.
Definition: java_bytecode_language.cpp:1477
jsont
Definition: json.h:25
class_to_declared_symbols
std::unordered_multimap< irep_idt, symbolt > class_to_declared_symbols(const symbol_tablet &symbol_table)
Definition: java_static_initializers.cpp:772
configt::javat::classpath
classpatht classpath
Definition: config.h:157
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:54
java_object_factory_parameterst::set
void set(const optionst &)
Assigns the parameters from given options.
Definition: java_object_factory_parameters.cpp:17
symbol_tablet::begin
virtual iteratort begin() override
Definition: symbol_table.h:114
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:183
class_name_from_method_name
NODISCARD optionalt< std::string > class_name_from_method_name(const std::string &method_name)
Get JVM type name of the class in which method_name is defined.
Definition: java_utils.cpp:512
java_bytecode_languaget::stub_global_initializer_factory
stub_global_initializer_factoryt stub_global_initializer_factory
Definition: java_bytecode_language.h:394
main_function_resultt::is_error
bool is_error() const
Definition: java_entry_point.h:113
main_function_resultt::is_success
bool is_success() const
Definition: java_entry_point.h:109
symbolt::pretty_name
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
java_class_typet
Definition: java_types.h:199
to_code
const codet & to_code(const exprt &expr)
Definition: std_code.h:158
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:689
java_bytecode_language_optionst::lazy_methods_mode
lazy_methods_modet lazy_methods_mode
Definition: java_bytecode_language.h:238
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
get_user_specified_clinit_body
code_blockt get_user_specified_clinit_body(const irep_idt &class_id, const json_objectt &static_values_json, symbol_table_baset &symbol_table, optionalt< ci_lazy_methods_neededt > needed_lazy_methods, size_t max_user_array_length, std::unordered_map< std::string, object_creation_referencet > &references, const std::unordered_multimap< irep_idt, symbolt > &class_to_declared_symbols_map)
Create the body of a user_specified_clinit function for a given class, which includes assignments for...
Definition: java_static_initializers.cpp:784
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:644
string2int.h
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
const_depth_iteratort
Definition: expr_iterator.h:216
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:402
can_cast_type< code_typet >
bool can_cast_type< code_typet >(const typet &type)
Check whether a reference to a typet is a code_typet.
Definition: std_types.h:933
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:261
cmdlinet
Definition: cmdline.h:21
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:1585
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
messaget::result
mstreamt & result() const
Definition: message.h:395
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_class_loadert::set_java_cp_include_files
void set_java_cp_include_files(const std::string &cp_include_files)
Set the argument of the class loader limit java_class_loader_limitt.
Definition: java_class_loader.h:56
java_bytecode_languaget::main_jar_classes
std::vector< irep_idt > main_jar_classes
Definition: java_bytecode_language.h:379
synthetic_method_typet::USER_SPECIFIED_STATIC_INITIALIZER
@ USER_SPECIFIED_STATIC_INITIALIZER
Only exists if the --static-values option was used.
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:511
symbol_tablet::end
virtual iteratort end() override
Definition: symbol_table.h:118
null_pointer_exprt
The null pointer constant.
Definition: std_expr.h:4018
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:121
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:1577
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:562
java_bytecode_languaget::java_class_loader
java_class_loadert java_class_loader
Definition: java_bytecode_language.h:380
java_bytecode_parse_treet::classt::name
irep_idt name
Definition: java_bytecode_parse_tree.h:212
java_bytecode_language_optionst::ignore_manifest_main_class
bool ignore_manifest_main_class
Definition: java_bytecode_language.h:230
java_static_lifetime_init
void java_static_lifetime_init(symbol_table_baset &symbol_table, const source_locationt &source_location, bool assume_init_pointers_not_null, java_object_factory_parameterst object_factory_parameters, const select_pointer_typet &pointer_type_selector, bool string_refinement_enabled, message_handlert &message_handler)
Adds the body to __CPROVER_initialize.
Definition: java_entry_point.cpp:106
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:1181
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:62
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:22
java_bytecode_languaget::do_ci_lazy_method_conversion
bool do_ci_lazy_method_conversion(symbol_tablet &)
Uses a simple context-insensitive ('ci') analysis to determine which methods may be reachable from th...
Definition: java_bytecode_language.cpp:1105
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:1398
create_array_with_type_intrinsic.h
java_bytecode_languaget::show_parse
void show_parse(std::ostream &out) override
Definition: java_bytecode_language.cpp:1483
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:1413
java_bytecode_language_optionst::java_load_classes
std::vector< irep_idt > java_load_classes
list of classes to force load even without reference from the entry point
Definition: java_bytecode_language.h:242
get_context
prefix_filtert get_context(const optionst &options)
Definition: java_bytecode_language.cpp:115
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:1045
INITIALIZE_FUNCTION
#define INITIALIZE_FUNCTION
Definition: static_lifetime_init.h:23
cmdlinet::get_value
std::string get_value(char option) const
Definition: cmdline.cpp:46
java_bytecode_internal_additions.h
java_entry_point.h
java_bytecode_languaget::initialize_class_loader
void initialize_class_loader()
Definition: java_bytecode_language.cpp:299
select_pointer_typet
Definition: select_pointer_type.h:26
messaget::set_message_handler
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:176
struct_typet::bases
const basest & bases() const
Get the collection of base classes/structs.
Definition: std_types.h:257
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:731
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:1174
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:20
java_bytecode_languaget::parse
virtual bool parse()
We set the main class (i.e. class to start the class loading analysis, see java_class_loadert) when w...
Definition: java_bytecode_language.cpp:367
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:152
throwMainClassLoadingError
static void throwMainClassLoadingError(const std::string &main_class)
Definition: java_bytecode_language.cpp:321
irept::is_nil
bool is_nil() const
Definition: irep.h:398
irept::id
const irep_idt & id() const
Definition: irep.h:418
message_handlert
Definition: message.h:27
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:88
java_bytecode_language_optionst::java_cp_include_files
std::string java_cp_include_files
Definition: java_bytecode_language.h:243
java_bytecode_languaget::modules_provided
void modules_provided(std::set< std::string > &modules) override
Definition: java_bytecode_language.cpp:277
java_bytecode_languaget::string_preprocess
java_string_library_preprocesst string_preprocess
Definition: java_bytecode_language.h:383
java_bytecode_parse_treet::classt::methods
methodst methods
Definition: java_bytecode_parse_tree.h:275
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1526
java_bytecode_language_optionst::assert_no_exceptions_thrown
bool assert_no_exceptions_thrown
Transform athrow bytecode instructions into assert FALSE followed by assume FALSE.
Definition: java_bytecode_language.h:234
java_class_loadert::can_load_class
bool can_load_class(const irep_idt &class_name)
Checks whether class_name is parseable from the classpath, ignoring class loading limits.
Definition: java_class_loader.cpp:106
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:64
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, const build_argumentst &build_arguments)
Given the symbol_table and the main_class to test, this function generates a new function __CPROVER__...
Definition: java_entry_point.cpp:568
optionst::get_unsigned_int_option
unsigned int get_unsigned_int_option(const std::string &option) const
Definition: options.cpp:56
main_function_resultt
Definition: java_entry_point.h:87
get_inherited_component
optionalt< resolve_inherited_componentt::inherited_componentt > get_inherited_component(const irep_idt &component_class_id, const irep_idt &component_name, const symbol_tablet &symbol_table, bool include_interfaces)
Finds an inherited component (method or field), taking component visibility into account.
Definition: java_utils.cpp:379
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:58
ci_lazy_methods.h
lazy_class_to_declared_symbols_mapt::get
std::unordered_multimap< irep_idt, symbolt > & get(const symbol_tablet &symbol_table)
Definition: java_bytecode_language.cpp:127
synthetic_method_typet::CREATE_ARRAY_WITH_TYPE
@ CREATE_ARRAY_WITH_TYPE
Our internal implementation of CProver.createArrayWithType, which needs to access internal type-id fi...
java_bytecode_language_optionst::assume_inputs_non_null
bool assume_inputs_non_null
assume inputs variables to be non-null
Definition: java_bytecode_language.h:223
side_effect_exprt::get_statement
const irep_idt & get_statement() const
Definition: std_code.h:1907
config
configt config
Definition: config.cpp:24
java_bytecode_concurrency_instrumentation.h
invokedynamic_synthetic_constructor
codet invokedynamic_synthetic_constructor(const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler)
Create invokedynamic synthetic constructor.
Definition: lambda_synthesis.cpp:375
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:595
java_class_loader_limitt
Class representing a filter for class file loading.
Definition: java_class_loader_limit.h:23
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:1506
lambda_synthesis.h
java_class_typet::components
const componentst & components() const
Definition: java_types.h:226
java_bytecode_parse_treet::parsed_class
classt parsed_class
Definition: java_bytecode_parse_tree.h:305
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
messaget::get_message_handler
message_handlert & get_message_handler()
Definition: message.h:181
class_hierarchy.h
java_bytecode_languaget::get_pointer_type_selector
const select_pointer_typet & get_pointer_type_selector() const
Definition: java_bytecode_language.cpp:1139
java_bytecode_languaget::class_hierarchy
class_hierarchyt class_hierarchy
Definition: java_bytecode_language.h:395
java_internal_additions
void java_internal_additions(symbol_table_baset &dest)
Definition: java_bytecode_internal_additions.cpp:19
fieldref_exprt::class_name
irep_idt class_name() const
Definition: java_bytecode_parse_tree.h:341
synthetic_method_typet::STUB_CLASS_STATIC_INITIALIZER
@ STUB_CLASS_STATIC_INITIALIZER
A generated (synthetic) static initializer function for a stub type.
messaget::message_handler
message_handlert * message_handler
Definition: message.h:425
java_bytecode_languaget::typecheck
bool typecheck(symbol_tablet &context, const std::string &module) override
Definition: java_bytecode_language.cpp:806
java_bytecode_language_optionst::static_values_json
optionalt< json_objectt > static_values_json
JSON which contains initial values of static fields (right after the static initializer of the class ...
Definition: java_bytecode_language.h:247
expr_iterator.h
create_java_initialize
void create_java_initialize(symbol_table_baset &symbol_table)
Adds __cprover_initialize to the symbol_table but does not generate code for it yet.
Definition: java_entry_point.cpp:44
java_bytecode_languaget::set_message_handler
void set_message_handler(message_handlert &message_handler) override
Definition: java_bytecode_language.cpp:292
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:71
suffix.h
to_json_object
json_objectt & to_json_object(jsont &json)
Definition: json.h:442
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
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:918
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
exprt::depth_cend
const_depth_iteratort depth_cend() const
Definition: expr.cpp:341
symbolt::location
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
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:81
cmdline.h
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:98
symbolt
Symbol table entry.
Definition: symbol.h:28
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:442
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:340
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:520
optionst::get_bool_option
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
java_bytecode_language_optionst::throw_runtime_exceptions
bool throw_runtime_exceptions
Definition: java_bytecode_language.h:225
symbol_table_buildert
Author: Diffblue Ltd.
Definition: symbol_table_builder.h:14
symbolt::is_type
bool is_type
Definition: symbol.h:61
jsont::is_array
bool is_array() const
Definition: json.h:59
java_bytecode_language_optionst::extra_methods
std::vector< load_extra_methodst > extra_methods
Definition: java_bytecode_language.h:252
java_bytecode_language_optionst::assert_uncaught_exceptions
bool assert_uncaught_exceptions
Definition: java_bytecode_language.h:226
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:599
java_bytecode_language_optionst::throw_assertion_error
bool throw_assertion_error
Definition: java_bytecode_language.h:227
configt::java
struct configt::javat java
type2java
std::string type2java(const typet &type, const namespacet &ns)
Definition: expr2java.cpp:462
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:187
java_bytecode_languaget::object_factory_parameters
java_object_factory_parameterst object_factory_parameters
Definition: java_bytecode_language.h:381
config.h
expr2java
std::string expr2java(const exprt &expr, const namespacet &ns)
Definition: expr2java.cpp:455
lazy_class_to_declared_symbols_mapt
Map classes to the symbols they declare but is only computed once it is needed and the map is then ke...
Definition: java_bytecode_language.h:202
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:95
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:847
java_bytecode_language_optionst::threading_support
bool threading_support
Definition: java_bytecode_language.h:228
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:545
ci_lazy_methods_neededt
Definition: ci_lazy_methods_needed.h:25
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:1470
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:54
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:527
java_bytecode_languaget::parse_from_main_class
void parse_from_main_class()
Definition: java_bytecode_language.cpp:327
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
java_bytecode_language_optionst::no_load_classes
std::unordered_set< std::string > no_load_classes
List of classes to never load.
Definition: java_bytecode_language.h:250
expr2java.h
static_lifetime_init.h
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:2815
java_bytecode_languaget::convert_single_method
void convert_single_method(const irep_idt &function_id, symbol_table_baset &symbol_table, lazy_class_to_declared_symbols_mapt &class_to_declared_symbols)
Definition: java_bytecode_language.h:352
to_java_method_type
const java_method_typet & to_java_method_type(const typet &type)
Definition: java_types.h:186
java_class_typet::get_is_stub
bool get_is_stub() const
Definition: java_types.h:388
java_bytecode_instrument.h
symbol_table.h
Author: Diffblue Ltd.
java_bytecode_language_optionst::string_refinement_enabled
bool string_refinement_enabled
Definition: java_bytecode_language.h:224
lift_clinit_calls.h
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1488
bytecode_info
struct bytecode_infot const bytecode_info[]
Definition: bytecode_info.cpp:16
LAZY_METHODS_MODE_EXTERNAL_DRIVER
@ LAZY_METHODS_MODE_EXTERNAL_DRIVER
Definition: java_bytecode_language.h:188
java_utils.h
symbol_table_builder.h
messaget::warning
mstreamt & warning() const
Definition: message.h:390
invalid_command_line_argument_exceptiont
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
Definition: exception_utils.h:38
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:283
cmdlinet::get_values
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:107
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:36
java_method_typet
Definition: java_types.h:103
java_bytecode_language_optionst
Definition: java_bytecode_language.h:217
optionst::get_list_option
const value_listt & get_list_option(const std::string &option) const
Definition: options.cpp:80
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:998
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:3147
lazy_class_to_declared_symbols_mapt::map
std::unordered_multimap< irep_idt, symbolt > map
Definition: java_bytecode_language.h:213
java_bytecode_typecheck.h
validation_modet::INVARIANT
@ INVARIANT
java_bytecode_convert_class.h
java_bytecode_parser.h
java_bytecode_language_optionst::max_user_array_length
size_t max_user_array_length
max size for user code created arrays
Definition: java_bytecode_language.h:237
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35
get_create_array_with_type_name
irep_idt get_create_array_with_type_name()
Returns the symbol name for org.cprover.CProver.createArrayWithType
Definition: create_array_with_type_intrinsic.cpp:21
java_bytecode_language_optionst::nondet_static
bool nondet_static
Definition: java_bytecode_language.h:229