Add validation for array select argument sorts

Author: thomasspriggs

src/solvers/smt2_incremental/response_or_error.h

@@ -0,0 +1,64 @@
+// Author: Diffblue Ltd.
+
+#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_RESPONSE_OR_ERROR_H
+#define CPROVER_SOLVERS_SMT2_INCREMENTAL_RESPONSE_OR_ERROR_H
+
+#include <util/invariant.h>
+#include <util/optional.h>
+
+#include <string>
+#include <vector>
+
+/// Holds either a valid parsed response or response sub-tree of type \tparam
+/// smtt or a collection of message strings explaining why the given input was
+/// not valid.
+template <class smtt>
+class response_or_errort final
+{
+public:
+  explicit response_or_errort(smtt smt) : smt{std::move(smt)}
+  {
+  }
+
+  explicit response_or_errort(std::string message)
+    : messages{std::move(message)}
+  {
+  }
+
+  explicit response_or_errort(std::vector<std::string> messages)
+    : messages{std::move(messages)}
+  {
+  }
+
+  /// \brief Gets the smt response if the response is valid, or returns nullptr
+  ///   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;
+  }
+
+  /// \brief Gets the error messages if the response is invalid, or returns
+  ///   nullptr otherwise.
+  const std::vector<std::string> *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;
+  }
+
+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<smtt> smt;
+  std::vector<std::string> messages;
+};
+
+#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_RESPONSE_OR_ERROR_H

src/solvers/smt2_incremental/smt_array_theory.cpp

@@ -14,15 +14,24 @@ smt_sortt smt_array_theoryt::selectt::return_sort(
   return array.get_sort().cast<smt_array_sortt>()->element_sort();
 }
 
-void smt_array_theoryt::selectt::validate(
+std::vector<std::string> smt_array_theoryt::selectt::validation_errors(
   const smt_termt &array,
   const smt_termt &index)
 {
   const auto array_sort = array.get_sort().cast<smt_array_sortt>();
-  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.");
+  if(!array_sort)
+    return {"\"select\" may only select from an array."};
+  if(array_sort->index_sort() != index.get_sort())
+    return {"Sort of arrays index must match the sort of the index supplied."};
+  return {};
+}
+
+void smt_array_theoryt::selectt::validate(
+  const smt_termt &array,
+  const smt_termt &index)
+{
+  const auto validation_errors = selectt::validation_errors(array, index);
+  INVARIANT(validation_errors.empty(), validation_errors[0]);
 }
 
 const smt_function_application_termt::factoryt<smt_array_theoryt::selectt>

src/solvers/smt2_incremental/smt_array_theory.h

@@ -13,6 +13,8 @@ class smt_array_theoryt
     static const char *identifier();
     static smt_sortt
     return_sort(const smt_termt &array, const smt_termt &index);
+    static std::vector<std::string>
+    validation_errors(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<selectt> select;

src/solvers/smt2_incremental/smt_response_validation.cpp

@@ -29,45 +29,6 @@ static response_or_errort<smt_termt> validate_term(
   const irept &parse_tree,
   const std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table);
 
-template <class smtt>
-response_or_errort<smtt>::response_or_errort(smtt smt) : smt{std::move(smt)}
-{
-}
-
-template <class smtt>
-response_or_errort<smtt>::response_or_errort(std::string message)
-  : messages{std::move(message)}
-{
-}
-
-template <class smtt>
-response_or_errort<smtt>::response_or_errort(std::vector<std::string> messages)
-  : messages{std::move(messages)}
-{
-}
-
-template <class smtt>
-const smtt *response_or_errort<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;
-}
-
-template <class smtt>
-const std::vector<std::string> *response_or_errort<smtt>::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;
-}
-
-template class response_or_errort<smt_responset>;
-
 // Implementation detail of `collect_messages` below.
 template <typename argumentt, typename... argumentst>
 void collect_messages_impl(
@@ -297,8 +258,8 @@ static optionalt<response_or_errort<smt_termt>> try_select_validation(
   const auto messages = collect_messages(array, index);
   if(!messages.empty())
     return response_or_errort<smt_termt>{messages};
-  return response_or_errort<smt_termt>{
-    smt_array_theoryt::select(*array.get_if_valid(), *index.get_if_valid())};
+  return {smt_array_theoryt::select.validation(
+    *array.get_if_valid(), *index.get_if_valid())};
 }
 
 static response_or_errort<smt_termt> validate_term(

src/solvers/smt2_incremental/smt_response_validation.h

@@ -3,40 +3,10 @@
 #ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_RESPONSE_VALIDATION_H
 #define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_RESPONSE_VALIDATION_H
 
-#include <solvers/smt2_incremental/smt_responses.h>
-#include <util/invariant.h>
 #include <util/nodiscard.h>
-#include <util/optional.h>
-
-#include <string>
-#include <vector>
-
-/// Holds either a valid parsed response or response sub-tree of type \tparam
-/// smtt or a collection of message strings explaining why the given input was
-/// not valid.
-template <class smtt>
-class response_or_errort final
-{
-public:
-  explicit response_or_errort(smtt smt);
-  explicit response_or_errort(std::string message);
-  explicit response_or_errort(std::vector<std::string> messages);
 
-  /// \brief Gets the smt response if the response is valid, or returns nullptr
-  ///   otherwise.
-  const smtt *get_if_valid() const;
-  /// \brief Gets the error messages if the response is invalid, or returns
-  ///   nullptr otherwise.
-  const std::vector<std::string> *get_if_error() const;
-
-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<smtt> smt;
-  std::vector<std::string> messages;
-};
+#include <solvers/smt2_incremental/response_or_error.h>
+#include <solvers/smt2_incremental/smt_responses.h>
 
 NODISCARD response_or_errort<smt_responset> validate_smt_response(
   const irept &parse_tree,

src/solvers/smt2_incremental/smt_terms.h

@@ -5,6 +5,7 @@
 
 #include <util/irep.h>
 
+#include <solvers/smt2_incremental/response_or_error.h>
 #include <solvers/smt2_incremental/smt_index.h>
 #include <solvers/smt2_incremental/smt_sorts.h>
 #include <solvers/smt2_incremental/type_traits.h>
@@ -204,6 +205,20 @@ class smt_function_application_termt : public smt_termt
           function.identifier(), std::move(return_sort), indices(function)},
         {std::forward<argument_typest>(arguments)...}};
     }
