diff --git a/src/solvers/smt2_incremental/smt_response_validation.cpp b/src/solvers/smt2_incremental/smt_response_validation.cpp index c81026ede29..68675084203 100644 --- a/src/solvers/smt2_incremental/smt_response_validation.cpp +++ b/src/solvers/smt2_incremental/smt_response_validation.cpp @@ -22,6 +22,7 @@ #include #include "smt_array_theory.h" +#include "smt_to_smt2_string.h" #include @@ -29,40 +30,40 @@ static response_or_errort validate_term( const irept &parse_tree, const std::unordered_map &identifier_table); -// Implementation detail of `collect_messages` below. +// Implementation detail of `collect_error_messages` below. template -void collect_messages_impl( - std::vector &collected_messages, +void collect_error_messages_impl( + std::vector &collected_error_messages, argumentt &&argument) { if(const auto messages = argument.get_if_error()) { - collected_messages.insert( - collected_messages.end(), messages->cbegin(), messages->end()); + collected_error_messages.insert( + collected_error_messages.end(), messages->cbegin(), messages->end()); } } -// Implementation detail of `collect_messages` below. +// Implementation detail of `collect_error_messages` below. template -void collect_messages_impl( - std::vector &collected_messages, +void collect_error_messages_impl( + std::vector &collected_error_messages, argumentt &&argument, argumentst &&... arguments) { - collect_messages_impl(collected_messages, argument); - collect_messages_impl(collected_messages, arguments...); + collect_error_messages_impl(collected_error_messages, argument); + collect_error_messages_impl(collected_error_messages, arguments...); } -/// Builds a collection of messages composed all messages in the +/// Builds a collection of error messages composed all error messages in the /// `response_or_errort` typed arguments in \p arguments. This is a templated /// function in order to handle `response_or_errort` instances which are /// specialised differently. template -std::vector collect_messages(argumentst &&... arguments) +std::vector collect_error_messages(argumentst &&... arguments) { - std::vector collected_messages; - collect_messages_impl(collected_messages, arguments...); - return collected_messages; + std::vector collected_error_messages; + collect_error_messages_impl(collected_error_messages, arguments...); + return collected_error_messages; } /// \brief Given a class to construct and a set of arguments to its constructor @@ -85,9 +86,9 @@ template < typename... argumentst> response_or_errort validation_propagating(argumentst &&... arguments) { - const auto collected_messages = collect_messages(arguments...); - if(!collected_messages.empty()) - return response_or_errort(collected_messages); + const auto collected_error_messages = collect_error_messages(arguments...); + if(!collected_error_messages.empty()) + return response_or_errort(collected_error_messages); else { return response_or_errort{ @@ -255,9 +256,9 @@ static optionalt> try_select_validation( } const auto array = validate_term(parse_tree.get_sub()[1], identifier_table); const auto index = validate_term(parse_tree.get_sub()[2], identifier_table); - const auto messages = collect_messages(array, index); - if(!messages.empty()) - return response_or_errort{messages}; + const auto error_messages = collect_error_messages(array, index); + if(!error_messages.empty()) + return response_or_errort{error_messages}; return {smt_array_theoryt::select.validation( *array.get_if_valid(), *index.get_if_valid())}; } @@ -288,12 +289,27 @@ validate_valuation_pair( const irept &pair_parse_tree, const std::unordered_map &identifier_table) { + using resultt = response_or_errort; PRECONDITION(pair_parse_tree.get_sub().size() == 2); - const auto &descriptor = pair_parse_tree.get_sub()[0]; - const auto &value = pair_parse_tree.get_sub()[1]; - return validation_propagating( - validate_term(descriptor, identifier_table), - validate_term(value, identifier_table)); + const auto descriptor_validation = + validate_term(pair_parse_tree.get_sub()[0], identifier_table); + const auto value_validation = + validate_term(pair_parse_tree.get_sub()[1], identifier_table); + const auto error_messages = + collect_error_messages(descriptor_validation, value_validation); + if(!error_messages.empty()) + return resultt{error_messages}; + const auto &valid_descriptor = *descriptor_validation.get_if_valid(); + const auto &valid_value = *value_validation.get_if_valid(); + if(valid_descriptor.get_sort() != valid_value.get_sort()) + { + return resultt{ + "Mismatched descriptor and value sorts in - " + + print_parse_tree(pair_parse_tree) + "\nDescriptor has sort " + + smt_to_smt2_string(valid_descriptor.get_sort()) + "\nValue has sort " + + smt_to_smt2_string(valid_value.get_sort())}; + } + return resultt{{valid_descriptor, valid_value}}; } /// \returns: A response or error in the case where the parse tree appears to be diff --git a/unit/solvers/smt2_incremental/smt_response_validation.cpp b/unit/solvers/smt2_incremental/smt_response_validation.cpp index 5fe8344f6bb..cfc0be72b45 100644 --- a/unit/solvers/smt2_incremental/smt_response_validation.cpp +++ b/unit/solvers/smt2_incremental/smt_response_validation.cpp @@ -339,5 +339,19 @@ TEST_CASE("smt get-value response validation", "[core][smt2_incremental]") *empty_pair.get_if_error() == std::vector{ "Unrecognised SMT term - \"\".", "Unrecognised SMT term - \"\"."}); + SECTION("Mismatched descriptor and value sorts") + { + const response_or_errort mismatched_pair = + validate_smt_response( + *smt2irep("((foo #x2A)))").parsed_output, + table_with_identifiers({{"foo", smt_bool_sortt{}}})); + CHECK( + *mismatched_pair.get_if_error() == + std::vector{"Mismatched descriptor and value sorts in - \n" + "0: foo\n" + "1: #x2A\n" + "Descriptor has sort Bool\n" + "Value has sort (_ BitVec 8)"}); + } } }