Merge pull request #5018 from diffblue/java_bytecode-opX

fix exprt::opX accesses in java_bytecode

Author: Daniel Kroening

jbmc/src/java_bytecode/expr2java.cpp

@@ -326,7 +326,10 @@ std::string expr2javat::convert_java_instanceof(const exprt &src)
     return convert_norep(src, precedence);
   }
 
-  return convert(src.op0())+" instanceof "+convert(src.op1().type());
+  const auto &binary_expr = to_binary_expr(src);
+
+  return convert(binary_expr.op0()) + " instanceof " +
+         convert(binary_expr.op1().type());
 }
 
 std::string expr2javat::convert_code_java_new(const exprt &src, unsigned indent)
@@ -370,7 +373,7 @@ std::string expr2javat::convert_code_java_delete(
     return convert_norep(src, precedence);
   }
 
-  std::string tmp=convert(src.op0());
+  std::string tmp = convert(to_unary_expr(src).op());
 
   dest+=tmp+";\n";
 

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -914,10 +914,10 @@ void add_java_array_types(symbol_tablet &symbol_table)
 
     code_declt declare_index(index_symexpr);
 
-    side_effect_exprt inc(ID_assign, typet(), location);
-    inc.operands().resize(2);
-    inc.op0()=index_symexpr;
-    inc.op1()=plus_exprt(index_symexpr, from_integer(1, index_symexpr.type()));
+    side_effect_expr_assignt inc(
+      index_symexpr,
+      plus_exprt(index_symexpr, from_integer(1, index_symexpr.type())),
+      location);
 
     dereference_exprt old_cell(
       plus_exprt(old_data, index_symexpr), old_data.type().subtype());

jbmc/src/java_bytecode/java_bytecode_instrument.cpp

@@ -378,11 +378,10 @@ void java_bytecode_instrumentt::instrument_code(codet &code)
         code_assert.assertion().operands().size()==2,
         "Instanceof should have 2 operands");
 
-      code=
-        check_class_cast(
-          code_assert.assertion().op0(),
-          code_assert.assertion().op1(),
-          code_assert.source_location());
+      const auto & instanceof = to_binary_expr(code_assert.assertion());
+
+      code = check_class_cast(
+        instanceof.op0(), instanceof.op1(), code_assert.source_location());
     }
   }
   else if(statement==ID_block)
