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 
11 #include "assignments_from_json.h"
12 #include "ci_lazy_methods_needed.h"
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 
48 enum class clinit_statest
49 {
50  NOT_INIT,
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.
62 const std::string clinit_wrapper_suffix = ".<clinit_wrapper>"; // NOLINT(*)
63 const std::string user_specified_clinit_suffix = ".<user_specified_clinit>"; // NOLINT(*)
64 const 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 
85 bool is_clinit_wrapper_function(const irep_idt &function_id)
86 {
87  return has_suffix(id2string(function_id), clinit_wrapper_suffix);
88 }
89 
93 bool is_clinit_function(const irep_idt &function_id)
94 {
95  return has_suffix(id2string(function_id), clinit_function_suffix);
96 }
97 
102 {
103  return has_suffix(id2string(function_id), user_specified_clinit_suffix);
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 
151 static irep_idt clinit_function_name(const irep_idt &class_name)
152 {
153  return id2string(class_name) + clinit_function_suffix;
154 }
155 
160 static 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 
190 static code_assignt
191 gen_clinit_assign(const exprt &expr, const clinit_statest state)
192 {
193  mp_integer initv(static_cast<int>(state));
195  return code_assignt(expr, init_s);
196 }
197 
206 static equal_exprt
207 gen_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,
234  code_blockt &init_body,
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();
245  irep_idt base_init_routine = clinit_wrapper_name(base_name);
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 
250  const irep_idt &clinit_name = replace_clinit
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  {
280  const symbol_exprt new_global_symbol =
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 
289  new_global_symbol,
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,
332  const irep_idt &function_base_name,
333  const synthetic_method_typet &synthetic_method_type,
334  symbol_tablet &symbol_table,
335  synthetic_methods_mapt &synthetic_methods)
336 {
337  symbolt function_symbol;
338  const java_method_typet function_type({}, java_void_type());
339  function_symbol.name = function_name;
340  function_symbol.pretty_name = function_symbol.name;
341  function_symbol.base_name = function_base_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.
345  set_declaring_class(function_symbol, class_name);
346  function_symbol.mode = ID_java;
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 " +
355  id2string(function_base_name));
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  {
406  exprt not_init_value = from_integer(
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),
416  not_init_value,
417  false,
418  true);
419 
421  symbol_table,
424  not_init_value,
425  true,
426  true);
427  }
428  else
429  {
430  const irep_idt &already_run_name =
432 
434  symbol_table,
435  already_run_name,
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 
536  const symbolt &clinit_state_sym =
537  symbol_table.lookup_ref(clinit_state_var_name(*class_name));
538  const symbolt &clinit_thread_local_state_sym =
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.
544  const symbolt &init_complete = add_new_variable_symbol(
545  symbol_table,
547  bool_typet(),
548  nil_exprt(),
549  true,
550  false);
551 
552  code_blockt function_body;
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  {
589  code_ifthenelset conditional(
591  clinit_thread_local_state_sym.symbol_expr(),
593  code_returnt());
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(
613  clinit_state_sym.symbol_expr(), clinit_statest::IN_PROGRESS);
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  {
629  code_ifthenelset init_conditional(
631  clinit_state_sym.symbol_expr(), clinit_statest::INIT_COMPLETE),
632  code_blockt({code_assignt(init_complete.symbol_expr(), true_exprt())}));
633 
634  code_ifthenelset not_init_conditional(
636  clinit_state_sym.symbol_expr(), clinit_statest::NOT_INIT),
637  code_blockt(
639  clinit_state_sym.symbol_expr(), clinit_statest::IN_PROGRESS),
640  code_assignt(init_complete.symbol_expr(), false_exprt())}),
641  std::move(init_conditional));
642 
643  function_body.add(std::move(not_init_conditional));
644  }
645 
646  // ATOMIC_END
647  {
648  function_body.add(atomic_end);
649  }
650 
651  // if(init_complete) return;
652  {
653  code_ifthenelset conditional(init_complete.symbol_expr(), code_returnt());
654  function_body.add(std::move(conditional));
655  }
656 
657  // Initialize the super-class C' and
658  // the implemented interfaces l_1 ... l_n.
659  // see JVMS p.359 step 7, for the exact definition of
660  // the sequence l_1 to l_n.
661  // This is achieved by iterating through the base types and
662  // adding recursive calls to the clinit_wrapper()
663  //
664  // java::C'.<clinit_wrapper>();
665  // java::I1.<clinit_wrapper>();
666  // java::I2.<clinit_wrapper>();
667  // // ...
668  // java::In.<clinit_wrapper>();
669  //
670  // java::C.<clinit>(); // or nondet-initialization of all static
671  // // variables of C if nondet-static is true
672  //
673  {
674  code_blockt init_body;
676  symbol_table,
677  *class_name,
678  init_body,
680  replace_clinit,
681  object_factory_parameters,
682  pointer_type_selector,
683  message_handler);
684  function_body.append(init_body);
685  }
686 
687  // ATOMIC_START
688  // C::__CPROVER_PREFIX_clinit_state = INIT_COMPLETE;
689  // ATOMIC_END
690  // return;
691  {
692  // synchronization prologue
693  function_body.add(atomic_begin);
694  function_body.add(
696  clinit_state_sym.symbol_expr(), clinit_statest::INIT_COMPLETE));
697  function_body.add(atomic_end);
698  function_body.add(code_returnt());
699  }
700 
701  return function_body;
702 }
703 
720  const irep_idt &function_id,
721  symbol_table_baset &symbol_table,
722  const bool nondet_static,
723  const bool replace_clinit,
724  const java_object_factory_parameterst &object_factory_parameters,
725  const select_pointer_typet &pointer_type_selector,
726  message_handlert &message_handler)
727 {
728  // Assume that class C extends class C' and implements interfaces
729  // I1, ..., In. We now create the following function (possibly recursively
730  // creating the clinit_wrapper functions for C' and I1, ..., In):
731  //
732  // java::C.<clinit_wrapper>()
733  // {
734  // if (!java::C::clinit_already_run)
735  // {
736  // java::C::clinit_already_run = true; // before recursive calls!
737  //
738  // java::C'.<clinit_wrapper>();
739  // java::I1.<clinit_wrapper>();
740  // java::I2.<clinit_wrapper>();
741  // // ...
742  // java::In.<clinit_wrapper>();
743  //
744  // java::C.<clinit>(); // or nondet-initialization of all static
745  // // variables of C if nondet-static is true
746  // }
747  // }
748  const symbolt &wrapper_method_symbol = symbol_table.lookup_ref(function_id);
749  const auto class_name = declaring_class(wrapper_method_symbol);
750  INVARIANT(class_name, "Wrapper function should have an owning class.");
751 
752  const symbolt &already_run_symbol =
753  symbol_table.lookup_ref(clinit_already_run_variable_name(*class_name));
754 
755  equal_exprt check_already_run(
756  already_run_symbol.symbol_expr(),
757  false_exprt());
758 
759  // add the "already-run = false" statement
760  code_assignt set_already_run(already_run_symbol.symbol_expr(), true_exprt());
761  code_blockt init_body({set_already_run});
762 
764  symbol_table,
765  *class_name,
766  init_body,
768  replace_clinit,
769  object_factory_parameters,
770  pointer_type_selector,
771  message_handler);
772 
773  // the entire body of the function is an if-then-else
774  return code_ifthenelset(std::move(check_already_run), std::move(init_body));
775 }
776 
778 std::unordered_multimap<irep_idt, symbolt>
780 {
781  std::unordered_multimap<irep_idt, symbolt> result;
782  for(const auto &symbol_pair : symbol_table)
783  {
784  const symbolt &symbol = symbol_pair.second;
785  if(optionalt<irep_idt> declaring = declaring_class(symbol))
786  result.emplace(*declaring, symbol);
787  }
788  return result;
789 }
790 
792  const irep_idt &class_id,
793  const json_objectt &static_values_json,
794  symbol_table_baset &symbol_table,
795  optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
796  size_t max_user_array_length,
797  std::unordered_map<std::string, object_creation_referencet> &references,
798  const std::unordered_multimap<irep_idt, symbolt>
799  &class_to_declared_symbols_map)
800 {
801  const irep_idt &real_clinit_name = clinit_function_name(class_id);
802  const auto clinit_func = symbol_table.lookup(real_clinit_name);
803  if(clinit_func == nullptr)
804  {
805  // Case where the real clinit doesn't appear in the symbol table, even
806  // though their is user specifed one. This may occur when some class
807  // substitution happened after compilation.
808  return code_blockt{};
809  }
810  const auto class_entry =
811  static_values_json.find(id2string(strip_java_namespace_prefix(class_id)));
812  if(class_entry != static_values_json.end() && class_entry->second.is_object())
813  {
814  const auto &class_json_object = to_json_object(class_entry->second);
815  std::map<symbol_exprt, jsont> static_field_values;
816  for(const auto &symbol_pair :
817  equal_range(class_to_declared_symbols_map, class_id))
818  {
819  const symbolt &symbol = symbol_pair.second;
820  if(symbol.is_static_lifetime)
821  {
822  const symbol_exprt &static_field_expr = symbol.symbol_expr();
823  const auto &static_field_entry =
824  class_json_object.find(id2string(symbol.base_name));
825  if(static_field_entry != class_json_object.end())
826  {
827  static_field_values.insert(
828  {static_field_expr, static_field_entry->second});
829  }
830  }
831  }
832  code_with_references_listt code_with_references;
833  for(const auto &value_pair : static_field_values)
834  {
835  code_with_references.append(assign_from_json(
836  value_pair.first,
837  value_pair.second,
838  real_clinit_name,
839  symbol_table,
840  needed_lazy_methods,
841  max_user_array_length,
842  references));
843  }
844  code_with_referencest::reference_substitutiont reference_substitution =
845  [&](const std::string &reference_id) -> object_creation_referencet & {
846  auto it = references.find(reference_id);
847  INVARIANT(it != references.end(), "reference id must be present in map");
848  return it->second;
849  };
850  code_blockt body;
851  for(const auto &code_with_ref : code_with_references.list)
852  body.append(code_with_ref->to_code(reference_substitution));
853  return body;
854  }
855  return code_blockt{{code_function_callt{clinit_func->symbol_expr()}}};
856 }
857 
875  symbol_tablet &symbol_table,
876  synthetic_methods_mapt &synthetic_methods,
877  const bool thread_safe,
878  const bool is_user_clinit_needed)
879 {
880  // Top-sort the class hierarchy, such that we visit parents before children,
881  // and can so identify parents that need static initialisation by whether we
882  // have made them a clinit_wrapper method.
883  class_hierarchy_grapht class_graph;
884  class_graph.populate(symbol_table);
885  std::list<class_hierarchy_grapht::node_indext> topsorted_nodes =
886  class_graph.topsort();
887 
888  for(const auto node : topsorted_nodes)
889  {
890  const irep_idt &class_identifier = class_graph[node].class_identifier;
891  if(needs_clinit_wrapper(class_identifier, symbol_table))
892  {
894  class_identifier, symbol_table, synthetic_methods, thread_safe);
895  if(is_user_clinit_needed)
896  {
898  class_identifier, symbol_table, synthetic_methods);
899  }
900  }
901  }
902 }
903 
907 template<class itertype>
908 static itertype advance_to_next_key(itertype in, itertype end)
909 {
910  PRECONDITION(in != end);
911  auto initial_key = in->first;
912  while(in != end && in->first == initial_key)
913  ++in;
914  return in;
915 }
916 
926  symbol_tablet &symbol_table,
927  const std::unordered_set<irep_idt> &stub_globals_set,
928  synthetic_methods_mapt &synthetic_methods)
929 {
930  // Populate map from class id -> stub globals:
931  for(const irep_idt &stub_global : stub_globals_set)
932  {
933  const symbolt &global_symbol = symbol_table.lookup_ref(stub_global);
934  if(global_symbol.value.is_nil())
935  {
936  // This symbol is already nondet-initialised during __CPROVER_initialize
937  // (generated in java_static_lifetime_init). In future this will only
938  // be the case for primitive-typed fields, but for now reference-typed
939  // fields can also be treated this way in the exceptional case that they
940  // belong to a non-stub class. Skip the field, as it does not need a
941  // synthetic static initializer.
942  continue;
943  }
944 
945  const auto class_id = declaring_class(global_symbol);
946  INVARIANT(class_id, "Static field should have a defining class.");
947  stub_globals_by_class.insert({*class_id, stub_global});
948  }
949 
950  // For each distinct class that has stub globals, create a clinit symbol:
951 
952  for(auto it = stub_globals_by_class.begin(),
953  itend = stub_globals_by_class.end();
954  it != itend;
955  it = advance_to_next_key(it, itend))
956  {
957  const irep_idt static_init_name = clinit_function_name(it->first);
958 
959  INVARIANT(
960  to_java_class_type(symbol_table.lookup_ref(it->first).type).get_is_stub(),
961  "only stub classes should be given synthetic static initialisers");
962  INVARIANT(
963  !symbol_table.has_symbol(static_init_name),
964  "a class cannot be both incomplete, and so have stub static fields, and "
965  "also define a static initializer");
966 
967  const java_method_typet thunk_type({}, java_void_type());
968 
969  symbolt static_init_symbol;
970  static_init_symbol.name = static_init_name;
971  static_init_symbol.pretty_name = static_init_name;
972  static_init_symbol.base_name = "clinit():V";
973  static_init_symbol.mode = ID_java;
974  static_init_symbol.type = thunk_type;
975  // This provides a back-link from a method to its associated class, as is
976  // done for java_bytecode_convert_methodt::convert.
977  set_declaring_class(static_init_symbol, it->first);
978 
979  bool failed = symbol_table.add(static_init_symbol);
980  INVARIANT(!failed, "symbol should not already exist");
981 
982  auto insert_result = synthetic_methods.emplace(
983  static_init_symbol.name,
985  INVARIANT(
986  insert_result.second,
987  "synthetic methods map should not already contain entry for "
988  "stub static initializer");
989  }
990 }
991 
1007  const irep_idt &function_id,
1008  symbol_table_baset &symbol_table,
1009  const java_object_factory_parameterst &object_factory_parameters,
1010  const select_pointer_typet &pointer_type_selector,
1011  message_handlert &message_handler)
1012 {
1013  const symbolt &stub_initializer_symbol = symbol_table.lookup_ref(function_id);
1014  const auto class_id = declaring_class(stub_initializer_symbol);
1015  INVARIANT(
1016  class_id, "Synthetic static initializer should have an owning class.");
1017  code_blockt static_init_body;
1018 
1019  // Add a standard nondet initialisation for each global declared on this
1020  // class. Note this is the same invocation used in
1021  // java_static_lifetime_init.
1022 
1023  auto class_globals = equal_range(stub_globals_by_class, *class_id);
1024  INVARIANT(
1025  !class_globals.empty(),
1026  "class with synthetic clinit should have at least one global to init");
1027 
1028  java_object_factory_parameterst parameters = object_factory_parameters;
1029  parameters.function_id = function_id;
1030 
1031  for(const auto &pair : class_globals)
1032  {
1033  const symbol_exprt new_global_symbol =
1034  symbol_table.lookup_ref(pair.second).symbol_expr();
1035 
1036  parameters.min_null_tree_depth =
1037  is_non_null_library_global(pair.second)
1038  ? object_factory_parameters.min_null_tree_depth + 1
1039  : object_factory_parameters.min_null_tree_depth;
1040 
1041  source_locationt location;
1042  location.set_function(function_id);
1044  new_global_symbol,
1045  static_init_body,
1046  symbol_table,
1047  location,
1048  false,
1050  parameters,
1051  pointer_type_selector,
1053  message_handler);
1054  }
1055 
1056  return static_init_body;
1057 }
@ DYNAMIC
Allocate dynamic objects (using ALLOCATE)
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
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.
The Boolean type.
Definition: std_types.h:36
Class hierarchy, represented using grapht and therefore suitable for use with generic graph algorithm...
void populate(const symbol_tablet &)
Populate the class hierarchy graph, such that there is a node for every struct type in the symbol tab...
Class type.
Definition: std_types.h:325
A codet representing an assignment in the program.
Definition: std_code.h:293
An assumption, which must hold in subsequent code.
Definition: std_code.h:565
A codet representing sequential composition of program statements.
Definition: std_code.h:168
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
Definition: std_code.cpp:89
void add(const codet &code)
Definition: std_code.h:206
A codet representing the declaration of a local variable.
Definition: std_code.h:400
codet representation of a function call statement.
Definition: std_code.h:1213
codet representation of an if-then-else statement.
Definition: std_code.h:776
codet representation of a "return from a function" statement.
Definition: std_code.h:1340
Wrapper around a list of shared pointer to code_with_referencest objects, which provides a nicer inte...
std::list< std::shared_ptr< code_with_referencest > > list
void append(code_with_references_listt &&other)
std::function< const object_creation_referencet &(const std::string &)> reference_substitutiont
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:33
A constant literal expression.
Definition: std_expr.h:2753
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
source_locationt & add_source_location()
Definition: expr.h:235
The Boolean constant false.
Definition: std_expr.h:2811
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:879
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
const irept & find(const irep_namet &name) const
Definition: irep.cpp:106
bool is_nil() const
Definition: irep.h:387
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:2820
Boolean negation.
Definition: std_expr.h:2127
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.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
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.
The symbol table.
Definition: symbol_table.h:14
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
bool is_static_lifetime
Definition: symbol.h:65
bool is_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
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:2802
The type of an expression, extends irept.
Definition: type.h:28
#define CPROVER_PREFIX
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
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) ...
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.
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...
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,...
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.
std::unordered_multimap< irep_idt, symbolt > class_to_declared_symbols(const symbol_tablet &symbol_table)
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()
Definition: java_types.cpp:37
signedbv_typet java_byte_type()
Definition: java_types.cpp:55
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.
Definition: java_utils.cpp:522
optionalt< irep_idt > declaring_class(const symbolt &symbol)
Gets the identifier of the class which declared a given symbol.
Definition: java_utils.cpp:571
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:577
irep_idt strip_java_namespace_prefix(const irep_idt &to_strip)
Strip java:: prefix from given identifier.
Definition: java_utils.cpp:410
json_objectt & to_json_object(jsont &json)
Definition: json.h:444
void nondet_static(const namespacet &ns, goto_functionst &goto_functions, const irep_idt &fct_name)
Nondeterministically initializes global scope variables in a goto-function.
nonstd::optional< T > optionalt
Definition: optional.h:35
static std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:109
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
BigInt mp_integer
Definition: smt_terms.h:12
#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.