Add java_instanceof_exprt, and use it in place of raw exprts

jbmc/src/java_bytecode/expr2java.cpp

@@ -22,6 +22,7 @@ Author: Daniel Kroening, [email protected]
 #include <ansi-c/c_misc.h>
 #include <ansi-c/expr2c_class.h>
 
+#include "java_expr.h"
 #include "java_qualifiers.h"
 #include "java_string_literal_expr.h"
 #include "java_types.h"
@@ -320,16 +321,10 @@ std::string expr2javat::convert_java_this()
 
 std::string expr2javat::convert_java_instanceof(const exprt &src)
 {
-  if(src.operands().size()!=2)
-  {
-    unsigned precedence;
-    return convert_norep(src, precedence);
-  }
-
-  const auto &binary_expr = to_binary_expr(src);
+  const auto &instanceof_expr = to_java_instanceof_expr(src);
 
-  return convert(binary_expr.op0()) + " instanceof " +
-         convert(binary_expr.op1().type());
+  return convert(instanceof_expr.tested_expr()) + " instanceof " +
+         convert(instanceof_expr.target_type());
 }
 
 std::string expr2javat::convert_code_java_new(const exprt &src, unsigned indent)

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -16,6 +16,7 @@ Author: Daniel Kroening, [email protected]
 #include "bytecode_info.h"
 #include "java_bytecode_convert_method.h"
 #include "java_bytecode_convert_method_class.h"
+#include "java_expr.h"
 #include "java_static_initializers.h"
 #include "java_string_library_preprocess.h"
 #include "java_string_literal_expr.h"
