Merge branch 'develop' of github.com:diffblue/cbmc into develop

Author: kroening

src/java_bytecode/character_refine_preprocess.cpp

@@ -581,7 +581,7 @@ codet character_refine_preprocesst::convert_is_identifier_ignorable_int(
 }
 
 /// Converts function call to an assignment of an expression corresponding to
-/// the java method Character.isIdeographic:(C)Z
+/// the java method Character.isIdeographic:(I)Z
 /// \param target: a position in a goto program
 codet character_refine_preprocesst::convert_is_ideographic(
   conversion_inputt &target)
@@ -753,7 +753,7 @@ codet character_refine_preprocesst::convert_is_lower_case_int(
 }
 
 /// Converts function call to an assignment of an expression corresponding to
-/// the java method Character.isLowSurrogate:(I)Z
+/// the java method Character.isLowSurrogate:(C)Z
 /// \param target: a position in a goto program
 codet character_refine_preprocesst::convert_is_low_surrogate(
   conversion_inputt &target)
@@ -1127,7 +1127,7 @@ exprt character_refine_preprocesst::expr_of_low_surrogate(
 }
 
 /// Converts function call to an assignment of an expression corresponding to
-/// the java method Character.lowSurrogate:(I)Z
+/// the java method Character.lowSurrogate:(I)C
 /// \param target: a position in a goto program
 codet character_refine_preprocesst::convert_low_surrogate(
   conversion_inputt &target)
@@ -1394,7 +1394,7 @@ void character_refine_preprocesst::initialize_conversion_table()
   //   "(Ljava.lang.CharSequence;I)I"
   // Not supported "java::java.lang.Character.codePointCount:([CII)I"
   // Not supported "java::java.lang.Character.codePointCount:"
-  //   "(Ljava.lang.CharSequence;I)I"
+  //   "(Ljava.lang.CharSequence;II)I"
   // Not supported "java::java.lang.Character.compareTo:"
   //   "(Ljava.lang.Character;)I"
 
@@ -1422,11 +1422,11 @@ void character_refine_preprocesst::initialize_conversion_table()
       &character_refine_preprocesst::convert_get_numeric_value_int;
   conversion_table["java::java.lang.Character.getType:(C)I"]=
       &character_refine_preprocesst::convert_get_type_char;
-  conversion_table["java::java.lang.Character.getType:(I)Z"]=
+  conversion_table["java::java.lang.Character.getType:(I)I"]=
       &character_refine_preprocesst::convert_get_type_int;
   conversion_table["java::java.lang.Character.hashCode:()I"]=
       &character_refine_preprocesst::convert_hash_code;
-  conversion_table["java::java.lang.Character.highSurrogate:(C)Z"]=
+  conversion_table["java::java.lang.Character.highSurrogate:(I)C"]=
       &character_refine_preprocesst::convert_high_surrogate;
   conversion_table["java::java.lang.Character.isAlphabetic:(I)Z"]=
       &character_refine_preprocesst::convert_is_alphabetic;
@@ -1446,7 +1446,7 @@ void character_refine_preprocesst::initialize_conversion_table()
       &character_refine_preprocesst::convert_is_identifier_ignorable_char;
   conversion_table["java::java.lang.Character.isIdentifierIgnorable:(I)Z"]=
       &character_refine_preprocesst::convert_is_identifier_ignorable_int;
-  conversion_table["java::java.lang.Character.isIdeographic:(C)Z"]=
+  conversion_table["java::java.lang.Character.isIdeographic:(I)Z"]=
       &character_refine_preprocesst::convert_is_ideographic;
   conversion_table["java::java.lang.Character.isISOControl:(C)Z"]=
       &character_refine_preprocesst::convert_is_ISO_control_char;
@@ -1476,7 +1476,7 @@ void character_refine_preprocesst::initialize_conversion_table()
       &character_refine_preprocesst::convert_is_lower_case_char;
   conversion_table["java::java.lang.Character.isLowerCase:(I)Z"]=
       &character_refine_preprocesst::convert_is_lower_case_int;
-  conversion_table["java::java.lang.Character.isLowSurrogate:(I)Z"]=
+  conversion_table["java::java.lang.Character.isLowSurrogate:(C)Z"]=
       &character_refine_preprocesst::convert_is_low_surrogate;
   conversion_table["java::java.lang.Character.isMirrored:(C)Z"]=
       &character_refine_preprocesst::convert_is_mirrored_char;
@@ -1516,7 +1516,7 @@ void character_refine_preprocesst::initialize_conversion_table()
       &character_refine_preprocesst::convert_is_whitespace_char;
   conversion_table["java::java.lang.Character.isWhitespace:(I)Z"]=
       &character_refine_preprocesst::convert_is_whitespace_int;
-  conversion_table["java::java.lang.Character.lowSurrogate:(I)Z"]=
+  conversion_table["java::java.lang.Character.lowSurrogate:(I)C"]=
       &character_refine_preprocesst::convert_is_low_surrogate;
 
   // Not supported "java::java.lang.Character.offsetByCodePoints:([CIIII)I"
