Merge pull request #6915 from tautschnig/bugfixes/use-bv_pointerst

String refinement: support pointers

Author: tautschnig

jbmc/regression/strings-smoke-tests/java_set_length/test.desc

@@ -8,3 +8,4 @@ test_set_length
 ^\[.*assertion.3\].* line 11.* FAILURE$
 --
 non equal types
+^warning: ignoring

jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp

@@ -218,7 +218,7 @@ SCENARIO(
       {ab, b, from_integer(2)}};
 
     // Generating the corresponding axioms and simplifying, recording info
-    string_constraint_generatort generator(empty_ns);
+    string_constraint_generatort generator(empty_ns, null_message_handler);
     const auto pair = generator.add_axioms_for_function_application(func);
     const string_constraintst &constraints = pair.second;
 
@@ -313,7 +313,7 @@ SCENARIO(
                                                      a_array};
 
     // Create witness for axiom
-    string_constraint_generatort generator(empty_ns);
+    string_constraint_generatort generator(empty_ns, null_message_handler);
     std::unordered_map<string_not_contains_constraintt, symbol_exprt> witnesses;
     witnesses.emplace(vacuous, generator.fresh_symbol("w", t.witness_type()));
 
@@ -363,7 +363,7 @@ SCENARIO(
                                                      b_array};
 
     // Create witness for axiom
-    string_constraint_generatort generator(empty_ns);
+    string_constraint_generatort generator(empty_ns, null_message_handler);
     std::unordered_map<string_not_contains_constraintt, symbol_exprt> witnesses;
     witnesses.emplace(trivial, generator.fresh_symbol("w", t.witness_type()));
 
@@ -414,7 +414,7 @@ SCENARIO(
                                                      empty_array};
 
     // Create witness for axiom
-    string_constraint_generatort generator(empty_ns);
+    string_constraint_generatort generator(empty_ns, null_message_handler);
     std::unordered_map<string_not_contains_constraintt, symbol_exprt> witnesses;
     witnesses.emplace(trivial, generator.fresh_symbol("w", t.witness_type()));
 
@@ -467,7 +467,7 @@ SCENARIO(
                                                      ab_array};
 
     // Create witness for axiom
-    string_constraint_generatort generator(empty_ns);
+    string_constraint_generatort generator(empty_ns, null_message_handler);
     std::unordered_map<string_not_contains_constraintt, symbol_exprt> witnesses;
     witnesses.emplace(trivial, generator.fresh_symbol("w", t.witness_type()));
 
@@ -518,7 +518,7 @@ SCENARIO(
                                                      cd_array};
 
     // Create witness for axiom
-    string_constraint_generatort generator(empty_ns);
+    string_constraint_generatort generator(empty_ns, null_message_handler);
     std::unordered_map<string_not_contains_constraintt, symbol_exprt> witnesses;
     witnesses.emplace(trivial, generator.fresh_symbol("w", t.witness_type()));
 

src/goto-instrument/wmm/goto2graph.cpp

@@ -1385,7 +1385,6 @@ bool instrumentert::is_cfg_spurious(const event_grapht::critical_cyclet &cyc)
   goto_functionst this_interleaving;
   this_interleaving.function_map=std::move(map);
   optionst no_option;
-  null_message_handlert no_message;
 
   #if 0
   bmct bmc(no_option, symbol_table, no_message);

src/solvers/README.md

@@ -461,8 +461,8 @@ This is described in more detail \link string_builtin_functiont here. \endlink
     \copybrief string_constraint_generatort::add_axioms_for_delete(const function_application_exprt &f)
     \link string_constraint_generatort::add_axioms_for_delete(const function_application_exprt &f) More... \endlink
   * `cprover_string_insert` :
-    \copybrief string_insertion_builtin_functiont::constraints(string_constraint_generatort &generator) const
-    \link string_insertion_builtin_functiont::constraints(string_constraint_generatort &generator) const More... \endlink
+    \copybrief string_insertion_builtin_functiont::constraints(string_constraint_generatort &generator, message_handlert &message_handler) const
+    \link string_insertion_builtin_functiont::constraints(string_constraint_generatort &generator, message_handlert &message_handler) const More... \endlink
   * `cprover_string_replace` :
     \copybrief string_constraint_generatort::add_axioms_for_replace(const function_application_exprt &f)
     \link string_constraint_generatort::add_axioms_for_replace(const function_application_exprt &f) More... \endlink

