Add temporary variables for values on stack for write operations

concerned bytecode instructions:
 - iinc
 - pustatic
 - putfield
 - ?store
 - ?astore

Author: Matthias Güdemann

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -1319,15 +1319,24 @@ codet java_bytecode_convert_methodt::convert_instructions(
       typet element_type=data_ptr.type().subtype();
       const dereference_exprt element(data_plus_offset, element_type);
 
-      c=code_blockt();
+      code_blockt block;
+      block.add_source_location()=i_it->source_location;
+
+      save_stack_entries(
+        "stack_astore",
+        element_type,
+        block,
+        bytecode_write_typet::ARRAY_REF,
+        "");
+
       codet bounds_check=
         get_array_bounds_check(deref, op[1], i_it->source_location);
       bounds_check.add_source_location()=i_it->source_location;
-      c.move_to_operands(bounds_check);
+      block.move_to_operands(bounds_check);
       code_assignt array_put(element, op[2]);
       array_put.add_source_location()=i_it->source_location;
-      c.move_to_operands(array_put);
-      c.add_source_location()=i_it->source_location;
+      block.move_to_operands(array_put);
+      c=block;
     }
     else if(statement==patternt("?store"))
     {
@@ -1336,12 +1345,24 @@ codet java_bytecode_convert_methodt::convert_instructions(
 
       exprt var=
         variable(arg0, statement[0], i_it->address, NO_CAST);
+      const irep_idt &var_name=to_symbol_expr(var).get_identifier();
 
       exprt toassign=op[0];
       if('a'==statement[0] && toassign.type()!=var.type())
         toassign=typecast_exprt(toassign, var.type());
 
-      c=code_assignt(var, toassign);
+      code_blockt block;
+
+      save_stack_entries(
+        "stack_store",
+        toassign.type(),
+        block,
+        bytecode_write_typet::VARIABLE,
+        var_name);
+      code_assignt assign(var, toassign);
+      assign.add_source_location()=i_it->source_location;
+      block.copy_to_operands(assign);
+      c=block;
     }
     else if(statement==patternt("?aload"))
     {
@@ -1587,13 +1608,25 @@ codet java_bytecode_convert_methodt::convert_instructions(
     }
     else if(statement=="iinc")
     {
+      code_blockt block;
+      block.add_source_location()=i_it->source_location;
+      // search variable on stack
+      const exprt &locvar=variable(arg0, 'i', i_it->address, NO_CAST);
+      save_stack_entries(
+        "stack_iinc",
+        java_int_type(),
+        block,
+        bytecode_write_typet::VARIABLE,
+        to_symbol_expr(locvar).get_identifier());
+
       code_assignt code_assign;
       code_assign.lhs()=
         variable(arg0, 'i', i_it->address, NO_CAST);
       code_assign.rhs()=plus_exprt(
         variable(arg0, 'i', i_it->address, CAST_AS_NEEDED),
         typecast_exprt(arg1, java_int_type()));
-      c=code_assign;
+      block.copy_to_operands(code_assign);
+      c=block;
     }
     else if(statement==patternt("?xor"))
     {
@@ -1828,7 +1861,15 @@ codet java_bytecode_convert_methodt::convert_instructions(
     else if(statement=="putfield")
     {
       assert(op.size()==2 && results.size()==0);
-      c=code_assignt(to_member(op[0], arg0), op[1]);
+      code_blockt block;
+      save_stack_entries(
+        "stack_field",
+        op[1].type(),
+        block,
+        bytecode_write_typet::FIELD,
+        arg0.get(ID_component_name));
+      block.copy_to_operands(code_assignt(to_member(op[0], arg0), op[1]));
+      c=block;
     }
     else if(statement=="putstatic")
     {
@@ -1841,7 +1882,17 @@ codet java_bytecode_convert_methodt::convert_instructions(
         lazy_methods->add_needed_class(
           to_symbol_type(arg0.type()).get_identifier());
       }
-      c=code_assignt(symbol_expr, op[0]);
+      code_blockt block;
+      block.add_source_location()=i_it->source_location;
+
+      save_stack_entries(
+        "stack_static_field",
+        symbol_expr.type(),
+        block,
+        bytecode_write_typet::STATIC_FIELD,
+        symbol_expr.get_identifier());
+      block.copy_to_operands(code_assignt(symbol_expr, op[0]));
+      c=block;
     }
     else if(statement==patternt("?2?")) // i2c etc.
     {
@@ -1860,6 +1911,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
 
       const exprt tmp=tmp_variable("new", ref_type);
       c=code_assignt(tmp, java_new_expr);
+      c.add_source_location()=i_it->source_location;
       results[0]=tmp;
     }
     else if(statement=="newarray" ||
@@ -2443,3 +2495,81 @@ void java_bytecode_convert_method(
 
   java_bytecode_convert_method(class_symbol, method);
 }
+
+/*******************************************************************\
+
+Function: java_bytecode_convert_methodt::save_stack_entries
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: create temporary variables if a write instruction can have undesired
+          side-effects
+
+\*******************************************************************/
+
+void java_bytecode_convert_methodt::save_stack_entries(
+  const std::string &tmp_var_prefix,
+  const typet &tmp_var_type,
+  code_blockt &block,
+  const bytecode_write_typet write_type,
+  const irep_idt &identifier)
+{
+  for(auto &stack_entry : stack)
+  {
+    // remove typecasts if existing
+    while(stack_entry.id()==ID_typecast)
+      stack_entry=to_typecast_expr(stack_entry).op();
+
+    // variables or static fields and symbol -> save symbols with same id
+    if((write_type==bytecode_write_typet::VARIABLE ||
+        write_type==bytecode_write_typet::STATIC_FIELD) &&
+       stack_entry.id()==ID_symbol)
+    {
+      const symbol_exprt &var=to_symbol_expr(stack_entry);
+      if(var.get_identifier()==identifier)
+        create_stack_tmp_var(tmp_var_prefix, tmp_var_type, block, stack_entry);
+    }
+
+    // array reference and dereference -> save all references on the stack
+    else if(write_type==bytecode_write_typet::ARRAY_REF &&
+            stack_entry.id()==ID_dereference)
+      create_stack_tmp_var(tmp_var_prefix, tmp_var_type, block, stack_entry);
+
+    // field and member access -> compare component name
+    else if(write_type==bytecode_write_typet::FIELD &&
+            stack_entry.id()==ID_member)
+    {
+      const irep_idt &entry_id=
+        to_member_expr(stack_entry).get_component_name();
+      if(entry_id==identifier)
+        create_stack_tmp_var(tmp_var_prefix, tmp_var_type, block, stack_entry);
+    }
+  }
+}
+
+/*******************************************************************\
+
+Function: java_bytecode_convert_methodt::create_stack_tmp_var
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: actually create a temporary variable to hold the value of a stack
+          entry
+
+\*******************************************************************/
+
+void java_bytecode_convert_methodt::create_stack_tmp_var(
+  const std::string &tmp_var_prefix,
+  const typet &tmp_var_type,
+  code_blockt &block,
+  exprt &stack_entry)
+{
+  const exprt tmp_var=
+    tmp_variable(tmp_var_prefix, tmp_var_type);
+  block.copy_to_operands(code_assignt(tmp_var, stack_entry));
+  stack_entry=tmp_var;
+}

src/java_bytecode/java_bytecode_convert_method_class.h

@@ -215,6 +215,19 @@ class java_bytecode_convert_methodt:public messaget
     const code_typet &);
 
   const bytecode_infot &get_bytecode_info(const irep_idt &statement);
+
+  enum class bytecode_write_typet { VARIABLE, ARRAY_REF, STATIC_FIELD, FIELD};
+  void save_stack_entries(
+    const std::string &,
+    const typet &,
+    code_blockt &,
+    const bytecode_write_typet,
+    const irep_idt &);
+  void create_stack_tmp_var(
+    const std::string &,
+    const typet &,
+    code_blockt &,
+    exprt &);
 };
 
 #endif