Merge pull request #460 from mgudemann/java_unwind_enum_static

Java unwind enum static

src/cbmc/cbmc_parse_options.cpp

@@ -27,6 +27,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/remove_complex.h>
 #include <goto-programs/remove_asm.h>
 #include <goto-programs/remove_unused_functions.h>
+#include <goto-programs/remove_static_init_loops.h>
 #include <goto-programs/goto_inline.h>
 #include <goto-programs/show_properties.h>
 #include <goto-programs/set_properties.h>
@@ -221,6 +222,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);
@@ -541,6 +546,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);
 }
@@ -1126,6 +1134,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(*)

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,

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 ..
 

src/goto-programs/remove_static_init_loops.cpp

@@ -0,0 +1,118 @@
+/*******************************************************************\
+
+Module: Unwind loops in static initializers
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#include <util/message.h>
+#include <util/string2int.h>
+
+#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 <clinit> 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="<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 <clinit> 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<unwind_max)
+      throw "cannot unwind <clinit> due to insufficient max vla length";
+  }
+}
+
+/*******************************************************************\
+
+Function: remove_static_init_loops
+
+  Inputs: symbol table, goto_functions and options
+
+ Outputs: side effect is adding <clinit> 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);
+}

src/goto-programs/remove_static_init_loops.h

@@ -0,0 +1,22 @@
+/*******************************************************************\
+
+Module: Unwind loops in static initializers
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#include <goto-programs/goto_functions.h>
+
+#include <util/options.h>
+#include <util/symbol_table.h>
+
+#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

src/java_bytecode/java_bytecode_convert_class.cpp

@@ -79,6 +79,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())
   {

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<exprt>::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

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<verification_type_infot> local_verification_type_infot;
-      typedef std::vector<verification_type_infot> stack_verification_type_infot;
+      typedef std::vector<verification_type_infot>
+        local_verification_type_infot;
+      typedef std::vector<verification_type_infot>
+        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,13 +159,17 @@ class java_bytecode_parse_treet
   {
   public:
     virtual void output(std::ostream &out) const;
+    bool is_enum;
   };
 
   class classt
   {
   public:
     irep_idt name, extends;
     bool is_abstract;
+    bool is_enum;
+    size_t enum_elements=0;
+
     typedef std::list<irep_idt> implementst;
     implementst implements;
 

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<attributes_count; j++)
@@ -698,6 +706,7 @@ void java_bytecode_parsert::rfields(classt &parsed_class)
     field.name=pool_entry(name_index).s;
     field.is_static=(access_flags&ACC_STATIC)!=0;
     field.is_final=(access_flags&ACC_FINAL)!=0;
+    field.is_enum=(access_flags&ACC_ENUM)!=0;
     field.signature=id2string(pool_entry(descriptor_index).s);
 
     for(std::size_t j=0; j<attributes_count; j++)

src/util/irep_ids.txt

@@ -736,3 +736,4 @@ bswap
 java_bytecode_index
 java_instanceof
 java_super_method_call
+java_enum_static_unwind