From 043f02f68b6ec46c015ce47a869b205793e62dc2 Mon Sep 17 00:00:00 2001
From: Chris Smowton <chris@smowton.net>
Date: Wed, 3 Aug 2016 11:09:44 +0100
Subject: [PATCH] Treat all anonymous locals as void*

The existing code tried to infer local type from the assignment, but (a) the information wasn't recorded in the variable table leading to later misuse, and (b) I'm not convinced it's safe to infer types for locals this way because a pattern like if(x) a = new A(); else a = new B(); (where A and B are unrelated) can use the same local slot for both classes. In this case we'd want to give it java.lang.Object* type.

In view of all this it is surely simplest to just treat locals as generic, like the bytecode does, then cast the void* to needed types at use sites.
---
 .../java_bytecode_convert_method.cpp          | 19 +++++++++++--------
 1 file changed, 11 insertions(+), 8 deletions(-)

diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp
index a289ee14f58..19685508b00 100644
--- a/src/java_bytecode/java_bytecode_convert_method.cpp
+++ b/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -731,6 +731,8 @@ codet java_bytecode_convert_methodt::convert_instructions(
 
       // do some type adjustment for the arguments,
       // as Java promotes arguments
+      // Also cast pointers since intermediate locals
+      // can be void*.
 
       for(std::size_t i=0; i<parameters.size(); i++)
       {
@@ -738,10 +740,12 @@ codet java_bytecode_convert_methodt::convert_instructions(
         if(type==java_boolean_type() ||
            type==java_char_type() ||
            type==java_byte_type() ||
-           type==java_short_type())
+           type==java_short_type() ||
+           type.id()==ID_pointer)
         {
           assert(i<call.arguments().size());
-          call.arguments()[i].make_typecast(type);
+          if(type!=call.arguments()[i].type())
+            call.arguments()[i].make_typecast(type);
         }
       }
 
@@ -831,12 +835,11 @@ codet java_bytecode_convert_methodt::convert_instructions(
 
       exprt var=variable(arg0, statement[0], i_it->address, INST_INDEX);
 
-      const bool is_array('a' == statement[0]);
+      exprt toassign=op[0];
+      if('a'==statement[0] && toassign.type()!=var.type())
+        toassign=typecast_exprt(toassign, var.type());
 
-      if(is_array)
-        var.type()=op[0].type();
-
-      c=code_assignt(var, op[0]);
+      c=code_assignt(var, toassign);
     }
     else if(statement==patternt("?aload"))
     {
@@ -997,7 +1000,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
       irep_idt number=to_constant_expr(arg0).get_value();
       assert(op.size()==1 && results.empty());
       code_ifthenelset code_branch;
-      const typecast_exprt lhs(op[0], pointer_typet());
+      const typecast_exprt lhs(op[0], pointer_typet(empty_typet()));
       const exprt rhs(gen_zero(lhs.type()));
       code_branch.cond()=binary_relation_exprt(lhs, ID_notequal, rhs);
       code_branch.then_case()=code_gotot(label(number));