Allow user specify the command to run CBMC in goto-synthesizer

doc/man/goto-synthesizer.1

@@ -27,6 +27,9 @@ dump the synthesized loop contracts as JSON
 specify the output destination of the loop-contracts JSON
 .SS "Backend options:"
 .TP
+\fB\-\-cbmc\-cmd\fR cmd
+command used to run cbmc to check candidate loop contracts
+.TP
 \fB\-\-object\-bits\fR n
 number of bits used for object addresses
 .TP

regression/goto-synthesizer/address_space_size_limit/test_cbmc_cmd.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check _ --cbmc-cmd 'cbmc --object-bits 1'
+too many addressed objects
+^EXIT=6$
+^SIGNAL=0$
+--
+Check if the synthesizer can correctly set object bits when calling CBMC.

src/goto-synthesizer/goto_synthesizer_parse_options.cpp

@@ -14,14 +14,19 @@ Author: Qinheping Hu
 
 #include <goto-programs/read_goto_binary.h>
 #include <goto-programs/set_properties.h>
+#include <goto-programs/show_goto_functions.h>
+#include <goto-programs/show_properties.h>
 #include <goto-programs/write_goto_binary.h>
 
 #include <ansi-c/gcc_version.h>
+#include <cbmc/cbmc_parse_options.h>
 #include <goto-instrument/contracts/contracts.h>
 #include <goto-instrument/nondet_volatile.h>
+#include <goto-instrument/reachability_slicer.h>
 
 #include "enumerative_loop_contracts_synthesizer.h"
 
+#include <cstring>
 #include <fstream>
 #include <iostream>
 
@@ -61,8 +66,49 @@ int goto_synthesizer_parse_optionst::doit()
     configure_gcc(gcc_version);
   }
 
-  // Get options and preprocess `goto_model`.
-  const auto &options = get_options();
+  optionalt<cmdlinet> cbmc_cmdline;
+  if(cmdline.isset("cbmc-cmd"))
+  {
+    std::string cbmc_cmdline_str = cmdline.get_value("cbmc-cmd");
+
+    // Tokenize cbmc_cmdline_str
+    std::vector<char *> cbmc_args;
+    std::istringstream iss(cbmc_cmdline_str);
+    std::string token;
+    while(iss >> token)
+    {
+      char *cbmc_arg = new char[token.size() + 1];
+      copy(token.begin(), token.end(), cbmc_arg);
+      cbmc_arg[token.size()] = '\0';
+      cbmc_args.push_back(cbmc_arg);
+    }
+
+    // cbmc-cmd must starts with `cbmc`
+    if(strcmp(cbmc_args[0], "cbmc") != 0)
+    {
+      throw invalid_command_line_argument_exceptiont(
+        "cbmc-cmd must starts with cbmc, e.g., --cbmc-cmd \"cbmc [args]\"",
+        "--cbmc-cmd");
+    }
+
+    // Parse cbmc_cmdline.
+    cmdlinet tmp_cmdline;
+    cbmc_cmdline = tmp_cmdline;
+    cbmc_cmdline.value().parse(
+      cbmc_args.size(),
+      const_cast<const char **>(&cbmc_args[0]),
+      (std::string("?h(help)") + CBMC_OPTIONS).c_str());
+
+    std::cout << cbmc_args.size() << "\n";
+    for(int i = 0; i < cbmc_args.size(); i++)
+      std::cout << cbmc_args[i] << "\n";
+
+    for(size_t i = 0; i < cbmc_args.size(); i++)
+      delete[] cbmc_args[i];
+  }
+
+  // Get options for the backend verifier.
+  const auto &options = get_options(cbmc_cmdline);
 
   // Synthesize loop invariants and annotate them into `goto_model`
   enumerative_loop_contracts_synthesizert synthesizer(goto_model, options, log);
@@ -180,7 +226,8 @@ int goto_synthesizer_parse_optionst::get_goto_program()
   return CPROVER_EXIT_SUCCESS;
 }
 
-optionst goto_synthesizer_parse_optionst::get_options()
+optionst goto_synthesizer_parse_optionst::get_options(
+  const optionalt<cmdlinet> &cbmc_cmdline)
 {
   optionst options;
 
@@ -204,15 +251,27 @@ optionst goto_synthesizer_parse_optionst::get_options()
   options.set_option("self-loops-to-assumptions", true);
 
   options.set_option("arrays-uf", "auto");
-  if(cmdline.isset("arrays-uf-always"))
+  if(
+    cmdline.isset("arrays-uf-always") ||
+    (cbmc_cmdline.has_value() &&
+     cbmc_cmdline.value().isset("arrays-uf-always")))
+  {
     options.set_option("arrays-uf", "always");
-  else if(cmdline.isset("arrays-uf-never"))
+  }
+  else if(
+    cmdline.isset("arrays-uf-never") ||
+    (cbmc_cmdline.has_value() && cbmc_cmdline.value().isset("arrays-uf-never")))
+  {
     options.set_option("arrays-uf", "never");
+  }
 
   // Generating trace for counterexamples.
   options.set_option("trace", true);
 
   parse_solver_options(cmdline, options);
+  // Also set options specified in `cbmc_cmdline`.
+  if(cbmc_cmdline.has_value())
+    parse_solver_options(cbmc_cmdline.value(), options);
 
   return options;
 }
@@ -237,8 +296,9 @@ void goto_synthesizer_parse_optionst::help()
     "\n"
     "Main options:\n" HELP_DUMP_LOOP_CONTRACTS HELP_LOOP_CONTRACTS_NO_UNWIND
     "\n"
-    "Backend options:\n" HELP_CONFIG_BACKEND HELP_SOLVER
-    "\n"
+    "Backend options:\n"
+    " {y--cbmc-cmd} {ucmd} \t command used to run cbmc to check candidate loop "
+    "contracts\n" HELP_CONFIG_BACKEND HELP_SOLVER
     " {y--arrays-uf-never} \t never turn arrays into uninterpreted functions\n"
     " {y--arrays-uf-always} \t always turn arrays into uninterpreted"
     " functions\n"

src/goto-synthesizer/goto_synthesizer_parse_options.h

@@ -24,6 +24,7 @@ Author: Qinheping Hu
 #define GOTO_SYNTHESIZER_OPTIONS \
   OPT_DUMP_LOOP_CONTRACTS \
   "(" FLAG_LOOP_CONTRACTS_NO_UNWIND ")" \
+  "(cbmc-cmd):" \
   OPT_CONFIG_BACKEND \
   OPT_SOLVER \
   "(arrays-uf-always)(arrays-uf-never)" \
@@ -54,7 +55,8 @@ class goto_synthesizer_parse_optionst : public parse_options_baset
 
   // Get the options same as using CBMC api without any flags and set any
   // options specified in the command line.
-  optionst get_options();
+  // Also set options that are specified in `cbmc_cmdline`.
+  optionst get_options(const optionalt<cmdlinet> &cbmc_cmdline);
 
   goto_modelt goto_model;
 };

src/goto-synthesizer/module_dependencies.txt

@@ -1,6 +1,7 @@
 analyses
 ansi-c
 assembler
+cbmc
 cpp
 goto-checker
 goto-instrument