Skip to content

Cleanup expression/code cast validation #4176

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 12 commits into from
Mar 7, 2019
Merged

Cleanup expression/code cast validation #4176

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
12 commits
Select commit Hold shift + click to select a range
1de6c23
code_declt::check: for now accept more than one operand
tautschnig Feb 13, 2019
3c85341
code_deadt::check: to_symbol_expr requires a symbol_exprt
tautschnig Feb 13, 2019
92c140f
Replace misleading comments about validate_expr
tautschnig Feb 13, 2019
1d7789f
Re-use code_*t::check in validate_expr and to_code_*t
tautschnig Feb 13, 2019
8a21dea
Re-use validate_expr in to_code_*t
tautschnig Feb 13, 2019
10d61b2
mathematical_expr.h: move can_cast and validate_expr
tautschnig Feb 13, 2019
35262aa
Re-use validate_expr in mathematical_expr.h
tautschnig Feb 13, 2019
b61e3f1
std_expr.h: move can_cast and validate_expr
tautschnig Feb 13, 2019
0a73e03
std_expr.h: add/enable missing can_cast, validate_expr
tautschnig Feb 13, 2019
5e8af57
std_expr.h: remove commented-out validation steps
tautschnig Feb 13, 2019
4b5d356
Re-use validate_expr in to_*exprt
tautschnig Feb 13, 2019
d4dc77f
Re-use *_exprt::check in validate_expr and to_*exprt
tautschnig Feb 13, 2019
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
205 changes: 104 additions & 101 deletions src/util/mathematical_expr.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -61,35 +61,36 @@ class transt : public ternary_exprt
}
};

template <>
inline bool can_cast_expr<transt>(const exprt &base)
{
return base.id() == ID_trans;
}

inline void validate_expr(const transt &value)
{
validate_operands(value, 3, "Transition systems must have three operands");
}

/// Cast an exprt to a \ref transt
/// \a expr must be known to be \ref transt.
/// \param expr: Source expression
/// \return Object of type \ref transt
inline const transt &to_trans_expr(const exprt &expr)
{
PRECONDITION(expr.id() == ID_trans);
DATA_INVARIANT(
expr.operands().size() == 3, "Transition systems must have three operands");
return static_cast<const transt &>(expr);
const transt &ret = static_cast<const transt &>(expr);
validate_expr(ret);
return ret;
}

/// \copydoc to_trans_expr(const exprt &)
inline transt &to_trans_expr(exprt &expr)
{
PRECONDITION(expr.id() == ID_trans);
DATA_INVARIANT(
expr.operands().size() == 3, "Transition systems must have three operands");
return static_cast<transt &>(expr);
}

template <>
inline bool can_cast_expr<transt>(const exprt &base)
{
return base.id() == ID_trans;
}
inline void validate_expr(const transt &value)
{
validate_operands(value, 3, "Transition systems must have three operands");
transt &ret = static_cast<transt &>(expr);
validate_expr(ret);
return ret;
}

/// \brief Exponentiation
Expand All @@ -107,6 +108,17 @@ class power_exprt : public binary_exprt
}
};

template <>
inline bool can_cast_expr<power_exprt>(const exprt &base)
{
return base.id() == ID_power;
}

inline void validate_expr(const power_exprt &value)
{
validate_operands(value, 2, "Power must have two operands");
}

/// \brief Cast an exprt to a \ref power_exprt
///
/// \a expr must be known to be \ref power_exprt.
Expand All @@ -116,26 +128,18 @@ class power_exprt : public binary_exprt
inline const power_exprt &to_power_expr(const exprt &expr)
{
PRECONDITION(expr.id() == ID_power);
DATA_INVARIANT(expr.operands().size() == 2, "Power must have two operands");
return static_cast<const power_exprt &>(expr);
const power_exprt &ret = static_cast<const power_exprt &>(expr);
validate_expr(ret);
return ret;
}

/// \copydoc to_power_expr(const exprt &)
inline power_exprt &to_power_expr(exprt &expr)
{
PRECONDITION(expr.id() == ID_power);
DATA_INVARIANT(expr.operands().size() == 2, "Power must have two operands");
return static_cast<power_exprt &>(expr);
}

