Fixes parameter detection on bytecode->goto translation

The JVM spec document (Sec. 3.6) mandates that Java method arguments occupy the
lowest local variables. The only sound way to detect which variable slots are
function parameters is by counting the number and type of arguments in the
method descriptor.

This commit adds a new function `java_method_parameter_slots` which can
determine the number of variable slots used by a method's parameters. It also
fixes `setup_local_variables` (which were previously checking whether
`v.start_pc=0` to determine if an LVT entry is a parameter).

Author: cesaro

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -30,6 +30,7 @@ Author: Daniel Kroening, [email protected]
 #include "java_bytecode_convert_method_class.h"
 #include "bytecode_info.h"
 #include "java_types.h"
+#include "java_utils.h"
 #include "java_string_library_preprocess.h"
 
 #include <limits>
@@ -106,25 +107,10 @@ static bool operator==(const irep_idt &what, const patternt &pattern)
   return pattern==what;
 }
 
-const size_t SLOTS_PER_INTEGER(1u);
-const size_t INTEGER_WIDTH(64u);
-static size_t count_slots(
-  const size_t value,
-  const code_typet::parametert &param)
-{
-  const std::size_t width(param.type().get_unsigned_int(ID_width));
-  return value+SLOTS_PER_INTEGER+width/INTEGER_WIDTH;
-}
-
-static size_t get_variable_slots(const code_typet::parametert &param)
-{
-  return count_slots(0, param);
-}
-
 static irep_idt strip_java_namespace_prefix(const irep_idt to_strip)
 {
   const auto to_strip_str=id2string(to_strip);
-  assert(has_prefix(to_strip_str, "java::"));
+  PRECONDITION(has_prefix(to_strip_str, "java::"));
   return to_strip_str.substr(6, std::string::npos);
 }
 