src/solvers/strings/string_builtin_function.cpp

@@ -101,7 +101,8 @@ optionalt<exprt> string_concat_char_builtin_functiont::eval(
 ///   * result[input.length] = character
 ///   * return_code = 0
 string_constraintst string_concat_char_builtin_functiont::constraints(
-  string_constraint_generatort &generator) const
+  string_constraint_generatort &generator,
+  message_handlert &message_handler) const
 {
   string_constraintst constraints;
   constraints.existential.push_back(length_constraint());
@@ -111,7 +112,7 @@ string_constraintst string_concat_char_builtin_functiont::constraints(
     const exprt upper_bound =
       zero_if_negative(array_pool.get_or_create_length(input));
     return string_constraintt(
-      idx, upper_bound, equal_exprt(input[idx], result[idx]));
+      idx, upper_bound, equal_exprt(input[idx], result[idx]), message_handler);
   }());
   constraints.existential.push_back(
     equal_exprt(result[array_pool.get_or_create_length(input)], character));
@@ -151,7 +152,8 @@ optionalt<exprt> string_set_char_builtin_functiont::eval(
 ///   3. forall 0 <= i < max(0, min(res.length, pos)). res[i] = str[i]
 ///   4. forall max(0, pos+1) <= i < res.length. res[i] = str[i]
 string_constraintst string_set_char_builtin_functiont::constraints(
-  string_constraint_generatort &generator) const
+  string_constraint_generatort &generator,
+  message_handlert &message_handler) const
 {
   string_constraintst constraints;
   constraints.existential.push_back(length_constraint());
@@ -169,7 +171,8 @@ string_constraintst string_set_char_builtin_functiont::constraints(
       q,
       zero_if_negative(
         minimum(array_pool.get_or_create_length(result), position)),
-      a3_body);
+      a3_body,
+      message_handler);
   }());
   constraints.universal.push_back([&] {
     const symbol_exprt q2 =
@@ -179,7 +182,8 @@ string_constraintst string_set_char_builtin_functiont::constraints(
       q2,
       zero_if_negative(plus_exprt(position, from_integer(1, position.type()))),
       zero_if_negative(array_pool.get_or_create_length(result)),
-      a4_body);
+      a4_body,
+      message_handler);
   }());
   return constraints;
 }
@@ -279,7 +283,8 @@ static exprt is_lower_case(const exprt &character)
 /// characters: `diff = 'a'-'A' = 0x20` and `is_upper_case` is true for the
 /// upper case characters of Basic Latin and Latin-1 supplement of unicode.
 string_constraintst string_to_lower_case_builtin_functiont::constraints(
-  string_constraint_generatort &generator) const
+  string_constraint_generatort &generator,
+  message_handlert &message_handler) const
 {
   // \todo for now, only characters in Basic Latin and Latin-1 supplement
   // are supported (up to 0x100), we should add others using case mapping
@@ -302,7 +307,8 @@ string_constraintst string_to_lower_case_builtin_functiont::constraints(
     return string_constraintt(
       idx,
       zero_if_negative(array_pool.get_or_create_length(result)),
-      conditional_convert);
+      conditional_convert,
+      message_handler);
   }());
   return constraints;
 }
@@ -332,9 +338,11 @@ optionalt<exprt> string_to_upper_case_builtin_functiont::eval(
 ///        is_lower_case(str[i]) ? res[i] = str[i] - 0x20 : res[i] = str[i]
 ///
 /// \param fresh_symbol: generator of fresh symbols
+/// \param message_handler: message handler
 /// \return set of constraints
 string_constraintst string_to_upper_case_builtin_functiont::constraints(
-  symbol_generatort &fresh_symbol) const
+  symbol_generatort &fresh_symbol,
+  message_handlert &message_handler) const
 {
   string_constraintst constraints;
   constraints.existential.push_back(length_constraint());
@@ -350,7 +358,8 @@ string_constraintst string_to_upper_case_builtin_functiont::constraints(
       zero_if_negative(array_pool.get_or_create_length(result)),
       equal_exprt(
         result[idx],
-        if_exprt(is_lower_case(input[idx]), converted, input[idx])));
+        if_exprt(is_lower_case(input[idx]), converted, input[idx])),
+      message_handler);
   }());
   return constraints;
 }
