Fixed universal constraints that break invariants.

In preparation for checking the invariant of universal constraints, all violations have been fixed. Additionally, an `indexOf` axiom had an off-by-one error and the contains regression test was missing a `--string-max-length`.

Author: jasigal

regression/strings-smoke-tests/java_case/test_case.class

@@ -1,6 +1,6 @@
 CORE
 test_contains.class
---refine-strings
+--refine-strings --string-max-length 100
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* SUCCESS$

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

@@ -15,7 +15,7 @@ Author: Romain Brenguier, [email protected]
 #include <solvers/refinement/string_constraint_generator.h>
 
 /// Add axioms stating that the returned value is the index within str of the
-/// first occurence of c starting the search at from_index, or -1 if no such
+/// first occurrence of c starting the search at from_index, or -1 if no such
 /// character occurs at or after position from_index.
 /// \param str: a string expression
 /// \param c: an expression representing a character
@@ -69,7 +69,7 @@ exprt string_constraint_generatort::add_axioms_for_index_of(
 }
 
 /// Add axioms stating that the returned value is the index within haystack of
-/// the first occurence of needle starting the search at from_index, or -1 if
+/// the first occurrence of needle starting the search at from_index, or -1 if
 /// needle does not occur at or after position from_index.
 /// \param haystack: a string expression
 /// \param needle: a string expression
