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