From b9c6c2727cb800075eda6801cd2c76a2b5f8d4ec Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Tue, 28 Nov 2023 18:56:25 +0000 Subject: [PATCH 1/8] Replace hand-rolled variant with `std::variant` Though there may be a (minor) memory saving here, the main benefit is the use of a standard version. This gives us the use of a C++ standard interface and avoids the need to understand and maintain our own implementation. --- .../smt2_incremental/response_or_error.h | 27 +++++-------------- 1 file changed, 7 insertions(+), 20 deletions(-) diff --git a/src/solvers/smt2_incremental/response_or_error.h b/src/solvers/smt2_incremental/response_or_error.h index 48d8eab5b66..7c9c4236ace 100644 --- a/src/solvers/smt2_incremental/response_or_error.h +++ b/src/solvers/smt2_incremental/response_or_error.h @@ -4,9 +4,9 @@ #define CPROVER_SOLVERS_SMT2_INCREMENTAL_RESPONSE_OR_ERROR_H #include -#include #include +#include #include /// Holds either a valid parsed response or response sub-tree of type \tparam @@ -16,17 +16,17 @@ template class response_or_errort final { public: - explicit response_or_errort(smtt smt) : smt{std::move(smt)} + explicit response_or_errort(smtt smt) : smt_or_messages{std::move(smt)} { } explicit response_or_errort(std::string message) - : messages{std::move(message)} + : smt_or_messages{std::vector{std::move(message)}} { } explicit response_or_errort(std::vector messages) - : messages{std::move(messages)} + : smt_or_messages{std::move(messages)} { } @@ -34,31 +34,18 @@ class response_or_errort final /// otherwise. const smtt *get_if_valid() const { - INVARIANT( - smt.has_value() == messages.empty(), - "The response_or_errort class must be in the valid state or error state, " - "exclusively."); - return smt.has_value() ? &smt.value() : nullptr; + return std::get_if(&smt_or_messages); } /// \brief Gets the error messages if the response is invalid, or returns /// nullptr otherwise. const std::vector *get_if_error() const { - INVARIANT( - smt.has_value() == messages.empty(), - "The response_or_errort class must be in the valid state or error state, " - "exclusively."); - return smt.has_value() ? nullptr : &messages; + return std::get_if>(&smt_or_messages); } private: - // The below two fields could be a single `std::variant` field, if there was - // an implementation of it available in the cbmc repository. However at the - // time of writing we are targeting C++11, `std::variant` was introduced in - // C++17 and we have no backported version. - optionalt smt; - std::vector messages; + std::variant> smt_or_messages; }; #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_RESPONSE_OR_ERROR_H From 570ef6e0991b0d102b261aed807c54398d365613 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Tue, 28 Nov 2023 19:02:32 +0000 Subject: [PATCH 2/8] Use `std::optional` for `smt_sortt::cast` --- src/solvers/smt2_incremental/ast/smt_sorts.cpp | 3 ++- src/solvers/smt2_incremental/ast/smt_sorts.h | 4 ++-- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/src/solvers/smt2_incremental/ast/smt_sorts.cpp b/src/solvers/smt2_incremental/ast/smt_sorts.cpp index ac33d75306e..589a21df8c9 100644 --- a/src/solvers/smt2_incremental/ast/smt_sorts.cpp +++ b/src/solvers/smt2_incremental/ast/smt_sorts.cpp @@ -24,7 +24,8 @@ #define SORT_ID(the_id) \ template <> \ - optionalt smt_sortt::cast() && \ + std::optional smt_sortt::cast() \ + && \ { \ if(id() == ID_smt_##the_id##_sort) \ return {std::move(*static_cast(this))}; \ diff --git a/src/solvers/smt2_incremental/ast/smt_sorts.h b/src/solvers/smt2_incremental/ast/smt_sorts.h index 307cb4a3134..f8506bea95e 100644 --- a/src/solvers/smt2_incremental/ast/smt_sorts.h +++ b/src/solvers/smt2_incremental/ast/smt_sorts.h @@ -8,8 +8,8 @@ #define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_SORTS_H #include -#include +#include #include class smt_sort_const_downcast_visitort; @@ -47,7 +47,7 @@ class smt_sortt : protected irept const sub_classt *cast() const &; template - optionalt cast() &&; + std::optional cast() &&; protected: using irept::irept; From 17752d365afb455f431048c690336a7de6f386ca Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Tue, 28 Nov 2023 19:06:20 +0000 Subject: [PATCH 3/8] Use `std::optional` in `struct_encodingt` --- src/solvers/smt2_incremental/encoding/struct_encoding.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/solvers/smt2_incremental/encoding/struct_encoding.cpp b/src/solvers/smt2_incremental/encoding/struct_encoding.cpp index 3a77517173c..592c9b9b12f 100644 --- a/src/solvers/smt2_incremental/encoding/struct_encoding.cpp +++ b/src/solvers/smt2_incremental/encoding/struct_encoding.cpp @@ -15,6 +15,7 @@ #include #include +#include #include struct_encodingt::struct_encodingt(const namespacet &ns) @@ -33,7 +34,7 @@ struct_encodingt::~struct_encodingt() = default; /// If the given \p type needs re-encoding as a bit-vector then this function /// \returns the width of the new bitvector type. The width calculation is /// delegated to \p boolbv_width. -static optionalt +static std::optional needs_width(const typet &type, const boolbv_widtht &boolbv_width) { if(const auto struct_tag = type_try_dynamic_cast(type)) @@ -222,7 +223,7 @@ exprt struct_encodingt::encode(exprt expr) const if(can_cast_type(current.type())) current = ::encode(*with_expr, ns); current.type() = encode(current.type()); - optionalt update; + std::optional update; if(const auto struct_expr = expr_try_dynamic_cast(current)) update = ::encode(*struct_expr); if(const auto union_expr = expr_try_dynamic_cast(current)) From d8c60c911e2577a33004751159a094868b9d43da Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Tue, 28 Nov 2023 19:08:35 +0000 Subject: [PATCH 4/8] Use `std::optional` in `convert_expr_to_smt` --- src/solvers/smt2_incremental/convert_expr_to_smt.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp index 2d5b38879ba..c1286bc3d7e 100644 --- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -206,7 +206,7 @@ struct sort_based_cast_to_bit_vector_convertert final const smt_termt &from_term; const typet &from_type; const bitvector_typet &to_type; - optionalt result; + std::optional result; sort_based_cast_to_bit_vector_convertert( const smt_termt &from_term, @@ -299,7 +299,7 @@ static smt_termt convert_expr_to_smt( struct sort_based_literal_convertert : public smt_sort_const_downcast_visitort { const constant_exprt &member_input; - optionalt result; + std::optional result; explicit sort_based_literal_convertert(const constant_exprt &input) : member_input{input} @@ -591,7 +591,7 @@ static smt_termt convert_relational_to_smt( binary_relation.pretty()); } -static optionalt try_relational_conversion( +static std::optional try_relational_conversion( const exprt &expr, const sub_expression_mapt &converted) { From d7b937a78b10efed0b14f3a4d5648f380bbe06b4 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Tue, 28 Nov 2023 19:11:20 +0000 Subject: [PATCH 5/8] Use `std::optional` in `smt2_incremental_decision_proceduret` --- .../smt2_incremental_decision_procedure.cpp | 14 +++++++------- .../smt2_incremental_decision_procedure.h | 10 +++++----- 2 files changed, 12 insertions(+), 12 deletions(-) diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp index f189e95130a..3b8638e8aa4 100644 --- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp +++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp @@ -44,7 +44,7 @@ static smt_responset get_response_to_command( /// Returns a message string describing the problem in the case where the /// response from the solver is an error status. Returns empty otherwise. -static optionalt +static std::optional get_problem_messages(const smt_responset &response) { if(const auto error = response.cast()) @@ -413,7 +413,7 @@ exprt smt2_incremental_decision_proceduret::handle(const exprt &expr) return expr; } -optionalt +std::optional smt2_incremental_decision_proceduret::get_identifier(const exprt &expr) const { // Lookup the non-lowered form first. @@ -437,7 +437,7 @@ smt2_incremental_decision_proceduret::get_identifier(const exprt &expr) const return {}; } -optionalt smt2_incremental_decision_proceduret::get_expr( +std::optional smt2_incremental_decision_proceduret::get_expr( const smt_termt &array, const array_typet &type) const { @@ -467,7 +467,7 @@ optionalt smt2_incremental_decision_proceduret::get_expr( return array_exprt{elements, type}; } -optionalt smt2_incremental_decision_proceduret::get_expr( +std::optional smt2_incremental_decision_proceduret::get_expr( const smt_termt &struct_term, const struct_tag_typet &type) const { @@ -478,7 +478,7 @@ optionalt smt2_incremental_decision_proceduret::get_expr( return {struct_encoding.decode(*encoded_result, type)}; } -optionalt smt2_incremental_decision_proceduret::get_expr( +std::optional smt2_incremental_decision_proceduret::get_expr( const smt_termt &union_term, const union_tag_typet &type) const { @@ -489,7 +489,7 @@ optionalt smt2_incremental_decision_proceduret::get_expr( return {struct_encoding.decode(*encoded_result, type)}; } -optionalt smt2_incremental_decision_proceduret::get_expr( +std::optional smt2_incremental_decision_proceduret::get_expr( const smt_termt &descriptor, const typet &type) const { @@ -556,7 +556,7 @@ exprt smt2_incremental_decision_proceduret::get(const exprt &expr) const log.conditional_output(log.debug(), [&](messaget::mstreamt &debug) { debug << "`get` - \n " + expr.pretty(2, 0) << messaget::eom; }); - auto descriptor = [&]() -> optionalt { + auto descriptor = [&]() -> std::optional { if(const auto index_expr = expr_try_dynamic_cast(expr)) { const auto array = get_identifier(index_expr->array()); diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h index 3aaf5b3bc70..911dae5491a 100644 --- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h +++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h @@ -56,13 +56,13 @@ class smt2_incremental_decision_proceduret final /// Gets the value of \p descriptor from the solver and returns the solver /// response expressed as an exprt of type \p type. This is an implementation /// detail of the `get(exprt)` member function. - optionalt + std::optional get_expr(const smt_termt &descriptor, const typet &type) const; - optionalt + std::optional get_expr(const smt_termt &struct_term, const struct_tag_typet &type) const; - optionalt + std::optional get_expr(const smt_termt &union_term, const union_tag_typet &type) const; - optionalt + std::optional get_expr(const smt_termt &array, const array_typet &type) const; protected: @@ -117,7 +117,7 @@ class smt2_incremental_decision_proceduret final /// possible expression forms by expressing these in terms of the remaining /// language features. exprt lower(exprt expression) const; - optionalt get_identifier(const exprt &expr) const; + std::optional get_identifier(const exprt &expr) const; /// Namespace for looking up the expressions which symbol_exprts relate to. /// This includes the symbols defined outside of the decision procedure but From 1ab6db21f5ef2e4885836cc52b5a39c1c18a6a0f Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Tue, 28 Nov 2023 19:12:55 +0000 Subject: [PATCH 6/8] Update SMT AST to refer to `std::optional` instead of `optionalt` --- src/solvers/smt2_incremental/ast/smt_commands.h | 2 +- src/solvers/smt2_incremental/ast/smt_index.h | 2 +- src/solvers/smt2_incremental/ast/smt_logics.h | 2 +- src/solvers/smt2_incremental/ast/smt_options.h | 2 +- src/solvers/smt2_incremental/ast/smt_responses.h | 4 ++-- src/solvers/smt2_incremental/ast/smt_sorts.h | 2 +- src/solvers/smt2_incremental/ast/smt_terms.h | 2 +- 7 files changed, 8 insertions(+), 8 deletions(-) diff --git a/src/solvers/smt2_incremental/ast/smt_commands.h b/src/solvers/smt2_incremental/ast/smt_commands.h index 6f3fd4b46db..cda788aec9a 100644 --- a/src/solvers/smt2_incremental/ast/smt_commands.h +++ b/src/solvers/smt2_incremental/ast/smt_commands.h @@ -15,7 +15,7 @@ class smt_commandt : protected irept { public: // smt_commandt does not support the notion of an empty / null state. Use - // optionalt instead if an empty command is required. + // std::optional instead if an empty command is required. smt_commandt() = delete; using irept::pretty; diff --git a/src/solvers/smt2_incremental/ast/smt_index.h b/src/solvers/smt2_incremental/ast/smt_index.h index 252d904feb8..533a789630f 100644 --- a/src/solvers/smt2_incremental/ast/smt_index.h +++ b/src/solvers/smt2_incremental/ast/smt_index.h @@ -14,7 +14,7 @@ class smt_indext : protected irept { public: // smt_indext does not support the notion of an empty / null state. Use - // optionalt instead if an empty index is required. + // std::optional instead if an empty index is required. smt_indext() = delete; using irept::pretty; diff --git a/src/solvers/smt2_incremental/ast/smt_logics.h b/src/solvers/smt2_incremental/ast/smt_logics.h index 9d68b469d5b..e25415f9333 100644 --- a/src/solvers/smt2_incremental/ast/smt_logics.h +++ b/src/solvers/smt2_incremental/ast/smt_logics.h @@ -11,7 +11,7 @@ class smt_logict : protected irept { public: // smt_logict does not support the notion of an empty / null state. Use - // optionalt instead if an empty logic is required. + // std::optional instead if an empty logic is required. smt_logict() = delete; using irept::pretty; diff --git a/src/solvers/smt2_incremental/ast/smt_options.h b/src/solvers/smt2_incremental/ast/smt_options.h index b65f0384d66..275efd2f3bd 100644 --- a/src/solvers/smt2_incremental/ast/smt_options.h +++ b/src/solvers/smt2_incremental/ast/smt_options.h @@ -11,7 +11,7 @@ class smt_optiont : protected irept { public: // smt_optiont does not support the notion of an empty / null state. Use - // optionalt instead if an empty option is required. + // std::optional instead if an empty option is required. smt_optiont() = delete; using irept::pretty; diff --git a/src/solvers/smt2_incremental/ast/smt_responses.h b/src/solvers/smt2_incremental/ast/smt_responses.h index 854ab474d9a..4521f788bdf 100644 --- a/src/solvers/smt2_incremental/ast/smt_responses.h +++ b/src/solvers/smt2_incremental/ast/smt_responses.h @@ -11,7 +11,7 @@ class smt_responset : protected irept { public: // smt_responset does not support the notion of an empty / null state. Use - // optionalt instead if an empty response is required. + // std::optional instead if an empty response is required. smt_responset() = delete; using irept::pretty; @@ -36,7 +36,7 @@ class smt_check_sat_response_kindt : protected irept { public: // smt_responset does not support the notion of an empty / null state. Use - // optionalt instead if an empty response is required. + // std::optional instead if an empty response is required. smt_check_sat_response_kindt() = delete; using irept::pretty; diff --git a/src/solvers/smt2_incremental/ast/smt_sorts.h b/src/solvers/smt2_incremental/ast/smt_sorts.h index f8506bea95e..4cc58a9b94d 100644 --- a/src/solvers/smt2_incremental/ast/smt_sorts.h +++ b/src/solvers/smt2_incremental/ast/smt_sorts.h @@ -18,7 +18,7 @@ class smt_sortt : protected irept { public: // smt_sortt does not support the notion of an empty / null state. Use - // optionalt instead if an empty sort is required. + // std::optional instead if an empty sort is required. smt_sortt() = delete; using irept::pretty; diff --git a/src/solvers/smt2_incremental/ast/smt_terms.h b/src/solvers/smt2_incremental/ast/smt_terms.h index eef3b3dbb0f..5354cd62d72 100644 --- a/src/solvers/smt2_incremental/ast/smt_terms.h +++ b/src/solvers/smt2_incremental/ast/smt_terms.h @@ -21,7 +21,7 @@ class smt_termt : protected irept, private smt_sortt::storert { public: // smt_termt does not support the notion of an empty / null state. Use - // optionalt instead if an empty term is required. + // std::optional instead if an empty term is required. smt_termt() = delete; using irept::pretty; From a479356d7e12464104860ca2c33ad4bd8c412517 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Tue, 28 Nov 2023 19:14:43 +0000 Subject: [PATCH 7/8] Update smt_response_validation to use `std::optional` --- .../smt2_incremental/smt_response_validation.cpp | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/solvers/smt2_incremental/smt_response_validation.cpp b/src/solvers/smt2_incremental/smt_response_validation.cpp index 36709b52aea..1f8bdb754ad 100644 --- a/src/solvers/smt2_incremental/smt_response_validation.cpp +++ b/src/solvers/smt2_incremental/smt_response_validation.cpp @@ -125,7 +125,7 @@ validate_string_literal(const irept &parse_tree) /// \note: Because this kind of response does not start with an identifying /// keyword, it will be considered that the response is intended to be a /// get-value response if it is composed of a collection of one or more pairs. -static optionalt> +static std::optional> valid_smt_error_response(const irept &parse_tree) { // Check if the parse tree looks to be an error response. @@ -162,7 +162,7 @@ static bool all_subs_are_pairs(const irept &parse_tree) /// Checks for valid bit vector constants of the form `(_ bv(value) (width))` /// for example - `(_ bv4 64)`. -static optionalt +static std::optional valid_smt_indexed_bit_vector(const irept &parse_tree) { if(parse_tree.get_sub().size() != 3) @@ -189,7 +189,7 @@ valid_smt_indexed_bit_vector(const irept &parse_tree) return smt_bit_vector_constant_termt{value, bit_width}; } -static optionalt valid_smt_bool(const irept &parse_tree) +static std::optional valid_smt_bool(const irept &parse_tree) { if(!parse_tree.get_sub().empty()) return {}; @@ -200,7 +200,7 @@ static optionalt valid_smt_bool(const irept &parse_tree) return {}; } -static optionalt valid_smt_binary(const std::string &text) +static std::optional valid_smt_binary(const std::string &text) { static const std::regex binary_format{"#b[01]+"}; if(!std::regex_match(text, binary_format)) @@ -211,7 +211,7 @@ static optionalt valid_smt_binary(const std::string &text) return {smt_bit_vector_constant_termt{value, width}}; } -static optionalt valid_smt_hex(const std::string &text) +static std::optional valid_smt_hex(const std::string &text) { static const std::regex hex_format{"#x[0-9A-Za-z]+"}; if(!std::regex_match(text, hex_format)) @@ -225,7 +225,7 @@ static optionalt valid_smt_hex(const std::string &text) return {smt_bit_vector_constant_termt{value, width}}; } -static optionalt +static std::optional valid_smt_bit_vector_constant(const irept &parse_tree) { if(const auto indexed = valid_smt_indexed_bit_vector(parse_tree)) @@ -240,7 +240,7 @@ valid_smt_bit_vector_constant(const irept &parse_tree) return {}; } -static optionalt> try_select_validation( +static std::optional> try_select_validation( const irept &parse_tree, const std::unordered_map &identifier_table) { @@ -321,7 +321,7 @@ validate_valuation_pair( /// \note: Because this kind of response does not start with an identifying /// keyword, it will be considered that the response is intended to be a /// get-value response if it is composed of a collection of one or more pairs. -static optionalt> +static std::optional> valid_smt_get_value_response( const irept &parse_tree, const std::unordered_map &identifier_table) From 062d6c67e1878119fb37f633ad377ec006c32da8 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Tue, 28 Nov 2023 19:16:01 +0000 Subject: [PATCH 8/8] Use `std::optional` in `value_expr_from_smt_factoryt` --- src/solvers/smt2_incremental/construct_value_expr_from_smt.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/solvers/smt2_incremental/construct_value_expr_from_smt.cpp b/src/solvers/smt2_incremental/construct_value_expr_from_smt.cpp index ef0379e4c57..d9d3b7a1ce0 100644 --- a/src/solvers/smt2_incremental/construct_value_expr_from_smt.cpp +++ b/src/solvers/smt2_incremental/construct_value_expr_from_smt.cpp @@ -16,7 +16,7 @@ class value_expr_from_smt_factoryt : public smt_term_const_downcast_visitort private: const typet &type_to_construct; const namespacet &ns; - optionalt result; + std::optional result; explicit value_expr_from_smt_factoryt( const typet &type_to_construct,