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