Adding the string refinement option to the CBMC solvers

We add the option `--string-refine` which can be used to activate the
string solver, in order to deal precisely with string functions.

Author: romainbrenguier

src/cbmc/cbmc_parse_options.cpp

@@ -26,6 +26,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <ansi-c/c_preprocess.h>
 
 #include <goto-programs/goto_convert_functions.h>
+#include <goto-programs/string_refine_preprocess.h>
 #include <goto-programs/remove_function_pointers.h>
 #include <goto-programs/remove_virtual_functions.h>
 #include <goto-programs/remove_instanceof.h>
@@ -268,6 +269,11 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
     options.set_option("refine-arithmetic", true);
   }
 
+  if(cmdline.isset("string-refine"))
+  {
+    options.set_option("string-refine", true);
+  }
+
   if(cmdline.isset("max-node-refinement"))
     options.set_option(
       "max-node-refinement",
@@ -793,6 +799,14 @@ bool cbmc_parse_optionst::process_goto_program(
     status() << "Partial Inlining" << eom;
     goto_partial_inline(goto_functions, ns, ui_message_handler);
 
+
+    if(cmdline.isset("string-refine"))
+    {
+      status() << "Preprocessing for string refinement" << eom;
+      string_refine_preprocesst(
+        symbol_table, goto_functions, ui_message_handler);
+    }
+
     // remove returns, gcc vectors, complex
     remove_returns(symbol_table, goto_functions);
     remove_vector(symbol_table, goto_functions);
@@ -1052,6 +1066,10 @@ void cbmc_parse_optionst::help()
     " --yices                      use Yices\n"
     " --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

@@ -41,6 +41,7 @@ class optionst;
   "(no-sat-preprocessor)" \
   "(no-pretty-names)(beautify)" \
   "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\
+  "(string-refine)" \
   "(aig)(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
   "(little-endian)(big-endian)" \
   "(show-goto-functions)(show-loops)" \

src/cbmc/cbmc_solvers.cpp

@@ -19,6 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <solvers/sat/satcheck.h>
 #include <solvers/refinement/bv_refinement.h>
+#include <solvers/refinement/string_refinement.h>
 #include <solvers/smt1/smt1_dec.h>
 #include <solvers/smt2/smt2_dec.h>
 #include <solvers/cvc/cvc_dec.h>
@@ -160,6 +161,21 @@ cbmc_solverst::solvert* cbmc_solverst::get_bv_refinement()
   return new solvert(bv_refinement, prop);
 }
 
+/// the string refinement adds to the bit vector refinement specifications for
+/// functions from the Java string library
+/// \return a solver for cbmc
+cbmc_solverst::solvert* cbmc_solverst::get_string_refinement()
+{
+  propt *prop;
+  prop=new satcheck_no_simplifiert();
+  prop->set_message_handler(get_message_handler());
+
+  string_refinementt *string_refinement=new string_refinementt(
+    ns, *prop, MAX_NB_REFINEMENT);
+  string_refinement->set_ui(ui);
+  return new solvert(string_refinement, prop);
+}
+
 cbmc_solverst::solvert* cbmc_solverst::get_smt1(smt1_dect::solvert solver)
 {
   no_beautification();

src/cbmc/cbmc_solvers.h

@@ -108,15 +108,17 @@ class cbmc_solverst:public messaget
     solvert *solver;
 
     if(options.get_bool_option("dimacs"))
-      solver = get_dimacs();
+      solver=get_dimacs();
     else if(options.get_bool_option("refine"))
-      solver = get_bv_refinement();
+      solver=get_bv_refinement();
+    else if(options.get_bool_option("string-refine"))
+      solver=get_string_refinement();
     else if(options.get_bool_option("smt1"))
-      solver = get_smt1(get_smt1_solver_type());
+      solver=get_smt1(get_smt1_solver_type());
     else if(options.get_bool_option("smt2"))
-      solver = get_smt2(get_smt2_solver_type());
+      solver=get_smt2(get_smt2_solver_type());
     else
-      solver = get_default();
+      solver=get_default();
 
     return std::unique_ptr<solvert>(solver);
   }
@@ -138,6 +140,7 @@ class cbmc_solverst:public messaget
   solvert *get_default();
   solvert *get_dimacs();
   solvert *get_bv_refinement();
+  solvert *get_string_refinement();
   solvert *get_smt1(smt1_dect::solvert solver);
   solvert *get_smt2(smt2_dect::solvert solver);