diff --git a/jbmc/src/java_bytecode/expr2java.cpp b/jbmc/src/java_bytecode/expr2java.cpp index 2633893a6d8..267a3ee73b4 100644 --- a/jbmc/src/java_bytecode/expr2java.cpp +++ b/jbmc/src/java_bytecode/expr2java.cpp @@ -22,6 +22,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include +#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) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index a8dbc42dacc..9c05fcc7e78 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -16,6 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com #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"); diff --git a/jbmc/src/java_bytecode/java_bytecode_instrument.cpp b/jbmc/src/java_bytecode/java_bytecode_instrument.cpp index 05fd7334388..af8c110bc17 100644 --- a/jbmc/src/java_bytecode/java_bytecode_instrument.cpp +++ b/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 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) diff --git a/jbmc/src/java_bytecode/java_expr.h b/jbmc/src/java_bytecode/java_expr.h new file mode 100644 index 00000000000..a70584ac7ea --- /dev/null +++ b/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 + +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(expr.op1()), + "java_instanceof_exprt rhs should be a type_exprt"); + DATA_CHECK( + vm, + can_cast_type(expr.op1().type()), + "java_instanceof_exprt rhs should denote a struct_tag_typet"); + } +}; + +template <> +inline bool can_cast_expr(const exprt &base) +{ + return can_cast_expr(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(expr)); + return static_cast(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(expr)); + return static_cast(expr); +} + +#endif // CPROVER_JAVA_BYTECODE_JAVA_EXPR_H diff --git a/jbmc/src/java_bytecode/remove_exceptions.cpp b/jbmc/src/java_bytecode/remove_exceptions.cpp index 72902e8b041..6cbb3c12b9b 100644 --- a/jbmc/src/java_bytecode/remove_exceptions.cpp +++ b/jbmc/src/java_bytecode/remove_exceptions.cpp @@ -32,6 +32,7 @@ Date: December 2016 #include +#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) diff --git a/src/util/std_expr.h b/src/util/std_expr.h index 2f7cb43cd77..657141a4fd1 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -4071,6 +4071,33 @@ class type_exprt : public nullary_exprt } }; +template <> +inline bool can_cast_expr(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(expr)); + const type_exprt &ret = static_cast(expr); + return ret; +} + +/// \copydoc to_type_expr(const exprt &) +inline type_exprt &to_type_expr(exprt &expr) +{ + PRECONDITION(can_cast_expr(expr)); + type_exprt &ret = static_cast(expr); + return ret; +} + /// \brief A constant literal expression class constant_exprt : public expr_protectedt {