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

@@ -38,7 +38,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

@@ -13,6 +13,7 @@ Author: Romain Brenguier, [email protected]
 #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>
@@ -22,30 +23,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

@@ -35,7 +35,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

@@ -40,17 +40,32 @@ Function: string_constraint_generatort::add_axioms_for_insert
 
  Outputs: a new string expression
 
- Purpose: add axioms corresponding to the StringBuilder.insert(String) java
-          function
+ Purpose: add axioms corresponding to the
+          StringBuilder.insert(int, CharSequence)
+          and StringBuilder.insert(int, CharSequence, int, int)
+          java functions
 
 \*******************************************************************/
 
 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);
+  }
 }
 
 /*******************************************************************\

src/solvers/refinement/string_constraint_generator_main.cpp

@@ -224,7 +224,6 @@ Function: string_constraint_generatort::convert_java_string_to_string_exprt
 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());
@@ -269,7 +268,7 @@ void string_constraint_generatort::add_default_axioms(
   const string_exprt &s)
 {
   s.axiom_for_is_longer_than(from_integer(0, s.length().type()));
-  if(max_string_length>=0)
+  if(max_string_length!=std::numeric_limits<size_t>::max())
     axioms.push_back(s.axiom_for_is_shorter_than(max_string_length));
 
   if(force_printable_characters)
@@ -433,7 +432,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

@@ -49,35 +49,20 @@ string_refinementt::string_refinementt(
 
 /*******************************************************************\
 
-Function: string_refinementt::set_mode
-
- Purpose: determine which language should be used
-
-\*******************************************************************/
-
-void string_refinementt::set_mode()
-{
-  debug() << "initializing mode" << eom;
-  symbolt init=ns.lookup(irep_idt(CPROVER_PREFIX"initialize"));
-  irep_idt mode=init.mode;
-  debug() << "mode detected as " << mode << eom;
-  generator.set_mode(mode);
-}
-
-/*******************************************************************\
-
 Function: string_refinementt::set_max_string_length
 
   Inputs:
     i - maximum length which is allowed for strings.
-        negative number means no limit
+        by default the strings length has no other limit
+        than the maximal integer according to the type of their
+        length, for instance 2^31-1 for Java.
 
  Purpose: Add constraints on the size of strings used in the
           program.
 
 \*******************************************************************/
 
-void string_refinementt::set_max_string_length(int i)
+void string_refinementt::set_max_string_length(size_t i)
 {
   generator.max_string_length=i;
 }
@@ -355,16 +340,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)
         {
@@ -391,9 +378,9 @@ Function: string_refinementt::concretize_results
 
 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();
 }
@@ -409,7 +396,7 @@ Function: string_refinementt::concretize_lengths
 
 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()))
     {
@@ -420,7 +407,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()))
     {
@@ -448,12 +435,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);
@@ -743,7 +724,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;
@@ -947,6 +928,125 @@ void string_refinementt::fill_model()
 }
 
 
+/*******************************************************************\
+
+Function: string_refinementt::substitute_array_with_expr()
+
+  Inputs:
+    expr - A (possibly nested) 'with' expression on an `array_of`
+           expression
+    index - An index with which to build the equality condition
+
+ Outputs: An expression containing no 'with' expression
+
+ Purpose: Create a new expression where 'with' expressions on arrays
+          are replaced by 'if' expressions.
+          e.g. 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`
+
+\*******************************************************************/
+
+exprt string_refinementt::substitute_array_with_expr(
+  const exprt &expr, const exprt &index) const
+{
+  if(expr.id()==ID_with)
+  {
+    const with_exprt &with_expr=to_with_expr(expr);
+    const exprt &then_expr=with_expr.new_value();
+    exprt else_expr=substitute_array_with_expr(with_expr.old(), index);
+    const typet &type=then_expr.type();
+    assert(else_expr.type()==type);
+    return if_exprt(
+      equal_exprt(index, with_expr.where()), then_expr, else_expr, type);
+  }
+  else
+  {
+    // Only handle 'with' expressions on 'array_of' expressions.
+    assert(expr.id()==ID_array_of);
+    return to_array_of_expr(expr).what();
+  }
+}
+
+/*******************************************************************\
+
+Function: string_refinementt::substitute_array_access()
+
+  Inputs:
+    expr - an expression containing array accesses
+
+ Outputs: an expression containing no array access
+
+ Purpose: 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`
+
+\*******************************************************************/
+
+void string_refinementt::substitute_array_access(exprt &expr) const
+{
+  for(auto &op : expr.operands())
+    substitute_array_access(op);
+
+  if(expr.id()==ID_index)
+  {
+    index_exprt &index_expr=to_index_expr(expr);
+
+    if(index_expr.array().id()==ID_symbol)
+    {
+      expr=index_expr;
+      return;
+    }
+
+    if(index_expr.array().id()==ID_with)
+    {
+      expr=substitute_array_with_expr(
+        index_expr.array(), index_expr.index());
+      return;
+    }
+
+    if(index_expr.array().id()==ID_array_of)
+    {
+      expr=to_array_of_expr(index_expr.array()).op();
+      return;
+    }
+
+    assert(index_expr.array().id()==ID_array);
+    array_exprt &array_expr=to_array_expr(index_expr.array());
+
+    assert(!array_expr.operands().empty());
+    size_t last_index=array_expr.operands().size()-1;
+
+    const typet &char_type=index_expr.array().type().subtype();
+    exprt ite=array_expr.operands().back();
+
+    if(ite.type()!=char_type)
+    {
+      // We have to manualy set the type for unknown values
+      assert(ite.id()==ID_unknown);
+      ite.type()=char_type;
+    }
+
+    auto op_it=++array_expr.operands().rbegin();
+    for(size_t i=last_index-1;
+        op_it!=array_expr.operands().rend(); ++op_it, --i)
+    {
+      equal_exprt equals(index_expr.index(), from_integer(i, java_int_type()));
+      ite=if_exprt(equals, *op_it, ite);
+      if(ite.type()!=char_type)
+      {
+        assert(ite.id()==ID_unknown);
+        ite.type()=char_type;
+      }
+    }
+    expr=ite;
+  }
+}
+
 /*******************************************************************\
 
 Function: string_refinementt::add_negation_of_constraint_to_solver
@@ -991,6 +1091,7 @@ void string_refinementt::add_negation_of_constraint_to_solver(
   and_exprt negaxiom(premise, not_exprt(axiom.body()));
 
   debug() << "(sr::check_axioms) negated axiom: " << from_expr(negaxiom) << eom;
+  substitute_array_access(negaxiom);
   solver << negaxiom;
 }
 
@@ -1031,6 +1132,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())
@@ -1085,6 +1187,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);