Merge pull request #1104 from romainbrenguier/feature/string-solver-if-expr#275

Handling of if_exprt in string solver

Author: romainbrenguier

regression/strings-smoke-tests/java_if/test.class

@@ -0,0 +1,9 @@
+CORE
+test.class
+--refine-strings --string-max-length 100
+^EXIT=10$
+^SIGNAL=0$
+^\[.*assertion.1\].* line 12.* SUCCESS$
+^\[.*assertion.2\].* line 13.* FAILURE$
+--
+$ignoring\s*char\s*array

regression/strings-smoke-tests/java_if/test.desc

@@ -0,0 +1,16 @@
+public class test
+{
+    public static String main()
+    {
+        Object t[] = new Object[5];
+        t[0] = "world!";
+        StringBuilder s = new StringBuilder("Hello ");
+        if(t[0] instanceof String)
+        {
+            s.append((String) t[0]);
+        }
+        assert(s.toString().equals("Hello world!"));
+        assert(!s.toString().equals("Hello world!"));
+        return s.toString();
+    }
+}

regression/strings-smoke-tests/java_if/test.java

@@ -94,6 +94,9 @@ class string_constraint_generatort
 
   static constant_exprt constant_char(int i, const typet &char_type);
 
+  // Used by string refinement
+  void add_axioms_for_if_array(const exprt &lhs, const if_exprt &expr);
+
 private:
   // The integer with the longest string is Integer.MIN_VALUE which is -2^31,
   // that is -2147483648 so takes 11 characters to write.

src/solvers/refinement/string_constraint_generator.h

@@ -272,6 +272,46 @@ string_exprt string_constraint_generatort::add_axioms_for_if(
   return res;
 }
 
+/// Add axioms enforcing that the content of the first array is equal to
+/// the true case array if the condition is true and
+/// the else case array otherwise.
+/// \param lhs: an expression
+/// \param expr: an if expression of type array
+void string_constraint_generatort::add_axioms_for_if_array(
+  const exprt &lhs, const if_exprt &expr)
+{
+  PRECONDITION(lhs.type()==expr.type());
+  PRECONDITION(expr.type().id()==ID_array);
+  exprt t=expr.true_case();
+  exprt f=expr.false_case();
+  INVARIANT(t.type()==f.type(), "branches of if_exprt should have same type");
+  const array_typet &type=to_array_type(t.type());
+  const typet &index_type=type.size().type();
+  const exprt max_length=from_integer(max_string_length, index_type);
+
+  // We add axioms:
+  // a1 : forall qvar<max_length, cond => lhs[qvar] = t[qvar]
+  // a1 : forall qvar2<max_length, !cond => lhs[qvar] = f[qvar]
+  symbol_exprt qvar=fresh_univ_index("QA_array_if_true", index_type);
+  equal_exprt qequal(index_exprt(lhs, qvar), index_exprt(t, qvar));
+
+  // In case t is a constant array of fixed length is does not make sense
+  // to talk about indexes exceeding this length
+  exprt upper_bound_t=
+    (t.id()==ID_array)?from_integer(t.operands().size(), index_type):max_length;
+  string_constraintt a1(qvar, upper_bound_t, expr.cond(), qequal);
+  axioms.push_back(a1);
+
+  symbol_exprt qvar2=fresh_univ_index("QA_array_if_false", index_type);
+  equal_exprt qequal2(index_exprt(lhs, qvar2), index_exprt(f, qvar2));
+  // In case f is a constant array of fixed length is does not make sense
+  // to talk about indexes exceeding this length
+  exprt upper_bound_f=
+    (f.id()==ID_array)?from_integer(f.operands().size(), index_type):max_length;
+  string_constraintt a2(qvar2, upper_bound_f, not_exprt(expr.cond()), qequal2);
+  axioms.push_back(a2);
+}
+
 /// if a symbol representing a string is present in the symbol_to_string table,
 /// returns the corresponding string, if the symbol is not yet present, creates
 /// a new string with the correct type depending on whether the mode is java or

src/solvers/refinement/string_constraint_generator_main.cpp

@@ -218,16 +218,20 @@ bool string_refinementt::add_axioms_for_string_assigns(
       add_symbol_to_symbol_map(lhs, rhs);
       return false;
     }
