From a18c48129b2bcfc9a3b217b8c7be57ba714aec29 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 6 Jan 2024 09:10:59 -0800 Subject: [PATCH 1/3] add unary_exprt::check(expr) This adds unary_exprt::check(expr), which checks that the expression is indeed unary. This follows the same pattern as binary_exprt::check and ternary_exprt::check. --- src/util/std_expr.h | 130 +++++++++++++++++++++----------------------- 1 file changed, 63 insertions(+), 67 deletions(-) diff --git a/src/util/std_expr.h b/src/util/std_expr.h index 45850e1cc63..d21596befa1 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -323,6 +323,24 @@ class unary_exprt : public expr_protectedt { } + static void check( + const exprt &expr, + const validation_modet vm = validation_modet::INVARIANT) + { + DATA_CHECK( + vm, + expr.operands().size() == 1, + "unary expression must have one operand"); + } + + static void validate( + const exprt &expr, + const namespacet &, + const validation_modet vm = validation_modet::INVARIANT) + { + check(expr, vm); + } + const exprt &op() const { return op0(); @@ -349,7 +367,7 @@ inline bool can_cast_expr(const exprt &base) inline void validate_expr(const unary_exprt &value) { - validate_operands(value, 1, "Unary expressions must have one operand"); + unary_exprt::check(value); } /// \brief Cast an exprt to a \ref unary_exprt @@ -360,17 +378,15 @@ 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) { - const unary_exprt &ret = static_cast(expr); - validate_expr(ret); - return ret; + unary_exprt::check(expr); + return static_cast(expr); } /// \copydoc to_unary_expr(const exprt &) inline unary_exprt &to_unary_expr(exprt &expr) { - unary_exprt &ret = static_cast(expr); - validate_expr(ret); - return ret; + unary_exprt::check(expr); + return static_cast(expr); } @@ -403,18 +419,16 @@ inline void validate_expr(const abs_exprt &value) inline const abs_exprt &to_abs_expr(const exprt &expr) { PRECONDITION(expr.id()==ID_abs); - const abs_exprt &ret = static_cast(expr); - validate_expr(ret); - return ret; + abs_exprt::check(expr); + return static_cast(expr); } /// \copydoc to_abs_expr(const exprt &) inline abs_exprt &to_abs_expr(exprt &expr) { PRECONDITION(expr.id()==ID_abs); - abs_exprt &ret = static_cast(expr); - validate_expr(ret); - return ret; + abs_exprt::check(expr); + return static_cast(expr); } @@ -453,18 +467,16 @@ 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); - const unary_minus_exprt &ret = static_cast(expr); - validate_expr(ret); - return ret; + unary_minus_exprt::check(expr); + return static_cast(expr); } /// \copydoc to_unary_minus_expr(const exprt &) inline unary_minus_exprt &to_unary_minus_expr(exprt &expr) { PRECONDITION(expr.id()==ID_unary_minus); - unary_minus_exprt &ret = static_cast(expr); - validate_expr(ret); - return ret; + unary_minus_exprt::check(expr); + return static_cast(expr); } /// \brief The unary plus expression @@ -497,18 +509,16 @@ 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); - const unary_plus_exprt &ret = static_cast(expr); - validate_expr(ret); - return ret; + unary_plus_exprt::check(expr); + return static_cast(expr); } /// \copydoc to_unary_minus_expr(const exprt &) inline unary_plus_exprt &to_unary_plus_expr(exprt &expr) { PRECONDITION(expr.id() == ID_unary_plus); - unary_plus_exprt &ret = static_cast(expr); - validate_expr(ret); - return ret; + unary_plus_exprt::check(expr); + return static_cast(expr); } /// \brief A base class for expressions that are predicates, @@ -564,18 +574,16 @@ inline void validate_expr(const sign_exprt &expr) inline const sign_exprt &to_sign_expr(const exprt &expr) { PRECONDITION(expr.id() == ID_sign); - const sign_exprt &ret = static_cast(expr); - validate_expr(ret); - return ret; + sign_exprt::check(expr); + return static_cast(expr); } /// \copydoc to_sign_expr(const exprt &) inline sign_exprt &to_sign_expr(exprt &expr) { PRECONDITION(expr.id() == ID_sign); - sign_exprt &ret = static_cast(expr); - validate_expr(ret); - return ret; + sign_exprt::check(expr); + return static_cast(expr); } /// \brief A base class for binary expressions @@ -1543,18 +1551,16 @@ 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); - const array_of_exprt &ret = static_cast(expr); - validate_expr(ret); - return ret; + array_of_exprt::check(expr); + return static_cast(expr); } /// \copydoc to_array_of_expr(const exprt &) inline array_of_exprt &to_array_of_expr(exprt &expr) { PRECONDITION(expr.id()==ID_array_of); - array_of_exprt &ret = static_cast(expr); - validate_expr(ret); - return ret; + array_of_exprt::check(expr); + return static_cast(expr); } @@ -1754,18 +1760,16 @@ inline void validate_expr(const union_exprt &value) inline const union_exprt &to_union_expr(const exprt &expr) { PRECONDITION(expr.id()==ID_union); - const union_exprt &ret = static_cast(expr); - validate_expr(ret); - return ret; + union_exprt::check(expr); + return static_cast(expr); } /// \copydoc to_union_expr(const exprt &) inline union_exprt &to_union_expr(exprt &expr) { PRECONDITION(expr.id()==ID_union); - union_exprt &ret = static_cast(expr); - validate_expr(ret); - return ret; + union_exprt::check(expr); + return static_cast(expr); } /// \brief Union constructor to support unions without any member (a GCC/Clang @@ -1952,18 +1956,16 @@ 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); - const complex_real_exprt &ret = static_cast(expr); - validate_expr(ret); - return ret; + complex_real_exprt::check(expr); + return static_cast(expr); } /// \copydoc to_complex_real_expr(const exprt &) inline complex_real_exprt &to_complex_real_expr(exprt &expr) { PRECONDITION(expr.id() == ID_complex_real); - complex_real_exprt &ret = static_cast(expr); - validate_expr(ret); - return ret; + complex_real_exprt::check(expr); + return static_cast(expr); } /// \brief Imaginary part of the expression describing a complex number. @@ -2051,18 +2053,16 @@ inline void validate_expr(const typecast_exprt &value) inline const typecast_exprt &to_typecast_expr(const exprt &expr) { PRECONDITION(expr.id()==ID_typecast); - const typecast_exprt &ret = static_cast(expr); - validate_expr(ret); - return ret; + typecast_exprt::check(expr); + return static_cast(expr); } /// \copydoc to_typecast_expr(const exprt &) inline typecast_exprt &to_typecast_expr(exprt &expr) { PRECONDITION(expr.id()==ID_typecast); - typecast_exprt &ret = static_cast(expr); - validate_expr(ret); - return ret; + typecast_exprt::check(expr); + return static_cast(expr); } @@ -2303,18 +2303,16 @@ inline void validate_expr(const not_exprt &value) inline const not_exprt &to_not_expr(const exprt &expr) { PRECONDITION(expr.id()==ID_not); - const not_exprt &ret = static_cast(expr); - validate_expr(ret); - return ret; + not_exprt::check(expr); + return static_cast(expr); } /// \copydoc to_not_expr(const exprt &) inline not_exprt &to_not_expr(exprt &expr) { PRECONDITION(expr.id()==ID_not); - not_exprt &ret = static_cast(expr); - validate_expr(ret); - return ret; + not_exprt::check(expr); + return static_cast(expr); } @@ -2886,18 +2884,16 @@ inline void validate_expr(const member_exprt &value) inline const member_exprt &to_member_expr(const exprt &expr) { PRECONDITION(expr.id()==ID_member); - const member_exprt &ret = static_cast(expr); - validate_expr(ret); - return ret; + member_exprt::check(expr); + return static_cast(expr); } /// \copydoc to_member_expr(const exprt &) inline member_exprt &to_member_expr(exprt &expr) { PRECONDITION(expr.id()==ID_member); - member_exprt &ret = static_cast(expr); - validate_expr(ret); - return ret; + member_exprt::check(expr); + return static_cast(expr); } From 9002f8e04541456fa5cd6d2cc88c05e64a21aaee Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 6 Jan 2024 09:46:06 -0800 Subject: [PATCH 2/3] fix a mis-encoding in three tests Three wrongly hand-crafted bit-vector constants are fixed. Bit-vector constants are hex, and must not use leading zeros. --- regression/symtab2gb/multiple_symtabs/entry_point.json_symtab | 2 +- regression/symtab2gb/single_symtab/entry_point.json_symtab | 2 +- unit/solvers/smt2_incremental/encoding/struct_encoding.cpp | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/regression/symtab2gb/multiple_symtabs/entry_point.json_symtab b/regression/symtab2gb/multiple_symtabs/entry_point.json_symtab index a2583ff57eb..1514e1470d1 100644 --- a/regression/symtab2gb/multiple_symtabs/entry_point.json_symtab +++ b/regression/symtab2gb/multiple_symtabs/entry_point.json_symtab @@ -1000,7 +1000,7 @@ } }, "value": { - "id": "00000000000000000000000000000000", + "id": "0", "sub": [ ], "namedSub": { diff --git a/regression/symtab2gb/single_symtab/entry_point.json_symtab b/regression/symtab2gb/single_symtab/entry_point.json_symtab index 8276db2cdf0..00e8c7fcbb2 100644 --- a/regression/symtab2gb/single_symtab/entry_point.json_symtab +++ b/regression/symtab2gb/single_symtab/entry_point.json_symtab @@ -809,7 +809,7 @@ } }, "value": { - "id": "00000000000000000000000000000000", + "id": "0", "sub": [ ], "namedSub": { diff --git a/unit/solvers/smt2_incremental/encoding/struct_encoding.cpp b/unit/solvers/smt2_incremental/encoding/struct_encoding.cpp index 5123eae8737..22924801927 100644 --- a/unit/solvers/smt2_incremental/encoding/struct_encoding.cpp +++ b/unit/solvers/smt2_incremental/encoding/struct_encoding.cpp @@ -414,7 +414,7 @@ TEST_CASE("decoding into struct expressions.", "[core][smt2_incremental]") from_integer(2, unsignedbv_typet{16}), from_integer(1, signedbv_typet{24})}, struct_tag}; - const exprt encoded = constant_exprt{"000000030002000001", bv_typet{72}}; + const exprt encoded = constant_exprt{"30002000001", bv_typet{72}}; REQUIRE(test.struct_encoding.decode(encoded, struct_tag) == expected); } From 550251bf6b972730fec28abcb31c0c8e35ed756a Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 6 Jan 2024 09:16:08 -0800 Subject: [PATCH 3/3] add nullary_exprt::check(expr) This adds nullary_exprt::check(expr), which checks that the expression is indeed nullary. This follows the same pattern as binary_exprt::check and ternary_exprt::check. --- src/util/std_expr.cpp | 17 +++++++------ src/util/std_expr.h | 55 ++++++++++++++++++++++++++----------------- 2 files changed, 42 insertions(+), 30 deletions(-) diff --git a/src/util/std_expr.cpp b/src/util/std_expr.cpp index 9eda7364a8f..3b95e3e96b9 100644 --- a/src/util/std_expr.cpp +++ b/src/util/std_expr.cpp @@ -23,28 +23,27 @@ bool constant_exprt::value_is_zero_string() const void constant_exprt::check(const exprt &expr, const validation_modet vm) { - DATA_CHECK( - vm, !expr.has_operands(), "constant expression must not have operands"); + nullary_exprt::check(expr, vm); + + const auto value = expr.get(ID_value); DATA_CHECK( vm, - !can_cast_type(expr.type()) || - !id2string(to_constant_expr(expr).get_value()).empty(), + !can_cast_type(expr.type()) || !value.empty(), "bitvector constant must have a non-empty value"); DATA_CHECK( vm, !can_cast_type(expr.type()) || can_cast_type(expr.type()) || - id2string(to_constant_expr(expr).get_value()) - .find_first_not_of("0123456789ABCDEF") == std::string::npos, + id2string(value).find_first_not_of("0123456789ABCDEF") == + std::string::npos, "negative bitvector constant must use two's complement"); DATA_CHECK( vm, - !can_cast_type(expr.type()) || - to_constant_expr(expr).get_value() == ID_0 || - id2string(to_constant_expr(expr).get_value())[0] != '0', + !can_cast_type(expr.type()) || value == ID_0 || + id2string(value)[0] != '0', "bitvector constant must not have leading zeros"); } diff --git a/src/util/std_expr.h b/src/util/std_expr.h index d21596befa1..3445073c17c 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -26,6 +26,24 @@ class nullary_exprt : public expr_protectedt { } + static void check( + const exprt &expr, + const validation_modet vm = validation_modet::INVARIANT) + { + DATA_CHECK( + vm, + expr.operands().size() == 0, + "nullary expression must not have operands"); + } + + static void validate( + const exprt &expr, + const namespacet &, + const validation_modet vm = validation_modet::INVARIANT) + { + check(expr, vm); + } + /// remove all operand methods operandst &operands() = delete; const operandst &operands() const = delete; @@ -293,19 +311,16 @@ 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); - const nondet_symbol_exprt &ret = - static_cast(expr); - validate_expr(ret); - return ret; + nondet_symbol_exprt::check(expr); + return static_cast(expr); } /// \copydoc to_nondet_symbol_expr(const exprt &) inline nondet_symbol_exprt &to_nondet_symbol_expr(exprt &expr) { PRECONDITION(expr.id()==ID_symbol); - nondet_symbol_exprt &ret = static_cast(expr); - validate_expr(ret); - return ret; + nondet_symbol_exprt::check(expr); + return static_cast(expr); } @@ -1804,18 +1819,16 @@ inline void validate_expr(const empty_union_exprt &value) inline const empty_union_exprt &to_empty_union_expr(const exprt &expr) { PRECONDITION(expr.id() == ID_empty_union); - const empty_union_exprt &ret = static_cast(expr); - validate_expr(ret); - return ret; + empty_union_exprt::check(expr); + return static_cast(expr); } /// \copydoc to_empty_union_expr(const exprt &) inline empty_union_exprt &to_empty_union_expr(exprt &expr) { PRECONDITION(expr.id() == ID_empty_union); - empty_union_exprt &ret = static_cast(expr); - validate_expr(ret); - return ret; + empty_union_exprt::check(expr); + return static_cast(expr); } /// \brief Struct constructor from list of elements @@ -2921,16 +2934,16 @@ inline bool can_cast_expr(const exprt &base) inline const type_exprt &to_type_expr(const exprt &expr) { PRECONDITION(can_cast_expr(expr)); - const type_exprt &ret = static_cast(expr); - return ret; + type_exprt::check(expr); + return static_cast(expr); } /// \copydoc to_type_expr(const exprt &) inline type_exprt &to_type_expr(exprt &expr) { PRECONDITION(can_cast_expr(expr)); - type_exprt &ret = static_cast(expr); - return ret; + type_exprt::check(expr); + return static_cast(expr); } /// \brief A constant literal expression @@ -2988,6 +3001,7 @@ inline void validate_expr(const constant_exprt &value) inline const constant_exprt &to_constant_expr(const exprt &expr) { PRECONDITION(expr.is_constant()); + constant_exprt::check(expr); return static_cast(expr); } @@ -2995,6 +3009,7 @@ inline const constant_exprt &to_constant_expr(const exprt &expr) inline constant_exprt &to_constant_expr(exprt &expr) { PRECONDITION(expr.is_constant()); + constant_exprt::check(expr); return static_cast(expr); } @@ -3534,10 +3549,8 @@ inline const class_method_descriptor_exprt & to_class_method_descriptor_expr(const exprt &expr) { PRECONDITION(expr.id() == ID_virtual_function); - const class_method_descriptor_exprt &ret = - static_cast(expr); - validate_expr(ret); - return ret; + class_method_descriptor_exprt::check(expr); + return static_cast(expr); } template <>