-
Notifications
You must be signed in to change notification settings - Fork 273
Implementation of expr_dynamic_cast #1279
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Merged
smowton
merged 8 commits into
diffblue:develop
from
NathanJPhillips:feature/expr_dynamic_cast
Sep 22, 2017
Merged
Changes from all commits
Commits
Show all changes
8 commits
Select commit
Hold shift + click to select a range
de8a8d0
Implementation of expr_dynamic_cast
NathanJPhillips d35710f
Made validate_expr non-template
NathanJPhillips 95f6505
Comment on types for which expr_dynamic_cast is not implemented
NathanJPhillips c372eb3
Used typeinfo functions instead of rolling own
NathanJPhillips 775d9dd
Renamed can_cast_expr
NathanJPhillips b8ab624
Code review fixup
NathanJPhillips 96f2d9e
Added a PRECONDITION assert/invariant
NathanJPhillips da4df03
Switch from pointers to optionalt
smowton File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,172 @@ | ||
/*******************************************************************\ | ||
|
||
Module: | ||
|
||
Author: Nathan Phillips <[email protected]> | ||
|
||
\*******************************************************************/ | ||
|
||
#ifndef CPROVER_UTIL_EXPR_CAST_H | ||
#define CPROVER_UTIL_EXPR_CAST_H | ||
|
||
/// \file util/expr_cast.h | ||
/// \brief Templated functions to cast to specific exprt-derived classes | ||
|
||
#include <typeinfo> | ||
#include <type_traits> | ||
#include <functional> | ||
|
||
#include "invariant.h" | ||
#include "expr.h" | ||
#include "optional.h" | ||
|
||
/// \brief Check whether a reference to a generic \ref exprt is of a specific | ||
/// derived class. | ||
/// | ||
/// Implement template specializations of this function to enable casting | ||
/// | ||
/// \tparam T The exprt-derived class to check for | ||
/// \param base Reference to a generic \ref exprt | ||
/// \return true if \a base is of type \a T | ||
template<typename T> bool can_cast_expr(const exprt &base); | ||
|
||
|
||
/// \brief Try to cast a constant reference to a generic exprt to a specific | ||
/// derived class | ||
/// \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 or valueless optional if \a base | ||
/// is not an instance of \a T | ||
template<typename T> | ||
optionalt<std::reference_wrapper<typename std::remove_reference<T>::type>> | ||
expr_try_dynamic_cast(const exprt &base) | ||
{ | ||
return expr_try_dynamic_cast< | ||
T, | ||
typename std::remove_reference<T>::type, | ||
typename std::remove_const<typename std::remove_reference<T>::type>::type, | ||
const exprt>(base); | ||
} | ||
|
||
/// \brief Try to cast a reference to a generic exprt to a specific derived | ||
/// class | ||
/// \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 or valueless optional if \a base is | ||
/// not an instance of \a T | ||
template<typename T> | ||
optionalt<std::reference_wrapper<typename std::remove_reference<T>::type>> | ||
expr_try_dynamic_cast(exprt &base) | ||
{ | ||
return expr_try_dynamic_cast< | ||
T, | ||
typename std::remove_reference<T>::type, | ||
typename std::remove_const<typename std::remove_reference<T>::type>::type, | ||
exprt>(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 | ||
/// \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<typename T, typename TConst, typename TUnderlying, typename TExpr> | ||
optionalt<std::reference_wrapper<TConst>> expr_try_dynamic_cast(TExpr &base) | ||
{ | ||
static_assert( | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. use invariant.h? There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. This is a compile-time assertion. |
||
std::is_same<typename std::remove_const<TExpr>::type, exprt>::value, | ||
"Tried to expr_try_dynamic_cast from something that wasn't an exprt"); | ||
static_assert( | ||
std::is_reference<T>::value, | ||
"Tried to convert exprt & to non-reference type"); | ||
static_assert( | ||
std::is_base_of<exprt, TUnderlying>::value, | ||
"The template argument T must be derived from exprt."); | ||
if(!can_cast_expr<TUnderlying>(base)) | ||
return optionalt<std::reference_wrapper<TConst>>(); | ||
T value=static_cast<T>(base); | ||
validate_expr(value); | ||
return optionalt<std::reference_wrapper<TConst>>(value); | ||
} | ||
|
||
/// \brief Cast a constant reference to a generic exprt to a specific derived | ||
/// class | ||
/// \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<typename T> | ||
T expr_dynamic_cast(const exprt &base) | ||
{ | ||
return expr_dynamic_cast< | ||
T, | ||
typename std::remove_const<typename std::remove_reference<T>::type>::type, | ||
const exprt>(base); | ||
} | ||
|
||
/// \brief Cast a reference to a generic exprt to a specific derived class | ||
/// \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<typename T> | ||
T expr_dynamic_cast(exprt &base) | ||
{ | ||
return expr_dynamic_cast< | ||
T, | ||
typename std::remove_const<typename std::remove_reference<T>::type>::type, | ||
exprt>(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 | ||
/// \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<typename T, typename TUnderlying, typename TExpr> | ||
T expr_dynamic_cast(TExpr &base) | ||
{ | ||
static_assert( | ||
std::is_same<typename std::remove_const<TExpr>::type, exprt>::value, | ||
"Tried to expr_dynamic_cast from something that wasn't an exprt"); | ||
static_assert( | ||
std::is_reference<T>::value, | ||
"Tried to convert exprt & to non-reference type"); | ||
static_assert( | ||
std::is_base_of<exprt, TUnderlying>::value, | ||
"The template argument T must be derived from exprt."); | ||
PRECONDITION(can_cast_expr<TUnderlying>(base)); | ||
if(!can_cast_expr<TUnderlying>(base)) | ||
throw std::bad_cast(); | ||
T value=static_cast<T>(base); | ||
validate_expr(value); | ||
return value; | ||
} | ||
|
||
|
||
inline void validate_operands( | ||
const exprt &value, | ||
exprt::operandst::size_type number, | ||
const char *message, | ||
bool allow_more=false) | ||
{ | ||
DATA_INVARIANT( | ||
allow_more | ||
? value.operands().size()==number | ||
: value.operands().size()>=number, | ||
message); | ||
} | ||
|
||
#endif // CPROVER_UTIL_EXPR_CAST_H |
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Move comment header with author here (look at other files)