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 {
296 }
297 
299 {
301 
302  for(const auto &p : config.java.classpath)
304 
306  language_options->java_cp_include_files);
308  if(language_options->string_refinement_enabled)
309  {
311 
312  auto get_string_base_classes = [this](const irep_idt &id) {
314  };
315 
316  java_class_loader.set_extra_class_refs_function(get_string_base_classes);
317  }
318 }
319 
320 static void throwMainClassLoadingError(const std::string &main_class)
321 {
323  "Error: Could not find or load main class " + main_class);
324 }
325 
327 {
328  if(!main_class.empty())
329  {
330  // Try to load class
331  status() << "Trying to load Java main class: " << main_class << eom;
333  {
334  // Try to extract class name and load class
335  const auto maybe_class_name =
337  if(!maybe_class_name)
338  {
340  return;
341  }
342  status() << "Trying to load Java main class: " << maybe_class_name.value()
343  << eom;
345  maybe_class_name.value(), get_message_handler()))
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 =
359  if(parse_trees.empty() || !parse_trees.front().loading_successful)
360  {
362  }
363  }
364 }
365 
369 {
370  PRECONDITION(language_options.has_value());
374  return false;
375 }
376 
384  std::istream &instream,
385  const std::string &path)
386 {
387  PRECONDITION(language_options.has_value());
389 
390  // look at extension
391  if(has_suffix(path, ".jar"))
392  {
393  std::ifstream jar_file(path);
394  if(!jar_file.good())
395  {
397  "Error: Unable to access jarfile " + path);
398  }
399 
400  // build an object to potentially limit which classes are loaded
401  java_class_loader_limitt class_loader_limit(
402  get_message_handler(), language_options->java_cp_include_files);
404  {
405  // If we have an entry method, we can derive a main class.
406  if(config.main.has_value())
407  {
408  const std::string &entry_method = config.main.value();
409  const auto last_dot_position = entry_method.find_last_of('.');
410  main_class = entry_method.substr(0, last_dot_position);
411  }
412  else
413  {
414  auto manifest = java_class_loader.jar_pool(path).get_manifest();
415  std::string manifest_main_class = manifest["Main-Class"];
416 
417  // if the manifest declares a Main-Class line, we got a main class
418  if(
419  !manifest_main_class.empty() &&
420  !language_options->ignore_manifest_main_class)
421  {
422  main_class = manifest_main_class;
423  }
424  }
425  }
426  else
428 
429  // do we have one now?
430  if(main_class.empty())
431  {
432  status() << "JAR file without entry point: loading class files" << eom;
433  const auto classes =
435  for(const auto &c : classes)
436  main_jar_classes.push_back(c);
437  }
438  else
440  }
441  else
443 
445  return false;
446 }
447 
458  const java_bytecode_parse_treet &parse_tree,
459  symbol_tablet &symbol_table)
460 {
461  namespacet ns(symbol_table);
462  for(const auto &method : parse_tree.parsed_class.methods)
463  {
464  for(const java_bytecode_parse_treet::instructiont &instruction :
465  method.instructions)
466  {
467  const std::string statement =
468  bytecode_info[instruction.bytecode].mnemonic;
469  if(statement == "getfield" || statement == "putfield")
470  {
471  const fieldref_exprt &fieldref =
472  expr_dynamic_cast<fieldref_exprt>(instruction.args[0]);
473  irep_idt class_symbol_id = fieldref.class_name();
474  const symbolt *class_symbol = symbol_table.lookup(class_symbol_id);
475  INVARIANT(
476  class_symbol != nullptr,
477  "all types containing fields should have been loaded");
478 
479  const java_class_typet *class_type =
480  &to_java_class_type(class_symbol->type);
481  const irep_idt &component_name = fieldref.component_name();
482  while(!class_type->has_component(component_name))
483  {
484  if(class_type->get_is_stub())
485  {
486  // Accessing a field of an incomplete (opaque) type.
487  symbolt &writable_class_symbol =
488  symbol_table.get_writeable_ref(class_symbol_id);
489  auto &components =
490  to_java_class_type(writable_class_symbol.type).components();
491  components.emplace_back(component_name, fieldref.type());
492  components.back().set_base_name(component_name);
493  components.back().set_pretty_name(component_name);
494  components.back().set_is_final(true);
495  break;
496  }
497  else
498  {
499  // Not present here: check the superclass.
500  INVARIANT(
501  !class_type->bases().empty(),
502  "class '" + id2string(class_symbol->name) +
503  "' (which was missing a field '" + id2string(component_name) +
504  "' referenced from method '" + id2string(method.name) +
505  "' of class '" + id2string(parse_tree.parsed_class.name) +
506  "') should have an opaque superclass");
507  const auto &superclass_type = class_type->bases().front().type();
508  class_symbol_id = superclass_type.get_identifier();
509  class_type = &to_java_class_type(ns.follow(superclass_type));
510  }
511  }
512  }
513  }
514  }
515 }
516 
523  const irep_idt &class_id, symbol_tablet &symbol_table)
524 {
525  struct_tag_typet java_lang_Class("java::java.lang.Class");
526  symbol_exprt symbol_expr(
528  java_lang_Class);
529  if(!symbol_table.has_symbol(symbol_expr.get_identifier()))
530  {
531  symbolt new_class_symbol;
532  new_class_symbol.name = symbol_expr.get_identifier();
533  new_class_symbol.type = symbol_expr.type();
534  INVARIANT(
535  has_prefix(id2string(new_class_symbol.name), "java::"),
536  "class identifier should have 'java::' prefix");
537  new_class_symbol.base_name =
538  id2string(new_class_symbol.name).substr(6);
539  new_class_symbol.mode = ID_java;
540  new_class_symbol.is_lvalue = true;
541  new_class_symbol.is_state_var = true;
542  new_class_symbol.is_static_lifetime = true;
543  new_class_symbol.type.set(ID_C_no_nondet_initialization, true);
544  symbol_table.add(new_class_symbol);
545  }
546 
547  return symbol_expr;
548 }
549 
565  const exprt &ldc_arg0,
566  symbol_tablet &symbol_table,
567  bool string_refinement_enabled)
568 {
569  if(ldc_arg0.id() == ID_type)
570  {
571  const irep_idt &class_id = ldc_arg0.type().get(ID_identifier);
572  return
574  get_or_create_class_literal_symbol(class_id, symbol_table));
575  }
576  else if(
577  const auto &literal =
578  expr_try_dynamic_cast<java_string_literal_exprt>(ldc_arg0))
579  {
581  *literal, symbol_table, string_refinement_enabled));
582  }
583  else
584  {
585  INVARIANT(
586  ldc_arg0.id() == ID_constant,
587  "ldc argument should be constant, string literal or class literal");
588  return ldc_arg0;
589  }
590 }
591 
602  java_bytecode_parse_treet &parse_tree,
603  symbol_tablet &symbol_table,
604  bool string_refinement_enabled)
605 {
606  for(auto &method : parse_tree.parsed_class.methods)
607  {
608  for(java_bytecode_parse_treet::instructiont &instruction :
609  method.instructions)
610  {
611  // ldc* instructions are Java bytecode "load constant" ops, which can
612  // retrieve a numeric constant, String literal, or Class literal.
613  const std::string statement =
614  bytecode_info[instruction.bytecode].mnemonic;
615  // clang-format off
616  if(statement == "ldc" ||
617  statement == "ldc2" ||
618  statement == "ldc_w" ||
619  statement == "ldc2_w")
620  {
621  // clang-format on
622  INVARIANT(
623  instruction.args.size() != 0,
624  "ldc instructions should have an argument");
625  instruction.args[0] =
627  instruction.args[0],
628  symbol_table,
629  string_refinement_enabled);
630  }
631  }
632  }
633 }
634 
647  symbol_table_baset &symbol_table,
648  const irep_idt &symbol_id,
649  const irep_idt &symbol_basename,
650  const typet &symbol_type,
651  const irep_idt &class_id,
652  bool force_nondet_init)
653 {
654  symbolt new_symbol;
655  new_symbol.is_static_lifetime = true;
656  new_symbol.is_lvalue = true;
657  new_symbol.is_state_var = true;
658  new_symbol.name = symbol_id;
659  new_symbol.base_name = symbol_basename;
660  new_symbol.type = symbol_type;
661  set_declaring_class(new_symbol, class_id);
662  // Public access is a guess; it encourages merging like-typed static fields,
663  // whereas a more restricted visbility would encourage separating them.
664  // Neither is correct, as without the class file we can't know the truth.
665  new_symbol.type.set(ID_C_access, ID_public);
666  // We set the field as final to avoid assuming they can be overridden.
667  new_symbol.type.set(ID_C_constant, true);
668  new_symbol.pretty_name = new_symbol.name;
669  new_symbol.mode = ID_java;
670  new_symbol.is_type = false;
671  // If pointer-typed, initialise to null and a static initialiser will be
672  // created to initialise on first reference. If primitive-typed, specify
673  // nondeterministic initialisation by setting a nil value.
674  if(symbol_type.id() == ID_pointer && !force_nondet_init)
675  new_symbol.value = null_pointer_exprt(to_pointer_type(symbol_type));
676  else
677  new_symbol.value.make_nil();
678  bool add_failed = symbol_table.add(new_symbol);
679  INVARIANT(
680  !add_failed, "caller should have checked symbol not already in table");
681 }
682 
692  const irep_idt &start_class_id,
693  const symbol_tablet &symbol_table,
694  const class_hierarchyt &class_hierarchy)
695 {
696  // Depth-first search: return the first stub ancestor, or irep_idt() if none
697  // found.
698  std::vector<irep_idt> classes_to_check;
699  classes_to_check.push_back(start_class_id);
700 
701  while(!classes_to_check.empty())
702  {
703  irep_idt to_check = classes_to_check.back();
704  classes_to_check.pop_back();
705 
706  // Exclude java.lang.Object because it can
707  if(
708  to_java_class_type(symbol_table.lookup_ref(to_check).type)
709  .get_is_stub() &&
710  to_check != "java::java.lang.Object")
711  {
712  return to_check;
713  }
714 
715  const class_hierarchyt::idst &parents =
716  class_hierarchy.class_map.at(to_check).parents;
717  classes_to_check.insert(
718  classes_to_check.end(), parents.begin(), parents.end());
719  }
720 
721  return irep_idt();
722 }
723 
734  const java_bytecode_parse_treet &parse_tree,
735  symbol_table_baset &symbol_table,
736  const class_hierarchyt &class_hierarchy,
737  messaget &log)
738 {
739  namespacet ns(symbol_table);
740  for(const auto &method : parse_tree.parsed_class.methods)
741  {
742  for(const java_bytecode_parse_treet::instructiont &instruction :
743  method.instructions)
744  {
745  const std::string statement =
746  bytecode_info[instruction.bytecode].mnemonic;
747  if(statement == "getstatic" || statement == "putstatic")
748  {
749  INVARIANT(
750  instruction.args.size() > 0,
751  "get/putstatic should have at least one argument");
752  const fieldref_exprt &field_ref =
753  expr_dynamic_cast<fieldref_exprt>(instruction.args[0]);
754  irep_idt component = field_ref.component_name();
755  irep_idt class_id = field_ref.class_name();
756 
757  // The final 'true' parameter here includes interfaces, as they can
758  // define static fields.
759  const auto referred_component =
760  get_inherited_component(class_id, component, symbol_table, true);
761  if(!referred_component)
762  {
763  // Create a new stub global on an arbitrary incomplete ancestor of the
764  // class that was referred to. This is just a guess, but we have no
765  // better information to go on.
766  irep_idt add_to_class_id =
768  class_id, symbol_table, class_hierarchy);
769 
770  // If there are no incomplete ancestors to ascribe the missing field
771  // to, we must have an incomplete model of a class or simply a
772  // version mismatch of some kind. Normally this would be an error, but
773  // our models library currently triggers this error in some cases
774  // (notably java.lang.System, which is missing System.in/out/err).
775  // Therefore for this case we ascribe the missing field to the class
776  // it was directly referenced from, and fall back to initialising the
777  // field in __CPROVER_initialize, rather than try to create or augment
778  // a clinit method for a non-stub class.
779 
780  bool no_incomplete_ancestors = add_to_class_id.empty();
781  if(no_incomplete_ancestors)
782  {
783  add_to_class_id = class_id;
784 
785  // TODO forbid this again once the models library has been checked
786  // for missing static fields.
787  log.warning() << "Stub static field " << component << " found for "
788  << "non-stub type " << class_id << ". In future this "
789  << "will be a fatal error." << messaget::eom;
790  }
791 
792  irep_idt identifier =
793  id2string(add_to_class_id) + "." + id2string(component);
794 
796  symbol_table,
797  identifier,
798  component,
799  instruction.args[0].type(),
800  add_to_class_id,
801  no_incomplete_ancestors);
802  }
803  }
804  }
805  }
806 }
807 
809  symbol_tablet &symbol_table,
810  const std::string &)
811 {
812  PRECONDITION(language_options.has_value());
813  // There are various cases in the Java front-end where pre-existing symbols
814  // from a previous load are not handled. We just rule this case out for now;
815  // a user wishing to ensure a particular class is loaded should use
816  // --java-load-class (to force class-loading) or
817  // --lazy-methods-extra-entry-point (to ensure a method body is loaded)
818  // instead of creating two instances of the front-end.
819  INVARIANT(
820  symbol_table.begin() == symbol_table.end(),
821  "the Java front-end should only be used with an empty symbol table");
822 
823  java_internal_additions(symbol_table);
824  create_java_initialize(symbol_table);
825 
826  if(language_options->string_refinement_enabled)
828 
829  // Must load java.lang.Object first to avoid stubbing
830  // This ordering could alternatively be enforced by
831  // moving the code below to the class loader.
832  java_class_loadert::parse_tree_with_overridest_mapt::const_iterator it =
833  java_class_loader.get_class_with_overlays_map().find("java.lang.Object");
835  {
837  it->second,
838  symbol_table,
840  language_options->max_user_array_length,
843  language_options->no_load_classes))
844  {
845  return true;
846  }
847  }
848 
849  // first generate a new struct symbol for each class and a new function symbol
850  // for every method
851  for(const auto &class_trees : java_class_loader.get_class_with_overlays_map())
852  {
853  if(class_trees.second.front().parsed_class.name.empty())
854  continue;
855 
857  class_trees.second,
858  symbol_table,
860  language_options->max_user_array_length,
863  language_options->no_load_classes))
864  {
865  return true;
866  }
867  }
868 
869  // Register synthetic method that replaces a real definition if one is
870  // available:
871  if(symbol_table.has_symbol(get_create_array_with_type_name()))
872  {
875  }
876 
877  // Now add synthetic classes for every invokedynamic instruction found (it
878  // makes this easier that all interface types and their methods have been
879  // created above):
880  {
881  std::vector<irep_idt> methods_to_check;
882 
883  // Careful not to add to the symtab while iterating over it:
884  for(const auto &id_and_symbol : symbol_table)
885  {
886  const auto &symbol = id_and_symbol.second;
887  const auto &id = symbol.name;
888  if(can_cast_type<code_typet>(symbol.type) && method_bytecode.get(id))
889  {
890  methods_to_check.push_back(id);
891  }
892  }
893 
894  for(const auto &id : methods_to_check)
895  {
897  id,
898  method_bytecode.get(id)->get().method.instructions,
899  symbol_table,
902  }
903  }
904 
905  // Now that all classes have been created in the symbol table we can populate
906  // the class hierarchy:
907  class_hierarchy(symbol_table);
908 
909  // find and mark all implicitly generic class types
910  // this can only be done once all the class symbols have been created
911  for(const auto &c : java_class_loader.get_class_with_overlays_map())
912  {
913  if(c.second.front().parsed_class.name.empty())
914  continue;
915  try
916  {
918  c.second.front().parsed_class.name, symbol_table);
919  }
921  {
923  << "Not marking class " << c.first
924  << " implicitly generic due to missing outer class symbols"
925  << messaget::eom;
926  }
927  }
928 
929  // Infer fields on opaque types based on the method instructions just loaded.
930  // For example, if we don't have bytecode for field x of class A, but we can
931  // see an int-typed getfield instruction referring to it, add that field now.
932  for(auto &class_to_trees : java_class_loader.get_class_with_overlays_map())
933  {
934  for(const java_bytecode_parse_treet &parse_tree : class_to_trees.second)
935  infer_opaque_type_fields(parse_tree, symbol_table);
936  }
937 
938  // Create global variables for constants (String and Class literals) up front.
939  // This means that when running with lazy loading, we will be aware of these
940  // literal globals' existence when __CPROVER_initialize is generated in
941  // `generate_support_functions`.
942  const std::size_t before_constant_globals_size = symbol_table.symbols.size();
943  for(auto &class_to_trees : java_class_loader.get_class_with_overlays_map())
944  {
945  for(java_bytecode_parse_treet &parse_tree : class_to_trees.second)
946  {
948  parse_tree, symbol_table, language_options->string_refinement_enabled);
949  }
950  }
951  status() << "Java: added "
952  << (symbol_table.symbols.size() - before_constant_globals_size)
953  << " String or Class constant symbols"
954  << messaget::eom;
955 
956  // For each reference to a stub global (that is, a global variable declared on
957  // a class we don't have bytecode for, and therefore don't know the static
958  // initialiser for), create a synthetic static initialiser (clinit method)
959  // to nondet initialise it.
960  // Note this must be done before making static initialiser wrappers below, as
961  // this makes a Classname.clinit method, then the next pass makes a wrapper
962  // that ensures it is only run once, and that static initialisation happens
963  // in class-graph topological order.
964 
965  {
966  journalling_symbol_tablet symbol_table_journal =
967  journalling_symbol_tablet::wrap(symbol_table);
968  for(auto &class_to_trees : java_class_loader.get_class_with_overlays_map())
969  {
970  for(const java_bytecode_parse_treet &parse_tree : class_to_trees.second)
971  {
973  parse_tree, symbol_table_journal, class_hierarchy, *this);
974  }
975  }
976 
978  symbol_table, symbol_table_journal.get_inserted(), synthetic_methods);
979  }
980 
982  symbol_table,
984  language_options->threading_support,
985  language_options->static_values_json.has_value());
986 
988 
989  // Now incrementally elaborate methods
990  // that are reachable from this entry point.
991  switch(language_options->lazy_methods_mode)
992  {
994  // ci = context-insensitive
995  if(do_ci_lazy_method_conversion(symbol_table))
996  return true;
997  break;
999  {
1000  symbol_table_buildert symbol_table_builder =
1001  symbol_table_buildert::wrap(symbol_table);
1002 
1003  journalling_symbol_tablet journalling_symbol_table =
1004  journalling_symbol_tablet::wrap(symbol_table_builder);
1005 
1006  // Convert all synthetic methods:
1007  for(const auto &function_id_and_type : synthetic_methods)
1008  {
1010  function_id_and_type.first,
1011  journalling_symbol_table,
1013  }
1014  // Convert all methods for which we have bytecode now
1015  for(const auto &method_sig : method_bytecode)
1016  {
1018  method_sig.first, journalling_symbol_table, class_to_declared_symbols);
1019  }
1021  INITIALIZE_FUNCTION, journalling_symbol_table, class_to_declared_symbols);
1022  // Now convert all newly added string methods
1023  for(const auto &fn_name : journalling_symbol_table.get_inserted())
1024  {
1026  convert_single_method(fn_name, symbol_table, class_to_declared_symbols);
1027  }
1028  }
1029  break;
1031  // Our caller is in charge of elaborating methods on demand.
1032  break;
1033  }
1034 
1035  // now instrument runtime exceptions
1037  symbol_table,
1038  language_options->throw_runtime_exceptions,
1040 
1041  // now typecheck all
1042  bool res = java_bytecode_typecheck(
1043  symbol_table,
1045  language_options->string_refinement_enabled);
1046 
1047  // now instrument thread-blocks and synchronized methods.
1048  if(language_options->threading_support)
1049  {
1050  convert_threadblock(symbol_table);
1052  }
1053 
1054  return res;
1055 }
1056 
1058  symbol_tablet &symbol_table)
1059 {
1060  PRECONDITION(language_options.has_value());
1061 
1062  symbol_table_buildert symbol_table_builder =
1063  symbol_table_buildert::wrap(symbol_table);
1064 
1067  if(!res.is_success())
1068  return res.is_error();
1069 
1070  // Load the main function into the symbol table to get access to its
1071  // parameter names
1072  convert_lazy_method(res.main_function.name, symbol_table_builder);
1073 
1074  const symbolt &symbol =
1075  symbol_table_builder.lookup_ref(res.main_function.name);
1076  if(symbol.value.is_nil())
1077  {
1079  "the program has no entry point",
1080  "function",
1081  "Check that the specified entry point is included by your "
1082  "--context-include or --context-exclude options");
1083  }
1084 
1085  // generate the test harness in __CPROVER__start and a call the entry point
1086  return java_entry_point(
1087  symbol_table_builder,
1088  main_class,
1090  language_options->assume_inputs_non_null,
1091  language_options->assert_uncaught_exceptions,
1094  language_options->string_refinement_enabled,
1095  [&](const symbolt &function, symbol_table_baset &symbol_table) {
1096  return java_build_arguments(
1097  function,
1098  symbol_table,
1099  language_options->assume_inputs_non_null,
1100  object_factory_parameters,
1101  get_pointer_type_selector(),
1102  get_message_handler());
1103  });
1104 }
1105 
1118  symbol_tablet &symbol_table)
1119 {
1120  symbol_table_buildert symbol_table_builder =
1121  symbol_table_buildert::wrap(symbol_table);
1122 
1124 
1125  const method_convertert method_converter =
1126  [this, &symbol_table_builder, &class_to_declared_symbols](
1127  const irep_idt &function_id,
1128  ci_lazy_methods_neededt lazy_methods_needed) {
1129  return convert_single_method(
1130  function_id,
1131  symbol_table_builder,
1132  std::move(lazy_methods_needed),
1134  };
1135 
1136  ci_lazy_methodst method_gather(
1137  symbol_table,
1138  main_class,
1140  language_options->extra_methods,
1142  language_options->java_load_classes,
1145 
1146  return method_gather(
1147  symbol_table, method_bytecode, method_converter, get_message_handler());
1148 }
1149 
1150 const select_pointer_typet &
1152 {
1153  PRECONDITION(pointer_type_selector.get()!=nullptr);
1154  return *pointer_type_selector;
1155 }
1156 
1163  std::unordered_set<irep_idt> &methods) const
1164 {
1165  const std::string cprover_class_prefix = "java::org.cprover.CProver.";
1166 
1167  // Add all string solver methods to map
1169  // Add all concrete methods to map
1170  for(const auto &kv : method_bytecode)
1171  methods.insert(kv.first);
1172  // Add all synthetic methods to map
1173  for(const auto &kv : synthetic_methods)
1174  methods.insert(kv.first);
1175  methods.insert(INITIALIZE_FUNCTION);
1176 }
1177 
1187  const irep_idt &function_id,
1188  symbol_table_baset &symtab)
1189 {
1190  const symbolt &symbol = symtab.lookup_ref(function_id);
1191  if(symbol.value.is_not_nil())
1192  return;
1193 
1194  journalling_symbol_tablet symbol_table=
1196 
1198  convert_single_method(function_id, symbol_table, class_to_declared_symbols);
1199 
1200  // Instrument runtime exceptions (unless symbol is a stub or is the
1201  // INITIALISE_FUNCTION).
1202  if(symbol.value.is_not_nil() && function_id != INITIALIZE_FUNCTION)
1203  {
1205  symbol_table,
1206  symbol_table.get_writeable_ref(function_id),
1207  language_options->throw_runtime_exceptions,
1209  }
1210 
1211  // now typecheck this function
1213  symbol_table,
1215  language_options->string_refinement_enabled);
1216 }
1217 
1229  const codet &function_body,
1230  optionalt<ci_lazy_methods_neededt> needed_lazy_methods)
1231 {
1232  if(needed_lazy_methods)
1233  {
1234  for(const_depth_iteratort it = function_body.depth_cbegin();
1235  it != function_body.depth_cend();
1236  ++it)
1237  {
1238  if(it->id() == ID_code)
1239  {
1240  const auto fn_call = expr_try_dynamic_cast<code_function_callt>(*it);
1241  if(!fn_call)
1242  continue;
1243  const symbol_exprt *fn_sym =
1244  expr_try_dynamic_cast<symbol_exprt>(fn_call->function());
1245  if(fn_sym)
1246  needed_lazy_methods->add_needed_method(fn_sym->get_identifier());
1247  }
1248  else if(
1249  it->id() == ID_side_effect &&
1250  to_side_effect_expr(*it).get_statement() == ID_function_call)
1251  {
1252  const auto &call_expr = to_side_effect_expr_function_call(*it);
1253  const symbol_exprt *fn_sym =
1254  expr_try_dynamic_cast<symbol_exprt>(call_expr.function());
1255  if(fn_sym)
1256  {
1257  INVARIANT(
1258  false,
1259  "Java synthetic methods are not "
1260  "expected to produce side_effect_expr_function_callt. If "
1261  "that has changed, remove this invariant. Also note that "
1262  "as of the time of writing remove_virtual_functions did "
1263  "not support this form of function call.");
1264  // needed_lazy_methods->add_needed_method(fn_sym->get_identifier());
1265  }
1266  }
1267  }
1268  }
1269 }
1270 
1284  const irep_idt &function_id,
1285  symbol_table_baset &symbol_table,
1286  optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
1288 {
1289  const symbolt &symbol = symbol_table.lookup_ref(function_id);
1290 
1291  // Nothing to do if body is already loaded
1292  if(symbol.value.is_not_nil())
1293  return false;
1294 
1295  if(function_id == INITIALIZE_FUNCTION)
1296  {
1298  symbol_table,
1299  symbol.location,
1300  language_options->assume_inputs_non_null,
1303  language_options->string_refinement_enabled,
1305  return false;
1306  }
1307 
1308  INVARIANT(declaring_class(symbol), "Method must have a declaring class.");
1309 
1310  bool ret = convert_single_method_code(
1311  function_id, symbol_table, needed_lazy_methods, class_to_declared_symbols);
1312 
1313  if(symbol.value.is_not_nil() && language_options->should_lift_clinit_calls)
1314  {
1315  auto &writable_symbol = symbol_table.get_writeable_ref(function_id);
1316  writable_symbol.value =
1317  lift_clinit_calls(std::move(to_code(writable_symbol.value)));
1318  }
1319 
1320  INVARIANT(declaring_class(symbol), "Method must have a declaring class.");
1321 
1322  return ret;
1323 }
1324 
1337  const irep_idt &function_id,
1338  symbol_table_baset &symbol_table,
1339  optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
1341 {
1342  const auto &symbol = symbol_table.lookup_ref(function_id);
1343  PRECONDITION(symbol.value.is_nil());
1344 
1345  // Get bytecode for specified function if we have it
1346  method_bytecodet::opt_reft cmb = method_bytecode.get(function_id);
1347 
1348  synthetic_methods_mapt::iterator synthetic_method_it;
1349 
1350  // Check if have a string solver implementation
1351  if(string_preprocess.implements_function(function_id))
1352  {
1353  symbolt &writable_symbol = symbol_table.get_writeable_ref(function_id);
1354  // Load parameter names from any extant bytecode before filling in body
1355  if(cmb)
1356  {
1358  writable_symbol, cmb->get().method.local_variable_table, symbol_table);
1359  }
1360  // Populate body of the function with code generated by string preprocess
1361  codet generated_code = string_preprocess.code_for_function(
1362  writable_symbol, symbol_table, get_message_handler());
1363  // String solver can make calls to functions that haven't yet been seen.
1364  // Add these to the needed_lazy_methods collection
1365  notify_static_method_calls(generated_code, needed_lazy_methods);
1366  writable_symbol.value = std::move(generated_code);
1367  return false;
1368  }
1369  else if(
1370  (synthetic_method_it = synthetic_methods.find(function_id)) !=
1371  synthetic_methods.end())
1372  {
1373  // Synthetic method (i.e. one generated by the Java frontend and which
1374  // doesn't occur in the source bytecode):
1375  symbolt &writable_symbol = symbol_table.get_writeable_ref(function_id);
1376  switch(synthetic_method_it->second)
1377  {
1379  if(language_options->threading_support)
1380  writable_symbol.value = get_thread_safe_clinit_wrapper_body(
1381  function_id,
1382  symbol_table,
1383  language_options->nondet_static,
1384  language_options->static_values_json.has_value(),
1388  else
1389  writable_symbol.value = get_clinit_wrapper_body(
1390  function_id,
1391  symbol_table,
1392  language_options->nondet_static,
1393  language_options->static_values_json.has_value(),
1397  break;
1399  {
1400  const auto class_name =
1401  declaring_class(symbol_table.lookup_ref(function_id));
1402  INVARIANT(
1403  class_name, "user_specified_clinit must be declared by a class.");
1404  INVARIANT(
1405  language_options->static_values_json.has_value(),
1406  "static-values JSON must be available");
1407  writable_symbol.value = get_user_specified_clinit_body(
1408  *class_name,
1409  *language_options->static_values_json,
1410  symbol_table,
1411  needed_lazy_methods,
1412  language_options->max_user_array_length,
1413  references,
1414  class_to_declared_symbols.get(symbol_table));
1415  break;
1416  }
1418  writable_symbol.value =
1420  function_id,
1421  symbol_table,
1425  break;
1427  writable_symbol.value = invokedynamic_synthetic_constructor(
1428  function_id, symbol_table, get_message_handler());
1429  break;
1431  writable_symbol.value = invokedynamic_synthetic_method(
1432  function_id, symbol_table, get_message_handler());
1433  break;
1435  {
1436  INVARIANT(
1437  cmb,
1438  "CProver.createArrayWithType should only be registered if "
1439  "we have a real implementation available");
1441  writable_symbol, cmb->get().method.local_variable_table, symbol_table);
1442  writable_symbol.value = create_array_with_type_body(
1443  function_id, symbol_table, get_message_handler());
1444  break;
1445  }
1446  }
1447  // Notify lazy methods of static calls made from the newly generated
1448  // function:
1450  to_code(writable_symbol.value), needed_lazy_methods);
1451  return false;
1452  }
1453 
1454  // No string solver or static init wrapper implementation;
1455  // check if have bytecode for it
1456  if(cmb)
1457  {
1459  symbol_table.lookup_ref(cmb->get().class_id),
1460  cmb->get().method,
1461  symbol_table,
1463  language_options->max_user_array_length,
1464  language_options->throw_assertion_error,
1465  std::move(needed_lazy_methods),
1468  language_options->threading_support,
1469  language_options->method_context,
1470  language_options->assert_no_exceptions_thrown);
1471  return false;
1472  }
1473 
1474  if(needed_lazy_methods)
1475  {
1476  // The return of an opaque function is a source of an otherwise invisible
1477  // instantiation, so here we ensure we've loaded the appropriate classes.
1478  const java_method_typet function_type = to_java_method_type(symbol.type);
1479  if(
1480  const pointer_typet *pointer_return_type =
1481  type_try_dynamic_cast<pointer_typet>(function_type.return_type()))
1482  {
1483  // If the return type is abstract, we won't forcibly instantiate it here
1484  // otherwise this can cause abstract methods to be explictly called
1485  // TODO(tkiley): Arguably no abstract class should ever be added to
1486  // TODO(tkiley): ci_lazy_methods_neededt, but this needs further
1487  // TODO(tkiley): investigation
1488  namespacet ns{symbol_table};
1489  const java_class_typet &underlying_type =
1490  to_java_class_type(ns.follow(pointer_return_type->subtype()));
1491 
1492  if(!underlying_type.is_abstract())
1493  needed_lazy_methods->add_all_needed_classes(*pointer_return_type);
1494  }
1495  }
1496 
1497  return true;
1498 }
1499 
1501 {
1502  PRECONDITION(language_options.has_value());
1503  return false;
1504 }
1505 
1507 {
1510  parse_trees.front().output(out);
1511  if(parse_trees.size() > 1)
1512  {
1513  out << "\n\nClass has the following overlays:\n\n";
1514  for(auto parse_tree_it = std::next(parse_trees.begin());
1515  parse_tree_it != parse_trees.end();
1516  ++parse_tree_it)
1517  {
1518  parse_tree_it->output(out);
1519  }
1520  out << "End of class overlays.\n";
1521  }
1522 }
1523 
1524 std::unique_ptr<languaget> new_java_bytecode_language()
1525 {
1526  return util_make_unique<java_bytecode_languaget>();
1527 }
1528 
1530  const exprt &expr,
1531  std::string &code,
1532  const namespacet &ns)
1533 {
1534  code=expr2java(expr, ns);
1535  return false;
1536 }
1537 
1539  const typet &type,
1540  std::string &code,
1541  const namespacet &ns)
1542 {
1543  code=type2java(type, ns);
1544  return false;
1545 }
1546 
1548  const std::string &code,
1549  const std::string &module,
1550  exprt &expr,
1551  const namespacet &ns)
1552 {
1553 #if 0
1554  expr.make_nil();
1555 
1556  // no preprocessing yet...
1557 
1558  std::istringstream i_preprocessed(code);
1559 
1560  // parsing
1561 
1562  java_bytecode_parser.clear();
1563  java_bytecode_parser.filename="";
1564  java_bytecode_parser.in=&i_preprocessed;
1565  java_bytecode_parser.set_message_handler(message_handler);
1566  java_bytecode_parser.grammar=java_bytecode_parsert::EXPRESSION;
1567  java_bytecode_parser.mode=java_bytecode_parsert::GCC;
1568  java_bytecode_scanner_init();
1569 
1570  bool result=java_bytecode_parser.parse();
1571 
1572  if(java_bytecode_parser.parse_tree.items.empty())
1573  result=true;
1574  else
1575  {
1576  expr=java_bytecode_parser.parse_tree.items.front().value();
1577 
1578  result=java_bytecode_convert(expr, "", message_handler);
1579 
1580  // typecheck it
1581  if(!result)
1583  }
1584 
1585  // save some memory
1586  java_bytecode_parser.clear();
1587 
1588  return result;
1589 #else
1590  // unused parameters
1591  (void)code;
1592  (void)module;
1593  (void)expr;
1594  (void)ns;
1595 #endif
1596 
1597  return true; // fail for now
1598 }
1599 
1601 {
1602 }
1603 
1607 std::vector<load_extra_methodst>
1609 {
1610  (void)options; // unused parameter
1611  return {};
1612 }
struct bytecode_infot const bytecode_info[]
Collect methods needed to be loaded using the lazy method.
std::function< bool(const irep_idt &function_id, ci_lazy_methods_neededt)> method_convertert
Class Hierarchy.
Operator to return the address of an object.
Definition: pointer_expr.h:200
Non-graph-based representation of the class hierarchy.
class_mapt class_map
std::vector< irep_idt > idst
bool is_abstract() const
Definition: std_types.h:353
std::string get_value(char option) const
Definition: cmdline.cpp:47
virtual bool isset(char option) const
Definition: cmdline.cpp:29
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:108
const typet & return_type() const
Definition: std_types.h:850
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35
optionalt< std::string > main
Definition: config.h:261
struct configt::javat java
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
Base class for all expressions.
Definition: expr.h:54
const_depth_iteratort depth_cend() const
Definition: expr.cpp:289
typet & type()
Return the type of the expression.
Definition: expr.h:82
const_depth_iteratort depth_cbegin() const
Definition: expr.cpp:287
Represents the argument of an instruction that uses a CONSTANT_Fieldref This is used for example as a...
irep_idt class_name() const
irep_idt component_name() const
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
Thrown when we can't handle something in an input source file.
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
bool is_not_nil() const
Definition: irep.h:391
const irep_idt & id() const
Definition: irep.h:407
void make_nil()
Definition: irep.h:464
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
bool is_nil() const
Definition: irep.h:387
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...
void show_parse(std::ostream &out) override
synthetic_methods_mapt synthetic_methods
Maps synthetic method names on to the particular type of synthetic method (static initializer,...
std::vector< irep_idt > main_jar_classes
virtual bool final(symbol_table_baset &context) override
Final adjustments, e.g.
virtual bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream) override
ANSI-C preprocessing.
std::string id() const override
stub_global_initializer_factoryt stub_global_initializer_factory
std::set< std::string > extensions() const override
void set_message_handler(message_handlert &message_handler) override
void set_language_options(const optionst &) override
Consume options that are java bytecode specific.
bool from_type(const typet &type, std::string &code, const namespacet &ns) override
Formats the given type in a language-specific way.
bool to_expr(const std::string &code, const std::string &module, exprt &expr, const namespacet &ns) override
Parses the given string into an expression.
const std::unique_ptr< const select_pointer_typet > pointer_type_selector
bool do_ci_lazy_method_conversion(symbol_tablet &)
Uses a simple context-insensitive ('ci') analysis to determine which methods may be reachable from th...
bool generate_support_functions(symbol_tablet &symbol_table) override
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
java_object_factory_parameterst object_factory_parameters
optionalt< java_bytecode_language_optionst > language_options
java_string_library_preprocesst string_preprocess
void modules_provided(std::set< std::string > &modules) override
java_class_loadert java_class_loader
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...
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.
virtual bool parse()
We set the main class (i.e. class to start the class loading analysis, see java_class_loadert) when w...
const select_pointer_typet & get_pointer_type_selector() const
bool typecheck(symbol_tablet &context, const std::string &module) override
bool from_expr(const exprt &expr, std::string &code, const namespacet &ns) override
Formats the given expression in a language-specific way.
std::unordered_map< std::string, object_creation_referencet > references
Map used in all calls to functions that deterministically create objects (currently only assign_from_...
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...
void convert_single_method(const irep_idt &function_id, symbol_table_baset &symbol_table, lazy_class_to_declared_symbols_mapt &class_to_declared_symbols)
void add_classpath_entry(const std::string &, message_handlert &)
Appends an entry to the class path, used for loading classes.
void clear_classpath()
Clear all classpath entries.
jar_poolt jar_pool
a cache for jar_filet, by path name
Class representing a filter for class file loading.
std::vector< irep_idt > load_entire_jar(const std::string &jar_path, message_handlert &)
Load all class files from a .jar file.
bool can_load_class(const irep_idt &class_name, message_handlert &)
Checks whether class_name is parseable from the classpath, ignoring class loading limits.
void set_extra_class_refs_function(get_extra_class_refs_functiont func)
Sets a function that provides extra dependencies for a particular class.
void set_java_cp_include_files(const std::string &cp_include_files)
Set the argument of the class loader limit java_class_loader_limitt.
fixed_keys_map_wrappert< parse_tree_with_overridest_mapt > get_class_with_overlays_map()
Map from class names to the bytecode parse trees.
std::list< java_bytecode_parse_treet > parse_tree_with_overlayst
A list of parse trees supporting overlay 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...
bool get_is_stub() const
Definition: java_types.h:400
const componentst & components() const
Definition: java_types.h:226
void get_all_function_names(std::unordered_set< irep_idt > &methods) const
bool implements_function(const irep_idt &function_id) const
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...
void initialize_conversion_table()
fill maps with correspondence from java method names to conversion functions
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...
A symbol table wrapper that records which entries have been updated/removedA caller can pass a journa...
static journalling_symbol_tablet wrap(symbol_table_baset &base_symbol_table)
const changesett & get_inserted() const
Definition: json.h:27
bool is_array() const
Definition: json.h:61
bool is_object() const
Definition: json.h:56
Map classes to the symbols they declare but is only computed once it is needed and the map is then ke...
std::unordered_multimap< irep_idt, symbolt > & get(const symbol_tablet &symbol_table)
std::unordered_multimap< irep_idt, symbolt > map
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
message_handlert * message_handler
Definition: message.h:439
mstreamt & warning() const
Definition: message.h:404
mstreamt & status() const
Definition: message.h:414
mstreamt & result() const
Definition: message.h:409
message_handlert & get_message_handler()
Definition: message.h:184
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:179
static eomt eom
Definition: message.h:297
opt_reft get(const irep_idt &method_id)
optionalt< std::reference_wrapper< const class_method_and_bytecodet > > opt_reft
An exception that is raised checking whether a class is implicitly generic if a symbol for an outer c...
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
The null pointer constant.
Definition: std_expr.h:2751
unsigned int get_unsigned_int_option(const std::string &option) const
Definition: options.cpp:56
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
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
void set_option(const std::string &option, const bool value)
Definition: options.cpp:28
const std::string get_option(const std::string &option) const
Definition: options.cpp:67
const value_listt & get_list_option(const std::string &option) const
Definition: options.cpp:80
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1495
Provides filtering of strings vai inclusion/exclusion lists of prefixes.
Definition: prefix_filter.h:20
const irep_idt & get_statement() const
Definition: std_code.h:1920
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:498
const basest & bases() const
Get the collection of base classes/structs.
Definition: std_types.h:257
bool has_component(const irep_idt &component_name) const
Definition: std_types.h:152
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...
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.
Expression to hold a symbol (variable)
Definition: std_expr.h:81
const irep_idt & get_identifier() const
Definition: std_expr.h:110
The symbol table base class interface.
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Author: Diffblue Ltd.
static symbol_table_buildert wrap(symbol_table_baset &base_symbol_table)
The symbol table.
Definition: symbol_table.h:20
virtual iteratort begin() override
Definition: symbol_table.h:114
virtual iteratort end() override
Definition: symbol_table.h:118
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
bool is_static_lifetime
Definition: symbol.h:65
bool is_type
Definition: symbol.h:61
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
bool is_state_var
Definition: symbol.h:62
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt name
The unique identifier.
Definition: symbol.h:40
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
bool is_lvalue
Definition: symbol.h:66
exprt value
Initial value of symbol.
Definition: symbol.h:34
irep_idt mode
Language mode.
Definition: symbol.h:49
The type of an expression, extends irept.
Definition: type.h:28
configt config
Definition: config.cpp:24
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
irep_idt get_create_array_with_type_name()
Returns the symbol name for org.cprover.CProver.createArrayWithType
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.
Implementation of CProver.createArrayWithType intrinsic.
std::string type2java(const typet &type, const namespacet &ns)
Definition: expr2java.cpp:461
std::string expr2java(const exprt &expr, const namespacet &ns)
Definition: expr2java.cpp:454
Forward depth-first search iterators These iterators' copy operations are expensive,...
dstringt irep_idt
Definition: irep.h:37
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
void convert_synchronized_methods(symbol_tablet &symbol_table, message_handlert &message_handler)
Iterate through the symbol table to find and instrument synchronized methods.
void convert_threadblock(symbol_tablet &symbol_table)
Iterate through the symbol table to find and appropriately instrument thread-blocks.
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.
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.
JAVA Bytecode Language Conversion.
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...
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)
JAVA Bytecode Language Conversion.
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.
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.
const std::vector< std::string > exception_needed_classes
void java_internal_additions(symbol_table_baset &dest)
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.
void parse_java_language_options(const cmdlinet &cmd, optionst &options)
Parse options that are java bytecode specific.
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.
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.
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...
static void throwMainClassLoadingError(const std::string &main_class)
prefix_filtert get_context(const optionst &options)
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.
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 ...
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.
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.
std::unique_ptr< languaget > new_java_bytecode_language()
@ LAZY_METHODS_MODE_EAGER
@ LAZY_METHODS_MODE_EXTERNAL_DRIVER
@ LAZY_METHODS_MODE_CONTEXT_INSENSITIVE
#define JAVA_CLASS_MODEL_SUFFIX
bool java_bytecode_typecheck(symbol_table_baset &symbol_table, message_handlert &message_handler, bool string_refinement_enabled)
void java_bytecode_typecheck_updated_symbols(journalling_symbol_tablet &symbol_table, message_handlert &message_handler, bool string_refinement_enabled)
JAVA Bytecode Language Type Checking.
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__...
void create_java_initialize(symbol_table_baset &symbol_table)
Adds __cprover_initialize to the symbol_table but does not generate code for it yet.
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.
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.
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...
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.
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...
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.
std::unordered_multimap< irep_idt, symbolt > class_to_declared_symbols(const symbol_tablet &symbol_table)
Representation of a constant Java string.
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.
const java_class_typet & to_java_class_type(const typet &type)
Definition: java_types.h:584
const java_method_typet & to_java_method_type(const typet &type)
Definition: java_types.h:186
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
optionalt< irep_idt > declaring_class(const symbolt &symbol)
Gets the identifier of the class which declared a given symbol.
Definition: java_utils.cpp:571
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
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
Author: Diffblue Ltd.
json_arrayt & to_json_array(jsont &json)
Definition: json.h:426
json_objectt & to_json_object(jsont &json)
Definition: json.h:444
bool parse_json(std::istream &in, const std::string &filename, message_handlert &message_handler, jsont &dest)
Definition: json_parser.cpp:16
codet invokedynamic_synthetic_constructor(const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler)
Create invokedynamic synthetic constructor.
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.
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)
Java lambda code synthesis.
codet lift_clinit_calls(codet input)
file Static initializer call lifting
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...
Process a pattern to use as a regex for selecting extra entry points for ci_lazy_methodst.
nonstd::optional< T > optionalt
Definition: optional.h:35
Options.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
#define INITIALIZE_FUNCTION
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1954
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Definition: std_code.h:2187
const codet & to_code(const exprt &expr)
Definition: std_code.h:155
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:55
bool can_cast_type< code_typet >(const typet &type)
Check whether a reference to a typet is a code_typet.
Definition: std_types.h:936
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1533
const char * mnemonic
Definition: bytecode_info.h:46
classpatht classpath
Definition: config.h:247
irep_idt main_class
Definition: config.h:248
bool assert_no_exceptions_thrown
Transform athrow bytecode instructions into assert FALSE followed by assume FALSE.
bool should_lift_clinit_calls
Should we lift clinit calls in function bodies to the top? For example, turning if(x) A....
optionalt< prefix_filtert > method_context
If set, method bodies are only elaborated if they pass the filter.
optionalt< json_objectt > static_values_json
JSON which contains initial values of static fields (right after the static initializer of the class ...
bool assume_inputs_non_null
assume inputs variables to be non-null
size_t max_user_array_length
max size for user code created arrays
std::vector< irep_idt > java_load_classes
list of classes to force load even without reference from the entry point
std::unordered_set< std::string > no_load_classes
List of classes to never load.
std::vector< load_extra_methodst > extra_methods
void set(const optionst &)
Assigns the parameters from given options.
bool has_suffix(const std::string &s, const std::string &suffix)
Definition: suffix.h:17
Author: Diffblue Ltd.
@ INVOKEDYNAMIC_METHOD
A generated method for a class capturing the parameters of an invokedynamic instruction.
@ USER_SPECIFIED_STATIC_INITIALIZER
Only exists if the --static-values option was used.
@ STATIC_INITIALIZER_WRAPPER
A static initializer wrapper (code of the form if(!already_run) clinit(); already_run = true;) These ...
@ STUB_CLASS_STATIC_INITIALIZER
A generated (synthetic) static initializer function for a stub type.
@ CREATE_ARRAY_WITH_TYPE
Our internal implementation of CProver.createArrayWithType, which needs to access internal type-id fi...
@ INVOKEDYNAMIC_CAPTURE_CONSTRUCTOR
A generated constructor for a class capturing the parameters of an invokedynamic instruction.