Skip to content

Move existing type validation checks to new framework #3147

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.

Sign up for GitHub

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
merged 1 commit into from
Mar 4, 2019
Merged

Move existing type validation checks to new framework #3147

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
15 changes: 2 additions & 13 deletions src/util/expr_cast.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -48,16 +48,6 @@ inline bool can_cast_type(const typet &base);
/// validate objects in this way at any time.
inline void validate_expr(const exprt &) {}

/// Called after casting. Provides a point to check data invariants on the
/// structure of the typet. 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_type(const typet &)
{
}

namespace detail // NOLINT
{

Expand Down Expand Up @@ -129,9 +119,8 @@ auto type_try_dynamic_cast(TType &base) ->
"The template argument T must be derived from typet.");
if(!can_cast_type<typename std::remove_const<T>::type>(base))
return nullptr;
const auto ret = static_cast<returnt>(&base);
validate_type(*ret);
return ret;
TType::check(base);
return static_cast<returnt>(&base);
}

namespace detail // NOLINT
Expand Down
142 changes: 71 additions & 71 deletions src/util/std_types.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1003,15 +1003,15 @@ inline bool can_cast_type<code_typet>(const typet &type)
inline const code_typet &to_code_type(const typet &type)
{
PRECONDITION(can_cast_type<code_typet>(type));
validate_type(type);
code_typet::check(type);
return static_cast<const code_typet &>(type);
}

/// \copydoc to_code_type(const typet &)
inline code_typet &to_code_type(typet &type)
{
PRECONDITION(can_cast_type<code_typet>(type));
validate_type(type);
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Shouldn't this get a corresponding check call?

code_typet::check(type);
return static_cast<code_typet &>(type);
}

Expand Down Expand Up @@ -1198,6 +1198,13 @@ class bv_typet:public bitvector_typet
{
set_width(width);
}

static void check(
const typet &type,
const validation_modet vm = validation_modet::INVARIANT)
{
DATA_CHECK(!type.get(ID_width).empty(), "bitvector type must have width");
}
};

/// Check whether a reference to a typet is a \ref bv_typet.
Expand All @@ -1209,11 +1216,6 @@ inline bool can_cast_type<bv_typet>(const typet &type)
return type.id() == ID_bv;
}

inline void validate_type(const bv_typet &type)
{
DATA_INVARIANT(!type.get(ID_width).empty(), "bitvector type must have width");
}

/// \brief Cast a typet to a \ref bv_typet
///
/// This is an unchecked conversion. \a type must be known to be \ref
Expand All @@ -1225,18 +1227,16 @@ inline void validate_type(const bv_typet &type)
inline const bv_typet &to_bv_type(const typet &type)
{
PRECONDITION(can_cast_type<bv_typet>(type));
const bv_typet &ret = static_cast<const bv_typet &>(type);
validate_type(ret);
return ret;
bv_typet::check(type);
return static_cast<const bv_typet &>(type);
}

/// \copydoc to_bv_type(const typet &)
inline bv_typet &to_bv_type(typet &type)
{
PRECONDITION(can_cast_type<bv_typet>(type));
bv_typet &ret = static_cast<bv_typet &>(type);
validate_type(ret);
return ret;
bv_typet::check(type);
return static_cast<bv_typet &>(type);
}

/// Fixed-width bit-vector with unsigned binary interpretation
Expand Down Expand Up @@ -1308,6 +1308,14 @@ class signedbv_typet:public bitvector_typet
constant_exprt smallest_expr() const;
constant_exprt zero_expr() const;
constant_exprt largest_expr() const;

static void check(
const typet &type,
const validation_modet vm = validation_modet::INVARIANT)
{
DATA_CHECK(
!type.get(ID_width).empty(), "signed bitvector type must have width");
}
};

/// Check whether a reference to a typet is a \ref signedbv_typet.
Expand All @@ -1319,12 +1327,6 @@ inline bool can_cast_type<signedbv_typet>(const typet &type)
return type.id() == ID_signedbv;
}

inline void validate_type(const signedbv_typet &type)
{
DATA_INVARIANT(
!type.get(ID_width).empty(), "signed bitvector type must have width");
}