@@ -92,7 +92,7 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string(
   //        contains ==> haystack[n+offset]=needle[n]
   // a4 : forall n:[from_index,offset[.
   //        contains ==> (exists m:[0,|needle|[. haystack[m+n] != needle[m]])
-  // a5:  forall n:[from_index,|haystack|-|needle|[.
+  // a5:  forall n:[from_index,|haystack|-|needle|].
   //        !contains ==> (exists m:[0,|needle|[. haystack[m+n] != needle[m])
 
   implies_exprt a1(
@@ -116,70 +116,35 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string(
     equal_exprt(haystack[plus_exprt(qvar, offset)], needle[qvar]));
   axioms.push_back(a3);
 
-  if(!is_constant_string(needle))
-  {
-    // string_not contains_constraintt are formulas of the form:
-    // forall x in [lb,ub[. p(x) => exists y in [lb,ub[. s1[x+y] != s2[y]
-    string_not_contains_constraintt a4(
-      from_index,
-      offset,
-      contains,
-      from_integer(0, index_type),
-      needle.length(),
-      haystack,
-      needle);
-    axioms.push_back(a4);
-
-    string_not_contains_constraintt a5(
-      from_index,
+  // string_not contains_constraintt are formulas of the form:
+  // forall x in [lb,ub[. p(x) => exists y in [lb,ub[. s1[x+y] != s2[y]
+  string_not_contains_constraintt a4(
+    from_index,
+    offset,
+    contains,
+    from_integer(0, index_type),
+    needle.length(),
+    haystack,
+    needle);
+  axioms.push_back(a4);
+
+  string_not_contains_constraintt a5(
+    from_index,
+    plus_exprt( // Add 1 for inclusive upper bound.
       minus_exprt(haystack.length(), needle.length()),
-      not_exprt(contains),
-      from_integer(0, index_type),
-      needle.length(),
-      haystack,
-      needle);
-    axioms.push_back(a5);
-  }
-  else
-  {
-    // Unfold the existential quantifier as a disjunction in case of a constant
-    // a4 && a5 <=> a6:
-    //  forall n:[from_index,|haystack|-|needle|].
-    //    !contains || n < offset ==>
-    //      haystack[n] != needle[0] || ... ||
-    //      haystack[n+|needle|-1] != needle[|needle|-1]
-    symbol_exprt qvar2=fresh_univ_index("QA_index_of_string_2", index_type);
-    mp_integer sub_length;
-    INVARIANT(
-      !to_integer(needle.length(), sub_length),
-      string_refinement_invariantt("a constant string must have constant "
-        "length"));
-    exprt::operandst disjuncts;
-    for(mp_integer offset=0; offset<sub_length; ++offset)
-    {
-      exprt expr_offset=from_integer(offset, index_type);
-      plus_exprt shifted(expr_offset, qvar2);
-      disjuncts.push_back(
-        not_exprt(equal_exprt(haystack[shifted], needle[expr_offset])));
-    }
-
-    or_exprt premise(
-      not_exprt(contains), binary_relation_exprt(qvar2, ID_lt, offset));
-    minus_exprt length_diff(haystack.length(), needle.length());
-    string_constraintt a6(
-      qvar2,
-      from_index,
-      plus_exprt(from_integer(1, index_type), length_diff),
-      premise,
-      disjunction(disjuncts));
-    axioms.push_back(a6);
-  }
+      from_integer(1, index_type)),
+    not_exprt(contains),
+    from_integer(0, index_type),
+    needle.length(),
+    haystack,
+    needle);
+  axioms.push_back(a5);
 
   return offset;
 }
 
 /// Add axioms stating that the returned value is the index within haystack of
-/// the last occurence of needle starting the search backward at from_index (ie
+/// the last occurrence of needle starting the search backward at from_index (ie
 /// the index is smaller or equal to from_index), or -1 if needle does not occur
 /// before from_index.
 /// \param haystack: a string expression
@@ -235,62 +200,25 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of_string(
     from_index,
     length_diff);
 
-  if(!is_constant_string(needle))
-  {
-    string_not_contains_constraintt a4(
-      plus_exprt(offset, from_integer(1, index_type)),
-      plus_exprt(end_index, from_integer(1, index_type)),
-      contains,
-      from_integer(0, index_type),
-      needle.length(),
-      haystack,
-      needle);
-    axioms.push_back(a4);
-
-    string_not_contains_constraintt a5(
-      from_integer(0, index_type),
-      plus_exprt(end_index, from_integer(1, index_type)),
-      not_exprt(contains),
-      from_integer(0, index_type),
-      needle.length(),
-      haystack,
-      needle);
-    axioms.push_back(a5);
-  }
-  else
-  {
-    // Unfold the existential quantifier as a disjunction in case of a constant
-    // a4 && a5 <=> a6:
-    //  forall n:[0, min(from_index, |haystack| - |needle|)].
-    //    !contains || (n > offset) ==>
-    //      haystack[n] != needle[0] || ... ||
-    //      haystack[n+|needle|-1] != needle[|needle|-1]
-    symbol_exprt qvar2=fresh_univ_index("QA_index_of_string_2", index_type);
-    mp_integer sub_length;
-    INVARIANT(
-      !to_integer(needle.length(), sub_length),
-      string_refinement_invariantt("a constant string must have constant "
-        "length"));
-    exprt::operandst disjuncts;
-    for(mp_integer offset=0; offset<sub_length; ++offset)
-    {
-      exprt expr_offset=from_integer(offset, index_type);
-      plus_exprt shifted(expr_offset, qvar2);
-      disjuncts.push_back(
-        not_exprt(equal_exprt(haystack[shifted], needle[expr_offset])));
-    }
-
-    or_exprt premise(
-      not_exprt(contains), binary_relation_exprt(qvar2, ID_gt, offset));
-
-    string_constraintt a6(
-      qvar2,
-      from_integer(0, index_type),
-      plus_exprt(from_integer(1, index_type), end_index),
-      premise,
-      disjunction(disjuncts));
-    axioms.push_back(a6);
-  }
+  string_not_contains_constraintt a4(
+    plus_exprt(offset, from_integer(1, index_type)),
+    plus_exprt(end_index, from_integer(1, index_type)),
+    contains,
+    from_integer(0, index_type),
+    needle.length(),
+    haystack,
+    needle);
+  axioms.push_back(a4);
+
+  string_not_contains_constraintt a5(
+    from_integer(0, index_type),
+    plus_exprt(end_index, from_integer(1, index_type)),
+    not_exprt(contains),
+    from_integer(0, index_type),
+    needle.length(),
+    haystack,
+    needle);
+  axioms.push_back(a5);
 
   return offset;
 }
@@ -333,7 +261,7 @@ exprt string_constraint_generatort::add_axioms_for_index_of(
 }
 
 /// Add axioms stating that the returned value is the index within str of the
-/// last occurence of c starting the search backward at from_index, or -1 if no
+/// last occurrence of c starting the search backward at from_index, or -1 if no
 /// such character occurs at or before position from_index.
 /// \param str: a string expression
 /// \param c: an expression representing a character
