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  {
879  std::vector<irep_idt> methods_to_check;
880 
881  // Careful not to add to the symtab while iterating over it:
882  for(const auto &id_and_symbol : symbol_table)
883  {
884  const auto &symbol = id_and_symbol.second;
885  const auto &id = symbol.name;
886  if(can_cast_type<code_typet>(symbol.type) && method_bytecode.get(id))
887  {
888  methods_to_check.push_back(id);
889  }
890  }
891 
892  for(const auto &id : methods_to_check)
893  {
895  id,
896  method_bytecode.get(id)->get().method.instructions,
897  symbol_table,
900  }
901  }
902 
903  // Now that all classes have been created in the symbol table we can populate
904  // the class hierarchy:
905  class_hierarchy(symbol_table);
906 
907  // find and mark all implicitly generic class types
908  // this can only be done once all the class symbols have been created
909  for(const auto &c : java_class_loader.get_class_with_overlays_map())
910  {
911  if(c.second.front().parsed_class.name.empty())
912  continue;
913  try
914  {
916  c.second.front().parsed_class.name, symbol_table);
917  }
919  {
921  << "Not marking class " << c.first
922  << " implicitly generic due to missing outer class symbols"
923  << messaget::eom;
924  }
925  }
926 
927  // Infer fields on opaque types based on the method instructions just loaded.
928  // For example, if we don't have bytecode for field x of class A, but we can
929  // see an int-typed getfield instruction referring to it, add that field now.
930  for(auto &class_to_trees : java_class_loader.get_class_with_overlays_map())
931  {
932  for(const java_bytecode_parse_treet &parse_tree : class_to_trees.second)
933  infer_opaque_type_fields(parse_tree, symbol_table);
934  }
935 
936  // Create global variables for constants (String and Class literals) up front.
937  // This means that when running with lazy loading, we will be aware of these
938  // literal globals' existence when __CPROVER_initialize is generated in
939  // `generate_support_functions`.
940  const std::size_t before_constant_globals_size = symbol_table.symbols.size();
941  for(auto &class_to_trees : java_class_loader.get_class_with_overlays_map())
942  {
943  for(java_bytecode_parse_treet &parse_tree : class_to_trees.second)
944  {
946  parse_tree, symbol_table, language_options->string_refinement_enabled);
947  }
948  }
949  status() << "Java: added "
950  << (symbol_table.symbols.size() - before_constant_globals_size)
951  << " String or Class constant symbols"
952  << messaget::eom;
953 
954  // For each reference to a stub global (that is, a global variable declared on
955  // a class we don't have bytecode for, and therefore don't know the static
956  // initialiser for), create a synthetic static initialiser (clinit method)
957  // to nondet initialise it.
958  // Note this must be done before making static initialiser wrappers below, as
959  // this makes a Classname.clinit method, then the next pass makes a wrapper
960  // that ensures it is only run once, and that static initialisation happens
961  // in class-graph topological order.
962 
963  {
964  journalling_symbol_tablet symbol_table_journal =
965  journalling_symbol_tablet::wrap(symbol_table);
966  for(auto &class_to_trees : java_class_loader.get_class_with_overlays_map())
967  {
968  for(const java_bytecode_parse_treet &parse_tree : class_to_trees.second)
969  {
971  parse_tree, symbol_table_journal, class_hierarchy, *this);
972  }
973  }
974 
976  symbol_table, symbol_table_journal.get_inserted(), synthetic_methods);
977  }
978 
980  symbol_table,
982  language_options->threading_support,
983  language_options->static_values_json.has_value());
984 
986 
987  // Now incrementally elaborate methods
988  // that are reachable from this entry point.
989  switch(language_options->lazy_methods_mode)
990  {
992  // ci = context-insensitive
993  if(do_ci_lazy_method_conversion(symbol_table))
994  return true;
995  break;
997  {
998  symbol_table_buildert symbol_table_builder =
999  symbol_table_buildert::wrap(symbol_table);
1000 
1001  journalling_symbol_tablet journalling_symbol_table =
1002  journalling_symbol_tablet::wrap(symbol_table_builder);
1003 
1004  // Convert all synthetic methods:
1005  for(const auto &function_id_and_type : synthetic_methods)
1006  {
1008  function_id_and_type.first,
1009  journalling_symbol_table,
1011  }
1012  // Convert all methods for which we have bytecode now
1013  for(const auto &method_sig : method_bytecode)
1014  {
1016  method_sig.first, journalling_symbol_table, class_to_declared_symbols);
1017  }
1019  INITIALIZE_FUNCTION, journalling_symbol_table, class_to_declared_symbols);
1020  // Now convert all newly added string methods
1021  for(const auto &fn_name : journalling_symbol_table.get_inserted())
1022  {
1024  convert_single_method(fn_name, symbol_table, class_to_declared_symbols);
1025  }
1026  }
1027  break;
1029  // Our caller is in charge of elaborating methods on demand.
1030  break;
1031  }
1032 
1033  // now instrument runtime exceptions
1035  symbol_table,
1036  language_options->throw_runtime_exceptions,
1038 
1039  // now typecheck all
1040  bool res = java_bytecode_typecheck(
1041  symbol_table,
1043  language_options->string_refinement_enabled);
1044 
1045  // now instrument thread-blocks and synchronized methods.
1046  if(language_options->threading_support)
1047  {
1048  convert_threadblock(symbol_table);
1050  }
1051 
1052  return res;
1053 }
1054 
1056  symbol_tablet &symbol_table)
1057 {
1058  PRECONDITION(language_options.has_value());
1059 
1060  symbol_table_buildert symbol_table_builder =
1061  symbol_table_buildert::wrap(symbol_table);
1062 
1065  if(!res.is_success())
1066  return res.is_error();
1067 
1068  // Load the main function into the symbol table to get access to its
1069  // parameter names
1070  convert_lazy_method(res.main_function.name, symbol_table_builder);
1071 
1072  const symbolt &symbol =
1073  symbol_table_builder.lookup_ref(res.main_function.name);
1074  if(symbol.value.is_nil())
1075  {
1077  "the program has no entry point",
1078  "function",
1079  "Check that the specified entry point is included by your "
1080  "--context-include or --context-exclude options");
1081  }
1082 
1083  // generate the test harness in __CPROVER__start and a call the entry point
1084  return java_entry_point(
1085  symbol_table_builder,
1086  main_class,
1088  language_options->assume_inputs_non_null,
1089  language_options->assert_uncaught_exceptions,
1092  language_options->string_refinement_enabled,
1093  [&](const symbolt &function, symbol_table_baset &symbol_table) {
1094  return java_build_arguments(
1095  function,
1096  symbol_table,
1097  language_options->assume_inputs_non_null,
1098  object_factory_parameters,
1099  get_pointer_type_selector(),
1100  get_message_handler());
1101  });
1102 }
1103 
1116  symbol_tablet &symbol_table)
1117 {
1118  symbol_table_buildert symbol_table_builder =
1119  symbol_table_buildert::wrap(symbol_table);
1120 
1122 
1123  const method_convertert method_converter =
1124  [this, &symbol_table_builder, &class_to_declared_symbols](
1125  const irep_idt &function_id,
1126  ci_lazy_methods_neededt lazy_methods_needed) {
1127  return convert_single_method(
1128  function_id,
1129  symbol_table_builder,
1130  std::move(lazy_methods_needed),
1132  };
1133 
1134  ci_lazy_methodst method_gather(
1135  symbol_table,
1136  main_class,
1138  language_options->extra_methods,
1140  language_options->java_load_classes,
1144 
1145  return method_gather(symbol_table, method_bytecode, method_converter);
1146 }
1147 
1148 const select_pointer_typet &
1150 {
1151  PRECONDITION(pointer_type_selector.get()!=nullptr);
1152  return *pointer_type_selector;
1153 }
1154 
1161  std::unordered_set<irep_idt> &methods) const
1162 {
1163  const std::string cprover_class_prefix = "java::org.cprover.CProver.";
1164 
1165  // Add all string solver methods to map
1167  // Add all concrete methods to map
1168  for(const auto &kv : method_bytecode)
1169  methods.insert(kv.first);
1170  // Add all synthetic methods to map
1171  for(const auto &kv : synthetic_methods)
1172  methods.insert(kv.first);
1173  methods.insert(INITIALIZE_FUNCTION);
1174 }
1175 
1185  const irep_idt &function_id,
1186  symbol_table_baset &symtab)
1187 {
1188  const symbolt &symbol = symtab.lookup_ref(function_id);
1189  if(symbol.value.is_not_nil())
1190  return;
1191 
1192  journalling_symbol_tablet symbol_table=
1194 
1196  convert_single_method(function_id, symbol_table, class_to_declared_symbols);
1197 
1198  // Instrument runtime exceptions (unless symbol is a stub or is the
1199  // INITIALISE_FUNCTION).
1200  if(symbol.value.is_not_nil() && function_id != INITIALIZE_FUNCTION)
1201  {
1203  symbol_table,
1204  symbol_table.get_writeable_ref(function_id),
1205  language_options->throw_runtime_exceptions,
1207  }
1208 
1209  // now typecheck this function
1211  symbol_table,
1213  language_options->string_refinement_enabled);
1214 }
1215 
1227  const codet &function_body,
1228  optionalt<ci_lazy_methods_neededt> needed_lazy_methods)
1229 {
1230  if(needed_lazy_methods)
1231  {
1232  for(const_depth_iteratort it = function_body.depth_cbegin();
1233  it != function_body.depth_cend();
1234  ++it)
1235  {
1236  if(it->id() == ID_code)
1237  {
1238  const auto fn_call = expr_try_dynamic_cast<code_function_callt>(*it);
1239  if(!fn_call)
1240  continue;
1241  const symbol_exprt *fn_sym =
1242  expr_try_dynamic_cast<symbol_exprt>(fn_call->function());
1243  if(fn_sym)
1244  needed_lazy_methods->add_needed_method(fn_sym->get_identifier());
1245  }
1246  else if(
1247  it->id() == ID_side_effect &&
1248  to_side_effect_expr(*it).get_statement() == ID_function_call)
1249  {
1250  const auto &call_expr = to_side_effect_expr_function_call(*it);
1251  const symbol_exprt *fn_sym =
1252  expr_try_dynamic_cast<symbol_exprt>(call_expr.function());
1253  if(fn_sym)
1254  {
1255  INVARIANT(
1256  false,
1257  "Java synthetic methods are not "
1258  "expected to produce side_effect_expr_function_callt. If "
1259  "that has changed, remove this invariant. Also note that "
1260  "as of the time of writing remove_virtual_functions did "
1261  "not support this form of function call.");
1262  // needed_lazy_methods->add_needed_method(fn_sym->get_identifier());
1263  }
1264  }
1265  }
1266  }
1267 }
1268 
1282  const irep_idt &function_id,
1283  symbol_table_baset &symbol_table,
1284  optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
1286 {
1287  const symbolt &symbol = symbol_table.lookup_ref(function_id);
1288 
1289  // Nothing to do if body is already loaded
1290  if(symbol.value.is_not_nil())
1291  return false;
1292 
1293  if(function_id == INITIALIZE_FUNCTION)
1294  {
1296  symbol_table,
1297  symbol.location,
1298  language_options->assume_inputs_non_null,
1301  language_options->string_refinement_enabled,
1303  return false;
1304  }
1305 
1306  INVARIANT(declaring_class(symbol), "Method must have a declaring class.");
1307 
1308  bool ret = convert_single_method_code(
1309  function_id, symbol_table, needed_lazy_methods, class_to_declared_symbols);
1310 
1311  if(symbol.value.is_not_nil() && language_options->should_lift_clinit_calls)
1312  {
1313  auto &writable_symbol = symbol_table.get_writeable_ref(function_id);
1314  writable_symbol.value =
1315  lift_clinit_calls(std::move(to_code(writable_symbol.value)));
1316  }
1317 
1318  INVARIANT(declaring_class(symbol), "Method must have a declaring class.");
1319 
1320  return ret;
1321 }
1322 
1335  const irep_idt &function_id,
1336  symbol_table_baset &symbol_table,
1337  optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
1339 {
1340  const auto &symbol = symbol_table.lookup_ref(function_id);
1341  PRECONDITION(symbol.value.is_nil());
1342 
1343  // Get bytecode for specified function if we have it
1344  method_bytecodet::opt_reft cmb = method_bytecode.get(function_id);
1345 
1346  synthetic_methods_mapt::iterator synthetic_method_it;
1347 
1348  // Check if have a string solver implementation
1349  if(string_preprocess.implements_function(function_id))
1350  {
1351  symbolt &writable_symbol = symbol_table.get_writeable_ref(function_id);
1352  // Load parameter names from any extant bytecode before filling in body
1353  if(cmb)
1354  {
1356  writable_symbol, cmb->get().method.local_variable_table, symbol_table);
1357  }
1358  // Populate body of the function with code generated by string preprocess
1359  codet generated_code =
1360  string_preprocess.code_for_function(writable_symbol, symbol_table);
1361  // String solver can make calls to functions that haven't yet been seen.
1362  // Add these to the needed_lazy_methods collection
1363  notify_static_method_calls(generated_code, needed_lazy_methods);
1364  writable_symbol.value = std::move(generated_code);
1365  return false;
1366  }
1367  else if(
1368  (synthetic_method_it = synthetic_methods.find(function_id)) !=
1369  synthetic_methods.end())
1370  {
1371  // Synthetic method (i.e. one generated by the Java frontend and which
1372  // doesn't occur in the source bytecode):
1373  symbolt &writable_symbol = symbol_table.get_writeable_ref(function_id);
1374  switch(synthetic_method_it->second)
1375  {
1377  if(language_options->threading_support)
1378  writable_symbol.value = get_thread_safe_clinit_wrapper_body(
1379  function_id,
1380  symbol_table,
1381  language_options->nondet_static,
1382  language_options->static_values_json.has_value(),
1386  else
1387  writable_symbol.value = get_clinit_wrapper_body(
1388  function_id,
1389  symbol_table,
1390  language_options->nondet_static,
1391  language_options->static_values_json.has_value(),
1395  break;
1397  {
1398  const auto class_name =
1399  declaring_class(symbol_table.lookup_ref(function_id));
1400  INVARIANT(
1401  class_name, "user_specified_clinit must be declared by a class.");
1402  INVARIANT(
1403  language_options->static_values_json.has_value(),
1404  "static-values JSON must be available");
1405  writable_symbol.value = get_user_specified_clinit_body(
1406  *class_name,
1407  *language_options->static_values_json,
1408  symbol_table,
1409  needed_lazy_methods,
1410  language_options->max_user_array_length,
1411  references,
1412  class_to_declared_symbols.get(symbol_table));
1413  break;
1414  }
1416  writable_symbol.value =
1418  function_id,
1419  symbol_table,
1423  break;
1425  writable_symbol.value = invokedynamic_synthetic_constructor(
1426  function_id, symbol_table, get_message_handler());
1427  break;
1429  writable_symbol.value = invokedynamic_synthetic_method(
1430  function_id, symbol_table, get_message_handler());
1431  break;
1433  {
1434  INVARIANT(
1435  cmb,
1436  "CProver.createArrayWithType should only be registered if "
1437  "we have a real implementation available");
1439  writable_symbol, cmb->get().method.local_variable_table, symbol_table);
1440  writable_symbol.value = create_array_with_type_body(
1441  function_id, symbol_table, get_message_handler());
1442  break;
1443  }
1444  }
1445  // Notify lazy methods of static calls made from the newly generated
1446  // function:
1448  to_code(writable_symbol.value), needed_lazy_methods);
1449  return false;
1450  }
1451 
1452  // No string solver or static init wrapper implementation;
1453  // check if have bytecode for it
1454  if(cmb)
1455  {
1457  symbol_table.lookup_ref(cmb->get().class_id),
1458  cmb->get().method,
1459  symbol_table,
1461  language_options->max_user_array_length,
1462  language_options->throw_assertion_error,
1463  std::move(needed_lazy_methods),
1466  language_options->threading_support,
1467  language_options->method_context,
1468  language_options->assert_no_exceptions_thrown);
1469  return false;
1470  }
1471 
1472  if(needed_lazy_methods)
1473  {
1474  // The return of an opaque function is a source of an otherwise invisible
1475  // instantiation, so here we ensure we've loaded the appropriate classes.
1476  const java_method_typet function_type = to_java_method_type(symbol.type);
1477  if(
1478  const pointer_typet *pointer_return_type =
1479  type_try_dynamic_cast<pointer_typet>(function_type.return_type()))
1480  {
1481  // If the return type is abstract, we won't forcibly instantiate it here
1482  // otherwise this can cause abstract methods to be explictly called
1483  // TODO(tkiley): Arguably no abstract class should ever be added to
1484  // TODO(tkiley): ci_lazy_methods_neededt, but this needs further
1485  // TODO(tkiley): investigation
1486  namespacet ns{symbol_table};
1487  const java_class_typet &underlying_type =
1488  to_java_class_type(ns.follow(pointer_return_type->subtype()));
1489 
1490  if(!underlying_type.is_abstract())
1491  needed_lazy_methods->add_all_needed_classes(*pointer_return_type);
1492  }
1493  }
1494 
1495  return true;
1496 }
1497 
1499 {
1500  PRECONDITION(language_options.has_value());
1501  return false;
1502 }
1503 
1505 {
1508  parse_trees.front().output(out);
1509  if(parse_trees.size() > 1)
1510  {
1511  out << "\n\nClass has the following overlays:\n\n";
1512  for(auto parse_tree_it = std::next(parse_trees.begin());
1513  parse_tree_it != parse_trees.end();
1514  ++parse_tree_it)
1515  {
1516  parse_tree_it->output(out);
1517  }
1518  out << "End of class overlays.\n";
1519  }
1520 }
1521 
1522 std::unique_ptr<languaget> new_java_bytecode_language()
1523 {
1524  return util_make_unique<java_bytecode_languaget>();
1525 }
1526 
1528  const exprt &expr,
1529  std::string &code,
1530  const namespacet &ns)
1531 {
1532  code=expr2java(expr, ns);
1533  return false;
1534 }
1535 
1537  const typet &type,
1538  std::string &code,
1539  const namespacet &ns)
1540 {
1541  code=type2java(type, ns);
1542  return false;
1543 }
1544 
1546  const std::string &code,
1547  const std::string &module,
1548  exprt &expr,
1549  const namespacet &ns)
1550 {
1551 #if 0
1552  expr.make_nil();
1553 
1554  // no preprocessing yet...
1555 
1556  std::istringstream i_preprocessed(code);
1557 
1558  // parsing
1559 
1560  java_bytecode_parser.clear();
1561  java_bytecode_parser.filename="";
1562  java_bytecode_parser.in=&i_preprocessed;
1563  java_bytecode_parser.set_message_handler(message_handler);
1564  java_bytecode_parser.grammar=java_bytecode_parsert::EXPRESSION;
1565  java_bytecode_parser.mode=java_bytecode_parsert::GCC;
1566  java_bytecode_scanner_init();
1567 
1568  bool result=java_bytecode_parser.parse();
1569 
1570  if(java_bytecode_parser.parse_tree.items.empty())
1571  result=true;
1572  else
1573  {
1574  expr=java_bytecode_parser.parse_tree.items.front().value();
1575 
1576  result=java_bytecode_convert(expr, "", message_handler);
1577 
1578  // typecheck it
1579  if(!result)
1581  }
1582 
1583  // save some memory
1584  java_bytecode_parser.clear();
1585 
1586  return result;
1587 #else
1588  // unused parameters
1589  (void)code;
1590  (void)module;
1591  (void)expr;
1592  (void)ns;
1593 #endif
1594 
1595  return true; // fail for now
1596 }
1597 
1599 {
1600 }
1601 
1605 std::vector<load_extra_methodst>
1607 {
1608  (void)options; // unused parameter
1609  return {};
1610 }
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: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:62
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:1334
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:168
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:2182
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 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: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:29
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:24
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:585
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:1545
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: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: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:1160
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:335
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: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:60
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:579
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:1522
configt::main
optionalt< std::string > main
Definition: config.h:181
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:81
java_bytecode_parse_treet::instructiont
Definition: java_bytecode_parse_tree.h:57
java_bytecode_languaget::main_class
irep_idt main_class
Definition: java_bytecode_language.h: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:1226
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:1400
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:1536
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
Options.
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:3229
java_string_library_preprocesst::initialize_known_type_table
void initialize_known_type_table()
Definition: java_string_library_preprocess.cpp:1487
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:352
irep_idt
dstringt irep_idt
Definition: irep.h:32
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:1931
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:426
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:1498
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:772
configt::javat::classpath
classpatht classpath
Definition: config.h:167
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: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:591
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:155
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:219
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:1606
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: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:3989
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:1598
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:213
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:1182
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:1115
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:1424
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:1504
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:1439
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:1055
INITIALIZE_FUNCTION
#define INITIALIZE_FUNCTION
Definition: static_lifetime_init.h:23
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: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:179
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:1184
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: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: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:281
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:458
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: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:1897
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: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: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:1527
lambda_synthesis.h
Java lambda code synthesis.
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:311
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:1149
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:347
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:439
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
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: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:444
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
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: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:1496
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: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:584
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:146
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:2786
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:400
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: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:283
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: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:999
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:3151
lazy_class_to_declared_symbols_mapt::map
std::unordered_multimap< irep_idt, symbolt > map
Definition: java_bytecode_language.h:213
java_bytecode_typecheck.h
JAVA Bytecode Language Type Checking.
validation_modet::INVARIANT
@ INVARIANT
java_bytecode_convert_class.h
JAVA Bytecode Language Conversion.
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