Merge pull request #2651 from smowton/smowton/feature/unroll-enum-clone-loops

Unroll enumeration values() loops

Author: smowton

jbmc/regression/jbmc/enum_switch/com/diffblue/regression/Foo$1.class

@@ -0,0 +1,16 @@
+package com.diffblue.regression;
+
+public class Foo {
+  public int foo(MyEnum e) {
+    if (e == null) return 0;
+    switch (e) {
+      case A:
+        return 1;
+      case B:
+        return 2;
+      case C:
+        return 3;
+    }
+    return 5;
+  }
+}

jbmc/regression/jbmc/enum_switch/com/diffblue/regression/Foo.class

@@ -0,0 +1,5 @@
+package com.diffblue.regression;
+
+enum MyEnum {
+ A, B, C, D;
+}

jbmc/regression/jbmc/enum_switch/com/diffblue/regression/Foo.java

@@ -0,0 +1,10 @@
+CORE symex-driven-lazy-loading-expected-failure
+com/diffblue/regression/Foo.class
+--trace --cover location --depth 1024 --java-max-vla-length 16 --refine-strings --max-nondet-string-length 20 --string-printable --unwind 10 --function "com.diffblue.regression.Foo.foo" --java-unwind-enum-static
+line 8.*SATISFIED
+line 10.*SATISFIED
+line 12.*SATISFIED
+line 14.*SATISFIED
+^EXIT=0$
+^SIGNAL=0$
+--

jbmc/regression/jbmc/enum_switch/com/diffblue/regression/MyEnum.class

@@ -0,0 +1,8 @@
+package com.diffblue.regression;
+public class EnumIter {
+    int f() {
+        MyEnum[] a = MyEnum.values();
+        int num = a[2].ordinal() + a[3].ordinal();
+        return num ;
+    }
+}

jbmc/regression/jbmc/enum_switch/com/diffblue/regression/MyEnum.java

@@ -0,0 +1,5 @@
+package com.diffblue.regression;
+
+enum MyEnum {
+ A, B, C, D;
+}

jbmc/regression/jbmc/enum_switch/test.desc

@@ -0,0 +1,7 @@
+CORE symex-driven-lazy-loading-expected-failure
+com/diffblue/regression/EnumIter.class
+--trace  --cover location --depth 1024  --java-max-vla-length 16 --refine-strings --max-nondet-string-length 20 --string-printable --unwind 2 --function "com.diffblue.regression.EnumIter.f" --java-unwind-enum-static
+\d+ of \d+ covered \(100\.0%\)
+^EXIT=0$
+^SIGNAL=0$
+--

jbmc/regression/jbmc/enum_values_clone/com/diffblue/regression/EnumIter.class

@@ -0,0 +1,7 @@
+package com.diffblue.regression;
+public class EnumIter {
+    String f() {
+        MyEnum[] a = MyEnum.values();
+        return a[2].name() + a[3].name();
+    }
+}

jbmc/regression/jbmc/enum_values_clone/com/diffblue/regression/EnumIter.java

@@ -0,0 +1,5 @@
+package com.diffblue.regression;
+
+enum MyEnum {
+ A, B, C, D;
+}

jbmc/regression/jbmc/enum_values_clone/com/diffblue/regression/MyEnum.class

@@ -0,0 +1,7 @@
+CORE symex-driven-lazy-loading-expected-failure
+com/diffblue/regression/EnumIter.class
+--trace --cover location --depth 1024 --java-max-vla-length 16 --refine-strings --max-nondet-string-length 20 --string-printable --unwind 2 --function "com.diffblue.regression.EnumIter.f" --java-unwind-enum-static
+\d+ of \d+ covered \(100\.0%\)
+^EXIT=0$
+^SIGNAL=0$
+--

jbmc/regression/jbmc/enum_values_clone/com/diffblue/regression/MyEnum.java

