String solver

regression/strings/cprover-string-hack.h

@@ -68,5 +68,6 @@ extern int __CPROVER_uninterpreted_string_index_of_func(__CPROVER_string str, __
 extern int __CPROVER_uninterpreted_string_last_index_of_func(__CPROVER_string str, __CPROVER_char c);
 extern __CPROVER_string __CPROVER_uninterpreted_string_char_set_func(__CPROVER_string str, int pos, __CPROVER_char c);
 extern __CPROVER_string __CPROVER_uninterpreted_string_copy_func(__CPROVER_string str);
-extern unsigned __CPROVER_uninterpreted_string_parse_int_func(__CPROVER_string str);
-extern __CPROVER_string __CPROVER_uninterpreted_string_of_int_func(unsigned i);
+extern int __CPROVER_uninterpreted_string_parse_int_func(__CPROVER_string str);
+extern __CPROVER_string __CPROVER_uninterpreted_string_of_int_func(int i);
+

regression/strings/java_char_array/test.desc

@@ -0,0 +1,9 @@
+CORE
+test_char_array.class
+--pass
+^EXIT=10$
+^SIGNAL=0$
+^\[assertion.1\] assertion at file test_char_array.java line 11: SUCCESS$
+^\[assertion.2\] assertion at file test_char_array.java line 12: SUCCESS$
+^\[assertion.3\] assertion at file test_char_array.java line 13: FAILURE$
+--

regression/strings/java_char_array/test_char_array.java

@@ -0,0 +1,15 @@
+public class test_char_array {
+
+    public static void main(String[] argv)
+    {
+	String s = "abc";
+	char [] str = s.toCharArray();
+	int[] test = new int[312];
+	char c = str[2];
+	String t = argv[0];
+	char d = t.charAt(0);
+	assert(str.length == 3);
+	assert(c == 'c');
+	assert(c == d || d < 'a' || d > 'z' );
+    }
+}

regression/strings/java_char_array_init/test.desc

@@ -0,0 +1,11 @@
+CORE
+test_init.class
+--pass
+^EXIT=10$
+^SIGNAL=0$
+^\[assertion.1\] assertion at file test_init.java line 16: SUCCESS$
+^\[assertion.2\] assertion at file test_init.java line 17: SUCCESS$
+^\[assertion.3\] assertion at file test_init.java line 18: SUCCESS$
+^\[assertion.4\] assertion at file test_init.java line 20: SUCCESS$
+^\[assertion.5\] assertion at file test_init.java line 21: FAILURE$
+--

regression/strings/java_char_array_init/test_init.java

@@ -0,0 +1,23 @@
+public class test_init {
+
+    public static void main(String[] argv)
+    {
+	char [] str = new char[10];
+	str[0] = 'H';
+	str[1] = 'e';
+	str[2] = 'l';
+	str[3] = 'l';
+	str[4] = 'o';
+	String s = new String(str);
+	String t = new String(str,1,2);
+
+	System.out.println(s);
+	System.out.println(s.length());
+	assert(s.startsWith("Hello"));
+	assert(s.length() == 10);
+	assert(t.equals("el"));
+	String u = String.valueOf(str,3,2);
+	assert(u.equals("lo"));
+	assert(s.equals("Hello") || !t.equals("el") || !u.equals("lo"));
+    }
+}

regression/strings/java_string_builder_insert/test.desc

@@ -0,0 +1,8 @@
+CORE
+test_insert.class
+--pass
+^EXIT=10$
+^SIGNAL=0$
+^\[assertion.1\] assertion at file test_insert.java line 17: SUCCESS$
+^\[assertion.2\] assertion at file test_insert.java line 18: FAILURE$
+--

regression/strings/java_string_builder_insert/test_insert.java

@@ -0,0 +1,20 @@
+public class test_insert {
+
+    public static void main(String[] argv)
+    {
+	char [] str = new char[5];
+	str[0] = 'H';
+	str[1] = 'e';
+	str[2] = 'l';
+	str[3] = 'l';
+	str[4] = 'o';
+
+
+	StringBuilder sb = new StringBuilder(" world");
+	sb.insert(0,str);
+	String s = sb.toString();
+	System.out.println(s);
+	assert(s.equals("Hello world"));
+	assert(!s.equals("Hello world"));
+    }
+}

regression/strings/test3/test.desc

@@ -3,8 +3,8 @@ test.c
 --pass
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.assertion.1\] assertion __CPROVER_uninterpreted_string_length_func(s) == i + 5: SUCCESS$
-^\[main.assertion.2\] assertion __CPROVER_uninterpreted_string_is_suffix_func(__CPROVER_uninterpreted_string_literal_func(\"po\"), s): SUCCESS$
-^\[main.assertion.3\] assertion __CPROVER_uninterpreted_string_char_at_func(s, i) == __CPROVER_uninterpreted_char_literal_func(\"p\"): SUCCESS$
-^\[main.assertion.4\] assertion __CPROVER_uninterpreted_string_is_suffix_func(__CPROVER_uninterpreted_string_literal_func(\"p!o\"), s): FAILURE$
+^\[main.assertion.1\] assertion __CPROVER_string_length(s) == i + 5: SUCCESS$
+^\[main.assertion.2\] assertion __CPROVER_string_issuffix(__CPROVER_string_literal(\"po\"),s): SUCCESS$
+^\[main.assertion.3\] assertion __CPROVER_char_at(s, i) == __CPROVER_char_literal(\"p\"): SUCCESS$
+^\[main.assertion.4\] assertion __CPROVER_string_issuffix(__CPROVER_string_literal(\"p!o\"), s): FAILURE$
 --

regression/strings/test_char_set/test.desc

@@ -3,6 +3,6 @@ test.c
 --pass
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.assertion.1\] assertion __CPROVER_uninterpreted_string_equal_func(t, __CPROVER_uninterpreted_string_literal_func("apc")): SUCCESS$
-^\[main.assertion.2\] assertion __CPROVER_uninterpreted_string_equal_func(t, __CPROVER_uninterpreted_string_literal_func("abc")): FAILURE$
+^\[main.assertion.1\] assertion __CPROVER_string_equal(t, __CPROVER_string_literal("apc")): SUCCESS$
+^\[main.assertion.2\] assertion __CPROVER_string_equal(t, __CPROVER_string_literal("abc")): FAILURE$
 --

regression/strings/test_concat/test.desc

@@ -3,6 +3,6 @@ test.c
 --pass
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.assertion.1\] assertion c == __CPROVER_uninterpreted_char_literal_func(\"p\"): SUCCESS$
-^\[main.assertion.2\] assertion __CPROVER_uninterpreted_string_char_at_func(u, 2) == __CPROVER_uninterpreted_char_literal_func(\"p\"): FAILURE$
+^\[main.assertion.1\] assertion c == __CPROVER_char_literal("p"): SUCCESS$
+^\[main.assertion.2\] assertion __CPROVER_char_at(u,2) == __CPROVER_char_literal("p"): FAILURE$
 --

regression/strings/test_equal/test.desc

@@ -3,6 +3,6 @@ test.c
 --pass
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.assertion.1\] assertion __CPROVER_uninterpreted_string_equal_func(s, __CPROVER_uninterpreted_string_literal_func(\"pippo\")): SUCCESS$
-^\[main.assertion.2\] assertion __CPROVER_uninterpreted_string_equal_func(s, __CPROVER_uninterpreted_string_literal_func(\"mippo\")): FAILURE$
+^\[main.assertion.1\] assertion __CPROVER_string_equal(s, __CPROVER_string_literal("pippo")): SUCCESS$
+^\[main.assertion.2\] assertion __CPROVER_string_equal(s, __CPROVER_string_literal("mippo")): FAILURE$
 --

regression/strings/test_int/test.c

@@ -5,12 +5,12 @@
 int main()
 {
   __CPROVER_string s;
-  unsigned i = 10;
+  int i = 10;
   s = __CPROVER_string_of_int(123);
   assert(__CPROVER_char_at(s,0)  == '1');
   assert(__CPROVER_char_at(s,1)  == '2');
 
-  unsigned j = __CPROVER_parse_int(__CPROVER_string_literal("234"));
+  int j = __CPROVER_parse_int(__CPROVER_string_literal("234"));
 
   assert(j == 234);
   assert(j < 233 || __CPROVER_char_at(s,2)  == '4');

regression/strings/test_int/test.desc

@@ -3,8 +3,8 @@ test.c
 --pass
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.assertion.1\] assertion __CPROVER_uninterpreted_string_char_at_func(s, 0) == .1.: SUCCESS$
-^\[main.assertion.2\] assertion __CPROVER_uninterpreted_string_char_at_func(s, 1) == .2.: SUCCESS$
+^\[main.assertion.1\] assertion __CPROVER_char_at(s,0) == .1.: SUCCESS$
+^\[main.assertion.2\] assertion __CPROVER_char_at(s,1) == .2.: SUCCESS$
 ^\[main.assertion.3\] assertion j == 234: SUCCESS$
-^\[main.assertion.4\] assertion j < 233 || __CPROVER_uninterpreted_string_char_at_func(s, 2) == .4.: FAILURE$
+^\[main.assertion.4\] assertion j < 233 || __CPROVER_char_at(s,2) == .4.: FAILURE$
 --

regression/strings/test_pass_pc3/test.desc

@@ -3,6 +3,6 @@ test.c
 --pass
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.assertion.1\] assertion __CPROVER_uninterpreted_string_length_func(s3) == 0: FAILURE$
-^\[main.assertion.2\] assertion __CPROVER_uninterpreted_string_length_func(s3) < 2: SUCCESS$
+^\[main.assertion.1\] assertion __CPROVER_string_length(s3) == 0: FAILURE$
+^\[main.assertion.2\] assertion __CPROVER_string_length(s3) < 2: SUCCESS$
 ^VERIFICATION FAILED$

regression/strings/test_substring/test.desc

@@ -3,8 +3,8 @@ test.c
 --pass
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.assertion.1\] assertion __CPROVER_uninterpreted_string_equal_func(t, __CPROVER_uninterpreted_string_literal_func(\"cd\")): SUCCESS$
-^\[main.assertion.2\] assertion __CPROVER_uninterpreted_string_equal_func(t, __CPROVER_uninterpreted_string_literal_func(\"cc\")): FAILURE$
-^\[main.assertion.3\] assertion !__CPROVER_uninterpreted_string_equal_func(t, __CPROVER_uninterpreted_string_literal_func(\"bc\")): SUCCESS$
-^\[main.assertion.4\] assertion !__CPROVER_uninterpreted_string_equal_func(t, __CPROVER_uninterpreted_string_literal_func(\"cd\")): FAILURE$
+^\[main.assertion.1\] assertion __CPROVER_string_equal(t,__CPROVER_string_literal("cd")): SUCCESS$
+^\[main.assertion.2\] assertion __CPROVER_string_equal(t,__CPROVER_string_literal("cc")): FAILURE$
+^\[main.assertion.3\] assertion !__CPROVER_string_equal(t,__CPROVER_string_literal("bc")): SUCCESS$
+^\[main.assertion.4\] assertion !__CPROVER_string_equal(t,__CPROVER_string_literal("cd")): FAILURE$
 --

regression/strings/test_suffix/test.desc

@@ -3,6 +3,6 @@ test.c
 --pass
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.assertion.1\] assertion __CPROVER_uninterpreted_string_is_suffix_func(__CPROVER_uninterpreted_string_literal_func(\"po\"), s): SUCCESS$
-^\[main.assertion.2\] assertion __CPROVER_uninterpreted_string_is_suffix_func(__CPROVER_uninterpreted_string_literal_func(\"pp\"), s): FAILURE$
+^\[main.assertion.1\] assertion __CPROVER_string_issuffix(__CPROVER_string_literal("po"),s): SUCCESS$
+^\[main.assertion.2\] assertion __CPROVER_string_issuffix(__CPROVER_string_literal("pp"),s): FAILURE$
 --

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>
@@ -339,6 +340,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"));
 
@@ -913,6 +919,13 @@ 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_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);
@@ -1188,6 +1201,7 @@ void cbmc_parse_optionst::help()
     " --yices                      use Yices\n"
     " --z3                         use Z3\n"
     " --refine                     use refinement procedure (experimental)\n"
+    " --pass                       use parameterized array for string solving (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

@@ -84,6 +84,8 @@ class cbmc_solverst:public messaget
       solver = get_dimacs();
     else if(options.get_bool_option("refine"))
       solver = get_bv_refinement();
+    else if(options.get_bool_option("pass"))
+      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 +113,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

@@ -16,7 +16,8 @@ SRC = goto_convert.cpp goto_convert_function_call.cpp \
       remove_returns.cpp osx_fat_reader.cpp remove_complex.cpp \
       goto_trace.cpp xml_goto_trace.cpp vcd_goto_trace.cpp \
       graphml_witness.cpp remove_virtual_functions.cpp \
-      class_hierarchy.cpp show_goto_functions.cpp get_goto_model.cpp
+      class_hierarchy.cpp show_goto_functions.cpp get_goto_model.cpp \
+      pass_preprocess.cpp
 
 INCLUDES= -I ..