-    else if(rhs.id() == ID_nondet_symbol)
+    else if(rhs.id()==ID_nondet_symbol)
     {
       add_symbol_to_symbol_map(
         lhs, generator.fresh_symbol("nondet_array", lhs.type()));
       return false;
     }
+    else if(rhs.id()==ID_if)
+    {
+      generator.add_axioms_for_if_array(lhs, to_if_expr(rhs));
+      return false;
+    }
     else
     {
-      debug() << "string_refinement warning: not handling char_array: "
-              << from_expr(ns, "", rhs) << eom;
+      warning() << "ignoring char array " << from_expr(ns, "", rhs) << eom;
       return true;
     }
   }
@@ -370,8 +374,8 @@ void string_refinementt::set_to(const exprt &expr, bool value)
 
     if(eq_expr.lhs().type()!=eq_expr.rhs().type())
     {
-      debug() << "(sr::set_to) WARNING: ignoring "
-              << from_expr(ns, "", expr) << " [inconsistent types]" << eom;
+      warning() << "ignoring " << from_expr(ns, "", expr)
+                << " [inconsistent types]" << eom;
       debug() << "lhs has type: " << eq_expr.lhs().type().pretty(12) << eom;
       debug() << "rhs has type: " << eq_expr.rhs().type().pretty(12) << eom;
       return;
@@ -392,8 +396,7 @@ void string_refinementt::set_to(const exprt &expr, bool value)
     // TODO: See if this happens at all.
     if(lhs.id()!=ID_symbol)
     {
-      debug() << "(sr::set_to) WARNING: ignoring "
-              << from_expr(ns, "", expr) << eom;
+      warning() << "ignoring " << from_expr(ns, "", expr) << eom;
       return;
     }
 
@@ -404,9 +407,8 @@ void string_refinementt::set_to(const exprt &expr, bool value)
          subst_rhs.type().id() != ID_array ||
          eq_expr.lhs().type().subtype() != subst_rhs.type().subtype())
       {
-        debug() << "(sr::set_to) WARNING: ignoring "
-                << from_expr(ns, "", expr) << " [inconsistent types after substitution]"
-                << eom;
+        warning() << "ignoring " << from_expr(ns, "", expr)
+                  << " [inconsistent types after substitution]" << eom;
         return;
       }
       else
@@ -857,9 +859,15 @@ exprt string_refinementt::substitute_array_with_expr(
 }
 
 /// create an equivalent expression where array accesses and 'with' expressions
-/// are replaced by 'if' expressions. e.g. for an array access arr[x], where:
-/// `arr := {12, 24, 48}` the constructed expression will be: `index==0 ? 12 :
-/// index==1 ? 24 : 48`
+/// are replaced by 'if' expressions, in particular:
+///  * for an array access `arr[x]`, where:
+///    `arr := {12, 24, 48}` the constructed expression will be:
+///    `index==0 ? 12 : index==1 ? 24 : 48`
+///  * for an array access `arr[x]`, where:
+///    `arr := array_of(12) with {0:=24} with {2:=42}` the constructed
+///    expression will be: `index==0 ? 24 : index==2 ? 42 : 12`
+///  * for an array access `(g1?arr1:arr2)[x]` where `arr1 := {12}` and
+///    `arr2 := {34}`, the constructed expression will be: `g1 ? 12 : 34`
 /// \param expr: an expression containing array accesses
 /// \return an expression containing no array access
 void string_refinementt::substitute_array_access(exprt &expr) const
@@ -890,6 +898,18 @@ void string_refinementt::substitute_array_access(exprt &expr) const
       return;
     }
 
+    if(index_expr.array().id()==ID_if)
+    {
+      // Substitute recursively in branches of conditional expressions
+      if_exprt if_expr=to_if_expr(index_expr.array());
+      exprt true_case=index_exprt(if_expr.true_case(), index_expr.index());
+      substitute_array_access(true_case);
+      exprt false_case=index_exprt(if_expr.false_case(), index_expr.index());
+      substitute_array_access(false_case);
+      expr=if_exprt(if_expr.cond(), true_case, false_case);
+      return;
+    }
+
     assert(index_expr.array().id()==ID_array);
     array_exprt &array_expr=to_array_expr(index_expr.array());