template <>
inline bool can_cast_expr<power_exprt>(const exprt &base)
{
return base.id() == ID_power;
}
inline void validate_expr(const power_exprt &value)
{
validate_operands(value, 2, "Power must have two operands");
power_exprt &ret = static_cast<power_exprt &>(expr);
validate_expr(ret);
return ret;
}

/// \brief Falling factorial power
Expand All @@ -153,6 +157,17 @@ class factorial_power_exprt : public binary_exprt
}
};

template <>
inline bool can_cast_expr<factorial_power_exprt>(const exprt &base)
{
return base.id() == ID_factorial_power;
}

inline void validate_expr(const factorial_power_exprt &value)
{
validate_operands(value, 2, "Factorial power must have two operands");
}

/// \brief Cast an exprt to a \ref factorial_power_exprt
///
/// \a expr must be known to be \ref factorial_power_exprt.
Expand All @@ -162,28 +177,19 @@ class factorial_power_exprt : public binary_exprt
inline const factorial_power_exprt &to_factorial_power_expr(const exprt &expr)
{
PRECONDITION(expr.id() == ID_factorial_power);
DATA_INVARIANT(
expr.operands().size() == 2, "Factorial power must have two operands");
return static_cast<const factorial_power_exprt &>(expr);
const factorial_power_exprt &ret =
static_cast<const factorial_power_exprt &>(expr);
validate_expr(ret);
return ret;
}

/// \copydoc to_factorial_power_expr(const exprt &)
inline factorial_power_exprt &to_factorial_expr(exprt &expr)
{
PRECONDITION(expr.id() == ID_factorial_power);
DATA_INVARIANT(
expr.operands().size() == 2, "Factorial power must have two operands");
return static_cast<factorial_power_exprt &>(expr);
}

template <>
inline bool can_cast_expr<factorial_power_exprt>(const exprt &base)
{
return base.id() == ID_factorial_power;
}
inline void validate_expr(const factorial_power_exprt &value)
{
validate_operands(value, 2, "Factorial power must have two operands");
factorial_power_exprt &ret = static_cast<factorial_power_exprt &>(expr);
validate_expr(ret);
return ret;
}

class tuple_exprt : public multi_ary_exprt
Expand Down Expand Up @@ -239,6 +245,17 @@ class function_application_exprt : public binary_exprt
}
};

template <>
inline bool can_cast_expr<function_application_exprt>(const exprt &base)
{
return base.id() == ID_function_application;
}

inline void validate_expr(const function_application_exprt &value)
{
validate_operands(value, 2, "Function application must have two operands");
}

/// \brief Cast an exprt to a \ref function_application_exprt
///
/// \a expr must be known to be \ref function_application_exprt.
Expand All @@ -249,28 +266,20 @@ inline const function_application_exprt &
to_function_application_expr(const exprt &expr)
{
PRECONDITION(expr.id() == ID_function_application);
DATA_INVARIANT(
expr.operands().size() == 2, "Function application must have two operands");
return static_cast<const function_application_exprt &>(expr);
const function_application_exprt &ret =
static_cast<const function_application_exprt &>(expr);
validate_expr(ret);
return ret;
}

/// \copydoc to_function_application_expr(const exprt &)
inline function_application_exprt &to_function_application_expr(exprt &expr)
{
PRECONDITION(expr.id() == ID_function_application);
DATA_INVARIANT(
expr.operands().size() == 2, "Function application must have two operands");
return static_cast<function_application_exprt &>(expr);
}

template <>
inline bool can_cast_expr<function_application_exprt>(const exprt &base)
{
return base.id() == ID_function_application;
}
inline void validate_expr(const function_application_exprt &value)
{
validate_operands(value, 2, "Function application must have two operands");
function_application_exprt &ret =
static_cast<function_application_exprt &>(expr);
validate_expr(ret);
return ret;
}

/// \brief A base class for quantifier expressions
Expand Down Expand Up @@ -306,6 +315,19 @@ class quantifier_exprt : public binary_predicate_exprt
}
};

