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.value = value;
95  new_symbol.is_lvalue = true;
96  new_symbol.is_state_var = true;
97  new_symbol.is_static_lifetime = is_static_lifetime;
98  new_symbol.is_thread_local = is_thread_local;
99  new_symbol.mode = ID_java;
100  symbol_table.add(new_symbol);
101  return new_symbol;
102 }
103 
109 {
110  return id2string(class_name) + "::clinit_already_run";
111 }
112 
117 static irep_idt clinit_function_name(const irep_idt &class_name)
118 {
119  return id2string(class_name) + clinit_function_suffix;
120 }
121 
126 static irep_idt clinit_state_var_name(const irep_idt &class_name)
127 {
128  return id2string(class_name) + CPROVER_PREFIX "clinit_state";
129 }
130 
136 {
137  return id2string(class_name) + CPROVER_PREFIX "clinit_threadlocal_state";
138 }
139 
144 {
145  return id2string(class_name) + CPROVER_PREFIX "clinit_wrapper::init_complete";
146 }
147 
156 static code_assignt
157 gen_clinit_assign(const exprt &expr, const clinit_statest state)
158 {
159  mp_integer initv(static_cast<int>(state));
161  return code_assignt(expr, init_s);
162 }
163 
172 static equal_exprt
173 gen_clinit_eqexpr(const exprt &expr, const clinit_statest state)
174 {
175  mp_integer initv(static_cast<int>(state));
177  return equal_exprt(expr, init_s);
178 }
179 
187  const symbol_tablet &symbol_table,
188  const irep_idt &class_name,
189  code_blockt &init_body)
190 {
191  const symbolt &class_symbol = symbol_table.lookup_ref(class_name);
192  for(const auto &base : to_class_type(class_symbol.type).bases())
193  {
194  const auto base_name = to_symbol_type(base.type()).get_identifier();
195  irep_idt base_init_routine = clinit_wrapper_name(base_name);
196  auto findit = symbol_table.symbols.find(base_init_routine);
197  if(findit == symbol_table.symbols.end())
198  continue;
199  code_function_callt call_base;
200  call_base.function() = findit->second.symbol_expr();
201  init_body.move_to_operands(call_base);
202  }
203 
204  const irep_idt &real_clinit_name = clinit_function_name(class_name);
205  auto find_sym_it = symbol_table.symbols.find(real_clinit_name);
206  if(find_sym_it != symbol_table.symbols.end())
207  {
208  code_function_callt call_real_init;
209  call_real_init.function() = find_sym_it->second.symbol_expr();
210  init_body.move_to_operands(call_real_init);
211  }
212 }
213 
220  const irep_idt &class_name, const symbol_tablet &symbol_table)
221 {
222  if(symbol_table.has_symbol(clinit_function_name(class_name)))
223  return true;
224 
225  const class_typet &class_type =
226  to_class_type(symbol_table.lookup_ref(class_name).type);
227 
228  for(const class_typet::baset &base : class_type.bases())
229  {
230  if(symbol_table.has_symbol(
231  clinit_wrapper_name(to_symbol_type(base.type()).get_identifier())))
232  {
233  return true;
234  }
235  }
236 
237  return false;
238 }
239 
251  const irep_idt &class_name,
252  symbol_tablet &symbol_table,
253  synthetic_methods_mapt &synthetic_methods,
254  const bool thread_safe)
255 {
256  if(thread_safe)
257  {
258  exprt not_init_value = from_integer(
259  static_cast<int>(clinit_statest::NOT_INIT), clinit_states_type);
260 
261  // Create two global static synthetic "fields" for the class "id"
262  // these two variables hold the state of the class initialization algorithm
263  // across calls to the clinit_wrapper
265  symbol_table,
266  clinit_state_var_name(class_name),
268  not_init_value,
269  false,
270  true);
271 
273  symbol_table,
276  not_init_value,
277  true,
278  true);
279  }
280  else
281  {
282  const irep_idt &already_run_name =
284 
286  symbol_table,
287  already_run_name,
288  bool_typet(),
289  false_exprt(),
290  false,
291  true);
292  }
293 
294  // Create symbol for the "clinit_wrapper"
295  symbolt wrapper_method_symbol;
296  const code_typet wrapper_method_type({}, void_typet());
297  wrapper_method_symbol.name = clinit_wrapper_name(class_name);
298  wrapper_method_symbol.pretty_name = wrapper_method_symbol.name;
299  wrapper_method_symbol.base_name = "clinit_wrapper";
300  wrapper_method_symbol.type = wrapper_method_type;
301  // Note this use of a type-comment to provide a back-link from a method
302  // to its associated class is the same one used in
303  // java_bytecode_convert_methodt::convert
304  wrapper_method_symbol.type.set(ID_C_class, class_name);
305  wrapper_method_symbol.mode = ID_java;
306  bool failed = symbol_table.add(wrapper_method_symbol);
307  INVARIANT(!failed, "clinit-wrapper symbol should be fresh");
308 
309  auto insert_result = synthetic_methods.emplace(
310  wrapper_method_symbol.name,
312  INVARIANT(
313  insert_result.second,
314  "synthetic methods map should not already contain entry for "
315  "clinit wrapper");
316 }
317 
386  const irep_idt &function_id,
387  symbol_table_baset &symbol_table)
388 {
389  const symbolt &wrapper_method_symbol = symbol_table.lookup_ref(function_id);
390  irep_idt class_name = wrapper_method_symbol.type.get(ID_C_class);
391  INVARIANT(
392  !class_name.empty(), "wrapper function should be annotated with its class");
393 
394  const symbolt &clinit_state_sym =
395  symbol_table.lookup_ref(clinit_state_var_name(class_name));
396  const symbolt &clinit_thread_local_state_sym =
397  symbol_table.lookup_ref(clinit_thread_local_state_var_name(class_name));
398 
399  // Create a function-local variable "init_complete". This variable is used to
400  // avoid inspecting the global state (clinit_state_sym) outside of
401  // the critical-section.
402  const symbolt &init_complete = add_new_variable_symbol(
403  symbol_table,
405  bool_typet(),
406  nil_exprt(),
407  true,
408  false);
409 
410  code_blockt function_body;
411  codet atomic_begin(ID_atomic_begin);
412  codet atomic_end(ID_atomic_end);
413 
414 #if 0
415  // This code defines source locations for every codet generated below for
416  // the static initializer wrapper. Enable this for debugging the symex going
417  // through the clinit_wrapper.
418  //
419  // java::C::clinit_wrapper()
420  // You will additionally need to associate the `location` with the
421  // `function_body` and then manually set lines of code for each of the
422  // statements of the function, using something along the lines of:
423  // `mycodet.then_case().add_source_location().set_line(17);`/
424 
425  source_locationt &location = function_body.add_source_location();
426  location.set_file ("<generated>");
427  location.set_line ("<generated>");
429  std::string comment =
430  "Automatically generated function. States are:\n"
431  " 0 = class not initialized, init val of clinit_state/clinit_local_state\n"
432  " 1 = class initialization in progress, by this or another thread\n"
433  " 2 = initialization finished with success, by this or another thread\n";
434  static_assert((int) clinit_statest::NOT_INIT==0, "Check commment above");
435  static_assert((int) clinit_statest::IN_PROGRESS==1, "Check comment above");
436  static_assert((int) clinit_statest::INIT_COMPLETE==2, "Check comment above");
437 #endif
438 
439  // bool init_complete;
440  {
441  code_declt decl(init_complete.symbol_expr());
442  function_body.add(decl);
443  }
444 
445  // if(C::__CPROVER_PREFIX_clinit_thread_local_state == INIT_COMPLETE) return;
446  {
447  code_ifthenelset conditional;
448  conditional.cond() = gen_clinit_eqexpr(
449  clinit_thread_local_state_sym.symbol_expr(),
451  conditional.then_case() = code_returnt();
452  function_body.add(conditional);
453  }
454 
455  // C::__CPROVER_PREFIX_clinit_thread_local_state = INIT_COMPLETE;
456  {
458  clinit_thread_local_state_sym.symbol_expr(),
460  function_body.add(assign);
461  }
462 
463  // ATOMIC_BEGIN
464  {
465  function_body.add(atomic_begin);
466  }
467 
468  // Assume: clinit_state_sym != IN_PROGRESS
469  {
470  exprt assumption = gen_clinit_eqexpr(
471  clinit_state_sym.symbol_expr(), clinit_statest::IN_PROGRESS);
472  assumption = not_exprt(assumption);
473  code_assumet assume(assumption);
474  function_body.add(assume);
475  }
476 
477  // If(C::__CPROVER_PREFIX_clinit_state == NOT_INIT)
478  // {
479  // C::__CPROVER_PREFIX_clinit_state = IN_PROGRESS;
480  // init_complete = false;
481  // }
482  // else If(C::__CPROVER_PREFIX_clinit_state == INIT_COMPLETE)
483  // {
484  // init_complete = true;
485  // }
486  {
487  code_ifthenelset not_init_conditional;
488  code_blockt then_block;
489  not_init_conditional.cond() = gen_clinit_eqexpr(
490  clinit_state_sym.symbol_expr(), clinit_statest::NOT_INIT);
491  then_block.add(
493  clinit_state_sym.symbol_expr(), clinit_statest::IN_PROGRESS));
494  then_block.add(code_assignt(init_complete.symbol_expr(), false_exprt()));
495  not_init_conditional.then_case() = then_block;
496 
497  code_ifthenelset init_conditional;
498  code_blockt init_conditional_body;
499  init_conditional.cond() = gen_clinit_eqexpr(
500  clinit_state_sym.symbol_expr(), clinit_statest::INIT_COMPLETE);
501  init_conditional_body.add(
502  code_assignt(init_complete.symbol_expr(), true_exprt()));
503  init_conditional.then_case() = init_conditional_body;
504  not_init_conditional.else_case() = init_conditional;
505  function_body.add(not_init_conditional);
506  }
507 
508  // ATOMIC_END
509  {
510  function_body.add(atomic_end);
511  }
512 
513  // if(init_complete) return;
514  {
515  code_ifthenelset conditional;
516  conditional.cond() = init_complete.symbol_expr();
517  conditional.then_case() = code_returnt();
518  function_body.add(conditional);
519  }
520 
521  // Initialize the super-class C' and
522  // the implemented interfaces l_1 ... l_n.
523  // see JVMS p.359 step 7, for the exact definition of
524  // the sequence l_1 to l_n.
525  // This is achieved by iterating through the base types and
526  // adding recursive calls to the clinit_wrapper()
527  //
528  // java::C'::clinit_wrapper();
529  // java::I1::clinit_wrapper();
530  // java::I2::clinit_wrapper();
531  // // ...
532  // java::In::clinit_wrapper();
533  //
534  // java::C::<clinit>();
535  //
536  {
537  code_blockt init_body;
538  clinit_wrapper_do_recursive_calls(symbol_table, class_name, init_body);
539  function_body.append(init_body);
540  }
541 
542  // ATOMIC_START
543  // C::__CPROVER_PREFIX_clinit_state = INIT_COMPLETE;
544  // ATOMIC_END
545  // return;
546  {
547  // synchronization prologue
548  function_body.add(atomic_begin);
549  function_body.add(
551  clinit_state_sym.symbol_expr(), clinit_statest::INIT_COMPLETE));
552  function_body.add(atomic_end);
553  function_body.add(code_returnt());
554  }
555 
556  return function_body;
557 }
558 
566  const irep_idt &function_id,
567  symbol_table_baset &symbol_table)
568 {
569  // Assume that class C extends class C' and implements interfaces
570  // I1, ..., In. We now create the following function (possibly recursively
571  // creating the clinit_wrapper functions for C' and I1, ..., In):
572  //
573  // java::C::clinit_wrapper()
574  // {
575  // if (java::C::clinit_already_run == false)
576  // {
577  // java::C::clinit_already_run = true; // before recursive calls!
578  //
579  // java::C'::clinit_wrapper();
580  // java::I1::clinit_wrapper();
581  // java::I2::clinit_wrapper();
582  // // ...
583  // java::In::clinit_wrapper();
584  //
585  // java::C::<clinit>();
586  // }
587  // }
588  const symbolt &wrapper_method_symbol = symbol_table.lookup_ref(function_id);
589  irep_idt class_name = wrapper_method_symbol.type.get(ID_C_class);
590  INVARIANT(
591  !class_name.empty(), "wrapper function should be annotated with its class");
592 
593  const symbolt &already_run_symbol =
594  symbol_table.lookup_ref(clinit_already_run_variable_name(class_name));
595 
596  equal_exprt check_already_run(
597  already_run_symbol.symbol_expr(),
598  false_exprt());
599 
600  // the entire body of the function is an if-then-else
601  code_ifthenelset wrapper_body;
602 
603  // add the condition to the if
604  wrapper_body.cond() = check_already_run;
605 
606  // add the "already-run = false" statement
607  code_blockt init_body;
608  code_assignt set_already_run(already_run_symbol.symbol_expr(), true_exprt());
609  init_body.move_to_operands(set_already_run);
610 
611  clinit_wrapper_do_recursive_calls(symbol_table, class_name, init_body);
612 
613  wrapper_body.then_case() = init_body;
614 
615  return wrapper_body;
616 }
617 
618 
627  symbol_tablet &symbol_table,
628  synthetic_methods_mapt &synthetic_methods,
629  const bool thread_safe)
630 {
631  // Top-sort the class hierarchy, such that we visit parents before children,
632  // and can so identify parents that need static initialisation by whether we
633  // have made them a clinit_wrapper method.
634  class_hierarchy_grapht class_graph;
635  class_graph.populate(symbol_table);
636  std::list<class_hierarchy_grapht::node_indext> topsorted_nodes =
637  class_graph.topsort();
638 
639  for(const auto node : topsorted_nodes)
640  {
641  const irep_idt &class_identifier = class_graph[node].class_identifier;
642  if(needs_clinit_wrapper(class_identifier, symbol_table))
643  {
645  class_identifier, symbol_table, synthetic_methods, thread_safe);
646  }
647  }
648 }
649 
653 template<class itertype>
654 static itertype advance_to_next_key(itertype in, itertype end)
655 {
656  PRECONDITION(in != end);
657  auto initial_key = in->first;
658  while(in != end && in->first == initial_key)
659  ++in;
660  return in;
661 }
662 
672  symbol_tablet &symbol_table,
673  const std::unordered_set<irep_idt> &stub_globals_set,
674  synthetic_methods_mapt &synthetic_methods)
675 {
676  // Populate map from class id -> stub globals:
677  for(const irep_idt &stub_global : stub_globals_set)
678  {
679  const symbolt &global_symbol = symbol_table.lookup_ref(stub_global);
680  if(global_symbol.value.is_nil())
681  {
682  // This symbol is already nondet-initialised during __CPROVER_initialize
683  // (generated in java_static_lifetime_init). In future this will only
684  // be the case for primitive-typed fields, but for now reference-typed
685  // fields can also be treated this way in the exceptional case that they
686  // belong to a non-stub class. Skip the field, as it does not need a
687  // synthetic static initializer.
688  continue;
689  }
690 
691  const irep_idt class_id =
692  global_symbol.type.get(ID_C_class);
693  INVARIANT(
694  !class_id.empty(),
695  "static field should be annotated with its defining class");
696  stub_globals_by_class.insert({class_id, stub_global});
697  }
698 
699  // For each distinct class that has stub globals, create a clinit symbol:
700 
701  for(auto it = stub_globals_by_class.begin(),
702  itend = stub_globals_by_class.end();
703  it != itend;
704  it = advance_to_next_key(it, itend))
705  {
706  const irep_idt static_init_name = clinit_function_name(it->first);
707 
708  INVARIANT(
709  symbol_table.lookup_ref(it->first).type.get_bool(ID_incomplete_class),
710  "only incomplete classes should be given synthetic static initialisers");
711  INVARIANT(
712  !symbol_table.has_symbol(static_init_name),
713  "a class cannot be both incomplete, and so have stub static fields, and "
714  "also define a static initializer");
715 
716  const code_typet thunk_type({}, void_typet());
717 
718  symbolt static_init_symbol;
719  static_init_symbol.name = static_init_name;
720  static_init_symbol.pretty_name = static_init_name;
721  static_init_symbol.base_name = "clinit():V";
722  static_init_symbol.mode = ID_java;
723  static_init_symbol.type = thunk_type;
724  // Note this use of a type-comment to provide a back-link from a method
725  // to its associated class is the same one used in
726  // java_bytecode_convert_methodt::convert
727  static_init_symbol.type.set(ID_C_class, it->first);
728 
729  bool failed = symbol_table.add(static_init_symbol);
730  INVARIANT(!failed, "symbol should not already exist");
731 
732  auto insert_result = synthetic_methods.emplace(
733  static_init_symbol.name,
735  INVARIANT(
736  insert_result.second,
737  "synthetic methods map should not already contain entry for "
738  "stub static initializer");
739  }
740 }
741 
756  const irep_idt &function_id,
757  symbol_table_baset &symbol_table,
758  const object_factory_parameterst &object_factory_parameters,
759  const select_pointer_typet &pointer_type_selector)
760 {
761  const symbolt &stub_initializer_symbol = symbol_table.lookup_ref(function_id);
762  irep_idt class_id = stub_initializer_symbol.type.get(ID_C_class);
763  INVARIANT(
764  !class_id.empty(),
765  "synthetic static initializer should be annotated with its class");
766  code_blockt static_init_body;
767 
768  // Add a standard nondet initialisation for each global declared on this
769  // class. Note this is the same invocation used in
770  // java_static_lifetime_init.
771 
772  auto class_globals = stub_globals_by_class.equal_range(class_id);
773  INVARIANT(
774  class_globals.first != class_globals.second,
775  "class with synthetic clinit should have at least one global to init");
776 
777  object_factory_parameterst parameters = object_factory_parameters;
778  parameters.function_id = function_id;
779 
780  for(auto it = class_globals.first; it != class_globals.second; ++it)
781  {
782  const symbol_exprt new_global_symbol =
783  symbol_table.lookup_ref(it->second).symbol_expr();
784 
785  parameters.max_nonnull_tree_depth =
786  is_non_null_library_global(it->second)
787  ? object_factory_parameters.max_nonnull_tree_depth + 1
788  : object_factory_parameters.max_nonnull_tree_depth;
789 
791  new_global_symbol,
792  static_init_body,
793  symbol_table,
795  false,
797  parameters,
798  pointer_type_selector,
800  }
801 
802  return static_init_body;
803 }
The void type.
Definition: std_types.h:64
The type of an expression.
Definition: type.h:22
irep_idt name
The unique identifier.
Definition: symbol.h:43
irep_idt function_id
Function id, used as a prefix for identifiers of temporaries.
const codet & then_case() const
Definition: std_code.h:481
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.
Boolean negation.
Definition: std_expr.h:3230
void set_function(const irep_idt &function)
BigInt mp_integer
Definition: mp_arith.h:22
A static initializer wrapper (code of the form if(!already_run) clinit(); already_run = true;) These ...
Base type of functions.
Definition: std_types.h:764
bool is_nil() const
Definition: irep.h:102
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
bool is_thread_local
Definition: symbol.h:67
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
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...
#define CPROVER_PREFIX
This module is responsible for the synthesis of code (in the form of a sequence of codet statements) ...
irep_idt mode
Language mode.
Definition: symbol.h:52
std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:107
const exprt & cond() const
Definition: std_code.h:471
void populate(const symbol_tablet &)
Populate the class hierarchy graph, such that there is a node for every struct type in the symbol tab...
void move_to_operands(exprt &expr)
Definition: expr.cpp:22
static irep_idt clinit_function_name(const irep_idt &class_name)
Get name of the real static initializer for a given class.
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
Definition: std_types.h:139
exprt value
Initial value of symbol.
Definition: symbol.h:37
codet get_thread_safe_clinit_wrapper_body(const irep_idt &function_id, symbol_table_baset &symbol_table)
Thread safe version of the static initialiser.
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:55
const class_typet & to_class_type(const typet &type)
Cast a generic typet to a class_typet.
Definition: std_types.h:435
The proper Booleans.
Definition: std_types.h:34
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
A constant literal expression.
Definition: std_expr.h:4424
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.
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
codet get_clinit_wrapper_body(const irep_idt &function_id, symbol_table_baset &symbol_table)
Produces the static initialiser wrapper body for the given function.
bool is_static_lifetime
Definition: symbol.h:67
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:205
equality
Definition: std_expr.h:1354
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.
Class Hierarchy.
const typet clinit_states_type
void add(const codet &code)
Definition: std_code.h:111
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:111
The boolean constant true.
Definition: std_expr.h:4488
A declaration of a local variable.
Definition: std_code.h:253
const std::string clinit_function_suffix
The NIL expression.
Definition: std_expr.h:4510
Class hierarchy, represented using grapht and therefore suitable for use with generic graph algorithm...
void set_file(const irep_idt &file)
API to expression classes.
static itertype advance_to_next_key(itertype in, itertype end)
Advance map iterator to next distinct key.
The symbol table.
Definition: symbol_table.h:19
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
void set_line(const irep_idt &line)
codet get_stub_initializer_body(const irep_idt &function_id, symbol_table_baset &symbol_table, const 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...
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
Definition: std_code.cpp:101
#define PRECONDITION(CONDITION)
Definition: invariant.h:230
A function call.
Definition: std_code.h:828
typet java_byte_type()
Definition: java_types.cpp:52
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:699
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.
const std::string clinit_wrapper_suffix
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:421
const symbolst & symbols
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
The boolean constant false.
Definition: std_expr.h:4499
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.
static void clinit_wrapper_do_recursive_calls(const symbol_tablet &symbol_table, const irep_idt &class_name, code_blockt &init_body)
Generates codet that iterates through the base types of the class specified by class_name, C, and recursively adds calls to their clinit wrapper.
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.
An assumption, which must hold in subsequent code.
Definition: std_code.h:354
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.
typet type
Type of symbol.
Definition: symbol.h:34
API to type classes.
Allocate dynamic objects (using MALLOC)
stub_globals_by_classt stub_globals_by_class
exprt & function()
Definition: std_code.h:848
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...
Base class for all expressions.
Definition: expr.h:42
bool is_state_var
Definition: symbol.h:63
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:49
The symbol table base class interface.
clinit_statest
The three states in which a <clinit> method for a class can be before, after, and during static class...
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 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...
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.
const basest & bases() const
Definition: std_types.h:386
source_locationt & add_source_location()
Definition: expr.h:130
Sequential composition.
Definition: std_code.h:88
An if-then-else.
Definition: std_code.h:461
Expression to hold a symbol (variable)
Definition: std_expr.h:90
std::unordered_map< irep_idt, synthetic_method_typet > synthetic_methods_mapt
Maps method names on to a synthetic method kind.
A generated (synthetic) static initializer function for a stub type.
bool has_suffix(const std::string &s, const std::string &suffix)
Definition: suffix.h:15
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
A statement in a programming language.
Definition: std_code.h:21
Return from a function.
Definition: std_code.h:893
C++ class type.
Definition: std_types.h:341
bool is_clinit_wrapper_function(const irep_idt &function_id)
Check if function_id is a clinit wrapper.
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
const codet & else_case() const
Definition: std_code.h:491
bool empty() const
Definition: dstring.h:61
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...
Assignment.
Definition: std_code.h:195
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
size_t max_nonnull_tree_depth
To force a certain depth of non-null objects.
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...
bool is_lvalue
Definition: symbol.h:68