Many corrections in string refinement

Overhaul of string solver contributions

The code adding lemmas to the solver for each equality has been
completely remastered. It has been simplified and should
now cover all foreseable cases.

 Add overflow constraints on sums for string solver
 When creating sum expressions during string
refinement, e.g. when
 adding string lengths, we shall add axioms to prevent the solver
 from finding values that actually come from an integer
overflow.
 Therefore, we introduce a new method plus_exprt_with_overflow_check()
 that wraps around plus_exprt and generates the
relevant axioms.

Cache function applications
Cache converted function applications to avoid re-generating the axioms
if it has already been done for a given function application.
This seems to happen for function applications that are in an
assertion, and thus are treated separately by convert_bitvector.

Remove string_refinement::convert_symbol: the behaviour of
this function was to convert java strings to strings of
symbols. In hindsight, this was not a good idea, as we still refer
to the actual java string fields in some cases, e.g. to read its
length.

Replace add_axioms_for_string_expr
In all add_axioms_... methods, we replace all calls to
add_axioms_for_string_expr by the newly created function
get_string_expr, which simply returns a
string_exprt when we give it
an refined expr (such as a string_exprt or a symbol).

Update doc in add_axioms_for_index_string
Simplify constraint for is_prefix: apply distribution
law and update (and refactor) documentation.

Remove set_string_symbol_equal_to_expr()

Removed mentions of java string type in the string solver

Removing mentions of is_c_string_type
To use the string solver in C, we
should use a struct type with tag
    __CPROVER_refined_string_type

Keep non-string axioms in a list
Instead of giving axioms to
super::boolbv_set_equality_to_true, which
may contain un-substituted symbols, we keep them in a list and
substitute them in dec_solve() before giving them to the
function.

Cleaning the add_axioms_for_string_expr method and renamed it
to add_axioms_for_refined_string to signify that it should
 only be called on expression of type refined string.
An assertion was added at the beginning to ensure that.

Better get_array and string_of_array functions.
Cleaned the implementation of get_array and factorized
part of it.
Made string_of_array directly take a array_exprt, which can be
 obtained from get_array.
Improved string_of_array for non printable characters

Resolve symbol to char arrays in non-string axioms.
We introduce a mapping that expresses the
maximal traversal of symbols
of char array type.
We use that map to, either obtain a char array from a symbol,
either get a unique symbol the aliases equivalence class.
This map is used to replace all symbols of char array type in
the axioms that are added using the parent method:
        supert::boolbv_set_equality_to_true.

Defining several intermediary functions for
check_axioms and cleaning.
Check axioms is quite complicated so we splitted it in several
parts.

Avoid using same universal variable name in string comparison function.

Corrected test in index_of as characters could be signed

Corrected return type retrieval in
from_float functions.
The return type should be given as argument of the helper function
add_axioms_from_float.

Fixed type of contains in constraint generation

Introduce string_refinementt::set_to.
We now override the set_to() method
instead of set_equality_to_true().
This solves a problem where many lemmas were being dropped.

Handle array_of in set_char_array_equality.
Java assignments such as char[] str=new char[10]
involves assigning
the char array to 0, which is done using the array_of operator.
This operator is now handled when found on the rhs of a char
array assignment.

Optimized string hash code and intern functions to only
look at seen strings.
We only compare the argument to the strings on which hash_code
(resp. intern) was already called.

Add missing override keyword in declarations

Integrate strings into symbol resolution.
We now use for strings the mechanism that was
made for resolving symbols
    to char arrays.
  As a result, the symbol_to_string map has been removed.
 We introduce an unresolved_symbol map to associate symbols
to string
    expressions that were introduced during constraint generation.

 Preventing return of nil exprt in sum_over_map

Enforce -1 for witnesses when strings are unequal.
This makes it easier to see when models for string
have different length.

Correct array index in get_array
Correct a bad array access that caused a segmentation fault on
the java_delete test.

Adding option to concretize result and get method in string solver
The option to concretize makes sure that the model that we get in the
end is correct.
Overiding the get method is necessary to get the actual valuation of
string gotten by the solver.
This two additions makes the trace generation for program with strings
more likely to be actual traces of the program.

Avoid adding axioms for copy

Corrected `get` to not replace strings