template <>
inline bool can_cast_expr<quantifier_exprt>(const exprt &base)
{
return base.id() == ID_forall || base.id() == ID_exists;
}

inline void validate_expr(const quantifier_exprt &value)
{
validate_operands(value, 2, "quantifier expressions must have two operands");
DATA_INVARIANT(
value.op0().id() == ID_symbol, "quantified variable shall be a symbol");
}

/// \brief Cast an exprt to a \ref quantifier_exprt
///
/// \a expr must be known to be \ref quantifier_exprt.
Expand All @@ -314,34 +336,19 @@ class quantifier_exprt : public binary_predicate_exprt
/// \return Object of type \ref quantifier_exprt
inline const quantifier_exprt &to_quantifier_expr(const exprt &expr)
{
DATA_INVARIANT(
expr.operands().size() == 2,
"quantifier expressions must have two operands");
DATA_INVARIANT(
expr.op0().id() == ID_symbol, "quantified variable shall be a symbol");
return static_cast<const quantifier_exprt &>(expr);
PRECONDITION(can_cast_expr<quantifier_exprt>(expr));
const quantifier_exprt &ret = static_cast<const quantifier_exprt &>(expr);
validate_expr(ret);
return ret;
}

/// \copydoc to_quantifier_expr(const exprt &)
inline quantifier_exprt &to_quantifier_expr(exprt &expr)
{
DATA_INVARIANT(
expr.operands().size() == 2,
"quantifier expressions must have two operands");
DATA_INVARIANT(
expr.op0().id() == ID_symbol, "quantified variable shall be a symbol");
return static_cast<quantifier_exprt &>(expr);
}

template <>
inline bool can_cast_expr<quantifier_exprt>(const exprt &base)
{
return base.id() == ID_forall || base.id() == ID_exists;
}

inline void validate_expr(const quantifier_exprt &value)
{
validate_operands(value, 2, "quantifier expressions must have two operands");
PRECONDITION(can_cast_expr<quantifier_exprt>(expr));
quantifier_exprt &ret = static_cast<quantifier_exprt &>(expr);
validate_expr(ret);
return ret;
}

/// \brief A forall expression
Expand All @@ -357,19 +364,17 @@ class forall_exprt : public quantifier_exprt
inline const forall_exprt &to_forall_expr(const exprt &expr)
{
PRECONDITION(expr.id() == ID_forall);
DATA_INVARIANT(
expr.operands().size() == 2,
"forall expressions have exactly two operands");
return static_cast<const forall_exprt &>(expr);
const forall_exprt &ret = static_cast<const forall_exprt &>(expr);
validate_expr(static_cast<const quantifier_exprt &>(ret));
return ret;
}

inline forall_exprt &to_forall_expr(exprt &expr)
{
PRECONDITION(expr.id() == ID_forall);
DATA_INVARIANT(
expr.operands().size() == 2,
"forall expressions have exactly two operands");
return static_cast<forall_exprt &>(expr);
forall_exprt &ret = static_cast<forall_exprt &>(expr);
validate_expr(static_cast<const quantifier_exprt &>(ret));
return ret;
}

/// \brief An exists expression
Expand All @@ -385,19 +390,17 @@ class exists_exprt : public quantifier_exprt
inline const exists_exprt &to_exists_expr(const exprt &expr)
{
PRECONDITION(expr.id() == ID_exists);
DATA_INVARIANT(
expr.operands().size() == 2,
"exists expressions have exactly two operands");
return static_cast<const exists_exprt &>(expr);
const exists_exprt &ret = static_cast<const exists_exprt &>(expr);
validate_expr(static_cast<const quantifier_exprt &>(ret));
return ret;
}

inline exists_exprt &to_exists_expr(exprt &expr)
{
PRECONDITION(expr.id() == ID_exists);
DATA_INVARIANT(
expr.operands().size() == 2,
"exists expressions have exactly two operands");
return static_cast<exists_exprt &>(expr);
exists_exprt &ret = static_cast<exists_exprt &>(expr);
validate_expr(static_cast<const quantifier_exprt &>(ret));
return ret;
}

#endif // CPROVER_UTIL_MATHEMATICAL_EXPR_H
Loading