cprover
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 <fstream>
12#include <string>
13
15
16#include <util/cmdline.h>
17#include <util/config.h>
18#include <util/expr_iterator.h>
19#include <util/invariant.h>
21#include <util/options.h>
22#include <util/prefix.h>
23#include <util/suffix.h>
25
26#include <json/json_parser.h>
27
29
30#include "ci_lazy_methods.h"
38#include "java_class_loader.h"
40#include "java_entry_point.h"
44#include "java_utils.h"
45#include "lambda_synthesis.h"
46#include "lift_clinit_calls.h"
47
48#include "expr2java.h"
50
55{
56 options.set_option(
57 "java-assume-inputs-non-null", cmd.isset("java-assume-inputs-non-null"));
58 options.set_option(
59 "throw-runtime-exceptions", cmd.isset("throw-runtime-exceptions"));
60 options.set_option(
61 "uncaught-exception-check", !cmd.isset("disable-uncaught-exception-check"));
62 options.set_option(
63 "throw-assertion-error", cmd.isset("throw-assertion-error"));
64 options.set_option(
65 "assert-no-exceptions-thrown", cmd.isset("assert-no-exceptions-thrown"));
66 options.set_option("java-threading", cmd.isset("java-threading"));
67
68 if(cmd.isset("java-max-vla-length"))
69 {
70 options.set_option(
71 "java-max-vla-length", cmd.get_value("java-max-vla-length"));
72 }
73
74 options.set_option(
75 "symex-driven-lazy-loading", cmd.isset("symex-driven-lazy-loading"));
76
77 options.set_option(
78 "ignore-manifest-main-class", cmd.isset("ignore-manifest-main-class"));
79
80 if(cmd.isset("context-include"))
81 options.set_option("context-include", cmd.get_values("context-include"));
82
83 if(cmd.isset("context-exclude"))
84 options.set_option("context-exclude", cmd.get_values("context-exclude"));
85
86 if(cmd.isset("java-load-class"))
87 options.set_option("java-load-class", cmd.get_values("java-load-class"));
88
89 if(cmd.isset("java-no-load-class"))
90 {
91 options.set_option(
92 "java-no-load-class", cmd.get_values("java-no-load-class"));
93 }
94 if(cmd.isset("lazy-methods-extra-entry-point"))
95 {
96 options.set_option(
97 "lazy-methods-extra-entry-point",
98 cmd.get_values("lazy-methods-extra-entry-point"));
99 }
100 if(cmd.isset("java-cp-include-files"))
101 {
102 options.set_option(
103 "java-cp-include-files", cmd.get_value("java-cp-include-files"));
104 }
105 if(cmd.isset("static-values"))
106 {
107 options.set_option("static-values", cmd.get_value("static-values"));
108 }
109 options.set_option(
110 "java-lift-clinit-calls", cmd.isset("java-lift-clinit-calls"));
111
112 options.set_option("lazy-methods", !cmd.isset("no-lazy-methods"));
113}
114
116{
117 std::vector<std::string> context_include;
118 std::vector<std::string> context_exclude;
119 for(const auto &include : options.get_list_option("context-include"))
120 context_include.push_back("java::" + include);
121 for(const auto &exclude : options.get_list_option("context-exclude"))
122 context_exclude.push_back("java::" + exclude);
123 return prefix_filtert(std::move(context_include), std::move(context_exclude));
124}
125
126std::unordered_multimap<irep_idt, symbolt> &
128{
129 if(!initialized)
130 {
131 map = class_to_declared_symbols(symbol_table);
132 initialized = true;
133 }
134 return map;
135}
136
142
144 const optionst &options,
145 messaget &log)
146{
148 options.get_bool_option("java-assume-inputs-non-null");
149 string_refinement_enabled = options.get_bool_option("refine-strings");
151 options.get_bool_option("throw-runtime-exceptions");
153 options.get_bool_option("uncaught-exception-check");
154 throw_assertion_error = options.get_bool_option("throw-assertion-error");
156 options.get_bool_option("assert-no-exceptions-thrown");
157 threading_support = options.get_bool_option("java-threading");
159 options.get_unsigned_int_option("java-max-vla-length");
160
161 if(options.get_bool_option("symex-driven-lazy-loading"))
163 else if(options.get_bool_option("lazy-methods"))
165 else
167
169 {
170 java_load_classes.insert(
171 java_load_classes.end(),
174 }
175
176 if(options.is_set("java-load-class"))
177 {
178 const auto &load_values = options.get_list_option("java-load-class");
179 java_load_classes.insert(
180 java_load_classes.end(), load_values.begin(), load_values.end());
181 }
182 if(options.is_set("java-no-load-class"))
183 {
184 const auto &no_load_values = options.get_list_option("java-no-load-class");
186 }
187 const std::list<std::string> &extra_entry_points =
188 options.get_list_option("lazy-methods-extra-entry-point");
189 std::transform(
190 extra_entry_points.begin(),
191 extra_entry_points.end(),
192 std::back_inserter(extra_methods),
194
195 java_cp_include_files = options.get_option("java-cp-include-files");
196 if(!java_cp_include_files.empty())
197 {
198 // load file list from JSON file
199 if(java_cp_include_files[0]=='@')
200 {
202 if(parse_json(
203 java_cp_include_files.substr(1),
206 throw "cannot read JSON input configuration for JAR loading";
207
208 if(!json_cp_config.is_object())
209 throw "the JSON file has a wrong format";
210 jsont include_files=json_cp_config["jar"];
211 if(!include_files.is_array())
212 throw "the JSON file has a wrong format";
213
214 // add jars from JSON config file to classpath
215 for(const jsont &file_entry : to_json_array(include_files))
216 {
218 file_entry.is_string() && has_suffix(file_entry.value, ".jar"),
219 "classpath entry must be jar filename, but '" + file_entry.value +
220 "' found");
221 config.java.classpath.push_back(file_entry.value);
222 }
223 }
224 }
225 else
227
228 nondet_static = options.get_bool_option("nondet-static");
229 if(options.is_set("static-values"))
230 {
231 const std::string filename = options.get_option("static-values");
233 if(parse_json(filename, log.get_message_handler(), tmp_json))
234 {
235 log.warning()
236 << "Provided JSON file for static-values cannot be parsed; it"
237 << " will be ignored." << messaget::eom;
238 }
239 else
240 {
241 if(!tmp_json.is_object())
242 {
243 log.warning() << "Provided JSON file for static-values is not a JSON "
244 << "object; it will be ignored." << messaget::eom;
245 }
246 else
248 }
249 }
250
252 options.get_bool_option("ignore-manifest-main-class");
253
254 if(options.is_set("context-include") || options.is_set("context-exclude"))
255 method_context = get_context(options);
256
257 should_lift_clinit_calls = options.get_bool_option("java-lift-clinit-calls");
258}
259
262{
265 const auto &new_points = build_extra_entry_points(options);
266 language_options->extra_methods.insert(
267 language_options->extra_methods.end(),
268 new_points.begin(),
269 new_points.end());
270}
271
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 &)
287{
288 // there is no preprocessing!
289 return true;
290}
291
297
319
320static void throwMainClassLoadingError(const std::string &main_class)
321{
322 throw system_exceptiont(
323 "Error: Could not find or load main class " + main_class);
324}
325
327{
328 if(!main_class.empty())
329 {
330 // Try to load class
331 status() << "Trying to load Java main class: " << main_class << eom;
333 {
334 // Try to extract class name and load class
335 const auto maybe_class_name =
338 {
340 return;
341 }
342 status() << "Trying to load Java main class: " << maybe_class_name.value()
343 << eom;
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 status() << "Found Java main class: " << main_class << eom;
356 // Now really load it.
357 const auto &parse_trees =
359 if(parse_trees.empty() || !parse_trees.front().loading_successful)
360 {
362 }
363 }
364}
365
369{
370 PRECONDITION(language_options.has_value());
372 main_class = config.java.main_class;
374 return false;
375}
376
384 std::istream &instream,
385 const std::string &path)
386{
387 PRECONDITION(language_options.has_value());
389
390 // look at extension
391 if(has_suffix(path, ".jar"))
392 {
393 std::ifstream jar_file(path);
394 if(!jar_file.good())
395 {
396 throw system_exceptiont("Error: Unable to access jarfile " + path);
397 }
398
399 // build an object to potentially limit which classes are loaded
401 get_message_handler(), language_options->java_cp_include_files);
402 if(config.java.main_class.empty())
403 {
404 // If we have an entry method, we can derive a main class.
405 if(config.main.has_value())
406 {
407 const std::string &entry_method = config.main.value();
408 const auto last_dot_position = entry_method.find_last_of('.');
410 }
411 else
412 {
413 auto manifest = java_class_loader.jar_pool(path).get_manifest();
414 std::string manifest_main_class = manifest["Main-Class"];
415
416 // if the manifest declares a Main-Class line, we got a main class
417 if(
418 !manifest_main_class.empty() &&
419 !language_options->ignore_manifest_main_class)
420 {
422 }
423 }
424 }
425 else
426 main_class=config.java.main_class;
427
428 // do we have one now?
429 if(main_class.empty())
430 {
431 status() << "JAR file without entry point: loading class files" << eom;
432 const auto classes =
434 for(const auto &c : classes)
435 main_jar_classes.push_back(c);
436 }
437 else
439 }
440 else
441 main_class = config.java.main_class;
442
444 return false;
445}
446
457 const java_bytecode_parse_treet &parse_tree,
458 symbol_table_baset &symbol_table)
459{
460 namespacet ns(symbol_table);
461 for(const auto &method : parse_tree.parsed_class.methods)
462 {
463 for(const java_bytecode_parse_treet::instructiont &instruction :
464 method.instructions)
465 {
466 const std::string statement =
467 bytecode_info[instruction.bytecode].mnemonic;
468 if(statement == "getfield" || statement == "putfield")
469 {
470 const fieldref_exprt &fieldref =
471 expr_dynamic_cast<fieldref_exprt>(instruction.args[0]);
472 irep_idt class_symbol_id = fieldref.class_name();
473 const symbolt *class_symbol = symbol_table.lookup(class_symbol_id);
474 INVARIANT(
475 class_symbol != nullptr,
476 "all types containing fields should have been loaded");
477
480 const irep_idt &component_name = fieldref.component_name();
481 while(!class_type->has_component(component_name))
482 {
483 if(class_type->get_is_stub())
484 {
485 // Accessing a field of an incomplete (opaque) type.
488 auto &components =
489 to_java_class_type(writable_class_symbol.type).components();
490 components.emplace_back(component_name, fieldref.type());
491 components.back().set_base_name(component_name);
492 components.back().set_pretty_name(component_name);
493 components.back().set_is_final(true);
494 break;
495 }
496 else
497 {
498 // Not present here: check the superclass.
499 INVARIANT(
500 !class_type->bases().empty(),
501 "class '" + id2string(class_symbol->name) +
502 "' (which was missing a field '" + id2string(component_name) +
503 "' referenced from method '" + id2string(method.name) +
504 "' of class '" + id2string(parse_tree.parsed_class.name) +
505 "') should have an opaque superclass");
506 const auto &superclass_type = class_type->bases().front().type();
507 class_symbol_id = superclass_type.get_identifier();
509 }
510 }
511 }
512 }
513 }
514}
515
522 const irep_idt &class_id,
523 symbol_table_baset &symbol_table)
524{
525 struct_tag_typet java_lang_Class("java::java.lang.Class");
526 symbol_exprt symbol_expr(
529 if(!symbol_table.has_symbol(symbol_expr.get_identifier()))
530 {
532 symbol_expr.get_identifier(), symbol_expr.type(), ID_java};
533 INVARIANT(
534 has_prefix(id2string(new_class_symbol.name), "java::"),
535 "class identifier should have 'java::' prefix");
536 new_class_symbol.base_name =
537 id2string(new_class_symbol.name).substr(6);
538 new_class_symbol.is_lvalue = true;
539 new_class_symbol.is_state_var = true;
540 new_class_symbol.is_static_lifetime = true;
542 symbol_table.add(new_class_symbol);
543 }
544
545 return symbol_expr;
546}
547
563 const exprt &ldc_arg0,
564 symbol_table_baset &symbol_table,
565 bool string_refinement_enabled)
566{
567 if(ldc_arg0.id() == ID_type)
568 {
569 const irep_idt &class_id = ldc_arg0.type().get(ID_identifier);
570 return
572 get_or_create_class_literal_symbol(class_id, symbol_table));
573 }
574 else if(
575 const auto &literal =
577 {
579 *literal, symbol_table, string_refinement_enabled));
580 }
581 else
582 {
583 INVARIANT(
584 ldc_arg0.is_constant(),
585 "ldc argument should be constant, string literal or class literal");
586 return ldc_arg0;
587 }
588}
589
600 java_bytecode_parse_treet &parse_tree,
601 symbol_table_baset &symbol_table,
602 bool string_refinement_enabled)
603{
604 for(auto &method : parse_tree.parsed_class.methods)
605 {
607 method.instructions)
608 {
609 // ldc* instructions are Java bytecode "load constant" ops, which can
610 // retrieve a numeric constant, String literal, or Class literal.
611 const std::string statement =
612 bytecode_info[instruction.bytecode].mnemonic;
613 // clang-format off
614 if(statement == "ldc" ||
615 statement == "ldc2" ||
616 statement == "ldc_w" ||
617 statement == "ldc2_w")
618 {
619 // clang-format on
620 INVARIANT(
621 instruction.args.size() != 0,
622 "ldc instructions should have an argument");
623 instruction.args[0] =
625 instruction.args[0],
626 symbol_table,
627 string_refinement_enabled);
628 }
629 }
630 }
631}
632
645 symbol_table_baset &symbol_table,
646 const irep_idt &symbol_id,
648 const typet &symbol_type,
649 const irep_idt &class_id,
651{
652 symbolt new_symbol{symbol_id, symbol_type, ID_java};
653 new_symbol.is_static_lifetime = true;
654 new_symbol.is_lvalue = true;
655 new_symbol.is_state_var = true;
656 new_symbol.base_name = symbol_basename;
657 set_declaring_class(new_symbol, class_id);
658 // Public access is a guess; it encourages merging like-typed static fields,
659 // whereas a more restricted visbility would encourage separating them.
660 // Neither is correct, as without the class file we can't know the truth.
661 new_symbol.type.set(ID_C_access, ID_public);
662 // We set the field as final to avoid assuming they can be overridden.
663 new_symbol.type.set(ID_C_constant, true);
664 new_symbol.pretty_name = new_symbol.name;
665 // If pointer-typed, initialise to null and a static initialiser will be
666 // created to initialise on first reference. If primitive-typed, specify
667 // nondeterministic initialisation by setting a nil value.
670 else
671 new_symbol.value.make_nil();
672 bool add_failed = symbol_table.add(new_symbol);
673 INVARIANT(
674 !add_failed, "caller should have checked symbol not already in table");
675}
676
687 const symbol_table_baset &symbol_table,
688 const class_hierarchyt &class_hierarchy)
689{
690 // Depth-first search: return the first stub ancestor, or irep_idt() if none
691 // found.
692 std::vector<irep_idt> classes_to_check;
694
695 while(!classes_to_check.empty())
696 {
697 irep_idt to_check = classes_to_check.back();
698 classes_to_check.pop_back();
699
700 // Exclude java.lang.Object because it can
701 if(
702 to_java_class_type(symbol_table.lookup_ref(to_check).type)
703 .get_is_stub() &&
704 to_check != "java::java.lang.Object")
705 {
706 return to_check;
707 }
708
709 const class_hierarchyt::idst &parents =
710 class_hierarchy.class_map.at(to_check).parents;
711 classes_to_check.insert(
712 classes_to_check.end(), parents.begin(), parents.end());
713 }
714
715 return irep_idt();
716}
717
728 const java_bytecode_parse_treet &parse_tree,
729 symbol_table_baset &symbol_table,
730 const class_hierarchyt &class_hierarchy,
731 messaget &log)
732{
733 namespacet ns(symbol_table);
734 for(const auto &method : parse_tree.parsed_class.methods)
735 {
736 for(const java_bytecode_parse_treet::instructiont &instruction :
737 method.instructions)
738 {
739 const std::string statement =
740 bytecode_info[instruction.bytecode].mnemonic;
741 if(statement == "getstatic" || statement == "putstatic")
742 {
743 INVARIANT(
744 instruction.args.size() > 0,
745 "get/putstatic should have at least one argument");
747 expr_dynamic_cast<fieldref_exprt>(instruction.args[0]);
748 irep_idt component = field_ref.component_name();
749 irep_idt class_id = field_ref.class_name();
750
751 // The final 'true' parameter here includes interfaces, as they can
752 // define static fields.
753 const auto referred_component =
754 get_inherited_component(class_id, component, symbol_table, true);
756 {
757 // Create a new stub global on an arbitrary incomplete ancestor of the
758 // class that was referred to. This is just a guess, but we have no
759 // better information to go on.
762 class_id, symbol_table, class_hierarchy);
763
764 // If there are no incomplete ancestors to ascribe the missing field
765 // to, we must have an incomplete model of a class or simply a
766 // version mismatch of some kind. Normally this would be an error, but
767 // our models library currently triggers this error in some cases
768 // (notably java.lang.System, which is missing System.in/out/err).
769 // Therefore for this case we ascribe the missing field to the class
770 // it was directly referenced from, and fall back to initialising the
771 // field in __CPROVER_initialize, rather than try to create or augment
772 // a clinit method for a non-stub class.
773
776 {
777 add_to_class_id = class_id;
778
779 // TODO forbid this again once the models library has been checked
780 // for missing static fields.
781 log.warning() << "Stub static field " << component << " found for "
782 << "non-stub type " << class_id << ". In future this "
783 << "will be a fatal error." << messaget::eom;
784 }
785
786 irep_idt identifier =
788
790 symbol_table,
791 identifier,
792 component,
793 instruction.args[0].type(),
796 }
797 }
798 }
799 }
800}
801
803 symbol_table_baset &symbol_table,
804 const std::string &)
805{
806 PRECONDITION(language_options.has_value());
807 // There are various cases in the Java front-end where pre-existing symbols
808 // from a previous load are not handled. We just rule this case out for now;
809 // a user wishing to ensure a particular class is loaded should use
810 // --java-load-class (to force class-loading) or
811 // --lazy-methods-extra-entry-point (to ensure a method body is loaded)
812 // instead of creating two instances of the front-end.
813 INVARIANT(
814 symbol_table.begin() == symbol_table.end(),
815 "the Java front-end should only be used with an empty symbol table");
816
817 java_internal_additions(symbol_table);
818 create_java_initialize(symbol_table);
819
820 if(language_options->string_refinement_enabled)
822
823 // Must load java.lang.Object first to avoid stubbing
824 // This ordering could alternatively be enforced by
825 // moving the code below to the class loader.
826 java_class_loadert::parse_tree_with_overridest_mapt::const_iterator it =
827 java_class_loader.get_class_with_overlays_map().find("java.lang.Object");
829 {
831 it->second,
832 symbol_table,
834 language_options->max_user_array_length,
837 language_options->no_load_classes))
838 {
839 return true;
840 }
841 }
842
843 // first generate a new struct symbol for each class and a new function symbol
844 // for every method
846 {
847 if(class_trees.second.front().parsed_class.name.empty())
848 continue;
849
851 class_trees.second,
852 symbol_table,
854 language_options->max_user_array_length,
857 language_options->no_load_classes))
858 {
859 return true;
860 }
861 }
862
863 // Register synthetic method that replaces a real definition if one is
864 // available:
866 {
869 }
870
871 // Now add synthetic classes for every invokedynamic instruction found (it
872 // makes this easier that all interface types and their methods have been
873 // created above):
874 {
875 std::vector<irep_idt> methods_to_check;
876
877 // Careful not to add to the symtab while iterating over it:
878 for(const auto &id_and_symbol : symbol_table)
879 {
880 const auto &symbol = id_and_symbol.second;
881 const auto &id = symbol.name;
882 if(can_cast_type<code_typet>(symbol.type) && method_bytecode.get(id))
883 {
884 methods_to_check.push_back(id);
885 }
886 }
887
888 for(const auto &id : methods_to_check)
889 {
891 id,
892 method_bytecode.get(id)->get().method.instructions,
893 symbol_table,
896 }
897 }
898
899 // Now that all classes have been created in the symbol table we can populate
900 // the class hierarchy:
901 class_hierarchy(symbol_table);
902
903 // find and mark all implicitly generic class types
904 // this can only be done once all the class symbols have been created
906 {
907 if(c.second.front().parsed_class.name.empty())
908 continue;
909 try
910 {
912 c.second.front().parsed_class.name, symbol_table);
913 }
915 {
917 << "Not marking class " << c.first
918 << " implicitly generic due to missing outer class symbols"
919 << messaget::eom;
920 }
921 }
922
923 // Infer fields on opaque types based on the method instructions just loaded.
924 // For example, if we don't have bytecode for field x of class A, but we can
925 // see an int-typed getfield instruction referring to it, add that field now.
927 {
928 for(const java_bytecode_parse_treet &parse_tree : class_to_trees.second)
929 infer_opaque_type_fields(parse_tree, symbol_table);
930 }
931
932 // Create global variables for constants (String and Class literals) up front.
933 // This means that when running with lazy loading, we will be aware of these
934 // literal globals' existence when __CPROVER_initialize is generated in
935 // `generate_support_functions`.
936 const std::size_t before_constant_globals_size = symbol_table.symbols.size();
938 {
939 for(java_bytecode_parse_treet &parse_tree : class_to_trees.second)
940 {
942 parse_tree, symbol_table, language_options->string_refinement_enabled);
943 }
944 }
945 status() << "Java: added "
946 << (symbol_table.symbols.size() - before_constant_globals_size)
947 << " String or Class constant symbols"
948 << messaget::eom;
949
950 // For each reference to a stub global (that is, a global variable declared on
951 // a class we don't have bytecode for, and therefore don't know the static
952 // initialiser for), create a synthetic static initialiser (clinit method)
953 // to nondet initialise it.
954 // Note this must be done before making static initialiser wrappers below, as
955 // this makes a Classname.clinit method, then the next pass makes a wrapper
956 // that ensures it is only run once, and that static initialisation happens
957 // in class-graph topological order.
958
959 {
963 {
964 for(const java_bytecode_parse_treet &parse_tree : class_to_trees.second)
965 {
967 parse_tree, symbol_table_journal, class_hierarchy, *this);
968 }
969 }
970
972 symbol_table, symbol_table_journal.get_inserted(), synthetic_methods);
973 }
974
976 symbol_table,
978 language_options->threading_support,
979 language_options->static_values_json.has_value());
980
982
983 // Now incrementally elaborate methods
984 // that are reachable from this entry point.
985 switch(language_options->lazy_methods_mode)
986 {
988 // ci = context-insensitive
989 if(do_ci_lazy_method_conversion(symbol_table))
990 return true;
991 break;
993 {
995 symbol_table_buildert::wrap(symbol_table);
996
999
1000 // Convert all synthetic methods:
1001 for(const auto &function_id_and_type : synthetic_methods)
1002 {
1007 }
1008 // Convert all methods for which we have bytecode now
1009 for(const auto &method_sig : method_bytecode)
1010 {
1013 }
1016 // Now convert all newly added string methods
1017 for(const auto &fn_name : journalling_symbol_table.get_inserted())
1018 {
1021 }
1022 }
1023 break;
1025 // Our caller is in charge of elaborating methods on demand.
1026 break;
1027 }
1028
1029 // now instrument runtime exceptions
1031 symbol_table,
1032 language_options->throw_runtime_exceptions,
1034
1035 // now typecheck all
1037 symbol_table,
1039 language_options->string_refinement_enabled);
1040
1041 // now instrument thread-blocks and synchronized methods.
1042 if(language_options->threading_support)
1043 {
1044 convert_threadblock(symbol_table);
1046 }
1047
1048 return res;
1049}
1050
1052 symbol_table_baset &symbol_table)
1053{
1054 PRECONDITION(language_options.has_value());
1055
1057 symbol_table_buildert::wrap(symbol_table);
1058
1061 if(!res.is_success())
1062 return res.is_error();
1063
1064 // Load the main function into the symbol table to get access to its
1065 // parameter names
1066 convert_lazy_method(res.main_function.name, symbol_table_builder);
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,
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 get_message_handler());
1097 });
1098}
1099
1143
1150
1157 std::unordered_set<irep_idt> &methods) const
1158{
1159 const std::string cprover_class_prefix = "java::org.cprover.CProver.";
1160
1161 // Add all string solver methods to map
1163 // Add all concrete methods to map
1164 for(const auto &kv : method_bytecode)
1165 methods.insert(kv.first);
1166 // Add all synthetic methods to map
1167 for(const auto &kv : synthetic_methods)
1168 methods.insert(kv.first);
1169 methods.insert(INITIALIZE_FUNCTION);
1170}
1171
1181 const irep_idt &function_id,
1183{
1184 const symbolt &symbol = symtab.lookup_ref(function_id);
1185 if(symbol.value.is_not_nil())
1186 return;
1187
1188 journalling_symbol_tablet symbol_table=
1190
1192 convert_single_method(function_id, symbol_table, class_to_declared_symbols);
1193
1194 // Instrument runtime exceptions (unless symbol is a stub or is the
1195 // INITIALISE_FUNCTION).
1196 if(symbol.value.is_not_nil() && function_id != INITIALIZE_FUNCTION)
1197 {
1199 symbol_table,
1200 symbol_table.get_writeable_ref(function_id),
1201 language_options->throw_runtime_exceptions,
1203 }
1204
1205 // now typecheck this function
1207 symbol_table,
1209 language_options->string_refinement_enabled);
1210}
1211
1223 const codet &function_body,
1224 optionalt<ci_lazy_methods_neededt> needed_lazy_methods)
1225{
1226 if(needed_lazy_methods)
1227 {
1228 for(const_depth_iteratort it = function_body.depth_cbegin();
1229 it != function_body.depth_cend();
1230 ++it)
1231 {
1232 if(it->id() == ID_code)
1233 {
1235 if(!fn_call)
1236 continue;
1237 const symbol_exprt *fn_sym =
1239 if(fn_sym)
1240 needed_lazy_methods->add_needed_method(fn_sym->get_identifier());
1241 }
1242 else if(
1243 it->id() == ID_side_effect &&
1245 {
1247 const symbol_exprt *fn_sym =
1249 if(fn_sym)
1250 {
1251 INVARIANT(
1252 false,
1253 "Java synthetic methods are not "
1254 "expected to produce side_effect_expr_function_callt. If "
1255 "that has changed, remove this invariant. Also note that "
1256 "as of the time of writing remove_virtual_functions did "
1257 "not support this form of function call.");
1258 // needed_lazy_methods->add_needed_method(fn_sym->get_identifier());
1259 }
1260 }
1261 }
1262 }
1263}
1264
1278 const irep_idt &function_id,
1279 symbol_table_baset &symbol_table,
1280 optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
1282{
1283 const symbolt &symbol = symbol_table.lookup_ref(function_id);
1284
1285 // Nothing to do if body is already loaded
1286 if(symbol.value.is_not_nil())
1287 return false;
1288
1289 if(function_id == INITIALIZE_FUNCTION)
1290 {
1292 symbol_table,
1293 symbol.location,
1294 language_options->assume_inputs_non_null,
1297 language_options->string_refinement_enabled,
1299 return false;
1300 }
1301
1302 INVARIANT(declaring_class(symbol), "Method must have a declaring class.");
1303
1305 function_id, symbol_table, needed_lazy_methods, class_to_declared_symbols);
1306
1307 if(symbol.value.is_not_nil() && language_options->should_lift_clinit_calls)
1308 {
1309 auto &writable_symbol = symbol_table.get_writeable_ref(function_id);
1310 writable_symbol.value =
1311 lift_clinit_calls(std::move(to_code(writable_symbol.value)));
1312 }
1313
1314 INVARIANT(declaring_class(symbol), "Method must have a declaring class.");
1315
1316 return ret;
1317}
1318
1331 const irep_idt &function_id,
1332 symbol_table_baset &symbol_table,
1333 optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
1335{
1336 const auto &symbol = symbol_table.lookup_ref(function_id);
1337 PRECONDITION(symbol.value.is_nil());
1338
1339 // Get bytecode for specified function if we have it
1341
1342 synthetic_methods_mapt::iterator synthetic_method_it;
1343
1344 // Check if have a string solver implementation
1345 if(string_preprocess.implements_function(function_id))
1346 {
1347 symbolt &writable_symbol = symbol_table.get_writeable_ref(function_id);
1348 // Load parameter names from any extant bytecode before filling in body
1349 if(cmb)
1350 {
1352 writable_symbol, cmb->get().method.local_variable_table, symbol_table);
1353 }
1354 // Populate body of the function with code generated by string preprocess
1356 writable_symbol, symbol_table, get_message_handler());
1357 // String solver can make calls to functions that haven't yet been seen.
1358 // Add these to the needed_lazy_methods collection
1359 notify_static_method_calls(generated_code, needed_lazy_methods);
1360 writable_symbol.value = std::move(generated_code);
1361 return false;
1362 }
1363 else if(
1364 (synthetic_method_it = synthetic_methods.find(function_id)) !=
1365 synthetic_methods.end())
1366 {
1367 // Synthetic method (i.e. one generated by the Java frontend and which
1368 // doesn't occur in the source bytecode):
1369 symbolt &writable_symbol = symbol_table.get_writeable_ref(function_id);
1370 switch(synthetic_method_it->second)
1371 {
1373 if(language_options->threading_support)
1375 function_id,
1376 symbol_table,
1377 language_options->nondet_static,
1378 language_options->static_values_json.has_value(),
1382 else
1384 function_id,
1385 symbol_table,
1386 language_options->nondet_static,
1387 language_options->static_values_json.has_value(),
1391 break;
1393 {
1394 const auto class_name =
1395 declaring_class(symbol_table.lookup_ref(function_id));
1396 INVARIANT(
1397 class_name, "user_specified_clinit must be declared by a class.");
1398 INVARIANT(
1399 language_options->static_values_json.has_value(),
1400 "static-values JSON must be available");
1402 *class_name,
1403 *language_options->static_values_json,
1404 symbol_table,
1405 needed_lazy_methods,
1406 language_options->max_user_array_length,
1407 references,
1408 class_to_declared_symbols.get(symbol_table));
1409 break;
1410 }
1412 writable_symbol.value =
1414 function_id,
1415 symbol_table,
1419 break;
1422 function_id, symbol_table, get_message_handler());
1423 break;
1426 function_id, symbol_table, get_message_handler());
1427 break;
1429 {
1430 INVARIANT(
1431 cmb,
1432 "CProver.createArrayWithType should only be registered if "
1433 "we have a real implementation available");
1435 writable_symbol, cmb->get().method.local_variable_table, symbol_table);
1437 function_id, symbol_table, get_message_handler());
1438 break;
1439 }
1440 }
1441 // Notify lazy methods of static calls made from the newly generated
1442 // function:
1444 to_code(writable_symbol.value), needed_lazy_methods);
1445 return false;
1446 }
1447
1448 // No string solver or static init wrapper implementation;
1449 // check if have bytecode for it
1450 if(cmb)
1451 {
1453 symbol_table.lookup_ref(cmb->get().class_id),
1454 cmb->get().method,
1455 symbol_table,
1457 language_options->max_user_array_length,
1458 language_options->throw_assertion_error,
1459 std::move(needed_lazy_methods),
1462 language_options->threading_support,
1463 language_options->method_context,
1464 language_options->assert_no_exceptions_thrown);
1465 return false;
1466 }
1467
1468 if(needed_lazy_methods)
1469 {
1470 // The return of an opaque function is a source of an otherwise invisible
1471 // instantiation, so here we ensure we've loaded the appropriate classes.
1472 const java_method_typet function_type = to_java_method_type(symbol.type);
1473 if(
1476 {
1477 // If the return type is abstract, we won't forcibly instantiate it here
1478 // otherwise this can cause abstract methods to be explictly called
1479 // TODO(tkiley): Arguably no abstract class should ever be added to
1480 // TODO(tkiley): ci_lazy_methods_neededt, but this needs further
1481 // TODO(tkiley): investigation
1482 namespacet ns{symbol_table};
1483 const java_class_typet &underlying_type =
1484 to_java_class_type(ns.follow(pointer_return_type->base_type()));
1485
1486 if(!underlying_type.is_abstract())
1487 needed_lazy_methods->add_all_needed_classes(*pointer_return_type);
1488 }
1489 }
1490
1491 return true;
1492}
1493
1495{
1496 PRECONDITION(language_options.has_value());
1497 return false;
1498}
1499
1501{
1504 parse_trees.front().output(out);
1505 if(parse_trees.size() > 1)
1506 {
1507 out << "\n\nClass has the following overlays:\n\n";
1508 for(auto parse_tree_it = std::next(parse_trees.begin());
1509 parse_tree_it != parse_trees.end();
1510 ++parse_tree_it)
1511 {
1512 parse_tree_it->output(out);
1513 }
1514 out << "End of class overlays.\n";
1515 }
1516}
1517
1518std::unique_ptr<languaget> new_java_bytecode_language()
1519{
1521}
1522
1524 const exprt &expr,
1525 std::string &code,
1526 const namespacet &ns)
1527{
1528 code=expr2java(expr, ns);
1529 return false;
1530}
1531
1533 const typet &type,
1534 std::string &code,
1535 const namespacet &ns)
1536{
1537 code=type2java(type, ns);
1538 return false;
1539}
1540
1542 const std::string &code,
1543 const std::string &module,
1544 exprt &expr,
1545 const namespacet &ns)
1546{
1547#if 0
1548 expr.make_nil();
1549
1550 // no preprocessing yet...
1551
1552 std::istringstream i_preprocessed(code);
1553
1554 // parsing
1555
1557 java_bytecode_parser.filename="";
1559 java_bytecode_parser.set_message_handler(message_handler);
1560 java_bytecode_parser.grammar=java_bytecode_parsert::EXPRESSION;
1561 java_bytecode_parser.mode=java_bytecode_parsert::GCC;
1563
1564 bool result=java_bytecode_parser.parse();
1565
1566 if(java_bytecode_parser.parse_tree.items.empty())
1567 result=true;
1568 else
1569 {
1570 expr=java_bytecode_parser.parse_tree.items.front().value();
1571
1573
1574 // typecheck it
1575 if(!result)
1577 }
1578
1579 // save some memory
1581
1582 return result;
1583#else
1584 // unused parameters
1585 (void)code;
1586 (void)module;
1587 (void)expr;
1588 (void)ns;
1589#endif
1590
1591 return true; // fail for now
1592}
1593
1597
1601std::vector<load_extra_methodst>
1603{
1604 (void)options; // unused parameter
1605 return {};
1606}
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:266
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
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:645
Data structure for representing an arbitrary statement in a program.
optionalt< std::string > main
Definition config.h:353
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:39
bool empty() const
Definition dstring.h:90
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:380
void make_nil()
Definition irep.h:454
bool is_nil() const
Definition irep.h:376
virtual void methods_provided(std::unordered_set< irep_idt > &methods) const override
Provide feedback to language_filest so that when asked for a lazy method, it can delegate to this ins...
void show_parse(std::ostream &out) override
synthetic_methods_mapt synthetic_methods
Maps synthetic method names on to the particular type of synthetic method (static initializer,...
std::vector< irep_idt > main_jar_classes
virtual bool final(symbol_table_baset &context) override
Final adjustments, e.g.
virtual bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream) override
ANSI-C preprocessing.
std::string id() const override
stub_global_initializer_factoryt stub_global_initializer_factory
std::set< std::string > extensions() const override
bool generate_support_functions(symbol_table_baset &symbol_table) override
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
void set_message_handler(message_handlert &message_handler) override
bool typecheck(symbol_table_baset &context, const std::string &module) override
void set_language_options(const optionst &) override
Consume options that are java bytecode specific.
bool from_type(const typet &type, std::string &code, const namespacet &ns) override
Formats the given type in a language-specific way.
bool to_expr(const std::string &code, const std::string &module, exprt &expr, const namespacet &ns) override
Parses the given string into an expression.
const std::unique_ptr< const select_pointer_typet > pointer_type_selector
java_object_factory_parameterst object_factory_parameters
bool do_ci_lazy_method_conversion(symbol_table_baset &)
Uses a simple context-insensitive ('ci') analysis to determine which methods may be reachable from th...
optionalt< java_bytecode_language_optionst > language_options
java_string_library_preprocesst string_preprocess
void modules_provided(std::set< std::string > &modules) override
java_class_loadert java_class_loader
bool convert_single_method_code(const irep_idt &function_id, symbol_table_baset &symbol_table, optionalt< ci_lazy_methods_neededt > needed_lazy_methods, lazy_class_to_declared_symbols_mapt &class_to_declared_symbols)
Convert a method (one whose type is known but whose body hasn't been converted) but don't run typeche...
virtual std::vector< load_extra_methodst > build_extra_entry_points(const optionst &) const
This method should be overloaded to provide alternative approaches for specifying extra entry points.
virtual bool parse()
We set the main class (i.e. class to start the class loading analysis, see java_class_loadert) when w...
const select_pointer_typet & get_pointer_type_selector() const
bool from_expr(const exprt &expr, std::string &code, const namespacet &ns) override
Formats the given expression in a language-specific way.
std::unordered_map< std::string, object_creation_referencet > references
Map used in all calls to functions that deterministically create objects (currently only assign_from_...
virtual void convert_lazy_method(const irep_idt &function_id, symbol_table_baset &symbol_table) override
Promote a lazy-converted method (one whose type is known but whose body hasn't been converted) into a...
void convert_single_method(const irep_idt &function_id, symbol_table_baset &symbol_table, lazy_class_to_declared_symbols_mapt &class_to_declared_symbols)
void add_classpath_entry(const std::string &, message_handlert &)
Appends an entry to the class path, used for loading classes.
void clear_classpath()
Clear all classpath entries.
jar_poolt jar_pool
a cache for jar_filet, by path name
Class representing a filter for class file loading.
std::vector< irep_idt > load_entire_jar(const std::string &jar_path, message_handlert &)
Load all class files from a .jar file.
bool can_load_class(const irep_idt &class_name, message_handlert &)
Checks whether class_name is parseable from the classpath, ignoring class loading limits.
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:155
message_handlert * message_handler
Definition message.h:439
message_handlert & get_message_handler()
Definition message.h:184
mstreamt & warning() const
Definition message.h:404
virtual void set_message_handler(message_handlert &_message_handler)
Definition message.h:179
mstreamt & result() const
Definition message.h:409
static eomt eom
Definition message.h:297
mstreamt & status() const
Definition message.h:414
opt_reft get(const irep_idt &method_id)
An exception that is raised checking whether a class is implicitly generic if a symbol for an outer c...
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition namespace.cpp:49
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The null pointer constant.
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:449
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:113
const irep_idt & get_identifier() const
Definition std_expr.h:142
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
bool has_prefix(const std::string &s, const std::string &prefix)
Definition converter.cpp:13
irep_idt get_create_array_with_type_name()
Returns the symbol name for org.cprover.CProver.createArrayWithType
codet create_array_with_type_body(const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler)
Returns the internal implementation for org.cprover.CProver.createArrayWithType.
Implementation of CProver.createArrayWithType intrinsic.
std::string type2java(const typet &type, const namespacet &ns)
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:47
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, optionalt< ci_lazy_methods_neededt > needed_lazy_methods, java_string_library_preprocesst &string_preprocess, const class_hierarchyt &class_hierarchy, bool threading_support, const optionalt< prefix_filtert > &method_context, bool assert_no_exceptions_thrown)
JAVA Bytecode Language Conversion.
void java_bytecode_instrument_symbol(symbol_table_baset &symbol_table, symbolt &symbol, const bool throw_runtime_exceptions, message_handlert &message_handler)
Instruments the code attached to symbol with runtime exceptions or corresponding assertions.
void java_bytecode_instrument(symbol_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 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.
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.
@ 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)
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_user_specified_clinit_body(const irep_idt &class_id, const json_objectt &static_values_json, symbol_table_baset &symbol_table, optionalt< ci_lazy_methods_neededt > needed_lazy_methods, size_t max_user_array_length, std::unordered_map< std::string, object_creation_referencet > &references, const std::unordered_multimap< irep_idt, symbolt > &class_to_declared_symbols_map)
Create the body of a user_specified_clinit function for a given class, which includes assignments for...
code_blockt get_thread_safe_clinit_wrapper_body(const irep_idt &function_id, symbol_table_baset &symbol_table, const bool nondet_static, const bool replace_clinit, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, message_handlert &message_handler)
Thread safe version of the static initializer.
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:184
const java_class_typet & to_java_class_type(const typet &type)
Definition java_types.h:582
NODISCARD optionalt< std::string > class_name_from_method_name(const std::string &method_name)
Get JVM type name of the class in which method_name is defined.
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.
optionalt< irep_idt > declaring_class(const symbolt &symbol)
Gets the identifier of the class which declared a given symbol.
optionalt< 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:444
json_arrayt & to_json_array(jsont &json)
Definition json.h:426
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.
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:77
bool assert_no_exceptions_thrown
Transform athrow bytecode instructions into assert FALSE followed by assume FALSE.
bool should_lift_clinit_calls
Should we lift clinit calls in function bodies to the top? For example, turning if(x) A....
optionalt< prefix_filtert > method_context
If set, method bodies are only elaborated if they pass the filter.
optionalt< json_objectt > static_values_json
JSON which contains initial values of static fields (right after the static initializer of the class ...
bool assume_inputs_non_null
assume inputs variables to be non-null
size_t max_user_array_length
max size for user code created arrays
std::vector< irep_idt > java_load_classes
list of classes to force load even without reference from the entry point
std::unordered_set< std::string > no_load_classes
List of classes to never load.
std::vector< load_extra_methodst > extra_methods
void set(const optionst &)
Assigns the parameters from given options.
bool has_suffix(const std::string &s, const std::string &suffix)
Definition suffix.h:17
@ 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