String solver cbmc pass option

src/cbmc/cbmc_parse_options.cpp

@@ -22,6 +22,7 @@ Author: Daniel Kroening, [email protected]
 #include <ansi-c/c_preprocess.h>
 
 #include <goto-programs/goto_convert_functions.h>
+#include <goto-programs/pass_preprocess.h>
 #include <goto-programs/remove_function_pointers.h>
 #include <goto-programs/remove_virtual_functions.h>
 #include <goto-programs/remove_returns.h>
@@ -341,6 +342,11 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
     options.set_option("refine-arithmetic", true);
   }
 
+  if(cmdline.isset("pass"))
+  {
+    options.set_option("pass", true);
+  }
+
   if(cmdline.isset("max-node-refinement"))
     options.set_option("max-node-refinement", cmdline.get_value("max-node-refinement"));
 
@@ -911,6 +917,12 @@ bool cbmc_parse_optionst::process_goto_program(
     status() << "Partial Inlining" << eom;
     goto_partial_inline(goto_functions, ns, ui_message_handler);
 
+
+    if(cmdline.isset("pass")) {
+      status() << "PASS Preprocessing " << eom;
+      pass_preprocess(symbol_table, goto_functions);
+    }
+
     // remove returns, gcc vectors, complex
     remove_returns(symbol_table, goto_functions);
     remove_vector(symbol_table, goto_functions);
@@ -1175,6 +1187,7 @@ void cbmc_parse_optionst::help()
     " --yices                      use Yices\n"
     " --z3                         use Z3\n"
     " --refine                     use refinement procedure (experimental)\n"
+    " --pass                       use pass procedure (experimental)\n"
     " --outfile filename           output formula to given file\n"
     " --arrays-uf-never            never turn arrays into uninterpreted functions\n"
     " --arrays-uf-always           always turn arrays into uninterpreted functions\n"

src/cbmc/cbmc_parse_options.h

@@ -36,7 +36,7 @@ class optionst;
   "(no-sat-preprocessor)" \
   "(no-pretty-names)(beautify)" \
   "(fixedbv)" \
-  "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)(aig)" \
+  "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)(aig)(pass)" \
   "(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>
@@ -324,6 +325,29 @@ cbmc_solverst::solvert* cbmc_solverst::get_bv_refinement()
 
 /*******************************************************************\
 
+Function: cbmc_solverst::get_string_refinement
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+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);
+  string_refinement->set_ui(ui);
+  return new cbmc_solver_with_propt(string_refinement, prop);
+}
+
+/*******************************************************************\
+
 Function: cbmc_solverst::get_smt1
 
   Inputs:

src/cbmc/cbmc_solvers.h

@@ -79,11 +79,14 @@ class cbmc_solverst:public messaget
   virtual std::unique_ptr<solvert> get_solver()
   {
     solvert *solver;
-
     if(options.get_bool_option("dimacs"))
       solver = get_dimacs();
     else if(options.get_bool_option("refine")) 
       solver = get_bv_refinement();
+    else if(options.get_bool_option("pass")) {
+      std::cout << "PASS solver" << std::endl;
+      solver = get_string_refinement(); 
+    }
     else if(options.get_bool_option("smt1")) 
       solver = get_smt1(get_smt1_solver_type());
     else if(options.get_bool_option("smt2"))
@@ -111,6 +114,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);