Making substitute_array_list ignore out of bounds indexes

src/solvers/refinement/string_refinement.cpp

@@ -1623,16 +1623,20 @@ std::vector<exprt> string_refinementt::instantiate_not_contains(
     axiom, index_set0, index_set1, generator);
 }
 
-/// replace array-lists by 'with' expressions
-/// \par parameters: an expression containing array-list expressions
+/// Replace array-lists by 'with' expressions.
+/// For instance `array-list [ 0 , x , 1 , y ]` is replaced by
+/// `ARRAYOF(0) WITH [0:=x] WITH [1:=y]`.
+/// Indexes exceeding the maximal string length are ignored.
+/// \param expr: an expression containing array-list expressions
+/// \param string_max_length: maximum length allowed for strings
 /// \return an expression containing no array-list
-exprt string_refinementt::substitute_array_lists(exprt expr) const
+exprt substitute_array_lists(exprt expr, size_t string_max_length)
 {
   for(size_t i=0; i<expr.operands().size(); ++i)
   {
     // TODO: only copy when necessary
-    exprt op(expr.operands()[i]);
-    expr.operands()[i]=substitute_array_lists(op);
+    exprt op=(expr.operands()[i]);
+    expr.operands()[i]=substitute_array_lists(op, string_max_length);
   }
 
   if(expr.id()=="array-list")
@@ -1643,18 +1647,17 @@ exprt string_refinementt::substitute_array_lists(exprt expr) const
         "operands"));
     typet &char_type=expr.operands()[1].type();
     array_typet arr_type(char_type, infinity_exprt(char_type));
-    array_of_exprt new_arr(from_integer(0, char_type),
-                           arr_type);
-
-    with_exprt ret_expr(new_arr,
-                        expr.operands()[0],
-                        expr.operands()[1]);
+    exprt ret_expr=array_of_exprt(from_integer(0, char_type), arr_type);
 
-    for(size_t i=1; i<expr.operands().size()/2; i++)
+    for(size_t i=0; i<expr.operands().size()/2; i++)
     {
-      ret_expr=with_exprt(ret_expr,
-                          expr.operands()[i*2],
-                          expr.operands()[i*2+1]);
+      const exprt &index=expr.operands()[i*2];
+      const exprt &value=expr.operands()[i*2+1];
+      mp_integer index_value;
+      bool not_constant=to_integer(index, index_value);
+      if(not_constant ||
+         (index_value>=0 && index_value<string_max_length))
+        ret_expr=with_exprt(ret_expr, index, value);
     }
     return ret_expr;
   }
@@ -1692,7 +1695,7 @@ exprt string_refinementt::get(const exprt &expr) const
 
   ecopy=supert::get(ecopy);
 
-  return substitute_array_lists(ecopy);
+  return substitute_array_lists(ecopy, generator.max_string_length);
 }
 
 /// Creates a solver with `axiom` as the only formula added and runs it. If it

src/solvers/refinement/string_refinement.h

@@ -136,8 +136,6 @@ class string_refinementt: public bv_refinementt
   std::vector<exprt> instantiate_not_contains(
     const string_not_contains_constraintt &axiom);
 
-  exprt substitute_array_lists(exprt) const;
-
   exprt compute_inverse_function(
     const exprt &qvar, const exprt &val, const exprt &f);
 
@@ -164,6 +162,8 @@ class string_refinementt: public bv_refinementt
   std::string string_of_array(const array_exprt &arr);
 };
 
+exprt substitute_array_lists(exprt expr, size_t string_max_length);
+
 /// Utility function for concretization of strings. Copies concretized values to
 /// the left to initialize the unconcretized indices of concrete_array.
 /// \param concrete_array: the vector to populate

unit/Makefile

@@ -25,6 +25,7 @@ SRC += unit_tests.cpp \
        solvers/refinement/string_constraint_generator_valueof/is_digit_with_radix.cpp \
        solvers/refinement/string_constraint_generator_valueof/is_digit_with_radix_lower_case.cpp \
        solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp \
+       solvers/refinement/string_refinement/substitute_array_list.cpp \
        catch_example.cpp \
        # Empty last line
 

unit/solvers/refinement/string_refinement/substitute_array_list.cpp

@@ -0,0 +1,55 @@
+/*******************************************************************\
+
+ Module: Unit tests for get_numeric_value_from_character in
+   solvers/refinement/string_constraint_generator_valueof.cpp
+
+ Author: DiffBlue Limited. All rights reserved.
+
+\*******************************************************************/
+
+#include <catch.hpp>
+
+#include <util/arith_tools.h>
+#include <util/std_types.h>
+#include <util/std_expr.h>
+#include <solvers/refinement/string_refinement.h>
+#include <iostream>
+
+SCENARIO("substitute_array_list",
+  "[core][solvers][refinement][string_refinement]")
+{
+  const typet char_type=unsignedbv_typet(16);
+  const typet int_type=signedbv_typet(32);
+  exprt arr("array-list");
+  const exprt index0=from_integer(0, int_type);
+  const exprt charx=from_integer('x', char_type);
+  const exprt index1=from_integer(1, int_type);
+  const exprt chary=from_integer('y', char_type);
+  const exprt index100=from_integer(100, int_type);
+
+  // arr is `array-list [ 0 , 'x' , 1 , 'y' , 2 , 'z']`
+  arr.operands()=
+    { index0, charx, index1, chary, index100, from_integer('z', char_type) };
+
+  // Max length is 2, so index 2 should get ignored.
+  const exprt subst=substitute_array_lists(arr, 2);
+
+  // Check that `subst = e1 WITH [1:='y']`
+  REQUIRE(subst.id()==ID_with);
+  REQUIRE(subst.operands().size()==3);
+  const exprt &e1=subst.op0();
+  REQUIRE(subst.op1()==index1);
+  REQUIRE(subst.op2()==chary);
+
+  // Check that `e1 = e2 WITH [0:='x']`
+  REQUIRE(e1.id()==ID_with);
+  REQUIRE(e1.operands().size()==3);
+  const exprt &e2=e1.op0();
+  REQUIRE(e1.op1()==index0);
+  REQUIRE(e1.op2()==charx);
+
+  // Check that `e1 = ARRAY_OF 0`
+  REQUIRE(e2.id()==ID_array_of);
+  REQUIRE(e2.operands().size()==1);
+  REQUIRE(e2.op0()==from_integer(0, char_type));
+}