Simplifying lemmas before handing them to the solver
This seems to improve performances

Ignoring char array that are not symbol or constants

Avoid creating new length variable for concat

Adding constraint on positive length for refined strings

Using get method of the parent class for the size

Add function to fill the found_length map

Signature for get_array should be constant

Corrected overflow problem when integer get to the max size

Removing overflow check in universal constraint

Enforcing witness -1 when length is not sufficient in suffix

Corrected index variable which should be universally quantified

Factorizing addition to index set and more debug information

Avoiding generating a fresh string for the empty string

Enabling string solver to treat more cases and more debug infos

Conversion from char pointer to array in the solver

Raise a warning if found length is negative

Ensure the arguments of parseInt are of the right format
For now we add axioms asking for the argument to have the right format
but ultimately we should raise an exception when it is not the case
(which is not done right now).

Corrects the specification of int to string conversion
Some problems where encountered for strings with the maximal size
possible for an int, which could cause an overflow.

Disallow + sign in string from int
Java will not add the sign for positive numbers

Use get instead of current_model in check_axioms

Streamline code of check_axioms() by calling get() insteand of relying
on the 'current_model' variable.
get() has been adapted to convert array-lists into with expressions, the
former not being handled by the string solver.

Author: romainbrenguier

src/solvers/refinement/string_constraint.h

@@ -48,7 +48,6 @@ class string_constraintt: public exprt
     return operands()[4];
   }
 
-
  private:
   string_constraintt();
 

src/solvers/refinement/string_constraint_generator.h

@@ -14,6 +14,7 @@ Author: Romain Brenguier, [email protected]
 #define CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_GENERATOR_H
 
 #include <util/string_expr.h>
+#include <util/replace_expr.h>
 #include <util/refined_string_type.h>
 #include <solvers/refinement/string_constraint.h>
 
@@ -65,21 +66,20 @@ class string_constraint_generatort
   symbol_exprt fresh_univ_index(const irep_idt &prefix, const typet &type);
   symbol_exprt fresh_boolean(const irep_idt &prefix);
   string_exprt fresh_string(const refined_string_typet &type);
+  string_exprt get_string_expr(const exprt &expr);
+  string_exprt convert_java_string_to_string_exprt(
+    const exprt &underlying);
+  plus_exprt plus_exprt_with_overflow_check(const exprt &op1, const exprt &op2);
 
-  // We maintain a map from symbols to strings.
-  std::map<irep_idt, string_exprt> symbol_to_string;
+  // Maps unresolved symbols to the string_exprt that was created for them
+  std::map<irep_idt, string_exprt> unresolved_symbols;
 
-  string_exprt find_or_add_string_of_symbol(const symbol_exprt &sym);
 
-  void assign_to_symbol(
-    const symbol_exprt &sym, const string_exprt &expr)
-  {
-    symbol_to_string[sym.get_identifier()]=expr;
-  }
+  string_exprt find_or_add_string_of_symbol(
+    const symbol_exprt &sym,
+    const refined_string_typet &ref_type);
 
-  string_exprt add_axioms_for_string_expr(const exprt &expr);
-  void set_string_symbol_equal_to_expr(
-    const symbol_exprt &sym, const exprt &str);
+  string_exprt add_axioms_for_refined_string(const exprt &expr);
 
   exprt add_axioms_for_function_application(
     const function_application_exprt &expr);
@@ -96,6 +96,8 @@ class string_constraint_generatort
   const std::size_t MAX_FLOAT_LENGTH=15;
   const std::size_t MAX_DOUBLE_LENGTH=30;
 
+  std::map<function_application_exprt, exprt> function_application_cache;
+
   static irep_idt extract_java_string(const symbol_exprt &s);
 
   exprt axiom_for_is_positive_index(const exprt &x);
@@ -117,6 +119,9 @@ class string_constraint_generatort
   // The specification is partial: the actual value is not actually computed
   // but we ensure that hash codes of equal strings are equal.
   exprt add_axioms_for_hash_code(const function_application_exprt &f);
