Change interface of try_get_string_data_array()

Take the content field of a refined string expression instead of taking the
whole refined string expression. This will allow it to be used from the string
mutators constant propagation code in goto_symex.cpp.

Author: danpoe

src/util/simplify_expr.cpp

@@ -158,14 +158,14 @@ static simplify_exprt::resultt<> simplify_string_endswith(
   const namespacet &ns)
 {
   const refined_string_exprt &s1 = to_string_expr(expr.arguments().at(0));
-  const auto s1_data_opt = try_get_string_data_array(s1, ns);
+  const auto s1_data_opt = try_get_string_data_array(s1.content(), ns);
 
   if(!s1_data_opt)
     return simplify_exprt::unchanged(expr);
 
   const array_exprt &s1_data = s1_data_opt->get();
   const refined_string_exprt &s2 = to_string_expr(expr.arguments().at(1));
-  const auto s2_data_opt = try_get_string_data_array(s2, ns);
+  const auto s2_data_opt = try_get_string_data_array(s2.content(), ns);
 
   if(!s2_data_opt)
     return simplify_exprt::unchanged(expr);
@@ -214,13 +214,13 @@ static simplify_exprt::resultt<> simplify_string_compare_to(
   const namespacet &ns)
 {
   const refined_string_exprt &s1 = to_string_expr(expr.arguments().at(0));
-  const auto s1_data_opt = try_get_string_data_array(s1, ns);
+  const auto s1_data_opt = try_get_string_data_array(s1.content(), ns);
 
   if(!s1_data_opt)
     return simplify_exprt::unchanged(expr);
 
   const refined_string_exprt &s2 = to_string_expr(expr.arguments().at(1));
-  const auto s2_data_opt = try_get_string_data_array(s2, ns);
+  const auto s2_data_opt = try_get_string_data_array(s2.content(), ns);
 
   if(!s2_data_opt)
     return simplify_exprt::unchanged(expr);
@@ -285,7 +285,7 @@ static simplify_exprt::resultt<> simplify_string_index_of(
 
   const refined_string_exprt &s1 = to_string_expr(expr.arguments().at(0));
 
-  const auto s1_data_opt = try_get_string_data_array(s1, ns);
+  const auto s1_data_opt = try_get_string_data_array(s1.content(), ns);
 
   if(!s1_data_opt)
   {
@@ -310,7 +310,7 @@ static simplify_exprt::resultt<> simplify_string_index_of(
     const refined_string_exprt &s2 =
       to_string_expr(expr.arguments().at(1));
 
-    const auto s2_data_opt = try_get_string_data_array(s2, ns);
+    const auto s2_data_opt = try_get_string_data_array(s2.content(), ns);
 
     if(!s2_data_opt)
     {
@@ -379,7 +379,7 @@ static simplify_exprt::resultt<> simplify_string_char_at(
 
   const refined_string_exprt &s = to_string_expr(expr.arguments().at(0));
 
-  const auto char_seq_opt = try_get_string_data_array(s, ns);
+  const auto char_seq_opt = try_get_string_data_array(s.content(), ns);
 
   if(!char_seq_opt)
   {
@@ -420,7 +420,8 @@ static simplify_exprt::resultt<> simplify_string_startswith(
   auto &first_argument = to_string_expr(expr.arguments().at(0));
   auto &second_argument = to_string_expr(expr.arguments().at(1));
 
-  const auto first_value_opt = try_get_string_data_array(first_argument, ns);
+  const auto first_value_opt =
+    try_get_string_data_array(first_argument.content(), ns);
 
   if(!first_value_opt)
   {
@@ -429,7 +430,8 @@ static simplify_exprt::resultt<> simplify_string_startswith(
 
   const array_exprt &first_value = first_value_opt->get();
 
-  const auto second_value_opt = try_get_string_data_array(second_argument, ns);
+  const auto second_value_opt =
+    try_get_string_data_array(second_argument.content(), ns);
 
   if(!second_value_opt)
   {
@@ -1666,21 +1668,21 @@ optionalt<std::string> simplify_exprt::expr2bits(
 }
 
 optionalt<std::reference_wrapper<const array_exprt>>
-try_get_string_data_array(const refined_string_exprt &s, const namespacet &ns)
+try_get_string_data_array(const exprt &content, const namespacet &ns)
 {
-  if(s.content().id() != ID_address_of)
+  if(content.id() != ID_address_of)
   {
     return {};
   }
 
-  const auto &content = to_address_of_expr(s.content());
+  const auto &array_pointer = to_address_of_expr(content);
 
-  if(content.object().id() != ID_index)
+  if(array_pointer.object().id() != ID_index)
   {
     return {};
   }
 
-  const auto &array_start = to_index_expr(content.object());
+  const auto &array_start = to_index_expr(array_pointer.object());
 
   if(array_start.array().id() != ID_symbol ||
      array_start.array().type().id() != ID_array)

src/util/simplify_expr.h

@@ -31,19 +31,19 @@ bool simplify(
 // this is the preferred interface
 exprt simplify_expr(exprt src, const namespacet &ns);
 
-/// Get char sequence from refined string expression
+/// Get char sequence from content field of a refined string expression
 ///
-/// If `s.content()` is of the form `&id[e]`, where `id` is an array-typed
-/// symbol expression (and `e` is any expression), return the value of the
-/// symbol `id` (as given by the `value` field of the symbol in the namespace
-/// `ns`); otherwise return an empty optional.
+/// If `content` is of the form `&id[e]`, where `id` is an array-typed symbol
+/// expression (and `e` is any expression), return the value of the symbol `id`
+/// (as given by the `value` field of the symbol in the namespace `ns`);
+/// otherwise return an empty optional.
 ///
-/// \param s: refined string expression
+/// \param content: content field of a refined string expression
 /// \param ns: namespace
 /// \return array expression representing the char sequence which forms the
 ///   content of the refined string expression, empty optional if the content
 ///   cannot be determined
 optionalt<std::reference_wrapper<const array_exprt>>
-try_get_string_data_array(const refined_string_exprt &s, const namespacet &ns);
+try_get_string_data_array(const exprt &content, const namespacet &ns);
 
 #endif // CPROVER_UTIL_SIMPLIFY_EXPR_H