@@ -1687,8 +1688,8 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method)
     {
       PRECONDITION(op.size() == 1 && results.size() == 1);
 
-      results[0]=
-        binary_predicate_exprt(op[0], ID_java_instanceof, arg0);
+      results[0] =
+        java_instanceof_exprt(op[0], to_struct_tag_type(arg0.type()));
     }
     else if(bytecode == BC_monitorenter || bytecode == BC_monitorexit)
     {
@@ -2326,7 +2327,7 @@ void java_bytecode_convert_methodt::convert_checkcast(
   codet &c,
   exprt::operandst &results) const
 {
-  binary_predicate_exprt check(op[0], ID_java_instanceof, arg0);
+  java_instanceof_exprt check(op[0], to_struct_tag_type(arg0.type()));
   code_assertt assert_class(check);
   assert_class.add_source_location().set_comment("Dynamic cast check");
   assert_class.add_source_location().set_property_class("bad-dynamic-cast");

jbmc/src/java_bytecode/java_bytecode_instrument.cpp

@@ -19,6 +19,7 @@ Date:   June 2017
 
 #include "java_bytecode_convert_class.h"
 #include "java_entry_point.h"
+#include "java_expr.h"
 #include "java_utils.h"
 
 class java_bytecode_instrumentt:public messaget
@@ -61,8 +62,8 @@ class java_bytecode_instrumentt:public messaget
     const source_locationt &original_loc);
 
   code_ifthenelset check_class_cast(
-    const exprt &class1,
-    const exprt &class2,
+    const exprt &tested_expr,
+    const struct_tag_typet &target_type,
     const source_locationt &original_loc);
 
   codet check_array_length(
@@ -203,22 +204,21 @@ codet java_bytecode_instrumentt::check_array_access(
 /// ClassCastException/generates an assertion when necessary;
 /// Exceptions are thrown when the `throw_runtime_exceptions` flag is set.
 /// Otherwise, assertions are emitted.
-/// \param class1: the subclass
-/// \param class2: the super class
+/// \param tested_expr: expression to test
+/// \param target_type: type to test for
 /// \param original_loc: source location in the original code
 /// \return Based on the value of the flag `throw_runtime_exceptions`,
 ///   it returns code that either throws an ClassCastException or emits an
 ///   assertion checking the subtype relation
 code_ifthenelset java_bytecode_instrumentt::check_class_cast(
-  const exprt &class1,
-  const exprt &class2,
+  const exprt &tested_expr,
+  const struct_tag_typet &target_type,
   const source_locationt &original_loc)
 {
-  binary_predicate_exprt class_cast_check(
-    class1, ID_java_instanceof, class2);
+  java_instanceof_exprt class_cast_check(tested_expr, target_type);
 
   pointer_typet voidptr = pointer_type(java_void_type());
-  exprt null_check_op = typecast_exprt::conditional_cast(class1, voidptr);
+  exprt null_check_op = typecast_exprt::conditional_cast(tested_expr, voidptr);
 
   optionalt<codet> check_code;
   if(throw_runtime_exceptions)
@@ -373,15 +373,12 @@ void java_bytecode_instrumentt::instrument_code(codet &code)
     if(code_assert.assertion().id()==ID_java_instanceof)
     {
       code_blockt block;
+      const auto & instanceof
+        = to_java_instanceof_expr(code_assert.assertion());
 
-      INVARIANT(
-        code_assert.assertion().operands().size()==2,
-        "Instanceof should have 2 operands");
-
-      const auto & instanceof = to_binary_expr(code_assert.assertion());
-
-      code = check_class_cast(
-        instanceof.op0(), instanceof.op1(), code_assert.source_location());
+      code = check_class_cast(instanceof.tested_expr(),
+                              instanceof
+                                .target_type(), code_assert.source_location());
     }
   }
   else if(statement==ID_block)

jbmc/src/java_bytecode/java_expr.h

@@ -0,0 +1,99 @@
+/*******************************************************************\
+
+Module: Java-specific exprt subclasses
+
+Author: Diffblue Ltd
+
+\*******************************************************************/
+
+/// \file
+/// Java-specific exprt subclasses
+
+#ifndef CPROVER_JAVA_BYTECODE_JAVA_EXPR_H
+#define CPROVER_JAVA_BYTECODE_JAVA_EXPR_H
+
+#include <util/std_expr.h>
+
+class java_instanceof_exprt : public binary_predicate_exprt
+{
+public:
+  java_instanceof_exprt(exprt lhs, const struct_tag_typet &target_type)
+    : binary_predicate_exprt(
+        std::move(lhs),
+        ID_java_instanceof,
+        type_exprt(target_type))
+  {
+  }
+
+  const exprt &tested_expr() const
+  {
+    return op0();
+  }
+  exprt &tested_expr()
+  {
+    return op0();
+  }
+
+  const struct_tag_typet &target_type() const
+  {
+    return to_struct_tag_type(op1().type());
+  }
+
+  static void check(
+    const exprt &expr,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    binary_predicate_exprt::check(expr, vm);
+  }
+
+  static void validate(
+    const exprt &expr,
+    const namespacet &ns,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    binary_predicate_exprt::validate(expr, ns, vm);
+
+    DATA_CHECK(
+      vm,
+      can_cast_expr<type_exprt>(expr.op1()),
+      "java_instanceof_exprt rhs should be a type_exprt");
+    DATA_CHECK(
+      vm,
+      can_cast_type<struct_tag_typet>(expr.op1().type()),
+      "java_instanceof_exprt rhs should denote a struct_tag_typet");
+  }
+};
+
+template <>
+inline bool can_cast_expr<java_instanceof_exprt>(const exprt &base)
+{
+  return can_cast_expr<binary_exprt>(base) && base.id() == ID_java_instanceof;
+}
+
+inline void validate_expr(const java_instanceof_exprt &value)
+{
+  java_instanceof_exprt::check(value);
+}
+
+/// \brief Cast an exprt to a \ref java_instanceof_exprt
+///
+/// \a expr must be known to be \ref java_instanceof_exprt.
+///
+/// \param expr: Source expression
+/// \return Object of type \ref java_instanceof_exprt
+inline const java_instanceof_exprt &to_java_instanceof_expr(const exprt &expr)
+{
+  java_instanceof_exprt::check(expr);
+  PRECONDITION(can_cast_expr<java_instanceof_exprt>(expr));
+  return static_cast<const java_instanceof_exprt &>(expr);
+}
+
+/// \copydoc to_java_instanceof_expr(const exprt &)
+inline java_instanceof_exprt &to_java_instanceof_expr(exprt &expr)
+{
+  java_instanceof_exprt::check(expr);
+  PRECONDITION(can_cast_expr<java_instanceof_exprt>(expr));
+  return static_cast<java_instanceof_exprt &>(expr);
+}
+
+#endif // CPROVER_JAVA_BYTECODE_JAVA_EXPR_H

jbmc/src/java_bytecode/remove_exceptions.cpp

@@ -32,6 +32,7 @@ Date:   December 2016
 
 #include <linking/static_lifetime_init.h>
 
+#include "java_expr.h"
 #include "java_types.h"
 
 /// Lowers high-level exception descriptions into low-level operations suitable
@@ -366,9 +367,8 @@ void remove_exceptionst::add_exception_dispatch_sequence(
 
         // use instanceof to check that this is the correct handler
         struct_tag_typet type(stack_catch[i][j].first);
-        type_exprt expr(type);
 
-        binary_predicate_exprt check(exc_thrown, ID_java_instanceof, expr);
+        java_instanceof_exprt check(exc_thrown, type);
         t_exc->guard=check;
 
         if(remove_added_instanceof)

src/util/std_expr.h

@@ -4071,6 +4071,33 @@ class type_exprt : public nullary_exprt
   }
 };
 
+template <>
+inline bool can_cast_expr<type_exprt>(const exprt &base)
+{
+  return base.id() == ID_type;
+}
+
+/// \brief Cast an exprt to an \ref type_exprt
+///
+/// \a expr must be known to be \ref type_exprt.
+///
+/// \param expr: Source expression
+/// \return Object of type \ref type_exprt
+inline const type_exprt &to_type_expr(const exprt &expr)
+{
+  PRECONDITION(can_cast_expr<type_exprt>(expr));
+  const type_exprt &ret = static_cast<const type_exprt &>(expr);
+  return ret;
+}
+
+/// \copydoc to_type_expr(const exprt &)
+inline type_exprt &to_type_expr(exprt &expr)
+{
+  PRECONDITION(can_cast_expr<type_exprt>(expr));
+  type_exprt &ret = static_cast<type_exprt &>(expr);
+  return ret;
+}
+
 /// \brief A constant literal expression
 class constant_exprt : public expr_protectedt
 {