cprover
java_static_initializers.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Java Static Initializers
4 
5 Author: Chris Smowton, chris.smowton@diffblue.com
6 
7 \*******************************************************************/
8 
10 #include "java_object_factory.h"
11 #include "java_utils.h"
13 #include <util/std_types.h>
14 #include <util/std_expr.h>
15 #include <util/std_code.h>
16 #include <util/suffix.h>
17 #include <util/arith_tools.h>
18 
40 enum class clinit_statest
41 {
42  NOT_INIT,
45 };
46 
48 
49 // Disable linter here to allow a std::string constant, since that holds
50 // a length, whereas a cstr would require strlen every time.
51 const std::string clinit_wrapper_suffix = "::clinit_wrapper"; // NOLINT(*)
52 const std::string clinit_function_suffix = ".<clinit>:()V"; // NOLINT(*)
53 
61 {
62  return id2string(class_name) + clinit_wrapper_suffix;
63 }
64 
68 bool is_clinit_wrapper_function(const irep_idt &function_id)
69 {
70  return has_suffix(id2string(function_id), clinit_wrapper_suffix);
71 }
72 
82  symbol_table_baset &symbol_table,
83  const irep_idt &name,
84  const typet &type,
85  const exprt &value,
86  const bool is_thread_local,
87  const bool is_static_lifetime)
88 {
89  symbolt new_symbol;
90  new_symbol.name = name;
91  new_symbol.pretty_name = name;
92  new_symbol.base_name = name;
93  new_symbol.type = type;
94  new_symbol.type.set(ID_C_no_nondet_initialization, true);
95  new_symbol.value = value;
96  new_symbol.is_lvalue = true;
97  new_symbol.is_state_var = true;
98  new_symbol.is_static_lifetime = is_static_lifetime;
99  new_symbol.is_thread_local = is_thread_local;
100  new_symbol.mode = ID_java;
101  symbol_table.add(new_symbol);
102  return new_symbol;
103 }
104 
110 {
111  return id2string(class_name) + "::clinit_already_run";
112 }
113 
118 static irep_idt clinit_function_name(const irep_idt &class_name)
119 {
120  return id2string(class_name) + clinit_function_suffix;
121 }
122 
127 static irep_idt clinit_state_var_name(const irep_idt &class_name)
128 {
129  return id2string(class_name) + CPROVER_PREFIX "clinit_state";
130 }
131 
137 {
138  return id2string(class_name) + CPROVER_PREFIX "clinit_threadlocal_state";
139 }
140 
145 {
146  return id2string(class_name) + CPROVER_PREFIX "clinit_wrapper::init_complete";
147 }
148 
157 static code_assignt
158 gen_clinit_assign(const exprt &expr, const clinit_statest state)
159 {
160  mp_integer initv(static_cast<int>(state));
162  return code_assignt(expr, init_s);
163 }
164 
173 static equal_exprt
174 gen_clinit_eqexpr(const exprt &expr, const clinit_statest state)
175 {
176  mp_integer initv(static_cast<int>(state));
178  return equal_exprt(expr, init_s);
179 }
180 
188  const symbol_tablet &symbol_table,
189  const irep_idt &class_name,
190  code_blockt &init_body)
191 {
192  const symbolt &class_symbol = symbol_table.lookup_ref(class_name);
193  for(const auto &base : to_class_type(class_symbol.type).bases())
194  {
195  const auto base_name = to_symbol_type(base.type()).get_identifier();
196  irep_idt base_init_routine = clinit_wrapper_name(base_name);
197  auto findit = symbol_table.symbols.find(base_init_routine);
198  if(findit == symbol_table.symbols.end())
199  continue;
200  code_function_callt call_base;
201  call_base.function() = findit->second.symbol_expr();
202  init_body.move_to_operands(call_base);
203  }
204 
205  const irep_idt &real_clinit_name = clinit_function_name(class_name);
206  auto find_sym_it = symbol_table.symbols.find(real_clinit_name);
207  if(find_sym_it != symbol_table.symbols.end())
208  {
209  code_function_callt call_real_init;
210  call_real_init.function() = find_sym_it->second.symbol_expr();
211  init_body.move_to_operands(call_real_init);
212  }
213 }
214 
221  const irep_idt &class_name, const symbol_tablet &symbol_table)
222 {
223  if(symbol_table.has_symbol(clinit_function_name(class_name)))
224  return true;
225 
226  const class_typet &class_type =
227  to_class_type(symbol_table.lookup_ref(class_name).type);
228 
229  for(const class_typet::baset &base : class_type.bases())
230  {
231  if(symbol_table.has_symbol(
232  clinit_wrapper_name(to_symbol_type(base.type()).get_identifier())))
233  {
234  return true;
235  }
236  }
237 
238  return false;
239 }
240 
252  const irep_idt &class_name,
253  symbol_tablet &symbol_table,
254  synthetic_methods_mapt &synthetic_methods,
255  const bool thread_safe)
256 {
257  if(thread_safe)
258  {
259  exprt not_init_value = from_integer(
260  static_cast<int>(clinit_statest::NOT_INIT), clinit_states_type);
261 
262  // Create two global static synthetic "fields" for the class "id"
263  // these two variables hold the state of the class initialization algorithm
264  // across calls to the clinit_wrapper
266  symbol_table,
267  clinit_state_var_name(class_name),
269  not_init_value,
270  false,
271  true);
272 
274  symbol_table,
277  not_init_value,
278  true,
279  true);
280  }
281  else
282  {
283  const irep_idt &already_run_name =
285 
287  symbol_table,
288  already_run_name,
289  bool_typet(),
290  false_exprt(),
291  false,
292  true);
293  }
294 
295  // Create symbol for the "clinit_wrapper"
296  symbolt wrapper_method_symbol;
297  const java_method_typet wrapper_method_type({}, void_typet());
298  wrapper_method_symbol.name = clinit_wrapper_name(class_name);
299  wrapper_method_symbol.pretty_name = wrapper_method_symbol.name;
300  wrapper_method_symbol.base_name = "clinit_wrapper";
301  wrapper_method_symbol.type = wrapper_method_type;
302  // Note this use of a type-comment to provide a back-link from a method
303  // to its associated class is the same one used in
304  // java_bytecode_convert_methodt::convert
305  wrapper_method_symbol.type.set(ID_C_class, class_name);
306  wrapper_method_symbol.mode = ID_java;
307  bool failed = symbol_table.add(wrapper_method_symbol);
308  INVARIANT(!failed, "clinit-wrapper symbol should be fresh");
309 
310  auto insert_result = synthetic_methods.emplace(
311  wrapper_method_symbol.name,
313  INVARIANT(
314  insert_result.second,
315  "synthetic methods map should not already contain entry for "
316  "clinit wrapper");
317 }
318 
387  const irep_idt &function_id,
388  symbol_table_baset &symbol_table)
389 {
390  const symbolt &wrapper_method_symbol = symbol_table.lookup_ref(function_id);
391  irep_idt class_name = wrapper_method_symbol.type.get(ID_C_class);
392  INVARIANT(
393  !class_name.empty(), "wrapper function should be annotated with its class");
394 
395  const symbolt &clinit_state_sym =
396  symbol_table.lookup_ref(clinit_state_var_name(class_name));
397  const symbolt &clinit_thread_local_state_sym =
398  symbol_table.lookup_ref(clinit_thread_local_state_var_name(class_name));
399 
400  // Create a function-local variable "init_complete". This variable is used to
401  // avoid inspecting the global state (clinit_state_sym) outside of
402  // the critical-section.
403  const symbolt &init_complete = add_new_variable_symbol(
404  symbol_table,
406  bool_typet(),
407  nil_exprt(),
408  true,
409  false);
410 
411  code_blockt function_body;
412  codet atomic_begin(ID_atomic_begin);
413  codet atomic_end(ID_atomic_end);
414 
415 #if 0
416  // This code defines source locations for every codet generated below for
417  // the static initializer wrapper. Enable this for debugging the symex going
418  // through the clinit_wrapper.
419  //
420  // java::C::clinit_wrapper()
421  // You will additionally need to associate the `location` with the
422  // `function_body` and then manually set lines of code for each of the
423  // statements of the function, using something along the lines of:
424  // `mycodet.then_case().add_source_location().set_line(17);`/
425 
426  source_locationt &location = function_body.add_source_location();
427  location.set_file ("<generated>");
428  location.set_line ("<generated>");
430  std::string comment =
431  "Automatically generated function. States are:\n"
432  " 0 = class not initialized, init val of clinit_state/clinit_local_state\n"
433  " 1 = class initialization in progress, by this or another thread\n"
434  " 2 = initialization finished with success, by this or another thread\n";
435  static_assert((int) clinit_statest::NOT_INIT==0, "Check commment above");
436  static_assert((int) clinit_statest::IN_PROGRESS==1, "Check comment above");
437  static_assert((int) clinit_statest::INIT_COMPLETE==2, "Check comment above");
438 #endif
439 
440  // bool init_complete;
441  {
442  code_declt decl(init_complete.symbol_expr());
443  function_body.add(decl);
444  }
445 
446  // if(C::__CPROVER_PREFIX_clinit_thread_local_state == INIT_COMPLETE) return;
447  {
448  code_ifthenelset conditional;
449  conditional.cond() = gen_clinit_eqexpr(
450  clinit_thread_local_state_sym.symbol_expr(),
452  conditional.then_case() = code_returnt();
453  function_body.add(conditional);
454  }
455 
456  // C::__CPROVER_PREFIX_clinit_thread_local_state = INIT_COMPLETE;
457  {
459  clinit_thread_local_state_sym.symbol_expr(),
461  function_body.add(assign);
462  }
463 
464  // ATOMIC_BEGIN
465  {
466  function_body.add(atomic_begin);
467  }
468 
469  // Assume: clinit_state_sym != IN_PROGRESS
470  {
471  exprt assumption = gen_clinit_eqexpr(
472  clinit_state_sym.symbol_expr(), clinit_statest::IN_PROGRESS);
473  assumption = not_exprt(assumption);
474  code_assumet assume(assumption);
475  function_body.add(assume);
476  }
477 
478  // If(C::__CPROVER_PREFIX_clinit_state == NOT_INIT)
479  // {
480  // C::__CPROVER_PREFIX_clinit_state = IN_PROGRESS;
481  // init_complete = false;
482  // }
483  // else If(C::__CPROVER_PREFIX_clinit_state == INIT_COMPLETE)
484  // {
485  // init_complete = true;
486  // }
487  {
488  code_ifthenelset not_init_conditional;
489  code_blockt then_block;
490  not_init_conditional.cond() = gen_clinit_eqexpr(
491  clinit_state_sym.symbol_expr(), clinit_statest::NOT_INIT);
492  then_block.add(
494  clinit_state_sym.symbol_expr(), clinit_statest::IN_PROGRESS));
495  then_block.add(code_assignt(init_complete.symbol_expr(), false_exprt()));
496  not_init_conditional.then_case() = then_block;
497 
498  code_ifthenelset init_conditional;
499  code_blockt init_conditional_body;
500  init_conditional.cond() = gen_clinit_eqexpr(
501  clinit_state_sym.symbol_expr(), clinit_statest::INIT_COMPLETE);
502  init_conditional_body.add(
503  code_assignt(init_complete.symbol_expr(), true_exprt()));
504  init_conditional.then_case() = init_conditional_body;
505  not_init_conditional.else_case() = init_conditional;
506  function_body.add(not_init_conditional);
507  }
508 
509  // ATOMIC_END
510  {
511  function_body.add(atomic_end);
512  }
513 
514  // if(init_complete) return;
515  {
516  code_ifthenelset conditional;
517  conditional.cond() = init_complete.symbol_expr();
518  conditional.then_case() = code_returnt();
519  function_body.add(conditional);
520  }
521 
522  // Initialize the super-class C' and
523  // the implemented interfaces l_1 ... l_n.
524  // see JVMS p.359 step 7, for the exact definition of
525  // the sequence l_1 to l_n.
526  // This is achieved by iterating through the base types and
527  // adding recursive calls to the clinit_wrapper()
528  //
529  // java::C'::clinit_wrapper();
530  // java::I1::clinit_wrapper();
531  // java::I2::clinit_wrapper();
532  // // ...
533  // java::In::clinit_wrapper();
534  //
535  // java::C::<clinit>();
536  //
537  {
538  code_blockt init_body;
539  clinit_wrapper_do_recursive_calls(symbol_table, class_name, init_body);
540  function_body.append(init_body);
541  }
542 
543  // ATOMIC_START
544  // C::__CPROVER_PREFIX_clinit_state = INIT_COMPLETE;
545  // ATOMIC_END
546  // return;
547  {
548  // synchronization prologue
549  function_body.add(atomic_begin);
550  function_body.add(
552  clinit_state_sym.symbol_expr(), clinit_statest::INIT_COMPLETE));
553  function_body.add(atomic_end);
554  function_body.add(code_returnt());
555  }
556 
557  return function_body;
558 }
559 
567  const irep_idt &function_id,
568  symbol_table_baset &symbol_table)
569 {
570  // Assume that class C extends class C' and implements interfaces
571  // I1, ..., In. We now create the following function (possibly recursively
572  // creating the clinit_wrapper functions for C' and I1, ..., In):
573  //
574  // java::C::clinit_wrapper()
575  // {
576  // if (java::C::clinit_already_run == false)
577  // {
578  // java::C::clinit_already_run = true; // before recursive calls!
579  //
580  // java::C'::clinit_wrapper();
581  // java::I1::clinit_wrapper();
582  // java::I2::clinit_wrapper();
583  // // ...
584  // java::In::clinit_wrapper();
585  //
586  // java::C::<clinit>();
587  // }
588  // }
589  const symbolt &wrapper_method_symbol = symbol_table.lookup_ref(function_id);
590  irep_idt class_name = wrapper_method_symbol.type.get(ID_C_class);
591  INVARIANT(
592  !class_name.empty(), "wrapper function should be annotated with its class");
593 
594  const symbolt &already_run_symbol =
595  symbol_table.lookup_ref(clinit_already_run_variable_name(class_name));
596 
597  equal_exprt check_already_run(
598  already_run_symbol.symbol_expr(),
599  false_exprt());
600 
601  // the entire body of the function is an if-then-else
602  code_ifthenelset wrapper_body;
603 
604  // add the condition to the if
605  wrapper_body.cond() = check_already_run;
606 
607  // add the "already-run = false" statement
608  code_blockt init_body;
609  code_assignt set_already_run(already_run_symbol.symbol_expr(), true_exprt());
610  init_body.move_to_operands(set_already_run);
611 
612  clinit_wrapper_do_recursive_calls(symbol_table, class_name, init_body);
613 
614  wrapper_body.then_case() = init_body;
615 
616  return wrapper_body;
617 }
618 
619 
628  symbol_tablet &symbol_table,
629  synthetic_methods_mapt &synthetic_methods,
630  const bool thread_safe)
631 {
632  // Top-sort the class hierarchy, such that we visit parents before children,
633  // and can so identify parents that need static initialisation by whether we
634  // have made them a clinit_wrapper method.
635  class_hierarchy_grapht class_graph;
636  class_graph.populate(symbol_table);
637  std::list<class_hierarchy_grapht::node_indext> topsorted_nodes =
638  class_graph.topsort();
639 
640  for(const auto node : topsorted_nodes)
641  {
642  const irep_idt &class_identifier = class_graph[node].class_identifier;
643  if(needs_clinit_wrapper(class_identifier, symbol_table))
644  {
646  class_identifier, symbol_table, synthetic_methods, thread_safe);
647  }
648  }
649 }
650 
654 template<class itertype>
655 static itertype advance_to_next_key(itertype in, itertype end)
656 {
657  PRECONDITION(in != end);
658  auto initial_key = in->first;
659  while(in != end && in->first == initial_key)
660  ++in;
661  return in;
662 }
663 
673  symbol_tablet &symbol_table,
674  const std::unordered_set<irep_idt> &stub_globals_set,
675  synthetic_methods_mapt &synthetic_methods)
676 {
677  // Populate map from class id -> stub globals:
678  for(const irep_idt &stub_global : stub_globals_set)
679  {
680  const symbolt &global_symbol = symbol_table.lookup_ref(stub_global);
681  if(global_symbol.value.is_nil())
682  {
683  // This symbol is already nondet-initialised during __CPROVER_initialize
684  // (generated in java_static_lifetime_init). In future this will only
685  // be the case for primitive-typed fields, but for now reference-typed
686  // fields can also be treated this way in the exceptional case that they
687  // belong to a non-stub class. Skip the field, as it does not need a
688  // synthetic static initializer.
689  continue;
690  }
691 
692  const irep_idt class_id =
693  global_symbol.type.get(ID_C_class);
694  INVARIANT(
695  !class_id.empty(),
696  "static field should be annotated with its defining class");
697  stub_globals_by_class.insert({class_id, stub_global});
698  }
699 
700  // For each distinct class that has stub globals, create a clinit symbol:
701 
702  for(auto it = stub_globals_by_class.begin(),
703  itend = stub_globals_by_class.end();
704  it != itend;
705  it = advance_to_next_key(it, itend))
706  {
707  const irep_idt static_init_name = clinit_function_name(it->first);
708 
709  INVARIANT(
710  symbol_table.lookup_ref(it->first).type.get_bool(ID_incomplete_class),
711  "only incomplete classes should be given synthetic static initialisers");
712  INVARIANT(
713  !symbol_table.has_symbol(static_init_name),
714  "a class cannot be both incomplete, and so have stub static fields, and "
715  "also define a static initializer");
716 
717  const java_method_typet thunk_type({}, void_typet());
718 
719  symbolt static_init_symbol;
720  static_init_symbol.name = static_init_name;
721  static_init_symbol.pretty_name = static_init_name;
722  static_init_symbol.base_name = "clinit():V";
723  static_init_symbol.mode = ID_java;
724  static_init_symbol.type = thunk_type;
725  // Note this use of a type-comment to provide a back-link from a method
726  // to its associated class is the same one used in
727  // java_bytecode_convert_methodt::convert
728  static_init_symbol.type.set(ID_C_class, it->first);
729 
730  bool failed = symbol_table.add(static_init_symbol);
731  INVARIANT(!failed, "symbol should not already exist");
732 
733  auto insert_result = synthetic_methods.emplace(
734  static_init_symbol.name,
736  INVARIANT(
737  insert_result.second,
738  "synthetic methods map should not already contain entry for "
739  "stub static initializer");
740  }
741 }
742 
757  const irep_idt &function_id,
758  symbol_table_baset &symbol_table,
759  const object_factory_parameterst &object_factory_parameters,
760  const select_pointer_typet &pointer_type_selector)
761 {
762  const symbolt &stub_initializer_symbol = symbol_table.lookup_ref(function_id);
763  irep_idt class_id = stub_initializer_symbol.type.get(ID_C_class);
764  INVARIANT(
765  !class_id.empty(),
766  "synthetic static initializer should be annotated with its class");
767  code_blockt static_init_body;
768 
769  // Add a standard nondet initialisation for each global declared on this
770  // class. Note this is the same invocation used in
771  // java_static_lifetime_init.
772 
773  auto class_globals = stub_globals_by_class.equal_range(class_id);
774  INVARIANT(
775  class_globals.first != class_globals.second,
776  "class with synthetic clinit should have at least one global to init");
777 
778  object_factory_parameterst parameters = object_factory_parameters;
779  parameters.function_id = function_id;
780 
781  for(auto it = class_globals.first; it != class_globals.second; ++it)
782  {
783  const symbol_exprt new_global_symbol =
784  symbol_table.lookup_ref(it->second).symbol_expr();
785 
786  parameters.max_nonnull_tree_depth =
787  is_non_null_library_global(it->second)
788  ? object_factory_parameters.max_nonnull_tree_depth + 1
789  : object_factory_parameters.max_nonnull_tree_depth;
790 
791  source_locationt location;
792  location.set_function(function_id);
794  new_global_symbol,
795  static_init_body,
796  symbol_table,
797  location,
798  false,
800  parameters,
801  pointer_type_selector,
803  }
804 
805  return static_init_body;
806 }
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:486
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:3228
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 ...
bool is_nil() const
Definition: irep.h:172
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
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:476
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:4422
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:204
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:112
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:4486
A declaration of a local variable.
Definition: std_code.h:254
const std::string clinit_function_suffix
The NIL expression.
Definition: std_expr.h:4508
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:100
#define PRECONDITION(CONDITION)
Definition: invariant.h:242
A function call.
Definition: std_code.h:858
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:829
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
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:414
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:4497
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:357
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:878
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:89
An if-then-else.
Definition: std_code.h:466
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:923
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:496
bool empty() const
Definition: dstring.h:73
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:196
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
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