@@ -406,7 +415,8 @@ optionalt<exprt> string_of_int_builtin_functiont::eval(
 }
 
 string_constraintst string_of_int_builtin_functiont::constraints(
-  string_constraint_generatort &generator) const
+  string_constraint_generatort &generator,
+  message_handlert &message_handler) const
 {
   auto pair =
     generator.add_axioms_for_string_of_int_with_radix(result, arg, radix, 0);
@@ -475,7 +485,8 @@ string_builtin_function_with_no_evalt::string_builtin_function_with_no_evalt(
 }
 
 string_constraintst string_builtin_function_with_no_evalt::constraints(
-  string_constraint_generatort &generator) const
+  string_constraint_generatort &generator,
+  message_handlert &message_handler) const
 {
   auto pair =
     generator.add_axioms_for_function_application(function_application);

src/solvers/strings/string_builtin_function.h

@@ -102,7 +102,7 @@ class string_builtin_functiont
   /// the result of this function.
   /// This logic is implemented in add_constraints().
   virtual string_constraintst
-  constraints(string_constraint_generatort &constraint_generator) const = 0;
+  constraints(string_constraint_generatort &, message_handlert &) const = 0;
 
   /// Constraint ensuring that the length of the strings are coherent with
   /// the function call.
@@ -198,8 +198,9 @@ class string_concat_char_builtin_functiont
     return "concat_char";
   }
 
-  string_constraintst
-  constraints(string_constraint_generatort &generator) const override;
+  string_constraintst constraints(
+    string_constraint_generatort &generator,
+    message_handlert &message_handlert) const override;
 
   exprt length_constraint() const override;
 };
@@ -235,8 +236,9 @@ class string_set_char_builtin_functiont
     return "set_char";
   }
 
-  string_constraintst
-  constraints(string_constraint_generatort &generator) const override;
+  string_constraintst constraints(
+    string_constraint_generatort &generator,
+    message_handlert &message_handler) const override;
 
   // \todo: length_constraint is not the best possible name because we also
   // \todo: add constraint about the return code
@@ -265,8 +267,9 @@ class string_to_lower_case_builtin_functiont
     return "to_lower_case";
   }
 
-  string_constraintst
-  constraints(string_constraint_generatort &generator) const override;
+  string_constraintst constraints(
+    string_constraint_generatort &generator,
+    message_handlert &message_handler) const override;
 
   exprt length_constraint() const override
   {
@@ -313,12 +316,15 @@ class string_to_upper_case_builtin_functiont
     return "to_upper_case";
   }
 
-  string_constraintst constraints(class symbol_generatort &fresh_symbol) const;
+  string_constraintst constraints(
+    class symbol_generatort &fresh_symbol,
+    message_handlert &message_handler) const;
 
-  string_constraintst
-  constraints(string_constraint_generatort &generator) const override
+  string_constraintst constraints(
+    string_constraint_generatort &generator,
+    message_handlert &message_handler) const override
   {
-    return constraints(generator.fresh_symbol);
+    return constraints(generator.fresh_symbol, message_handler);
   };
 
   exprt length_constraint() const override
@@ -379,8 +385,9 @@ class string_of_int_builtin_functiont : public string_creation_builtin_functiont
     return "string_of_int";
   }
 
-  string_constraintst
-  constraints(string_constraint_generatort &generator) const override;
+  string_constraintst constraints(
+    string_constraint_generatort &generator,
+    message_handlert &message_handler) const override;
 
   exprt length_constraint() const override;
 
@@ -439,8 +446,9 @@ class string_builtin_function_with_no_evalt : public string_builtin_functiont
     return {};
   }
 
