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/suffix.h>
24 #include <util/symbol_table.h>
26 
27 #include <json/json_parser.h>
28 
30 
31 #include "ci_lazy_methods.h"
39 #include "java_class_loader.h"
41 #include "java_entry_point.h"
44 #include "java_string_literals.h"
45 #include "java_utils.h"
46 #include "lambda_synthesis.h"
47 #include "lift_clinit_calls.h"
48 
49 #include "expr2java.h"
50 #include "load_method_by_regex.h"
51 
55 void parse_java_language_options(const cmdlinet &cmd, optionst &options)
56 {
57  options.set_option(
58  "java-assume-inputs-non-null", cmd.isset("java-assume-inputs-non-null"));
59  options.set_option(
60  "throw-runtime-exceptions", cmd.isset("throw-runtime-exceptions"));
61  options.set_option(
62  "uncaught-exception-check", !cmd.isset("disable-uncaught-exception-check"));
63  options.set_option(
64  "throw-assertion-error", cmd.isset("throw-assertion-error"));
65  options.set_option(
66  "assert-no-exceptions-thrown", cmd.isset("assert-no-exceptions-thrown"));
67  options.set_option("java-threading", cmd.isset("java-threading"));
68 
69  if(cmd.isset("java-max-vla-length"))
70  {
71  options.set_option(
72  "java-max-vla-length", cmd.get_value("java-max-vla-length"));
73  }
74 
75  options.set_option(
76  "symex-driven-lazy-loading", cmd.isset("symex-driven-lazy-loading"));
77 
78  options.set_option(
79  "ignore-manifest-main-class", cmd.isset("ignore-manifest-main-class"));
80 
81  if(cmd.isset("context-include"))
82  options.set_option("context-include", cmd.get_values("context-include"));
83 
84  if(cmd.isset("context-exclude"))
85  options.set_option("context-exclude", cmd.get_values("context-exclude"));
86 
87  if(cmd.isset("java-load-class"))
88  options.set_option("java-load-class", cmd.get_values("java-load-class"));
89 
90  if(cmd.isset("java-no-load-class"))
91  {
92  options.set_option(
93  "java-no-load-class", cmd.get_values("java-no-load-class"));
94  }
95  if(cmd.isset("lazy-methods-extra-entry-point"))
96  {
97  options.set_option(
98  "lazy-methods-extra-entry-point",
99  cmd.get_values("lazy-methods-extra-entry-point"));
100  }
101  if(cmd.isset("java-cp-include-files"))
102  {
103  options.set_option(
104  "java-cp-include-files", cmd.get_value("java-cp-include-files"));
105  }
106  if(cmd.isset("static-values"))
107  {
108  options.set_option("static-values", cmd.get_value("static-values"));
109  }
110  options.set_option(
111  "java-lift-clinit-calls", cmd.isset("java-lift-clinit-calls"));
112 }
113 
115 {
116  std::vector<std::string> context_include;
117  std::vector<std::string> context_exclude;
118  for(const auto &include : options.get_list_option("context-include"))
119  context_include.push_back("java::" + include);
120  for(const auto &exclude : options.get_list_option("context-exclude"))
121  context_exclude.push_back("java::" + exclude);
122  return prefix_filtert(std::move(context_include), std::move(context_exclude));
123 }
124 
125 std::unordered_multimap<irep_idt, symbolt> &
127 {
128  if(!initialized)
129  {
130  map = class_to_declared_symbols(symbol_table);
131  initialized = true;
132  }
133  return map;
134 }
135 
137 {
138  initialized = false;
139  map.clear();
140 }
141 
143  const optionst &options,
144  messaget &log)
145 {
147  options.get_bool_option("java-assume-inputs-non-null");
148  string_refinement_enabled = options.get_bool_option("refine-strings");
150  options.get_bool_option("throw-runtime-exceptions");
152  options.get_bool_option("uncaught-exception-check");
153  throw_assertion_error = options.get_bool_option("throw-assertion-error");
155  options.get_bool_option("assert-no-exceptions-thrown");
156  threading_support = options.get_bool_option("java-threading");
158  options.get_unsigned_int_option("java-max-vla-length");
159 
160  if(options.get_bool_option("symex-driven-lazy-loading"))
162  else if(options.get_bool_option("lazy-methods"))
164  else
166 
168  {
169  java_load_classes.insert(
170  java_load_classes.end(),
171  exception_needed_classes.begin(),
173  }
174 
175  if(options.is_set("java-load-class"))
176  {
177  const auto &load_values = options.get_list_option("java-load-class");
178  java_load_classes.insert(
179  java_load_classes.end(), load_values.begin(), load_values.end());
180  }
181  if(options.is_set("java-no-load-class"))
182  {
183  const auto &no_load_values = options.get_list_option("java-no-load-class");
184  no_load_classes = {no_load_values.begin(), no_load_values.end()};
185  }
186  const std::list<std::string> &extra_entry_points =
187  options.get_list_option("lazy-methods-extra-entry-point");
189  extra_entry_points.begin(),
190  extra_entry_points.end(),
191  std::back_inserter(extra_methods),
193 
194  java_cp_include_files = options.get_option("java-cp-include-files");
195  if(!java_cp_include_files.empty())
196  {
197  // load file list from JSON file
198  if(java_cp_include_files[0]=='@')
199  {
200  jsont json_cp_config;
201  if(parse_json(
202  java_cp_include_files.substr(1),
203  log.get_message_handler(),
204  json_cp_config))
205  throw "cannot read JSON input configuration for JAR loading";
206 
207  if(!json_cp_config.is_object())
208  throw "the JSON file has a wrong format";
209  jsont include_files=json_cp_config["jar"];
210  if(!include_files.is_array())
211  throw "the JSON file has a wrong format";
212 
213  // add jars from JSON config file to classpath
214  for(const jsont &file_entry : to_json_array(include_files))
215  {
217  file_entry.is_string() && has_suffix(file_entry.value, ".jar"),
218  "classpath entry must be jar filename, but '" + file_entry.value +
219  "' found");
220  config.java.classpath.push_back(file_entry.value);
221  }
222  }
223  }
224  else
226 
227  nondet_static = options.get_bool_option("nondet-static");
228  if(options.is_set("static-values"))
229  {
230  const std::string filename = options.get_option("static-values");
231  jsont tmp_json;
232  if(parse_json(filename, log.get_message_handler(), tmp_json))
233  {
234  log.warning()
235  << "Provided JSON file for static-values cannot be parsed; it"
236  << " will be ignored." << messaget::eom;
237  }
238  else
239  {
240  if(!tmp_json.is_object())
241  {
242  log.warning() << "Provided JSON file for static-values is not a JSON "
243  << "object; it will be ignored." << messaget::eom;
244  }
245  else
246  static_values_json = std::move(to_json_object(tmp_json));
247  }
248  }
249 
251  options.get_bool_option("ignore-manifest-main-class");
252 
253  if(options.is_set("context-include") || options.is_set("context-exclude"))
254  method_context = get_context(options);
255 
256  should_lift_clinit_calls = options.get_bool_option("java-lift-clinit-calls");
257 }
258 
261 {
264  const auto &new_points = build_extra_entry_points(options);
265  language_options->extra_methods.insert(
266  language_options->extra_methods.end(),
267  new_points.begin(),
268  new_points.end());
269 }
270 
271 std::set<std::string> java_bytecode_languaget::extensions() const
272 {
273  return { "class", "jar" };
274 }
275 
276 void java_bytecode_languaget::modules_provided(std::set<std::string> &)
277 {
278  // modules.insert(translation_unit(parse_path));
279 }
280 
283  std::istream &,
284  const std::string &,
285  std::ostream &)
286 {
287  // there is no preprocessing!
288  return true;
289 }
290 
292  message_handlert &message_handler)
293 {
295 }
296 
298 {
300 
301  for(const auto &p : config.java.classpath)
303 
305  language_options->java_cp_include_files);
307  if(language_options->string_refinement_enabled)
308  {
310 
311  auto get_string_base_classes = [this](const irep_idt &id) {
313  };
314 
315  java_class_loader.set_extra_class_refs_function(get_string_base_classes);
316  }
317 }
318 
319 static void throwMainClassLoadingError(const std::string &main_class)
320 {
322  "Error: Could not find or load main class " + main_class);
323 }
324 
326 {
327  if(!main_class.empty())
328  {
329  // Try to load class
330  status() << "Trying to load Java main class: " << main_class << eom;
332  {
333  // Try to extract class name and load class
334  const auto maybe_class_name =
336  if(!maybe_class_name)
337  {
339  return;
340  }
341  status() << "Trying to load Java main class: " << maybe_class_name.value()
342  << eom;
344  maybe_class_name.value(), get_message_handler()))
345  {
347  return;
348  }
349  // Everything went well. We have a loadable main class.
350  // The entry point ('main') will be checked later.
352  main_class = maybe_class_name.value();
353  }
354  status() << "Found Java main class: " << main_class << eom;
355  // Now really load it.
356  const auto &parse_trees =
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 =
434  for(const auto &c : classes)
435  main_jar_classes.push_back(c);
436  }
437  else
439  }
440  else
442 
444  return false;
445 }
446 
457  const java_bytecode_parse_treet &parse_tree,
458  symbol_tablet &symbol_table)
459 {
460  namespacet ns(symbol_table);
461  for(const auto &method : parse_tree.parsed_class.methods)
462  {
463  for(const java_bytecode_parse_treet::instructiont &instruction :
464  method.instructions)
465  {
466  const std::string statement =
467  bytecode_info[instruction.bytecode].mnemonic;
468  if(statement == "getfield" || statement == "putfield")
469  {
470  const fieldref_exprt &fieldref =
471  expr_dynamic_cast<fieldref_exprt>(instruction.args[0]);
472  irep_idt class_symbol_id = fieldref.class_name();
473  const symbolt *class_symbol = symbol_table.lookup(class_symbol_id);
474  INVARIANT(
475  class_symbol != nullptr,
476  "all types containing fields should have been loaded");
477 
478  const java_class_typet *class_type =
479  &to_java_class_type(class_symbol->type);
480  const irep_idt &component_name = fieldref.component_name();
481  while(!class_type->has_component(component_name))
482  {
483  if(class_type->get_is_stub())
484  {
485  // Accessing a field of an incomplete (opaque) type.
486  symbolt &writable_class_symbol =
487  symbol_table.get_writeable_ref(class_symbol_id);
488  auto &components =
489  to_java_class_type(writable_class_symbol.type).components();
490  components.emplace_back(component_name, fieldref.type());
491  components.back().set_base_name(component_name);
492  components.back().set_pretty_name(component_name);
493  components.back().set_is_final(true);
494  break;
495  }
496  else
497  {
498  // Not present here: check the superclass.
499  INVARIANT(
500  !class_type->bases().empty(),
501  "class '" + id2string(class_symbol->name) +
502  "' (which was missing a field '" + id2string(component_name) +
503  "' referenced from method '" + id2string(method.name) +
504  "' of class '" + id2string(parse_tree.parsed_class.name) +
505  "') should have an opaque superclass");
506  const auto &superclass_type = class_type->bases().front().type();
507  class_symbol_id = superclass_type.get_identifier();
508  class_type = &to_java_class_type(ns.follow(superclass_type));
509  }
510  }
511  }
512  }
513  }
514 }
515 
522  const irep_idt &class_id, symbol_tablet &symbol_table)
523 {
524  struct_tag_typet java_lang_Class("java::java.lang.Class");
525  symbol_exprt symbol_expr(
527  java_lang_Class);
528  if(!symbol_table.has_symbol(symbol_expr.get_identifier()))
529  {
530  symbolt new_class_symbol;
531  new_class_symbol.name = symbol_expr.get_identifier();
532  new_class_symbol.type = symbol_expr.type();
533  INVARIANT(
534  has_prefix(id2string(new_class_symbol.name), "java::"),
535  "class identifier should have 'java::' prefix");
536  new_class_symbol.base_name =
537  id2string(new_class_symbol.name).substr(6);
538  new_class_symbol.mode = ID_java;
539  new_class_symbol.is_lvalue = true;
540  new_class_symbol.is_state_var = true;
541  new_class_symbol.is_static_lifetime = true;
542  new_class_symbol.type.set(ID_C_no_nondet_initialization, true);
543  symbol_table.add(new_class_symbol);
544  }
545 
546  return symbol_expr;
547 }
548 
564  const exprt &ldc_arg0,
565  symbol_tablet &symbol_table,
566  bool string_refinement_enabled)
567 {
568  if(ldc_arg0.id() == ID_type)
569  {
570  const irep_idt &class_id = ldc_arg0.type().get(ID_identifier);
571  return
573  get_or_create_class_literal_symbol(class_id, symbol_table));
574  }
575  else if(
576  const auto &literal =
577  expr_try_dynamic_cast<java_string_literal_exprt>(ldc_arg0))
578  {
580  *literal, symbol_table, string_refinement_enabled));
581  }
582  else
583  {
584  INVARIANT(
585  ldc_arg0.id() == ID_constant,
586  "ldc argument should be constant, string literal or class literal");
587  return ldc_arg0;
588  }
589 }
590 
601  java_bytecode_parse_treet &parse_tree,
602  symbol_tablet &symbol_table,
603  bool string_refinement_enabled)
604 {
605  for(auto &method : parse_tree.parsed_class.methods)
606  {
607  for(java_bytecode_parse_treet::instructiont &instruction :
608  method.instructions)
609  {
610  // ldc* instructions are Java bytecode "load constant" ops, which can
611  // retrieve a numeric constant, String literal, or Class literal.
612  const std::string statement =
613  bytecode_info[instruction.bytecode].mnemonic;
614  // clang-format off
615  if(statement == "ldc" ||
616  statement == "ldc2" ||
617  statement == "ldc_w" ||
618  statement == "ldc2_w")
619  {
620  // clang-format on
621  INVARIANT(
622  instruction.args.size() != 0,
623  "ldc instructions should have an argument");
624  instruction.args[0] =
626  instruction.args[0],
627  symbol_table,
628  string_refinement_enabled);
629  }
630  }
631  }
632 }
633 
646  symbol_table_baset &symbol_table,
647  const irep_idt &symbol_id,
648  const irep_idt &symbol_basename,
649  const typet &symbol_type,
650  const irep_idt &class_id,
651  bool force_nondet_init)
652 {
653  symbolt new_symbol;
654  new_symbol.is_static_lifetime = true;
655  new_symbol.is_lvalue = true;
656  new_symbol.is_state_var = true;
657  new_symbol.name = symbol_id;
658  new_symbol.base_name = symbol_basename;
659  new_symbol.type = symbol_type;
660  set_declaring_class(new_symbol, class_id);
661  // Public access is a guess; it encourages merging like-typed static fields,
662  // whereas a more restricted visbility would encourage separating them.
663  // Neither is correct, as without the class file we can't know the truth.
664  new_symbol.type.set(ID_C_access, ID_public);
665  // We set the field as final to avoid assuming they can be overridden.
666  new_symbol.type.set(ID_C_constant, true);
667  new_symbol.pretty_name = new_symbol.name;
668  new_symbol.mode = ID_java;
669  new_symbol.is_type = false;
670  // If pointer-typed, initialise to null and a static initialiser will be
671  // created to initialise on first reference. If primitive-typed, specify
672  // nondeterministic initialisation by setting a nil value.
673  if(symbol_type.id() == ID_pointer && !force_nondet_init)
674  new_symbol.value = null_pointer_exprt(to_pointer_type(symbol_type));
675  else
676  new_symbol.value.make_nil();
677  bool add_failed = symbol_table.add(new_symbol);
678  INVARIANT(
679  !add_failed, "caller should have checked symbol not already in table");
680 }
681 
691  const irep_idt &start_class_id,
692  const symbol_tablet &symbol_table,
693  const class_hierarchyt &class_hierarchy)
694 {
695  // Depth-first search: return the first stub ancestor, or irep_idt() if none
696  // found.
697  std::vector<irep_idt> classes_to_check;
698  classes_to_check.push_back(start_class_id);
699 
700  while(!classes_to_check.empty())
701  {
702  irep_idt to_check = classes_to_check.back();
703  classes_to_check.pop_back();
704 
705  // Exclude java.lang.Object because it can
706  if(
707  to_java_class_type(symbol_table.lookup_ref(to_check).type)
708  .get_is_stub() &&
709  to_check != "java::java.lang.Object")
710  {
711  return to_check;
712  }
713 
714  const class_hierarchyt::idst &parents =
715  class_hierarchy.class_map.at(to_check).parents;
716  classes_to_check.insert(
717  classes_to_check.end(), parents.begin(), parents.end());
718  }
719 
720  return irep_idt();
721 }
722 
733  const java_bytecode_parse_treet &parse_tree,
734  symbol_table_baset &symbol_table,
735  const class_hierarchyt &class_hierarchy,
736  messaget &log)
737 {
738  namespacet ns(symbol_table);
739  for(const auto &method : parse_tree.parsed_class.methods)
740  {
741  for(const java_bytecode_parse_treet::instructiont &instruction :
742  method.instructions)
743  {
744  const std::string statement =
745  bytecode_info[instruction.bytecode].mnemonic;
746  if(statement == "getstatic" || statement == "putstatic")
747  {
748  INVARIANT(
749  instruction.args.size() > 0,
750  "get/putstatic should have at least one argument");
751  const fieldref_exprt &field_ref =
752  expr_dynamic_cast<fieldref_exprt>(instruction.args[0]);
753  irep_idt component = field_ref.component_name();
754  irep_idt class_id = field_ref.class_name();
755 
756  // The final 'true' parameter here includes interfaces, as they can
757  // define static fields.
758  const auto referred_component =
759  get_inherited_component(class_id, component, symbol_table, true);
760  if(!referred_component)
761  {
762  // Create a new stub global on an arbitrary incomplete ancestor of the
763  // class that was referred to. This is just a guess, but we have no
764  // better information to go on.
765  irep_idt add_to_class_id =
767  class_id, symbol_table, class_hierarchy);
768 
769  // If there are no incomplete ancestors to ascribe the missing field
770  // to, we must have an incomplete model of a class or simply a
771  // version mismatch of some kind. Normally this would be an error, but
772  // our models library currently triggers this error in some cases
773  // (notably java.lang.System, which is missing System.in/out/err).
774  // Therefore for this case we ascribe the missing field to the class
775  // it was directly referenced from, and fall back to initialising the
776  // field in __CPROVER_initialize, rather than try to create or augment
777  // a clinit method for a non-stub class.
778 
779  bool no_incomplete_ancestors = add_to_class_id.empty();
780  if(no_incomplete_ancestors)
781  {
782  add_to_class_id = class_id;
783 
784  // TODO forbid this again once the models library has been checked
785  // for missing static fields.
786  log.warning() << "Stub static field " << component << " found for "
787  << "non-stub type " << class_id << ". In future this "
788  << "will be a fatal error." << messaget::eom;
789  }
790 
791  irep_idt identifier =
792  id2string(add_to_class_id) + "." + id2string(component);
793 
795  symbol_table,
796  identifier,
797  component,
798  instruction.args[0].type(),
799  add_to_class_id,
800  no_incomplete_ancestors);
801  }
802  }
803  }
804  }
805 }
806 
808  symbol_tablet &symbol_table,
809  const std::string &)
810 {
811  PRECONDITION(language_options.has_value());
812  // There are various cases in the Java front-end where pre-existing symbols
813  // from a previous load are not handled. We just rule this case out for now;
814  // a user wishing to ensure a particular class is loaded should use
815  // --java-load-class (to force class-loading) or
816  // --lazy-methods-extra-entry-point (to ensure a method body is loaded)
817  // instead of creating two instances of the front-end.
818  INVARIANT(
819  symbol_table.begin() == symbol_table.end(),
820  "the Java front-end should only be used with an empty symbol table");
821 
822  java_internal_additions(symbol_table);
823  create_java_initialize(symbol_table);
824 
825  if(language_options->string_refinement_enabled)
827 
828  // Must load java.lang.Object first to avoid stubbing
829  // This ordering could alternatively be enforced by
830  // moving the code below to the class loader.
831  java_class_loadert::parse_tree_with_overridest_mapt::const_iterator it =
832  java_class_loader.get_class_with_overlays_map().find("java.lang.Object");
834  {
836  it->second,
837  symbol_table,
839  language_options->max_user_array_length,
842  language_options->no_load_classes))
843  {
844  return true;
845  }
846  }
847 
848  // first generate a new struct symbol for each class and a new function symbol
849  // for every method
850  for(const auto &class_trees : java_class_loader.get_class_with_overlays_map())
851  {
852  if(class_trees.second.front().parsed_class.name.empty())
853  continue;
854 
856  class_trees.second,
857  symbol_table,
859  language_options->max_user_array_length,
862  language_options->no_load_classes))
863  {
864  return true;
865  }
866  }
867 
868  // Register synthetic method that replaces a real definition if one is
869  // available:
870  if(symbol_table.has_symbol(get_create_array_with_type_name()))
871  {
874  }
875 
876  // Now add synthetic classes for every invokedynamic instruction found (it
877  // makes this easier that all interface types and their methods have been
878  // created above):
879  {
880  std::vector<irep_idt> methods_to_check;
881 
882  // Careful not to add to the symtab while iterating over it:
883  for(const auto &id_and_symbol : symbol_table)
884  {
885  const auto &symbol = id_and_symbol.second;
886  const auto &id = symbol.name;
887  if(can_cast_type<code_typet>(symbol.type) && method_bytecode.get(id))
888  {
889  methods_to_check.push_back(id);
890  }
891  }
892 
893  for(const auto &id : methods_to_check)
894  {
896  id,
897  method_bytecode.get(id)->get().method.instructions,
898  symbol_table,
901  }
902  }
903 
904  // Now that all classes have been created in the symbol table we can populate
905  // the class hierarchy:
906  class_hierarchy(symbol_table);
907 
908  // find and mark all implicitly generic class types
909  // this can only be done once all the class symbols have been created
910  for(const auto &c : java_class_loader.get_class_with_overlays_map())
911  {
912  if(c.second.front().parsed_class.name.empty())
913  continue;
914  try
915  {
917  c.second.front().parsed_class.name, symbol_table);
918  }
920  {
922  << "Not marking class " << c.first
923  << " implicitly generic due to missing outer class symbols"
924  << messaget::eom;
925  }
926  }
927 
928  // Infer fields on opaque types based on the method instructions just loaded.
929  // For example, if we don't have bytecode for field x of class A, but we can
930  // see an int-typed getfield instruction referring to it, add that field now.
931  for(auto &class_to_trees : java_class_loader.get_class_with_overlays_map())
932  {
933  for(const java_bytecode_parse_treet &parse_tree : class_to_trees.second)
934  infer_opaque_type_fields(parse_tree, symbol_table);
935  }
936 
937  // Create global variables for constants (String and Class literals) up front.
938  // This means that when running with lazy loading, we will be aware of these
939  // literal globals' existence when __CPROVER_initialize is generated in
940  // `generate_support_functions`.
941  const std::size_t before_constant_globals_size = symbol_table.symbols.size();
942  for(auto &class_to_trees : java_class_loader.get_class_with_overlays_map())
943  {
944  for(java_bytecode_parse_treet &parse_tree : class_to_trees.second)
945  {
947  parse_tree, symbol_table, language_options->string_refinement_enabled);
948  }
949  }
950  status() << "Java: added "
951  << (symbol_table.symbols.size() - before_constant_globals_size)
952  << " String or Class constant symbols"
953  << messaget::eom;
954 
955  // For each reference to a stub global (that is, a global variable declared on
956  // a class we don't have bytecode for, and therefore don't know the static
957  // initialiser for), create a synthetic static initialiser (clinit method)
958  // to nondet initialise it.
959  // Note this must be done before making static initialiser wrappers below, as
960  // this makes a Classname.clinit method, then the next pass makes a wrapper
961  // that ensures it is only run once, and that static initialisation happens
962  // in class-graph topological order.
963 
964  {
965  journalling_symbol_tablet symbol_table_journal =
966  journalling_symbol_tablet::wrap(symbol_table);
967  for(auto &class_to_trees : java_class_loader.get_class_with_overlays_map())
968  {
969  for(const java_bytecode_parse_treet &parse_tree : class_to_trees.second)
970  {
972  parse_tree, symbol_table_journal, class_hierarchy, *this);
973  }
974  }
975 
977  symbol_table, symbol_table_journal.get_inserted(), synthetic_methods);
978  }
979 
981  symbol_table,
983  language_options->threading_support,
984  language_options->static_values_json.has_value());
985 
987 
988  // Now incrementally elaborate methods
989  // that are reachable from this entry point.
990  switch(language_options->lazy_methods_mode)
991  {
993  // ci = context-insensitive
994  if(do_ci_lazy_method_conversion(symbol_table))
995  return true;
996  break;
998  {
999  symbol_table_buildert symbol_table_builder =
1000  symbol_table_buildert::wrap(symbol_table);
1001 
1002  journalling_symbol_tablet journalling_symbol_table =
1003  journalling_symbol_tablet::wrap(symbol_table_builder);
1004 
1005  // Convert all synthetic methods:
1006  for(const auto &function_id_and_type : synthetic_methods)
1007  {
1009  function_id_and_type.first,
1010  journalling_symbol_table,
1012  }
1013  // Convert all methods for which we have bytecode now
1014  for(const auto &method_sig : method_bytecode)
1015  {
1017  method_sig.first, journalling_symbol_table, class_to_declared_symbols);
1018  }
1020  INITIALIZE_FUNCTION, journalling_symbol_table, class_to_declared_symbols);
1021  // Now convert all newly added string methods
1022  for(const auto &fn_name : journalling_symbol_table.get_inserted())
1023  {
1025  convert_single_method(fn_name, symbol_table, class_to_declared_symbols);
1026  }
1027  }
1028  break;
1030  // Our caller is in charge of elaborating methods on demand.
1031  break;
1032  }
1033 
1034  // now instrument runtime exceptions
1036  symbol_table,
1037  language_options->throw_runtime_exceptions,
1039 
1040  // now typecheck all
1041  bool res = java_bytecode_typecheck(
1042  symbol_table,
1044  language_options->string_refinement_enabled);
1045 
1046  // now instrument thread-blocks and synchronized methods.
1047  if(language_options->threading_support)
1048  {
1049  convert_threadblock(symbol_table);
1051  }
1052 
1053  return res;
1054 }
1055 
1057  symbol_tablet &symbol_table)
1058 {
1059  PRECONDITION(language_options.has_value());
1060 
1061  symbol_table_buildert symbol_table_builder =
1062  symbol_table_buildert::wrap(symbol_table);
1063 
1066  if(!res.is_success())
1067  return res.is_error();
1068 
1069  // Load the main function into the symbol table to get access to its
1070  // parameter names
1071  convert_lazy_method(res.main_function.name, symbol_table_builder);
1072 
1073  const symbolt &symbol =
1074  symbol_table_builder.lookup_ref(res.main_function.name);
1075  if(symbol.value.is_nil())
1076  {
1078  "the program has no entry point",
1079  "function",
1080  "Check that the specified entry point is included by your "
1081  "--context-include or --context-exclude options");
1082  }
1083 
1084  // generate the test harness in __CPROVER__start and a call the entry point
1085  return java_entry_point(
1086  symbol_table_builder,
1087  main_class,
1089  language_options->assume_inputs_non_null,
1090  language_options->assert_uncaught_exceptions,
1093  language_options->string_refinement_enabled,
1094  [&](const symbolt &function, symbol_table_baset &symbol_table) {
1095  return java_build_arguments(
1096  function,
1097  symbol_table,
1098  language_options->assume_inputs_non_null,
1099  object_factory_parameters,
1100  get_pointer_type_selector(),
1101  get_message_handler());
1102  });
1103 }
1104 
1117  symbol_tablet &symbol_table)
1118 {
1119  symbol_table_buildert symbol_table_builder =
1120  symbol_table_buildert::wrap(symbol_table);
1121 
1123 
1124  const method_convertert method_converter =
1125  [this, &symbol_table_builder, &class_to_declared_symbols](
1126  const irep_idt &function_id,
1127  ci_lazy_methods_neededt lazy_methods_needed) {
1128  return convert_single_method(
1129  function_id,
1130  symbol_table_builder,
1131  std::move(lazy_methods_needed),
1133  };
1134 
1135  ci_lazy_methodst method_gather(
1136  symbol_table,
1137  main_class,
1139  language_options->extra_methods,
1141  language_options->java_load_classes,
1144 
1145  return method_gather(
1146  symbol_table, method_bytecode, method_converter, get_message_handler());
1147 }
1148 
1149 const select_pointer_typet &
1151 {
1152  PRECONDITION(pointer_type_selector.get()!=nullptr);
1153  return *pointer_type_selector;
1154 }
1155 
1162  std::unordered_set<irep_idt> &methods) const
1163 {
1164  const std::string cprover_class_prefix = "java::org.cprover.CProver.";
1165 
1166  // Add all string solver methods to map
1168  // Add all concrete methods to map
1169  for(const auto &kv : method_bytecode)
1170  methods.insert(kv.first);
1171  // Add all synthetic methods to map
1172  for(const auto &kv : synthetic_methods)
1173  methods.insert(kv.first);
1174  methods.insert(INITIALIZE_FUNCTION);
1175 }
1176 
1186  const irep_idt &function_id,
1187  symbol_table_baset &symtab)
1188 {
1189  const symbolt &symbol = symtab.lookup_ref(function_id);
1190  if(symbol.value.is_not_nil())
1191  return;
1192 
1193  journalling_symbol_tablet symbol_table=
1195 
1197  convert_single_method(function_id, symbol_table, class_to_declared_symbols);
1198 
1199  // Instrument runtime exceptions (unless symbol is a stub or is the
1200  // INITIALISE_FUNCTION).
1201  if(symbol.value.is_not_nil() && function_id != INITIALIZE_FUNCTION)
1202  {
1204  symbol_table,
1205  symbol_table.get_writeable_ref(function_id),
1206  language_options->throw_runtime_exceptions,
1208  }
1209 
1210  // now typecheck this function
1212  symbol_table,
1214  language_options->string_refinement_enabled);
1215 }
1216 
1228  const codet &function_body,
1229  optionalt<ci_lazy_methods_neededt> needed_lazy_methods)
1230 {
1231  if(needed_lazy_methods)
1232  {
1233  for(const_depth_iteratort it = function_body.depth_cbegin();
1234  it != function_body.depth_cend();
1235  ++it)
1236  {
1237  if(it->id() == ID_code)
1238  {
1239  const auto fn_call = expr_try_dynamic_cast<code_function_callt>(*it);
1240  if(!fn_call)
1241  continue;
1242  const symbol_exprt *fn_sym =
1243  expr_try_dynamic_cast<symbol_exprt>(fn_call->function());
1244  if(fn_sym)
1245  needed_lazy_methods->add_needed_method(fn_sym->get_identifier());
1246  }
1247  else if(
1248  it->id() == ID_side_effect &&
1249  to_side_effect_expr(*it).get_statement() == ID_function_call)
1250  {
1251  const auto &call_expr = to_side_effect_expr_function_call(*it);
1252  const symbol_exprt *fn_sym =
1253  expr_try_dynamic_cast<symbol_exprt>(call_expr.function());
1254  if(fn_sym)
1255  {
1256  INVARIANT(
1257  false,
1258  "Java synthetic methods are not "
1259  "expected to produce side_effect_expr_function_callt. If "
1260  "that has changed, remove this invariant. Also note that "
1261  "as of the time of writing remove_virtual_functions did "
1262  "not support this form of function call.");
1263  // needed_lazy_methods->add_needed_method(fn_sym->get_identifier());
1264  }
1265  }
1266  }
1267  }
1268 }
1269 
1283  const irep_idt &function_id,
1284  symbol_table_baset &symbol_table,
1285  optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
1287 {
1288  const symbolt &symbol = symbol_table.lookup_ref(function_id);
1289 
1290  // Nothing to do if body is already loaded
1291  if(symbol.value.is_not_nil())
1292  return false;
1293 
1294  if(function_id == INITIALIZE_FUNCTION)
1295  {
1297  symbol_table,
1298  symbol.location,
1299  language_options->assume_inputs_non_null,
1302  language_options->string_refinement_enabled,
1304  return false;
1305  }
1306 
1307  INVARIANT(declaring_class(symbol), "Method must have a declaring class.");
1308 
1309  bool ret = convert_single_method_code(
1310  function_id, symbol_table, needed_lazy_methods, class_to_declared_symbols);
1311 
1312  if(symbol.value.is_not_nil() && language_options->should_lift_clinit_calls)
1313  {
1314  auto &writable_symbol = symbol_table.get_writeable_ref(function_id);
1315  writable_symbol.value =
1316  lift_clinit_calls(std::move(to_code(writable_symbol.value)));
1317  }
1318 
1319  INVARIANT(declaring_class(symbol), "Method must have a declaring class.");
1320 
1321  return ret;
1322 }
1323 
1336  const irep_idt &function_id,
1337  symbol_table_baset &symbol_table,
1338  optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
1340 {
1341  const auto &symbol = symbol_table.lookup_ref(function_id);
1342  PRECONDITION(symbol.value.is_nil());
1343 
1344  // Get bytecode for specified function if we have it
1345  method_bytecodet::opt_reft cmb = method_bytecode.get(function_id);
1346 
1347  synthetic_methods_mapt::iterator synthetic_method_it;
1348 
1349  // Check if have a string solver implementation
1350  if(string_preprocess.implements_function(function_id))
1351  {
1352  symbolt &writable_symbol = symbol_table.get_writeable_ref(function_id);
1353  // Load parameter names from any extant bytecode before filling in body
1354  if(cmb)
1355  {
1357  writable_symbol, cmb->get().method.local_variable_table, symbol_table);
1358  }
1359  // Populate body of the function with code generated by string preprocess
1360  codet generated_code = string_preprocess.code_for_function(
1361  writable_symbol, symbol_table, get_message_handler());
1362  // String solver can make calls to functions that haven't yet been seen.
1363  // Add these to the needed_lazy_methods collection
1364  notify_static_method_calls(generated_code, needed_lazy_methods);
1365  writable_symbol.value = std::move(generated_code);
1366  return false;
1367  }
1368  else if(
1369  (synthetic_method_it = synthetic_methods.find(function_id)) !=
1370  synthetic_methods.end())
1371  {
1372  // Synthetic method (i.e. one generated by the Java frontend and which
1373  // doesn't occur in the source bytecode):
1374  symbolt &writable_symbol = symbol_table.get_writeable_ref(function_id);
1375  switch(synthetic_method_it->second)
1376  {
1377  case synthetic_method_typet::STATIC_INITIALIZER_WRAPPER:
1378  if(language_options->threading_support)
1379  writable_symbol.value = get_thread_safe_clinit_wrapper_body(
1380  function_id,
1381  symbol_table,
1382  language_options->nondet_static,
1383  language_options->static_values_json.has_value(),
1387  else
1388  writable_symbol.value = get_clinit_wrapper_body(
1389  function_id,
1390  symbol_table,
1391  language_options->nondet_static,
1392  language_options->static_values_json.has_value(),
1396  break;
1397  case synthetic_method_typet::USER_SPECIFIED_STATIC_INITIALIZER:
1398  {
1399  const auto class_name =
1400  declaring_class(symbol_table.lookup_ref(function_id));
1401  INVARIANT(
1402  class_name, "user_specified_clinit must be declared by a class.");
1403  INVARIANT(
1404  language_options->static_values_json.has_value(),
1405  "static-values JSON must be available");
1406  writable_symbol.value = get_user_specified_clinit_body(
1407  *class_name,
1408  *language_options->static_values_json,
1409  symbol_table,
1410  needed_lazy_methods,
1411  language_options->max_user_array_length,
1412  references,
1413  class_to_declared_symbols.get(symbol_table));
1414  break;
1415  }
1416  case synthetic_method_typet::STUB_CLASS_STATIC_INITIALIZER:
1417  writable_symbol.value =
1419  function_id,
1420  symbol_table,
1424  break;
1425  case synthetic_method_typet::INVOKEDYNAMIC_CAPTURE_CONSTRUCTOR:
1426  writable_symbol.value = invokedynamic_synthetic_constructor(
1427  function_id, symbol_table, get_message_handler());
1428  break;
1429  case synthetic_method_typet::INVOKEDYNAMIC_METHOD:
1430  writable_symbol.value = invokedynamic_synthetic_method(
1431  function_id, symbol_table, get_message_handler());
1432  break;
1434  {
1435  INVARIANT(
1436  cmb,
1437  "CProver.createArrayWithType should only be registered if "
1438  "we have a real implementation available");
1440  writable_symbol, cmb->get().method.local_variable_table, symbol_table);
1441  writable_symbol.value = create_array_with_type_body(
1442  function_id, symbol_table, get_message_handler());
1443  break;
1444  }
1445  }
1446  // Notify lazy methods of static calls made from the newly generated
1447  // function:
1449  to_code(writable_symbol.value), needed_lazy_methods);
1450  return false;
1451  }
1452 
1453  // No string solver or static init wrapper implementation;
1454  // check if have bytecode for it
1455  if(cmb)
1456  {
1458  symbol_table.lookup_ref(cmb->get().class_id),
1459  cmb->get().method,
1460  symbol_table,
1462  language_options->max_user_array_length,
1463  language_options->throw_assertion_error,
1464  std::move(needed_lazy_methods),
1467  language_options->threading_support,
1468  language_options->method_context,
1469  language_options->assert_no_exceptions_thrown);
1470  return false;
1471  }
1472 
1473  if(needed_lazy_methods)
1474  {
1475  // The return of an opaque function is a source of an otherwise invisible
1476  // instantiation, so here we ensure we've loaded the appropriate classes.
1477  const java_method_typet function_type = to_java_method_type(symbol.type);
1478  if(
1479  const pointer_typet *pointer_return_type =
1480  type_try_dynamic_cast<pointer_typet>(function_type.return_type()))
1481  {
1482  // If the return type is abstract, we won't forcibly instantiate it here
1483  // otherwise this can cause abstract methods to be explictly called
1484  // TODO(tkiley): Arguably no abstract class should ever be added to
1485  // TODO(tkiley): ci_lazy_methods_neededt, but this needs further
1486  // TODO(tkiley): investigation
1487  namespacet ns{symbol_table};
1488  const java_class_typet &underlying_type =
1489  to_java_class_type(ns.follow(pointer_return_type->subtype()));
1490 
1491  if(!underlying_type.is_abstract())
1492  needed_lazy_methods->add_all_needed_classes(*pointer_return_type);
1493  }
1494  }
1495 
1496  return true;
1497 }
1498 
1500 {
1501  PRECONDITION(language_options.has_value());
1502  return false;
1503 }
1504 
1506 {
1509  parse_trees.front().output(out);
1510  if(parse_trees.size() > 1)
1511  {
1512  out << "\n\nClass has the following overlays:\n\n";
1513  for(auto parse_tree_it = std::next(parse_trees.begin());
1514  parse_tree_it != parse_trees.end();
1515  ++parse_tree_it)
1516  {
1517  parse_tree_it->output(out);
1518  }
1519  out << "End of class overlays.\n";
1520  }
1521 }
1522 
1523 std::unique_ptr<languaget> new_java_bytecode_language()
1524 {
1525  return util_make_unique<java_bytecode_languaget>();
1526 }
1527 
1529  const exprt &expr,
1530  std::string &code,
1531  const namespacet &ns)
1532 {
1533  code=expr2java(expr, ns);
1534  return false;
1535 }
1536 
1538  const typet &type,
1539  std::string &code,
1540  const namespacet &ns)
1541 {
1542  code=type2java(type, ns);
1543  return false;
1544 }
1545 
1547  const std::string &code,
1548  const std::string &module,
1549  exprt &expr,
1550  const namespacet &ns)
1551 {
1552 #if 0
1553  expr.make_nil();
1554 
1555  // no preprocessing yet...
1556 
1557  std::istringstream i_preprocessed(code);
1558 
1559  // parsing
1560 
1561  java_bytecode_parser.clear();
1562  java_bytecode_parser.filename="";
1563  java_bytecode_parser.in=&i_preprocessed;
1564  java_bytecode_parser.set_message_handler(message_handler);
1565  java_bytecode_parser.grammar=java_bytecode_parsert::EXPRESSION;
1566  java_bytecode_parser.mode=java_bytecode_parsert::GCC;
1567  java_bytecode_scanner_init();
1568 
1569  bool result=java_bytecode_parser.parse();
1570 
1571  if(java_bytecode_parser.parse_tree.items.empty())
1572  result=true;
1573  else
1574  {
1575  expr=java_bytecode_parser.parse_tree.items.front().value();
1576 
1577  result=java_bytecode_convert(expr, "", message_handler);
1578 
1579  // typecheck it
1580  if(!result)
1582  }
1583 
1584  // save some memory
1585  java_bytecode_parser.clear();
1586 
1587  return result;
1588 #else
1589  // unused parameters
1590  (void)code;
1591  (void)module;
1592  (void)expr;
1593  (void)ns;
1594 #endif
1595 
1596  return true; // fail for now
1597 }
1598 
1600 {
1601 }
1602 
1606 std::vector<load_extra_methodst>
1608 {
1609  (void)options; // unused parameter
1610  return {};
1611 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
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:40
java_class_loader_baset::jar_pool
jar_poolt jar_pool
a cache for jar_filet, by path name
Definition: java_class_loader_base.h:41
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:380
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:1335
JAVA_CLASS_MODEL_SUFFIX
#define JAVA_CLASS_MODEL_SUFFIX
Definition: java_bytecode_language.h:270
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:605
java_bytecode_languaget::extensions
std::set< std::string > extensions() const override
Definition: java_bytecode_language.cpp:271
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:719
lazy_class_to_declared_symbols_mapt::reinitialize
void reinitialize()
Definition: java_bytecode_language.cpp:136
java_string_library_preprocesst::code_for_function
codet code_for_function(const symbolt &symbol, symbol_table_baset &symbol_table, message_handlert &message_handler)
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:1457
symbolt::is_state_var
bool is_state_var
Definition: symbol.h:62
symbol_tablet
The symbol table.
Definition: symbol_table.h:14
exprt::depth_cbegin
const_depth_iteratort depth_cbegin() const
Definition: expr.cpp:273
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:247
LAZY_METHODS_MODE_EAGER
@ LAZY_METHODS_MODE_EAGER
Definition: java_bytecode_language.h:184
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:259
to_side_effect_expr_function_call
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Definition: std_code.h:2185
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:1006
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 the body for the synthetic method implementing an invokedynamic method.
Definition: lambda_synthesis.cpp:773
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:55
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:29
main_function_resultt::main_function
symbolt main_function
Definition: java_entry_point.h:96
java_bytecode_languaget::pointer_type_selector
const std::unique_ptr< const select_pointer_typet > pointer_type_selector
Definition: java_bytecode_language.h:386
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:358
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:577
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:264
optionst
Definition: options.h:23
irept::make_nil
void make_nil()
Definition: irep.h:465
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:391
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:1546
typet
The type of an expression, extends irept.
Definition: type.h:28
optionst::get_option
const std::string get_option(const std::string &option) const
Definition: options.cpp:67
transform
static abstract_object_pointert transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns)
Definition: abstract_value_object.cpp:159
messaget::status
mstreamt & status() const
Definition: message.h:414
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:518
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:210
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:1161
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:523
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:334
load_method_by_regex.h
Process a pattern to use as a regex for selecting extra entry points for ci_lazy_methodst.
method_bytecodet::opt_reft
optionalt< std::reference_wrapper< const class_method_and_bytecodet > > opt_reft
Definition: ci_lazy_methods.h:44
java_bytecode_languaget::language_options
optionalt< java_bytecode_language_optionst > language_options
Definition: java_bytecode_language.h:375
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:403
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:571
prefix.h
new_java_bytecode_language
std::unique_ptr< languaget > new_java_bytecode_language()
Definition: java_bytecode_language.cpp:1523
configt::main
optionalt< std::string > main
Definition: config.h:260
invariant.h
java_string_literal_expr.h
Representation of a constant Java string.
method_bytecodet::get
opt_reft get(const irep_idt &method_id)
Definition: ci_lazy_methods.h:80
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:376
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:1227
exprt
Base class for all expressions.
Definition: expr.h:54
java_string_library_preprocesst::implements_function
bool implements_function(const irep_idt &function_id) const
Definition: java_string_library_preprocess.cpp:1417
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:456
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:874
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:399
struct_tag_typet
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:449
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:1537
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:487
invalid_source_file_exceptiont
Thrown when we can't handle something in an input source file.
Definition: exception_utils.h:171
options.h
Options.
component
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:48
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:3284
java_string_library_preprocesst::initialize_known_type_table
void initialize_known_type_table()
Definition: java_string_library_preprocess.cpp:1506
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:351
irep_idt
dstringt irep_idt
Definition: irep.h:37
messaget::eom
static eomt eom
Definition: message.h:297
to_side_effect_expr
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1952
method_convertert
std::function< bool(const irep_idt &function_id, ci_lazy_methods_neededt)> method_convertert
Definition: ci_lazy_methods.h:91
to_json_array
json_arrayt & to_json_array(jsont &json)
Definition: json.h:426
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:80
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:1499
jsont
Definition: json.h:27
class_to_declared_symbols
std::unordered_multimap< irep_idt, symbolt > class_to_declared_symbols(const symbol_tablet &symbol_table)
Definition: java_static_initializers.cpp:779
java_class_loader_baset::add_classpath_entry
void add_classpath_entry(const std::string &, message_handlert &)
Appends an entry to the class path, used for loading classes.
Definition: java_class_loader_base.cpp:22
configt::javat::classpath
classpatht classpath
Definition: config.h:246
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:56
java_object_factory_parameterst::set
void set(const optionst &)
Assigns the parameters from given options.
Definition: java_object_factory_parameters.cpp:15
symbol_tablet::begin
virtual iteratort begin() override
Definition: symbol_table.h:108
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:184
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:583
java_bytecode_languaget::stub_global_initializer_factory
stub_global_initializer_factoryt stub_global_initializer_factory
Definition: java_bytecode_language.h:392
main_function_resultt::is_error
bool is_error() const
Definition: java_entry_point.h:115
main_function_resultt::is_success
bool is_success() const
Definition: java_entry_point.h:111
symbolt::pretty_name
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
java_class_typet
Definition: java_types.h:197
to_code
const codet & to_code(const exprt &expr)
Definition: std_code.h:153
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:690
java_bytecode_language_optionst::lazy_methods_mode
lazy_methods_modet lazy_methods_mode
Definition: java_bytecode_language.h:236
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
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:791
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:645
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
java_class_loadert::can_load_class
bool can_load_class(const irep_idt &class_name, message_handlert &)
Checks whether class_name is parseable from the classpath, ignoring class loading limits.
Definition: java_class_loader.cpp:107
const_depth_iteratort
Definition: expr_iterator.h:219
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:391
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:731
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:260
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:1607
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
messaget::result
mstreamt & result() const
Definition: message.h:409
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:29
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
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:57
java_bytecode_languaget::main_jar_classes
std::vector< irep_idt > main_jar_classes
Definition: java_bytecode_language.h:377
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:510
symbol_tablet::end
virtual iteratort end() override
Definition: symbol_table.h:112
null_pointer_exprt
The null pointer constant.
Definition: pointer_expr.h:703
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:49
java_bytecode_languaget::~java_bytecode_languaget
virtual ~java_bytecode_languaget()
Definition: java_bytecode_language.cpp:1599
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:563
java_bytecode_languaget::java_class_loader
java_class_loadert java_class_loader
Definition: java_bytecode_language.h:378
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:228
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:109
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:1186
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:463
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:109
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:1116
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:1441
create_array_with_type_intrinsic.h
Implementation of CProver.createArrayWithType intrinsic.
java_bytecode_languaget::show_parse
void show_parse(std::ostream &out) override
Definition: java_bytecode_language.cpp:1505
java_class_loader.h
java_class_loader_limit.h
limit class path loading
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:240
get_context
prefix_filtert get_context(const optionst &options)
Definition: java_bytecode_language.cpp:114
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:1056
INITIALIZE_FUNCTION
#define INITIALIZE_FUNCTION
Definition: static_lifetime_init.h:22
cmdlinet::get_value
std::string get_value(char option) const
Definition: cmdline.cpp:47
java_bytecode_internal_additions.h
java_entry_point.h
java_bytecode_languaget::initialize_class_loader
void initialize_class_loader()
Definition: java_bytecode_language.cpp:297
select_pointer_typet
Definition: select_pointer_type.h:23
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:62
messaget::set_message_handler
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:179
struct_typet::bases
const basest & bases() const
Get the collection of base classes/structs.
Definition: std_types.h:262
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:732
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:1185
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:74
struct_union_typet::has_component
bool has_component(const irep_idt &component_name) const
Definition: std_types.h:157
throwMainClassLoadingError
static void throwMainClassLoadingError(const std::string &main_class)
Definition: java_bytecode_language.cpp:319
irept::is_nil
bool is_nil() const
Definition: irep.h:387
irept::id
const irep_idt & id() const
Definition: irep.h:407
message_handlert
Definition: message.h:28
class_hierarchyt::idst
std::vector< irep_idt > idst
Definition: class_hierarchy.h:45
java_bytecode_convert_method.h
JAVA Bytecode Language Conversion.
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:241
java_bytecode_languaget::modules_provided
void modules_provided(std::set< std::string > &modules) override
Definition: java_bytecode_language.cpp:276
java_bytecode_languaget::string_preprocess
java_string_library_preprocesst string_preprocess
Definition: java_bytecode_language.h:381
java_bytecode_parse_treet::classt::methods
methodst methods
Definition: java_bytecode_parse_tree.h:280
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:232
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:65
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:572
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:89
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:451
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
Collect methods needed to be loaded using the lazy method.
lazy_class_to_declared_symbols_mapt::get
std::unordered_multimap< irep_idt, symbolt > & get(const symbol_tablet &symbol_table)
Definition: java_bytecode_language.cpp:126
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:221
java_class_loadert::load_entire_jar
std::vector< irep_idt > load_entire_jar(const std::string &jar_path, message_handlert &)
Load all class files from a .jar file.
Definition: java_class_loader.cpp:212
side_effect_exprt::get_statement
const irep_idt & get_statement() const
Definition: std_code.h:1918
config
configt config
Definition: config.cpp:25
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:479
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:591
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:1528
lambda_synthesis.h
Java lambda code synthesis.
java_class_typet::components
const componentst & components() const
Definition: java_types.h:224
java_bytecode_parse_treet::parsed_class
classt parsed_class
Definition: java_bytecode_parse_tree.h:310
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
messaget::get_message_handler
message_handlert & get_message_handler()
Definition: message.h:184
class_hierarchy.h
Class Hierarchy.
java_bytecode_languaget::get_pointer_type_selector
const select_pointer_typet & get_pointer_type_selector() const
Definition: java_bytecode_language.cpp:1150
java_bytecode_languaget::class_hierarchy
class_hierarchyt class_hierarchy
Definition: java_bytecode_language.h:393
java_internal_additions
void java_internal_additions(symbol_table_baset &dest)
Definition: java_bytecode_internal_additions.cpp:23
fieldref_exprt::class_name
irep_idt class_name() const
Definition: java_bytecode_parse_tree.h:346
messaget::message_handler
message_handlert * message_handler
Definition: message.h:439
java_bytecode_languaget::typecheck
bool typecheck(symbol_tablet &context, const std::string &module) override
Definition: java_bytecode_language.cpp:807
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:245
expr_iterator.h
Forward depth-first search iterators These iterators' copy operations are expensive,...
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:47
java_bytecode_languaget::set_message_handler
void set_message_handler(message_handlert &message_handler) override
Definition: java_bytecode_language.cpp:291
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:72
suffix.h
to_json_object
json_objectt & to_json_object(jsont &json)
Definition: json.h:444
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:49
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:925
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:45
exprt::depth_cend
const_depth_iteratort depth_cend() const
Definition: expr.cpp:275
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:83
cmdline.h
exception_needed_classes
const std::vector< std::string > exception_needed_classes
Definition: java_bytecode_instrument.cpp:75
ci_lazy_methodst
Definition: ci_lazy_methods.h:97
symbolt
Symbol table entry.
Definition: symbol.h:28
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
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:338
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:521
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:223
symbol_table_buildert
Author: Diffblue Ltd.
Definition: symbol_table_builder.h:14
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
symbolt::is_type
bool is_type
Definition: symbol.h:61
jsont::is_array
bool is_array() const
Definition: json.h:61
java_bytecode_language_optionst::extra_methods
std::vector< load_extra_methodst > extra_methods
Definition: java_bytecode_language.h:250
java_bytecode_language_optionst::assert_uncaught_exceptions
bool assert_uncaught_exceptions
Definition: java_bytecode_language.h:224
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:600
java_bytecode_language_optionst::throw_assertion_error
bool throw_assertion_error
Definition: java_bytecode_language.h:225
configt::java
struct configt::javat java
type2java
std::string type2java(const typet &type, const namespacet &ns)
Definition: expr2java.cpp:457
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:185
java_bytecode_languaget::object_factory_parameters
java_object_factory_parameterst object_factory_parameters
Definition: java_bytecode_language.h:379
config.h
expr2java
std::string expr2java(const exprt &expr, const namespacet &ns)
Definition: expr2java.cpp:450
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:200
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:645
java_bytecode_language_optionst::threading_support
bool threading_support
Definition: java_bytecode_language.h:226
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:541
ci_lazy_methods_neededt
Definition: ci_lazy_methods_needed.h:26
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:1515
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:64
jsont::is_object
bool is_object() const
Definition: json.h:56
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:582
java_bytecode_languaget::parse_from_main_class
void parse_from_main_class()
Definition: java_bytecode_language.cpp:325
journalling_symbol_tablet::get_inserted
const changesett & get_inserted() const
Definition: journalling_symbol_table.h:146
java_class_loader_baset::clear_classpath
void clear_classpath()
Clear all classpath entries.
Definition: java_class_loader_base.h:25
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:248
expr2java.h
static_lifetime_init.h
address_of_exprt
Operator to return the address of an object.
Definition: pointer_expr.h:341
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
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:350
to_java_method_type
const java_method_typet & to_java_method_type(const typet &type)
Definition: java_types.h:184
java_class_typet::get_is_stub
bool get_is_stub() const
Definition: java_types.h:398
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:222
lift_clinit_calls.h
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
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:186
java_utils.h
symbol_table_builder.h
messaget::warning
mstreamt & warning() const
Definition: message.h:404
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:282
cmdlinet::get_values
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:108
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/removedA caller can pass a journa...
Definition: journalling_symbol_table.h:36
java_method_typet
Definition: java_types.h:101
java_bytecode_language_optionst
Definition: java_bytecode_language.h:215
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:1001
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:3206
lazy_class_to_declared_symbols_mapt::map
std::unordered_multimap< irep_idt, symbolt > map
Definition: java_bytecode_language.h:211
java_bytecode_typecheck.h
JAVA Bytecode Language Type Checking.
java_bytecode_convert_class.h
JAVA Bytecode Language Conversion.
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:235
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:33
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:22
java_bytecode_language_optionst::nondet_static
bool nondet_static
Definition: java_bytecode_language.h:227