Merge pull request #7094 from thomasspriggs/tas/get-value-sort-valida…

…tion

Add validation messaging for sorts in SMT get-value responses

src/solvers/smt2_incremental/smt_response_validation.cpp

@@ -22,47 +22,48 @@
 #include <util/range.h>
 
 #include "smt_array_theory.h"
+#include "smt_to_smt2_string.h"
 
 #include <regex>
 
 static response_or_errort<smt_termt> validate_term(
   const irept &parse_tree,
   const std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table);
 
-// Implementation detail of `collect_messages` below.
+// Implementation detail of `collect_error_messages` below.
 template <typename argumentt, typename... argumentst>
-void collect_messages_impl(
-  std::vector<std::string> &collected_messages,
+void collect_error_messages_impl(
+  std::vector<std::string> &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 <typename argumentt, typename... argumentst>
-void collect_messages_impl(
-  std::vector<std::string> &collected_messages,
+void collect_error_messages_impl(
+  std::vector<std::string> &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 <typename... argumentst>
-std::vector<std::string> collect_messages(argumentst &&... arguments)
+std::vector<std::string> collect_error_messages(argumentst &&... arguments)
 {
-  std::vector<std::string> collected_messages;
-  collect_messages_impl(collected_messages, arguments...);
-  return collected_messages;
+  std::vector<std::string> 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<smt_baset> validation_propagating(argumentst &&... arguments)
 {
-  const auto collected_messages = collect_messages(arguments...);
-  if(!collected_messages.empty())
-    return response_or_errort<smt_baset>(collected_messages);
+  const auto collected_error_messages = collect_error_messages(arguments...);
+  if(!collected_error_messages.empty())
+    return response_or_errort<smt_baset>(collected_error_messages);
   else
   {
     return response_or_errort<smt_baset>{
@@ -255,9 +256,9 @@ static optionalt<response_or_errort<smt_termt>> 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<smt_termt>{messages};
+  const auto error_messages = collect_error_messages(array, index);
+  if(!error_messages.empty())
+    return response_or_errort<smt_termt>{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<irep_idt, smt_identifier_termt> &identifier_table)
 {
+  using resultt = response_or_errort<smt_get_value_responset::valuation_pairt>;
   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<smt_get_value_responset::valuation_pairt>(
-    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

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<std::string>{
         "Unrecognised SMT term - \"\".", "Unrecognised SMT term - \"\"."});
+    SECTION("Mismatched descriptor and value sorts")
+    {
+      const response_or_errort<smt_responset> 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<std::string>{"Mismatched descriptor and value sorts in - \n"
+                                 "0: foo\n"
+                                 "1: #x2A\n"
+                                 "Descriptor has sort Bool\n"
+                                 "Value has sort (_ BitVec 8)"});
+    }
   }
 }