Added option to the string solver for string length and printability

Added field in string_refinement and string_constraint_generator to
bound size of strings in the program and enforce a range on the
characters.

Author: romainbrenguier

src/solvers/refinement/string_constraint_generator.h

@@ -33,9 +33,17 @@ class string_constraint_generatort
   // to the axiom list.
 
   string_constraint_generatort():
-    mode(ID_unknown)
+    mode(ID_unknown),
+    max_string_length(-1),
+    force_printable_characters(false)
   { }
 
+  // Constraints on the maximal length of strings
+  int 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
@@ -81,6 +89,8 @@ class string_constraint_generatort
   // Maps unresolved symbols to the string_exprt that was created for them
   std::map<irep_idt, string_exprt> unresolved_symbols;
 
+  // Set of strings that have been created by the generator
+  std::set<string_exprt> created_strings;
 
   string_exprt find_or_add_string_of_symbol(
     const symbol_exprt &sym,
@@ -107,6 +117,7 @@ class string_constraint_generatort
 
   static irep_idt extract_java_string(const symbol_exprt &s);
 
+  void add_default_axioms(const string_exprt &s);
   exprt axiom_for_is_positive_index(const exprt &x);
 
   // The following functions add axioms for the returned value

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]
 
-  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_main.cpp

@@ -117,10 +117,11 @@ plus_exprt string_constraint_generatort::plus_exprt_with_overflow_check(
 string_exprt string_constraint_generatort::fresh_string(
   const refined_string_typet &type)
 {
-  symbol_exprt length=
-    fresh_symbol("string_length", type.get_index_type());
+  symbol_exprt length=fresh_symbol("string_length", type.get_index_type());
   symbol_exprt content=fresh_symbol("string_content", type.get_content_type());
-  return string_exprt(length, content, type);
+  string_exprt str(length, content, type);
+  created_strings.insert(str);
+  return str;
 }
 
 /// casts an expression to a string expression, or fetches the actual
@@ -215,15 +216,13 @@ string_exprt string_constraint_generatort::add_axioms_for_refined_string(
   {
     const symbol_exprt &sym=to_symbol_expr(string);
     string_exprt s=find_or_add_string_of_symbol(sym, type);
-    axioms.push_back(
-      s.axiom_for_is_longer_than(from_integer(0, s.length().type())));
+    add_default_axioms(s);
     return s;
   }
   else if(string.id()==ID_nondet_symbol)
   {
     string_exprt s=fresh_string(type);
-    axioms.push_back(
-      s.axiom_for_is_longer_than(from_integer(0, s.length().type())));
+    add_default_axioms(s);
     return s;
   }
   else if(string.id()==ID_if)
@@ -233,8 +232,7 @@ string_exprt string_constraint_generatort::add_axioms_for_refined_string(
   else if(string.id()==ID_struct)
   {
     const string_exprt &s=to_string_expr(string);
-    axioms.push_back(
-      s.axiom_for_is_longer_than(from_integer(0, s.length().type())));
+    add_default_axioms(s);
     return s;
   }
   else