Documentation: functionality around setup_local_variables

- The commit also contains some lightweight code style changes and a function
  has been renamed

Author: cesaro

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -109,9 +109,11 @@ static bool operator==(const irep_idt &what, const patternt &pattern)
 
 static irep_idt strip_java_namespace_prefix(const irep_idt to_strip)
 {
-  const auto to_strip_str=id2string(to_strip);
-  PRECONDITION(has_prefix(to_strip_str, "java::"));
-  return to_strip_str.substr(6, std::string::npos);
+  const std::string to_strip_str=id2string(to_strip);
+  const std::string prefix="java::";
+
+  PRECONDITION(has_prefix(to_strip_str, prefix));
+  return to_strip_str.substr(prefix.size(), std::string::npos);
 }
 
 // name contains <init> or <clinit>
@@ -283,20 +285,26 @@ void java_bytecode_convert_methodt::convert(
   const symbolt &class_symbol,
   const methodt &m)
 {
+  // Construct the fully qualified method name
+  // (e.g. "my.package.ClassName.myMethodName:(II)I") and query the symbol table
+  // to retrieve the symbol (constructed by java_bytecode_convert_method_lazy)
+  // associated to the method
   const irep_idt method_identifier=
     id2string(class_symbol.name)+"."+id2string(m.name)+":"+m.signature;
   method_id=method_identifier;
 
   const auto &old_sym=symbol_table.lookup(method_identifier);
 
+  // Obtain a std::vector of code_typet::parametert objects from the
+  // (function) type of the symbol
   typet member_type=old_sym.type;
   code_typet &code_type=to_code_type(member_type);
   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);
+  slots_for_parameters=java_method_parameter_slots(code_type);
 
   debug() << "Generating codet: class "
              << class_symbol.name << ", method "
@@ -312,49 +320,70 @@ void java_bytecode_convert_methodt::convert(
     if(!is_parameter(v))
       continue;
 
+    // Construct a fully qualified name for the parameter v,
+    // e.g. my.package.ClassName.myMethodName:(II)I::anIntParam, and then a
+    // symbol_exprt with the parameter and its type
     typet t=java_type_from_string(v.signature);
     std::ostringstream id_oss;
     id_oss << method_id << "::" << v.name;
     irep_idt identifier(id_oss.str());
     symbol_exprt result(identifier, t);
     result.set(ID_C_base_name, v.name);
 
+    // Create a new variablet in the variables vector; in fact this entry will
+    // be rewritten below in the loop that iterates through the method
+    // parameters; the only field that seem to be useful to write here is the
+    // symbol_expr, others will be rewritten
     variables[v.index].push_back(variablet());
     auto &newv=variables[v.index].back();
     newv.symbol_expr=result;
     newv.start_pc=v.start_pc;
     newv.length=v.length;
   }
 
-  // set up variables array
+  // The variables is a expanding_vectort, and the loop above may have expanded
+  // the vector introducing gaps where the entries are empty vectors. We now
+  // make sure that the vector of each LV slot contains exactly one variablet,
+  // possibly default-initialized
   std::size_t param_index=0;
   for(const auto &param : parameters)
   {
     variables[param_index].resize(1);
     param_index+=java_local_variable_slots(param.type());
   }