/// \brief Cast a typet to a \ref signedbv_typet
///
/// This is an unchecked conversion. \a type must be known to be \ref
Expand All @@ -1336,18 +1338,16 @@ inline void validate_type(const signedbv_typet &type)
inline const signedbv_typet &to_signedbv_type(const typet &type)
{
PRECONDITION(can_cast_type<signedbv_typet>(type));
const signedbv_typet &ret = static_cast<const signedbv_typet &>(type);
validate_type(ret);
return ret;
signedbv_typet::check(type);
return static_cast<const signedbv_typet &>(type);
}

/// \copydoc to_signedbv_type(const typet &)
inline signedbv_typet &to_signedbv_type(typet &type)
{
PRECONDITION(can_cast_type<signedbv_typet>(type));
signedbv_typet &ret = static_cast<signedbv_typet &>(type);
validate_type(ret);
return ret;
signedbv_typet::check(type);
return static_cast<signedbv_typet &>(type);
}

/// Fixed-width bit-vector with signed fixed-point interpretation
Expand All @@ -1372,6 +1372,14 @@ class fixedbv_typet:public bitvector_typet
{
set(ID_integer_bits, b);
}

static void check(
const typet &type,
const validation_modet vm = validation_modet::INVARIANT)
{
DATA_CHECK(
!type.get(ID_width).empty(), "fixed bitvector type must have width");
}
};

/// Check whether a reference to a typet is a \ref fixedbv_typet.
Expand All @@ -1383,12 +1391,6 @@ inline bool can_cast_type<fixedbv_typet>(const typet &type)
return type.id() == ID_fixedbv;
}

inline void validate_type(const fixedbv_typet &type)
{
DATA_INVARIANT(
!type.get(ID_width).empty(), "fixed bitvector type must have width");
}

/// \brief Cast a typet to a \ref fixedbv_typet
///
/// This is an unchecked conversion. \a type must be known to be \ref
Expand All @@ -1400,18 +1402,16 @@ inline void validate_type(const fixedbv_typet &type)
inline const fixedbv_typet &to_fixedbv_type(const typet &type)
{
PRECONDITION(can_cast_type<fixedbv_typet>(type));
const fixedbv_typet &ret = static_cast<const fixedbv_typet &>(type);
validate_type(ret);
return ret;
fixedbv_typet::check(type);
return static_cast<const fixedbv_typet &>(type);
}

/// \copydoc to_fixedbv_type(const typet &)
inline fixedbv_typet &to_fixedbv_type(typet &type)
{
PRECONDITION(can_cast_type<fixedbv_typet>(type));
fixedbv_typet &ret = static_cast<fixedbv_typet &>(type);
validate_type(ret);
return ret;
fixedbv_typet::check(type);
return static_cast<fixedbv_typet &>(type);
}

/// Fixed-width bit-vector with IEEE floating-point interpretation
Expand All @@ -1434,6 +1434,14 @@ class floatbv_typet:public bitvector_typet
{
set(ID_f, b);
}

static void check(
const typet &type,
const validation_modet vm = validation_modet::INVARIANT)
{
DATA_CHECK(
!type.get(ID_width).empty(), "float bitvector type must have width");
}
};

/// Check whether a reference to a typet is a \ref floatbv_typet.
Expand All @@ -1445,12 +1453,6 @@ inline bool can_cast_type<floatbv_typet>(const typet &type)
return type.id() == ID_floatbv;
}

inline void validate_type(const floatbv_typet &type)
{
DATA_INVARIANT(
!type.get(ID_width).empty(), "float bitvector type must have width");
}

/// \brief Cast a typet to a \ref floatbv_typet
///
/// This is an unchecked conversion. \a type must be known to be \ref
Expand All @@ -1462,18 +1464,16 @@ inline void validate_type(const floatbv_typet &type)
inline const floatbv_typet &to_floatbv_type(const typet &type)
{
PRECONDITION(can_cast_type<floatbv_typet>(type));
const floatbv_typet &ret = static_cast<const floatbv_typet &>(type);
validate_type(ret);
return ret;
floatbv_typet::check(type);
return static_cast<const floatbv_typet &>(type);
}

/// \copydoc to_floatbv_type(const typet &)
inline floatbv_typet &to_floatbv_type(typet &type)
{
PRECONDITION(can_cast_type<floatbv_typet>(type));
floatbv_typet &ret = static_cast<floatbv_typet &>(type);
validate_type(ret);
return ret;
floatbv_typet::check(type);
return static_cast<floatbv_typet &>(type);
}

/// Type for C bit fields
Expand Down Expand Up @@ -1537,6 +1537,13 @@ class pointer_typet:public bitvector_typet
{
return signedbv_typet(get_width());
}

