From b49a7fc3a32bcc3e883c81ee4bec6f085a074bfa Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Sat, 21 Jan 2017 00:42:53 +0100 Subject: [PATCH] loop unwinding in static init of Java enum Static initialization of Java enums sometimes contains extra code that loops over the array of enum elements. This often prevents initialization of the enumeration and leads to zero coverage. This patch counts the number of enum elements, and explicitely unwinds all loops in to this number + 1. This acts as a heuristic to make static inits of enums finish. --- src/cbmc/cbmc_parse_options.cpp | 12 ++ src/cbmc/cbmc_parse_options.h | 11 +- src/goto-programs/Makefile | 3 +- .../remove_static_init_loops.cpp | 118 ++++++++++++++++++ src/goto-programs/remove_static_init_loops.h | 22 ++++ .../java_bytecode_convert_class.cpp | 4 + .../java_bytecode_parse_tree.cpp | 19 +-- src/java_bytecode/java_bytecode_parse_tree.h | 22 +++- src/java_bytecode/java_bytecode_parser.cpp | 11 +- src/util/irep_ids.txt | 1 + 10 files changed, 204 insertions(+), 19 deletions(-) create mode 100644 src/goto-programs/remove_static_init_loops.cpp create mode 100644 src/goto-programs/remove_static_init_loops.h diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 35a5002572d..4c918747c31 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -28,6 +28,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include @@ -222,6 +223,10 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) // all checks supported by goto_check GOTO_CHECK_PARSE_OPTIONS(cmdline, options); + // unwind loops in java enum static initialization + if(cmdline.isset("java-unwind-enum-static")) + options.set_option("java-unwind-enum-static", true); + // check assertions if(cmdline.isset("no-assertions")) options.set_option("assertions", false); @@ -542,6 +547,9 @@ int cbmc_parse_optionst::doit() if(set_properties(goto_functions)) return 7; // should contemplate EX_USAGE from sysexits.h + if(options.get_bool_option("java-unwind-enum-static")) + remove_static_init_loops(symbol_table, goto_functions, options); + // do actual BMC return do_bmc(bmc, goto_functions); } @@ -1127,6 +1135,10 @@ void cbmc_parse_optionst::help() "Java Bytecode frontend options:\n" " --classpath dir/jar set the classpath\n" " --main-class class-name set the name of the main class\n" + // NOLINTNEXTLINE(whitespace/line_length) + " --java-max-vla-length limit the length of user-code-created arrays\n" + // NOLINTNEXTLINE(whitespace/line_length) + " --java-unwind-enum-static try to unwind loops in static initialization of enums\n" "\n" "Semantic transformations:\n" " --nondet-static add nondeterministic initialization of variables with static lifetime\n" // NOLINT(*) diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index 72387bcb4fc..3fcc98231f7 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -36,13 +36,13 @@ class optionst; "(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(opensmt)(mathsat)" \ "(no-sat-preprocessor)" \ "(no-pretty-names)(beautify)" \ - "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)(aig)" \ - "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \ + "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\ + "(aig)(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \ "(little-endian)(big-endian)" \ "(show-goto-functions)(show-loops)" \ "(show-symbol-table)(show-parse-tree)(show-vcc)" \ - "(show-claims)(claim):(show-properties)(show-reachable-properties)(property):" \ - "(stop-on-fail)(trace)" \ + "(show-claims)(claim):(show-properties)(show-reachable-properties)" \ + "(property):(stop-on-fail)(trace)" \ "(error-label):(verbosity):(no-library)" \ "(nondet-static)" \ "(version)" \ @@ -54,8 +54,9 @@ class optionst; "(string-abstraction)(no-arch)(arch):" \ "(round-to-nearest)(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \ "(graphml-witness):" \ + "(java-max-vla-length):(java-unwind-enum-static)" \ "(localize-faults)(localize-faults-method):" \ - "(fixedbv)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear + "(fixedbv)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length) class cbmc_parse_optionst: public parse_options_baset, diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile index 813be9a18b7..14516b8c38c 100644 --- a/src/goto-programs/Makefile +++ b/src/goto-programs/Makefile @@ -17,7 +17,8 @@ SRC = goto_convert.cpp goto_convert_function_call.cpp \ goto_trace.cpp xml_goto_trace.cpp vcd_goto_trace.cpp \ graphml_witness.cpp remove_virtual_functions.cpp \ class_hierarchy.cpp show_goto_functions.cpp get_goto_model.cpp \ - slice_global_inits.cpp goto_inline_class.cpp class_identifier.cpp + slice_global_inits.cpp goto_inline_class.cpp class_identifier.cpp \ + remove_static_init_loops.cpp INCLUDES= -I .. diff --git a/src/goto-programs/remove_static_init_loops.cpp b/src/goto-programs/remove_static_init_loops.cpp new file mode 100644 index 00000000000..25d48ccf654 --- /dev/null +++ b/src/goto-programs/remove_static_init_loops.cpp @@ -0,0 +1,118 @@ +/*******************************************************************\ + +Module: Unwind loops in static initializers + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +#include +#include + +#include "remove_static_init_loops.h" + +class remove_static_init_loopst +{ +public: + explicit remove_static_init_loopst( + const symbol_tablet &_symbol_table): + symbol_table(_symbol_table) + {} + + void unwind_enum_static( + const goto_functionst &goto_functions, + optionst &options); +protected: + const symbol_tablet &symbol_table; +}; + +/*******************************************************************\ + +Function: unwind_enum_static + + Inputs: goto_functions and options + + Outputs: side effect is adding loops to unwindset + + Purpose: unwind static initialization loops of Java enums as far as + the enum has elements, thus flattening them completely + +\*******************************************************************/ + +void remove_static_init_loopst::unwind_enum_static( + const goto_functionst &goto_functions, + optionst &options) +{ + size_t unwind_max=0; + forall_goto_functions(f, goto_functions) + { + auto &p=f->second.body; + for(const auto &ins : p.instructions) + { + // is this a loop? + if(ins.is_backwards_goto()) + { + size_t loop_id=ins.loop_number; + const std::string java_clinit=":()V"; + const std::string &fname=id2string(ins.function); + size_t class_prefix_length=fname.find_last_of('.'); + assert( + class_prefix_length!=std::string::npos && + "could not identify class name"); + const std::string &classname=fname.substr(0, class_prefix_length); + const symbolt &class_symbol=symbol_table.lookup(classname); + const class_typet &class_type=to_class_type(class_symbol.type); + size_t unwinds=class_type.get_size_t(ID_java_enum_static_unwind); + + unwind_max=std::max(unwind_max, unwinds); + if(fname.length()>java_clinit.length()) + { + // extend unwindset with unwinds for of enum + if(fname.compare( + fname.length()-java_clinit.length(), + java_clinit.length(), + java_clinit)==0 && unwinds>0) + { + const std::string &set=options.get_option("unwindset"); + std::string newset; + if(set!="") + newset=","; + newset+= + id2string(ins.function)+"."+std::to_string(loop_id)+":"+ + std::to_string(unwinds); + options.set_option("unwindset", set+newset); + } + } + } + } + } + const std::string &vla_length=options.get_option("java-max-vla-length"); + if(!vla_length.empty()) + { + size_t max_vla_length=safe_string2unsigned(vla_length); + if(max_vla_length due to insufficient max vla length"; + } +} + +/*******************************************************************\ + +Function: remove_static_init_loops + + Inputs: symbol table, goto_functions and options + + Outputs: side effect is adding loops to unwindset + + Purpose: this is the entry point for the removal of loops in static + initialization code of Java enums + +\*******************************************************************/ + +void remove_static_init_loops( + const symbol_tablet &symbol_table, + const goto_functionst &goto_functions, + optionst &options) +{ + remove_static_init_loopst remove_loops(symbol_table); + remove_loops.unwind_enum_static(goto_functions, options); +} diff --git a/src/goto-programs/remove_static_init_loops.h b/src/goto-programs/remove_static_init_loops.h new file mode 100644 index 00000000000..dd07ec6a670 --- /dev/null +++ b/src/goto-programs/remove_static_init_loops.h @@ -0,0 +1,22 @@ +/*******************************************************************\ + +Module: Unwind loops in static initializers + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +#include + +#include +#include + +#ifndef CPROVER_GOTO_PROGRAMS_REMOVE_STATIC_INIT_LOOPS_H +#define CPROVER_GOTO_PROGRAMS_REMOVE_STATIC_INIT_LOOPS_H + +void remove_static_init_loops( + const symbol_tablet &, + const goto_functionst &, + optionst &); + +#endif // CPROVER_GOTO_PROGRAMS_REMOVE_STATIC_INIT_LOOPS_H diff --git a/src/java_bytecode/java_bytecode_convert_class.cpp b/src/java_bytecode/java_bytecode_convert_class.cpp index 113a8b9422d..9b9e41d890b 100644 --- a/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/src/java_bytecode/java_bytecode_convert_class.cpp @@ -77,6 +77,10 @@ void java_bytecode_convert_classt::convert(const classt &c) class_type.set_tag(c.name); class_type.set(ID_base_name, c.name); + if(c.is_enum) + class_type.set( + ID_java_enum_static_unwind, + std::to_string(c.enum_elements+1)); if(!c.extends.empty()) { diff --git a/src/java_bytecode/java_bytecode_parse_tree.cpp b/src/java_bytecode/java_bytecode_parse_tree.cpp index b7f3be50007..e48675d275f 100644 --- a/src/java_bytecode/java_bytecode_parse_tree.cpp +++ b/src/java_bytecode/java_bytecode_parse_tree.cpp @@ -34,6 +34,8 @@ void java_bytecode_parse_treet::classt::swap( { other.name.swap(name); other.extends.swap(extends); + other.is_enum=is_enum; + other.enum_elements=enum_elements; std::swap(other.is_abstract, is_abstract); other.implements.swap(implements); other.fields.swap(fields); @@ -61,10 +63,7 @@ void java_bytecode_parse_treet::output(std::ostream &out) const for(class_refst::const_iterator it=class_refs.begin(); it!=class_refs.end(); it++) - { out << " " << *it << '\n'; - } - } /*******************************************************************\ @@ -88,7 +87,8 @@ void java_bytecode_parse_treet::classt::output(std::ostream &out) const } out << "class " << name; - if(!extends.empty()) out << " extends " << extends; + if(!extends.empty()) + out << " extends " << extends; out << " {" << '\n'; for(fieldst::const_iterator @@ -139,7 +139,10 @@ void java_bytecode_parse_treet::annotationt::output(std::ostream &out) const bool first=true; for(const auto &element_value_pair : element_value_pairs) { - if(first) first=false; else out << ", "; + if(first) + first=false; + else + out << ", "; element_value_pair.output(out); } @@ -159,7 +162,8 @@ Function: java_bytecode_parse_treet::annotationt::element_value_pairt::output \*******************************************************************/ -void java_bytecode_parse_treet::annotationt::element_value_pairt::output(std::ostream &out) const +void java_bytecode_parse_treet::annotationt::element_value_pairt::output( + std::ostream &out) const { symbol_tablet symbol_table; namespacet ns(symbol_table); @@ -233,7 +237,8 @@ void java_bytecode_parse_treet::methodt::output(std::ostream &out) const for(std::vector::const_iterator a_it=i.args.begin(); a_it!=i.args.end(); a_it++) { - if(a_it!=i.args.begin()) out << ','; + if(a_it!=i.args.begin()) + out << ','; #if 0 out << ' ' << from_expr(*a_it); #else diff --git a/src/java_bytecode/java_bytecode_parse_tree.h b/src/java_bytecode/java_bytecode_parse_tree.h index 398e3959d1a..bd62b0e1377 100644 --- a/src/java_bytecode/java_bytecode_parse_tree.h +++ b/src/java_bytecode/java_bytecode_parse_tree.h @@ -123,15 +123,20 @@ class java_bytecode_parse_treet class stack_map_table_entryt { public: - enum stack_frame_type { SAME, SAME_LOCALS_ONE_STACK, SAME_LOCALS_ONE_STACK_EXTENDED, - CHOP, SAME_EXTENDED, APPEND, FULL}; + enum stack_frame_type + { + SAME, SAME_LOCALS_ONE_STACK, SAME_LOCALS_ONE_STACK_EXTENDED, + CHOP, SAME_EXTENDED, APPEND, FULL + }; stack_frame_type type; size_t offset_delta; size_t chops; size_t appends; - typedef std::vector local_verification_type_infot; - typedef std::vector stack_verification_type_infot; + typedef std::vector + local_verification_type_infot; + typedef std::vector + stack_verification_type_infot; local_verification_type_infot locals; stack_verification_type_infot stack; @@ -142,7 +147,10 @@ class java_bytecode_parse_treet virtual void output(std::ostream &out) const; - inline methodt():is_native(false), is_abstract(false), is_synchronized(false) + inline methodt(): + is_native(false), + is_abstract(false), + is_synchronized(false) { } }; @@ -151,6 +159,7 @@ class java_bytecode_parse_treet { public: virtual void output(std::ostream &out) const; + bool is_enum; }; class classt @@ -158,6 +167,9 @@ class java_bytecode_parse_treet public: irep_idt name, extends; bool is_abstract; + bool is_enum; + size_t enum_elements=0; + typedef std::list implementst; implementst implements; diff --git a/src/java_bytecode/java_bytecode_parser.cpp b/src/java_bytecode/java_bytecode_parser.cpp index 7138ab3951b..323ef603af8 100644 --- a/src/java_bytecode/java_bytecode_parser.cpp +++ b/src/java_bytecode/java_bytecode_parser.cpp @@ -264,6 +264,7 @@ Function: java_bytecode_parsert::rClassFile #define ACC_ABSTRACT 0x0400 #define ACC_STRICT 0x0800 #define ACC_SYNTHETIC 0x1000 +#define ACC_ENUM 0x4000 #ifdef _MSC_VER #define UNUSED @@ -295,10 +296,11 @@ void java_bytecode_parsert::rClassFile() classt &parsed_class=parse_tree.parsed_class; - u2 UNUSED access_flags=read_u2(); + u2 access_flags=read_u2(); u2 this_class=read_u2(); u2 super_class=read_u2(); + parsed_class.is_enum=(access_flags&ACC_ENUM)!=0; parsed_class.name= constant(this_class).type().get(ID_C_base_name); @@ -310,6 +312,12 @@ void java_bytecode_parsert::rClassFile() rfields(parsed_class); rmethods(parsed_class); + // count elements of enum + if(parsed_class.is_enum) + for(fieldt &field : parse_tree.parsed_class.fields) + if(field.is_enum) + parse_tree.parsed_class.enum_elements++; + u2 attributes_count=read_u2(); for(std::size_t j=0; j