Bug corrections in string refinement

Case of array-of in substitute array access
making substitute_array_access do in-place substitution
Setting the type for unknown values in substitute_array_access
Unknown values could cause type problems if we do not force the type
for them.

Setting ui for temporary solver

Remove the mode option from string solver

This option is no longer requiered because the implementation is now
language independent.

Adapt add_axioms_for_insert for 5 arguments #110

Fixed linting issue in string_constraint_generator_concat.cpp

Comment on the maximal length for string

Using max_string_length as the limit for refinement

Using unsigned type for max string length

Using const ref in substitute_array_with_expr

Correcting type of max_string_length and length comparison functions

space before & sign instead of after

Correcting initial_loop_bound type

Putting each cbmc option on a  separate line for easy merging

Use size_t for string sizes

Add comment in concretize_string

Author: romainbrenguier

src/cbmc/cbmc_parse_options.h

@@ -41,7 +41,10 @@ class optionst;
   "(no-sat-preprocessor)" \
   "(no-pretty-names)(beautify)" \
   "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\
-  "(refine-strings)(string-non-empty)(string-printable)(string-max-length):" \
+  "(refine-strings)" \
+  "(string-non-empty)" \
+  "(string-printable)" \
+  "(string-max-length):" \
   "(aig)(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
   "(little-endian)(big-endian)" \
   "(show-goto-functions)(show-loops)" \

src/solvers/refinement/string_constraint_generator.h

@@ -20,6 +20,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 #ifndef CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_GENERATOR_H
 #define CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_GENERATOR_H
 
+#include <limits>
 #include <util/string_expr.h>
 #include <util/replace_expr.h>
 #include <util/refined_string_type.h>
@@ -29,30 +30,20 @@ class string_constraint_generatort
 {
 public:
   // This module keeps a list of axioms. It has methods which generate
-  // string constraints for different string funcitons and add them
+  // string constraints for different string functions and add them
   // to the axiom list.
 
   string_constraint_generatort():
-    mode(ID_unknown),
-    max_string_length(-1),
+    max_string_length(std::numeric_limits<size_t>::max()),
     force_printable_characters(false)
   { }
 
   // Constraints on the maximal length of strings
-  int max_string_length;
+  size_t max_string_length;
 
   // Should we add constraints on the characters
   bool force_printable_characters;
 
-  void set_mode(irep_idt _mode)
-  {
-    // only C and java modes supported
-    assert((_mode==ID_java) || (_mode==ID_C));
-    mode=_mode;
-  }
-
-  irep_idt &get_mode() { return mode; }
-
   // Axioms are of three kinds: universally quantified string constraint,
   // not contains string constraints and simple formulas.
   std::list<exprt> axioms;

src/solvers/refinement/string_constraint_generator_concat.cpp

@@ -30,7 +30,8 @@ string_exprt string_constraint_generatort::add_axioms_for_concat(
   // a4 : forall i<|s1|. res[i]=s1[i]
   // a5 : forall i<|s2|. res[i+|s1|]=s2[i]
 
-  equal_exprt a1(res.length(), plus_exprt_with_overflow_check(s1.length(), s2.length()));
+  equal_exprt a1(
+    res.length(), plus_exprt_with_overflow_check(s1.length(), s2.length()));
   axioms.push_back(a1);
   axioms.push_back(s1.axiom_for_is_shorter_than(res));
   axioms.push_back(s2.axiom_for_is_shorter_than(res));

src/solvers/refinement/string_constraint_generator_insert.cpp

@@ -26,16 +26,30 @@ string_exprt string_constraint_generatort::add_axioms_for_insert(
   return add_axioms_for_concat(concat1, suf);
 }
 
-/// add axioms corresponding to the StringBuilder.insert(String) java function
+/// add axioms corresponding to the StringBuilder.insert(int, CharSequence) and
+/// StringBuilder.insert(int, CharSequence, int, int) java functions
 /// \par parameters: function application with three arguments: two strings and
 ///   an index
 /// \return a new string expression
 string_exprt string_constraint_generatort::add_axioms_for_insert(
   const function_application_exprt &f)
 {
-  string_exprt s1=get_string_expr(args(f, 3)[0]);
-  string_exprt s2=get_string_expr(args(f, 3)[2]);
-  return add_axioms_for_insert(s1, s2, args(f, 3)[1]);
+  assert(f.arguments().size()>=3);
+  string_exprt s1=get_string_expr(f.arguments()[0]);
+  string_exprt s2=get_string_expr(f.arguments()[2]);
+  const exprt &offset=f.arguments()[1];
+  if(f.arguments().size()==5)
+  {
+    const exprt &start=f.arguments()[3];
+    const exprt &end=f.arguments()[4];
+    string_exprt substring=add_axioms_for_substring(s2, start, end);
+    return add_axioms_for_insert(s1, substring, offset);
+  }
+  else
+  {
+    assert(f.arguments().size()==3);
+    return add_axioms_for_insert(s1, s2, offset);
+  }
 }
 
 /// add axioms corresponding to the StringBuilder.insert(I) java function

src/solvers/refinement/string_constraint_generator_main.cpp

@@ -149,7 +149,6 @@ string_exprt string_constraint_generatort::get_string_expr(const exprt &expr)
 string_exprt string_constraint_generatort::convert_java_string_to_string_exprt(
     const exprt &jls)
 {
-  assert(get_mode()==ID_java);
   assert(jls.id()==ID_struct);
 
   exprt length(to_struct_expr(jls).op1());
@@ -319,7 +318,6 @@ exprt string_constraint_generatort::add_axioms_for_function_application(
     // TODO: This part needs some improvement.
     // Stripping the symbol name is not a very robust process.
     new_expr.function() = symbol_exprt(str_id.substr(0, pos+4));
-    assert(get_mode()==ID_java);
     new_expr.type() = refined_string_typet(java_int_type(), java_char_type());
 
     auto res_it=function_application_cache.insert(std::make_pair(new_expr,

src/solvers/refinement/string_refinement.cpp

@@ -287,16 +287,18 @@ void string_refinementt::concretize_string(const exprt &expr)
     if(!to_integer(length, found_length))
     {
       assert(found_length.is_long());
-      if(found_length < 0)
+      if(found_length<0)
       {
+        // Lengths should not be negative.
+        // TODO: Add constraints no the sign of string lengths.
         debug() << "concretize_results: WARNING found length is negative"
                 << eom;
       }
       else
       {
         size_t concretize_limit=found_length.to_long();
-        concretize_limit=concretize_limit>MAX_CONCRETE_STRING_SIZE?
-              MAX_CONCRETE_STRING_SIZE:concretize_limit;
+        concretize_limit=concretize_limit>generator.max_string_length?
+              generator.max_string_length:concretize_limit;
         exprt content_expr=str.content();
         for(size_t i=0; i<concretize_limit; ++i)
         {
@@ -316,9 +318,9 @@ void string_refinementt::concretize_string(const exprt &expr)
 /// map `found_length`
 void string_refinementt::concretize_results()
 {
-  for(const auto& it : symbol_resolve)
+  for(const auto &it : symbol_resolve)
     concretize_string(it.second);
-  for(const auto& it : generator.created_strings)
+  for(const auto &it : generator.created_strings)
     concretize_string(it);
   add_instantiations();
 }
@@ -327,7 +329,7 @@ void string_refinementt::concretize_results()
 /// `found_length`
 void string_refinementt::concretize_lengths()
 {
-  for(const auto& it : symbol_resolve)
+  for(const auto &it : symbol_resolve)
   {
     if(refined_string_typet::is_refined_string_type(it.second.type()))
     {
@@ -338,7 +340,7 @@ void string_refinementt::concretize_lengths()
       found_length[content]=length;
      }
   }
-  for(const auto& it : generator.created_strings)
+  for(const auto &it : generator.created_strings)
   {
     if(refined_string_typet::is_refined_string_type(it.type()))
     {
@@ -357,12 +359,6 @@ void string_refinementt::set_to(const exprt &expr, bool value)
 {
   assert(equality_propagation);
 
-  // TODO: remove the mode field of generator since we should be language
-  // independent.
-  // We only set the mode once.
-  if(generator.get_mode()==ID_unknown)
-    set_mode();
-
   if(expr.id()==ID_equal)
   {
     equal_exprt eq_expr=to_equal_expr(expr);
@@ -620,7 +616,7 @@ exprt string_refinementt::get_array(const exprt &arr, const exprt &size) const
   array_typet ret_type(char_type, from_integer(n, index_type));
   array_exprt ret(ret_type);
 
-  if(n>MAX_CONCRETE_STRING_SIZE)
+  if(n>generator.max_string_length)
   {
 #if 0
     debug() << "(sr::get_array) long string (size=" << n << ")" << eom;
@@ -1006,6 +1002,7 @@ exprt string_refinementt::negation_of_constraint(
   and_exprt negaxiom(premise, not_exprt(axiom.body()));
 
   debug() << "(sr::check_axioms) negated axiom: " << from_expr(negaxiom) << eom;
+  substitute_array_access(negaxiom);
   solver << negaxiom;
 }
 
@@ -1038,6 +1035,7 @@ bool string_refinementt::check_axioms()
 
     satcheck_no_simplifiert sat_check;
     supert solver(ns, sat_check);
+    solver.set_ui(ui);
     add_negation_of_constraint_to_solver(axiom_in_model, solver);
 
     switch(solver())
@@ -1092,6 +1090,7 @@ bool string_refinementt::check_axioms()
         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);
         debug() << "adding counter example " << from_expr(instance) << eom;
         add_lemma(instance);

src/solvers/refinement/string_refinement.h

@@ -25,11 +25,6 @@ Author: Alberto Griggio, alberto.griggio@gmail.com
 #include <solvers/refinement/string_constraint.h>
 #include <solvers/refinement/string_constraint_generator.h>
 
-// Defines a limit on the string witnesses we will output.
-// Longer strings are still concidered possible by the solver but
-// it will not output them.
-#define MAX_CONCRETE_STRING_SIZE 500
-
 #define MAX_NB_REFINEMENT 100
 
 class string_refinementt: public bv_refinementt
@@ -48,7 +43,7 @@ class string_refinementt: public bv_refinementt
   // Should we concretize strings when the solver finished
   bool do_concretizing;
 
-  void set_max_string_length(int i);
+  void set_max_string_length(size_t i);
   void enforce_non_empty_string();
   void enforce_printable_characters();
 
@@ -113,8 +108,8 @@ class string_refinementt: public bv_refinementt
   exprt substitute_function_applications(exprt expr);
   typet substitute_java_string_types(typet type);
   exprt substitute_java_strings(exprt expr);
-  exprt substitute_array_with_expr(exprt &expr, exprt &index) const;
-  exprt substitute_array_access(exprt &expr) const;
+  exprt substitute_array_with_expr(const exprt &expr, const exprt &index) const;
+  void substitute_array_access(exprt &expr) const;
   void add_symbol_to_symbol_map(const exprt &lhs, const exprt &rhs);
   bool is_char_array(const typet &type) const;
   bool add_axioms_for_string_assigns(const exprt &lhs, const exprt &rhs);

src/util/string_expr.h

@@ -77,7 +77,7 @@ class string_exprt: public struct_exprt
     return binary_relation_exprt(rhs.length(), ID_lt, length());
   }
 
-  binary_relation_exprt axiom_for_is_strictly_longer_than(int i) const
+  binary_relation_exprt axiom_for_is_strictly_longer_than(mp_integer i) const
   {
     return axiom_for_is_strictly_longer_than(from_integer(i, length().type()));
   }
@@ -94,7 +94,7 @@ class string_exprt: public struct_exprt
     return binary_relation_exprt(length(), ID_le, rhs);
   }
 
-  binary_relation_exprt axiom_for_is_shorter_than(int i) const
+  binary_relation_exprt axiom_for_is_shorter_than(mp_integer i) const
   {
     return axiom_for_is_shorter_than(from_integer(i, length().type()));
   }
@@ -122,7 +122,7 @@ class string_exprt: public struct_exprt
     return equal_exprt(length(), rhs);
   }
 
-  equal_exprt axiom_for_has_length(int i) const
+  equal_exprt axiom_for_has_length(mp_integer i) const
   {
     return axiom_for_has_length(from_integer(i, length().type()));
   }