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

@@ -26,9 +26,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
@@ -74,6 +82,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,
@@ -100,6 +110,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

@@ -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]
 
-  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

@@ -173,10 +173,11 @@ Function: string_constraint_generatort::fresh_string
 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;
 }
 
 /*******************************************************************\
@@ -246,6 +247,45 @@ string_exprt string_constraint_generatort::convert_java_string_to_string_exprt(
 
 /*******************************************************************\
 
+Function: string_constraint_generatort::add_default_constraints
+
+  Inputs:
+    s - a string expression
+
+ Outputs: a string expression that is linked to the argument through
+          axioms that are added to the list
+
+ Purpose: adds standard axioms about the length of the string and
+          its content:
+          * its length should be positive
+          * it should not exceed max_string_length
+          * if force_printable_characters is true then all characters
+            should belong to the range of ASCII characters between ' ' and '~'
+
+
+\*******************************************************************/
+
+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)
+    axioms.push_back(s.axiom_for_is_shorter_than(max_string_length));
+
+  if(force_printable_characters)
+  {
+    symbol_exprt qvar=fresh_univ_index("printable", s.length().type());
+    exprt chr=s[qvar];
+    and_exprt printable(
+      binary_relation_exprt(chr, ID_ge, from_integer(' ', chr.type())),
+      binary_relation_exprt(chr, ID_le, from_integer('~', chr.type())));
+    string_constraintt sc(qvar, s.length(), printable);
+    axioms.push_back(sc);
+  }
+}
+
+/*******************************************************************\
+
 Function: string_constraint_generatort::add_axioms_for_refined_string
 
   Inputs: an expression of refined string type
@@ -258,7 +298,6 @@ Function: string_constraint_generatort::add_axioms_for_refined_string
 
 \*******************************************************************/
 
-
 string_exprt string_constraint_generatort::add_axioms_for_refined_string(
   const exprt &string)
 {
@@ -272,15 +311,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)
@@ -290,8 +327,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

src/solvers/refinement/string_refinement.cpp