@@ -1528,7 +1528,7 @@ void character_refine_preprocesst::initialize_conversion_table()
   conversion_table["java::java.lang.Character.toChars:(I)[C"]=
       &character_refine_preprocesst::convert_to_chars;
 
-  // Not supported "java::java.lang.Character.toChars:(I[CI])I"
+  // Not supported "java::java.lang.Character.toChars:(I[CI)I"
 
   conversion_table["java::java.lang.Character.toCodePoint:(CC)I"]=
       &character_refine_preprocesst::convert_to_code_point;

src/solvers/refinement/string_constraint_instantiation.cpp

@@ -11,61 +11,46 @@ Author: Jesse Sigal, jesse.sigal@diffblue.com
 
 #include <solvers/refinement/string_constraint_instantiation.h>
 
-#include <solvers/refinement/string_constraint.h>
-#include <solvers/refinement/string_constraint_generator.h>
-#include <solvers/refinement/string_refinement.h>
-
 /// Instantiates a quantified formula representing `not_contains` by
 /// substituting the quantifiers and generating axioms.
 /// \related string_refinementt
 /// \param [in] axiom: the axiom to instantiate
-/// \param [in] index_set0: the index set for `axiom.s0()`
-/// \param [in] index_set1: the index set for `axiom.s1()`
+/// \param [in] index_pairs: the pairs of indices to at which to instantiate
 /// \param [in] generator: generator to be used to get `axiom`'s witness
 /// \return the lemmas produced through instantiation
 std::vector<exprt> instantiate_not_contains(
   const string_not_contains_constraintt &axiom,
-  const std::set<exprt> &index_set0,
-  const std::set<exprt> &index_set1,
+  const std::set<std::pair<exprt, exprt>> &index_pairs,
   const string_constraint_generatort &generator)
 {
   std::vector<exprt> lemmas;
 
-  const string_exprt s0=to_string_expr(axiom.s0());
-  const string_exprt s1=to_string_expr(axiom.s1());
-
-  for(const auto &i0 : index_set0)
-    for(const auto &i1 : index_set1)
-    {
-      const minus_exprt val(i0, i1);
-      const exprt witness=generator.get_witness_of(axiom, val);
-      const and_exprt prem_and_is_witness(
-        axiom.premise(),
-        equal_exprt(witness, i1));
-
-      const not_exprt differ(equal_exprt(s0[i0], s1[i1]));
-      const implies_exprt lemma(prem_and_is_witness, differ);
-      lemmas.push_back(lemma);
-
-      // we put bounds on the witnesses:
-      // 0 <= v <= |s0| - |s1| ==> 0 <= v+w[v] < |s0| && 0 <= w[v] < |s1|
-      const exprt zero=from_integer(0, val.type());
-      const binary_relation_exprt c1(zero, ID_le, plus_exprt(val, witness));
-      const binary_relation_exprt c2(
-        s0.length(), ID_gt, plus_exprt(val, witness));
-      const binary_relation_exprt c3(s1.length(), ID_gt, witness);
-      const binary_relation_exprt c4(zero, ID_le, witness);
-
-      const minus_exprt diff(s0.length(), s1.length());
-
-      const and_exprt premise(
-        binary_relation_exprt(zero, ID_le, val),
-        binary_relation_exprt(diff, ID_ge, val));
-      const implies_exprt witness_bounds(
-        premise,
-        and_exprt(and_exprt(c1, c2), and_exprt(c3, c4)));
-      lemmas.push_back(witness_bounds);
-    }
+  const string_exprt &s0=to_string_expr(axiom.s0());
+  const string_exprt &s1=to_string_expr(axiom.s1());
+
+  for(const auto &pair : index_pairs)
+  {
+    // We have s0[x+f(x)] and s1[f(x)], so to have i0 indexing s0 and i1
+    // indexing s1, we need x = i0 - i1 and f(i0 - i1) = f(x) = i1.
+    const exprt &i0=pair.first;
+    const exprt &i1=pair.second;
+    const minus_exprt val(i0, i1);
+    const and_exprt universal_bound(
+      binary_relation_exprt(axiom.univ_lower_bound(), ID_le, val),
+      binary_relation_exprt(axiom.univ_upper_bound(), ID_gt, val));
+    const exprt f=generator.get_witness_of(axiom, val);
+    const equal_exprt relevancy(f, i1);
+    const and_exprt premise(relevancy, axiom.premise(), universal_bound);
+
+    const notequal_exprt differ(s0[i0], s1[i1]);
+    const and_exprt existential_bound(
+      binary_relation_exprt(axiom.exists_lower_bound(), ID_le, i1),
+      binary_relation_exprt(axiom.exists_upper_bound(), ID_gt, i1));
+    const and_exprt body(differ, existential_bound);
+
+    const implies_exprt lemma(premise, body);
+    lemmas.push_back(lemma);
+  }
 
   return lemmas;
 }

src/solvers/refinement/string_constraint_instantiation.h

