From f51c4ccfdd3adbe7740bd3c6bcdcb571ca080e82 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Mon, 27 Jun 2022 12:41:34 +0100 Subject: [PATCH 1/2] Add SMT2 array theory select function --- src/solvers/Makefile | 1 + .../smt2_incremental/smt_array_theory.cpp | 29 +++++++++++++++ .../smt2_incremental/smt_array_theory.h | 21 +++++++++++ unit/Makefile | 1 + .../smt2_incremental/smt_array_theory.cpp | 35 +++++++++++++++++++ 5 files changed, 87 insertions(+) create mode 100644 src/solvers/smt2_incremental/smt_array_theory.cpp create mode 100644 src/solvers/smt2_incremental/smt_array_theory.h create mode 100644 unit/solvers/smt2_incremental/smt_array_theory.cpp diff --git a/src/solvers/Makefile b/src/solvers/Makefile index 22d82c59e5b..85800d1473c 100644 --- a/src/solvers/Makefile +++ b/src/solvers/Makefile @@ -197,6 +197,7 @@ SRC = $(BOOLEFORCE_SRC) \ smt2_incremental/convert_expr_to_smt.cpp \ smt2_incremental/object_tracking.cpp \ smt2_incremental/type_size_mapping.cpp \ + smt2_incremental/smt_array_theory.cpp \ smt2_incremental/smt_bit_vector_theory.cpp \ smt2_incremental/smt_commands.cpp \ smt2_incremental/smt_core_theory.cpp \ diff --git a/src/solvers/smt2_incremental/smt_array_theory.cpp b/src/solvers/smt2_incremental/smt_array_theory.cpp new file mode 100644 index 00000000000..a2f885094c4 --- /dev/null +++ b/src/solvers/smt2_incremental/smt_array_theory.cpp @@ -0,0 +1,29 @@ +// Author: Diffblue Ltd. + +#include "smt_array_theory.h" + +const char *smt_array_theoryt::selectt::identifier() +{ + return "select"; +} + +smt_sortt smt_array_theoryt::selectt::return_sort( + const smt_termt &array, + const smt_termt &index) +{ + return array.get_sort().cast()->element_sort(); +} + +void smt_array_theoryt::selectt::validate( + const smt_termt &array, + const smt_termt &index) +{ + const auto array_sort = array.get_sort().cast(); + INVARIANT(array_sort, "\"select\" may only select from an array."); + INVARIANT( + array_sort->index_sort() == index.get_sort(), + "Sort of arrays index must match the sort of the index supplied."); +} + +const smt_function_application_termt::factoryt + smt_array_theoryt::select{}; diff --git a/src/solvers/smt2_incremental/smt_array_theory.h b/src/solvers/smt2_incremental/smt_array_theory.h new file mode 100644 index 00000000000..fe96389518e --- /dev/null +++ b/src/solvers/smt2_incremental/smt_array_theory.h @@ -0,0 +1,21 @@ +// Author: Diffblue Ltd. + +#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_ARRAY_THEORY_H +#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_ARRAY_THEORY_H + +#include + +class smt_array_theoryt +{ +public: + struct selectt final + { + static const char *identifier(); + static smt_sortt + return_sort(const smt_termt &array, const smt_termt &index); + static void validate(const smt_termt &array, const smt_termt &index); + }; + static const smt_function_application_termt::factoryt select; +}; + +#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_ARRAY_THEORY_H diff --git a/unit/Makefile b/unit/Makefile index 00dda05f264..10a80eb1e74 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -104,6 +104,7 @@ SRC += analyses/ai/ai.cpp \ solvers/smt2_incremental/convert_expr_to_smt.cpp \ solvers/smt2_incremental/object_tracking.cpp \ solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp \ + solvers/smt2_incremental/smt_array_theory.cpp \ solvers/smt2_incremental/smt_bit_vector_theory.cpp \ solvers/smt2_incremental/smt_commands.cpp \ solvers/smt2_incremental/smt_core_theory.cpp \ diff --git a/unit/solvers/smt2_incremental/smt_array_theory.cpp b/unit/solvers/smt2_incremental/smt_array_theory.cpp new file mode 100644 index 00000000000..2d3234461ae --- /dev/null +++ b/unit/solvers/smt2_incremental/smt_array_theory.cpp @@ -0,0 +1,35 @@ +// Author: Diffblue Ltd. + +#include + +#include +#include +#include + +#include "testing-utils/invariant.h" + +TEST_CASE("SMT array theory \"select\".", "[core][smt2_incremental]") +{ + const smt_identifier_termt index_term("index", smt_bit_vector_sortt(64)); + const smt_sortt value_sort(smt_bit_vector_sortt(32)); + const smt_identifier_termt array_term( + "array", smt_array_sortt(index_term.get_sort(), value_sort)); + const smt_function_application_termt select = + smt_array_theoryt::select(array_term, index_term); + CHECK(select.get_sort() == value_sort); + CHECK(select.function_identifier().identifier() == "select"); + REQUIRE(select.arguments().size() == 2); + CHECK(select.arguments()[0].get() == array_term); + CHECK(select.arguments()[1].get() == index_term); + cbmc_invariants_should_throwt invariants_throw; + const smt_bit_vector_constant_termt two{2, 8}; + REQUIRE_THROWS_MATCHES( + smt_array_theoryt::select(two, index_term), + invariant_failedt, + invariant_failure_containing("\"select\" may only select from an array.")); + REQUIRE_THROWS_MATCHES( + smt_array_theoryt::select(array_term, two), + invariant_failedt, + invariant_failure_containing( + "Sort of arrays index must match the sort of the index supplied.")); +} \ No newline at end of file From 257bfc4633d3c5b43ab3dfb9e43edfff0858a58e Mon Sep 17 00:00:00 2001 From: Enrico Steffinlongo Date: Tue, 28 Jun 2022 12:32:30 +0100 Subject: [PATCH 2/2] Add SMT2 array theory store function --- .../smt2_incremental/smt_array_theory.cpp | 29 ++++++++++++++++ .../smt2_incremental/smt_array_theory.h | 14 ++++++++ .../smt2_incremental/smt_array_theory.cpp | 34 ++++++++++++++++++- 3 files changed, 76 insertions(+), 1 deletion(-) diff --git a/src/solvers/smt2_incremental/smt_array_theory.cpp b/src/solvers/smt2_incremental/smt_array_theory.cpp index a2f885094c4..94cb6befb3c 100644 --- a/src/solvers/smt2_incremental/smt_array_theory.cpp +++ b/src/solvers/smt2_incremental/smt_array_theory.cpp @@ -27,3 +27,32 @@ void smt_array_theoryt::selectt::validate( const smt_function_application_termt::factoryt smt_array_theoryt::select{}; + +const char *smt_array_theoryt::storet::identifier() +{ + return "store"; +} +smt_sortt smt_array_theoryt::storet::return_sort( + const smt_termt &array, + const smt_termt &index, + const smt_termt &value) +{ + return array.get_sort(); +} +void smt_array_theoryt::storet::validate( + const smt_termt &array, + const smt_termt &index, + const smt_termt &value) +{ + const auto array_sort = array.get_sort().cast(); + INVARIANT(array_sort, "\"store\" may only update an array."); + INVARIANT( + array_sort->index_sort() == index.get_sort(), + "Sort of arrays index must match the sort of the index supplied."); + INVARIANT( + array_sort->element_sort() == value.get_sort(), + "Sort of arrays value must match the sort of the value supplied."); +} + +const smt_function_application_termt::factoryt + smt_array_theoryt::store{}; diff --git a/src/solvers/smt2_incremental/smt_array_theory.h b/src/solvers/smt2_incremental/smt_array_theory.h index fe96389518e..d56f049d745 100644 --- a/src/solvers/smt2_incremental/smt_array_theory.h +++ b/src/solvers/smt2_incremental/smt_array_theory.h @@ -16,6 +16,20 @@ class smt_array_theoryt static void validate(const smt_termt &array, const smt_termt &index); }; static const smt_function_application_termt::factoryt select; + + struct storet final + { + static const char *identifier(); + static smt_sortt return_sort( + const smt_termt &array, + const smt_termt &index, + const smt_termt &value); + static void validate( + const smt_termt &array, + const smt_termt &index, + const smt_termt &value); + }; + static const smt_function_application_termt::factoryt store; }; #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_ARRAY_THEORY_H diff --git a/unit/solvers/smt2_incremental/smt_array_theory.cpp b/unit/solvers/smt2_incremental/smt_array_theory.cpp index 2d3234461ae..99e427e9c3f 100644 --- a/unit/solvers/smt2_incremental/smt_array_theory.cpp +++ b/unit/solvers/smt2_incremental/smt_array_theory.cpp @@ -32,4 +32,36 @@ TEST_CASE("SMT array theory \"select\".", "[core][smt2_incremental]") invariant_failedt, invariant_failure_containing( "Sort of arrays index must match the sort of the index supplied.")); -} \ No newline at end of file +} + +TEST_CASE("SMT array theory \"store\".", "[core][smt2_incremental]") +{ + const smt_identifier_termt index_term("index", smt_bit_vector_sortt(64)); + const smt_identifier_termt value_term("value", smt_bit_vector_sortt(32)); + const smt_identifier_termt array_term( + "array", smt_array_sortt(index_term.get_sort(), value_term.get_sort())); + const smt_function_application_termt store = + smt_array_theoryt::store(array_term, index_term, value_term); + CHECK(store.get_sort() == array_term.get_sort()); + CHECK(store.function_identifier().identifier() == "store"); + REQUIRE(store.arguments().size() == 3); + CHECK(store.arguments()[0].get() == array_term); + CHECK(store.arguments()[1].get() == index_term); + CHECK(store.arguments()[2].get() == value_term); + cbmc_invariants_should_throwt invariants_throw; + const smt_bit_vector_constant_termt two{2, 8}; + REQUIRE_THROWS_MATCHES( + smt_array_theoryt::store(two, index_term, value_term), + invariant_failedt, + invariant_failure_containing("\"store\" may only update an array.")); + REQUIRE_THROWS_MATCHES( + smt_array_theoryt::store(array_term, two, value_term), + invariant_failedt, + invariant_failure_containing( + "Sort of arrays index must match the sort of the index supplied.")); + REQUIRE_THROWS_MATCHES( + smt_array_theoryt::store(array_term, index_term, two), + invariant_failedt, + invariant_failure_containing( + "Sort of arrays value must match the sort of the value supplied.")); +}