Merge pull request #7808 from thomasspriggs/tas/smt_string_literals

Add string literal support to incremental SMT decision procedure

Author: thomasspriggs

regression/cbmc-incr-smt2/arrays/string_literal.c

@@ -0,0 +1,11 @@
+#include <assert.h>
+#include <stdint.h>
+
+int main()
+{
+  const char *my_string = "hello!";
+  uint8_t index;
+  __CPROVER_assume(index < 6);
+  char element = my_string[index];
+  assert(element != 'o');
+}

regression/cbmc-incr-smt2/arrays/string_literal.desc

@@ -0,0 +1,13 @@
+CORE
+string_literal.c
+--trace
+Passing problem to incremental SMT2 solving
+line 10 assertion element \!\= \'o\'\: FAILURE
+index=4
+element='o'
+VERIFICATION FAILED
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Test of indexing into a string literal.

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -8,6 +8,7 @@
 #include <util/nodiscard.h>
 #include <util/range.h>
 #include <util/std_expr.h>
+#include <util/string_constant.h>
 #include <util/symbol.h>
 
 #include <solvers/smt2_incremental/ast/smt_commands.h>
@@ -74,7 +75,8 @@ static std::vector<exprt> gather_dependent_expressions(const exprt &expr)
       can_cast_expr<symbol_exprt>(expr_node) ||
       can_cast_expr<array_exprt>(expr_node) ||
       can_cast_expr<array_of_exprt>(expr_node) ||
-      can_cast_expr<nondet_symbol_exprt>(expr_node))
+      can_cast_expr<nondet_symbol_exprt>(expr_node) ||
+      can_cast_expr<string_constantt>(expr_node))
     {
       dependent_expressions.push_back(expr_node);
     }
@@ -117,6 +119,13 @@ void smt2_incremental_decision_proceduret::initialize_array_elements(
   solver_process->send(elements_definition);
 }
 
+void smt2_incremental_decision_proceduret::initialize_array_elements(
+  const string_constantt &string,
+  const smt_identifier_termt &array_identifier)
+{
+  initialize_array_elements(string.to_array_expr(), array_identifier);
+}
+
 template <typename t_exprt>
 void smt2_incremental_decision_proceduret::define_array_function(
   const t_exprt &array)
@@ -209,6 +218,11 @@ void smt2_incremental_decision_proceduret::define_dependent_functions(
     {
       define_array_function(*array_of_expr);
     }
+    else if(
+      const auto string = expr_try_dynamic_cast<string_constantt>(current))
+    {
+      define_array_function(*string);
+    }
     else if(
       const auto nondet_symbol =
         expr_try_dynamic_cast<nondet_symbol_exprt>(current))

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h

@@ -22,6 +22,7 @@
 
 class namespacet;
 class smt_base_solver_processt; // IWYU pragma: keep
+class string_constantt;
 
 class smt2_incremental_decision_proceduret final
   : public stack_decision_proceduret
@@ -87,6 +88,9 @@ class smt2_incremental_decision_proceduret final
   void initialize_array_elements(
     const array_of_exprt &array,
     const smt_identifier_termt &array_identifier);
+  void initialize_array_elements(
+    const string_constantt &string,
+    const smt_identifier_termt &array_identifier);
   /// \brief Defines any functions which \p expr depends on, which have not yet
   ///   been defined, along with their dependencies in turn.
   void define_dependent_functions(const exprt &expr);

unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -6,6 +6,7 @@
 #include <util/exception_utils.h>
 #include <util/make_unique.h>
 #include <util/namespace.h>
+#include <util/string_constant.h>
 #include <util/symbol_table.h>
 
 #include <solvers/smt2_incremental/ast/smt_commands.h>
@@ -683,6 +684,53 @@ TEST_CASE(
   }
 }
 
+TEST_CASE(
+  "smt2_incremental_decision_proceduret string literal commands.",
+  "[core][smt2_incremental]")
+{
+  auto test = decision_procedure_test_environmentt::make();
+  const string_constantt constant{"Chips"};
+  const typet array_type = constant.to_array_expr().type();
+  const symbolt fish{"fish", array_type, ID_C};
+  test.symbol_table.insert(fish);
+  test.sent_commands.clear();
+  test.procedure.set_to(equal_exprt{fish.symbol_expr(), constant}, true);
+  const smt_array_sortt expected_sort{
+    smt_bit_vector_sortt{32}, smt_bit_vector_sortt{8}};
+  const smt_identifier_termt expected_fish{"fish", expected_sort};
+  const smt_identifier_termt expected_chips{"array_0", expected_sort};
+  const std::vector<smt_commandt> expected_commands{
+    smt_declare_function_commandt{expected_fish, {}},
+    smt_declare_function_commandt{expected_chips, {}},
+    smt_assert_commandt{smt_core_theoryt::equal(
+      smt_array_theoryt::select(
+        expected_chips, smt_bit_vector_constant_termt{0, 32}),
+      smt_bit_vector_constant_termt{'C', 8})},
+    smt_assert_commandt{smt_core_theoryt::equal(
+      smt_array_theoryt::select(
+        expected_chips, smt_bit_vector_constant_termt{1, 32}),
+      smt_bit_vector_constant_termt{'h', 8})},
+    smt_assert_commandt{smt_core_theoryt::equal(
+      smt_array_theoryt::select(
+        expected_chips, smt_bit_vector_constant_termt{2, 32}),
+      smt_bit_vector_constant_termt{'i', 8})},
+    smt_assert_commandt{smt_core_theoryt::equal(
+      smt_array_theoryt::select(
+        expected_chips, smt_bit_vector_constant_termt{3, 32}),
+      smt_bit_vector_constant_termt{'p', 8})},
+    smt_assert_commandt{smt_core_theoryt::equal(
+      smt_array_theoryt::select(
+        expected_chips, smt_bit_vector_constant_termt{4, 32}),
+      smt_bit_vector_constant_termt{'s', 8})},
+    smt_assert_commandt{smt_core_theoryt::equal(
+      smt_array_theoryt::select(
+        expected_chips, smt_bit_vector_constant_termt{5, 32}),
+      smt_bit_vector_constant_termt{'\0', 8})},
+    smt_assert_commandt{
+      smt_core_theoryt::equal(expected_fish, expected_chips)}};
+  REQUIRE(test.sent_commands == expected_commands);
+}
+
 TEST_CASE(
   "smt2_incremental_decision_proceduret multi-ary with_exprt introduces "
   "correct number of indexes.",