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.

Author: smowton

src/java_bytecode/java_bytecode_convert.cpp

@@ -808,7 +808,7 @@ codet java_bytecode_convertt::convert_instructions(
     }
     else if(statement=="invokedynamic")
     {
-      // not used in Java
+      // TODO: Java 8 lambdas use this.
       code_typet &code_type=to_code_type(arg0.type());
       const code_typet::parameterst &parameters(code_type.parameters());
 
@@ -866,17 +866,21 @@ codet java_bytecode_convertt::convert_instructions(
 
       // do some type adjustment for the arguments,
       // as Java promotes arguments
+      // Also cast pointers since intermediate locals
+      // can be void*.
 
       for(unsigned i=0; i<parameters.size(); i++)
       {
         const typet &type=parameters[i].type();
         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);
         }
       }
 
@@ -968,13 +972,12 @@ codet java_bytecode_convertt::convert_instructions(
       assert(op.size()==1 && results.empty());
 
       exprt var=variable(arg0, statement[0]);
-      
-      const bool is_array('a' == statement[0]);
-      
-      if(is_array)
-        var.type()=op[0].type();
 
-      c=code_assignt(var, op[0]);
+      exprt toassign=op[0];
+      if('a'==statement[0] && toassign.type()!=var.type())
+        toassign=typecast_exprt(toassign,var.type());
+
+      c=code_assignt(var,toassign);
     }
     else if(statement==patternt("?aload"))
     {
@@ -1135,7 +1138,7 @@ codet java_bytecode_convertt::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));