Fall back to anonlocal:: local variables for goto functions if LVT contains unexpected entries

regression/cbmc-java/lvt-groovy/test.desc

@@ -0,0 +1,7 @@
+CORE
+DetectSplitPackagesTask.class
+--show-symbol-table
+^EXIT=0$
+^SIGNAL=0$
+--
+--

regression/cbmc-java/lvt-unexpected/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 unexpected.class
 --verbosity 10 --show-symbol-table
 ^EXIT=0$

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -186,6 +186,21 @@ symbol_exprt java_bytecode_convert_methodt::tmp_variable(
   return result;
 }
 
+/// Returns a symbol_exprt indicating a local variable suitable to load/store
+/// from a bytecode at address `address` a value of type `type_char` stored in
+/// the JVM's slot `arg`.
+///
+/// \param arg
+///   The local variable slot
+/// \param type_char
+///   The type of the value stored in the slot pointed by `arg`.
+/// \param address
+///   Bytecode address used to find a variable that the LVT declares to be live
+///   and living in the slot pointed by `arg` for this bytecode.
+/// \param do_cast
+///   Indicates whether we should return the original symbol_exprt or a
+///   typecast_exprt if the type of the symbol_exprt does not equal that
+///   represented by `type_char`.
 const exprt java_bytecode_convert_methodt::variable(
   const exprt &arg,
   char type_char,

src/java_bytecode/java_local_variable_table.cpp

@@ -289,10 +289,12 @@ static void populate_predecessor_map(
     if(it->is_parameter)
       continue;
 
-    msg.debug() << "ppm: processing var idx " << it->var.index
+#ifdef DEBUG
+    msg.debug() << "jcm: ppm: processing var idx " << it->var.index
                 << " name '" << it->var.name << "' start-pc "
                 << it->var.start_pc << " len " << it->var.length
                 << "; holes " << it->holes.size() << messaget::eom;
+#endif
 
     // Find the last instruction within the live range:
     unsigned end_pc=it->var.start_pc+it->var.length;
@@ -362,11 +364,11 @@ static void populate_predecessor_map(
                *(inst_before_this->second.source),
                it->var.index))
           {
-            msg.error() << "Local variable table: didn't find initializing "
-                        << "store for predecessor of bytecode at address "
-                        << amapit->first << " ("
-                        << amapit->second.predecessors.size()
-                        << " predecessors)" << msg.eom;
+            msg.warning() << "Local variable table: didn't find initializing "
+                          << "store for predecessor of bytecode at address "
+                          << amapit->first << " ("
+                          << amapit->second.predecessors.size()
+                          << " predecessors)" << msg.eom;
             throw "local variable table: unexpected live ranges";
           }
           new_start_pc=pred;
@@ -541,7 +543,7 @@ static void merge_variable_table_entries(
 /// Given a sequence of users of the same local variable slot, this figures out
 /// which ones are related by control flow, and combines them into a single
 /// entry with holes, such that after combination we can create a single
-/// declaration per variable table entry, placed at the live range's start
+/// GOTO variable per variable table entry, placed at the live range's start
 /// address, which may be moved back so that the declaration dominates all uses.
 /// \par parameters: `firstvar`-`varlimit`: sequence of variable table entries,
 ///   all of which should concern the same slot index.
@@ -720,8 +722,24 @@ void java_bytecode_convert_methodt::setup_local_variables(
   for(const auto &v : m.local_variable_table)
     vars_with_holes.push_back({v, is_parameter(v), {}});
 
-  // Merge variable records:
-  find_initializers(vars_with_holes, amap, dominator_analysis);
+  // Merge variable records. See documentation of in
+  // `find_initializers_for_slot` for more details. If the strategy employed
+  // there fails with an exception, we just ignore the LVT for this method, no
+  // variable is generated in `this->variables[]` (because we return here and
+  // dont let the for loop below to execute), and as a result the method
+  // this->variable() will be forced to create new `anonlocal::` variables, as
+  // the only source of variable names for that method is `this->variables[]`.
+  try
+  {
+    find_initializers(vars_with_holes, amap, dominator_analysis);
+  }
+  catch(const char *message)
+  {
+    warning() << "Bytecode -> codet translation error: " << message << eom
+              << "This is probably due to an unexpected LVT, "
+              << "falling back to translation without LVT" << eom;
+    return;
+  }
 
   // Clean up removed records from the variable table:
   cleanup_var_table(vars_with_holes);