-  string_constraintst
-  constraints(string_constraint_generatort &generator) const override;
+  string_constraintst constraints(
+    string_constraint_generatort &generator,
+    message_handlert &message_handler) const override;
 
   exprt length_constraint() const override
   {

src/solvers/strings/string_concatenation_builtin_function.cpp

@@ -73,7 +73,8 @@ string_constraint_generatort::add_axioms_for_concat_substr(
     return string_constraintt(
       idx,
       zero_if_negative(array_pool.get_or_create_length(s1)),
-      equal_exprt(s1[idx], res[idx]));
+      equal_exprt(s1[idx], res[idx]),
+      message_handler);
   }());
 
   // Axiom 3.
@@ -86,7 +87,8 @@ string_constraint_generatort::add_axioms_for_concat_substr(
     const minus_exprt upper_bound(
       array_pool.get_or_create_length(res),
       array_pool.get_or_create_length(s1));
-    return string_constraintt(idx2, zero_if_negative(upper_bound), res_eq);
+    return string_constraintt(
+      idx2, zero_if_negative(upper_bound), res_eq, message_handler);
   }());
 
   return {from_integer(0, get_return_code_type()), std::move(constraints)};
@@ -208,7 +210,8 @@ std::vector<mp_integer> string_concatenation_builtin_functiont::eval(
 }
 
 string_constraintst string_concatenation_builtin_functiont::constraints(
-  string_constraint_generatort &generator) const
+  string_constraint_generatort &generator,
+  message_handlert &message_handler) const
 
 {
   auto pair = [&]() -> std::pair<exprt, string_constraintst> {

src/solvers/strings/string_concatenation_builtin_function.h

@@ -39,8 +39,9 @@ class string_concatenation_builtin_functiont final
     return "concat";
   }
 
-  string_constraintst
-  constraints(string_constraint_generatort &generator) const override;
+  string_constraintst constraints(
+    string_constraint_generatort &generator,
+    message_handlert &message_handler) const override;
 
   exprt length_constraint() const override;
 };

src/solvers/strings/string_constraint.cpp

@@ -11,21 +11,20 @@ Author: Diffblue Ltd.
 #include <util/namespace.h>
 #include <util/symbol_table.h>
 
-#include <solvers/flattening/boolbv.h>
+#include <solvers/flattening/bv_pointers.h>
 #include <solvers/sat/satcheck.h>
 
 /// Runs a solver instance to verify whether an expression can only be
 /// non-negative.
 /// \param expr: the expression to check for negativity
+/// \param message_handler: message handler
 /// \return true if `expr < 0` is unsatisfiable, false otherwise
-static bool cannot_be_neg(const exprt &expr)
+static bool cannot_be_neg(const exprt &expr, message_handlert &message_handler)
 {
-  // this is an internal check, no need for user visibility
-  null_message_handlert null_message_handler;
-  satcheck_no_simplifiert sat_check(null_message_handler);
+  satcheck_no_simplifiert sat_check(message_handler);
   symbol_tablet symbol_table;
   namespacet ns(symbol_table);
-  boolbvt solver{ns, sat_check, null_message_handler};
+  bv_pointerst solver{ns, sat_check, message_handler};
   const exprt zero = from_integer(0, expr.type());
   const binary_relation_exprt non_neg(expr, ID_lt, zero);
   solver << non_neg;
@@ -36,18 +35,19 @@ string_constraintt::string_constraintt(
   const symbol_exprt &_univ_var,
   const exprt &lower_bound,
   const exprt &upper_bound,
-  const exprt &body)
+  const exprt &body,
+  message_handlert &message_handler)
   : univ_var(_univ_var),
     lower_bound(lower_bound),
     upper_bound(upper_bound),
     body(body)
 {
   INVARIANT(
-    cannot_be_neg(lower_bound),
+    cannot_be_neg(lower_bound, message_handler),
     "String constraints must have non-negative lower bound.\n" +
       lower_bound.pretty());
   INVARIANT(
-    cannot_be_neg(upper_bound),
+    cannot_be_neg(upper_bound, message_handler),
     "String constraints must have non-negative upper bound.\n" +
       upper_bound.pretty());
 }