CONTRACTS: Add --dfcc switch to the goto-instrument CLI interface

parse_options fix format

Author: Remi Delmas

doc/man/goto-instrument.1

@@ -1003,6 +1003,12 @@ replace calls to \fIfun\fR with \fIfun\fR's contract
 .TP
 \fB\-\-enforce\-contract\fR \fIfun\fR
 wrap \fIfun\fR with an assertion of its contract
+.TP
+\fB\-\-enforce\-contract\-rec\fR \fIfun\fR
+wrap \fIfun\fR with an assertion of its contract that can handle recursive calls
+.TP
+\fB\-\-dfcc\fR \fIfun\fR
+instrument dynamic frame condition checks method using \fIfun\fR as entry point
 .SS "User-interface options:"
 .TP
 \fB\-\-flush\fR

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1157,9 +1157,71 @@ void goto_instrument_parse_optionst::instrument_goto_program()
     annotate_invariants(synthesizer.synthesize_all(), goto_model, log);
   }
 
+  bool use_dfcc = false;
+  if(cmdline.isset(FLAG_DFCC))
+  {
+    use_dfcc = true;
+
+    if(cmdline.get_values(FLAG_DFCC).size() != 1)
+    {
+      log.error() << "Only a single --" << FLAG_DFCC << " is allowed"
+                  << messaget::eom;
+      throw 0;
+    }
+
+    if(cmdline.isset(FLAG_LOOP_CONTRACTS))
+    {
+      log.error() << " The combination of " << FLAG_DFCC << " and "
+                  << FLAG_LOOP_CONTRACTS << " is not yet supported"
+                  << messaget::eom;
+      throw 0;
+    }
+
+    do_indirect_call_and_rtti_removal();
+
+    const std::string &harness_id = *cmdline.get_values(FLAG_DFCC).begin();
+
+    std::set<std::string> to_replace(
+      cmdline.get_values(FLAG_REPLACE_CALL).begin(),
+      cmdline.get_values(FLAG_REPLACE_CALL).end());
+
+    if(
+      !cmdline.get_values(FLAG_ENFORCE_CONTRACT).empty() &&
+      !cmdline.get_values(FLAG_ENFORCE_CONTRACT_REC).empty())
+    {
+      log.error() << "--" << FLAG_ENFORCE_CONTRACT << " and --"
+                  << FLAG_ENFORCE_CONTRACT_REC << " are mutually exclusive"
+                  << messaget::eom;
+      throw 0;
+    }
+
+    auto &to_enforce = !cmdline.get_values(FLAG_ENFORCE_CONTRACT_REC).empty()
+                         ? cmdline.get_values(FLAG_ENFORCE_CONTRACT_REC)
+                         : cmdline.get_values(FLAG_ENFORCE_CONTRACT);
+
+    bool allow_recursive_calls =
+      !cmdline.get_values(FLAG_ENFORCE_CONTRACT_REC).empty();
+    std::set<std::string> to_check(to_enforce.begin(), to_enforce.end());
+
+    std::set<std::string> to_exclude_from_nondet_static(
+      cmdline.get_values("nondet-static-exclude").begin(),
+      cmdline.get_values("nondet-static-exclude").end());
+
+    dfcc(
+      goto_model,
+      harness_id,
+      to_check,
+      allow_recursive_calls,
+      to_replace,
+      false,
+      to_exclude_from_nondet_static,
+      log);
+  }
+
   if(
-    cmdline.isset(FLAG_LOOP_CONTRACTS) || cmdline.isset(FLAG_REPLACE_CALL) ||
-    cmdline.isset(FLAG_ENFORCE_CONTRACT))
+    !use_dfcc &&
+    (cmdline.isset(FLAG_LOOP_CONTRACTS) || cmdline.isset(FLAG_REPLACE_CALL) ||
+     cmdline.isset(FLAG_ENFORCE_CONTRACT)))
   {
     do_indirect_call_and_rtti_removal();
     code_contractst contracts(goto_model, log);
@@ -1911,10 +1973,12 @@ void goto_instrument_parse_optionst::help()
     "                             force aggressive slicer to preserve all direct paths\n" // NOLINT(*)
     "\n"
     "Code contracts:\n"
+    HELP_DFCC
     HELP_LOOP_CONTRACTS
     HELP_LOOP_INVARIANT_SYNTHESIZER
     HELP_REPLACE_CALL
     HELP_ENFORCE_CONTRACT
+    HELP_ENFORCE_CONTRACT_REC
     "\n"
     "User-interface options:\n"
     HELP_FLUSH

src/goto-instrument/goto_instrument_parse_options.h

@@ -41,6 +41,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "unwindset.h"
 
 #include "contracts/contracts.h"
+#include "contracts/dynamic-frames/dfcc.h"
 #include "synthesizer/enumerative_loop_invariant_synthesizer.h"
 #include "wmm/weak_memory.h"
 
@@ -95,9 +96,11 @@ Author: Daniel Kroening, kroening@kroening.com
   "(list-symbols)(list-undefined-functions)" \
   "(z3)(add-library)(show-dependence-graph)" \
   "(horn)(skip-loops):(model-argc-argv):" \
+  OPT_DFCC \
   "(" FLAG_LOOP_CONTRACTS ")" \
   "(" FLAG_REPLACE_CALL "):" \
   "(" FLAG_ENFORCE_CONTRACT "):" \
+  OPT_ENFORCE_CONTRACT_REC \
   "(show-threaded)(list-calls-args)" \
   "(undefined-function-is-assume-false)" \
   "(remove-function-body):"\