@@ -43,7 +43,8 @@ string_refinementt::string_refinementt(
   supert(_ns, _prop),
   use_counter_example(false),
   do_concretizing(false),
-  initial_loop_bound(refinement_bound)
+  initial_loop_bound(refinement_bound),
+  non_empty_string(false)
 { }
 
 /*******************************************************************\
@@ -65,6 +66,52 @@ void string_refinementt::set_mode()
 
 /*******************************************************************\
 
+Function: string_refinementt::set_max_string_length
+
+  Inputs:
+    i - maximum length which is allowed for strings.
+        negative number means no limit
+
+ Purpose: Add constraints on the size of strings used in the
+          program.
+
+\*******************************************************************/
+
+void string_refinementt::set_max_string_length(int i)
+{
+  generator.max_string_length=i;
+}
+
+/*******************************************************************\
+
+Function: string_refinementt::set_max_string_length
+
+ Purpose: Add constraints on the size of nondet character arrays
+          to ensure they have length at least 1
+
+\*******************************************************************/
+
+void string_refinementt::enforce_non_empty_string()
+{
+  non_empty_string=true;
+}
+
+/*******************************************************************\
+
+Function: string_refinementt::enforce_printable_characters
+
+ Purpose: Add constraints on characters used in the program
+          to ensure they are printable
+
+\*******************************************************************/
+
+void string_refinementt::enforce_printable_characters()
+{
+  generator.force_printable_characters=true;
+}
+
+/*******************************************************************\
+
 Function: string_refinementt::display_index_set
 
  Purpose: display the current index set, for debugging
@@ -283,52 +330,71 @@ bool string_refinementt::add_axioms_for_string_assigns(const exprt &lhs,
 
 /*******************************************************************\
 
-Function: string_refinementt::concretize_results
+Function: string_refinementt::concretize_string
 
- Purpose: For each string whose length has been solved, add constants
+  Input:
+    expr - an expression
+
+ Purpose: If the expression is of type string, then adds constants
           to the index set to force the solver to pick concrete values
           for each character, and fill the map `found_length`
 
 \*******************************************************************/
 
-void string_refinementt::concretize_results()
+void string_refinementt::concretize_string(const exprt &expr)
 {
-  for(const auto& it : symbol_resolve)
+  if(refined_string_typet::is_refined_string_type(expr.type()))
   {
-    if(refined_string_typet::is_refined_string_type(it.second.type()))
+    string_exprt str=to_string_expr(expr);
+    exprt length=get(str.length());
+    add_lemma(equal_exprt(str.length(), length));
+    exprt content=str.content();
+    replace_expr(symbol_resolve, content);
+    found_length[content]=length;
+    mp_integer found_length;
+    if(!to_integer(length, found_length))
     {
-      string_exprt str=to_string_expr(it.second);
-      exprt length=current_model[str.length()];
-      exprt content=str.content();
-      replace_expr(symbol_resolve, content);
-      found_length[content]=length;
-      mp_integer found_length;
-      if(!to_integer(length, found_length))
+      assert(found_length.is_long());
+      if(found_length < 0)
       {
-        assert(found_length.is_long());
-        if(found_length < 0)
-        {
-          debug() << "concretize_results: WARNING found length is negative"
-                  << eom;
-        }
-        else
+        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;
+        exprt content_expr=str.content();
+        for(size_t i=0; i<concretize_limit; ++i)
         {
-          size_t concretize_limit=found_length.to_long();
-          concretize_limit=concretize_limit>MAX_CONCRETE_STRING_SIZE?
-                MAX_CONCRETE_STRING_SIZE:concretize_limit;
-          exprt content_expr=str.content();
-          replace_expr(current_model, content_expr);
-          for(size_t i=0; i<concretize_limit; ++i)
-          {
-            auto i_expr=from_integer(i, str.length().type());
-            debug() << "Concretizing " << from_expr(content_expr)
-                    << " / " << i << eom;
-            current_index_set[str.content()].insert(i_expr);
-          }
+          auto i_expr=from_integer(i, str.length().type());
+          debug() << "Concretizing " << from_expr(content_expr)
+                  << " / " << i << eom;
+          current_index_set[str.content()].insert(i_expr);
+          index_set[str.content()].insert(i_expr);
         }
       }
     }
   }
+}
+
+/*******************************************************************\
+
+Function: string_refinementt::concretize_results
+
+ Purpose: For each string whose length has been solved, add constants
+          to the index set to force the solver to pick concrete values
+          for each character, and fill the map `found_length`
+
+\*******************************************************************/
+
+void string_refinementt::concretize_results()
+{
+  for(const auto& it : symbol_resolve)
+    concretize_string(it.second);
+  for(const auto& it : generator.created_strings)
+    concretize_string(it);
   add_instantiations();
 }
 
@@ -348,7 +414,18 @@ void string_refinementt::concretize_lengths()
     if(refined_string_typet::is_refined_string_type(it.second.type()))
     {
       string_exprt str=to_string_expr(it.second);
-      exprt length=current_model[str.length()];
+      exprt length=get(str.length());
+      exprt content=str.content();
+      replace_expr(symbol_resolve, content);
+      found_length[content]=length;
+     }
+  }
+  for(const auto& it : generator.created_strings)
+  {
+    if(refined_string_typet::is_refined_string_type(it.type()))
+    {
+      string_exprt str=to_string_expr(it);
+      exprt length=get(str.length());
       exprt content=str.content();
       replace_expr(symbol_resolve, content);
       found_length[content]=length;
@@ -869,6 +946,7 @@ void string_refinementt::fill_model()
   }
 }
 
+
 /*******************************************************************\
 
 Function: string_refinementt::add_negation_of_constraint_to_solver

src/solvers/refinement/string_refinement.h

@@ -2,7 +2,7 @@
 
 Module: String support via creating string constraints and progressively
         instantiating the universal constraints as needed.
-	The procedure is described in the PASS paper at HVC'13:
+        The procedure is described in the PASS paper at HVC'13:
         "PASS: String Solving with Parameterized Array and Interval Automaton"
         by Guodong Li and Indradeep Ghosh
 
@@ -38,8 +38,13 @@ class string_refinementt: public bv_refinementt
   // Should we use counter examples at each iteration?
   bool use_counter_example;
 
+  // Should we concretize strings when the solver finished
   bool do_concretizing;
 
+  void set_max_string_length(int i);
+  void enforce_non_empty_string();
+  void enforce_printable_characters();
+
   virtual std::string decision_procedure_text() const override
   {
     return "string refinement loop with "+prop.solver_text();
@@ -65,6 +70,9 @@ class string_refinementt: public bv_refinementt
 
   string_constraint_generatort generator;
 
+  bool non_empty_string;
+  expr_sett nondet_arrays;
+
   // Simple constraints that have been given to the solver
   expr_sett seen_instances;
 
@@ -98,6 +106,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;
   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);
@@ -134,8 +144,10 @@ class string_refinementt: public bv_refinementt
 
   exprt simplify_sum(const exprt &f) const;
 
+  void concretize_string(const exprt &expr);
   void concretize_results();
   void concretize_lengths();
+
   // Length of char arrays found during concretization
   std::map<exprt, exprt> found_length;