Merge pull request #4777 from danpoe/feature/simplify-expression-char-at

Expression simplification for charAt()

Author: danpoe

jbmc/regression/jbmc-strings/CharAtConstantEvaluation/Main.class

@@ -0,0 +1,7 @@
+public class Main {
+    public void constantCharAt() {
+        StringBuilder sb = new StringBuilder("abc");
+        char c = sb.charAt(1);
+        assert c == 'b';
+    }
+}

jbmc/regression/jbmc-strings/CharAtConstantEvaluation/Main.java

@@ -0,0 +1,8 @@
+CORE
+Main.class
+--function Main.constantCharAt --show-vcc
+^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+--
+--

jbmc/regression/jbmc-strings/CharAtConstantEvaluation/test.desc

@@ -181,67 +181,34 @@ bool simplify_exprt::simplify_function_application(exprt &expr)
     auto &first_argument = to_string_expr(function_app.arguments().at(0));
     auto &second_argument = to_string_expr(function_app.arguments().at(1));
 
-    if(
-      first_argument.content().id() != ID_address_of ||
-      second_argument.content().id() != ID_address_of)
+    const auto first_value_opt = try_get_string_data_array(first_argument, ns);
+
+    if(!first_value_opt)
     {
       return true;
     }
 
-    mp_integer offset_int = 0;
-    if(function_app.arguments().size() == 3)
-    {
-      auto &offset = function_app.arguments()[2];
-      if(offset.id() != ID_constant)
-        return true;
-      offset_int = numeric_cast_v<mp_integer>(to_constant_expr(offset));
-    }
+    const array_exprt &first_value = first_value_opt->get();
 
-    const address_of_exprt &first_address_of =
-      to_address_of_expr(first_argument.content());
-    const address_of_exprt &second_address_of =
-      to_address_of_expr(second_argument.content());
+    const auto second_value_opt =
+      try_get_string_data_array(second_argument, ns);
 
-    // Constants are got via address_of expressions, so this helps filter out
-    // things that are non-constant.
-    if(
-      first_address_of.object().id() != ID_index ||
-      second_address_of.object().id() != ID_index)
+    if(!second_value_opt)
     {
       return true;
     }
 
-    const index_exprt &first_index_expression =
-      to_index_expr(first_address_of.object());
-    const index_exprt &second_index_expression =
-      to_index_expr(second_address_of.object());
-
-    const exprt &first_string_array = first_index_expression.array();
-    const exprt &second_string_array = second_index_expression.array();
+    const array_exprt &second_value = second_value_opt->get();
 
-    // Check if our symbols type is an array.
-    if(
-      first_string_array.type().id() != ID_array ||
-      second_string_array.type().id() != ID_array)
+    mp_integer offset_int = 0;
+    if(function_app.arguments().size() == 3)
     {
-      return true;
+      auto &offset = function_app.arguments()[2];
+      if(offset.id() != ID_constant)
+        return true;
+      offset_int = numeric_cast_v<mp_integer>(to_constant_expr(offset));
     }
 
-    // get their initial values from the symbol table
-    const symbolt *symbol_ptr = nullptr;
-    if(ns.lookup(
-         to_symbol_expr(first_string_array).get_identifier(), symbol_ptr))
-      return true;
-    const exprt &first_value = symbol_ptr->value;
-    if(ns.lookup(
-         to_symbol_expr(second_string_array).get_identifier(), symbol_ptr))
-      return true;
-    const exprt &second_value = symbol_ptr->value;
-
-    // only compare if both are arrays
-    if(first_value.id() != ID_array || second_value.id() != ID_array)
-      return true;
-
     // test whether second_value is a prefix of first_value
     bool is_prefix =
       offset_int >= 0 && mp_integer(first_value.operands().size()) >=
@@ -268,6 +235,45 @@ bool simplify_exprt::simplify_function_application(exprt &expr)
     expr = from_integer(is_prefix ? 1 : 0, expr.type());
     return false;
   }
+  else if(func_id == ID_cprover_string_char_at_func)
+  {
+    if(function_app.arguments().at(1).id() != ID_constant)
+    {
+      return true;
+    }
+
+    const auto &index = to_constant_expr(function_app.arguments().at(1));
+
+    const refined_string_exprt &s =
+      to_string_expr(function_app.arguments().at(0));
+
+    const auto char_seq_opt = try_get_string_data_array(s, ns);
+
+    if(!char_seq_opt)
+    {
+      return true;
+    }
+
+    const array_exprt &char_seq = char_seq_opt->get();
+
+    const auto i_opt = numeric_cast<std::size_t>(index);
+
+    if(!i_opt || *i_opt >= char_seq.operands().size())
+    {
+      return true;
+    }
+
+    const auto &c = to_constant_expr(char_seq.operands().at(*i_opt));
+
+    if(c.type() != expr.type())
+    {
+      return true;
+    }
+
+    expr = c;
+
+    return false;
+  }
 
   return true;
 }
@@ -1826,6 +1832,46 @@ optionalt<std::string> simplify_exprt::expr2bits(
   return {};
 }
 
+optionalt<std::reference_wrapper<const array_exprt>>
+  simplify_exprt::try_get_string_data_array(
+    const refined_string_exprt &s,
+    const namespacet &ns)
+{
+  if(s.content().id() != ID_address_of)
+  {
+    return {};
+  }
+
+  const auto &content = to_address_of_expr(s.content());
+
+  if(content.object().id() != ID_index)
+  {
+    return {};
+  }
+
+  const auto &array_start = to_index_expr(content.object());
+
+  if(array_start.array().id() != ID_symbol ||
+     array_start.array().type().id() != ID_array)
+  {
+    return {};
+  }
+
+  const auto &array = to_symbol_expr(array_start.array());
+
+  const symbolt *symbol_ptr = nullptr;
+
+  if(ns.lookup(array.get_identifier(), symbol_ptr) ||
+     symbol_ptr->value.id() != ID_array)
+  {
+    return {};
+  }
+
+  const auto &char_seq = to_array_expr(symbol_ptr->value);
+
+  return optionalt<std::reference_wrapper<const array_exprt>>(char_seq);
+}
+
 bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)
 {
   // lift up any ID_if on the object

src/util/simplify_expr.cpp

@@ -25,6 +25,7 @@ Author: Daniel Kroening, [email protected]
 #include "replace_expr.h"
 #endif
 
+class array_exprt;
 class bswap_exprt;
 class byte_extract_exprt;
 class byte_update_exprt;
@@ -35,6 +36,7 @@ class index_exprt;
 class member_exprt;
 class namespacet;
 class popcount_exprt;
+class refined_string_exprt;
 class tvt;
 class typecast_exprt;
 
@@ -215,6 +217,23 @@ class simplify_exprt
 #ifdef USE_LOCAL_REPLACE_MAP
   replace_mapt local_replace_map;
 #endif
+
+  /// Get char sequence from 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.
+  ///
+  /// \param s: 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
+  static optionalt<std::reference_wrapper<const array_exprt>>
+    try_get_string_data_array(
+      const refined_string_exprt &s,
+      const namespacet &ns);
 };
 
 #endif // CPROVER_UTIL_SIMPLIFY_EXPR_CLASS_H