Merge pull request #738 from allredj/test-gen-support-string-additional-options-2

Test gen support string additional options 2

Author: peterschrammel

src/cbmc/cbmc_parse_options.cpp

@@ -320,6 +320,11 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("refine-strings"))
   {
     options.set_option("refine-strings", true);
+    options.set_option("string-non-empty", cmdline.isset("string-non-empty"));
+    options.set_option("string-printable", cmdline.isset("string-printable"));
+    if(cmdline.isset("string-max-length"))
+      options.set_option(
+        "string-max-length", cmdline.get_value("string-max-length"));
   }
 
   if(cmdline.isset("max-node-refinement"))
@@ -1207,6 +1212,9 @@ void cbmc_parse_optionst::help()
     " --z3                         use Z3\n"
     " --refine                     use refinement procedure (experimental)\n"
     " --refine-strings             use string refinement (experimental)\n"
+    " --string-non-empty           add constraint that strings are non empty (experimental)\n" // NOLINT(*)
+    " --string-printable           add constraint that strings are printable (experimental)\n" // NOLINT(*)
+    " --string-max-length          add constraint on the length of strings (experimental)\n" // NOLINT(*)
     " --outfile filename           output formula to given file\n"
     " --arrays-uf-never            never turn arrays into uninterpreted functions\n" // NOLINT(*)
     " --arrays-uf-always           always turn arrays into uninterpreted functions\n" // NOLINT(*)

src/cbmc/cbmc_parse_options.h

@@ -39,6 +39,9 @@ class optionst;
   "(no-pretty-names)(beautify)" \
   "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\
   "(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/cbmc/cbmc_solvers.cpp

@@ -232,6 +232,16 @@ cbmc_solverst::solvert* cbmc_solverst::get_string_refinement()
   string_refinementt *string_refinement=new string_refinementt(
     ns, *prop, MAX_NB_REFINEMENT);
   string_refinement->set_ui(ui);
+
+  string_refinement->do_concretizing=options.get_bool_option("trace");
+  if(options.get_bool_option("string-max-length"))
+    string_refinement->set_max_string_length(
+      options.get_signed_int_option("string-max-length"));
+  if(options.get_bool_option("string-non-empty"))
+    string_refinement->enforce_non_empty_string();
+  if(options.get_bool_option("string-printable"))
+    string_refinement->enforce_printable_characters();
+
   return new solvert(string_refinement, prop);
 }
 

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,21 +23,19 @@ 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(std::numeric_limits<size_t>::max()),
+    force_printable_characters(false)
   { }
 
-  void set_mode(irep_idt _mode)
-  {
-    // only C and java modes supported
-    assert((_mode==ID_java) || (_mode==ID_C));
-    mode=_mode;
-  }
+  // Constraints on the maximal length of strings
+  size_t max_string_length;
 
-  irep_idt &get_mode() { return mode; }
+  // Should we add constraints on the characters
+  bool force_printable_characters;
 
   // Axioms are of three kinds: universally quantified string constraint,
   // not contains string constraints and simple formulas.
@@ -74,6 +73,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 +101,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,9 @@ 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_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

@@ -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;
 }
 
 /*******************************************************************\
@@ -223,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());
@@ -246,6 +246,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!=std::numeric_limits<size_t>::max())
+    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 +297,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 +310,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 +326,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
@@ -397,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,