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 <string>
12 
13 #include <util/cmdline.h>
14 #include <util/config.h>
15 #include <util/expr_iterator.h>
16 #include <util/invariant.h>
18 #include <util/options.h>
19 #include <util/string2int.h>
20 #include <util/suffix.h>
21 #include <util/symbol_table.h>
23 
24 #include <json/json_parser.h>
25 
27 
34 #include "java_entry_point.h"
35 #include "java_bytecode_parser.h"
36 #include "java_class_loader.h"
37 #include "java_string_literals.h"
39 #include "java_utils.h"
40 #include "ci_lazy_methods.h"
41 
42 #include "expr2java.h"
43 #include "load_method_by_regex.h"
44 
48 void parse_java_language_options(const cmdlinet &cmd, optionst &options)
49 {
50  options.set_option(
51  "java-assume-inputs-non-null", cmd.isset("java-assume-inputs-non-null"));
52  options.set_option(
53  "throw-runtime-exceptions", cmd.isset("throw-runtime-exceptions"));
54  options.set_option(
55  "uncaught-exception-check", !cmd.isset("disable-uncaught-exception-check"));
56  options.set_option(
57  "throw-assertion-error", cmd.isset("throw-assertion-error"));
58  options.set_option("java-threading", cmd.isset("java-threading"));
59 
60  if(cmd.isset("java-max-vla-length"))
61  {
62  options.set_option(
63  "java-max-vla-length", cmd.get_value("java-max-vla-length"));
64  }
65 
66  options.set_option(
67  "symex-driven-lazy-loading", cmd.isset("symex-driven-lazy-loading"));
68 
69  if(cmd.isset("java-load-class"))
70  options.set_option("java-load-class", cmd.get_values("java-load-class"));
71 
72  if(cmd.isset("java-no-load-class"))
73  {
74  options.set_option(
75  "java-no-load-class", cmd.get_values("java-no-load-class"));
76  }
77  if(cmd.isset("lazy-methods-extra-entry-point"))
78  {
79  options.set_option(
80  "lazy-methods-extra-entry-point",
81  cmd.get_values("lazy-methods-extra-entry-point"));
82  }
83  if(cmd.isset("java-cp-include-files"))
84  {
85  options.set_option(
86  "java-cp-include-files", cmd.get_value("java-cp-include-files"));
87  }
88 }
89 
92 {
94 
96  options.get_bool_option("java-assume-inputs-non-null");
97  string_refinement_enabled = options.get_bool_option("refine-strings");
99  options.get_bool_option("throw-runtime-exceptions");
101  options.get_bool_option("uncaught-exception-check");
102  throw_assertion_error = options.get_bool_option("throw-assertion-error");
103  threading_support = options.get_bool_option("java-threading");
105  options.get_unsigned_int_option("java-max-vla-length");
106 
107  if(options.get_bool_option("symex-driven-lazy-loading"))
109  else if(options.get_bool_option("lazy-methods"))
111  else
113 
115  {
116  java_load_classes.insert(
117  java_load_classes.end(),
118  exception_needed_classes.begin(),
120  }
121 
122  if(options.is_set("java-load-class"))
123  {
124  const auto &load_values = options.get_list_option("java-load-class");
125  java_load_classes.insert(
126  java_load_classes.end(), load_values.begin(), load_values.end());
127  }
128  if(options.is_set("java-no-load-class"))
129  {
130  const auto &no_load_values = options.get_list_option("java-no-load-class");
131  no_load_classes = {no_load_values.begin(), no_load_values.end()};
132  }
133  const std::list<std::string> &extra_entry_points =
134  options.get_list_option("lazy-methods-extra-entry-point");
135  std::transform(
136  extra_entry_points.begin(),
137  extra_entry_points.end(),
138  std::back_inserter(extra_methods),
140  const auto &new_points = build_extra_entry_points(options);
141  extra_methods.insert(
142  extra_methods.end(), new_points.begin(), new_points.end());
143 
144  java_cp_include_files = options.get_option("java-cp-include-files");
145  if(!java_cp_include_files.empty())
146  {
147  // load file list from JSON file
148  if(java_cp_include_files[0]=='@')
149  {
150  jsont json_cp_config;
151  if(parse_json(
152  java_cp_include_files.substr(1),
154  json_cp_config))
155  throw "cannot read JSON input configuration for JAR loading";
156 
157  if(!json_cp_config.is_object())
158  throw "the JSON file has a wrong format";
159  jsont include_files=json_cp_config["jar"];
160  if(!include_files.is_array())
161  throw "the JSON file has a wrong format";
162 
163  // add jars from JSON config file to classpath
164  for(const jsont &file_entry : include_files.array)
165  {
167  file_entry.is_string() && has_suffix(file_entry.value, ".jar"),
168  "classpath entry must be jar filename, but '" + file_entry.value +
169  "' found");
170  config.java.classpath.push_back(file_entry.value);
171  }
172  }
173  }
174  else
176 
177  nondet_static = options.get_bool_option("nondet-static");
178 
180 }
181 
182 std::set<std::string> java_bytecode_languaget::extensions() const
183 {
184  return { "class", "jar" };
185 }
186 
187 void java_bytecode_languaget::modules_provided(std::set<std::string> &)
188 {
189  // modules.insert(translation_unit(parse_path));
190 }
191 
194  std::istream &,
195  const std::string &,
196  std::ostream &)
197 {
198  // there is no preprocessing!
199  return true;
200 }
201 
212  std::istream &,
213  const std::string &path)
214 {
216 
218 
219  for(const auto &p : config.java.classpath)
221 
226  {
228 
229  auto get_string_base_classes = [this](const irep_idt &id) {
231  };
232 
233  java_class_loader.set_extra_class_refs_function(get_string_base_classes);
234  }
235 
236  // look at extension
237  if(has_suffix(path, ".class"))
238  {
239  // override main_class
241  }
242  else if(has_suffix(path, ".jar"))
243  {
244  // build an object to potentially limit which classes are loaded
245  java_class_loader_limitt class_loader_limit(
249  {
250  const std::string &entry_method = config.main;
251  // If we have an entry method, we can derive a main class.
252  if(!entry_method.empty())
253  {
254  const auto last_dot_position = entry_method.find_last_of('.');
255  main_class = entry_method.substr(0, last_dot_position);
256  }
257  else
258  {
259  auto manifest = java_class_loader.jar_pool(path).get_manifest();
260  std::string manifest_main_class = manifest["Main-Class"];
261 
262  // if the manifest declares a Main-Class line, we got a main class
263  if(!manifest_main_class.empty())
264  main_class = manifest_main_class;
265  }
266  }
267  else
269 
270  // do we have one now?
271  if(main_class.empty())
272  {
273  status() << "JAR file without entry point: loading class files" << eom;
274  const auto classes = java_class_loader.load_entire_jar(path);
275  for(const auto &c : classes)
276  main_jar_classes.push_back(c);
277  }
278  else
280  }
281  else
282  UNREACHABLE;
283 
284  if(!main_class.empty())
285  {
286  status() << "Java main class: " << main_class << eom;
288  }
289 
290  return false;
291 }
292 
302  const java_bytecode_parse_treet &parse_tree,
303  symbol_tablet &symbol_table)
304 {
305  namespacet ns(symbol_table);
306  for(const auto &method : parse_tree.parsed_class.methods)
307  {
308  for(const java_bytecode_parse_treet::instructiont &instruction :
309  method.instructions)
310  {
311  if(instruction.statement == "getfield" ||
312  instruction.statement == "putfield")
313  {
314  const exprt &fieldref = instruction.args[0];
315  irep_idt class_symbol_id = fieldref.get(ID_class);
316  const symbolt *class_symbol = symbol_table.lookup(class_symbol_id);
317  INVARIANT(
318  class_symbol != nullptr,
319  "all types containing fields should have been loaded");
320 
321  const java_class_typet *class_type =
322  &to_java_class_type(class_symbol->type);
323  const irep_idt &component_name = fieldref.get(ID_component_name);
324  while(!class_type->has_component(component_name))
325  {
326  if(class_type->get_is_stub())
327  {
328  // Accessing a field of an incomplete (opaque) type.
329  symbolt &writable_class_symbol =
330  symbol_table.get_writeable_ref(class_symbol_id);
331  auto &components =
332  to_struct_type(writable_class_symbol.type).components();
333  components.emplace_back(component_name, fieldref.type());
334  components.back().set_base_name(component_name);
335  components.back().set_pretty_name(component_name);
336  break;
337  }
338  else
339  {
340  // Not present here: check the superclass.
341  INVARIANT(
342  !class_type->bases().empty(),
343  "class '" + id2string(class_symbol->name)
344  + "' (which was missing a field '" + id2string(component_name)
345  + "' referenced from method '" + id2string(method.name)
346  + "') should have an opaque superclass");
347  const auto &superclass_type = class_type->bases().front().type();
348  class_symbol_id = superclass_type.get_identifier();
349  class_type = &to_java_class_type(ns.follow(superclass_type));
350  }
351  }
352  }
353  }
354  }
355 }
356 
363  const irep_idt &class_id, symbol_tablet &symbol_table)
364 {
365  struct_tag_typet java_lang_Class("java::java.lang.Class");
366  symbol_exprt symbol_expr(
368  java_lang_Class);
369  if(!symbol_table.has_symbol(symbol_expr.get_identifier()))
370  {
371  symbolt new_class_symbol;
372  new_class_symbol.name = symbol_expr.get_identifier();
373  new_class_symbol.type = symbol_expr.type();
374  INVARIANT(
375  has_prefix(id2string(new_class_symbol.name), "java::"),
376  "class identifier should have 'java::' prefix");
377  new_class_symbol.base_name =
378  id2string(new_class_symbol.name).substr(6);
379  new_class_symbol.mode = ID_java;
380  new_class_symbol.is_lvalue = true;
381  new_class_symbol.is_state_var = true;
382  new_class_symbol.is_static_lifetime = true;
383  new_class_symbol.type.set(ID_C_no_nondet_initialization, true);
384  symbol_table.add(new_class_symbol);
385  }
386 
387  return symbol_expr;
388 }
389 
405  const exprt &ldc_arg0,
406  symbol_tablet &symbol_table,
407  bool string_refinement_enabled)
408 {
409  if(ldc_arg0.id() == ID_type)
410  {
411  const irep_idt &class_id = ldc_arg0.type().get(ID_identifier);
412  return
414  get_or_create_class_literal_symbol(class_id, symbol_table));
415  }
416  else if(ldc_arg0.id() == ID_java_string_literal)
417  {
418  return
421  ldc_arg0, symbol_table, string_refinement_enabled));
422  }
423  else
424  {
425  INVARIANT(
426  ldc_arg0.id() == ID_constant,
427  "ldc argument should be constant, string literal or class literal");
428  return ldc_arg0;
429  }
430 }
431 
442  java_bytecode_parse_treet &parse_tree,
443  symbol_tablet &symbol_table,
444  bool string_refinement_enabled)
445 {
446  for(auto &method : parse_tree.parsed_class.methods)
447  {
448  for(java_bytecode_parse_treet::instructiont &instruction :
449  method.instructions)
450  {
451  // ldc* instructions are Java bytecode "load constant" ops, which can
452  // retrieve a numeric constant, String literal, or Class literal.
453  if(instruction.statement == "ldc" ||
454  instruction.statement == "ldc2" ||
455  instruction.statement == "ldc_w" ||
456  instruction.statement == "ldc2_w")
457  {
458  INVARIANT(
459  instruction.args.size() != 0,
460  "ldc instructions should have an argument");
461  instruction.args[0] =
463  instruction.args[0],
464  symbol_table,
465  string_refinement_enabled);
466  }
467  }
468  }
469 }
470 
483  symbol_table_baset &symbol_table,
484  const irep_idt &symbol_id,
485  const irep_idt &symbol_basename,
486  const typet &symbol_type,
487  const irep_idt &class_id,
488  bool force_nondet_init)
489 {
490  symbolt new_symbol;
491  new_symbol.is_static_lifetime = true;
492  new_symbol.is_lvalue = true;
493  new_symbol.is_state_var = true;
494  new_symbol.name = symbol_id;
495  new_symbol.base_name = symbol_basename;
496  new_symbol.type = symbol_type;
497  new_symbol.type.set(ID_C_class, class_id);
498  // Public access is a guess; it encourages merging like-typed static fields,
499  // whereas a more restricted visbility would encourage separating them.
500  // Neither is correct, as without the class file we can't know the truth.
501  new_symbol.type.set(ID_C_access, ID_public);
502  new_symbol.pretty_name = new_symbol.name;
503  new_symbol.mode = ID_java;
504  new_symbol.is_type = false;
505  // If pointer-typed, initialise to null and a static initialiser will be
506  // created to initialise on first reference. If primitive-typed, specify
507  // nondeterministic initialisation by setting a nil value.
508  if(symbol_type.id() == ID_pointer && !force_nondet_init)
509  new_symbol.value = null_pointer_exprt(to_pointer_type(symbol_type));
510  else
511  new_symbol.value.make_nil();
512  bool add_failed = symbol_table.add(new_symbol);
513  INVARIANT(
514  !add_failed, "caller should have checked symbol not already in table");
515 }
516 
526  const irep_idt &start_class_id,
527  const symbol_tablet &symbol_table,
528  const class_hierarchyt &class_hierarchy)
529 {
530  // Depth-first search: return the first stub ancestor, or irep_idt() if none
531  // found.
532  std::vector<irep_idt> classes_to_check;
533  classes_to_check.push_back(start_class_id);
534 
535  while(!classes_to_check.empty())
536  {
537  irep_idt to_check = classes_to_check.back();
538  classes_to_check.pop_back();
539 
540  // Exclude java.lang.Object because it can
541  if(
542  to_java_class_type(symbol_table.lookup_ref(to_check).type)
543  .get_is_stub() &&
544  to_check != "java::java.lang.Object")
545  {
546  return to_check;
547  }
548 
549  const class_hierarchyt::idst &parents =
550  class_hierarchy.class_map.at(to_check).parents;
551  classes_to_check.insert(
552  classes_to_check.end(), parents.begin(), parents.end());
553  }
554 
555  return irep_idt();
556 }
557 
568  const java_bytecode_parse_treet &parse_tree,
569  symbol_table_baset &symbol_table,
570  const class_hierarchyt &class_hierarchy,
571  messaget &log)
572 {
573  namespacet ns(symbol_table);
574  for(const auto &method : parse_tree.parsed_class.methods)
575  {
576  for(const java_bytecode_parse_treet::instructiont &instruction :
577  method.instructions)
578  {
579  if(instruction.statement == "getstatic" ||
580  instruction.statement == "putstatic")
581  {
582  INVARIANT(
583  instruction.args.size() > 0,
584  "get/putstatic should have at least one argument");
585  irep_idt component = instruction.args[0].get_string(ID_component_name);
586  INVARIANT(
587  !component.empty(), "get/putstatic should specify a component");
588  irep_idt class_id = instruction.args[0].get_string(ID_class);
589  INVARIANT(
590  !class_id.empty(), "get/putstatic should specify a class");
591 
592  // The final 'true' parameter here includes interfaces, as they can
593  // define static fields.
596  class_id,
597  component,
598  symbol_table,
599  class_hierarchy,
600  true);
601  if(!referred_component.is_valid())
602  {
603  // Create a new stub global on an arbitrary incomplete ancestor of the
604  // class that was referred to. This is just a guess, but we have no
605  // better information to go on.
606  irep_idt add_to_class_id =
608  class_id, symbol_table, class_hierarchy);
609 
610  // If there are no incomplete ancestors to ascribe the missing field
611  // to, we must have an incomplete model of a class or simply a
612  // version mismatch of some kind. Normally this would be an error, but
613  // our models library currently triggers this error in some cases
614  // (notably java.lang.System, which is missing System.in/out/err).
615  // Therefore for this case we ascribe the missing field to the class
616  // it was directly referenced from, and fall back to initialising the
617  // field in __CPROVER_initialize, rather than try to create or augment
618  // a clinit method for a non-stub class.
619 
620  bool no_incomplete_ancestors = add_to_class_id.empty();
621  if(no_incomplete_ancestors)
622  {
623  add_to_class_id = class_id;
624 
625  // TODO forbid this again once the models library has been checked
626  // for missing static fields.
627  log.warning() << "Stub static field " << component << " found for "
628  << "non-stub type " << class_id << ". In future this "
629  << "will be a fatal error." << messaget::eom;
630  }
631 
632  irep_idt identifier =
633  id2string(add_to_class_id) + "." + id2string(component);
634 
636  symbol_table,
637  identifier,
638  component,
639  instruction.args[0].type(),
640  add_to_class_id,
641  no_incomplete_ancestors);
642  }
643  }
644  }
645  }
646 }
647 
649  symbol_tablet &symbol_table,
650  const std::string &)
651 {
653 
654  java_internal_additions(symbol_table);
655 
658 
659  // Must load java.lang.Object first to avoid stubbing
660  // This ordering could alternatively be enforced by
661  // moving the code below to the class loader.
662  java_class_loadert::parse_tree_with_overridest_mapt::const_iterator it =
663  java_class_loader.get_class_with_overlays_map().find("java.lang.Object");
665  {
666  if(
668  it->second,
669  symbol_table,
675  {
676  return true;
677  }
678  }
679 
680  // first generate a new struct symbol for each class and a new function symbol
681  // for every method
682  for(const auto &class_trees : java_class_loader.get_class_with_overlays_map())
683  {
684  if(class_trees.second.front().parsed_class.name.empty())
685  continue;
686 
687  if(
689  class_trees.second,
690  symbol_table,
696  {
697  return true;
698  }
699  }
700 
701  // Now that all classes have been created in the symbol table we can populate
702  // the class hierarchy:
703  class_hierarchy(symbol_table);
704 
705  // find and mark all implicitly generic class types
706  // this can only be done once all the class symbols have been created
707  for(const auto &c : java_class_loader.get_class_with_overlays_map())
708  {
709  if(c.second.front().parsed_class.name.empty())
710  continue;
711  try
712  {
714  c.second.front().parsed_class.name, symbol_table);
715  }
717  {
719  << "Not marking class " << c.first
720  << " implicitly generic due to missing outer class symbols"
721  << messaget::eom;
722  }
723  }
724 
725  // Infer fields on opaque types based on the method instructions just loaded.
726  // For example, if we don't have bytecode for field x of class A, but we can
727  // see an int-typed getfield instruction referring to it, add that field now.
728  for(auto &class_to_trees : java_class_loader.get_class_with_overlays_map())
729  {
730  for(const java_bytecode_parse_treet &parse_tree : class_to_trees.second)
731  infer_opaque_type_fields(parse_tree, symbol_table);
732  }
733 
734  // Create global variables for constants (String and Class literals) up front.
735  // This means that when running with lazy loading, we will be aware of these
736  // literal globals' existence when __CPROVER_initialize is generated in
737  // `generate_support_functions`.
738  const std::size_t before_constant_globals_size = symbol_table.symbols.size();
739  for(auto &class_to_trees : java_class_loader.get_class_with_overlays_map())
740  {
741  for(java_bytecode_parse_treet &parse_tree : class_to_trees.second)
742  {
744  parse_tree, symbol_table, string_refinement_enabled);
745  }
746  }
747  status() << "Java: added "
748  << (symbol_table.symbols.size() - before_constant_globals_size)
749  << " String or Class constant symbols"
750  << messaget::eom;
751 
752  // For each reference to a stub global (that is, a global variable declared on
753  // a class we don't have bytecode for, and therefore don't know the static
754  // initialiser for), create a synthetic static initialiser (clinit method)
755  // to nondet initialise it.
756  // Note this must be done before making static initialiser wrappers below, as
757  // this makes a Classname.clinit method, then the next pass makes a wrapper
758  // that ensures it is only run once, and that static initialisation happens
759  // in class-graph topological order.
760 
761  {
762  journalling_symbol_tablet symbol_table_journal =
763  journalling_symbol_tablet::wrap(symbol_table);
764  for(auto &class_to_trees : java_class_loader.get_class_with_overlays_map())
765  {
766  for(const java_bytecode_parse_treet &parse_tree : class_to_trees.second)
767  {
769  parse_tree, symbol_table_journal, class_hierarchy, *this);
770  }
771  }
772 
774  symbol_table, symbol_table_journal.get_inserted(), synthetic_methods);
775  }
776 
777  // For each class that will require a static initializer wrapper, create a
778  // function named package.classname::clinit_wrapper, and a corresponding
779  // global tracking whether it has run or not:
781  symbol_table, synthetic_methods, threading_support);
782 
783  // Now incrementally elaborate methods
784  // that are reachable from this entry point.
785  switch(lazy_methods_mode)
786  {
788  // ci = context-insensitive
790  return true;
791  break;
793  {
794  symbol_table_buildert symbol_table_builder =
795  symbol_table_buildert::wrap(symbol_table);
796 
797  journalling_symbol_tablet journalling_symbol_table =
798  journalling_symbol_tablet::wrap(symbol_table_builder);
799 
800  // Convert all synthetic methods:
801  for(const auto &function_id_and_type : synthetic_methods)
802  {
804  function_id_and_type.first, journalling_symbol_table);
805  }
806  // Convert all methods for which we have bytecode now
807  for(const auto &method_sig : method_bytecode)
808  {
809  convert_single_method(method_sig.first, journalling_symbol_table);
810  }
811  // Now convert all newly added string methods
812  for(const auto &fn_name : journalling_symbol_table.get_inserted())
813  {
815  convert_single_method(fn_name, symbol_table);
816  }
817  }
818  break;
819  default:
820  // Our caller is in charge of elaborating methods on demand.
821  break;
822  }
823 
824  // now instrument runtime exceptions
826  symbol_table,
829 
830  // now typecheck all
831  bool res = java_bytecode_typecheck(
833 
834  // now instrument thread-blocks and synchronized methods.
836  {
837  convert_threadblock(symbol_table);
839  }
840 
841  return res;
842 }
843 
845  symbol_tablet &symbol_table)
846 {
848 
849  symbol_table_buildert symbol_table_builder =
850  symbol_table_buildert::wrap(symbol_table);
851 
854  if(!res.is_success())
855  return res.is_error();
856 
857  // Load the main function into the symbol table to get access to its
858  // parameter names
859  convert_lazy_method(res.main_function.name, symbol_table_builder);
860 
861  // generate the test harness in __CPROVER__start and a call the entry point
862  return java_entry_point(
863  symbol_table_builder,
864  main_class,
871 }
872 
887  symbol_tablet &symbol_table,
888  method_bytecodet &method_bytecode)
889 {
890  symbol_table_buildert symbol_table_builder =
891  symbol_table_buildert::wrap(symbol_table);
892 
893  const method_convertert method_converter =
894  [this, &symbol_table_builder](
895  const irep_idt &function_id,
896  ci_lazy_methods_neededt lazy_methods_needed) {
897  return convert_single_method(
898  function_id, symbol_table_builder, std::move(lazy_methods_needed));
899  };
900 
901  ci_lazy_methodst method_gather(
902  symbol_table,
903  main_class,
911 
912  return method_gather(symbol_table, method_bytecode, method_converter);
913 }
914 
915 const select_pointer_typet &
917 {
918  PRECONDITION(pointer_type_selector.get()!=nullptr);
919  return *pointer_type_selector;
920 }
921 
928  std::unordered_set<irep_idt> &methods) const
929 {
930  const std::string cprover_class_prefix = "java::org.cprover.CProver.";
931 
932  // Add all string solver methods to map
934  // Add all concrete methods to map
935  for(const auto &kv : method_bytecode)
936  {
937  const std::string &method_id = id2string(kv.first);
938 
939  // Avoid advertising org.cprover.CProver methods that the Java frontend will
940  // never provide bodies for (java_bytecode_convert_method always leaves them
941  // bodyless with intent for the driver program to stub them):
942  if(has_prefix(method_id, cprover_class_prefix))
943  {
944  std::size_t method_name_end_offset =
945  method_id.find(':', cprover_class_prefix.length());
946  INVARIANT(
947  method_name_end_offset != std::string::npos,
948  "org.cprover.CProver method should have a postfix type descriptor");
949 
950  const std::string method_name =
951  method_id.substr(
952  cprover_class_prefix.length(),
953  method_name_end_offset - cprover_class_prefix.length());
954 
955  if(cprover_methods_to_ignore.count(method_name))
956  continue;
957  }
958  methods.insert(kv.first);
959  }
960  // Add all synthetic methods to map
961  for(const auto &kv : synthetic_methods)
962  methods.insert(kv.first);
963 }
964 
974  const irep_idt &function_id,
975  symbol_table_baset &symtab)
976 {
977  const symbolt &symbol = symtab.lookup_ref(function_id);
978  if(symbol.value.is_not_nil())
979  return;
980 
981  journalling_symbol_tablet symbol_table=
983 
984  convert_single_method(function_id, symbol_table);
985 
986  // Instrument runtime exceptions (unless symbol is a stub)
987  if(symbol.value.is_not_nil())
988  {
990  symbol_table,
991  symbol_table.get_writeable_ref(function_id),
994  }
995 
996  // now typecheck this function
999 }
1000 
1008  const codet &function_body,
1009  optionalt<ci_lazy_methods_neededt> needed_lazy_methods)
1010 {
1011  if(needed_lazy_methods)
1012  {
1013  for(const_depth_iteratort it = function_body.depth_cbegin();
1014  it != function_body.depth_cend();
1015  ++it)
1016  {
1017  if(it->id() == ID_code)
1018  {
1019  const auto fn_call = expr_try_dynamic_cast<code_function_callt>(*it);
1020  if(!fn_call)
1021  continue;
1022  // Only support non-virtual function calls for now, if string solver
1023  // starts to introduce virtual function calls then we will need to
1024  // duplicate the behavior of java_bytecode_convert_method where it
1025  // handles the invokevirtual instruction
1026  const symbol_exprt &fn_sym =
1027  expr_dynamic_cast<symbol_exprt>(fn_call->function());
1028  needed_lazy_methods->add_needed_method(fn_sym.get_identifier());
1029  }
1030  }
1031  }
1032 }
1033 
1044  const irep_idt &function_id,
1045  symbol_table_baset &symbol_table,
1046  optionalt<ci_lazy_methods_neededt> needed_lazy_methods)
1047 {
1048  const symbolt &symbol = symbol_table.lookup_ref(function_id);
1049 
1050  // Nothing to do if body is already loaded
1051  if(symbol.value.is_not_nil())
1052  return false;
1053 
1054  // Get bytecode for specified function if we have it
1055  method_bytecodet::opt_reft cmb = method_bytecode.get(function_id);
1056 
1057  synthetic_methods_mapt::iterator synthetic_method_it;
1058 
1059  // Check if have a string solver implementation
1060  if(string_preprocess.implements_function(function_id))
1061  {
1062  symbolt &symbol = symbol_table.get_writeable_ref(function_id);
1063  // Load parameter names from any extant bytecode before filling in body
1064  if(cmb)
1065  {
1067  symbol, cmb->get().method.local_variable_table, symbol_table);
1068  }
1069  // Populate body of the function with code generated by string preprocess
1070  const codet generated_code =
1071  string_preprocess.code_for_function(symbol, symbol_table);
1072  // String solver can make calls to functions that haven't yet been seen.
1073  // Add these to the needed_lazy_methods collection
1074  notify_static_method_calls(generated_code, needed_lazy_methods);
1075  symbol.value = std::move(generated_code);
1076  return false;
1077  }
1078  else if(
1079  (synthetic_method_it = synthetic_methods.find(function_id)) !=
1080  synthetic_methods.end())
1081  {
1082  // Synthetic method (i.e. one generated by the Java frontend and which
1083  // doesn't occur in the source bytecode):
1084  symbolt &symbol = symbol_table.get_writeable_ref(function_id);
1085  switch(synthetic_method_it->second)
1086  {
1088  if(threading_support)
1090  function_id,
1091  symbol_table,
1092  nondet_static,
1095  else
1096  symbol.value = get_clinit_wrapper_body(
1097  function_id,
1098  symbol_table,
1099  nondet_static,
1102  break;
1104  symbol.value =
1106  function_id,
1107  symbol_table,
1110  break;
1111  }
1112  // Notify lazy methods of static calls made from the newly generated
1113  // function:
1114  notify_static_method_calls(to_code(symbol.value), needed_lazy_methods);
1115  return false;
1116  }
1117 
1118  // No string solver or static init wrapper implementation;
1119  // check if have bytecode for it
1120  if(cmb)
1121  {
1123  symbol_table.lookup_ref(cmb->get().class_id),
1124  cmb->get().method,
1125  symbol_table,
1129  std::move(needed_lazy_methods),
1133  return false;
1134  }
1135 
1136  // The return of an opaque function is a source of an otherwise invisible
1137  // instantiation, so here we ensure we've loaded the appropriate classes.
1138  const java_method_typet function_type = to_java_method_type(symbol.type);
1139  if(
1140  const pointer_typet *pointer_return_type =
1141  type_try_dynamic_cast<pointer_typet>(function_type.return_type()))
1142  {
1143  // If the return type is abstract, we won't forcibly instantiate it here
1144  // otherwise this can cause abstract methods to be explictly called
1145  // TODO(tkiley): Arguably no abstract class should ever be added to
1146  // TODO(tkiley): ci_lazy_methods_neededt, but this needs further
1147  // TODO(tkiley): investigation
1148  namespacet ns{symbol_table};
1149  const java_class_typet &underlying_type =
1150  to_java_class_type(ns.follow(pointer_return_type->subtype()));
1151 
1152  if(!underlying_type.is_abstract())
1153  needed_lazy_methods->add_all_needed_classes(*pointer_return_type);
1154  }
1155 
1156  return true;
1157 }
1158 
1160 {
1162  return false;
1163 }
1164 
1166 {
1169  parse_trees.front().output(out);
1170  if(parse_trees.size() > 1)
1171  {
1172  out << "\n\nClass has the following overlays:\n\n";
1173  for(auto parse_tree_it = std::next(parse_trees.begin());
1174  parse_tree_it != parse_trees.end();
1175  ++parse_tree_it)
1176  {
1177  parse_tree_it->output(out);
1178  }
1179  out << "End of class overlays.\n";
1180  }
1181 }
1182 
1183 std::unique_ptr<languaget> new_java_bytecode_language()
1184 {
1185  return util_make_unique<java_bytecode_languaget>();
1186 }
1187 
1189  const exprt &expr,
1190  std::string &code,
1191  const namespacet &ns)
1192 {
1193  code=expr2java(expr, ns);
1194  return false;
1195 }
1196 
1198  const typet &type,
1199  std::string &code,
1200  const namespacet &ns)
1201 {
1202  code=type2java(type, ns);
1203  return false;
1204 }
1205 
1207  const std::string &code,
1208  const std::string &module,
1209  exprt &expr,
1210  const namespacet &ns)
1211 {
1212 #if 0
1213  expr.make_nil();
1214 
1215  // no preprocessing yet...
1216 
1217  std::istringstream i_preprocessed(code);
1218 
1219  // parsing
1220 
1221  java_bytecode_parser.clear();
1222  java_bytecode_parser.filename="";
1223  java_bytecode_parser.in=&i_preprocessed;
1224  java_bytecode_parser.set_message_handler(message_handler);
1225  java_bytecode_parser.grammar=java_bytecode_parsert::EXPRESSION;
1226  java_bytecode_parser.mode=java_bytecode_parsert::GCC;
1227  java_bytecode_scanner_init();
1228 
1229  bool result=java_bytecode_parser.parse();
1230 
1231  if(java_bytecode_parser.parse_tree.items.empty())
1232  result=true;
1233  else
1234  {
1235  expr=java_bytecode_parser.parse_tree.items.front().value();
1236 
1237  result=java_bytecode_convert(expr, "", message_handler);
1238 
1239  // typecheck it
1240  if(!result)
1242  }
1243 
1244  // save some memory
1245  java_bytecode_parser.clear();
1246 
1247  return result;
1248 #else
1249  // unused parameters
1250  (void)code;
1251  (void)module;
1252  (void)expr;
1253  (void)ns;
1254 #endif
1255 
1256  return true; // fail for now
1257 }
1258 
1260 {
1261 }
1262 
1266 std::vector<load_extra_methodst>
1268 {
1269  (void)options; // unused parameter
1270  return {};
1271 }
std::vector< irep_idt > java_load_classes
The type of an expression, extends irept.
Definition: type.h:27
irep_idt name
The unique identifier.
Definition: symbol.h:40
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:110
std::string type2java(const typet &type, const namespacet &ns)
Definition: expr2java.cpp:448
void create_static_initializer_wrappers(symbol_tablet &symbol_table, synthetic_methods_mapt &synthetic_methods, const bool thread_safe)
Create static initializer wrappers for all classes that need them.
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.
optionalt< std::reference_wrapper< const class_method_and_bytecodet > > opt_reft
void java_bytecode_typecheck_updated_symbols(journalling_symbol_tablet &symbol_table, message_handlert &message_handler, bool string_refinement_enabled)
A static initializer wrapper (code of the form if(!already_run) clinit(); already_run = true;) These ...
bool is_object() const
Definition: json.h:49
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:173
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
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.
const_depth_iteratort depth_cbegin() const
Definition: expr.cpp:290
void add_classpath_entry(const std::string &)
Appends an entry to the class path, used for loading classes.
Non-graph-based representation of the class hierarchy.
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.
unsigned int get_unsigned_int_option(const std::string &option) const
Definition: options.cpp:54
java_class_loadert java_class_loader
std::function< bool(const irep_idt &function_id, ci_lazy_methods_neededt)> method_convertert
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)
Given the symbol_table and the main_class to test, this function generates a new function __CPROVER__...
Process a pattern to use as a regex for selecting extra entry points for ci_lazy_methodst.
irep_idt mode
Language mode.
Definition: symbol.h:49
code_ifthenelset get_clinit_wrapper_body(const irep_idt &function_id, symbol_table_baset &symbol_table, const bool nondet_static, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector)
Produces the static initializer wrapper body for the given function.
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 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.
void modules_provided(std::set< std::string > &modules) override
const irep_idt & get_identifier() const
Definition: std_expr.h:176
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:173
Definition: json.h:23
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
bool java_bytecode_typecheck(symbol_table_baset &symbol_table, message_handlert &message_handler, bool string_refinement_enabled)
The null pointer constant.
Definition: std_expr.h:4471
exprt value
Initial value of symbol.
Definition: symbol.h:34
const componentst & components() const
Definition: std_types.h:205
std::string get_value(char option) const
Definition: cmdline.cpp:45
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:517
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
const select_pointer_typet & get_pointer_type_selector() const
typet & type()
Return the type of the expression.
Definition: expr.h:68
const value_listt & get_list_option(const std::string &option) const
Definition: options.cpp:78
Symbol table entry.
Definition: symbol.h:27
java_string_library_preprocesst string_preprocess
void show_parse(std::ostream &out) override
void initialize_conversion_table()
fill maps with correspondence from java method names to conversion functions
Forward depth-first search iterators These iterators' copy operations are expensive,...
configt config
Definition: config.cpp:24
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.
java_object_factory_parameterst object_factory_parameters
bool parse_json(std::istream &in, const std::string &filename, message_handlert &message_handler, jsont &dest)
Definition: json_parser.cpp:16
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...
bool is_static_lifetime
Definition: symbol.h:65
std::list< java_bytecode_parse_treet > parse_tree_with_overlayst
A list of parse trees supporting overlay classes.
mstreamt & warning() const
Definition: message.h:391
bool from_expr(const exprt &expr, std::string &code, const namespacet &ns) override
Formats the given expression in a language-specific way.
Class Hierarchy.
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 ...
JAVA Bytecode Language Type Checking.
A symbol table wrapper that records which entries have been updated/removedA caller can pass a journa...
const irep_idt & id() const
Definition: irep.h:259
bool get_is_stub() const
Definition: java_types.h:179
codet code_for_function(const symbolt &symbol, symbol_table_baset &symbol_table)
Should be called to provide code for string functions that are used in the code but for which no impl...
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.
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...
classpatht classpath
Definition: config.h:156
std::set< std::string > extensions() const override
virtual bool isset(char option) const
Definition: cmdline.cpp:27
void convert_synchronized_methods(symbol_tablet &symbol_table, message_handlert &message_handler)
Iterate through the symbol table to find and instrument synchronized methods.
const basest & bases() const
Get the collection of base classes/structs.
Definition: std_types.h:303
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 clear_classpath()
Clear all classpath entries.
resolve_inherited_componentt::inherited_componentt get_inherited_component(const irep_idt &component_class_id, const irep_idt &component_name, const symbol_tablet &symbol_table, const class_hierarchyt &class_hierarchy, bool include_interfaces)
Finds an inherited component (method or field), taking component visibility into account.
Definition: java_utils.cpp:335
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1507
void get_all_function_names(std::unordered_set< irep_idt > &methods) const
JAVA Bytecode Language Conversion.
const changesett & get_inserted() const
fixed_keys_map_wrappert< parse_tree_with_overridest_mapt > get_class_with_overlays_map()
Map from class names to the bytecode parse trees.
const std::string get_option(const std::string &option) const
Definition: options.cpp:65
std::string main
Definition: config.h:172
bool typecheck(symbol_tablet &context, const std::string &module) override
void set_java_cp_include_files(const std::string &java_cp_include_files)
Set the argument of the class loader limit java_class_loader_limitt.
nonstd::optional< T > optionalt
Definition: optional.h:35
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
virtual bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream) override
ANSI-C preprocessing.
The symbol table.
Definition: symbol_table.h:19
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
static std::string file_to_class_name(const std::string &)
Convert a file name to the class name.
Collect methods needed to be loaded using the lazy method.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
std::vector< load_extra_methodst > extra_methods
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)
std::string id() const override
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
std::unique_ptr< languaget > new_java_bytecode_language()
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
class_mapt class_map
const std::unordered_set< std::string > cprover_methods_to_ignore
Methods belonging to the class org.cprover.CProver that should be ignored (not converted),...
Definition: java_utils.cpp:421
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:169
struct configt::javat java
jar_poolt jar_pool
a cache for jar_filet, by path name
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
synthetic_methods_mapt synthetic_methods
Maps synthetic method names on to the particular type of synthetic method (static initializer,...
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:144
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:349
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
Author: Diffblue Ltd.
Class representing a filter for class file loading.
Operator to return the address of an object.
Definition: std_expr.h:3255
bool language_options_initialized
Definition: language.h:190
const symbolst & symbols
bool to_expr(const std::string &code, const std::string &module, exprt &expr, const namespacet &ns) override
Parses the given string into an expression.
bool from_type(const typet &type, std::string &code, const namespacet &ns) override
Formats the given type in a language-specific way.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
bool implements_function(const irep_idt &function_id) const
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 has_component(const irep_idt &component_name) const
Definition: std_types.h:215
An exception that is raised checking whether a class is implicitly generic if a symbol for an outer c...
std::vector< irep_idt > idst
const std::unique_ptr< const select_pointer_typet > pointer_type_selector
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 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.
std::unordered_set< std::string > no_load_classes
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.
static eomt eom
Definition: message.h:284
code_blockt get_thread_safe_clinit_wrapper_body(const irep_idt &function_id, symbol_table_baset &symbol_table, const bool nondet_static, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector)
Thread safe version of the static initializer.
typet type
Type of symbol.
Definition: symbol.h:31
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...
message_handlert & get_message_handler()
Definition: message.h:174
bool do_ci_lazy_method_conversion(symbol_tablet &, method_bytecodet &)
Uses a simple context-insensitive ('ci') analysis to determine which methods may be reachable from th...
const java_method_typet & to_java_method_type(const typet &type)
Definition: java_types.h:338
bool is_string() const
Definition: json.h:39
bool is_array() const
Definition: json.h:54
std::string value
Definition: json.h:137
mstreamt & result() const
Definition: message.h:396
static symbol_table_buildert wrap(symbol_table_baset &base_symbol_table)
mstreamt & status() const
Definition: message.h:401
void set_extra_class_refs_function(get_extra_class_refs_functiont func)
Sets a function that provides extra dependencies for a particular class.
Base class for all expressions.
Definition: expr.h:54
static journalling_symbol_tablet wrap(symbol_table_baset &base_symbol_table)
bool is_state_var
Definition: symbol.h:61
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.
bool parse(std::istream &instream, const std::string &path) override
We set the main class (i.e. class to start the class loading analysis from, see java_class_loadert) d...
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
The symbol table base class interface.
const std::vector< std::string > exception_needed_classes
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.
bool is_abstract() const
Definition: std_types.h:386
#define JAVA_CLASS_MODEL_SUFFIX
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
const_depth_iteratort depth_cend() const
Definition: expr.cpp:292
symbol_exprt get_or_create_string_literal_symbol(const 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.
void set(const optionst &)
Assigns the parameters from given options.
void make_nil()
Definition: irep.h:315
void parse_java_language_options(const cmdlinet &cmd, optionst &options)
Parse options that are java bytecode specific.
const codet & to_code(const exprt &expr)
Definition: std_code.h:136
Author: Diffblue Ltd.
void convert_threadblock(symbol_tablet &symbol_table)
Iterate through the symbol table to find and appropriately instrument thread-blocks.
void set_language_options(const optionst &) override
Consume options that are java bytecode specific.
void java_internal_additions(symbol_table_baset &dest)
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)
Create the body of a synthetic static initializer (clinit method), which initialise stub globals in t...
Expression to hold a symbol (variable)
Definition: std_expr.h:143
Options.
A generated (synthetic) static initializer function for a stub type.
bool has_suffix(const std::string &s, const std::string &suffix)
Definition: suffix.h:15
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1544
Author: Diffblue Ltd.
lazy_methods_modet lazy_methods_mode
irep_idt main_class
Definition: config.h:157
dstringt irep_idt
Definition: irep.h:32
void set_option(const std::string &option, const bool value)
Definition: options.cpp:26
bool generate_support_functions(symbol_tablet &symbol_table) override
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:34
opt_reft get(const irep_idt &method_id)
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.
bool is_type
Definition: symbol.h:61
JAVA Bytecode Language Conversion.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:485
arrayt array
Definition: json.h:129
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...
stub_global_initializer_factoryt stub_global_initializer_factory
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
message_handlert * message_handler
Definition: message.h:426
bool empty() const
Definition: dstring.h:75
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:60
const typet & return_type() const
Definition: std_types.h:883
const java_class_typet & to_java_class_type(const typet &type)
Definition: java_types.h:246
virtual bool final(symbol_table_baset &context) override
Final adjustments, e.g.
std::vector< irep_idt > load_entire_jar(const std::string &jar_path)
Load all class files from a .jar file.
std::vector< irep_idt > main_jar_classes
std::vector< irep_idt > get_string_type_base_classes(const irep_idt &class_name)
Gets the base classes for known String and String-related types, or returns an empty list for other t...
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
std::string expr2java(const exprt &expr, const namespacet &ns)
Definition: expr2java.cpp:441
void convert_single_method(const irep_idt &function_id, symbol_table_baset &symbol_table)
bool is_lvalue
Definition: symbol.h:66