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 <json/json_parser.h>
14 #include <util/arith_tools.h>
15 #include <util/std_code.h>
16 #include <util/std_expr.h>
17 #include <util/std_types.h>
18 #include <util/suffix.h>
19 
41 enum class clinit_statest
42 {
43  NOT_INIT,
46 };
47 
49 {
50  return java_byte_type();
51 }
52 
53 // Disable linter here to allow a std::string constant, since that holds
54 // a length, whereas a cstr would require strlen every time.
55 const std::string clinit_wrapper_suffix = ".<clinit_wrapper>"; // NOLINT(*)
56 const std::string user_specified_clinit_suffix = ".<user_specified_clinit>"; // NOLINT(*)
57 const std::string clinit_function_suffix = ".<clinit>:()V"; // NOLINT(*)
58 
66 {
67  return id2string(class_name) + clinit_wrapper_suffix;
68 }
69 
71 {
72  return id2string(class_name) + user_specified_clinit_suffix;
73 }
74 
78 bool is_clinit_wrapper_function(const irep_idt &function_id)
79 {
80  return has_suffix(id2string(function_id), clinit_wrapper_suffix);
81 }
82 
86 bool is_clinit_function(const irep_idt &function_id)
87 {
88  return has_suffix(id2string(function_id), clinit_function_suffix);
89 }
90 
95 {
97 }
98 
108  symbol_table_baset &symbol_table,
109  const irep_idt &name,
110  const typet &type,
111  const exprt &value,
112  const bool is_thread_local,
113  const bool is_static_lifetime)
114 {
115  symbolt new_symbol;
116  new_symbol.name = name;
117  new_symbol.pretty_name = name;
118  new_symbol.base_name = name;
119  new_symbol.type = type;
120  new_symbol.type.set(ID_C_no_nondet_initialization, true);
121  new_symbol.value = value;
122  new_symbol.is_lvalue = true;
123  new_symbol.is_state_var = true;
124  new_symbol.is_static_lifetime = is_static_lifetime;
125  new_symbol.is_thread_local = is_thread_local;
126  new_symbol.mode = ID_java;
127  symbol_table.add(new_symbol);
128  return new_symbol;
129 }
130 
136 {
137  return id2string(class_name) + "::clinit_already_run";
138 }
139 
144 static irep_idt clinit_function_name(const irep_idt &class_name)
145 {
146  return id2string(class_name) + clinit_function_suffix;
147 }
148 
153 static irep_idt clinit_state_var_name(const irep_idt &class_name)
154 {
155  return id2string(class_name) + CPROVER_PREFIX "clinit_state";
156 }
157 
163 {
164  return id2string(class_name) + CPROVER_PREFIX "clinit_threadlocal_state";
165 }
166 
171 {
172  return id2string(class_name) + CPROVER_PREFIX "clinit_wrapper::init_complete";
173 }
174 
183 static code_assignt
184 gen_clinit_assign(const exprt &expr, const clinit_statest state)
185 {
186  mp_integer initv(static_cast<int>(state));
188  return code_assignt(expr, init_s);
189 }
190 
199 static equal_exprt
200 gen_clinit_eqexpr(const exprt &expr, const clinit_statest state)
201 {
202  mp_integer initv(static_cast<int>(state));
204  return equal_exprt(expr, init_s);
205 }
206 
225  symbol_table_baset &symbol_table,
226  const irep_idt &class_name,
227  code_blockt &init_body,
228  const bool nondet_static,
229  const bool replace_clinit,
230  const java_object_factory_parameterst &object_factory_parameters,
231  const select_pointer_typet &pointer_type_selector,
232  message_handlert &message_handler)
233 {
234  const symbolt &class_symbol = symbol_table.lookup_ref(class_name);
235  for(const auto &base : to_class_type(class_symbol.type).bases())
236  {
237  const auto base_name = base.type().get_identifier();
238  irep_idt base_init_routine = clinit_wrapper_name(base_name);
239  if(const auto base_init_func = symbol_table.lookup(base_init_routine))
240  init_body.add(code_function_callt{base_init_func->symbol_expr()});
241  }
242 
243  const irep_idt &clinit_name = replace_clinit
244  ? user_specified_clinit_name(class_name)
245  : clinit_function_name(class_name);
246  if(const auto clinit_func = symbol_table.lookup(clinit_name))
247  init_body.add(code_function_callt{clinit_func->symbol_expr()});
248 
249  // If nondet-static option is given, add a standard nondet initialization for
250  // each non-final static field of this class. Note this is the same invocation
251  // used in get_stub_initializer_body and java_static_lifetime_init.
252  if(nondet_static)
253  {
254  java_object_factory_parameterst parameters = object_factory_parameters;
255  parameters.function_id = clinit_wrapper_name(class_name);
256 
257  std::vector<irep_idt> nondet_ids;
258  std::for_each(
259  symbol_table.symbols.begin(),
260  symbol_table.symbols.end(),
261  [&](const std::pair<irep_idt, symbolt> &symbol) {
262  if(
263  declaring_class(symbol.second) == class_name &&
264  symbol.second.is_static_lifetime &&
265  !symbol.second.type.get_bool(ID_C_constant))
266  {
267  nondet_ids.push_back(symbol.first);
268  }
269  });
270 
271  for(const auto &id : nondet_ids)
272  {
273  const symbol_exprt new_global_symbol =
274  symbol_table.lookup_ref(id).symbol_expr();
275 
276  parameters.min_null_tree_depth =
278  ? std::max(size_t(1), object_factory_parameters.min_null_tree_depth)
279  : object_factory_parameters.min_null_tree_depth;
280 
282  new_global_symbol,
283  init_body,
284  symbol_table,
286  false,
288  parameters,
289  pointer_type_selector,
291  message_handler);
292  }
293  }
294 }
295 
302  const irep_idt &class_name, const symbol_tablet &symbol_table)
303 {
304  if(symbol_table.has_symbol(clinit_function_name(class_name)))
305  return true;
306 
307  const class_typet &class_type =
308  to_class_type(symbol_table.lookup_ref(class_name).type);
309 
310  for(const class_typet::baset &base : class_type.bases())
311  {
312  if(symbol_table.has_symbol(
313  clinit_wrapper_name(base.type().get_identifier())))
314  {
315  return true;
316  }
317  }
318 
319  return false;
320 }
321 
323  const irep_idt &class_name,
324  const irep_idt &function_name,
325  const irep_idt &function_base_name,
326  const synthetic_method_typet &synthetic_method_type,
327  symbol_tablet &symbol_table,
328  synthetic_methods_mapt &synthetic_methods)
329 {
330  symbolt function_symbol;
331  const java_method_typet function_type({}, java_void_type());
332  function_symbol.name = function_name;
333  function_symbol.pretty_name = function_symbol.name;
334  function_symbol.base_name = function_base_name;
335  function_symbol.type = function_type;
336  // This provides a back-link from a method to its associated class, as is done
337  // for java_bytecode_convert_methodt::convert.
338  set_declaring_class(function_symbol, class_name);
339  function_symbol.mode = ID_java;
340  bool failed = symbol_table.add(function_symbol);
341  INVARIANT(!failed, id2string(function_base_name) + " symbol should be fresh");
342 
343  auto insert_result =
344  synthetic_methods.emplace(function_symbol.name, synthetic_method_type);
345  INVARIANT(
346  insert_result.second,
347  "synthetic methods map should not already contain entry for " +
348  id2string(function_base_name));
349 }
350 
351 // Create symbol for the "clinit_wrapper"
353  const irep_idt &class_name,
354  symbol_tablet &symbol_table,
355  synthetic_methods_mapt &synthetic_methods)
356 {
358  class_name,
359  clinit_wrapper_name(class_name),
360  "clinit_wrapper",
362  symbol_table,
363  synthetic_methods);
364 }
365 
366 // Create symbol for the "user_specified_clinit"
368  const irep_idt &class_name,
369  symbol_tablet &symbol_table,
370  synthetic_methods_mapt &synthetic_methods)
371 {
373  class_name,
374  user_specified_clinit_name(class_name),
375  "user_specified_clinit",
377  symbol_table,
378  synthetic_methods);
379 }
380 
392  const irep_idt &class_name,
393  symbol_tablet &symbol_table,
394  synthetic_methods_mapt &synthetic_methods,
395  const bool thread_safe)
396 {
397  if(thread_safe)
398  {
399  exprt not_init_value = from_integer(
400  static_cast<int>(clinit_statest::NOT_INIT), clinit_states_type());
401 
402  // Create two global static synthetic "fields" for the class "id"
403  // these two variables hold the state of the class initialization algorithm
404  // across calls to the clinit_wrapper
406  symbol_table,
407  clinit_state_var_name(class_name),
409  not_init_value,
410  false,
411  true);
412 
414  symbol_table,
417  not_init_value,
418  true,
419  true);
420  }
421  else
422  {
423  const irep_idt &already_run_name =
425 
427  symbol_table,
428  already_run_name,
429  bool_typet(),
430  false_exprt(),
431  false,
432  true);
433  }
434 
436  class_name, symbol_table, synthetic_methods);
437 }
438 
517  const irep_idt &function_id,
518  symbol_table_baset &symbol_table,
519  const bool nondet_static,
520  const bool replace_clinit,
521  const java_object_factory_parameterst &object_factory_parameters,
522  const select_pointer_typet &pointer_type_selector,
523  message_handlert &message_handler)
524 {
525  const symbolt &wrapper_method_symbol = symbol_table.lookup_ref(function_id);
526  const auto class_name = declaring_class(wrapper_method_symbol);
527  INVARIANT(class_name, "Wrapper function should have an owning class.");
528 
529  const symbolt &clinit_state_sym =
530  symbol_table.lookup_ref(clinit_state_var_name(*class_name));
531  const symbolt &clinit_thread_local_state_sym =
532  symbol_table.lookup_ref(clinit_thread_local_state_var_name(*class_name));
533 
534  // Create a function-local variable "init_complete". This variable is used to
535  // avoid inspecting the global state (clinit_state_sym) outside of
536  // the critical-section.
537  const symbolt &init_complete = add_new_variable_symbol(
538  symbol_table,
540  bool_typet(),
541  nil_exprt(),
542  true,
543  false);
544 
545  code_blockt function_body;
546  codet atomic_begin(ID_atomic_begin);
547  codet atomic_end(ID_atomic_end);
548 
549 #if 0
550  // This code defines source locations for every codet generated below for
551  // the static initializer wrapper. Enable this for debugging the symex going
552  // through the clinit_wrapper.
553  //
554  // java::C.<clinit_wrapper>()
555  // You will additionally need to associate the `location` with the
556  // `function_body` and then manually set lines of code for each of the
557  // statements of the function, using something along the lines of:
558  // `mycodet.then_case().add_source_location().set_line(17);`/
559 
560  source_locationt &location = function_body.add_source_location();
561  location.set_file ("<generated>");
562  location.set_line ("<generated>");
564  std::string comment =
565  "Automatically generated function. States are:\n"
566  " 0 = class not initialized, init val of clinit_state/clinit_local_state\n"
567  " 1 = class initialization in progress, by this or another thread\n"
568  " 2 = initialization finished with success, by this or another thread\n";
569  static_assert((int) clinit_statest::NOT_INIT==0, "Check commment above");
570  static_assert((int) clinit_statest::IN_PROGRESS==1, "Check comment above");
571  static_assert((int) clinit_statest::INIT_COMPLETE==2, "Check comment above");
572 #endif
573 
574  // bool init_complete;
575  {
576  code_declt decl(init_complete.symbol_expr());
577  function_body.add(decl);
578  }
579 
580  // if(C::__CPROVER_PREFIX_clinit_thread_local_state == INIT_COMPLETE) return;
581  {
582  code_ifthenelset conditional(
584  clinit_thread_local_state_sym.symbol_expr(),
586  code_returnt());
587  function_body.add(std::move(conditional));
588  }
589 
590  // C::__CPROVER_PREFIX_clinit_thread_local_state = INIT_COMPLETE;
591  {
593  clinit_thread_local_state_sym.symbol_expr(),
595  function_body.add(assign);
596  }
597 
598  // ATOMIC_BEGIN
599  {
600  function_body.add(atomic_begin);
601  }
602 
603  // Assume: clinit_state_sym != IN_PROGRESS
604  {
605  exprt assumption = gen_clinit_eqexpr(
606  clinit_state_sym.symbol_expr(), clinit_statest::IN_PROGRESS);
607  assumption = not_exprt(assumption);
608  code_assumet assume(assumption);
609  function_body.add(assume);
610  }
611 
612  // If(C::__CPROVER_PREFIX_clinit_state == NOT_INIT)
613  // {
614  // C::__CPROVER_PREFIX_clinit_state = IN_PROGRESS;
615  // init_complete = false;
616  // }
617  // else If(C::__CPROVER_PREFIX_clinit_state == INIT_COMPLETE)
618  // {
619  // init_complete = true;
620  // }
621  {
622  code_ifthenelset init_conditional(
624  clinit_state_sym.symbol_expr(), clinit_statest::INIT_COMPLETE),
625  code_blockt({code_assignt(init_complete.symbol_expr(), true_exprt())}));
626 
627  code_ifthenelset not_init_conditional(
629  clinit_state_sym.symbol_expr(), clinit_statest::NOT_INIT),
630  code_blockt(
632  clinit_state_sym.symbol_expr(), clinit_statest::IN_PROGRESS),
633  code_assignt(init_complete.symbol_expr(), false_exprt())}),
634  std::move(init_conditional));
635 
636  function_body.add(std::move(not_init_conditional));
637  }
638 
639  // ATOMIC_END
640  {
641  function_body.add(atomic_end);
642  }
643 
644  // if(init_complete) return;
645  {
646  code_ifthenelset conditional(init_complete.symbol_expr(), code_returnt());
647  function_body.add(std::move(conditional));
648  }
649 
650  // Initialize the super-class C' and
651  // the implemented interfaces l_1 ... l_n.
652  // see JVMS p.359 step 7, for the exact definition of
653  // the sequence l_1 to l_n.
654  // This is achieved by iterating through the base types and
655  // adding recursive calls to the clinit_wrapper()
656  //
657  // java::C'.<clinit_wrapper>();
658  // java::I1.<clinit_wrapper>();
659  // java::I2.<clinit_wrapper>();
660  // // ...
661  // java::In.<clinit_wrapper>();
662  //
663  // java::C.<clinit>(); // or nondet-initialization of all static
664  // // variables of C if nondet-static is true
665  //
666  {
667  code_blockt init_body;
669  symbol_table,
670  *class_name,
671  init_body,
673  replace_clinit,
674  object_factory_parameters,
675  pointer_type_selector,
676  message_handler);
677  function_body.append(init_body);
678  }
679 
680  // ATOMIC_START
681  // C::__CPROVER_PREFIX_clinit_state = INIT_COMPLETE;
682  // ATOMIC_END
683  // return;
684  {
685  // synchronization prologue
686  function_body.add(atomic_begin);
687  function_body.add(
689  clinit_state_sym.symbol_expr(), clinit_statest::INIT_COMPLETE));
690  function_body.add(atomic_end);
691  function_body.add(code_returnt());
692  }
693 
694  return function_body;
695 }
696 
713  const irep_idt &function_id,
714  symbol_table_baset &symbol_table,
715  const bool nondet_static,
716  const bool replace_clinit,
717  const java_object_factory_parameterst &object_factory_parameters,
718  const select_pointer_typet &pointer_type_selector,
719  message_handlert &message_handler)
720 {
721  // Assume that class C extends class C' and implements interfaces
722  // I1, ..., In. We now create the following function (possibly recursively
723  // creating the clinit_wrapper functions for C' and I1, ..., In):
724  //
725  // java::C.<clinit_wrapper>()
726  // {
727  // if (!java::C::clinit_already_run)
728  // {
729  // java::C::clinit_already_run = true; // before recursive calls!
730  //
731  // java::C'.<clinit_wrapper>();
732  // java::I1.<clinit_wrapper>();
733  // java::I2.<clinit_wrapper>();
734  // // ...
735  // java::In.<clinit_wrapper>();
736  //
737  // java::C.<clinit>(); // or nondet-initialization of all static
738  // // variables of C if nondet-static is true
739  // }
740  // }
741  const symbolt &wrapper_method_symbol = symbol_table.lookup_ref(function_id);
742  const auto class_name = declaring_class(wrapper_method_symbol);
743  INVARIANT(class_name, "Wrapper function should have an owning class.");
744 
745  const symbolt &already_run_symbol =
746  symbol_table.lookup_ref(clinit_already_run_variable_name(*class_name));
747 
748  equal_exprt check_already_run(
749  already_run_symbol.symbol_expr(),
750  false_exprt());
751 
752  // add the "already-run = false" statement
753  code_assignt set_already_run(already_run_symbol.symbol_expr(), true_exprt());
754  code_blockt init_body({set_already_run});
755 
757  symbol_table,
758  *class_name,
759  init_body,
761  replace_clinit,
762  object_factory_parameters,
763  pointer_type_selector,
764  message_handler);
765 
766  // the entire body of the function is an if-then-else
767  return code_ifthenelset(std::move(check_already_run), std::move(init_body));
768 }
769 
771 std::unordered_multimap<irep_idt, symbolt>
773 {
774  std::unordered_multimap<irep_idt, symbolt> result;
775  for(const auto &symbol_pair : symbol_table)
776  {
777  const symbolt &symbol = symbol_pair.second;
778  if(optionalt<irep_idt> declaring = declaring_class(symbol))
779  result.emplace(*declaring, symbol);
780  }
781  return result;
782 }
783 
785  const irep_idt &class_id,
786  const json_objectt &static_values_json,
787  symbol_table_baset &symbol_table,
788  optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
789  size_t max_user_array_length,
790  std::unordered_map<std::string, object_creation_referencet> &references,
791  const std::unordered_multimap<irep_idt, symbolt>
792  &class_to_declared_symbols_map)
793 {
794  const irep_idt &real_clinit_name = clinit_function_name(class_id);
795  const auto clinit_func = symbol_table.lookup(real_clinit_name);
796  if(clinit_func == nullptr)
797  {
798  // Case where the real clinit doesn't appear in the symbol table, even
799  // though their is user specifed one. This may occur when some class
800  // substitution happened after compilation.
801  return code_blockt{};
802  }
803  const auto class_entry =
804  static_values_json.find(id2string(strip_java_namespace_prefix(class_id)));
805  if(class_entry != static_values_json.end() && class_entry->second.is_object())
806  {
807  const auto &class_json_object = to_json_object(class_entry->second);
808  std::map<symbol_exprt, jsont> static_field_values;
809  for(const auto &symbol_pair :
810  equal_range(class_to_declared_symbols_map, class_id))
811  {
812  const symbolt &symbol = symbol_pair.second;
813  if(symbol.is_static_lifetime)
814  {
815  const symbol_exprt &static_field_expr = symbol.symbol_expr();
816  const auto &static_field_entry =
817  class_json_object.find(id2string(symbol.base_name));
818  if(static_field_entry != class_json_object.end())
819  {
820  static_field_values.insert(
821  {static_field_expr, static_field_entry->second});
822  }
823  }
824  }
825  code_with_references_listt code_with_references;
826  for(const auto &value_pair : static_field_values)
827  {
828  code_with_references.append(assign_from_json(
829  value_pair.first,
830  value_pair.second,
831  real_clinit_name,
832  symbol_table,
833  needed_lazy_methods,
834  max_user_array_length,
835  references));
836  }
837  code_with_referencest::reference_substitutiont reference_substitution =
838  [&](const std::string &reference_id) -> object_creation_referencet & {
839  auto it = references.find(reference_id);
840  INVARIANT(it != references.end(), "reference id must be present in map");
841  return it->second;
842  };
843  code_blockt body;
844  for(const auto &code_with_ref : code_with_references.list)
845  body.append(code_with_ref->to_code(reference_substitution));
846  return body;
847  }
848  return code_blockt{{code_function_callt{clinit_func->symbol_expr()}}};
849 }
850 
868  symbol_tablet &symbol_table,
869  synthetic_methods_mapt &synthetic_methods,
870  const bool thread_safe,
871  const bool is_user_clinit_needed)
872 {
873  // Top-sort the class hierarchy, such that we visit parents before children,
874  // and can so identify parents that need static initialisation by whether we
875  // have made them a clinit_wrapper method.
876  class_hierarchy_grapht class_graph;
877  class_graph.populate(symbol_table);
878  std::list<class_hierarchy_grapht::node_indext> topsorted_nodes =
879  class_graph.topsort();
880 
881  for(const auto node : topsorted_nodes)
882  {
883  const irep_idt &class_identifier = class_graph[node].class_identifier;
884  if(needs_clinit_wrapper(class_identifier, symbol_table))
885  {
887  class_identifier, symbol_table, synthetic_methods, thread_safe);
888  if(is_user_clinit_needed)
889  {
891  class_identifier, symbol_table, synthetic_methods);
892  }
893  }
894  }
895 }
896 
900 template<class itertype>
901 static itertype advance_to_next_key(itertype in, itertype end)
902 {
903  PRECONDITION(in != end);
904  auto initial_key = in->first;
905  while(in != end && in->first == initial_key)
906  ++in;
907  return in;
908 }
909 
919  symbol_tablet &symbol_table,
920  const std::unordered_set<irep_idt> &stub_globals_set,
921  synthetic_methods_mapt &synthetic_methods)
922 {
923  // Populate map from class id -> stub globals:
924  for(const irep_idt &stub_global : stub_globals_set)
925  {
926  const symbolt &global_symbol = symbol_table.lookup_ref(stub_global);
927  if(global_symbol.value.is_nil())
928  {
929  // This symbol is already nondet-initialised during __CPROVER_initialize
930  // (generated in java_static_lifetime_init). In future this will only
931  // be the case for primitive-typed fields, but for now reference-typed
932  // fields can also be treated this way in the exceptional case that they
933  // belong to a non-stub class. Skip the field, as it does not need a
934  // synthetic static initializer.
935  continue;
936  }
937 
938  const auto class_id = declaring_class(global_symbol);
939  INVARIANT(class_id, "Static field should have a defining class.");
940  stub_globals_by_class.insert({*class_id, stub_global});
941  }
942 
943  // For each distinct class that has stub globals, create a clinit symbol:
944 
945  for(auto it = stub_globals_by_class.begin(),
946  itend = stub_globals_by_class.end();
947  it != itend;
948  it = advance_to_next_key(it, itend))
949  {
950  const irep_idt static_init_name = clinit_function_name(it->first);
951 
952  INVARIANT(
953  to_java_class_type(symbol_table.lookup_ref(it->first).type).get_is_stub(),
954  "only stub classes should be given synthetic static initialisers");
955  INVARIANT(
956  !symbol_table.has_symbol(static_init_name),
957  "a class cannot be both incomplete, and so have stub static fields, and "
958  "also define a static initializer");
959 
960  const java_method_typet thunk_type({}, java_void_type());
961 
962  symbolt static_init_symbol;
963  static_init_symbol.name = static_init_name;
964  static_init_symbol.pretty_name = static_init_name;
965  static_init_symbol.base_name = "clinit():V";
966  static_init_symbol.mode = ID_java;
967  static_init_symbol.type = thunk_type;
968  // This provides a back-link from a method to its associated class, as is
969  // done for java_bytecode_convert_methodt::convert.
970  set_declaring_class(static_init_symbol, it->first);
971 
972  bool failed = symbol_table.add(static_init_symbol);
973  INVARIANT(!failed, "symbol should not already exist");
974 
975  auto insert_result = synthetic_methods.emplace(
976  static_init_symbol.name,
978  INVARIANT(
979  insert_result.second,
980  "synthetic methods map should not already contain entry for "
981  "stub static initializer");
982  }
983 }
984 
1000  const irep_idt &function_id,
1001  symbol_table_baset &symbol_table,
1002  const java_object_factory_parameterst &object_factory_parameters,
1003  const select_pointer_typet &pointer_type_selector,
1004  message_handlert &message_handler)
1005 {
1006  const symbolt &stub_initializer_symbol = symbol_table.lookup_ref(function_id);
1007  const auto class_id = declaring_class(stub_initializer_symbol);
1008  INVARIANT(
1009  class_id, "Synthetic static initializer should have an owning class.");
1010  code_blockt static_init_body;
1011 
1012  // Add a standard nondet initialisation for each global declared on this
1013  // class. Note this is the same invocation used in
1014  // java_static_lifetime_init.
1015 
1016  auto class_globals = equal_range(stub_globals_by_class, *class_id);
1017  INVARIANT(
1018  !class_globals.empty(),
1019  "class with synthetic clinit should have at least one global to init");
1020 
1021  java_object_factory_parameterst parameters = object_factory_parameters;
1022  parameters.function_id = function_id;
1023 
1024  for(const auto &pair : class_globals)
1025  {
1026  const symbol_exprt new_global_symbol =
1027  symbol_table.lookup_ref(pair.second).symbol_expr();
1028 
1029  parameters.min_null_tree_depth =
1030  is_non_null_library_global(pair.second)
1031  ? object_factory_parameters.min_null_tree_depth + 1
1032  : object_factory_parameters.min_null_tree_depth;
1033 
1034  source_locationt location;
1035  location.set_function(function_id);
1037  new_global_symbol,
1038  static_init_body,
1039  symbol_table,
1040  location,
1041  false,
1043  parameters,
1044  pointer_type_selector,
1046  message_handler);
1047  }
1048 
1049  return static_init_body;
1050 }
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:87
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:170
synthetic_method_typet::STATIC_INITIALIZER_WRAPPER
@ STATIC_INITIALIZER_WRAPPER
A static initializer wrapper (code of the form if(!already_run) clinit(); already_run = true;) These ...
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 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.
Definition: java_static_initializers.cpp:712
create_clinit_wrapper_function_symbol
static void create_clinit_wrapper_function_symbol(const irep_idt &class_name, symbol_tablet &symbol_table, synthetic_methods_mapt &synthetic_methods)
Definition: java_static_initializers.cpp:352
symbolt::is_state_var
bool is_state_var
Definition: symbol.h:62
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
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:104
clinit_statest::NOT_INIT
@ NOT_INIT
class_typet
Class type.
Definition: std_types.h:320
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:200
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, message_handlert &message_handler)
Create the body of a synthetic static initializer (clinit method), which initialise stub globals in t...
Definition: java_static_initializers.cpp:999
arith_tools.h
source_locationt::set_function
void set_function(const irep_idt &function)
Definition: source_location.h:126
synthetic_method_typet
synthetic_method_typet
Synthetic method kinds.
Definition: synthetic_methods_map.h:24
set_declaring_class
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.
Definition: java_utils.cpp:585
code_with_referencest::reference_substitutiont
std::function< const object_creation_referencet &(const std::string &)> reference_substitutiont
Definition: code_with_references.h:44
typet
The type of an expression, extends irept.
Definition: type.h:29
to_class_type
const class_typet & to_class_type(const typet &type)
Cast a typet to a class_typet.
Definition: std_types.h:376
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
create_user_specified_clinit_function_symbol
static void create_user_specified_clinit_function_symbol(const irep_idt &class_name, symbol_tablet &symbol_table, synthetic_methods_mapt &synthetic_methods)
Definition: java_static_initializers.cpp:367
object_factory_parameterst::function_id
irep_idt function_id
Function id, used as a prefix for identifiers of temporaries.
Definition: object_factory_parameters.h:82
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
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 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.
Definition: java_static_initializers.cpp:516
json_objectt::find
iterator find(const std::string &key)
Definition: json.h:356
declaring_class
optionalt< irep_idt > declaring_class(const symbolt &symbol)
Gets the identifier of the class which declared a given symbol.
Definition: java_utils.cpp:579
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
user_specified_clinit_suffix
const std::string user_specified_clinit_suffix
Definition: java_static_initializers.cpp:56
code_declt
A codet representing the declaration of a local variable.
Definition: std_code.h:402
is_clinit_function
bool is_clinit_function(const irep_idt &function_id)
Check if function_id is a clinit.
Definition: java_static_initializers.cpp:86
user_specified_clinit_name
irep_idt user_specified_clinit_name(const irep_idt &class_name)
Definition: java_static_initializers.cpp:70
exprt
Base class for all expressions.
Definition: expr.h:53
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
create_static_initializer_symbols
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...
Definition: java_static_initializers.cpp:867
bool_typet
The Boolean type.
Definition: std_types.h:37
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:170
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:53
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
clinit_function_suffix
const std::string clinit_function_suffix
Definition: java_static_initializers.cpp:57
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:144
has_suffix
bool has_suffix(const std::string &s, const std::string &suffix)
Definition: suffix.h:17
equal_exprt
Equality.
Definition: std_expr.h:1190
class_to_declared_symbols
std::unordered_multimap< irep_idt, symbolt > class_to_declared_symbols(const symbol_tablet &symbol_table)
Definition: java_static_initializers.cpp:772
create_function_symbol
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)
Definition: java_static_initializers.cpp:322
code_ifthenelset
codet representation of an if-then-else statement.
Definition: std_code.h:746
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:79
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:876
symbolt::pretty_name
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
json_objectt
Definition: json.h:300
json_parser.h
strip_java_namespace_prefix
irep_idt strip_java_namespace_prefix(const irep_idt &to_strip)
Strip java:: prefix from given identifier.
Definition: java_utils.cpp:417
source_locationt::set_line
void set_line(const irep_idt &line)
Definition: source_location.h:106
get_user_specified_clinit_body
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...
Definition: java_static_initializers.cpp:784
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:1183
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
java_object_factory.h
This module is responsible for the synthesis of code (in the form of a sequence of codet statements) ...
synthetic_method_typet::USER_SPECIFIED_STATIC_INITIALIZER
@ USER_SPECIFIED_STATIC_INITIALIZER
Only exists if the --static-values option was used.
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:153
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
failed
static bool failed(bool error_indicator)
Definition: symtab2gb_parse_options.cpp:34
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 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,...
Definition: java_static_initializers.cpp:224
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:22
nil_exprt
The NIL expression.
Definition: std_expr.h:3973
clinit_states_type
static typet clinit_states_type()
Definition: java_static_initializers.cpp:48
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:301
code_assumet
An assumption, which must hold in subsequent code.
Definition: std_code.h:535
std_types.h
Pre-defined types.
source_locationt::set_file
void set_file(const irep_idt &file)
Definition: source_location.h:96
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
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:529
select_pointer_typet
Definition: select_pointer_type.h:26
struct_typet::bases
const basest & bases() const
Get the collection of base classes/structs.
Definition: std_types.h:257
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:135
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:901
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, 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...
Definition: java_object_factory.cpp:1624
object_creation_referencet
Information to store when several references point to the same Java object.
Definition: code_with_references.h:24
irept::is_nil
bool is_nil() const
Definition: irep.h:398
message_handlert
Definition: message.h:28
code_blockt::add
void add(const codet &code)
Definition: std_code.h:208
false_exprt
The Boolean constant false.
Definition: std_expr.h:3964
std_code.h
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
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:73
source_locationt
Definition: source_location.h:20
java_byte_type
signedbv_typet java_byte_type()
Definition: java_types.cpp:56
code_with_references_listt::append
void append(code_with_references_listt &&other)
Definition: code_with_references.cpp:67
symbol_table_baset::add
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Definition: symbol_table_base.cpp:18
is_user_specified_clinit_function
bool is_user_specified_clinit_function(const irep_idt &function_id)
Check if function_id is a user-specified clinit.
Definition: java_static_initializers.cpp:94
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
class_hierarchy.h
Class Hierarchy.
synthetic_method_typet::STUB_CLASS_STATIC_INITIALIZER
@ 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:55
json_objectt::end
iterator end()
Definition: json.h:386
code_returnt
codet representation of a "return from a function" statement.
Definition: std_code.h:1310
code_with_references_listt
Wrapper around a list of shared pointer to code_with_referencest objects, which provides a nicer inte...
Definition: code_with_references.h:93
suffix.h
to_json_object
json_objectt & to_json_object(jsont &json)
Definition: json.h:444
class_hierarchy_grapht
Class hierarchy, represented using grapht and therefore suitable for use with generic graph algorithm...
Definition: class_hierarchy.h:103
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:918
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:42
code_with_references_listt::list
std::list< std::shared_ptr< code_with_referencest > > list
Definition: code_with_references.h:95
clinit_statest::IN_PROGRESS
@ IN_PROGRESS
symbolt
Symbol table entry.
Definition: symbol.h:28
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:442
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
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:87
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
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:96
update_in_placet::NO_UPDATE_IN_PLACE
@ NO_UPDATE_IN_PLACE
clinit_statest::INIT_COMPLETE
@ 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:65
lifetimet::DYNAMIC
@ DYNAMIC
Allocate dynamic objects (using ALLOCATE)
symbol_table_baset::lookup
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:95
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:184
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:584
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:107
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:391
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:259
java_class_typet::get_is_stub
bool get_is_stub() const
Definition: java_types.h:400
java_void_type
empty_typet java_void_type()
Definition: java_types.cpp:38
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
true_exprt
The Boolean constant true.
Definition: std_expr.h:3955
java_utils.h
constant_exprt
A constant literal expression.
Definition: std_expr.h:3906
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:162
comment
static std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:109
std_expr.h
API to expression classes.
java_method_typet
Definition: java_types.h:103
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:78
java_object_factory_parameterst
Definition: java_object_factory_parameters.h:16
assign_from_json
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...
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
validation_modet::INVARIANT
@ INVARIANT
struct_typet::baset
Base class or struct that a class or struct inherits from.
Definition: std_types.h:247
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35
not_exprt
Boolean negation.
Definition: std_expr.h:2843
equal_range
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
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