Merge pull request #7834 from qinheping/features/array_theory_in_synthesizer

SYNTHESIZER: add array-uf options

Author: tautschnig

doc/man/goto-synthesizer.1

@@ -121,6 +121,12 @@ output smt incremental formula to the given file
 .TP
 \fB\-\-write\-solver\-stats\-to\fR json\-file
 collect the solver query complexity
+.TP
+\fB\-\-arrays\-uf\-never\fR
+never turn arrays into uninterpreted functions
+.TP
+\fB\-\-arrays\-uf\-always\fR
+always turn arrays into uninterpreted functions
 .SS "User-interface options:"
 .TP
 \fB\-\-xml\-ui\fR

regression/goto-synthesizer/array_uf/main.c

@@ -0,0 +1,35 @@
+#include <stdlib.h>
+
+inline int memcmp(const char *s1, const char *s2, unsigned n)
+{
+  int res = 0;
+  const unsigned char *sc1 = s1, *sc2 = s2;
+  for(; n != 0; n--)
+    // clang-format off
+    __CPROVER_loop_invariant(n <= __CPROVER_loop_entry(n))
+    __CPROVER_loop_invariant(__CPROVER_same_object(sc1, __CPROVER_loop_entry(sc1)))
+    __CPROVER_loop_invariant(__CPROVER_same_object(sc2, __CPROVER_loop_entry(sc2)))
+    __CPROVER_loop_invariant(sc1 <= s1 + __CPROVER_loop_entry(n))
+    __CPROVER_loop_invariant(sc2 <= s2 + __CPROVER_loop_entry(n))
+    __CPROVER_loop_invariant(res == 0)
+    __CPROVER_loop_invariant(sc1 -(const unsigned char*)s1 == sc2 -(const unsigned char*)s2
+      &&  sc1 -(const unsigned char*)s1== __CPROVER_loop_entry(n) - n)
+    // clang-format on
+    {
+      res = (*sc1++) - (*sc2++);
+      long d1 = sc1 - (const unsigned char *)s1;
+      long d2 = sc2 - (const unsigned char *)s2;
+      if(res != 0)
+        return res;
+    }
+  return res;
+}
+
+int main()
+{
+  const unsigned SIZE = 4096;
+  unsigned char *a = malloc(SIZE);
+  unsigned char *b = malloc(SIZE);
+  memcpy(b, a, SIZE);
+  assert(memcmp(a, b, SIZE) == 0);
+}

regression/goto-synthesizer/array_uf/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--pointer-check _ --arrays-uf-always _ --arrays-uf-always
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Check if the flag --array-uf-always is correctly passed from the synthesizer
+to the verifier. Note that there is no loop contracts synthesized in this test.

regression/goto-synthesizer/chain.sh

@@ -12,13 +12,20 @@ name=${*:$#}
 name=${name%.c}
 
 args=${*:6:$#-6}
-if [[ "$args" != *" _ "* ]]
-then
+if [[ "$args" != *" _ "* ]]; then
   args_inst=$args
   args_synthesizer=""
+  args_cbmc=""
 else
   args_inst="${args%%" _ "*}"
-  args_synthesizer="${args#*" _ "}"
+  args=${args#*" _ "}
+  if [[ "$args" != *" _ "* ]]; then
+    args_synthesizer=$args
+    args_cbmc=""
+  else
+    args_synthesizer="${args%%" _ "*}"
+    args_cbmc="${args#*" _ "}"
+  fi
 fi
 
 if [[ "${is_windows}" == "true" ]]; then
@@ -50,5 +57,5 @@ if echo $args_synthesizer | grep -q -- "--dump-loop-contracts" ; then
 else
   $goto_synthesizer ${args_synthesizer} "${name}-mod.gb" "${name}-mod-2.gb"
   echo "Running CBMC: "
-  $cbmc "${name}-mod-2.gb"
+  $cbmc ${args_cbmc} "${name}-mod-2.gb"
 fi

src/goto-synthesizer/goto_synthesizer_parse_options.cpp

@@ -195,13 +195,18 @@ optionst goto_synthesizer_parse_optionst::get_options()
   options.set_option("built-in-assertions", true);
   options.set_option("assertions", true);
   options.set_option("assumptions", true);
-  options.set_option("arrays-uf", "auto");
   options.set_option("depth", UINT32_MAX);
   options.set_option("exploration-strategy", "lifo");
   options.set_option("symex-cache-dereferences", false);
   options.set_option("rewrite-union", true);
   options.set_option("self-loops-to-assumptions", true);
 
+  options.set_option("arrays-uf", "auto");
+  if(cmdline.isset("arrays-uf-always"))
+    options.set_option("arrays-uf", "always");
+  else if(cmdline.isset("arrays-uf-never"))
+    options.set_option("arrays-uf", "never");
+
   // Generating trace for counterexamples.
   options.set_option("trace", true);
 
@@ -233,6 +238,8 @@ void goto_synthesizer_parse_optionst::help()
     HELP_CONFIG_BACKEND
     HELP_SOLVER
     "\n"
+    " --arrays-uf-never            never turn arrays into uninterpreted functions\n" // NOLINT(*)
+    " --arrays-uf-always           always turn arrays into uninterpreted functions\n" // NOLINT(*)
     "Other options:\n"
     " --version                    show version and exit\n"
     " --xml-ui                     use XML-formatted output\n"

src/goto-synthesizer/goto_synthesizer_parse_options.h

@@ -26,6 +26,7 @@ Author: Qinheping Hu
   "(" FLAG_LOOP_CONTRACTS_NO_UNWIND ")" \
   OPT_CONFIG_BACKEND \
   OPT_SOLVER \
+  "(arrays-uf-always)(arrays-uf-never)" \
   "(verbosity):(version)(xml-ui)(json-ui)" \
   // empty last line