-  INVARIANT(param_index==slots_for_parameters,
+  INVARIANT(
+    param_index==slots_for_parameters,
     "java_parameter_count and local computation must agree");
 
-  // assign names to parameters
+  // Assign names to parameters
   param_index=0;
   for(auto &param : parameters)
   {
     irep_idt base_name, identifier;
 
+    // Construct a sensible base name (base_name) and a fully qualified name
+    // (identifier) for every parameter of the method under translation,
+    // regardless of whether we have an LVT or not; and assign it to the
+    // parameter object (which is stored in the type of the symbol, not in the
+    // symbol table)
     if(param_index==0 && param.get_this())
     {
+      // my.package.ClassName.myMethodName:(II)I::this
       base_name="this";
       identifier=id2string(method_identifier)+"::"+id2string(base_name);
     }
     else
     {
-      // in the variable table?
+      // if already present in the LVT ...
       base_name=variables[param_index][0].symbol_expr.get(ID_C_base_name);
       identifier=variables[param_index][0].symbol_expr.get(ID_identifier);
 
+      // ... then base_name will not be empty
       if(base_name.empty())
       {
+        // my.package.ClassName.myMethodName:(II)I::argNT, where N is the local
+        // variable slot where the parameter is stored and T is a character
+        // indicating the type
         const typet &type=param.type();
         char suffix=java_char_from_type(type);
         base_name="arg"+std::to_string(param_index)+suffix;
@@ -364,7 +393,7 @@ void java_bytecode_convert_methodt::convert(
     param.set_base_name(base_name);
     param.set_identifier(identifier);
 
-    // add to symbol table
+    // Build a new symbol for the parameter and add it to the symbol table
     parameter_symbolt parameter_symbol;
     parameter_symbol.base_name=base_name;
     parameter_symbol.mode=ID_java;
@@ -382,7 +411,8 @@ void java_bytecode_convert_methodt::convert(
 
   // The parameter slots detected in this function should agree with what
   // java_parameter_count() thinks about this method
-  INVARIANT(param_index==slots_for_parameters,
+  INVARIANT(
+    param_index==slots_for_parameters,
     "java_parameter_count and local computation must agree");
 
   const bool is_virtual=!m.is_static && !m.is_final;
@@ -406,6 +436,10 @@ void java_bytecode_convert_methodt::convert(
   method_symbol.location=m.source_location;
   method_symbol.location.set_function(method_identifier);
 
+  // Set up the pretty name for the method entry in the symbol table.
+  // The pretty name of a constructor includes the base name of the class
+  // instead of the internal method name "<init>". For regular methods, it's
+  // just the base name of the method.
   if(method.get_base_name()=="<init>")
     method_symbol.pretty_name=id2string(class_symbol.pretty_name)+"."+
                               id2string(class_symbol.base_name)+"()";
@@ -416,17 +450,20 @@ void java_bytecode_convert_methodt::convert(
   method_symbol.type=member_type;
   if(is_constructor(method))
     method_symbol.type.set(ID_constructor, true);
+
   current_method=method_symbol.name;
   method_has_this=code_type.has_this();
   if((!m.is_abstract) && (!m.is_native))
     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());
-  INVARIANT(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);
 
+  // Insert the method symbol in the symbol table
   symbol_table.add(method_symbol);
 }
 

src/java_bytecode/java_bytecode_convert_method_class.h

@@ -62,9 +62,18 @@ class java_bytecode_convert_methodt:public messaget
   const size_t max_array_length;
   safe_pointer<ci_lazy_methodst> lazy_methods;
 
+  /// Fully qualified name of the method under translation.
+  /// Initialized by `convert`.
+  /// Example: "my.package.ClassName.myMethodName:(II)I"
   irep_idt method_id;
+
+  /// A copy of `method_id` :/
   irep_idt current_method;
+
+  /// Return type of the method under conversion.
+  /// Initialized by `convert`.
   typet method_return_type;
+
   java_string_library_preprocesst &string_preprocess;
 
   /// Number of local variable slots used by the JVM to pass parameters upon
@@ -100,7 +109,7 @@ class java_bytecode_convert_methodt:public messaget
     variablet() : symbol_expr(), start_pc(0), length(0), is_parameter(false) {}
   };
 
- protected:
+protected:
   typedef std::vector<variablet> variablest;
   expanding_vectort<variablest> variables;
   std::set<symbol_exprt> used_local_names;
@@ -154,14 +163,16 @@ class java_bytecode_convert_methodt:public messaget
   void pop_residue(std::size_t n);
   void push(const exprt::operandst &o);
 
+  /// Determines whether the `method` is a constructor or a static initializer,
+  /// by checking whether its name equals either <init> or <clinit>
   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;
+    return v.index<slots_for_parameters;
   }
 
   struct converted_instructiont
@@ -186,12 +197,12 @@ class java_bytecode_convert_methodt:public messaget
     java_cfg_dominatorst;
 
 protected:
-  void find_initialisers(
+  void find_initializers(
     local_variable_table_with_holest &vars,
     const address_mapt &amap,
     const java_cfg_dominatorst &doms);
 
-  void find_initialisers_for_slot(
+  void find_initializers_for_slot(
     local_variable_table_with_holest::iterator firstvar,
     local_variable_table_with_holest::iterator varlimit,
     const address_mapt &amap,

src/java_bytecode/java_bytecode_language.cpp

@@ -401,7 +401,7 @@ bool java_bytecode_languaget::typecheck(
     if(c_it->second.parsed_class.name.empty())
       continue;
 
-    debug() << "Converting class " << c_it->first << eom;
+    debug() << "Generating class/member symbols: " << c_it->first << eom;
 
     if(java_bytecode_convert_class(
          c_it->second,