From 18583323ea436b042db137442371136a2a83d047 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Wed, 20 Sep 2023 20:26:22 +0100 Subject: [PATCH 1/6] Add nondet_padding expression This data structure will be used to allow encoding/lowering passes to insert padding bitvectors with non deteriministic values. Unlike the SAT decision procedures, generating an SMT formula for nondet padding will require a corresponding parameter-less function to be defined. This placeholder expression is intended to be inserted in lowering passes and then substituted at the point of term generation. Note that it doesn't quite make sense to use symbols for this as the decision procedure doesn't have mutable symbol table access and adding an extra decision procedure symbol table would have other complications. --- .../encoding/nondet_padding.h | 41 ++++++++++++++++++ unit/Makefile | 1 + .../encoding/nondet_padding.cpp | 43 +++++++++++++++++++ 3 files changed, 85 insertions(+) create mode 100644 src/solvers/smt2_incremental/encoding/nondet_padding.h create mode 100644 unit/solvers/smt2_incremental/encoding/nondet_padding.cpp diff --git a/src/solvers/smt2_incremental/encoding/nondet_padding.h b/src/solvers/smt2_incremental/encoding/nondet_padding.h new file mode 100644 index 00000000000..5610f75fb2c --- /dev/null +++ b/src/solvers/smt2_incremental/encoding/nondet_padding.h @@ -0,0 +1,41 @@ +// Author: Diffblue Ltd. + +/// \file +/// Expressions for use in incremental SMT2 decision procedure + +#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_ENCODING_NONDET_PADDING_H +#define CPROVER_SOLVERS_SMT2_INCREMENTAL_ENCODING_NONDET_PADDING_H + +#include +#include +#include + +class nondet_padding_exprt; +void validate_expr(const nondet_padding_exprt &padding); + +const irep_idt ID_nondet_padding = "nondet_padding"; + +class nondet_padding_exprt : public expr_protectedt +{ +public: + explicit nondet_padding_exprt(typet type) + : expr_protectedt{ID_nondet_padding, std::move(type)} + { + validate_expr(*this); + } +}; + +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_nondet_padding; +} + +inline void validate_expr(const nondet_padding_exprt &padding) +{ + INVARIANT( + can_cast_type(padding.type()), + "Nondet padding is expected to pad a bit vector type."); +} + +#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_ENCODING_NONDET_PADDING_H diff --git a/unit/Makefile b/unit/Makefile index 7d2bc4360b0..34609e728f9 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -117,6 +117,7 @@ SRC += analyses/ai/ai.cpp \ solvers/smt2_incremental/smt_to_smt2_string.cpp \ solvers/smt2_incremental/encoding/struct_encoding.cpp \ solvers/smt2_incremental/encoding/enum_encoding.cpp \ + solvers/smt2_incremental/encoding/nondet_padding.cpp \ solvers/smt2_incremental/theories/smt_array_theory.cpp \ solvers/smt2_incremental/theories/smt_bit_vector_theory.cpp \ solvers/smt2_incremental/theories/smt_core_theory.cpp \ diff --git a/unit/solvers/smt2_incremental/encoding/nondet_padding.cpp b/unit/solvers/smt2_incremental/encoding/nondet_padding.cpp new file mode 100644 index 00000000000..fdb5b953c2e --- /dev/null +++ b/unit/solvers/smt2_incremental/encoding/nondet_padding.cpp @@ -0,0 +1,43 @@ +// Author: Diffblue Ltd. + +#include +#include + +#include +#include +#include + +TEST_CASE("Nondet padding expression", "[core][smt2_incremental]") +{ + const bv_typet type{8}; + const exprt padding = nondet_padding_exprt{type}; + SECTION("Valid usage") + { + REQUIRE(padding.type() == type); + REQUIRE(nullptr != expr_try_dynamic_cast(padding)); + } + const auto type_error = invariant_failure_containing( + "Nondet padding is expected to pad a bit vector type."); + SECTION("Failed downcasts") + { + const exprt not_padding = symbol_exprt{"foo", empty_typet{}}; + REQUIRE( + nullptr == expr_try_dynamic_cast(not_padding)); + const exprt wrong_type = [&]() { + exprt padding = nondet_padding_exprt{type}; + padding.type() = empty_typet{}; + return padding; + }(); + cbmc_invariants_should_throwt invariants_throw; + CHECK_THROWS_MATCHES( + expr_checked_cast(wrong_type), + invariant_failedt, + type_error); + } + SECTION("Construction with incorrect type") + { + cbmc_invariants_should_throwt invariants_throw; + CHECK_THROWS_MATCHES( + nondet_padding_exprt{empty_typet{}}, invariant_failedt, type_error); + } +} From bf987e4ef3a75f70d6066871218209dbbe2878b2 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Thu, 28 Sep 2023 13:41:41 +0100 Subject: [PATCH 2/6] Move `ID_nondet_padding` inside the scope of class As requested in code review. --- src/solvers/Makefile | 1 + src/solvers/smt2_incremental/encoding/nondet_padding.cpp | 5 +++++ src/solvers/smt2_incremental/encoding/nondet_padding.h | 6 +++--- 3 files changed, 9 insertions(+), 3 deletions(-) create mode 100644 src/solvers/smt2_incremental/encoding/nondet_padding.cpp diff --git a/src/solvers/Makefile b/src/solvers/Makefile index 452cf38febf..64f606312af 100644 --- a/src/solvers/Makefile +++ b/src/solvers/Makefile @@ -211,6 +211,7 @@ SRC = $(BOOLEFORCE_SRC) \ smt2_incremental/smt2_incremental_decision_procedure.cpp \ smt2_incremental/encoding/struct_encoding.cpp \ smt2_incremental/encoding/enum_encoding.cpp \ + smt2_incremental/encoding/nondet_padding.cpp \ smt2_incremental/theories/smt_array_theory.cpp \ smt2_incremental/theories/smt_bit_vector_theory.cpp \ smt2_incremental/theories/smt_core_theory.cpp \ diff --git a/src/solvers/smt2_incremental/encoding/nondet_padding.cpp b/src/solvers/smt2_incremental/encoding/nondet_padding.cpp new file mode 100644 index 00000000000..e19b09cbc91 --- /dev/null +++ b/src/solvers/smt2_incremental/encoding/nondet_padding.cpp @@ -0,0 +1,5 @@ +// Author: Diffblue Ltd. + +#include "nondet_padding.h" + +const irep_idt nondet_padding_exprt::ID_nondet_padding = "nondet_padding"; diff --git a/src/solvers/smt2_incremental/encoding/nondet_padding.h b/src/solvers/smt2_incremental/encoding/nondet_padding.h index 5610f75fb2c..c7009d218a2 100644 --- a/src/solvers/smt2_incremental/encoding/nondet_padding.h +++ b/src/solvers/smt2_incremental/encoding/nondet_padding.h @@ -13,11 +13,11 @@ class nondet_padding_exprt; void validate_expr(const nondet_padding_exprt &padding); -const irep_idt ID_nondet_padding = "nondet_padding"; - class nondet_padding_exprt : public expr_protectedt { public: + static const irep_idt ID_nondet_padding; + explicit nondet_padding_exprt(typet type) : expr_protectedt{ID_nondet_padding, std::move(type)} { @@ -28,7 +28,7 @@ class nondet_padding_exprt : public expr_protectedt template <> inline bool can_cast_expr(const exprt &base) { - return base.id() == ID_nondet_padding; + return base.id() == nondet_padding_exprt::ID_nondet_padding; } inline void validate_expr(const nondet_padding_exprt &padding) From 607aec2e256256d9b0573386150d488f28240b15 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Thu, 28 Sep 2023 13:48:27 +0100 Subject: [PATCH 3/6] Document `nondet_padding_exprt` class --- src/solvers/smt2_incremental/encoding/nondet_padding.h | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/solvers/smt2_incremental/encoding/nondet_padding.h b/src/solvers/smt2_incremental/encoding/nondet_padding.h index c7009d218a2..e5155a3e8c3 100644 --- a/src/solvers/smt2_incremental/encoding/nondet_padding.h +++ b/src/solvers/smt2_incremental/encoding/nondet_padding.h @@ -13,6 +13,10 @@ class nondet_padding_exprt; void validate_expr(const nondet_padding_exprt &padding); +/// This expression serves as a placeholder for the bits which have non +/// deterministic value in a larger bit vector. It is inserted in contexts where +/// a subset of the bits are assigned to an expression and the remainder are +/// left unspecified. class nondet_padding_exprt : public expr_protectedt { public: From d070507f7151ceb8cfb7eb3bcba9addbbb6ada45 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Fri, 22 Sep 2023 14:26:44 +0100 Subject: [PATCH 4/6] Add padding instantiation to decision procedure --- .../smt2_incremental_decision_procedure.cpp | 21 ++++++++++++++-- .../smt2_incremental_decision_procedure.h | 7 +++++- .../smt2_incremental_decision_procedure.cpp | 24 +++++++++++++++++++ 3 files changed, 49 insertions(+), 3 deletions(-) diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp index a2932fc0c1f..6bc254fde8c 100644 --- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp +++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp @@ -18,6 +18,7 @@ #include #include #include +#include #include #include #include @@ -364,12 +365,28 @@ void smt2_incremental_decision_proceduret::define_index_identifiers( }); } +exprt smt2_incremental_decision_proceduret::substitute_defined_padding( + exprt root_expr) +{ + root_expr.visit_pre([&](exprt &node) { + if(const auto pad = expr_try_dynamic_cast(node)) + { + const auto instance = "padding_" + std::to_string(padding_sequence()); + const auto term = + smt_identifier_termt{instance, convert_type_to_smt_sort(pad->type())}; + solver_process->send(smt_declare_function_commandt{term, {}}); + node = symbol_exprt{instance, node.type()}; + } + }); + return root_expr; +} + smt_termt smt2_incremental_decision_proceduret::convert_expr_to_smt(const exprt &expr) { define_index_identifiers(expr); - const exprt substituted = - substitute_identifiers(expr, expression_identifiers); + const exprt substituted = substitute_defined_padding( + substitute_identifiers(expr, expression_identifiers)); track_expression_objects(substituted, ns, object_map); associate_pointer_sizes( substituted, diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h index 7dcc0278e95..01ad03ffea0 100644 --- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h +++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h @@ -102,6 +102,11 @@ class smt2_incremental_decision_proceduret final /// \note This function is non-const because it mutates the object_map. smt_termt convert_expr_to_smt(const exprt &expr); void define_index_identifiers(const exprt &expr); + /// In the case where lowering passes insert instances of the anonymous + /// `nondet_padding_exprt`, these need functions declaring for each instance. + /// These instances are then substituted for the function identifier in order + /// to free the solver to choose a non-det value. + exprt substitute_defined_padding(exprt expr); /// Sends the solver the definitions of the object sizes and dynamic memory /// statuses. void define_object_properties(); @@ -135,7 +140,7 @@ class smt2_incremental_decision_proceduret final { return next_id++; } - } handle_sequence, array_sequence, index_sequence; + } handle_sequence, array_sequence, index_sequence, padding_sequence; /// When the `handle(exprt)` member function is called, the decision procedure /// commands the SMT solver to define a new function corresponding to the /// given expression. The mapping of the expressions to the function diff --git a/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp index b9e961de810..b9122200d4d 100644 --- a/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp +++ b/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp @@ -1,6 +1,7 @@ // Author: Diffblue Ltd. #include +#include #include #include #include @@ -13,6 +14,7 @@ #include #include #include +#include #include #include #include @@ -268,6 +270,28 @@ TEST_CASE( smt_identifier_termt{"third_comparison", smt_bool_sortt{}})}, smt_assert_commandt{comparison_conjunction_term}}); } + SECTION("Set with nondet_padding") + { + const exprt to_set = equal_exprt{ + concatenation_exprt{ + {nondet_padding_exprt{bv_typet{8}}, from_integer(42, bv_typet{8})}, + bv_typet{16}}, + from_integer(42, bv_typet{16})}; + test.sent_commands.clear(); + test.procedure.set_to(to_set, true); + // (declare-fun padding_0 () (_ BitVec 8)) + // (assert (= (concat padding_0 (_ bv42 8)) (_ bv42 16))) + const auto expected_padding_term = + smt_identifier_termt{"padding_0", smt_bit_vector_sortt{8}}; + REQUIRE( + test.sent_commands == + std::vector{ + smt_declare_function_commandt{expected_padding_term, {}}, + smt_assert_commandt{smt_core_theoryt::equal( + smt_bit_vector_theoryt::concat( + expected_padding_term, smt_bit_vector_constant_termt{42, 8}), + smt_bit_vector_constant_termt{42, 16})}}); + } SECTION("Handle of value-less symbol.") { const symbolt foo = make_test_symbol("foo", bool_typet{}); From f957a80cfb4e070b3860670a7d9d5fccf7d8b970 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Wed, 20 Sep 2023 13:04:52 +0100 Subject: [PATCH 5/6] Add `union_exprt` encoding --- .../encoding/module_dependencies.txt | 3 +- .../encoding/struct_encoding.cpp | 19 ++++++++++ .../encoding/struct_encoding.cpp | 37 +++++++++++++++++++ 3 files changed, 58 insertions(+), 1 deletion(-) diff --git a/src/solvers/smt2_incremental/encoding/module_dependencies.txt b/src/solvers/smt2_incremental/encoding/module_dependencies.txt index 46217848995..03f2e726f1e 100644 --- a/src/solvers/smt2_incremental/encoding/module_dependencies.txt +++ b/src/solvers/smt2_incremental/encoding/module_dependencies.txt @@ -1 +1,2 @@ -util \ No newline at end of file +solvers/smt2_incremental/encoding +util diff --git a/src/solvers/smt2_incremental/encoding/struct_encoding.cpp b/src/solvers/smt2_incremental/encoding/struct_encoding.cpp index 32401ab0547..b761a00fc19 100644 --- a/src/solvers/smt2_incremental/encoding/struct_encoding.cpp +++ b/src/solvers/smt2_incremental/encoding/struct_encoding.cpp @@ -12,6 +12,7 @@ #include #include +#include #include #include @@ -136,6 +137,22 @@ static exprt encode(const struct_exprt &struct_expr) return concatenation_exprt{struct_expr.operands(), struct_expr.type()}; } +static exprt +encode(const union_exprt &union_expr, const boolbv_widtht &bit_width) +{ + const std::size_t union_width = bit_width(union_expr.type()); + const exprt &component = union_expr.op(); + const std::size_t component_width = bit_width(union_expr.op().type()); + if(union_width == component_width) + return typecast_exprt(component, bv_typet{union_width}); + INVARIANT( + union_width >= component_width, + "Union must be at least as wide as its component."); + return concatenation_exprt{ + {nondet_padding_exprt{bv_typet{union_width - component_width}}, component}, + bv_typet{union_width}}; +} + static std::size_t count_trailing_bit_width( const struct_typet &type, const irep_idt name, @@ -195,6 +212,8 @@ exprt struct_encodingt::encode(exprt expr) const current.type() = encode(current.type()); if(const auto struct_expr = expr_try_dynamic_cast(current)) current = ::encode(*struct_expr); + if(const auto union_expr = expr_try_dynamic_cast(current)) + current = ::encode(*union_expr, *boolbv_width); if(const auto member_expr = expr_try_dynamic_cast(current)) current = encode_member(*member_expr); for(auto &operand : current.operands()) diff --git a/unit/solvers/smt2_incremental/encoding/struct_encoding.cpp b/unit/solvers/smt2_incremental/encoding/struct_encoding.cpp index dcc502d1bc1..30b98c5ef27 100644 --- a/unit/solvers/smt2_incremental/encoding/struct_encoding.cpp +++ b/unit/solvers/smt2_incremental/encoding/struct_encoding.cpp @@ -8,6 +8,7 @@ #include #include +#include #include #include @@ -453,3 +454,39 @@ TEST_CASE( REQUIRE(test.struct_encoding.encode(struct_expr) == dozen); } } + +TEST_CASE("encoding of union expressions", "[core][smt2_incremental]") +{ + const struct_union_typet::componentst components{ + {"eggs", unsignedbv_typet{8}}, {"ham", signedbv_typet{32}}}; + const type_symbolt type_symbol{"foot", union_typet{components}, ID_C}; + auto test = struct_encoding_test_environmentt::make(); + test.symbol_table.insert(type_symbol); + const union_tag_typet union_tag{type_symbol.name}; + const symbolt union_value_symbol{"foo", union_tag, ID_C}; + test.symbol_table.insert(union_value_symbol); + const auto symbol_expr = union_value_symbol.symbol_expr(); + const auto symbol_expr_as_bv = symbol_exprt{"foo", bv_typet{32}}; + const auto dozen = from_integer(12, unsignedbv_typet{8}); + const auto partial_union = union_exprt{"eggs", dozen, union_tag}; + const auto partial_union_as_bv = concatenation_exprt{ + {nondet_padding_exprt{bv_typet{24}}, dozen}, bv_typet{32}}; + SECTION("Union typed symbol expression") + { + REQUIRE(test.struct_encoding.encode(symbol_expr) == symbol_expr_as_bv); + } + SECTION("Expression for a union from a component") + { + REQUIRE(test.struct_encoding.encode(partial_union) == partial_union_as_bv); + const auto one = from_integer(1, unsignedbv_typet{32}); + const auto full_union = union_exprt{"ham", one, union_tag}; + const auto full_union_as_bv = typecast_exprt{one, bv_typet{32}}; + REQUIRE(test.struct_encoding.encode(full_union) == full_union_as_bv); + } + SECTION("Union equality expression") + { + const auto union_equal = equal_exprt{symbol_expr, partial_union}; + const auto bv_equal = equal_exprt{symbol_expr_as_bv, partial_union_as_bv}; + REQUIRE(test.struct_encoding.encode(union_equal) == bv_equal); + } +} From c78a2f6d9d2ec2b766b0313741d50cf59b82946b Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Wed, 27 Sep 2023 20:30:08 +0100 Subject: [PATCH 6/6] Test that SMT decision procedure supports union expressions --- .../smt2_incremental_decision_procedure.cpp | 37 +++++++++++++++++++ 1 file changed, 37 insertions(+) diff --git a/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp index b9122200d4d..8426bfb34e4 100644 --- a/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp +++ b/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp @@ -844,6 +844,43 @@ TEST_CASE( REQUIRE(test.sent_commands == expected_commands); } +TEST_CASE( + "smt2_incremental_decision_proceduret union support.", + "[core][smt2_incremental]") +{ + auto test = decision_procedure_test_environmentt::make(); + // union foot{ int8_t eggs, uint32_t ham } foo; + const struct_union_typet::componentst components{ + {"eggs", unsignedbv_typet{8}}, {"ham", signedbv_typet{32}}}; + const type_symbolt type_symbol{"foot", union_typet{components}, ID_C}; + test.symbol_table.insert(type_symbol); + const union_tag_typet union_tag{type_symbol.name}; + const symbolt union_value_symbol{"foo", union_tag, ID_C}; + test.symbol_table.insert(union_value_symbol); + // assume(foo == foot{ .eggs = 12 }); + const auto symbol_expr = union_value_symbol.symbol_expr(); + const auto dozen = from_integer(12, unsignedbv_typet{8}); + const auto union_needing_padding = union_exprt{"eggs", dozen, union_tag}; + const auto equals = equal_exprt{symbol_expr, union_needing_padding}; + test.sent_commands.clear(); + test.procedure.set_to(equals, true); + + // (declare-fun foo () (_ BitVec 32)) + // (declare-fun padding_0 () (_ BitVec 24)) + // (assert (= foo (concat padding_0 (_ bv12 8)))) } + const auto foo_term = smt_identifier_termt{"foo", smt_bit_vector_sortt{32}}; + const auto padding_term = + smt_identifier_termt{"padding_0", smt_bit_vector_sortt{24}}; + const std::vector expected_commands{ + smt_declare_function_commandt{foo_term, {}}, + smt_declare_function_commandt{padding_term, {}}, + smt_assert_commandt{smt_core_theoryt::equal( + foo_term, + smt_bit_vector_theoryt::concat( + padding_term, smt_bit_vector_constant_termt{12, 8}))}}; + REQUIRE(test.sent_commands == expected_commands); +} + TEST_CASE( "smt2_incremental_decision_proceduret byte update-extract commands.", "[core][smt2_incremental]")