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 
14 #include <util/invariant.h>
15 #include <util/suffix.h>
16 
27 static irep_idt
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 goto_symex_statet::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  irep_idt class_id = function_symbol.type.get(ID_C_class);
81  INVARIANT(
82  !class_id.empty(), "functions should have their defining class annotated");
83 
84  const typet &class_type = symbol_table.lookup_ref(class_id).type;
85  size_t unwinds = class_type.get_size_t(ID_java_enum_static_unwind);
86  if(unwinds != 0 && unwind_count < unwinds)
87  {
88  unwind_max = unwinds;
89  return tvt(false); // Must unwind
90  }
91  else
92  {
93  return tvt::unknown(); // Defer to other unwind handlers
94  }
95 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
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:96
typet
The type of an expression, extends irept.
Definition: type.h:27
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
java_enum_static_init_unwind_handler.h
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:400
invariant.h
irep_idt
dstringt irep_idt
Definition: irep.h:32
java_enum_static_init_unwind_handler
tvt java_enum_static_init_unwind_handler(const goto_symex_statet::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
has_suffix
bool has_suffix(const std::string &s, const std::string &suffix)
Definition: suffix.h:15
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
tvt::unknown
static tvt unknown()
Definition: threeval.h:33
dstringt::empty
bool empty() const
Definition: dstring.h:75
goto_symex_statet::call_stackt
std::vector< framet > call_stackt
Definition: goto_symex_state.h:201
tvt
Definition: threeval.h:19
find_enum_function_on_stack
static irep_idt find_enum_function_on_stack(const goto_symex_statet::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
irept::get_size_t
std::size_t get_size_t(const irep_namet &name) const
Definition: irep.cpp:254
suffix.h
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
symbolt
Symbol table entry.
Definition: symbol.h:27