Model strchr inside string.h

regression/cbmc/string-refinement-strchr1/test.c

@@ -0,0 +1,15 @@
+#include <assert.h>
+#include <string.h>
+
+int main()
+{
+  char test[] = "foo";
+
+  char *first_o = strchr(test, 'o');
+  assert(*first_o == test[1]);
+  assert(*first_o == test[0]);
+  char *first_t = strchr(test, 't');
+  assert(*first_t == test[1]);
+  assert(*first_t == test[0]);
+  return 0;
+}

regression/cbmc/string-refinement-strchr1/test.desc

@@ -0,0 +1,12 @@
+CORE broken-smt-backend
+test.c
+--refine-strings --max-nondet-string-length 10
+^EXIT=10$
+^SIGNAL=0$
+^\[main.assertion.\d+\] line \d+ assertion \*first_o == test\[1\]: SUCCESS$
+^\[main.assertion.\d+\] line \d+ assertion \*first_o == test\[0\]: FAILURE$
+^\[main.assertion.\d+\] line \d+ assertion \*first_t == test\[1\]: FAILURE$
+^\[main.assertion.\d+\] line \d+ assertion \*first_t == test\[0\]: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc/string-refinement-strchr2/test.c

@@ -0,0 +1,13 @@
+#include <assert.h>
+#include <string.h>
+
+int main()
+{
+  int i;
+  char *test = i ? "fo\0tis" : "notfoti";
+
+  char *first_o = strchr(test, 'o');
+  assert(first_o != NULL);
+  assert(*first_o == test[0]);
+  return 0;
+}

regression/cbmc/string-refinement-strchr2/test.desc

@@ -0,0 +1,10 @@
+CORE broken-smt-backend
+test.c
+--refine-strings
+^EXIT=10$
+^SIGNAL=0$
+^\[main.assertion.\d+\] line \d+ assertion first_o != (NULL|\(\(void \*\)0\)): SUCCESS$
+^\[main.assertion.\d+\] line \d+ assertion \*first_o == test\[0\]: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc/string-refinement-strchr3/test.c

@@ -0,0 +1,24 @@
+#include <assert.h>
+#include <stdlib.h>
+#include <string.h>
+
+int main()
+{
+  int size = 4;
+  char *str = malloc(sizeof(char) * size);
+  char nondet_char;
+  __CPROVER_assume(nondet_char != '\0');
+  str[0] = nondet_char;
+  char nondet_char2;
+  __CPROVER_assume(str[1] != '\0');
+  //  str[1] = nondet_char2;
+  str[2] = 'z';
+  str[3] = '\0';
+  char *result = strchr(str, 'z');
+  assert(result);
+  __CPROVER_assert(0, "unreachable");
+  // assert(result == str+1);
+  //  assert(result == str);
+
+  return 0;
+}

regression/cbmc/string-refinement-strchr3/test.desc

@@ -0,0 +1,11 @@
+CORE broken-smt-backend
+test.c
+--refine-strings
+^EXIT=10$
+^SIGNAL=0$
+^\[strchr.assertion.\d+\] line \d+ zero should be present: SUCCESS$
+^\[main.assertion.\d+\] line \d+ assertion result: SUCCESS$
+^\[main.assertion.\d+\] line \d+ unreachable: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

src/ansi-c/library/cprover.h

@@ -159,4 +159,9 @@ __CPROVER_bool __CPROVER_overflow_plus();
 __CPROVER_bool __CPROVER_overflow_shl();
 __CPROVER_bool __CPROVER_overflow_unary_minus();
 
+long __CPROVER_math_func_string_index_of(
+  const char *haystack,
+  __CPROVER_size_t length,
+  char needle);
+
 #endif // CPROVER_ANSI_C_LIBRARY_CPROVER_H

src/ansi-c/library/string.c

@@ -1,3 +1,19 @@
+
+/* FUNCTION: __CPROVER_math_func_string_index_of */
+
+long __CPROVER_math_func_string_index_of(
+  const char *haystack,
+  __CPROVER_size_t length,
+  char needle)
+{
+  for(__CPROVER_size_t i = 0; i < length; i++)
+  {
+    if(haystack[i] == needle)
+      return i;
+  }
+  return -1;
+}
+
 /* FUNCTION: __builtin___strcpy_chk */
 
 inline char *__builtin___strcpy_chk(char *dst, const char *src, __CPROVER_size_t s)
