cprover
java_enum_static_init_unwind_handler.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Unwind loops in static initializers
4 
5 Author: Chris Smowton, chris.smowton@diffblue.com
6 
7 \*******************************************************************/
8 
11 
13 #include "java_utils.h"
14 
15 #include <util/invariant.h>
16 #include <util/suffix.h>
17 
29 {
30  static irep_idt reference_array_clone_id =
31  "java::array[reference].clone:()Ljava/lang/Object;";
32 
33  PRECONDITION(!context.empty());
34  const irep_idt &current_function = context.back().function_identifier;
35 
36  if(context.size() >= 2 && current_function == reference_array_clone_id)
37  {
38  const irep_idt &clone_caller =
39  context.at(context.size() - 2).function_identifier;
40  if(id2string(clone_caller).find(".values:()[L") != std::string::npos)
41  return clone_caller;
42  else
43  return irep_idt();
44  }
45  else if(has_suffix(id2string(current_function), ".<clinit>:()V"))
46  return current_function;
47  else
48  return irep_idt();
49 }
50 
67  const call_stackt &context,
68  unsigned loop_number,
69  unsigned unwind_count,
70  unsigned &unwind_max,
71  const symbol_tablet &symbol_table)
72 {
73  (void)loop_number; // unused parameter
74 
75  const irep_idt enum_function_id = find_enum_function_on_stack(context);
76  if(enum_function_id.empty())
77  return tvt::unknown();
78 
79  const symbolt &function_symbol = symbol_table.lookup_ref(enum_function_id);
80  const auto class_id = declaring_class(function_symbol);
81  INVARIANT(class_id, "Java methods should have a defining class.");
82 
83  const typet &class_type = symbol_table.lookup_ref(*class_id).type;
84  size_t unwinds = class_type.get_size_t(ID_java_enum_static_unwind);
85  if(unwinds != 0 && unwind_count < unwinds)
86  {
87  unwind_max = unwinds;
88  return tvt(false); // Must unwind
89  }
90  else
91  {
92  return tvt::unknown(); // Defer to other unwind handlers
93  }
94 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
java_enum_static_init_unwind_handler
tvt java_enum_static_init_unwind_handler(const call_stackt &context, unsigned loop_number, unsigned unwind_count, unsigned &unwind_max, const symbol_tablet &symbol_table)
Unwind handler that special-cases the clinit (static initializer) functions of enumeration classes,...
Definition: java_enum_static_init_unwind_handler.cpp:66
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
symbol_table_baset::lookup_ref
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:104
typet
The type of an expression, extends irept.
Definition: type.h:29
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
java_enum_static_init_unwind_handler.h
Unwind loops in static initializers.
declaring_class
optionalt< irep_idt > declaring_class(const symbolt &symbol)
Gets the identifier of the class which declared a given symbol.
Definition: java_utils.cpp:579
invariant.h
irep_idt
dstringt irep_idt
Definition: irep.h:32
call_stackt
Definition: call_stack.h:15
has_suffix
bool has_suffix(const std::string &s, const std::string &suffix)
Definition: suffix.h:17
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
tvt::unknown
static tvt unknown()
Definition: threeval.h:33
dstringt::empty
bool empty() const
Definition: dstring.h:88
tvt
Definition: threeval.h:20
irept::get_size_t
std::size_t get_size_t(const irep_namet &name) const
Definition: irep.cpp:74
suffix.h
symbolt
Symbol table entry.
Definition: symbol.h:28
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
java_utils.h
find_enum_function_on_stack
static irep_idt find_enum_function_on_stack(const call_stackt &context)
Check if we may be in a function that loops over the cases of an enumeration (note we return a candid...
Definition: java_enum_static_init_unwind_handler.cpp:28