static void check(
const typet &type,
const validation_modet vm = validation_modet::INVARIANT)
{
DATA_CHECK(!type.get(ID_width).empty(), "pointer must have width");
}
};

/// Check whether a reference to a typet is a \ref pointer_typet.
Expand All @@ -1548,11 +1555,6 @@ inline bool can_cast_type<pointer_typet>(const typet &type)
return type.id() == ID_pointer;
}

inline void validate_type(const pointer_typet &type)
{
DATA_INVARIANT(!type.get(ID_width).empty(), "pointer must have width");
}

/// \brief Cast a typet to a \ref pointer_typet
///
/// This is an unchecked conversion. \a type must be known to be \ref
Expand All @@ -1564,18 +1566,16 @@ inline void validate_type(const pointer_typet &type)
inline const pointer_typet &to_pointer_type(const typet &type)
{
PRECONDITION(can_cast_type<pointer_typet>(type));
const pointer_typet &ret = static_cast<const pointer_typet &>(type);
validate_type(ret);
return ret;
pointer_typet::check(type);
return static_cast<const pointer_typet &>(type);
}

/// \copydoc to_pointer_type(const typet &)
inline pointer_typet &to_pointer_type(typet &type)
{
PRECONDITION(can_cast_type<pointer_typet>(type));
pointer_typet &ret = static_cast<pointer_typet &>(type);
validate_type(ret);
return ret;
pointer_typet::check(type);
return static_cast<pointer_typet &>(type);
}

/// The reference type
Expand Down Expand Up @@ -1635,6 +1635,13 @@ class c_bool_typet:public bitvector_typet
bitvector_typet(ID_c_bool, width)
{
}

static void check(
const typet &type,
const validation_modet vm = validation_modet::INVARIANT)
{
DATA_CHECK(!type.get(ID_width).empty(), "C bool type must have width");
}
};

/// Check whether a reference to a typet is a \ref c_bool_typet.
Expand All @@ -1646,11 +1653,6 @@ inline bool can_cast_type<c_bool_typet>(const typet &type)
return type.id() == ID_c_bool;
}

inline void validate_type(const c_bool_typet &type)
{
DATA_INVARIANT(!type.get(ID_width).empty(), "C bool type must have width");
}

/// \brief Cast a typet to a \ref c_bool_typet
///
/// This is an unchecked conversion. \a type must be known to be \ref
Expand All @@ -1662,18 +1664,16 @@ inline void validate_type(const c_bool_typet &type)
inline const c_bool_typet &to_c_bool_type(const typet &type)
{
PRECONDITION(can_cast_type<c_bool_typet>(type));
const c_bool_typet &ret = static_cast<const c_bool_typet &>(type);
validate_type(ret);
return ret;
c_bool_typet::check(type);
return static_cast<const c_bool_typet &>(type);
}

/// \copydoc to_c_bool_type(const typet &)
inline c_bool_typet &to_c_bool_type(typet &type)
{
PRECONDITION(can_cast_type<c_bool_typet>(type));
c_bool_typet &ret = static_cast<c_bool_typet &>(type);
validate_type(ret);
return ret;
c_bool_typet::check(type);
return static_cast<c_bool_typet &>(type);
}

/// String type
Expand Down
24 changes: 22 additions & 2 deletions src/util/validate_types.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,14 +24,34 @@ Author: Daniel Poetzl
template <template <typename, typename> class C, typename... Args>
void call_on_type(const typet &type, Args &&... args)
{
if(type.id() == ID_signedbv)
if(type.id() == ID_bv)
{
CALL_ON_TYPE(signedbv_typet);
CALL_ON_TYPE(bv_typet);
}
else if(type.id() == ID_unsignedbv)
{
CALL_ON_TYPE(unsignedbv_typet);
}
else if(type.id() == ID_signedbv)
{
CALL_ON_TYPE(signedbv_typet);
}
else if(type.id() == ID_fixedbv)
{
CALL_ON_TYPE(fixedbv_typet);
}
else if(type.id() == ID_floatbv)
{
CALL_ON_TYPE(floatbv_typet);
}
else if(type.id() == ID_pointer)
{
CALL_ON_TYPE(pointer_typet);
}
else if(type.id() == ID_c_bool)
{
CALL_ON_TYPE(c_bool_typet);
}
else
{
#ifdef REPORT_UNIMPLEMENTED_TYPE_CHECKS
Expand Down