+
+    template <typename... argument_typest>
+    response_or_errort<smt_termt>
+    validation(argument_typest &&... arguments) const
+    {
+      const auto validation_errors = function.validation_errors(arguments...);
+      if(!validation_errors.empty())
+        return response_or_errort<smt_termt>{validation_errors};
+      auto return_sort = function.return_sort(arguments...);
+      return response_or_errort<smt_termt>{smt_function_application_termt{
+        smt_identifier_termt{
+          function.identifier(), std::move(return_sort), indices(function)},
+        {std::forward<argument_typest>(arguments)...}}};
+    }
   };
 };
 

unit/solvers/smt2_incremental/smt_response_validation.cpp

@@ -176,15 +176,40 @@ TEST_CASE("smt get-value response validation", "[core][smt2_incremental]")
           smt_array_sortt{
             smt_bit_vector_sortt{32}, smt_bit_vector_sortt{32}}}});
 
-      const response_or_errort<smt_responset> response_get_select =
-        validate_smt_response(
-          *smt2irep("(((select |b| (_ bv10 32)) #x0000002a))").parsed_output,
-          identifier_table);
-
-      CHECK(
-        *response_get_select.get_if_valid() ==
-        smt_get_value_responset{{smt_get_value_responset::valuation_pairt{
-          select, smt_bit_vector_constant_termt{0x2A, 32}}}});
+      SECTION("Valid application of smt_array_theoryt::select")
+      {
+        const response_or_errort<smt_responset> response_get_select =
+          validate_smt_response(
+            *smt2irep("(((select |b| (_ bv10 32)) #x0000002a))").parsed_output,
+            identifier_table);
+        CHECK(
+          *response_get_select.get_if_valid() ==
+          smt_get_value_responset{{smt_get_value_responset::valuation_pairt{
+            select, smt_bit_vector_constant_termt{0x2A, 32}}}});
+      }
+      SECTION("Invalid due to selecting from non-array")
+      {
+        const response_or_errort<smt_responset> response_get_select =
+          validate_smt_response(
+            *smt2irep("(((select (_ bv10 32) (_ bv10 32)) #x0000002a))")
+               .parsed_output,
+            identifier_table);
+        CHECK(
+          *response_get_select.get_if_error() ==
+          std::vector<std::string>{
+            "\"select\" may only select from an array."});
+      }
+      SECTION("Invalid due to selecting invalid index sort")
+      {
+        const response_or_errort<smt_responset> response_get_select =
+          validate_smt_response(
+            *smt2irep("(((select |b| (_ bv10 16)) #x0000002a))").parsed_output,
+            identifier_table);
+        CHECK(
+          *response_get_select.get_if_error() ==
+          std::vector<std::string>{
+            "Sort of arrays index must match the sort of the index supplied."});
+      }
     }
     SECTION("Descriptors which are bit vector constants")
     {