cprover
java_static_initializers.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Java Static Initializers
4 
5 Author: Chris Smowton, chris.smowton@diffblue.com
6 
7 \*******************************************************************/
8 
10 #include "java_object_factory.h"
11 #include "java_utils.h"
13 #include <util/std_types.h>
14 #include <util/std_expr.h>
15 #include <util/std_code.h>
16 #include <util/suffix.h>
17 #include <util/arith_tools.h>
18 
40 enum class clinit_statest
41 {
42  NOT_INIT,
45 };
46 
48 
49 // Disable linter here to allow a std::string constant, since that holds
50 // a length, whereas a cstr would require strlen every time.
51 const std::string clinit_wrapper_suffix = "::clinit_wrapper"; // NOLINT(*)
52 const std::string clinit_function_suffix = ".<clinit>:()V"; // NOLINT(*)
53 
61 {
62  return id2string(class_name) + clinit_wrapper_suffix;
63 }
64 
68 bool is_clinit_wrapper_function(const irep_idt &function_id)
69 {
70  return has_suffix(id2string(function_id), clinit_wrapper_suffix);
71 }
72 
82  symbol_table_baset &symbol_table,
83  const irep_idt &name,
84  const typet &type,
85  const exprt &value,
86  const bool is_thread_local,
87  const bool is_static_lifetime)
88 {
89  symbolt new_symbol;
90  new_symbol.name = name;
91  new_symbol.pretty_name = name;
92  new_symbol.base_name = name;
93  new_symbol.type = type;
94  new_symbol.type.set(ID_C_no_nondet_initialization, true);
95  new_symbol.value = value;
96  new_symbol.is_lvalue = true;
97  new_symbol.is_state_var = true;
98  new_symbol.is_static_lifetime = is_static_lifetime;
99  new_symbol.is_thread_local = is_thread_local;
100  new_symbol.mode = ID_java;
101  symbol_table.add(new_symbol);
102  return new_symbol;
103 }
104 
110 {
111  return id2string(class_name) + "::clinit_already_run";
112 }
113 
118 static irep_idt clinit_function_name(const irep_idt &class_name)
119 {
120  return id2string(class_name) + clinit_function_suffix;
121 }
122 
127 static irep_idt clinit_state_var_name(const irep_idt &class_name)
128 {
129  return id2string(class_name) + CPROVER_PREFIX "clinit_state";
130 }
131 
137 {
138  return id2string(class_name) + CPROVER_PREFIX "clinit_threadlocal_state";
139 }
140 
145 {
146  return id2string(class_name) + CPROVER_PREFIX "clinit_wrapper::init_complete";
147 }
148 
157 static code_assignt
158 gen_clinit_assign(const exprt &expr, const clinit_statest state)
159 {
160  mp_integer initv(static_cast<int>(state));
162  return code_assignt(expr, init_s);
163 }
164 
173 static equal_exprt
174 gen_clinit_eqexpr(const exprt &expr, const clinit_statest state)
175 {
176  mp_integer initv(static_cast<int>(state));
178  return equal_exprt(expr, init_s);
179 }
180 
196  symbol_table_baset &symbol_table,
197  const irep_idt &class_name,
198  code_blockt &init_body,
199  const bool nondet_static,
200  const java_object_factory_parameterst &object_factory_parameters,
201  const select_pointer_typet &pointer_type_selector)
202 {
203  const symbolt &class_symbol = symbol_table.lookup_ref(class_name);
204  for(const auto &base : to_class_type(class_symbol.type).bases())
205  {
206  const auto base_name = base.type().get_identifier();
207  irep_idt base_init_routine = clinit_wrapper_name(base_name);
208  auto findit = symbol_table.symbols.find(base_init_routine);
209  if(findit == symbol_table.symbols.end())
210  continue;
211 
212  const code_function_callt call_base(findit->second.symbol_expr());
213  init_body.add(call_base);
214  }
215 
216  const irep_idt &real_clinit_name = clinit_function_name(class_name);
217  auto find_sym_it = symbol_table.symbols.find(real_clinit_name);
218  if(find_sym_it != symbol_table.symbols.end())
219  {
220  const code_function_callt call_real_init(find_sym_it->second.symbol_expr());
221  init_body.add(call_real_init);
222  }
223 
224  // If nondet-static option is given, add a standard nondet initialization for
225  // each non-final static field of this class. Note this is the same invocation
226  // used in get_stub_initializer_body and java_static_lifetime_init.
227  if(nondet_static)
228  {
229  java_object_factory_parameterst parameters = object_factory_parameters;
230  parameters.function_id = clinit_wrapper_name(class_name);
231 
232  std::vector<irep_idt> nondet_ids;
233  std::for_each(
234  symbol_table.symbols.begin(),
235  symbol_table.symbols.end(),
236  [&](const std::pair<irep_idt, symbolt> &symbol) {
237  if(
238  symbol.second.type.get(ID_C_class) == class_name &&
239  symbol.second.is_static_lifetime &&
240  !symbol.second.type.get_bool(ID_C_constant))
241  {
242  nondet_ids.push_back(symbol.first);
243  }
244  });
245 
246  for(const auto &id : nondet_ids)
247  {
248  const symbol_exprt new_global_symbol =
249  symbol_table.lookup_ref(id).symbol_expr();
250 
251  parameters.min_null_tree_depth =
253  ? std::max(size_t(1), object_factory_parameters.min_null_tree_depth)
254  : object_factory_parameters.min_null_tree_depth;
255 
257  new_global_symbol,
258  init_body,
259  symbol_table,
261  false,
263  parameters,
264  pointer_type_selector,
266  }
267  }
268 }
269 
276  const irep_idt &class_name, const symbol_tablet &symbol_table)
277 {
278  if(symbol_table.has_symbol(clinit_function_name(class_name)))
279  return true;
280 
281  const class_typet &class_type =
282  to_class_type(symbol_table.lookup_ref(class_name).type);
283 
284  for(const class_typet::baset &base : class_type.bases())
285  {
286  if(symbol_table.has_symbol(
287  clinit_wrapper_name(base.type().get_identifier())))
288  {
289  return true;
290  }
291  }
292 
293  return false;
294 }
295 
307  const irep_idt &class_name,
308  symbol_tablet &symbol_table,
309  synthetic_methods_mapt &synthetic_methods,
310  const bool thread_safe)
311 {
312  if(thread_safe)
313  {
314  exprt not_init_value = from_integer(
315  static_cast<int>(clinit_statest::NOT_INIT), clinit_states_type);
316 
317  // Create two global static synthetic "fields" for the class "id"
318  // these two variables hold the state of the class initialization algorithm
319  // across calls to the clinit_wrapper
321  symbol_table,
322  clinit_state_var_name(class_name),
324  not_init_value,
325  false,
326  true);
327 
329  symbol_table,
332  not_init_value,
333  true,
334  true);
335  }
336  else
337  {
338  const irep_idt &already_run_name =
340 
342  symbol_table,
343  already_run_name,
344  bool_typet(),
345  false_exprt(),
346  false,
347  true);
348  }
349 
350  // Create symbol for the "clinit_wrapper"
351  symbolt wrapper_method_symbol;
352  const java_method_typet wrapper_method_type({}, void_typet());
353  wrapper_method_symbol.name = clinit_wrapper_name(class_name);
354  wrapper_method_symbol.pretty_name = wrapper_method_symbol.name;
355  wrapper_method_symbol.base_name = "clinit_wrapper";
356  wrapper_method_symbol.type = wrapper_method_type;
357  // Note this use of a type-comment to provide a back-link from a method
358  // to its associated class is the same one used in
359  // java_bytecode_convert_methodt::convert
360  wrapper_method_symbol.type.set(ID_C_class, class_name);
361  wrapper_method_symbol.mode = ID_java;
362  bool failed = symbol_table.add(wrapper_method_symbol);
363  INVARIANT(!failed, "clinit-wrapper symbol should be fresh");
364 
365  auto insert_result = synthetic_methods.emplace(
366  wrapper_method_symbol.name,
368  INVARIANT(
369  insert_result.second,
370  "synthetic methods map should not already contain entry for "
371  "clinit wrapper");
372 }
373 
449  const irep_idt &function_id,
450  symbol_table_baset &symbol_table,
451  const bool nondet_static,
452  const java_object_factory_parameterst &object_factory_parameters,
453  const select_pointer_typet &pointer_type_selector)
454 {
455  const symbolt &wrapper_method_symbol = symbol_table.lookup_ref(function_id);
456  irep_idt class_name = wrapper_method_symbol.type.get(ID_C_class);
457  INVARIANT(
458  !class_name.empty(), "wrapper function should be annotated with its class");
459 
460  const symbolt &clinit_state_sym =
461  symbol_table.lookup_ref(clinit_state_var_name(class_name));
462  const symbolt &clinit_thread_local_state_sym =
463  symbol_table.lookup_ref(clinit_thread_local_state_var_name(class_name));
464 
465  // Create a function-local variable "init_complete". This variable is used to
466  // avoid inspecting the global state (clinit_state_sym) outside of
467  // the critical-section.
468  const symbolt &init_complete = add_new_variable_symbol(
469  symbol_table,
471  bool_typet(),
472  nil_exprt(),
473  true,
474  false);
475 
476  code_blockt function_body;
477  codet atomic_begin(ID_atomic_begin);
478  codet atomic_end(ID_atomic_end);
479 
480 #if 0
481  // This code defines source locations for every codet generated below for
482  // the static initializer wrapper. Enable this for debugging the symex going
483  // through the clinit_wrapper.
484  //
485  // java::C::clinit_wrapper()
486  // You will additionally need to associate the `location` with the
487  // `function_body` and then manually set lines of code for each of the
488  // statements of the function, using something along the lines of:
489  // `mycodet.then_case().add_source_location().set_line(17);`/
490 
491  source_locationt &location = function_body.add_source_location();
492  location.set_file ("<generated>");
493  location.set_line ("<generated>");
495  std::string comment =
496  "Automatically generated function. States are:\n"
497  " 0 = class not initialized, init val of clinit_state/clinit_local_state\n"
498  " 1 = class initialization in progress, by this or another thread\n"
499  " 2 = initialization finished with success, by this or another thread\n";
500  static_assert((int) clinit_statest::NOT_INIT==0, "Check commment above");
501  static_assert((int) clinit_statest::IN_PROGRESS==1, "Check comment above");
502  static_assert((int) clinit_statest::INIT_COMPLETE==2, "Check comment above");
503 #endif
504 
505  // bool init_complete;
506  {
507  code_declt decl(init_complete.symbol_expr());
508  function_body.add(decl);
509  }
510 
511  // if(C::__CPROVER_PREFIX_clinit_thread_local_state == INIT_COMPLETE) return;
512  {
513  code_ifthenelset conditional(
515  clinit_thread_local_state_sym.symbol_expr(),
517  code_returnt());
518  function_body.add(std::move(conditional));
519  }
520 
521  // C::__CPROVER_PREFIX_clinit_thread_local_state = INIT_COMPLETE;
522  {
524  clinit_thread_local_state_sym.symbol_expr(),
526  function_body.add(assign);
527  }
528 
529  // ATOMIC_BEGIN
530  {
531  function_body.add(atomic_begin);
532  }
533 
534  // Assume: clinit_state_sym != IN_PROGRESS
535  {
536  exprt assumption = gen_clinit_eqexpr(
537  clinit_state_sym.symbol_expr(), clinit_statest::IN_PROGRESS);
538  assumption = not_exprt(assumption);
539  code_assumet assume(assumption);
540  function_body.add(assume);
541  }
542 
543  // If(C::__CPROVER_PREFIX_clinit_state == NOT_INIT)
544  // {
545  // C::__CPROVER_PREFIX_clinit_state = IN_PROGRESS;
546  // init_complete = false;
547  // }
548  // else If(C::__CPROVER_PREFIX_clinit_state == INIT_COMPLETE)
549  // {
550  // init_complete = true;
551  // }
552  {
553  code_ifthenelset init_conditional(
555  clinit_state_sym.symbol_expr(), clinit_statest::INIT_COMPLETE),
556  code_blockt({code_assignt(init_complete.symbol_expr(), true_exprt())}));
557 
558  code_ifthenelset not_init_conditional(
560  clinit_state_sym.symbol_expr(), clinit_statest::NOT_INIT),
561  code_blockt(
563  clinit_state_sym.symbol_expr(), clinit_statest::IN_PROGRESS),
564  code_assignt(init_complete.symbol_expr(), false_exprt())}),
565  std::move(init_conditional));
566 
567  function_body.add(std::move(not_init_conditional));
568  }
569 
570  // ATOMIC_END
571  {
572  function_body.add(atomic_end);
573  }
574 
575  // if(init_complete) return;
576  {
577  code_ifthenelset conditional(init_complete.symbol_expr(), code_returnt());
578  function_body.add(std::move(conditional));
579  }
580 
581  // Initialize the super-class C' and
582  // the implemented interfaces l_1 ... l_n.
583  // see JVMS p.359 step 7, for the exact definition of
584  // the sequence l_1 to l_n.
585  // This is achieved by iterating through the base types and
586  // adding recursive calls to the clinit_wrapper()
587  //
588  // java::C'::clinit_wrapper();
589  // java::I1::clinit_wrapper();
590  // java::I2::clinit_wrapper();
591  // // ...
592  // java::In::clinit_wrapper();
593  //
594  // java::C::<clinit>(); // or nondet-initialization of all static
595  // // variables of C if nondet-static is true
596  //
597  {
598  code_blockt init_body;
600  symbol_table,
601  class_name,
602  init_body,
604  object_factory_parameters,
605  pointer_type_selector);
606  function_body.append(init_body);
607  }
608 
609  // ATOMIC_START
610  // C::__CPROVER_PREFIX_clinit_state = INIT_COMPLETE;
611  // ATOMIC_END
612  // return;
613  {
614  // synchronization prologue
615  function_body.add(atomic_begin);
616  function_body.add(
618  clinit_state_sym.symbol_expr(), clinit_statest::INIT_COMPLETE));
619  function_body.add(atomic_end);
620  function_body.add(code_returnt());
621  }
622 
623  return function_body;
624 }
625 
639  const irep_idt &function_id,
640  symbol_table_baset &symbol_table,
641  const bool nondet_static,
642  const java_object_factory_parameterst &object_factory_parameters,
643  const select_pointer_typet &pointer_type_selector)
644 {
645  // Assume that class C extends class C' and implements interfaces
646  // I1, ..., In. We now create the following function (possibly recursively
647  // creating the clinit_wrapper functions for C' and I1, ..., In):
648  //
649  // java::C::clinit_wrapper()
650  // {
651  // if (!java::C::clinit_already_run)
652  // {
653  // java::C::clinit_already_run = true; // before recursive calls!
654  //
655  // java::C'::clinit_wrapper();
656  // java::I1::clinit_wrapper();
657  // java::I2::clinit_wrapper();
658  // // ...
659  // java::In::clinit_wrapper();
660  //
661  // java::C::<clinit>(); // or nondet-initialization of all static
662  // // variables of C if nondet-static is true
663  // }
664  // }
665  const symbolt &wrapper_method_symbol = symbol_table.lookup_ref(function_id);
666  irep_idt class_name = wrapper_method_symbol.type.get(ID_C_class);
667  INVARIANT(
668  !class_name.empty(), "wrapper function should be annotated with its class");
669 
670  const symbolt &already_run_symbol =
671  symbol_table.lookup_ref(clinit_already_run_variable_name(class_name));
672 
673  equal_exprt check_already_run(
674  already_run_symbol.symbol_expr(),
675  false_exprt());
676 
677  // add the "already-run = false" statement
678  code_assignt set_already_run(already_run_symbol.symbol_expr(), true_exprt());
679  code_blockt init_body({set_already_run});
680 
682  symbol_table,
683  class_name,
684  init_body,
686  object_factory_parameters,
687  pointer_type_selector);
688 
689  // the entire body of the function is an if-then-else
690  return code_ifthenelset(std::move(check_already_run), std::move(init_body));
691 }
692 
693 
702  symbol_tablet &symbol_table,
703  synthetic_methods_mapt &synthetic_methods,
704  const bool thread_safe)
705 {
706  // Top-sort the class hierarchy, such that we visit parents before children,
707  // and can so identify parents that need static initialisation by whether we
708  // have made them a clinit_wrapper method.
709  class_hierarchy_grapht class_graph;
710  class_graph.populate(symbol_table);
711  std::list<class_hierarchy_grapht::node_indext> topsorted_nodes =
712  class_graph.topsort();
713 
714  for(const auto node : topsorted_nodes)
715  {
716  const irep_idt &class_identifier = class_graph[node].class_identifier;
717  if(needs_clinit_wrapper(class_identifier, symbol_table))
718  {
720  class_identifier, symbol_table, synthetic_methods, thread_safe);
721  }
722  }
723 }
724 
728 template<class itertype>
729 static itertype advance_to_next_key(itertype in, itertype end)
730 {
731  PRECONDITION(in != end);
732  auto initial_key = in->first;
733  while(in != end && in->first == initial_key)
734  ++in;
735  return in;
736 }
737 
747  symbol_tablet &symbol_table,
748  const std::unordered_set<irep_idt> &stub_globals_set,
749  synthetic_methods_mapt &synthetic_methods)
750 {
751  // Populate map from class id -> stub globals:
752  for(const irep_idt &stub_global : stub_globals_set)
753  {
754  const symbolt &global_symbol = symbol_table.lookup_ref(stub_global);
755  if(global_symbol.value.is_nil())
756  {
757  // This symbol is already nondet-initialised during __CPROVER_initialize
758  // (generated in java_static_lifetime_init). In future this will only
759  // be the case for primitive-typed fields, but for now reference-typed
760  // fields can also be treated this way in the exceptional case that they
761  // belong to a non-stub class. Skip the field, as it does not need a
762  // synthetic static initializer.
763  continue;
764  }
765 
766  const irep_idt class_id =
767  global_symbol.type.get(ID_C_class);
768  INVARIANT(
769  !class_id.empty(),
770  "static field should be annotated with its defining class");
771  stub_globals_by_class.insert({class_id, stub_global});
772  }
773 
774  // For each distinct class that has stub globals, create a clinit symbol:
775 
776  for(auto it = stub_globals_by_class.begin(),
777  itend = stub_globals_by_class.end();
778  it != itend;
779  it = advance_to_next_key(it, itend))
780  {
781  const irep_idt static_init_name = clinit_function_name(it->first);
782 
783  INVARIANT(
784  to_java_class_type(symbol_table.lookup_ref(it->first).type).get_is_stub(),
785  "only stub classes should be given synthetic static initialisers");
786  INVARIANT(
787  !symbol_table.has_symbol(static_init_name),
788  "a class cannot be both incomplete, and so have stub static fields, and "
789  "also define a static initializer");
790 
791  const java_method_typet thunk_type({}, void_typet());
792 
793  symbolt static_init_symbol;
794  static_init_symbol.name = static_init_name;
795  static_init_symbol.pretty_name = static_init_name;
796  static_init_symbol.base_name = "clinit():V";
797  static_init_symbol.mode = ID_java;
798  static_init_symbol.type = thunk_type;
799  // Note this use of a type-comment to provide a back-link from a method
800  // to its associated class is the same one used in
801  // java_bytecode_convert_methodt::convert
802  static_init_symbol.type.set(ID_C_class, it->first);
803 
804  bool failed = symbol_table.add(static_init_symbol);
805  INVARIANT(!failed, "symbol should not already exist");
806 
807  auto insert_result = synthetic_methods.emplace(
808  static_init_symbol.name,
810  INVARIANT(
811  insert_result.second,
812  "synthetic methods map should not already contain entry for "
813  "stub static initializer");
814  }
815 }
816 
831  const irep_idt &function_id,
832  symbol_table_baset &symbol_table,
833  const java_object_factory_parameterst &object_factory_parameters,
834  const select_pointer_typet &pointer_type_selector)
835 {
836  const symbolt &stub_initializer_symbol = symbol_table.lookup_ref(function_id);
837  irep_idt class_id = stub_initializer_symbol.type.get(ID_C_class);
838  INVARIANT(
839  !class_id.empty(),
840  "synthetic static initializer should be annotated with its class");
841  code_blockt static_init_body;
842 
843  // Add a standard nondet initialisation for each global declared on this
844  // class. Note this is the same invocation used in
845  // java_static_lifetime_init.
846 
847  auto class_globals = stub_globals_by_class.equal_range(class_id);
848  INVARIANT(
849  class_globals.first != class_globals.second,
850  "class with synthetic clinit should have at least one global to init");
851 
852  java_object_factory_parameterst parameters = object_factory_parameters;
853  parameters.function_id = function_id;
854 
855  for(auto it = class_globals.first; it != class_globals.second; ++it)
856  {
857  const symbol_exprt new_global_symbol =
858  symbol_table.lookup_ref(it->second).symbol_expr();
859 
860  parameters.min_null_tree_depth =
861  is_non_null_library_global(it->second)
862  ? object_factory_parameters.min_null_tree_depth + 1
863  : object_factory_parameters.min_null_tree_depth;
864 
865  source_locationt location;
866  location.set_function(function_id);
868  new_global_symbol,
869  static_init_body,
870  symbol_table,
871  location,
872  false,
874  parameters,
875  pointer_type_selector,
877  }
878 
879  return static_init_body;
880 }
java_static_initializers.h
symbol_table_baset::has_symbol
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
Definition: symbol_table_base.h:78
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:150
synthetic_method_typet::STATIC_INITIALIZER_WRAPPER
A static initializer wrapper (code of the form if(!already_run) clinit(); already_run = true;) These ...
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
symbolt::is_state_var
bool is_state_var
Definition: symbol.h:61
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
create_static_initializer_wrappers
void create_static_initializer_wrappers(symbol_tablet &symbol_table, synthetic_methods_mapt &synthetic_methods, const bool thread_safe)
Create static initializer wrappers for all classes that need them.
Definition: java_static_initializers.cpp:701
symbol_table_baset::lookup_ref
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:96
clinit_statest::NOT_INIT
get_clinit_wrapper_body
code_ifthenelset get_clinit_wrapper_body(const irep_idt &function_id, symbol_table_baset &symbol_table, const bool nondet_static, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector)
Produces the static initializer wrapper body for the given function.
Definition: java_static_initializers.cpp:638
class_typet
Class type.
Definition: std_types.h:365
gen_clinit_eqexpr
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...
Definition: java_static_initializers.cpp:174
arith_tools.h
source_locationt::set_function
void set_function(const irep_idt &function)
Definition: source_location.h:122
comment
std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:107
typet
The type of an expression, extends irept.
Definition: type.h:27
to_class_type
const class_typet & to_class_type(const typet &type)
Cast a typet to a class_typet.
Definition: std_types.h:409
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
object_factory_parameterst::function_id
irep_idt function_id
Function id, used as a prefix for identifiers of temporaries.
Definition: object_factory_parameters.h:77
mp_integer
BigInt mp_integer
Definition: mp_arith.h:22
code_declt
A codet representing the declaration of a local variable.
Definition: std_code.h:352
exprt
Base class for all expressions.
Definition: expr.h:54
clinit_states_type
const typet clinit_states_type
Definition: java_static_initializers.cpp:47
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:400
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
bool_typet
The Boolean type.
Definition: std_types.h:28
clinit_local_init_complete_var_name
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.
Definition: java_static_initializers.cpp:144
synthetic_methods_mapt
std::unordered_map< irep_idt, synthetic_method_typet > synthetic_methods_mapt
Maps method names on to a synthetic method kind.
Definition: synthetic_methods_map.h:38
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:143
clinit_function_suffix
const std::string clinit_function_suffix
Definition: java_static_initializers.cpp:52
clinit_function_name
static irep_idt clinit_function_name(const irep_idt &class_name)
Get name of the real static initializer for a given class.
Definition: java_static_initializers.cpp:118
has_suffix
bool has_suffix(const std::string &s, const std::string &suffix)
Definition: suffix.h:15
equal_exprt
Equality.
Definition: std_expr.h:1484
code_ifthenelset
codet representation of an if-then-else statement.
Definition: std_code.h:614
nondet_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.
Definition: nondet_static.cpp:71
grapht::topsort
std::list< node_indext > topsort() const
Find a topological order of the nodes if graph is DAG, return empty list for non-DAG or empty graph.
Definition: graph.h:874
symbolt::pretty_name
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
source_locationt::set_line
void set_line(const irep_idt &line)
Definition: source_location.h:102
symbolt::is_thread_local
bool is_thread_local
Definition: symbol.h:65
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1036
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
java_object_factory.h
void_typet
The void type, the same as empty_typet.
Definition: std_types.h:57
clinit_state_var_name
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.
Definition: java_static_initializers.cpp:127
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
clinit_wrapper_do_recursive_calls
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 java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector)
Generates codet that iterates through the base types of the class specified by class_name,...
Definition: java_static_initializers.cpp:195
java_byte_type
typet java_byte_type()
Definition: java_types.cpp:52
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:21
nil_exprt
The NIL expression.
Definition: std_expr.h:4461
needs_clinit_wrapper
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.
Definition: java_static_initializers.cpp:275
code_assumet
An assumption, which must hold in subsequent code.
Definition: std_code.h:496
std_types.h
source_locationt::set_file
void set_file(const irep_idt &file)
Definition: source_location.h:92
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
is_non_null_library_global
bool is_non_null_library_global(const irep_idt &symbolid)
Check if a symbol is a well-known non-null global.
Definition: java_utils.cpp:410
select_pointer_typet
Definition: select_pointer_type.h:28
struct_typet::bases
const basest & bases() const
Get the collection of base classes/structs.
Definition: std_types.h:303
clinit_already_run_variable_name
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.
Definition: java_static_initializers.cpp:109
advance_to_next_key
static itertype advance_to_next_key(itertype in, itertype end)
Advance map iterator to next distinct key.
Definition: java_static_initializers.cpp:729
irept::is_nil
bool is_nil() const
Definition: irep.h:172
dstringt::empty
bool empty() const
Definition: dstring.h:75
code_blockt::add
void add(const codet &code)
Definition: std_code.h:189
false_exprt
The Boolean constant false.
Definition: std_expr.h:4452
std_code.h
object_factory_parameterst::min_null_tree_depth
size_t min_null_tree_depth
To force a certain depth of non-null objects.
Definition: object_factory_parameters.h:68
source_locationt
Definition: source_location.h:20
symbol_table_baset::add
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Definition: symbol_table_base.cpp:18
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
class_hierarchy.h
synthetic_method_typet::STUB_CLASS_STATIC_INITIALIZER
A generated (synthetic) static initializer function for a stub type.
clinit_wrapper_suffix
const std::string clinit_wrapper_suffix
Definition: java_static_initializers.cpp:51
stub_global_initializer_factoryt::get_stub_initializer_body
code_blockt get_stub_initializer_body(const irep_idt &function_id, symbol_table_baset &symbol_table, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector)
Create the body of a synthetic static initializer (clinit method), which initialise stub globals in t...
Definition: java_static_initializers.cpp:830
code_returnt
codet representation of a "return from a function" statement.
Definition: std_code.h:1191
suffix.h
class_hierarchy_grapht
Class hierarchy, represented using grapht and therefore suitable for use with generic graph algorithm...
Definition: class_hierarchy.h:102
stub_global_initializer_factoryt::create_stub_global_initializer_symbols
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.
Definition: java_static_initializers.cpp:746
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
get_thread_safe_clinit_wrapper_body
code_blockt get_thread_safe_clinit_wrapper_body(const irep_idt &function_id, symbol_table_baset &symbol_table, const bool nondet_static, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector)
Thread safe version of the static initializer.
Definition: java_static_initializers.cpp:448
clinit_statest
clinit_statest
The three states in which a <clinit> method for a class can be before, after, and during static class...
Definition: java_static_initializers.cpp:40
clinit_statest::IN_PROGRESS
symbolt
Symbol table entry.
Definition: symbol.h:27
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:123
code_blockt::append
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
Definition: std_code.cpp:102
symbol_table_baset::symbols
const symbolst & symbols
Definition: symbol_table_base.h:27
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
stub_global_initializer_factoryt::stub_globals_by_class
stub_globals_by_classt stub_globals_by_class
Definition: java_static_initializers.h:48
update_in_placet::NO_UPDATE_IN_PLACE
clinit_statest::INIT_COMPLETE
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
clinit_wrapper_name
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...
Definition: java_static_initializers.cpp:60
gen_nondet_init
void gen_nondet_init(const exprt &expr, code_blockt &init_code, symbol_table_baset &symbol_table, const source_locationt &loc, bool skip_classid, allocation_typet alloc_type, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, update_in_placet update_in_place)
Initializes a primitive-typed or reference-typed object tree rooted at expr, allocating child objects...
Definition: java_object_factory.cpp:1681
gen_clinit_assign
static code_assignt gen_clinit_assign(const exprt &expr, const clinit_statest state)
Generates a code_assignt for clinit_statest /param expr: expression to be used as the LHS of generate...
Definition: java_static_initializers.cpp:158
symbolt::is_lvalue
bool is_lvalue
Definition: symbol.h:66
to_java_class_type
const java_class_typet & to_java_class_type(const typet &type)
Definition: java_types.h:246
add_new_variable_symbol
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.
Definition: java_static_initializers.cpp:81
create_clinit_wrapper_symbols
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...
Definition: java_static_initializers.cpp:306
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:233
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:256
true_exprt
The Boolean constant true.
Definition: std_expr.h:4443
java_utils.h
constant_exprt
A constant literal expression.
Definition: std_expr.h:4384
allocation_typet::DYNAMIC
Allocate dynamic objects (using MALLOC)
clinit_thread_local_state_var_name
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.
Definition: java_static_initializers.cpp:136
std_expr.h
java_method_typet
Definition: java_types.h:264
is_clinit_wrapper_function
bool is_clinit_wrapper_function(const irep_idt &function_id)
Check if function_id is a clinit wrapper.
Definition: java_static_initializers.cpp:68
java_object_factory_parameterst
Definition: java_object_factory_parameters.h:14
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
validation_modet::INVARIANT
struct_typet::baset
Base class or struct that a class or struct inherits from.
Definition: std_types.h:292
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:34
not_exprt
Boolean negation.
Definition: std_expr.h:3308
class_hierarchy_grapht::populate
void populate(const symbol_tablet &)
Populate the class hierarchy graph, such that there is a node for every struct type in the symbol tab...
Definition: class_hierarchy.cpp:28