|
| 1 | +/*******************************************************************\ |
| 2 | +
|
| 3 | +Module: Unwind loops in static initializers |
| 4 | +
|
| 5 | +Author: Daniel Kroening, [email protected] |
| 6 | +
|
| 7 | +\*******************************************************************/ |
| 8 | + |
| 9 | +#include <util/message.h> |
| 10 | +#include <util/string2int.h> |
| 11 | + |
| 12 | +#include "remove_static_init_loops.h" |
| 13 | + |
| 14 | +class remove_static_init_loopst |
| 15 | +{ |
| 16 | +public: |
| 17 | + explicit remove_static_init_loopst( |
| 18 | + const symbol_tablet &_symbol_table): |
| 19 | + symbol_table(_symbol_table) |
| 20 | + {} |
| 21 | + |
| 22 | + void unwind_enum_static( |
| 23 | + const goto_functionst &goto_functions, |
| 24 | + optionst &options); |
| 25 | +protected: |
| 26 | + const symbol_tablet &symbol_table; |
| 27 | +}; |
| 28 | + |
| 29 | +/*******************************************************************\ |
| 30 | +
|
| 31 | +Function: unwind_enum_static |
| 32 | +
|
| 33 | + Inputs: goto_functions and options |
| 34 | +
|
| 35 | + Outputs: side effect is adding <clinit> loops to unwindset |
| 36 | +
|
| 37 | + Purpose: unwind static initialization loops of Java enums as far as |
| 38 | + the enum has elements, thus flattening them completely |
| 39 | +
|
| 40 | +\*******************************************************************/ |
| 41 | + |
| 42 | +void remove_static_init_loopst::unwind_enum_static( |
| 43 | + const goto_functionst &goto_functions, |
| 44 | + optionst &options) |
| 45 | +{ |
| 46 | + size_t unwind_max=0; |
| 47 | + forall_goto_functions(f, goto_functions) |
| 48 | + { |
| 49 | + auto &p=f->second.body; |
| 50 | + for(const auto &ins : p.instructions) |
| 51 | + { |
| 52 | + // is this a loop? |
| 53 | + if(ins.is_backwards_goto()) |
| 54 | + { |
| 55 | + size_t loop_id=ins.loop_number; |
| 56 | + const std::string java_clinit="<clinit>:()V"; |
| 57 | + const std::string &fname=id2string(ins.function); |
| 58 | + size_t class_prefix_length=fname.find_last_of('.'); |
| 59 | + assert( |
| 60 | + class_prefix_length!=std::string::npos && |
| 61 | + "could not identify class name"); |
| 62 | + const std::string &classname=fname.substr(0, class_prefix_length); |
| 63 | + const symbolt &class_symbol=symbol_table.lookup(classname); |
| 64 | + const class_typet &class_type=to_class_type(class_symbol.type); |
| 65 | + size_t unwinds=class_type.get_size_t(ID_java_enum_static_unwind); |
| 66 | + |
| 67 | + unwind_max=std::max(unwind_max, unwinds); |
| 68 | + if(fname.length()>java_clinit.length()) |
| 69 | + { |
| 70 | + // extend unwindset with unwinds for <clinit> of enum |
| 71 | + if(fname.compare( |
| 72 | + fname.length()-java_clinit.length(), |
| 73 | + java_clinit.length(), |
| 74 | + java_clinit)==0 && unwinds>0) |
| 75 | + { |
| 76 | + const std::string &set=options.get_option("unwindset"); |
| 77 | + std::string newset; |
| 78 | + if(set!="") |
| 79 | + newset=","; |
| 80 | + newset+= |
| 81 | + id2string(ins.function)+"."+std::to_string(loop_id)+":"+ |
| 82 | + std::to_string(unwinds); |
| 83 | + options.set_option("unwindset", set+newset); |
| 84 | + } |
| 85 | + } |
| 86 | + } |
| 87 | + } |
| 88 | + } |
| 89 | + const std::string &vla_length=options.get_option("java-max-vla-length"); |
| 90 | + if(!vla_length.empty()) |
| 91 | + { |
| 92 | + size_t max_vla_length=safe_string2unsigned(vla_length); |
| 93 | + if(max_vla_length<unwind_max) |
| 94 | + throw "cannot unwind <clinit> due to insufficient max vla length"; |
| 95 | + } |
| 96 | +} |
| 97 | + |
| 98 | +/*******************************************************************\ |
| 99 | +
|
| 100 | +Function: remove_static_init_loops |
| 101 | +
|
| 102 | + Inputs: symbol table, goto_functions and options |
| 103 | +
|
| 104 | + Outputs: side effect is adding <clinit> loops to unwindset |
| 105 | +
|
| 106 | + Purpose: this is the entry point for the removal of loops in static |
| 107 | + initialization code of Java enums |
| 108 | +
|
| 109 | +\*******************************************************************/ |
| 110 | + |
| 111 | +void remove_static_init_loops( |
| 112 | + const symbol_tablet &symbol_table, |
| 113 | + const goto_functionst &goto_functions, |
| 114 | + optionst &options) |
| 115 | +{ |
| 116 | + remove_static_init_loopst remove_loops(symbol_table); |
| 117 | + remove_loops.unwind_enum_static(goto_functions, options); |
| 118 | +} |
0 commit comments