diff --git a/src/util/expr_cast.h b/src/util/expr_cast.h index e5cc222c49a..694c5e47106 100644 --- a/src/util/expr_cast.h +++ b/src/util/expr_cast.h @@ -30,6 +30,50 @@ Author: Nathan Phillips /// \return true if \a base is of type \a T template bool can_cast_expr(const exprt &base); +/// Called after casting. Provides a point to assert on the structure of the +/// expr. By default, this is a no-op, but you can provide an overload to +/// validate particular types. Should always succeed unless the program has +/// entered an invalid state. We validate objects at cast time as that is when +/// these checks have been used historically, but it would be reasonable to +/// validate objects in this way at any time. +inline void validate_expr(const exprt &) {} + +namespace detail // NOLINT +{ + +// We hide these functions in a namespace so that they only participate in +// overload resolution when explicitly requested. + +/// \brief Try to cast a reference to a generic exprt to a specific derived +/// class +/// \tparam T The reference or const reference type to \a TUnderlying to cast +/// to +/// \tparam TExpr The original type to cast from, either exprt or const exprt +/// \param base Reference to a generic \ref exprt +/// \return Reference to object of type \a TUnderlying +/// or valueless optional if \a base is not an instance of \a TUnderlying +template +optionalt::type>> +expr_try_dynamic_cast(TExpr &base) +{ + typedef typename std::decay::type decayt; + static_assert( + std::is_same::type, exprt>::value, + "Tried to expr_try_dynamic_cast from something that wasn't an exprt"); + static_assert( + std::is_reference::value, + "Tried to convert exprt & to non-reference type"); + static_assert( + std::is_base_of::value, + "The template argument T must be derived from exprt."); + if(!can_cast_expr(base)) + return {}; + T ret=static_cast(base); + validate_expr(ret); + return std::reference_wrapper::type>(ret); +} + +} // namespace detail /// \brief Try to cast a constant reference to a generic exprt to a specific /// derived class @@ -41,11 +85,7 @@ template optionalt::type>> expr_try_dynamic_cast(const exprt &base) { - return expr_try_dynamic_cast< - T, - typename std::remove_reference::type, - typename std::remove_const::type>::type, - const exprt>(base); + return detail::expr_try_dynamic_cast(base); } /// \brief Try to cast a reference to a generic exprt to a specific derived @@ -58,41 +98,59 @@ template optionalt::type>> expr_try_dynamic_cast(exprt &base) { - return expr_try_dynamic_cast< - T, - typename std::remove_reference::type, - typename std::remove_const::type>::type, - exprt>(base); + return detail::expr_try_dynamic_cast(base); } -/// \brief Try to cast a reference to a generic exprt to a specific derived -/// class -/// \tparam T The reference or const reference type to \a TUnderlying to cast -/// to -/// \tparam TUnderlying An exprt-derived class type +namespace detail // NOLINT +{ + +// We hide these functions in a namespace so that they only participate in +// overload resolution when explicitly requested. + +/// \brief Cast a reference to a generic exprt to a specific derived class. +/// \tparam T The reference or const reference type to \a TUnderlying to cast to /// \tparam TExpr The original type to cast from, either exprt or const exprt /// \param base Reference to a generic \ref exprt -/// \return Reference to object of type \a TUnderlying -/// or valueless optional if \a base is not an instance of \a TUnderlying -template -optionalt> expr_try_dynamic_cast(TExpr &base) +/// \return Reference to object of type \a T +/// \throw std::bad_cast If \a base is not an instance of \a TUnderlying +template +T expr_dynamic_cast(TExpr &base) { + typedef typename std::decay::type decayt; static_assert( std::is_same::type, exprt>::value, - "Tried to expr_try_dynamic_cast from something that wasn't an exprt"); + "Tried to expr_dynamic_cast from something that wasn't an exprt"); static_assert( std::is_reference::value, "Tried to convert exprt & to non-reference type"); static_assert( - std::is_base_of::value, + std::is_base_of::value, "The template argument T must be derived from exprt."); - if(!can_cast_expr(base)) - return optionalt>(); - T value=static_cast(base); - validate_expr(value); - return optionalt>(value); + if(!can_cast_expr(base)) + throw std::bad_cast(); + T ret=static_cast(base); + validate_expr(ret); + return ret; } +/// \brief Cast a reference to a generic exprt to a specific derived class. +/// Also assert that the expression has the expected type. +/// \tparam T The reference or const reference type to \a TUnderlying to cast to +/// \tparam TExpr The original type to cast from, either exprt or const exprt +/// \param base Reference to a generic \ref exprt +/// \return Reference to object of type \a T +/// \throw std::bad_cast If \a base is not an instance of \a TUnderlying +/// \remark If CBMC assertions (PRECONDITION) are set to abort then this will +/// abort rather than throw if \a base is not an instance of \a TUnderlying +template +T expr_checked_cast(TExpr &base) +{ + PRECONDITION(can_cast_expr::type>(base)); + return expr_dynamic_cast(base); +} + +} // namespace detail + /// \brief Cast a constant reference to a generic exprt to a specific derived /// class /// \tparam T The exprt-derived class to cast to @@ -104,10 +162,7 @@ optionalt> expr_try_dynamic_cast(TExpr &base) template T expr_dynamic_cast(const exprt &base) { - return expr_dynamic_cast< - T, - typename std::remove_const::type>::type, - const exprt>(base); + return detail::expr_dynamic_cast(base); } /// \brief Cast a reference to a generic exprt to a specific derived class @@ -120,41 +175,36 @@ T expr_dynamic_cast(const exprt &base) template T expr_dynamic_cast(exprt &base) { - return expr_dynamic_cast< - T, - typename std::remove_const::type>::type, - exprt>(base); + return detail::expr_dynamic_cast(base); } -/// \brief Cast a reference to a generic exprt to a specific derived class -/// \tparam T The reference or const reference type to \a TUnderlying to cast to -/// \tparam TUnderlying An exprt-derived class type -/// \tparam TExpr The original type to cast from, either exprt or const exprt +/// \brief Cast a constant reference to a generic exprt to a specific derived +/// class. Also assert that the exprt invariants are not violated. +/// \tparam T The exprt-derived class to cast to /// \param base Reference to a generic \ref exprt /// \return Reference to object of type \a T -/// \throw std::bad_cast If \a base is not an instance of \a TUnderlying +/// \throw std::bad_cast If \a base is not an instance of \a T /// \remark If CBMC assertions (PRECONDITION) are set to abort then this will -/// abort rather than throw if \a base is not an instance of \a TUnderlying -template -T expr_dynamic_cast(TExpr &base) +/// abort rather than throw if \a base is not an instance of \a T +template +T expr_checked_cast(const exprt &base) { - static_assert( - std::is_same::type, exprt>::value, - "Tried to expr_dynamic_cast from something that wasn't an exprt"); - static_assert( - std::is_reference::value, - "Tried to convert exprt & to non-reference type"); - static_assert( - std::is_base_of::value, - "The template argument T must be derived from exprt."); - PRECONDITION(can_cast_expr(base)); - if(!can_cast_expr(base)) - throw std::bad_cast(); - T value=static_cast(base); - validate_expr(value); - return value; + return detail::expr_checked_cast(base); } +/// \brief Cast a reference to a generic exprt to a specific derived class. +/// Also assert that the exprt invariants are not violated. +/// \tparam T The exprt-derived class to cast to +/// \param base Reference to a generic \ref exprt +/// \return Reference to object of type \a T +/// \throw std::bad_cast If \a base is not an instance of \a T +/// \remark If CBMC assertions (PRECONDITION) are set to abort then this will +/// abort rather than throw if \a base is not an instance of \a T +template +T expr_checked_cast(exprt &base) +{ + return detail::expr_checked_cast(base); +} inline void validate_operands( const exprt &value, @@ -164,8 +214,8 @@ inline void validate_operands( { DATA_INVARIANT( allow_more - ? value.operands().size()==number - : value.operands().size()>=number, + ? value.operands().size()>=number + : value.operands().size()==number, message); } diff --git a/src/util/std_code.h b/src/util/std_code.h index f48c48cb71a..0de8de0779f 100644 --- a/src/util/std_code.h +++ b/src/util/std_code.h @@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include "expr.h" +#include "expr_cast.h" /*! \brief A statement in a programming language */ @@ -46,6 +47,32 @@ class codet:public exprt class code_blockt &make_block(); }; +namespace detail // NOLINT +{ + +template +inline bool can_cast_code_impl(const exprt &expr, const Tag &tag) +{ + try + { + return expr_dynamic_cast(expr).get_statement()==tag; + } + catch(const std::bad_cast &) + { + return false; + } +} + +} // namespace detail + +template<> inline bool can_cast_expr(const exprt &base) +{ + return base.id()==ID_code; +} + +// to_code has no validation other than checking the id(), so no validate_expr +// is provided for codet + inline const codet &to_code(const exprt &expr) { assert(expr.id()==ID_code); @@ -117,6 +144,14 @@ class code_blockt:public codet } }; +template<> inline bool can_cast_expr(const exprt &base) +{ + return detail::can_cast_code_impl(base, ID_block); +} + +// to_code_block has no validation other than checking the statement(), so no +// validate_expr is provided for code_blockt + inline const code_blockt &to_code_block(const codet &code) { assert(code.get_statement()==ID_block); @@ -139,6 +174,13 @@ class code_skipt:public codet } }; +template<> inline bool can_cast_expr(const exprt &base) +{ + return detail::can_cast_code_impl(base, ID_skip); +} + +// there is no to_code_skip, so no validate_expr is provided for code_skipt + /*! \brief Assignment */ class code_assignt:public codet @@ -175,6 +217,16 @@ class code_assignt:public codet } }; +template<> inline bool can_cast_expr(const exprt &base) +{ + return detail::can_cast_code_impl(base, ID_assign); +} + +inline void validate_expr(const code_assignt & x) +{ + validate_operands(x, 2, "Assignment must have two operands"); +} + inline const code_assignt &to_code_assign(const codet &code) { assert(code.get_statement()==ID_assign && code.operands().size()==2); @@ -215,6 +267,16 @@ class code_declt:public codet const irep_idt &get_identifier() const; }; +template<> inline bool can_cast_expr(const exprt &base) +{ + return detail::can_cast_code_impl(base, ID_decl); +} + +inline void validate_expr(const code_declt &x) +{ + validate_operands(x, 1, "Decls must have one or more operands", true); +} + inline const code_declt &to_code_decl(const codet &code) { // will be size()==1 in the future @@ -257,6 +319,16 @@ class code_deadt:public codet const irep_idt &get_identifier() const; }; +template<> inline bool can_cast_expr(const exprt &base) +{ + return detail::can_cast_code_impl(base, ID_dead); +} + +inline void validate_expr(const code_deadt &x) +{ + validate_operands(x, 1, "Dead code must have one operand"); +} + inline const code_deadt &to_code_dead(const codet &code) { assert(code.get_statement()==ID_dead && code.operands().size()==1); @@ -295,6 +367,14 @@ class code_assumet:public codet } }; +template<> inline bool can_cast_expr(const exprt &base) +{ + return detail::can_cast_code_impl(base, ID_assume); +} + +// to_code_assume only checks the code statement, so no validate_expr is +// provided for code_assumet + inline const code_assumet &to_code_assume(const codet &code) { assert(code.get_statement()==ID_assume); @@ -333,6 +413,14 @@ class code_assertt:public codet } }; +template<> inline bool can_cast_expr(const exprt &base) +{ + return detail::can_cast_code_impl(base, ID_assert); +} + +// to_code_assert only checks the code statement, so no validate_expr is +// provided for code_assertt + inline const code_assertt &to_code_assert(const codet &code) { assert(code.get_statement()==ID_assert); @@ -393,6 +481,16 @@ class code_ifthenelset:public codet } }; +template<> inline bool can_cast_expr(const exprt &base) +{ + return detail::can_cast_code_impl(base, ID_ifthenelse); +} + +inline void validate_expr(const code_ifthenelset &x) +{ + validate_operands(x, 3, "If-then-else must have three operands"); +} + inline const code_ifthenelset &to_code_ifthenelse(const codet &code) { assert(code.get_statement()==ID_ifthenelse && @@ -438,6 +536,16 @@ class code_switcht:public codet } }; +template<> inline bool can_cast_expr(const exprt &base) +{ + return detail::can_cast_code_impl(base, ID_switch); +} + +inline void validate_expr(const code_switcht &x) +{ + validate_operands(x, 2, "Switch must have two operands"); +} + inline const code_switcht &to_code_switch(const codet &code) { assert(code.get_statement()==ID_switch && @@ -483,6 +591,16 @@ class code_whilet:public codet } }; +template<> inline bool can_cast_expr(const exprt &base) +{ + return detail::can_cast_code_impl(base, ID_while); +} + +inline void validate_expr(const code_whilet &x) +{ + validate_operands(x, 2, "While must have two operands"); +} + inline const code_whilet &to_code_while(const codet &code) { assert(code.get_statement()==ID_while && @@ -528,6 +646,16 @@ class code_dowhilet:public codet } }; +template<> inline bool can_cast_expr(const exprt &base) +{ + return detail::can_cast_code_impl(base, ID_dowhile); +} + +inline void validate_expr(const code_dowhilet &x) +{ + validate_operands(x, 2, "Do-while must have two operands"); +} + inline const code_dowhilet &to_code_dowhile(const codet &code) { assert(code.get_statement()==ID_dowhile && @@ -594,6 +722,16 @@ class code_fort:public codet } }; +template<> inline bool can_cast_expr(const exprt &base) +{ + return detail::can_cast_code_impl(base, ID_for); +} + +inline void validate_expr(const code_fort &x) +{ + validate_operands(x, 4, "For must have four operands"); +} + inline const code_fort &to_code_for(const codet &code) { assert(code.get_statement()==ID_for && @@ -633,6 +771,16 @@ class code_gotot:public codet } }; +template<> inline bool can_cast_expr(const exprt &base) +{ + return detail::can_cast_code_impl(base, ID_goto); +} + +inline void validate_expr(const code_gotot &x) +{ + validate_operands(x, 0, "Goto must not have operands"); +} + inline const code_gotot &to_code_goto(const codet &code) { assert(code.get_statement()==ID_goto && @@ -697,6 +845,14 @@ class code_function_callt:public codet } }; +template<> inline bool can_cast_expr(const exprt &base) +{ + return detail::can_cast_code_impl(base, ID_function_call); +} + +// to_code_function_call only checks the code statement, so no validate_expr is +// provided for code_function_callt + inline const code_function_callt &to_code_function_call(const codet &code) { assert(code.get_statement()==ID_function_call); @@ -743,6 +899,14 @@ class code_returnt:public codet } }; +template<> inline bool can_cast_expr(const exprt &base) +{ + return detail::can_cast_code_impl(base, ID_return); +} + +// to_code_return only checks the code statement, so no validate_expr is +// provided for code_returnt + inline const code_returnt &to_code_return(const codet &code) { assert(code.get_statement()==ID_return); @@ -800,6 +964,16 @@ class code_labelt:public codet } }; +template<> inline bool can_cast_expr(const exprt &base) +{ + return detail::can_cast_code_impl(base, ID_label); +} + +inline void validate_expr(const code_labelt &x) +{ + validate_operands(x, 1, "Label must have one operand"); +} + inline const code_labelt &to_code_label(const codet &code) { assert(code.get_statement()==ID_label && code.operands().size()==1); @@ -859,6 +1033,16 @@ class code_switch_caset:public codet } }; +template<> inline bool can_cast_expr(const exprt &base) +{ + return detail::can_cast_code_impl(base, ID_switch_case); +} + +inline void validate_expr(const code_switch_caset &x) +{ + validate_operands(x, 2, "Switch-case must have two operands"); +} + inline const code_switch_caset &to_code_switch_case(const codet &code) { assert(code.get_statement()==ID_switch_case && code.operands().size()==2); @@ -881,6 +1065,14 @@ class code_breakt:public codet } }; +template<> inline bool can_cast_expr(const exprt &base) +{ + return detail::can_cast_code_impl(base, ID_break); +} + +// to_code_break only checks the code statement, so no validate_expr is +// provided for code_breakt + inline const code_breakt &to_code_break(const codet &code) { assert(code.get_statement()==ID_break); @@ -903,6 +1095,14 @@ class code_continuet:public codet } }; +template<> inline bool can_cast_expr(const exprt &base) +{ + return detail::can_cast_code_impl(base, ID_continue); +} + +// to_code_continue only checks the code statement, so no validate_expr is +// provided for code_continuet + inline const code_continuet &to_code_continue(const codet &code) { assert(code.get_statement()==ID_continue); @@ -940,6 +1140,14 @@ class code_asmt:public codet } }; +template<> inline bool can_cast_expr(const exprt &base) +{ + return detail::can_cast_code_impl(base, ID_asm); +} + +// to_code_asm only checks the code statement, so no validate_expr is +// provided for code_asmt + inline code_asmt &to_code_asm(codet &code) { assert(code.get_statement()==ID_asm); @@ -978,6 +1186,16 @@ class code_expressiont:public codet } }; +template<> inline bool can_cast_expr(const exprt &base) +{ + return detail::can_cast_code_impl(base, ID_expression); +} + +inline void validate_expr(const code_expressiont &x) +{ + validate_operands(x, 1, "Expression must have one operand"); +} + inline code_expressiont &to_code_expression(codet &code) { assert(code.get_statement()==ID_expression && @@ -1020,6 +1238,33 @@ class side_effect_exprt:public exprt } }; +namespace detail // NOLINT +{ + +template +inline bool can_cast_side_effect_expr_impl(const exprt &expr, const Tag &tag) +{ + try + { + return + expr_dynamic_cast(expr).get_statement()==tag; + } + catch(const std::bad_cast &) + { + return false; + } +} + +} // namespace detail + +template<> inline bool can_cast_expr(const exprt &base) +{ + return base.id()==ID_side_effect; +} + +// to_side_effect_expr only checks the id, so no validate_expr is provided for +// side_effect_exprt + inline side_effect_exprt &to_side_effect_expr(exprt &expr) { assert(expr.id()==ID_side_effect); @@ -1059,6 +1304,15 @@ class side_effect_expr_nondett:public side_effect_exprt } }; +template<> +inline bool can_cast_expr(const exprt &base) +{ + return detail::can_cast_side_effect_expr_impl(base, ID_nondet); +} + +// to_side_effect_expr_nondet only checks the id, so no validate_expr is +// provided for side_effect_expr_nondett + inline side_effect_expr_nondett &to_side_effect_expr_nondet(exprt &expr) { auto &side_effect_expr_nondet=to_side_effect_expr(expr); @@ -1106,6 +1360,15 @@ class side_effect_expr_function_callt:public side_effect_exprt } }; +template<> +inline bool can_cast_expr(const exprt &base) +{ + return detail::can_cast_side_effect_expr_impl(base, ID_function_call); +} + +// to_side_effect_expr_function_call only checks the id, so no validate_expr is +// provided for side_effect_expr_function_callt + inline side_effect_expr_function_callt &to_side_effect_expr_function_call(exprt &expr) { @@ -1138,6 +1401,15 @@ class side_effect_expr_throwt:public side_effect_exprt } }; +template<> +inline bool can_cast_expr(const exprt &base) +{ + return detail::can_cast_side_effect_expr_impl(base, ID_throw); +} + +// to_side_effect_expr_throw only checks the id, so no validate_expr is +// provided for side_effect_expr_throwt + inline side_effect_expr_throwt &to_side_effect_expr_throw(exprt &expr) { assert(expr.id()==ID_side_effect); @@ -1229,6 +1501,14 @@ class code_push_catcht:public codet } }; +template<> inline bool can_cast_expr(const exprt &base) +{ + return detail::can_cast_code_impl(base, ID_push_catch); +} + +// to_code_push_catch only checks the code statement, so no validate_expr is +// provided for code_push_catcht + static inline code_push_catcht &to_code_push_catch(codet &code) { assert(code.get_statement()==ID_push_catch); @@ -1252,6 +1532,14 @@ class code_pop_catcht:public codet } }; +template<> inline bool can_cast_expr(const exprt &base) +{ + return detail::can_cast_code_impl(base, ID_pop_catch); +} + +// to_code_pop_catch only checks the code statement, so no validate_expr is +// provided for code_pop_catcht + static inline code_pop_catcht &to_code_pop_catch(codet &code) { assert(code.get_statement()==ID_pop_catch); @@ -1289,6 +1577,14 @@ class code_landingpadt:public codet } }; +template<> inline bool can_cast_expr(const exprt &base) +{ + return detail::can_cast_code_impl(base, ID_exception_landingpad); +} + +// to_code_landingpad only checks the code statement, so no validate_expr is +// provided for code_landingpadt + static inline code_landingpadt &to_code_landingpad(codet &code) { assert(code.get_statement()==ID_exception_landingpad); @@ -1353,6 +1649,16 @@ class code_try_catcht:public codet } }; +template<> inline bool can_cast_expr(const exprt &base) +{ + return detail::can_cast_code_impl(base, ID_try_catch); +} + +inline void validate_expr(const code_try_catcht &x) +{ + validate_operands(x, 3, "Try-catch must have three or more operands", true); +} + inline const code_try_catcht &to_code_try_catch(const codet &code) { assert(code.get_statement()==ID_try_catch && code.operands().size()>=3);