@@ -494,20 +493,23 @@ optionalt<codet> java_bytecode_instrumentt::instrument_expr(const exprt &expr)
     {
       // this corresponds to a throw and so we check that
       // we don't throw null
-      result.add(check_null_dereference(expr.op0(), expr.source_location()));
+      result.add(check_null_dereference(
+        to_unary_expr(expr).op(), expr.source_location()));
     }
     else if(statement==ID_java_new_array)
     {
       // this corresponds to new array so we check that
       // length is >=0
-      result.add(check_array_length(expr.op0(), expr.source_location()));
+      result.add(check_array_length(
+        to_multi_ary_expr(expr).op0(), expr.source_location()));
     }
   }
   else if((expr.id()==ID_div || expr.id()==ID_mod) &&
           expr.type().id()==ID_signedbv)
   {
     // check division by zero (for integer types only)
-    result.add(check_arithmetic_exception(expr.op1(), expr.source_location()));
+    result.add(check_arithmetic_exception(
+      to_binary_expr(expr).op1(), expr.source_location()));
   }
   else if(expr.id()==ID_dereference &&
           expr.get_bool(ID_java_member_access))

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -239,7 +239,7 @@ void java_object_factoryt::gen_pointer_target_init(
   else
   {
     if(expr.id() == ID_address_of)
-      init_expr = expr.op0();
+      init_expr = to_address_of_expr(expr).object();
     else
     {
       init_expr = dereference_exprt(expr);

jbmc/src/java_bytecode/java_pointer_casts.cpp

@@ -21,7 +21,8 @@ Author: Daniel Kroening, [email protected]
 /// \return dereferenced pointer
 static exprt clean_deref(const exprt &ptr)
 {
-  return ptr.id() == ID_address_of ? ptr.op0() : dereference_exprt{ptr};
+  return ptr.id() == ID_address_of ? to_address_of_expr(ptr).object()
+                                   : dereference_exprt{ptr};
 }
 
 /// \par parameters: pointer
@@ -71,7 +72,7 @@ static const exprt &look_through_casts(const exprt &in)
   if(in.id()==ID_typecast)
   {
     assert(in.type().id()==ID_pointer);
-    return look_through_casts(in.op0());
+    return look_through_casts(to_typecast_expr(in).op());
   }
   else
     return in;
@@ -108,7 +109,7 @@ exprt make_clean_pointer_cast(
       bare_ptr.type().id()==ID_pointer &&
       "Non-pointer in make_clean_pointer_cast?");
     if(bare_ptr.type().subtype() == java_void_type())
-      bare_ptr=bare_ptr.op0();
+      bare_ptr = to_typecast_expr(bare_ptr).op();
   }
 
   assert(

jbmc/src/java_bytecode/java_trace_validation.cpp

@@ -85,8 +85,8 @@ bool check_index_structure(const exprt &index_expr)
   return (can_cast_expr<index_exprt>(index_expr) ||
           can_cast_expr<byte_extract_exprt>(index_expr)) &&
          index_expr.operands().size() == 2 &&
-         check_symbol_structure(index_expr.op0()) &&
-         can_evaluate_to_constant(index_expr.op1());
+         check_symbol_structure(to_binary_expr(index_expr).op0()) &&
+         can_evaluate_to_constant(to_binary_expr(index_expr).op1());
 }
 
 bool check_struct_structure(const struct_exprt &expr)

jbmc/src/java_bytecode/remove_instanceof.cpp

@@ -83,12 +83,12 @@ bool remove_instanceoft::lower_instanceof(
     expr.operands().size()==2,
     "java_instanceof should have two operands");
 
-  const exprt &check_ptr=expr.op0();
+  const exprt &check_ptr = to_binary_expr(expr).op0();
   INVARIANT(
     check_ptr.type().id()==ID_pointer,
     "instanceof first operand should be a pointer");
 
-  const exprt &target_arg=expr.op1();
+  const exprt &target_arg = to_binary_expr(expr).op1();
   INVARIANT(
     target_arg.id()==ID_type,
     "instanceof second operand should be a type");

jbmc/src/java_bytecode/remove_java_new.cpp

@@ -176,7 +176,8 @@ goto_programt::targett remove_java_newt::lower_java_new_array(
     struct_type.components()[1].type());
   dest.insert_before(
     next,
-    goto_programt::make_assignment(code_assignt(length, rhs.op0()), location));
+    goto_programt::make_assignment(
+      code_assignt(length, to_multi_ary_expr(rhs).op0()), location));
 
   // we also need to allocate space for the data
   member_exprt data(
@@ -205,7 +206,7 @@ goto_programt::targett remove_java_newt::lower_java_new_array(
   // backend.
   const irept size_bound = rhs.find(ID_length_upper_bound);
   if(size_bound.is_nil())
-    data_java_new_expr.set(ID_size, rhs.op0());
+    data_java_new_expr.set(ID_size, to_multi_ary_expr(rhs).op0());
   else
     data_java_new_expr.set(ID_size, size_bound);
 
@@ -276,8 +277,9 @@ goto_programt::targett remove_java_newt::lower_java_new_array(
 
     side_effect_exprt inc(ID_assign, typet(), location);
     inc.operands().resize(2);
-    inc.op0() = tmp_i;
-    inc.op1() = plus_exprt(tmp_i, from_integer(1, tmp_i.type()));
+    to_binary_expr(inc).op0() = tmp_i;
+    to_binary_expr(inc).op1() =
+      plus_exprt(tmp_i, from_integer(1, tmp_i.type()));
 
     dereference_exprt deref_expr(
       plus_exprt(data, tmp_i), data.type().subtype());
@@ -299,7 +301,7 @@ goto_programt::targett remove_java_newt::lower_java_new_array(
 
     const code_fort for_loop(
       code_assignt(tmp_i, from_integer(0, tmp_i.type())),
-      binary_relation_exprt(tmp_i, ID_lt, rhs.op0()),
+      binary_relation_exprt(tmp_i, ID_lt, to_multi_ary_expr(rhs).op0()),
       std::move(inc),
       std::move(for_body));