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