From 1de6c23c5becdbd072e9616278d2d8684a667257 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 13 Feb 2019 08:55:20 +0000 Subject: [PATCH 01/12] code_declt::check: for now accept more than one operand This is consistent with what validate_expr and to_code_declt assert at the moment. --- src/util/std_code.h | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/util/std_code.h b/src/util/std_code.h index 8f62251aee0..d2bcfacef6b 100644 --- a/src/util/std_code.h +++ b/src/util/std_code.h @@ -412,8 +412,11 @@ class code_declt:public codet const codet &code, const validation_modet vm = validation_modet::INVARIANT) { + // will be size()==1 in the future DATA_CHECK( - vm, code.operands().size() == 1, "declaration must have one operand"); + vm, + code.operands().size() >= 1, + "declaration must have one or more operands"); DATA_CHECK( vm, code.op0().id() == ID_symbol, From 3c85341828fea9909b9abaf3b797b222ccacec0c Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 13 Feb 2019 08:55:35 +0000 Subject: [PATCH 02/12] code_deadt::check: to_symbol_expr requires a symbol_exprt The error message would fail to print as it uses a conversion that is invalid for the very reason that the error message wants to print. --- src/util/std_code.h | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/util/std_code.h b/src/util/std_code.h index d2bcfacef6b..938d53908f9 100644 --- a/src/util/std_code.h +++ b/src/util/std_code.h @@ -493,8 +493,7 @@ class code_deadt:public codet DATA_CHECK( vm, code.op0().id() == ID_symbol, - "removing a non-symbol: " + - id2string(to_symbol_expr(code.op0()).get_identifier()) + "from scope"); + "removing a non-symbol: " + id2string(code.op0().id()) + "from scope"); } protected: From 92c140f7c449fa1cdfd409f043fbcdee99a2a411 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 13 Feb 2019 08:59:34 +0000 Subject: [PATCH 03/12] Replace misleading comments about validate_expr Adds one implementation of validate_expr, and moves the other existing ones to replace the comment that claims there is no implementation. --- src/util/std_code.h | 50 ++++++++++++++++++--------------------------- 1 file changed, 20 insertions(+), 30 deletions(-) diff --git a/src/util/std_code.h b/src/util/std_code.h index 938d53908f9..ab9df69c424 100644 --- a/src/util/std_code.h +++ b/src/util/std_code.h @@ -571,8 +571,10 @@ 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 void validate_expr(const code_assumet &x) +{ + validate_operands(x, 1, "assume must have one operand"); +} inline const code_assumet &to_code_assume(const codet &code) { @@ -586,11 +588,6 @@ inline code_assumet &to_code_assume(codet &code) return static_cast(code); } -inline void validate_expr(const code_assumet &x) -{ - validate_operands(x, 1, "assume must have one operand"); -} - /// A non-fatal assertion, which checks a condition then permits execution to /// continue. class code_assertt:public codet @@ -628,8 +625,10 @@ 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 void validate_expr(const code_assertt &x) +{ + validate_operands(x, 1, "assert must have one operand"); +} inline const code_assertt &to_code_assert(const codet &code) { @@ -643,11 +642,6 @@ inline code_assertt &to_code_assert(codet &code) return static_cast(code); } -inline void validate_expr(const code_assertt &x) -{ - validate_operands(x, 1, "assert must have one operand"); -} - /// Create a fatal assertion, which checks a condition and then halts if it does /// not hold. Equivalent to `ASSERT(condition); ASSUME(condition)`. /// @@ -1246,8 +1240,10 @@ 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 void validate_expr(const code_function_callt &x) +{ + validate_operands(x, 3, "function calls must have three operands"); +} inline const code_function_callt &to_code_function_call(const codet &code) { @@ -1261,11 +1257,6 @@ inline code_function_callt &to_code_function_call(codet &code) return static_cast(code); } -inline void validate_expr(const code_function_callt &x) -{ - validate_operands(x, 3, "function calls must have three operands"); -} - /// \ref codet representation of a "return from a function" statement. class code_returnt:public codet { @@ -1312,8 +1303,10 @@ 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 void validate_expr(const code_returnt &x) +{ + validate_operands(x, 1, "return must have one operand"); +} inline const code_returnt &to_code_return(const codet &code) { @@ -1327,11 +1320,6 @@ inline code_returnt &to_code_return(codet &code) return static_cast(code); } -inline void validate_expr(const code_returnt &x) -{ - validate_operands(x, 1, "return must have one operand"); -} - /// \ref codet representation of a label for branch targets. class code_labelt:public codet { @@ -1760,8 +1748,10 @@ inline bool can_cast_expr(const exprt &base) return detail::can_cast_code_impl(base, ID_asm); } -// to_code_asm_gcc only checks the code statement, so no validate_expr is -// provided for code_asmt +inline void validate_expr(const code_asm_gcct &x) +{ + validate_operands(x, 5, "code_asm_gcc must have five operands"); +} inline code_asm_gcct &to_code_asm_gcc(codet &code) { From 1d7789f0f23fc13136eb4b21a90e419550915905 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 13 Feb 2019 08:52:38 +0000 Subject: [PATCH 04/12] Re-use code_*t::check in validate_expr and to_code_*t Prefer code re-use over duplicated (and possibly inconsistent) implementations. --- src/util/std_code.h | 39 +++++++++++++-------------------------- 1 file changed, 13 insertions(+), 26 deletions(-) diff --git a/src/util/std_code.h b/src/util/std_code.h index ab9df69c424..19cd64c40fa 100644 --- a/src/util/std_code.h +++ b/src/util/std_code.h @@ -364,7 +364,7 @@ template<> inline bool can_cast_expr(const exprt &base) inline void validate_expr(const code_assignt & x) { - validate_operands(x, 2, "assignment must have two operands"); + code_assignt::check(x); } inline const code_assignt &to_code_assign(const codet &code) @@ -432,29 +432,20 @@ template<> inline bool can_cast_expr(const exprt &base) inline void validate_expr(const code_declt &x) { - validate_operands(x, 1, "decls must have one or more operands", true); + code_declt::check(x); } inline const code_declt &to_code_decl(const codet &code) { PRECONDITION(code.get_statement() == ID_decl); - - // will be size()==1 in the future - DATA_INVARIANT( - code.operands().size() >= 1, "decls must have one or more operands"); - DATA_INVARIANT( - code.op0().id() == ID_symbol, "decls symbols must be a \"symbol\""); - + code_declt::check(code); return static_cast(code); } inline code_declt &to_code_decl(codet &code) { PRECONDITION(code.get_statement() == ID_decl); - - // will be size()==1 in the future - DATA_INVARIANT( - code.operands().size() >= 1, "decls must have one or more operands"); + code_declt::check(code); return static_cast(code); } @@ -510,28 +501,20 @@ template<> inline bool can_cast_expr(const exprt &base) inline void validate_expr(const code_deadt &x) { - validate_operands(x, 1, "dead statement must have one operand"); + code_deadt::check(x); } inline const code_deadt &to_code_dead(const codet &code) { PRECONDITION(code.get_statement() == ID_dead); - DATA_INVARIANT( - code.operands().size() == 1, "dead statement must have one operand"); - DATA_INVARIANT( - to_unary_expr(code).op().id() == ID_symbol, - "dead statement must take symbol operand"); + code_deadt::check(code); return static_cast(code); } inline code_deadt &to_code_dead(codet &code) { PRECONDITION(code.get_statement() == ID_dead); - DATA_INVARIANT( - code.operands().size() == 1, "dead statement must have one operand"); - DATA_INVARIANT( - to_unary_expr(code).op().id() == ID_symbol, - "dead statement must take symbol operand"); + code_deadt::check(code); return static_cast(code); } @@ -1242,18 +1225,20 @@ template<> inline bool can_cast_expr(const exprt &base) inline void validate_expr(const code_function_callt &x) { - validate_operands(x, 3, "function calls must have three operands"); + code_function_callt::check(x); } inline const code_function_callt &to_code_function_call(const codet &code) { PRECONDITION(code.get_statement() == ID_function_call); + code_function_callt::check(code); return static_cast(code); } inline code_function_callt &to_code_function_call(codet &code) { PRECONDITION(code.get_statement() == ID_function_call); + code_function_callt::check(code); return static_cast(code); } @@ -1305,18 +1290,20 @@ template<> inline bool can_cast_expr(const exprt &base) inline void validate_expr(const code_returnt &x) { - validate_operands(x, 1, "return must have one operand"); + code_returnt::check(x); } inline const code_returnt &to_code_return(const codet &code) { PRECONDITION(code.get_statement() == ID_return); + code_returnt::check(code); return static_cast(code); } inline code_returnt &to_code_return(codet &code) { PRECONDITION(code.get_statement() == ID_return); + code_returnt::check(code); return static_cast(code); } From 8a21dea7ea5bb548ffc4a5e209459a9c1e13eb32 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 13 Feb 2019 09:01:52 +0000 Subject: [PATCH 05/12] Re-use validate_expr in to_code_*t This provides two advantages: 1) Member access such as testing the number of operands does not break sharing, because it is done in a const context. 2) Code re-use: we no longer implement the same check in two different ways. All changes in this commit were applied automatically via text replacement. --- src/util/std_code.h | 154 +++++++++++++++++++++++++------------------- 1 file changed, 86 insertions(+), 68 deletions(-) diff --git a/src/util/std_code.h b/src/util/std_code.h index 19cd64c40fa..246106d1d48 100644 --- a/src/util/std_code.h +++ b/src/util/std_code.h @@ -562,13 +562,17 @@ inline void validate_expr(const code_assumet &x) inline const code_assumet &to_code_assume(const codet &code) { PRECONDITION(code.get_statement() == ID_assume); - return static_cast(code); + const code_assumet &ret = static_cast(code); + validate_expr(ret); + return ret; } inline code_assumet &to_code_assume(codet &code) { PRECONDITION(code.get_statement() == ID_assume); - return static_cast(code); + code_assumet &ret = static_cast(code); + validate_expr(ret); + return ret; } /// A non-fatal assertion, which checks a condition then permits execution to @@ -616,13 +620,17 @@ inline void validate_expr(const code_assertt &x) inline const code_assertt &to_code_assert(const codet &code) { PRECONDITION(code.get_statement() == ID_assert); - return static_cast(code); + const code_assertt &ret = static_cast(code); + validate_expr(ret); + return ret; } inline code_assertt &to_code_assert(codet &code) { PRECONDITION(code.get_statement() == ID_assert); - return static_cast(code); + code_assertt &ret = static_cast(code); + validate_expr(ret); + return ret; } /// Create a fatal assertion, which checks a condition and then halts if it does @@ -722,17 +730,17 @@ inline void validate_expr(const code_ifthenelset &x) inline const code_ifthenelset &to_code_ifthenelse(const codet &code) { PRECONDITION(code.get_statement() == ID_ifthenelse); - DATA_INVARIANT( - code.operands().size() == 3, "if-then-else must have three operands"); - return static_cast(code); + const code_ifthenelset &ret = static_cast(code); + validate_expr(code); + return ret; } inline code_ifthenelset &to_code_ifthenelse(codet &code) { PRECONDITION(code.get_statement() == ID_ifthenelse); - DATA_INVARIANT( - code.operands().size() == 3, "if-then-else must have three operands"); - return static_cast(code); + code_ifthenelset &ret = static_cast(code); + validate_expr(code); + return ret; } /// \ref codet representing a `switch` statement. @@ -790,15 +798,17 @@ inline void validate_expr(const code_switcht &x) inline const code_switcht &to_code_switch(const codet &code) { PRECONDITION(code.get_statement() == ID_switch); - DATA_INVARIANT(code.operands().size() == 2, "switch must have two operands"); - return static_cast(code); + const code_switcht &ret = static_cast(code); + validate_expr(code); + return ret; } inline code_switcht &to_code_switch(codet &code) { PRECONDITION(code.get_statement() == ID_switch); - DATA_INVARIANT(code.operands().size() == 2, "switch must have two operands"); - return static_cast(code); + code_switcht &ret = static_cast(code); + validate_expr(code); + return ret; } /// \ref codet representing a `while` statement. @@ -856,15 +866,17 @@ inline void validate_expr(const code_whilet &x) inline const code_whilet &to_code_while(const codet &code) { PRECONDITION(code.get_statement() == ID_while); - DATA_INVARIANT(code.operands().size() == 2, "while must have two operands"); - return static_cast(code); + const code_whilet &ret = static_cast(code); + validate_expr(code); + return ret; } inline code_whilet &to_code_while(codet &code) { PRECONDITION(code.get_statement() == ID_while); - DATA_INVARIANT(code.operands().size() == 2, "while must have two operands"); - return static_cast(code); + code_whilet &ret = static_cast(code); + validate_expr(code); + return ret; } /// \ref codet representation of a `do while` statement. @@ -922,17 +934,17 @@ inline void validate_expr(const code_dowhilet &x) inline const code_dowhilet &to_code_dowhile(const codet &code) { PRECONDITION(code.get_statement() == ID_dowhile); - DATA_INVARIANT( - code.operands().size() == 2, "do-while must have two operands"); - return static_cast(code); + const code_dowhilet &ret = static_cast(code); + validate_expr(code); + return ret; } inline code_dowhilet &to_code_dowhile(codet &code) { PRECONDITION(code.get_statement() == ID_dowhile); - DATA_INVARIANT( - code.operands().size() == 2, "do-while must have two operands"); - return static_cast(code); + code_dowhilet &ret = static_cast(code); + validate_expr(code); + return ret; } /// \ref codet representation of a `for` statement. @@ -1017,15 +1029,17 @@ inline void validate_expr(const code_fort &x) inline const code_fort &to_code_for(const codet &code) { PRECONDITION(code.get_statement() == ID_for); - DATA_INVARIANT(code.operands().size() == 4, "for must have four operands"); - return static_cast(code); + const code_fort &ret = static_cast(code); + validate_expr(code); + return ret; } inline code_fort &to_code_for(codet &code) { PRECONDITION(code.get_statement() == ID_for); - DATA_INVARIANT(code.operands().size() == 4, "for must have four operands"); - return static_cast(code); + code_fort &ret = static_cast(code); + validate_expr(code); + return ret; } /// \ref codet representation of a `goto` statement. @@ -1072,15 +1086,17 @@ inline void validate_expr(const code_gotot &x) inline const code_gotot &to_code_goto(const codet &code) { PRECONDITION(code.get_statement() == ID_goto); - DATA_INVARIANT(code.operands().empty(), "goto must not have operands"); - return static_cast(code); + const code_gotot &ret = static_cast(code); + validate_expr(code); + return ret; } inline code_gotot &to_code_goto(codet &code) { PRECONDITION(code.get_statement() == ID_goto); - DATA_INVARIANT(code.operands().empty(), "goto must not have operands"); - return static_cast(code); + code_gotot &ret = static_cast(code); + validate_expr(code); + return ret; } /// \ref codet representation of a function call statement. @@ -1370,15 +1386,17 @@ inline void validate_expr(const code_labelt &x) inline const code_labelt &to_code_label(const codet &code) { PRECONDITION(code.get_statement() == ID_label); - DATA_INVARIANT(code.operands().size() == 1, "label must have one operand"); - return static_cast(code); + const code_labelt &ret = static_cast(code); + validate_expr(code); + return ret; } inline code_labelt &to_code_label(codet &code) { PRECONDITION(code.get_statement() == ID_label); - DATA_INVARIANT(code.operands().size() == 1, "label must have one operand"); - return static_cast(code); + code_labelt &ret = static_cast(code); + validate_expr(code); + return ret; } /// \ref codet representation of a switch-case, i.e.\ a `case` statement within @@ -1447,17 +1465,17 @@ inline void validate_expr(const code_switch_caset &x) inline const code_switch_caset &to_code_switch_case(const codet &code) { PRECONDITION(code.get_statement() == ID_switch_case); - DATA_INVARIANT( - code.operands().size() == 2, "switch-case must have two operands"); - return static_cast(code); + const code_switch_caset &ret = static_cast(code); + validate_expr(code); + return ret; } inline code_switch_caset &to_code_switch_case(codet &code) { PRECONDITION(code.get_statement() == ID_switch_case); - DATA_INVARIANT( - code.operands().size() == 2, "switch-case must have two operands"); - return static_cast(code); + code_switch_caset &ret = static_cast(code); + validate_expr(code); + return ret; } /// \ref codet representation of a switch-case, i.e.\ a `case` statement @@ -1531,19 +1549,19 @@ inline const code_gcc_switch_case_ranget & to_code_gcc_switch_case_range(const codet &code) { PRECONDITION(code.get_statement() == ID_gcc_switch_case_range); - DATA_INVARIANT( - code.operands().size() == 3, - "gcc-switch-case-range must have three operands"); - return static_cast(code); + const code_gcc_switch_case_ranget &ret = + static_cast(code); + validate_expr(code); + return ret; } inline code_gcc_switch_case_ranget &to_code_gcc_switch_case_range(codet &code) { PRECONDITION(code.get_statement() == ID_gcc_switch_case_range); - DATA_INVARIANT( - code.operands().size() == 3, - "gcc-switch-case-range must have three operands"); - return static_cast(code); + code_gcc_switch_case_ranget &ret = + static_cast(code); + validate_expr(code); + return ret; } /// \ref codet representation of a `break` statement (within a `for` or `while` @@ -1744,18 +1762,18 @@ inline code_asm_gcct &to_code_asm_gcc(codet &code) { PRECONDITION(code.get_statement() == ID_asm); PRECONDITION(to_code_asm(code).get_flavor() == ID_gcc); - DATA_INVARIANT( - code.operands().size() == 5, "code_asm_gcc must have give operands"); - return static_cast(code); + code_asm_gcct &ret = static_cast(code); + validate_expr(code); + return ret; } inline const code_asm_gcct &to_code_asm_gcc(const codet &code) { PRECONDITION(code.get_statement() == ID_asm); PRECONDITION(to_code_asm(code).get_flavor() == ID_gcc); - DATA_INVARIANT( - code.operands().size() == 5, "code_asm_gcc must have give operands"); - return static_cast(code); + const code_asm_gcct &ret = static_cast(code); + validate_expr(code); + return ret; } /// \ref codet representation of an expression statement. @@ -1803,17 +1821,17 @@ inline void validate_expr(const code_expressiont &x) inline code_expressiont &to_code_expression(codet &code) { PRECONDITION(code.get_statement() == ID_expression); - DATA_INVARIANT( - code.operands().size() == 1, "expression statement must have one operand"); - return static_cast(code); + code_expressiont &ret = static_cast(code); + validate_expr(code); + return ret; } inline const code_expressiont &to_code_expression(const codet &code) { PRECONDITION(code.get_statement() == ID_expression); - DATA_INVARIANT( - code.operands().size() == 1, "expression statement must have one operand"); - return static_cast(code); + const code_expressiont &ret = static_cast(code); + validate_expr(code); + return ret; } /// An expression containing a side effect. @@ -2456,17 +2474,17 @@ inline void validate_expr(const code_try_catcht &x) inline const code_try_catcht &to_code_try_catch(const codet &code) { PRECONDITION(code.get_statement() == ID_try_catch); - DATA_INVARIANT( - code.operands().size() >= 3, "try-catch must have three or more operands"); - return static_cast(code); + const code_try_catcht &ret = static_cast(code); + validate_expr(code); + return ret; } inline code_try_catcht &to_code_try_catch(codet &code) { PRECONDITION(code.get_statement() == ID_try_catch); - DATA_INVARIANT( - code.operands().size() >= 3, "try-catch must have three or more operands"); - return static_cast(code); + code_try_catcht &ret = static_cast(code); + validate_expr(code); + return ret; } /// This class is used to interface between a language frontend From 10d61b20df047529b8773df195d18e287cccb53c Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 13 Feb 2019 09:23:13 +0000 Subject: [PATCH 06/12] mathematical_expr.h: move can_cast and validate_expr Placing them above to_*_expr is the layout that std_code.h uses. Furthermore it will facilitate re-use of validate_expr. No code changes, just text motion. --- src/util/mathematical_expr.h | 106 ++++++++++++++++++----------------- 1 file changed, 55 insertions(+), 51 deletions(-) diff --git a/src/util/mathematical_expr.h b/src/util/mathematical_expr.h index ea793dd4ee3..089fa2a599b 100644 --- a/src/util/mathematical_expr.h +++ b/src/util/mathematical_expr.h @@ -61,6 +61,17 @@ class transt : public ternary_exprt } }; +template <> +inline bool can_cast_expr(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 @@ -82,16 +93,6 @@ inline transt &to_trans_expr(exprt &expr) return static_cast(expr); } -template <> -inline bool can_cast_expr(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"); -} - /// \brief Exponentiation class power_exprt : public binary_exprt { @@ -107,6 +108,17 @@ class power_exprt : public binary_exprt } }; +template <> +inline bool can_cast_expr(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. @@ -128,16 +140,6 @@ inline power_exprt &to_power_expr(exprt &expr) return static_cast(expr); } -template <> -inline bool can_cast_expr(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 Falling factorial power class factorial_power_exprt : public binary_exprt { @@ -153,6 +155,17 @@ class factorial_power_exprt : public binary_exprt } }; +template <> +inline bool can_cast_expr(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. @@ -176,16 +189,6 @@ inline factorial_power_exprt &to_factorial_expr(exprt &expr) return static_cast(expr); } -template <> -inline bool can_cast_expr(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"); -} - class tuple_exprt : public multi_ary_exprt { public: @@ -239,6 +242,17 @@ class function_application_exprt : public binary_exprt } }; +template <> +inline bool can_cast_expr(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. @@ -263,16 +277,6 @@ inline function_application_exprt &to_function_application_expr(exprt &expr) return static_cast(expr); } -template <> -inline bool can_cast_expr(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 A base class for quantifier expressions class quantifier_exprt : public binary_predicate_exprt { @@ -306,6 +310,17 @@ class quantifier_exprt : public binary_predicate_exprt } }; +template <> +inline bool can_cast_expr(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"); +} + /// \brief Cast an exprt to a \ref quantifier_exprt /// /// \a expr must be known to be \ref quantifier_exprt. @@ -333,17 +348,6 @@ inline quantifier_exprt &to_quantifier_expr(exprt &expr) return static_cast(expr); } -template <> -inline bool can_cast_expr(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"); -} - /// \brief A forall expression class forall_exprt : public quantifier_exprt { From 35262aae59beaf5e8417415e93a1e56f2dbc3c89 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 13 Feb 2019 09:39:03 +0000 Subject: [PATCH 07/12] Re-use validate_expr in mathematical_expr.h This provides two advantages: 1) Member access such as testing the number of operands does not break sharing, because it is done in a const context. 2) Code re-use: we no longer implement the same check in two different ways. With the exception of {exist,forall,quantifier}_exprt, all changes in this commit were applied automatically via text replacement. For quantifiers, additional checks were inserted (use of can_cast_expr, validate_expr uses quantifier_exprt's validate_expr). --- src/util/mathematical_expr.h | 99 ++++++++++++++++++------------------ 1 file changed, 49 insertions(+), 50 deletions(-) diff --git a/src/util/mathematical_expr.h b/src/util/mathematical_expr.h index 089fa2a599b..aa17ab018f0 100644 --- a/src/util/mathematical_expr.h +++ b/src/util/mathematical_expr.h @@ -79,18 +79,18 @@ inline void validate_expr(const transt &value) 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(expr); + const transt &ret = static_cast(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(expr); + transt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \brief Exponentiation @@ -128,16 +128,18 @@ inline void validate_expr(const power_exprt &value) 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(expr); + const power_exprt &ret = static_cast(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(expr); + power_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \brief Falling factorial power @@ -175,18 +177,19 @@ inline void validate_expr(const factorial_power_exprt &value) 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(expr); + const factorial_power_exprt &ret = + static_cast(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(expr); + factorial_power_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } class tuple_exprt : public multi_ary_exprt @@ -263,18 +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(expr); + const function_application_exprt &ret = + static_cast(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(expr); + function_application_exprt &ret = + static_cast(expr); + validate_expr(ret); + return ret; } /// \brief A base class for quantifier expressions @@ -319,6 +324,8 @@ inline bool can_cast_expr(const exprt &base) 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 @@ -329,23 +336,19 @@ inline void validate_expr(const quantifier_exprt &value) /// \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(expr); + PRECONDITION(can_cast_expr(expr)); + const quantifier_exprt &ret = static_cast(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(expr); + PRECONDITION(can_cast_expr(expr)); + quantifier_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \brief A forall expression @@ -361,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(expr); + const forall_exprt &ret = static_cast(expr); + validate_expr(static_cast(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(expr); + forall_exprt &ret = static_cast(expr); + validate_expr(static_cast(ret)); + return ret; } /// \brief An exists expression @@ -389,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(expr); + const exists_exprt &ret = static_cast(expr); + validate_expr(static_cast(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(expr); + exists_exprt &ret = static_cast(expr); + validate_expr(static_cast(ret)); + return ret; } #endif // CPROVER_UTIL_MATHEMATICAL_EXPR_H From b61e3f10432e40b9aef10c1c269ce0476d28df81 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 13 Feb 2019 09:55:14 +0000 Subject: [PATCH 08/12] std_expr.h: move can_cast and validate_expr Placing them above to_*_expr is the layout that std_code.h uses. Furthermore it will facilitate re-use of validate_expr. No code changes, just text motion. --- src/util/std_expr.h | 1312 +++++++++++++++++++++++-------------------- 1 file changed, 705 insertions(+), 607 deletions(-) diff --git a/src/util/std_expr.h b/src/util/std_expr.h index e2790ae3a67..058f1d32e65 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -206,6 +206,17 @@ class decorated_symbol_exprt:public symbol_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_symbol; +} + +inline void validate_expr(const symbol_exprt &value) +{ + validate_operands(value, 0, "Symbols must not have operands"); +} + /// \brief Cast an exprt to a \ref symbol_exprt /// /// \a expr must be known to be \ref symbol_exprt. @@ -227,15 +238,6 @@ inline symbol_exprt &to_symbol_expr(exprt &expr) return static_cast(expr); } -template<> inline bool can_cast_expr(const exprt &base) -{ - return base.id()==ID_symbol; -} -inline void validate_expr(const symbol_exprt &value) -{ - validate_operands(value, 0, "Symbols must not have operands"); -} - /// \brief Expression to hold a nondeterministic choice class nondet_symbol_exprt : public nullary_exprt @@ -260,6 +262,17 @@ class nondet_symbol_exprt : public nullary_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_nondet_symbol; +} + +inline void validate_expr(const nondet_symbol_exprt &value) +{ + validate_operands(value, 0, "Symbols must not have operands"); +} + /// \brief Cast an exprt to a \ref nondet_symbol_exprt /// /// \a expr must be known to be \ref nondet_symbol_exprt. @@ -281,15 +294,6 @@ inline nondet_symbol_exprt &to_nondet_symbol_expr(exprt &expr) return static_cast(expr); } -template<> inline bool can_cast_expr(const exprt &base) -{ - return base.id()==ID_nondet_symbol; -} -inline void validate_expr(const nondet_symbol_exprt &value) -{ - validate_operands(value, 0, "Symbols must not have operands"); -} - /// \brief Generic base class for unary expressions class unary_exprt : public expr_protectedt @@ -344,6 +348,12 @@ class unary_exprt : public expr_protectedt exprt &op3() = delete; }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.operands().size() == 1; +} + /// \brief Cast an exprt to a \ref unary_exprt /// /// \a expr must be known to be \ref unary_exprt. @@ -367,11 +377,6 @@ inline unary_exprt &to_unary_expr(exprt &expr) return static_cast(expr); } -template<> inline bool can_cast_expr(const exprt &base) -{ - return base.operands().size()==1; -} - /// \brief Absolute value class abs_exprt:public unary_exprt @@ -388,6 +393,17 @@ class abs_exprt:public unary_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_abs; +} + +inline void validate_expr(const abs_exprt &value) +{ + validate_operands(value, 1, "Absolute value must have one operand"); +} + /// \brief Cast an exprt to a \ref abs_exprt /// /// \a expr must be known to be \ref abs_exprt. @@ -413,15 +429,6 @@ inline abs_exprt &to_abs_expr(exprt &expr) return static_cast(expr); } -template<> inline bool can_cast_expr(const exprt &base) -{ - return base.id()==ID_abs; -} -inline void validate_expr(const abs_exprt &value) -{ - validate_operands(value, 1, "Absolute value must have one operand"); -} - /// \brief The unary minus expression class unary_minus_exprt:public unary_exprt @@ -445,6 +452,17 @@ class unary_minus_exprt:public unary_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_unary_minus; +} + +inline void validate_expr(const unary_minus_exprt &value) +{ + validate_operands(value, 1, "Unary minus must have one operand"); +} + /// \brief Cast an exprt to a \ref unary_minus_exprt /// /// \a expr must be known to be \ref unary_minus_exprt. @@ -470,15 +488,6 @@ inline unary_minus_exprt &to_unary_minus_expr(exprt &expr) return static_cast(expr); } -template<> inline bool can_cast_expr(const exprt &base) -{ - return base.id()==ID_unary_minus; -} -inline void validate_expr(const unary_minus_exprt &value) -{ - validate_operands(value, 1, "Unary minus must have one operand"); -} - /// \brief The unary plus expression class unary_plus_exprt : public unary_exprt { @@ -489,6 +498,17 @@ class unary_plus_exprt : public unary_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_unary_plus; +} + +inline void validate_expr(const unary_plus_exprt &value) +{ + validate_operands(value, 1, "unary plus must have one operand"); +} + /// \brief Cast an exprt to a \ref unary_plus_exprt /// /// \a expr must be known to be \ref unary_plus_exprt. @@ -512,16 +532,6 @@ inline unary_plus_exprt &to_unary_plus_expr(exprt &expr) return static_cast(expr); } -template <> -inline bool can_cast_expr(const exprt &base) -{ - return base.id() == ID_unary_plus; -} -inline void validate_expr(const unary_plus_exprt &value) -{ - validate_operands(value, 1, "unary plus must have one operand"); -} - /// \brief The byte swap expression class bswap_exprt: public unary_exprt { @@ -549,6 +559,19 @@ class bswap_exprt: public unary_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_bswap; +} + +inline void validate_expr(const bswap_exprt &value) +{ + validate_operands(value, 1, "bswap must have one operand"); + DATA_INVARIANT( + value.op().type() == value.type(), "bswap type must match operand type"); +} + /// \brief Cast an exprt to a \ref bswap_exprt /// /// \a expr must be known to be \ref bswap_exprt. @@ -574,18 +597,6 @@ inline bswap_exprt &to_bswap_expr(exprt &expr) return static_cast(expr); } -template <> -inline bool can_cast_expr(const exprt &base) -{ - return base.id() == ID_bswap; -} -inline void validate_expr(const bswap_exprt &value) -{ - validate_operands(value, 1, "bswap must have one operand"); - DATA_INVARIANT( - value.op().type() == value.type(), "bswap type must match operand type"); -} - /// \brief A base class for expressions that are predicates, /// i.e., Boolean-typed. class predicate_exprt : public expr_protectedt @@ -656,6 +667,17 @@ class sign_exprt:public unary_predicate_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_sign; +} + +inline void validate_expr(const sign_exprt &expr) +{ + validate_operands(expr, 1, "sign expression must have one operand"); +} + /// \brief Cast an exprt to a \ref sign_exprt /// /// \a expr must be known to be a \ref sign_exprt. @@ -679,16 +701,6 @@ inline sign_exprt &to_sign_expr(exprt &expr) return static_cast(expr); } -template <> -inline bool can_cast_expr(const exprt &base) -{ - return base.id() == ID_sign; -} -inline void validate_expr(const sign_exprt &expr) -{ - validate_operands(expr, 1, "sign expression must have one operand"); -} - /// \brief A base class for binary expressions class binary_exprt : public expr_protectedt { @@ -756,6 +768,12 @@ class binary_exprt : public expr_protectedt exprt &op3() = delete; }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.operands().size() == 2; +} + /// \brief Cast an exprt to a \ref binary_exprt /// /// \a expr must be known to be \ref binary_exprt. @@ -779,11 +797,6 @@ inline binary_exprt &to_binary_expr(exprt &expr) return static_cast(expr); } -template<> inline bool can_cast_expr(const exprt &base) -{ - return base.operands().size()==2; -} - /// \brief A base class for expressions that are predicates, /// i.e., Boolean-typed, and that take exactly two arguments. class binary_predicate_exprt:public binary_exprt @@ -893,6 +906,12 @@ class binary_relation_exprt:public binary_predicate_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return can_cast_expr(base); +} + /// \brief Cast an exprt to a \ref binary_relation_exprt /// /// \a expr must be known to be \ref binary_relation_exprt. @@ -916,11 +935,6 @@ inline binary_relation_exprt &to_binary_relation_expr(exprt &expr) return static_cast(expr); } -template<> inline bool can_cast_expr(const exprt &base) -{ - return can_cast_expr(base); -} - /// \brief A base class for multi-ary expressions /// Associativity is not specified. @@ -1073,6 +1087,17 @@ class plus_exprt:public multi_ary_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_plus; +} + +inline void validate_expr(const plus_exprt &value) +{ + validate_operands(value, 2, "Plus must have two or more operands", true); +} + /// \brief Cast an exprt to a \ref plus_exprt /// /// \a expr must be known to be \ref plus_exprt. @@ -1098,15 +1123,6 @@ inline plus_exprt &to_plus_expr(exprt &expr) return static_cast(expr); } -template<> inline bool can_cast_expr(const exprt &base) -{ - return base.id()==ID_plus; -} -inline void validate_expr(const plus_exprt &value) -{ - validate_operands(value, 2, "Plus must have two or more operands", true); -} - /// \brief Binary minus class minus_exprt:public binary_exprt @@ -1125,6 +1141,17 @@ class minus_exprt:public binary_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_minus; +} + +inline void validate_expr(const minus_exprt &value) +{ + validate_operands(value, 2, "Minus must have two or more operands", true); +} + /// \brief Cast an exprt to a \ref minus_exprt /// /// \a expr must be known to be \ref minus_exprt. @@ -1150,15 +1177,6 @@ inline minus_exprt &to_minus_expr(exprt &expr) return static_cast(expr); } -template<> inline bool can_cast_expr(const exprt &base) -{ - return base.id()==ID_minus; -} -inline void validate_expr(const minus_exprt &value) -{ - validate_operands(value, 2, "Minus must have two or more operands", true); -} - /// \brief Binary multiplication /// Associativity is not specified. @@ -1178,6 +1196,17 @@ class mult_exprt:public multi_ary_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_mult; +} + +inline void validate_expr(const mult_exprt &value) +{ + validate_operands(value, 2, "Multiply must have two or more operands", true); +} + /// \brief Cast an exprt to a \ref mult_exprt /// /// \a expr must be known to be \ref mult_exprt. @@ -1203,15 +1232,6 @@ inline mult_exprt &to_mult_expr(exprt &expr) return static_cast(expr); } -template<> inline bool can_cast_expr(const exprt &base) -{ - return base.id()==ID_mult; -} -inline void validate_expr(const mult_exprt &value) -{ - validate_operands(value, 2, "Multiply must have two or more operands", true); -} - /// \brief Division class div_exprt:public binary_exprt @@ -1254,6 +1274,17 @@ class div_exprt:public binary_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_div; +} + +inline void validate_expr(const div_exprt &value) +{ + validate_operands(value, 2, "Divide must have two operands"); +} + /// \brief Cast an exprt to a \ref div_exprt /// /// \a expr must be known to be \ref div_exprt. @@ -1279,15 +1310,6 @@ inline div_exprt &to_div_expr(exprt &expr) return static_cast(expr); } -template<> inline bool can_cast_expr(const exprt &base) -{ - return base.id()==ID_div; -} -inline void validate_expr(const div_exprt &value) -{ - validate_operands(value, 2, "Divide must have two operands"); -} - /// \brief Modulo class mod_exprt:public binary_exprt @@ -1306,6 +1328,17 @@ class mod_exprt:public binary_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_mod; +} + +inline void validate_expr(const mod_exprt &value) +{ + validate_operands(value, 2, "Modulo must have two operands"); +} + /// \brief Cast an exprt to a \ref mod_exprt /// /// \a expr must be known to be \ref mod_exprt. @@ -1327,15 +1360,6 @@ inline mod_exprt &to_mod_expr(exprt &expr) return static_cast(expr); } -template<> inline bool can_cast_expr(const exprt &base) -{ - return base.id()==ID_mod; -} -inline void validate_expr(const mod_exprt &value) -{ - validate_operands(value, 2, "Modulo must have two operands"); -} - /// \brief Remainder of division class rem_exprt:public binary_exprt @@ -1354,6 +1378,17 @@ class rem_exprt:public binary_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_rem; +} + +inline void validate_expr(const rem_exprt &value) +{ + validate_operands(value, 2, "Remainder must have two operands"); +} + /// \brief Cast an exprt to a \ref rem_exprt /// /// \a expr must be known to be \ref rem_exprt. @@ -1375,15 +1410,6 @@ inline rem_exprt &to_rem_expr(exprt &expr) return static_cast(expr); } -template<> inline bool can_cast_expr(const exprt &base) -{ - return base.id()==ID_rem; -} -inline void validate_expr(const rem_exprt &value) -{ - validate_operands(value, 2, "Remainder must have two operands"); -} - /// \brief Equality class equal_exprt:public binary_relation_exprt @@ -1415,12 +1441,23 @@ class equal_exprt:public binary_relation_exprt } }; -/// \brief Cast an exprt to an \ref equal_exprt -/// -/// \a expr must be known to be \ref equal_exprt. -/// -/// \param expr: Source expression -/// \return Object of type \ref equal_exprt +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_equal; +} + +inline void validate_expr(const equal_exprt &value) +{ + validate_operands(value, 2, "Equality must have two operands"); +} + +/// \brief Cast an exprt to an \ref equal_exprt +/// +/// \a expr must be known to be \ref equal_exprt. +/// +/// \param expr: Source expression +/// \return Object of type \ref equal_exprt inline const equal_exprt &to_equal_expr(const exprt &expr) { PRECONDITION(expr.id()==ID_equal); @@ -1436,15 +1473,6 @@ inline equal_exprt &to_equal_expr(exprt &expr) return static_cast(expr); } -template<> inline bool can_cast_expr(const exprt &base) -{ - return base.id()==ID_equal; -} -inline void validate_expr(const equal_exprt &value) -{ - validate_operands(value, 2, "Equality must have two operands"); -} - /// \brief Disequality class notequal_exprt:public binary_relation_exprt @@ -1461,6 +1489,17 @@ class notequal_exprt:public binary_relation_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_notequal; +} + +inline void validate_expr(const notequal_exprt &value) +{ + validate_operands(value, 2, "Inequality must have two operands"); +} + /// \brief Cast an exprt to an \ref notequal_exprt /// /// \a expr must be known to be \ref notequal_exprt. @@ -1486,15 +1525,6 @@ inline notequal_exprt &to_notequal_expr(exprt &expr) return static_cast(expr); } -template<> inline bool can_cast_expr(const exprt &base) -{ - return base.id()==ID_notequal; -} -inline void validate_expr(const notequal_exprt &value) -{ - validate_operands(value, 2, "Inequality must have two operands"); -} - /// \brief Array index operator class index_exprt:public binary_exprt @@ -1544,6 +1574,17 @@ class index_exprt:public binary_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_index; +} + +inline void validate_expr(const index_exprt &value) +{ + validate_operands(value, 2, "Array index must have two operands"); +} + /// \brief Cast an exprt to an \ref index_exprt /// /// \a expr must be known to be \ref index_exprt. @@ -1569,15 +1610,6 @@ inline index_exprt &to_index_expr(exprt &expr) return static_cast(expr); } -template<> inline bool can_cast_expr(const exprt &base) -{ - return base.id()==ID_index; -} -inline void validate_expr(const index_exprt &value) -{ - validate_operands(value, 2, "Array index must have two operands"); -} - /// \brief Array constructor from single element class array_of_exprt:public unary_exprt @@ -1605,6 +1637,17 @@ class array_of_exprt:public unary_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_array_of; +} + +inline void validate_expr(const array_of_exprt &value) +{ + validate_operands(value, 1, "'Array of' must have one operand"); +} + /// \brief Cast an exprt to an \ref array_of_exprt /// /// \a expr must be known to be \ref array_of_exprt. @@ -1630,15 +1673,6 @@ inline array_of_exprt &to_array_of_expr(exprt &expr) return static_cast(expr); } -template<> inline bool can_cast_expr(const exprt &base) -{ - return base.id()==ID_array_of; -} -inline void validate_expr(const array_of_exprt &value) -{ - validate_operands(value, 1, "'Array of' must have one operand"); -} - /// \brief Array constructor from list of elements class array_exprt : public multi_ary_exprt @@ -1661,6 +1695,12 @@ class array_exprt : public multi_ary_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_array; +} + /// \brief Cast an exprt to an \ref array_exprt /// /// \a expr must be known to be \ref array_exprt. @@ -1680,11 +1720,6 @@ inline array_exprt &to_array_expr(exprt &expr) return static_cast(expr); } -template<> inline bool can_cast_expr(const exprt &base) -{ - return base.id()==ID_array; -} - /// Array constructor from a list of index-element pairs /// Operands are index/value pairs, alternating. class array_list_exprt : public multi_ary_exprt @@ -1734,6 +1769,12 @@ class vector_exprt : public multi_ary_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_vector; +} + /// \brief Cast an exprt to an \ref vector_exprt /// /// \a expr must be known to be \ref vector_exprt. @@ -1753,11 +1794,6 @@ inline vector_exprt &to_vector_expr(exprt &expr) return static_cast(expr); } -template<> inline bool can_cast_expr(const exprt &base) -{ - return base.id()==ID_vector; -} - /// \brief Union constructor from single element class union_exprt:public unary_exprt @@ -1804,6 +1840,17 @@ class union_exprt:public unary_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_union; +} + +inline void validate_expr(const union_exprt &value) +{ + validate_operands(value, 1, "Union constructor must have one operand"); +} + /// \brief Cast an exprt to a \ref union_exprt /// /// \a expr must be known to be \ref union_exprt. @@ -1829,15 +1876,6 @@ inline union_exprt &to_union_expr(exprt &expr) return static_cast(expr); } -template<> inline bool can_cast_expr(const exprt &base) -{ - return base.id()==ID_union; -} -inline void validate_expr(const union_exprt &value) -{ - validate_operands(value, 1, "Union constructor must have one operand"); -} - /// \brief Struct constructor from list of elements class struct_exprt : public multi_ary_exprt @@ -1862,6 +1900,12 @@ class struct_exprt : public multi_ary_exprt const exprt &component(const irep_idt &name, const namespacet &ns) const; }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_struct; +} + /// \brief Cast an exprt to a \ref struct_exprt /// /// \a expr must be known to be \ref struct_exprt. @@ -1881,11 +1925,6 @@ inline struct_exprt &to_struct_expr(exprt &expr) return static_cast(expr); } -template<> inline bool can_cast_expr(const exprt &base) -{ - return base.id()==ID_struct; -} - /// \brief Complex constructor from a pair of numbers class complex_exprt:public binary_exprt @@ -1931,6 +1970,17 @@ class complex_exprt:public binary_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_complex; +} + +inline void validate_expr(const complex_exprt &value) +{ + validate_operands(value, 2, "Complex constructor must have two operands"); +} + /// \brief Cast an exprt to a \ref complex_exprt /// /// \a expr must be known to be \ref complex_exprt. @@ -1956,15 +2006,6 @@ inline complex_exprt &to_complex_expr(exprt &expr) return static_cast(expr); } -template<> inline bool can_cast_expr(const exprt &base) -{ - return base.id()==ID_complex; -} -inline void validate_expr(const complex_exprt &value) -{ - validate_operands(value, 2, "Complex constructor must have two operands"); -} - /// \brief Real part of the expression describing a complex number. class complex_real_exprt : public unary_exprt { @@ -1975,6 +2016,18 @@ class complex_real_exprt : public unary_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_complex_real; +} + +inline void validate_expr(const complex_real_exprt &expr) +{ + validate_operands( + expr, 1, "real part retrieval operation must have one operand"); +} + /// \brief Cast an exprt to a \ref complex_real_exprt /// /// \a expr must be known to be a \ref complex_real_exprt. @@ -2000,18 +2053,6 @@ inline complex_real_exprt &to_complex_real_expr(exprt &expr) return static_cast(expr); } -template <> -inline bool can_cast_expr(const exprt &base) -{ - return base.id() == ID_complex_real; -} - -inline void validate_expr(const complex_real_exprt &expr) -{ - validate_operands( - expr, 1, "real part retrieval operation must have one operand"); -} - /// \brief Imaginary part of the expression describing a complex number. class complex_imag_exprt : public unary_exprt { @@ -2022,6 +2063,18 @@ class complex_imag_exprt : public unary_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_complex_imag; +} + +inline void validate_expr(const complex_imag_exprt &expr) +{ + validate_operands( + expr, 1, "imaginary part retrieval operation must have one operand"); +} + /// \brief Cast an exprt to a \ref complex_imag_exprt /// /// \a expr must be known to be a \ref complex_imag_exprt. @@ -2047,18 +2100,6 @@ inline complex_imag_exprt &to_complex_imag_expr(exprt &expr) return static_cast(expr); } -template <> -inline bool can_cast_expr(const exprt &base) -{ - return base.id() == ID_complex_imag; -} - -inline void validate_expr(const complex_imag_exprt &expr) -{ - validate_operands( - expr, 1, "imaginary part retrieval operation must have one operand"); -} - class namespacet; /// \brief Split an expression into a base object and a (byte) offset @@ -2099,6 +2140,17 @@ class object_descriptor_exprt:public binary_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_object_descriptor; +} + +inline void validate_expr(const object_descriptor_exprt &value) +{ + validate_operands(value, 2, "Object descriptor must have two operands"); +} + /// \brief Cast an exprt to an \ref object_descriptor_exprt /// /// \a expr must be known to be \ref object_descriptor_exprt. @@ -2125,16 +2177,6 @@ inline object_descriptor_exprt &to_object_descriptor_expr(exprt &expr) return static_cast(expr); } -template<> -inline bool can_cast_expr(const exprt &base) -{ - return base.id()==ID_object_descriptor; -} -inline void validate_expr(const object_descriptor_exprt &value) -{ - validate_operands(value, 2, "Object descriptor must have two operands"); -} - /// Representation of heap-allocated objects class dynamic_object_exprt:public binary_exprt @@ -2169,6 +2211,17 @@ class dynamic_object_exprt:public binary_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_dynamic_object; +} + +inline void validate_expr(const dynamic_object_exprt &value) +{ + validate_operands(value, 2, "Dynamic object must have two operands"); +} + /// \brief Cast an exprt to a \ref dynamic_object_exprt /// /// \a expr must be known to be \ref dynamic_object_exprt. @@ -2195,16 +2248,6 @@ inline dynamic_object_exprt &to_dynamic_object_expr(exprt &expr) return static_cast(expr); } -template<> inline bool can_cast_expr(const exprt &base) -{ - return base.id()==ID_dynamic_object; -} - -inline void validate_expr(const dynamic_object_exprt &value) -{ - validate_operands(value, 2, "Dynamic object must have two operands"); -} - /// \brief Semantic type conversion class typecast_exprt:public unary_exprt @@ -2230,6 +2273,17 @@ class typecast_exprt:public unary_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_typecast; +} + +inline void validate_expr(const typecast_exprt &value) +{ + validate_operands(value, 1, "Typecast must have one operand"); +} + /// \brief Cast an exprt to a \ref typecast_exprt /// /// \a expr must be known to be \ref typecast_exprt. @@ -2255,15 +2309,6 @@ inline typecast_exprt &to_typecast_expr(exprt &expr) return static_cast(expr); } -template<> inline bool can_cast_expr(const exprt &base) -{ - return base.id()==ID_typecast; -} -inline void validate_expr(const typecast_exprt &value) -{ - validate_operands(value, 1, "Typecast must have one operand"); -} - /// \brief Semantic type conversion from/to floating-point formats class floatbv_typecast_exprt:public binary_exprt @@ -2302,6 +2347,17 @@ class floatbv_typecast_exprt:public binary_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_floatbv_typecast; +} + +inline void validate_expr(const floatbv_typecast_exprt &value) +{ + validate_operands(value, 2, "Float typecast must have two operands"); +} + /// \brief Cast an exprt to a \ref floatbv_typecast_exprt /// /// \a expr must be known to be \ref floatbv_typecast_exprt. @@ -2327,16 +2383,6 @@ inline floatbv_typecast_exprt &to_floatbv_typecast_expr(exprt &expr) return static_cast(expr); } -template<> -inline bool can_cast_expr(const exprt &base) -{ - return base.id()==ID_floatbv_typecast; -} -inline void validate_expr(const floatbv_typecast_exprt &value) -{ - validate_operands(value, 2, "Float typecast must have two operands"); -} - /// \brief Boolean AND class and_exprt:public multi_ary_exprt @@ -2378,6 +2424,17 @@ class and_exprt:public multi_ary_exprt exprt conjunction(const exprt::operandst &); +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_and; +} + +// inline void validate_expr(const and_exprt &value) +// { +// validate_operands(value, 2, "And must have two or more operands", true); +// } + /// \brief Cast an exprt to a \ref and_exprt /// /// \a expr must be known to be \ref and_exprt. @@ -2403,15 +2460,6 @@ inline and_exprt &to_and_expr(exprt &expr) return static_cast(expr); } -template<> inline bool can_cast_expr(const exprt &base) -{ - return base.id()==ID_and; -} -// inline void validate_expr(const and_exprt &value) -// { -// validate_operands(value, 2, "And must have two or more operands", true); -// } - /// \brief Boolean implication class implies_exprt:public binary_exprt @@ -2428,6 +2476,17 @@ class implies_exprt:public binary_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_implies; +} + +inline void validate_expr(const implies_exprt &value) +{ + validate_operands(value, 2, "Implies must have two operands"); +} + /// \brief Cast an exprt to a \ref implies_exprt /// /// \a expr must be known to be \ref implies_exprt. @@ -2449,15 +2508,6 @@ inline implies_exprt &to_implies_expr(exprt &expr) return static_cast(expr); } -template<> inline bool can_cast_expr(const exprt &base) -{ - return base.id()==ID_implies; -} -inline void validate_expr(const implies_exprt &value) -{ - validate_operands(value, 2, "Implies must have two operands"); -} - /// \brief Boolean OR class or_exprt:public multi_ary_exprt @@ -2499,6 +2549,17 @@ class or_exprt:public multi_ary_exprt exprt disjunction(const exprt::operandst &); +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_or; +} + +// inline void validate_expr(const or_exprt &value) +// { +// validate_operands(value, 2, "Or must have two or more operands", true); +// } + /// \brief Cast an exprt to a \ref or_exprt /// /// \a expr must be known to be \ref or_exprt. @@ -2524,15 +2585,6 @@ inline or_exprt &to_or_expr(exprt &expr) return static_cast(expr); } -template<> inline bool can_cast_expr(const exprt &base) -{ - return base.id()==ID_or; -} -// inline void validate_expr(const or_exprt &value) -// { -// validate_operands(value, 2, "Or must have two or more operands", true); -// } - /// \brief Boolean XOR class xor_exprt:public multi_ary_exprt @@ -2549,6 +2601,21 @@ class xor_exprt:public multi_ary_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_xor; +} + +// inline void validate_expr(const bitxor_exprt &value) +// { +// validate_operands( +// value, +// 2, +// "Bit-wise xor must have two or more operands", +// true); +// } + /// \brief Cast an exprt to a \ref xor_exprt /// /// \a expr must be known to be \ref xor_exprt. @@ -2568,19 +2635,6 @@ inline xor_exprt &to_xor_expr(exprt &expr) return static_cast(expr); } -template<> inline bool can_cast_expr(const exprt &base) -{ - return base.id()==ID_xor; -} -// inline void validate_expr(const bitxor_exprt &value) -// { -// validate_operands( -// value, -// 2, -// "Bit-wise xor must have two or more operands", -// true); -// } - /// \brief Bit-wise negation of bit-vectors class bitnot_exprt:public unary_exprt @@ -2597,6 +2651,17 @@ class bitnot_exprt:public unary_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_bitnot; +} + +// inline void validate_expr(const bitnot_exprt &value) +// { +// validate_operands(value, 1, "Bit-wise not must have one operand"); +// } + /// \brief Cast an exprt to a \ref bitnot_exprt /// /// \a expr must be known to be \ref bitnot_exprt. @@ -2620,15 +2685,6 @@ inline bitnot_exprt &to_bitnot_expr(exprt &expr) return static_cast(expr); } -template<> inline bool can_cast_expr(const exprt &base) -{ - return base.id()==ID_bitnot; -} -// inline void validate_expr(const bitnot_exprt &value) -// { -// validate_operands(value, 1, "Bit-wise not must have one operand"); -// } - /// \brief Bit-wise OR class bitor_exprt:public multi_ary_exprt @@ -2645,6 +2701,21 @@ class bitor_exprt:public multi_ary_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_bitor; +} + +// inline void validate_expr(const bitor_exprt &value) +// { +// validate_operands( +// value, +// 2, +// "Bit-wise or must have two or more operands", +// true); +// } + /// \brief Cast an exprt to a \ref bitor_exprt /// /// \a expr must be known to be \ref bitor_exprt. @@ -2670,19 +2741,6 @@ inline bitor_exprt &to_bitor_expr(exprt &expr) return static_cast(expr); } -template<> inline bool can_cast_expr(const exprt &base) -{ - return base.id()==ID_bitor; -} -// inline void validate_expr(const bitor_exprt &value) -// { -// validate_operands( -// value, -// 2, -// "Bit-wise or must have two or more operands", -// true); -// } - /// \brief Bit-wise XOR class bitxor_exprt:public multi_ary_exprt @@ -2699,6 +2757,21 @@ class bitxor_exprt:public multi_ary_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_bitxor; +} + +// inline void validate_expr(const bitxor_exprt &value) +// { +// validate_operands( +// value, +// 2, +// "Bit-wise xor must have two or more operands", +// true); +// } + /// \brief Cast an exprt to a \ref bitxor_exprt /// /// \a expr must be known to be \ref bitxor_exprt. @@ -2724,19 +2797,6 @@ inline bitxor_exprt &to_bitxor_expr(exprt &expr) return static_cast(expr); } -template<> inline bool can_cast_expr(const exprt &base) -{ - return base.id()==ID_bitxor; -} -// inline void validate_expr(const bitxor_exprt &value) -// { -// validate_operands( -// value, -// 2, -// "Bit-wise xor must have two or more operands", -// true); -// } - /// \brief Bit-wise AND class bitand_exprt:public multi_ary_exprt @@ -2753,6 +2813,21 @@ class bitand_exprt:public multi_ary_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_bitand; +} + +// inline void validate_expr(const bitand_exprt &value) +// { +// validate_operands( +// value, +// 2, +// "Bit-wise and must have two or more operands", +// true); +// } + /// \brief Cast an exprt to a \ref bitand_exprt /// /// \a expr must be known to be \ref bitand_exprt. @@ -2778,19 +2853,6 @@ inline bitand_exprt &to_bitand_expr(exprt &expr) return static_cast(expr); } -template<> inline bool can_cast_expr(const exprt &base) -{ - return base.id()==ID_bitand; -} -// inline void validate_expr(const bitand_exprt &value) -// { -// validate_operands( -// value, -// 2, -// "Bit-wise and must have two or more operands", -// true); -// } - /// \brief A base class for shift operators class shift_exprt:public binary_exprt @@ -2838,6 +2900,14 @@ class shift_exprt:public binary_exprt } }; +// The to_*_expr function for this type doesn't do any checks before casting, +// therefore the implementation is essentially a static_cast. +// Enabling expr_dynamic_cast would hide this; instead use static_cast directly. +// inline void validate_expr(const shift_exprt &value) +// { +// validate_operands(value, 2, "Shifts must have two operands"); +// } + /// \brief Cast an exprt to a \ref shift_exprt /// /// \a expr must be known to be \ref shift_exprt. @@ -2861,14 +2931,6 @@ inline shift_exprt &to_shift_expr(exprt &expr) return static_cast(expr); } -// The to_*_expr function for this type doesn't do any checks before casting, -// therefore the implementation is essentially a static_cast. -// Enabling expr_dynamic_cast would hide this; instead use static_cast directly. -// inline void validate_expr(const shift_exprt &value) -// { -// validate_operands(value, 2, "Shifts must have two operands"); -// } - /// \brief Left shift class shl_exprt:public shift_exprt @@ -2995,6 +3057,17 @@ class extractbit_exprt:public binary_predicate_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_extractbit; +} + +inline void validate_expr(const extractbit_exprt &value) +{ + validate_operands(value, 2, "Extract bit must have two operands"); +} + /// \brief Cast an exprt to an \ref extractbit_exprt /// /// \a expr must be known to be \ref extractbit_exprt. @@ -3020,15 +3093,6 @@ inline extractbit_exprt &to_extractbit_expr(exprt &expr) return static_cast(expr); } -template<> inline bool can_cast_expr(const exprt &base) -{ - return base.id()==ID_extractbit; -} -inline void validate_expr(const extractbit_exprt &value) -{ - validate_operands(value, 2, "Extract bit must have two operands"); -} - /// \brief Extracts a sub-range of a bit-vector operand class extractbits_exprt : public expr_protectedt @@ -3094,6 +3158,17 @@ class extractbits_exprt : public expr_protectedt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_extractbits; +} + +inline void validate_expr(const extractbits_exprt &value) +{ + validate_operands(value, 3, "Extract bits must have three operands"); +} + /// \brief Cast an exprt to an \ref extractbits_exprt /// /// \a expr must be known to be \ref extractbits_exprt. @@ -3119,15 +3194,6 @@ inline extractbits_exprt &to_extractbits_expr(exprt &expr) return static_cast(expr); } -template<> inline bool can_cast_expr(const exprt &base) -{ - return base.id()==ID_extractbits; -} -inline void validate_expr(const extractbits_exprt &value) -{ - validate_operands(value, 3, "Extract bits must have three operands"); -} - /// \brief Operator to return the address of an object class address_of_exprt:public unary_exprt @@ -3151,6 +3217,17 @@ class address_of_exprt:public unary_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_address_of; +} + +inline void validate_expr(const address_of_exprt &value) +{ + validate_operands(value, 1, "Address of must have one operand"); +} + /// \brief Cast an exprt to an \ref address_of_exprt /// /// \a expr must be known to be \ref address_of_exprt. @@ -3172,15 +3249,6 @@ inline address_of_exprt &to_address_of_expr(exprt &expr) return static_cast(expr); } -template<> inline bool can_cast_expr(const exprt &base) -{ - return base.id()==ID_address_of; -} -inline void validate_expr(const address_of_exprt &value) -{ - validate_operands(value, 1, "Address of must have one operand"); -} - /// \brief Boolean negation class not_exprt:public unary_exprt @@ -3198,6 +3266,17 @@ class not_exprt:public unary_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_not; +} + +inline void validate_expr(const not_exprt &value) +{ + validate_operands(value, 1, "Not must have one operand"); +} + /// \brief Cast an exprt to an \ref not_exprt /// /// \a expr must be known to be \ref not_exprt. @@ -3219,16 +3298,6 @@ inline not_exprt &to_not_expr(exprt &expr) return static_cast(expr); } -template<> inline bool can_cast_expr(const exprt &base) -{ - return base.id()==ID_not; -} - -inline void validate_expr(const not_exprt &value) -{ - validate_operands(value, 1, "Not must have one operand"); -} - /// \brief Operator to dereference a pointer class dereference_exprt:public unary_exprt @@ -3267,6 +3336,17 @@ class dereference_exprt:public unary_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_dereference; +} + +inline void validate_expr(const dereference_exprt &value) +{ + validate_operands(value, 1, "Dereference must have one operand"); +} + /// \brief Cast an exprt to a \ref dereference_exprt /// /// \a expr must be known to be \ref dereference_exprt. @@ -3292,15 +3372,6 @@ inline dereference_exprt &to_dereference_expr(exprt &expr) return static_cast(expr); } -template<> inline bool can_cast_expr(const exprt &base) -{ - return base.id()==ID_dereference; -} -inline void validate_expr(const dereference_exprt &value) -{ - validate_operands(value, 1, "Dereference must have one operand"); -} - /// \brief The trinary if-then-else operator class if_exprt : public ternary_exprt @@ -3352,6 +3423,17 @@ class if_exprt : public ternary_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_if; +} + +inline void validate_expr(const if_exprt &value) +{ + validate_operands(value, 3, "If-then-else must have three operands"); +} + /// \brief Cast an exprt to an \ref if_exprt /// /// \a expr must be known to be \ref if_exprt. @@ -3377,15 +3459,6 @@ inline if_exprt &to_if_expr(exprt &expr) return static_cast(expr); } -template<> inline bool can_cast_expr(const exprt &base) -{ - return base.id()==ID_if; -} -inline void validate_expr(const if_exprt &value) -{ - validate_operands(value, 3, "If-then-else must have three operands"); -} - /// \brief Operator to update elements in structs and arrays /// \remark This expression will eventually be replaced by separate /// array and struct update operators. @@ -3435,6 +3508,19 @@ class with_exprt : public expr_protectedt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_with; +} + +inline void validate_expr(const with_exprt &value) +{ + DATA_INVARIANT( + value.operands().size() % 2 == 1, + "array/structure update must have an odd number of operands"); +} + /// \brief Cast an exprt to a \ref with_exprt /// /// \a expr must be known to be \ref with_exprt. @@ -3460,17 +3546,6 @@ inline with_exprt &to_with_expr(exprt &expr) return static_cast(expr); } -template<> inline bool can_cast_expr(const exprt &base) -{ - return base.id()==ID_with; -} -inline void validate_expr(const with_exprt &value) -{ - DATA_INVARIANT( - value.operands().size() % 2 == 1, - "array/structure update must have an odd number of operands"); -} - class index_designatort : public expr_protectedt { public: @@ -3491,6 +3566,17 @@ class index_designatort : public expr_protectedt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_index_designator; +} + +inline void validate_expr(const index_designatort &value) +{ + validate_operands(value, 1, "Index designator must have one operand"); +} + /// \brief Cast an exprt to an \ref index_designatort /// /// \a expr must be known to be \ref index_designatort. @@ -3516,15 +3602,6 @@ inline index_designatort &to_index_designator(exprt &expr) return static_cast(expr); } -template<> inline bool can_cast_expr(const exprt &base) -{ - return base.id()==ID_index_designator; -} -inline void validate_expr(const index_designatort &value) -{ - validate_operands(value, 1, "Index designator must have one operand"); -} - class member_designatort : public expr_protectedt { public: @@ -3540,6 +3617,17 @@ class member_designatort : public expr_protectedt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_member_designator; +} + +inline void validate_expr(const member_designatort &value) +{ + validate_operands(value, 0, "Member designator must not have operands"); +} + /// \brief Cast an exprt to an \ref member_designatort /// /// \a expr must be known to be \ref member_designatort. @@ -3565,15 +3653,6 @@ inline member_designatort &to_member_designator(exprt &expr) return static_cast(expr); } -template<> inline bool can_cast_expr(const exprt &base) -{ - return base.id()==ID_member_designator; -} -inline void validate_expr(const member_designatort &value) -{ - validate_operands(value, 0, "Member designator must not have operands"); -} - /// \brief Operator to update elements in structs and arrays class update_exprt : public ternary_exprt @@ -3633,6 +3712,18 @@ class update_exprt : public ternary_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_update; +} + +inline void validate_expr(const update_exprt &value) +{ + validate_operands( + value, 3, "Array/structure update must have three operands"); +} + /// \brief Cast an exprt to an \ref update_exprt /// /// \a expr must be known to be \ref update_exprt. @@ -3651,23 +3742,11 @@ inline const update_exprt &to_update_expr(const exprt &expr) /// \copydoc to_update_expr(const exprt &) inline update_exprt &to_update_expr(exprt &expr) { - PRECONDITION(expr.id()==ID_update); - DATA_INVARIANT( - expr.operands().size()==3, - "Array/structure update must have three operands"); - return static_cast(expr); -} - -template<> inline bool can_cast_expr(const exprt &base) -{ - return base.id()==ID_update; -} -inline void validate_expr(const update_exprt &value) -{ - validate_operands( - value, - 3, + PRECONDITION(expr.id()==ID_update); + DATA_INVARIANT( + expr.operands().size() == 3, "Array/structure update must have three operands"); + return static_cast(expr); } @@ -3721,6 +3800,16 @@ class array_update_exprt:public expr_protectedt } }; +template<> inline bool can_cast_expr(const exprt &base) +{ + return base.id()==ID_array_update; +} + +inline void validate_expr(const array_update_exprt &value) +{ + validate_operands(value, 3, "Array update must have three operands"); +} + /// \brief Cast an exprt to an \ref array_update_exprt /// /// \a expr must be known to be \ref array_update_exprt. @@ -3746,15 +3835,6 @@ inline array_update_exprt &to_array_update_expr(exprt &expr) return static_cast(expr); } -template<> inline bool can_cast_expr(const exprt &base) -{ - return base.id()==ID_array_update; -} -inline void validate_expr(const array_update_exprt &value) -{ - validate_operands(value, 3, "Array update must have three operands"); -} - #endif @@ -3822,6 +3902,17 @@ class member_exprt:public unary_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_member; +} + +inline void validate_expr(const member_exprt &value) +{ + validate_operands(value, 1, "Extract member must have one operand"); +} + /// \brief Cast an exprt to a \ref member_exprt /// /// \a expr must be known to be \ref member_exprt. @@ -3847,15 +3938,6 @@ inline member_exprt &to_member_expr(exprt &expr) return static_cast(expr); } -template<> inline bool can_cast_expr(const exprt &base) -{ - return base.id()==ID_member; -} -inline void validate_expr(const member_exprt &value) -{ - validate_operands(value, 1, "Extract member must have one operand"); -} - /// \brief Evaluates to true if the operand is NaN class isnan_exprt:public unary_predicate_exprt @@ -3872,6 +3954,17 @@ class isnan_exprt:public unary_predicate_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_isnan; +} + +inline void validate_expr(const isnan_exprt &value) +{ + validate_operands(value, 1, "Is NaN must have one operand"); +} + /// \brief Cast an exprt to a \ref isnan_exprt /// /// \a expr must be known to be \ref isnan_exprt. @@ -3893,15 +3986,6 @@ inline isnan_exprt &to_isnan_expr(exprt &expr) return static_cast(expr); } -template<> inline bool can_cast_expr(const exprt &base) -{ - return base.id()==ID_isnan; -} -inline void validate_expr(const isnan_exprt &value) -{ - validate_operands(value, 1, "Is NaN must have one operand"); -} - /// \brief Evaluates to true if the operand is infinite class isinf_exprt:public unary_predicate_exprt @@ -3918,6 +4002,17 @@ class isinf_exprt:public unary_predicate_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_isinf; +} + +inline void validate_expr(const isinf_exprt &value) +{ + validate_operands(value, 1, "Is infinite must have one operand"); +} + /// \brief Cast an exprt to a \ref isinf_exprt /// /// \a expr must be known to be \ref isinf_exprt. @@ -3943,15 +4038,6 @@ inline isinf_exprt &to_isinf_expr(exprt &expr) return static_cast(expr); } -template<> inline bool can_cast_expr(const exprt &base) -{ - return base.id()==ID_isinf; -} -inline void validate_expr(const isinf_exprt &value) -{ - validate_operands(value, 1, "Is infinite must have one operand"); -} - /// \brief Evaluates to true if the operand is finite class isfinite_exprt:public unary_predicate_exprt @@ -3968,6 +4054,17 @@ class isfinite_exprt:public unary_predicate_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_isfinite; +} + +inline void validate_expr(const isfinite_exprt &value) +{ + validate_operands(value, 1, "Is finite must have one operand"); +} + /// \brief Cast an exprt to a \ref isfinite_exprt /// /// \a expr must be known to be \ref isfinite_exprt. @@ -3989,15 +4086,6 @@ inline isfinite_exprt &to_isfinite_expr(exprt &expr) return static_cast(expr); } -template<> inline bool can_cast_expr(const exprt &base) -{ - return base.id()==ID_isfinite; -} -inline void validate_expr(const isfinite_exprt &value) -{ - validate_operands(value, 1, "Is finite must have one operand"); -} - /// \brief Evaluates to true if the operand is a normal number class isnormal_exprt:public unary_predicate_exprt @@ -4014,6 +4102,17 @@ class isnormal_exprt:public unary_predicate_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_isnormal; +} + +inline void validate_expr(const isnormal_exprt &value) +{ + validate_operands(value, 1, "Is normal must have one operand"); +} + /// \brief Cast an exprt to a \ref isnormal_exprt /// /// \a expr must be known to be \ref isnormal_exprt. @@ -4035,15 +4134,6 @@ inline isnormal_exprt &to_isnormal_expr(exprt &expr) return static_cast(expr); } -template<> inline bool can_cast_expr(const exprt &base) -{ - return base.id()==ID_isnormal; -} -inline void validate_expr(const isnormal_exprt &value) -{ - validate_operands(value, 1, "Is normal must have one operand"); -} - /// \brief IEEE-floating-point equality class ieee_float_equal_exprt:public binary_relation_exprt @@ -4060,6 +4150,17 @@ class ieee_float_equal_exprt:public binary_relation_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_ieee_float_equal; +} + +inline void validate_expr(const ieee_float_equal_exprt &value) +{ + validate_operands(value, 2, "IEEE equality must have two operands"); +} + /// \brief Cast an exprt to an \ref ieee_float_equal_exprt /// /// \a expr must be known to be \ref ieee_float_equal_exprt. @@ -4085,16 +4186,6 @@ inline ieee_float_equal_exprt &to_ieee_float_equal_expr(exprt &expr) return static_cast(expr); } -template<> -inline bool can_cast_expr(const exprt &base) -{ - return base.id()==ID_ieee_float_equal; -} -inline void validate_expr(const ieee_float_equal_exprt &value) -{ - validate_operands(value, 2, "IEEE equality must have two operands"); -} - /// \brief IEEE floating-point disequality class ieee_float_notequal_exprt:public binary_relation_exprt @@ -4112,6 +4203,17 @@ class ieee_float_notequal_exprt:public binary_relation_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_ieee_float_notequal; +} + +inline void validate_expr(const ieee_float_notequal_exprt &value) +{ + validate_operands(value, 2, "IEEE inequality must have two operands"); +} + /// \brief Cast an exprt to an \ref ieee_float_notequal_exprt /// /// \a expr must be known to be \ref ieee_float_notequal_exprt. @@ -4138,16 +4240,6 @@ inline ieee_float_notequal_exprt &to_ieee_float_notequal_expr(exprt &expr) return static_cast(expr); } -template<> -inline bool can_cast_expr(const exprt &base) -{ - return base.id()==ID_ieee_float_notequal; -} -inline void validate_expr(const ieee_float_notequal_exprt &value) -{ - validate_operands(value, 2, "IEEE inequality must have two operands"); -} - /// \brief IEEE floating-point operations /// These have two data operands (op0 and op1) and one rounding mode (op2). /// The type of the result is that of the data operands. @@ -4194,6 +4286,19 @@ class ieee_float_op_exprt : public ternary_exprt } }; +// The to_*_expr function for this type doesn't do any checks before casting, +// therefore the implementation is essentially a static_cast. +// Enabling expr_dynamic_cast would hide this; instead use static_cast directly. +// template<> +// inline void validate_expr( +// const ieee_float_op_exprt &value) +// { +// validate_operands( +// value, +// 3, +// "IEEE float operations must have three arguments"); +// } + /// \brief Cast an exprt to an \ref ieee_float_op_exprt /// /// \a expr must be known to be \ref ieee_float_op_exprt. @@ -4217,19 +4322,6 @@ inline ieee_float_op_exprt &to_ieee_float_op_expr(exprt &expr) return static_cast(expr); } -// The to_*_expr function for this type doesn't do any checks before casting, -// therefore the implementation is essentially a static_cast. -// Enabling expr_dynamic_cast would hide this; instead use static_cast directly. -// template<> -// inline void validate_expr( -// const ieee_float_op_exprt &value) -// { -// validate_operands( -// value, -// 3, -// "IEEE float operations must have three arguments"); -// } - /// \brief An expression denoting a type class type_exprt : public nullary_exprt @@ -4279,6 +4371,11 @@ class constant_exprt : public expr_protectedt bool value_is_zero_string() const; }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_constant; +} /// \brief Cast an exprt to a \ref constant_exprt /// @@ -4299,11 +4396,6 @@ inline constant_exprt &to_constant_expr(exprt &expr) return static_cast(expr); } -template<> inline bool can_cast_expr(const exprt &base) -{ - return base.id()==ID_constant; -} - /// \brief The Boolean constant true class true_exprt:public constant_exprt @@ -4384,6 +4476,17 @@ class replication_exprt : public binary_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_replication; +} + +inline void validate_expr(const replication_exprt &value) +{ + validate_operands(value, 2, "Bit-wise replication must have two operands"); +} + /// \brief Cast an exprt to a \ref replication_exprt /// /// \a expr must be known to be \ref replication_exprt. @@ -4407,16 +4510,6 @@ inline replication_exprt &to_replication_expr(exprt &expr) return static_cast(expr); } -template <> -inline bool can_cast_expr(const exprt &base) -{ - return base.id() == ID_replication; -} -inline void validate_expr(const replication_exprt &value) -{ - validate_operands(value, 2, "Bit-wise replication must have two operands"); -} - /// \brief Concatenation of bit-vector operands /// /// This expression takes any number of operands @@ -4447,6 +4540,23 @@ class concatenation_exprt : public multi_ary_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_concatenation; +} + +// template<> +// inline void validate_expr( +// const concatenation_exprt &value) +// { +// validate_operands( +// value, +// 2, +// "Concatenation must have two or more operands", +// true); +// } + /// \brief Cast an exprt to a \ref concatenation_exprt /// /// \a expr must be known to be \ref concatenation_exprt. @@ -4472,21 +4582,6 @@ inline concatenation_exprt &to_concatenation_expr(exprt &expr) return static_cast(expr); } -template<> inline bool can_cast_expr(const exprt &base) -{ - return base.id()==ID_concatenation; -} -// template<> -// inline void validate_expr( -// const concatenation_exprt &value) -// { -// validate_operands( -// value, -// 2, -// "Concatenation must have two or more operands", -// true); -// } - /// \brief An expression denoting infinity class infinity_exprt : public nullary_exprt @@ -4541,6 +4636,17 @@ class let_exprt : public ternary_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_let; +} + +inline void validate_expr(const let_exprt &value) +{ + validate_operands(value, 3, "Let must have three operands"); +} + /// \brief Cast an exprt to a \ref let_exprt /// /// \a expr must be known to be \ref let_exprt. @@ -4562,15 +4668,6 @@ inline let_exprt &to_let_expr(exprt &expr) return static_cast(expr); } -template<> inline bool can_cast_expr(const exprt &base) -{ - return base.id()==ID_let; -} -inline void validate_expr(const let_exprt &value) -{ - validate_operands(value, 3, "Let must have three operands"); -} - /// \brief The popcount (counting the number of bits set to 1) expression class popcount_exprt: public unary_exprt { @@ -4591,6 +4688,17 @@ class popcount_exprt: public unary_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_popcount; +} + +inline void validate_expr(const popcount_exprt &value) +{ + validate_operands(value, 1, "popcount must have one operand"); +} + /// \brief Cast an exprt to a \ref popcount_exprt /// /// \a expr must be known to be \ref popcount_exprt. @@ -4612,16 +4720,6 @@ inline popcount_exprt &to_popcount_expr(exprt &expr) return static_cast(expr); } -template <> -inline bool can_cast_expr(const exprt &base) -{ - return base.id() == ID_popcount; -} -inline void validate_expr(const popcount_exprt &value) -{ - validate_operands(value, 1, "popcount must have one operand"); -} - /// this is a parametric version of an if-expression: it returns /// the value of the first case (using the ordering of the operands) /// whose condition evaluates to true. From 0a73e03b2458b2b6d45a1a9d45fb83622a9af86a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 13 Feb 2019 10:17:26 +0000 Subject: [PATCH 09/12] std_expr.h: add/enable missing can_cast, validate_expr Some were unnecessarily missing, others were wrongly commented out. --- src/util/std_expr.h | 86 ++++++++++++++------ unit/util/expr_cast/expr_undefined_casts.cpp | 11 --- 2 files changed, 59 insertions(+), 38 deletions(-) diff --git a/src/util/std_expr.h b/src/util/std_expr.h index 058f1d32e65..905aac1684e 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -354,6 +354,11 @@ inline bool can_cast_expr(const exprt &base) return base.operands().size() == 1; } +inline void validate_expr(const unary_exprt &value) +{ + validate_operands(value, 1, "Unary expressions must have one operand"); +} + /// \brief Cast an exprt to a \ref unary_exprt /// /// \a expr must be known to be \ref unary_exprt. @@ -774,6 +779,11 @@ inline bool can_cast_expr(const exprt &base) return base.operands().size() == 2; } +inline void validate_expr(const binary_exprt &value) +{ + validate_operands(value, 2, "Binary expressions must have two operands"); +} + /// \brief Cast an exprt to a \ref binary_exprt /// /// \a expr must be known to be \ref binary_exprt. @@ -912,6 +922,11 @@ inline bool can_cast_expr(const exprt &base) return can_cast_expr(base); } +inline void validate_expr(const binary_relation_exprt &value) +{ + validate_operands(value, 2, "Binary relations must have two operands"); +} + /// \brief Cast an exprt to a \ref binary_relation_exprt /// /// \a expr must be known to be \ref binary_relation_exprt. @@ -2657,10 +2672,10 @@ inline bool can_cast_expr(const exprt &base) return base.id() == ID_bitnot; } -// inline void validate_expr(const bitnot_exprt &value) -// { -// validate_operands(value, 1, "Bit-wise not must have one operand"); -// } +inline void validate_expr(const bitnot_exprt &value) +{ + validate_operands(value, 1, "Bit-wise not must have one operand"); +} /// \brief Cast an exprt to a \ref bitnot_exprt /// @@ -2671,8 +2686,8 @@ inline bool can_cast_expr(const exprt &base) inline const bitnot_exprt &to_bitnot_expr(const exprt &expr) { PRECONDITION(expr.id()==ID_bitnot); - // DATA_INVARIANT(expr.operands().size()==1, - // "Bit-wise not must have one operand"); + DATA_INVARIANT( + expr.operands().size() == 1, "Bit-wise not must have one operand"); return static_cast(expr); } @@ -2680,8 +2695,8 @@ inline const bitnot_exprt &to_bitnot_expr(const exprt &expr) inline bitnot_exprt &to_bitnot_expr(exprt &expr) { PRECONDITION(expr.id()==ID_bitnot); - // DATA_INVARIANT(expr.operands().size()==1, - // "Bit-wise not must have one operand"); + DATA_INVARIANT( + expr.operands().size() == 1, "Bit-wise not must have one operand"); return static_cast(expr); } @@ -2900,13 +2915,16 @@ class shift_exprt:public binary_exprt } }; -// The to_*_expr function for this type doesn't do any checks before casting, -// therefore the implementation is essentially a static_cast. -// Enabling expr_dynamic_cast would hide this; instead use static_cast directly. -// inline void validate_expr(const shift_exprt &value) -// { -// validate_operands(value, 2, "Shifts must have two operands"); -// } +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_shl || base.id() == ID_ashr || base.id() == ID_lshr; +} + +inline void validate_expr(const shift_exprt &value) +{ + validate_operands(value, 2, "Shifts must have two operands"); +} /// \brief Cast an exprt to a \ref shift_exprt /// @@ -3516,6 +3534,8 @@ inline bool can_cast_expr(const exprt &base) inline void validate_expr(const with_exprt &value) { + validate_operands( + value, 3, "array/structure update must have at least 3 operands", true); DATA_INVARIANT( value.operands().size() % 2 == 1, "array/structure update must have an odd number of operands"); @@ -4286,18 +4306,18 @@ class ieee_float_op_exprt : public ternary_exprt } }; -// The to_*_expr function for this type doesn't do any checks before casting, -// therefore the implementation is essentially a static_cast. -// Enabling expr_dynamic_cast would hide this; instead use static_cast directly. -// template<> -// inline void validate_expr( -// const ieee_float_op_exprt &value) -// { -// validate_operands( -// value, -// 3, -// "IEEE float operations must have three arguments"); -// } +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_floatbv_plus || base.id() == ID_floatbv_minus || + base.id() == ID_floatbv_div || base.id() == ID_floatbv_mult; +} + +inline void validate_expr(const ieee_float_op_exprt &value) +{ + validate_operands( + value, 3, "IEEE float operations must have three arguments"); +} /// \brief Cast an exprt to an \ref ieee_float_op_exprt /// @@ -4748,6 +4768,18 @@ class cond_exprt : public multi_ary_exprt } }; +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_cond; +} + +inline void validate_expr(const cond_exprt &value) +{ + DATA_INVARIANT( + value.operands().size() % 2 == 0, "cond must have even number of operands"); +} + /// \brief Cast an exprt to a \ref cond_exprt /// /// \a expr must be known to be \ref cond_exprt. diff --git a/unit/util/expr_cast/expr_undefined_casts.cpp b/unit/util/expr_cast/expr_undefined_casts.cpp index 4974f16aede..1a5abbfac63 100644 --- a/unit/util/expr_cast/expr_undefined_casts.cpp +++ b/unit/util/expr_cast/expr_undefined_casts.cpp @@ -26,17 +26,6 @@ SCENARIO("expr_dynamic_cast", { const exprt &expr=symbol_expr; - THEN("Casting from exprt reference to ieee_float_op_exprt " - "should not compile") - { - // This shouldn't compile - expr_dynamic_cast(expr); - } - THEN("Casting from exprt reference to shift_exprt should not compile") - { - // This shouldn't compile - expr_dynamic_cast(expr); - } THEN( "Casting from exprt reference to non-reference should not compile") { From 5e8af57404076f6d23c5f08965190363833ac693 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 13 Feb 2019 10:18:19 +0000 Subject: [PATCH 10/12] std_expr.h: remove commented-out validation steps Commented-out checks obviously don't check anything, and the code that was commented out wasn't particularly deep so that restoring it in future is trivial anyway. --- src/util/std_expr.h | 93 --------------------------------------------- 1 file changed, 93 deletions(-) diff --git a/src/util/std_expr.h b/src/util/std_expr.h index 905aac1684e..0043e6a00d1 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -2445,11 +2445,6 @@ inline bool can_cast_expr(const exprt &base) return base.id() == ID_and; } -// inline void validate_expr(const and_exprt &value) -// { -// validate_operands(value, 2, "And must have two or more operands", true); -// } - /// \brief Cast an exprt to a \ref and_exprt /// /// \a expr must be known to be \ref and_exprt. @@ -2459,9 +2454,6 @@ inline bool can_cast_expr(const exprt &base) inline const and_exprt &to_and_expr(const exprt &expr) { PRECONDITION(expr.id()==ID_and); - // DATA_INVARIANT( - // expr.operands().size()>=2, - // "And must have two or more operands"); return static_cast(expr); } @@ -2469,9 +2461,6 @@ inline const and_exprt &to_and_expr(const exprt &expr) inline and_exprt &to_and_expr(exprt &expr) { PRECONDITION(expr.id()==ID_and); - // DATA_INVARIANT( - // expr.operands().size()>=2, - // "And must have two or more operands"); return static_cast(expr); } @@ -2570,11 +2559,6 @@ inline bool can_cast_expr(const exprt &base) return base.id() == ID_or; } -// inline void validate_expr(const or_exprt &value) -// { -// validate_operands(value, 2, "Or must have two or more operands", true); -// } - /// \brief Cast an exprt to a \ref or_exprt /// /// \a expr must be known to be \ref or_exprt. @@ -2584,9 +2568,6 @@ inline bool can_cast_expr(const exprt &base) inline const or_exprt &to_or_expr(const exprt &expr) { PRECONDITION(expr.id()==ID_or); - // DATA_INVARIANT( - // expr.operands().size()>=2, - // "Or must have two or more operands"); return static_cast(expr); } @@ -2594,9 +2575,6 @@ inline const or_exprt &to_or_expr(const exprt &expr) inline or_exprt &to_or_expr(exprt &expr) { PRECONDITION(expr.id()==ID_or); - // DATA_INVARIANT( - // expr.operands().size()>=2, - // "Or must have two or more operands"); return static_cast(expr); } @@ -2622,15 +2600,6 @@ inline bool can_cast_expr(const exprt &base) return base.id() == ID_xor; } -// inline void validate_expr(const bitxor_exprt &value) -// { -// validate_operands( -// value, -// 2, -// "Bit-wise xor must have two or more operands", -// true); -// } - /// \brief Cast an exprt to a \ref xor_exprt /// /// \a expr must be known to be \ref xor_exprt. @@ -2722,15 +2691,6 @@ inline bool can_cast_expr(const exprt &base) return base.id() == ID_bitor; } -// inline void validate_expr(const bitor_exprt &value) -// { -// validate_operands( -// value, -// 2, -// "Bit-wise or must have two or more operands", -// true); -// } - /// \brief Cast an exprt to a \ref bitor_exprt /// /// \a expr must be known to be \ref bitor_exprt. @@ -2740,9 +2700,6 @@ inline bool can_cast_expr(const exprt &base) inline const bitor_exprt &to_bitor_expr(const exprt &expr) { PRECONDITION(expr.id()==ID_bitor); - // DATA_INVARIANT( - // expr.operands().size()>=2, - // "Bit-wise or must have two or more operands"); return static_cast(expr); } @@ -2750,9 +2707,6 @@ inline const bitor_exprt &to_bitor_expr(const exprt &expr) inline bitor_exprt &to_bitor_expr(exprt &expr) { PRECONDITION(expr.id()==ID_bitor); - // DATA_INVARIANT( - // expr.operands().size()>=2, - // "Bit-wise or must have two or more operands"); return static_cast(expr); } @@ -2778,15 +2732,6 @@ inline bool can_cast_expr(const exprt &base) return base.id() == ID_bitxor; } -// inline void validate_expr(const bitxor_exprt &value) -// { -// validate_operands( -// value, -// 2, -// "Bit-wise xor must have two or more operands", -// true); -// } - /// \brief Cast an exprt to a \ref bitxor_exprt /// /// \a expr must be known to be \ref bitxor_exprt. @@ -2796,9 +2741,6 @@ inline bool can_cast_expr(const exprt &base) inline const bitxor_exprt &to_bitxor_expr(const exprt &expr) { PRECONDITION(expr.id()==ID_bitxor); - // DATA_INVARIANT( - // expr.operands().size()>=2, - // "Bit-wise xor must have two or more operands"); return static_cast(expr); } @@ -2806,9 +2748,6 @@ inline const bitxor_exprt &to_bitxor_expr(const exprt &expr) inline bitxor_exprt &to_bitxor_expr(exprt &expr) { PRECONDITION(expr.id()==ID_bitxor); - // DATA_INVARIANT( - // expr.operands().size()>=2, - // "Bit-wise xor must have two or more operands"); return static_cast(expr); } @@ -2834,15 +2773,6 @@ inline bool can_cast_expr(const exprt &base) return base.id() == ID_bitand; } -// inline void validate_expr(const bitand_exprt &value) -// { -// validate_operands( -// value, -// 2, -// "Bit-wise and must have two or more operands", -// true); -// } - /// \brief Cast an exprt to a \ref bitand_exprt /// /// \a expr must be known to be \ref bitand_exprt. @@ -2852,9 +2782,6 @@ inline bool can_cast_expr(const exprt &base) inline const bitand_exprt &to_bitand_expr(const exprt &expr) { PRECONDITION(expr.id()==ID_bitand); - // DATA_INVARIANT( - // expr.operands().size()>=2, - // "Bit-wise and must have two or more operands"); return static_cast(expr); } @@ -2862,9 +2789,6 @@ inline const bitand_exprt &to_bitand_expr(const exprt &expr) inline bitand_exprt &to_bitand_expr(exprt &expr) { PRECONDITION(expr.id()==ID_bitand); - // DATA_INVARIANT( - // expr.operands().size()>=2, - // "Bit-wise and must have two or more operands"); return static_cast(expr); } @@ -4566,17 +4490,6 @@ inline bool can_cast_expr(const exprt &base) return base.id() == ID_concatenation; } -// template<> -// inline void validate_expr( -// const concatenation_exprt &value) -// { -// validate_operands( -// value, -// 2, -// "Concatenation must have two or more operands", -// true); -// } - /// \brief Cast an exprt to a \ref concatenation_exprt /// /// \a expr must be known to be \ref concatenation_exprt. @@ -4586,9 +4499,6 @@ inline bool can_cast_expr(const exprt &base) inline const concatenation_exprt &to_concatenation_expr(const exprt &expr) { PRECONDITION(expr.id()==ID_concatenation); - // DATA_INVARIANT( - // expr.operands().size()>=2, - // "Concatenation must have two or more operands"); return static_cast(expr); } @@ -4596,9 +4506,6 @@ inline const concatenation_exprt &to_concatenation_expr(const exprt &expr) inline concatenation_exprt &to_concatenation_expr(exprt &expr) { PRECONDITION(expr.id()==ID_concatenation); - // DATA_INVARIANT( - // expr.operands().size()>=2, - // "Concatenation must have two or more operands"); return static_cast(expr); } From 4b5d3563e5e6cae8140f2c1154b5a8747e50564f Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 13 Feb 2019 10:30:32 +0000 Subject: [PATCH 11/12] Re-use validate_expr in to_*exprt This provides two advantages: 1) Member access such as testing the number of operands does not break sharing, because it is done in a const context. 2) Code re-use: we no longer implement the same check in two different ways. All changes in this commit were applied automatically via text replacement. --- src/util/std_expr.h | 676 +++++++++++++++++++++----------------------- 1 file changed, 320 insertions(+), 356 deletions(-) diff --git a/src/util/std_expr.h b/src/util/std_expr.h index 0043e6a00d1..bc2968dd93c 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -226,16 +226,18 @@ inline void validate_expr(const symbol_exprt &value) inline const symbol_exprt &to_symbol_expr(const exprt &expr) { PRECONDITION(expr.id()==ID_symbol); - DATA_INVARIANT(!expr.has_operands(), "Symbols must not have operands"); - return static_cast(expr); + const symbol_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \copydoc to_symbol_expr(const exprt &) inline symbol_exprt &to_symbol_expr(exprt &expr) { PRECONDITION(expr.id()==ID_symbol); - DATA_INVARIANT(!expr.has_operands(), "Symbols must not have operands"); - return static_cast(expr); + symbol_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } @@ -282,16 +284,19 @@ inline void validate_expr(const nondet_symbol_exprt &value) inline const nondet_symbol_exprt &to_nondet_symbol_expr(const exprt &expr) { PRECONDITION(expr.id()==ID_nondet_symbol); - DATA_INVARIANT(!expr.has_operands(), "Symbols must not have operands"); - return static_cast(expr); + const nondet_symbol_exprt &ret = + static_cast(expr); + validate_expr(ret); + return ret; } /// \copydoc to_nondet_symbol_expr(const exprt &) inline nondet_symbol_exprt &to_nondet_symbol_expr(exprt &expr) { PRECONDITION(expr.id()==ID_symbol); - DATA_INVARIANT(!expr.has_operands(), "Symbols must not have operands"); - return static_cast(expr); + nondet_symbol_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } @@ -367,19 +372,17 @@ inline void validate_expr(const unary_exprt &value) /// \return Object of type \ref unary_exprt inline const unary_exprt &to_unary_expr(const exprt &expr) { - DATA_INVARIANT( - expr.operands().size()==1, - "Unary expressions must have one operand"); - return static_cast(expr); + const unary_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \copydoc to_unary_expr(const exprt &) inline unary_exprt &to_unary_expr(exprt &expr) { - DATA_INVARIANT( - expr.operands().size()==1, - "Unary expressions must have one operand"); - return static_cast(expr); + unary_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } @@ -418,20 +421,18 @@ inline void validate_expr(const abs_exprt &value) inline const abs_exprt &to_abs_expr(const exprt &expr) { PRECONDITION(expr.id()==ID_abs); - DATA_INVARIANT( - expr.operands().size()==1, - "Absolute value must have one operand"); - return static_cast(expr); + const abs_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \copydoc to_abs_expr(const exprt &) inline abs_exprt &to_abs_expr(exprt &expr) { PRECONDITION(expr.id()==ID_abs); - DATA_INVARIANT( - expr.operands().size()==1, - "Absolute value must have one operand"); - return static_cast(expr); + abs_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } @@ -477,20 +478,18 @@ inline void validate_expr(const unary_minus_exprt &value) inline const unary_minus_exprt &to_unary_minus_expr(const exprt &expr) { PRECONDITION(expr.id()==ID_unary_minus); - DATA_INVARIANT( - expr.operands().size()==1, - "Unary minus must have one operand"); - return static_cast(expr); + const unary_minus_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \copydoc to_unary_minus_expr(const exprt &) inline unary_minus_exprt &to_unary_minus_expr(exprt &expr) { PRECONDITION(expr.id()==ID_unary_minus); - DATA_INVARIANT( - expr.operands().size()==1, - "Unary minus must have one operand"); - return static_cast(expr); + unary_minus_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \brief The unary plus expression @@ -523,18 +522,18 @@ inline void validate_expr(const unary_plus_exprt &value) inline const unary_plus_exprt &to_unary_plus_expr(const exprt &expr) { PRECONDITION(expr.id() == ID_unary_plus); - DATA_INVARIANT( - expr.operands().size() == 1, "unary plus must have one operand"); - return static_cast(expr); + const unary_plus_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \copydoc to_unary_minus_expr(const exprt &) inline unary_plus_exprt &to_unary_plus_expr(exprt &expr) { PRECONDITION(expr.id() == ID_unary_plus); - DATA_INVARIANT( - expr.operands().size() == 1, "unary plus must have one operand"); - return static_cast(expr); + unary_plus_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \brief The byte swap expression @@ -586,20 +585,18 @@ inline void validate_expr(const bswap_exprt &value) inline const bswap_exprt &to_bswap_expr(const exprt &expr) { PRECONDITION(expr.id() == ID_bswap); - DATA_INVARIANT(expr.operands().size() == 1, "bswap must have one operand"); - DATA_INVARIANT( - expr.op0().type() == expr.type(), "bswap type must match operand type"); - return static_cast(expr); + const bswap_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \copydoc to_bswap_expr(const exprt &) inline bswap_exprt &to_bswap_expr(exprt &expr) { PRECONDITION(expr.id() == ID_bswap); - DATA_INVARIANT(expr.operands().size() == 1, "bswap must have one operand"); - DATA_INVARIANT( - expr.op0().type() == expr.type(), "bswap type must match operand type"); - return static_cast(expr); + bswap_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \brief A base class for expressions that are predicates, @@ -692,18 +689,18 @@ inline void validate_expr(const sign_exprt &expr) inline const sign_exprt &to_sign_expr(const exprt &expr) { PRECONDITION(expr.id() == ID_sign); - DATA_INVARIANT( - expr.operands().size() == 1, "sign expression must have one operand"); - return static_cast(expr); + const sign_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \copydoc to_sign_expr(const exprt &) inline sign_exprt &to_sign_expr(exprt &expr) { PRECONDITION(expr.id() == ID_sign); - DATA_INVARIANT( - expr.operands().size() == 1, "sign expression must have one operand"); - return static_cast(expr); + sign_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \brief A base class for binary expressions @@ -1122,20 +1119,18 @@ inline void validate_expr(const plus_exprt &value) inline const plus_exprt &to_plus_expr(const exprt &expr) { PRECONDITION(expr.id()==ID_plus); - DATA_INVARIANT( - expr.operands().size()>=2, - "Plus must have two or more operands"); - return static_cast(expr); + const plus_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \copydoc to_plus_expr(const exprt &) inline plus_exprt &to_plus_expr(exprt &expr) { PRECONDITION(expr.id()==ID_plus); - DATA_INVARIANT( - expr.operands().size()>=2, - "Plus must have two or more operands"); - return static_cast(expr); + plus_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } @@ -1176,20 +1171,18 @@ inline void validate_expr(const minus_exprt &value) inline const minus_exprt &to_minus_expr(const exprt &expr) { PRECONDITION(expr.id()==ID_minus); - DATA_INVARIANT( - expr.operands().size()>=2, - "Minus must have two or more operands"); - return static_cast(expr); + const minus_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \copydoc to_minus_expr(const exprt &) inline minus_exprt &to_minus_expr(exprt &expr) { PRECONDITION(expr.id()==ID_minus); - DATA_INVARIANT( - expr.operands().size()>=2, - "Minus must have two or more operands"); - return static_cast(expr); + minus_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } @@ -1231,20 +1224,18 @@ inline void validate_expr(const mult_exprt &value) inline const mult_exprt &to_mult_expr(const exprt &expr) { PRECONDITION(expr.id()==ID_mult); - DATA_INVARIANT( - expr.operands().size()>=2, - "Multiply must have two or more operands"); - return static_cast(expr); + const mult_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \copydoc to_mult_expr(const exprt &) inline mult_exprt &to_mult_expr(exprt &expr) { PRECONDITION(expr.id()==ID_mult); - DATA_INVARIANT( - expr.operands().size()>=2, - "Multiply must have two or more operands"); - return static_cast(expr); + mult_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } @@ -1309,20 +1300,18 @@ inline void validate_expr(const div_exprt &value) inline const div_exprt &to_div_expr(const exprt &expr) { PRECONDITION(expr.id()==ID_div); - DATA_INVARIANT( - expr.operands().size()==2, - "Divide must have two operands"); - return static_cast(expr); + const div_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \copydoc to_div_expr(const exprt &) inline div_exprt &to_div_expr(exprt &expr) { PRECONDITION(expr.id()==ID_div); - DATA_INVARIANT( - expr.operands().size()==2, - "Divide must have two operands"); - return static_cast(expr); + div_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } @@ -1363,16 +1352,18 @@ inline void validate_expr(const mod_exprt &value) inline const mod_exprt &to_mod_expr(const exprt &expr) { PRECONDITION(expr.id()==ID_mod); - DATA_INVARIANT(expr.operands().size()==2, "Modulo must have two operands"); - return static_cast(expr); + const mod_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \copydoc to_mod_expr(const exprt &) inline mod_exprt &to_mod_expr(exprt &expr) { PRECONDITION(expr.id()==ID_mod); - DATA_INVARIANT(expr.operands().size()==2, "Modulo must have two operands"); - return static_cast(expr); + mod_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } @@ -1413,16 +1404,18 @@ inline void validate_expr(const rem_exprt &value) inline const rem_exprt &to_rem_expr(const exprt &expr) { PRECONDITION(expr.id()==ID_rem); - DATA_INVARIANT(expr.operands().size()==2, "Remainder must have two operands"); - return static_cast(expr); + const rem_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \copydoc to_rem_expr(const exprt &) inline rem_exprt &to_rem_expr(exprt &expr) { PRECONDITION(expr.id()==ID_rem); - DATA_INVARIANT(expr.operands().size()==2, "Remainder must have two operands"); - return static_cast(expr); + rem_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } @@ -1524,20 +1517,18 @@ inline void validate_expr(const notequal_exprt &value) inline const notequal_exprt &to_notequal_expr(const exprt &expr) { PRECONDITION(expr.id()==ID_notequal); - DATA_INVARIANT( - expr.operands().size()==2, - "Inequality must have two operands"); - return static_cast(expr); + const notequal_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \copydoc to_notequal_expr(const exprt &) inline notequal_exprt &to_notequal_expr(exprt &expr) { PRECONDITION(expr.id()==ID_notequal); - DATA_INVARIANT( - expr.operands().size()==2, - "Inequality must have two operands"); - return static_cast(expr); + notequal_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } @@ -1609,20 +1600,18 @@ inline void validate_expr(const index_exprt &value) inline const index_exprt &to_index_expr(const exprt &expr) { PRECONDITION(expr.id()==ID_index); - DATA_INVARIANT( - expr.operands().size()==2, - "Array index must have two operands"); - return static_cast(expr); + const index_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \copydoc to_index_expr(const exprt &) inline index_exprt &to_index_expr(exprt &expr) { PRECONDITION(expr.id()==ID_index); - DATA_INVARIANT( - expr.operands().size()==2, - "Array index must have two operands"); - return static_cast(expr); + index_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } @@ -1672,20 +1661,18 @@ inline void validate_expr(const array_of_exprt &value) inline const array_of_exprt &to_array_of_expr(const exprt &expr) { PRECONDITION(expr.id()==ID_array_of); - DATA_INVARIANT( - expr.operands().size()==1, - "'Array of' must have one operand"); - return static_cast(expr); + const array_of_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \copydoc to_array_of_expr(const exprt &) inline array_of_exprt &to_array_of_expr(exprt &expr) { PRECONDITION(expr.id()==ID_array_of); - DATA_INVARIANT( - expr.operands().size()==1, - "'Array of' must have one operand"); - return static_cast(expr); + array_of_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } @@ -1875,20 +1862,18 @@ inline void validate_expr(const union_exprt &value) inline const union_exprt &to_union_expr(const exprt &expr) { PRECONDITION(expr.id()==ID_union); - DATA_INVARIANT( - expr.operands().size()==1, - "Union constructor must have one operand"); - return static_cast(expr); + const union_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \copydoc to_union_expr(const exprt &) inline union_exprt &to_union_expr(exprt &expr) { PRECONDITION(expr.id()==ID_union); - DATA_INVARIANT( - expr.operands().size()==1, - "Union constructor must have one operand"); - return static_cast(expr); + union_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } @@ -2005,20 +1990,18 @@ inline void validate_expr(const complex_exprt &value) inline const complex_exprt &to_complex_expr(const exprt &expr) { PRECONDITION(expr.id()==ID_complex); - DATA_INVARIANT( - expr.operands().size()==2, - "Complex constructor must have two operands"); - return static_cast(expr); + const complex_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \copydoc to_complex_expr(const exprt &) inline complex_exprt &to_complex_expr(exprt &expr) { PRECONDITION(expr.id()==ID_complex); - DATA_INVARIANT( - expr.operands().size()==2, - "Complex constructor must have two operands"); - return static_cast(expr); + complex_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \brief Real part of the expression describing a complex number. @@ -2052,20 +2035,18 @@ inline void validate_expr(const complex_real_exprt &expr) inline const complex_real_exprt &to_complex_real_expr(const exprt &expr) { PRECONDITION(expr.id() == ID_complex_real); - DATA_INVARIANT( - expr.operands().size() == 1, - "real part retrieval operation must have one operand"); - return static_cast(expr); + const complex_real_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \copydoc to_complex_real_expr(const exprt &) inline complex_real_exprt &to_complex_real_expr(exprt &expr) { PRECONDITION(expr.id() == ID_complex_real); - DATA_INVARIANT( - expr.operands().size() == 1, - "real part retrieval operation must have one operand"); - return static_cast(expr); + complex_real_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \brief Imaginary part of the expression describing a complex number. @@ -2099,20 +2080,18 @@ inline void validate_expr(const complex_imag_exprt &expr) inline const complex_imag_exprt &to_complex_imag_expr(const exprt &expr) { PRECONDITION(expr.id() == ID_complex_imag); - DATA_INVARIANT( - expr.operands().size() == 1, - "imaginary part retrieval operation must have one operand"); - return static_cast(expr); + const complex_imag_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \copydoc to_complex_imag_expr(const exprt &) inline complex_imag_exprt &to_complex_imag_expr(exprt &expr) { PRECONDITION(expr.id() == ID_complex_imag); - DATA_INVARIANT( - expr.operands().size() == 1, - "imaginary part retrieval operation must have one operand"); - return static_cast(expr); + complex_imag_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } class namespacet; @@ -2176,20 +2155,19 @@ inline const object_descriptor_exprt &to_object_descriptor_expr( const exprt &expr) { PRECONDITION(expr.id()==ID_object_descriptor); - DATA_INVARIANT( - expr.operands().size()==2, - "Object descriptor must have two operands"); - return static_cast(expr); + const object_descriptor_exprt &ret = + static_cast(expr); + validate_expr(ret); + return ret; } /// \copydoc to_object_descriptor_expr(const exprt &) inline object_descriptor_exprt &to_object_descriptor_expr(exprt &expr) { PRECONDITION(expr.id()==ID_object_descriptor); - DATA_INVARIANT( - expr.operands().size()==2, - "Object descriptor must have two operands"); - return static_cast(expr); + object_descriptor_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } @@ -2247,20 +2225,19 @@ inline const dynamic_object_exprt &to_dynamic_object_expr( const exprt &expr) { PRECONDITION(expr.id()==ID_dynamic_object); - DATA_INVARIANT( - expr.operands().size()==2, - "Dynamic object must have two operands"); - return static_cast(expr); + const dynamic_object_exprt &ret = + static_cast(expr); + validate_expr(ret); + return ret; } /// \copydoc to_dynamic_object_expr(const exprt &) inline dynamic_object_exprt &to_dynamic_object_expr(exprt &expr) { PRECONDITION(expr.id()==ID_dynamic_object); - DATA_INVARIANT( - expr.operands().size()==2, - "Dynamic object must have two operands"); - return static_cast(expr); + dynamic_object_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } @@ -2308,20 +2285,18 @@ inline void validate_expr(const typecast_exprt &value) inline const typecast_exprt &to_typecast_expr(const exprt &expr) { PRECONDITION(expr.id()==ID_typecast); - DATA_INVARIANT( - expr.operands().size()==1, - "Typecast must have one operand"); - return static_cast(expr); + const typecast_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \copydoc to_typecast_expr(const exprt &) inline typecast_exprt &to_typecast_expr(exprt &expr) { PRECONDITION(expr.id()==ID_typecast); - DATA_INVARIANT( - expr.operands().size()==1, - "Typecast must have one operand"); - return static_cast(expr); + typecast_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } @@ -2382,20 +2357,19 @@ inline void validate_expr(const floatbv_typecast_exprt &value) inline const floatbv_typecast_exprt &to_floatbv_typecast_expr(const exprt &expr) { PRECONDITION(expr.id()==ID_floatbv_typecast); - DATA_INVARIANT( - expr.operands().size()==2, - "Float typecast must have two operands"); - return static_cast(expr); + const floatbv_typecast_exprt &ret = + static_cast(expr); + validate_expr(ret); + return ret; } /// \copydoc to_floatbv_typecast_expr(const exprt &) inline floatbv_typecast_exprt &to_floatbv_typecast_expr(exprt &expr) { PRECONDITION(expr.id()==ID_floatbv_typecast); - DATA_INVARIANT( - expr.operands().size()==2, - "Float typecast must have two operands"); - return static_cast(expr); + floatbv_typecast_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } @@ -2500,16 +2474,18 @@ inline void validate_expr(const implies_exprt &value) inline const implies_exprt &to_implies_expr(const exprt &expr) { PRECONDITION(expr.id()==ID_implies); - DATA_INVARIANT(expr.operands().size()==2, "Implies must have two operands"); - return static_cast(expr); + const implies_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \copydoc to_implies_expr(const exprt &) inline implies_exprt &to_implies_expr(exprt &expr) { PRECONDITION(expr.id()==ID_implies); - DATA_INVARIANT(expr.operands().size()==2, "Implies must have two operands"); - return static_cast(expr); + implies_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } @@ -2655,18 +2631,18 @@ inline void validate_expr(const bitnot_exprt &value) inline const bitnot_exprt &to_bitnot_expr(const exprt &expr) { PRECONDITION(expr.id()==ID_bitnot); - DATA_INVARIANT( - expr.operands().size() == 1, "Bit-wise not must have one operand"); - return static_cast(expr); + const bitnot_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \copydoc to_bitnot_expr(const exprt &) inline bitnot_exprt &to_bitnot_expr(exprt &expr) { PRECONDITION(expr.id()==ID_bitnot); - DATA_INVARIANT( - expr.operands().size() == 1, "Bit-wise not must have one operand"); - return static_cast(expr); + bitnot_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } @@ -2858,19 +2834,17 @@ inline void validate_expr(const shift_exprt &value) /// \return Object of type \ref shift_exprt inline const shift_exprt &to_shift_expr(const exprt &expr) { - DATA_INVARIANT( - expr.operands().size()==2, - "Shifts must have two operands"); - return static_cast(expr); + const shift_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \copydoc to_shift_expr(const exprt &) inline shift_exprt &to_shift_expr(exprt &expr) { - DATA_INVARIANT( - expr.operands().size()==2, - "Shifts must have two operands"); - return static_cast(expr); + shift_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } @@ -2903,18 +2877,18 @@ class shl_exprt:public shift_exprt inline const shl_exprt &to_shl_expr(const exprt &expr) { PRECONDITION(expr.id() == ID_shl); - DATA_INVARIANT( - expr.operands().size() == 2, "Bit-wise shl must have two operands"); - return static_cast(expr); + const shl_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \copydoc to_shl_expr(const exprt &) inline shl_exprt &to_shl_expr(exprt &expr) { PRECONDITION(expr.id() == ID_shl); - DATA_INVARIANT( - expr.operands().size() == 2, "Bit-wise shl must have two operands"); - return static_cast(expr); + shl_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \brief Arithmetic right shift @@ -3019,20 +2993,18 @@ inline void validate_expr(const extractbit_exprt &value) inline const extractbit_exprt &to_extractbit_expr(const exprt &expr) { PRECONDITION(expr.id()==ID_extractbit); - DATA_INVARIANT( - expr.operands().size()==2, - "Extract bit must have two operands"); - return static_cast(expr); + const extractbit_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \copydoc to_extractbit_expr(const exprt &) inline extractbit_exprt &to_extractbit_expr(exprt &expr) { PRECONDITION(expr.id()==ID_extractbit); - DATA_INVARIANT( - expr.operands().size()==2, - "Extract bit must have two operands"); - return static_cast(expr); + extractbit_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } @@ -3120,20 +3092,18 @@ inline void validate_expr(const extractbits_exprt &value) inline const extractbits_exprt &to_extractbits_expr(const exprt &expr) { PRECONDITION(expr.id()==ID_extractbits); - DATA_INVARIANT( - expr.operands().size()==3, - "Extract bits must have three operands"); - return static_cast(expr); + const extractbits_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \copydoc to_extractbits_expr(const exprt &) inline extractbits_exprt &to_extractbits_expr(exprt &expr) { PRECONDITION(expr.id()==ID_extractbits); - DATA_INVARIANT( - expr.operands().size()==3, - "Extract bits must have three operands"); - return static_cast(expr); + extractbits_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } @@ -3179,16 +3149,18 @@ inline void validate_expr(const address_of_exprt &value) inline const address_of_exprt &to_address_of_expr(const exprt &expr) { PRECONDITION(expr.id()==ID_address_of); - DATA_INVARIANT(expr.operands().size()==1, "Address of must have one operand"); - return static_cast(expr); + const address_of_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \copydoc to_address_of_expr(const exprt &) inline address_of_exprt &to_address_of_expr(exprt &expr) { PRECONDITION(expr.id()==ID_address_of); - DATA_INVARIANT(expr.operands().size()==1, "Address of must have one operand"); - return static_cast(expr); + address_of_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } @@ -3228,16 +3200,18 @@ inline void validate_expr(const not_exprt &value) inline const not_exprt &to_not_expr(const exprt &expr) { PRECONDITION(expr.id()==ID_not); - DATA_INVARIANT(expr.operands().size()==1, "Not must have one operand"); - return static_cast(expr); + const not_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \copydoc to_not_expr(const exprt &) inline not_exprt &to_not_expr(exprt &expr) { PRECONDITION(expr.id()==ID_not); - DATA_INVARIANT(expr.operands().size()==1, "Not must have one operand"); - return static_cast(expr); + not_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } @@ -3298,20 +3272,18 @@ inline void validate_expr(const dereference_exprt &value) inline const dereference_exprt &to_dereference_expr(const exprt &expr) { PRECONDITION(expr.id()==ID_dereference); - DATA_INVARIANT( - expr.operands().size()==1, - "Dereference must have one operand"); - return static_cast(expr); + const dereference_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \copydoc to_dereference_expr(const exprt &) inline dereference_exprt &to_dereference_expr(exprt &expr) { PRECONDITION(expr.id()==ID_dereference); - DATA_INVARIANT( - expr.operands().size()==1, - "Dereference must have one operand"); - return static_cast(expr); + dereference_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } @@ -3385,20 +3357,18 @@ inline void validate_expr(const if_exprt &value) inline const if_exprt &to_if_expr(const exprt &expr) { PRECONDITION(expr.id()==ID_if); - DATA_INVARIANT( - expr.operands().size()==3, - "If-then-else must have three operands"); - return static_cast(expr); + const if_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \copydoc to_if_expr(const exprt &) inline if_exprt &to_if_expr(exprt &expr) { PRECONDITION(expr.id()==ID_if); - DATA_INVARIANT( - expr.operands().size()==3, - "If-then-else must have three operands"); - return static_cast(expr); + if_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \brief Operator to update elements in structs and arrays @@ -3474,20 +3444,18 @@ inline void validate_expr(const with_exprt &value) inline const with_exprt &to_with_expr(const exprt &expr) { PRECONDITION(expr.id()==ID_with); - DATA_INVARIANT( - expr.operands().size() >= 3 && expr.operands().size() % 2 == 1, - "array/structure update must have at least three operands"); - return static_cast(expr); + const with_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \copydoc to_with_expr(const exprt &) inline with_exprt &to_with_expr(exprt &expr) { PRECONDITION(expr.id()==ID_with); - DATA_INVARIANT( - expr.operands().size() >= 3 && expr.operands().size() % 2 == 1, - "array/structure update must have at least three operands"); - return static_cast(expr); + with_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } class index_designatort : public expr_protectedt @@ -3530,20 +3498,18 @@ inline void validate_expr(const index_designatort &value) inline const index_designatort &to_index_designator(const exprt &expr) { PRECONDITION(expr.id()==ID_index_designator); - DATA_INVARIANT( - expr.operands().size()==1, - "Index designator must have one operand"); - return static_cast(expr); + const index_designatort &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \copydoc to_index_designator(const exprt &) inline index_designatort &to_index_designator(exprt &expr) { PRECONDITION(expr.id()==ID_index_designator); - DATA_INVARIANT( - expr.operands().size()==1, - "Index designator must have one operand"); - return static_cast(expr); + index_designatort &ret = static_cast(expr); + validate_expr(ret); + return ret; } class member_designatort : public expr_protectedt @@ -3581,20 +3547,18 @@ inline void validate_expr(const member_designatort &value) inline const member_designatort &to_member_designator(const exprt &expr) { PRECONDITION(expr.id()==ID_member_designator); - DATA_INVARIANT( - !expr.has_operands(), - "Member designator must not have operands"); - return static_cast(expr); + const member_designatort &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \copydoc to_member_designator(const exprt &) inline member_designatort &to_member_designator(exprt &expr) { PRECONDITION(expr.id()==ID_member_designator); - DATA_INVARIANT( - !expr.has_operands(), - "Member designator must not have operands"); - return static_cast(expr); + member_designatort &ret = static_cast(expr); + validate_expr(ret); + return ret; } @@ -3677,20 +3641,18 @@ inline void validate_expr(const update_exprt &value) inline const update_exprt &to_update_expr(const exprt &expr) { PRECONDITION(expr.id()==ID_update); - DATA_INVARIANT( - expr.operands().size()==3, - "Array/structure update must have three operands"); - return static_cast(expr); + const update_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \copydoc to_update_expr(const exprt &) inline update_exprt &to_update_expr(exprt &expr) { PRECONDITION(expr.id()==ID_update); - DATA_INVARIANT( - expr.operands().size() == 3, - "Array/structure update must have three operands"); - return static_cast(expr); + update_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } @@ -3763,20 +3725,18 @@ inline void validate_expr(const array_update_exprt &value) inline const array_update_exprt &to_array_update_expr(const exprt &expr) { PRECONDITION(expr.id()==ID_array_update); - DATA_INVARIANT( - expr.operands().size()==3, - "Array update must have three operands"); - return static_cast(expr); + const array_update_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \copydoc to_array_update_expr(const exprt &) inline array_update_exprt &to_array_update_expr(exprt &expr) { PRECONDITION(expr.id()==ID_array_update); - DATA_INVARIANT( - expr.operands().size()==3, - "Array update must have three operands"); - return static_cast(expr); + array_update_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } #endif @@ -3866,20 +3826,18 @@ inline void validate_expr(const member_exprt &value) inline const member_exprt &to_member_expr(const exprt &expr) { PRECONDITION(expr.id()==ID_member); - DATA_INVARIANT( - expr.operands().size()==1, - "Extract member must have one operand"); - return static_cast(expr); + const member_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \copydoc to_member_expr(const exprt &) inline member_exprt &to_member_expr(exprt &expr) { PRECONDITION(expr.id()==ID_member); - DATA_INVARIANT( - expr.operands().size()==1, - "Extract member must have one operand"); - return static_cast(expr); + member_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } @@ -3918,16 +3876,18 @@ inline void validate_expr(const isnan_exprt &value) inline const isnan_exprt &to_isnan_expr(const exprt &expr) { PRECONDITION(expr.id()==ID_isnan); - DATA_INVARIANT(expr.operands().size()==1, "Is NaN must have one operand"); - return static_cast(expr); + const isnan_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \copydoc to_isnan_expr(const exprt &) inline isnan_exprt &to_isnan_expr(exprt &expr) { PRECONDITION(expr.id()==ID_isnan); - DATA_INVARIANT(expr.operands().size()==1, "Is NaN must have one operand"); - return static_cast(expr); + isnan_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } @@ -3966,20 +3926,18 @@ inline void validate_expr(const isinf_exprt &value) inline const isinf_exprt &to_isinf_expr(const exprt &expr) { PRECONDITION(expr.id()==ID_isinf); - DATA_INVARIANT( - expr.operands().size()==1, - "Is infinite must have one operand"); - return static_cast(expr); + const isinf_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \copydoc to_isinf_expr(const exprt &) inline isinf_exprt &to_isinf_expr(exprt &expr) { PRECONDITION(expr.id()==ID_isinf); - DATA_INVARIANT( - expr.operands().size()==1, - "Is infinite must have one operand"); - return static_cast(expr); + isinf_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } @@ -4018,16 +3976,18 @@ inline void validate_expr(const isfinite_exprt &value) inline const isfinite_exprt &to_isfinite_expr(const exprt &expr) { PRECONDITION(expr.id()==ID_isfinite); - DATA_INVARIANT(expr.operands().size()==1, "Is finite must have one operand"); - return static_cast(expr); + const isfinite_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \copydoc to_isfinite_expr(const exprt &) inline isfinite_exprt &to_isfinite_expr(exprt &expr) { PRECONDITION(expr.id()==ID_isfinite); - DATA_INVARIANT(expr.operands().size()==1, "Is finite must have one operand"); - return static_cast(expr); + isfinite_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } @@ -4066,16 +4026,18 @@ inline void validate_expr(const isnormal_exprt &value) inline const isnormal_exprt &to_isnormal_expr(const exprt &expr) { PRECONDITION(expr.id()==ID_isnormal); - DATA_INVARIANT(expr.operands().size()==1, "Is normal must have one operand"); - return static_cast(expr); + const isnormal_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \copydoc to_isnormal_expr(const exprt &) inline isnormal_exprt &to_isnormal_expr(exprt &expr) { PRECONDITION(expr.id()==ID_isnormal); - DATA_INVARIANT(expr.operands().size()==1, "Is normal must have one operand"); - return static_cast(expr); + isnormal_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } @@ -4114,20 +4076,19 @@ inline void validate_expr(const ieee_float_equal_exprt &value) inline const ieee_float_equal_exprt &to_ieee_float_equal_expr(const exprt &expr) { PRECONDITION(expr.id()==ID_ieee_float_equal); - DATA_INVARIANT( - expr.operands().size()==2, - "IEEE equality must have two operands"); - return static_cast(expr); + const ieee_float_equal_exprt &ret = + static_cast(expr); + validate_expr(ret); + return ret; } /// \copydoc to_ieee_float_equal_expr(const exprt &) inline ieee_float_equal_exprt &to_ieee_float_equal_expr(exprt &expr) { PRECONDITION(expr.id()==ID_ieee_float_equal); - DATA_INVARIANT( - expr.operands().size()==2, - "IEEE equality must have two operands"); - return static_cast(expr); + ieee_float_equal_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } @@ -4168,20 +4129,20 @@ inline const ieee_float_notequal_exprt &to_ieee_float_notequal_expr( const exprt &expr) { PRECONDITION(expr.id()==ID_ieee_float_notequal); - DATA_INVARIANT( - expr.operands().size()==2, - "IEEE inequality must have two operands"); - return static_cast(expr); + const ieee_float_notequal_exprt &ret = + static_cast(expr); + validate_expr(ret); + return ret; } /// \copydoc to_ieee_float_notequal_expr(const exprt &) inline ieee_float_notequal_exprt &to_ieee_float_notequal_expr(exprt &expr) { PRECONDITION(expr.id()==ID_ieee_float_notequal); - DATA_INVARIANT( - expr.operands().size()==2, - "IEEE inequality must have two operands"); - return static_cast(expr); + ieee_float_notequal_exprt &ret = + static_cast(expr); + validate_expr(ret); + return ret; } /// \brief IEEE floating-point operations @@ -4251,19 +4212,18 @@ inline void validate_expr(const ieee_float_op_exprt &value) /// \return Object of type \ref ieee_float_op_exprt inline const ieee_float_op_exprt &to_ieee_float_op_expr(const exprt &expr) { - DATA_INVARIANT( - expr.operands().size()==3, - "IEEE float operations must have three arguments"); - return static_cast(expr); + const ieee_float_op_exprt &ret = + static_cast(expr); + validate_expr(ret); + return ret; } /// \copydoc to_ieee_float_op_expr(const exprt &) inline ieee_float_op_exprt &to_ieee_float_op_expr(exprt &expr) { - DATA_INVARIANT( - expr.operands().size()==3, - "IEEE float operations must have three arguments"); - return static_cast(expr); + ieee_float_op_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } @@ -4440,18 +4400,18 @@ inline void validate_expr(const replication_exprt &value) inline const replication_exprt &to_replication_expr(const exprt &expr) { PRECONDITION(expr.id() == ID_replication); - DATA_INVARIANT( - expr.operands().size() == 2, "Bit-wise replication must have two operands"); - return static_cast(expr); + const replication_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \copydoc to_replication_expr(const exprt &) inline replication_exprt &to_replication_expr(exprt &expr) { PRECONDITION(expr.id() == ID_replication); - DATA_INVARIANT( - expr.operands().size() == 2, "Bit-wise replication must have two operands"); - return static_cast(expr); + replication_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \brief Concatenation of bit-vector operands @@ -4583,16 +4543,18 @@ inline void validate_expr(const let_exprt &value) inline const let_exprt &to_let_expr(const exprt &expr) { PRECONDITION(expr.id()==ID_let); - DATA_INVARIANT(expr.operands().size()==3, "Let must have three operands"); - return static_cast(expr); + const let_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \copydoc to_let_expr(const exprt &) inline let_exprt &to_let_expr(exprt &expr) { PRECONDITION(expr.id()==ID_let); - DATA_INVARIANT(expr.operands().size()==3, "Let must have three operands"); - return static_cast(expr); + let_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \brief The popcount (counting the number of bits set to 1) expression @@ -4635,16 +4597,18 @@ inline void validate_expr(const popcount_exprt &value) inline const popcount_exprt &to_popcount_expr(const exprt &expr) { PRECONDITION(expr.id() == ID_popcount); - DATA_INVARIANT(expr.operands().size() == 1, "popcount must have one operand"); - return static_cast(expr); + const popcount_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \copydoc to_popcount_expr(const exprt &) inline popcount_exprt &to_popcount_expr(exprt &expr) { PRECONDITION(expr.id() == ID_popcount); - DATA_INVARIANT(expr.operands().size() == 1, "popcount must have one operand"); - return static_cast(expr); + popcount_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// this is a parametric version of an if-expression: it returns @@ -4696,18 +4660,18 @@ inline void validate_expr(const cond_exprt &value) inline const cond_exprt &to_cond_expr(const exprt &expr) { PRECONDITION(expr.id() == ID_cond); - DATA_INVARIANT( - expr.operands().size() % 2 == 0, "cond must have even number of operands"); - return static_cast(expr); + const cond_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } /// \copydoc to_popcount_expr(const exprt &) inline cond_exprt &to_cond_expr(exprt &expr) { PRECONDITION(expr.id() == ID_cond); - DATA_INVARIANT( - expr.operands().size() % 2 != 0, "cond must have even number of operands"); - return static_cast(expr); + cond_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; } #endif // CPROVER_UTIL_STD_EXPR_H From d4dc77f4e5e7a2c84b47cea6b745ab9da7acb0ce Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 13 Feb 2019 10:31:34 +0000 Subject: [PATCH 12/12] Re-use *_exprt::check in validate_expr and to_*exprt Prefer code re-use over duplicated (and possibly inconsistent) implementations. --- src/util/std_expr.h | 22 +++++++--------------- 1 file changed, 7 insertions(+), 15 deletions(-) diff --git a/src/util/std_expr.h b/src/util/std_expr.h index bc2968dd93c..803569e6f98 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -778,7 +778,7 @@ inline bool can_cast_expr(const exprt &base) inline void validate_expr(const binary_exprt &value) { - validate_operands(value, 2, "Binary expressions must have two operands"); + binary_exprt::check(value); } /// \brief Cast an exprt to a \ref binary_exprt @@ -789,18 +789,14 @@ inline void validate_expr(const binary_exprt &value) /// \return Object of type \ref binary_exprt inline const binary_exprt &to_binary_expr(const exprt &expr) { - DATA_INVARIANT( - expr.operands().size()==2, - "Binary expressions must have two operands"); + binary_exprt::check(expr); return static_cast(expr); } /// \copydoc to_binary_expr(const exprt &) inline binary_exprt &to_binary_expr(exprt &expr) { - DATA_INVARIANT( - expr.operands().size()==2, - "Binary expressions must have two operands"); + binary_exprt::check(expr); return static_cast(expr); } @@ -921,7 +917,7 @@ inline bool can_cast_expr(const exprt &base) inline void validate_expr(const binary_relation_exprt &value) { - validate_operands(value, 2, "Binary relations must have two operands"); + binary_relation_exprt::check(value); } /// \brief Cast an exprt to a \ref binary_relation_exprt @@ -932,18 +928,14 @@ inline void validate_expr(const binary_relation_exprt &value) /// \return Object of type \ref binary_relation_exprt inline const binary_relation_exprt &to_binary_relation_expr(const exprt &expr) { - DATA_INVARIANT( - expr.operands().size()==2, - "Binary relations must have two operands"); + binary_relation_exprt::check(expr); return static_cast(expr); } /// \copydoc to_binary_relation_expr(const exprt &) inline binary_relation_exprt &to_binary_relation_expr(exprt &expr) { - DATA_INVARIANT( - expr.operands().size()==2, - "Binary relations must have two operands"); + binary_relation_exprt::check(expr); return static_cast(expr); } @@ -1457,7 +1449,7 @@ inline bool can_cast_expr(const exprt &base) inline void validate_expr(const equal_exprt &value) { - validate_operands(value, 2, "Equality must have two operands"); + equal_exprt::check(value); } /// \brief Cast an exprt to an \ref equal_exprt