fix type inconsistencies when using temporary

[kroening]

Triggers type inconsistency in bitand expression in
org.apache.tika.io.LookaheadInputStream.read()

[allredj]

Passed Diffblue compatibility checks (cbmc commit: dec622c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/77781049

[smowton]

So this will cause the code below to get hit much less often (looking for symbol, or deref, or member operator at top level) -- what is the upshot of this? Did this code ever have tests? If not this bug surely cries out for some, perhaps requested from @mgudemann as the original author?

[mgudemann]

@smowton there are some (synthetic, compiled via Jasmin byecode assembler) regression tests, cf. #931 I'll try to find the bytecodes here and add one that recreates the above situation.
@kroening I'll have a closer look whether the typcecast removal is/was required

[mgudemann]

@kroening How about the following fix (tested on the above class from Tika)

1 file changed, 21 insertions(+), 14 deletions(-)
.../java_bytecode/java_bytecode_convert_method.cpp | 35 +++++++++++++---------

modified   jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -3185,31 +3185,38 @@ void java_bytecode_convert_methodt::save_stack_entries(
   for(auto &stack_entry : stack)
   {
     // remove typecasts if existing
-    while(stack_entry.id()==ID_typecast)
-      stack_entry=to_typecast_expr(stack_entry).op();
+    auto entry = std::ref(stack_entry);
+    while(entry.get().id() == ID_typecast)
+    {
+      entry = std::ref(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)
+    if(
+      (write_type == bytecode_write_typet::VARIABLE ||
+       write_type == bytecode_write_typet::STATIC_FIELD) &&
+      entry.get().id() == ID_symbol)
     {
-      const symbol_exprt &var=to_symbol_expr(stack_entry);
-      if(var.get_identifier()==identifier)
+      const symbol_exprt &var = to_symbol_expr(entry.get());
+      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)
+    else if(
+      write_type == bytecode_write_typet::ARRAY_REF &&
+      entry.get().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)
+    else if(
+      write_type == bytecode_write_typet::FIELD &&
+      entry.get().id() == ID_member)
     {
-      const irep_idt &entry_id=
-        to_member_expr(stack_entry).get_component_name();
-      if(entry_id==identifier)
+      const irep_idt &entry_id = to_member_expr(entry).get_component_name();
+      if(entry_id == identifier)
         create_stack_tmp_var(tmp_var_prefix, tmp_var_type, block, stack_entry);
     }
   }

so we unwrap the typecasts in an auxiliary variable, check the base expression for its identifier, ID_dereference or component name and then modify the stack entry but keep the original casts?

[mgudemann]

see #2507

[kroening]

I am concerned that the problem is deeper -- on the stack, there might be an arbitrarily complicated expression, say s.th. like 1+7*SOME_VAR, and SOME_VAR gets modified. I.e., I think the 'search' needs to do a full expression traversal.
Yes, the original expression should then be saved.

[mgudemann]

Ok, I see the point. We could write an expression visitor that looks for the 4 different cases on the stack. That doesn't sound too difficult to do. Would that need one visitor to read and another to actually do the change or can that be done in one go?

[kroening]

Three lambda functions should do the trick, like this:

  std::function<bool(const exprt &, const irep_idt &)> has_member;
  has_member=[&has_member](const exprt &expr, const irep_idt &identifier)->bool {
    if(expr.id()==ID_member)
      return to_member_expr(expr).get_component_name()==identifier;
    else
    {
      for(const auto &op : expr.operands())
        if(has_member(op, identifier))
          return true;
      return false;
    }
  };

(Perhaps also check the type of the struct).

No need for any visitor or the like to do the change, simply substitute the entire stack entry.

[mgudemann]

done in #2507