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