@@ -1959,9 +1959,12 @@ codet java_bytecode_convert_methodt::convert_switch(
       mp_integer number;
       bool ret = to_integer(to_constant_expr(*a_it), number);
       DATA_INVARIANT(!ret, "case label expected to be integer");
+      // The switch case does not contain any code, it just branches via a GOTO
+      // to the jump target of the tableswitch/lookupswitch case at
+      // hand. Therefore we consider this code to belong to the source bytecode
+      // instruction and not the target instruction.
       code_case.code() = code_gotot(label(integer2string(number)));
-      code_case.code().add_source_location() =
-        address_map.at(integer2unsigned(number)).source->source_location;
+      code_case.code().add_source_location() = location;
 
       if(a_it == args.begin())
         code_case.set_default();

jbmc/regression/jbmc/enum_values_clone/test.desc

@@ -14,12 +14,47 @@ Author: Chris Smowton, [email protected]
 #include <util/invariant.h>
 #include <util/suffix.h>
 
+/// Check if we may be in a function that loops over the cases of an
+/// enumeration (note we return a candidate function that matches a pattern;
+/// our caller must verify it really belongs to an enumeration).
+/// At the moment we know of two cases that definitely do so:
+/// * An enumeration type's static initialiser
+/// * The array[reference].clone() method when called from an enumeration type's
+///   'values()'  method
+/// \param context: the current call stack
+/// \return the name of an enclosing function that may be defined on the
+///   relevant enum type, or an empty string if we don't find one.
+static irep_idt
+find_enum_function_on_stack(const goto_symex_statet::call_stackt &context)
+{
+  static irep_idt reference_array_clone_id =
+    "java::array[reference].clone:()Ljava/lang/Object;";
+
+  PRECONDITION(!context.empty());
+  const irep_idt &current_function = context.back().function_identifier;
+
+  if(context.size() >= 2 && current_function == reference_array_clone_id)
+  {
+    const irep_idt &clone_caller =
+      context.at(context.size() - 2).function_identifier;
+    if(id2string(clone_caller).find(".values:()[L") != std::string::npos)
+      return clone_caller;
+    else
+      return irep_idt();
+  }
+  else if(has_suffix(id2string(current_function), ".<clinit>:()V"))
+    return current_function;
+  else
+    return irep_idt();
+}
+
 /// Unwind handler that special-cases the clinit (static initializer) functions
-/// of enumeration classes. When java_bytecode_convert_classt has annotated them
+/// of enumeration classes, and VALUES array cloning in their values() methods.
+/// When java_bytecode_convert_classt has annotated them
 /// with a size of the enumeration type, this forces unwinding of any loop in
 /// the static initializer to at least that many iterations, with intent to
-/// permit population of the enumeration's value array.
-/// \param function_id: function the loop is in
+/// permit population / copying of the enumeration's value array.
+/// \param context: call stack when the loop back-edge was taken
 /// \param loop_number: ordinal number of the loop (ignored)
 /// \param unwind_count: iteration count that is about to begin
 /// \param [out] unwind_max: may be set to an advisory (unenforced) maximum when
@@ -29,17 +64,17 @@ Author: Chris Smowton, [email protected]
 ///   unwind_count is <= the enumeration size, or unknown (defer / no decision)
 ///   otherwise.
 tvt java_enum_static_init_unwind_handler(
-  const irep_idt &function_id,
+  const goto_symex_statet::call_stackt &context,
   unsigned loop_number,
   unsigned unwind_count,
   unsigned &unwind_max,
   const symbol_tablet &symbol_table)
 {
-  const std::string &function_str = id2string(function_id);
-  if(!has_suffix(function_str, ".<clinit>:()V"))
+  const irep_idt enum_function_id = find_enum_function_on_stack(context);
+  if(enum_function_id.empty())
     return tvt::unknown();
 
-  const symbolt &function_symbol = symbol_table.lookup_ref(function_str);
+  const symbolt &function_symbol = symbol_table.lookup_ref(enum_function_id);
   irep_idt class_id = function_symbol.type.get(ID_C_class);
   INVARIANT(
     !class_id.empty(), "functions should have their defining class annotated");

jbmc/regression/jbmc/enum_values_clone_name/com/diffblue/regression/EnumIter.class

@@ -12,11 +12,13 @@ Author: Chris Smowton, [email protected]
 #ifndef CPROVER_JAVA_BYTECODE_JAVA_ENUM_STATIC_INIT_UNWIND_HANDLER_H
 #define CPROVER_JAVA_BYTECODE_JAVA_ENUM_STATIC_INIT_UNWIND_HANDLER_H
 
+#include <goto-symex/goto_symex_state.h>
+
 #include <util/symbol_table.h>
 #include <util/threeval.h>
 
 tvt java_enum_static_init_unwind_handler(
-  const irep_idt &function_id,
+  const goto_symex_statet::call_stackt &context,
   unsigned loop_number,
   unsigned unwind_count,
   unsigned &unwind_max,

jbmc/regression/jbmc/enum_values_clone_name/com/diffblue/regression/EnumIter.java

@@ -479,16 +479,12 @@ int jbmc_parse_optionst::doit()
     configure_bmc = [](bmct &bmc, const symbol_tablet &symbol_table) {
       bmc.add_loop_unwind_handler(
         [&symbol_table](
-          const irep_idt &function_id,
+          const goto_symex_statet::call_stackt &context,
           unsigned loop_number,
           unsigned unwind,
           unsigned &max_unwind) {
           return java_enum_static_init_unwind_handler(
-            function_id,
-            loop_number,
-            unwind,
-            max_unwind,
-            symbol_table);
+            context, loop_number, unwind, max_unwind, symbol_table);
         });
     };
   }

jbmc/regression/jbmc/enum_values_clone_name/com/diffblue/regression/MyEnum.class

@@ -106,6 +106,7 @@ void symex_bmct::merge_goto(
 
 bool symex_bmct::get_unwind(
   const symex_targett::sourcet &source,
+  const goto_symex_statet::call_stackt &context,
   unsigned unwind)
 {
   const irep_idt id=goto_programt::loop_id(*source.pc);
@@ -116,11 +117,7 @@ bool symex_bmct::get_unwind(
   for(auto handler : loop_unwind_handlers)
   {
     abort_unwind_decision =
-      handler(
-        source.pc->function,
-        source.pc->loop_number,
-        unwind,
-        this_loop_limit);
+      handler(context, source.pc->loop_number, unwind, this_loop_limit);
     if(abort_unwind_decision.is_known())
       break;
   }

jbmc/regression/jbmc/enum_values_clone_name/com/diffblue/regression/MyEnum.java

@@ -35,14 +35,15 @@ class symex_bmct: public goto_symext
   // To show progress
   source_locationt last_source_location;
 
-  /// Loop unwind handlers take the function ID and loop number, the unwind
-  /// count so far, and an out-parameter specifying an advisory maximum, which
-  /// they may set. If set the advisory maximum is set it is *only* used to
-  /// print useful information for the user (e.g. "unwinding iteration N, max
-  /// M"), and is not enforced. They return true to halt unwinding, false to
-  /// authorise unwinding, or Unknown to indicate they have no opinion.
+  /// Loop unwind handlers take the call stack, loop number, the unwind count so
+  /// far, and an out-parameter specifying an advisory maximum, which they may
+  /// set. If set the advisory maximum is set it is *only* used to print useful
+  /// information for the user (e.g. "unwinding iteration N, max M"), and is not
+  /// enforced. They return true to halt unwinding, false to authorise
+  /// unwinding, or Unknown to indicate they have no opinion.
   typedef
-    std::function<tvt(const irep_idt &, unsigned, unsigned, unsigned &)>
+    std::function<tvt(
+      const goto_symex_statet::call_stackt &, unsigned, unsigned, unsigned &)>
     loop_unwind_handlert;
 
   /// Recursion unwind handlers take the function ID, the unwind count so far,
@@ -105,6 +106,7 @@ class symex_bmct: public goto_symext
   // for loop unwinding
   virtual bool get_unwind(
     const symex_targett::sourcet &source,
+    const goto_symex_statet::call_stackt &context,
     unsigned unwind);
 
   virtual bool get_unwind_recursion(

jbmc/regression/jbmc/enum_values_clone_name/test.desc

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/fixedbv.h>
 #include <util/ieee_float.h>
 #include <util/pointer_offset_size.h>
+#include <util/simplify_expr.h>
 #include <util/string_container.h>
 
 #include <langapi/language_util.h>
@@ -894,52 +895,38 @@ void interpretert::evaluate(
     mp_integer address=evaluate_address(
       expr,
       true); // fail quietly
-    if(address.is_zero() && expr.id()==ID_index)
+    if(address.is_zero())
     {
-      // Try reading from a constant array:
-      mp_vectort idx;
-      evaluate(expr.op1(), idx);
-      if(idx.size()==1)
+      exprt simplified;
+      // In case of being an indexed access, try to evaluate the index, then
+      // simplify.
+      if(expr.id() == ID_index)
       {
-        mp_integer read_from_index=idx[0];
-        if(expr.op0().id()==ID_array)
+        exprt evaluated_index = expr;
+        mp_vectort idx;
+        evaluate(expr.op1(), idx);
+        if(idx.size() == 1)
         {
-          const auto &ops=expr.op0().operands();
-          DATA_INVARIANT(read_from_index.is_long(), "index is too large");
-          if(read_from_index>=0 && read_from_index<ops.size())
-          {
-            evaluate(ops[read_from_index.to_long()], dest);
-            if(dest.size()!=0)
-              return;
-          }
-        }
-        else if(expr.op0().id() == ID_array_list)
-        {
-          // This sort of construct comes from boolbv_get, but doesn't seem
-          // to have an exprt yet. Its operands are a list of key-value pairs.
-          const auto &ops=expr.op0().operands();
-          DATA_INVARIANT(
-            ops.size()%2==0,
-            "array-list has odd number of operands");
-          for(size_t listidx=0; listidx!=ops.size(); listidx+=2)
-          {
-            mp_vectort elem_idx;
-            evaluate(ops[listidx], elem_idx);
-            CHECK_RETURN(elem_idx.size()==1);
-            if(elem_idx[0]==read_from_index)
-            {
-              evaluate(ops[listidx+1], dest);
-              if(dest.size()!=0)
-                return;
-              else
-                break;
-            }
-          }
-          // If we fall out the end of this loop then the constant array-list
-          // didn't define an element matching the index we're looking for.
+          evaluated_index.op1() =
+            constant_exprt(integer2string(idx[0]), expr.op1().type());
         }
+        simplified = simplify_expr(evaluated_index, ns);
+      }
+      else
+      {
+        // Try reading from a constant -- simplify_expr has all the relevant
+        // cases (index-of-constant-array, member-of-constant-struct and so on)
+        // Note we complain of a problem even if simplify did *something* but
+        // still left us with an unresolved index, member, etc.
+        simplified = simplify_expr(expr, ns);
+      }
+      if(simplified.id() == expr.id())
+        evaluate_address(expr); // Evaluate again to print error message.
+      else
+      {
+        evaluate(simplified, dest);
+        return;
       }
-      evaluate_address(expr); // Evaluate again to print error message.
     }
     else if(!address.is_zero())
     {

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -328,6 +328,7 @@ class goto_symext
   // with false we continue.
   virtual bool get_unwind(
     const symex_targett::sourcet &source,
+    const goto_symex_statet::call_stackt &context,
     unsigned unwind);
 
   virtual void loop_bound_exceeded(statet &, const exprt &guard);

jbmc/src/java_bytecode/java_enum_static_init_unwind_handler.cpp

@@ -86,7 +86,7 @@ void goto_symext::symex_goto(statet &state)
     unwind++;
 
     // continue unwinding?
-    if(get_unwind(state.source, unwind))
+    if(get_unwind(state.source, state.call_stack(), unwind))
     {
       // no!
       loop_bound_exceeded(state, new_guard);
@@ -540,6 +540,7 @@ void goto_symext::loop_bound_exceeded(
 
 bool goto_symext::get_unwind(
   const symex_targett::sourcet &source,
+  const goto_symex_statet::call_stackt &context,
   unsigned unwind)
 {
   // by default, we keep going