cprover
remove_static_init_loops.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Unwind loops in static initializers
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
13 
14 #include <algorithm>
15 
16 #include <util/message.h>
17 #include <util/suffix.h>
18 #include <util/string2int.h>
19 
21 {
22 public:
24  const symbol_tablet &_symbol_table):
25  symbol_table(_symbol_table)
26  {}
27 
28  void unwind_enum_static(
29  const goto_functionst &goto_functions,
30  optionst &options);
31 protected:
33 };
34 
40  const goto_functionst &goto_functions,
41  optionst &options)
42 {
43  size_t unwind_max=0;
44  forall_goto_functions(f, goto_functions)
45  {
46  auto &p=f->second.body;
47  for(const auto &ins : p.instructions)
48  {
49  // is this a loop?
50  if(ins.is_backwards_goto())
51  {
52  size_t loop_id=ins.loop_number;
53  const std::string java_clinit="<clinit>:()V";
54  const std::string &fname=id2string(ins.function);
55  size_t class_prefix_length=fname.find_last_of('.');
56  // is Java function and static init?
57  const symbolt &function_name=symbol_table.lookup(ins.function);
58  if(!(function_name.mode==ID_java && has_suffix(fname, java_clinit)))
59  continue;
60  assert(
61  class_prefix_length!=std::string::npos &&
62  "could not identify class name");
63  const std::string &classname=fname.substr(0, class_prefix_length);
64  const symbolt &class_symbol=symbol_table.lookup(classname);
65  const class_typet &class_type=to_class_type(class_symbol.type);
66  size_t unwinds=class_type.get_size_t(ID_java_enum_static_unwind);
67 
68  unwind_max=std::max(unwind_max, unwinds);
69  if(unwinds>0)
70  {
71  const std::string &set=options.get_option("unwindset");
72  std::string newset;
73  if(set!="")
74  newset=",";
75  newset+=
76  id2string(ins.function)+"."+std::to_string(loop_id)+":"+
77  std::to_string(unwinds);
78  options.set_option("unwindset", set+newset);
79  }
80  }
81  }
82  }
83  const std::string &vla_length=options.get_option("java-max-vla-length");
84  if(!vla_length.empty())
85  {
86  size_t max_vla_length=safe_string2unsigned(vla_length);
87  if(max_vla_length<unwind_max)
88  throw "cannot unwind <clinit> due to insufficient max vla length";
89  }
90 }
91 
98  const goto_functionst &goto_functions,
99  optionst &options)
100 {
101  remove_static_init_loopst remove_loops(symbol_table);
102  remove_loops.unwind_enum_static(goto_functions, options);
103 }
symbolt & lookup(const irep_idt &identifier)
Find a symbol in the symbol table.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
irep_idt mode
Language mode.
Definition: symbol.h:55
void remove_static_init_loops(const symbol_tablet &symbol_table, const goto_functionst &goto_functions, optionst &options)
this is the entry point for the removal of loops in static initialization code of Java enums ...
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
void unwind_enum_static(const goto_functionst &goto_functions, optionst &options)
unwind static initialization loops of Java enums as far as the enum has elements, thus flattening the...
const std::string get_option(const std::string &option) const
Definition: options.cpp:60
The symbol table.
Definition: symbol_table.h:52
unsigned safe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:51
typet type
Type of symbol.
Definition: symbol.h:37
remove_static_init_loopst(const symbol_tablet &_symbol_table)
bool has_suffix(const std::string &s, const std::string &suffix)
Definition: suffix.h:15
void set_option(const std::string &option, const bool value)
Definition: options.cpp:24
C++ class type.
Definition: std_types.h:334
#define forall_goto_functions(it, functions)
Unwind loops in static initializers.
std::size_t get_size_t(const irep_namet &name) const
Definition: irep.cpp:255
const class_typet & to_class_type(const typet &type)
Cast a generic typet to a class_typet.
Definition: std_types.h:407