+  // To each string on which hash_code was called we associate a symbol
+  // representing the return value of the hash_code function.
+  std::map<string_exprt, exprt> hash_code_of_string;
 
   exprt add_axioms_for_is_empty(const function_application_exprt &f);
   exprt add_axioms_for_is_prefix(
@@ -224,7 +229,9 @@ class string_constraint_generatort
   // the start for negative number
   string_exprt add_axioms_from_float(const function_application_exprt &f);
   string_exprt add_axioms_from_float(
-    const exprt &f, bool double_precision=false);
+    const exprt &f,
+    const refined_string_typet &ref_type,
+    bool double_precision);
 
   // Add axioms corresponding to the String.valueOf(D) java function
   // TODO: the specifications is only partial
@@ -253,6 +260,7 @@ class string_constraint_generatort
   string_exprt add_axioms_for_code_point(
     const exprt &code_point, const refined_string_typet &ref_type);
   string_exprt add_axioms_for_java_char_array(const exprt &char_array);
+  exprt add_axioms_for_char_pointer(const function_application_exprt &fun);
   string_exprt add_axioms_for_if(const if_exprt &expr);
   exprt add_axioms_for_char_literal(const function_application_exprt &f);
 
@@ -270,6 +278,8 @@ class string_constraint_generatort
     const function_application_exprt &f);
 
   exprt add_axioms_for_parse_int(const function_application_exprt &f);
+  exprt add_axioms_for_correct_number_format(
+    const string_exprt &str, std::size_t max_size=10);
   exprt add_axioms_for_to_char_array(const function_application_exprt &f);
   exprt add_axioms_for_compare_to(const function_application_exprt &f);
 
@@ -278,6 +288,9 @@ class string_constraint_generatort
   // string pointers
   symbol_exprt add_axioms_for_intern(const function_application_exprt &f);
 
+  // Pool used for the intern method
+  std::map<string_exprt, symbol_exprt> intern_of_string;
+
   // Tells which language is used. C and Java are supported
   irep_idt mode;
 
@@ -293,14 +306,8 @@ class string_constraint_generatort
   exprt int_of_hex_char(const exprt &chr) const;
   exprt is_high_surrogate(const exprt &chr) const;
   exprt is_low_surrogate(const exprt &chr) const;
-  static exprt character_equals_ignore_case(
+  exprt character_equals_ignore_case(
     exprt char1, exprt char2, exprt char_a, exprt char_A, exprt char_Z);
-
-  // Pool used for the intern method
-  std::map<string_exprt, symbol_exprt> pool;
-
-  // Used to determine whether hashcode should be equal
-  std::map<string_exprt, symbol_exprt> hash;
 };
 
 #endif

src/solvers/refinement/string_constraint_generator_code_points.cpp

