CBMC
Loading...
Searching...
No Matches
java_bytecode_language.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
10
11#include <util/cmdline.h>
12#include <util/config.h>
13#include <util/expr_iterator.h>
14#include <util/invariant.h>
16#include <util/options.h>
17#include <util/suffix.h>
19
21
22#include <json/json_parser.h>
24
25#include "ci_lazy_methods.h"
27#include "expr2java.h"
34#include "java_class_loader.h"
36#include "java_entry_point.h"
40#include "java_utils.h"
41#include "lambda_synthesis.h"
42#include "lift_clinit_calls.h"
44
45#include <fstream>
46#include <string>
47
52{
53 options.set_option(
54 "java-assume-inputs-non-null", cmd.isset("java-assume-inputs-non-null"));
55 options.set_option(
56 "throw-runtime-exceptions", cmd.isset("throw-runtime-exceptions"));
57 options.set_option(
58 "uncaught-exception-check", !cmd.isset("disable-uncaught-exception-check"));
59 options.set_option(
60 "throw-assertion-error", cmd.isset("throw-assertion-error"));
61 options.set_option(
62 "assert-no-exceptions-thrown", cmd.isset("assert-no-exceptions-thrown"));
63 options.set_option("java-threading", cmd.isset("java-threading"));
64
65 if(cmd.isset("java-max-vla-length"))
66 {
67 options.set_option(
68 "java-max-vla-length", cmd.get_value("java-max-vla-length"));
69 }
70
71 options.set_option(
72 "symex-driven-lazy-loading", cmd.isset("symex-driven-lazy-loading"));
73
74 options.set_option(
75 "ignore-manifest-main-class", cmd.isset("ignore-manifest-main-class"));
76
77 if(cmd.isset("context-include"))
78 options.set_option("context-include", cmd.get_values("context-include"));
79
80 if(cmd.isset("context-exclude"))
81 options.set_option("context-exclude", cmd.get_values("context-exclude"));
82
83 if(cmd.isset("java-load-class"))
84 options.set_option("java-load-class", cmd.get_values("java-load-class"));
85
86 if(cmd.isset("java-no-load-class"))
87 {
88 options.set_option(
89 "java-no-load-class", cmd.get_values("java-no-load-class"));
90 }
91 if(cmd.isset("lazy-methods-extra-entry-point"))
92 {
93 options.set_option(
94 "lazy-methods-extra-entry-point",
95 cmd.get_values("lazy-methods-extra-entry-point"));
96 }
97 if(cmd.isset("java-cp-include-files"))
98 {
99 options.set_option(
100 "java-cp-include-files", cmd.get_value("java-cp-include-files"));
101 }
102 if(cmd.isset("static-values"))
103 {
104 options.set_option("static-values", cmd.get_value("static-values"));
105 }
106 options.set_option(
107 "java-lift-clinit-calls", cmd.isset("java-lift-clinit-calls"));
108
109 options.set_option("lazy-methods", !cmd.isset("no-lazy-methods"));
110}
111
113{
114 std::vector<std::string> context_include;
115 std::vector<std::string> context_exclude;
116 for(const auto &include : options.get_list_option("context-include"))
117 context_include.push_back("java::" + include);
118 for(const auto &exclude : options.get_list_option("context-exclude"))
119 context_exclude.push_back("java::" + exclude);
120 return prefix_filtert(std::move(context_include), std::move(context_exclude));
121}
122
123std::unordered_multimap<irep_idt, symbolt> &
125{
126 if(!initialized)
127 {
128 map = class_to_declared_symbols(symbol_table);
129 initialized = true;
130 }
131 return map;
132}
133
139
141 const optionst &options,
142 message_handlert &message_handler)
143{
145 options.get_bool_option("java-assume-inputs-non-null");
146 string_refinement_enabled = options.get_bool_option("refine-strings");
148 options.get_bool_option("throw-runtime-exceptions");
150 options.get_bool_option("uncaught-exception-check");
151 throw_assertion_error = options.get_bool_option("throw-assertion-error");
153 options.get_bool_option("assert-no-exceptions-thrown");
154 threading_support = options.get_bool_option("java-threading");
156 options.get_unsigned_int_option("java-max-vla-length");
157
158 if(options.get_bool_option("symex-driven-lazy-loading"))
160 else if(options.get_bool_option("lazy-methods"))
162 else
164
166 {
167 java_load_classes.insert(
168 java_load_classes.end(),
171 }
172
173 if(options.is_set("java-load-class"))
174 {
175 const auto &load_values = options.get_list_option("java-load-class");
176 java_load_classes.insert(
177 java_load_classes.end(), load_values.begin(), load_values.end());
178 }
179 if(options.is_set("java-no-load-class"))
180 {
181 const auto &no_load_values = options.get_list_option("java-no-load-class");
183 }
184 const std::list<std::string> &extra_entry_points =
185 options.get_list_option("lazy-methods-extra-entry-point");
186 std::transform(
187 extra_entry_points.begin(),
188 extra_entry_points.end(),
189 std::back_inserter(extra_methods),
191
192 java_cp_include_files = options.get_option("java-cp-include-files");
193 if(!java_cp_include_files.empty())
194 {
195 // load file list from JSON file
196 if(java_cp_include_files[0]=='@')
197 {
199 if(parse_json(
200 java_cp_include_files.substr(1), message_handler, json_cp_config))
201 {
202 throw "cannot read JSON input configuration for JAR loading";
203 }
204
205 if(!json_cp_config.is_object())
206 throw "the JSON file has a wrong format";
207 jsont include_files=json_cp_config["jar"];
208 if(!include_files.is_array())
209 throw "the JSON file has a wrong format";
210
211 // add jars from JSON config file to classpath
212 for(const jsont &file_entry : to_json_array(include_files))
213 {
215 file_entry.is_string() && has_suffix(file_entry.value, ".jar"),
216 "classpath entry must be jar filename, but '" + file_entry.value +
217 "' found");
218 config.java.classpath.push_back(file_entry.value);
219 }
220 }
221 }
222 else
224
225 nondet_static = options.get_bool_option("nondet-static");
226 if(options.is_set("static-values"))
227 {
228 const std::string filename = options.get_option("static-values");
230 messaget log{message_handler};
231 if(parse_json(filename, message_handler, tmp_json))
232 {
233 log.warning()
234 << "Provided JSON file for static-values cannot be parsed; it"
235 << " will be ignored." << messaget::eom;
236 }
237 else
238 {
239 if(!tmp_json.is_object())
240 {
241 log.warning() << "Provided JSON file for static-values is not a JSON "
242 << "object; it will be ignored." << messaget::eom;
243 }
244 else
246 }
247 }
248
250 options.get_bool_option("ignore-manifest-main-class");
251
252 if(options.is_set("context-include") || options.is_set("context-exclude"))
253 method_context = get_context(options);
254
255 should_lift_clinit_calls = options.get_bool_option("java-lift-clinit-calls");
256}
257
260 const optionst &options,
261 message_handlert &message_handler)
262{
264 language_options = java_bytecode_language_optionst{options, message_handler};
265 const auto &new_points = build_extra_entry_points(options);
266 language_options->extra_methods.insert(
267 language_options->extra_methods.end(),
268 new_points.begin(),
269 new_points.end());
270}
271
272std::set<std::string> java_bytecode_languaget::extensions() const
273{
274 return { "class", "jar" };
275}
276
277void java_bytecode_languaget::modules_provided(std::set<std::string> &)
278{
279 // modules.insert(translation_unit(parse_path));
280}
281
284 std::istream &,
285 const std::string &,
286 std::ostream &,
288{
289 // there is no preprocessing!
290 return true;
291}
292
294 message_handlert &message_handler)
295{
297
298 for(const auto &p : config.java.classpath)
299 java_class_loader.add_classpath_entry(p, message_handler);
300
302 language_options->java_cp_include_files);
304 if(language_options->string_refinement_enabled)
305 {
307
308 auto get_string_base_classes = [this](const irep_idt &id) {
310 };
311
313 }
314}
315
316static void throwMainClassLoadingError(const std::string &main_class)
317{
318 throw system_exceptiont(
319 "Error: Could not find or load main class " + main_class);
320}
321
323 message_handlert &message_handler)
324{
325 messaget log{message_handler};
326
327 if(!main_class.empty())
328 {
329 // Try to load class
330 log.status() << "Trying to load Java main class: " << main_class
331 << messaget::eom;
332 if(!java_class_loader.can_load_class(main_class, message_handler))
333 {
334 // Try to extract class name and load class
335 const auto maybe_class_name =
338 {
340 return;
341 }
342 log.status() << "Trying to load Java main class: "
343 << maybe_class_name.value() << messaget::eom;
345 maybe_class_name.value(), message_handler))
346 {
348 return;
349 }
350 // Everything went well. We have a loadable main class.
351 // The entry point ('main') will be checked later.
354 }
355 log.status() << "Found Java main class: " << main_class << messaget::eom;
356 // Now really load it.
357 const auto &parse_trees = java_class_loader(main_class, message_handler);
358 if(parse_trees.empty() || !parse_trees.front().loading_successful)
359 {
361 }
362 }
363}
364
372 std::istream &instream,
373 const std::string &path,
374 message_handlert &message_handler)
375{
376 PRECONDITION(language_options.has_value());
377 initialize_class_loader(message_handler);
378
379 // look at extension
380 if(has_suffix(path, ".jar"))
381 {
382 std::ifstream jar_file(path);
383 if(!jar_file.good())
384 {
385 throw system_exceptiont("Error: Unable to access jarfile " + path);
386 }
387
388 // build an object to potentially limit which classes are loaded
390 message_handler, language_options->java_cp_include_files);
391 if(config.java.main_class.empty())
392 {
393 // If we have an entry method, we can derive a main class.
394 if(config.main.has_value())
395 {
396 const std::string &entry_method = config.main.value();
397 const auto last_dot_position = entry_method.find_last_of('.');
399 }
400 else
401 {
402 auto manifest = java_class_loader.jar_pool(path).get_manifest();
403 std::string manifest_main_class = manifest["Main-Class"];
404
405 // if the manifest declares a Main-Class line, we got a main class
406 if(
407 !manifest_main_class.empty() &&
408 !language_options->ignore_manifest_main_class)
409 {
411 }
412 }
413 }
414 else
415 main_class=config.java.main_class;
416
417 // do we have one now?
418 if(main_class.empty())
419 {
420 messaget log{message_handler};
421 log.status() << "JAR file without entry point: loading class files"
422 << messaget::eom;
423 const auto classes =
424 java_class_loader.load_entire_jar(path, message_handler);
425 for(const auto &c : classes)
426 main_jar_classes.push_back(c);
427 }
428 else
429 java_class_loader.add_classpath_entry(path, message_handler);
430 }
431 else
432 main_class = config.java.main_class;
433
434 parse_from_main_class(message_handler);
435 return false;
436}
437
448 const java_bytecode_parse_treet &parse_tree,
449 symbol_table_baset &symbol_table)
450{
451 namespacet ns(symbol_table);
452 for(const auto &method : parse_tree.parsed_class.methods)
453 {
454 for(const java_bytecode_parse_treet::instructiont &instruction :
455 method.instructions)
456 {
457 const std::string statement =
458 bytecode_info[instruction.bytecode].mnemonic;
459 if(statement == "getfield" || statement == "putfield")
460 {
461 const fieldref_exprt &fieldref =
462 expr_dynamic_cast<fieldref_exprt>(instruction.args[0]);
463 irep_idt class_symbol_id = fieldref.class_name();
464 const symbolt *class_symbol = symbol_table.lookup(class_symbol_id);
465 INVARIANT(
466 class_symbol != nullptr,
467 "all types containing fields should have been loaded");
468
471 const irep_idt &component_name = fieldref.component_name();
472 while(!class_type->has_component(component_name))
473 {
474 if(class_type->get_is_stub())
475 {
476 // Accessing a field of an incomplete (opaque) type.
479 auto &components =
480 to_java_class_type(writable_class_symbol.type).components();
481 components.emplace_back(component_name, fieldref.type());
482 components.back().set_base_name(component_name);
483 components.back().set_pretty_name(component_name);
484 components.back().set_is_final(true);
485 break;
486 }
487 else
488 {
489 // Not present here: check the superclass.
490 INVARIANT(
491 !class_type->bases().empty(),
492 "class '" + id2string(class_symbol->name) +
493 "' (which was missing a field '" + id2string(component_name) +
494 "' referenced from method '" + id2string(method.name) +
495 "' of class '" + id2string(parse_tree.parsed_class.name) +
496 "') should have an opaque superclass");
497 const auto &superclass_type = class_type->bases().front().type();
498 class_symbol_id = superclass_type.get_identifier();
501 }
502 }
503 }
504 }
505 }
506}
507
514 const irep_idt &class_id,
515 symbol_table_baset &symbol_table)
516{
517 struct_tag_typet java_lang_Class("java::java.lang.Class");
518 symbol_exprt symbol_expr(
521 if(!symbol_table.has_symbol(symbol_expr.get_identifier()))
522 {
524 symbol_expr.get_identifier(), symbol_expr.type(), ID_java};
525 INVARIANT(
526 new_class_symbol.name.starts_with("java::"),
527 "class identifier should have 'java::' prefix");
528 new_class_symbol.base_name =
529 id2string(new_class_symbol.name).substr(6);
530 new_class_symbol.is_lvalue = true;
531 new_class_symbol.is_state_var = true;
532 new_class_symbol.is_static_lifetime = true;
534 symbol_table.add(new_class_symbol);
535 }
536
537 return symbol_expr;
538}
539
555 const exprt &ldc_arg0,
556 symbol_table_baset &symbol_table,
557 bool string_refinement_enabled)
558{
559 if(ldc_arg0.id() == ID_type)
560 {
561 const irep_idt &class_id = ldc_arg0.type().get(ID_identifier);
562 return
564 get_or_create_class_literal_symbol(class_id, symbol_table));
565 }
566 else if(
567 const auto &literal =
569 {
571 *literal, symbol_table, string_refinement_enabled));
572 }
573 else
574 {
575 INVARIANT(
576 ldc_arg0.is_constant(),
577 "ldc argument should be constant, string literal or class literal");
578 return ldc_arg0;
579 }
580}
581
592 java_bytecode_parse_treet &parse_tree,
593 symbol_table_baset &symbol_table,
594 bool string_refinement_enabled)
595{
596 for(auto &method : parse_tree.parsed_class.methods)
597 {
599 method.instructions)
600 {
601 // ldc* instructions are Java bytecode "load constant" ops, which can
602 // retrieve a numeric constant, String literal, or Class literal.
603 const std::string statement =
604 bytecode_info[instruction.bytecode].mnemonic;
605 // clang-format off
606 if(statement == "ldc" ||
607 statement == "ldc2" ||
608 statement == "ldc_w" ||
609 statement == "ldc2_w")
610 {
611 // clang-format on
612 INVARIANT(
613 instruction.args.size() != 0,
614 "ldc instructions should have an argument");
615 instruction.args[0] =
617 instruction.args[0],
618 symbol_table,
619 string_refinement_enabled);
620 }
621 }
622 }
623}
624
637 symbol_table_baset &symbol_table,
638 const irep_idt &symbol_id,
640 const typet &symbol_type,
641 const irep_idt &class_id,
643{
644 symbolt new_symbol{symbol_id, symbol_type, ID_java};
645 new_symbol.is_static_lifetime = true;
646 new_symbol.is_lvalue = true;
647 new_symbol.is_state_var = true;
648 new_symbol.base_name = symbol_basename;
649 set_declaring_class(new_symbol, class_id);
650 // Public access is a guess; it encourages merging like-typed static fields,
651 // whereas a more restricted visbility would encourage separating them.
652 // Neither is correct, as without the class file we can't know the truth.
653 new_symbol.type.set(ID_C_access, ID_public);
654 // We set the field as final to avoid assuming they can be overridden.
655 new_symbol.type.set(ID_C_constant, true);
656 new_symbol.pretty_name = new_symbol.name;
657 // If pointer-typed, initialise to null and a static initialiser will be
658 // created to initialise on first reference. If primitive-typed, specify
659 // nondeterministic initialisation by setting a nil value.
662 else
663 new_symbol.value.make_nil();
664 bool add_failed = symbol_table.add(new_symbol);
665 INVARIANT(
666 !add_failed, "caller should have checked symbol not already in table");
667}
668
679 const symbol_table_baset &symbol_table,
680 const class_hierarchyt &class_hierarchy)
681{
682 // Depth-first search: return the first stub ancestor, or irep_idt() if none
683 // found.
684 std::vector<irep_idt> classes_to_check;
686
687 while(!classes_to_check.empty())
688 {
689 irep_idt to_check = classes_to_check.back();
690 classes_to_check.pop_back();
691
692 // Exclude java.lang.Object because it can
693 if(
694 to_java_class_type(symbol_table.lookup_ref(to_check).type)
695 .get_is_stub() &&
696 to_check != "java::java.lang.Object")
697 {
698 return to_check;
699 }
700
701 const class_hierarchyt::idst &parents =
702 class_hierarchy.class_map.at(to_check).parents;
703 classes_to_check.insert(
704 classes_to_check.end(), parents.begin(), parents.end());
705 }
706
707 return irep_idt();
708}
709
720 const java_bytecode_parse_treet &parse_tree,
721 symbol_table_baset &symbol_table,
722 const class_hierarchyt &class_hierarchy,
723 messaget &log)
724{
725 namespacet ns(symbol_table);
726 for(const auto &method : parse_tree.parsed_class.methods)
727 {
728 for(const java_bytecode_parse_treet::instructiont &instruction :
729 method.instructions)
730 {
731 const std::string statement =
732 bytecode_info[instruction.bytecode].mnemonic;
733 if(statement == "getstatic" || statement == "putstatic")
734 {
735 INVARIANT(
736 instruction.args.size() > 0,
737 "get/putstatic should have at least one argument");
739 expr_dynamic_cast<fieldref_exprt>(instruction.args[0]);
740 irep_idt component = field_ref.component_name();
741 irep_idt class_id = field_ref.class_name();
742
743 // The final 'true' parameter here includes interfaces, as they can
744 // define static fields.
745 const auto referred_component =
746 get_inherited_component(class_id, component, symbol_table, true);
748 {
749 // Create a new stub global on an arbitrary incomplete ancestor of the
750 // class that was referred to. This is just a guess, but we have no
751 // better information to go on.
754 class_id, symbol_table, class_hierarchy);
755
756 // If there are no incomplete ancestors to ascribe the missing field
757 // to, we must have an incomplete model of a class or simply a
758 // version mismatch of some kind. Normally this would be an error, but
759 // our models library currently triggers this error in some cases
760 // (notably java.lang.System, which is missing System.in/out/err).
761 // Therefore for this case we ascribe the missing field to the class
762 // it was directly referenced from, and fall back to initialising the
763 // field in __CPROVER_initialize, rather than try to create or augment
764 // a clinit method for a non-stub class.
765
768 {
769 add_to_class_id = class_id;
770
771 // TODO forbid this again once the models library has been checked
772 // for missing static fields.
773 log.warning() << "Stub static field " << component << " found for "
774 << "non-stub type " << class_id << ". In future this "
775 << "will be a fatal error." << messaget::eom;
776 }
777
778 irep_idt identifier =
780
782 symbol_table,
783 identifier,
784 component,
785 instruction.args[0].type(),
788 }
789 }
790 }
791 }
792}
793
795 symbol_table_baset &symbol_table,
796 const std::string &,
797 message_handlert &message_handler)
798{
799 PRECONDITION(language_options.has_value());
800 // There are various cases in the Java front-end where pre-existing symbols
801 // from a previous load are not handled. We just rule this case out for now;
802 // a user wishing to ensure a particular class is loaded should use
803 // --java-load-class (to force class-loading) or
804 // --lazy-methods-extra-entry-point (to ensure a method body is loaded)
805 // instead of creating two instances of the front-end.
806 INVARIANT(
807 symbol_table.begin() == symbol_table.end(),
808 "the Java front-end should only be used with an empty symbol table");
809
810 java_internal_additions(symbol_table);
811 create_java_initialize(symbol_table);
812
813 if(language_options->string_refinement_enabled)
815
816 // Must load java.lang.Object first to avoid stubbing
817 // This ordering could alternatively be enforced by
818 // moving the code below to the class loader.
819 java_class_loadert::parse_tree_with_overridest_mapt::const_iterator it =
820 java_class_loader.get_class_with_overlays_map().find("java.lang.Object");
822 {
824 it->second,
825 symbol_table,
826 message_handler,
827 language_options->max_user_array_length,
830 language_options->no_load_classes))
831 {
832 return true;
833 }
834 }
835
836 // first generate a new struct symbol for each class and a new function symbol
837 // for every method
839 {
840 if(class_trees.second.front().parsed_class.name.empty())
841 continue;
842
844 class_trees.second,
845 symbol_table,
846 message_handler,
847 language_options->max_user_array_length,
850 language_options->no_load_classes))
851 {
852 return true;
853 }
854 }
855
856 // Register synthetic method that replaces a real definition if one is
857 // available:
859 {
862 }
863
864 // Now add synthetic classes for every invokedynamic instruction found (it
865 // makes this easier that all interface types and their methods have been
866 // created above):
867 {
868 std::vector<irep_idt> methods_to_check;
869
870 // Careful not to add to the symtab while iterating over it:
871 for(const auto &id_and_symbol : symbol_table)
872 {
873 const auto &symbol = id_and_symbol.second;
874 const auto &id = symbol.name;
875 if(can_cast_type<code_typet>(symbol.type) && method_bytecode.get(id))
876 {
877 methods_to_check.push_back(id);
878 }
879 }
880
881 for(const auto &id : methods_to_check)
882 {
884 id,
885 method_bytecode.get(id)->get().method.instructions,
886 symbol_table,
888 message_handler);
889 }
890 }
891
892 // Now that all classes have been created in the symbol table we can populate
893 // the class hierarchy:
894 class_hierarchy(symbol_table);
895
896 // find and mark all implicitly generic class types
897 // this can only be done once all the class symbols have been created
899 {
900 if(c.second.front().parsed_class.name.empty())
901 continue;
902 try
903 {
905 c.second.front().parsed_class.name, symbol_table);
906 }
908 {
909 messaget log(message_handler);
910 log.warning() << "Not marking class " << c.first
911 << " implicitly generic due to missing outer class symbols"
912 << messaget::eom;
913 }
914 }
915
916 // Infer fields on opaque types based on the method instructions just loaded.
917 // For example, if we don't have bytecode for field x of class A, but we can
918 // see an int-typed getfield instruction referring to it, add that field now.
920 {
921 for(const java_bytecode_parse_treet &parse_tree : class_to_trees.second)
922 infer_opaque_type_fields(parse_tree, symbol_table);
923 }
924
925 // Create global variables for constants (String and Class literals) up front.
926 // This means that when running with lazy loading, we will be aware of these
927 // literal globals' existence when __CPROVER_initialize is generated in
928 // `generate_support_functions`.
929 const std::size_t before_constant_globals_size = symbol_table.symbols.size();
931 {
932 for(java_bytecode_parse_treet &parse_tree : class_to_trees.second)
933 {
935 parse_tree, symbol_table, language_options->string_refinement_enabled);
936 }
937 }
938
939 messaget log(message_handler);
940 log.status() << "Java: added "
941 << (symbol_table.symbols.size() - before_constant_globals_size)
942 << " String or Class constant symbols" << messaget::eom;
943
944 // For each reference to a stub global (that is, a global variable declared on
945 // a class we don't have bytecode for, and therefore don't know the static
946 // initialiser for), create a synthetic static initialiser (clinit method)
947 // to nondet initialise it.
948 // Note this must be done before making static initialiser wrappers below, as
949 // this makes a Classname.clinit method, then the next pass makes a wrapper
950 // that ensures it is only run once, and that static initialisation happens
951 // in class-graph topological order.
952
953 {
957 {
958 for(const java_bytecode_parse_treet &parse_tree : class_to_trees.second)
959 {
962 }
963 }
964
966 symbol_table, symbol_table_journal.get_inserted(), synthetic_methods);
967 }
968
970 symbol_table,
972 language_options->threading_support,
973 language_options->static_values_json.has_value());
974
976
977 // Now incrementally elaborate methods
978 // that are reachable from this entry point.
979 switch(language_options->lazy_methods_mode)
980 {
982 // ci = context-insensitive
983 if(do_ci_lazy_method_conversion(symbol_table, message_handler))
984 return true;
985 break;
987 {
989 symbol_table_buildert::wrap(symbol_table);
990
993
994 // Convert all synthetic methods:
995 for(const auto &function_id_and_type : synthetic_methods)
996 {
1001 message_handler);
1002 }
1003 // Convert all methods for which we have bytecode now
1004 for(const auto &method_sig : method_bytecode)
1005 {
1007 method_sig.first,
1010 message_handler);
1011 }
1016 message_handler);
1017 // Now convert all newly added string methods
1018 for(const auto &fn_name : journalling_symbol_table.get_inserted())
1019 {
1022 fn_name, symbol_table, class_to_declared_symbols, message_handler);
1023 }
1024 }
1025 break;
1027 // Our caller is in charge of elaborating methods on demand.
1028 break;
1029 }
1030
1031 // now instrument runtime exceptions
1033 symbol_table, language_options->throw_runtime_exceptions, message_handler);
1034
1035 // now typecheck all
1037 symbol_table, message_handler, language_options->string_refinement_enabled);
1038
1039 // now instrument thread-blocks and synchronized methods.
1040 if(language_options->threading_support)
1041 {
1042 convert_threadblock(symbol_table);
1043 convert_synchronized_methods(symbol_table, message_handler);
1044 }
1045
1046 return res;
1047}
1048
1050 symbol_table_baset &symbol_table,
1051 message_handlert &message_handler)
1052{
1053 PRECONDITION(language_options.has_value());
1054
1056 symbol_table_buildert::wrap(symbol_table);
1057
1059 get_main_symbol(symbol_table, main_class, message_handler);
1060 if(!res.is_success())
1061 return res.is_error();
1062
1063 // Load the main function into the symbol table to get access to its
1064 // parameter names
1066 res.main_function.name, symbol_table_builder, message_handler);
1067
1068 const symbolt &symbol =
1069 symbol_table_builder.lookup_ref(res.main_function.name);
1070 if(symbol.value.is_nil())
1071 {
1073 "the program has no entry point",
1074 "function",
1075 "Check that the specified entry point is included by your "
1076 "--context-include or --context-exclude options");
1077 }
1078
1079 // generate the test harness in __CPROVER__start and a call the entry point
1080 return java_entry_point(
1082 main_class,
1083 message_handler,
1084 language_options->assume_inputs_non_null,
1085 language_options->assert_uncaught_exceptions,
1088 language_options->string_refinement_enabled,
1089 [&](const symbolt &function, symbol_table_baset &symbol_table) {
1090 return java_build_arguments(
1091 function,
1092 symbol_table,
1093 language_options->assume_inputs_non_null,
1094 object_factory_parameters,
1095 get_pointer_type_selector(),
1096 message_handler);
1097 });
1098}
1099
1113 symbol_table_baset &symbol_table,
1114 message_handlert &message_handler)
1115{
1117 symbol_table_buildert::wrap(symbol_table);
1118
1120
1122 [this, &symbol_table_builder, &class_to_declared_symbols, &message_handler](
1123 const irep_idt &function_id,
1125 return convert_single_method(
1126 function_id,
1128 std::move(lazy_methods_needed),
1130 message_handler);
1131 };
1132
1134 symbol_table,
1135 main_class,
1137 language_options->extra_methods,
1142
1143 return method_gather(
1144 symbol_table, method_bytecode, method_converter, message_handler);
1145}
1146
1153
1160 std::unordered_set<irep_idt> &methods) const
1161{
1162 const std::string cprover_class_prefix = "java::org.cprover.CProver.";
1163
1164 // Add all string solver methods to map
1166 // Add all concrete methods to map
1167 for(const auto &kv : method_bytecode)
1168 methods.insert(kv.first);
1169 // Add all synthetic methods to map
1170 for(const auto &kv : synthetic_methods)
1171 methods.insert(kv.first);
1172 methods.insert(INITIALIZE_FUNCTION);
1173}
1174
1185 const irep_idt &function_id,
1187 message_handlert &message_handler)
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
1198 function_id, symbol_table, class_to_declared_symbols, message_handler);
1199
1200 // Instrument runtime exceptions (unless symbol is a stub or is the
1201 // INITIALISE_FUNCTION).
1202 if(symbol.value.is_not_nil() && function_id != INITIALIZE_FUNCTION)
1203 {
1205 symbol_table,
1206 symbol_table.get_writeable_ref(function_id),
1207 language_options->throw_runtime_exceptions,
1208 message_handler);
1209 }
1210
1211 // now typecheck this function
1213 symbol_table, message_handler, language_options->string_refinement_enabled);
1214}
1215
1227 const codet &function_body,
1228 std::optional<ci_lazy_methods_neededt> needed_lazy_methods)
1229{
1230 if(needed_lazy_methods)
1231 {
1232 for(const_depth_iteratort it = function_body.depth_cbegin();
1233 it != function_body.depth_cend();
1234 ++it)
1235 {
1236 if(it->id() == ID_code)
1237 {
1239 if(!fn_call)
1240 continue;
1241 const symbol_exprt *fn_sym =
1243 if(fn_sym)
1244 needed_lazy_methods->add_needed_method(fn_sym->get_identifier());
1245 }
1246 else if(
1247 it->id() == ID_side_effect &&
1249 {
1251 const symbol_exprt *fn_sym =
1253 if(fn_sym)
1254 {
1255 INVARIANT(
1256 false,
1257 "Java synthetic methods are not "
1258 "expected to produce side_effect_expr_function_callt. If "
1259 "that has changed, remove this invariant. Also note that "
1260 "as of the time of writing remove_virtual_functions did "
1261 "not support this form of function call.");
1262 // needed_lazy_methods->add_needed_method(fn_sym->get_identifier());
1263 }
1264 }
1265 }
1266 }
1267}
1268
1283 const irep_idt &function_id,
1284 symbol_table_baset &symbol_table,
1285 std::optional<ci_lazy_methods_neededt> needed_lazy_methods,
1287 message_handlert &message_handler)
1288{
1289 const symbolt &symbol = symbol_table.lookup_ref(function_id);
1290
1291 // Nothing to do if body is already loaded
1292 if(symbol.value.is_not_nil())
1293 return false;
1294
1295 if(function_id == INITIALIZE_FUNCTION)
1296 {
1298 symbol_table,
1299 symbol.location,
1300 language_options->assume_inputs_non_null,
1303 language_options->string_refinement_enabled,
1304 message_handler);
1305 return false;
1306 }
1307
1308 INVARIANT(declaring_class(symbol), "Method must have a declaring class.");
1309
1311 function_id,
1312 symbol_table,
1313 needed_lazy_methods,
1315 message_handler);
1316
1317 if(symbol.value.is_not_nil() && language_options->should_lift_clinit_calls)
1318 {
1319 auto &writable_symbol = symbol_table.get_writeable_ref(function_id);
1320 writable_symbol.value =
1321 lift_clinit_calls(std::move(to_code(writable_symbol.value)));
1322 }
1323
1324 INVARIANT(declaring_class(symbol), "Method must have a declaring class.");
1325
1326 return ret;
1327}
1328
1342 const irep_idt &function_id,
1343 symbol_table_baset &symbol_table,
1344 std::optional<ci_lazy_methods_neededt> needed_lazy_methods,
1346 message_handlert &message_handler)
1347{
1348 const auto &symbol = symbol_table.lookup_ref(function_id);
1349 PRECONDITION(symbol.value.is_nil());
1350
1351 // Get bytecode for specified function if we have it
1353
1354 synthetic_methods_mapt::iterator synthetic_method_it;
1355
1356 // Check if have a string solver implementation
1357 if(string_preprocess.implements_function(function_id))
1358 {
1359 symbolt &writable_symbol = symbol_table.get_writeable_ref(function_id);
1360 // Load parameter names from any extant bytecode before filling in body
1361 if(cmb)
1362 {
1364 writable_symbol, cmb->get().method.local_variable_table, symbol_table);
1365 }
1366 // Populate body of the function with code generated by string preprocess
1368 writable_symbol, symbol_table, message_handler);
1369 // String solver can make calls to functions that haven't yet been seen.
1370 // Add these to the needed_lazy_methods collection
1371 notify_static_method_calls(generated_code, needed_lazy_methods);
1372 writable_symbol.value = std::move(generated_code);
1373 return false;
1374 }
1375 else if(
1376 (synthetic_method_it = synthetic_methods.find(function_id)) !=
1377 synthetic_methods.end())
1378 {
1379 // Synthetic method (i.e. one generated by the Java frontend and which
1380 // doesn't occur in the source bytecode):
1381 symbolt &writable_symbol = symbol_table.get_writeable_ref(function_id);
1382 switch(synthetic_method_it->second)
1383 {
1385 if(language_options->threading_support)
1387 function_id,
1388 symbol_table,
1389 language_options->nondet_static,
1390 language_options->static_values_json.has_value(),
1393 message_handler);
1394 else
1396 function_id,
1397 symbol_table,
1398 language_options->nondet_static,
1399 language_options->static_values_json.has_value(),
1402 message_handler);
1403 break;
1405 {
1406 const auto class_name =
1407 declaring_class(symbol_table.lookup_ref(function_id));
1408 INVARIANT(
1409 class_name, "user_specified_clinit must be declared by a class.");
1410 INVARIANT(
1411 language_options->static_values_json.has_value(),
1412 "static-values JSON must be available");
1414 *class_name,
1415 *language_options->static_values_json,
1416 symbol_table,
1417 needed_lazy_methods,
1418 language_options->max_user_array_length,
1419 references,
1420 class_to_declared_symbols.get(symbol_table));
1421 break;
1422 }
1424 writable_symbol.value =
1426 function_id,
1427 symbol_table,
1430 message_handler);
1431 break;
1434 function_id, symbol_table, message_handler);
1435 break;
1438 function_id, symbol_table, message_handler);
1439 break;
1441 {
1442 INVARIANT(
1443 cmb,
1444 "CProver.createArrayWithType should only be registered if "
1445 "we have a real implementation available");
1447 writable_symbol, cmb->get().method.local_variable_table, symbol_table);
1448 writable_symbol.value =
1449 create_array_with_type_body(function_id, symbol_table, message_handler);
1450 break;
1451 }
1452 }
1453 // Notify lazy methods of static calls made from the newly generated
1454 // function:
1456 to_code(writable_symbol.value), needed_lazy_methods);
1457 return false;
1458 }
1459
1460 // No string solver or static init wrapper implementation;
1461 // check if have bytecode for it
1462 if(cmb)
1463 {
1465 symbol_table.lookup_ref(cmb->get().class_id),
1466 cmb->get().method,
1467 symbol_table,
1468 message_handler,
1469 language_options->max_user_array_length,
1470 language_options->throw_assertion_error,
1471 std::move(needed_lazy_methods),
1474 language_options->threading_support,
1475 language_options->method_context,
1476 language_options->assert_no_exceptions_thrown);
1477 return false;
1478 }
1479
1480 if(needed_lazy_methods)
1481 {
1482 // The return of an opaque function is a source of an otherwise invisible
1483 // instantiation, so here we ensure we've loaded the appropriate classes.
1484 const java_method_typet function_type = to_java_method_type(symbol.type);
1485 if(
1488 {
1489 // If the return type is abstract, we won't forcibly instantiate it here
1490 // otherwise this can cause abstract methods to be explictly called
1491 // TODO(tkiley): Arguably no abstract class should ever be added to
1492 // TODO(tkiley): ci_lazy_methods_neededt, but this needs further
1493 // TODO(tkiley): investigation
1494 namespacet ns{symbol_table};
1495 const java_class_typet &underlying_type = to_java_class_type(
1496 ns.follow_tag(to_struct_tag_type(pointer_return_type->base_type())));
1497
1498 if(!underlying_type.is_abstract())
1499 needed_lazy_methods->add_all_needed_classes(*pointer_return_type);
1500 }
1501 }
1502
1503 return true;
1504}
1505
1507{
1508 PRECONDITION(language_options.has_value());
1509 return false;
1510}
1511
1513 std::ostream &out,
1514 message_handlert &message_handler)
1515{
1517 java_class_loader(main_class, message_handler);
1518 parse_trees.front().output(out);
1519 if(parse_trees.size() > 1)
1520 {
1521 out << "\n\nClass has the following overlays:\n\n";
1522 for(auto parse_tree_it = std::next(parse_trees.begin());
1523 parse_tree_it != parse_trees.end();
1524 ++parse_tree_it)
1525 {
1526 parse_tree_it->output(out);
1527 }
1528 out << "End of class overlays.\n";
1529 }
1530}
1531
1532std::unique_ptr<languaget> new_java_bytecode_language()
1533{
1534 return std::make_unique<java_bytecode_languaget>();
1535}
1536
1538 const exprt &expr,
1539 std::string &code,
1540 const namespacet &ns)
1541{
1542 code=expr2java(expr, ns);
1543 return false;
1544}
1545
1547 const typet &type,
1548 std::string &code,
1549 const namespacet &ns)
1550{
1551 code=type2java(type, ns);
1552 return false;
1553}
1554
1556 const std::string &code,
1557 const std::string &module,
1558 exprt &expr,
1559 const namespacet &ns,
1560 message_handlert &message_handler)
1561{
1562#if 0
1563 expr.make_nil();
1564
1565 // no preprocessing yet...
1566
1567 std::istringstream i_preprocessed(code);
1568
1569 // parsing
1570
1572 java_bytecode_parser.filename="";
1574 java_bytecode_parser.set_message_handler(message_handler);
1575 java_bytecode_parser.grammar=java_bytecode_parsert::EXPRESSION;
1576 java_bytecode_parser.mode=java_bytecode_parsert::GCC;
1578
1579 bool result=java_bytecode_parser.parse();
1580
1581 if(java_bytecode_parser.parse_tree.items.empty())
1582 result=true;
1583 else
1584 {
1585 expr=java_bytecode_parser.parse_tree.items.front().value();
1586
1587 result=java_bytecode_convert(expr, "", message_handler);
1588
1589 // typecheck it
1590 if(!result)
1591 result=java_bytecode_typecheck(expr, message_handler, ns);
1592 }
1593
1594 // save some memory
1596
1597 return result;
1598#else
1599 // unused parameters
1600 (void)code;
1601 (void)module;
1602 (void)expr;
1603 (void)ns;
1604 (void)message_handler;
1605#endif
1606
1607 return true; // fail for now
1608}
1609
1613
1617std::vector<load_extra_methodst>
1619{
1620 (void)options; // unused parameter
1621 return {};
1622}
configt config
Definition config.cpp:25
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.
virtual void output(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const
Output the abstract states for a single function.
Definition ai.cpp:39
virtual void clear()
Reset the abstract state.
Definition ai.h:265
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Non-graph-based representation of the class hierarchy.
std::vector< irep_idt > idst
bool is_abstract() const
Definition std_types.h:358
const typet & return_type() const
Definition std_types.h:689
Data structure for representing an arbitrary statement in a program.
std::optional< std::string > main
Definition config.h:390
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:38
bool empty() const
Definition dstring.h:89
Base class for all expressions.
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:84
Represents the argument of an instruction that uses a CONSTANT_Fieldref This is used for example as a...
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
bool is_not_nil() const
Definition irep.h:372
void make_nil()
Definition irep.h:446
bool is_nil() const
Definition irep.h:368
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...
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
bool to_expr(const std::string &code, const std::string &module, exprt &expr, const namespacet &ns, message_handlert &message_handler) override
Parses the given string into an expression.
virtual bool final(symbol_table_baset &context) override
Final adjustments, e.g.
std::string id() const override
stub_global_initializer_factoryt stub_global_initializer_factory
std::set< std::string > extensions() const override
bool from_type(const typet &type, std::string &code, const namespacet &ns) override
Formats the given type in a language-specific way.
void set_language_options(const optionst &, message_handlert &) override
Consume options that are java bytecode specific.
const std::unique_ptr< const select_pointer_typet > pointer_type_selector
java_object_factory_parameterst object_factory_parameters
void show_parse(std::ostream &out, message_handlert &) override
void initialize_class_loader(message_handlert &)
java_string_library_preprocesst string_preprocess
void modules_provided(std::set< std::string > &modules) override
java_class_loadert java_class_loader
virtual void convert_lazy_method(const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler) override
Promote a lazy-converted method (one whose type is known but whose body hasn't been converted) into a...
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.
std::optional< java_bytecode_language_optionst > language_options
const select_pointer_typet & get_pointer_type_selector() const
void parse_from_main_class(message_handlert &)
bool convert_single_method_code(const irep_idt &function_id, symbol_table_baset &symbol_table, std::optional< ci_lazy_methods_neededt > needed_lazy_methods, lazy_class_to_declared_symbols_mapt &class_to_declared_symbols, message_handlert &)
Convert a method (one whose type is known but whose body hasn't been converted) but don't run typeche...
bool from_expr(const exprt &expr, std::string &code, const namespacet &ns) override
Formats the given expression in a language-specific way.
void convert_single_method(const irep_idt &function_id, symbol_table_baset &symbol_table, lazy_class_to_declared_symbols_mapt &class_to_declared_symbols, message_handlert &message_handler)
std::unordered_map< std::string, object_creation_referencet > references
Map used in all calls to functions that deterministically create objects (currently only assign_from_...
bool typecheck(symbol_table_baset &context, const std::string &module, message_handlert &message_handler) override
virtual bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream, message_handlert &message_handler) override
ANSI-C preprocessing.
bool generate_support_functions(symbol_table_baset &symbol_table, message_handlert &message_handler) override
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
bool do_ci_lazy_method_conversion(symbol_table_baset &, message_handlert &)
Uses a simple context-insensitive ('ci') analysis to determine which methods may be reachable from th...
bool parse(std::istream &instream, const std::string &path, message_handlert &message_handler) override
We set the main class (i.e. class to start the class loading analysis, see java_class_loadert) when w...
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 > java_load_classes
Classes to be explicitly loaded.
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.
fixed_keys_map_wrappert< parse_tree_with_overridest_mapt > get_class_with_overlays_map()
Map from class names to the bytecode parse trees.
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.
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...
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)
Definition json.h:27
bool is_array() const
Definition json.h:61
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_table_baset &symbol_table)
std::unordered_multimap< irep_idt, symbolt > map
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
static eomt eom
Definition message.h:289
opt_reft get(const irep_idt &method_id)
std::optional< 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 union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
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.
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 ...
Provides filtering of strings vai inclusion/exclusion lists of prefixes.
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:493
void create_stub_global_initializer_symbols(symbol_table_baset &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.
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...
Expression to hold a symbol (variable)
Definition std_expr.h:131
const irep_idt & get_identifier() const
Definition std_expr.h:160
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.
virtual iteratort begin()=0
const symbolst & symbols
Read-only field, used to look up symbols given their names.
virtual iteratort end()=0
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.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Author: Diffblue Ltd.
static symbol_table_buildert wrap(symbol_table_baset &base_symbol_table)
Symbol table entry.
Definition symbol.h:28
source_locationt location
Source code location of definition of symbol.
Definition symbol.h:37
exprt value
Initial value of symbol.
Definition symbol.h:34
Thrown when some external system fails unexpectedly.
The type of an expression, extends irept.
Definition type.h:29
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)
std::string expr2java(const exprt &expr, const namespacet &ns)
Forward depth-first search iterators These iterators' copy operations are expensive,...
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
void convert_synchronized_methods(symbol_table_baset &symbol_table, message_handlert &message_handler)
Iterate through the symbol table to find and instrument synchronized methods.
void convert_threadblock(symbol_table_baset &symbol_table)
Iterate through the symbol table to find and appropriately instrument thread-blocks.
void mark_java_implicitly_generic_class_type(const irep_idt &class_name, symbol_table_baset &symbol_table)
Checks if the class is implicitly generic, i.e., it is an inner class of any generic class.
bool java_bytecode_convert_class(const java_class_loadert::parse_tree_with_overlayst &parse_trees, symbol_table_baset &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.
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, std::optional< ci_lazy_methods_neededt > needed_lazy_methods, java_string_library_preprocesst &string_preprocess, const class_hierarchyt &class_hierarchy, bool threading_support, const std::optional< 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_table_baset &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 generate_constant_global_variables(java_bytecode_parse_treet &parse_tree, symbol_table_baset &symbol_table, bool string_refinement_enabled)
Creates global variables for constants mentioned in a given method.
static exprt get_ldc_result(const exprt &ldc_arg0, symbol_table_baset &symbol_table, bool string_refinement_enabled)
Get result of a Java load-constant (ldc) instruction.
void parse_java_language_options(const cmdlinet &cmd, optionst &options)
Parse options that are java bytecode specific.
std::unique_ptr< languaget > new_java_bytecode_language()
static symbol_exprt get_or_create_class_literal_symbol(const irep_idt &class_id, symbol_table_baset &symbol_table)
Create if necessary, then return the constant global java.lang.Class symbol for a given class id.
static void infer_opaque_type_fields(const java_bytecode_parse_treet &parse_tree, symbol_table_baset &symbol_table)
Infer fields that must exist on opaque types from field accesses against them.
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 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_table_baset &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 void notify_static_method_calls(const codet &function_body, std::optional< ci_lazy_methods_neededt > needed_lazy_methods)
Notify ci_lazy_methods, if present, of any static function calls made by the given function body.
@ LAZY_METHODS_MODE_EAGER
@ LAZY_METHODS_MODE_EXTERNAL_DRIVER
@ LAZY_METHODS_MODE_CONTEXT_INSENSITIVE
#define JAVA_CLASS_MODEL_SUFFIX
prefix_filtert get_context(const optionst &options)
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.
std::unordered_multimap< irep_idt, symbolt > class_to_declared_symbols(const symbol_table_baset &symbol_table)
code_blockt get_user_specified_clinit_body(const irep_idt &class_id, const json_objectt &static_values_json, symbol_table_baset &symbol_table, std::optional< 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...
void create_static_initializer_symbols(symbol_table_baset &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_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.
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_method_typet & to_java_method_type(const typet &type)
Definition java_types.h:183
const java_class_typet & to_java_class_type(const typet &type)
Definition java_types.h:581
std::optional< irep_idt > declaring_class(const symbolt &symbol)
Gets the identifier of the class which declared a given symbol.
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.
std::optional< 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.
std::optional< resolve_inherited_componentt::inherited_componentt > get_inherited_component(const irep_idt &component_class_id, const irep_idt &component_name, const symbol_table_baset &symbol_table, bool include_interfaces)
Finds an inherited component (method or field), taking component visibility into account.
Author: Diffblue Ltd.
json_objectt & to_json_object(jsont &json)
Definition json.h:442
json_arrayt & to_json_array(jsont &json)
Definition json.h:424
bool parse_json(std::istream &in, const std::string &filename, message_handlert &message_handler, jsont &dest)
void create_invokedynamic_synthetic_classes(const irep_idt &method_identifier, const java_bytecode_parse_treet::methodt::instructionst &instructions, symbol_table_baset &symbol_table, synthetic_methods_mapt &synthetic_methods, message_handlert &message_handler)
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.
Java lambda code synthesis.
codet lift_clinit_calls(codet input)
file Static initializer call lifting
std::function< std::vector< irep_idt >(const symbol_table_baset &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.
double log(double x)
Definition math.c:2449
Options.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#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:122
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition std_types.h:518
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....
std::optional< prefix_filtert > method_context
If set, method bodies are only elaborated if they pass the filter.
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
std::optional< json_objectt > static_values_json
JSON which contains initial values of static fields (right after the static initializer of the class ...
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
@ 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.
dstringt irep_idt