cprover
Loading...
Searching...
No Matches
java_static_initializers.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Java Static Initializers
4
5Author: Chris Smowton, chris.smowton@diffblue.com
6
7\*******************************************************************/
8
10
13#include "java_object_factory.h"
15#include "java_types.h"
16#include "java_utils.h"
17
19
20#include <util/arith_tools.h>
21#include <util/cprover_prefix.h>
22#include <util/json.h>
23#include <util/std_code.h>
24#include <util/suffix.h>
25#include <util/symbol_table.h>
26
49{
53};
54
56{
57 return java_byte_type();
58}
59
60// Disable linter here to allow a std::string constant, since that holds
61// a length, whereas a cstr would require strlen every time.
62const std::string clinit_wrapper_suffix = ".<clinit_wrapper>"; // NOLINT(*)
63const std::string user_specified_clinit_suffix = ".<user_specified_clinit>"; // NOLINT(*)
64const std::string clinit_function_suffix = ".<clinit>:()V"; // NOLINT(*)
65
73{
74 return id2string(class_name) + clinit_wrapper_suffix;
75}
76
78{
79 return id2string(class_name) + user_specified_clinit_suffix;
80}
81
85bool is_clinit_wrapper_function(const irep_idt &function_id)
86{
87 return has_suffix(id2string(function_id), clinit_wrapper_suffix);
88}
89
93bool is_clinit_function(const irep_idt &function_id)
94{
95 return has_suffix(id2string(function_id), clinit_function_suffix);
96}
97
102{
104}
105
115 symbol_table_baset &symbol_table,
116 const irep_idt &name,
117 const typet &type,
118 const exprt &value,
119 const bool is_thread_local,
120 const bool is_static_lifetime)
121{
122 symbolt new_symbol;
123 new_symbol.name = name;
124 new_symbol.pretty_name = name;
125 new_symbol.base_name = name;
126 new_symbol.type = type;
127 new_symbol.type.set(ID_C_no_nondet_initialization, true);
128 new_symbol.value = value;
129 new_symbol.is_lvalue = true;
130 new_symbol.is_state_var = true;
131 new_symbol.is_static_lifetime = is_static_lifetime;
132 new_symbol.is_thread_local = is_thread_local;
133 new_symbol.mode = ID_java;
134 symbol_table.add(new_symbol);
135 return new_symbol;
136}
137
143{
144 return id2string(class_name) + "::clinit_already_run";
145}
146
151static irep_idt clinit_function_name(const irep_idt &class_name)
152{
153 return id2string(class_name) + clinit_function_suffix;
154}
155
160static irep_idt clinit_state_var_name(const irep_idt &class_name)
161{
162 return id2string(class_name) + CPROVER_PREFIX "clinit_state";
163}
164
170{
171 return id2string(class_name) + CPROVER_PREFIX "clinit_threadlocal_state";
172}
173
178{
179 return id2string(class_name) + CPROVER_PREFIX "clinit_wrapper::init_complete";
180}
181
191gen_clinit_assign(const exprt &expr, const clinit_statest state)
192{
193 mp_integer initv(static_cast<int>(state));
195 return code_frontend_assignt(expr, init_s);
196}
197
206static equal_exprt
207gen_clinit_eqexpr(const exprt &expr, const clinit_statest state)
208{
209 mp_integer initv(static_cast<int>(state));
211 return equal_exprt(expr, init_s);
212}
213
232 symbol_table_baset &symbol_table,
233 const irep_idt &class_name,
235 const bool nondet_static,
236 const bool replace_clinit,
237 const java_object_factory_parameterst &object_factory_parameters,
238 const select_pointer_typet &pointer_type_selector,
239 message_handlert &message_handler)
240{
241 const symbolt &class_symbol = symbol_table.lookup_ref(class_name);
242 for(const auto &base : to_class_type(class_symbol.type).bases())
243 {
244 const auto base_name = base.type().get_identifier();
246 if(const auto base_init_func = symbol_table.lookup(base_init_routine))
247 init_body.add(code_function_callt{base_init_func->symbol_expr()});
248 }
249
251 ? user_specified_clinit_name(class_name)
252 : clinit_function_name(class_name);
253 if(const auto clinit_func = symbol_table.lookup(clinit_name))
254 init_body.add(code_function_callt{clinit_func->symbol_expr()});
255
256 // If nondet-static option is given, add a standard nondet initialization for
257 // each non-final static field of this class. Note this is the same invocation
258 // used in get_stub_initializer_body and java_static_lifetime_init.
259 if(nondet_static)
260 {
261 java_object_factory_parameterst parameters = object_factory_parameters;
262 parameters.function_id = clinit_wrapper_name(class_name);
263
264 std::vector<irep_idt> nondet_ids;
265 std::for_each(
266 symbol_table.symbols.begin(),
267 symbol_table.symbols.end(),
268 [&](const std::pair<irep_idt, symbolt> &symbol) {
269 if(
270 declaring_class(symbol.second) == class_name &&
271 symbol.second.is_static_lifetime &&
272 !symbol.second.type.get_bool(ID_C_constant))
273 {
274 nondet_ids.push_back(symbol.first);
275 }
276 });
277
278 for(const auto &id : nondet_ids)
279 {
281 symbol_table.lookup_ref(id).symbol_expr();
282
283 parameters.min_null_tree_depth =
285 ? std::max(size_t(1), object_factory_parameters.min_null_tree_depth)
286 : object_factory_parameters.min_null_tree_depth;
287
290 init_body,
291 symbol_table,
293 false,
295 parameters,
296 pointer_type_selector,
298 message_handler);
299 }
300 }
301}
302
309 const irep_idt &class_name, const symbol_tablet &symbol_table)
310{
311 if(symbol_table.has_symbol(clinit_function_name(class_name)))
312 return true;
313
314 const class_typet &class_type =
315 to_class_type(symbol_table.lookup_ref(class_name).type);
316
317 for(const class_typet::baset &base : class_type.bases())
318 {
319 if(symbol_table.has_symbol(
320 clinit_wrapper_name(base.type().get_identifier())))
321 {
322 return true;
323 }
324 }
325
326 return false;
327}
328
330 const irep_idt &class_name,
331 const irep_idt &function_name,
334 symbol_tablet &symbol_table,
335 synthetic_methods_mapt &synthetic_methods)
336{
338 const java_method_typet function_type({}, java_void_type());
339 function_symbol.name = function_name;
340 function_symbol.pretty_name = function_symbol.name;
342 function_symbol.type = function_type;
343 // This provides a back-link from a method to its associated class, as is done
344 // for java_bytecode_convert_methodt::convert.
347 bool failed = symbol_table.add(function_symbol);
348 INVARIANT(!failed, id2string(function_base_name) + " symbol should be fresh");
349
350 auto insert_result =
351 synthetic_methods.emplace(function_symbol.name, synthetic_method_type);
352 INVARIANT(
353 insert_result.second,
354 "synthetic methods map should not already contain entry for " +
356}
357
358// Create symbol for the "clinit_wrapper"
360 const irep_idt &class_name,
361 symbol_tablet &symbol_table,
362 synthetic_methods_mapt &synthetic_methods)
363{
365 class_name,
366 clinit_wrapper_name(class_name),
367 "clinit_wrapper",
369 symbol_table,
370 synthetic_methods);
371}
372
373// Create symbol for the "user_specified_clinit"
375 const irep_idt &class_name,
376 symbol_tablet &symbol_table,
377 synthetic_methods_mapt &synthetic_methods)
378{
380 class_name,
381 user_specified_clinit_name(class_name),
382 "user_specified_clinit",
384 symbol_table,
385 synthetic_methods);
386}
387
399 const irep_idt &class_name,
400 symbol_tablet &symbol_table,
401 synthetic_methods_mapt &synthetic_methods,
402 const bool thread_safe)
403{
404 if(thread_safe)
405 {
407 static_cast<int>(clinit_statest::NOT_INIT), clinit_states_type());
408
409 // Create two global static synthetic "fields" for the class "id"
410 // these two variables hold the state of the class initialization algorithm
411 // across calls to the clinit_wrapper
413 symbol_table,
414 clinit_state_var_name(class_name),
417 false,
418 true);
419
421 symbol_table,
425 true,
426 true);
427 }
428 else
429 {
432
434 symbol_table,
436 bool_typet(),
437 false_exprt(),
438 false,
439 true);
440 }
441
443 class_name, symbol_table, synthetic_methods);
444}
445
524 const irep_idt &function_id,
525 symbol_table_baset &symbol_table,
526 const bool nondet_static,
527 const bool replace_clinit,
528 const java_object_factory_parameterst &object_factory_parameters,
529 const select_pointer_typet &pointer_type_selector,
530 message_handlert &message_handler)
531{
532 const symbolt &wrapper_method_symbol = symbol_table.lookup_ref(function_id);
533 const auto class_name = declaring_class(wrapper_method_symbol);
534 INVARIANT(class_name, "Wrapper function should have an owning class.");
535
537 symbol_table.lookup_ref(clinit_state_var_name(*class_name));
539 symbol_table.lookup_ref(clinit_thread_local_state_var_name(*class_name));
540
541 // Create a function-local variable "init_complete". This variable is used to
542 // avoid inspecting the global state (clinit_state_sym) outside of
543 // the critical-section.
545 symbol_table,
547 bool_typet(),
548 nil_exprt(),
549 true,
550 false);
551
553 codet atomic_begin(ID_atomic_begin);
554 codet atomic_end(ID_atomic_end);
555
556#if 0
557 // This code defines source locations for every codet generated below for
558 // the static initializer wrapper. Enable this for debugging the symex going
559 // through the clinit_wrapper.
560 //
561 // java::C.<clinit_wrapper>()
562 // You will additionally need to associate the `location` with the
563 // `function_body` and then manually set lines of code for each of the
564 // statements of the function, using something along the lines of:
565 // `mycodet.then_case().add_source_location().set_line(17);`/
566
567 source_locationt &location = function_body.add_source_location();
568 location.set_file ("<generated>");
569 location.set_line ("<generated>");
571 std::string comment =
572 "Automatically generated function. States are:\n"
573 " 0 = class not initialized, init val of clinit_state/clinit_local_state\n"
574 " 1 = class initialization in progress, by this or another thread\n"
575 " 2 = initialization finished with success, by this or another thread\n";
576 static_assert((int) clinit_statest::NOT_INIT==0, "Check commment above");
577 static_assert((int) clinit_statest::IN_PROGRESS==1, "Check comment above");
578 static_assert((int) clinit_statest::INIT_COMPLETE==2, "Check comment above");
579#endif
580
581 // bool init_complete;
582 {
583 code_declt decl(init_complete.symbol_expr());
584 function_body.add(decl);
585 }
586
587 // if(C::__CPROVER_PREFIX_clinit_thread_local_state == INIT_COMPLETE) return;
588 {
591 clinit_thread_local_state_sym.symbol_expr(),
594 function_body.add(std::move(conditional));
595 }
596
597 // C::__CPROVER_PREFIX_clinit_thread_local_state = INIT_COMPLETE;
598 {
600 clinit_thread_local_state_sym.symbol_expr(),
602 function_body.add(assign);
603 }
604
605 // ATOMIC_BEGIN
606 {
607 function_body.add(atomic_begin);
608 }
609
610 // Assume: clinit_state_sym != IN_PROGRESS
611 {
612 exprt assumption = gen_clinit_eqexpr(
614 assumption = not_exprt(assumption);
615 code_assumet assume(assumption);
616 function_body.add(assume);
617 }
618
619 // If(C::__CPROVER_PREFIX_clinit_state == NOT_INIT)
620 // {
621 // C::__CPROVER_PREFIX_clinit_state = IN_PROGRESS;
622 // init_complete = false;
623 // }
624 // else If(C::__CPROVER_PREFIX_clinit_state == INIT_COMPLETE)
625 // {
626 // init_complete = true;
627 // }
628 {
633 {code_frontend_assignt(init_complete.symbol_expr(), true_exprt())}));
634
642 std::move(init_conditional));
643
644 function_body.add(std::move(not_init_conditional));
645 }
646
647 // ATOMIC_END
648 {
649 function_body.add(atomic_end);
650 }
651
652 // if(init_complete) return;
653 {
655 init_complete.symbol_expr(), code_frontend_returnt());
656 function_body.add(std::move(conditional));
657 }
658
659 // Initialize the super-class C' and
660 // the implemented interfaces l_1 ... l_n.
661 // see JVMS p.359 step 7, for the exact definition of
662 // the sequence l_1 to l_n.
663 // This is achieved by iterating through the base types and
664 // adding recursive calls to the clinit_wrapper()
665 //
666 // java::C'.<clinit_wrapper>();
667 // java::I1.<clinit_wrapper>();
668 // java::I2.<clinit_wrapper>();
669 // // ...
670 // java::In.<clinit_wrapper>();
671 //
672 // java::C.<clinit>(); // or nondet-initialization of all static
673 // // variables of C if nondet-static is true
674 //
675 {
678 symbol_table,
679 *class_name,
680 init_body,
683 object_factory_parameters,
684 pointer_type_selector,
685 message_handler);
686 function_body.append(init_body);
687 }
688
689 // ATOMIC_START
690 // C::__CPROVER_PREFIX_clinit_state = INIT_COMPLETE;
691 // ATOMIC_END
692 // return;
693 {
694 // synchronization prologue
695 function_body.add(atomic_begin);
696 function_body.add(
699 function_body.add(atomic_end);
701 }
702
703 return function_body;
704}
705
722 const irep_idt &function_id,
723 symbol_table_baset &symbol_table,
724 const bool nondet_static,
725 const bool replace_clinit,
726 const java_object_factory_parameterst &object_factory_parameters,
727 const select_pointer_typet &pointer_type_selector,
728 message_handlert &message_handler)
729{
730 // Assume that class C extends class C' and implements interfaces
731 // I1, ..., In. We now create the following function (possibly recursively
732 // creating the clinit_wrapper functions for C' and I1, ..., In):
733 //
734 // java::C.<clinit_wrapper>()
735 // {
736 // if (!java::C::clinit_already_run)
737 // {
738 // java::C::clinit_already_run = true; // before recursive calls!
739 //
740 // java::C'.<clinit_wrapper>();
741 // java::I1.<clinit_wrapper>();
742 // java::I2.<clinit_wrapper>();
743 // // ...
744 // java::In.<clinit_wrapper>();
745 //
746 // java::C.<clinit>(); // or nondet-initialization of all static
747 // // variables of C if nondet-static is true
748 // }
749 // }
750 const symbolt &wrapper_method_symbol = symbol_table.lookup_ref(function_id);
751 const auto class_name = declaring_class(wrapper_method_symbol);
752 INVARIANT(class_name, "Wrapper function should have an owning class.");
753
755 symbol_table.lookup_ref(clinit_already_run_variable_name(*class_name));
756
758 already_run_symbol.symbol_expr(),
759 false_exprt());
760
761 // add the "already-run = false" statement
763 already_run_symbol.symbol_expr(), true_exprt());
765
767 symbol_table,
768 *class_name,
769 init_body,
772 object_factory_parameters,
773 pointer_type_selector,
774 message_handler);
775
776 // the entire body of the function is an if-then-else
777 return code_ifthenelset(std::move(check_already_run), std::move(init_body));
778}
779
781std::unordered_multimap<irep_idt, symbolt>
783{
784 std::unordered_multimap<irep_idt, symbolt> result;
785 for(const auto &symbol_pair : symbol_table)
786 {
787 const symbolt &symbol = symbol_pair.second;
789 result.emplace(*declaring, symbol);
790 }
791 return result;
792}
793
795 const irep_idt &class_id,
796 const json_objectt &static_values_json,
797 symbol_table_baset &symbol_table,
798 optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
799 size_t max_user_array_length,
800 std::unordered_map<std::string, object_creation_referencet> &references,
801 const std::unordered_multimap<irep_idt, symbolt>
803{
805 const auto clinit_func = symbol_table.lookup(real_clinit_name);
806 if(clinit_func == nullptr)
807 {
808 // Case where the real clinit doesn't appear in the symbol table, even
809 // though their is user specifed one. This may occur when some class
810 // substitution happened after compilation.
811 return code_blockt{};
812 }
813 const auto class_entry =
814 static_values_json.find(id2string(strip_java_namespace_prefix(class_id)));
815 if(class_entry != static_values_json.end() && class_entry->second.is_object())
816 {
817 const auto &class_json_object = to_json_object(class_entry->second);
818 std::map<symbol_exprt, jsont> static_field_values;
819 for(const auto &symbol_pair :
821 {
822 const symbolt &symbol = symbol_pair.second;
823 if(symbol.is_static_lifetime)
824 {
826 const auto &static_field_entry =
829 {
830 static_field_values.insert(
832 }
833 }
834 }
836 for(const auto &value_pair : static_field_values)
837 {
839 value_pair.first,
840 value_pair.second,
842 symbol_table,
843 needed_lazy_methods,
844 max_user_array_length,
845 references));
846 }
848 [&](const std::string &reference_id) -> object_creation_referencet & {
849 auto it = references.find(reference_id);
850 INVARIANT(it != references.end(), "reference id must be present in map");
851 return it->second;
852 };
853 code_blockt body;
854 for(const auto &code_with_ref : code_with_references.list)
856 return body;
857 }
858 return code_blockt{{code_function_callt{clinit_func->symbol_expr()}}};
859}
860
878 symbol_tablet &symbol_table,
879 synthetic_methods_mapt &synthetic_methods,
880 const bool thread_safe,
881 const bool is_user_clinit_needed)
882{
883 // Top-sort the class hierarchy, such that we visit parents before children,
884 // and can so identify parents that need static initialisation by whether we
885 // have made them a clinit_wrapper method.
887 class_graph.populate(symbol_table);
888 std::list<class_hierarchy_grapht::node_indext> topsorted_nodes =
889 class_graph.topsort();
890
891 for(const auto node : topsorted_nodes)
892 {
893 const irep_idt &class_identifier = class_graph[node].class_identifier;
894 if(needs_clinit_wrapper(class_identifier, symbol_table))
895 {
897 class_identifier, symbol_table, synthetic_methods, thread_safe);
899 {
901 class_identifier, symbol_table, synthetic_methods);
902 }
903 }
904 }
905}
906
910template<class itertype>
912{
913 PRECONDITION(in != end);
914 auto initial_key = in->first;
915 while(in != end && in->first == initial_key)
916 ++in;
917 return in;
918}
919
929 symbol_tablet &symbol_table,
930 const std::unordered_set<irep_idt> &stub_globals_set,
931 synthetic_methods_mapt &synthetic_methods)
932{
933 // Populate map from class id -> stub globals:
935 {
936 const symbolt &global_symbol = symbol_table.lookup_ref(stub_global);
937 if(global_symbol.value.is_nil())
938 {
939 // This symbol is already nondet-initialised during __CPROVER_initialize
940 // (generated in java_static_lifetime_init). In future this will only
941 // be the case for primitive-typed fields, but for now reference-typed
942 // fields can also be treated this way in the exceptional case that they
943 // belong to a non-stub class. Skip the field, as it does not need a
944 // synthetic static initializer.
945 continue;
946 }
947
948 const auto class_id = declaring_class(global_symbol);
949 INVARIANT(class_id, "Static field should have a defining class.");
950 stub_globals_by_class.insert({*class_id, stub_global});
951 }
952
953 // For each distinct class that has stub globals, create a clinit symbol:
954
955 for(auto it = stub_globals_by_class.begin(),
957 it != itend;
958 it = advance_to_next_key(it, itend))
959 {
961
962 INVARIANT(
963 to_java_class_type(symbol_table.lookup_ref(it->first).type).get_is_stub(),
964 "only stub classes should be given synthetic static initialisers");
965 INVARIANT(
966 !symbol_table.has_symbol(static_init_name),
967 "a class cannot be both incomplete, and so have stub static fields, and "
968 "also define a static initializer");
969
971
975 static_init_symbol.base_name = "clinit():V";
978 // This provides a back-link from a method to its associated class, as is
979 // done for java_bytecode_convert_methodt::convert.
981
982 bool failed = symbol_table.add(static_init_symbol);
983 INVARIANT(!failed, "symbol should not already exist");
984
985 auto insert_result = synthetic_methods.emplace(
988 INVARIANT(
989 insert_result.second,
990 "synthetic methods map should not already contain entry for "
991 "stub static initializer");
992 }
993}
994
1010 const irep_idt &function_id,
1011 symbol_table_baset &symbol_table,
1012 const java_object_factory_parameterst &object_factory_parameters,
1013 const select_pointer_typet &pointer_type_selector,
1014 message_handlert &message_handler)
1015{
1016 const symbolt &stub_initializer_symbol = symbol_table.lookup_ref(function_id);
1017 const auto class_id = declaring_class(stub_initializer_symbol);
1018 INVARIANT(
1019 class_id, "Synthetic static initializer should have an owning class.");
1021
1022 // Add a standard nondet initialisation for each global declared on this
1023 // class. Note this is the same invocation used in
1024 // java_static_lifetime_init.
1025
1027 INVARIANT(
1028 !class_globals.empty(),
1029 "class with synthetic clinit should have at least one global to init");
1030
1031 java_object_factory_parameterst parameters = object_factory_parameters;
1032 parameters.function_id = function_id;
1033
1034 for(const auto &pair : class_globals)
1035 {
1037 symbol_table.lookup_ref(pair.second).symbol_expr();
1038
1039 parameters.min_null_tree_depth =
1041 ? object_factory_parameters.min_null_tree_depth + 1
1042 : object_factory_parameters.min_null_tree_depth;
1043
1044 source_locationt location;
1045 location.set_function(function_id);
1049 symbol_table,
1050 location,
1051 false,
1053 parameters,
1054 pointer_type_selector,
1056 message_handler);
1057 }
1058
1059 return static_init_body;
1060}
@ DYNAMIC
Allocate dynamic objects (using ALLOCATE)
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
code_with_references_listt assign_from_json(const exprt &expr, const jsont &json, const irep_idt &function_id, 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)
Given an expression expr representing a Java object or primitive and a JSON representation json of th...
Context-insensitive lazy methods container.
Class Hierarchy.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
The Boolean type.
Definition std_types.h:36
Class hierarchy, represented using grapht and therefore suitable for use with generic graph algorithm...
Class type.
Definition std_types.h:325
An assumption, which must hold in subsequent code.
Definition std_code.h:217
A codet representing sequential composition of program statements.
Definition std_code.h:130
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
Definition std_code.cpp:89
A codet representing the declaration of a local variable.
A codet representing an assignment in the program.
Definition std_code.h:24
codet representation of a "return from a function" statement.
Definition std_code.h:893
codet representation of a function call statement.
codet representation of an if-then-else statement.
Definition std_code.h:460
Wrapper around a list of shared pointer to code_with_referencest objects, which provides a nicer inte...
std::function< const object_creation_referencet &(const std::string &)> reference_substitutiont
Data structure for representing an arbitrary statement in a program.
A constant literal expression.
Definition std_expr.h:2807
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
Equality.
Definition std_expr.h:1225
Base class for all expressions.
Definition expr.h:54
The Boolean constant false.
Definition std_expr.h:2865
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:420
bool get_is_stub() const
Definition java_types.h:398
iterator find(const std::string &key)
Definition json.h:356
iterator end()
Definition json.h:386
The NIL expression.
Definition std_expr.h:2874
Boolean negation.
Definition std_expr.h:2181
void set_file(const irep_idt &file)
void set_line(const irep_idt &line)
void set_function(const irep_idt &function)
Base class or struct that a class or struct inherits from.
Definition std_types.h:252
const basest & bases() const
Get the collection of base classes/structs.
Definition std_types.h:262
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
The symbol table base class interface.
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.
The symbol table.
Symbol table entry.
Definition symbol.h:28
bool is_static_lifetime
Definition symbol.h:65
bool is_thread_local
Definition symbol.h:65
bool is_state_var
Definition symbol.h:62
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition symbol.cpp:121
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
irep_idt irep_idt base_name
Name of module the symbol belongs to.
Definition symbol.h:46
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 Boolean constant true.
Definition std_expr.h:2856
The type of an expression, extends irept.
Definition type.h:29
#define CPROVER_PREFIX
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
void gen_nondet_init(const exprt &expr, code_blockt &init_code, symbol_table_baset &symbol_table, const source_locationt &loc, bool skip_classid, lifetimet lifetime, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, update_in_placet update_in_place, message_handlert &log)
Initializes a primitive-typed or reference-typed object tree rooted at expr, allocating child objects...
This module is responsible for the synthesis of code (in the form of a sequence of codet statements) ...
static code_frontend_assignt gen_clinit_assign(const exprt &expr, const clinit_statest state)
Generates a code_frontend_assignt for clinit_statest /param expr: expression to be used as the LHS of...
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...
clinit_statest
The three states in which a <clinit> method for a class can be before, after, and during static class...
static void create_clinit_wrapper_symbols(const irep_idt &class_name, symbol_tablet &symbol_table, synthetic_methods_mapt &synthetic_methods, const bool thread_safe)
Creates a static initializer wrapper symbol for the given class, along with a global boolean that tra...
static void create_function_symbol(const irep_idt &class_name, const irep_idt &function_name, const irep_idt &function_base_name, const synthetic_method_typet &synthetic_method_type, symbol_tablet &symbol_table, synthetic_methods_mapt &synthetic_methods)
static typet clinit_states_type()
static irep_idt clinit_state_var_name(const irep_idt &class_name)
Get name of the static-initialization-state global variable for a given class.
const std::string clinit_function_suffix
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.
static equal_exprt gen_clinit_eqexpr(const exprt &expr, const clinit_statest state)
Generates an equal_exprt for clinit_statest /param expr: expression to be used as the LHS of generate...
static void clinit_wrapper_do_recursive_calls(symbol_table_baset &symbol_table, const irep_idt &class_name, code_blockt &init_body, 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)
Generates codet that iterates through the base types of the class specified by class_name,...
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...
bool is_user_specified_clinit_function(const irep_idt &function_id)
Check if function_id is a user-specified clinit.
static bool needs_clinit_wrapper(const irep_idt &class_name, const symbol_tablet &symbol_table)
Checks whether a static initializer wrapper is needed for a given class, i.e.
irep_idt user_specified_clinit_name(const irep_idt &class_name)
const std::string user_specified_clinit_suffix
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.
static irep_idt clinit_thread_local_state_var_name(const irep_idt &class_name)
Get name of the static-initialization-state local state variable for a given class.
static itertype advance_to_next_key(itertype in, itertype end)
Advance map iterator to next distinct key.
bool is_clinit_wrapper_function(const irep_idt &function_id)
Check if function_id is a clinit wrapper.
static void create_user_specified_clinit_function_symbol(const irep_idt &class_name, symbol_tablet &symbol_table, synthetic_methods_mapt &synthetic_methods)
irep_idt clinit_wrapper_name(const irep_idt &class_name)
Get the Java static initializer wrapper name for a given class (the wrapper checks if static initiali...
static void create_clinit_wrapper_function_symbol(const irep_idt &class_name, symbol_tablet &symbol_table, synthetic_methods_mapt &synthetic_methods)
static irep_idt clinit_function_name(const irep_idt &class_name)
Get name of the real static initializer for a given class.
static irep_idt clinit_already_run_variable_name(const irep_idt &class_name)
Get name of the static-initialization-already-done global variable for a given class.
bool is_clinit_function(const irep_idt &function_id)
Check if function_id is a clinit.
static irep_idt clinit_local_init_complete_var_name(const irep_idt &class_name)
Get name of the static-initialization local variable for a given class.
static symbolt add_new_variable_symbol(symbol_table_baset &symbol_table, const irep_idt &name, const typet &type, const exprt &value, const bool is_thread_local, const bool is_static_lifetime)
Add a new symbol to the symbol table.
const std::string clinit_wrapper_suffix
empty_typet java_void_type()
signedbv_typet java_byte_type()
const java_class_typet & to_java_class_type(const typet &type)
Definition java_types.h:582
bool is_non_null_library_global(const irep_idt &symbolid)
Check if a symbol is a well-known non-null global.
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.
irep_idt strip_java_namespace_prefix(const irep_idt &to_strip)
Strip java:: prefix from given identifier.
json_objectt & to_json_object(jsont &json)
Definition json.h:444
static void nondet_static(const namespacet &ns, goto_functionst &goto_functions, const irep_idt &fct_name)
Nondeterministically initializes global scope variables in a goto-function.
static std::string comment(const rw_set_baset::entryt &entry, bool write)
ranget< typename multimapt::const_iterator > equal_range(const multimapt &multimap, const typename multimapt::key_type &key)
Utility function to make equal_range method of multimap easier to use by returning a ranget object.
Definition range.h:541
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
const class_typet & to_class_type(const typet &type)
Cast a typet to a class_typet.
Definition std_types.h:381
Information to store when several references point to the same Java object.
irep_idt function_id
Function id, used as a prefix for identifiers of temporaries.
size_t min_null_tree_depth
To force a certain depth of non-null objects.
bool has_suffix(const std::string &s, const std::string &suffix)
Definition suffix.h:17
Author: Diffblue Ltd.
static bool failed(bool error_indicator)
std::unordered_map< irep_idt, synthetic_method_typet > synthetic_methods_mapt
Maps method names on to a synthetic method kind.
synthetic_method_typet
Synthetic method kinds.
@ 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.