@@ -17,8 +17,7 @@ Author: Jesse Sigal, jesse.sigal@diffblue.com
 
 std::vector<exprt> instantiate_not_contains(
   const string_not_contains_constraintt &axiom,
-  const std::set<exprt> &index_set0,
-  const std::set<exprt> &index_set1,
+  const std::set<std::pair<exprt, exprt>> &index_pairs,
   const string_constraint_generatort &generator);
 
 #endif // CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_INSTANTIATION_H

src/solvers/refinement/string_refinement.cpp

@@ -99,6 +99,7 @@ static std::vector<exprt> instantiate_not_contains(
   const namespacet &ns,
   const string_not_contains_constraintt &axiom,
   const std::map<exprt, std::set<exprt>> &index_set,
+  const std::map<exprt, std::set<exprt>> &current_index_set,
   const string_constraint_generatort &generator);
 
 static exprt get_array(
@@ -850,7 +851,12 @@ decision_proceduret::resultt string_refinementt::dec_solve()
         debug() << "constraint " << i << '\n';
         const std::vector<exprt> lemmas=
           instantiate_not_contains(
-            debug(), ns, not_contains_axioms[i], index_set, generator);
+            debug(),
+            ns,
+            not_contains_axioms[i],
+            index_set,
+            current_index_set,
+            generator);
         for(const exprt &lemma : lemmas)
           add_lemma(lemma);
       }
@@ -1510,23 +1516,26 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
 
     if(use_counter_example)
     {
-      // TODO: add counter examples for not_contains?
+      stream << "Adding counter-examples: " << eom;
+      // TODO: add counter-examples for universal constraints?
 
-      // Checking if the current solution satisfies the constraints
       std::vector<exprt> lemmas;
-      for(const auto &v : violated)
+      for(const auto &v : violated_not_contains)
       {
         const exprt &val=v.second;
-        const string_constraintt &axiom=universal_axioms[v.first];
-
-        exprt premise(axiom.premise());
-        exprt body(axiom.body());
-        implies_exprt instance(premise, body);
-        replace_expr(symbol_resolve, instance);
-        replace_expr(axiom.univ_var(), val, instance);
-        stream << "adding counter example " << from_expr(ns, "", instance)
-               << eom;
-        lemmas.push_back(instance);
+        const string_not_contains_constraintt &axiom=
+          not_contains_axioms[v.first];
+
+        const exprt func_val=generator.get_witness_of(axiom, val);
+        const exprt comp_val=simplify_sum(plus_exprt(val, func_val));
+
+        std::set<std::pair<exprt, exprt>> indices;
+        indices.insert(std::pair<exprt, exprt>(comp_val, func_val));
+        const exprt counter=::instantiate_not_contains(
+          axiom, indices, generator)[0];
+
+        stream << "    -  " << from_expr(ns, "", counter) << eom;
+        lemmas.push_back(counter);
       }
       return { false, lemmas };
     }
@@ -1960,19 +1969,36 @@ static std::vector<exprt> instantiate_not_contains(
   const namespacet &ns,
   const string_not_contains_constraintt &axiom,
   const std::map<exprt, std::set<exprt>> &index_set,
+  const std::map<exprt, std::set<exprt>> &current_index_set,
   const string_constraint_generatort &generator)
 {
-  const string_exprt s0=to_string_expr(axiom.s0());
-  const string_exprt s1=to_string_expr(axiom.s1());
+  const string_exprt &s0=axiom.s0();
+  const string_exprt &s1=axiom.s1();
 
   stream << "instantiate not contains " << from_expr(ns, "", s0) << " : "
          << from_expr(ns, "", s1) << messaget::eom;
-  const auto &i0=index_set.find(s0.content());
-  const auto &i1=index_set.find(s1.content());
-  if(i0!=index_set.end() && i1!=index_set.end())
+
+  const auto &index_set0=index_set.find(s0.content());
+  const auto &index_set1=index_set.find(s1.content());
+  const auto &current_index_set0=current_index_set.find(s0.content());
+  const auto &current_index_set1=current_index_set.find(s1.content());
+
+  if(index_set0!=index_set.end() &&
+     index_set1!=index_set.end() &&
+     current_index_set0!=index_set.end() &&
+     current_index_set1!=index_set.end())
   {
-    return ::instantiate_not_contains(
-      axiom, i0->second, i1->second, generator);
+    typedef std::pair<exprt, exprt> expr_pairt;
+    std::set<expr_pairt> index_pairs;
+
+    for(const auto &ic0 : current_index_set0->second)
+      for(const auto &i1 : index_set1->second)
+        index_pairs.insert(expr_pairt(ic0, i1));
+    for(const auto &ic1 : current_index_set1->second)
+      for(const auto &i0 : index_set0->second)
+        index_pairs.insert(expr_pairt(i0, ic1));
+
+    return ::instantiate_not_contains(axiom, index_pairs, generator);
   }
   return { };
 }

src/solvers/refinement/string_refinement.h

@@ -39,7 +39,7 @@ class string_refinementt final: public bv_refinementt
     bool string_non_empty=false;
     /// Concretize strings after solver is finished
     bool trace=false;
-    bool use_counter_example=false;
+    bool use_counter_example=true;
   };
 public:
   /// string_refinementt constructor arguments