Merge pull request #3796 from peterschrammel/stop-on-fail-verifier

Stop-on-fail verifier [blocks: 3968]

Author: tautschnig

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -19,16 +19,18 @@ Author: Daniel Kroening, [email protected]
 #include <util/config.h>
 #include <util/exit_codes.h>
 #include <util/invariant.h>
+#include <util/make_unique.h>
 #include <util/unicode.h>
-#include <util/xml.h>
 #include <util/version.h>
+#include <util/xml.h>
 
 #include <langapi/language.h>
 
 #include <ansi-c/ansi_c_language.h>
 
 #include <goto-checker/all_properties_verifier.h>
 #include <goto-checker/all_properties_verifier_with_trace_storage.h>
+#include <goto-checker/stop_on_fail_verifier.h>
 
 #include <goto-programs/adjust_float_expressions.h>
 #include <goto-programs/lazy_goto_model.h>
@@ -566,11 +568,33 @@ int jbmc_parse_optionst::doit()
       }
     }
 
+    if(
+      options.get_bool_option("dimacs") ||
+      !options.get_option("outfile").empty())
+    {
+      if(!options.get_bool_option("paths"))
+      {
+        stop_on_fail_verifiert<multi_path_symex_checkert> verifier(
+          options, ui_message_handler, goto_model);
+        (void)verifier();
+        return CPROVER_EXIT_SUCCESS;
+      }
+    }
+
     std::unique_ptr<goto_verifiert> verifier = nullptr;
 
-    if(!options.get_bool_option("paths") && !options.is_set("cover"))
+    if(
+      !options.get_bool_option("paths") && !options.is_set("cover") &&
+      !options.get_bool_option("dimacs") &&
+      options.get_option("outfile").empty())
     {
-      if(!options.get_bool_option("stop-on-fail"))
+      if(options.get_bool_option("stop-on-fail"))
+      {
+        verifier = util_make_unique<
+          stop_on_fail_verifiert<java_multi_path_symex_checkert>>(
+          options, ui_message_handler, goto_model);
+      }
+      else
       {
         verifier = util_make_unique<all_properties_verifier_with_trace_storaget<
           java_multi_path_symex_checkert>>(

src/cbmc/cbmc_parse_options.cpp

@@ -20,6 +20,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/exception_utils.h>
 #include <util/exit_codes.h>
 #include <util/invariant.h>
+#include <util/make_unique.h>
 #include <util/unicode.h>
 #include <util/version.h>
 
@@ -38,6 +39,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-checker/multi_path_symex_checker.h>
 #include <goto-checker/multi_path_symex_only_checker.h>
 #include <goto-checker/properties.h>
+#include <goto-checker/stop_on_fail_verifier.h>
 
 #include <goto-programs/adjust_float_expressions.h>
 #include <goto-programs/initialize_goto_model.h>
@@ -564,11 +566,31 @@ int cbmc_parse_optionst::doit()
     }
   }
 
+  if(
+    options.get_bool_option("dimacs") || !options.get_option("outfile").empty())
+  {
+    if(!options.get_bool_option("paths"))
+    {
+      stop_on_fail_verifiert<multi_path_symex_checkert> verifier(
+        options, ui_message_handler, goto_model);
+      (void)verifier();
+      return CPROVER_EXIT_SUCCESS;
+    }
+  }
+
   std::unique_ptr<goto_verifiert> verifier = nullptr;
 
-  if(!options.get_bool_option("paths") && !options.is_set("cover"))
+  if(
+    !options.get_bool_option("paths") && !options.is_set("cover") &&
+    !options.get_bool_option("dimacs") && options.get_option("outfile").empty())
   {
-    if(!options.get_bool_option("stop-on-fail"))
+    if(options.get_bool_option("stop-on-fail"))
+    {
+      verifier =
+        util_make_unique<stop_on_fail_verifiert<multi_path_symex_checkert>>(
+          options, ui_message_handler, goto_model);
+    }
+    else
     {
       verifier = util_make_unique<
         all_properties_verifier_with_trace_storaget<multi_path_symex_checkert>>(

src/goto-checker/README.md

@@ -51,6 +51,9 @@ The combination of these three concepts enables:
   without impacting others.
 
 There are the following variants of goto verifiers at the moment:
+* \ref stop_on_fail_verifiert : Checks all properties, but terminates
+  as soon as the first violated property is found and reports this violation.
+  A trace ends at a violated property.
 * \ref all_properties_verifier_with_trace_storaget : Determines the status of
   all properties and outputs results when the verification algorithm has
   terminated. A trace ends at a violated property.

src/goto-checker/stop_on_fail_verifier.h

@@ -0,0 +1,79 @@
+/*******************************************************************\
+
+Module: Goto Verifier for stopping at the first failing property
+
+Author: Daniel Kroening, Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// Goto Verifier for stopping at the first failing property
+
+#ifndef CPROVER_GOTO_CHECKER_STOP_ON_FAIL_VERIFIER_H
+#define CPROVER_GOTO_CHECKER_STOP_ON_FAIL_VERIFIER_H
+
+#include "bmc_util.h"
+#include "goto_verifier.h"
+
+/// Stops when the first failing property is found.
+/// Requires an incremental goto checker that is a
+/// `goto_trace_providert` and `witness_providert`.
+template <class incremental_goto_checkerT>
+class stop_on_fail_verifiert : public goto_verifiert
+{
+public:
+  stop_on_fail_verifiert(
+    const optionst &options,
+    ui_message_handlert &ui_message_handler,
+    abstract_goto_modelt &goto_model)
+    : goto_verifiert(options, ui_message_handler),
+      goto_model(goto_model),
+      incremental_goto_checker(options, ui_message_handler, goto_model)
+  {
+    properties = std::move(initialize_properties(goto_model));
+  }
+
+  resultt operator()() override
+  {
+    (void)incremental_goto_checker(properties);
+    return determine_result(properties);
+  }
+
+  void report() override
+  {
+    switch(determine_result(properties))
+    {
+    case resultt::PASS:
+      report_success(ui_message_handler);
+      incremental_goto_checker.output_proof();
+      break;
+
+    case resultt::FAIL:
+    {
+      goto_tracet goto_trace = incremental_goto_checker.build_trace();
+      output_error_trace(
+        goto_trace,
+        incremental_goto_checker.get_namespace(),
+        trace_optionst(options),
+        ui_message_handler);
+      report_failure(ui_message_handler);
+      incremental_goto_checker.output_error_witness(goto_trace);
+      break;
+    }
+
+    case resultt::UNKNOWN:
+      report_inconclusive(ui_message_handler);
+      break;
+
+    case resultt::ERROR:
+      report_error(ui_message_handler);
+      break;
+    }
+  }
+
+protected:
+  abstract_goto_modelt &goto_model;
+  incremental_goto_checkerT incremental_goto_checker;
+};
+
+#endif // CPROVER_GOTO_CHECKER_STOP_ON_FAIL_VERIFIER_H