@@ -160,17 +160,18 @@ exprt string_constraint_generatort::add_axioms_for_code_point_at(
 {
   typet return_type=f.type();
   assert(return_type.id()==ID_signedbv);
-  string_exprt str=add_axioms_for_string_expr(args(f, 2)[0]);
+  string_exprt str=get_string_expr(args(f, 2)[0]);
   const exprt &pos=args(f, 2)[1];
 
   symbol_exprt result=fresh_symbol("char", return_type);
   exprt index1=from_integer(1, str.length().type());
   const exprt &char1=str[pos];
-  const exprt &char2=str[plus_exprt(pos, index1)];
+  const exprt &char2=str[plus_exprt_with_overflow_check(pos, index1)];
   exprt char1_as_int=typecast_exprt(char1, return_type);
   exprt char2_as_int=typecast_exprt(char2, return_type);
   exprt pair=pair_value(char1_as_int, char2_as_int, return_type);
-  exprt is_low=is_low_surrogate(str[plus_exprt(pos, index1)]);
+  exprt is_low=is_low_surrogate(
+    str[plus_exprt_with_overflow_check(pos, index1)]);
   exprt return_pair=and_exprt(is_high_surrogate(str[pos]), is_low);
 
   axioms.push_back(implies_exprt(return_pair, equal_exprt(result, pair)));
@@ -199,7 +200,7 @@ exprt string_constraint_generatort::add_axioms_for_code_point_before(
   typet return_type=f.type();
   assert(return_type.id()==ID_signedbv);
   symbol_exprt result=fresh_symbol("char", return_type);
-  string_exprt str=add_axioms_for_string_expr(args[0]);
+  string_exprt str=get_string_expr(args[0]);
 
   const exprt &char1=
     str[minus_exprt(args[1], from_integer(2, str.length().type()))];
@@ -234,7 +235,7 @@ Function: string_constraint_generatort::add_axioms_for_code_point_count
 exprt string_constraint_generatort::add_axioms_for_code_point_count(
   const function_application_exprt &f)
 {
-  string_exprt str=add_axioms_for_string_expr(args(f, 3)[0]);
+  string_exprt str=get_string_expr(args(f, 3)[0]);
   const exprt &begin=args(f, 3)[1];
   const exprt &end=args(f, 3)[2];
   const typet &return_type=f.type();
@@ -265,14 +266,15 @@ Function: string_constraint_generatort::add_axioms_for_offset_by_code_point
 exprt string_constraint_generatort::add_axioms_for_offset_by_code_point(
   const function_application_exprt &f)
 {
-  string_exprt str=add_axioms_for_string_expr(args(f, 3)[0]);
+  string_exprt str=get_string_expr(args(f, 3)[0]);
   const exprt &index=args(f, 3)[1];
   const exprt &offset=args(f, 3)[2];
   const typet &return_type=f.type();
   symbol_exprt result=fresh_symbol("offset_by_code_point", return_type);
 
-  exprt minimum=plus_exprt(index, offset);
-  exprt maximum=plus_exprt(index, plus_exprt(offset, offset));
+  exprt minimum=plus_exprt_with_overflow_check(index, offset);
+  exprt maximum=plus_exprt_with_overflow_check(
+    index, plus_exprt_with_overflow_check(offset, offset));
   axioms.push_back(binary_relation_exprt(result, ID_le, maximum));
   axioms.push_back(binary_relation_exprt(result, ID_ge, minimum));
 

src/solvers/refinement/string_constraint_generator_comparison.cpp

@@ -18,7 +18,9 @@ Function: string_constraint_generatort::add_axioms_for_equals
  Outputs: a expression of Boolean type
 
  Purpose: add axioms stating that the result is true exactly when the strings
-          represented by the arguments are equal
+          represented by the arguments are equal.
+          the variable ending in `witness_unequal` is -1 if the length differs
+          or an index at which the strings are different
 
 \*******************************************************************/
 
@@ -29,8 +31,8 @@ exprt string_constraint_generatort::add_axioms_for_equals(
   symbol_exprt eq=fresh_boolean("equal");
   typecast_exprt tc_eq(eq, f.type());
 
-  string_exprt s1=add_axioms_for_string_expr(args(f, 2)[0]);
-  string_exprt s2=add_axioms_for_string_expr(args(f, 2)[1]);
+  string_exprt s1=get_string_expr(args(f, 2)[0]);
+  string_exprt s2=get_string_expr(args(f, 2)[1]);
   typet index_type=s1.length().type();
 
   // We want to write:
@@ -54,9 +56,10 @@ exprt string_constraint_generatort::add_axioms_for_equals(
     binary_relation_exprt(witness, ID_lt, s1.length()),
     binary_relation_exprt(witness, ID_ge, zero));
   and_exprt witnessing(bound_witness, notequal_exprt(s1[witness], s2[witness]));
-  implies_exprt a3(
-    not_exprt(eq),
-    or_exprt(notequal_exprt(s1.length(), s2.length()), witnessing));
+  and_exprt diff_length(
+    notequal_exprt(s1.length(), s2.length()),
+    equal_exprt(witness, from_integer(-1, index_type)));
+  implies_exprt a3(not_exprt(eq), or_exprt(diff_length, witnessing));
   axioms.push_back(a3);
 
   return tc_eq;
@@ -92,8 +95,13 @@ exprt string_constraint_generatort::character_equals_ignore_case(
   // p3 : (is_up2&&'a'-'A'+char2=char1)
   equal_exprt p1(char1, char2);
   minus_exprt diff=minus_exprt(char_a, char_A);
-  and_exprt p2(is_upper_case_1, equal_exprt(plus_exprt(diff, char1), char2));
-  and_exprt p3(is_upper_case_2, equal_exprt(plus_exprt(diff, char2), char1));
+
+  // Overflow is not a problem here because is_upper_case conditions
+  // ensure that we are within a safe range.
+  and_exprt p2(is_upper_case_1,
+               equal_exprt(plus_exprt(diff, char1), char2));
+  and_exprt p3(is_upper_case_2,
+               equal_exprt(plus_exprt(diff, char2), char1));
   return or_exprt(or_exprt(p1, p2), p3);
 }
 
@@ -116,8 +124,8 @@ exprt string_constraint_generatort::add_axioms_for_equals_ignore_case(
 
   symbol_exprt eq=fresh_boolean("equal_ignore_case");
   typecast_exprt tc_eq(eq, f.type());
-  string_exprt s1=add_axioms_for_string_expr(args(f, 2)[0]);
-  string_exprt s2=add_axioms_for_string_expr(args(f, 2)[1]);
+  string_exprt s1=get_string_expr(args(f, 2)[0]);
+  string_exprt s2=get_string_expr(args(f, 2)[1]);
   typet char_type=to_refined_string_type(s1.type()).get_char_type();
   exprt char_a=constant_char('a', char_type);
   exprt char_A=constant_char('A', char_type);
@@ -174,37 +182,35 @@ Function: string_constraint_generatort::add_axioms_for_hash_code
 exprt string_constraint_generatort::add_axioms_for_hash_code(
   const function_application_exprt &f)
 {
-  string_exprt str=add_axioms_for_string_expr(args(f, 1)[0]);
+  string_exprt str=get_string_expr(args(f, 1)[0]);
   typet return_type=f.type();
   typet index_type=str.length().type();
 
-  // initialisation of the missing pool variable
-  std::map<irep_idt, string_exprt>::iterator it;
-  for(it=symbol_to_string.begin(); it!=symbol_to_string.end(); it++)
-    if(hash.find(it->second)==hash.end())
-      hash[it->second]=fresh_symbol("hash", return_type);
+  auto pair=hash_code_of_string.insert(
+    std::make_pair(str, fresh_symbol("hash", return_type)));
+  exprt hash=pair.first->second;
 
   // for each string s. either:
   //   c1: hash(str)=hash(s)
   //   c2: |str|!=|s|
-  //   c3: (|str|==|s| &&exists i<|s|. s[i]!=str[i])
+  //   c3: (|str|==|s| && exists i<|s|. s[i]!=str[i])
 
   // WARNING: the specification may be incomplete
-  for(it=symbol_to_string.begin(); it!=symbol_to_string.end(); it++)
+  for(auto it : hash_code_of_string)
   {
     symbol_exprt i=fresh_exist_index("index_hash", index_type);
-    equal_exprt c1(hash[it->second], hash[str]);
-    not_exprt c2(equal_exprt(it->second.length(), str.length()));
+    equal_exprt c1(it.second, hash);
+    not_exprt c2(equal_exprt(it.first.length(), str.length()));
     and_exprt c3(
-      equal_exprt(it->second.length(), str.length()),
+      equal_exprt(it.first.length(), str.length()),
       and_exprt(
-        not_exprt(equal_exprt(str[i], it->second[i])),
+        not_exprt(equal_exprt(str[i], it.first[i])),
         and_exprt(
           str.axiom_for_is_strictly_longer_than(i),
           axiom_for_is_positive_index(i))));
     axioms.push_back(or_exprt(c1, or_exprt(c2, c3)));
   }
-  return hash[str];
+  return hash;
 }
 
 /*******************************************************************\
@@ -222,8 +228,8 @@ Function: string_constraint_generatort::add_axioms_for_compare_to
 exprt string_constraint_generatort::add_axioms_for_compare_to(
   const function_application_exprt &f)
 {
-  string_exprt s1=add_axioms_for_string_expr(args(f, 2)[0]);
-  string_exprt s2=add_axioms_for_string_expr(args(f, 2)[1]);
+  string_exprt s1=get_string_expr(args(f, 2)[0]);
+  string_exprt s2=get_string_expr(args(f, 2)[1]);
   const typet &return_type=f.type();
   symbol_exprt res=fresh_symbol("compare_to", return_type);
   typet index_type=s1.length().type();
@@ -234,12 +240,12 @@ exprt string_constraint_generatort::add_axioms_for_compare_to(
   // a1 : res==0 => |s1|=|s2|
   // a2 : forall i<|s1|. s1[i]==s2[i]
   // a3 : exists x.
-  // res!=0 ==> x> 0 &&
-  //   ((|s1| <= |s2| &&x<|s1|) || (|s1| >= |s2| &&x<|s2|)
-  //   &&res=s1[x]-s2[x] )
-  // || cond2:
-  //   (|s1|<|s2| &&x=|s1|) || (|s1| > |s2| &&x=|s2|) &&res=|s1|-|s2|)
-  // a4 : forall i<x. res!=0 => s1[i]=s2[i]
+  //        res!=0 ==> x > 0
+  //        && ((|s1| <= |s2| && x<|s1|) || (|s1| >= |s2| &&x<|s2|)
+  //        && res=s1[x]-s2[x] )
+  //     || cond2:
+  //       (|s1|<|s2| &&x=|s1|) || (|s1| > |s2| &&x=|s2|) &&res=|s1|-|s2|)
+  // a4 : forall i'<x. res!=0 => s1[i]=s2[i]
 
   assert(return_type.id()==ID_signedbv);
 
@@ -282,7 +288,9 @@ exprt string_constraint_generatort::add_axioms_for_compare_to(
       or_exprt(cond1, cond2)));
   axioms.push_back(a3);
 
-  string_constraintt a4(i, x, not_exprt(res_null), equal_exprt(s1[i], s2[i]));
+  symbol_exprt i2=fresh_univ_index("QA_compare_to", index_type);
+  string_constraintt a4(
+    i2, x, not_exprt(res_null), equal_exprt(s1[i2], s2[i2]));
   axioms.push_back(a4);
 
   return res;
@@ -304,46 +312,46 @@ Function: string_constraint_generatort::add_axioms_for_intern
 symbol_exprt string_constraint_generatort::add_axioms_for_intern(
   const function_application_exprt &f)
 {
-  string_exprt str=add_axioms_for_string_expr(args(f, 1)[0]);
+  string_exprt str=get_string_expr(args(f, 1)[0]);
+  // For now we only enforce content equality and not pointer equality
   const typet &return_type=f.type();
+
   typet index_type=str.length().type();
 
-  // initialisation of the missing pool variable
-  std::map<irep_idt, string_exprt>::iterator it;
-  for(it=symbol_to_string.begin(); it!=symbol_to_string.end(); it++)
-    if(pool.find(it->second)==pool.end())
-      pool[it->second]=fresh_symbol("pool", return_type);
+  auto pair=intern_of_string.insert(
+    std::make_pair(str, fresh_symbol("pool", return_type)));
+  symbol_exprt intern=pair.first->second;
 
   // intern(str)=s_0 || s_1 || ...
   // for each string s.
   //    intern(str)=intern(s) || |str|!=|s|
   //    || (|str|==|s| &&exists i<|s|. s[i]!=str[i])
 
   exprt disj=false_exprt();
-  for(it=symbol_to_string.begin(); it!=symbol_to_string.end(); it++)
+  for(auto it : intern_of_string)
     disj=or_exprt(
-      disj, equal_exprt(pool[str], symbol_exprt(it->first, return_type)));
+      disj, equal_exprt(intern, it.second));
 
   axioms.push_back(disj);
 
 
   // WARNING: the specification may be incomplete or incorrect
-  for(it=symbol_to_string.begin(); it!=symbol_to_string.end(); it++)
-    if(it->second!=str)
+  for(auto it : intern_of_string)
+    if(it.second!=str)
     {
       symbol_exprt i=fresh_exist_index("index_intern", index_type);
       axioms.push_back(
         or_exprt(
-          equal_exprt(pool[it->second], pool[str]),
+          equal_exprt(it.second, intern),
           or_exprt(
-            not_exprt(str.axiom_for_has_same_length_as(it->second)),
+            not_exprt(str.axiom_for_has_same_length_as(it.first)),
             and_exprt(
-              str.axiom_for_has_same_length_as(it->second),
+              str.axiom_for_has_same_length_as(it.first),
               and_exprt(
-                not_exprt(equal_exprt(str[i], it->second[i])),
+                not_exprt(equal_exprt(str[i], it.first[i])),
                 and_exprt(str.axiom_for_is_strictly_longer_than(i),
                           axiom_for_is_positive_index(i)))))));
     }
 
-  return pool[str];
+  return intern;
 }