String refine option

src/cbmc/cbmc_parse_options.cpp

@@ -20,6 +20,7 @@ Author: Daniel Kroening, [email protected]
 #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>
@@ -310,6 +311,11 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
     options.set_option("refine-arithmetic", true);
   }
 
+  if(cmdline.isset("refine-strings"))
+  {
+    options.set_option("refine-strings", true);
+  }
+
   if(cmdline.isset("max-node-refinement"))
     options.set_option(
       "max-node-refinement",
@@ -904,6 +910,14 @@ bool cbmc_parse_optionst::process_goto_program(
     status() << "Partial Inlining" << eom;
     goto_partial_inline(goto_functions, ns, ui_message_handler);
 
+
+    if(cmdline.isset("refine-strings"))
+    {
+      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);
@@ -1191,6 +1205,7 @@ 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"
     " --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

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

src/cbmc/cbmc_solvers.cpp

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 
 #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>
@@ -213,6 +214,29 @@ cbmc_solverst::solvert* cbmc_solverst::get_bv_refinement()
 
 /*******************************************************************\
 
+Function: cbmc_solverst::get_string_refinement
+
+ Outputs: a solver for cbmc
+
+ Purpose: the string refinement adds to the bit vector refinement
+          specifications for functions from the Java string library
+
+\*******************************************************************/
+
+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);
+}
+
+/*******************************************************************\
+
 Function: cbmc_solverst::get_smt1
 
   Inputs:

src/cbmc/cbmc_solvers.h

@@ -111,15 +111,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("refine-strings"))
+      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);
   }
@@ -141,6 +143,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);
 

src/goto-programs/Makefile

@@ -24,7 +24,8 @@ SRC = goto_convert.cpp goto_convert_function_call.cpp \
       remove_instanceof.cpp \
       class_identifier.cpp \
       system_library_symbols.cpp \
-
+      string_refine_preprocess.cpp \
+      # Empty last line
 
 INCLUDES= -I ..
 

src/java_bytecode/java_bytecode_language.cpp

@@ -44,7 +44,7 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
 {
   disable_runtime_checks=cmd.isset("disable-runtime-check");
   assume_inputs_non_null=cmd.isset("java-assume-inputs-non-null");
-  string_refinement_enabled=cmd.isset("string-refine");
+  string_refinement_enabled=cmd.isset("refine-strings");
   if(cmd.isset("java-max-input-array-length"))
     max_nondet_array_length=
       std::stoi(cmd.get_value("java-max-input-array-length"));

src/solvers/Makefile

@@ -118,6 +118,17 @@ SRC = $(CHAFF_SRC) $(BOOLEFORCE_SRC) $(MINISAT_SRC) $(MINISAT2_SRC) \
       floatbv/float_utils.cpp floatbv/float_bv.cpp \
       refinement/bv_refinement_loop.cpp refinement/refine_arithmetic.cpp \
       refinement/refine_arrays.cpp \
+      refinement/string_refinement.cpp \
+      refinement/string_constraint_generator_code_points.cpp \
+      refinement/string_constraint_generator_comparison.cpp \
+      refinement/string_constraint_generator_concat.cpp \
+      refinement/string_constraint_generator_constants.cpp \
+      refinement/string_constraint_generator_indexof.cpp \
+      refinement/string_constraint_generator_insert.cpp \
+      refinement/string_constraint_generator_main.cpp \
+      refinement/string_constraint_generator_testing.cpp \
+      refinement/string_constraint_generator_transformation.cpp \
+      refinement/string_constraint_generator_valueof.cpp \
       miniBDD/miniBDD.cpp
 
 INCLUDES += -I .. \

src/util/Makefile

@@ -23,7 +23,11 @@ SRC = arith_tools.cpp base_type.cpp cmdline.cpp config.cpp symbol_table.cpp \
       memory_info.cpp pipe_stream.cpp irep_hash.cpp endianness_map.cpp \
       ssa_expr.cpp json_irep.cpp json_expr.cpp \
       fresh_symbol.cpp \
-      format_number_range.cpp string_utils.cpp nondet_ifthenelse.cpp
+      format_number_range.cpp \
+      nondet_ifthenelse.cpp \
+      string_utils.cpp \
+      refined_string_type.cpp \
+      #Empty last line
 
 INCLUDES= -I ..