@@ -373,7 +301,7 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of(
       equal_exprt(str[index], c)));
   axioms.push_back(a3);
 
-  symbol_exprt n=fresh_univ_index("QA_last_index_of", index_type);
+  symbol_exprt n=fresh_univ_index("QA_last_index_of1", index_type);
   string_constraintt a4(
     n,
     plus_exprt(index, index1),
@@ -382,7 +310,7 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of(
     not_exprt(equal_exprt(str[n], c)));
   axioms.push_back(a4);
 
-  symbol_exprt m=fresh_univ_index("QA_last_index_of", index_type);
+  symbol_exprt m=fresh_univ_index("QA_last_index_of2", index_type);
   string_constraintt a5(
     m,
     from_index_plus_one,

src/solvers/refinement/string_constraint_generator_indexof.cpp

@@ -164,7 +164,6 @@ string_exprt string_constraint_generatort::convert_java_string_to_string_exprt(
   {
     java_content=dereference_exprt(java_content, java_content.type());
   }
-
   refined_string_typet type(java_int_type(), java_char_type());
 
   return string_exprt(length, java_content, type);

src/solvers/refinement/string_constraint_generator_main.cpp

@@ -187,7 +187,6 @@ exprt string_constraint_generatort::add_axioms_for_contains(
   PRECONDITION(f.type()==bool_typet() || f.type().id()==ID_c_bool);
   string_exprt s0=get_string_expr(args(f, 2)[0]);
   string_exprt s1=get_string_expr(args(f, 2)[1]);
-  bool constant=is_constant_string(s1);
 
   symbol_exprt contains=fresh_boolean("contains");
   const refined_string_typet ref_type=to_refined_string_type(s0.type());
@@ -218,66 +217,24 @@ exprt string_constraint_generatort::add_axioms_for_contains(
     equal_exprt(startpos, from_integer(-1, index_type)));
   axioms.push_back(a3);
 
-  if(constant)
-  {
-    // If the string is constant, we can use a more efficient axiom for a4:
-    // contains ==> AND_{i < |s1|} s1[i] = s0[startpos + i]
-    mp_integer s1_length;
-    INVARIANT(
-      !to_integer(s1.length(), s1_length),
-      string_refinement_invariantt("a constant string expression must have a "
-        "constant length"));
-    exprt::operandst conjuncts;
-    for(mp_integer i=0; i<s1_length; ++i)
-    {
-      exprt expr_i=from_integer(i, index_type);
-      plus_exprt shifted_i(expr_i, startpos);
-      conjuncts.push_back(equal_exprt(s1[expr_i], s0[shifted_i]));
-    }
-    implies_exprt a4(contains, conjunction(conjuncts));
-    axioms.push_back(a4);
-
-    // The a5 constraint for constant strings translates to:
-    // !contains ==> |s1| > |s0| ||
-    //               (forall qvar <= |s0| - |s1|.
-    //                 !(AND_{i < |s1|} s1[i] == s0[i + qvar])
-    //
-    // which we implement as:
-    // forall qvar <= |s0| - |s1|.  (!contains && |s0| >= |s1|)
-    //     ==> !(AND_{i < |s1|} (s1[i] == s0[qvar+i]))
-    symbol_exprt qvar=fresh_univ_index("QA_contains_constant", index_type);
-    exprt::operandst conjuncts1;
-    for(mp_integer i=0; i<s1_length; ++i)
-    {
-      exprt expr_i=from_integer(i, index_type);
-      plus_exprt shifted_i(expr_i, qvar);
-      conjuncts1.push_back(equal_exprt(s1[expr_i], s0[shifted_i]));
-    }
-
-    string_constraintt a5(
-      qvar,
-      plus_exprt(from_integer(1, index_type), length_diff),
-      and_exprt(not_exprt(contains), s0.axiom_for_is_longer_than(s1)),
-      not_exprt(conjunction(conjuncts1)));
-    axioms.push_back(a5);
-  }
-  else
-  {
-    symbol_exprt qvar=fresh_univ_index("QA_contains", index_type);
-    exprt qvar_shifted=plus_exprt(qvar, startpos);
-    string_constraintt a4(
-      qvar, s1.length(), contains, equal_exprt(s1[qvar], s0[qvar_shifted]));
-    axioms.push_back(a4);
-
-    // We rewrite axiom a4 as:
-    // forall startpos <= |s0|-|s1|.  (!contains && |s0| >= |s1|)
-    //     ==> exists witness < |s1|. s1[witness] != s0[startpos+witness]
-    string_not_contains_constraintt a5(
-      from_integer(0, index_type),
-      plus_exprt(from_integer(1, index_type), length_diff),
-      and_exprt(not_exprt(contains), s0.axiom_for_is_longer_than(s1)),
-      from_integer(0, index_type), s1.length(), s0, s1);
-    axioms.push_back(a5);
-  }
+  symbol_exprt qvar=fresh_univ_index("QA_contains", index_type);
+  exprt qvar_shifted=plus_exprt(qvar, startpos);
+  string_constraintt a4(
+    qvar, s1.length(), contains, equal_exprt(s1[qvar], s0[qvar_shifted]));
+  axioms.push_back(a4);
+
+  // We rewrite axiom a4 as:
+  // forall startpos <= |s0|-|s1|.  (!contains && |s0| >= |s1|)
+  //     ==> exists witness < |s1|. s1[witness] != s0[startpos+witness]
+  string_not_contains_constraintt a5(
+    from_integer(0, index_type),
+    plus_exprt(from_integer(1, index_type), length_diff),
+    and_exprt(not_exprt(contains), s0.axiom_for_is_longer_than(s1)),
+    from_integer(0, index_type),
+    s1.length(),
+    s0,
+    s1);
+  axioms.push_back(a5);
+
   return typecast_exprt(contains, f.type());
 }

src/solvers/refinement/string_constraint_generator_testing.cpp

@@ -287,7 +287,6 @@ string_exprt string_constraint_generatort::add_axioms_for_to_upper_case(
   exprt char_a=constant_char('a', char_type);
   exprt char_A=constant_char('A', char_type);
   exprt char_z=constant_char('z', char_type);
-  exprt char_Z=constant_char('Z', char_type);
 
   // TODO: add support for locales using case mapping information
   // from the UnicodeData file.
@@ -296,21 +295,29 @@ string_exprt string_constraint_generatort::add_axioms_for_to_upper_case(
   // a1 : |res| = |str|
   // a2 : forall idx<str.length, 'a'<=str[idx]<='z' => res[idx]=str[idx]+'A'-'a'
   // a3 : forall idx<str.length, !('a'<=str[idx]<='z') => res[idx]=str[idx]
+  // Note that index expressions are only allowed in the body of universal
+  // axioms, so we use a trivial premise and push our premise into the body.
 
   exprt a1=res.axiom_for_has_same_length_as(str);
   axioms.push_back(a1);
 
-  symbol_exprt idx=fresh_univ_index("QA_upper_case", index_type);
+  symbol_exprt idx1=fresh_univ_index("QA_upper_case1", index_type);
   exprt is_lower_case=and_exprt(
-    binary_relation_exprt(char_a, ID_le, str[idx]),
-    binary_relation_exprt(str[idx], ID_le, char_z));
+    binary_relation_exprt(char_a, ID_le, str[idx1]),
+    binary_relation_exprt(str[idx1], ID_le, char_z));
   minus_exprt diff(char_A, char_a);
-  equal_exprt convert(res[idx], plus_exprt(str[idx], diff));
-  string_constraintt a2(idx, res.length(), is_lower_case, convert);
+  equal_exprt convert(res[idx1], plus_exprt(str[idx1], diff));
+  implies_exprt body1(is_lower_case, convert);
+  string_constraintt a2(idx1, res.length(), body1);
   axioms.push_back(a2);
 
-  equal_exprt eq(res[idx], str[idx]);
-  string_constraintt a3(idx, res.length(), not_exprt(is_lower_case), eq);
+  symbol_exprt idx2=fresh_univ_index("QA_upper_case2", index_type);
+  exprt is_not_lower_case=not_exprt(and_exprt(
+    binary_relation_exprt(char_a, ID_le, str[idx2]),
+    binary_relation_exprt(str[idx2], ID_le, char_z)));
+  equal_exprt eq(res[idx2], str[idx2]);
+  implies_exprt body2(is_not_lower_case, eq);
+  string_constraintt a3(idx2, res.length(), body2);
   axioms.push_back(a3);
   return res;
 }