Add Java locals to the symbol table and give them declarations

This is required for SSA renaming to work on Java local symbols.

Author: smowton

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -82,11 +82,12 @@ class java_bytecode_convert_methodt:public messaget
     symbol_exprt symbol_expr;
     size_t start_pc;
     size_t length;
+    bool is_parameter;
   };
 
   typedef std::vector<variablet> variablest;
   expanding_vector<variablest> variables;
-
+  std::set<symbol_exprt> used_local_names;
   bool method_has_this;
 
   typedef enum instruction_sizet
@@ -150,13 +151,16 @@ class java_bytecode_convert_methodt:public messaget
 
       symbol_exprt result(identifier, t);
       result.set(ID_C_base_name, base_name);
+      used_local_names.insert(result);
 
       return result;
     }
     else
     {
       exprt result=var.symbol_expr;
-      if(do_cast==CAST_AS_NEEDED && t!=result.type()) result=typecast_exprt(result, t);
+      if(!var.is_parameter)
+        used_local_names.insert(to_symbol_expr(result));
+      if(do_cast==CAST_AS_NEEDED && t!=result.type()) result=typecast_exprt(result, t);      
       return result;
     }
   }
@@ -379,6 +383,7 @@ void java_bytecode_convert_methodt::convert(
     variables[param_index][0].symbol_expr=parameter_symbol.symbol_expr();
     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;
   }
 
@@ -1529,6 +1534,22 @@ codet java_bytecode_convert_methodt::convert_instructions(
   // review successor computation of athrow!
   code_blockt code;
 
+  // locals
+  for(const auto & var : used_local_names)
+  {
+    code.add(code_declt(var));
+    symbolt new_symbol;
+    new_symbol.name=var.get_identifier();
+    new_symbol.type=var.type();
+    new_symbol.base_name=var.get(ID_C_base_name);
+    new_symbol.pretty_name=id2string(var.get_identifier()).substr(6, std::string::npos);
+    new_symbol.mode=ID_java;
+    new_symbol.is_type=false;
+    new_symbol.is_file_local=true;
+    new_symbol.is_thread_local=true;
+    new_symbol.is_lvalue=true;
+    symbol_table.add(new_symbol);
+  }
   // temporaries
   for(const auto & var : tmp_vars)
   {