@@ -932,9 +948,16 @@ inline int memcmp(const void *s1, const void *s2, size_t n)
 #include <string.h>
 #define __CPROVER_STRING_H_INCLUDED
 #endif
+#include <stdint.h> // SIZE_MAX
 
 #undef strchr
 
+__CPROVER_size_t __VERIFIER_nondet___CPROVER_size_t();
+long __CPROVER_math_func_string_index_of(
+  const char *haystack,
+  __CPROVER_size_t length,
+  char needle);
+
 inline char *strchr(const char *src, int c)
 {
   __CPROVER_HIDE:;
@@ -945,14 +968,27 @@ inline char *strchr(const char *src, int c)
   __CPROVER_size_t i;
   return found?src+i:0;
   #else
-  for(__CPROVER_size_t i=0; ; i++)
-  {
-    if(src[i]==(char)c)
-      return ((char *)src)+i; // cast away const-ness
-    if(src[i]==0) break;
-  }
-  return 0;
-  #endif
+
+    /* for(__CPROVER_size_t i=0; ; i++) */
+    /* { */
+    /*   if(src[i]==(char)c) */
+    /*     return ((char *)src)+i; // cast away const-ness */
+    /*   if(src[i]==0) break; */
+    /* } */
+    /* return 0; */
+
+    __CPROVER_size_t src_array_length =
+      SIZE_MAX; // __VERIFIER_nondet___CPROVER_size_t();
+    long index_of_zero =
+      __CPROVER_math_func_string_index_of(src, src_array_length, '\0');
+    __CPROVER_assert(index_of_zero >= 0, "zero should be present");
+    long index_of_c =
+      __CPROVER_math_func_string_index_of(src, src_array_length, (char)c);
+    if(index_of_c >= 0 && index_of_c < index_of_zero)
+      return ((char *)src) + (__CPROVER_size_t)index_of_c;
+    else
+      return (char *)0;
+#endif
 }
 
 /* FUNCTION: strrchr */

src/cbmc/cbmc_parse_options.cpp

@@ -49,6 +49,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-checker/stop_on_fail_verifier_with_fault_localization.h>
 
 #include <goto-programs/adjust_float_expressions.h>
+#include <goto-programs/c_string_refinement.h>
 #include <goto-programs/initialize_goto_model.h>
 #include <goto-programs/instrument_preconditions.h>
 #include <goto-programs/link_to_library.h>
@@ -242,6 +243,8 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
 
   if(cmdline.isset("string-abstraction"))
     options.set_option("string-abstraction", true);
+  if(cmdline.isset("refine-strings"))
+    options.set_option("refine-strings", true);
 
   if(cmdline.isset("reachability-slice-fb"))
     options.set_option("reachability-slice-fb", true);
@@ -363,6 +366,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   {
     options.set_option("refine-strings", true);
     options.set_option("string-printable", cmdline.isset("string-printable"));
+    options.set_option(
+      "max-nondet-string-length",
+      cmdline.get_value("max-nondet-string-length"));
   }
 
   if(cmdline.isset("max-node-refinement"))
@@ -872,6 +878,11 @@ bool cbmc_parse_optionst::process_goto_program(
 
   if(options.get_bool_option("string-abstraction"))
     string_instrumentation(goto_model, log.get_message_handler());
+  else if(options.get_bool_option("refine-strings"))
+    c_string_refinement(
+      goto_model,
+      log.get_message_handler(),
+      options.get_option("max-nondet-string-length"));
 
   // remove function pointers
   log.status() << "Removal of function pointers and virtual functions"

src/goto-programs/Makefile

@@ -1,5 +1,6 @@
 SRC = adjust_float_expressions.cpp \
       builtin_functions.cpp \
+      c_string_refinement.cpp \
       class_hierarchy.cpp \
       class_identifier.cpp \
       compute_called_functions.cpp \