@@ -308,12 +294,22 @@ void java_bytecode_convert_methodt::convert(
   method_return_type=code_type.return_type();
   code_typet::parameterst &parameters=code_type.parameters();
 
+  // Determine the number of local variable slots used by the JVM to maintan the
+  // formal parameters
+  slots_for_parameters = java_method_parameter_slots(code_type);
+
+  debug() << "Generating codet: class "
+             << class_symbol.name << ", method "
+             << m.name << eom;
+
+  // We now set up the local variables for the method parameters
   variables.clear();
 
-  // find parameter names in the local variable table:
+  // Find parameter names in the local variable table:
   for(const auto &v : m.local_variable_table)
   {
-    if(v.start_pc!=0) // Local?
+    // Skip this variable if it is not a method parameter
+    if(!is_parameter(v))
       continue;
 
     typet t=java_type_from_string(v.signature);
@@ -335,8 +331,10 @@ void java_bytecode_convert_methodt::convert(
   for(const auto &param : parameters)
   {
     variables[param_index].resize(1);
-    param_index+=get_variable_slots(param);
+    param_index+=java_local_variable_slots(param.type());
   }
+  INVARIANT(param_index==slots_for_parameters,
+    "java_parameter_count and local computation must agree");
 
   // assign names to parameters
   param_index=0;
@@ -348,8 +346,6 @@ void java_bytecode_convert_methodt::convert(
     {
       base_name="this";
       identifier=id2string(method_identifier)+"::"+id2string(base_name);
-      param.set_base_name(base_name);
-      param.set_identifier(identifier);
     }
     else
     {
@@ -364,10 +360,9 @@ void java_bytecode_convert_methodt::convert(
         base_name="arg"+std::to_string(param_index)+suffix;
         identifier=id2string(method_identifier)+"::"+id2string(base_name);
       }
-
-      param.set_base_name(base_name);
-      param.set_identifier(identifier);
     }
+    param.set_base_name(base_name);
+    param.set_identifier(identifier);
 
     // add to symbol table
     parameter_symbolt parameter_symbol;
@@ -377,41 +372,34 @@ void java_bytecode_convert_methodt::convert(
     parameter_symbol.type=param.type();
     symbol_table.add(parameter_symbol);
 
-    // add as a JVM variable
-    std::size_t slots=get_variable_slots(param);
+    // Add as a JVM local variable
     variables[param_index][0].symbol_expr=parameter_symbol.symbol_expr();
     variables[param_index][0].is_parameter=true;
     variables[param_index][0].start_pc=0;
     variables[param_index][0].length=std::numeric_limits<size_t>::max();
-    variables[param_index][0].is_parameter=true;
-    param_index+=slots;
-    assert(param_index>0);
+    param_index+=java_local_variable_slots(param.type());
   }
 
+  // The parameter slots detected in this function should agree with what
+  // java_parameter_count() thinks about this method
+  INVARIANT(param_index==slots_for_parameters,
+    "java_parameter_count and local computation must agree");
+
   const bool is_virtual=!m.is_static && !m.is_final;
 
-  #if 0
-  class_type.methods().push_back(class_typet::methodt());
-  class_typet::methodt &method=class_type.methods().back();
-  #else
+  // Construct a methodt, which lives within the class type; this object is
+  // never used for anything useful and could be removed
   class_typet::methodt method;
-  #endif
-
   method.set_base_name(m.base_name);
   method.set_name(method_identifier);
-
   method.set(ID_abstract, m.is_abstract);
   method.set(ID_is_virtual, is_virtual);
-
+  method.type()=member_type;
   if(is_constructor(method))
     method.set(ID_constructor, true);
 
-  method.type()=member_type;
-
   // we add the symbol for the method
-
   symbolt method_symbol;
-
   method_symbol.name=method.get_name();
   method_symbol.base_name=method.get_base_name();
   method_symbol.mode=ID_java;
@@ -430,15 +418,13 @@ void java_bytecode_convert_methodt::convert(
     method_symbol.type.set(ID_constructor, true);
   current_method=method_symbol.name;
   method_has_this=code_type.has_this();
-
-  tmp_vars.clear();
   if((!m.is_abstract) && (!m.is_native))
-    method_symbol.value=convert_instructions(
-      m, code_type, method_symbol.name);
+    method_symbol.value=convert_instructions(m, code_type, method_symbol.name);
 
   // Replace the existing stub symbol with the real deal:
   const auto s_it=symbol_table.symbols.find(method.get_name());
-  assert(s_it!=symbol_table.symbols.end());
+  INVARIANT(s_it!=symbol_table.symbols.end(),
+    "the symbol was there earlier on this function; it must be there now");
   symbol_table.symbols.erase(s_it);
 
   symbol_table.add(method_symbol);
@@ -1138,6 +1124,12 @@ codet java_bytecode_convert_methodt::convert_instructions(
     }
   }
 
+  // Clean the list of temporary variables created by a call to `tmp_variable`.
+  // These are local variables in the goto function used to represent temporary
+  // values of the JVM operand stack, newly allocated objects before the
+  // constructor is called, ...
+  tmp_vars.clear();
+
   // Now that the control flow graph is built, set up our local variables
   // (these require the graph to determine live ranges)
   setup_local_variables(method, address_map);

src/java_bytecode/java_bytecode_convert_method_class.h

@@ -41,7 +41,8 @@ class java_bytecode_convert_methodt:public messaget
     symbol_table(_symbol_table),
     max_array_length(_max_array_length),
     lazy_methods(_lazy_methods),
-    string_preprocess(_string_preprocess)
+    string_preprocess(_string_preprocess),
+    slots_for_parameters(0)
   {
   }
 
@@ -66,6 +67,11 @@ class java_bytecode_convert_methodt:public messaget
   typet method_return_type;
   java_string_library_preprocesst &string_preprocess;
 
+  /// Number of local variable slots used by the JVM to pass parameters upon
+  /// invocation of the method under translation.
+  /// Initialized in `convert`.
+  unsigned slots_for_parameters;
+
 public:
   struct holet
   {
@@ -76,6 +82,7 @@ class java_bytecode_convert_methodt:public messaget
   struct local_variable_with_holest
   {
     local_variablet var;
+    bool is_parameter;
     std::vector<holet> holes;
   };
 
@@ -149,6 +156,14 @@ class java_bytecode_convert_methodt:public messaget
 
   bool is_constructor(const class_typet::methodt &method);
 
+  /// Returns true iff the slot index of the local variable of a method (coming
+  /// from the LVT) is a parameter of that method. Assumes that
+  /// `slots_for_parameters` is initialized upon call.
+  bool is_parameter(const local_variablet &v)
+  {
+    return v.index < slots_for_parameters;
+  }
+
   struct converted_instructiont
   {
     converted_instructiont(

src/java_bytecode/java_local_variable_table.cpp

@@ -11,6 +11,7 @@ Author: Chris Smowton, [email protected]
 
 #include "java_bytecode_convert_method_class.h"
 #include "java_types.h"
+#include "java_utils.h"
 
 #include <util/string2int.h>
 
@@ -55,7 +56,7 @@ struct procedure_local_cfg_baset<
     for(const auto &table_entry : method.exception_table)
     {
       auto findit=amap.find(table_entry.start_pc);
-      assert(findit!=amap.end() &&
+      INVARIANT(findit!=amap.end(),
              "Exception table entry doesn't point to an instruction?");
       for(; findit->first<table_entry.end_pc; ++findit)
       {
@@ -186,9 +187,11 @@ static bool is_store_to_slot(
   else
   {
     // Store shorthands, like "store_0", "store_1"
-    assert(prevstatement[6]=='_' && prevstatement.size()==8);
+    INVARIANT(prevstatement[6]=='_' && prevstatement.size()==8,
+      "expected store instruction looks like store_0, store_1...");
     storeslot=prevstatement[7];
-    assert(isdigit(storeslot[0]));
+    INVARIANT(isdigit(storeslot[0]),
+      "store_? instructions should end in a digit");
   }
   auto storeslotidx=safe_string2unsigned(storeslot);
   return storeslotidx==slotidx;
@@ -203,7 +206,7 @@ static void maybe_add_hole(
   unsigned from,
   unsigned to)
 {
-  assert(to>=from);
+  PRECONDITION(to>=from);
   if(to!=from)
     var.holes.push_back({from, to-from});
 }
@@ -230,7 +233,7 @@ static void populate_variable_address_map(
         idx!=idxlim;
         ++idx)
     {
-      assert((!live_variable_at_address[idx]) && "Local variable table clash?");
+      INVARIANT(!live_variable_at_address[idx], "Local variable table clash?");
       live_variable_at_address[idx]=&*it;
     }
   }
@@ -261,20 +264,28 @@ static void populate_predecessor_map(
   messaget msg(msg_handler);
   for(auto it=firstvar, itend=varlimit; it!=itend; ++it)
   {
-    // Parameters are irrelevant to us and shouldn't be changed:
-    if(it->var.start_pc==0)
+    // All entries of the "local_variable_table_with_holest" processed in this
+    // function concern the same Java Local Variable Table slot/register. This
+    // is because "find_initialisers()" has already sorted them.
+    INVARIANT(it->var.index==firstvar->var.index,
+      "all entries are for the same local variable slot");
+
+    // Parameters are irrelevant to us and shouldn't be changed. This is because
+    // they cannot have live predecessor ranges: they are initialized by the JVM
+    // and no other live variable range can flow into them.
+    if(it->is_parameter)
       continue;
 
     // Find the last instruction within the live range:
     unsigned end_pc=it->var.start_pc+it->var.length;
     auto amapit=amap.find(end_pc);
-    assert(amapit!=amap.begin());
+    INVARIANT(amapit!=amap.begin(),
+      "current bytecode shall not be the first");
     auto old_amapit=amapit;
     --amapit;
     if(old_amapit==amap.end())
     {
-      assert(
-        end_pc>amapit->first &&
+      INVARIANT(end_pc>amapit->first,
         "Instruction live range doesn't align to instruction boundary?");
     }
 
@@ -287,7 +298,8 @@ static void populate_predecessor_map(
         auto pred_var=
           (pred<live_variable_at_address.size() ?
            live_variable_at_address[pred] :
-           0);
+           nullptr);
+
         if(pred_var==&*it)
         {
           // Flow from within same live range?
@@ -299,7 +311,8 @@ static void populate_predecessor_map(
           // Check if this is an initialiser, and if so expand the live range
           // to include it, but don't check its predecessors:
           auto inst_before_this=amapit;
-          assert(inst_before_this!=amap.begin());
+          INVARIANT(inst_before_this!=amap.begin(),
+            "we shall not be on the first bytecode of the method");
           --inst_before_this;
           if(amapit->first!=it->var.start_pc || inst_before_this->first!=pred)
           {
@@ -360,7 +373,7 @@ static unsigned get_common_dominator(
   const std::set<local_variable_with_holest*> &merge_vars,
   const java_cfg_dominatorst &dominator_analysis)
 {
-  assert(!merge_vars.empty());
+  PRECONDITION(!merge_vars.empty());
 
   unsigned first_pc=UINT_MAX;
   for(auto v : merge_vars)
@@ -652,10 +665,11 @@ void java_bytecode_convert_methodt::setup_local_variables(
   dominator_analysis(dominator_args);
 
   // Find out which local variable table entries should be merged:
-  // Wrap each entry so we have somewhere to record live ranges with holes:
+  // Wrap each entry so we have a data structure to work during function calls,
+  // where we record live ranges with holes:
   std::vector<local_variable_with_holest> vars_with_holes;
   for(const auto &v : m.local_variable_table)
-    vars_with_holes.push_back({v, {}});
+    vars_with_holes.push_back({v, is_parameter(v), {}});
 
   // Merge variable records:
   find_initialisers(vars_with_holes, amap, dominator_analysis);
@@ -673,7 +687,7 @@ void java_bytecode_convert_methodt::setup_local_variables(
   // length values in the local variable table
   for(const auto &v : vars_with_holes)
   {
-    if(v.var.start_pc==0) // Parameter?
+    if(v.is_parameter)
       continue;
 
     typet t=java_type_from_string(v.var.signature);